PA00A2

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.

Exact expanded 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)))

Structural proof guide

Generated structural guide

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

Use the direct prerequisites eq_decidable, prime_ne_two_is_odd, nonzero_is_succ, mul_succ_left, mul_zero_left, zero_add, add_succ_left, add_assoc, add_comm as previously established PA formulas.

The proof proceeds by case analysis (4), intermediate claims (5), equality transport (2), certified simplification (2).

Referenced ingredients

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

Proof neighborhood

Direct dependencies

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 dependents

PA00BJ prime_factorial_wilson_congruence

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

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.

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
    have hodd : exists h. p = 2 * h + 1
  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 : (~(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)
  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 exact 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 : 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 : (~(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]