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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. RR* /\ A < 0 ) -> A e. RR* )
2 pnfxr 
 |-  +oo e. RR*
3 xmulneg1 
 |-  ( ( A e. RR* /\ +oo e. RR* ) -> ( -e A *e +oo ) = -e ( A *e +oo ) )
4 1 2 3 sylancl 
 |-  ( ( A e. RR* /\ A < 0 ) -> ( -e A *e +oo ) = -e ( A *e +oo ) )
5 xnegcl 
 |-  ( A e. RR* -> -e A e. RR* )
6 xlt0neg1 
 |-  ( A e. RR* -> ( A < 0 <-> 0 < -e A ) )
7 6 biimpa 
 |-  ( ( A e. RR* /\ A < 0 ) -> 0 < -e A )
8 xmulpnf1 
 |-  ( ( -e A e. RR* /\ 0 < -e A ) -> ( -e A *e +oo ) = +oo )
9 5 7 8 syl2an2r 
 |-  ( ( A e. RR* /\ A < 0 ) -> ( -e A *e +oo ) = +oo )
10 4 9 eqtr3d 
 |-  ( ( A e. RR* /\ A < 0 ) -> -e ( A *e +oo ) = +oo )
11 xnegmnf 
 |-  -e -oo = +oo
12 10 11 eqtr4di 
 |-  ( ( A e. RR* /\ A < 0 ) -> -e ( A *e +oo ) = -e -oo )
13 xmulcl 
 |-  ( ( A e. RR* /\ +oo e. RR* ) -> ( A *e +oo ) e. RR* )
14 1 2 13 sylancl 
 |-  ( ( A e. RR* /\ A < 0 ) -> ( A *e +oo ) e. RR* )
15 mnfxr 
 |-  -oo e. RR*
16 xneg11 
 |-  ( ( ( A *e +oo ) e. RR* /\ -oo e. RR* ) -> ( -e ( A *e +oo ) = -e -oo <-> ( A *e +oo ) = -oo ) )
17 14 15 16 sylancl 
 |-  ( ( A e. RR* /\ A < 0 ) -> ( -e ( A *e +oo ) = -e -oo <-> ( A *e +oo ) = -oo ) )
18 12 17 mpbid 
 |-  ( ( A e. RR* /\ A < 0 ) -> ( A *e +oo ) = -oo )