BT000M

mul_eq_zero

Stable · empty-context checked

Zero products have a zero factor: the 23-entry core capstone.

Exact expanded PA statement

forall n m. n * m = 0 -> n = 0 \/ m = 0

Structural proof guide

Zero products have a zero factor: the 23-entry core capstone.

Direct prerequisites: add_eq_zero_right. The authored body proceeds by structural induction (1), equality transport (1).

Proof neighborhood

Direct dependencies

BT000L add_eq_zero_right

Direct dependents

BT0021 mul_ne_zero BT0022 mul_left_cancel_nonzero BT0024 two_large_factors_impossible BT004M bounded_common_multiple_step BT006N prime_three

Formal native tactic body

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

  1. 0001intro n
  2. 0002induction m
  3. 0003intro h
  4. 0004right
  5. 0005refl
  6. 0006intro h
  7. 0007left
  8. 0008specialize add_eq_zero_right (n * m)
  9. 0009specialize add_eq_zero_right n
  10. 0010apply add_eq_zero_right
  11. 0011rewrite PA6 at h
  12. 0012exact h