Step | Hyp | Ref
| Expression |
1 | | plyssc 25584 |
. . . . 5
โข
(Polyโ๐)
โ (Polyโโ) |
2 | 1 | sseli 3944 |
. . . 4
โข (๐น โ (Polyโ๐) โ ๐น โ
(Polyโโ)) |
3 | | elply2 25580 |
. . . . . 6
โข (๐น โ (Polyโโ)
โ (โ โ โ โง โ๐ โ โ0 โ๐ โ ((โ โช {0})
โm โ0)((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) |
4 | 3 | simprbi 498 |
. . . . 5
โข (๐น โ (Polyโโ)
โ โ๐ โ
โ0 โ๐ โ ((โ โช {0})
โm โ0)((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) |
5 | | rexcom 3272 |
. . . . 5
โข
(โ๐ โ
โ0 โ๐ โ ((โ โช {0})
โm โ0)((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โ โ๐ โ ((โ โช {0})
โm โ0)โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) |
6 | 4, 5 | sylib 217 |
. . . 4
โข (๐น โ (Polyโโ)
โ โ๐ โ
((โ โช {0}) โm โ0)โ๐ โ โ0
((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) |
7 | 2, 6 | syl 17 |
. . 3
โข (๐น โ (Polyโ๐) โ โ๐ โ ((โ โช {0})
โm โ0)โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) |
8 | | 0cn 11155 |
. . . . . . 7
โข 0 โ
โ |
9 | | snssi 4772 |
. . . . . . 7
โข (0 โ
โ โ {0} โ โ) |
10 | 8, 9 | ax-mp 5 |
. . . . . 6
โข {0}
โ โ |
11 | | ssequn2 4147 |
. . . . . 6
โข ({0}
โ โ โ (โ โช {0}) = โ) |
12 | 10, 11 | mpbi 229 |
. . . . 5
โข (โ
โช {0}) = โ |
13 | 12 | oveq1i 7371 |
. . . 4
โข ((โ
โช {0}) โm โ0) = (โ
โm โ0) |
14 | 13 | rexeqi 3311 |
. . 3
โข
(โ๐ โ
((โ โช {0}) โm โ0)โ๐ โ โ0
((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โ โ๐ โ (โ โm
โ0)โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) |
15 | 7, 14 | sylib 217 |
. 2
โข (๐น โ (Polyโ๐) โ โ๐ โ (โ
โm โ0)โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) |
16 | | reeanv 3216 |
. . . 4
โข
(โ๐ โ
โ0 โ๐ โ โ0 (((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง ((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) โ (โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) |
17 | | simp1l 1198 |
. . . . . . 7
โข (((๐น โ (Polyโ๐) โง (๐ โ (โ โm
โ0) โง ๐ โ (โ โm
โ0))) โง (๐ โ โ0 โง ๐ โ โ0)
โง (((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง ((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) โ ๐น โ (Polyโ๐)) |
18 | | simp1rl 1239 |
. . . . . . 7
โข (((๐น โ (Polyโ๐) โง (๐ โ (โ โm
โ0) โง ๐ โ (โ โm
โ0))) โง (๐ โ โ0 โง ๐ โ โ0)
โง (((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง ((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) โ ๐ โ (โ โm
โ0)) |
19 | | simp1rr 1240 |
. . . . . . 7
โข (((๐น โ (Polyโ๐) โง (๐ โ (โ โm
โ0) โง ๐ โ (โ โm
โ0))) โง (๐ โ โ0 โง ๐ โ โ0)
โง (((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง ((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) โ ๐ โ (โ โm
โ0)) |
20 | | simp2l 1200 |
. . . . . . 7
โข (((๐น โ (Polyโ๐) โง (๐ โ (โ โm
โ0) โง ๐ โ (โ โm
โ0))) โง (๐ โ โ0 โง ๐ โ โ0)
โง (((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง ((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) โ ๐ โ โ0) |
21 | | simp2r 1201 |
. . . . . . 7
โข (((๐น โ (Polyโ๐) โง (๐ โ (โ โm
โ0) โง ๐ โ (โ โm
โ0))) โง (๐ โ โ0 โง ๐ โ โ0)
โง (((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง ((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) โ ๐ โ โ0) |
22 | | simp3ll 1245 |
. . . . . . 7
โข (((๐น โ (Polyโ๐) โง (๐ โ (โ โm
โ0) โง ๐ โ (โ โm
โ0))) โง (๐ โ โ0 โง ๐ โ โ0)
โง (((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง ((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) โ (๐ โ (โคโฅโ(๐ + 1))) = {0}) |
23 | | simp3rl 1247 |
. . . . . . 7
โข (((๐น โ (Polyโ๐) โง (๐ โ (โ โm
โ0) โง ๐ โ (โ โm
โ0))) โง (๐ โ โ0 โง ๐ โ โ0)
โง (((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง ((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) โ (๐ โ (โคโฅโ(๐ + 1))) = {0}) |
24 | | simp3lr 1246 |
. . . . . . . 8
โข (((๐น โ (Polyโ๐) โง (๐ โ (โ โm
โ0) โง ๐ โ (โ โm
โ0))) โง (๐ โ โ0 โง ๐ โ โ0)
โง (((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง ((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) โ ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) |
25 | | oveq1 7368 |
. . . . . . . . . . . 12
โข (๐ง = ๐ค โ (๐งโ๐) = (๐คโ๐)) |
26 | 25 | oveq2d 7377 |
. . . . . . . . . . 11
โข (๐ง = ๐ค โ ((๐โ๐) ยท (๐งโ๐)) = ((๐โ๐) ยท (๐คโ๐))) |
27 | 26 | sumeq2sdv 15597 |
. . . . . . . . . 10
โข (๐ง = ๐ค โ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)) = ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐คโ๐))) |
28 | | fveq2 6846 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
29 | | oveq2 7369 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐คโ๐) = (๐คโ๐)) |
30 | 28, 29 | oveq12d 7379 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐โ๐) ยท (๐คโ๐)) = ((๐โ๐) ยท (๐คโ๐))) |
31 | 30 | cbvsumv 15589 |
. . . . . . . . . 10
โข
ฮฃ๐ โ
(0...๐)((๐โ๐) ยท (๐คโ๐)) = ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐คโ๐)) |
32 | 27, 31 | eqtrdi 2789 |
. . . . . . . . 9
โข (๐ง = ๐ค โ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)) = ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐คโ๐))) |
33 | 32 | cbvmptv 5222 |
. . . . . . . 8
โข (๐ง โ โ โฆ
ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) = (๐ค โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐คโ๐))) |
34 | 24, 33 | eqtrdi 2789 |
. . . . . . 7
โข (((๐น โ (Polyโ๐) โง (๐ โ (โ โm
โ0) โง ๐ โ (โ โm
โ0))) โง (๐ โ โ0 โง ๐ โ โ0)
โง (((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง ((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) โ ๐น = (๐ค โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐คโ๐)))) |
35 | | simp3rr 1248 |
. . . . . . . 8
โข (((๐น โ (Polyโ๐) โง (๐ โ (โ โm
โ0) โง ๐ โ (โ โm
โ0))) โง (๐ โ โ0 โง ๐ โ โ0)
โง (((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง ((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) โ ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) |
36 | 25 | oveq2d 7377 |
. . . . . . . . . . 11
โข (๐ง = ๐ค โ ((๐โ๐) ยท (๐งโ๐)) = ((๐โ๐) ยท (๐คโ๐))) |
37 | 36 | sumeq2sdv 15597 |
. . . . . . . . . 10
โข (๐ง = ๐ค โ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)) = ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐คโ๐))) |
38 | | fveq2 6846 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
39 | 38, 29 | oveq12d 7379 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐โ๐) ยท (๐คโ๐)) = ((๐โ๐) ยท (๐คโ๐))) |
40 | 39 | cbvsumv 15589 |
. . . . . . . . . 10
โข
ฮฃ๐ โ
(0...๐)((๐โ๐) ยท (๐คโ๐)) = ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐คโ๐)) |
41 | 37, 40 | eqtrdi 2789 |
. . . . . . . . 9
โข (๐ง = ๐ค โ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)) = ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐คโ๐))) |
42 | 41 | cbvmptv 5222 |
. . . . . . . 8
โข (๐ง โ โ โฆ
ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) = (๐ค โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐คโ๐))) |
43 | 35, 42 | eqtrdi 2789 |
. . . . . . 7
โข (((๐น โ (Polyโ๐) โง (๐ โ (โ โm
โ0) โง ๐ โ (โ โm
โ0))) โง (๐ โ โ0 โง ๐ โ โ0)
โง (((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง ((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) โ ๐น = (๐ค โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐คโ๐)))) |
44 | 17, 18, 19, 20, 21, 22, 23, 34, 43 | coeeulem 25608 |
. . . . . 6
โข (((๐น โ (Polyโ๐) โง (๐ โ (โ โm
โ0) โง ๐ โ (โ โm
โ0))) โง (๐ โ โ0 โง ๐ โ โ0)
โง (((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง ((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) โ ๐ = ๐) |
45 | 44 | 3expia 1122 |
. . . . 5
โข (((๐น โ (Polyโ๐) โง (๐ โ (โ โm
โ0) โง ๐ โ (โ โm
โ0))) โง (๐ โ โ0 โง ๐ โ โ0))
โ ((((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง ((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) โ ๐ = ๐)) |
46 | 45 | rexlimdvva 3202 |
. . . 4
โข ((๐น โ (Polyโ๐) โง (๐ โ (โ โm
โ0) โง ๐ โ (โ โm
โ0))) โ (โ๐ โ โ0 โ๐ โ โ0
(((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง ((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) โ ๐ = ๐)) |
47 | 16, 46 | biimtrrid 242 |
. . 3
โข ((๐น โ (Polyโ๐) โง (๐ โ (โ โm
โ0) โง ๐ โ (โ โm
โ0))) โ ((โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) โ ๐ = ๐)) |
48 | 47 | ralrimivva 3194 |
. 2
โข (๐น โ (Polyโ๐) โ โ๐ โ (โ
โm โ0)โ๐ โ (โ โm
โ0)((โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) โ ๐ = ๐)) |
49 | | imaeq1 6012 |
. . . . . . 7
โข (๐ = ๐ โ (๐ โ (โคโฅโ(๐ + 1))) = (๐ โ (โคโฅโ(๐ + 1)))) |
50 | 49 | eqeq1d 2735 |
. . . . . 6
โข (๐ = ๐ โ ((๐ โ (โคโฅโ(๐ + 1))) = {0} โ (๐ โ
(โคโฅโ(๐ + 1))) = {0})) |
51 | | fveq1 6845 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
52 | 51 | oveq1d 7376 |
. . . . . . . . 9
โข (๐ = ๐ โ ((๐โ๐) ยท (๐งโ๐)) = ((๐โ๐) ยท (๐งโ๐))) |
53 | 52 | sumeq2sdv 15597 |
. . . . . . . 8
โข (๐ = ๐ โ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)) = ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) |
54 | 53 | mpteq2dv 5211 |
. . . . . . 7
โข (๐ = ๐ โ (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) |
55 | 54 | eqeq2d 2744 |
. . . . . 6
โข (๐ = ๐ โ (๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) โ ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) |
56 | 50, 55 | anbi12d 632 |
. . . . 5
โข (๐ = ๐ โ (((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โ ((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) |
57 | 56 | rexbidv 3172 |
. . . 4
โข (๐ = ๐ โ (โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โ โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) |
58 | | fvoveq1 7384 |
. . . . . . . 8
โข (๐ = ๐ โ (โคโฅโ(๐ + 1)) =
(โคโฅโ(๐ + 1))) |
59 | 58 | imaeq2d 6017 |
. . . . . . 7
โข (๐ = ๐ โ (๐ โ (โคโฅโ(๐ + 1))) = (๐ โ (โคโฅโ(๐ + 1)))) |
60 | 59 | eqeq1d 2735 |
. . . . . 6
โข (๐ = ๐ โ ((๐ โ (โคโฅโ(๐ + 1))) = {0} โ (๐ โ
(โคโฅโ(๐ + 1))) = {0})) |
61 | | oveq2 7369 |
. . . . . . . . 9
โข (๐ = ๐ โ (0...๐) = (0...๐)) |
62 | 61 | sumeq1d 15594 |
. . . . . . . 8
โข (๐ = ๐ โ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)) = ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) |
63 | 62 | mpteq2dv 5211 |
. . . . . . 7
โข (๐ = ๐ โ (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) |
64 | 63 | eqeq2d 2744 |
. . . . . 6
โข (๐ = ๐ โ (๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))) โ ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) |
65 | 60, 64 | anbi12d 632 |
. . . . 5
โข (๐ = ๐ โ (((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โ ((๐ โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) |
66 | 65 | cbvrexvw 3225 |
. . . 4
โข
(โ๐ โ
โ0 ((๐
โ (โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โ โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) |
67 | 57, 66 | bitrdi 287 |
. . 3
โข (๐ = ๐ โ (โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โ โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))))) |
68 | 67 | reu4 3693 |
. 2
โข
(โ!๐ โ
(โ โm โ0)โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โ (โ๐ โ (โ โm
โ0)โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง โ๐ โ (โ โm
โ0)โ๐ โ (โ โm
โ0)((โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐)))) โง โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) โ ๐ = ๐))) |
69 | 15, 48, 68 | sylanbrc 584 |
1
โข (๐น โ (Polyโ๐) โ โ!๐ โ (โ
โm โ0)โ๐ โ โ0 ((๐ โ
(โคโฅโ(๐ + 1))) = {0} โง ๐น = (๐ง โ โ โฆ ฮฃ๐ โ (0...๐)((๐โ๐) ยท (๐งโ๐))))) |