xmulmnf2

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

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

Step	Hyp	Ref	Expression
1		mnfxr	$⊢ −∞ \in ℝ^{*}$
2		xmulcom	$⊢ (−∞ \in ℝ^{} \land A \in ℝ^{}) \to −∞ \cdot_{𝑒} A = A \cdot_{𝑒} −∞$
3	1 2	mpan	$⊢ A \in ℝ^{*} \to −∞ \cdot_{𝑒} A = A \cdot_{𝑒} −∞$
4	3	adantr	$⊢ (A \in ℝ^{*} \land 0 < A) \to −∞ \cdot_{𝑒} A = A \cdot_{𝑒} −∞$
5		xmulmnf1	$⊢ (A \in ℝ^{*} \land 0 < A) \to A \cdot_{𝑒} −∞ = −∞$
6	4 5	eqtrd	$⊢ (A \in ℝ^{*} \land 0 < A) \to −∞ \cdot_{𝑒} A = −∞$

Metamath Proof Explorer