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