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