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 syl5ibr
 |-  ( y e. _om -> ( ( (/) .o y ) = (/) -> ( (/) .o suc y ) = (/) ) )
21 2 4 6 8 11 20 finds
 |-  ( A e. _om -> ( (/) .o A ) = (/) )