Metamath Proof Explorer


Theorem xmulmnf1

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

Ref Expression
Assertion xmulmnf1 A * 0 < A A 𝑒 −∞ = −∞

Proof

Step Hyp Ref Expression
1 xnegpnf +∞ = −∞
2 1 oveq2i A 𝑒 +∞ = A 𝑒 −∞
3 simpl A * 0 < A A *
4 pnfxr +∞ *
5 xmulneg2 A * +∞ * A 𝑒 +∞ = A 𝑒 +∞
6 3 4 5 sylancl A * 0 < A A 𝑒 +∞ = A 𝑒 +∞
7 xmulpnf1 A * 0 < A A 𝑒 +∞ = +∞
8 xnegeq A 𝑒 +∞ = +∞ A 𝑒 +∞ = +∞
9 7 8 syl A * 0 < A A 𝑒 +∞ = +∞
10 9 1 eqtrdi A * 0 < A A 𝑒 +∞ = −∞
11 6 10 eqtrd A * 0 < A A 𝑒 +∞ = −∞
12 2 11 eqtr3id A * 0 < A A 𝑒 −∞ = −∞