This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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