BT00VE · Bertrand theorem

primorial_interval_pairwise_coprime

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Distinct positions in an interval decode coprime selector factors.

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

∀ a. ∀ b. ∀ c. ∀ l. (∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ (Prime(S (a + x)) ∧ y = S (a + x) ∨ ¬Prime(S (a + x)) ∧ y = 1)) → ∀ x. ∀ y. ∀ z. ∀ n. Lt(x,l) → Lt(y,l) → BetaAt(b,c,x,z) → BetaAt(b,c,y,n) → ¬x = y → Coprime(z,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 PD0004 Prime PD0005 Coprime PD0013 BetaAt

9 occurrences

In local proof propositions

PD0004 Prime PD0013 BetaAt

6 occurrences

Exact expanded native-PA statement
forall a b c l. (forall bpr_index_bpipc_source. (exists bpr_gap_bpipc_source_bound. bpr_gap_bpipc_source_bound + S (bpr_index_bpipc_source) = l) -> exists bpr_value_bpipc_source. ((((exists bpr_height_bpipc_source_decoded. bpr_height_bpipc_source_decoded + S (bpr_value_bpipc_source) = S ((S (bpr_index_bpipc_source)) * c)) /\ exists bpr_quotient_bpipc_source_decoded. b = bpr_quotient_bpipc_source_decoded * S ((S (bpr_index_bpipc_source)) * c) + (bpr_value_bpipc_source))) /\ (((((~(S (a + bpr_index_bpipc_source) = 1) /\ forall bpr_left_bpipc_source_choice_prime bpr_right_bpipc_source_choice_prime. S (a + bpr_index_bpipc_source) = bpr_left_bpipc_source_choice_prime * bpr_right_bpipc_source_choice_prime -> bpr_left_bpipc_source_choice_prime = 1 \/ bpr_right_bpipc_source_choice_prime = 1)) /\ bpr_value_bpipc_source = S (a + bpr_index_bpipc_source)) \/ (~((~(S (a + bpr_index_bpipc_source) = 1) /\ forall bpr_left_bpipc_source_choice_prime bpr_right_bpipc_source_choice_prime. S (a + bpr_index_bpipc_source) = bpr_left_bpipc_source_choice_prime * bpr_right_bpipc_source_choice_prime -> bpr_left_bpipc_source_choice_prime = 1 \/ bpr_right_bpipc_source_choice_prime = 1)) /\ bpr_value_bpipc_source = 1))))) -> (forall bpr_left_index_bpipc_result bpr_right_index_bpipc_result bpr_left_value_bpipc_result bpr_right_value_bpipc_result. (exists bpr_gap_bpipc_result_left_bound. bpr_gap_bpipc_result_left_bound + S (bpr_left_index_bpipc_result) = l) -> (exists bpr_gap_bpipc_result_right_bound. bpr_gap_bpipc_result_right_bound + S (bpr_right_index_bpipc_result) = l) -> (((exists bpr_height_bpipc_result_left_at. bpr_height_bpipc_result_left_at + S (bpr_left_value_bpipc_result) = S ((S (bpr_left_index_bpipc_result)) * c)) /\ exists bpr_quotient_bpipc_result_left_at. b = bpr_quotient_bpipc_result_left_at * S ((S (bpr_left_index_bpipc_result)) * c) + (bpr_left_value_bpipc_result))) -> (((exists bpr_height_bpipc_result_right_at. bpr_height_bpipc_result_right_at + S (bpr_right_value_bpipc_result) = S ((S (bpr_right_index_bpipc_result)) * c)) /\ exists bpr_quotient_bpipc_result_right_at. b = bpr_quotient_bpipc_result_right_at * S ((S (bpr_right_index_bpipc_result)) * c) + (bpr_right_value_bpipc_result))) -> ~(bpr_left_index_bpipc_result = bpr_right_index_bpipc_result) -> (forall bpr_coprime_divisor_bpipc_result_coprime. (exists bpr_coprime_left_factor_bpipc_result_coprime. bpr_left_value_bpipc_result = bpr_coprime_divisor_bpipc_result_coprime * bpr_coprime_left_factor_bpipc_result_coprime) -> (exists bpr_coprime_right_factor_bpipc_result_coprime. bpr_right_value_bpipc_result = bpr_coprime_divisor_bpipc_result_coprime * bpr_coprime_right_factor_bpipc_result_coprime) -> bpr_coprime_divisor_bpipc_result_coprime = 1))

Proof neighborhood

Direct theorem prerequisites

BT0042 beta_at_unique BT000V add_left_cancel BT008S distinct_primes_coprime BT002Y coprime_one_left BT002X coprime_one_right

Direct theorem dependents

BT00VF primorial_interval_divides_choose_between

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

114 script commands · 27 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 (5)
beta at uniqueadd left canceldistinct primes coprimecoprime one leftcoprime one right
01Fix variables and assumptionsL1–10

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro l
  5. L5
    intro hprefix
  6. L6
    intro i
  7. L7
    intro j
  8. L8
    intro p
  9. L9
    intro q
  10. L10
    intro hi
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hj
  2. L12
    intro hp
  3. L13
    intro hq
  4. L14
    intro hij
03Establish hleftL15–17

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

  1. L15
    have hleft : ∃ x. BetaAt(b,c,i,x) ∧ (Prime(S (a + i)) ∧ x = S (a + i) ∨ ¬Prime(S (a + i)) ∧ x = 1)Definitions: BetaAt(b,c,i,x)Prime(S (a + i))Original native command in the exact edition
  2. L16
    apply hprefix
  3. L17
    exact hi
04Separate the logical casesL18–19

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

  1. L18
    cases hleft
  2. L19
    cases hleft_witness
05Establish hrightL20–22

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

  1. L20
    have hright : ∃ x1. BetaAt(b,c,j,x1) ∧ (Prime(S (a + j)) ∧ x1 = S (a + j) ∨ ¬Prime(S (a + j)) ∧ x1 = 1)Definitions: BetaAt(b,c,j,x1)Prime(S (a + j))Original native command in the exact edition
  2. L21
    apply hprefix
  3. L22
    exact hj
06Separate the logical casesL23–24

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

  1. L23
    cases hright
  2. L24
    cases hright_witness
07Establish hxpL25–33

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

  1. L25
    have hxp : x = p
  2. L26
    specialize beta_at_unique b
  3. L27
    specialize beta_at_unique c
  4. L28
    specialize beta_at_unique i
  5. L29
    specialize beta_at_unique x
  6. L30
    specialize beta_at_unique p
  7. L31
    apply beta_at_unique
  8. L32
    exact hleft_witness_left
  9. L33
    exact hp
08Establish hxqL34–42

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

  1. L34
    have hxq : x1 = q
  2. L35
    specialize beta_at_unique b
  3. L36
    specialize beta_at_unique c
  4. L37
    specialize beta_at_unique j
  5. L38
    specialize beta_at_unique x1
  6. L39
    specialize beta_at_unique q
  7. L40
    apply beta_at_unique
  8. L41
    exact hright_witness_left
  9. L42
    exact hq
09Separate the logical casesL43–46

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

  1. L43
    cases hleft_witness_right
  2. L44
    cases hright_witness_right
  3. L45
    cases hleft_witness_right_left
  4. L46
    cases hright_witness_right_left
10Establish hp_candidateL47–51

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

  1. L47
    have hp_candidate : p = S (a + i)
  2. L48
    trans x
  3. L49
    symm
  4. L50
    exact hxp
  5. L51
    exact hleft_witness_right_left_right
11Establish hq_candidateL52–61

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

  1. L52
    have hq_candidate : q = S (a + j)
  2. L53
    trans x1
  3. L54
    symm
  4. L55
    exact hxq
  5. L56
    exact hright_witness_right_left_right
  6. L57
    specialize distinct_primes_coprime p
  7. L58
    specialize distinct_primes_coprime q
  8. L59
    apply distinct_primes_coprime
  9. L60
    rewrite hp_candidate
  10. L61
    rewrite hp_candidate
12Use earlier factsL62–62

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

  1. L62
    exact hleft_witness_right_left_left
13Calculate and transport equalitiesL63–64

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

  1. L63
    rewrite hq_candidate
  2. L64
    rewrite hq_candidate
14Use earlier factsL65–65

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

  1. L65
    exact hright_witness_right_left_left
15Fix variables and assumptionsL66–66

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

  1. L66
    intro hpq
16Use earlier factsL67–72

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

  1. L67
    apply hij
  2. L68
    specialize add_left_cancel a
  3. L69
    specialize add_left_cancel i
  4. L70
    specialize add_left_cancel j
  5. L71
    apply add_left_cancel
  6. L72
    apply PA2
17Calculate and transport equalitiesL73–74

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

  1. L73
    trans p
  2. L74
    symm
18Use earlier factsL75–75

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

  1. L75
    exact hp_candidate
19Calculate and transport equalitiesL76–76

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

  1. L76
    trans q
20Use earlier factsL77–78

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

  1. L77
    exact hpq
  2. L78
    exact hq_candidate
21Separate the logical casesL79–80

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

  1. L79
    cases hleft_witness_right_left
  2. L80
    cases hright_witness_right_right
22Establish hp_candidateL81–85

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

  1. L81
    have hp_candidate : p = S (a + i)
  2. L82
    trans x
  3. L83
    symm
  4. L84
    exact hxp
  5. L85
    exact hleft_witness_right_left_right
23Establish hq_oneL86–93

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

  1. L86
    have hq_one : q = 1
  2. L87
    trans x1
  3. L88
    symm
  4. L89
    exact hxq
  5. L90
    exact hright_witness_right_right_right
  6. L91
    rewrite hq_one
  7. L92
    specialize coprime_one_right p
  8. L93
    exact coprime_one_right
24Separate the logical casesL94–96

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

  1. L94
    cases hright_witness_right
  2. L95
    cases hleft_witness_right_right
  3. L96
    cases hright_witness_right_left
25Establish hp_oneL97–104

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

  1. L97
    have hp_one : p = 1
  2. L98
    trans x
  3. L99
    symm
  4. L100
    exact hxp
  5. L101
    exact hleft_witness_right_right_right
  6. L102
    rewrite hp_one
  7. L103
    specialize coprime_one_left q
  8. L104
    exact coprime_one_left
26Separate the logical casesL105–106

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

  1. L105
    cases hleft_witness_right_right
  2. L106
    cases hright_witness_right_right
27Establish hp_oneL107–114

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

  1. L107
    have hp_one : p = 1
  2. L108
    trans x
  3. L109
    symm
  4. L110
    exact hxp
  5. L111
    exact hleft_witness_right_right_right
  6. L112
    rewrite hp_one
  7. L113
    specialize coprime_one_left q
  8. L114
    exact coprime_one_left

Library-wide reading audit

Original defined command ledger · 114 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro l
  5. 0005intro hprefix
  6. 0006intro i
  7. 0007intro j
  8. 0008intro p
  9. 0009intro q
  10. 0010intro hi
  11. 0011intro hj
  12. 0012intro hp
  13. 0013intro hq
  14. 0014intro hij
  15. 0015have hleft : ∃ x. BetaAt(b,c,i,x) ∧ (Prime(S (a + i)) ∧ x = S (a + i) ∨ ¬Prime(S (a + i)) ∧ x = 1)
    Exact native replay linehave hleft : exists x. (((exists bpr_height_bpipc_left_entry. bpr_height_bpipc_left_entry + S (x) = S ((S (i)) * c)) /\ exists bpr_quotient_bpipc_left_entry. b = bpr_quotient_bpipc_left_entry * S ((S (i)) * c) + (x))) /\ (((((~(S (a + i) = 1) /\ forall bpr_left_bpipc_left_choice_prime bpr_right_bpipc_left_choice_prime. S (a + i) = bpr_left_bpipc_left_choice_prime * bpr_right_bpipc_left_choice_prime -> bpr_left_bpipc_left_choice_prime = 1 \/ bpr_right_bpipc_left_choice_prime = 1)) /\ x = S (a + i)) \/ (~((~(S (a + i) = 1) /\ forall bpr_left_bpipc_left_choice_prime bpr_right_bpipc_left_choice_prime. S (a + i) = bpr_left_bpipc_left_choice_prime * bpr_right_bpipc_left_choice_prime -> bpr_left_bpipc_left_choice_prime = 1 \/ bpr_right_bpipc_left_choice_prime = 1)) /\ x = 1)))
  16. 0016apply hprefix
  17. 0017exact hi
  18. 0018cases hleft
  19. 0019cases hleft_witness
  20. 0020have hright : ∃ x1. BetaAt(b,c,j,x1) ∧ (Prime(S (a + j)) ∧ x1 = S (a + j) ∨ ¬Prime(S (a + j)) ∧ x1 = 1)
    Exact native replay linehave hright : exists x1. (((exists bpr_height_bpipc_right_entry. bpr_height_bpipc_right_entry + S (x1) = S ((S (j)) * c)) /\ exists bpr_quotient_bpipc_right_entry. b = bpr_quotient_bpipc_right_entry * S ((S (j)) * c) + (x1))) /\ (((((~(S (a + j) = 1) /\ forall bpr_left_bpipc_right_choice_prime bpr_right_bpipc_right_choice_prime. S (a + j) = bpr_left_bpipc_right_choice_prime * bpr_right_bpipc_right_choice_prime -> bpr_left_bpipc_right_choice_prime = 1 \/ bpr_right_bpipc_right_choice_prime = 1)) /\ x1 = S (a + j)) \/ (~((~(S (a + j) = 1) /\ forall bpr_left_bpipc_right_choice_prime bpr_right_bpipc_right_choice_prime. S (a + j) = bpr_left_bpipc_right_choice_prime * bpr_right_bpipc_right_choice_prime -> bpr_left_bpipc_right_choice_prime = 1 \/ bpr_right_bpipc_right_choice_prime = 1)) /\ x1 = 1)))
  21. 0021apply hprefix
  22. 0022exact hj
  23. 0023cases hright
  24. 0024cases hright_witness
  25. 0025have hxp : x = p
  26. 0026specialize beta_at_unique b
  27. 0027specialize beta_at_unique c
  28. 0028specialize beta_at_unique i
  29. 0029specialize beta_at_unique x
  30. 0030specialize beta_at_unique p
  31. 0031apply beta_at_unique
  32. 0032exact hleft_witness_left
  33. 0033exact hp
  34. 0034have hxq : x1 = q
  35. 0035specialize beta_at_unique b
  36. 0036specialize beta_at_unique c
  37. 0037specialize beta_at_unique j
  38. 0038specialize beta_at_unique x1
  39. 0039specialize beta_at_unique q
  40. 0040apply beta_at_unique
  41. 0041exact hright_witness_left
  42. 0042exact hq
  43. 0043cases hleft_witness_right
  44. 0044cases hright_witness_right
  45. 0045cases hleft_witness_right_left
  46. 0046cases hright_witness_right_left
  47. 0047have hp_candidate : p = S (a + i)
  48. 0048trans x
  49. 0049symm
  50. 0050exact hxp
  51. 0051exact hleft_witness_right_left_right
  52. 0052have hq_candidate : q = S (a + j)
  53. 0053trans x1
  54. 0054symm
  55. 0055exact hxq
  56. 0056exact hright_witness_right_left_right
  57. 0057specialize distinct_primes_coprime p
  58. 0058specialize distinct_primes_coprime q
  59. 0059apply distinct_primes_coprime
  60. 0060rewrite hp_candidate
  61. 0061rewrite hp_candidate
  62. 0062exact hleft_witness_right_left_left
  63. 0063rewrite hq_candidate
  64. 0064rewrite hq_candidate
  65. 0065exact hright_witness_right_left_left
  66. 0066intro hpq
  67. 0067apply hij
  68. 0068specialize add_left_cancel a
  69. 0069specialize add_left_cancel i
  70. 0070specialize add_left_cancel j
  71. 0071apply add_left_cancel
  72. 0072apply PA2
  73. 0073trans p
  74. 0074symm
  75. 0075exact hp_candidate
  76. 0076trans q
  77. 0077exact hpq
  78. 0078exact hq_candidate
  79. 0079cases hleft_witness_right_left
  80. 0080cases hright_witness_right_right
  81. 0081have hp_candidate : p = S (a + i)
  82. 0082trans x
  83. 0083symm
  84. 0084exact hxp
  85. 0085exact hleft_witness_right_left_right
  86. 0086have hq_one : q = 1
  87. 0087trans x1
  88. 0088symm
  89. 0089exact hxq
  90. 0090exact hright_witness_right_right_right
  91. 0091rewrite hq_one
  92. 0092specialize coprime_one_right p
  93. 0093exact coprime_one_right
  94. 0094cases hright_witness_right
  95. 0095cases hleft_witness_right_right
  96. 0096cases hright_witness_right_left
  97. 0097have hp_one : p = 1
  98. 0098trans x
  99. 0099symm
  100. 0100exact hxp
  101. 0101exact hleft_witness_right_right_right
  102. 0102rewrite hp_one
  103. 0103specialize coprime_one_left q
  104. 0104exact coprime_one_left
  105. 0105cases hleft_witness_right_right
  106. 0106cases hright_witness_right_right
  107. 0107have hp_one : p = 1
  108. 0108trans x
  109. 0109symm
  110. 0110exact hxp
  111. 0111exact hleft_witness_right_right_right
  112. 0112rewrite hp_one
  113. 0113specialize coprime_one_left q
  114. 0114exact coprime_one_left