BT00AW

prime_is_succ_succ

Stable · empty-context checked

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

Every prime natural is the second successor of a natural.

Direct prerequisites: prime_nonzero, nonzero_is_succ. The authored body proceeds by case analysis (3), intermediate claims (4), equality transport (4).

Proof neighborhood

Direct dependencies

BT003G prime_nonzero BT000R nonzero_is_succ

Direct dependents

BT00QD prime_two_le BT00VA factorial_prime_divides_of_le BT00YA prime_square_tail_of_two_three_range BT0102 prime_contribution_cofactor_prime_contradiction BT011A prime_le_twenty_two_cases

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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