Theorem xmulpnf1n

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

	Ref	Expression
Assertion	xmulpnf1n	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ( 𝐴 ·e +∞ ) = -∞ )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → 𝐴 ∈ ℝ* )
2		pnfxr	⊢ +∞ ∈ ℝ*
3		xmulneg1	⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( -𝑒 𝐴 ·e +∞ ) = -𝑒 ( 𝐴 ·e +∞ ) )
4	1 2 3	sylancl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ( -𝑒 𝐴 ·e +∞ ) = -𝑒 ( 𝐴 ·e +∞ ) )
5		xnegcl	⊢ ( 𝐴 ∈ ℝ* → -𝑒 𝐴 ∈ ℝ* )
6		xlt0neg1	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 < 0 ↔ 0 < -𝑒 𝐴 ) )
7	6	biimpa	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → 0 < -𝑒 𝐴 )
8		xmulpnf1	⊢ ( ( -𝑒 𝐴 ∈ ℝ* ∧ 0 < -𝑒 𝐴 ) → ( -𝑒 𝐴 ·e +∞ ) = +∞ )
9	5 7 8	syl2an2r	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ( -𝑒 𝐴 ·e +∞ ) = +∞ )
10	4 9	eqtr3d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → -𝑒 ( 𝐴 ·e +∞ ) = +∞ )
11		xnegmnf	⊢ -𝑒 -∞ = +∞
12	10 11	eqtr4di	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → -𝑒 ( 𝐴 ·e +∞ ) = -𝑒 -∞ )
13		xmulcl	⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐴 ·e +∞ ) ∈ ℝ* )
14	1 2 13	sylancl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ( 𝐴 ·e +∞ ) ∈ ℝ* )
15		mnfxr	⊢ -∞ ∈ ℝ*
16		xneg11	⊢ ( ( ( 𝐴 ·e +∞ ) ∈ ℝ* ∧ -∞ ∈ ℝ* ) → ( -𝑒 ( 𝐴 ·e +∞ ) = -𝑒 -∞ ↔ ( 𝐴 ·e +∞ ) = -∞ ) )
17	14 15 16	sylancl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ( -𝑒 ( 𝐴 ·e +∞ ) = -𝑒 -∞ ↔ ( 𝐴 ·e +∞ ) = -∞ ) )
18	12 17	mpbid	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ( 𝐴 ·e +∞ ) = -∞ )