Step | Hyp | Ref
| Expression |
1 | | taylpfval.s |
. . . 4
β’ (π β π β {β, β}) |
2 | | taylpfval.f |
. . . 4
β’ (π β πΉ:π΄βΆβ) |
3 | | taylpfval.a |
. . . 4
β’ (π β π΄ β π) |
4 | | taylpfval.n |
. . . . 5
β’ (π β π β
β0) |
5 | 4 | orcd 872 |
. . . 4
β’ (π β (π β β0 β¨ π = +β)) |
6 | | taylpfval.b |
. . . . 5
β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) |
7 | 1, 2, 3, 4, 6 | taylplem1 25738 |
. . . 4
β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) |
8 | | taylpfval.t |
. . . 4
β’ π = (π(π Tayl πΉ)π΅) |
9 | 1, 2, 3, 5, 7, 8 | taylfval 25734 |
. . 3
β’ (π β π = βͺ π₯ β β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))))) |
10 | | cnfldbas 20816 |
. . . . . . 7
β’ β =
(Baseββfld) |
11 | | cnfld0 20837 |
. . . . . . 7
β’ 0 =
(0gββfld) |
12 | | cnring 20835 |
. . . . . . . 8
β’
βfld β Ring |
13 | | ringcmn 20010 |
. . . . . . . 8
β’
(βfld β Ring β βfld β
CMnd) |
14 | 12, 13 | mp1i 13 |
. . . . . . 7
β’ ((π β§ π₯ β β) β βfld
β CMnd) |
15 | | cnfldtps 24157 |
. . . . . . . 8
β’
βfld β TopSp |
16 | 15 | a1i 11 |
. . . . . . 7
β’ ((π β§ π₯ β β) β βfld
β TopSp) |
17 | | ovex 7395 |
. . . . . . . . 9
β’
(0[,]π) β
V |
18 | 17 | inex1 5279 |
. . . . . . . 8
β’
((0[,]π) β©
β€) β V |
19 | 18 | a1i 11 |
. . . . . . 7
β’ ((π β§ π₯ β β) β ((0[,]π) β© β€) β
V) |
20 | 1, 2, 3, 5, 7 | taylfvallem1 25732 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ π β ((0[,]π) β© β€)) β (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)) β β) |
21 | 20 | fmpttd 7068 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))):((0[,]π) β©
β€)βΆβ) |
22 | | eqid 2737 |
. . . . . . . 8
β’ (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))) = (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))) |
23 | | 0z 12517 |
. . . . . . . . . . 11
β’ 0 β
β€ |
24 | 4 | nn0zd 12532 |
. . . . . . . . . . 11
β’ (π β π β β€) |
25 | | fzval2 13434 |
. . . . . . . . . . 11
β’ ((0
β β€ β§ π
β β€) β (0...π) = ((0[,]π) β© β€)) |
26 | 23, 24, 25 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (0...π) = ((0[,]π) β© β€)) |
27 | 26 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (0...π) = ((0[,]π) β© β€)) |
28 | | fzfid 13885 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (0...π) β Fin) |
29 | 27, 28 | eqeltrrd 2839 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β ((0[,]π) β© β€) β
Fin) |
30 | | ovexd 7397 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ π β ((0[,]π) β© β€)) β (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)) β V) |
31 | | c0ex 11156 |
. . . . . . . . 9
β’ 0 β
V |
32 | 31 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β 0 β
V) |
33 | 22, 29, 30, 32 | fsuppmptdm 9323 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))) finSupp 0) |
34 | | eqid 2737 |
. . . . . . 7
β’
(TopOpenββfld) =
(TopOpenββfld) |
35 | 34 | cnfldhaus 24164 |
. . . . . . . 8
β’
(TopOpenββfld) β Haus |
36 | 35 | a1i 11 |
. . . . . . 7
β’ ((π β§ π₯ β β) β
(TopOpenββfld) β Haus) |
37 | 10, 11, 14, 16, 19, 21, 33, 34, 36 | haustsmsid 23508 |
. . . . . 6
β’ ((π β§ π₯ β β) β
(βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) = {(βfld
Ξ£g (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))}) |
38 | 29, 20 | gsumfsum 20880 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β
(βfld Ξ£g (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) = Ξ£π β ((0[,]π) β© β€)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))) |
39 | 27 | sumeq1d 15593 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)) = Ξ£π β ((0[,]π) β© β€)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))) |
40 | 38, 39 | eqtr4d 2780 |
. . . . . . 7
β’ ((π β§ π₯ β β) β
(βfld Ξ£g (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) = Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))) |
41 | 40 | sneqd 4603 |
. . . . . 6
β’ ((π β§ π₯ β β) β
{(βfld Ξ£g (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))} = {Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))}) |
42 | 37, 41 | eqtrd 2777 |
. . . . 5
β’ ((π β§ π₯ β β) β
(βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) = {Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))}) |
43 | 42 | xpeq2d 5668 |
. . . 4
β’ ((π β§ π₯ β β) β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) = ({π₯} Γ {Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))})) |
44 | 43 | iuneq2dv 4983 |
. . 3
β’ (π β βͺ π₯ β β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) = βͺ
π₯ β β ({π₯} Γ {Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))})) |
45 | 9, 44 | eqtrd 2777 |
. 2
β’ (π β π = βͺ π₯ β β ({π₯} Γ {Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))})) |
46 | | dfmpt3 6640 |
. 2
β’ (π₯ β β β¦
Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))) = βͺ
π₯ β β ({π₯} Γ {Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))}) |
47 | 45, 46 | eqtr4di 2795 |
1
β’ (π β π = (π₯ β β β¦ Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) |