Step | Hyp | Ref
| Expression |
1 | | taylfval.s |
. . . . . . 7
β’ (π β π β {β, β}) |
2 | | taylfval.f |
. . . . . . 7
β’ (π β πΉ:π΄βΆβ) |
3 | | taylfval.a |
. . . . . . 7
β’ (π β π΄ β π) |
4 | | taylfval.n |
. . . . . . 7
β’ (π β (π β β0 β¨ π = +β)) |
5 | | taylfval.b |
. . . . . . 7
β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) |
6 | | taylfval.t |
. . . . . . 7
β’ π = (π(π Tayl πΉ)π΅) |
7 | 1, 2, 3, 4, 5, 6 | taylfval 25734 |
. . . . . 6
β’ (π β π = βͺ π₯ β β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))))) |
8 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β) β π₯ β β) |
9 | 8 | snssd 4774 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β {π₯} β β) |
10 | 1, 2, 3, 4, 5 | taylfvallem 25733 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β
(βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) β β) |
11 | | xpss12 5653 |
. . . . . . . . 9
β’ (({π₯} β β β§
(βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) β β) β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) β (β Γ
β)) |
12 | 9, 10, 11 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) β (β Γ
β)) |
13 | 12 | ralrimiva 3144 |
. . . . . . 7
β’ (π β βπ₯ β β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) β (β Γ
β)) |
14 | | iunss 5010 |
. . . . . . 7
β’ (βͺ π₯ β β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) β (β Γ β)
β βπ₯ β
β ({π₯} Γ
(βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) β (β Γ
β)) |
15 | 13, 14 | sylibr 233 |
. . . . . 6
β’ (π β βͺ π₯ β β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) β (β Γ
β)) |
16 | 7, 15 | eqsstrd 3987 |
. . . . 5
β’ (π β π β (β Γ
β)) |
17 | | relxp 5656 |
. . . . 5
β’ Rel
(β Γ β) |
18 | | relss 5742 |
. . . . 5
β’ (π β (β Γ
β) β (Rel (β Γ β) β Rel π)) |
19 | 16, 17, 18 | mpisyl 21 |
. . . 4
β’ (π β Rel π) |
20 | 1, 2, 3, 4, 5, 6 | eltayl 25735 |
. . . . . . . 8
β’ (π β (π₯ππ¦ β (π₯ β β β§ π¦ β (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))))) |
21 | 20 | biimpd 228 |
. . . . . . 7
β’ (π β (π₯ππ¦ β (π₯ β β β§ π¦ β (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))))) |
22 | 21 | alrimiv 1931 |
. . . . . 6
β’ (π β βπ¦(π₯ππ¦ β (π₯ β β β§ π¦ β (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))))) |
23 | | cnfldbas 20816 |
. . . . . . . . 9
β’ β =
(Baseββfld) |
24 | | cnring 20835 |
. . . . . . . . . 10
β’
βfld β Ring |
25 | | ringcmn 20010 |
. . . . . . . . . 10
β’
(βfld β Ring β βfld β
CMnd) |
26 | 24, 25 | mp1i 13 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β βfld
β CMnd) |
27 | | cnfldtps 24157 |
. . . . . . . . . 10
β’
βfld β TopSp |
28 | 27 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β βfld
β TopSp) |
29 | | ovex 7395 |
. . . . . . . . . . 11
β’
(0[,]π) β
V |
30 | 29 | inex1 5279 |
. . . . . . . . . 10
β’
((0[,]π) β©
β€) β V |
31 | 30 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β ((0[,]π) β© β€) β
V) |
32 | 1, 2, 3, 4, 5 | taylfvallem1 25732 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π β ((0[,]π) β© β€)) β (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)) β β) |
33 | 32 | fmpttd 7068 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))):((0[,]π) β©
β€)βΆβ) |
34 | | eqid 2737 |
. . . . . . . . 9
β’
(TopOpenββfld) =
(TopOpenββfld) |
35 | 34 | cnfldhaus 24164 |
. . . . . . . . . 10
β’
(TopOpenββfld) β Haus |
36 | 35 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β
(TopOpenββfld) β Haus) |
37 | 23, 26, 28, 31, 33, 34, 36 | haustsms 23503 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β β*π¦ π¦ β (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) |
38 | 37 | ex 414 |
. . . . . . 7
β’ (π β (π₯ β β β β*π¦ π¦ β (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))))) |
39 | | moanimv 2620 |
. . . . . . 7
β’
(β*π¦(π₯ β β β§ π¦ β (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) β (π₯ β β β β*π¦ π¦ β (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))))) |
40 | 38, 39 | sylibr 233 |
. . . . . 6
β’ (π β β*π¦(π₯ β β β§ π¦ β (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))))) |
41 | | moim 2543 |
. . . . . 6
β’
(βπ¦(π₯ππ¦ β (π₯ β β β§ π¦ β (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))))) β (β*π¦(π₯ β β β§ π¦ β (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) β β*π¦ π₯ππ¦)) |
42 | 22, 40, 41 | sylc 65 |
. . . . 5
β’ (π β β*π¦ π₯ππ¦) |
43 | 42 | alrimiv 1931 |
. . . 4
β’ (π β βπ₯β*π¦ π₯ππ¦) |
44 | | dffun6 6514 |
. . . 4
β’ (Fun
π β (Rel π β§ βπ₯β*π¦ π₯ππ¦)) |
45 | 19, 43, 44 | sylanbrc 584 |
. . 3
β’ (π β Fun π) |
46 | 45 | funfnd 6537 |
. 2
β’ (π β π Fn dom π) |
47 | | rnss 5899 |
. . . 4
β’ (π β (β Γ
β) β ran π
β ran (β Γ β)) |
48 | 16, 47 | syl 17 |
. . 3
β’ (π β ran π β ran (β Γ
β)) |
49 | | rnxpss 6129 |
. . 3
β’ ran
(β Γ β) β β |
50 | 48, 49 | sstrdi 3961 |
. 2
β’ (π β ran π β β) |
51 | | df-f 6505 |
. 2
β’ (π:dom πβΆβ β (π Fn dom π β§ ran π β β)) |
52 | 46, 50, 51 | sylanbrc 584 |
1
β’ (π β π:dom πβΆβ) |