BT005D · Bertrand theorem

beta_prefix_extend

Stable checked-use theorem · independently kernel verified

Rebase an arbitrary decoded prefix and append one exact natural value.

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

∀ k. ∀ b. ∀ e. ∀ s. ∃ z. ∃ c. BetaAt(z,c,k,s) ∧ (∀ x. ∀ y. Lt(x,k) → BetaAt(b,e,x,y) → BetaAt(z,c,x,y))

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

PD0002 Lt PD0013 BetaAt

4 occurrences

In local proof propositions

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

27 occurrences

Exact expanded native-PA statement
forall k b e s. exists z c. (((exists h. h + S s = S ((S k) * c)) /\ exists q. z = q * S ((S k) * c) + s) /\ 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 h. h + S a = S ((S i) * c)) /\ exists q. z = q * S ((S i) * c) + a))

Proof neighborhood

Direct theorem prerequisites

BT004N bounded_common_multiple_exists BT0056 scaled_bounded_common_multiple BT005C bounded_beta_exclusive_recode_invariant BT000E le_refl BT003Y beta_modulus_nonzero BT004U binary_crt_fold_step BT0058 new_value_lt_scaled_base BT0057 beta_value_lt_scaled_base BT0045 beta_at_of_mod_eq_bound

Direct theorem dependents

BT005E beta_prefix_product_trace_exists BT005K beta_product_succ_append BT007V beta_repeat_succ_extend BT0085 beta_range_succ_extend BT0089 beta_prefix_sum_trace_exists BT00S0 prime_power_quotient_prefix_exists BT00SE eisenstein_initial_segment_prefix_extend BT00T2 beta_pascal_zero_row_extend BT00T4 beta_pascal_row_step_extend BT00T6 beta_pascal_table_prefix_extend BT00U7 primorial_factor_prefix_extend BT00UR primorial_interval_factor_prefix_extend BT00XW double_quotient_carry_prefix_extend BT00YP prime_contribution_prefix_extend BT010K prime_contribution_interval_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

105 script commands · 21 reading checkpoints · 10 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 (9)
bounded common multiple existsscaled bounded common multiplebounded beta exclusive recode invariantle reflbeta modulus nonzerobinary crt fold stepnew value lt scaled basebeta value lt scaled basebeta at of mod eq bound
01Fix variables and assumptionsL1–4

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

  1. L1
    intro k
  2. L2
    intro b
  3. L3
    intro e
  4. L4
    intro s
02Establish hCL5–7

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

  1. L5
    have hC : ∃ C. ¬C = 0 ∧ (∀ x. (∃ y. S x + S y = S k) → Dvd(S x,C))Definitions: Dvd(S x,C)Original native command in the exact edition
  2. L6
    specialize bounded_common_multiple_exists k
  3. L7
    exact bounded_common_multiple_exists
03Separate the logical casesL8–9

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

  1. L8
    cases hC
  2. L9
    cases hC_witness
04Establish hcm2L10–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply scaled bounded common multiple.

  1. L10
    have hcm2 : ∀ t. (∃ y. S t + S y = S k) → Dvd(S t,x · S (b + s))Definitions: Dvd(S t,x · S (b + s))Original native command in the exact edition
  2. L11
    specialize scaled_bounded_common_multiple k
  3. L12
    specialize scaled_bounded_common_multiple x
  4. L13
    specialize scaled_bounded_common_multiple (S (b + s))
  5. L14
    apply scaled_bounded_common_multiple
  6. L15
    exact hC_witness_right
05Establish hallL16–22

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

  1. L16
    have hall : ∀ n. Le(n,k) → ∃ y. ∃ z. ¬y = 0 ∧ ((∀ m. Lt(m,n) → Dvd(S (S m · (x · S (b + s))),y)) ∧ ((∀ m. ∀ i. Lt(m,n) → BetaAt(b,e,m,i) → ModEq(S (S m · (x · S (b + s))),z,i)) ∧ (∀ m. Le(n,m) → Le(m,k) → Coprime(y,S (S m · (x · S (b + s)))))))Definitions: Le(n,k)Lt(m,n)Dvd(S (S m · (x · S (b + s))),y)BetaAt(b,e,m,i)ModEq(S (S m · (x · S (b + s))),z,i)Le(n,m)Le(m,k)Coprime(y,S (S m · (x · S (b + s))))Original native command in the exact edition
  2. L17
    specialize bounded_beta_exclusive_recode_invariant k
  3. L18
    specialize bounded_beta_exclusive_recode_invariant (x * S (b + s))
  4. L19
    specialize bounded_beta_exclusive_recode_invariant b
  5. L20
    specialize bounded_beta_exclusive_recode_invariant e
  6. L21
    apply bounded_beta_exclusive_recode_invariant
  7. L22
    exact hcm2
06Establish hinvL23–27

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

  1. L23
    have hinv : ∃ P. ∃ z. ¬P = 0 ∧ ((∀ y. Lt(y,k) → Dvd(S (S y · (x · S (b + s))),P)) ∧ ((∀ y. ∀ n. Lt(y,k) → BetaAt(b,e,y,n) → ModEq(S (S y · (x · S (b + s))),z,n)) ∧ (∀ y. Le(k,y) → Le(y,k) → Coprime(P,S (S y · (x · S (b + s)))))))Definitions: Lt(y,k)Dvd(S (S y · (x · S (b + s))),P)BetaAt(b,e,y,n)ModEq(S (S y · (x · S (b + s))),z,n)Le(k,y)Le(y,k)Coprime(P,S (S y · (x · S (b + s))))Original native command in the exact edition
  2. L24
    specialize hall k
  3. L25
    apply hall
  4. L26
    specialize le_refl k
  5. L27
    exact le_refl
07Separate the logical casesL28–32

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

  1. L28
    cases hinv
  2. L29
    cases hinv_witness
  3. L30
    cases hinv_witness_witness
  4. L31
    cases hinv_witness_witness_right
  5. L32
    cases hinv_witness_witness_right_right
08Establish hcopL33–39

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

  1. L33
    have hcop : Coprime(x1,S (S k · (x · S (b + s))))Definitions: Coprime(x1,S (S k · (x · S (b + s))))Original native command in the exact edition
  2. L34
    specialize hinv_witness_witness_right_right_right k
  3. L35
    apply hinv_witness_witness_right_right_right
  4. L36
    specialize le_refl k
  5. L37
    exact le_refl
  6. L38
    specialize le_refl k
  7. L39
    exact le_refl
09Establish hnew0L40–43

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

  1. L40
    have hnew0 : ~(S ((S k) * (x * S (b + s))) = 0)
  2. L41
    specialize beta_modulus_nonzero (x * S (b + s))
  3. L42
    specialize beta_modulus_nonzero k
  4. L43
    exact beta_modulus_nonzero
10Establish hfoldL44–52

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

  1. L44
    have hfold : ∃ z2. (∀ y. ∀ z. Dvd(y,x1) → ModEq(y,x2,z) → ModEq(y,z2,z)) ∧ ModEq(S (S k · (x · S (b + s))),z2,s)Definitions: Dvd(y,x1)ModEq(y,x2,z)ModEq(y,z2,z)ModEq(S (S k · (x · S (b + s))),z2,s)Original native command in the exact edition
  2. L45
    specialize binary_crt_fold_step x1
  3. L46
    specialize binary_crt_fold_step (S ((S k) * (x * S (b + s))))
  4. L47
    specialize binary_crt_fold_step x2
  5. L48
    specialize binary_crt_fold_step s
  6. L49
    apply binary_crt_fold_step
  7. L50
    exact hinv_witness_witness_left
  8. L51
    exact hnew0
  9. L52
    exact hcop
11Separate the logical casesL53–54

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

  1. L53
    cases hfold
  2. L54
    cases hfold_witness
12Construct an explicit witnessL55–56

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

  1. L55
    exists x3
  2. L56
    exists x * S (b + s)
13Separate the logical casesL57–57

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

  1. L57
    split
14Use earlier factsL58–67

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

  1. L58
    specialize beta_at_of_mod_eq_bound x3
  2. L59
    specialize beta_at_of_mod_eq_bound (x * S (b + s))
  3. L60
    specialize beta_at_of_mod_eq_bound k
  4. L61
    specialize beta_at_of_mod_eq_bound s
  5. L62
    apply beta_at_of_mod_eq_bound
  6. L63
    specialize new_value_lt_scaled_base b
  7. L64
    specialize new_value_lt_scaled_base s
  8. L65
    specialize new_value_lt_scaled_base x
  9. L66
    specialize new_value_lt_scaled_base k
  10. L67
    apply new_value_lt_scaled_base
15Use earlier factsL68–69

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

  1. L68
    exact hC_witness_left
  2. L69
    exact hfold_witness_right
16Fix variables and assumptionsL70–73

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

  1. L70
    intro i
  2. L71
    intro a
  3. L72
    intro hi
  4. L73
    intro hati
17Establish hmiL74–77

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hinv witness witness right left.

  1. L74
    have hmi : Dvd(S (S i · (x · S (b + s))),x1)Definitions: Dvd(S (S i · (x · S (b + s))),x1)Original native command in the exact edition
  2. L75
    specialize hinv_witness_witness_right_left i
  3. L76
    apply hinv_witness_witness_right_left
  4. L77
    exact hi
18Establish hzoldL78–83

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hinv witness witness right right left.

  1. L78
    have hzold : ModEq(S (S i · (x · S (b + s))),x2,a)Definitions: ModEq(S (S i · (x · S (b + s))),x2,a)Original native command in the exact edition
  2. L79
    specialize hinv_witness_witness_right_right_left i
  3. L80
    specialize hinv_witness_witness_right_right_left a
  4. L81
    apply hinv_witness_witness_right_right_left
  5. L82
    exact hi
  6. L83
    exact hati
19Establish hznewL84–93

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

  1. L84
    have hznew : ModEq(S (S i · (x · S (b + s))),x3,a)Definitions: ModEq(S (S i · (x · S (b + s))),x3,a)Original native command in the exact edition
  2. L85
    specialize hfold_witness_left (S ((S i) * (x * S (b + s))))
  3. L86
    specialize hfold_witness_left a
  4. L87
    apply hfold_witness_left
  5. L88
    exact hmi
  6. L89
    exact hzold
  7. L90
    specialize beta_at_of_mod_eq_bound x3
  8. L91
    specialize beta_at_of_mod_eq_bound (x * S (b + s))
  9. L92
    specialize beta_at_of_mod_eq_bound i
  10. L93
    specialize beta_at_of_mod_eq_bound a
20Use earlier factsL94–103

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

  1. L94
    apply beta_at_of_mod_eq_bound
  2. L95
    specialize beta_value_lt_scaled_base b
  3. L96
    specialize beta_value_lt_scaled_base e
  4. L97
    specialize beta_value_lt_scaled_base i
  5. L98
    specialize beta_value_lt_scaled_base a
  6. L99
    specialize beta_value_lt_scaled_base x
  7. L100
    specialize beta_value_lt_scaled_base s
  8. L101
    specialize beta_value_lt_scaled_base i
  9. L102
    apply beta_value_lt_scaled_base
  10. L103
    exact hati
21Use earlier factsL104–105

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

  1. L104
    exact hC_witness_left
  2. L105
    exact hznew

Library-wide reading audit

Original defined command ledger · 105 lines
  1. 0001intro k
  2. 0002intro b
  3. 0003intro e
  4. 0004intro s
  5. 0005have hC : ∃ C. ¬C = 0 ∧ (∀ x. (∃ y. S x + S y = S k) → Dvd(S x,C))
    Exact native replay linehave hC : exists C. (~(C = 0) /\ forall t. (exists h. S t + S h = S k) -> exists q. C = S t * q)
  6. 0006specialize bounded_common_multiple_exists k
  7. 0007exact bounded_common_multiple_exists
  8. 0008cases hC
  9. 0009cases hC_witness
  10. 0010have hcm2 : ∀ t. (∃ y. S t + S y = S k) → Dvd(S t,x · S (b + s))
    Exact native replay linehave hcm2 : forall t. (exists h. S t + S h = S k) -> exists q. x * S (b + s) = S t * q
  11. 0011specialize scaled_bounded_common_multiple k
  12. 0012specialize scaled_bounded_common_multiple x
  13. 0013specialize scaled_bounded_common_multiple (S (b + s))
  14. 0014apply scaled_bounded_common_multiple
  15. 0015exact hC_witness_right
  16. 0016have hall : ∀ n. Le(n,k) → ∃ y. ∃ z. ¬y = 0 ∧ ((∀ m. Lt(m,n) → Dvd(S (S m · (x · S (b + s))),y)) ∧ ((∀ m. ∀ i. Lt(m,n) → BetaAt(b,e,m,i) → ModEq(S (S m · (x · S (b + s))),z,i)) ∧ (∀ m. Le(n,m) → Le(m,k) → Coprime(y,S (S m · (x · S (b + s)))))))
    Exact native replay linehave hall : forall n. (exists h. h + n = k) -> exists P z. (~(P = 0) /\ ((forall i. (exists h. h + S i = n) -> exists q. P = S ((S i) * (x * S (b + s))) * q) /\ ((forall i a. (exists h. h + S i = n) -> ((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) * (x * S (b + s))) * u = a + S ((S i) * (x * S (b + s))) * v) /\ forall j. (exists g. g + n = j) -> (exists h. h + j = k) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * (x * S (b + s))) = d * v) -> d = 1)))
  17. 0017specialize bounded_beta_exclusive_recode_invariant k
  18. 0018specialize bounded_beta_exclusive_recode_invariant (x * S (b + s))
  19. 0019specialize bounded_beta_exclusive_recode_invariant b
  20. 0020specialize bounded_beta_exclusive_recode_invariant e
  21. 0021apply bounded_beta_exclusive_recode_invariant
  22. 0022exact hcm2
  23. 0023have hinv : ∃ P. ∃ z. ¬P = 0 ∧ ((∀ y. Lt(y,k) → Dvd(S (S y · (x · S (b + s))),P)) ∧ ((∀ y. ∀ n. Lt(y,k) → BetaAt(b,e,y,n) → ModEq(S (S y · (x · S (b + s))),z,n)) ∧ (∀ y. Le(k,y) → Le(y,k) → Coprime(P,S (S y · (x · S (b + s)))))))
    Exact native replay linehave hinv : exists P z. (~(P = 0) /\ ((forall i. (exists h. h + S i = k) -> exists q. P = S ((S i) * (x * S (b + s))) * 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) * (x * S (b + s))) * u = a + S ((S i) * (x * S (b + s))) * v) /\ forall j. (exists g. g + k = j) -> (exists h. h + j = k) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * (x * S (b + s))) = d * v) -> d = 1)))
  24. 0024specialize hall k
  25. 0025apply hall
  26. 0026specialize le_refl k
  27. 0027exact le_refl
  28. 0028cases hinv
  29. 0029cases hinv_witness
  30. 0030cases hinv_witness_witness
  31. 0031cases hinv_witness_witness_right
  32. 0032cases hinv_witness_witness_right_right
  33. 0033have hcop : Coprime(x1,S (S k · (x · S (b + s))))
    Exact native replay linehave hcop : forall d. (exists u. x1 = d * u) -> (exists v. S ((S k) * (x * S (b + s))) = d * v) -> d = 1
  34. 0034specialize hinv_witness_witness_right_right_right k
  35. 0035apply hinv_witness_witness_right_right_right
  36. 0036specialize le_refl k
  37. 0037exact le_refl
  38. 0038specialize le_refl k
  39. 0039exact le_refl
  40. 0040have hnew0 : ~(S ((S k) * (x * S (b + s))) = 0)
  41. 0041specialize beta_modulus_nonzero (x * S (b + s))
  42. 0042specialize beta_modulus_nonzero k
  43. 0043exact beta_modulus_nonzero
  44. 0044have hfold : ∃ z2. (∀ y. ∀ z. Dvd(y,x1) → ModEq(y,x2,z) → ModEq(y,z2,z)) ∧ ModEq(S (S k · (x · S (b + s))),z2,s)
    Exact native replay linehave hfold : exists z2. ((forall m a. (exists q. x1 = m * q) -> (exists u v. x2 + m * u = a + m * v) -> exists r t. z2 + m * r = a + m * t) /\ exists q r. z2 + S ((S k) * (x * S (b + s))) * q = s + S ((S k) * (x * S (b + s))) * r)
  45. 0045specialize binary_crt_fold_step x1
  46. 0046specialize binary_crt_fold_step (S ((S k) * (x * S (b + s))))
  47. 0047specialize binary_crt_fold_step x2
  48. 0048specialize binary_crt_fold_step s
  49. 0049apply binary_crt_fold_step
  50. 0050exact hinv_witness_witness_left
  51. 0051exact hnew0
  52. 0052exact hcop
  53. 0053cases hfold
  54. 0054cases hfold_witness
  55. 0055exists x3
  56. 0056exists x * S (b + s)
  57. 0057split
  58. 0058specialize beta_at_of_mod_eq_bound x3
  59. 0059specialize beta_at_of_mod_eq_bound (x * S (b + s))
  60. 0060specialize beta_at_of_mod_eq_bound k
  61. 0061specialize beta_at_of_mod_eq_bound s
  62. 0062apply beta_at_of_mod_eq_bound
  63. 0063specialize new_value_lt_scaled_base b
  64. 0064specialize new_value_lt_scaled_base s
  65. 0065specialize new_value_lt_scaled_base x
  66. 0066specialize new_value_lt_scaled_base k
  67. 0067apply new_value_lt_scaled_base
  68. 0068exact hC_witness_left
  69. 0069exact hfold_witness_right
  70. 0070intro i
  71. 0071intro a
  72. 0072intro hi
  73. 0073intro hati
  74. 0074have hmi : Dvd(S (S i · (x · S (b + s))),x1)
    Exact native replay linehave hmi : exists q. x1 = S ((S i) * (x * S (b + s))) * q
  75. 0075specialize hinv_witness_witness_right_left i
  76. 0076apply hinv_witness_witness_right_left
  77. 0077exact hi
  78. 0078have hzold : ModEq(S (S i · (x · S (b + s))),x2,a)
    Exact native replay linehave hzold : exists u v. x2 + S ((S i) * (x * S (b + s))) * u = a + S ((S i) * (x * S (b + s))) * v
  79. 0079specialize hinv_witness_witness_right_right_left i
  80. 0080specialize hinv_witness_witness_right_right_left a
  81. 0081apply hinv_witness_witness_right_right_left
  82. 0082exact hi
  83. 0083exact hati
  84. 0084have hznew : ModEq(S (S i · (x · S (b + s))),x3,a)
    Exact native replay linehave hznew : exists u v. x3 + S ((S i) * (x * S (b + s))) * u = a + S ((S i) * (x * S (b + s))) * v
  85. 0085specialize hfold_witness_left (S ((S i) * (x * S (b + s))))
  86. 0086specialize hfold_witness_left a
  87. 0087apply hfold_witness_left
  88. 0088exact hmi
  89. 0089exact hzold
  90. 0090specialize beta_at_of_mod_eq_bound x3
  91. 0091specialize beta_at_of_mod_eq_bound (x * S (b + s))
  92. 0092specialize beta_at_of_mod_eq_bound i
  93. 0093specialize beta_at_of_mod_eq_bound a
  94. 0094apply beta_at_of_mod_eq_bound
  95. 0095specialize beta_value_lt_scaled_base b
  96. 0096specialize beta_value_lt_scaled_base e
  97. 0097specialize beta_value_lt_scaled_base i
  98. 0098specialize beta_value_lt_scaled_base a
  99. 0099specialize beta_value_lt_scaled_base x
  100. 0100specialize beta_value_lt_scaled_base s
  101. 0101specialize beta_value_lt_scaled_base i
  102. 0102apply beta_value_lt_scaled_base
  103. 0103exact hati
  104. 0104exact hC_witness_left
  105. 0105exact hznew