Theorem xaddmnf2

Description: Addition of negative infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xaddmnf2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) → ( -∞ +𝑒 𝐴 ) = -∞ )

Proof

Step	Hyp	Ref	Expression
1		mnfxr	⊢ -∞ ∈ ℝ*
2		xaddval	⊢ ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( -∞ +𝑒 𝐴 ) = if ( -∞ = +∞ , if ( 𝐴 = -∞ , 0 , +∞ ) , if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) ) ) )
3	1 2	mpan	⊢ ( 𝐴 ∈ ℝ* → ( -∞ +𝑒 𝐴 ) = if ( -∞ = +∞ , if ( 𝐴 = -∞ , 0 , +∞ ) , if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) ) ) )
4		mnfnepnf	⊢ -∞ ≠ +∞
5		ifnefalse	⊢ ( -∞ ≠ +∞ → if ( -∞ = +∞ , if ( 𝐴 = -∞ , 0 , +∞ ) , if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) ) ) = if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) ) )
6	4 5	ax-mp	⊢ if ( -∞ = +∞ , if ( 𝐴 = -∞ , 0 , +∞ ) , if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) ) ) = if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) )
7		eqid	⊢ -∞ = -∞
8	7	iftruei	⊢ if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) ) = if ( 𝐴 = +∞ , 0 , -∞ )
9	6 8	eqtri	⊢ if ( -∞ = +∞ , if ( 𝐴 = -∞ , 0 , +∞ ) , if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) ) ) = if ( 𝐴 = +∞ , 0 , -∞ )
10		ifnefalse	⊢ ( 𝐴 ≠ +∞ → if ( 𝐴 = +∞ , 0 , -∞ ) = -∞ )
11	9 10	eqtrid	⊢ ( 𝐴 ≠ +∞ → if ( -∞ = +∞ , if ( 𝐴 = -∞ , 0 , +∞ ) , if ( -∞ = -∞ , if ( 𝐴 = +∞ , 0 , -∞ ) , if ( 𝐴 = +∞ , +∞ , if ( 𝐴 = -∞ , -∞ , ( -∞ + 𝐴 ) ) ) ) ) = -∞ )
12	3 11	sylan9eq	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) → ( -∞ +𝑒 𝐴 ) = -∞ )