BT00YA · Bertrand theorem

prime_square_tail_of_two_three_range

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

The scaled two-thirds range places the prime square above 2*n.

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

∀ p. ∀ n. ∀ s. Prime(p) → Lt(2,n) → Lt(n + n,p + p + p) → Pow(p,2,s) → Lt(n + n,s)

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 PD0020 Pow

5 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

8 occurrences

Exact expanded native-PA statement
forall p n s. ((~(p = 1) /\ forall frm_prime_left_bpstt_prime frm_prime_right_bpstt_prime. p = frm_prime_left_bpstt_prime * frm_prime_right_bpstt_prime -> frm_prime_left_bpstt_prime = 1 \/ frm_prime_right_bpstt_prime = 1)) -> (exists bcf_lt_gap_bpstt_positive. bcf_lt_gap_bpstt_positive + S (2) = n) -> (exists bcf_lt_gap_bpstt_scaled. bcf_lt_gap_bpstt_scaled + S (n + n) = (p + p) + p) -> (exists bpvi_b_bpstt_power bpvi_c_bpstt_power. ((forall bpvi_i_bpstt_power. (exists bpvi_repeat_gap_bpstt_power. bpvi_repeat_gap_bpstt_power + S bpvi_i_bpstt_power = 2) -> (((exists bpvi_h_bpstt_power_repeat. bpvi_h_bpstt_power_repeat + S (p) = S ((S (bpvi_i_bpstt_power)) * bpvi_c_bpstt_power)) /\ exists bpvi_q_bpstt_power_repeat. bpvi_b_bpstt_power = bpvi_q_bpstt_power_repeat * S ((S (bpvi_i_bpstt_power)) * bpvi_c_bpstt_power) + (p)))) /\ (exists bpvi_u_bpstt_power bpvi_v_bpstt_power. ((((exists bpvi_h_bpstt_power_start. bpvi_h_bpstt_power_start + S (1) = S ((S (0)) * bpvi_v_bpstt_power)) /\ exists bpvi_q_bpstt_power_start. bpvi_u_bpstt_power = bpvi_q_bpstt_power_start * S ((S (0)) * bpvi_v_bpstt_power) + (1))) /\ ((((exists bpvi_h_bpstt_power_terminal. bpvi_h_bpstt_power_terminal + S (s) = S ((S (2)) * bpvi_v_bpstt_power)) /\ exists bpvi_q_bpstt_power_terminal. bpvi_u_bpstt_power = bpvi_q_bpstt_power_terminal * S ((S (2)) * bpvi_v_bpstt_power) + (s))) /\ forall bpvi_j_bpstt_power. (exists bpvi_product_gap_bpstt_power. bpvi_product_gap_bpstt_power + S bpvi_j_bpstt_power = 2) -> exists bpvi_factor_bpstt_power bpvi_partial_bpstt_power bpvi_successor_bpstt_power. ((((exists bpvi_h_bpstt_power_factor. bpvi_h_bpstt_power_factor + S (bpvi_factor_bpstt_power) = S ((S (bpvi_j_bpstt_power)) * bpvi_c_bpstt_power)) /\ exists bpvi_q_bpstt_power_factor. bpvi_b_bpstt_power = bpvi_q_bpstt_power_factor * S ((S (bpvi_j_bpstt_power)) * bpvi_c_bpstt_power) + (bpvi_factor_bpstt_power))) /\ ((((exists bpvi_h_bpstt_power_partial. bpvi_h_bpstt_power_partial + S (bpvi_partial_bpstt_power) = S ((S (bpvi_j_bpstt_power)) * bpvi_v_bpstt_power)) /\ exists bpvi_q_bpstt_power_partial. bpvi_u_bpstt_power = bpvi_q_bpstt_power_partial * S ((S (bpvi_j_bpstt_power)) * bpvi_v_bpstt_power) + (bpvi_partial_bpstt_power))) /\ ((((exists bpvi_h_bpstt_power_successor. bpvi_h_bpstt_power_successor + S (bpvi_successor_bpstt_power) = S ((S (S bpvi_j_bpstt_power)) * bpvi_v_bpstt_power)) /\ exists bpvi_q_bpstt_power_successor. bpvi_u_bpstt_power = bpvi_q_bpstt_power_successor * S ((S (S bpvi_j_bpstt_power)) * bpvi_v_bpstt_power) + (bpvi_successor_bpstt_power))) /\ bpvi_successor_bpstt_power = bpvi_partial_bpstt_power * bpvi_factor_bpstt_power)))))))) -> (exists bcf_lt_gap_bpstt_result. bcf_lt_gap_bpstt_result + S (n + n) = s)

Proof neighborhood

Direct theorem prerequisites

BT00AW prime_is_succ_succ BT000Q zero_or_succ BT0014 add_le_add_right BT0015 add_le_add_left BT000F le_trans BT001I lt_not_le BT001L mul_le_mul_left BT000A mul_one BT001D lt_of_lt_of_le BT009W pow_two

Direct theorem dependents

BT00YE central_binom_prime_valuation_zero_two_thirds_range

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

85 script commands · 23 reading checkpoints · 12 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 (10)
prime is succ succzero or succadd le add rightadd le add leftle translt not lemul le mul leftmul onelt of lt of lepow two
01Fix variables and assumptionsL1–7

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro s
  4. L4
    intro hp
  5. L5
    intro hpositive
  6. L6
    intro hscaled
  7. L7
    intro hsquare
02Establish hshapeL8–11

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

  1. L8
    have hshape : exists k. p = S (S k)
  2. L9
    specialize prime_is_succ_succ p
  3. L10
    apply prime_is_succ_succ
  4. L11
    exact hp
03Separate the logical casesL12–12

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

  1. L12
    cases hshape
04Use earlier factsL13–13

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

  1. L13
    specialize zero_or_succ x
05Separate the logical casesL14–14

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

  1. L14
    cases zero_or_succ
06Establish hn_lowerL15–16

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

  1. L15
    have hn_lower : Lt(2,n)Definitions: Lt(2,n)Original native command in the exact edition
  2. L16
    exact hpositive
07Establish hdouble_lowerL17–17

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

  1. L17
    have hdouble_lower : Le(3 + 3,n + n)Definitions: Le(3 + 3,n + n)Original native command in the exact edition
08Establish hfirst_addL18–23

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

  1. L18
    have hfirst_add : Le(3 + 3,n + 3)Definitions: Le(3 + 3,n + 3)Original native command in the exact edition
  2. L19
    specialize add_le_add_right 3
  3. L20
    specialize add_le_add_right n
  4. L21
    specialize add_le_add_right 3
  5. L22
    apply add_le_add_right
  6. L23
    exact hn_lower
09Establish hsecond_addL24–33

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

  1. L24
    have hsecond_add : Le(n + 3,n + n)Definitions: Le(n + 3,n + n)Original native command in the exact edition
  2. L25
    specialize add_le_add_left 3
  3. L26
    specialize add_le_add_left n
  4. L27
    specialize add_le_add_left n
  5. L28
    apply add_le_add_left
  6. L29
    exact hn_lower
  7. L30
    specialize le_trans (3 + 3)
  8. L31
    specialize le_trans (n + 3)
  9. L32
    specialize le_trans (n + n)
  10. L33
    apply le_trans
10Use earlier factsL34–35

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

  1. L34
    exact hfirst_add
  2. L35
    exact hsecond_add
11Calculate and transport equalitiesL36–39

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

  1. L36
    rewrite zero_or_succ_left at hshape_witness
  2. L37
    rewrite hshape_witness at hscaled
  3. L38
    rewrite hshape_witness at hscaled
  4. L39
    rewrite hshape_witness at hscaled
12Separate the logical casesL40–40

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

  1. L40
    exfalso
13Use earlier factsL41–44

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

  1. L41
    specialize lt_not_le (n + n)
  2. L42
    specialize lt_not_le ((2 + 2) + 2)
  3. L43
    apply lt_not_le
  4. L44
    exact hscaled
14Establish hsmallL45–48

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

  1. L45
    have hsmall : (2 + 2) + 2 = 3 + 3
  2. L46
    norm_num
  3. L47
    rewrite hsmall
  4. L48
    exact hdouble_lower
15Separate the logical casesL49–49

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

  1. L49
    cases zero_or_succ_right
16Establish hp_lowerL50–50

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

  1. L50
    have hp_lower : Lt(2,p)Definitions: Lt(2,p)Original native command in the exact edition
17Construct an explicit witnessL51–51

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

  1. L51
    exists x1
18Calculate and transport equalitiesL52–54

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

  1. L52
    rewrite hshape_witness
  2. L53
    rewrite zero_or_succ_right_witness
  3. L54
    simp
19Establish hproduct_lowerL55–55

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

  1. L55
    have hproduct_lower : Le(p + p + p,p · p)Definitions: Le(p + p + p,p · p)Original native command in the exact edition
20Establish hraw_product_lowerL56–61

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

  1. L56
    have hraw_product_lower : Le(p · 3,p · p)Definitions: Le(p · 3,p · p)Original native command in the exact edition
  2. L57
    specialize mul_le_mul_left 3
  3. L58
    specialize mul_le_mul_left p
  4. L59
    specialize mul_le_mul_left p
  5. L60
    apply mul_le_mul_left
  6. L61
    exact hp_lower
21Establish htripleL62–69

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

  1. L62
    have htriple : p * 3 = (p + p) + p
  2. L63
    rewrite PA6
  3. L64
    rewrite PA6
  4. L65
    specialize mul_one p
  5. L66
    rewrite mul_one
  6. L67
    refl
  7. L68
    rewrite htriple at hraw_product_lower
  8. L69
    exact hraw_product_lower
22Establish hstrict_productL70–76

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

  1. L70
    have hstrict_product : Lt(n + n,p · p)Definitions: Lt(n + n,p · p)Original native command in the exact edition
  2. L71
    specialize lt_of_lt_of_le (n + n)
  3. L72
    specialize lt_of_lt_of_le ((p + p) + p)
  4. L73
    specialize lt_of_lt_of_le (p * p)
  5. L74
    apply lt_of_lt_of_le
  6. L75
    exact hscaled
  7. L76
    exact hproduct_lower
23Establish hsquare_valueL77–85

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

  1. L77
    have hsquare_value : s = p * p
  2. L78
    specialize pow_two p
  3. L79
    specialize pow_two 2
  4. L80
    specialize pow_two s
  5. L81
    apply pow_two
  6. L82
    refl
  7. L83
    exact hsquare
  8. L84
    rewrite hsquare_value
  9. L85
    exact hstrict_product

Library-wide reading audit

Original defined command ledger · 85 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro s
  4. 0004intro hp
  5. 0005intro hpositive
  6. 0006intro hscaled
  7. 0007intro hsquare
  8. 0008have hshape : exists k. p = S (S k)
  9. 0009specialize prime_is_succ_succ p
  10. 0010apply prime_is_succ_succ
  11. 0011exact hp
  12. 0012cases hshape
  13. 0013specialize zero_or_succ x
  14. 0014cases zero_or_succ
  15. 0015have hn_lower : Lt(2,n)
    Exact native replay linehave hn_lower : exists bcf_le_gap_bpstt_three_lower. bcf_le_gap_bpstt_three_lower + (3) = n
  16. 0016exact hpositive
  17. 0017have hdouble_lower : Le(3 + 3,n + n)
    Exact native replay linehave hdouble_lower : exists bcf_le_gap_bpstt_six_lower. bcf_le_gap_bpstt_six_lower + (3 + 3) = n + n
  18. 0018have hfirst_add : Le(3 + 3,n + 3)
    Exact native replay linehave hfirst_add : exists bcf_le_gap_bpstt_first_add. bcf_le_gap_bpstt_first_add + (3 + 3) = n + 3
  19. 0019specialize add_le_add_right 3
  20. 0020specialize add_le_add_right n
  21. 0021specialize add_le_add_right 3
  22. 0022apply add_le_add_right
  23. 0023exact hn_lower
  24. 0024have hsecond_add : Le(n + 3,n + n)
    Exact native replay linehave hsecond_add : exists bcf_le_gap_bpstt_second_add. bcf_le_gap_bpstt_second_add + (n + 3) = n + n
  25. 0025specialize add_le_add_left 3
  26. 0026specialize add_le_add_left n
  27. 0027specialize add_le_add_left n
  28. 0028apply add_le_add_left
  29. 0029exact hn_lower
  30. 0030specialize le_trans (3 + 3)
  31. 0031specialize le_trans (n + 3)
  32. 0032specialize le_trans (n + n)
  33. 0033apply le_trans
  34. 0034exact hfirst_add
  35. 0035exact hsecond_add
  36. 0036rewrite zero_or_succ_left at hshape_witness
  37. 0037rewrite hshape_witness at hscaled
  38. 0038rewrite hshape_witness at hscaled
  39. 0039rewrite hshape_witness at hscaled
  40. 0040exfalso
  41. 0041specialize lt_not_le (n + n)
  42. 0042specialize lt_not_le ((2 + 2) + 2)
  43. 0043apply lt_not_le
  44. 0044exact hscaled
  45. 0045have hsmall : (2 + 2) + 2 = 3 + 3
  46. 0046norm_num
  47. 0047rewrite hsmall
  48. 0048exact hdouble_lower
  49. 0049cases zero_or_succ_right
  50. 0050have hp_lower : Lt(2,p)
    Exact native replay linehave hp_lower : exists bcf_le_gap_bpstt_prime_lower. bcf_le_gap_bpstt_prime_lower + (3) = p
  51. 0051exists x1
  52. 0052rewrite hshape_witness
  53. 0053rewrite zero_or_succ_right_witness
  54. 0054simp
  55. 0055have hproduct_lower : Le(p + p + p,p · p)
    Exact native replay linehave hproduct_lower : exists bcf_le_gap_bpstt_product_lower. bcf_le_gap_bpstt_product_lower + ((p + p) + p) = p * p
  56. 0056have hraw_product_lower : Le(p · 3,p · p)
    Exact native replay linehave hraw_product_lower : exists bcf_le_gap_bpstt_raw_product_lower. bcf_le_gap_bpstt_raw_product_lower + (p * 3) = p * p
  57. 0057specialize mul_le_mul_left 3
  58. 0058specialize mul_le_mul_left p
  59. 0059specialize mul_le_mul_left p
  60. 0060apply mul_le_mul_left
  61. 0061exact hp_lower
  62. 0062have htriple : p * 3 = (p + p) + p
  63. 0063rewrite PA6
  64. 0064rewrite PA6
  65. 0065specialize mul_one p
  66. 0066rewrite mul_one
  67. 0067refl
  68. 0068rewrite htriple at hraw_product_lower
  69. 0069exact hraw_product_lower
  70. 0070have hstrict_product : Lt(n + n,p · p)
    Exact native replay linehave hstrict_product : exists bcf_lt_gap_bpstt_strict_product. bcf_lt_gap_bpstt_strict_product + S (n + n) = p * p
  71. 0071specialize lt_of_lt_of_le (n + n)
  72. 0072specialize lt_of_lt_of_le ((p + p) + p)
  73. 0073specialize lt_of_lt_of_le (p * p)
  74. 0074apply lt_of_lt_of_le
  75. 0075exact hscaled
  76. 0076exact hproduct_lower
  77. 0077have hsquare_value : s = p * p
  78. 0078specialize pow_two p
  79. 0079specialize pow_two 2
  80. 0080specialize pow_two s
  81. 0081apply pow_two
  82. 0082refl
  83. 0083exact hsquare
  84. 0084rewrite hsquare_value
  85. 0085exact hstrict_product