Metamath Proof Explorer

Theorem xaddpnf2

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

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

Proof

Step Hyp Ref Expression
1 pnfxr ⊢+∞∈ℝ*
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 eqid ⊢+∞=+∞
5 4 iftruei ⊢if+∞=+∞ifA=−∞0+∞if+∞=−∞ifA=+∞0−∞ifA=+∞+∞ifA=−∞−∞+∞+A=ifA=−∞0+∞
6 ifnefalse ⊢A≠−∞→ifA=−∞0+∞=+∞
7 5 6 eqtrid ⊢A≠−∞→if+∞=+∞ifA=−∞0+∞if+∞=−∞ifA=+∞0−∞ifA=+∞+∞ifA=−∞−∞+∞+A=+∞
8 3 7 sylan9eq ⊢A∈ℝ*∧A≠−∞→+∞+𝑒A=+∞