Metamath Proof Explorer

Theorem 2times

Description: Two times a number. (Contributed by NM, 10-Oct-2004) (Revised by Mario Carneiro, 27-May-2016) (Proof shortened by AV, 26-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 df-2 
 |-  2 = ( 1 + 1 )
2 1 oveq1i 
 |-  ( 2 x. A ) = ( ( 1 + 1 ) x. A )
3 1p1times 
 |-  ( A e. CC -> ( ( 1 + 1 ) x. A ) = ( A + A ) )
4 2 3 syl5eq 
 |-  ( A e. CC -> ( 2 x. A ) = ( A + A ) )