Metamath Proof Explorer


Theorem mul01

Description: Multiplication by 0 . Theorem I.6 of Apostol p. 18. (Contributed by NM, 15-May-1999) (Revised by Scott Fenton, 3-Jan-2013)

Ref Expression
Assertion mul01 A A 0 = 0

Proof

Step Hyp Ref Expression
1 0cn 0
2 mulcom A 0 A 0 = 0 A
3 1 2 mpan2 A A 0 = 0 A
4 mul02 A 0 A = 0
5 3 4 eqtrd A A 0 = 0