Theorem xaddid1

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

	Ref	Expression
Assertion	xaddid1	$$⊢A\in {ℝ}^{*}\to A{+}_{𝑒}0=A$$

Proof

Step	Hyp	Ref	Expression
1		elxr	$$⊢A\in {ℝ}^{*}\leftrightarrow \left(A\in ℝ\vee A=\mathrm{+\infty }\vee A=\mathrm{-\infty }\right)$$
2		0re	$$⊢0\in ℝ$$
3		rexadd	$$⊢\left(A\in ℝ\wedge 0\in ℝ\right)\to A{+}_{𝑒}0=A+0$$
4	2 3	mpan2	$$⊢A\in ℝ\to A{+}_{𝑒}0=A+0$$
5		recn	$$⊢A\in ℝ\to A\in ℂ$$
6	5	addid1d	$$⊢A\in ℝ\to A+0=A$$
7	4 6	eqtrd	$$⊢A\in ℝ\to A{+}_{𝑒}0=A$$
8		0xr	$$⊢0\in {ℝ}^{*}$$
9		renemnf	$$⊢0\in ℝ\to 0\ne \mathrm{-\infty }$$
10	2 9	ax-mp	$$⊢0\ne \mathrm{-\infty }$$
11		xaddpnf2	$$⊢\left(0\in {ℝ}^{*}\wedge 0\ne \mathrm{-\infty }\right)\to \mathrm{+\infty }{+}_{𝑒}0=\mathrm{+\infty }$$
12	8 10 11	mp2an	$$⊢\mathrm{+\infty }{+}_{𝑒}0=\mathrm{+\infty }$$
13		oveq1	$$⊢A=\mathrm{+\infty }\to A{+}_{𝑒}0=\mathrm{+\infty }{+}_{𝑒}0$$
14		id	$$⊢A=\mathrm{+\infty }\to A=\mathrm{+\infty }$$
15	12 13 14	3eqtr4a	$$⊢A=\mathrm{+\infty }\to A{+}_{𝑒}0=A$$
16		renepnf	$$⊢0\in ℝ\to 0\ne \mathrm{+\infty }$$
17	2 16	ax-mp	$$⊢0\ne \mathrm{+\infty }$$
18		xaddmnf2	$$⊢\left(0\in {ℝ}^{*}\wedge 0\ne \mathrm{+\infty }\right)\to \mathrm{-\infty }{+}_{𝑒}0=\mathrm{-\infty }$$
19	8 17 18	mp2an	$$⊢\mathrm{-\infty }{+}_{𝑒}0=\mathrm{-\infty }$$
20		oveq1	$$⊢A=\mathrm{-\infty }\to A{+}_{𝑒}0=\mathrm{-\infty }{+}_{𝑒}0$$
21		id	$$⊢A=\mathrm{-\infty }\to A=\mathrm{-\infty }$$
22	19 20 21	3eqtr4a	$$⊢A=\mathrm{-\infty }\to A{+}_{𝑒}0=A$$
23	7 15 22	3jaoi	$$⊢\left(A\in ℝ\vee A=\mathrm{+\infty }\vee A=\mathrm{-\infty }\right)\to A{+}_{𝑒}0=A$$
24	1 23	sylbi	$$⊢A\in {ℝ}^{*}\to A{+}_{𝑒}0=A$$