Metamath Proof Explorer

Theorem xaddmnf1

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

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

Proof

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