Metamath Proof Explorer

Theorem nn2m

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

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

Proof

Step Hyp Ref Expression
1 2onn 
 |-  2o e. _om
2 nnmcom 
 |-  ( ( 2o e. _om /\ A e. _om ) -> ( 2o .o A ) = ( A .o 2o ) )
3 1 2 mpan 
 |-  ( A e. _om -> ( 2o .o A ) = ( A .o 2o ) )
4 nnm2 
 |-  ( A e. _om -> ( A .o 2o ) = ( A +o A ) )
5 3 4 eqtrd 
 |-  ( A e. _om -> ( 2o .o A ) = ( A +o A ) )