This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem x2times

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

Ref Expression
Assertion x2times ⊢ A ∈ ℝ * → 2 ⋅ 𝑒 A = A + 𝑒 A

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 ⋅ 𝑒 A = 1 + 𝑒 1 ⋅ 𝑒 A
7 1xr ⊢ 1 ∈ ℝ *
8 0le1 ⊢ 0 ≤ 1
9 7 8 pm3.2i ⊢ 1 ∈ ℝ * ∧ 0 ≤ 1
10 xadddi2r ⊢ 1 ∈ ℝ * ∧ 0 ≤ 1 ∧ 1 ∈ ℝ * ∧ 0 ≤ 1 ∧ A ∈ ℝ * → 1 + 𝑒 1 ⋅ 𝑒 A = 1 ⋅ 𝑒 A + 𝑒 1 ⋅ 𝑒 A
11 9 9 10 mp3an12 ⊢ A ∈ ℝ * → 1 + 𝑒 1 ⋅ 𝑒 A = 1 ⋅ 𝑒 A + 𝑒 1 ⋅ 𝑒 A
12 xmullid ⊢ A ∈ ℝ * → 1 ⋅ 𝑒 A = A
13 12 12 oveq12d ⊢ A ∈ ℝ * → 1 ⋅ 𝑒 A + 𝑒 1 ⋅ 𝑒 A = A + 𝑒 A
14 11 13 eqtrd ⊢ A ∈ ℝ * → 1 + 𝑒 1 ⋅ 𝑒 A = A + 𝑒 A
15 6 14 eqtrid ⊢ A ∈ ℝ * → 2 ⋅ 𝑒 A = A + 𝑒 A