Theorem ltdiv23ii

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
	ltdiv23i.4	|- 0 < B
	ltdiv23i.5	|- 0 < C
Assertion	ltdiv23ii	|- ( ( 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		ltdiv23i.4	|- 0 < B
5		ltdiv23i.5	|- 0 < C
6	1 2 3	ltdiv23i	|- ( ( 0 < B /\ 0 < C ) -> ( ( A / B ) < C <-> ( A / C ) < B ) )
7	4 5 6	mp2an	|- ( ( A / B ) < C <-> ( A / C ) < B )