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