BT0118 · Bertrand theorem

nonprime_has_small_prime_divisor_below_square

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

Every composite below (B+1)^2 has a prime divisor at most B.

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. ∀ n. ¬n = 0 → ¬n = 1 → Lt(n,S B · S B) → ¬Prime(n) → ∃ x. Prime(x) ∧ (Le(x,B) ∧ Dvd(x,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

PD0001 Le PD0002 Lt PD0003 Dvd PD0004 Prime

5 occurrences

In local proof propositions

PD0001 Le PD0003 Dvd PD0004 Prime

9 occurrences

Exact expanded native-PA statement
forall B n. ~(n = 0) -> ~(n = 1) -> (exists bpr_gap_bb8npsp_square. bpr_gap_bb8npsp_square + S (n) = S B * S B) -> ~((~(n = 1) /\ forall bpr_left_bb8npsp_source bpr_right_bb8npsp_source. n = bpr_left_bb8npsp_source * bpr_right_bb8npsp_source -> bpr_left_bb8npsp_source = 1 \/ bpr_right_bb8npsp_source = 1)) -> (exists p. ((~(p = 1) /\ forall bpr_left_bb8npsp_prime bpr_right_bb8npsp_prime. p = bpr_left_bb8npsp_prime * bpr_right_bb8npsp_prime -> bpr_left_bb8npsp_prime = 1 \/ bpr_right_bb8npsp_prime = 1)) /\ ((exists bpr_le_gap_bb8npsp_bound. bpr_le_gap_bb8npsp_bound + (p) = (B)) /\ (exists bpr_quotient_bb8npsp_divides. n = (p) * bpr_quotient_bb8npsp_divides)))

Proof neighborhood

Direct theorem prerequisites

BT003F prime_or_composite BT0117 factor_pair_has_small_member_below_square BT0004 mul_zero_left BT003L prime_divisor_exists BT002D divisor_le_nonzero BT000F le_trans BT002C multiple_trans BT0006 mul_comm

Direct theorem dependents

BT0119 prime_of_no_small_prime_divisor_below_square

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

106 script commands · 31 reading checkpoints · 9 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)
prime or compositefactor pair has small member below squaremul zero leftprime divisor existsdivisor le nonzerole transmultiple transmul comm
01Fix variables and assumptionsL1–6

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

  1. L1
    intro B
  2. L2
    intro n
  3. L3
    intro hn0
  4. L4
    intro hn1
  5. L5
    intro hbound
  6. L6
    intro hnotprime
02Use earlier factsL7–7

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

  1. L7
    specialize prime_or_composite n
03Establish hkindL8–11

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

  1. L8
    have hkind : Prime(n) ∨ (∃ x. ∃ y. ¬x = 1 ∧ ¬y = 1 ∧ n = x · y)Definitions: Prime(n)Original native command in the exact edition
  2. L9
    apply prime_or_composite
  3. L10
    exact hn0
  4. L11
    exact hn1
04Separate the logical casesL12–13

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

  1. L12
    cases hkind
  2. L13
    exfalso
05Use earlier factsL14–15

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

  1. L14
    apply hnotprime
  2. L15
    exact hkind_left
06Separate the logical casesL16–19

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

  1. L16
    cases hkind_right
  2. L17
    cases hkind_right_witness
  3. L18
    cases hkind_right_witness_witness
  4. L19
    cases hkind_right_witness_witness_left
07Establish hsmallL20–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor pair has small member below square.

  1. L20
    have hsmall : Le(x,B) ∨ Le(x1,B)Definitions: Le(x,B)Le(x1,B)Original native command in the exact edition
  2. L21
    specialize factor_pair_has_small_member_below_square B
  3. L22
    specialize factor_pair_has_small_member_below_square n
  4. L23
    specialize factor_pair_has_small_member_below_square x
  5. L24
    specialize factor_pair_has_small_member_below_square x1
  6. L25
    apply factor_pair_has_small_member_below_square
  7. L26
    exact hkind_right_witness_witness_right
  8. L27
    exact hbound
08Separate the logical casesL28–28

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

  1. L28
    cases hsmall
09Establish hx0L29–35

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

  1. L29
    have hx0 : ~(x = 0)
  2. L30
    intro hx0_source
  3. L31
    apply hn0
  4. L32
    trans x * x1
  5. L33
    exact hkind_right_witness_witness_right
  6. L34
    rewrite hx0_source
  7. L35
    apply mul_zero_left
10Establish hpL36–40

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

  1. L36
    have hp : ∃ p. Prime(p) ∧ Dvd(p,x)Definitions: Prime(p)Dvd(p,x)Original native command in the exact edition
  2. L37
    specialize prime_divisor_exists x
  3. L38
    apply prime_divisor_exists
  4. L39
    exact hx0
  5. L40
    exact hkind_right_witness_witness_left_left
11Separate the logical casesL41–42

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

  1. L41
    cases hp
  2. L42
    cases hp_witness
12Construct an explicit witnessL43–43

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

  1. L43
    exists x2
13Separate the logical casesL44–44

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

  1. L44
    split
14Use earlier factsL45–45

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

  1. L45
    exact hp_witness_left
15Separate the logical casesL46–46

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

  1. L46
    split
16Establish hpxL47–56

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

  1. L47
  2. L48
    specialize divisor_le_nonzero x2
  3. L49
    specialize divisor_le_nonzero x
  4. L50
    apply divisor_le_nonzero
  5. L51
    exact hx0
  6. L52
    exact hp_witness_right
  7. L53
    specialize le_trans x2
  8. L54
    specialize le_trans x
  9. L55
    specialize le_trans B
  10. L56
    apply le_trans
17Use earlier factsL57–62

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

  1. L57
    exact hpx
  2. L58
    exact hsmall_left
  3. L59
    specialize multiple_trans x
  4. L60
    specialize multiple_trans x2
  5. L61
    specialize multiple_trans n
  6. L62
    apply multiple_trans
18Construct an explicit witnessL63–63

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

  1. L63
    exists x1
19Use earlier factsL64–65

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

  1. L64
    exact hkind_right_witness_witness_right
  2. L65
    exact hp_witness_right
20Establish hswapL66–69

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

  1. L66
    have hswap : n = x1 * x
  2. L67
    trans x * x1
  3. L68
    exact hkind_right_witness_witness_right
  4. L69
    apply mul_comm
21Establish hx10L70–76

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

  1. L70
    have hx10 : ~(x1 = 0)
  2. L71
    intro hx10_source
  3. L72
    apply hn0
  4. L73
    trans x1 * x
  5. L74
    exact hswap
  6. L75
    rewrite hx10_source
  7. L76
    apply mul_zero_left
22Establish hpL77–81

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

  1. L77
    have hp : ∃ p. Prime(p) ∧ Dvd(p,x1)Definitions: Prime(p)Dvd(p,x1)Original native command in the exact edition
  2. L78
    specialize prime_divisor_exists x1
  3. L79
    apply prime_divisor_exists
  4. L80
    exact hx10
  5. L81
    exact hkind_right_witness_witness_left_right
23Separate the logical casesL82–83

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

  1. L82
    cases hp
  2. L83
    cases hp_witness
24Construct an explicit witnessL84–84

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

  1. L84
    exists x2
25Separate the logical casesL85–85

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

  1. L85
    split
26Use earlier factsL86–86

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

  1. L86
    exact hp_witness_left
27Separate the logical casesL87–87

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

  1. L87
    split
28Establish hpxL88–97

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

  1. L88
  2. L89
    specialize divisor_le_nonzero x2
  3. L90
    specialize divisor_le_nonzero x1
  4. L91
    apply divisor_le_nonzero
  5. L92
    exact hx10
  6. L93
    exact hp_witness_right
  7. L94
    specialize le_trans x2
  8. L95
    specialize le_trans x1
  9. L96
    specialize le_trans B
  10. L97
    apply le_trans
29Use earlier factsL98–103

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

  1. L98
    exact hpx
  2. L99
    exact hsmall_right
  3. L100
    specialize multiple_trans x1
  4. L101
    specialize multiple_trans x2
  5. L102
    specialize multiple_trans n
  6. L103
    apply multiple_trans
30Construct an explicit witnessL104–104

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

  1. L104
    exists x
31Use earlier factsL105–106

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

  1. L105
    exact hswap
  2. L106
    exact hp_witness_right

Library-wide reading audit

Original defined command ledger · 106 lines
  1. 0001intro B
  2. 0002intro n
  3. 0003intro hn0
  4. 0004intro hn1
  5. 0005intro hbound
  6. 0006intro hnotprime
  7. 0007specialize prime_or_composite n
  8. 0008have hkind : Prime(n) ∨ (∃ x. ∃ y. ¬x = 1 ∧ ¬y = 1 ∧ n = x · y)
    Exact native replay linehave hkind : ((~(n = 1) /\ forall a b. n = a * b -> a = 1 \/ b = 1) \/ exists c d. ((~(c = 1) /\ ~(d = 1)) /\ n = c * d))
  9. 0009apply prime_or_composite
  10. 0010exact hn0
  11. 0011exact hn1
  12. 0012cases hkind
  13. 0013exfalso
  14. 0014apply hnotprime
  15. 0015exact hkind_left
  16. 0016cases hkind_right
  17. 0017cases hkind_right_witness
  18. 0018cases hkind_right_witness_witness
  19. 0019cases hkind_right_witness_witness_left
  20. 0020have hsmall : Le(x,B) ∨ Le(x1,B)
    Exact native replay linehave hsmall : (exists k. k + x = B) \/ (exists k. k + x1 = B)
  21. 0021specialize factor_pair_has_small_member_below_square B
  22. 0022specialize factor_pair_has_small_member_below_square n
  23. 0023specialize factor_pair_has_small_member_below_square x
  24. 0024specialize factor_pair_has_small_member_below_square x1
  25. 0025apply factor_pair_has_small_member_below_square
  26. 0026exact hkind_right_witness_witness_right
  27. 0027exact hbound
  28. 0028cases hsmall
  29. 0029have hx0 : ~(x = 0)
  30. 0030intro hx0_source
  31. 0031apply hn0
  32. 0032trans x * x1
  33. 0033exact hkind_right_witness_witness_right
  34. 0034rewrite hx0_source
  35. 0035apply mul_zero_left
  36. 0036have hp : ∃ p. Prime(p) ∧ Dvd(p,x)
    Exact native replay linehave hp : exists p. ((~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) /\ exists q. x = p * q)
  37. 0037specialize prime_divisor_exists x
  38. 0038apply prime_divisor_exists
  39. 0039exact hx0
  40. 0040exact hkind_right_witness_witness_left_left
  41. 0041cases hp
  42. 0042cases hp_witness
  43. 0043exists x2
  44. 0044split
  45. 0045exact hp_witness_left
  46. 0046split
  47. 0047have hpx : Le(x2,x)
    Exact native replay linehave hpx : exists k. k + x2 = x
  48. 0048specialize divisor_le_nonzero x2
  49. 0049specialize divisor_le_nonzero x
  50. 0050apply divisor_le_nonzero
  51. 0051exact hx0
  52. 0052exact hp_witness_right
  53. 0053specialize le_trans x2
  54. 0054specialize le_trans x
  55. 0055specialize le_trans B
  56. 0056apply le_trans
  57. 0057exact hpx
  58. 0058exact hsmall_left
  59. 0059specialize multiple_trans x
  60. 0060specialize multiple_trans x2
  61. 0061specialize multiple_trans n
  62. 0062apply multiple_trans
  63. 0063exists x1
  64. 0064exact hkind_right_witness_witness_right
  65. 0065exact hp_witness_right
  66. 0066have hswap : n = x1 * x
  67. 0067trans x * x1
  68. 0068exact hkind_right_witness_witness_right
  69. 0069apply mul_comm
  70. 0070have hx10 : ~(x1 = 0)
  71. 0071intro hx10_source
  72. 0072apply hn0
  73. 0073trans x1 * x
  74. 0074exact hswap
  75. 0075rewrite hx10_source
  76. 0076apply mul_zero_left
  77. 0077have hp : ∃ p. Prime(p) ∧ Dvd(p,x1)
    Exact native replay linehave hp : exists p. ((~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) /\ exists q. x1 = p * q)
  78. 0078specialize prime_divisor_exists x1
  79. 0079apply prime_divisor_exists
  80. 0080exact hx10
  81. 0081exact hkind_right_witness_witness_left_right
  82. 0082cases hp
  83. 0083cases hp_witness
  84. 0084exists x2
  85. 0085split
  86. 0086exact hp_witness_left
  87. 0087split
  88. 0088have hpx : Le(x2,x1)
    Exact native replay linehave hpx : exists k. k + x2 = x1
  89. 0089specialize divisor_le_nonzero x2
  90. 0090specialize divisor_le_nonzero x1
  91. 0091apply divisor_le_nonzero
  92. 0092exact hx10
  93. 0093exact hp_witness_right
  94. 0094specialize le_trans x2
  95. 0095specialize le_trans x1
  96. 0096specialize le_trans B
  97. 0097apply le_trans
  98. 0098exact hpx
  99. 0099exact hsmall_right
  100. 0100specialize multiple_trans x1
  101. 0101specialize multiple_trans x2
  102. 0102specialize multiple_trans n
  103. 0103apply multiple_trans
  104. 0104exists x
  105. 0105exact hswap
  106. 0106exact hp_witness_right