PA00A2

prime_two_or_terminal_odd_shape

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

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

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-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  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]