This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 +∞ ) = -∞ )