Step | Hyp | Ref
| Expression |
1 | | mul2lt0.1 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
2 | | mul2lt0.2 |
. . . . . . . . 9
โข (๐ โ ๐ต โ โ) |
3 | 1, 2 | remulcld 11186 |
. . . . . . . 8
โข (๐ โ (๐ด ยท ๐ต) โ โ) |
4 | | 0red 11159 |
. . . . . . . 8
โข (๐ โ 0 โ
โ) |
5 | 3, 4 | ltnled 11303 |
. . . . . . 7
โข (๐ โ ((๐ด ยท ๐ต) < 0 โ ยฌ 0 โค (๐ด ยท ๐ต))) |
6 | 1 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง (0 โค ๐ด โง 0 โค ๐ต)) โ ๐ด โ โ) |
7 | 2 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง (0 โค ๐ด โง 0 โค ๐ต)) โ ๐ต โ โ) |
8 | | simprl 770 |
. . . . . . . . . 10
โข ((๐ โง (0 โค ๐ด โง 0 โค ๐ต)) โ 0 โค ๐ด) |
9 | | simprr 772 |
. . . . . . . . . 10
โข ((๐ โง (0 โค ๐ด โง 0 โค ๐ต)) โ 0 โค ๐ต) |
10 | 6, 7, 8, 9 | mulge0d 11733 |
. . . . . . . . 9
โข ((๐ โง (0 โค ๐ด โง 0 โค ๐ต)) โ 0 โค (๐ด ยท ๐ต)) |
11 | 10 | ex 414 |
. . . . . . . 8
โข (๐ โ ((0 โค ๐ด โง 0 โค ๐ต) โ 0 โค (๐ด ยท ๐ต))) |
12 | 11 | con3d 152 |
. . . . . . 7
โข (๐ โ (ยฌ 0 โค (๐ด ยท ๐ต) โ ยฌ (0 โค ๐ด โง 0 โค ๐ต))) |
13 | 5, 12 | sylbid 239 |
. . . . . 6
โข (๐ โ ((๐ด ยท ๐ต) < 0 โ ยฌ (0 โค ๐ด โง 0 โค ๐ต))) |
14 | | ianor 981 |
. . . . . 6
โข (ยฌ (0
โค ๐ด โง 0 โค ๐ต) โ (ยฌ 0 โค ๐ด โจ ยฌ 0 โค ๐ต)) |
15 | 13, 14 | syl6ib 251 |
. . . . 5
โข (๐ โ ((๐ด ยท ๐ต) < 0 โ (ยฌ 0 โค ๐ด โจ ยฌ 0 โค ๐ต))) |
16 | 1, 4 | ltnled 11303 |
. . . . . 6
โข (๐ โ (๐ด < 0 โ ยฌ 0 โค ๐ด)) |
17 | 2, 4 | ltnled 11303 |
. . . . . 6
โข (๐ โ (๐ต < 0 โ ยฌ 0 โค ๐ต)) |
18 | 16, 17 | orbi12d 918 |
. . . . 5
โข (๐ โ ((๐ด < 0 โจ ๐ต < 0) โ (ยฌ 0 โค ๐ด โจ ยฌ 0 โค ๐ต))) |
19 | 15, 18 | sylibrd 259 |
. . . 4
โข (๐ โ ((๐ด ยท ๐ต) < 0 โ (๐ด < 0 โจ ๐ต < 0))) |
20 | 19 | imp 408 |
. . 3
โข ((๐ โง (๐ด ยท ๐ต) < 0) โ (๐ด < 0 โจ ๐ต < 0)) |
21 | | simpr 486 |
. . . . . 6
โข (((๐ โง (๐ด ยท ๐ต) < 0) โง ๐ด < 0) โ ๐ด < 0) |
22 | 1 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐ด ยท ๐ต) < 0) โ ๐ด โ โ) |
23 | 2 | adantr 482 |
. . . . . . 7
โข ((๐ โง (๐ด ยท ๐ต) < 0) โ ๐ต โ โ) |
24 | | simpr 486 |
. . . . . . 7
โข ((๐ โง (๐ด ยท ๐ต) < 0) โ (๐ด ยท ๐ต) < 0) |
25 | 22, 23, 24 | mul2lt0llt0 13020 |
. . . . . 6
โข (((๐ โง (๐ด ยท ๐ต) < 0) โง ๐ด < 0) โ 0 < ๐ต) |
26 | 21, 25 | jca 513 |
. . . . 5
โข (((๐ โง (๐ด ยท ๐ต) < 0) โง ๐ด < 0) โ (๐ด < 0 โง 0 < ๐ต)) |
27 | 26 | ex 414 |
. . . 4
โข ((๐ โง (๐ด ยท ๐ต) < 0) โ (๐ด < 0 โ (๐ด < 0 โง 0 < ๐ต))) |
28 | 22, 23, 24 | mul2lt0rlt0 13018 |
. . . . . 6
โข (((๐ โง (๐ด ยท ๐ต) < 0) โง ๐ต < 0) โ 0 < ๐ด) |
29 | | simpr 486 |
. . . . . 6
โข (((๐ โง (๐ด ยท ๐ต) < 0) โง ๐ต < 0) โ ๐ต < 0) |
30 | 28, 29 | jca 513 |
. . . . 5
โข (((๐ โง (๐ด ยท ๐ต) < 0) โง ๐ต < 0) โ (0 < ๐ด โง ๐ต < 0)) |
31 | 30 | ex 414 |
. . . 4
โข ((๐ โง (๐ด ยท ๐ต) < 0) โ (๐ต < 0 โ (0 < ๐ด โง ๐ต < 0))) |
32 | 27, 31 | orim12d 964 |
. . 3
โข ((๐ โง (๐ด ยท ๐ต) < 0) โ ((๐ด < 0 โจ ๐ต < 0) โ ((๐ด < 0 โง 0 < ๐ต) โจ (0 < ๐ด โง ๐ต < 0)))) |
33 | 20, 32 | mpd 15 |
. 2
โข ((๐ โง (๐ด ยท ๐ต) < 0) โ ((๐ด < 0 โง 0 < ๐ต) โจ (0 < ๐ด โง ๐ต < 0))) |
34 | 1 | adantr 482 |
. . . . 5
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ ๐ด โ โ) |
35 | | 0red 11159 |
. . . . 5
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ 0 โ โ) |
36 | 2 | adantr 482 |
. . . . . 6
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ ๐ต โ โ) |
37 | | simprr 772 |
. . . . . 6
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ 0 < ๐ต) |
38 | 36, 37 | elrpd 12955 |
. . . . 5
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ ๐ต โ
โ+) |
39 | | simprl 770 |
. . . . 5
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ ๐ด < 0) |
40 | 34, 35, 38, 39 | ltmul1dd 13013 |
. . . 4
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ (๐ด ยท ๐ต) < (0 ยท ๐ต)) |
41 | 36 | recnd 11184 |
. . . . 5
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ ๐ต โ โ) |
42 | 41 | mul02d 11354 |
. . . 4
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ (0 ยท ๐ต) = 0) |
43 | 40, 42 | breqtrd 5132 |
. . 3
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ (๐ด ยท ๐ต) < 0) |
44 | 2 | adantr 482 |
. . . . 5
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ ๐ต โ โ) |
45 | | 0red 11159 |
. . . . 5
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ 0 โ
โ) |
46 | 1 | adantr 482 |
. . . . . 6
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ ๐ด โ โ) |
47 | | simprl 770 |
. . . . . 6
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ 0 < ๐ด) |
48 | 46, 47 | elrpd 12955 |
. . . . 5
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ ๐ด โ
โ+) |
49 | | simprr 772 |
. . . . 5
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ ๐ต < 0) |
50 | 44, 45, 48, 49 | ltmul2dd 13014 |
. . . 4
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ (๐ด ยท ๐ต) < (๐ด ยท 0)) |
51 | 46 | recnd 11184 |
. . . . 5
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ ๐ด โ โ) |
52 | 51 | mul01d 11355 |
. . . 4
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ (๐ด ยท 0) = 0) |
53 | 50, 52 | breqtrd 5132 |
. . 3
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ (๐ด ยท ๐ต) < 0) |
54 | 43, 53 | jaodan 957 |
. 2
โข ((๐ โง ((๐ด < 0 โง 0 < ๐ต) โจ (0 < ๐ด โง ๐ต < 0))) โ (๐ด ยท ๐ต) < 0) |
55 | 33, 54 | impbida 800 |
1
โข (๐ โ ((๐ด ยท ๐ต) < 0 โ ((๐ด < 0 โง 0 < ๐ต) โจ (0 < ๐ด โง ๐ต < 0)))) |