PA00A2 · theorem

prime_two_or_terminal_odd_shape

Alpha v34 checked-use theorem · independently closed; not Stable

A prime is two or has exactly the doubled terminal PairOrder shape.

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 ∨ (∃ x. p = S S S (x + x))

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

1 occurrences

In local proof propositions

PD0004 Prime PD0010 Odd

2 occurrences

Exact expanded native-PA statement
forall p. ((~(p = 1) /\ forall wip_prime_left_wer_shape_prime wip_prime_right_wer_shape_prime. p = wip_prime_left_wer_shape_prime * wip_prime_right_wer_shape_prime -> wip_prime_left_wer_shape_prime = 1 \/ wip_prime_right_wer_shape_prime = 1)) -> p = 2 \/ exists m. p = S (S (S (m + m)))

Proof neighborhood

Direct theorem prerequisites

PA004G eq_decidable PA0064 prime_ne_two_is_odd PA001V nonzero_is_succ PA000G mul_succ_left PA000D mul_zero_left PA0001 zero_add PA000E add_succ_left PA0009 add_assoc PA000F add_comm

Direct theorem dependents

PA00BJ prime_factorial_wilson_congruence

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

36 script commands · 16 reading checkpoints · 5 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 ne two is oddnonzero is succ
01Fix variables and assumptionsL1–2

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

  1. L1
    intro p
  2. L2
    intro hp
02Establish hcasesL3–6

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

  1. L3
    have hcases : p = 2 \/ ~(p = 2)
  2. L4
    specialize eq_decidable p
  3. L5
    specialize eq_decidable 2
  4. L6
    exact eq_decidable
03Separate the logical casesL7–8

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

  1. L7
    cases hcases
  2. L8
    left
04Use earlier factsL9–9

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

  1. L9
    exact hcases_left
05Separate the logical casesL10–10

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

  1. L10
    right
06Establish hoddL11–15

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

  1. L11
  2. L12
    specialize prime_ne_two_is_odd p
  3. L13
    apply prime_ne_two_is_odd
  4. L14
    exact hp
  5. L15
    exact hcases_right
07Separate the logical casesL16–16

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

  1. L16
    cases hodd
08Establish hpartsL17–18

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

  1. L17
    have hparts : Prime(p)Definitions: Prime(p)Original native command in the exact edition
  2. L18
    exact hp
09Separate the logical casesL19–19

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

  1. L19
    cases hparts
10Establish hhL20–26

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

  1. L20
    have hh : ~(x = 0)
  2. L21
    intro hxzero
  3. L22
    apply hparts_left
  4. L23
    trans 2 * x + 1
  5. L24
    exact hodd_witness
  6. L25
    rewrite hxzero
  7. L26
    simp [mul_succ_left, mul_zero_left, zero_add, add_succ_left]
11Establish hsuccL27–30

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

  1. L27
    have hsucc : exists m. x = S m
  2. L28
    specialize nonzero_is_succ x
  3. L29
    apply nonzero_is_succ
  4. L30
    exact hh
12Separate the logical casesL31–31

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

  1. L31
    cases hsucc
13Construct an explicit witnessL32–32

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

  1. L32
    exists x1
14Calculate and transport equalitiesL33–34

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

  1. L33
    trans 2 * S x1 + 1
  2. L34
    rewrite <- hsucc_witness
15Use earlier factsL35–35

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

  1. L35
    exact hodd_witness
16Calculate and transport equalitiesL36–36

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

  1. L36
    simp [mul_succ_left, mul_zero_left, zero_add, add_succ_left, add_assoc, add_comm]

Library-wide reading audit

Original defined command ledger · 36 lines
  1. 0001intro p
  2. 0002intro hp
  3. 0003have hcases : p = 2 \/ ~(p = 2)
  4. 0004specialize eq_decidable p
  5. 0005specialize eq_decidable 2
  6. 0006exact eq_decidable
  7. 0007cases hcases
  8. 0008left
  9. 0009exact hcases_left
  10. 0010right
  11. 0011have hodd : Odd(p)
    Exact native replay linehave hodd : exists h. p = 2 * h + 1
  12. 0012specialize prime_ne_two_is_odd p
  13. 0013apply prime_ne_two_is_odd
  14. 0014exact hp
  15. 0015exact hcases_right
  16. 0016cases hodd
  17. 0017have hparts : Prime(p)
    Exact native replay linehave hparts : (~(p = 1) /\ forall wip_prime_left_wer_shape_prime wip_prime_right_wer_shape_prime. p = wip_prime_left_wer_shape_prime * wip_prime_right_wer_shape_prime -> wip_prime_left_wer_shape_prime = 1 \/ wip_prime_right_wer_shape_prime = 1)
  18. 0018exact hp
  19. 0019cases hparts
  20. 0020have hh : ~(x = 0)
  21. 0021intro hxzero
  22. 0022apply hparts_left
  23. 0023trans 2 * x + 1
  24. 0024exact hodd_witness
  25. 0025rewrite hxzero
  26. 0026simp [mul_succ_left, mul_zero_left, zero_add, add_succ_left]
  27. 0027have hsucc : exists m. x = S m
  28. 0028specialize nonzero_is_succ x
  29. 0029apply nonzero_is_succ
  30. 0030exact hh
  31. 0031cases hsucc
  32. 0032exists x1
  33. 0033trans 2 * S x1 + 1
  34. 0034rewrite <- hsucc_witness
  35. 0035exact hodd_witness
  36. 0036simp [mul_succ_left, mul_zero_left, zero_add, add_succ_left, add_assoc, add_comm]