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

Metamath Proof Explorer

Theorem mulge0b

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

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

Proof

Step Hyp Ref Expression
1 ianor 
 |-  ( -. ( A <_ 0 /\ B <_ 0 ) <-> ( -. A <_ 0 \/ -. B <_ 0 ) )
2 0re 
 |-  0 e. RR
3 ltnle 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A <-> -. A <_ 0 ) )
4 2 3 mpan 
 |-  ( A e. RR -> ( 0 < A <-> -. A <_ 0 ) )
5 4 adantr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 < A <-> -. A <_ 0 ) )
6 ltnle 
 |-  ( ( 0 e. RR /\ B e. RR ) -> ( 0 < B <-> -. B <_ 0 ) )
7 2 6 mpan 
 |-  ( B e. RR -> ( 0 < B <-> -. B <_ 0 ) )
8 7 adantl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 < B <-> -. B <_ 0 ) )
9 5 8 orbi12d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 < A \/ 0 < B ) <-> ( -. A <_ 0 \/ -. B <_ 0 ) ) )
10 9 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ 0 <_ ( A x. B ) ) -> ( ( 0 < A \/ 0 < B ) <-> ( -. A <_ 0 \/ -. B <_ 0 ) ) )
11 ltle 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A -> 0 <_ A ) )
12 2 11 mpan 
 |-  ( A e. RR -> ( 0 < A -> 0 <_ A ) )
13 12 imp 
 |-  ( ( A e. RR /\ 0 < A ) -> 0 <_ A )
14 13 ad2ant2rl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < A ) ) -> 0 <_ A )
15 remulcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
16 15 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < A ) ) -> ( A x. B ) e. RR )
17 simprl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < A ) ) -> 0 <_ ( A x. B ) )
18 simpll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < A ) ) -> A e. RR )
19 simprr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < A ) ) -> 0 < A )
20 divge0 
 |-  ( ( ( ( A x. B ) e. RR /\ 0 <_ ( A x. B ) ) /\ ( A e. RR /\ 0 < A ) ) -> 0 <_ ( ( A x. B ) / A ) )
21 16 17 18 19 20 syl22anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < A ) ) -> 0 <_ ( ( A x. B ) / A ) )
22 recn 
 |-  ( B e. RR -> B e. CC )
23 22 ad2antlr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < A ) ) -> B e. CC )
24 recn 
 |-  ( A e. RR -> A e. CC )
25 24 ad2antrr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < A ) ) -> A e. CC )
26 gt0ne0 
 |-  ( ( A e. RR /\ 0 < A ) -> A =/= 0 )
27 26 ad2ant2rl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < A ) ) -> A =/= 0 )
28 23 25 27 divcan3d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < A ) ) -> ( ( A x. B ) / A ) = B )
29 21 28 breqtrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < A ) ) -> 0 <_ B )
30 14 29 jca 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < A ) ) -> ( 0 <_ A /\ 0 <_ B ) )
31 30 expr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ 0 <_ ( A x. B ) ) -> ( 0 < A -> ( 0 <_ A /\ 0 <_ B ) ) )
32 15 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < B ) ) -> ( A x. B ) e. RR )
33 simprl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < B ) ) -> 0 <_ ( A x. B ) )
34 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < B ) ) -> B e. RR )
35 simprr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < B ) ) -> 0 < B )
36 divge0 
 |-  ( ( ( ( A x. B ) e. RR /\ 0 <_ ( A x. B ) ) /\ ( B e. RR /\ 0 < B ) ) -> 0 <_ ( ( A x. B ) / B ) )
37 32 33 34 35 36 syl22anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < B ) ) -> 0 <_ ( ( A x. B ) / B ) )
38 24 ad2antrr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < B ) ) -> A e. CC )
39 22 ad2antlr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < B ) ) -> B e. CC )
40 gt0ne0 
 |-  ( ( B e. RR /\ 0 < B ) -> B =/= 0 )
41 40 ad2ant2l 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < B ) ) -> B =/= 0 )
42 38 39 41 divcan4d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < B ) ) -> ( ( A x. B ) / B ) = A )
43 37 42 breqtrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < B ) ) -> 0 <_ A )
44 ltle 
 |-  ( ( 0 e. RR /\ B e. RR ) -> ( 0 < B -> 0 <_ B ) )
45 2 44 mpan 
 |-  ( B e. RR -> ( 0 < B -> 0 <_ B ) )
46 45 imp 
 |-  ( ( B e. RR /\ 0 < B ) -> 0 <_ B )
47 46 ad2ant2l 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < B ) ) -> 0 <_ B )
48 43 47 jca 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ ( A x. B ) /\ 0 < B ) ) -> ( 0 <_ A /\ 0 <_ B ) )
49 48 expr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ 0 <_ ( A x. B ) ) -> ( 0 < B -> ( 0 <_ A /\ 0 <_ B ) ) )
50 31 49 jaod 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ 0 <_ ( A x. B ) ) -> ( ( 0 < A \/ 0 < B ) -> ( 0 <_ A /\ 0 <_ B ) ) )
51 10 50 sylbird 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ 0 <_ ( A x. B ) ) -> ( ( -. A <_ 0 \/ -. B <_ 0 ) -> ( 0 <_ A /\ 0 <_ B ) ) )
52 1 51 biimtrid 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ 0 <_ ( A x. B ) ) -> ( -. ( A <_ 0 /\ B <_ 0 ) -> ( 0 <_ A /\ 0 <_ B ) ) )
53 52 orrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ 0 <_ ( A x. B ) ) -> ( ( A <_ 0 /\ B <_ 0 ) \/ ( 0 <_ A /\ 0 <_ B ) ) )
54 53 ex 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ ( A x. B ) -> ( ( A <_ 0 /\ B <_ 0 ) \/ ( 0 <_ A /\ 0 <_ B ) ) ) )
55 le0neg1 
 |-  ( A e. RR -> ( A <_ 0 <-> 0 <_ -u A ) )
56 le0neg1 
 |-  ( B e. RR -> ( B <_ 0 <-> 0 <_ -u B ) )
57 55 56 bi2anan9 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A <_ 0 /\ B <_ 0 ) <-> ( 0 <_ -u A /\ 0 <_ -u B ) ) )
58 renegcl 
 |-  ( A e. RR -> -u A e. RR )
59 renegcl 
 |-  ( B e. RR -> -u B e. RR )
60 mulge0 
 |-  ( ( ( -u A e. RR /\ 0 <_ -u A ) /\ ( -u B e. RR /\ 0 <_ -u B ) ) -> 0 <_ ( -u A x. -u B ) )
61 60 an4s 
 |-  ( ( ( -u A e. RR /\ -u B e. RR ) /\ ( 0 <_ -u A /\ 0 <_ -u B ) ) -> 0 <_ ( -u A x. -u B ) )
62 61 ex 
 |-  ( ( -u A e. RR /\ -u B e. RR ) -> ( ( 0 <_ -u A /\ 0 <_ -u B ) -> 0 <_ ( -u A x. -u B ) ) )
63 58 59 62 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 <_ -u A /\ 0 <_ -u B ) -> 0 <_ ( -u A x. -u B ) ) )
64 mul2neg 
 |-  ( ( A e. CC /\ B e. CC ) -> ( -u A x. -u B ) = ( A x. B ) )
65 24 22 64 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( -u A x. -u B ) = ( A x. B ) )
66 65 breq2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ ( -u A x. -u B ) <-> 0 <_ ( A x. B ) ) )
67 63 66 sylibd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 <_ -u A /\ 0 <_ -u B ) -> 0 <_ ( A x. B ) ) )
68 57 67 sylbid 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A <_ 0 /\ B <_ 0 ) -> 0 <_ ( A x. B ) ) )
69 mulge0 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( A x. B ) )
70 69 an4s 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> 0 <_ ( A x. B ) )
71 70 ex 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 <_ A /\ 0 <_ B ) -> 0 <_ ( A x. B ) ) )
72 68 71 jaod 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A <_ 0 /\ B <_ 0 ) \/ ( 0 <_ A /\ 0 <_ B ) ) -> 0 <_ ( A x. B ) ) )
73 54 72 impbid 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 <_ ( A x. B ) <-> ( ( A <_ 0 /\ B <_ 0 ) \/ ( 0 <_ A /\ 0 <_ B ) ) ) )