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

Metamath Proof Explorer

Theorem xaddrid

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

Ref Expression
Assertion xaddrid ( 𝐴 ∈ ℝ* → ( 𝐴 +𝑒 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 addridd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 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 ) = 𝐴 )