xmulpnf1n

Description: Multiplication by plus infinity on the right, for negative input. (Contributed by Mario Carneiro, 20-Aug-2015)

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

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ℝ^{} \land A < 0) \to A \in ℝ^{}$
2		pnfxr	$⊢ +∞ \in ℝ^{*}$
3		xmulneg1	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{}) \to (- A) \cdot_{𝑒} +∞ = - (A \cdot_{𝑒} +∞)$
4	1 2 3	sylancl	$⊢ (A \in ℝ^{*} \land A < 0) \to (- A) \cdot_{𝑒} +∞ = - (A \cdot_{𝑒} +∞)$
5		xnegcl	$⊢ A \in ℝ^{} \to - A \in ℝ^{}$
6		xlt0neg1	$⊢ A \in ℝ^{*} \to (A < 0 \leftrightarrow 0 < - A)$
7	6	biimpa	$⊢ (A \in ℝ^{*} \land A < 0) \to 0 < - A$
8		xmulpnf1	$⊢ (- A \in ℝ^{*} \land 0 < - A) \to (- A) \cdot_{𝑒} +∞ = +∞$
9	5 7 8	syl2an2r	$⊢ (A \in ℝ^{*} \land A < 0) \to (- A) \cdot_{𝑒} +∞ = +∞$
10	4 9	eqtr3d	$⊢ (A \in ℝ^{*} \land A < 0) \to - (A \cdot_{𝑒} +∞) = +∞$
11		xnegmnf	$⊢ - −∞ = +∞$
12	10 11	eqtr4di	$⊢ (A \in ℝ^{*} \land A < 0) \to - (A \cdot_{𝑒} +∞) = - −∞$
13		xmulcl	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{}) \to A \cdot_{𝑒} +∞ \in ℝ^{*}$
14	1 2 13	sylancl	$⊢ (A \in ℝ^{} \land A < 0) \to A \cdot_{𝑒} +∞ \in ℝ^{}$
15		mnfxr	$⊢ −∞ \in ℝ^{*}$
16		xneg11	$⊢ (A \cdot_{𝑒} +∞ \in ℝ^{} \land −∞ \in ℝ^{}) \to (- (A \cdot_{𝑒} +∞) = - −∞ \leftrightarrow A \cdot_{𝑒} +∞ = −∞)$
17	14 15 16	sylancl	$⊢ (A \in ℝ^{*} \land A < 0) \to (- (A \cdot_{𝑒} +∞) = - −∞ \leftrightarrow A \cdot_{𝑒} +∞ = −∞)$
18	12 17	mpbid	$⊢ (A \in ℝ^{*} \land A < 0) \to A \cdot_{𝑒} +∞ = −∞$

Metamath Proof Explorer