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 +∞ = +∞ if A = −∞ 0 +∞ if +∞ = −∞ if A = +∞ 0 −∞ if A = +∞ +∞ if A = −∞ −∞ +∞ + A
3 1 2 mpan ⊢ A ∈ ℝ * → +∞ + 𝑒 A = if +∞ = +∞ if A = −∞ 0 +∞ if +∞ = −∞ if A = +∞ 0 −∞ if A = +∞ +∞ if A = −∞ −∞ +∞ + A
4 eqid ⊢ +∞ = +∞
5 4 iftruei ⊢ if +∞ = +∞ if A = −∞ 0 +∞ if +∞ = −∞ if A = +∞ 0 −∞ if A = +∞ +∞ if A = −∞ −∞ +∞ + A = if A = −∞ 0 +∞
6 ifnefalse ⊢ A ≠ −∞ → if A = −∞ 0 +∞ = +∞
7 5 6 syl5eq ⊢ A ≠ −∞ → if +∞ = +∞ if A = −∞ 0 +∞ if +∞ = −∞ if A = +∞ 0 −∞ if A = +∞ +∞ if A = −∞ −∞ +∞ + A = +∞
8 3 7 sylan9eq ⊢ A ∈ ℝ * ∧ A ≠ −∞ → +∞ + 𝑒 A = +∞