Theorem x2times

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

	Ref	Expression
Assertion	x2times	$$⊢A\in {ℝ}^{*}\to 2{\cdot }_{𝑒}A=A{+}_{𝑒}A$$

Proof

Step	Hyp	Ref	Expression
1		df-2	$$⊢2=1+1$$
2		1re	$$⊢1\in ℝ$$
3		rexadd	$$⊢\left(1\in ℝ\wedge 1\in ℝ\right)\to 1{+}_{𝑒}1=1+1$$
4	2 2 3	mp2an	$$⊢1{+}_{𝑒}1=1+1$$
5	1 4	eqtr4i	$$⊢2=1{+}_{𝑒}1$$
6	5	oveq1i	$$⊢2{\cdot }_{𝑒}A=\left(1{+}_{𝑒}1\right){\cdot }_{𝑒}A$$
7		1xr	$$⊢1\in {ℝ}^{*}$$
8		0le1	$$⊢0\le 1$$
9	7 8	pm3.2i	$$⊢\left(1\in {ℝ}^{*}\wedge 0\le 1\right)$$
10		xadddi2r	$$⊢\left(\left(1\in {ℝ}^{*}\wedge 0\le 1\right)\wedge \left(1\in {ℝ}^{*}\wedge 0\le 1\right)\wedge A\in {ℝ}^{*}\right)\to \left(1{+}_{𝑒}1\right){\cdot }_{𝑒}A=\left(1{\cdot }_{𝑒}A\right){+}_{𝑒}\left(1{\cdot }_{𝑒}A\right)$$
11	9 9 10	mp3an12	$$⊢A\in {ℝ}^{*}\to \left(1{+}_{𝑒}1\right){\cdot }_{𝑒}A=\left(1{\cdot }_{𝑒}A\right){+}_{𝑒}\left(1{\cdot }_{𝑒}A\right)$$
12		xmulid2	$$⊢A\in {ℝ}^{*}\to 1{\cdot }_{𝑒}A=A$$
13	12 12	oveq12d	$$⊢A\in {ℝ}^{*}\to \left(1{\cdot }_{𝑒}A\right){+}_{𝑒}\left(1{\cdot }_{𝑒}A\right)=A{+}_{𝑒}A$$
14	11 13	eqtrd	$$⊢A\in {ℝ}^{*}\to \left(1{+}_{𝑒}1\right){\cdot }_{𝑒}A=A{+}_{𝑒}A$$
15	6 14	syl5eq	$$⊢A\in {ℝ}^{*}\to 2{\cdot }_{𝑒}A=A{+}_{𝑒}A$$