Metamath Proof Explorer


Theorem ltdiv23i

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

Proof

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