PA000S

mul_ne_zero

Stable checked-use theorem · independently closed

A product of two nonzero naturals is nonzero.

Exact expanded PA statement

forall a b. ~(a = 0) -> ~(b = 0) -> ~(a * b = 0)

Structural proof guide

Generated structural guide

A product of two nonzero naturals is nonzero.

Use the direct prerequisites mul_eq_zero as previously established PA formulas.

The proof proceeds by case analysis (1), intermediate claims (1).

Referenced ingredients

PA0007 mul_eq_zero

Proof neighborhood

Direct dependencies

PA0007 mul_eq_zero

Direct dependents

PA001U beta_exclusive_accumulated_product_step PA006S mul_left_cancel_nonzero

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 a
  2. 0002intro b
  3. 0003intro ha
  4. 0004intro hb
  5. 0005intro hab
  6. 0006specialize mul_eq_zero a
  7. 0007specialize mul_eq_zero b
  8. 0008have hz : a = 0 \/ b = 0
  9. 0009apply mul_eq_zero
  10. 0010exact hab
  11. 0011cases hz
  12. 0012apply ha
  13. 0013exact hz_left
  14. 0014apply hb
  15. 0015exact hz_right