TS0020 · theorem body

prime_is_two_or_odd

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

Every prime is constructively either the exceptional prime two or an odd number.

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

∀ p. Prime(p) → p = 2 ∨ Odd(p)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0004 Prime PD0010 Odd

In local proof propositions

none
Exact expanded first-order statement
forall p. ((~(p = 1) /\ forall frm_prime_left_ftsc_prime frm_prime_right_ftsc_prime. p = frm_prime_left_ftsc_prime * frm_prime_right_ftsc_prime -> frm_prime_left_ftsc_prime = 1 \/ frm_prime_right_ftsc_prime = 1)) -> (p = 2 \/ (exists ftsc_odd_ftsc_prime. (p) = 2 * ftsc_odd_ftsc_prime + 1))

Proof neighborhood

Direct theorem prerequisites

parity_cases · Stable closed mul_one · Stable closed

Direct theorem dependents

TS0021 prime_mod_four_trichotomy

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

26 script commands · 10 reading checkpoints · 2 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.

01Fix variables and assumptionsL1–2

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

  1. L1
    intro p
  2. L2
    intro hprime
02Separate the logical casesL3–3

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

  1. L3
    cases hprime
03Use earlier factsL4–4

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

  1. L4
    specialize parity_cases p
04Separate the logical casesL5–7

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

  1. L5
    cases parity_cases
  2. L6
    cases parity_cases_witness
  3. L7
    left
05Establish hfactorL8–12

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

  1. L8
    have hfactor : 2 = 1 \/ x = 1
  2. L9
    specialize hprime_right 2
  3. L10
    specialize hprime_right x
  4. L11
    apply hprime_right
  5. L12
    exact parity_cases_witness_left
06Separate the logical casesL13–14

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

  1. L13
    cases hfactor
  2. L14
    exfalso
07Establish hzeroL15–23

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

  1. L15
    have hzero : 1 = 0
  2. L16
    apply PA2
  3. L17
    exact hfactor_left
  4. L18
    apply PA1
  5. L19
    exact hzero
  6. L20
    rewrite hfactor_right at parity_cases_witness_left
  7. L21
    specialize mul_one 2
  8. L22
    rewrite mul_one at parity_cases_witness_left
  9. L23
    exact parity_cases_witness_left
08Separate the logical casesL24–24

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

  1. L24
    right
09Construct an explicit witnessL25–25

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

  1. L25
    exists x
10Use earlier factsL26–26

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

  1. L26
    exact parity_cases_witness_right

Library-wide reading audit

Original defined command ledger · 26 lines
  1. 0001intro p
  2. 0002intro hprime
  3. 0003cases hprime
  4. 0004specialize parity_cases p
  5. 0005cases parity_cases
  6. 0006cases parity_cases_witness
  7. 0007left
  8. 0008have hfactor : 2 = 1 \/ x = 1
  9. 0009specialize hprime_right 2
  10. 0010specialize hprime_right x
  11. 0011apply hprime_right
  12. 0012exact parity_cases_witness_left
  13. 0013cases hfactor
  14. 0014exfalso
  15. 0015have hzero : 1 = 0
  16. 0016apply PA2
  17. 0017exact hfactor_left
  18. 0018apply PA1
  19. 0019exact hzero
  20. 0020rewrite hfactor_right at parity_cases_witness_left
  21. 0021specialize mul_one 2
  22. 0022rewrite mul_one at parity_cases_witness_left
  23. 0023exact parity_cases_witness_left
  24. 0024right
  25. 0025exists x
  26. 0026exact parity_cases_witness_right