Metamath Proof Explorer

Theorem pnfaddmnf

Description: Addition of positive and negative infinity. This is often taken to be a "null" value or out of the domain, but we define it (somewhat arbitrarily) to be zero so that the resulting function is total, which simplifies proofs. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion pnfaddmnf ⊢ +∞ + 𝑒 −∞ = 0

Proof

Step Hyp Ref Expression
1 pnfxr ⊢ +∞ ∈ ℝ *
2 mnfxr ⊢ −∞ ∈ ℝ *
3 xaddval ⊢ +∞ ∈ ℝ * ∧ −∞ ∈ ℝ * → +∞ + 𝑒 −∞ = if +∞ = +∞ if −∞ = −∞ 0 +∞ if +∞ = −∞ if −∞ = +∞ 0 −∞ if −∞ = +∞ +∞ if −∞ = −∞ −∞ +∞ + −∞
4 1 2 3 mp2an ⊢ +∞ + 𝑒 −∞ = if +∞ = +∞ if −∞ = −∞ 0 +∞ if +∞ = −∞ if −∞ = +∞ 0 −∞ if −∞ = +∞ +∞ if −∞ = −∞ −∞ +∞ + −∞
5 eqid ⊢ +∞ = +∞
6 5 iftruei ⊢ if +∞ = +∞ if −∞ = −∞ 0 +∞ if +∞ = −∞ if −∞ = +∞ 0 −∞ if −∞ = +∞ +∞ if −∞ = −∞ −∞ +∞ + −∞ = if −∞ = −∞ 0 +∞
7 eqid ⊢ −∞ = −∞
8 7 iftruei ⊢ if −∞ = −∞ 0 +∞ = 0
9 4 6 8 3eqtri ⊢ +∞ + 𝑒 −∞ = 0