Metamath Proof Explorer

Theorem mulle0b

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

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

Proof

Step Hyp Ref Expression
1 remulcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
2 1 le0neg1d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A x. B ) <_ 0 <-> 0 <_ -u ( A x. B ) ) )
3 le0neg2 
 |-  ( B e. RR -> ( 0 <_ B <-> -u B <_ 0 ) )
4 3 anbi2d 
 |-  ( B e. RR -> ( ( A <_ 0 /\ 0 <_ B ) <-> ( A <_ 0 /\ -u B <_ 0 ) ) )
5 le0neg1 
 |-  ( B e. RR -> ( B <_ 0 <-> 0 <_ -u B ) )
6 5 anbi2d 
 |-  ( B e. RR -> ( ( 0 <_ A /\ B <_ 0 ) <-> ( 0 <_ A /\ 0 <_ -u B ) ) )
7 4 6 orbi12d 
 |-  ( B e. RR -> ( ( ( A <_ 0 /\ 0 <_ B ) \/ ( 0 <_ A /\ B <_ 0 ) ) <-> ( ( A <_ 0 /\ -u B <_ 0 ) \/ ( 0 <_ A /\ 0 <_ -u B ) ) ) )
8 7 adantl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A <_ 0 /\ 0 <_ B ) \/ ( 0 <_ A /\ B <_ 0 ) ) <-> ( ( A <_ 0 /\ -u B <_ 0 ) \/ ( 0 <_ A /\ 0 <_ -u B ) ) ) )
9 renegcl 
 |-  ( B e. RR -> -u B e. RR )
10 mulge0b 
 |-  ( ( A e. RR /\ -u B e. RR ) -> ( 0 <_ ( A x. -u B ) <-> ( ( A <_ 0 /\ -u B <_ 0 ) \/ ( 0 <_ A /\ 0 <_ -u B ) ) ) )
11 9 10 sylan2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ ( A x. -u B ) <-> ( ( A <_ 0 /\ -u B <_ 0 ) \/ ( 0 <_ A /\ 0 <_ -u B ) ) ) )
12 recn 
 |-  ( A e. RR -> A e. CC )
13 recn 
 |-  ( B e. RR -> B e. CC )
14 mulneg2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. -u B ) = -u ( A x. B ) )
15 14 breq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 0 <_ ( A x. -u B ) <-> 0 <_ -u ( A x. B ) ) )
16 12 13 15 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ ( A x. -u B ) <-> 0 <_ -u ( A x. B ) ) )
17 8 11 16 3bitr2rd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ -u ( A x. B ) <-> ( ( A <_ 0 /\ 0 <_ B ) \/ ( 0 <_ A /\ B <_ 0 ) ) ) )
18 2 17 bitrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A x. B ) <_ 0 <-> ( ( A <_ 0 /\ 0 <_ B ) \/ ( 0 <_ A /\ B <_ 0 ) ) ) )