BT0059 · Bertrand theorem

beta_exclusive_accumulated_product_step

Stable checked-use theorem · independently kernel verified

Extend the accumulated target-modulus product 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. ∀ k. ∀ P. (∀ 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. Le(k,x) → Le(x,N) → Coprime(P,S (S x · c))) → ¬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))))

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

12 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0003 Dvd PD0005 Coprime

11 occurrences

Exact expanded native-PA statement
forall N c k P. (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 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) -> (~(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))

Proof neighborhood

Direct theorem prerequisites

BT0021 mul_ne_zero BT004V right_factor_divides_product BT003Y beta_modulus_nonzero BT0017 le_of_succ_le_succ BT001C le_eq_or_lt BT002A multiple_mul_right BT000X le_succ_self BT000F le_trans BT0019 lt_to_le BT001B lt_irrefl_expanded BT004P beta_moduli_pairwise_coprime_bounded BT004R coprime_mul_left

Direct theorem dependents

BT005B beta_exclusive_recode_invariant_step

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

95 script commands · 23 reading checkpoints · 11 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 (12)
mul ne zeroright factor divides productbeta modulus nonzerole of succ le succle eq or ltmultiple mul rightle succ selfle translt to lelt irrefl expandedbeta moduli pairwise coprime boundedcoprime mul left
01Fix variables and assumptionsL1–9

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

  1. L1
    intro N
  2. L2
    intro c
  3. L3
    intro k
  4. L4
    intro P
  5. L5
    intro hcm
  6. L6
    intro hkN
  7. L7
    intro hP
  8. L8
    intro hdiv
  9. L9
    intro hfuture
02Establish hnewL10–13

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

  1. L10
    have hnew : ~(S ((S k) * c) = 0)
  2. L11
    specialize beta_modulus_nonzero c
  3. L12
    specialize beta_modulus_nonzero k
  4. L13
    exact beta_modulus_nonzero
03Separate the logical casesL14–14

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

  1. L14
    split
04Use earlier factsL15–16

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

  1. L15
    specialize mul_ne_zero P
  2. L16
    specialize mul_ne_zero (S ((S k) * c))
05Fix variables and assumptionsL17–17

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

  1. L17
    intro hzero
06Use earlier factsL18–21

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

  1. L18
    apply mul_ne_zero
  2. L19
    exact hP
  3. L20
    exact hnew
  4. L21
    exact hzero
07Separate the logical casesL22–22

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

  1. L22
    split
08Fix variables and assumptionsL23–24

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

  1. L23
    intro i
  2. L24
    intro hi
09Establish hikL25–29

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

  1. L25
  2. L26
    specialize le_of_succ_le_succ i
  3. L27
    specialize le_of_succ_le_succ k
  4. L28
    apply le_of_succ_le_succ
  5. L29
    exact hi
10Establish hsplitL30–34

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

  1. L30
    have hsplit : i = k ∨ Lt(i,k)Definitions: Lt(i,k)Original native command in the exact edition
  2. L31
    specialize le_eq_or_lt i
  3. L32
    specialize le_eq_or_lt k
  4. L33
    apply le_eq_or_lt
  5. L34
    exact hik
11Separate the logical casesL35–35

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

  1. L35
    cases hsplit
12Calculate and transport equalitiesL36–36

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

  1. L36
    rewrite hsplit_left
13Use earlier factsL37–39

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

  1. L37
    specialize right_factor_divides_product P
  2. L38
    specialize right_factor_divides_product (S ((S k) * c))
  3. L39
    exact right_factor_divides_product
14Establish hiPL40–49

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

  1. L40
    have hiP : Dvd(S (S i · c),P)Definitions: Dvd(S (S i · c),P)Original native command in the exact edition
  2. L41
    specialize hdiv i
  3. L42
    apply hdiv
  4. L43
    exact hsplit_right
  5. L44
    specialize multiple_mul_right (S ((S i) * c))
  6. L45
    specialize multiple_mul_right P
  7. L46
    specialize multiple_mul_right (S ((S k) * c))
  8. L47
    apply multiple_mul_right
  9. L48
    exact hiP
  10. L49
    intro j
15Fix variables and assumptionsL50–51

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

  1. L50
    intro hSkj
  2. L51
    intro hjN
16Establish hkjL52–52

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

  1. L52
17Establish hkSkL53–61

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

  1. L53
  2. L54
    specialize le_succ_self k
  3. L55
    exact le_succ_self
  4. L56
    specialize le_trans k
  5. L57
    specialize le_trans (S k)
  6. L58
    specialize le_trans j
  7. L59
    apply le_trans
  8. L60
    exact hkSk
  9. L61
    exact hSkj
18Establish hPjL62–66

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

  1. L62
    have hPj : Coprime(P,S (S j · c))Definitions: Coprime(P,S (S j · c))Original native command in the exact edition
  2. L63
    specialize hfuture j
  3. L64
    apply hfuture
  4. L65
    exact hkj
  5. L66
    exact hjN
19Establish hneqL67–72

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

  1. L67
    have hneq : ~(k = j)
  2. L68
    intro heq
  3. L69
    rewrite <- heq at hSkj
  4. L70
    specialize lt_irrefl_expanded k
  5. L71
    apply lt_irrefl_expanded
  6. L72
    exact hSkj
20Establish hkboundL73–77

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

  1. L73
    have hkbound : Le(k,N)Definitions: Le(k,N)Original native command in the exact edition
  2. L74
    specialize lt_to_le k
  3. L75
    specialize lt_to_le N
  4. L76
    apply lt_to_le
  5. L77
    exact hkN
21Establish hpairsL78–82

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta moduli pairwise coprime bounded.

  1. L78
    have hpairs : ∀ i. ∀ j. ¬i = j → Le(i,N) → Le(j,N) → Coprime(S (S i · c),S (S j · c))Definitions: Le(i,N)Le(j,N)Coprime(S (S i · c),S (S j · c))Original native command in the exact edition
  2. L79
    specialize beta_moduli_pairwise_coprime_bounded N
  3. L80
    specialize beta_moduli_pairwise_coprime_bounded c
  4. L81
    apply beta_moduli_pairwise_coprime_bounded
  5. L82
    exact hcm
22Establish hnewjL83–92

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

  1. L83
    have hnewj : Coprime(S (S k · c),S (S j · c))Definitions: Coprime(S (S k · c),S (S j · c))Original native command in the exact edition
  2. L84
    specialize hpairs k
  3. L85
    specialize hpairs j
  4. L86
    apply hpairs
  5. L87
    exact hneq
  6. L88
    exact hkbound
  7. L89
    exact hjN
  8. L90
    specialize coprime_mul_left P
  9. L91
    specialize coprime_mul_left (S ((S k) * c))
  10. L92
    specialize coprime_mul_left (S ((S j) * c))
23Use earlier factsL93–95

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

  1. L93
    apply coprime_mul_left
  2. L94
    exact hPj
  3. L95
    exact hnewj

Library-wide reading audit

Original defined command ledger · 95 lines
  1. 0001intro N
  2. 0002intro c
  3. 0003intro k
  4. 0004intro P
  5. 0005intro hcm
  6. 0006intro hkN
  7. 0007intro hP
  8. 0008intro hdiv
  9. 0009intro hfuture
  10. 0010have hnew : ~(S ((S k) * c) = 0)
  11. 0011specialize beta_modulus_nonzero c
  12. 0012specialize beta_modulus_nonzero k
  13. 0013exact beta_modulus_nonzero
  14. 0014split
  15. 0015specialize mul_ne_zero P
  16. 0016specialize mul_ne_zero (S ((S k) * c))
  17. 0017intro hzero
  18. 0018apply mul_ne_zero
  19. 0019exact hP
  20. 0020exact hnew
  21. 0021exact hzero
  22. 0022split
  23. 0023intro i
  24. 0024intro hi
  25. 0025have hik : Le(i,k)
    Exact native replay linehave hik : exists r. r + i = k
  26. 0026specialize le_of_succ_le_succ i
  27. 0027specialize le_of_succ_le_succ k
  28. 0028apply le_of_succ_le_succ
  29. 0029exact hi
  30. 0030have hsplit : i = k ∨ Lt(i,k)
    Exact native replay linehave hsplit : i = k \/ exists r. r + S i = k
  31. 0031specialize le_eq_or_lt i
  32. 0032specialize le_eq_or_lt k
  33. 0033apply le_eq_or_lt
  34. 0034exact hik
  35. 0035cases hsplit
  36. 0036rewrite hsplit_left
  37. 0037specialize right_factor_divides_product P
  38. 0038specialize right_factor_divides_product (S ((S k) * c))
  39. 0039exact right_factor_divides_product
  40. 0040have hiP : Dvd(S (S i · c),P)
    Exact native replay linehave hiP : exists q. P = S ((S i) * c) * q
  41. 0041specialize hdiv i
  42. 0042apply hdiv
  43. 0043exact hsplit_right
  44. 0044specialize multiple_mul_right (S ((S i) * c))
  45. 0045specialize multiple_mul_right P
  46. 0046specialize multiple_mul_right (S ((S k) * c))
  47. 0047apply multiple_mul_right
  48. 0048exact hiP
  49. 0049intro j
  50. 0050intro hSkj
  51. 0051intro hjN
  52. 0052have hkj : Le(k,j)
    Exact native replay linehave hkj : exists r. r + k = j
  53. 0053have hkSk : Le(k,S k)
    Exact native replay linehave hkSk : exists r. r + k = S k
  54. 0054specialize le_succ_self k
  55. 0055exact le_succ_self
  56. 0056specialize le_trans k
  57. 0057specialize le_trans (S k)
  58. 0058specialize le_trans j
  59. 0059apply le_trans
  60. 0060exact hkSk
  61. 0061exact hSkj
  62. 0062have hPj : Coprime(P,S (S j · c))
    Exact native replay linehave hPj : forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1
  63. 0063specialize hfuture j
  64. 0064apply hfuture
  65. 0065exact hkj
  66. 0066exact hjN
  67. 0067have hneq : ~(k = j)
  68. 0068intro heq
  69. 0069rewrite <- heq at hSkj
  70. 0070specialize lt_irrefl_expanded k
  71. 0071apply lt_irrefl_expanded
  72. 0072exact hSkj
  73. 0073have hkbound : Le(k,N)
    Exact native replay linehave hkbound : exists r. r + k = N
  74. 0074specialize lt_to_le k
  75. 0075specialize lt_to_le N
  76. 0076apply lt_to_le
  77. 0077exact hkN
  78. 0078have hpairs : ∀ i. ∀ j. ¬i = j → Le(i,N) → Le(j,N) → Coprime(S (S i · c),S (S j · c))
    Exact native replay linehave hpairs : forall i j. ~(i = j) -> (exists hi. hi + i = N) -> (exists hj. hj + j = N) -> forall d. (exists u. S ((S i) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1
  79. 0079specialize beta_moduli_pairwise_coprime_bounded N
  80. 0080specialize beta_moduli_pairwise_coprime_bounded c
  81. 0081apply beta_moduli_pairwise_coprime_bounded
  82. 0082exact hcm
  83. 0083have hnewj : Coprime(S (S k · c),S (S j · c))
    Exact native replay linehave hnewj : forall d. (exists u. S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1
  84. 0084specialize hpairs k
  85. 0085specialize hpairs j
  86. 0086apply hpairs
  87. 0087exact hneq
  88. 0088exact hkbound
  89. 0089exact hjN
  90. 0090specialize coprime_mul_left P
  91. 0091specialize coprime_mul_left (S ((S k) * c))
  92. 0092specialize coprime_mul_left (S ((S j) * c))
  93. 0093apply coprime_mul_left
  94. 0094exact hPj
  95. 0095exact hnewj