Step | Hyp | Ref
| Expression |
1 | | coeval 25737 |
. . 3
โข (๐น โ (Polyโ๐) โ (coeffโ๐น) = (โฉ๐ โ (โ
โm โ0)โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) |
2 | | coeeu 25739 |
. . . 4
โข (๐น โ (Polyโ๐) โ โ!๐ โ (โ
โm โ0)โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) |
3 | | riotacl2 7382 |
. . . 4
โข
(โ!๐ โ
(โ โm โ0)โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โ (โฉ๐ โ (โ โm
โ0)โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) โ {๐ โ (โ โm
โ0) โฃ โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))}) |
4 | 2, 3 | syl 17 |
. . 3
โข (๐น โ (Polyโ๐) โ (โฉ๐ โ (โ
โm โ0)โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) โ {๐ โ (โ โm
โ0) โฃ โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))}) |
5 | 1, 4 | eqeltrd 2834 |
. 2
โข (๐น โ (Polyโ๐) โ (coeffโ๐น) โ {๐ โ (โ โm
โ0) โฃ โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))}) |
6 | | imaeq1 6055 |
. . . . . 6
โข (๐ = (coeffโ๐น) โ (๐ โ (โคโฅโ(๐ + 1))) = ((coeffโ๐น) โ
(โคโฅโ(๐ + 1)))) |
7 | 6 | eqeq1d 2735 |
. . . . 5
โข (๐ = (coeffโ๐น) โ ((๐ โ (โคโฅโ(๐ + 1))) = {0} โ
((coeffโ๐น) โ
(โคโฅโ(๐ + 1))) = {0})) |
8 | | fveq1 6891 |
. . . . . . . . 9
โข (๐ = (coeffโ๐น) โ (๐โ๐) = ((coeffโ๐น)โ๐)) |
9 | 8 | oveq1d 7424 |
. . . . . . . 8
โข (๐ = (coeffโ๐น) โ ((๐โ๐) ยท (๐งโ๐)) = (((coeffโ๐น)โ๐) ยท (๐งโ๐))) |
10 | 9 | sumeq2sdv 15650 |
. . . . . . 7
โข (๐ = (coeffโ๐น) โ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)) = ฮฃ๐ โ (0...๐)(((coeffโ๐น)โ๐) ยท (๐งโ๐))) |
11 | 10 | mpteq2dv 5251 |
. . . . . 6
โข (๐ = (coeffโ๐น) โ (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)(((coeffโ๐น)โ๐) ยท (๐งโ๐)))) |
12 | 11 | eqeq2d 2744 |
. . . . 5
โข (๐ = (coeffโ๐น) โ (๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) โ ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)(((coeffโ๐น)โ๐) ยท (๐งโ๐))))) |
13 | 7, 12 | anbi12d 632 |
. . . 4
โข (๐ = (coeffโ๐น) โ (((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โ (((coeffโ๐น) โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)(((coeffโ๐น)โ๐) ยท (๐งโ๐)))))) |
14 | 13 | rexbidv 3179 |
. . 3
โข (๐ = (coeffโ๐น) โ (โ๐ โ โ0
((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โ โ๐ โ โ0
(((coeffโ๐น) โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)(((coeffโ๐น)โ๐) ยท (๐งโ๐)))))) |
15 | 14 | elrab 3684 |
. 2
โข
((coeffโ๐น)
โ {๐ โ (โ
โm โ0) โฃ โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))} โ ((coeffโ๐น) โ (โ โm
โ0) โง โ๐ โ โ0
(((coeffโ๐น) โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)(((coeffโ๐น)โ๐) ยท (๐งโ๐)))))) |
16 | 5, 15 | sylib 217 |
1
โข (๐น โ (Polyโ๐) โ ((coeffโ๐น) โ (โ
โm โ0) โง โ๐ โ โ0
(((coeffโ๐น) โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)(((coeffโ๐น)โ๐) ยท (๐งโ๐)))))) |