Metamath Proof Explorer

Theorem 1p1times

Description: Two times a number. (Contributed by NM, 18-May-1999) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion 1p1times 
|- ( A e. CC -> ( ( 1 + 1 ) x. A ) = ( A + A ) )

Proof

Step Hyp Ref Expression
1 1cnd 
 |-  ( A e. CC -> 1 e. CC )
2 id 
 |-  ( A e. CC -> A e. CC )
3 mulid2 
 |-  ( A e. CC -> ( 1 x. A ) = A )
4 3 3 oveq12d 
 |-  ( A e. CC -> ( ( 1 x. A ) + ( 1 x. A ) ) = ( A + A ) )
5 1 2 1 4 joinlmuladdmuld 
 |-  ( A e. CC -> ( ( 1 + 1 ) x. A ) = ( A + A ) )