PA0061

prime_is_succ_succ

Stable checked-use theorem · independently closed

Every prime natural is the second successor of a natural.

Exact expanded PA statement

forall p. ((~(p = 1) /\ forall qrbu_factor_left_prime_p qrbu_factor_right_prime_p. p = qrbu_factor_left_prime_p * qrbu_factor_right_prime_p -> qrbu_factor_left_prime_p = 1 \/ qrbu_factor_right_prime_p = 1)) -> exists k. p = S (S k)

Structural proof guide

Generated structural guide

Every prime natural is the second successor of a natural.

Use the direct prerequisites prime_nonzero, nonzero_is_succ as previously established PA formulas.

The proof proceeds by case analysis (3), intermediate claims (4), equality transport (4).

Referenced ingredients

PA0031 prime_nonzero PA001V nonzero_is_succ

Proof neighborhood

Direct dependencies

PA0031 prime_nonzero PA001V nonzero_is_succ

Direct dependents

PA0063 prime_bounded_nonzero_mod_inverse PA008P prime_scaled_inverse_target_nonzero PA00AQ prime_inverse_prefix_nonendpoint_mate PA00BP odd_prime_one_not_mod_predecessor

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. 0003have hp0 : ~(p = 0)
  4. 0004intro hpzero
  5. 0005specialize prime_nonzero p
  6. 0006apply prime_nonzero
  7. 0007exact hp
  8. 0008exact hpzero
  9. 0009have hps : exists k. p = S k
  10. 0010specialize nonzero_is_succ p
  11. 0011apply nonzero_is_succ
  12. 0012exact hp0
  13. 0013cases hps
  14. 0014have hx0 : ~(x = 0)
  15. 0015intro hx0
  16. 0016cases hp
  17. 0017apply hp_left
  18. 0018rewrite hps_witness
  19. 0019rewrite hx0
  20. 0020refl
  21. 0021have hxs : exists k. x = S k
  22. 0022specialize nonzero_is_succ x
  23. 0023apply nonzero_is_succ
  24. 0024exact hx0
  25. 0025cases hxs
  26. 0026exists x1
  27. 0027rewrite hps_witness
  28. 0028rewrite hxs_witness
  29. 0029refl