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

Metamath Proof Explorer

Theorem ltdiv23neg

Description: Swap denominator with other side of 'less than', when both are negative. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses ltdiv23neg.1 
|- ( ph -> A e. RR )
ltdiv23neg.2 
|- ( ph -> B e. RR )
ltdiv23neg.3 
|- ( ph -> B < 0 )
ltdiv23neg.4 
|- ( ph -> C e. RR )
ltdiv23neg.5 
|- ( ph -> C < 0 )
Assertion ltdiv23neg 
|- ( ph -> ( ( A / B ) < C <-> ( A / C ) < B ) )

Proof

Step Hyp Ref Expression
1 ltdiv23neg.1 
 |-  ( ph -> A e. RR )
2 ltdiv23neg.2 
 |-  ( ph -> B e. RR )
3 ltdiv23neg.3 
 |-  ( ph -> B < 0 )
4 ltdiv23neg.4 
 |-  ( ph -> C e. RR )
5 ltdiv23neg.5 
 |-  ( ph -> C < 0 )
6 2 3 ltned 
 |-  ( ph -> B =/= 0 )
7 1 2 6 redivcld 
 |-  ( ph -> ( A / B ) e. RR )
8 7 4 2 3 ltmulneg 
 |-  ( ph -> ( ( A / B ) < C <-> ( C x. B ) < ( ( A / B ) x. B ) ) )
9 recn 
 |-  ( A e. RR -> A e. CC )
10 1 9 syl 
 |-  ( ph -> A e. CC )
11 recn 
 |-  ( B e. RR -> B e. CC )
12 2 11 syl 
 |-  ( ph -> B e. CC )
13 10 12 6 divcan1d 
 |-  ( ph -> ( ( A / B ) x. B ) = A )
14 13 breq2d 
 |-  ( ph -> ( ( C x. B ) < ( ( A / B ) x. B ) <-> ( C x. B ) < A ) )
15 remulcl 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C x. B ) e. RR )
16 4 2 15 syl2anc 
 |-  ( ph -> ( C x. B ) e. RR )
17 4 5 ltned 
 |-  ( ph -> C =/= 0 )
18 4 17 rereccld 
 |-  ( ph -> ( 1 / C ) e. RR )
19 4 5 reclt0d 
 |-  ( ph -> ( 1 / C ) < 0 )
20 16 1 18 19 ltmulneg 
 |-  ( ph -> ( ( C x. B ) < A <-> ( A x. ( 1 / C ) ) < ( ( C x. B ) x. ( 1 / C ) ) ) )
21 recn 
 |-  ( C e. RR -> C e. CC )
22 4 21 syl 
 |-  ( ph -> C e. CC )
23 10 22 17 divrecd 
 |-  ( ph -> ( A / C ) = ( A x. ( 1 / C ) ) )
24 23 eqcomd 
 |-  ( ph -> ( A x. ( 1 / C ) ) = ( A / C ) )
25 22 12 mulcld 
 |-  ( ph -> ( C x. B ) e. CC )
26 25 22 17 divrecd 
 |-  ( ph -> ( ( C x. B ) / C ) = ( ( C x. B ) x. ( 1 / C ) ) )
27 divcan3 
 |-  ( ( B e. CC /\ C e. CC /\ C =/= 0 ) -> ( ( C x. B ) / C ) = B )
28 27 3expb 
 |-  ( ( B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. B ) / C ) = B )
29 12 22 17 28 syl12anc 
 |-  ( ph -> ( ( C x. B ) / C ) = B )
30 26 29 eqtr3d 
 |-  ( ph -> ( ( C x. B ) x. ( 1 / C ) ) = B )
31 24 30 breq12d 
 |-  ( ph -> ( ( A x. ( 1 / C ) ) < ( ( C x. B ) x. ( 1 / C ) ) <-> ( A / C ) < B ) )
32 20 31 bitrd 
 |-  ( ph -> ( ( C x. B ) < A <-> ( A / C ) < B ) )
33 8 14 32 3bitrd 
 |-  ( ph -> ( ( A / B ) < C <-> ( A / C ) < B ) )