This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 -∞ ) = -∞ )