Step | Hyp | Ref
| Expression |
1 | | simplrr 777 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ ๐ต โ 0) |
2 | 1 | biantrud 533 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ (0 โค ๐ต โ (0 โค ๐ต โง ๐ต โ 0))) |
3 | | 0re 11164 |
. . . . . . . . . . 11
โข 0 โ
โ |
4 | | simpl2 1193 |
. . . . . . . . . . . . 13
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ๐ต โ โค) |
5 | 4 | zred 12614 |
. . . . . . . . . . . 12
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ๐ต โ โ) |
6 | 5 | adantr 482 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ ๐ต โ โ) |
7 | | ltlen 11263 |
. . . . . . . . . . 11
โข ((0
โ โ โง ๐ต
โ โ) โ (0 < ๐ต โ (0 โค ๐ต โง ๐ต โ 0))) |
8 | 3, 6, 7 | sylancr 588 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ (0 < ๐ต โ (0 โค ๐ต โง ๐ต โ 0))) |
9 | | simpl1 1192 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ๐ด โ โค) |
10 | 9 | zred 12614 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ๐ด โ โ) |
11 | 10 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ ๐ด โ โ) |
12 | 11 | renegcld 11589 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ -๐ด โ โ) |
13 | 12 | recnd 11190 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ -๐ด โ โ) |
14 | 13 | mul01d 11361 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ (-๐ด ยท 0) = 0) |
15 | 11 | recnd 11190 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ ๐ด โ โ) |
16 | 6 | recnd 11190 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ ๐ต โ โ) |
17 | 15, 16 | mulneg1d 11615 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ (-๐ด ยท ๐ต) = -(๐ด ยท ๐ต)) |
18 | 14, 17 | breq12d 5123 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ ((-๐ด ยท 0) < (-๐ด ยท ๐ต) โ 0 < -(๐ด ยท ๐ต))) |
19 | | 0red 11165 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ 0 โ
โ) |
20 | 10 | lt0neg1d 11731 |
. . . . . . . . . . . . 13
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ (๐ด < 0 โ 0 < -๐ด)) |
21 | 20 | biimpa 478 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ 0 < -๐ด) |
22 | | ltmul2 12013 |
. . . . . . . . . . . 12
โข ((0
โ โ โง ๐ต
โ โ โง (-๐ด
โ โ โง 0 < -๐ด)) โ (0 < ๐ต โ (-๐ด ยท 0) < (-๐ด ยท ๐ต))) |
23 | 19, 6, 12, 21, 22 | syl112anc 1375 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ (0 < ๐ต โ (-๐ด ยท 0) < (-๐ด ยท ๐ต))) |
24 | 10, 5 | remulcld 11192 |
. . . . . . . . . . . . 13
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ (๐ด ยท ๐ต) โ โ) |
25 | 24 | adantr 482 |
. . . . . . . . . . . 12
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ (๐ด ยท ๐ต) โ โ) |
26 | 25 | lt0neg1d 11731 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ ((๐ด ยท ๐ต) < 0 โ 0 < -(๐ด ยท ๐ต))) |
27 | 18, 23, 26 | 3bitr4d 311 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ (0 < ๐ต โ (๐ด ยท ๐ต) < 0)) |
28 | 2, 8, 27 | 3bitr2rd 308 |
. . . . . . . . 9
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ ((๐ด ยท ๐ต) < 0 โ 0 โค ๐ต)) |
29 | | lenlt 11240 |
. . . . . . . . . 10
โข ((0
โ โ โง ๐ต
โ โ) โ (0 โค ๐ต โ ยฌ ๐ต < 0)) |
30 | 3, 6, 29 | sylancr 588 |
. . . . . . . . 9
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ (0 โค ๐ต โ ยฌ ๐ต < 0)) |
31 | 28, 30 | bitrd 279 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ ((๐ด ยท ๐ต) < 0 โ ยฌ ๐ต < 0)) |
32 | 31 | ifbid 4514 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ if((๐ด ยท ๐ต) < 0, -1, 1) = if(ยฌ ๐ต < 0, -1,
1)) |
33 | | oveq2 7370 |
. . . . . . . . . 10
โข (if(๐ต < 0, -1, 1) = -1 โ (-1
ยท if(๐ต < 0, -1,
1)) = (-1 ยท -1)) |
34 | | neg1mulneg1e1 12373 |
. . . . . . . . . 10
โข (-1
ยท -1) = 1 |
35 | 33, 34 | eqtrdi 2793 |
. . . . . . . . 9
โข (if(๐ต < 0, -1, 1) = -1 โ (-1
ยท if(๐ต < 0, -1,
1)) = 1) |
36 | | oveq2 7370 |
. . . . . . . . . 10
โข (if(๐ต < 0, -1, 1) = 1 โ (-1
ยท if(๐ต < 0, -1,
1)) = (-1 ยท 1)) |
37 | | ax-1cn 11116 |
. . . . . . . . . . 11
โข 1 โ
โ |
38 | 37 | mulm1i 11607 |
. . . . . . . . . 10
โข (-1
ยท 1) = -1 |
39 | 36, 38 | eqtrdi 2793 |
. . . . . . . . 9
โข (if(๐ต < 0, -1, 1) = 1 โ (-1
ยท if(๐ต < 0, -1,
1)) = -1) |
40 | 35, 39 | ifsb 4504 |
. . . . . . . 8
โข (-1
ยท if(๐ต < 0, -1,
1)) = if(๐ต < 0, 1,
-1) |
41 | | ifnot 4543 |
. . . . . . . 8
โข if(ยฌ
๐ต < 0, -1, 1) = if(๐ต < 0, 1, -1) |
42 | 40, 41 | eqtr4i 2768 |
. . . . . . 7
โข (-1
ยท if(๐ต < 0, -1,
1)) = if(ยฌ ๐ต < 0,
-1, 1) |
43 | 32, 42 | eqtr4di 2795 |
. . . . . 6
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ if((๐ด ยท ๐ต) < 0, -1, 1) = (-1 ยท if(๐ต < 0, -1,
1))) |
44 | | iftrue 4497 |
. . . . . . . 8
โข (๐ด < 0 โ if(๐ด < 0, -1, 1) =
-1) |
45 | 44 | adantl 483 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ if(๐ด < 0, -1, 1) = -1) |
46 | 45 | oveq1d 7377 |
. . . . . 6
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ (if(๐ด < 0, -1, 1) ยท if(๐ต < 0, -1, 1)) = (-1 ยท
if(๐ต < 0, -1,
1))) |
47 | 43, 46 | eqtr4d 2780 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ด < 0) โ if((๐ด ยท ๐ต) < 0, -1, 1) = (if(๐ด < 0, -1, 1) ยท if(๐ต < 0, -1,
1))) |
48 | | iffalse 4500 |
. . . . . . . 8
โข (ยฌ
๐ด < 0 โ if(๐ด < 0, -1, 1) =
1) |
49 | 48 | adantl 483 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ด < 0) โ if(๐ด < 0, -1, 1) = 1) |
50 | 49 | oveq1d 7377 |
. . . . . 6
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ด < 0) โ (if(๐ด < 0, -1, 1) ยท if(๐ต < 0, -1, 1)) = (1 ยท
if(๐ต < 0, -1,
1))) |
51 | | neg1cn 12274 |
. . . . . . . . 9
โข -1 โ
โ |
52 | 51, 37 | ifcli 4538 |
. . . . . . . 8
โข if(๐ต < 0, -1, 1) โ
โ |
53 | 52 | mulid2i 11167 |
. . . . . . 7
โข (1
ยท if(๐ต < 0, -1,
1)) = if(๐ต < 0, -1,
1) |
54 | 5 | adantr 482 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ด < 0) โ ๐ต โ โ) |
55 | | 0red 11165 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ด < 0) โ 0 โ
โ) |
56 | 10 | adantr 482 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ด < 0) โ ๐ด โ โ) |
57 | | lenlt 11240 |
. . . . . . . . . . . . 13
โข ((0
โ โ โง ๐ด
โ โ) โ (0 โค ๐ด โ ยฌ ๐ด < 0)) |
58 | 3, 10, 57 | sylancr 588 |
. . . . . . . . . . . 12
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ (0 โค ๐ด โ ยฌ ๐ด < 0)) |
59 | 58 | biimpar 479 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ด < 0) โ 0 โค ๐ด) |
60 | | simplrl 776 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ด < 0) โ ๐ด โ 0) |
61 | 56, 59, 60 | ne0gt0d 11299 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ด < 0) โ 0 < ๐ด) |
62 | | ltmul2 12013 |
. . . . . . . . . 10
โข ((๐ต โ โ โง 0 โ
โ โง (๐ด โ
โ โง 0 < ๐ด))
โ (๐ต < 0 โ
(๐ด ยท ๐ต) < (๐ด ยท 0))) |
63 | 54, 55, 56, 61, 62 | syl112anc 1375 |
. . . . . . . . 9
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ด < 0) โ (๐ต < 0 โ (๐ด ยท ๐ต) < (๐ด ยท 0))) |
64 | 56 | recnd 11190 |
. . . . . . . . . . 11
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ด < 0) โ ๐ด โ โ) |
65 | 64 | mul01d 11361 |
. . . . . . . . . 10
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ด < 0) โ (๐ด ยท 0) = 0) |
66 | 65 | breq2d 5122 |
. . . . . . . . 9
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ด < 0) โ ((๐ด ยท ๐ต) < (๐ด ยท 0) โ (๐ด ยท ๐ต) < 0)) |
67 | 63, 66 | bitrd 279 |
. . . . . . . 8
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ด < 0) โ (๐ต < 0 โ (๐ด ยท ๐ต) < 0)) |
68 | 67 | ifbid 4514 |
. . . . . . 7
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ด < 0) โ if(๐ต < 0, -1, 1) = if((๐ด ยท ๐ต) < 0, -1, 1)) |
69 | 53, 68 | eqtrid 2789 |
. . . . . 6
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ด < 0) โ (1 ยท if(๐ต < 0, -1, 1)) = if((๐ด ยท ๐ต) < 0, -1, 1)) |
70 | 50, 69 | eqtr2d 2778 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ด < 0) โ if((๐ด ยท ๐ต) < 0, -1, 1) = (if(๐ด < 0, -1, 1) ยท if(๐ต < 0, -1,
1))) |
71 | 47, 70 | pm2.61dan 812 |
. . . 4
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ if((๐ด ยท ๐ต) < 0, -1, 1) = (if(๐ด < 0, -1, 1) ยท if(๐ต < 0, -1,
1))) |
72 | 71 | adantr 482 |
. . 3
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ < 0) โ if((๐ด ยท ๐ต) < 0, -1, 1) = (if(๐ด < 0, -1, 1) ยท if(๐ต < 0, -1,
1))) |
73 | | simpr 486 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ < 0) โ ๐ < 0) |
74 | 73 | biantrurd 534 |
. . . 4
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ < 0) โ ((๐ด ยท ๐ต) < 0 โ (๐ < 0 โง (๐ด ยท ๐ต) < 0))) |
75 | 74 | ifbid 4514 |
. . 3
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ < 0) โ if((๐ด ยท ๐ต) < 0, -1, 1) = if((๐ < 0 โง (๐ด ยท ๐ต) < 0), -1, 1)) |
76 | 73 | biantrurd 534 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ < 0) โ (๐ด < 0 โ (๐ < 0 โง ๐ด < 0))) |
77 | 76 | ifbid 4514 |
. . . 4
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ < 0) โ if(๐ด < 0, -1, 1) = if((๐ < 0 โง ๐ด < 0), -1, 1)) |
78 | 73 | biantrurd 534 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ < 0) โ (๐ต < 0 โ (๐ < 0 โง ๐ต < 0))) |
79 | 78 | ifbid 4514 |
. . . 4
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ < 0) โ if(๐ต < 0, -1, 1) = if((๐ < 0 โง ๐ต < 0), -1, 1)) |
80 | 77, 79 | oveq12d 7380 |
. . 3
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ < 0) โ (if(๐ด < 0, -1, 1) ยท if(๐ต < 0, -1, 1)) = (if((๐ < 0 โง ๐ด < 0), -1, 1) ยท if((๐ < 0 โง ๐ต < 0), -1, 1))) |
81 | 72, 75, 80 | 3eqtr3d 2785 |
. 2
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ๐ < 0) โ if((๐ < 0 โง (๐ด ยท ๐ต) < 0), -1, 1) = (if((๐ < 0 โง ๐ด < 0), -1, 1) ยท if((๐ < 0 โง ๐ต < 0), -1, 1))) |
82 | | simpr 486 |
. . . . . 6
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ < 0) โ ยฌ ๐ < 0) |
83 | 82 | intnanrd 491 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ < 0) โ ยฌ (๐ < 0 โง (๐ด ยท ๐ต) < 0)) |
84 | 83 | iffalsed 4502 |
. . . 4
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ < 0) โ if((๐ < 0 โง (๐ด ยท ๐ต) < 0), -1, 1) = 1) |
85 | | 1t1e1 12322 |
. . . 4
โข (1
ยท 1) = 1 |
86 | 84, 85 | eqtr4di 2795 |
. . 3
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ < 0) โ if((๐ < 0 โง (๐ด ยท ๐ต) < 0), -1, 1) = (1 ยท
1)) |
87 | 82 | intnanrd 491 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ < 0) โ ยฌ (๐ < 0 โง ๐ด < 0)) |
88 | 87 | iffalsed 4502 |
. . . 4
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ < 0) โ if((๐ < 0 โง ๐ด < 0), -1, 1) = 1) |
89 | 82 | intnanrd 491 |
. . . . 5
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ < 0) โ ยฌ (๐ < 0 โง ๐ต < 0)) |
90 | 89 | iffalsed 4502 |
. . . 4
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ < 0) โ if((๐ < 0 โง ๐ต < 0), -1, 1) = 1) |
91 | 88, 90 | oveq12d 7380 |
. . 3
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ < 0) โ (if((๐ < 0 โง ๐ด < 0), -1, 1) ยท if((๐ < 0 โง ๐ต < 0), -1, 1)) = (1 ยท
1)) |
92 | 86, 91 | eqtr4d 2780 |
. 2
โข ((((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โง ยฌ ๐ < 0) โ if((๐ < 0 โง (๐ด ยท ๐ต) < 0), -1, 1) = (if((๐ < 0 โง ๐ด < 0), -1, 1) ยท if((๐ < 0 โง ๐ต < 0), -1, 1))) |
93 | 81, 92 | pm2.61dan 812 |
1
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ if((๐ < 0 โง (๐ด ยท ๐ต) < 0), -1, 1) = (if((๐ < 0 โง ๐ด < 0), -1, 1) ยท if((๐ < 0 โง ๐ต < 0), -1, 1))) |