PA0064

prime_ne_two_is_odd

Stable checked-use theorem · independently closed

Every prime other than two is odd.

Exact expanded PA statement

forall p. (~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) -> ~(p = 2) -> exists h. p = 2 * h + 1

Structural proof guide

Generated structural guide

Every prime other than two is odd.

Use the direct prerequisites parity_cases as previously established PA formulas.

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

Referenced ingredients

PA0057 parity_cases

Proof neighborhood

Direct dependencies

PA0057 parity_cases

Direct dependents

PA00A2 prime_two_or_terminal_odd_shape

Formal native tactic body

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

  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