BT005B · Bertrand theorem

beta_exclusive_recode_invariant_step

Stable checked-use theorem · independently kernel verified

Combine modulus-product and cross-base congruence updates for an exclusive prefix.

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

∀ N. ∀ c. ∀ b. ∀ e. ∀ k. ∀ P. ∀ z. (∀ x. (∃ y. S x + S y = S N) → Dvd(S x,c)) → Lt(k,N) → ¬P = 0 → (∀ x. Lt(x,k) → Dvd(S (S x · c),P)) → (∀ x. ∀ y. Lt(x,k) → BetaAt(b,e,x,y) → ModEq(S (S x · c),z,y)) → (∀ x. Le(k,x) → Le(x,N) → Coprime(P,S (S x · c))) → ∃ x. ¬P · S (S k · c) = 0 ∧ ((∀ y. Lt(y,S k) → Dvd(S (S y · c),P · S (S k · c))) ∧ ((∀ y. ∀ n. Lt(y,S k) → BetaAt(b,e,y,n) → ModEq(S (S y · c),x,n)) ∧ (∀ y. Lt(k,y) → Le(y,N) → Coprime(P · S (S k · c),S (S y · c)))))

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

PD0001 Le PD0002 Lt PD0003 Dvd PD0005 Coprime PD0008 ModEq PD0013 BetaAt

18 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0003 Dvd PD0005 Coprime PD0008 ModEq PD0013 BetaAt

8 occurrences

Exact expanded native-PA statement
forall N c b e k P z. (forall t. (exists h. S t + S h = S N) -> exists q. c = S t * q) -> (exists h. h + S k = N) -> ~(P = 0) -> (forall i. (exists h. h + S i = k) -> exists q. P = S ((S i) * c) * q) -> (forall i a. (exists h. h + S i = k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z + S ((S i) * c) * u = a + S ((S i) * c) * v) -> (forall j. (exists g. g + k = j) -> (exists h. h + j = N) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1) -> exists z2. (~(P * S ((S k) * c) = 0) /\ ((forall i. (exists h. h + S i = S k) -> exists q. P * S ((S k) * c) = S ((S i) * c) * q) /\ ((forall i a. (exists h. h + S i = S k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z2 + S ((S i) * c) * u = a + S ((S i) * c) * v) /\ forall j. (exists g. g + S k = j) -> (exists h. h + j = N) -> forall d. (exists u. P * S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1)))

Proof neighborhood

Direct theorem prerequisites

BT0059 beta_exclusive_accumulated_product_step BT005A beta_exclusive_recode_congruence_step

Direct theorem dependents

BT005C bounded_beta_exclusive_recode_invariant

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

49 script commands · 14 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 (2)
beta exclusive accumulated product stepbeta exclusive recode congruence step
01Fix variables and assumptionsL1–10

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

  1. L1
    intro N
  2. L2
    intro c
  3. L3
    intro b
  4. L4
    intro e
  5. L5
    intro k
  6. L6
    intro P
  7. L7
    intro z
  8. L8
    intro hcm
  9. L9
    intro hkN
  10. L10
    intro hP
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hdiv
  2. L12
    intro hcong
  3. L13
    intro hfuture
03Establish hproductL14–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta exclusive accumulated product step.

  1. L14
    have hproduct : ¬P · S (S k · c) = 0 ∧ ((∀ x. Lt(x,S k) → Dvd(S (S x · c),P · S (S k · c))) ∧ (∀ x. Lt(k,x) → Le(x,N) → Coprime(P · S (S k · c),S (S x · c))))Definitions: Lt(x,S k)Dvd(S (S x · c),P · S (S k · c))Lt(k,x)Le(x,N)Coprime(P · S (S k · c),S (S x · c))Original native command in the exact edition
  2. L15
    specialize beta_exclusive_accumulated_product_step N
  3. L16
    specialize beta_exclusive_accumulated_product_step c
  4. L17
    specialize beta_exclusive_accumulated_product_step k
  5. L18
    specialize beta_exclusive_accumulated_product_step P
  6. L19
    apply beta_exclusive_accumulated_product_step
  7. L20
    exact hcm
  8. L21
    exact hkN
  9. L22
    exact hP
  10. L23
    exact hdiv
04Use earlier factsL24–24

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

  1. L24
    exact hfuture
05Establish hcodesL25–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta exclusive recode congruence step.

  1. L25
    have hcodes : ∃ z2. ∀ i. ∀ a. Lt(i,S k) → BetaAt(b,e,i,a) → ModEq(S (S i · c),z2,a)Definitions: Lt(i,S k)BetaAt(b,e,i,a)ModEq(S (S i · c),z2,a)Original native command in the exact edition
  2. L26
    specialize beta_exclusive_recode_congruence_step N
  3. L27
    specialize beta_exclusive_recode_congruence_step c
  4. L28
    specialize beta_exclusive_recode_congruence_step b
  5. L29
    specialize beta_exclusive_recode_congruence_step e
  6. L30
    specialize beta_exclusive_recode_congruence_step k
  7. L31
    specialize beta_exclusive_recode_congruence_step P
  8. L32
    specialize beta_exclusive_recode_congruence_step z
  9. L33
    apply beta_exclusive_recode_congruence_step
  10. L34
    exact hkN
06Use earlier factsL35–38

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

  1. L35
    exact hP
  2. L36
    exact hdiv
  3. L37
    exact hcong
  4. L38
    exact hfuture
07Separate the logical casesL39–41

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

  1. L39
    cases hcodes
  2. L40
    cases hproduct
  3. L41
    cases hproduct_right
08Construct an explicit witnessL42–42

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

  1. L42
    exists x
09Separate the logical casesL43–43

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

  1. L43
    split
10Use earlier factsL44–44

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

  1. L44
    exact hproduct_left
11Separate the logical casesL45–45

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

  1. L45
    split
12Use earlier factsL46–46

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

  1. L46
    exact hproduct_right_left
13Separate the logical casesL47–47

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

  1. L47
    split
14Use earlier factsL48–49

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

  1. L48
    exact hcodes_witness
  2. L49
    exact hproduct_right_right

Library-wide reading audit

Original defined command ledger · 49 lines
  1. 0001intro N
  2. 0002intro c
  3. 0003intro b
  4. 0004intro e
  5. 0005intro k
  6. 0006intro P
  7. 0007intro z
  8. 0008intro hcm
  9. 0009intro hkN
  10. 0010intro hP
  11. 0011intro hdiv
  12. 0012intro hcong
  13. 0013intro hfuture
  14. 0014have hproduct : ¬P · S (S k · c) = 0 ∧ ((∀ x. Lt(x,S k) → Dvd(S (S x · c),P · S (S k · c))) ∧ (∀ x. Lt(k,x) → Le(x,N) → Coprime(P · S (S k · c),S (S x · c))))
    Exact native replay linehave hproduct : (~(P * S ((S k) * c) = 0) /\ ((forall i. (exists h. h + S i = S k) -> exists q. P * S ((S k) * c) = S ((S i) * c) * q) /\ forall j. (exists g. g + S k = j) -> (exists h. h + j = N) -> forall d. (exists u. P * S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1))
  15. 0015specialize beta_exclusive_accumulated_product_step N
  16. 0016specialize beta_exclusive_accumulated_product_step c
  17. 0017specialize beta_exclusive_accumulated_product_step k
  18. 0018specialize beta_exclusive_accumulated_product_step P
  19. 0019apply beta_exclusive_accumulated_product_step
  20. 0020exact hcm
  21. 0021exact hkN
  22. 0022exact hP
  23. 0023exact hdiv
  24. 0024exact hfuture
  25. 0025have hcodes : ∃ z2. ∀ i. ∀ a. Lt(i,S k) → BetaAt(b,e,i,a) → ModEq(S (S i · c),z2,a)
    Exact native replay linehave hcodes : exists z2. forall i a. (exists h. h + S i = S k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z2 + S ((S i) * c) * u = a + S ((S i) * c) * v
  26. 0026specialize beta_exclusive_recode_congruence_step N
  27. 0027specialize beta_exclusive_recode_congruence_step c
  28. 0028specialize beta_exclusive_recode_congruence_step b
  29. 0029specialize beta_exclusive_recode_congruence_step e
  30. 0030specialize beta_exclusive_recode_congruence_step k
  31. 0031specialize beta_exclusive_recode_congruence_step P
  32. 0032specialize beta_exclusive_recode_congruence_step z
  33. 0033apply beta_exclusive_recode_congruence_step
  34. 0034exact hkN
  35. 0035exact hP
  36. 0036exact hdiv
  37. 0037exact hcong
  38. 0038exact hfuture
  39. 0039cases hcodes
  40. 0040cases hproduct
  41. 0041cases hproduct_right
  42. 0042exists x
  43. 0043split
  44. 0044exact hproduct_left
  45. 0045split
  46. 0046exact hproduct_right_left
  47. 0047split
  48. 0048exact hcodes_witness
  49. 0049exact hproduct_right_right