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 A * A < 0 A 𝑒 +∞ = −∞

Proof

Step Hyp Ref Expression
1 simpl A * A < 0 A *
2 pnfxr +∞ *
3 xmulneg1 A * +∞ * A 𝑒 +∞ = A 𝑒 +∞
4 1 2 3 sylancl A * A < 0 A 𝑒 +∞ = A 𝑒 +∞
5 xnegcl A * A *
6 xlt0neg1 A * A < 0 0 < A
7 6 biimpa A * A < 0 0 < A
8 xmulpnf1 A * 0 < A A 𝑒 +∞ = +∞
9 5 7 8 syl2an2r A * A < 0 A 𝑒 +∞ = +∞
10 4 9 eqtr3d A * A < 0 A 𝑒 +∞ = +∞
11 xnegmnf −∞ = +∞
12 10 11 eqtr4di A * A < 0 A 𝑒 +∞ = −∞
13 xmulcl A * +∞ * A 𝑒 +∞ *
14 1 2 13 sylancl A * A < 0 A 𝑒 +∞ *
15 mnfxr −∞ *
16 xneg11 A 𝑒 +∞ * −∞ * A 𝑒 +∞ = −∞ A 𝑒 +∞ = −∞
17 14 15 16 sylancl A * A < 0 A 𝑒 +∞ = −∞ A 𝑒 +∞ = −∞
18 12 17 mpbid A * A < 0 A 𝑒 +∞ = −∞