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

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≠ +∞ ) → ( 𝐴 +𝑒 -∞ ) = -∞ )