Step | Hyp | Ref
| Expression |
1 | | ianor 981 |
. . . . 5
โข (ยฌ
(๐ด โค 0 โง ๐ต โค 0) โ (ยฌ ๐ด โค 0 โจ ยฌ ๐ต โค 0)) |
2 | | 0re 11165 |
. . . . . . . . . 10
โข 0 โ
โ |
3 | | ltnle 11242 |
. . . . . . . . . 10
โข ((0
โ โ โง ๐ด
โ โ) โ (0 < ๐ด โ ยฌ ๐ด โค 0)) |
4 | 2, 3 | mpan 689 |
. . . . . . . . 9
โข (๐ด โ โ โ (0 <
๐ด โ ยฌ ๐ด โค 0)) |
5 | 4 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 <
๐ด โ ยฌ ๐ด โค 0)) |
6 | | ltnle 11242 |
. . . . . . . . . 10
โข ((0
โ โ โง ๐ต
โ โ) โ (0 < ๐ต โ ยฌ ๐ต โค 0)) |
7 | 2, 6 | mpan 689 |
. . . . . . . . 9
โข (๐ต โ โ โ (0 <
๐ต โ ยฌ ๐ต โค 0)) |
8 | 7 | adantl 483 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 <
๐ต โ ยฌ ๐ต โค 0)) |
9 | 5, 8 | orbi12d 918 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0 <
๐ด โจ 0 < ๐ต) โ (ยฌ ๐ด โค 0 โจ ยฌ ๐ต โค 0))) |
10 | 9 | adantr 482 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง 0 โค
(๐ด ยท ๐ต)) โ ((0 < ๐ด โจ 0 < ๐ต) โ (ยฌ ๐ด โค 0 โจ ยฌ ๐ต โค 0))) |
11 | | ltle 11251 |
. . . . . . . . . . . 12
โข ((0
โ โ โง ๐ด
โ โ) โ (0 < ๐ด โ 0 โค ๐ด)) |
12 | 2, 11 | mpan 689 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (0 <
๐ด โ 0 โค ๐ด)) |
13 | 12 | imp 408 |
. . . . . . . . . 10
โข ((๐ด โ โ โง 0 <
๐ด) โ 0 โค ๐ด) |
14 | 13 | ad2ant2rl 748 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ด)) โ 0 โค ๐ด) |
15 | | remulcl 11144 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |
16 | 15 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ด)) โ (๐ด ยท ๐ต) โ โ) |
17 | | simprl 770 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ด)) โ 0 โค (๐ด ยท ๐ต)) |
18 | | simpll 766 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ด)) โ ๐ด โ โ) |
19 | | simprr 772 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ด)) โ 0 < ๐ด) |
20 | | divge0 12032 |
. . . . . . . . . . 11
โข ((((๐ด ยท ๐ต) โ โ โง 0 โค (๐ด ยท ๐ต)) โง (๐ด โ โ โง 0 < ๐ด)) โ 0 โค ((๐ด ยท ๐ต) / ๐ด)) |
21 | 16, 17, 18, 19, 20 | syl22anc 838 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ด)) โ 0 โค ((๐ด ยท ๐ต) / ๐ด)) |
22 | | recn 11149 |
. . . . . . . . . . . 12
โข (๐ต โ โ โ ๐ต โ
โ) |
23 | 22 | ad2antlr 726 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ด)) โ ๐ต โ โ) |
24 | | recn 11149 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ ๐ด โ
โ) |
25 | 24 | ad2antrr 725 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ด)) โ ๐ด โ โ) |
26 | | gt0ne0 11628 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง 0 <
๐ด) โ ๐ด โ 0) |
27 | 26 | ad2ant2rl 748 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ด)) โ ๐ด โ 0) |
28 | 23, 25, 27 | divcan3d 11944 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ด)) โ ((๐ด ยท ๐ต) / ๐ด) = ๐ต) |
29 | 21, 28 | breqtrd 5135 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ด)) โ 0 โค ๐ต) |
30 | 14, 29 | jca 513 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ด)) โ (0 โค ๐ด โง 0 โค ๐ต)) |
31 | 30 | expr 458 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง 0 โค
(๐ด ยท ๐ต)) โ (0 < ๐ด โ (0 โค ๐ด โง 0 โค ๐ต))) |
32 | 15 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ต)) โ (๐ด ยท ๐ต) โ โ) |
33 | | simprl 770 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ต)) โ 0 โค (๐ด ยท ๐ต)) |
34 | | simplr 768 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ต)) โ ๐ต โ โ) |
35 | | simprr 772 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ต)) โ 0 < ๐ต) |
36 | | divge0 12032 |
. . . . . . . . . . 11
โข ((((๐ด ยท ๐ต) โ โ โง 0 โค (๐ด ยท ๐ต)) โง (๐ต โ โ โง 0 < ๐ต)) โ 0 โค ((๐ด ยท ๐ต) / ๐ต)) |
37 | 32, 33, 34, 35, 36 | syl22anc 838 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ต)) โ 0 โค ((๐ด ยท ๐ต) / ๐ต)) |
38 | 24 | ad2antrr 725 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ต)) โ ๐ด โ โ) |
39 | 22 | ad2antlr 726 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ต)) โ ๐ต โ โ) |
40 | | gt0ne0 11628 |
. . . . . . . . . . . 12
โข ((๐ต โ โ โง 0 <
๐ต) โ ๐ต โ 0) |
41 | 40 | ad2ant2l 745 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ต)) โ ๐ต โ 0) |
42 | 38, 39, 41 | divcan4d 11945 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ต)) โ ((๐ด ยท ๐ต) / ๐ต) = ๐ด) |
43 | 37, 42 | breqtrd 5135 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ต)) โ 0 โค ๐ด) |
44 | | ltle 11251 |
. . . . . . . . . . . 12
โข ((0
โ โ โง ๐ต
โ โ) โ (0 < ๐ต โ 0 โค ๐ต)) |
45 | 2, 44 | mpan 689 |
. . . . . . . . . . 11
โข (๐ต โ โ โ (0 <
๐ต โ 0 โค ๐ต)) |
46 | 45 | imp 408 |
. . . . . . . . . 10
โข ((๐ต โ โ โง 0 <
๐ต) โ 0 โค ๐ต) |
47 | 46 | ad2ant2l 745 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ต)) โ 0 โค ๐ต) |
48 | 43, 47 | jca 513 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
(๐ด ยท ๐ต) โง 0 < ๐ต)) โ (0 โค ๐ด โง 0 โค ๐ต)) |
49 | 48 | expr 458 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง 0 โค
(๐ด ยท ๐ต)) โ (0 < ๐ต โ (0 โค ๐ด โง 0 โค ๐ต))) |
50 | 31, 49 | jaod 858 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง 0 โค
(๐ด ยท ๐ต)) โ ((0 < ๐ด โจ 0 < ๐ต) โ (0 โค ๐ด โง 0 โค ๐ต))) |
51 | 10, 50 | sylbird 260 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง 0 โค
(๐ด ยท ๐ต)) โ ((ยฌ ๐ด โค 0 โจ ยฌ ๐ต โค 0) โ (0 โค ๐ด โง 0 โค ๐ต))) |
52 | 1, 51 | biimtrid 241 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง 0 โค
(๐ด ยท ๐ต)) โ (ยฌ (๐ด โค 0 โง ๐ต โค 0) โ (0 โค ๐ด โง 0 โค ๐ต))) |
53 | 52 | orrd 862 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง 0 โค
(๐ด ยท ๐ต)) โ ((๐ด โค 0 โง ๐ต โค 0) โจ (0 โค ๐ด โง 0 โค ๐ต))) |
54 | 53 | ex 414 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 โค
(๐ด ยท ๐ต) โ ((๐ด โค 0 โง ๐ต โค 0) โจ (0 โค ๐ด โง 0 โค ๐ต)))) |
55 | | le0neg1 11671 |
. . . . 5
โข (๐ด โ โ โ (๐ด โค 0 โ 0 โค -๐ด)) |
56 | | le0neg1 11671 |
. . . . 5
โข (๐ต โ โ โ (๐ต โค 0 โ 0 โค -๐ต)) |
57 | 55, 56 | bi2anan9 638 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โค 0 โง ๐ต โค 0) โ (0 โค -๐ด โง 0 โค -๐ต))) |
58 | | renegcl 11472 |
. . . . . 6
โข (๐ด โ โ โ -๐ด โ
โ) |
59 | | renegcl 11472 |
. . . . . 6
โข (๐ต โ โ โ -๐ต โ
โ) |
60 | | mulge0 11681 |
. . . . . . . 8
โข (((-๐ด โ โ โง 0 โค
-๐ด) โง (-๐ต โ โ โง 0 โค
-๐ต)) โ 0 โค (-๐ด ยท -๐ต)) |
61 | 60 | an4s 659 |
. . . . . . 7
โข (((-๐ด โ โ โง -๐ต โ โ) โง (0 โค
-๐ด โง 0 โค -๐ต)) โ 0 โค (-๐ด ยท -๐ต)) |
62 | 61 | ex 414 |
. . . . . 6
โข ((-๐ด โ โ โง -๐ต โ โ) โ ((0 โค
-๐ด โง 0 โค -๐ต) โ 0 โค (-๐ด ยท -๐ต))) |
63 | 58, 59, 62 | syl2an 597 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0 โค
-๐ด โง 0 โค -๐ต) โ 0 โค (-๐ด ยท -๐ต))) |
64 | | mul2neg 11602 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (-๐ด ยท -๐ต) = (๐ด ยท ๐ต)) |
65 | 24, 22, 64 | syl2an 597 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (-๐ด ยท -๐ต) = (๐ด ยท ๐ต)) |
66 | 65 | breq2d 5121 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 โค
(-๐ด ยท -๐ต) โ 0 โค (๐ด ยท ๐ต))) |
67 | 63, 66 | sylibd 238 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0 โค
-๐ด โง 0 โค -๐ต) โ 0 โค (๐ด ยท ๐ต))) |
68 | 57, 67 | sylbid 239 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โค 0 โง ๐ต โค 0) โ 0 โค (๐ด ยท ๐ต))) |
69 | | mulge0 11681 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ 0 โค (๐ด ยท ๐ต)) |
70 | 69 | an4s 659 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 โค
๐ด โง 0 โค ๐ต)) โ 0 โค (๐ด ยท ๐ต)) |
71 | 70 | ex 414 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((0 โค
๐ด โง 0 โค ๐ต) โ 0 โค (๐ด ยท ๐ต))) |
72 | 68, 71 | jaod 858 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (((๐ด โค 0 โง ๐ต โค 0) โจ (0 โค ๐ด โง 0 โค ๐ต)) โ 0 โค (๐ด ยท ๐ต))) |
73 | 54, 72 | impbid 211 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 โค
(๐ด ยท ๐ต) โ ((๐ด โค 0 โง ๐ต โค 0) โจ (0 โค ๐ด โง 0 โค ๐ต)))) |