Theorem nnm2

Description: Multiply an element of _om by 2o . (Contributed by Scott Fenton, 18-Apr-2012) (Revised by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Assertion	nnm2	|- ( A e. _om -> ( A .o 2o ) = ( A +o A ) )

Proof

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