Metamath Proof Explorer


Theorem ltdiv23

Description: Swap denominator with other side of 'less than'. (Contributed by NM, 3-Oct-1999)

Ref Expression
Assertion ltdiv23
|- ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / B ) < C <-> ( A / C ) < B ) )

Proof

Step Hyp Ref Expression
1 simpl
 |-  ( ( B e. RR /\ 0 < B ) -> B e. RR )
2 gt0ne0
 |-  ( ( B e. RR /\ 0 < B ) -> B =/= 0 )
3 1 2 jca
 |-  ( ( B e. RR /\ 0 < B ) -> ( B e. RR /\ B =/= 0 ) )
4 redivcl
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( A / B ) e. RR )
5 4 3expb
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) ) -> ( A / B ) e. RR )
6 3 5 sylan2
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( A / B ) e. RR )
7 6 3adant3
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ C e. RR ) -> ( A / B ) e. RR )
8 simp3
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ C e. RR ) -> C e. RR )
9 simp2
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ C e. RR ) -> ( B e. RR /\ 0 < B ) )
10 ltmul1
 |-  ( ( ( A / B ) e. RR /\ C e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( ( A / B ) < C <-> ( ( A / B ) x. B ) < ( C x. B ) ) )
11 7 8 9 10 syl3anc
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ C e. RR ) -> ( ( A / B ) < C <-> ( ( A / B ) x. B ) < ( C x. B ) ) )
12 11 3adant3r
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / B ) < C <-> ( ( A / B ) x. B ) < ( C x. B ) ) )
13 recn
 |-  ( A e. RR -> A e. CC )
14 13 adantr
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) -> A e. CC )
15 recn
 |-  ( B e. RR -> B e. CC )
16 15 ad2antrl
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) -> B e. CC )
17 2 adantl
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) -> B =/= 0 )
18 14 16 17 divcan1d
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( ( A / B ) x. B ) = A )
19 18 3adant3
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / B ) x. B ) = A )
20 19 breq1d
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( ( A / B ) x. B ) < ( C x. B ) <-> A < ( C x. B ) ) )
21 remulcl
 |-  ( ( C e. RR /\ B e. RR ) -> ( C x. B ) e. RR )
22 21 ancoms
 |-  ( ( B e. RR /\ C e. RR ) -> ( C x. B ) e. RR )
23 22 adantrr
 |-  ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( C x. B ) e. RR )
24 23 3adant1
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( C x. B ) e. RR )
25 ltdiv1
 |-  ( ( A e. RR /\ ( C x. B ) e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < ( C x. B ) <-> ( A / C ) < ( ( C x. B ) / C ) ) )
26 24 25 syld3an2
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < ( C x. B ) <-> ( A / C ) < ( ( C x. B ) / C ) ) )
27 recn
 |-  ( C e. RR -> C e. CC )
28 27 adantr
 |-  ( ( C e. RR /\ 0 < C ) -> C e. CC )
29 gt0ne0
 |-  ( ( C e. RR /\ 0 < C ) -> C =/= 0 )
30 28 29 jca
 |-  ( ( C e. RR /\ 0 < C ) -> ( C e. CC /\ C =/= 0 ) )
31 divcan3
 |-  ( ( B e. CC /\ C e. CC /\ C =/= 0 ) -> ( ( C x. B ) / C ) = B )
32 31 3expb
 |-  ( ( B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. B ) / C ) = B )
33 15 30 32 syl2an
 |-  ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( C x. B ) / C ) = B )
34 33 3adant1
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( C x. B ) / C ) = B )
35 34 breq2d
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) < ( ( C x. B ) / C ) <-> ( A / C ) < B ) )
36 26 35 bitrd
 |-  ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < ( C x. B ) <-> ( A / C ) < B ) )
37 36 3adant2r
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( A < ( C x. B ) <-> ( A / C ) < B ) )
38 12 20 37 3bitrd
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / B ) < C <-> ( A / C ) < B ) )