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

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