Metamath Proof Explorer

Theorem xaddpnf1

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

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

Proof

Step Hyp Ref Expression
1 pnfxr ⊢+∞∈ℝ*
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 pnfnemnf ⊢+∞≠−∞
5 ifnefalse ⊢+∞≠−∞→if+∞=−∞0+∞=+∞
6 4 5 mp1i ⊢A≠−∞→if+∞=−∞0+∞=+∞
7 ifnefalse ⊢A≠−∞→ifA=−∞if+∞=+∞0−∞if+∞=+∞+∞if+∞=−∞−∞A++∞=if+∞=+∞+∞if+∞=−∞−∞A++∞
8 eqid ⊢+∞=+∞
9 8 iftruei ⊢if+∞=+∞+∞if+∞=−∞−∞A++∞=+∞
10 7 9 eqtrdi ⊢A≠−∞→ifA=−∞if+∞=+∞0−∞if+∞=+∞+∞if+∞=−∞−∞A++∞=+∞
11 6 10 ifeq12d ⊢A≠−∞→ifA=+∞if+∞=−∞0+∞ifA=−∞if+∞=+∞0−∞if+∞=+∞+∞if+∞=−∞−∞A++∞=ifA=+∞+∞+∞
12 ifid ⊢ifA=+∞+∞+∞=+∞
13 11 12 eqtrdi ⊢A≠−∞→ifA=+∞if+∞=−∞0+∞ifA=−∞if+∞=+∞0−∞if+∞=+∞+∞if+∞=−∞−∞A++∞=+∞
14 3 13 sylan9eq ⊢A∈ℝ*∧A≠−∞→A+𝑒+∞=+∞