Metamath Proof Explorer


Theorem times2

Description: A number times 2. (Contributed by NM, 16-Oct-2007)

Ref Expression
Assertion times2
|- ( A e. CC -> ( A x. 2 ) = ( A + A ) )

Proof

Step Hyp Ref Expression
1 2cn
 |-  2 e. CC
2 mulcom
 |-  ( ( A e. CC /\ 2 e. CC ) -> ( A x. 2 ) = ( 2 x. A ) )
3 1 2 mpan2
 |-  ( A e. CC -> ( A x. 2 ) = ( 2 x. A ) )
4 2times
 |-  ( A e. CC -> ( 2 x. A ) = ( A + A ) )
5 3 4 eqtrd
 |-  ( A e. CC -> ( A x. 2 ) = ( A + A ) )