Step | Hyp | Ref
| Expression |
1 | | elply2 25710 |
. . . 4
β’ (πΉ β (Polyβπ) β (π β β β§ βπ β β0
βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))))) |
2 | 1 | simprbi 498 |
. . 3
β’ (πΉ β (Polyβπ) β βπ β β0
βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) |
3 | | simplrr 777 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β π β ((π βͺ {0}) βm
β0)) |
4 | | simpll 766 |
. . . . . . . . . . 11
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β πΉ β (Polyβπ)) |
5 | | plybss 25708 |
. . . . . . . . . . 11
β’ (πΉ β (Polyβπ) β π β β) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β π β β) |
7 | | 0cnd 11207 |
. . . . . . . . . . 11
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β 0 β
β) |
8 | 7 | snssd 4813 |
. . . . . . . . . 10
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β {0} β
β) |
9 | 6, 8 | unssd 4187 |
. . . . . . . . 9
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β (π βͺ {0}) β
β) |
10 | | cnex 11191 |
. . . . . . . . 9
β’ β
β V |
11 | | ssexg 5324 |
. . . . . . . . 9
β’ (((π βͺ {0}) β β
β§ β β V) β (π βͺ {0}) β V) |
12 | 9, 10, 11 | sylancl 587 |
. . . . . . . 8
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β (π βͺ {0}) β V) |
13 | | nn0ex 12478 |
. . . . . . . 8
β’
β0 β V |
14 | | elmapg 8833 |
. . . . . . . 8
β’ (((π βͺ {0}) β V β§
β0 β V) β (π β ((π βͺ {0}) βm
β0) β π:β0βΆ(π βͺ {0}))) |
15 | 12, 13, 14 | sylancl 587 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β (π β ((π βͺ {0}) βm
β0) β π:β0βΆ(π βͺ {0}))) |
16 | 3, 15 | mpbid 231 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β π:β0βΆ(π βͺ {0})) |
17 | | dgrval.1 |
. . . . . . . 8
β’ π΄ = (coeffβπΉ) |
18 | | simplrl 776 |
. . . . . . . . 9
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β π β β0) |
19 | 16, 9 | fssd 6736 |
. . . . . . . . 9
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β π:β0βΆβ) |
20 | | simprl 770 |
. . . . . . . . 9
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β (π β (β€β₯β(π + 1))) = {0}) |
21 | | simprr 772 |
. . . . . . . . 9
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) |
22 | 4, 18, 19, 20, 21 | coeeq 25741 |
. . . . . . . 8
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β (coeffβπΉ) = π) |
23 | 17, 22 | eqtr2id 2786 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β π = π΄) |
24 | 23 | feq1d 6703 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β (π:β0βΆ(π βͺ {0}) β π΄:β0βΆ(π βͺ {0}))) |
25 | 16, 24 | mpbid 231 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β π΄:β0βΆ(π βͺ {0})) |
26 | 25 | ex 414 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β (((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) β π΄:β0βΆ(π βͺ {0}))) |
27 | 26 | rexlimdvva 3212 |
. . 3
β’ (πΉ β (Polyβπ) β (βπ β β0
βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) β π΄:β0βΆ(π βͺ {0}))) |
28 | 2, 27 | mpd 15 |
. 2
β’ (πΉ β (Polyβπ) β π΄:β0βΆ(π βͺ {0})) |
29 | | nn0ssz 12581 |
. . 3
β’
β0 β β€ |
30 | | ffn 6718 |
. . . . . . . . . . . . . 14
β’ (π:β0βΆβ β
π Fn
β0) |
31 | | elpreima 7060 |
. . . . . . . . . . . . . 14
β’ (π Fn β0 β
(π₯ β (β‘π β (β β {0})) β (π₯ β β0
β§ (πβπ₯) β (β β
{0})))) |
32 | 19, 30, 31 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β (π₯ β (β‘π β (β β {0})) β (π₯ β β0
β§ (πβπ₯) β (β β
{0})))) |
33 | 32 | biimpa 478 |
. . . . . . . . . . . 12
β’ ((((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β§ π₯ β (β‘π β (β β {0}))) β
(π₯ β
β0 β§ (πβπ₯) β (β β
{0}))) |
34 | | eldifsni 4794 |
. . . . . . . . . . . 12
β’ ((πβπ₯) β (β β {0}) β (πβπ₯) β 0) |
35 | 33, 34 | simpl2im 505 |
. . . . . . . . . . 11
β’ ((((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β§ π₯ β (β‘π β (β β {0}))) β
(πβπ₯) β 0) |
36 | 33 | simpld 496 |
. . . . . . . . . . . 12
β’ ((((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β§ π₯ β (β‘π β (β β {0}))) β π₯ β
β0) |
37 | | plyco0 25706 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ π:β0βΆβ) β
((π β
(β€β₯β(π + 1))) = {0} β βπ₯ β β0
((πβπ₯) β 0 β π₯ β€ π))) |
38 | 18, 19, 37 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β ((π β (β€β₯β(π + 1))) = {0} β
βπ₯ β
β0 ((πβπ₯) β 0 β π₯ β€ π))) |
39 | 20, 38 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β βπ₯ β β0 ((πβπ₯) β 0 β π₯ β€ π)) |
40 | 39 | r19.21bi 3249 |
. . . . . . . . . . . 12
β’ ((((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β§ π₯ β β0) β ((πβπ₯) β 0 β π₯ β€ π)) |
41 | 36, 40 | syldan 592 |
. . . . . . . . . . 11
β’ ((((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β§ π₯ β (β‘π β (β β {0}))) β
((πβπ₯) β 0 β π₯ β€ π)) |
42 | 35, 41 | mpd 15 |
. . . . . . . . . 10
β’ ((((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β§ π₯ β (β‘π β (β β {0}))) β π₯ β€ π) |
43 | 42 | ralrimiva 3147 |
. . . . . . . . 9
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β βπ₯ β (β‘π β (β β {0}))π₯ β€ π) |
44 | 23 | cnveqd 5876 |
. . . . . . . . . . 11
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β β‘π = β‘π΄) |
45 | 44 | imaeq1d 6059 |
. . . . . . . . . 10
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β (β‘π β (β β {0})) = (β‘π΄ β (β β
{0}))) |
46 | 45 | raleqdv 3326 |
. . . . . . . . 9
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β (βπ₯ β (β‘π β (β β {0}))π₯ β€ π β βπ₯ β (β‘π΄ β (β β {0}))π₯ β€ π)) |
47 | 43, 46 | mpbid 231 |
. . . . . . . 8
β’ (((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ ((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β βπ₯ β (β‘π΄ β (β β {0}))π₯ β€ π) |
48 | 47 | ex 414 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β (((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) β βπ₯ β (β‘π΄ β (β β {0}))π₯ β€ π)) |
49 | 48 | expr 458 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ π β β0) β (π β ((π βͺ {0}) βm
β0) β (((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) β βπ₯ β (β‘π΄ β (β β {0}))π₯ β€ π))) |
50 | 49 | rexlimdv 3154 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ π β β0) β
(βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) β βπ₯ β (β‘π΄ β (β β {0}))π₯ β€ π)) |
51 | 50 | reximdva 3169 |
. . . 4
β’ (πΉ β (Polyβπ) β (βπ β β0
βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) β βπ β β0 βπ₯ β (β‘π΄ β (β β {0}))π₯ β€ π)) |
52 | 2, 51 | mpd 15 |
. . 3
β’ (πΉ β (Polyβπ) β βπ β β0
βπ₯ β (β‘π΄ β (β β {0}))π₯ β€ π) |
53 | | ssrexv 4052 |
. . 3
β’
(β0 β β€ β (βπ β β0 βπ₯ β (β‘π΄ β (β β {0}))π₯ β€ π β βπ β β€ βπ₯ β (β‘π΄ β (β β {0}))π₯ β€ π)) |
54 | 29, 52, 53 | mpsyl 68 |
. 2
β’ (πΉ β (Polyβπ) β βπ β β€ βπ₯ β (β‘π΄ β (β β {0}))π₯ β€ π) |
55 | 28, 54 | jca 513 |
1
β’ (πΉ β (Polyβπ) β (π΄:β0βΆ(π βͺ {0}) β§ βπ β β€ βπ₯ β (β‘π΄ β (β β {0}))π₯ β€ π)) |