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