PA0007

mul_eq_zero

Stable checked-use theorem · independently closed

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

Generated structural guide

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

Use the direct prerequisites add_eq_zero_right as previously established PA formulas.

The proof proceeds by structural induction (1), equality transport (1).

Referenced ingredients

PA0004 add_eq_zero_right

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right

Direct dependents

PA000I bounded_common_multiple_step PA000S mul_ne_zero 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 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