BT004U · Bertrand theorem

binary_crt_fold_step

Stable checked-use theorem · independently kernel verified

One binary CRT extension preserves every old congruence whose modulus divides the accumulated product.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ P. ∀ n. ∀ x. ∀ b. ¬P = 0 → ¬n = 0 → Coprime(P,n) → ∃ y. (∀ z. ∀ m. Dvd(z,P) → ModEq(z,x,m) → ModEq(z,y,m)) ∧ ModEq(n,y,b)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0003 Dvd PD0005 Coprime PD0008 ModEq

5 occurrences

In local proof propositions

PD0008 ModEq

3 occurrences

Exact expanded native-PA statement
forall P n x b. ~(P = 0) -> ~(n = 0) -> (forall d. (exists u. P = d * u) -> (exists v. n = d * v) -> d = 1) -> exists z. ((forall m a. (exists k. P = m * k) -> (exists u v. x + m * u = a + m * v) -> exists r s. z + m * r = a + m * s) /\ exists q r. z + n * q = b + n * r)

Proof neighborhood

Direct theorem prerequisites

BT004F binary_crt BT004T mod_eq_of_mod_eq_multiple BT003Q mod_eq_trans

Direct theorem dependents

BT005A beta_exclusive_recode_congruence_step BT005D beta_prefix_extend

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

40 script commands · 8 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
binary crtmod eq of mod eq multiplemod eq trans
01Fix variables and assumptionsL1–7

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro P
  2. L2
    intro n
  3. L3
    intro x
  4. L4
    intro b
  5. L5
    intro hP
  6. L6
    intro hn
  7. L7
    intro hcop
02Establish hcrtL8–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary crt.

  1. L8
    have hcrt : ∃ z. ModEq(P,z,x) ∧ ModEq(n,z,b)Definitions: ModEq(P,z,x)ModEq(n,z,b)Original native command in the exact edition
  2. L9
    specialize binary_crt P
  3. L10
    specialize binary_crt n
  4. L11
    specialize binary_crt x
  5. L12
    specialize binary_crt b
  6. L13
    apply binary_crt
  7. L14
    exact hP
  8. L15
    exact hn
  9. L16
    exact hcop
03Separate the logical casesL17–18

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L17
    cases hcrt
  2. L18
    cases hcrt_witness
04Construct an explicit witnessL19–19

Supply the displayed value, then prove that it has the required property.

  1. L19
    exists x1
05Separate the logical casesL20–20

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L20
    split
06Fix variables and assumptionsL21–24

Work with arbitrary variables or the premises of the current implication.

  1. L21
    intro m
  2. L22
    intro a
  3. L23
    intro hmP
  4. L24
    intro hxa
07Establish hzxL25–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq of mod eq multiple.

  1. L25
  2. L26
    specialize mod_eq_of_mod_eq_multiple m
  3. L27
    specialize mod_eq_of_mod_eq_multiple P
  4. L28
    specialize mod_eq_of_mod_eq_multiple x1
  5. L29
    specialize mod_eq_of_mod_eq_multiple x
  6. L30
    apply mod_eq_of_mod_eq_multiple
  7. L31
    exact hmP
  8. L32
    exact hcrt_witness_left
  9. L33
    specialize mod_eq_trans m
  10. L34
    specialize mod_eq_trans x1
08Use earlier factsL35–40

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L35
    specialize mod_eq_trans x
  2. L36
    specialize mod_eq_trans a
  3. L37
    apply mod_eq_trans
  4. L38
    exact hzx
  5. L39
    exact hxa
  6. L40
    exact hcrt_witness_right

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro P
  2. 0002intro n
  3. 0003intro x
  4. 0004intro b
  5. 0005intro hP
  6. 0006intro hn
  7. 0007intro hcop
  8. 0008have hcrt : ∃ z. ModEq(P,z,x) ∧ ModEq(n,z,b)
    Exact native replay linehave hcrt : exists z. (exists u v. z + P * u = x + P * v) /\ (exists q r. z + n * q = b + n * r)
  9. 0009specialize binary_crt P
  10. 0010specialize binary_crt n
  11. 0011specialize binary_crt x
  12. 0012specialize binary_crt b
  13. 0013apply binary_crt
  14. 0014exact hP
  15. 0015exact hn
  16. 0016exact hcop
  17. 0017cases hcrt
  18. 0018cases hcrt_witness
  19. 0019exists x1
  20. 0020split
  21. 0021intro m
  22. 0022intro a
  23. 0023intro hmP
  24. 0024intro hxa
  25. 0025have hzx : ModEq(m,x1,x)
    Exact native replay linehave hzx : exists u v. x1 + m * u = x + m * v
  26. 0026specialize mod_eq_of_mod_eq_multiple m
  27. 0027specialize mod_eq_of_mod_eq_multiple P
  28. 0028specialize mod_eq_of_mod_eq_multiple x1
  29. 0029specialize mod_eq_of_mod_eq_multiple x
  30. 0030apply mod_eq_of_mod_eq_multiple
  31. 0031exact hmP
  32. 0032exact hcrt_witness_left
  33. 0033specialize mod_eq_trans m
  34. 0034specialize mod_eq_trans x1
  35. 0035specialize mod_eq_trans x
  36. 0036specialize mod_eq_trans a
  37. 0037apply mod_eq_trans
  38. 0038exact hzx
  39. 0039exact hxa
  40. 0040exact hcrt_witness_right