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