BT005C · Bertrand theorem

bounded_beta_exclusive_recode_invariant

Stable checked-use theorem · independently kernel verified

Fold an empty-based, exclusive beta prefix into another base with append readiness.

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. (∀ x. (∃ y. S x + S y = S N) → Dvd(S x,c)) → ∀ x. Le(x,N) → ∃ y. ∃ z. ¬y = 0 ∧ ((∀ n. Lt(n,x) → Dvd(S (S n · c),y)) ∧ ((∀ n. ∀ m. Lt(n,x) → BetaAt(b,e,n,m) → ModEq(S (S n · c),z,m)) ∧ (∀ n. Le(x,n) → Le(n,N) → Coprime(y,S (S n · 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

10 occurrences

In local proof propositions

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

18 occurrences

Exact expanded native-PA statement
forall N c b e. (forall t. (exists h. S t + S h = S N) -> exists q. c = S t * q) -> forall k. (exists h. h + k = N) -> exists P z. (~(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)))

Proof neighborhood

Direct theorem prerequisites

BT000C succ_ne_zero BT000L add_eq_zero_right BT002Y coprime_one_left BT000X le_succ_self BT000F le_trans BT005B beta_exclusive_recode_invariant_step

Direct theorem dependents

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

89 script commands · 25 reading checkpoints · 6 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 (6)
succ ne zeroadd eq zero rightcoprime one leftle succ selfle transbeta exclusive recode invariant step
01Fix variables and assumptionsL1–5

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 hcm
02Induction on kL6–7

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L6
    induction k
  2. L7
    intro hkN
03Construct an explicit witnessL8–9

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

  1. L8
    exists 1
  2. L9
    exists 0
04Separate the logical casesL10–10

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

  1. L10
    split
05Use earlier factsL11–12

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

  1. L11
    specialize succ_ne_zero 0
  2. L12
    exact succ_ne_zero
06Separate the logical casesL13–13

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

  1. L13
    split
07Fix variables and assumptionsL14–15

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

  1. L14
    intro i
  2. L15
    intro hi
08Separate the logical casesL16–17

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

  1. L16
    exfalso
  2. L17
    cases hi
09Establish hsi0L18–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L18
    have hsi0 : S i = 0
  2. L19
    specialize add_eq_zero_right x
  3. L20
    specialize add_eq_zero_right (S i)
  4. L21
    apply add_eq_zero_right
  5. L22
    exact hi_witness
  6. L23
    specialize succ_ne_zero i
  7. L24
    apply succ_ne_zero
  8. L25
    exact hsi0
10Separate the logical casesL26–26

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

  1. L26
    split
11Fix variables and assumptionsL27–30

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

  1. L27
    intro i
  2. L28
    intro a
  3. L29
    intro hi
  4. L30
    intro hati
12Separate the logical casesL31–32

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

  1. L31
    exfalso
  2. L32
    cases hi
13Establish hsi0L33–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L33
    have hsi0 : S i = 0
  2. L34
    specialize add_eq_zero_right x
  3. L35
    specialize add_eq_zero_right (S i)
  4. L36
    apply add_eq_zero_right
  5. L37
    exact hi_witness
  6. L38
    specialize succ_ne_zero i
  7. L39
    apply succ_ne_zero
  8. L40
    exact hsi0
  9. L41
    intro j
  10. L42
    intro h0j
14Fix variables and assumptionsL43–46

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

  1. L43
    intro hjN
  2. L44
    intro d
  3. L45
    intro h1
  4. L46
    intro hm
15Use earlier factsL47–51

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

  1. L47
    specialize coprime_one_left (S ((S j) * c))
  2. L48
    specialize coprime_one_left d
  3. L49
    apply coprime_one_left
  4. L50
    exact h1
  5. L51
    exact hm
16Fix variables and assumptionsL52–52

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

  1. L52
    intro hkN
17Establish hkprevL53–53

Establish this local claim before using it. It is not an additional assumption.

  1. L53
    have hkprev : Le(k,N)Definitions: Le(k,N)Original native command in the exact edition
18Establish hkstepL54–62

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

  1. L54
    have hkstep : Le(k,S k)Definitions: Le(k,S k)Original native command in the exact edition
  2. L55
    specialize le_succ_self k
  3. L56
    exact le_succ_self
  4. L57
    specialize le_trans k
  5. L58
    specialize le_trans (S k)
  6. L59
    specialize le_trans N
  7. L60
    apply le_trans
  8. L61
    exact hkstep
  9. L62
    exact hkN
19Establish hprevL63–65

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

  1. L63
    have hprev : ∃ P. ∃ z. ¬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)))))Definitions: Lt(x,k)Dvd(S (S x · c),P)BetaAt(b,e,x,y)ModEq(S (S x · c),z,y)Le(k,x)Le(x,N)Coprime(P,S (S x · c))Original native command in the exact edition
  2. L64
    apply IH
  3. L65
    exact hkprev
20Separate the logical casesL66–70

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

  1. L66
    cases hprev
  2. L67
    cases hprev_witness
  3. L68
    cases hprev_witness_witness
  4. L69
    cases hprev_witness_witness_right
  5. L70
    cases hprev_witness_witness_right_right
21Establish hnextL71–80

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

  1. L71
    have hnext : ∃ z2. ¬x · S (S k · c) = 0 ∧ ((∀ y. Lt(y,S k) → Dvd(S (S y · c),x · S (S k · c))) ∧ ((∀ y. ∀ z. Lt(y,S k) → BetaAt(b,e,y,z) → ModEq(S (S y · c),z2,z)) ∧ (∀ y. Lt(k,y) → Le(y,N) → Coprime(x · S (S k · c),S (S y · c)))))Definitions: Lt(y,S k)Dvd(S (S y · c),x · S (S k · c))BetaAt(b,e,y,z)ModEq(S (S y · c),z2,z)Lt(k,y)Le(y,N)Coprime(x · S (S k · c),S (S y · c))Original native command in the exact edition
  2. L72
    specialize beta_exclusive_recode_invariant_step N
  3. L73
    specialize beta_exclusive_recode_invariant_step c
  4. L74
    specialize beta_exclusive_recode_invariant_step b
  5. L75
    specialize beta_exclusive_recode_invariant_step e
  6. L76
    specialize beta_exclusive_recode_invariant_step k
  7. L77
    specialize beta_exclusive_recode_invariant_step x
  8. L78
    specialize beta_exclusive_recode_invariant_step x1
  9. L79
    apply beta_exclusive_recode_invariant_step
  10. L80
    exact hcm
22Use earlier factsL81–85

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

  1. L81
    exact hkN
  2. L82
    exact hprev_witness_witness_left
  3. L83
    exact hprev_witness_witness_right_left
  4. L84
    exact hprev_witness_witness_right_right_left
  5. L85
    exact hprev_witness_witness_right_right_right
23Separate the logical casesL86–86

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

  1. L86
    cases hnext
24Construct an explicit witnessL87–88

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

  1. L87
    exists x * S ((S k) * c)
  2. L88
    exists x2
25Use earlier factsL89–89

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

  1. L89
    exact hnext_witness

Library-wide reading audit

Original defined command ledger · 89 lines
  1. 0001intro N
  2. 0002intro c
  3. 0003intro b
  4. 0004intro e
  5. 0005intro hcm
  6. 0006induction k
  7. 0007intro hkN
  8. 0008exists 1
  9. 0009exists 0
  10. 0010split
  11. 0011specialize succ_ne_zero 0
  12. 0012exact succ_ne_zero
  13. 0013split
  14. 0014intro i
  15. 0015intro hi
  16. 0016exfalso
  17. 0017cases hi
  18. 0018have hsi0 : S i = 0
  19. 0019specialize add_eq_zero_right x
  20. 0020specialize add_eq_zero_right (S i)
  21. 0021apply add_eq_zero_right
  22. 0022exact hi_witness
  23. 0023specialize succ_ne_zero i
  24. 0024apply succ_ne_zero
  25. 0025exact hsi0
  26. 0026split
  27. 0027intro i
  28. 0028intro a
  29. 0029intro hi
  30. 0030intro hati
  31. 0031exfalso
  32. 0032cases hi
  33. 0033have hsi0 : S i = 0
  34. 0034specialize add_eq_zero_right x
  35. 0035specialize add_eq_zero_right (S i)
  36. 0036apply add_eq_zero_right
  37. 0037exact hi_witness
  38. 0038specialize succ_ne_zero i
  39. 0039apply succ_ne_zero
  40. 0040exact hsi0
  41. 0041intro j
  42. 0042intro h0j
  43. 0043intro hjN
  44. 0044intro d
  45. 0045intro h1
  46. 0046intro hm
  47. 0047specialize coprime_one_left (S ((S j) * c))
  48. 0048specialize coprime_one_left d
  49. 0049apply coprime_one_left
  50. 0050exact h1
  51. 0051exact hm
  52. 0052intro hkN
  53. 0053have hkprev : Le(k,N)
    Exact native replay linehave hkprev : exists h. h + k = N
  54. 0054have hkstep : Le(k,S k)
    Exact native replay linehave hkstep : exists h. h + k = S k
  55. 0055specialize le_succ_self k
  56. 0056exact le_succ_self
  57. 0057specialize le_trans k
  58. 0058specialize le_trans (S k)
  59. 0059specialize le_trans N
  60. 0060apply le_trans
  61. 0061exact hkstep
  62. 0062exact hkN
  63. 0063have hprev : ∃ P. ∃ z. ¬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)))))
    Exact native replay linehave hprev : exists P z. (~(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)))
  64. 0064apply IH
  65. 0065exact hkprev
  66. 0066cases hprev
  67. 0067cases hprev_witness
  68. 0068cases hprev_witness_witness
  69. 0069cases hprev_witness_witness_right
  70. 0070cases hprev_witness_witness_right_right
  71. 0071have hnext : ∃ z2. ¬x · S (S k · c) = 0 ∧ ((∀ y. Lt(y,S k) → Dvd(S (S y · c),x · S (S k · c))) ∧ ((∀ y. ∀ z. Lt(y,S k) → BetaAt(b,e,y,z) → ModEq(S (S y · c),z2,z)) ∧ (∀ y. Lt(k,y) → Le(y,N) → Coprime(x · S (S k · c),S (S y · c)))))
    Exact native replay linehave hnext : exists z2. (~(x * S ((S k) * c) = 0) /\ ((forall i. (exists h. h + S i = S k) -> exists q. x * 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. x * S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1)))
  72. 0072specialize beta_exclusive_recode_invariant_step N
  73. 0073specialize beta_exclusive_recode_invariant_step c
  74. 0074specialize beta_exclusive_recode_invariant_step b
  75. 0075specialize beta_exclusive_recode_invariant_step e
  76. 0076specialize beta_exclusive_recode_invariant_step k
  77. 0077specialize beta_exclusive_recode_invariant_step x
  78. 0078specialize beta_exclusive_recode_invariant_step x1
  79. 0079apply beta_exclusive_recode_invariant_step
  80. 0080exact hcm
  81. 0081exact hkN
  82. 0082exact hprev_witness_witness_left
  83. 0083exact hprev_witness_witness_right_left
  84. 0084exact hprev_witness_witness_right_right_left
  85. 0085exact hprev_witness_witness_right_right_right
  86. 0086cases hnext
  87. 0087exists x * S ((S k) * c)
  88. 0088exists x2
  89. 0089exact hnext_witness