Description: Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ltplus1.1 | |- A e. RR |
|
prodgt0.2 | |- B e. RR |
||
ltmul1.3 | |- C e. RR |
||
Assertion | ltdiv23i | |- ( ( 0 < B /\ 0 < C ) -> ( ( A / B ) < C <-> ( A / C ) < B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltplus1.1 | |- A e. RR |
|
2 | prodgt0.2 | |- B e. RR |
|
3 | ltmul1.3 | |- C e. RR |
|
4 | ltdiv23 | |- ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / B ) < C <-> ( A / C ) < B ) ) |
|
5 | 1 4 | mp3an1 | |- ( ( ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / B ) < C <-> ( A / C ) < B ) ) |
6 | 2 5 | mpanl1 | |- ( ( 0 < B /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / B ) < C <-> ( A / C ) < B ) ) |
7 | 3 6 | mpanr1 | |- ( ( 0 < B /\ 0 < C ) -> ( ( A / B ) < C <-> ( A / C ) < B ) ) |