Metamath Proof Explorer

Theorem mnfaddpnf

Description: Addition of negative and positive 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 mnfaddpnf ⊢ −∞ + 𝑒 +∞ = 0

Proof

Step Hyp Ref Expression
1 mnfxr ⊢ −∞ ∈ ℝ *
2 pnfxr ⊢ +∞ ∈ ℝ *
3 xaddval ⊢ −∞ ∈ ℝ * ∧ +∞ ∈ ℝ * → −∞ + 𝑒 +∞ = if −∞ = +∞ if +∞ = −∞ 0 +∞ if −∞ = −∞ if +∞ = +∞ 0 −∞ if +∞ = +∞ +∞ if +∞ = −∞ −∞ −∞ + +∞
4 1 2 3 mp2an ⊢ −∞ + 𝑒 +∞ = if −∞ = +∞ if +∞ = −∞ 0 +∞ if −∞ = −∞ if +∞ = +∞ 0 −∞ if +∞ = +∞ +∞ if +∞ = −∞ −∞ −∞ + +∞
5 mnfnepnf ⊢ −∞ ≠ +∞
6 ifnefalse ⊢ −∞ ≠ +∞ → if −∞ = +∞ if +∞ = −∞ 0 +∞ if −∞ = −∞ if +∞ = +∞ 0 −∞ if +∞ = +∞ +∞ if +∞ = −∞ −∞ −∞ + +∞ = if −∞ = −∞ if +∞ = +∞ 0 −∞ if +∞ = +∞ +∞ if +∞ = −∞ −∞ −∞ + +∞
7 5 6 ax-mp ⊢ if −∞ = +∞ if +∞ = −∞ 0 +∞ if −∞ = −∞ if +∞ = +∞ 0 −∞ if +∞ = +∞ +∞ if +∞ = −∞ −∞ −∞ + +∞ = if −∞ = −∞ if +∞ = +∞ 0 −∞ if +∞ = +∞ +∞ if +∞ = −∞ −∞ −∞ + +∞
8 eqid ⊢ −∞ = −∞
9 8 iftruei ⊢ if −∞ = −∞ if +∞ = +∞ 0 −∞ if +∞ = +∞ +∞ if +∞ = −∞ −∞ −∞ + +∞ = if +∞ = +∞ 0 −∞
10 eqid ⊢ +∞ = +∞
11 10 iftruei ⊢ if +∞ = +∞ 0 −∞ = 0
12 9 11 eqtri ⊢ if −∞ = −∞ if +∞ = +∞ 0 −∞ if +∞ = +∞ +∞ if +∞ = −∞ −∞ −∞ + +∞ = 0
13 7 12 eqtri ⊢ if −∞ = +∞ if +∞ = −∞ 0 +∞ if −∞ = −∞ if +∞ = +∞ 0 −∞ if +∞ = +∞ +∞ if +∞ = −∞ −∞ −∞ + +∞ = 0
14 4 13 eqtri ⊢ −∞ + 𝑒 +∞ = 0