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 e. RR* /\ 0 < A ) -> ( A *e -oo ) = -oo )

Proof

Step Hyp Ref Expression
1 xnegpnf 
 |-  -e +oo = -oo
2 1 oveq2i 
 |-  ( A *e -e +oo ) = ( A *e -oo )
3 simpl 
 |-  ( ( A e. RR* /\ 0 < A ) -> A e. RR* )
4 pnfxr 
 |-  +oo e. RR*
5 xmulneg2 
 |-  ( ( A e. RR* /\ +oo e. RR* ) -> ( A *e -e +oo ) = -e ( A *e +oo ) )
6 3 4 5 sylancl 
 |-  ( ( A e. RR* /\ 0 < A ) -> ( A *e -e +oo ) = -e ( A *e +oo ) )
7 xmulpnf1 
 |-  ( ( A e. RR* /\ 0 < A ) -> ( A *e +oo ) = +oo )
8 xnegeq 
 |-  ( ( A *e +oo ) = +oo -> -e ( A *e +oo ) = -e +oo )
9 7 8 syl 
 |-  ( ( A e. RR* /\ 0 < A ) -> -e ( A *e +oo ) = -e +oo )
10 9 1 eqtrdi 
 |-  ( ( A e. RR* /\ 0 < A ) -> -e ( A *e +oo ) = -oo )
11 6 10 eqtrd 
 |-  ( ( A e. RR* /\ 0 < A ) -> ( A *e -e +oo ) = -oo )
12 2 11 eqtr3id 
 |-  ( ( A e. RR* /\ 0 < A ) -> ( A *e -oo ) = -oo )