Step | Hyp | Ref
| Expression |
1 | | taylpfval.s |
. . . . 5
β’ (π β π β {β, β}) |
2 | | taylpfval.f |
. . . . 5
β’ (π β πΉ:π΄βΆβ) |
3 | | taylpfval.a |
. . . . 5
β’ (π β π΄ β π) |
4 | | taylpfval.n |
. . . . 5
β’ (π β π β
β0) |
5 | | taylpfval.b |
. . . . 5
β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) |
6 | | taylpfval.t |
. . . . 5
β’ π = (π(π Tayl πΉ)π΅) |
7 | 1, 2, 3, 4, 5, 6 | taylpfval 25740 |
. . . 4
β’ (π β π = (π₯ β β β¦ Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) |
8 | | simpr 486 |
. . . . . 6
β’ ((π β§ π₯ β β) β π₯ β β) |
9 | | cnex 11139 |
. . . . . . . . . . . . 13
β’ β
β V |
10 | 9 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β β
V) |
11 | | elpm2r 8790 |
. . . . . . . . . . . 12
β’
(((β β V β§ π β {β, β}) β§ (πΉ:π΄βΆβ β§ π΄ β π)) β πΉ β (β βpm π)) |
12 | 10, 1, 2, 3, 11 | syl22anc 838 |
. . . . . . . . . . 11
β’ (π β πΉ β (β βpm π)) |
13 | | dvnbss 25308 |
. . . . . . . . . . 11
β’ ((π β {β, β} β§
πΉ β (β
βpm π)
β§ π β
β0) β dom ((π Dπ πΉ)βπ) β dom πΉ) |
14 | 1, 12, 4, 13 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β dom ((π Dπ πΉ)βπ) β dom πΉ) |
15 | 2, 14 | fssdmd 6692 |
. . . . . . . . 9
β’ (π β dom ((π Dπ πΉ)βπ) β π΄) |
16 | | recnprss 25284 |
. . . . . . . . . . 11
β’ (π β {β, β}
β π β
β) |
17 | 1, 16 | syl 17 |
. . . . . . . . . 10
β’ (π β π β β) |
18 | 3, 17 | sstrd 3959 |
. . . . . . . . 9
β’ (π β π΄ β β) |
19 | 15, 18 | sstrd 3959 |
. . . . . . . 8
β’ (π β dom ((π Dπ πΉ)βπ) β β) |
20 | 19, 5 | sseldd 3950 |
. . . . . . 7
β’ (π β π΅ β β) |
21 | 20 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β β) β π΅ β β) |
22 | 8, 21 | subcld 11519 |
. . . . 5
β’ ((π β§ π₯ β β) β (π₯ β π΅) β β) |
23 | | df-idp 25566 |
. . . . . . . 8
β’
Xp = ( I βΎ β) |
24 | | mptresid 6009 |
. . . . . . . 8
β’ ( I
βΎ β) = (π₯
β β β¦ π₯) |
25 | 23, 24 | eqtri 2765 |
. . . . . . 7
β’
Xp = (π₯ β β β¦ π₯) |
26 | 25 | a1i 11 |
. . . . . 6
β’ (π β Xp =
(π₯ β β β¦
π₯)) |
27 | | fconstmpt 5699 |
. . . . . . 7
β’ (β
Γ {π΅}) = (π₯ β β β¦ π΅) |
28 | 27 | a1i 11 |
. . . . . 6
β’ (π β (β Γ {π΅}) = (π₯ β β β¦ π΅)) |
29 | 10, 8, 21, 26, 28 | offval2 7642 |
. . . . 5
β’ (π β (Xp
βf β (β Γ {π΅})) = (π₯ β β β¦ (π₯ β π΅))) |
30 | | eqidd 2738 |
. . . . 5
β’ (π β (π¦ β β β¦ Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ))) = (π¦ β β β¦ Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ)))) |
31 | | oveq1 7369 |
. . . . . . 7
β’ (π¦ = (π₯ β π΅) β (π¦βπ) = ((π₯ β π΅)βπ)) |
32 | 31 | oveq2d 7378 |
. . . . . 6
β’ (π¦ = (π₯ β π΅) β (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ)) = (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))) |
33 | 32 | sumeq2sdv 15596 |
. . . . 5
β’ (π¦ = (π₯ β π΅) β Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ)) = Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))) |
34 | 22, 29, 30, 33 | fmptco 7080 |
. . . 4
β’ (π β ((π¦ β β β¦ Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ))) β (Xp
βf β (β Γ {π΅}))) = (π₯ β β β¦ Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) |
35 | 7, 34 | eqtr4d 2780 |
. . 3
β’ (π β π = ((π¦ β β β¦ Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ))) β (Xp
βf β (β Γ {π΅})))) |
36 | | taylply2.1 |
. . . . . 6
β’ (π β π· β
(SubRingββfld)) |
37 | | cnfldbas 20816 |
. . . . . . 7
β’ β =
(Baseββfld) |
38 | 37 | subrgss 20239 |
. . . . . 6
β’ (π· β
(SubRingββfld) β π· β β) |
39 | 36, 38 | syl 17 |
. . . . 5
β’ (π β π· β β) |
40 | | taylply2.3 |
. . . . 5
β’ ((π β§ π β (0...π)) β ((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) β π·) |
41 | 39, 4, 40 | elplyd 25579 |
. . . 4
β’ (π β (π¦ β β β¦ Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ))) β (Polyβπ·)) |
42 | | cnfld1 20838 |
. . . . . . . 8
β’ 1 =
(1rββfld) |
43 | 42 | subrg1cl 20246 |
. . . . . . 7
β’ (π· β
(SubRingββfld) β 1 β π·) |
44 | 36, 43 | syl 17 |
. . . . . 6
β’ (π β 1 β π·) |
45 | | plyid 25586 |
. . . . . 6
β’ ((π· β β β§ 1 β
π·) β
Xp β (Polyβπ·)) |
46 | 39, 44, 45 | syl2anc 585 |
. . . . 5
β’ (π β Xp
β (Polyβπ·)) |
47 | | taylply2.2 |
. . . . . 6
β’ (π β π΅ β π·) |
48 | | plyconst 25583 |
. . . . . 6
β’ ((π· β β β§ π΅ β π·) β (β Γ {π΅}) β (Polyβπ·)) |
49 | 39, 47, 48 | syl2anc 585 |
. . . . 5
β’ (π β (β Γ {π΅}) β (Polyβπ·)) |
50 | | subrgsubg 20244 |
. . . . . . 7
β’ (π· β
(SubRingββfld) β π· β
(SubGrpββfld)) |
51 | 36, 50 | syl 17 |
. . . . . 6
β’ (π β π· β
(SubGrpββfld)) |
52 | | cnfldadd 20817 |
. . . . . . . 8
β’ + =
(+gββfld) |
53 | 52 | subgcl 18945 |
. . . . . . 7
β’ ((π· β
(SubGrpββfld) β§ π’ β π· β§ π£ β π·) β (π’ + π£) β π·) |
54 | 53 | 3expb 1121 |
. . . . . 6
β’ ((π· β
(SubGrpββfld) β§ (π’ β π· β§ π£ β π·)) β (π’ + π£) β π·) |
55 | 51, 54 | sylan 581 |
. . . . 5
β’ ((π β§ (π’ β π· β§ π£ β π·)) β (π’ + π£) β π·) |
56 | | cnfldmul 20818 |
. . . . . . . 8
β’ Β·
= (.rββfld) |
57 | 56 | subrgmcl 20250 |
. . . . . . 7
β’ ((π· β
(SubRingββfld) β§ π’ β π· β§ π£ β π·) β (π’ Β· π£) β π·) |
58 | 57 | 3expb 1121 |
. . . . . 6
β’ ((π· β
(SubRingββfld) β§ (π’ β π· β§ π£ β π·)) β (π’ Β· π£) β π·) |
59 | 36, 58 | sylan 581 |
. . . . 5
β’ ((π β§ (π’ β π· β§ π£ β π·)) β (π’ Β· π£) β π·) |
60 | | ax-1cn 11116 |
. . . . . . 7
β’ 1 β
β |
61 | | cnfldneg 20839 |
. . . . . . 7
β’ (1 β
β β ((invgββfld)β1) =
-1) |
62 | 60, 61 | ax-mp 5 |
. . . . . 6
β’
((invgββfld)β1) =
-1 |
63 | | eqid 2737 |
. . . . . . . 8
β’
(invgββfld) =
(invgββfld) |
64 | 63 | subginvcl 18944 |
. . . . . . 7
β’ ((π· β
(SubGrpββfld) β§ 1 β π·) β
((invgββfld)β1) β π·) |
65 | 51, 44, 64 | syl2anc 585 |
. . . . . 6
β’ (π β
((invgββfld)β1) β π·) |
66 | 62, 65 | eqeltrrid 2843 |
. . . . 5
β’ (π β -1 β π·) |
67 | 46, 49, 55, 59, 66 | plysub 25596 |
. . . 4
β’ (π β (Xp
βf β (β Γ {π΅})) β (Polyβπ·)) |
68 | 41, 67, 55, 59 | plyco 25618 |
. . 3
β’ (π β ((π¦ β β β¦ Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ))) β (Xp
βf β (β Γ {π΅}))) β (Polyβπ·)) |
69 | 35, 68 | eqeltrd 2838 |
. 2
β’ (π β π β (Polyβπ·)) |
70 | 35 | fveq2d 6851 |
. . . 4
β’ (π β (degβπ) = (degβ((π¦ β β β¦
Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ))) β (Xp
βf β (β Γ {π΅}))))) |
71 | | eqid 2737 |
. . . . 5
β’
(degβ(π¦ β
β β¦ Ξ£π
β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ)))) = (degβ(π¦ β β β¦ Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ)))) |
72 | | eqid 2737 |
. . . . 5
β’
(degβ(Xp βf β (β
Γ {π΅}))) =
(degβ(Xp βf β (β Γ
{π΅}))) |
73 | 71, 72, 41, 67 | dgrco 25652 |
. . . 4
β’ (π β (degβ((π¦ β β β¦
Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ))) β (Xp
βf β (β Γ {π΅})))) = ((degβ(π¦ β β β¦ Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ)))) Β·
(degβ(Xp βf β (β Γ
{π΅}))))) |
74 | | eqid 2737 |
. . . . . . . . 9
β’
(Xp βf β (β Γ
{π΅})) =
(Xp βf β (β Γ {π΅})) |
75 | 74 | plyremlem 25680 |
. . . . . . . 8
β’ (π΅ β β β
((Xp βf β (β Γ {π΅})) β (Polyββ)
β§ (degβ(Xp βf β (β
Γ {π΅}))) = 1 β§
(β‘(Xp
βf β (β Γ {π΅})) β {0}) = {π΅})) |
76 | 20, 75 | syl 17 |
. . . . . . 7
β’ (π β ((Xp
βf β (β Γ {π΅})) β (Polyββ) β§
(degβ(Xp βf β (β Γ
{π΅}))) = 1 β§ (β‘(Xp βf
β (β Γ {π΅})) β {0}) = {π΅})) |
77 | 76 | simp2d 1144 |
. . . . . 6
β’ (π β
(degβ(Xp βf β (β Γ
{π΅}))) =
1) |
78 | 77 | oveq2d 7378 |
. . . . 5
β’ (π β ((degβ(π¦ β β β¦
Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ)))) Β·
(degβ(Xp βf β (β Γ
{π΅})))) =
((degβ(π¦ β
β β¦ Ξ£π
β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ)))) Β· 1)) |
79 | | dgrcl 25610 |
. . . . . . . 8
β’ ((π¦ β β β¦
Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ))) β (Polyβπ·) β (degβ(π¦ β β β¦ Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ)))) β
β0) |
80 | 41, 79 | syl 17 |
. . . . . . 7
β’ (π β (degβ(π¦ β β β¦
Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ)))) β
β0) |
81 | 80 | nn0cnd 12482 |
. . . . . 6
β’ (π β (degβ(π¦ β β β¦
Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ)))) β β) |
82 | 81 | mulid1d 11179 |
. . . . 5
β’ (π β ((degβ(π¦ β β β¦
Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ)))) Β· 1) = (degβ(π¦ β β β¦
Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ))))) |
83 | 78, 82 | eqtrd 2777 |
. . . 4
β’ (π β ((degβ(π¦ β β β¦
Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ)))) Β·
(degβ(Xp βf β (β Γ
{π΅})))) = (degβ(π¦ β β β¦
Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ))))) |
84 | 70, 73, 83 | 3eqtrd 2781 |
. . 3
β’ (π β (degβπ) = (degβ(π¦ β β β¦
Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ))))) |
85 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β π β {β, β}) |
86 | 12 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β πΉ β (β βpm π)) |
87 | | elfznn0 13541 |
. . . . . . . 8
β’ (π β (0...π) β π β β0) |
88 | 87 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β π β β0) |
89 | | dvnf 25307 |
. . . . . . 7
β’ ((π β {β, β} β§
πΉ β (β
βpm π)
β§ π β
β0) β ((π Dπ πΉ)βπ):dom ((π Dπ πΉ)βπ)βΆβ) |
90 | 85, 86, 88, 89 | syl3anc 1372 |
. . . . . 6
β’ ((π β§ π β (0...π)) β ((π Dπ πΉ)βπ):dom ((π Dπ πΉ)βπ)βΆβ) |
91 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β (0...π)) β π β (0...π)) |
92 | | dvn2bss 25310 |
. . . . . . . 8
β’ ((π β {β, β} β§
πΉ β (β
βpm π)
β§ π β (0...π)) β dom ((π Dπ πΉ)βπ) β dom ((π Dπ πΉ)βπ)) |
93 | 85, 86, 91, 92 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β dom ((π Dπ πΉ)βπ) β dom ((π Dπ πΉ)βπ)) |
94 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β π΅ β dom ((π Dπ πΉ)βπ)) |
95 | 93, 94 | sseldd 3950 |
. . . . . 6
β’ ((π β§ π β (0...π)) β π΅ β dom ((π Dπ πΉ)βπ)) |
96 | 90, 95 | ffvelcdmd 7041 |
. . . . 5
β’ ((π β§ π β (0...π)) β (((π Dπ πΉ)βπ)βπ΅) β β) |
97 | 88 | faccld 14191 |
. . . . . 6
β’ ((π β§ π β (0...π)) β (!βπ) β β) |
98 | 97 | nncnd 12176 |
. . . . 5
β’ ((π β§ π β (0...π)) β (!βπ) β β) |
99 | 97 | nnne0d 12210 |
. . . . 5
β’ ((π β§ π β (0...π)) β (!βπ) β 0) |
100 | 96, 98, 99 | divcld 11938 |
. . . 4
β’ ((π β§ π β (0...π)) β ((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) β β) |
101 | 41, 4, 100, 30 | dgrle 25620 |
. . 3
β’ (π β (degβ(π¦ β β β¦
Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· (π¦βπ)))) β€ π) |
102 | 84, 101 | eqbrtrd 5132 |
. 2
β’ (π β (degβπ) β€ π) |
103 | 69, 102 | jca 513 |
1
β’ (π β (π β (Polyβπ·) β§ (degβπ) β€ π)) |