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