Theorem xmulmnf1

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

	Ref	Expression
Assertion	xmulmnf1	$$⊢\left(A\in {ℝ}^{*}\wedge 0<A\right)\to A{\cdot }_{𝑒}\mathrm{-\infty }=\mathrm{-\infty }$$

Proof

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