Metamath Proof Explorer

Theorem mul2lt0bi

Description: If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 19-Sep-2018)

Ref Expression
Hypotheses mul2lt0.1 
|- ( ph -> A e. RR )
mul2lt0.2 
|- ( ph -> B e. RR )
Assertion mul2lt0bi 
|- ( ph -> ( ( A x. B ) < 0 <-> ( ( A < 0 /\ 0 < B ) \/ ( 0 < A /\ B < 0 ) ) ) )

Proof

Step Hyp Ref Expression
1 mul2lt0.1 
 |-  ( ph -> A e. RR )
2 mul2lt0.2 
 |-  ( ph -> B e. RR )
3 1 2 remulcld 
 |-  ( ph -> ( A x. B ) e. RR )
4 0red 
 |-  ( ph -> 0 e. RR )
5 3 4 ltnled 
 |-  ( ph -> ( ( A x. B ) < 0 <-> -. 0 <_ ( A x. B ) ) )
6 1 adantr 
 |-  ( ( ph /\ ( 0 <_ A /\ 0 <_ B ) ) -> A e. RR )
7 2 adantr 
 |-  ( ( ph /\ ( 0 <_ A /\ 0 <_ B ) ) -> B e. RR )
8 simprl 
 |-  ( ( ph /\ ( 0 <_ A /\ 0 <_ B ) ) -> 0 <_ A )
9 simprr 
 |-  ( ( ph /\ ( 0 <_ A /\ 0 <_ B ) ) -> 0 <_ B )
10 6 7 8 9 mulge0d 
 |-  ( ( ph /\ ( 0 <_ A /\ 0 <_ B ) ) -> 0 <_ ( A x. B ) )
11 10 ex 
 |-  ( ph -> ( ( 0 <_ A /\ 0 <_ B ) -> 0 <_ ( A x. B ) ) )
12 11 con3d 
 |-  ( ph -> ( -. 0 <_ ( A x. B ) -> -. ( 0 <_ A /\ 0 <_ B ) ) )
13 5 12 sylbid 
 |-  ( ph -> ( ( A x. B ) < 0 -> -. ( 0 <_ A /\ 0 <_ B ) ) )
14 ianor 
 |-  ( -. ( 0 <_ A /\ 0 <_ B ) <-> ( -. 0 <_ A \/ -. 0 <_ B ) )
15 13 14 imbitrdi 
 |-  ( ph -> ( ( A x. B ) < 0 -> ( -. 0 <_ A \/ -. 0 <_ B ) ) )
16 1 4 ltnled 
 |-  ( ph -> ( A < 0 <-> -. 0 <_ A ) )
17 2 4 ltnled 
 |-  ( ph -> ( B < 0 <-> -. 0 <_ B ) )
18 16 17 orbi12d 
 |-  ( ph -> ( ( A < 0 \/ B < 0 ) <-> ( -. 0 <_ A \/ -. 0 <_ B ) ) )
19 15 18 sylibrd 
 |-  ( ph -> ( ( A x. B ) < 0 -> ( A < 0 \/ B < 0 ) ) )
20 19 imp 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( A < 0 \/ B < 0 ) )
21 simpr 
 |-  ( ( ( ph /\ ( A x. B ) < 0 ) /\ A < 0 ) -> A < 0 )
22 1 adantr 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> A e. RR )
23 2 adantr 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> B e. RR )
24 simpr 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( A x. B ) < 0 )
25 22 23 24 mul2lt0llt0 
 |-  ( ( ( ph /\ ( A x. B ) < 0 ) /\ A < 0 ) -> 0 < B )
26 21 25 jca 
 |-  ( ( ( ph /\ ( A x. B ) < 0 ) /\ A < 0 ) -> ( A < 0 /\ 0 < B ) )
27 26 ex 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( A < 0 -> ( A < 0 /\ 0 < B ) ) )
28 22 23 24 mul2lt0rlt0 
 |-  ( ( ( ph /\ ( A x. B ) < 0 ) /\ B < 0 ) -> 0 < A )
29 simpr 
 |-  ( ( ( ph /\ ( A x. B ) < 0 ) /\ B < 0 ) -> B < 0 )
30 28 29 jca 
 |-  ( ( ( ph /\ ( A x. B ) < 0 ) /\ B < 0 ) -> ( 0 < A /\ B < 0 ) )
31 30 ex 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( B < 0 -> ( 0 < A /\ B < 0 ) ) )
32 27 31 orim12d 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( ( A < 0 \/ B < 0 ) -> ( ( A < 0 /\ 0 < B ) \/ ( 0 < A /\ B < 0 ) ) ) )
33 20 32 mpd 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( ( A < 0 /\ 0 < B ) \/ ( 0 < A /\ B < 0 ) ) )
34 1 adantr 
 |-  ( ( ph /\ ( A < 0 /\ 0 < B ) ) -> A e. RR )
35 0red 
 |-  ( ( ph /\ ( A < 0 /\ 0 < B ) ) -> 0 e. RR )
36 2 adantr 
 |-  ( ( ph /\ ( A < 0 /\ 0 < B ) ) -> B e. RR )
37 simprr 
 |-  ( ( ph /\ ( A < 0 /\ 0 < B ) ) -> 0 < B )
38 36 37 elrpd 
 |-  ( ( ph /\ ( A < 0 /\ 0 < B ) ) -> B e. RR+ )
39 simprl 
 |-  ( ( ph /\ ( A < 0 /\ 0 < B ) ) -> A < 0 )
40 34 35 38 39 ltmul1dd 
 |-  ( ( ph /\ ( A < 0 /\ 0 < B ) ) -> ( A x. B ) < ( 0 x. B ) )
41 36 recnd 
 |-  ( ( ph /\ ( A < 0 /\ 0 < B ) ) -> B e. CC )
42 41 mul02d 
 |-  ( ( ph /\ ( A < 0 /\ 0 < B ) ) -> ( 0 x. B ) = 0 )
43 40 42 breqtrd 
 |-  ( ( ph /\ ( A < 0 /\ 0 < B ) ) -> ( A x. B ) < 0 )
44 2 adantr 
 |-  ( ( ph /\ ( 0 < A /\ B < 0 ) ) -> B e. RR )
45 0red 
 |-  ( ( ph /\ ( 0 < A /\ B < 0 ) ) -> 0 e. RR )
46 1 adantr 
 |-  ( ( ph /\ ( 0 < A /\ B < 0 ) ) -> A e. RR )
47 simprl 
 |-  ( ( ph /\ ( 0 < A /\ B < 0 ) ) -> 0 < A )
48 46 47 elrpd 
 |-  ( ( ph /\ ( 0 < A /\ B < 0 ) ) -> A e. RR+ )
49 simprr 
 |-  ( ( ph /\ ( 0 < A /\ B < 0 ) ) -> B < 0 )
50 44 45 48 49 ltmul2dd 
 |-  ( ( ph /\ ( 0 < A /\ B < 0 ) ) -> ( A x. B ) < ( A x. 0 ) )
51 46 recnd 
 |-  ( ( ph /\ ( 0 < A /\ B < 0 ) ) -> A e. CC )
52 51 mul01d 
 |-  ( ( ph /\ ( 0 < A /\ B < 0 ) ) -> ( A x. 0 ) = 0 )
53 50 52 breqtrd 
 |-  ( ( ph /\ ( 0 < A /\ B < 0 ) ) -> ( A x. B ) < 0 )
54 43 53 jaodan 
 |-  ( ( ph /\ ( ( A < 0 /\ 0 < B ) \/ ( 0 < A /\ B < 0 ) ) ) -> ( A x. B ) < 0 )
55 33 54 impbida 
 |-  ( ph -> ( ( A x. B ) < 0 <-> ( ( A < 0 /\ 0 < B ) \/ ( 0 < A /\ B < 0 ) ) ) )