BT006N · Bertrand theorem

prime_three

Stable checked-use theorem · independently kernel verified

Three is prime in the expanded first-order prime predicate.

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

Prime(3)

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

PD0004 Prime

1 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
~(3 = 1) /\ forall a b. 3 = a * b -> a = 1 \/ b = 1

Proof neighborhood

Direct theorem prerequisites

BT0005 mul_succ_left BT0020 mul_eq_one_components BT001X add_eq_zero_left BT000M mul_eq_zero BT0004 mul_zero_left BT000Q zero_or_succ

Direct theorem dependents

BT0124 bertrand_small_closed_upper

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

94 script commands · 35 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 (6)
mul succ leftmul eq one componentsadd eq zero leftmul eq zeromul zero leftzero or succ
01Establish hlargeL1–9

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

  1. L1
    have hlarge : forall x y. ~(3 = S (S x) * S (S y))
  2. L2
    intro x
  3. L3
    intro y
  4. L4
    intro hlarge_eq
  5. L5
    specialize mul_succ_left (S x)
  6. L6
    specialize mul_succ_left (S (S y))
  7. L7
    rewrite mul_succ_left at hlarge_eq
  8. L8
    rewrite PA4 at hlarge_eq
  9. L9
    rewrite PA4 at hlarge_eq
02Establish honeL10–13

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

  1. L10
    have hone : 1 = S x * S (S y) + y
  2. L11
    apply PA2
  3. L12
    apply PA2
  4. L13
    exact hlarge_eq
03Establish hysplitL14–16

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

  1. L14
    have hysplit : y = 0 \/ exists z. y = S z
  2. L15
    specialize zero_or_succ y
  3. L16
    exact zero_or_succ
04Separate the logical casesL17–17

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

  1. L17
    cases hysplit
05Calculate and transport equalitiesL18–20

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

  1. L18
    rewrite hysplit_left at hone
  2. L19
    rewrite hysplit_left at hone
  3. L20
    rewrite PA3 at hone
06Establish hprod_oneL21–23

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

  1. L21
    have hprod_one : S x * S (S 0) = 1
  2. L22
    symm
  3. L23
    exact hone
07Establish hcomponentsL24–28

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

  1. L24
    have hcomponents : S x = 1 /\ S (S 0) = 1
  2. L25
    specialize mul_eq_one_components (S x)
  3. L26
    specialize mul_eq_one_components (S (S 0))
  4. L27
    apply mul_eq_one_components
  5. L28
    exact hprod_one
08Separate the logical casesL29–29

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

  1. L29
    cases hcomponents
09Establish h10L30–34

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

  1. L30
    have h10 : 1 = 0
  2. L31
    apply PA2
  3. L32
    exact hcomponents_right
  4. L33
    apply PA1
  5. L34
    exact h10
10Separate the logical casesL35–35

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

  1. L35
    cases hysplit_right
11Calculate and transport equalitiesL36–38

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

  1. L36
    rewrite hysplit_right_witness at hone
  2. L37
    rewrite hysplit_right_witness at hone
  3. L38
    rewrite PA4 at hone
12Establish hzeroL39–41

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

  1. L39
    have hzero : 0 = S x * S (S (S x1)) + x1
  2. L40
    apply PA2
  3. L41
    exact hone
13Establish hsumzeroL42–44

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

  1. L42
    have hsumzero : S x * S (S (S x1)) + x1 = 0
  2. L43
    symm
  3. L44
    exact hzero
14Establish hprodzeroL45–49

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

  1. L45
    have hprodzero : S x * S (S (S x1)) = 0
  2. L46
    specialize add_eq_zero_left (S x * S (S (S x1)))
  3. L47
    specialize add_eq_zero_left x1
  4. L48
    apply add_eq_zero_left
  5. L49
    exact hsumzero
15Establish hfactorsL50–54

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

  1. L50
    have hfactors : S x = 0 \/ S (S (S x1)) = 0
  2. L51
    specialize mul_eq_zero (S x)
  3. L52
    specialize mul_eq_zero (S (S (S x1)))
  4. L53
    apply mul_eq_zero
  5. L54
    exact hprodzero
16Separate the logical casesL55–55

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

  1. L55
    cases hfactors
17Use earlier factsL56–59

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

  1. L56
    apply PA1
  2. L57
    exact hfactors_left
  3. L58
    apply PA1
  4. L59
    exact hfactors_right
18Separate the logical casesL60–60

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

  1. L60
    split
19Fix variables and assumptionsL61–61

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

  1. L61
    intro h31
20Establish h20L62–67

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

  1. L62
    have h20 : 2 = 0
  2. L63
    apply PA2
  3. L64
    exact h31
  4. L65
    apply PA1
  5. L66
    exact h20
  6. L67
    intro a
21Induction on bL68–70

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

  1. L68
    induction b
  2. L69
    intro hab
  3. L70
    rewrite PA5 at hab
22Separate the logical casesL71–71

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

  1. L71
    exfalso
23Use earlier factsL72–73

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

  1. L72
    apply PA1
  2. L73
    exact hab
24Induction on bL74–75

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

  1. L74
    induction b
  2. L75
    intro hab
25Separate the logical casesL76–76

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

  1. L76
    right
26Calculate and transport equalitiesL77–77

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

  1. L77
    refl
27Induction on aL78–81

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

  1. L78
    induction a
  2. L79
    intro hab
  3. L80
    specialize mul_zero_left (S (S b))
  4. L81
    rewrite mul_zero_left at hab
28Separate the logical casesL82–82

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

  1. L82
    exfalso
29Use earlier factsL83–84

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

  1. L83
    apply PA1
  2. L84
    exact hab
30Induction on aL85–86

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

  1. L85
    induction a
  2. L86
    intro hab
31Separate the logical casesL87–87

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

  1. L87
    left
32Calculate and transport equalitiesL88–88

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

  1. L88
    refl
33Fix variables and assumptionsL89–89

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

  1. L89
    intro hab
34Separate the logical casesL90–90

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

  1. L90
    exfalso
35Use earlier factsL91–94

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

  1. L91
    specialize hlarge a
  2. L92
    specialize hlarge b
  3. L93
    apply hlarge
  4. L94
    exact hab

Library-wide reading audit

Original defined command ledger · 94 lines
  1. 0001have hlarge : forall x y. ~(3 = S (S x) * S (S y))
  2. 0002intro x
  3. 0003intro y
  4. 0004intro hlarge_eq
  5. 0005specialize mul_succ_left (S x)
  6. 0006specialize mul_succ_left (S (S y))
  7. 0007rewrite mul_succ_left at hlarge_eq
  8. 0008rewrite PA4 at hlarge_eq
  9. 0009rewrite PA4 at hlarge_eq
  10. 0010have hone : 1 = S x * S (S y) + y
  11. 0011apply PA2
  12. 0012apply PA2
  13. 0013exact hlarge_eq
  14. 0014have hysplit : y = 0 \/ exists z. y = S z
  15. 0015specialize zero_or_succ y
  16. 0016exact zero_or_succ
  17. 0017cases hysplit
  18. 0018rewrite hysplit_left at hone
  19. 0019rewrite hysplit_left at hone
  20. 0020rewrite PA3 at hone
  21. 0021have hprod_one : S x * S (S 0) = 1
  22. 0022symm
  23. 0023exact hone
  24. 0024have hcomponents : S x = 1 /\ S (S 0) = 1
  25. 0025specialize mul_eq_one_components (S x)
  26. 0026specialize mul_eq_one_components (S (S 0))
  27. 0027apply mul_eq_one_components
  28. 0028exact hprod_one
  29. 0029cases hcomponents
  30. 0030have h10 : 1 = 0
  31. 0031apply PA2
  32. 0032exact hcomponents_right
  33. 0033apply PA1
  34. 0034exact h10
  35. 0035cases hysplit_right
  36. 0036rewrite hysplit_right_witness at hone
  37. 0037rewrite hysplit_right_witness at hone
  38. 0038rewrite PA4 at hone
  39. 0039have hzero : 0 = S x * S (S (S x1)) + x1
  40. 0040apply PA2
  41. 0041exact hone
  42. 0042have hsumzero : S x * S (S (S x1)) + x1 = 0
  43. 0043symm
  44. 0044exact hzero
  45. 0045have hprodzero : S x * S (S (S x1)) = 0
  46. 0046specialize add_eq_zero_left (S x * S (S (S x1)))
  47. 0047specialize add_eq_zero_left x1
  48. 0048apply add_eq_zero_left
  49. 0049exact hsumzero
  50. 0050have hfactors : S x = 0 \/ S (S (S x1)) = 0
  51. 0051specialize mul_eq_zero (S x)
  52. 0052specialize mul_eq_zero (S (S (S x1)))
  53. 0053apply mul_eq_zero
  54. 0054exact hprodzero
  55. 0055cases hfactors
  56. 0056apply PA1
  57. 0057exact hfactors_left
  58. 0058apply PA1
  59. 0059exact hfactors_right
  60. 0060split
  61. 0061intro h31
  62. 0062have h20 : 2 = 0
  63. 0063apply PA2
  64. 0064exact h31
  65. 0065apply PA1
  66. 0066exact h20
  67. 0067intro a
  68. 0068induction b
  69. 0069intro hab
  70. 0070rewrite PA5 at hab
  71. 0071exfalso
  72. 0072apply PA1
  73. 0073exact hab
  74. 0074induction b
  75. 0075intro hab
  76. 0076right
  77. 0077refl
  78. 0078induction a
  79. 0079intro hab
  80. 0080specialize mul_zero_left (S (S b))
  81. 0081rewrite mul_zero_left at hab
  82. 0082exfalso
  83. 0083apply PA1
  84. 0084exact hab
  85. 0085induction a
  86. 0086intro hab
  87. 0087left
  88. 0088refl
  89. 0089intro hab
  90. 0090exfalso
  91. 0091specialize hlarge a
  92. 0092specialize hlarge b
  93. 0093apply hlarge
  94. 0094exact hab