Step | Hyp | Ref
| Expression |
1 | | taylpfval.s |
. . . 4
β’ (π β π β {β, β}) |
2 | | taylpfval.f |
. . . 4
β’ (π β πΉ:π΄βΆβ) |
3 | | taylpfval.a |
. . . 4
β’ (π β π΄ β π) |
4 | | taylpfval.n |
. . . . 5
β’ (π β π β
β0) |
5 | 4 | orcd 871 |
. . . 4
β’ (π β (π β β0 β¨ π = +β)) |
6 | | taylpfval.b |
. . . . 5
β’ (π β π΅ β dom ((π Dπ πΉ)βπ)) |
7 | 1, 2, 3, 4, 6 | taylplem1 26315 |
. . . 4
β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) |
8 | | taylpfval.t |
. . . 4
β’ π = (π(π Tayl πΉ)π΅) |
9 | 1, 2, 3, 5, 7, 8 | taylfval 26311 |
. . 3
β’ (π β π = βͺ π₯ β β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))))) |
10 | | cnfldbas 21287 |
. . . . . . 7
β’ β =
(Baseββfld) |
11 | | cnfld0 21324 |
. . . . . . 7
β’ 0 =
(0gββfld) |
12 | | cnring 21322 |
. . . . . . . 8
β’
βfld β Ring |
13 | | ringcmn 20222 |
. . . . . . . 8
β’
(βfld β Ring β βfld β
CMnd) |
14 | 12, 13 | mp1i 13 |
. . . . . . 7
β’ ((π β§ π₯ β β) β βfld
β CMnd) |
15 | | cnfldtps 24712 |
. . . . . . . 8
β’
βfld β TopSp |
16 | 15 | a1i 11 |
. . . . . . 7
β’ ((π β§ π₯ β β) β βfld
β TopSp) |
17 | | ovex 7449 |
. . . . . . . . 9
β’
(0[,]π) β
V |
18 | 17 | inex1 5312 |
. . . . . . . 8
β’
((0[,]π) β©
β€) β V |
19 | 18 | a1i 11 |
. . . . . . 7
β’ ((π β§ π₯ β β) β ((0[,]π) β© β€) β
V) |
20 | 1, 2, 3, 5, 7 | taylfvallem1 26309 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ π β ((0[,]π) β© β€)) β (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)) β β) |
21 | 20 | fmpttd 7120 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))):((0[,]π) β©
β€)βΆβ) |
22 | | eqid 2725 |
. . . . . . . 8
β’ (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))) = (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))) |
23 | | 0z 12599 |
. . . . . . . . . . 11
β’ 0 β
β€ |
24 | 4 | nn0zd 12614 |
. . . . . . . . . . 11
β’ (π β π β β€) |
25 | | fzval2 13519 |
. . . . . . . . . . 11
β’ ((0
β β€ β§ π
β β€) β (0...π) = ((0[,]π) β© β€)) |
26 | 23, 24, 25 | sylancr 585 |
. . . . . . . . . 10
β’ (π β (0...π) = ((0[,]π) β© β€)) |
27 | 26 | adantr 479 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (0...π) = ((0[,]π) β© β€)) |
28 | | fzfid 13970 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (0...π) β Fin) |
29 | 27, 28 | eqeltrrd 2826 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β ((0[,]π) β© β€) β
Fin) |
30 | | ovexd 7451 |
. . . . . . . 8
β’ (((π β§ π₯ β β) β§ π β ((0[,]π) β© β€)) β (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)) β V) |
31 | | c0ex 11238 |
. . . . . . . . 9
β’ 0 β
V |
32 | 31 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β 0 β
V) |
33 | 22, 29, 30, 32 | fsuppmptdm 9399 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))) finSupp 0) |
34 | | eqid 2725 |
. . . . . . 7
β’
(TopOpenββfld) =
(TopOpenββfld) |
35 | 34 | cnfldhaus 24719 |
. . . . . . . 8
β’
(TopOpenββfld) β Haus |
36 | 35 | a1i 11 |
. . . . . . 7
β’ ((π β§ π₯ β β) β
(TopOpenββfld) β Haus) |
37 | 10, 11, 14, 16, 19, 21, 33, 34, 36 | haustsmsid 24063 |
. . . . . 6
β’ ((π β§ π₯ β β) β
(βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) = {(βfld
Ξ£g (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))}) |
38 | 29, 20 | gsumfsum 21371 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β
(βfld Ξ£g (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) = Ξ£π β ((0[,]π) β© β€)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))) |
39 | 27 | sumeq1d 15679 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)) = Ξ£π β ((0[,]π) β© β€)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))) |
40 | 38, 39 | eqtr4d 2768 |
. . . . . . 7
β’ ((π β§ π₯ β β) β
(βfld Ξ£g (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) = Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))) |
41 | 40 | sneqd 4636 |
. . . . . 6
β’ ((π β§ π₯ β β) β
{(βfld Ξ£g (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))} = {Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))}) |
42 | 37, 41 | eqtrd 2765 |
. . . . 5
β’ ((π β§ π₯ β β) β
(βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) = {Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))}) |
43 | 42 | xpeq2d 5702 |
. . . 4
β’ ((π β§ π₯ β β) β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) = ({π₯} Γ {Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))})) |
44 | 43 | iuneq2dv 5015 |
. . 3
β’ (π β βͺ π₯ β β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) = βͺ
π₯ β β ({π₯} Γ {Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))})) |
45 | 9, 44 | eqtrd 2765 |
. 2
β’ (π β π = βͺ π₯ β β ({π₯} Γ {Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))})) |
46 | | dfmpt3 6684 |
. 2
β’ (π₯ β β β¦
Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))) = βͺ
π₯ β β ({π₯} Γ {Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))}) |
47 | 45, 46 | eqtr4di 2783 |
1
β’ (π β π = (π₯ β β β¦ Ξ£π β (0...π)(((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) |