Step | Hyp | Ref
| Expression |
1 | | mul2lt0.1 |
. . . . . . . . 9
โข (๐ โ ๐ด โ โ) |
2 | | mul2lt0.2 |
. . . . . . . . 9
โข (๐ โ ๐ต โ โ) |
3 | 1, 2 | remulcld 11248 |
. . . . . . . 8
โข (๐ โ (๐ด ยท ๐ต) โ โ) |
4 | | 0red 11221 |
. . . . . . . 8
โข (๐ โ 0 โ
โ) |
5 | 3, 4 | ltnled 11365 |
. . . . . . 7
โข (๐ โ ((๐ด ยท ๐ต) < 0 โ ยฌ 0 โค (๐ด ยท ๐ต))) |
6 | 1 | adantr 480 |
. . . . . . . . . 10
โข ((๐ โง (0 โค ๐ด โง 0 โค ๐ต)) โ ๐ด โ โ) |
7 | 2 | adantr 480 |
. . . . . . . . . 10
โข ((๐ โง (0 โค ๐ด โง 0 โค ๐ต)) โ ๐ต โ โ) |
8 | | simprl 768 |
. . . . . . . . . 10
โข ((๐ โง (0 โค ๐ด โง 0 โค ๐ต)) โ 0 โค ๐ด) |
9 | | simprr 770 |
. . . . . . . . . 10
โข ((๐ โง (0 โค ๐ด โง 0 โค ๐ต)) โ 0 โค ๐ต) |
10 | 6, 7, 8, 9 | mulge0d 11795 |
. . . . . . . . 9
โข ((๐ โง (0 โค ๐ด โง 0 โค ๐ต)) โ 0 โค (๐ด ยท ๐ต)) |
11 | 10 | ex 412 |
. . . . . . . 8
โข (๐ โ ((0 โค ๐ด โง 0 โค ๐ต) โ 0 โค (๐ด ยท ๐ต))) |
12 | 11 | con3d 152 |
. . . . . . 7
โข (๐ โ (ยฌ 0 โค (๐ด ยท ๐ต) โ ยฌ (0 โค ๐ด โง 0 โค ๐ต))) |
13 | 5, 12 | sylbid 239 |
. . . . . 6
โข (๐ โ ((๐ด ยท ๐ต) < 0 โ ยฌ (0 โค ๐ด โง 0 โค ๐ต))) |
14 | | ianor 978 |
. . . . . 6
โข (ยฌ (0
โค ๐ด โง 0 โค ๐ต) โ (ยฌ 0 โค ๐ด โจ ยฌ 0 โค ๐ต)) |
15 | 13, 14 | imbitrdi 250 |
. . . . 5
โข (๐ โ ((๐ด ยท ๐ต) < 0 โ (ยฌ 0 โค ๐ด โจ ยฌ 0 โค ๐ต))) |
16 | 1, 4 | ltnled 11365 |
. . . . . 6
โข (๐ โ (๐ด < 0 โ ยฌ 0 โค ๐ด)) |
17 | 2, 4 | ltnled 11365 |
. . . . . 6
โข (๐ โ (๐ต < 0 โ ยฌ 0 โค ๐ต)) |
18 | 16, 17 | orbi12d 915 |
. . . . 5
โข (๐ โ ((๐ด < 0 โจ ๐ต < 0) โ (ยฌ 0 โค ๐ด โจ ยฌ 0 โค ๐ต))) |
19 | 15, 18 | sylibrd 259 |
. . . 4
โข (๐ โ ((๐ด ยท ๐ต) < 0 โ (๐ด < 0 โจ ๐ต < 0))) |
20 | 19 | imp 406 |
. . 3
โข ((๐ โง (๐ด ยท ๐ต) < 0) โ (๐ด < 0 โจ ๐ต < 0)) |
21 | | simpr 484 |
. . . . . 6
โข (((๐ โง (๐ด ยท ๐ต) < 0) โง ๐ด < 0) โ ๐ด < 0) |
22 | 1 | adantr 480 |
. . . . . . 7
โข ((๐ โง (๐ด ยท ๐ต) < 0) โ ๐ด โ โ) |
23 | 2 | adantr 480 |
. . . . . . 7
โข ((๐ โง (๐ด ยท ๐ต) < 0) โ ๐ต โ โ) |
24 | | simpr 484 |
. . . . . . 7
โข ((๐ โง (๐ด ยท ๐ต) < 0) โ (๐ด ยท ๐ต) < 0) |
25 | 22, 23, 24 | mul2lt0llt0 13084 |
. . . . . 6
โข (((๐ โง (๐ด ยท ๐ต) < 0) โง ๐ด < 0) โ 0 < ๐ต) |
26 | 21, 25 | jca 511 |
. . . . 5
โข (((๐ โง (๐ด ยท ๐ต) < 0) โง ๐ด < 0) โ (๐ด < 0 โง 0 < ๐ต)) |
27 | 26 | ex 412 |
. . . 4
โข ((๐ โง (๐ด ยท ๐ต) < 0) โ (๐ด < 0 โ (๐ด < 0 โง 0 < ๐ต))) |
28 | 22, 23, 24 | mul2lt0rlt0 13082 |
. . . . . 6
โข (((๐ โง (๐ด ยท ๐ต) < 0) โง ๐ต < 0) โ 0 < ๐ด) |
29 | | simpr 484 |
. . . . . 6
โข (((๐ โง (๐ด ยท ๐ต) < 0) โง ๐ต < 0) โ ๐ต < 0) |
30 | 28, 29 | jca 511 |
. . . . 5
โข (((๐ โง (๐ด ยท ๐ต) < 0) โง ๐ต < 0) โ (0 < ๐ด โง ๐ต < 0)) |
31 | 30 | ex 412 |
. . . 4
โข ((๐ โง (๐ด ยท ๐ต) < 0) โ (๐ต < 0 โ (0 < ๐ด โง ๐ต < 0))) |
32 | 27, 31 | orim12d 961 |
. . 3
โข ((๐ โง (๐ด ยท ๐ต) < 0) โ ((๐ด < 0 โจ ๐ต < 0) โ ((๐ด < 0 โง 0 < ๐ต) โจ (0 < ๐ด โง ๐ต < 0)))) |
33 | 20, 32 | mpd 15 |
. 2
โข ((๐ โง (๐ด ยท ๐ต) < 0) โ ((๐ด < 0 โง 0 < ๐ต) โจ (0 < ๐ด โง ๐ต < 0))) |
34 | 1 | adantr 480 |
. . . . 5
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ ๐ด โ โ) |
35 | | 0red 11221 |
. . . . 5
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ 0 โ โ) |
36 | 2 | adantr 480 |
. . . . . 6
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ ๐ต โ โ) |
37 | | simprr 770 |
. . . . . 6
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ 0 < ๐ต) |
38 | 36, 37 | elrpd 13019 |
. . . . 5
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ ๐ต โ
โ+) |
39 | | simprl 768 |
. . . . 5
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ ๐ด < 0) |
40 | 34, 35, 38, 39 | ltmul1dd 13077 |
. . . 4
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ (๐ด ยท ๐ต) < (0 ยท ๐ต)) |
41 | 36 | recnd 11246 |
. . . . 5
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ ๐ต โ โ) |
42 | 41 | mul02d 11416 |
. . . 4
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ (0 ยท ๐ต) = 0) |
43 | 40, 42 | breqtrd 5167 |
. . 3
โข ((๐ โง (๐ด < 0 โง 0 < ๐ต)) โ (๐ด ยท ๐ต) < 0) |
44 | 2 | adantr 480 |
. . . . 5
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ ๐ต โ โ) |
45 | | 0red 11221 |
. . . . 5
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ 0 โ
โ) |
46 | 1 | adantr 480 |
. . . . . 6
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ ๐ด โ โ) |
47 | | simprl 768 |
. . . . . 6
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ 0 < ๐ด) |
48 | 46, 47 | elrpd 13019 |
. . . . 5
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ ๐ด โ
โ+) |
49 | | simprr 770 |
. . . . 5
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ ๐ต < 0) |
50 | 44, 45, 48, 49 | ltmul2dd 13078 |
. . . 4
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ (๐ด ยท ๐ต) < (๐ด ยท 0)) |
51 | 46 | recnd 11246 |
. . . . 5
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ ๐ด โ โ) |
52 | 51 | mul01d 11417 |
. . . 4
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ (๐ด ยท 0) = 0) |
53 | 50, 52 | breqtrd 5167 |
. . 3
โข ((๐ โง (0 < ๐ด โง ๐ต < 0)) โ (๐ด ยท ๐ต) < 0) |
54 | 43, 53 | jaodan 954 |
. 2
โข ((๐ โง ((๐ด < 0 โง 0 < ๐ต) โจ (0 < ๐ด โง ๐ต < 0))) โ (๐ด ยท ๐ต) < 0) |
55 | 33, 54 | impbida 798 |
1
โข (๐ โ ((๐ด ยท ๐ต) < 0 โ ((๐ด < 0 โง 0 < ๐ต) โจ (0 < ๐ด โง ๐ต < 0)))) |