Step |
Hyp |
Ref |
Expression |
1 |
|
ltmul1d.1 |
|- ( ph -> A e. RR ) |
2 |
|
ltmul1d.2 |
|- ( ph -> B e. RR ) |
3 |
|
ltmul1d.3 |
|- ( ph -> C e. RR+ ) |
4 |
|
lediv12ad.4 |
|- ( ph -> D e. RR ) |
5 |
|
lediv12ad.5 |
|- ( ph -> 0 <_ A ) |
6 |
|
lediv12ad.6 |
|- ( ph -> A <_ B ) |
7 |
|
lediv12ad.7 |
|- ( ph -> C <_ D ) |
8 |
1 2
|
jca |
|- ( ph -> ( A e. RR /\ B e. RR ) ) |
9 |
5 6
|
jca |
|- ( ph -> ( 0 <_ A /\ A <_ B ) ) |
10 |
3
|
rpred |
|- ( ph -> C e. RR ) |
11 |
10 4
|
jca |
|- ( ph -> ( C e. RR /\ D e. RR ) ) |
12 |
3
|
rpgt0d |
|- ( ph -> 0 < C ) |
13 |
12 7
|
jca |
|- ( ph -> ( 0 < C /\ C <_ D ) ) |
14 |
|
lediv12a |
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) ) -> ( A / D ) <_ ( B / C ) ) |
15 |
8 9 11 13 14
|
syl22anc |
|- ( ph -> ( A / D ) <_ ( B / C ) ) |