Step | Hyp | Ref
| Expression |
1 | | 1cubr.r |
. . . . 5
โข ๐
= {1, ((-1 + (i ยท
(โโ3))) / 2), ((-1 โ (i ยท (โโ3))) /
2)} |
2 | | ax-1cn 11116 |
. . . . . . 7
โข 1 โ
โ |
3 | | neg1cn 12274 |
. . . . . . . . 9
โข -1 โ
โ |
4 | | ax-icn 11117 |
. . . . . . . . . 10
โข i โ
โ |
5 | | 3cn 12241 |
. . . . . . . . . . 11
โข 3 โ
โ |
6 | | sqrtcl 15253 |
. . . . . . . . . . 11
โข (3 โ
โ โ (โโ3) โ โ) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . . 10
โข
(โโ3) โ โ |
8 | 4, 7 | mulcli 11169 |
. . . . . . . . 9
โข (i
ยท (โโ3)) โ โ |
9 | 3, 8 | addcli 11168 |
. . . . . . . 8
โข (-1 + (i
ยท (โโ3))) โ โ |
10 | | halfcl 12385 |
. . . . . . . 8
โข ((-1 + (i
ยท (โโ3))) โ โ โ ((-1 + (i ยท
(โโ3))) / 2) โ โ) |
11 | 9, 10 | ax-mp 5 |
. . . . . . 7
โข ((-1 + (i
ยท (โโ3))) / 2) โ โ |
12 | 3, 8 | subcli 11484 |
. . . . . . . 8
โข (-1
โ (i ยท (โโ3))) โ โ |
13 | | halfcl 12385 |
. . . . . . . 8
โข ((-1
โ (i ยท (โโ3))) โ โ โ ((-1 โ (i
ยท (โโ3))) / 2) โ โ) |
14 | 12, 13 | ax-mp 5 |
. . . . . . 7
โข ((-1
โ (i ยท (โโ3))) / 2) โ โ |
15 | 2, 11, 14 | 3pm3.2i 1340 |
. . . . . 6
โข (1 โ
โ โง ((-1 + (i ยท (โโ3))) / 2) โ โ โง
((-1 โ (i ยท (โโ3))) / 2) โ
โ) |
16 | 2 | elexi 3467 |
. . . . . . 7
โข 1 โ
V |
17 | | ovex 7395 |
. . . . . . 7
โข ((-1 + (i
ยท (โโ3))) / 2) โ V |
18 | | ovex 7395 |
. . . . . . 7
โข ((-1
โ (i ยท (โโ3))) / 2) โ V |
19 | 16, 17, 18 | tpss 4800 |
. . . . . 6
โข ((1
โ โ โง ((-1 + (i ยท (โโ3))) / 2) โ โ
โง ((-1 โ (i ยท (โโ3))) / 2) โ โ) โ
{1, ((-1 + (i ยท (โโ3))) / 2), ((-1 โ (i ยท
(โโ3))) / 2)} โ โ) |
20 | 15, 19 | mpbi 229 |
. . . . 5
โข {1, ((-1
+ (i ยท (โโ3))) / 2), ((-1 โ (i ยท
(โโ3))) / 2)} โ โ |
21 | 1, 20 | eqsstri 3983 |
. . . 4
โข ๐
โ
โ |
22 | 21 | sseli 3945 |
. . 3
โข (๐ด โ ๐
โ ๐ด โ โ) |
23 | 22 | pm4.71ri 562 |
. 2
โข (๐ด โ ๐
โ (๐ด โ โ โง ๐ด โ ๐
)) |
24 | | 3nn 12239 |
. . . . 5
โข 3 โ
โ |
25 | | cxpeq 26126 |
. . . . 5
โข ((๐ด โ โ โง 3 โ
โ โง 1 โ โ) โ ((๐ดโ3) = 1 โ โ๐ โ (0...(3 โ 1))๐ด =
((1โ๐(1 / 3)) ยท ((-1โ๐(2
/ 3))โ๐)))) |
26 | 24, 2, 25 | mp3an23 1454 |
. . . 4
โข (๐ด โ โ โ ((๐ดโ3) = 1 โ โ๐ โ (0...(3 โ 1))๐ด =
((1โ๐(1 / 3)) ยท ((-1โ๐(2
/ 3))โ๐)))) |
27 | | eltpg 4651 |
. . . . 5
โข (๐ด โ โ โ (๐ด โ {1, ((-1 + (i ยท
(โโ3))) / 2), ((-1 โ (i ยท (โโ3))) / 2)}
โ (๐ด = 1 โจ ๐ด = ((-1 + (i ยท
(โโ3))) / 2) โจ ๐ด = ((-1 โ (i ยท
(โโ3))) / 2)))) |
28 | 1 | eleq2i 2830 |
. . . . 5
โข (๐ด โ ๐
โ ๐ด โ {1, ((-1 + (i ยท
(โโ3))) / 2), ((-1 โ (i ยท (โโ3))) /
2)}) |
29 | | 3m1e2 12288 |
. . . . . . . . . 10
โข (3
โ 1) = 2 |
30 | | 2cn 12235 |
. . . . . . . . . . 11
โข 2 โ
โ |
31 | 30 | addid2i 11350 |
. . . . . . . . . 10
โข (0 + 2) =
2 |
32 | 29, 31 | eqtr4i 2768 |
. . . . . . . . 9
โข (3
โ 1) = (0 + 2) |
33 | 32 | oveq2i 7373 |
. . . . . . . 8
โข (0...(3
โ 1)) = (0...(0 + 2)) |
34 | | 0z 12517 |
. . . . . . . . 9
โข 0 โ
โค |
35 | | fztp 13504 |
. . . . . . . . 9
โข (0 โ
โค โ (0...(0 + 2)) = {0, (0 + 1), (0 + 2)}) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . 8
โข (0...(0 +
2)) = {0, (0 + 1), (0 + 2)} |
37 | 33, 36 | eqtri 2765 |
. . . . . . 7
โข (0...(3
โ 1)) = {0, (0 + 1), (0 + 2)} |
38 | 37 | rexeqi 3315 |
. . . . . 6
โข
(โ๐ โ
(0...(3 โ 1))๐ด =
((1โ๐(1 / 3)) ยท ((-1โ๐(2
/ 3))โ๐)) โ
โ๐ โ {0, (0 +
1), (0 + 2)}๐ด =
((1โ๐(1 / 3)) ยท ((-1โ๐(2
/ 3))โ๐))) |
39 | | 3ne0 12266 |
. . . . . . . . . . 11
โข 3 โ
0 |
40 | 5, 39 | reccli 11892 |
. . . . . . . . . 10
โข (1 / 3)
โ โ |
41 | | 1cxp 26043 |
. . . . . . . . . 10
โข ((1 / 3)
โ โ โ (1โ๐(1 / 3)) =
1) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . . 9
โข
(1โ๐(1 / 3)) = 1 |
43 | 42 | oveq1i 7372 |
. . . . . . . 8
โข
((1โ๐(1 / 3)) ยท
((-1โ๐(2 / 3))โ๐)) = (1 ยท
((-1โ๐(2 / 3))โ๐)) |
44 | 43 | eqeq2i 2750 |
. . . . . . 7
โข (๐ด =
((1โ๐(1 / 3)) ยท ((-1โ๐(2
/ 3))โ๐)) โ ๐ด = (1 ยท
((-1โ๐(2 / 3))โ๐))) |
45 | 44 | rexbii 3098 |
. . . . . 6
โข
(โ๐ โ {0,
(0 + 1), (0 + 2)}๐ด =
((1โ๐(1 / 3)) ยท ((-1โ๐(2
/ 3))โ๐)) โ
โ๐ โ {0, (0 +
1), (0 + 2)}๐ด = (1 ยท
((-1โ๐(2 / 3))โ๐))) |
46 | 34 | elexi 3467 |
. . . . . . 7
โข 0 โ
V |
47 | | ovex 7395 |
. . . . . . 7
โข (0 + 1)
โ V |
48 | | ovex 7395 |
. . . . . . 7
โข (0 + 2)
โ V |
49 | | oveq2 7370 |
. . . . . . . . . . 11
โข (๐ = 0 โ
((-1โ๐(2 / 3))โ๐) = ((-1โ๐(2 /
3))โ0)) |
50 | 30, 5, 39 | divcli 11904 |
. . . . . . . . . . . . 13
โข (2 / 3)
โ โ |
51 | | cxpcl 26045 |
. . . . . . . . . . . . 13
โข ((-1
โ โ โง (2 / 3) โ โ) โ
(-1โ๐(2 / 3)) โ โ) |
52 | 3, 50, 51 | mp2an 691 |
. . . . . . . . . . . 12
โข
(-1โ๐(2 / 3)) โ โ |
53 | | exp0 13978 |
. . . . . . . . . . . 12
โข
((-1โ๐(2 / 3)) โ โ โ
((-1โ๐(2 / 3))โ0) = 1) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . 11
โข
((-1โ๐(2 / 3))โ0) = 1 |
55 | 49, 54 | eqtrdi 2793 |
. . . . . . . . . 10
โข (๐ = 0 โ
((-1โ๐(2 / 3))โ๐) = 1) |
56 | 55 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ = 0 โ (1 ยท
((-1โ๐(2 / 3))โ๐)) = (1 ยท 1)) |
57 | | 1t1e1 12322 |
. . . . . . . . 9
โข (1
ยท 1) = 1 |
58 | 56, 57 | eqtrdi 2793 |
. . . . . . . 8
โข (๐ = 0 โ (1 ยท
((-1โ๐(2 / 3))โ๐)) = 1) |
59 | 58 | eqeq2d 2748 |
. . . . . . 7
โข (๐ = 0 โ (๐ด = (1 ยท
((-1โ๐(2 / 3))โ๐)) โ ๐ด = 1)) |
60 | | id 22 |
. . . . . . . . . . . . 13
โข (๐ = (0 + 1) โ ๐ = (0 + 1)) |
61 | 2 | addid2i 11350 |
. . . . . . . . . . . . 13
โข (0 + 1) =
1 |
62 | 60, 61 | eqtrdi 2793 |
. . . . . . . . . . . 12
โข (๐ = (0 + 1) โ ๐ = 1) |
63 | 62 | oveq2d 7378 |
. . . . . . . . . . 11
โข (๐ = (0 + 1) โ
((-1โ๐(2 / 3))โ๐) = ((-1โ๐(2 /
3))โ1)) |
64 | | exp1 13980 |
. . . . . . . . . . . 12
โข
((-1โ๐(2 / 3)) โ โ โ
((-1โ๐(2 / 3))โ1) =
(-1โ๐(2 / 3))) |
65 | 52, 64 | ax-mp 5 |
. . . . . . . . . . 11
โข
((-1โ๐(2 / 3))โ1) =
(-1โ๐(2 / 3)) |
66 | 63, 65 | eqtrdi 2793 |
. . . . . . . . . 10
โข (๐ = (0 + 1) โ
((-1โ๐(2 / 3))โ๐) = (-1โ๐(2 /
3))) |
67 | 66 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ = (0 + 1) โ (1 ยท
((-1โ๐(2 / 3))โ๐)) = (1 ยท
(-1โ๐(2 / 3)))) |
68 | 52 | mulid2i 11167 |
. . . . . . . . . 10
โข (1
ยท (-1โ๐(2 / 3))) =
(-1โ๐(2 / 3)) |
69 | | 1cubrlem 26207 |
. . . . . . . . . . 11
โข
((-1โ๐(2 / 3)) = ((-1 + (i ยท
(โโ3))) / 2) โง ((-1โ๐(2 / 3))โ2) =
((-1 โ (i ยท (โโ3))) / 2)) |
70 | 69 | simpli 485 |
. . . . . . . . . 10
โข
(-1โ๐(2 / 3)) = ((-1 + (i ยท
(โโ3))) / 2) |
71 | 68, 70 | eqtri 2765 |
. . . . . . . . 9
โข (1
ยท (-1โ๐(2 / 3))) = ((-1 + (i ยท
(โโ3))) / 2) |
72 | 67, 71 | eqtrdi 2793 |
. . . . . . . 8
โข (๐ = (0 + 1) โ (1 ยท
((-1โ๐(2 / 3))โ๐)) = ((-1 + (i ยท (โโ3))) /
2)) |
73 | 72 | eqeq2d 2748 |
. . . . . . 7
โข (๐ = (0 + 1) โ (๐ด = (1 ยท
((-1โ๐(2 / 3))โ๐)) โ ๐ด = ((-1 + (i ยท (โโ3))) /
2))) |
74 | | id 22 |
. . . . . . . . . . . 12
โข (๐ = (0 + 2) โ ๐ = (0 + 2)) |
75 | 74, 31 | eqtrdi 2793 |
. . . . . . . . . . 11
โข (๐ = (0 + 2) โ ๐ = 2) |
76 | 75 | oveq2d 7378 |
. . . . . . . . . 10
โข (๐ = (0 + 2) โ
((-1โ๐(2 / 3))โ๐) = ((-1โ๐(2 /
3))โ2)) |
77 | 76 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ = (0 + 2) โ (1 ยท
((-1โ๐(2 / 3))โ๐)) = (1 ยท
((-1โ๐(2 / 3))โ2))) |
78 | 52 | sqcli 14092 |
. . . . . . . . . . 11
โข
((-1โ๐(2 / 3))โ2) โ
โ |
79 | 78 | mulid2i 11167 |
. . . . . . . . . 10
โข (1
ยท ((-1โ๐(2 / 3))โ2)) =
((-1โ๐(2 / 3))โ2) |
80 | 69 | simpri 487 |
. . . . . . . . . 10
โข
((-1โ๐(2 / 3))โ2) = ((-1 โ (i
ยท (โโ3))) / 2) |
81 | 79, 80 | eqtri 2765 |
. . . . . . . . 9
โข (1
ยท ((-1โ๐(2 / 3))โ2)) = ((-1 โ (i
ยท (โโ3))) / 2) |
82 | 77, 81 | eqtrdi 2793 |
. . . . . . . 8
โข (๐ = (0 + 2) โ (1 ยท
((-1โ๐(2 / 3))โ๐)) = ((-1 โ (i ยท
(โโ3))) / 2)) |
83 | 82 | eqeq2d 2748 |
. . . . . . 7
โข (๐ = (0 + 2) โ (๐ด = (1 ยท
((-1โ๐(2 / 3))โ๐)) โ ๐ด = ((-1 โ (i ยท
(โโ3))) / 2))) |
84 | 46, 47, 48, 59, 73, 83 | rextp 4672 |
. . . . . 6
โข
(โ๐ โ {0,
(0 + 1), (0 + 2)}๐ด = (1
ยท ((-1โ๐(2 / 3))โ๐)) โ (๐ด = 1 โจ ๐ด = ((-1 + (i ยท (โโ3))) /
2) โจ ๐ด = ((-1 โ (i
ยท (โโ3))) / 2))) |
85 | 38, 45, 84 | 3bitri 297 |
. . . . 5
โข
(โ๐ โ
(0...(3 โ 1))๐ด =
((1โ๐(1 / 3)) ยท ((-1โ๐(2
/ 3))โ๐)) โ
(๐ด = 1 โจ ๐ด = ((-1 + (i ยท
(โโ3))) / 2) โจ ๐ด = ((-1 โ (i ยท
(โโ3))) / 2))) |
86 | 27, 28, 85 | 3bitr4g 314 |
. . . 4
โข (๐ด โ โ โ (๐ด โ ๐
โ โ๐ โ (0...(3 โ 1))๐ด = ((1โ๐(1 / 3))
ยท ((-1โ๐(2 / 3))โ๐)))) |
87 | 26, 86 | bitr4d 282 |
. . 3
โข (๐ด โ โ โ ((๐ดโ3) = 1 โ ๐ด โ ๐
)) |
88 | 87 | pm5.32i 576 |
. 2
โข ((๐ด โ โ โง (๐ดโ3) = 1) โ (๐ด โ โ โง ๐ด โ ๐
)) |
89 | 23, 88 | bitr4i 278 |
1
โข (๐ด โ ๐
โ (๐ด โ โ โง (๐ดโ3) = 1)) |