Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  xaddmnf2 Structured version   Visualization version   GIF version

 Description: Addition of negative infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xaddmnf2 ((𝐴 ∈ ℝ*𝐴 ≠ +∞) → (-∞ +𝑒 𝐴) = -∞)

StepHypRef Expression
1 mnfxr 10093 . . 3 -∞ ∈ ℝ*
2 xaddval 12051 . . 3 ((-∞ ∈ ℝ*𝐴 ∈ ℝ*) → (-∞ +𝑒 𝐴) = if(-∞ = +∞, if(𝐴 = -∞, 0, +∞), if(-∞ = -∞, if(𝐴 = +∞, 0, -∞), if(𝐴 = +∞, +∞, if(𝐴 = -∞, -∞, (-∞ + 𝐴))))))
31, 2mpan 706 . 2 (𝐴 ∈ ℝ* → (-∞ +𝑒 𝐴) = if(-∞ = +∞, if(𝐴 = -∞, 0, +∞), if(-∞ = -∞, if(𝐴 = +∞, 0, -∞), if(𝐴 = +∞, +∞, if(𝐴 = -∞, -∞, (-∞ + 𝐴))))))
4 mnfnepnf 10092 . . . . 5 -∞ ≠ +∞
5 ifnefalse 4096 . . . . 5 (-∞ ≠ +∞ → if(-∞ = +∞, if(𝐴 = -∞, 0, +∞), if(-∞ = -∞, if(𝐴 = +∞, 0, -∞), if(𝐴 = +∞, +∞, if(𝐴 = -∞, -∞, (-∞ + 𝐴))))) = if(-∞ = -∞, if(𝐴 = +∞, 0, -∞), if(𝐴 = +∞, +∞, if(𝐴 = -∞, -∞, (-∞ + 𝐴)))))
64, 5ax-mp 5 . . . 4 if(-∞ = +∞, if(𝐴 = -∞, 0, +∞), if(-∞ = -∞, if(𝐴 = +∞, 0, -∞), if(𝐴 = +∞, +∞, if(𝐴 = -∞, -∞, (-∞ + 𝐴))))) = if(-∞ = -∞, if(𝐴 = +∞, 0, -∞), if(𝐴 = +∞, +∞, if(𝐴 = -∞, -∞, (-∞ + 𝐴))))
7 eqid 2621 . . . . 5 -∞ = -∞
87iftruei 4091 . . . 4 if(-∞ = -∞, if(𝐴 = +∞, 0, -∞), if(𝐴 = +∞, +∞, if(𝐴 = -∞, -∞, (-∞ + 𝐴)))) = if(𝐴 = +∞, 0, -∞)
96, 8eqtri 2643 . . 3 if(-∞ = +∞, if(𝐴 = -∞, 0, +∞), if(-∞ = -∞, if(𝐴 = +∞, 0, -∞), if(𝐴 = +∞, +∞, if(𝐴 = -∞, -∞, (-∞ + 𝐴))))) = if(𝐴 = +∞, 0, -∞)
10 ifnefalse 4096 . . 3 (𝐴 ≠ +∞ → if(𝐴 = +∞, 0, -∞) = -∞)
119, 10syl5eq 2667 . 2 (𝐴 ≠ +∞ → if(-∞ = +∞, if(𝐴 = -∞, 0, +∞), if(-∞ = -∞, if(𝐴 = +∞, 0, -∞), if(𝐴 = +∞, +∞, if(𝐴 = -∞, -∞, (-∞ + 𝐴))))) = -∞)
123, 11sylan9eq 2675 1 ((𝐴 ∈ ℝ*𝐴 ≠ +∞) → (-∞ +𝑒 𝐴) = -∞)