xmulmnf1

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

		Ref	Expression
	Assertion	xmulmnf1	$⊢ (A \in ℝ^{*} \land 0 < A) \to A \cdot_{𝑒} −∞ = −∞$

Step	Hyp	Ref	Expression
1		xnegpnf	$⊢ - +∞ = −∞$
2	1	oveq2i	$⊢ A \cdot_{𝑒} (- +∞) = A \cdot_{𝑒} −∞$
3		simpl	$⊢ (A \in ℝ^{} \land 0 < A) \to A \in ℝ^{}$
4		pnfxr	$⊢ +∞ \in ℝ^{*}$
5		xmulneg2	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{}) \to A \cdot_{𝑒} (- +∞) = - (A \cdot_{𝑒} +∞)$
6	3 4 5	sylancl	$⊢ (A \in ℝ^{*} \land 0 < A) \to A \cdot_{𝑒} (- +∞) = - (A \cdot_{𝑒} +∞)$
7		xmulpnf1	$⊢ (A \in ℝ^{*} \land 0 < A) \to A \cdot_{𝑒} +∞ = +∞$
8		xnegeq	$⊢ A \cdot_{𝑒} +∞ = +∞ \to - (A \cdot_{𝑒} +∞) = - +∞$
9	7 8	syl	$⊢ (A \in ℝ^{*} \land 0 < A) \to - (A \cdot_{𝑒} +∞) = - +∞$
10	9 1	eqtrdi	$⊢ (A \in ℝ^{*} \land 0 < A) \to - (A \cdot_{𝑒} +∞) = −∞$
11	6 10	eqtrd	$⊢ (A \in ℝ^{*} \land 0 < A) \to A \cdot_{𝑒} (- +∞) = −∞$
12	2 11	eqtr3id	$⊢ (A \in ℝ^{*} \land 0 < A) \to A \cdot_{𝑒} −∞ = −∞$

Metamath Proof Explorer