Metamath Proof Explorer

Theorem xaddmnf2

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

Ref Expression
Assertion xaddmnf2 ⊢A∈ℝ*∧A≠+∞→−∞+𝑒A=−∞

Proof

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