BT0021

mul_ne_zero

Stable · empty-context checked

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

A product of two nonzero naturals is nonzero.

Direct prerequisites: mul_eq_zero. The authored body proceeds by case analysis (1), intermediate claims (1).

Proof neighborhood

Direct dependencies

BT000M mul_eq_zero

Direct dependents

BT0022 mul_left_cancel_nonzero BT0059 beta_exclusive_accumulated_product_step BT00QR power_valuation_mul_lower BT00RK factorial_nonzero BT00XM central_binom_factorial_valuation_balance

Formal native tactic body

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

  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