Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  xaddid1 Structured version   Visualization version   GIF version

 Description: Extended real version of addid1 10422. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xaddid1 (𝐴 ∈ ℝ* → (𝐴 +𝑒 0) = 𝐴)

Proof of Theorem xaddid1
StepHypRef Expression
1 elxr 12155 . 2 (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2 0re 10246 . . . . 5 0 ∈ ℝ
3 rexadd 12268 . . . . 5 ((𝐴 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐴 +𝑒 0) = (𝐴 + 0))
42, 3mpan2 671 . . . 4 (𝐴 ∈ ℝ → (𝐴 +𝑒 0) = (𝐴 + 0))
5 recn 10232 . . . . 5 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
65addid1d 10442 . . . 4 (𝐴 ∈ ℝ → (𝐴 + 0) = 𝐴)
74, 6eqtrd 2805 . . 3 (𝐴 ∈ ℝ → (𝐴 +𝑒 0) = 𝐴)
8 0xr 10292 . . . . 5 0 ∈ ℝ*
9 renemnf 10294 . . . . . 6 (0 ∈ ℝ → 0 ≠ -∞)
102, 9ax-mp 5 . . . . 5 0 ≠ -∞
11 xaddpnf2 12263 . . . . 5 ((0 ∈ ℝ* ∧ 0 ≠ -∞) → (+∞ +𝑒 0) = +∞)
128, 10, 11mp2an 672 . . . 4 (+∞ +𝑒 0) = +∞
13 oveq1 6803 . . . 4 (𝐴 = +∞ → (𝐴 +𝑒 0) = (+∞ +𝑒 0))
14 id 22 . . . 4 (𝐴 = +∞ → 𝐴 = +∞)
1512, 13, 143eqtr4a 2831 . . 3 (𝐴 = +∞ → (𝐴 +𝑒 0) = 𝐴)
16 renepnf 10293 . . . . . 6 (0 ∈ ℝ → 0 ≠ +∞)
172, 16ax-mp 5 . . . . 5 0 ≠ +∞
18 xaddmnf2 12265 . . . . 5 ((0 ∈ ℝ* ∧ 0 ≠ +∞) → (-∞ +𝑒 0) = -∞)
198, 17, 18mp2an 672 . . . 4 (-∞ +𝑒 0) = -∞
20 oveq1 6803 . . . 4 (𝐴 = -∞ → (𝐴 +𝑒 0) = (-∞ +𝑒 0))
21 id 22 . . . 4 (𝐴 = -∞ → 𝐴 = -∞)
2219, 20, 213eqtr4a 2831 . . 3 (𝐴 = -∞ → (𝐴 +𝑒 0) = 𝐴)
237, 15, 223jaoi 1539 . 2 ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐴 +𝑒 0) = 𝐴)
241, 23sylbi 207 1 (𝐴 ∈ ℝ* → (𝐴 +𝑒 0) = 𝐴)