BT003K · Bertrand theorem

prime_divisor_exists_up_to

Stable checked-use theorem · independently kernel verified

Bounded strong induction constructs a prime divisor of every nonzero nonunit natural.

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

3 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0003 Dvd PD0004 Prime

6 occurrences

Exact expanded native-PA statement
forall B n. (exists t. t + n = B) -> ~(n = 0) -> ~(n = 1) -> exists p. ((~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) /\ exists k. n = p * k)

Proof neighborhood

Direct theorem prerequisites

BT0004 mul_zero_left BT000Y le_zero BT001D lt_of_lt_of_le BT0017 le_of_succ_le_succ BT0028 multiple_refl BT002C multiple_trans BT003F prime_or_composite BT003J proper_factor_lt

Direct theorem dependents

BT003L prime_divisor_exists

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

71 script commands · 23 reading checkpoints · 6 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)
mul zero leftle zerolt of lt of lele of succ le succmultiple reflmultiple transprime or compositeproper factor lt
01Fix variables and assumptionsL1–1

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

  1. L1
    intro B
02Induction on BL2–6

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

  1. L2
    induction B
  2. L3
    intro n
  3. L4
    intro hnB
  4. L5
    intro hn0
  5. L6
    intro hn1
03Separate the logical casesL7–7

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

  1. L7
    exfalso
04Use earlier factsL8–10

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

  1. L8
    apply hn0
  2. L9
    apply le_zero
  3. L10
    exact hnB
05Fix variables and assumptionsL11–14

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

  1. L11
    intro n
  2. L12
    intro hnB
  3. L13
    intro hn0
  4. L14
    intro hn1
06Use earlier factsL15–15

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

  1. L15
    specialize prime_or_composite n
07Establish hpcL16–19

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

  1. L16
    have hpc : Prime(n) ∨ (∃ x. ∃ y. ¬x = 1 ∧ ¬y = 1 ∧ n = x · y)Definitions: Prime(n)Original native command in the exact edition
  2. L17
    apply prime_or_composite
  3. L18
    exact hn0
  4. L19
    exact hn1
08Separate the logical casesL20–20

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

  1. L20
    cases hpc
09Construct an explicit witnessL21–21

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

  1. L21
    exists n
10Separate the logical casesL22–22

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

  1. L22
    split
11Use earlier factsL23–24

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

  1. L23
    exact hpc_left
  2. L24
    apply multiple_refl
12Separate the logical casesL25–28

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

  1. L25
    cases hpc_right
  2. L26
    cases hpc_right_witness
  3. L27
    cases hpc_right_witness_witness
  4. L28
    cases hpc_right_witness_witness_left
13Establish hc0L29–35

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

  1. L29
    have hc0 : ~(x = 0)
  2. L30
    intro hc
  3. L31
    apply hn0
  4. L32
    trans x * x1
  5. L33
    exact hpc_right_witness_witness_right
  6. L34
    rewrite hc
  7. L35
    apply mul_zero_left
14Establish hcnL36–43

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

  1. L36
  2. L37
    specialize proper_factor_lt n
  3. L38
    specialize proper_factor_lt x
  4. L39
    specialize proper_factor_lt x1
  5. L40
    apply proper_factor_lt
  6. L41
    exact hn0
  7. L42
    exact hpc_right_witness_witness_right
  8. L43
    exact hpc_right_witness_witness_left_right
15Establish hcSBL44–50

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

  1. L44
  2. L45
    specialize lt_of_lt_of_le x
  3. L46
    specialize lt_of_lt_of_le n
  4. L47
    specialize lt_of_lt_of_le (S B)
  5. L48
    apply lt_of_lt_of_le
  6. L49
    exact hcn
  7. L50
    exact hnB
16Establish hcBL51–54

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

  1. L51
  2. L52
    apply le_of_succ_le_succ
  3. L53
    exact hcSB
  4. L54
    specialize IH x
17Establish hpL55–59

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

  1. L55
    have hp : ∃ p. Prime(p) ∧ Dvd(p,x)Definitions: Prime(p)Dvd(p,x)Original native command in the exact edition
  2. L56
    apply IH
  3. L57
    exact hcB
  4. L58
    exact hc0
  5. L59
    exact hpc_right_witness_witness_left_left
18Separate the logical casesL60–61

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

  1. L60
    cases hp
  2. L61
    cases hp_witness
19Construct an explicit witnessL62–62

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

  1. L62
    exists x2
20Separate the logical casesL63–63

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

  1. L63
    split
21Use earlier factsL64–68

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

  1. L64
    exact hp_witness_left
  2. L65
    specialize multiple_trans x
  3. L66
    specialize multiple_trans x2
  4. L67
    specialize multiple_trans n
  5. L68
    apply multiple_trans
22Construct an explicit witnessL69–69

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

  1. L69
    exists x1
23Use earlier factsL70–71

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

  1. L70
    exact hpc_right_witness_witness_right
  2. L71
    exact hp_witness_right

Library-wide reading audit

Original defined command ledger · 71 lines
  1. 0001intro B
  2. 0002induction B
  3. 0003intro n
  4. 0004intro hnB
  5. 0005intro hn0
  6. 0006intro hn1
  7. 0007exfalso
  8. 0008apply hn0
  9. 0009apply le_zero
  10. 0010exact hnB
  11. 0011intro n
  12. 0012intro hnB
  13. 0013intro hn0
  14. 0014intro hn1
  15. 0015specialize prime_or_composite n
  16. 0016have hpc : Prime(n) ∨ (∃ x. ∃ y. ¬x = 1 ∧ ¬y = 1 ∧ n = x · y)
    Exact native replay linehave hpc : (~(n = 1) /\ forall a b. n = a * b -> a = 1 \/ b = 1) \/ exists c d. ((~(c = 1) /\ ~(d = 1)) /\ n = c * d)
  17. 0017apply prime_or_composite
  18. 0018exact hn0
  19. 0019exact hn1
  20. 0020cases hpc
  21. 0021exists n
  22. 0022split
  23. 0023exact hpc_left
  24. 0024apply multiple_refl
  25. 0025cases hpc_right
  26. 0026cases hpc_right_witness
  27. 0027cases hpc_right_witness_witness
  28. 0028cases hpc_right_witness_witness_left
  29. 0029have hc0 : ~(x = 0)
  30. 0030intro hc
  31. 0031apply hn0
  32. 0032trans x * x1
  33. 0033exact hpc_right_witness_witness_right
  34. 0034rewrite hc
  35. 0035apply mul_zero_left
  36. 0036have hcn : Lt(x,n)
    Exact native replay linehave hcn : exists k. k + S x = n
  37. 0037specialize proper_factor_lt n
  38. 0038specialize proper_factor_lt x
  39. 0039specialize proper_factor_lt x1
  40. 0040apply proper_factor_lt
  41. 0041exact hn0
  42. 0042exact hpc_right_witness_witness_right
  43. 0043exact hpc_right_witness_witness_left_right
  44. 0044have hcSB : Lt(x,S B)
    Exact native replay linehave hcSB : exists k. k + S x = S B
  45. 0045specialize lt_of_lt_of_le x
  46. 0046specialize lt_of_lt_of_le n
  47. 0047specialize lt_of_lt_of_le (S B)
  48. 0048apply lt_of_lt_of_le
  49. 0049exact hcn
  50. 0050exact hnB
  51. 0051have hcB : Le(x,B)
    Exact native replay linehave hcB : exists k. k + x = B
  52. 0052apply le_of_succ_le_succ
  53. 0053exact hcSB
  54. 0054specialize IH x
  55. 0055have 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 k. x = p * k)
  56. 0056apply IH
  57. 0057exact hcB
  58. 0058exact hc0
  59. 0059exact hpc_right_witness_witness_left_left
  60. 0060cases hp
  61. 0061cases hp_witness
  62. 0062exists x2
  63. 0063split
  64. 0064exact hp_witness_left
  65. 0065specialize multiple_trans x
  66. 0066specialize multiple_trans x2
  67. 0067specialize multiple_trans n
  68. 0068apply multiple_trans
  69. 0069exists x1
  70. 0070exact hpc_right_witness_witness_right
  71. 0071exact hp_witness_right