This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lediv23

Description: Swap denominator with other side of 'less than or equal to'. (Contributed by NM, 30-May-2005)

Ref Expression
Assertion lediv23 
|- ( ( 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 lemul1 
 |-  ( ( ( 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 lediv1 
 |-  ( ( 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 ) )