Step | Hyp | Ref
| Expression |
1 | | dgrub.1 |
. . . 4
β’ π΄ = (coeffβπΉ) |
2 | | dgrub.2 |
. . . 4
β’ π = (degβπΉ) |
3 | 1, 2 | coeid2 25753 |
. . 3
β’ ((πΉ β (Polyβπ) β§ π β β) β (πΉβπ) = Ξ£π β (0...π)((π΄βπ) Β· (πβπ))) |
4 | 3 | 3adant2 1132 |
. 2
β’ ((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β (πΉβπ) = Ξ£π β (0...π)((π΄βπ) Β· (πβπ))) |
5 | | fzss2 13541 |
. . . 4
β’ (π β
(β€β₯βπ) β (0...π) β (0...π)) |
6 | 5 | 3ad2ant2 1135 |
. . 3
β’ ((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β (0...π) β (0...π)) |
7 | | elfznn0 13594 |
. . . 4
β’ (π β (0...π) β π β β0) |
8 | 1 | coef3 25746 |
. . . . . . 7
β’ (πΉ β (Polyβπ) β π΄:β0βΆβ) |
9 | 8 | 3ad2ant1 1134 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β π΄:β0βΆβ) |
10 | 9 | ffvelcdmda 7087 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β β0) β (π΄βπ) β β) |
11 | | expcl 14045 |
. . . . . 6
β’ ((π β β β§ π β β0)
β (πβπ) β
β) |
12 | 11 | 3ad2antl3 1188 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β β0) β (πβπ) β β) |
13 | 10, 12 | mulcld 11234 |
. . . 4
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β β0) β ((π΄βπ) Β· (πβπ)) β β) |
14 | 7, 13 | sylan2 594 |
. . 3
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β (0...π)) β ((π΄βπ) Β· (πβπ)) β β) |
15 | | eldifn 4128 |
. . . . . . 7
β’ (π β ((0...π) β (0...π)) β Β¬ π β (0...π)) |
16 | 15 | adantl 483 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β ((0...π) β (0...π))) β Β¬ π β (0...π)) |
17 | | simpl1 1192 |
. . . . . . . . 9
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β ((0...π) β (0...π))) β πΉ β (Polyβπ)) |
18 | | eldifi 4127 |
. . . . . . . . . . . 12
β’ (π β ((0...π) β (0...π)) β π β (0...π)) |
19 | | elfzuz 13497 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β
(β€β₯β0)) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((0...π) β (0...π)) β π β
(β€β₯β0)) |
21 | 20 | adantl 483 |
. . . . . . . . . 10
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β ((0...π) β (0...π))) β π β
(β€β₯β0)) |
22 | | nn0uz 12864 |
. . . . . . . . . 10
β’
β0 = (β€β₯β0) |
23 | 21, 22 | eleqtrrdi 2845 |
. . . . . . . . 9
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β ((0...π) β (0...π))) β π β β0) |
24 | 1, 2 | dgrub 25748 |
. . . . . . . . . 10
β’ ((πΉ β (Polyβπ) β§ π β β0 β§ (π΄βπ) β 0) β π β€ π) |
25 | 24 | 3expia 1122 |
. . . . . . . . 9
β’ ((πΉ β (Polyβπ) β§ π β β0) β ((π΄βπ) β 0 β π β€ π)) |
26 | 17, 23, 25 | syl2anc 585 |
. . . . . . . 8
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β ((0...π) β (0...π))) β ((π΄βπ) β 0 β π β€ π)) |
27 | | simpl2 1193 |
. . . . . . . . . 10
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β ((0...π) β (0...π))) β π β (β€β₯βπ)) |
28 | | eluzel2 12827 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β π β β€) |
29 | 27, 28 | syl 17 |
. . . . . . . . 9
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β ((0...π) β (0...π))) β π β β€) |
30 | | elfz5 13493 |
. . . . . . . . 9
β’ ((π β
(β€β₯β0) β§ π β β€) β (π β (0...π) β π β€ π)) |
31 | 21, 29, 30 | syl2anc 585 |
. . . . . . . 8
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β ((0...π) β (0...π))) β (π β (0...π) β π β€ π)) |
32 | 26, 31 | sylibrd 259 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β ((0...π) β (0...π))) β ((π΄βπ) β 0 β π β (0...π))) |
33 | 32 | necon1bd 2959 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β ((0...π) β (0...π))) β (Β¬ π β (0...π) β (π΄βπ) = 0)) |
34 | 16, 33 | mpd 15 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β ((0...π) β (0...π))) β (π΄βπ) = 0) |
35 | 34 | oveq1d 7424 |
. . . 4
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β ((0...π) β (0...π))) β ((π΄βπ) Β· (πβπ)) = (0 Β· (πβπ))) |
36 | | elfznn0 13594 |
. . . . . . 7
β’ (π β (0...π) β π β β0) |
37 | 18, 36 | syl 17 |
. . . . . 6
β’ (π β ((0...π) β (0...π)) β π β β0) |
38 | 37, 12 | sylan2 594 |
. . . . 5
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β ((0...π) β (0...π))) β (πβπ) β β) |
39 | 38 | mul02d 11412 |
. . . 4
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β ((0...π) β (0...π))) β (0 Β· (πβπ)) = 0) |
40 | 35, 39 | eqtrd 2773 |
. . 3
β’ (((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β§ π β ((0...π) β (0...π))) β ((π΄βπ) Β· (πβπ)) = 0) |
41 | | fzfid 13938 |
. . 3
β’ ((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β (0...π) β Fin) |
42 | 6, 14, 40, 41 | fsumss 15671 |
. 2
β’ ((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β Ξ£π β (0...π)((π΄βπ) Β· (πβπ)) = Ξ£π β (0...π)((π΄βπ) Β· (πβπ))) |
43 | 4, 42 | eqtrd 2773 |
1
β’ ((πΉ β (Polyβπ) β§ π β (β€β₯βπ) β§ π β β) β (πΉβπ) = Ξ£π β (0...π)((π΄βπ) Β· (πβπ))) |