BT003G

prime_nonzero

Stable · empty-context checked

Every prime natural is nonzero.

Exact expanded PA statement

forall p. (~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) -> ~(p = 0)

Structural proof guide

Every prime natural is nonzero.

Direct prerequisites: mul_zero_left, succ_ne_zero. The authored body proceeds by case analysis (2), intermediate claims (1), equality transport (1).

Proof neighborhood

Direct dependencies

BT0004 mul_zero_left BT000C succ_ne_zero

Direct dependents

BT003H prime_decidable BT00AW prime_is_succ_succ BT00PS bounded_prime_interval_search BT00QF prime_power_exponent_le BT00QN prime_power_successor_cancel_cofactor BT00S0 prime_power_quotient_prefix_exists BT00Y5 central_binom_prime_power_contribution_le_double BT00Y6 central_binom_prime_square_tail_exponent_not_two_le BT00YE central_binom_prime_valuation_zero_two_thirds_range

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. 0003intro hp0
  4. 0004cases hp
  5. 0005specialize hp_right 0
  6. 0006specialize hp_right 0
  7. 0007have hunit : 0 = 1 \/ 0 = 1
  8. 0008apply hp_right
  9. 0009rewrite hp0
  10. 0010symm
  11. 0011apply mul_zero_left
  12. 0012cases hunit
  13. 0013specialize succ_ne_zero 0
  14. 0014apply succ_ne_zero
  15. 0015symm
  16. 0016exact hunit_left
  17. 0017specialize succ_ne_zero 0
  18. 0018apply succ_ne_zero
  19. 0019symm
  20. 0020exact hunit_right