Theorem xaddid1

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

	Ref	Expression
Assertion	xaddid1	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 +𝑒 0 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elxr	⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
2		0re	⊢ 0 ∈ ℝ
3		rexadd	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐴 +𝑒 0 ) = ( 𝐴 + 0 ) )
4	2 3	mpan2	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 +𝑒 0 ) = ( 𝐴 + 0 ) )
5		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
6	5	addid1d	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 0 ) = 𝐴 )
7	4 6	eqtrd	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 +𝑒 0 ) = 𝐴 )
8		0xr	⊢ 0 ∈ ℝ*
9		renemnf	⊢ ( 0 ∈ ℝ → 0 ≠ -∞ )
10	2 9	ax-mp	⊢ 0 ≠ -∞
11		xaddpnf2	⊢ ( ( 0 ∈ ℝ* ∧ 0 ≠ -∞ ) → ( +∞ +𝑒 0 ) = +∞ )
12	8 10 11	mp2an	⊢ ( +∞ +𝑒 0 ) = +∞
13		oveq1	⊢ ( 𝐴 = +∞ → ( 𝐴 +𝑒 0 ) = ( +∞ +𝑒 0 ) )
14		id	⊢ ( 𝐴 = +∞ → 𝐴 = +∞ )
15	12 13 14	3eqtr4a	⊢ ( 𝐴 = +∞ → ( 𝐴 +𝑒 0 ) = 𝐴 )
16		renepnf	⊢ ( 0 ∈ ℝ → 0 ≠ +∞ )
17	2 16	ax-mp	⊢ 0 ≠ +∞
18		xaddmnf2	⊢ ( ( 0 ∈ ℝ* ∧ 0 ≠ +∞ ) → ( -∞ +𝑒 0 ) = -∞ )
19	8 17 18	mp2an	⊢ ( -∞ +𝑒 0 ) = -∞
20		oveq1	⊢ ( 𝐴 = -∞ → ( 𝐴 +𝑒 0 ) = ( -∞ +𝑒 0 ) )
21		id	⊢ ( 𝐴 = -∞ → 𝐴 = -∞ )
22	19 20 21	3eqtr4a	⊢ ( 𝐴 = -∞ → ( 𝐴 +𝑒 0 ) = 𝐴 )
23	7 15 22	3jaoi	⊢ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) → ( 𝐴 +𝑒 0 ) = 𝐴 )
24	1 23	sylbi	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 +𝑒 0 ) = 𝐴 )