BT0069 · Bertrand theorem

beta_factor_divides_product

Stable checked-use theorem · independently kernel verified

Every decoded factor inside an exact beta Product divides its terminal 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

∀ b. ∀ c. ∀ l. ∀ n. ∀ i. ∀ p. Lt(i,l) → BetaAt(b,c,i,p) → Product(b,c,l,n) → Dvd(p,n)

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 PD0003 Dvd PD0013 BetaAt PD0014 Product

4 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0003 Dvd PD0013 BetaAt PD0014 Product

6 occurrences

Exact expanded native-PA statement
forall b c l n i p. (exists h. h + S i = l) -> ((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * 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 n = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + n) /\ 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 q. n = p * q

Proof neighborhood

Direct theorem prerequisites

BT000L add_eq_zero_right BT000C succ_ne_zero BT005J beta_product_succ_decompose BT0017 le_of_succ_le_succ BT001C le_eq_or_lt BT0042 beta_at_unique BT0006 mul_comm BT002A multiple_mul_right

Direct theorem dependents

BT00VA factorial_prime_divides_of_le BT0100 prime_contribution_selected_entry

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

82 script commands · 23 reading checkpoints · 7 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 (8)
add eq zero rightsucc ne zerobeta product succ decomposele of succ le succle eq or ltbeta at uniquemul commmultiple mul right
01Fix variables and assumptionsL1–2

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

  1. L1
    intro b
  2. L2
    intro c
02Induction on lL3–9

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

  1. L3
    induction l
  2. L4
    intro n
  3. L5
    intro i
  4. L6
    intro p
  5. L7
    intro hi
  6. L8
    intro hp
  7. L9
    intro hproduct
03Separate the logical casesL10–11

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

  1. L10
    exfalso
  2. L11
    cases hi
04Establish hsi0L12–21

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

  1. L12
    have hsi0 : S i = 0
  2. L13
    specialize add_eq_zero_right x
  3. L14
    specialize add_eq_zero_right (S i)
  4. L15
    apply add_eq_zero_right
  5. L16
    exact hi_witness
  6. L17
    specialize succ_ne_zero i
  7. L18
    apply succ_ne_zero
  8. L19
    exact hsi0
  9. L20
    intro n
  10. L21
    intro i
05Fix variables and assumptionsL22–25

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

  1. L22
    intro p
  2. L23
    intro hi
  3. L24
    intro hp
  4. L25
    intro hproduct
06Establish hdecompL26–32

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

  1. L26
    have hdecomp : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Product(b,c,l,r) ∧ n = r · a)Definitions: BetaAt(b,c,l,a)Product(b,c,l,r)Original native command in the exact edition
  2. L27
    specialize beta_product_succ_decompose b
  3. L28
    specialize beta_product_succ_decompose c
  4. L29
    specialize beta_product_succ_decompose l
  5. L30
    specialize beta_product_succ_decompose n
  6. L31
    apply beta_product_succ_decompose
  7. L32
    exact hproduct
07Separate the logical casesL33–36

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

  1. L33
    cases hdecomp
  2. L34
    cases hdecomp_witness
  3. L35
    cases hdecomp_witness_witness
  4. L36
    cases hdecomp_witness_witness_right
08Establish hilL37–41

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

  1. L37
  2. L38
    specialize le_of_succ_le_succ i
  3. L39
    specialize le_of_succ_le_succ l
  4. L40
    apply le_of_succ_le_succ
  5. L41
    exact hi
09Establish hsplitL42–46

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

  1. L42
    have hsplit : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L43
    specialize le_eq_or_lt i
  3. L44
    specialize le_eq_or_lt l
  4. L45
    apply le_eq_or_lt
  5. L46
    exact hil
10Separate the logical casesL47–47

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

  1. L47
    cases hsplit
11Establish hpaL48–57

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

  1. L48
    have hpa : p = x
  2. L49
    specialize beta_at_unique b
  3. L50
    specialize beta_at_unique c
  4. L51
    specialize beta_at_unique l
  5. L52
    specialize beta_at_unique p
  6. L53
    specialize beta_at_unique x
  7. L54
    apply beta_at_unique
  8. L55
    rewrite hsplit_left at hp
  9. L56
    rewrite hsplit_left at hp
  10. L57
    exact hp
12Use earlier factsL58–58

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

  1. L58
    exact hdecomp_witness_witness_left
13Construct an explicit witnessL59–59

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

  1. L59
    exists x1
14Calculate and transport equalitiesL60–60

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

  1. L60
    trans x1 * x
15Use earlier factsL61–61

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

  1. L61
    exact hdecomp_witness_witness_right_right
16Calculate and transport equalitiesL62–62

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

  1. L62
    rewrite hpa
17Use earlier factsL63–63

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

  1. L63
    apply mul_comm
18Establish hidivL64–71

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

  1. L64
  2. L65
    specialize IH x1
  3. L66
    specialize IH i
  4. L67
    specialize IH p
  5. L68
    apply IH
  6. L69
    exact hsplit_right
  7. L70
    exact hp
  8. L71
    exact hdecomp_witness_witness_right_left
19Establish hmulL72–77

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

  1. L72
    have hmul : Dvd(p,x1 · x)Definitions: Dvd(p,x1 · x)Original native command in the exact edition
  2. L73
    specialize multiple_mul_right p
  3. L74
    specialize multiple_mul_right x1
  4. L75
    specialize multiple_mul_right x
  5. L76
    apply multiple_mul_right
  6. L77
    exact hidiv
20Separate the logical casesL78–78

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

  1. L78
    cases hmul
21Construct an explicit witnessL79–79

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

  1. L79
    exists x2
22Calculate and transport equalitiesL80–80

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

  1. L80
    trans x1 * x
23Use earlier factsL81–82

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

  1. L81
    exact hdecomp_witness_witness_right_right
  2. L82
    exact hmul_witness

Library-wide reading audit

Original defined command ledger · 82 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003induction l
  4. 0004intro n
  5. 0005intro i
  6. 0006intro p
  7. 0007intro hi
  8. 0008intro hp
  9. 0009intro hproduct
  10. 0010exfalso
  11. 0011cases hi
  12. 0012have hsi0 : S i = 0
  13. 0013specialize add_eq_zero_right x
  14. 0014specialize add_eq_zero_right (S i)
  15. 0015apply add_eq_zero_right
  16. 0016exact hi_witness
  17. 0017specialize succ_ne_zero i
  18. 0018apply succ_ne_zero
  19. 0019exact hsi0
  20. 0020intro n
  21. 0021intro i
  22. 0022intro p
  23. 0023intro hi
  24. 0024intro hp
  25. 0025intro hproduct
  26. 0026have hdecomp : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Product(b,c,l,r) ∧ n = r · a)
    Exact native replay linehave hdecomp : exists a r. (((exists h. h + S a = S ((S l) * c)) /\ exists q. b = q * S ((S l) * c) + a) /\ ((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)))))) /\ n = r * a))
  27. 0027specialize beta_product_succ_decompose b
  28. 0028specialize beta_product_succ_decompose c
  29. 0029specialize beta_product_succ_decompose l
  30. 0030specialize beta_product_succ_decompose n
  31. 0031apply beta_product_succ_decompose
  32. 0032exact hproduct
  33. 0033cases hdecomp
  34. 0034cases hdecomp_witness
  35. 0035cases hdecomp_witness_witness
  36. 0036cases hdecomp_witness_witness_right
  37. 0037have hil : Le(i,l)
    Exact native replay linehave hil : exists h. h + i = l
  38. 0038specialize le_of_succ_le_succ i
  39. 0039specialize le_of_succ_le_succ l
  40. 0040apply le_of_succ_le_succ
  41. 0041exact hi
  42. 0042have hsplit : i = l ∨ Lt(i,l)
    Exact native replay linehave hsplit : i = l \/ exists h. h + S i = l
  43. 0043specialize le_eq_or_lt i
  44. 0044specialize le_eq_or_lt l
  45. 0045apply le_eq_or_lt
  46. 0046exact hil
  47. 0047cases hsplit
  48. 0048have hpa : p = x
  49. 0049specialize beta_at_unique b
  50. 0050specialize beta_at_unique c
  51. 0051specialize beta_at_unique l
  52. 0052specialize beta_at_unique p
  53. 0053specialize beta_at_unique x
  54. 0054apply beta_at_unique
  55. 0055rewrite hsplit_left at hp
  56. 0056rewrite hsplit_left at hp
  57. 0057exact hp
  58. 0058exact hdecomp_witness_witness_left
  59. 0059exists x1
  60. 0060trans x1 * x
  61. 0061exact hdecomp_witness_witness_right_right
  62. 0062rewrite hpa
  63. 0063apply mul_comm
  64. 0064have hidiv : Dvd(p,x1)
    Exact native replay linehave hidiv : exists q. x1 = p * q
  65. 0065specialize IH x1
  66. 0066specialize IH i
  67. 0067specialize IH p
  68. 0068apply IH
  69. 0069exact hsplit_right
  70. 0070exact hp
  71. 0071exact hdecomp_witness_witness_right_left
  72. 0072have hmul : Dvd(p,x1 · x)
    Exact native replay linehave hmul : exists q. x1 * x = p * q
  73. 0073specialize multiple_mul_right p
  74. 0074specialize multiple_mul_right x1
  75. 0075specialize multiple_mul_right x
  76. 0076apply multiple_mul_right
  77. 0077exact hidiv
  78. 0078cases hmul
  79. 0079exists x2
  80. 0080trans x1 * x
  81. 0081exact hdecomp_witness_witness_right_right
  82. 0082exact hmul_witness