Step | Hyp | Ref
| Expression |
1 | | ccoe 25691 |
. 2
class
coeff |
2 | | vf |
. . 3
setvar ๐ |
3 | | cc 11104 |
. . . 4
class
โ |
4 | | cply 25689 |
. . . 4
class
Poly |
5 | 3, 4 | cfv 6540 |
. . 3
class
(Polyโโ) |
6 | | va |
. . . . . . . . 9
setvar ๐ |
7 | 6 | cv 1540 |
. . . . . . . 8
class ๐ |
8 | | vn |
. . . . . . . . . . 11
setvar ๐ |
9 | 8 | cv 1540 |
. . . . . . . . . 10
class ๐ |
10 | | c1 11107 |
. . . . . . . . . 10
class
1 |
11 | | caddc 11109 |
. . . . . . . . . 10
class
+ |
12 | 9, 10, 11 | co 7405 |
. . . . . . . . 9
class (๐ + 1) |
13 | | cuz 12818 |
. . . . . . . . 9
class
โคโฅ |
14 | 12, 13 | cfv 6540 |
. . . . . . . 8
class
(โคโฅโ(๐ + 1)) |
15 | 7, 14 | cima 5678 |
. . . . . . 7
class (๐ โ
(โคโฅโ(๐ + 1))) |
16 | | cc0 11106 |
. . . . . . . 8
class
0 |
17 | 16 | csn 4627 |
. . . . . . 7
class
{0} |
18 | 15, 17 | wceq 1541 |
. . . . . 6
wff (๐ โ
(โคโฅโ(๐ + 1))) = {0} |
19 | 2 | cv 1540 |
. . . . . . 7
class ๐ |
20 | | vz |
. . . . . . . 8
setvar ๐ง |
21 | | cfz 13480 |
. . . . . . . . . 10
class
... |
22 | 16, 9, 21 | co 7405 |
. . . . . . . . 9
class
(0...๐) |
23 | | vk |
. . . . . . . . . . . 12
setvar ๐ |
24 | 23 | cv 1540 |
. . . . . . . . . . 11
class ๐ |
25 | 24, 7 | cfv 6540 |
. . . . . . . . . 10
class (๐โ๐) |
26 | 20 | cv 1540 |
. . . . . . . . . . 11
class ๐ง |
27 | | cexp 14023 |
. . . . . . . . . . 11
class
โ |
28 | 26, 24, 27 | co 7405 |
. . . . . . . . . 10
class (๐งโ๐) |
29 | | cmul 11111 |
. . . . . . . . . 10
class
ยท |
30 | 25, 28, 29 | co 7405 |
. . . . . . . . 9
class ((๐โ๐) ยท (๐งโ๐)) |
31 | 22, 30, 23 | csu 15628 |
. . . . . . . 8
class
ฮฃ๐ โ
(0...๐)((๐โ๐) ยท (๐งโ๐)) |
32 | 20, 3, 31 | cmpt 5230 |
. . . . . . 7
class (๐ง โ โ โฆ
ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) |
33 | 19, 32 | wceq 1541 |
. . . . . 6
wff ๐ = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) |
34 | 18, 33 | wa 396 |
. . . . 5
wff ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐ = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) |
35 | | cn0 12468 |
. . . . 5
class
โ0 |
36 | 34, 8, 35 | wrex 3070 |
. . . 4
wff
โ๐ โ
โ0 ((๐
โ (โคโฅโ(๐ + 1))) = {0} โง ๐ = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) |
37 | | cmap 8816 |
. . . . 5
class
โm |
38 | 3, 35, 37 | co 7405 |
. . . 4
class (โ
โm โ0) |
39 | 36, 6, 38 | crio 7360 |
. . 3
class
(โฉ๐
โ (โ โm โ0)โ๐ โ โ0
((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐ = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) |
40 | 2, 5, 39 | cmpt 5230 |
. 2
class (๐ โ (Polyโโ)
โฆ (โฉ๐
โ (โ โm โ0)โ๐ โ โ0
((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐ = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) |
41 | 1, 40 | wceq 1541 |
1
wff coeff =
(๐ โ
(Polyโโ) โฆ (โฉ๐ โ (โ โm
โ0)โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐ = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) |