PA0064 · theorem

prime_ne_two_is_odd

Stable checked-use theorem · independently closed

Every prime other than two is odd.

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 is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0004 Prime PD0010 Odd

2 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall p. (~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) -> ~(p = 2) -> exists h. p = 2 * h + 1

Proof neighborhood

Direct theorem prerequisites

PA0057 parity_cases

Direct theorem dependents

PA00A2 prime_two_or_terminal_odd_shape

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

25 script commands · 14 reading checkpoints · 1 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 (1)
parity cases
01Fix variables and assumptionsL1–3

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

  1. L1
    intro p
  2. L2
    intro hp
  3. L3
    intro hne
02Separate the logical casesL4–4

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

  1. L4
    cases hp
03Use earlier factsL5–5

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

  1. L5
    specialize parity_cases p
04Separate the logical casesL6–7

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

  1. L6
    cases parity_cases
  2. L7
    cases parity_cases_witness
05Establish hfacL8–12

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

  1. L8
    have hfac : 2 = 1 \/ x = 1
  2. L9
    specialize hp_right 2
  3. L10
    specialize hp_right x
  4. L11
    apply hp_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 hfac
  2. L14
    exfalso
07Use earlier factsL15–17

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

  1. L15
    apply PA1
  2. L16
    apply PA2
  3. L17
    exact hfac_left
08Separate the logical casesL18–18

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

  1. L18
    exfalso
09Use earlier factsL19–19

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

  1. L19
    apply hne
10Calculate and transport equalitiesL20–20

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

  1. L20
    trans 2 * x
11Use earlier factsL21–21

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

  1. L21
    exact parity_cases_witness_left
12Calculate and transport equalitiesL22–23

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

  1. L22
    rewrite hfac_right
  2. L23
    simp
13Construct an explicit witnessL24–24

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

  1. L24
    exists x
14Use earlier factsL25–25

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

  1. L25
    exact parity_cases_witness_right

Library-wide reading audit

Original defined command ledger · 25 lines
  1. 0001intro p
  2. 0002intro hp
  3. 0003intro hne
  4. 0004cases hp
  5. 0005specialize parity_cases p
  6. 0006cases parity_cases
  7. 0007cases parity_cases_witness
  8. 0008have hfac : 2 = 1 \/ x = 1
  9. 0009specialize hp_right 2
  10. 0010specialize hp_right x
  11. 0011apply hp_right
  12. 0012exact parity_cases_witness_left
  13. 0013cases hfac
  14. 0014exfalso
  15. 0015apply PA1
  16. 0016apply PA2
  17. 0017exact hfac_left
  18. 0018exfalso
  19. 0019apply hne
  20. 0020trans 2 * x
  21. 0021exact parity_cases_witness_left
  22. 0022rewrite hfac_right
  23. 0023simp
  24. 0024exists x
  25. 0025exact parity_cases_witness_right