Metamath Proof Explorer


Theorem xmulmnf1

Description: Multiplication by minus infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmulmnf1 ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 𝐴 ·e -∞ ) = -∞ )

Proof

Step Hyp Ref Expression
1 xnegpnf -𝑒 +∞ = -∞
2 1 oveq2i ( 𝐴 ·e -𝑒 +∞ ) = ( 𝐴 ·e -∞ )
3 simpl ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → 𝐴 ∈ ℝ* )
4 pnfxr +∞ ∈ ℝ*
5 xmulneg2 ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐴 ·e -𝑒 +∞ ) = -𝑒 ( 𝐴 ·e +∞ ) )
6 3 4 5 sylancl ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 𝐴 ·e -𝑒 +∞ ) = -𝑒 ( 𝐴 ·e +∞ ) )
7 xmulpnf1 ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 𝐴 ·e +∞ ) = +∞ )
8 xnegeq ( ( 𝐴 ·e +∞ ) = +∞ → -𝑒 ( 𝐴 ·e +∞ ) = -𝑒 +∞ )
9 7 8 syl ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → -𝑒 ( 𝐴 ·e +∞ ) = -𝑒 +∞ )
10 9 1 eqtrdi ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → -𝑒 ( 𝐴 ·e +∞ ) = -∞ )
11 6 10 eqtrd ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 𝐴 ·e -𝑒 +∞ ) = -∞ )
12 2 11 eqtr3id ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( 𝐴 ·e -∞ ) = -∞ )