Metamath Proof Explorer

Theorem x2times

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

Ref Expression
Assertion x2times ( 𝐴 ∈ ℝ* → ( 2 ·e 𝐴 ) = ( 𝐴 +𝑒 𝐴 ) )

Proof

Step Hyp Ref Expression
1 df-2 ⊢ 2 = ( 1 + 1 )
2 1re ⊢ 1 ∈ ℝ
3 rexadd ⊢ ( ( 1 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 1 +𝑒 1 ) = ( 1 + 1 ) )
4 2 2 3 mp2an ⊢ ( 1 +𝑒 1 ) = ( 1 + 1 )
5 1 4 eqtr4i ⊢ 2 = ( 1 +𝑒 1 )
6 5 oveq1i ⊢ ( 2 ·e 𝐴 ) = ( ( 1 +𝑒 1 ) ·e 𝐴 )
7 1xr ⊢ 1 ∈ ℝ*
8 0le1 ⊢ 0 ≤ 1
9 7 8 pm3.2i ⊢ ( 1 ∈ ℝ* ∧ 0 ≤ 1 )
10 xadddi2r ⊢ ( ( ( 1 ∈ ℝ* ∧ 0 ≤ 1 ) ∧ ( 1 ∈ ℝ* ∧ 0 ≤ 1 ) ∧ 𝐴 ∈ ℝ* ) → ( ( 1 +𝑒 1 ) ·e 𝐴 ) = ( ( 1 ·e 𝐴 ) +𝑒 ( 1 ·e 𝐴 ) ) )
11 9 9 10 mp3an12 ⊢ ( 𝐴 ∈ ℝ* → ( ( 1 +𝑒 1 ) ·e 𝐴 ) = ( ( 1 ·e 𝐴 ) +𝑒 ( 1 ·e 𝐴 ) ) )
12 xmullid ⊢ ( 𝐴 ∈ ℝ* → ( 1 ·e 𝐴 ) = 𝐴 )
13 12 12 oveq12d ⊢ ( 𝐴 ∈ ℝ* → ( ( 1 ·e 𝐴 ) +𝑒 ( 1 ·e 𝐴 ) ) = ( 𝐴 +𝑒 𝐴 ) )
14 11 13 eqtrd ⊢ ( 𝐴 ∈ ℝ* → ( ( 1 +𝑒 1 ) ·e 𝐴 ) = ( 𝐴 +𝑒 𝐴 ) )
15 6 14 eqtrid ⊢ ( 𝐴 ∈ ℝ* → ( 2 ·e 𝐴 ) = ( 𝐴 +𝑒 𝐴 ) )