BT005K · Bertrand theorem

beta_product_succ_append

Stable checked-use theorem · independently kernel verified

Append one decoded factor to an existing fully expanded Product witness.

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

∀ b. ∀ c. ∀ l. ∀ r. ∀ p. Product(b,c,l,r) → BetaAt(b,c,l,p) → Product(b,c,S l,r · p)

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

PD0013 BetaAt PD0014 Product

3 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0013 BetaAt

10 occurrences

Exact expanded native-PA statement
forall b c l r p. (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S r = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + r) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))) -> ((exists h. h + S p = S ((S l) * c)) /\ exists q. b = q * S ((S l) * c) + p) -> (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S (r * p) = S ((S S l) * v)) /\ exists q. u = q * S ((S S l) * v) + (r * p)) /\ forall i. (exists h. h + S i = S l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p))))))

Proof neighborhood

Direct theorem prerequisites

BT005D beta_prefix_extend BT000W zero_le BT0016 succ_le_succ BT000E le_refl BT0017 le_of_succ_le_succ BT001C le_eq_or_lt

Direct theorem dependents

BT00UQ beta_product_prefix_suffix_split

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

101 script commands · 34 reading checkpoints · 5 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)
beta prefix extendzero lesucc le succle reflle of succ le succle eq or lt
01Fix variables and assumptionsL1–7

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro r
  5. L5
    intro p
  6. L6
    intro hproduct
  7. L7
    intro hp
02Separate the logical casesL8–11

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

  1. L8
    cases hproduct
  2. L9
    cases hproduct_witness
  3. L10
    cases hproduct_witness_witness
  4. L11
    cases hproduct_witness_witness_right
03Establish hextL12–17

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

  1. L12
    have hext : ∃ z. ∃ d. BetaAt(z,d,S l,r · p) ∧ (∀ y. ∀ n. Lt(y,S l) → BetaAt(x,x1,y,n) → BetaAt(z,d,y,n))Definitions: BetaAt(z,d,S l,r · p)Lt(y,S l)BetaAt(x,x1,y,n)BetaAt(z,d,y,n)Original native command in the exact edition
  2. L13
    specialize beta_prefix_extend (S l)
  3. L14
    specialize beta_prefix_extend x
  4. L15
    specialize beta_prefix_extend x1
  5. L16
    specialize beta_prefix_extend (r * p)
  6. L17
    exact beta_prefix_extend
04Separate the logical casesL18–20

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

  1. L18
    cases hext
  2. L19
    cases hext_witness
  3. L20
    cases hext_witness_witness
05Construct an explicit witnessL21–22

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

  1. L21
    exists x2
  2. L22
    exists x3
06Separate the logical casesL23–23

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

  1. L23
    split
07Use earlier factsL24–26

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

  1. L24
    specialize hext_witness_witness_right 0
  2. L25
    specialize hext_witness_witness_right 1
  3. L26
    apply hext_witness_witness_right
08Establish hzeroL27–34

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

  1. L27
  2. L28
    specialize zero_le l
  3. L29
    exact zero_le
  4. L30
    specialize succ_le_succ 0
  5. L31
    specialize succ_le_succ l
  6. L32
    apply succ_le_succ
  7. L33
    exact hzero
  8. L34
    exact hproduct_witness_witness_left
09Separate the logical casesL35–35

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

  1. L35
    split
10Use earlier factsL36–36

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

  1. L36
    exact hext_witness_witness_left
11Fix variables and assumptionsL37–38

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

  1. L37
    intro i
  2. L38
    intro hi
12Establish hilL39–43

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

  1. L39
  2. L40
    specialize le_of_succ_le_succ i
  3. L41
    specialize le_of_succ_le_succ l
  4. L42
    apply le_of_succ_le_succ
  5. L43
    exact hi
13Establish hsplitL44–48

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

  1. L44
    have hsplit : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L45
    specialize le_eq_or_lt i
  3. L46
    specialize le_eq_or_lt l
  4. L47
    apply le_eq_or_lt
  5. L48
    exact hil
14Separate the logical casesL49–49

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

  1. L49
    cases hsplit
15Construct an explicit witnessL50–52

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

  1. L50
    exists p
  2. L51
    exists r
  3. L52
    exists r * p
16Separate the logical casesL53–53

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

  1. L53
    split
17Calculate and transport equalitiesL54–55

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L54
    rewrite hsplit_left
  2. L55
    rewrite hsplit_left
18Use earlier factsL56–56

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

  1. L56
    exact hp
19Separate the logical casesL57–57

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

  1. L57
    split
20Calculate and transport equalitiesL58–59

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L58
    rewrite hsplit_left
  2. L59
    rewrite hsplit_left
21Use earlier factsL60–65

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

  1. L60
    specialize hext_witness_witness_right l
  2. L61
    specialize hext_witness_witness_right r
  3. L62
    apply hext_witness_witness_right
  4. L63
    specialize le_refl (S l)
  5. L64
    exact le_refl
  6. L65
    exact hproduct_witness_witness_right_left
22Separate the logical casesL66–66

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

  1. L66
    split
23Calculate and transport equalitiesL67–68

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L67
    rewrite hsplit_left
  2. L68
    rewrite hsplit_left
24Use earlier factsL69–69

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

  1. L69
    exact hext_witness_witness_left
25Calculate and transport equalitiesL70–70

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L70
    refl
26Establish holdL71–74

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

  1. L71
    have hold : ∃ p0. ∃ r0. ∃ s0. BetaAt(b,c,i,p0) ∧ (BetaAt(x,x1,i,r0) ∧ (BetaAt(x,x1,S i,s0) ∧ s0 = r0 · p0))Definitions: BetaAt(b,c,i,p0)BetaAt(x,x1,i,r0)BetaAt(x,x1,S i,s0)Original native command in the exact edition
  2. L72
    specialize hproduct_witness_witness_right_right i
  3. L73
    apply hproduct_witness_witness_right_right
  4. L74
    exact hsplit_right
27Separate the logical casesL75–80

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

  1. L75
    cases hold
  2. L76
    cases hold_witness
  3. L77
    cases hold_witness_witness
  4. L78
    cases hold_witness_witness_witness
  5. L79
    cases hold_witness_witness_witness_right
  6. L80
    cases hold_witness_witness_witness_right_right
28Construct an explicit witnessL81–83

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

  1. L81
    exists x4
  2. L82
    exists x5
  3. L83
    exists x6
29Separate the logical casesL84–84

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

  1. L84
    split
30Use earlier factsL85–85

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

  1. L85
    exact hold_witness_witness_witness_left
31Separate the logical casesL86–86

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

  1. L86
    split
32Use earlier factsL87–91

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

  1. L87
    specialize hext_witness_witness_right i
  2. L88
    specialize hext_witness_witness_right x5
  3. L89
    apply hext_witness_witness_right
  4. L90
    exact hi
  5. L91
    exact hold_witness_witness_witness_right_left
33Separate the logical casesL92–92

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

  1. L92
    split
34Use earlier factsL93–101

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

  1. L93
    specialize hext_witness_witness_right (S i)
  2. L94
    specialize hext_witness_witness_right x6
  3. L95
    apply hext_witness_witness_right
  4. L96
    specialize succ_le_succ (S i)
  5. L97
    specialize succ_le_succ l
  6. L98
    apply succ_le_succ
  7. L99
    exact hsplit_right
  8. L100
    exact hold_witness_witness_witness_right_right_left
  9. L101
    exact hold_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 101 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro r
  5. 0005intro p
  6. 0006intro hproduct
  7. 0007intro hp
  8. 0008cases hproduct
  9. 0009cases hproduct_witness
  10. 0010cases hproduct_witness_witness
  11. 0011cases hproduct_witness_witness_right
  12. 0012have hext : ∃ z. ∃ d. BetaAt(z,d,S l,r · p) ∧ (∀ y. ∀ n. Lt(y,S l) → BetaAt(x,x1,y,n) → BetaAt(z,d,y,n))
    Exact native replay linehave hext : exists z d. (((exists h. h + S (r * p) = S ((S S l) * d)) /\ exists q. z = q * S ((S S l) * d) + (r * p)) /\ forall i a. (exists h. h + S i = S l) -> ((exists h. h + S a = S ((S i) * x1)) /\ exists q. x = q * S ((S i) * x1) + a) -> ((exists h. h + S a = S ((S i) * d)) /\ exists q. z = q * S ((S i) * d) + a))
  13. 0013specialize beta_prefix_extend (S l)
  14. 0014specialize beta_prefix_extend x
  15. 0015specialize beta_prefix_extend x1
  16. 0016specialize beta_prefix_extend (r * p)
  17. 0017exact beta_prefix_extend
  18. 0018cases hext
  19. 0019cases hext_witness
  20. 0020cases hext_witness_witness
  21. 0021exists x2
  22. 0022exists x3
  23. 0023split
  24. 0024specialize hext_witness_witness_right 0
  25. 0025specialize hext_witness_witness_right 1
  26. 0026apply hext_witness_witness_right
  27. 0027have hzero : Le(0,l)
    Exact native replay linehave hzero : exists h. h + 0 = l
  28. 0028specialize zero_le l
  29. 0029exact zero_le
  30. 0030specialize succ_le_succ 0
  31. 0031specialize succ_le_succ l
  32. 0032apply succ_le_succ
  33. 0033exact hzero
  34. 0034exact hproduct_witness_witness_left
  35. 0035split
  36. 0036exact hext_witness_witness_left
  37. 0037intro i
  38. 0038intro hi
  39. 0039have hil : Le(i,l)
    Exact native replay linehave hil : exists h. h + i = l
  40. 0040specialize le_of_succ_le_succ i
  41. 0041specialize le_of_succ_le_succ l
  42. 0042apply le_of_succ_le_succ
  43. 0043exact hi
  44. 0044have hsplit : i = l ∨ Lt(i,l)
    Exact native replay linehave hsplit : i = l \/ exists h. h + S i = l
  45. 0045specialize le_eq_or_lt i
  46. 0046specialize le_eq_or_lt l
  47. 0047apply le_eq_or_lt
  48. 0048exact hil
  49. 0049cases hsplit
  50. 0050exists p
  51. 0051exists r
  52. 0052exists r * p
  53. 0053split
  54. 0054rewrite hsplit_left
  55. 0055rewrite hsplit_left
  56. 0056exact hp
  57. 0057split
  58. 0058rewrite hsplit_left
  59. 0059rewrite hsplit_left
  60. 0060specialize hext_witness_witness_right l
  61. 0061specialize hext_witness_witness_right r
  62. 0062apply hext_witness_witness_right
  63. 0063specialize le_refl (S l)
  64. 0064exact le_refl
  65. 0065exact hproduct_witness_witness_right_left
  66. 0066split
  67. 0067rewrite hsplit_left
  68. 0068rewrite hsplit_left
  69. 0069exact hext_witness_witness_left
  70. 0070refl
  71. 0071have hold : ∃ p0. ∃ r0. ∃ s0. BetaAt(b,c,i,p0) ∧ (BetaAt(x,x1,i,r0) ∧ (BetaAt(x,x1,S i,s0) ∧ s0 = r0 · p0))
    Exact native replay linehave hold : exists p0 r0 s0. (((exists h. h + S p0 = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p0) /\ (((exists h. h + S r0 = S ((S i) * x1)) /\ exists q. x = q * S ((S i) * x1) + r0) /\ (((exists h. h + S s0 = S ((S S i) * x1)) /\ exists q. x = q * S ((S S i) * x1) + s0) /\ s0 = r0 * p0)))
  72. 0072specialize hproduct_witness_witness_right_right i
  73. 0073apply hproduct_witness_witness_right_right
  74. 0074exact hsplit_right
  75. 0075cases hold
  76. 0076cases hold_witness
  77. 0077cases hold_witness_witness
  78. 0078cases hold_witness_witness_witness
  79. 0079cases hold_witness_witness_witness_right
  80. 0080cases hold_witness_witness_witness_right_right
  81. 0081exists x4
  82. 0082exists x5
  83. 0083exists x6
  84. 0084split
  85. 0085exact hold_witness_witness_witness_left
  86. 0086split
  87. 0087specialize hext_witness_witness_right i
  88. 0088specialize hext_witness_witness_right x5
  89. 0089apply hext_witness_witness_right
  90. 0090exact hi
  91. 0091exact hold_witness_witness_witness_right_left
  92. 0092split
  93. 0093specialize hext_witness_witness_right (S i)
  94. 0094specialize hext_witness_witness_right x6
  95. 0095apply hext_witness_witness_right
  96. 0096specialize succ_le_succ (S i)
  97. 0097specialize succ_le_succ l
  98. 0098apply succ_le_succ
  99. 0099exact hsplit_right
  100. 0100exact hold_witness_witness_witness_right_right_left
  101. 0101exact hold_witness_witness_witness_right_right_right