# Metamath Proof Explorer

## Theorem xnegid

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

Ref Expression
Assertion xnegid $⊢ A ∈ ℝ * → A + 𝑒 − A = 0$

### Proof

Step Hyp Ref Expression
1 elxr $⊢ A ∈ ℝ * ↔ A ∈ ℝ ∨ A = +∞ ∨ A = −∞$
2 rexneg $⊢ A ∈ ℝ → − A = − A$
3 2 oveq2d $⊢ A ∈ ℝ → A + 𝑒 − A = A + 𝑒 − A$
4 renegcl $⊢ A ∈ ℝ → − A ∈ ℝ$
5 rexadd $⊢ A ∈ ℝ ∧ − A ∈ ℝ → A + 𝑒 − A = A + − A$
6 4 5 mpdan $⊢ A ∈ ℝ → A + 𝑒 − A = A + − A$
7 recn $⊢ A ∈ ℝ → A ∈ ℂ$
8 7 negidd $⊢ A ∈ ℝ → A + − A = 0$
9 3 6 8 3eqtrd $⊢ A ∈ ℝ → A + 𝑒 − A = 0$
10 id $⊢ A = +∞ → A = +∞$
11 xnegeq $⊢ A = +∞ → − A = − +∞$
12 xnegpnf $⊢ − +∞ = −∞$
13 11 12 eqtrdi $⊢ A = +∞ → − A = −∞$
14 10 13 oveq12d $⊢ A = +∞ → A + 𝑒 − A = +∞ + 𝑒 −∞$
15 pnfaddmnf $⊢ +∞ + 𝑒 −∞ = 0$
16 14 15 eqtrdi $⊢ A = +∞ → A + 𝑒 − A = 0$
17 id $⊢ A = −∞ → A = −∞$
18 xnegeq $⊢ A = −∞ → − A = − −∞$
19 xnegmnf $⊢ − −∞ = +∞$
20 18 19 eqtrdi $⊢ A = −∞ → − A = +∞$
21 17 20 oveq12d $⊢ A = −∞ → A + 𝑒 − A = −∞ + 𝑒 +∞$
22 mnfaddpnf $⊢ −∞ + 𝑒 +∞ = 0$
23 21 22 eqtrdi $⊢ A = −∞ → A + 𝑒 − A = 0$
24 9 16 23 3jaoi $⊢ A ∈ ℝ ∨ A = +∞ ∨ A = −∞ → A + 𝑒 − A = 0$
25 1 24 sylbi $⊢ A ∈ ℝ * → A + 𝑒 − A = 0$