Metamath Proof Explorer

Theorem mulsuble0b

Description: A condition for multiplication of subtraction to be nonpositive. (Contributed by Scott Fenton, 25-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 resubcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )
2 1 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A - B ) e. RR )
3 resubcl 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C - B ) e. RR )
4 3 ancoms 
 |-  ( ( B e. RR /\ C e. RR ) -> ( C - B ) e. RR )
5 4 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C - B ) e. RR )
6 mulle0b 
 |-  ( ( ( A - B ) e. RR /\ ( C - B ) e. RR ) -> ( ( ( A - B ) x. ( C - B ) ) <_ 0 <-> ( ( ( A - B ) <_ 0 /\ 0 <_ ( C - B ) ) \/ ( 0 <_ ( A - B ) /\ ( C - B ) <_ 0 ) ) ) )
7 2 5 6 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( ( A - B ) x. ( C - B ) ) <_ 0 <-> ( ( ( A - B ) <_ 0 /\ 0 <_ ( C - B ) ) \/ ( 0 <_ ( A - B ) /\ ( C - B ) <_ 0 ) ) ) )
8 suble0 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A - B ) <_ 0 <-> A <_ B ) )
9 8 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - B ) <_ 0 <-> A <_ B ) )
10 subge0 
 |-  ( ( C e. RR /\ B e. RR ) -> ( 0 <_ ( C - B ) <-> B <_ C ) )
11 10 ancoms 
 |-  ( ( B e. RR /\ C e. RR ) -> ( 0 <_ ( C - B ) <-> B <_ C ) )
12 11 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( 0 <_ ( C - B ) <-> B <_ C ) )
13 9 12 anbi12d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( ( A - B ) <_ 0 /\ 0 <_ ( C - B ) ) <-> ( A <_ B /\ B <_ C ) ) )
14 subge0 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ ( A - B ) <-> B <_ A ) )
15 14 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( 0 <_ ( A - B ) <-> B <_ A ) )
16 suble0 
 |-  ( ( C e. RR /\ B e. RR ) -> ( ( C - B ) <_ 0 <-> C <_ B ) )
17 16 ancoms 
 |-  ( ( B e. RR /\ C e. RR ) -> ( ( C - B ) <_ 0 <-> C <_ B ) )
18 17 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C - B ) <_ 0 <-> C <_ B ) )
19 15 18 anbi12d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( 0 <_ ( A - B ) /\ ( C - B ) <_ 0 ) <-> ( B <_ A /\ C <_ B ) ) )
20 19 biancomd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( 0 <_ ( A - B ) /\ ( C - B ) <_ 0 ) <-> ( C <_ B /\ B <_ A ) ) )
21 13 20 orbi12d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( ( ( A - B ) <_ 0 /\ 0 <_ ( C - B ) ) \/ ( 0 <_ ( A - B ) /\ ( C - B ) <_ 0 ) ) <-> ( ( A <_ B /\ B <_ C ) \/ ( C <_ B /\ B <_ A ) ) ) )
22 7 21 bitrd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( ( A - B ) x. ( C - B ) ) <_ 0 <-> ( ( A <_ B /\ B <_ C ) \/ ( C <_ B /\ B <_ A ) ) ) )