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