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 ) = (/) )