Metamath Proof Explorer

Theorem xmulpnf1n

Description: Multiplication by plus infinity on the right, for negative input. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmulpnf1n ⊢ A ∈ ℝ * ∧ A < 0 → A ⋅ 𝑒 +∞ = −∞

Proof

Step Hyp Ref Expression
1 simpl ⊢ A ∈ ℝ * ∧ A < 0 → A ∈ ℝ *
2 pnfxr ⊢ +∞ ∈ ℝ *
3 xmulneg1 ⊢ A ∈ ℝ * ∧ +∞ ∈ ℝ * → − A ⋅ 𝑒 +∞ = − A ⋅ 𝑒 +∞
4 1 2 3 sylancl ⊢ A ∈ ℝ * ∧ A < 0 → − A ⋅ 𝑒 +∞ = − A ⋅ 𝑒 +∞
5 xnegcl ⊢ A ∈ ℝ * → − A ∈ ℝ *
6 xlt0neg1 ⊢ A ∈ ℝ * → A < 0 ↔ 0 < − A
7 6 biimpa ⊢ A ∈ ℝ * ∧ A < 0 → 0 < − A
8 xmulpnf1 ⊢ − A ∈ ℝ * ∧ 0 < − A → − A ⋅ 𝑒 +∞ = +∞
9 5 7 8 syl2an2r ⊢ A ∈ ℝ * ∧ A < 0 → − A ⋅ 𝑒 +∞ = +∞
10 4 9 eqtr3d ⊢ A ∈ ℝ * ∧ A < 0 → − A ⋅ 𝑒 +∞ = +∞
11 xnegmnf ⊢ − −∞ = +∞
12 10 11 eqtr4di ⊢ A ∈ ℝ * ∧ A < 0 → − A ⋅ 𝑒 +∞ = − −∞
13 xmulcl ⊢ A ∈ ℝ * ∧ +∞ ∈ ℝ * → A ⋅ 𝑒 +∞ ∈ ℝ *
14 1 2 13 sylancl ⊢ A ∈ ℝ * ∧ A < 0 → A ⋅ 𝑒 +∞ ∈ ℝ *
15 mnfxr ⊢ −∞ ∈ ℝ *
16 xneg11 ⊢ A ⋅ 𝑒 +∞ ∈ ℝ * ∧ −∞ ∈ ℝ * → − A ⋅ 𝑒 +∞ = − −∞ ↔ A ⋅ 𝑒 +∞ = −∞
17 14 15 16 sylancl ⊢ A ∈ ℝ * ∧ A < 0 → − A ⋅ 𝑒 +∞ = − −∞ ↔ A ⋅ 𝑒 +∞ = −∞
18 12 17 mpbid ⊢ A ∈ ℝ * ∧ A < 0 → A ⋅ 𝑒 +∞ = −∞