Theorem xmulid1

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

	Ref	Expression
Assertion	xmulid1	$$⊢A\in {ℝ}^{*}\to A{\cdot }_{𝑒}1=A$$

Proof

Step	Hyp	Ref	Expression
1		elxr	$$⊢A\in {ℝ}^{*}\leftrightarrow \left(A\in ℝ\vee A=\mathrm{+\infty }\vee A=\mathrm{-\infty }\right)$$
2		1re	$$⊢1\in ℝ$$
3		rexmul	$$⊢\left(A\in ℝ\wedge 1\in ℝ\right)\to A{\cdot }_{𝑒}1=A\cdot 1$$
4	2 3	mpan2	$$⊢A\in ℝ\to A{\cdot }_{𝑒}1=A\cdot 1$$
5		ax-1rid	$$⊢A\in ℝ\to A\cdot 1=A$$
6	4 5	eqtrd	$$⊢A\in ℝ\to A{\cdot }_{𝑒}1=A$$
7		1xr	$$⊢1\in {ℝ}^{*}$$
8		0lt1	$$⊢0<1$$
9		xmulpnf2	$$⊢\left(1\in {ℝ}^{*}\wedge 0<1\right)\to \mathrm{+\infty }{\cdot }_{𝑒}1=\mathrm{+\infty }$$
10	7 8 9	mp2an	$$⊢\mathrm{+\infty }{\cdot }_{𝑒}1=\mathrm{+\infty }$$
11		oveq1	$$⊢A=\mathrm{+\infty }\to A{\cdot }_{𝑒}1=\mathrm{+\infty }{\cdot }_{𝑒}1$$
12		id	$$⊢A=\mathrm{+\infty }\to A=\mathrm{+\infty }$$
13	10 11 12	3eqtr4a	$$⊢A=\mathrm{+\infty }\to A{\cdot }_{𝑒}1=A$$
14		xmulmnf2	$$⊢\left(1\in {ℝ}^{*}\wedge 0<1\right)\to \mathrm{-\infty }{\cdot }_{𝑒}1=\mathrm{-\infty }$$
15	7 8 14	mp2an	$$⊢\mathrm{-\infty }{\cdot }_{𝑒}1=\mathrm{-\infty }$$
16		oveq1	$$⊢A=\mathrm{-\infty }\to A{\cdot }_{𝑒}1=\mathrm{-\infty }{\cdot }_{𝑒}1$$
17		id	$$⊢A=\mathrm{-\infty }\to A=\mathrm{-\infty }$$
18	15 16 17	3eqtr4a	$$⊢A=\mathrm{-\infty }\to A{\cdot }_{𝑒}1=A$$
19	6 13 18	3jaoi	$$⊢\left(A\in ℝ\vee A=\mathrm{+\infty }\vee A=\mathrm{-\infty }\right)\to A{\cdot }_{𝑒}1=A$$
20	1 19	sylbi	$$⊢A\in {ℝ}^{*}\to A{\cdot }_{𝑒}1=A$$