Step |
Hyp |
Ref |
Expression |
0 |
|
cvts |
โข vts |
1 |
|
vl |
โข ๐ |
2 |
|
cc |
โข โ |
3 |
|
cmap |
โข โm |
4 |
|
cn |
โข โ |
5 |
2 4 3
|
co |
โข ( โ โm โ ) |
6 |
|
vn |
โข ๐ |
7 |
|
cn0 |
โข โ0 |
8 |
|
vx |
โข ๐ฅ |
9 |
|
va |
โข ๐ |
10 |
|
c1 |
โข 1 |
11 |
|
cfz |
โข ... |
12 |
6
|
cv |
โข ๐ |
13 |
10 12 11
|
co |
โข ( 1 ... ๐ ) |
14 |
1
|
cv |
โข ๐ |
15 |
9
|
cv |
โข ๐ |
16 |
15 14
|
cfv |
โข ( ๐ โ ๐ ) |
17 |
|
cmul |
โข ยท |
18 |
|
ce |
โข exp |
19 |
|
ci |
โข i |
20 |
|
c2 |
โข 2 |
21 |
|
cpi |
โข ฯ |
22 |
20 21 17
|
co |
โข ( 2 ยท ฯ ) |
23 |
19 22 17
|
co |
โข ( i ยท ( 2 ยท ฯ ) ) |
24 |
8
|
cv |
โข ๐ฅ |
25 |
15 24 17
|
co |
โข ( ๐ ยท ๐ฅ ) |
26 |
23 25 17
|
co |
โข ( ( i ยท ( 2 ยท ฯ ) ) ยท ( ๐ ยท ๐ฅ ) ) |
27 |
26 18
|
cfv |
โข ( exp โ ( ( i ยท ( 2 ยท ฯ ) ) ยท ( ๐ ยท ๐ฅ ) ) ) |
28 |
16 27 17
|
co |
โข ( ( ๐ โ ๐ ) ยท ( exp โ ( ( i ยท ( 2 ยท ฯ ) ) ยท ( ๐ ยท ๐ฅ ) ) ) ) |
29 |
13 28 9
|
csu |
โข ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( exp โ ( ( i ยท ( 2 ยท ฯ ) ) ยท ( ๐ ยท ๐ฅ ) ) ) ) |
30 |
8 2 29
|
cmpt |
โข ( ๐ฅ โ โ โฆ ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( exp โ ( ( i ยท ( 2 ยท ฯ ) ) ยท ( ๐ ยท ๐ฅ ) ) ) ) ) |
31 |
1 6 5 7 30
|
cmpo |
โข ( ๐ โ ( โ โm โ ) , ๐ โ โ0 โฆ ( ๐ฅ โ โ โฆ ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( exp โ ( ( i ยท ( 2 ยท ฯ ) ) ยท ( ๐ ยท ๐ฅ ) ) ) ) ) ) |
32 |
0 31
|
wceq |
โข vts = ( ๐ โ ( โ โm โ ) , ๐ โ โ0 โฆ ( ๐ฅ โ โ โฆ ฮฃ ๐ โ ( 1 ... ๐ ) ( ( ๐ โ ๐ ) ยท ( exp โ ( ( i ยท ( 2 ยท ฯ ) ) ยท ( ๐ ยท ๐ฅ ) ) ) ) ) ) |