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