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 + 𝑒 −∞ = 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 ifnefalse ⊢ A ≠ +∞ → if A = +∞ if −∞ = −∞ 0 +∞ if A = −∞ if −∞ = +∞ 0 −∞ if −∞ = +∞ +∞ if −∞ = −∞ −∞ A + −∞ = if A = −∞ 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 + −∞ = −∞ → if A = −∞ if −∞ = +∞ 0 −∞ if −∞ = +∞ +∞ if −∞ = −∞ −∞ A + −∞ = if A = −∞ −∞ −∞
14 7 12 13 mp2an ⊢ if A = −∞ if −∞ = +∞ 0 −∞ if −∞ = +∞ +∞ if −∞ = −∞ −∞ A + −∞ = if A = −∞ −∞ −∞
15 ifid ⊢ if A = −∞ −∞ −∞ = −∞
16 14 15 eqtri ⊢ if A = −∞ if −∞ = +∞ 0 −∞ if −∞ = +∞ +∞ if −∞ = −∞ −∞ A + −∞ = −∞
17 4 16 eqtrdi ⊢ A ≠ +∞ → if A = +∞ if −∞ = −∞ 0 +∞ if A = −∞ if −∞ = +∞ 0 −∞ if −∞ = +∞ +∞ if −∞ = −∞ −∞ A + −∞ = −∞
18 3 17 sylan9eq ⊢ A ∈ ℝ * ∧ A ≠ +∞ → A + 𝑒 −∞ = −∞