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 syl6ib
 |-  ( 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 ) ) ) )