Step | Hyp | Ref
| Expression |
1 | | aalioulem1.a |
. . . . 5
β’ (π β πΉ β
(Polyββ€)) |
2 | | aalioulem1.b |
. . . . . . 7
β’ (π β π β β€) |
3 | 2 | zcnd 12615 |
. . . . . 6
β’ (π β π β β) |
4 | | aalioulem1.c |
. . . . . . 7
β’ (π β π β β) |
5 | 4 | nncnd 12176 |
. . . . . 6
β’ (π β π β β) |
6 | 4 | nnne0d 12210 |
. . . . . 6
β’ (π β π β 0) |
7 | 3, 5, 6 | divcld 11938 |
. . . . 5
β’ (π β (π / π) β β) |
8 | | eqid 2737 |
. . . . . 6
β’
(coeffβπΉ) =
(coeffβπΉ) |
9 | | eqid 2737 |
. . . . . 6
β’
(degβπΉ) =
(degβπΉ) |
10 | 8, 9 | coeid2 25616 |
. . . . 5
β’ ((πΉ β (Polyββ€)
β§ (π / π) β β) β (πΉβ(π / π)) = Ξ£π β (0...(degβπΉ))(((coeffβπΉ)βπ) Β· ((π / π)βπ))) |
11 | 1, 7, 10 | syl2anc 585 |
. . . 4
β’ (π β (πΉβ(π / π)) = Ξ£π β (0...(degβπΉ))(((coeffβπΉ)βπ) Β· ((π / π)βπ))) |
12 | 11 | oveq1d 7377 |
. . 3
β’ (π β ((πΉβ(π / π)) Β· (πβ(degβπΉ))) = (Ξ£π β (0...(degβπΉ))(((coeffβπΉ)βπ) Β· ((π / π)βπ)) Β· (πβ(degβπΉ)))) |
13 | | fzfid 13885 |
. . . 4
β’ (π β (0...(degβπΉ)) β Fin) |
14 | | dgrcl 25610 |
. . . . . 6
β’ (πΉ β (Polyββ€)
β (degβπΉ) β
β0) |
15 | 1, 14 | syl 17 |
. . . . 5
β’ (π β (degβπΉ) β
β0) |
16 | 5, 15 | expcld 14058 |
. . . 4
β’ (π β (πβ(degβπΉ)) β β) |
17 | | 0z 12517 |
. . . . . . . 8
β’ 0 β
β€ |
18 | 8 | coef2 25608 |
. . . . . . . 8
β’ ((πΉ β (Polyββ€)
β§ 0 β β€) β (coeffβπΉ):β0βΆβ€) |
19 | 1, 17, 18 | sylancl 587 |
. . . . . . 7
β’ (π β (coeffβπΉ):β0βΆβ€) |
20 | | elfznn0 13541 |
. . . . . . 7
β’ (π β (0...(degβπΉ)) β π β β0) |
21 | | ffvelcdm 7037 |
. . . . . . 7
β’
(((coeffβπΉ):β0βΆβ€ β§
π β
β0) β ((coeffβπΉ)βπ) β β€) |
22 | 19, 20, 21 | syl2an 597 |
. . . . . 6
β’ ((π β§ π β (0...(degβπΉ))) β ((coeffβπΉ)βπ) β β€) |
23 | 22 | zcnd 12615 |
. . . . 5
β’ ((π β§ π β (0...(degβπΉ))) β ((coeffβπΉ)βπ) β β) |
24 | | expcl 13992 |
. . . . . 6
β’ (((π / π) β β β§ π β β0) β ((π / π)βπ) β β) |
25 | 7, 20, 24 | syl2an 597 |
. . . . 5
β’ ((π β§ π β (0...(degβπΉ))) β ((π / π)βπ) β β) |
26 | 23, 25 | mulcld 11182 |
. . . 4
β’ ((π β§ π β (0...(degβπΉ))) β (((coeffβπΉ)βπ) Β· ((π / π)βπ)) β β) |
27 | 13, 16, 26 | fsummulc1 15677 |
. . 3
β’ (π β (Ξ£π β (0...(degβπΉ))(((coeffβπΉ)βπ) Β· ((π / π)βπ)) Β· (πβ(degβπΉ))) = Ξ£π β (0...(degβπΉ))((((coeffβπΉ)βπ) Β· ((π / π)βπ)) Β· (πβ(degβπΉ)))) |
28 | 12, 27 | eqtrd 2777 |
. 2
β’ (π β ((πΉβ(π / π)) Β· (πβ(degβπΉ))) = Ξ£π β (0...(degβπΉ))((((coeffβπΉ)βπ) Β· ((π / π)βπ)) Β· (πβ(degβπΉ)))) |
29 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (0...(degβπΉ))) β π β β) |
30 | 15 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (0...(degβπΉ))) β (degβπΉ) β
β0) |
31 | 29, 30 | expcld 14058 |
. . . . 5
β’ ((π β§ π β (0...(degβπΉ))) β (πβ(degβπΉ)) β β) |
32 | 23, 25, 31 | mulassd 11185 |
. . . 4
β’ ((π β§ π β (0...(degβπΉ))) β ((((coeffβπΉ)βπ) Β· ((π / π)βπ)) Β· (πβ(degβπΉ))) = (((coeffβπΉ)βπ) Β· (((π / π)βπ) Β· (πβ(degβπΉ))))) |
33 | 2 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(degβπΉ))) β π β β€) |
34 | 33 | zcnd 12615 |
. . . . . . . . 9
β’ ((π β§ π β (0...(degβπΉ))) β π β β) |
35 | 6 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0...(degβπΉ))) β π β 0) |
36 | 20 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (0...(degβπΉ))) β π β β0) |
37 | 34, 29, 35, 36 | expdivd 14072 |
. . . . . . . 8
β’ ((π β§ π β (0...(degβπΉ))) β ((π / π)βπ) = ((πβπ) / (πβπ))) |
38 | 37 | oveq1d 7377 |
. . . . . . 7
β’ ((π β§ π β (0...(degβπΉ))) β (((π / π)βπ) Β· (πβ(degβπΉ))) = (((πβπ) / (πβπ)) Β· (πβ(degβπΉ)))) |
39 | 34, 36 | expcld 14058 |
. . . . . . . 8
β’ ((π β§ π β (0...(degβπΉ))) β (πβπ) β β) |
40 | | nnexpcl 13987 |
. . . . . . . . . 10
β’ ((π β β β§ π β β0)
β (πβπ) β
β) |
41 | 4, 20, 40 | syl2an 597 |
. . . . . . . . 9
β’ ((π β§ π β (0...(degβπΉ))) β (πβπ) β β) |
42 | 41 | nncnd 12176 |
. . . . . . . 8
β’ ((π β§ π β (0...(degβπΉ))) β (πβπ) β β) |
43 | 41 | nnne0d 12210 |
. . . . . . . 8
β’ ((π β§ π β (0...(degβπΉ))) β (πβπ) β 0) |
44 | 39, 42, 31, 43 | div13d 11962 |
. . . . . . 7
β’ ((π β§ π β (0...(degβπΉ))) β (((πβπ) / (πβπ)) Β· (πβ(degβπΉ))) = (((πβ(degβπΉ)) / (πβπ)) Β· (πβπ))) |
45 | 38, 44 | eqtrd 2777 |
. . . . . 6
β’ ((π β§ π β (0...(degβπΉ))) β (((π / π)βπ) Β· (πβ(degβπΉ))) = (((πβ(degβπΉ)) / (πβπ)) Β· (πβπ))) |
46 | | elfzelz 13448 |
. . . . . . . . . 10
β’ (π β (0...(degβπΉ)) β π β β€) |
47 | 46 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (0...(degβπΉ))) β π β β€) |
48 | 30 | nn0zd 12532 |
. . . . . . . . 9
β’ ((π β§ π β (0...(degβπΉ))) β (degβπΉ) β β€) |
49 | 29, 35, 47, 48 | expsubd 14069 |
. . . . . . . 8
β’ ((π β§ π β (0...(degβπΉ))) β (πβ((degβπΉ) β π)) = ((πβ(degβπΉ)) / (πβπ))) |
50 | 4 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(degβπΉ))) β π β β) |
51 | 50 | nnzd 12533 |
. . . . . . . . 9
β’ ((π β§ π β (0...(degβπΉ))) β π β β€) |
52 | | fznn0sub 13480 |
. . . . . . . . . 10
β’ (π β (0...(degβπΉ)) β ((degβπΉ) β π) β
β0) |
53 | 52 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (0...(degβπΉ))) β ((degβπΉ) β π) β
β0) |
54 | | zexpcl 13989 |
. . . . . . . . 9
β’ ((π β β€ β§
((degβπΉ) β
π) β
β0) β (πβ((degβπΉ) β π)) β β€) |
55 | 51, 53, 54 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π β (0...(degβπΉ))) β (πβ((degβπΉ) β π)) β β€) |
56 | 49, 55 | eqeltrrd 2839 |
. . . . . . 7
β’ ((π β§ π β (0...(degβπΉ))) β ((πβ(degβπΉ)) / (πβπ)) β β€) |
57 | | zexpcl 13989 |
. . . . . . . 8
β’ ((π β β€ β§ π β β0)
β (πβπ) β
β€) |
58 | 2, 20, 57 | syl2an 597 |
. . . . . . 7
β’ ((π β§ π β (0...(degβπΉ))) β (πβπ) β β€) |
59 | 56, 58 | zmulcld 12620 |
. . . . . 6
β’ ((π β§ π β (0...(degβπΉ))) β (((πβ(degβπΉ)) / (πβπ)) Β· (πβπ)) β β€) |
60 | 45, 59 | eqeltrd 2838 |
. . . . 5
β’ ((π β§ π β (0...(degβπΉ))) β (((π / π)βπ) Β· (πβ(degβπΉ))) β β€) |
61 | 22, 60 | zmulcld 12620 |
. . . 4
β’ ((π β§ π β (0...(degβπΉ))) β (((coeffβπΉ)βπ) Β· (((π / π)βπ) Β· (πβ(degβπΉ)))) β β€) |
62 | 32, 61 | eqeltrd 2838 |
. . 3
β’ ((π β§ π β (0...(degβπΉ))) β ((((coeffβπΉ)βπ) Β· ((π / π)βπ)) Β· (πβ(degβπΉ))) β β€) |
63 | 13, 62 | fsumzcl 15627 |
. 2
β’ (π β Ξ£π β (0...(degβπΉ))((((coeffβπΉ)βπ) Β· ((π / π)βπ)) Β· (πβ(degβπΉ))) β β€) |
64 | 28, 63 | eqeltrd 2838 |
1
β’ (π β ((πΉβ(π / π)) Β· (πβ(degβπΉ))) β β€) |