Metamath Proof Explorer


Theorem xlemul1a

Description: Extended real version of lemul1a . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xlemul1a
|- ( ( ( A e. RR* /\ B e. RR* /\ ( C e. RR* /\ 0 <_ C ) ) /\ A <_ B ) -> ( A *e C ) <_ ( B *e C ) )

Proof

Step Hyp Ref Expression
1 0xr
 |-  0 e. RR*
2 simpr
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) -> C e. RR* )
3 xrleloe
 |-  ( ( 0 e. RR* /\ C e. RR* ) -> ( 0 <_ C <-> ( 0 < C \/ 0 = C ) ) )
4 1 2 3 sylancr
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) -> ( 0 <_ C <-> ( 0 < C \/ 0 = C ) ) )
5 simpllr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> C e. RR* )
6 elxr
 |-  ( C e. RR* <-> ( C e. RR \/ C = +oo \/ C = -oo ) )
7 5 6 sylib
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( C e. RR \/ C = +oo \/ C = -oo ) )
8 simplrr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ C e. RR ) ) -> A <_ B )
9 simprll
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ C e. RR ) ) -> A e. RR )
10 simprlr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ C e. RR ) ) -> B e. RR )
11 simprr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ C e. RR ) ) -> C e. RR )
12 simplrl
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ C e. RR ) ) -> 0 < C )
13 lemul1
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( A x. C ) <_ ( B x. C ) ) )
14 9 10 11 12 13 syl112anc
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ C e. RR ) ) -> ( A <_ B <-> ( A x. C ) <_ ( B x. C ) ) )
15 8 14 mpbid
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ C e. RR ) ) -> ( A x. C ) <_ ( B x. C ) )
16 rexmul
 |-  ( ( A e. RR /\ C e. RR ) -> ( A *e C ) = ( A x. C ) )
17 9 11 16 syl2anc
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ C e. RR ) ) -> ( A *e C ) = ( A x. C ) )
18 rexmul
 |-  ( ( B e. RR /\ C e. RR ) -> ( B *e C ) = ( B x. C ) )
19 10 11 18 syl2anc
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ C e. RR ) ) -> ( B *e C ) = ( B x. C ) )
20 15 17 19 3brtr4d
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ C e. RR ) ) -> ( A *e C ) <_ ( B *e C ) )
21 20 expr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( C e. RR -> ( A *e C ) <_ ( B *e C ) ) )
22 simprl
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> A e. RR )
23 0re
 |-  0 e. RR
24 lttri4
 |-  ( ( A e. RR /\ 0 e. RR ) -> ( A < 0 \/ A = 0 \/ 0 < A ) )
25 22 23 24 sylancl
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( A < 0 \/ A = 0 \/ 0 < A ) )
26 simplll
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) -> A e. RR* )
27 26 adantr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> A e. RR* )
28 xmulpnf1n
 |-  ( ( A e. RR* /\ A < 0 ) -> ( A *e +oo ) = -oo )
29 27 28 sylan
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) /\ A < 0 ) -> ( A *e +oo ) = -oo )
30 simpllr
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) -> B e. RR* )
31 30 adantr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> B e. RR* )
32 31 adantr
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) /\ A < 0 ) -> B e. RR* )
33 pnfxr
 |-  +oo e. RR*
34 xmulcl
 |-  ( ( B e. RR* /\ +oo e. RR* ) -> ( B *e +oo ) e. RR* )
35 32 33 34 sylancl
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) /\ A < 0 ) -> ( B *e +oo ) e. RR* )
36 mnfle
 |-  ( ( B *e +oo ) e. RR* -> -oo <_ ( B *e +oo ) )
37 35 36 syl
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) /\ A < 0 ) -> -oo <_ ( B *e +oo ) )
38 29 37 eqbrtrd
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) /\ A < 0 ) -> ( A *e +oo ) <_ ( B *e +oo ) )
39 38 ex
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( A < 0 -> ( A *e +oo ) <_ ( B *e +oo ) ) )
40 oveq1
 |-  ( A = 0 -> ( A *e +oo ) = ( 0 *e +oo ) )
41 xmul02
 |-  ( +oo e. RR* -> ( 0 *e +oo ) = 0 )
42 33 41 ax-mp
 |-  ( 0 *e +oo ) = 0
43 40 42 eqtrdi
 |-  ( A = 0 -> ( A *e +oo ) = 0 )
44 43 adantl
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) /\ A = 0 ) -> ( A *e +oo ) = 0 )
45 simplrr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> A <_ B )
46 breq1
 |-  ( A = 0 -> ( A <_ B <-> 0 <_ B ) )
47 45 46 syl5ibcom
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( A = 0 -> 0 <_ B ) )
48 simprr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> B e. RR )
49 leloe
 |-  ( ( 0 e. RR /\ B e. RR ) -> ( 0 <_ B <-> ( 0 < B \/ 0 = B ) ) )
50 23 48 49 sylancr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( 0 <_ B <-> ( 0 < B \/ 0 = B ) ) )
51 47 50 sylibd
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( A = 0 -> ( 0 < B \/ 0 = B ) ) )
52 51 imp
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) /\ A = 0 ) -> ( 0 < B \/ 0 = B ) )
53 pnfge
 |-  ( 0 e. RR* -> 0 <_ +oo )
54 1 53 ax-mp
 |-  0 <_ +oo
55 xmulpnf1
 |-  ( ( B e. RR* /\ 0 < B ) -> ( B *e +oo ) = +oo )
56 31 55 sylan
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) /\ 0 < B ) -> ( B *e +oo ) = +oo )
57 54 56 breqtrrid
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) /\ 0 < B ) -> 0 <_ ( B *e +oo ) )
58 xrleid
 |-  ( 0 e. RR* -> 0 <_ 0 )
59 1 58 ax-mp
 |-  0 <_ 0
60 59 42 breqtrri
 |-  0 <_ ( 0 *e +oo )
61 simpr
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) /\ 0 = B ) -> 0 = B )
62 61 oveq1d
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) /\ 0 = B ) -> ( 0 *e +oo ) = ( B *e +oo ) )
63 60 62 breqtrid
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) /\ 0 = B ) -> 0 <_ ( B *e +oo ) )
64 57 63 jaodan
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) /\ ( 0 < B \/ 0 = B ) ) -> 0 <_ ( B *e +oo ) )
65 52 64 syldan
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) /\ A = 0 ) -> 0 <_ ( B *e +oo ) )
66 44 65 eqbrtrd
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) /\ A = 0 ) -> ( A *e +oo ) <_ ( B *e +oo ) )
67 66 ex
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( A = 0 -> ( A *e +oo ) <_ ( B *e +oo ) ) )
68 pnfge
 |-  ( +oo e. RR* -> +oo <_ +oo )
69 33 68 ax-mp
 |-  +oo <_ +oo
70 26 adantr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ 0 < A ) ) -> A e. RR* )
71 simprr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ 0 < A ) ) -> 0 < A )
72 xmulpnf1
 |-  ( ( A e. RR* /\ 0 < A ) -> ( A *e +oo ) = +oo )
73 70 71 72 syl2anc
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ 0 < A ) ) -> ( A *e +oo ) = +oo )
74 30 adantr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ 0 < A ) ) -> B e. RR* )
75 ltletr
 |-  ( ( 0 e. RR /\ A e. RR /\ B e. RR ) -> ( ( 0 < A /\ A <_ B ) -> 0 < B ) )
76 23 75 mp3an1
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 < A /\ A <_ B ) -> 0 < B ) )
77 76 adantl
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( ( 0 < A /\ A <_ B ) -> 0 < B ) )
78 45 77 mpan2d
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( 0 < A -> 0 < B ) )
79 78 impr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ 0 < A ) ) -> 0 < B )
80 74 79 55 syl2anc
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ 0 < A ) ) -> ( B *e +oo ) = +oo )
81 73 80 breq12d
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ 0 < A ) ) -> ( ( A *e +oo ) <_ ( B *e +oo ) <-> +oo <_ +oo ) )
82 69 81 mpbiri
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( ( A e. RR /\ B e. RR ) /\ 0 < A ) ) -> ( A *e +oo ) <_ ( B *e +oo ) )
83 82 expr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( 0 < A -> ( A *e +oo ) <_ ( B *e +oo ) ) )
84 39 67 83 3jaod
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( ( A < 0 \/ A = 0 \/ 0 < A ) -> ( A *e +oo ) <_ ( B *e +oo ) ) )
85 25 84 mpd
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( A *e +oo ) <_ ( B *e +oo ) )
86 oveq2
 |-  ( C = +oo -> ( A *e C ) = ( A *e +oo ) )
87 oveq2
 |-  ( C = +oo -> ( B *e C ) = ( B *e +oo ) )
88 86 87 breq12d
 |-  ( C = +oo -> ( ( A *e C ) <_ ( B *e C ) <-> ( A *e +oo ) <_ ( B *e +oo ) ) )
89 85 88 syl5ibrcom
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( C = +oo -> ( A *e C ) <_ ( B *e C ) ) )
90 nltmnf
 |-  ( 0 e. RR* -> -. 0 < -oo )
91 1 90 ax-mp
 |-  -. 0 < -oo
92 breq2
 |-  ( C = -oo -> ( 0 < C <-> 0 < -oo ) )
93 91 92 mtbiri
 |-  ( C = -oo -> -. 0 < C )
94 93 con2i
 |-  ( 0 < C -> -. C = -oo )
95 94 ad2antrl
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) -> -. C = -oo )
96 95 adantr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> -. C = -oo )
97 96 pm2.21d
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( C = -oo -> ( A *e C ) <_ ( B *e C ) ) )
98 21 89 97 3jaod
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( ( C e. RR \/ C = +oo \/ C = -oo ) -> ( A *e C ) <_ ( B *e C ) ) )
99 7 98 mpd
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ ( A e. RR /\ B e. RR ) ) -> ( A *e C ) <_ ( B *e C ) )
100 99 anassrs
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A e. RR ) /\ B e. RR ) -> ( A *e C ) <_ ( B *e C ) )
101 xmulcl
 |-  ( ( A e. RR* /\ C e. RR* ) -> ( A *e C ) e. RR* )
102 101 adantlr
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) -> ( A *e C ) e. RR* )
103 102 ad2antrr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ B = +oo ) -> ( A *e C ) e. RR* )
104 pnfge
 |-  ( ( A *e C ) e. RR* -> ( A *e C ) <_ +oo )
105 103 104 syl
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ B = +oo ) -> ( A *e C ) <_ +oo )
106 oveq1
 |-  ( B = +oo -> ( B *e C ) = ( +oo *e C ) )
107 xmulpnf2
 |-  ( ( C e. RR* /\ 0 < C ) -> ( +oo *e C ) = +oo )
108 107 ad2ant2lr
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) -> ( +oo *e C ) = +oo )
109 106 108 sylan9eqr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ B = +oo ) -> ( B *e C ) = +oo )
110 105 109 breqtrrd
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ B = +oo ) -> ( A *e C ) <_ ( B *e C ) )
111 110 adantlr
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A e. RR ) /\ B = +oo ) -> ( A *e C ) <_ ( B *e C ) )
112 simplrr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ B = -oo ) -> A <_ B )
113 simpr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ B = -oo ) -> B = -oo )
114 26 adantr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ B = -oo ) -> A e. RR* )
115 mnfle
 |-  ( A e. RR* -> -oo <_ A )
116 114 115 syl
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ B = -oo ) -> -oo <_ A )
117 113 116 eqbrtrd
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ B = -oo ) -> B <_ A )
118 xrletri3
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
119 118 ad3antrrr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ B = -oo ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
120 112 117 119 mpbir2and
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ B = -oo ) -> A = B )
121 120 oveq1d
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ B = -oo ) -> ( A *e C ) = ( B *e C ) )
122 xmulcl
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( B *e C ) e. RR* )
123 122 adantll
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) -> ( B *e C ) e. RR* )
124 123 ad2antrr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ B = -oo ) -> ( B *e C ) e. RR* )
125 xrleid
 |-  ( ( B *e C ) e. RR* -> ( B *e C ) <_ ( B *e C ) )
126 124 125 syl
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ B = -oo ) -> ( B *e C ) <_ ( B *e C ) )
127 121 126 eqbrtrd
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ B = -oo ) -> ( A *e C ) <_ ( B *e C ) )
128 127 adantlr
 |-  ( ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A e. RR ) /\ B = -oo ) -> ( A *e C ) <_ ( B *e C ) )
129 elxr
 |-  ( B e. RR* <-> ( B e. RR \/ B = +oo \/ B = -oo ) )
130 30 129 sylib
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) -> ( B e. RR \/ B = +oo \/ B = -oo ) )
131 130 adantr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A e. RR ) -> ( B e. RR \/ B = +oo \/ B = -oo ) )
132 100 111 128 131 mpjao3dan
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A e. RR ) -> ( A *e C ) <_ ( B *e C ) )
133 simplrr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A = +oo ) -> A <_ B )
134 30 adantr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A = +oo ) -> B e. RR* )
135 pnfge
 |-  ( B e. RR* -> B <_ +oo )
136 134 135 syl
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A = +oo ) -> B <_ +oo )
137 simpr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A = +oo ) -> A = +oo )
138 136 137 breqtrrd
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A = +oo ) -> B <_ A )
139 118 ad3antrrr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A = +oo ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
140 133 138 139 mpbir2and
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A = +oo ) -> A = B )
141 140 oveq1d
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A = +oo ) -> ( A *e C ) = ( B *e C ) )
142 123 125 syl
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) -> ( B *e C ) <_ ( B *e C ) )
143 142 ad2antrr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A = +oo ) -> ( B *e C ) <_ ( B *e C ) )
144 141 143 eqbrtrd
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A = +oo ) -> ( A *e C ) <_ ( B *e C ) )
145 oveq1
 |-  ( A = -oo -> ( A *e C ) = ( -oo *e C ) )
146 xmulmnf2
 |-  ( ( C e. RR* /\ 0 < C ) -> ( -oo *e C ) = -oo )
147 146 ad2ant2lr
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) -> ( -oo *e C ) = -oo )
148 145 147 sylan9eqr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A = -oo ) -> ( A *e C ) = -oo )
149 123 ad2antrr
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A = -oo ) -> ( B *e C ) e. RR* )
150 mnfle
 |-  ( ( B *e C ) e. RR* -> -oo <_ ( B *e C ) )
151 149 150 syl
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A = -oo ) -> -oo <_ ( B *e C ) )
152 148 151 eqbrtrd
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) /\ A = -oo ) -> ( A *e C ) <_ ( B *e C ) )
153 elxr
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
154 26 153 sylib
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) -> ( A e. RR \/ A = +oo \/ A = -oo ) )
155 132 144 152 154 mpjao3dan
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) /\ ( 0 < C /\ A <_ B ) ) -> ( A *e C ) <_ ( B *e C ) )
156 155 exp32
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) -> ( 0 < C -> ( A <_ B -> ( A *e C ) <_ ( B *e C ) ) ) )
157 xmul01
 |-  ( A e. RR* -> ( A *e 0 ) = 0 )
158 157 ad2antrr
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) -> ( A *e 0 ) = 0 )
159 xmul01
 |-  ( B e. RR* -> ( B *e 0 ) = 0 )
160 159 ad2antlr
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) -> ( B *e 0 ) = 0 )
161 158 160 breq12d
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) -> ( ( A *e 0 ) <_ ( B *e 0 ) <-> 0 <_ 0 ) )
162 59 161 mpbiri
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) -> ( A *e 0 ) <_ ( B *e 0 ) )
163 oveq2
 |-  ( 0 = C -> ( A *e 0 ) = ( A *e C ) )
164 oveq2
 |-  ( 0 = C -> ( B *e 0 ) = ( B *e C ) )
165 163 164 breq12d
 |-  ( 0 = C -> ( ( A *e 0 ) <_ ( B *e 0 ) <-> ( A *e C ) <_ ( B *e C ) ) )
166 162 165 syl5ibcom
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) -> ( 0 = C -> ( A *e C ) <_ ( B *e C ) ) )
167 166 a1dd
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) -> ( 0 = C -> ( A <_ B -> ( A *e C ) <_ ( B *e C ) ) ) )
168 156 167 jaod
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) -> ( ( 0 < C \/ 0 = C ) -> ( A <_ B -> ( A *e C ) <_ ( B *e C ) ) ) )
169 4 168 sylbid
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. RR* ) -> ( 0 <_ C -> ( A <_ B -> ( A *e C ) <_ ( B *e C ) ) ) )
170 169 expimpd
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( C e. RR* /\ 0 <_ C ) -> ( A <_ B -> ( A *e C ) <_ ( B *e C ) ) ) )
171 170 3impia
 |-  ( ( A e. RR* /\ B e. RR* /\ ( C e. RR* /\ 0 <_ C ) ) -> ( A <_ B -> ( A *e C ) <_ ( B *e C ) ) )
172 171 imp
 |-  ( ( ( A e. RR* /\ B e. RR* /\ ( C e. RR* /\ 0 <_ C ) ) /\ A <_ B ) -> ( A *e C ) <_ ( B *e C ) )