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

Metamath Proof Explorer

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