Metamath Proof Explorer

Theorem xaddmnf2

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

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

Proof

Step Hyp Ref Expression
1 mnfxr ⊢ −∞ ∈ ℝ *
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 mnfnepnf ⊢ −∞ ≠ +∞
5 ifnefalse ⊢ −∞ ≠ +∞ → if −∞ = +∞ if A = −∞ 0 +∞ if −∞ = −∞ if A = +∞ 0 −∞ if A = +∞ +∞ if A = −∞ −∞ −∞ + A = if −∞ = −∞ if A = +∞ 0 −∞ if A = +∞ +∞ if A = −∞ −∞ −∞ + A
6 4 5 ax-mp ⊢ if −∞ = +∞ if A = −∞ 0 +∞ if −∞ = −∞ if A = +∞ 0 −∞ if A = +∞ +∞ if A = −∞ −∞ −∞ + A = if −∞ = −∞ if A = +∞ 0 −∞ if A = +∞ +∞ if A = −∞ −∞ −∞ + A
7 eqid ⊢ −∞ = −∞
8 7 iftruei ⊢ if −∞ = −∞ if A = +∞ 0 −∞ if A = +∞ +∞ if A = −∞ −∞ −∞ + A = if A = +∞ 0 −∞
9 6 8 eqtri ⊢ if −∞ = +∞ if A = −∞ 0 +∞ if −∞ = −∞ if A = +∞ 0 −∞ if A = +∞ +∞ if A = −∞ −∞ −∞ + A = if A = +∞ 0 −∞
10 ifnefalse ⊢ A ≠ +∞ → if A = +∞ 0 −∞ = −∞
11 9 10 syl5eq ⊢ A ≠ +∞ → if −∞ = +∞ if A = −∞ 0 +∞ if −∞ = −∞ if A = +∞ 0 −∞ if A = +∞ +∞ if A = −∞ −∞ −∞ + A = −∞
12 3 11 sylan9eq ⊢ A ∈ ℝ * ∧ A ≠ +∞ → −∞ + 𝑒 A = −∞