BT003E · Bertrand theorem

factor_search_up_to

Stable checked-use theorem · independently kernel verified

Constructively decide whether a nonzero natural has a bounded nontrivial factor pair.

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 → (∀ x. ∀ y. Le(x,B) → n = x · y → x = 1 ∨ y = 1) ∨ (∃ x. ∃ y. Le(x,B) ∧ ¬x = 1 ∧ ¬y = 1 ∧ n = x · y)

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

2 occurrences

In local proof propositions

PD0001 Le PD0003 Dvd

4 occurrences

Exact expanded native-PA statement
forall B n. ~(n = 0) -> ((forall c d. (exists k. k + c = B) -> n = c * d -> c = 1 \/ d = 1) \/ exists c d. ((((exists k. k + c = B) /\ ~(c = 1)) /\ ~(d = 1)) /\ n = c * d))

Proof neighborhood

Direct theorem prerequisites

BT0004 mul_zero_left BT000C succ_ne_zero BT000Y le_zero BT000E le_refl BT0018 le_succ BT0022 mul_left_cancel_nonzero BT003A eq_decidable BT003B multiple_decidable_nonzero BT003D factor_property_succ

Direct theorem dependents

BT003F prime_or_composite

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

101 script commands · 49 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 (9)
mul zero leftsucc ne zerole zerole reflle succmul left cancel nonzeroeq decidablemultiple decidable nonzerofactor property succ
01Fix variables and assumptionsL1–1

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

  1. L1
    intro B
02Induction on BL2–4

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 hn
03Separate the logical casesL5–5

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

  1. L5
    left
04Fix variables and assumptionsL6–9

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

  1. L6
    intro c
  2. L7
    intro d
  3. L8
    intro hc
  4. L9
    intro hfac
05Establish hc0L10–12

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

  1. L10
    have hc0 : c = 0
  2. L11
    apply le_zero
  3. L12
    exact hc
06Separate the logical casesL13–13

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

  1. L13
    exfalso
07Use earlier factsL14–14

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

  1. L14
    apply hn
08Calculate and transport equalitiesL15–15

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

  1. L15
    trans c * d
09Use earlier factsL16–16

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

  1. L16
    exact hfac
10Calculate and transport equalitiesL17–17

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

  1. L17
    rewrite hc0
11Use earlier factsL18–18

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

  1. L18
    apply mul_zero_left
12Fix variables and assumptionsL19–20

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

  1. L19
    intro n
  2. L20
    intro hn
13Use earlier factsL21–21

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

  1. L21
    specialize IH n
14Establish hprevL22–24

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

  1. L22
    have hprev : (∀ x. ∀ y. Le(x,B) → n = x · y → x = 1 ∨ y = 1) ∨ (∃ x. ∃ y. Le(x,B) ∧ ¬x = 1 ∧ ¬y = 1 ∧ n = x · y)Definitions: Le(x,B)Original native command in the exact edition
  2. L23
    apply IH
  3. L24
    exact hn
15Separate the logical casesL25–25

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

  1. L25
    cases hprev
16Establish hs0L26–30

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

  1. L26
    have hs0 : ~(S B = 0)
  2. L27
    specialize succ_ne_zero B
  3. L28
    exact succ_ne_zero
  4. L29
    specialize multiple_decidable_nonzero (S B)
  5. L30
    specialize multiple_decidable_nonzero n
17Establish hdivL31–33

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

  1. L31
    have hdiv : Dvd(S B,n) ∨ ¬Dvd(S B,n)Definitions: Dvd(S B,n)Original native command in the exact edition
  2. L32
    apply multiple_decidable_nonzero
  3. L33
    exact hs0
18Separate the logical casesL34–35

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

  1. L34
    cases hdiv
  2. L35
    cases hdiv_left
19Use earlier factsL36–37

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

  1. L36
    specialize eq_decidable (S B)
  2. L37
    specialize eq_decidable 1
20Establish hc1L38–39

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

  1. L38
    have hc1 : S B = 1 \/ ~(S B = 1)
  2. L39
    apply eq_decidable
21Separate the logical casesL40–41

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

  1. L40
    cases hc1
  2. L41
    left
22Use earlier factsL42–43

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

  1. L42
    apply factor_property_succ
  2. L43
    exact hprev_left
23Fix variables and assumptionsL44–45

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

  1. L44
    intro d
  2. L45
    intro hboundary
24Separate the logical casesL46–46

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

  1. L46
    left
25Use earlier factsL47–49

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

  1. L47
    exact hc1_left
  2. L48
    specialize eq_decidable_before x
  3. L49
    specialize eq_decidable_before 1
26Establish hq1L50–51

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

  1. L50
    have hq1 : x = 1 \/ ~(x = 1)
  2. L51
    apply eq_decidable_before
27Separate the logical casesL52–53

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

  1. L52
    cases hq1
  2. L53
    left
28Use earlier factsL54–55

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

  1. L54
    apply factor_property_succ
  2. L55
    exact hprev_left
29Fix variables and assumptionsL56–57

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

  1. L56
    intro d
  2. L57
    intro hboundary
30Separate the logical casesL58–58

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

  1. L58
    right
31Calculate and transport equalitiesL59–59

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

  1. L59
    trans x
32Use earlier factsL60–61

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

  1. L60
    apply mul_left_cancel_nonzero
  2. L61
    exact hs0
33Calculate and transport equalitiesL62–63

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

  1. L62
    trans n
  2. L63
    symm
34Use earlier factsL64–66

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

  1. L64
    exact hboundary
  2. L65
    exact hdiv_left_witness
  3. L66
    exact hq1_left
35Separate the logical casesL67–67

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

  1. L67
    right
36Construct an explicit witnessL68–69

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

  1. L68
    exists S B
  2. L69
    exists x
37Separate the logical casesL70–72

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

  1. L70
    split
  2. L71
    split
  3. L72
    split
38Use earlier factsL73–76

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

  1. L73
    apply le_refl
  2. L74
    exact hc1_right
  3. L75
    exact hq1_right
  4. L76
    exact hdiv_left_witness
39Separate the logical casesL77–77

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

  1. L77
    left
40Use earlier factsL78–79

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

  1. L78
    apply factor_property_succ
  2. L79
    exact hprev_left
41Fix variables and assumptionsL80–81

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

  1. L80
    intro d
  2. L81
    intro hboundary
42Separate the logical casesL82–82

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

  1. L82
    exfalso
43Use earlier factsL83–83

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

  1. L83
    apply hdiv_right
44Construct an explicit witnessL84–84

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

  1. L84
    exists d
45Use earlier factsL85–85

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

  1. L85
    exact hboundary
46Separate the logical casesL86–91

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

  1. L86
    right
  2. L87
    cases hprev_right
  3. L88
    cases hprev_right_witness
  4. L89
    cases hprev_right_witness_witness
  5. L90
    cases hprev_right_witness_witness_left
  6. L91
    cases hprev_right_witness_witness_left_left
47Construct an explicit witnessL92–93

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

  1. L92
    exists x
  2. L93
    exists x1
48Separate the logical casesL94–96

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

  1. L94
    split
  2. L95
    split
  3. L96
    split
49Use earlier factsL97–101

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

  1. L97
    apply le_succ
  2. L98
    exact hprev_right_witness_witness_left_left_left
  3. L99
    exact hprev_right_witness_witness_left_left_right
  4. L100
    exact hprev_right_witness_witness_left_right
  5. L101
    exact hprev_right_witness_witness_right

Library-wide reading audit

Original defined command ledger · 101 lines
  1. 0001intro B
  2. 0002induction B
  3. 0003intro n
  4. 0004intro hn
  5. 0005left
  6. 0006intro c
  7. 0007intro d
  8. 0008intro hc
  9. 0009intro hfac
  10. 0010have hc0 : c = 0
  11. 0011apply le_zero
  12. 0012exact hc
  13. 0013exfalso
  14. 0014apply hn
  15. 0015trans c * d
  16. 0016exact hfac
  17. 0017rewrite hc0
  18. 0018apply mul_zero_left
  19. 0019intro n
  20. 0020intro hn
  21. 0021specialize IH n
  22. 0022have hprev : (∀ x. ∀ y. Le(x,B) → n = x · y → x = 1 ∨ y = 1) ∨ (∃ x. ∃ y. Le(x,B) ∧ ¬x = 1 ∧ ¬y = 1 ∧ n = x · y)
    Exact native replay linehave hprev : (forall c d. (exists k. k + c = B) -> n = c * d -> c = 1 \/ d = 1) \/ exists c d. ((((exists k. k + c = B) /\ ~(c = 1)) /\ ~(d = 1)) /\ n = c * d)
  23. 0023apply IH
  24. 0024exact hn
  25. 0025cases hprev
  26. 0026have hs0 : ~(S B = 0)
  27. 0027specialize succ_ne_zero B
  28. 0028exact succ_ne_zero
  29. 0029specialize multiple_decidable_nonzero (S B)
  30. 0030specialize multiple_decidable_nonzero n
  31. 0031have hdiv : Dvd(S B,n) ∨ ¬Dvd(S B,n)
    Exact native replay linehave hdiv : (exists q. n = S B * q) \/ ~(exists q. n = S B * q)
  32. 0032apply multiple_decidable_nonzero
  33. 0033exact hs0
  34. 0034cases hdiv
  35. 0035cases hdiv_left
  36. 0036specialize eq_decidable (S B)
  37. 0037specialize eq_decidable 1
  38. 0038have hc1 : S B = 1 \/ ~(S B = 1)
  39. 0039apply eq_decidable
  40. 0040cases hc1
  41. 0041left
  42. 0042apply factor_property_succ
  43. 0043exact hprev_left
  44. 0044intro d
  45. 0045intro hboundary
  46. 0046left
  47. 0047exact hc1_left
  48. 0048specialize eq_decidable_before x
  49. 0049specialize eq_decidable_before 1
  50. 0050have hq1 : x = 1 \/ ~(x = 1)
  51. 0051apply eq_decidable_before
  52. 0052cases hq1
  53. 0053left
  54. 0054apply factor_property_succ
  55. 0055exact hprev_left
  56. 0056intro d
  57. 0057intro hboundary
  58. 0058right
  59. 0059trans x
  60. 0060apply mul_left_cancel_nonzero
  61. 0061exact hs0
  62. 0062trans n
  63. 0063symm
  64. 0064exact hboundary
  65. 0065exact hdiv_left_witness
  66. 0066exact hq1_left
  67. 0067right
  68. 0068exists S B
  69. 0069exists x
  70. 0070split
  71. 0071split
  72. 0072split
  73. 0073apply le_refl
  74. 0074exact hc1_right
  75. 0075exact hq1_right
  76. 0076exact hdiv_left_witness
  77. 0077left
  78. 0078apply factor_property_succ
  79. 0079exact hprev_left
  80. 0080intro d
  81. 0081intro hboundary
  82. 0082exfalso
  83. 0083apply hdiv_right
  84. 0084exists d
  85. 0085exact hboundary
  86. 0086right
  87. 0087cases hprev_right
  88. 0088cases hprev_right_witness
  89. 0089cases hprev_right_witness_witness
  90. 0090cases hprev_right_witness_witness_left
  91. 0091cases hprev_right_witness_witness_left_left
  92. 0092exists x
  93. 0093exists x1
  94. 0094split
  95. 0095split
  96. 0096split
  97. 0097apply le_succ
  98. 0098exact hprev_right_witness_witness_left_left_left
  99. 0099exact hprev_right_witness_witness_left_left_right
  100. 0100exact hprev_right_witness_witness_left_right
  101. 0101exact hprev_right_witness_witness_right