Theorem xaddmnf1

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

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

Proof

Step	Hyp	Ref	Expression
1		mnfxr	⊢ -∞ ∈ ℝ*
2		xaddval	⊢ ( ( 𝐴 ∈ ℝ* ∧ -∞ ∈ ℝ* ) → ( 𝐴 +𝑒 -∞ ) = if ( 𝐴 = +∞ , if ( -∞ = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( -∞ = +∞ , 0 , -∞ ) , if ( -∞ = +∞ , +∞ , if ( -∞ = -∞ , -∞ , ( 𝐴 + -∞ ) ) ) ) ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 +𝑒 -∞ ) = if ( 𝐴 = +∞ , if ( -∞ = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( -∞ = +∞ , 0 , -∞ ) , if ( -∞ = +∞ , +∞ , if ( -∞ = -∞ , -∞ , ( 𝐴 + -∞ ) ) ) ) ) )
4		ifnefalse	⊢ ( 𝐴 ≠ +∞ → if ( 𝐴 = +∞ , if ( -∞ = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( -∞ = +∞ , 0 , -∞ ) , if ( -∞ = +∞ , +∞ , if ( -∞ = -∞ , -∞ , ( 𝐴 + -∞ ) ) ) ) ) = if ( 𝐴 = -∞ , if ( -∞ = +∞ , 0 , -∞ ) , if ( -∞ = +∞ , +∞ , if ( -∞ = -∞ , -∞ , ( 𝐴 + -∞ ) ) ) ) )
5		mnfnepnf	⊢ -∞ ≠ +∞
6		ifnefalse	⊢ ( -∞ ≠ +∞ → if ( -∞ = +∞ , 0 , -∞ ) = -∞ )
7	5 6	ax-mp	⊢ if ( -∞ = +∞ , 0 , -∞ ) = -∞
8		ifnefalse	⊢ ( -∞ ≠ +∞ → if ( -∞ = +∞ , +∞ , if ( -∞ = -∞ , -∞ , ( 𝐴 + -∞ ) ) ) = if ( -∞ = -∞ , -∞ , ( 𝐴 + -∞ ) ) )
9	5 8	ax-mp	⊢ if ( -∞ = +∞ , +∞ , if ( -∞ = -∞ , -∞ , ( 𝐴 + -∞ ) ) ) = if ( -∞ = -∞ , -∞ , ( 𝐴 + -∞ ) )
10		eqid	⊢ -∞ = -∞
11	10	iftruei	⊢ if ( -∞ = -∞ , -∞ , ( 𝐴 + -∞ ) ) = -∞
12	9 11	eqtri	⊢ if ( -∞ = +∞ , +∞ , if ( -∞ = -∞ , -∞ , ( 𝐴 + -∞ ) ) ) = -∞
13		ifeq12	⊢ ( ( if ( -∞ = +∞ , 0 , -∞ ) = -∞ ∧ if ( -∞ = +∞ , +∞ , if ( -∞ = -∞ , -∞ , ( 𝐴 + -∞ ) ) ) = -∞ ) → if ( 𝐴 = -∞ , if ( -∞ = +∞ , 0 , -∞ ) , if ( -∞ = +∞ , +∞ , if ( -∞ = -∞ , -∞ , ( 𝐴 + -∞ ) ) ) ) = if ( 𝐴 = -∞ , -∞ , -∞ ) )
14	7 12 13	mp2an	⊢ if ( 𝐴 = -∞ , if ( -∞ = +∞ , 0 , -∞ ) , if ( -∞ = +∞ , +∞ , if ( -∞ = -∞ , -∞ , ( 𝐴 + -∞ ) ) ) ) = if ( 𝐴 = -∞ , -∞ , -∞ )
15		ifid	⊢ if ( 𝐴 = -∞ , -∞ , -∞ ) = -∞
16	14 15	eqtri	⊢ if ( 𝐴 = -∞ , if ( -∞ = +∞ , 0 , -∞ ) , if ( -∞ = +∞ , +∞ , if ( -∞ = -∞ , -∞ , ( 𝐴 + -∞ ) ) ) ) = -∞
17	4 16	eqtrdi	⊢ ( 𝐴 ≠ +∞ → if ( 𝐴 = +∞ , if ( -∞ = -∞ , 0 , +∞ ) , if ( 𝐴 = -∞ , if ( -∞ = +∞ , 0 , -∞ ) , if ( -∞ = +∞ , +∞ , if ( -∞ = -∞ , -∞ , ( 𝐴 + -∞ ) ) ) ) ) = -∞ )
18	3 17	sylan9eq	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) → ( 𝐴 +𝑒 -∞ ) = -∞ )