Step |
Hyp |
Ref |
Expression |
1 |
|
simplll |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ ( 0 <_ C /\ C < D ) ) ) -> A e. RR ) |
2 |
|
simpllr |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ ( 0 <_ C /\ C < D ) ) ) -> B e. RR ) |
3 |
|
simpll |
|- ( ( ( C e. RR /\ D e. RR ) /\ ( 0 <_ C /\ C < D ) ) -> C e. RR ) |
4 |
|
simprl |
|- ( ( ( C e. RR /\ D e. RR ) /\ ( 0 <_ C /\ C < D ) ) -> 0 <_ C ) |
5 |
3 4
|
jca |
|- ( ( ( C e. RR /\ D e. RR ) /\ ( 0 <_ C /\ C < D ) ) -> ( C e. RR /\ 0 <_ C ) ) |
6 |
5
|
ad2ant2l |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ ( 0 <_ C /\ C < D ) ) ) -> ( C e. RR /\ 0 <_ C ) ) |
7 |
|
ltle |
|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) ) |
8 |
7
|
imp |
|- ( ( ( A e. RR /\ B e. RR ) /\ A < B ) -> A <_ B ) |
9 |
8
|
adantrl |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) -> A <_ B ) |
10 |
9
|
ad2ant2r |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ ( 0 <_ C /\ C < D ) ) ) -> A <_ B ) |
11 |
|
lemul1a |
|- ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( A x. C ) <_ ( B x. C ) ) |
12 |
1 2 6 10 11
|
syl31anc |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ ( 0 <_ C /\ C < D ) ) ) -> ( A x. C ) <_ ( B x. C ) ) |
13 |
|
simplrl |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( 0 <_ A /\ A < B ) ) -> C e. RR ) |
14 |
|
simplrr |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( 0 <_ A /\ A < B ) ) -> D e. RR ) |
15 |
|
simpllr |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( 0 <_ A /\ A < B ) ) -> B e. RR ) |
16 |
|
0re |
|- 0 e. RR |
17 |
|
lelttr |
|- ( ( 0 e. RR /\ A e. RR /\ B e. RR ) -> ( ( 0 <_ A /\ A < B ) -> 0 < B ) ) |
18 |
16 17
|
mp3an1 |
|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <_ A /\ A < B ) -> 0 < B ) ) |
19 |
18
|
imp |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) -> 0 < B ) |
20 |
19
|
adantlr |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( 0 <_ A /\ A < B ) ) -> 0 < B ) |
21 |
|
ltmul2 |
|- ( ( C e. RR /\ D e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( C < D <-> ( B x. C ) < ( B x. D ) ) ) |
22 |
13 14 15 20 21
|
syl112anc |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( 0 <_ A /\ A < B ) ) -> ( C < D <-> ( B x. C ) < ( B x. D ) ) ) |
23 |
22
|
biimpa |
|- ( ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( 0 <_ A /\ A < B ) ) /\ C < D ) -> ( B x. C ) < ( B x. D ) ) |
24 |
23
|
anasss |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ C < D ) ) -> ( B x. C ) < ( B x. D ) ) |
25 |
24
|
adantrrl |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ ( 0 <_ C /\ C < D ) ) ) -> ( B x. C ) < ( B x. D ) ) |
26 |
|
remulcl |
|- ( ( A e. RR /\ C e. RR ) -> ( A x. C ) e. RR ) |
27 |
26
|
ad2ant2r |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( A x. C ) e. RR ) |
28 |
|
remulcl |
|- ( ( B e. RR /\ C e. RR ) -> ( B x. C ) e. RR ) |
29 |
28
|
ad2ant2lr |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( B x. C ) e. RR ) |
30 |
|
remulcl |
|- ( ( B e. RR /\ D e. RR ) -> ( B x. D ) e. RR ) |
31 |
30
|
ad2ant2l |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( B x. D ) e. RR ) |
32 |
|
lelttr |
|- ( ( ( A x. C ) e. RR /\ ( B x. C ) e. RR /\ ( B x. D ) e. RR ) -> ( ( ( A x. C ) <_ ( B x. C ) /\ ( B x. C ) < ( B x. D ) ) -> ( A x. C ) < ( B x. D ) ) ) |
33 |
27 29 31 32
|
syl3anc |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( ( A x. C ) <_ ( B x. C ) /\ ( B x. C ) < ( B x. D ) ) -> ( A x. C ) < ( B x. D ) ) ) |
34 |
33
|
adantr |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ ( 0 <_ C /\ C < D ) ) ) -> ( ( ( A x. C ) <_ ( B x. C ) /\ ( B x. C ) < ( B x. D ) ) -> ( A x. C ) < ( B x. D ) ) ) |
35 |
12 25 34
|
mp2and |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) /\ ( ( 0 <_ A /\ A < B ) /\ ( 0 <_ C /\ C < D ) ) ) -> ( A x. C ) < ( B x. D ) ) |
36 |
35
|
an4s |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 <_ C /\ C < D ) ) ) -> ( A x. C ) < ( B x. D ) ) |