BT003H · Bertrand theorem

prime_decidable

Stable checked-use theorem · independently kernel verified

Primality of every natural number is constructively decidable.

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

∀ n. Prime(n) ∨ ¬Prime(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

PD0004 Prime

2 occurrences

In local proof propositions

PD0004 Prime

1 occurrences

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

Proof neighborhood

Direct theorem prerequisites

BT003A eq_decidable BT003F prime_or_composite BT003G prime_nonzero

Direct theorem dependents

BT00PR prime_strictly_above_decidable BT00U5 primorial_factor_choice_exists BT00YN prime_contribution_choice_exists 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

47 script commands · 21 reading checkpoints · 4 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 (3)
eq decidableprime or compositeprime nonzero
01Fix variables and assumptionsL1–1

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

  1. L1
    intro n
02Use earlier factsL2–3

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

  1. L2
    specialize eq_decidable n
  2. L3
    specialize eq_decidable 0
03Establish hn0L4–5

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

  1. L4
    have hn0 : n = 0 \/ ~(n = 0)
  2. L5
    apply eq_decidable
04Separate the logical casesL6–7

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

  1. L6
    cases hn0
  2. L7
    right
05Fix variables and assumptionsL8–8

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

  1. L8
    intro hp
06Use earlier factsL9–14

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

  1. L9
    specialize prime_nonzero n
  2. L10
    apply prime_nonzero
  3. L11
    exact hp
  4. L12
    exact hn0_left
  5. L13
    specialize eq_decidable_before n
  6. L14
    specialize eq_decidable_before 1
07Establish hn1L15–16

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

  1. L15
    have hn1 : n = 1 \/ ~(n = 1)
  2. L16
    apply eq_decidable_before
08Separate the logical casesL17–18

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

  1. L17
    cases hn1
  2. L18
    right
09Fix variables and assumptionsL19–19

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

  1. L19
    intro hp
10Separate the logical casesL20–20

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

  1. L20
    cases hp
11Use earlier factsL21–23

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

  1. L21
    apply hp_left
  2. L22
    exact hn1_left
  3. L23
    specialize prime_or_composite n
12Establish hkindL24–27

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

  1. L24
    have hkind : Prime(n) ∨ (∃ x. ∃ y. ¬x = 1 ∧ ¬y = 1 ∧ n = x · y)Definitions: Prime(n)Original native command in the exact edition
  2. L25
    apply prime_or_composite
  3. L26
    exact hn0_right
  4. L27
    exact hn1_right
13Separate the logical casesL28–29

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

  1. L28
    cases hkind
  2. L29
    left
14Use earlier factsL30–30

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

  1. L30
    exact hkind_left
15Separate the logical casesL31–31

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

  1. L31
    right
16Fix variables and assumptionsL32–32

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

  1. L32
    intro hp
17Separate the logical casesL33–37

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

  1. L33
    cases hp
  2. L34
    cases hkind_right
  3. L35
    cases hkind_right_witness
  4. L36
    cases hkind_right_witness_witness
  5. L37
    cases hkind_right_witness_witness_left
18Use earlier factsL38–39

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

  1. L38
    specialize hp_right x
  2. L39
    specialize hp_right x1
19Establish hunitL40–42

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

  1. L40
    have hunit : x = 1 \/ x1 = 1
  2. L41
    apply hp_right
  3. L42
    exact hkind_right_witness_witness_right
20Separate the logical casesL43–43

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

  1. L43
    cases hunit
21Use earlier factsL44–47

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

  1. L44
    apply hkind_right_witness_witness_left_left
  2. L45
    exact hunit_left
  3. L46
    apply hkind_right_witness_witness_left_right
  4. L47
    exact hunit_right

Library-wide reading audit

Original defined command ledger · 47 lines
  1. 0001intro n
  2. 0002specialize eq_decidable n
  3. 0003specialize eq_decidable 0
  4. 0004have hn0 : n = 0 \/ ~(n = 0)
  5. 0005apply eq_decidable
  6. 0006cases hn0
  7. 0007right
  8. 0008intro hp
  9. 0009specialize prime_nonzero n
  10. 0010apply prime_nonzero
  11. 0011exact hp
  12. 0012exact hn0_left
  13. 0013specialize eq_decidable_before n
  14. 0014specialize eq_decidable_before 1
  15. 0015have hn1 : n = 1 \/ ~(n = 1)
  16. 0016apply eq_decidable_before
  17. 0017cases hn1
  18. 0018right
  19. 0019intro hp
  20. 0020cases hp
  21. 0021apply hp_left
  22. 0022exact hn1_left
  23. 0023specialize prime_or_composite n
  24. 0024have 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))
  25. 0025apply prime_or_composite
  26. 0026exact hn0_right
  27. 0027exact hn1_right
  28. 0028cases hkind
  29. 0029left
  30. 0030exact hkind_left
  31. 0031right
  32. 0032intro hp
  33. 0033cases hp
  34. 0034cases hkind_right
  35. 0035cases hkind_right_witness
  36. 0036cases hkind_right_witness_witness
  37. 0037cases hkind_right_witness_witness_left
  38. 0038specialize hp_right x
  39. 0039specialize hp_right x1
  40. 0040have hunit : x = 1 \/ x1 = 1
  41. 0041apply hp_right
  42. 0042exact hkind_right_witness_witness_right
  43. 0043cases hunit
  44. 0044apply hkind_right_witness_witness_left_left
  45. 0045exact hunit_left
  46. 0046apply hkind_right_witness_witness_left_right
  47. 0047exact hunit_right