This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )