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