Metamath Proof Explorer

Theorem x2times

Description: Extended real version of 2times . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion x2times 
|- ( A e. RR* -> ( 2 *e A ) = ( A +e A ) )

Proof

Step Hyp Ref Expression
1 df-2 
 |-  2 = ( 1 + 1 )
2 1re 
 |-  1 e. RR
3 rexadd 
 |-  ( ( 1 e. RR /\ 1 e. RR ) -> ( 1 +e 1 ) = ( 1 + 1 ) )
4 2 2 3 mp2an 
 |-  ( 1 +e 1 ) = ( 1 + 1 )
5 1 4 eqtr4i 
 |-  2 = ( 1 +e 1 )
6 5 oveq1i 
 |-  ( 2 *e A ) = ( ( 1 +e 1 ) *e A )
7 1xr 
 |-  1 e. RR*
8 0le1 
 |-  0 <_ 1
9 7 8 pm3.2i 
 |-  ( 1 e. RR* /\ 0 <_ 1 )
10 xadddi2r 
 |-  ( ( ( 1 e. RR* /\ 0 <_ 1 ) /\ ( 1 e. RR* /\ 0 <_ 1 ) /\ A e. RR* ) -> ( ( 1 +e 1 ) *e A ) = ( ( 1 *e A ) +e ( 1 *e A ) ) )
11 9 9 10 mp3an12 
 |-  ( A e. RR* -> ( ( 1 +e 1 ) *e A ) = ( ( 1 *e A ) +e ( 1 *e A ) ) )
12 xmulid2 
 |-  ( A e. RR* -> ( 1 *e A ) = A )
13 12 12 oveq12d 
 |-  ( A e. RR* -> ( ( 1 *e A ) +e ( 1 *e A ) ) = ( A +e A ) )
14 11 13 eqtrd 
 |-  ( A e. RR* -> ( ( 1 +e 1 ) *e A ) = ( A +e A ) )
15 6 14 eqtrid 
 |-  ( A e. RR* -> ( 2 *e A ) = ( A +e A ) )