This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnm0r

Description: Multiplication with zero. Exercise 16 of Enderton p. 82. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nnm0r 
|- ( A e. _om -> ( (/) .o A ) = (/) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = (/) -> ( (/) .o x ) = ( (/) .o (/) ) )
2 1 eqeq1d 
 |-  ( x = (/) -> ( ( (/) .o x ) = (/) <-> ( (/) .o (/) ) = (/) ) )
3 oveq2 
 |-  ( x = y -> ( (/) .o x ) = ( (/) .o y ) )
4 3 eqeq1d 
 |-  ( x = y -> ( ( (/) .o x ) = (/) <-> ( (/) .o y ) = (/) ) )
5 oveq2 
 |-  ( x = suc y -> ( (/) .o x ) = ( (/) .o suc y ) )
6 5 eqeq1d 
 |-  ( x = suc y -> ( ( (/) .o x ) = (/) <-> ( (/) .o suc y ) = (/) ) )
7 oveq2 
 |-  ( x = A -> ( (/) .o x ) = ( (/) .o A ) )
8 7 eqeq1d 
 |-  ( x = A -> ( ( (/) .o x ) = (/) <-> ( (/) .o A ) = (/) ) )
9 0elon 
 |-  (/) e. On
10 om0 
 |-  ( (/) e. On -> ( (/) .o (/) ) = (/) )
11 9 10 ax-mp 
 |-  ( (/) .o (/) ) = (/)
12 oveq1 
 |-  ( ( (/) .o y ) = (/) -> ( ( (/) .o y ) +o (/) ) = ( (/) +o (/) ) )
13 oa0 
 |-  ( (/) e. On -> ( (/) +o (/) ) = (/) )
14 9 13 ax-mp 
 |-  ( (/) +o (/) ) = (/)
15 12 14 eqtrdi 
 |-  ( ( (/) .o y ) = (/) -> ( ( (/) .o y ) +o (/) ) = (/) )
16 peano1 
 |-  (/) e. _om
17 nnmsuc 
 |-  ( ( (/) e. _om /\ y e. _om ) -> ( (/) .o suc y ) = ( ( (/) .o y ) +o (/) ) )
18 16 17 mpan 
 |-  ( y e. _om -> ( (/) .o suc y ) = ( ( (/) .o y ) +o (/) ) )
19 18 eqeq1d 
 |-  ( y e. _om -> ( ( (/) .o suc y ) = (/) <-> ( ( (/) .o y ) +o (/) ) = (/) ) )
20 15 19 imbitrrid 
 |-  ( y e. _om -> ( ( (/) .o y ) = (/) -> ( (/) .o suc y ) = (/) ) )
21 2 4 6 8 11 20 finds 
 |-  ( A e. _om -> ( (/) .o A ) = (/) )