Theorem nnm1

Description: Multiply an element of _om by 1o . (Contributed by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Assertion	nnm1	|- ( A e. _om -> ( A .o 1o ) = A )

Proof

Step	Hyp	Ref	Expression
1		df-1o	|- 1o = suc (/)
2	1	oveq2i	|- ( A .o 1o ) = ( A .o suc (/) )
3		peano1	|- (/) e. _om
4		nnmsuc	|- ( ( A e. _om /\ (/) e. _om ) -> ( A .o suc (/) ) = ( ( A .o (/) ) +o A ) )
5	3 4	mpan2	|- ( A e. _om -> ( A .o suc (/) ) = ( ( A .o (/) ) +o A ) )
6		nnm0	|- ( A e. _om -> ( A .o (/) ) = (/) )
7	6	oveq1d	|- ( A e. _om -> ( ( A .o (/) ) +o A ) = ( (/) +o A ) )
8		nna0r	|- ( A e. _om -> ( (/) +o A ) = A )
9	5 7 8	3eqtrd	|- ( A e. _om -> ( A .o suc (/) ) = A )
10	2 9	eqtrid	|- ( A e. _om -> ( A .o 1o ) = A )