Step | Hyp | Ref
| Expression |
1 | | taylfval.t |
. 2
β’ π = (π(π Tayl πΉ)π΅) |
2 | | df-tayl 25666 |
. . . . 5
β’ Tayl =
(π β {β,
β}, π β (β
βpm π )
β¦ (π β
(β0 βͺ {+β}), π β β©
π β ((0[,]π) β© β€)dom ((π Dπ π)βπ) β¦ βͺ
π₯ β β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ π)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ))))))) |
3 | 2 | a1i 11 |
. . . 4
β’ (π β Tayl = (π β {β, β}, π β (β
βpm π )
β¦ (π β
(β0 βͺ {+β}), π β β©
π β ((0[,]π) β© β€)dom ((π Dπ π)βπ) β¦ βͺ
π₯ β β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ π)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ)))))))) |
4 | | eqidd 2738 |
. . . . 5
β’ ((π β§ (π = π β§ π = πΉ)) β (β0 βͺ
{+β}) = (β0 βͺ {+β})) |
5 | | oveq12 7360 |
. . . . . . . . 9
β’ ((π = π β§ π = πΉ) β (π Dπ π) = (π Dπ πΉ)) |
6 | 5 | ad2antlr 725 |
. . . . . . . 8
β’ (((π β§ (π = π β§ π = πΉ)) β§ π β ((0[,]π) β© β€)) β (π Dπ π) = (π Dπ πΉ)) |
7 | 6 | fveq1d 6841 |
. . . . . . 7
β’ (((π β§ (π = π β§ π = πΉ)) β§ π β ((0[,]π) β© β€)) β ((π Dπ π)βπ) = ((π Dπ πΉ)βπ)) |
8 | 7 | dmeqd 5859 |
. . . . . 6
β’ (((π β§ (π = π β§ π = πΉ)) β§ π β ((0[,]π) β© β€)) β dom ((π Dπ π)βπ) = dom ((π Dπ πΉ)βπ)) |
9 | 8 | iineq2dv 4977 |
. . . . 5
β’ ((π β§ (π = π β§ π = πΉ)) β β© π β ((0[,]π) β© β€)dom ((π Dπ π)βπ) = β© π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ)) |
10 | 7 | fveq1d 6841 |
. . . . . . . . . . 11
β’ (((π β§ (π = π β§ π = πΉ)) β§ π β ((0[,]π) β© β€)) β (((π Dπ π)βπ)βπ) = (((π Dπ πΉ)βπ)βπ)) |
11 | 10 | oveq1d 7366 |
. . . . . . . . . 10
β’ (((π β§ (π = π β§ π = πΉ)) β§ π β ((0[,]π) β© β€)) β ((((π Dπ π)βπ)βπ) / (!βπ)) = ((((π Dπ πΉ)βπ)βπ) / (!βπ))) |
12 | 11 | oveq1d 7366 |
. . . . . . . . 9
β’ (((π β§ (π = π β§ π = πΉ)) β§ π β ((0[,]π) β© β€)) β (((((π Dπ π)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ)) = (((((π Dπ πΉ)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ))) |
13 | 12 | mpteq2dva 5203 |
. . . . . . . 8
β’ ((π β§ (π = π β§ π = πΉ)) β (π β ((0[,]π) β© β€) β¦ (((((π Dπ π)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ))) = (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ)))) |
14 | 13 | oveq2d 7367 |
. . . . . . 7
β’ ((π β§ (π = π β§ π = πΉ)) β (βfld tsums
(π β ((0[,]π) β© β€) β¦
(((((π
Dπ π)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ)))) = (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ))))) |
15 | 14 | xpeq2d 5661 |
. . . . . 6
β’ ((π β§ (π = π β§ π = πΉ)) β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ π)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ))))) = ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ)))))) |
16 | 15 | iuneq2d 4981 |
. . . . 5
β’ ((π β§ (π = π β§ π = πΉ)) β βͺ π₯ β β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ π)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ))))) = βͺ
π₯ β β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ)))))) |
17 | 4, 9, 16 | mpoeq123dv 7426 |
. . . 4
β’ ((π β§ (π = π β§ π = πΉ)) β (π β (β0 βͺ
{+β}), π β
β© π β ((0[,]π) β© β€)dom ((π Dπ π)βπ) β¦ βͺ
π₯ β β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ π)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ)))))) = (π β (β0 βͺ
{+β}), π β
β© π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ) β¦ βͺ
π₯ β β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ))))))) |
18 | | simpr 485 |
. . . . 5
β’ ((π β§ π = π) β π = π) |
19 | 18 | oveq2d 7367 |
. . . 4
β’ ((π β§ π = π) β (β βpm π ) = (β βpm
π)) |
20 | | taylfval.s |
. . . 4
β’ (π β π β {β, β}) |
21 | | cnex 11090 |
. . . . . 6
β’ β
β V |
22 | 21 | a1i 11 |
. . . . 5
β’ (π β β β
V) |
23 | | taylfval.f |
. . . . 5
β’ (π β πΉ:π΄βΆβ) |
24 | | taylfval.a |
. . . . 5
β’ (π β π΄ β π) |
25 | | elpm2r 8741 |
. . . . 5
β’
(((β β V β§ π β {β, β}) β§ (πΉ:π΄βΆβ β§ π΄ β π)) β πΉ β (β βpm π)) |
26 | 22, 20, 23, 24, 25 | syl22anc 837 |
. . . 4
β’ (π β πΉ β (β βpm π)) |
27 | | nn0ex 12377 |
. . . . . . 7
β’
β0 β V |
28 | | snex 5386 |
. . . . . . 7
β’
{+β} β V |
29 | 27, 28 | unex 7672 |
. . . . . 6
β’
(β0 βͺ {+β}) β V |
30 | | 0xr 11160 |
. . . . . . . . . 10
β’ 0 β
β* |
31 | | nn0ssre 12375 |
. . . . . . . . . . . . 13
β’
β0 β β |
32 | | ressxr 11157 |
. . . . . . . . . . . . 13
β’ β
β β* |
33 | 31, 32 | sstri 3951 |
. . . . . . . . . . . 12
β’
β0 β β* |
34 | | pnfxr 11167 |
. . . . . . . . . . . . 13
β’ +β
β β* |
35 | | snssi 4766 |
. . . . . . . . . . . . 13
β’ (+β
β β* β {+β} β
β*) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . 12
β’
{+β} β β* |
37 | 33, 36 | unssi 4143 |
. . . . . . . . . . 11
β’
(β0 βͺ {+β}) β
β* |
38 | 37 | sseli 3938 |
. . . . . . . . . 10
β’ (π β (β0
βͺ {+β}) β π
β β*) |
39 | | elun 4106 |
. . . . . . . . . . 11
β’ (π β (β0
βͺ {+β}) β (π
β β0 β¨ π β {+β})) |
40 | | nn0ge0 12396 |
. . . . . . . . . . . 12
β’ (π β β0
β 0 β€ π) |
41 | | 0lepnf 13007 |
. . . . . . . . . . . . 13
β’ 0 β€
+β |
42 | | elsni 4601 |
. . . . . . . . . . . . 13
β’ (π β {+β} β π = +β) |
43 | 41, 42 | breqtrrid 5141 |
. . . . . . . . . . . 12
β’ (π β {+β} β 0 β€
π) |
44 | 40, 43 | jaoi 855 |
. . . . . . . . . . 11
β’ ((π β β0 β¨
π β {+β}) β
0 β€ π) |
45 | 39, 44 | sylbi 216 |
. . . . . . . . . 10
β’ (π β (β0
βͺ {+β}) β 0 β€ π) |
46 | | lbicc2 13335 |
. . . . . . . . . 10
β’ ((0
β β* β§ π β β* β§ 0 β€
π) β 0 β
(0[,]π)) |
47 | 30, 38, 45, 46 | mp3an2i 1466 |
. . . . . . . . 9
β’ (π β (β0
βͺ {+β}) β 0 β (0[,]π)) |
48 | | 0z 12468 |
. . . . . . . . 9
β’ 0 β
β€ |
49 | | inelcm 4422 |
. . . . . . . . 9
β’ ((0
β (0[,]π) β§ 0
β β€) β ((0[,]π) β© β€) β
β
) |
50 | 47, 48, 49 | sylancl 586 |
. . . . . . . 8
β’ (π β (β0
βͺ {+β}) β ((0[,]π) β© β€) β
β
) |
51 | | fvex 6852 |
. . . . . . . . . 10
β’ ((π Dπ πΉ)βπ) β V |
52 | 51 | dmex 7840 |
. . . . . . . . 9
β’ dom
((π Dπ
πΉ)βπ) β V |
53 | 52 | rgenw 3066 |
. . . . . . . 8
β’
βπ β
((0[,]π) β© β€)dom
((π Dπ
πΉ)βπ) β V |
54 | | iinexg 5296 |
. . . . . . . 8
β’
((((0[,]π) β©
β€) β β
β§ βπ β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ) β V) β β© π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ) β V) |
55 | 50, 53, 54 | sylancl 586 |
. . . . . . 7
β’ (π β (β0
βͺ {+β}) β β© π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ) β V) |
56 | 55 | rgen 3064 |
. . . . . 6
β’
βπ β
(β0 βͺ {+β})β© π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ) β V |
57 | | eqid 2737 |
. . . . . . 7
β’ (π β (β0
βͺ {+β}), π β
β© π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ) β¦ βͺ
π₯ β β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ)))))) = (π β (β0 βͺ
{+β}), π β
β© π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ) β¦ βͺ
π₯ β β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ)))))) |
58 | 57 | mpoexxg 8000 |
. . . . . 6
β’
(((β0 βͺ {+β}) β V β§ βπ β (β0
βͺ {+β})β© π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ) β V) β (π β (β0 βͺ
{+β}), π β
β© π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ) β¦ βͺ
π₯ β β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ)))))) β V) |
59 | 29, 56, 58 | mp2an 690 |
. . . . 5
β’ (π β (β0
βͺ {+β}), π β
β© π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ) β¦ βͺ
π₯ β β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ)))))) β V |
60 | 59 | a1i 11 |
. . . 4
β’ (π β (π β (β0 βͺ
{+β}), π β
β© π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ) β¦ βͺ
π₯ β β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ)))))) β V) |
61 | 3, 17, 19, 20, 26, 60 | ovmpodx 7500 |
. . 3
β’ (π β (π Tayl πΉ) = (π β (β0 βͺ
{+β}), π β
β© π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ) β¦ βͺ
π₯ β β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ))))))) |
62 | | simprl 769 |
. . . . . . . . 9
β’ ((π β§ (π = π β§ π = π΅)) β π = π) |
63 | 62 | oveq2d 7367 |
. . . . . . . 8
β’ ((π β§ (π = π β§ π = π΅)) β (0[,]π) = (0[,]π)) |
64 | 63 | ineq1d 4169 |
. . . . . . 7
β’ ((π β§ (π = π β§ π = π΅)) β ((0[,]π) β© β€) = ((0[,]π) β© β€)) |
65 | | simprr 771 |
. . . . . . . . . 10
β’ ((π β§ (π = π β§ π = π΅)) β π = π΅) |
66 | 65 | fveq2d 6843 |
. . . . . . . . 9
β’ ((π β§ (π = π β§ π = π΅)) β (((π Dπ πΉ)βπ)βπ) = (((π Dπ πΉ)βπ)βπ΅)) |
67 | 66 | oveq1d 7366 |
. . . . . . . 8
β’ ((π β§ (π = π β§ π = π΅)) β ((((π Dπ πΉ)βπ)βπ) / (!βπ)) = ((((π Dπ πΉ)βπ)βπ΅) / (!βπ))) |
68 | 65 | oveq2d 7367 |
. . . . . . . . 9
β’ ((π β§ (π = π β§ π = π΅)) β (π₯ β π) = (π₯ β π΅)) |
69 | 68 | oveq1d 7366 |
. . . . . . . 8
β’ ((π β§ (π = π β§ π = π΅)) β ((π₯ β π)βπ) = ((π₯ β π΅)βπ)) |
70 | 67, 69 | oveq12d 7369 |
. . . . . . 7
β’ ((π β§ (π = π β§ π = π΅)) β (((((π Dπ πΉ)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ)) = (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))) |
71 | 64, 70 | mpteq12dv 5194 |
. . . . . 6
β’ ((π β§ (π = π β§ π = π΅)) β (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ))) = (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) |
72 | 71 | oveq2d 7367 |
. . . . 5
β’ ((π β§ (π = π β§ π = π΅)) β (βfld tsums
(π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ)))) = (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) |
73 | 72 | xpeq2d 5661 |
. . . 4
β’ ((π β§ (π = π β§ π = π΅)) β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ))))) = ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))))) |
74 | 73 | iuneq2d 4981 |
. . 3
β’ ((π β§ (π = π β§ π = π΅)) β βͺ π₯ β β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ) / (!βπ)) Β· ((π₯ β π)βπ))))) = βͺ
π₯ β β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))))) |
75 | | simpr 485 |
. . . . . 6
β’ ((π β§ π = π) β π = π) |
76 | 75 | oveq2d 7367 |
. . . . 5
β’ ((π β§ π = π) β (0[,]π) = (0[,]π)) |
77 | 76 | ineq1d 4169 |
. . . 4
β’ ((π β§ π = π) β ((0[,]π) β© β€) = ((0[,]π) β© β€)) |
78 | | iineq1 4969 |
. . . 4
β’
(((0[,]π) β©
β€) = ((0[,]π) β©
β€) β β© π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ) = β© π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ)) |
79 | 77, 78 | syl 17 |
. . 3
β’ ((π β§ π = π) β β©
π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ) = β© π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ)) |
80 | | taylfval.n |
. . . . 5
β’ (π β (π β β0 β¨ π = +β)) |
81 | | pnfex 11166 |
. . . . . . 7
β’ +β
β V |
82 | 81 | elsn2 4623 |
. . . . . 6
β’ (π β {+β} β π = +β) |
83 | 82 | orbi2i 911 |
. . . . 5
β’ ((π β β0 β¨
π β {+β}) β
(π β
β0 β¨ π
= +β)) |
84 | 80, 83 | sylibr 233 |
. . . 4
β’ (π β (π β β0 β¨ π β
{+β})) |
85 | | elun 4106 |
. . . 4
β’ (π β (β0
βͺ {+β}) β (π
β β0 β¨ π β {+β})) |
86 | 84, 85 | sylibr 233 |
. . 3
β’ (π β π β (β0 βͺ
{+β})) |
87 | | taylfval.b |
. . . . 5
β’ ((π β§ π β ((0[,]π) β© β€)) β π΅ β dom ((π Dπ πΉ)βπ)) |
88 | 87 | ralrimiva 3141 |
. . . 4
β’ (π β βπ β ((0[,]π) β© β€)π΅ β dom ((π Dπ πΉ)βπ)) |
89 | | oveq2 7359 |
. . . . . . . . . 10
β’ (π = π β (0[,]π) = (0[,]π)) |
90 | 89 | ineq1d 4169 |
. . . . . . . . 9
β’ (π = π β ((0[,]π) β© β€) = ((0[,]π) β© β€)) |
91 | 90 | neeq1d 3001 |
. . . . . . . 8
β’ (π = π β (((0[,]π) β© β€) β β
β
((0[,]π) β© β€)
β β
)) |
92 | 91, 50 | vtoclga 3532 |
. . . . . . 7
β’ (π β (β0
βͺ {+β}) β ((0[,]π) β© β€) β
β
) |
93 | 86, 92 | syl 17 |
. . . . . 6
β’ (π β ((0[,]π) β© β€) β
β
) |
94 | | r19.2z 4450 |
. . . . . 6
β’
((((0[,]π) β©
β€) β β
β§ βπ β ((0[,]π) β© β€)π΅ β dom ((π Dπ πΉ)βπ)) β βπ β ((0[,]π) β© β€)π΅ β dom ((π Dπ πΉ)βπ)) |
95 | 93, 88, 94 | syl2anc 584 |
. . . . 5
β’ (π β βπ β ((0[,]π) β© β€)π΅ β dom ((π Dπ πΉ)βπ)) |
96 | | elex 3461 |
. . . . . 6
β’ (π΅ β dom ((π Dπ πΉ)βπ) β π΅ β V) |
97 | 96 | rexlimivw 3146 |
. . . . 5
β’
(βπ β
((0[,]π) β©
β€)π΅ β dom
((π Dπ
πΉ)βπ) β π΅ β V) |
98 | | eliin 4957 |
. . . . 5
β’ (π΅ β V β (π΅ β β© π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ) β βπ β ((0[,]π) β© β€)π΅ β dom ((π Dπ πΉ)βπ))) |
99 | 95, 97, 98 | 3syl 18 |
. . . 4
β’ (π β (π΅ β β©
π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ) β βπ β ((0[,]π) β© β€)π΅ β dom ((π Dπ πΉ)βπ))) |
100 | 88, 99 | mpbird 256 |
. . 3
β’ (π β π΅ β β©
π β ((0[,]π) β© β€)dom ((π Dπ πΉ)βπ)) |
101 | | snssi 4766 |
. . . . . . 7
β’ (π₯ β β β {π₯} β
β) |
102 | 20, 23, 24, 80, 87 | taylfvallem 25669 |
. . . . . . 7
β’ ((π β§ π₯ β β) β
(βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) β β) |
103 | | xpss12 5646 |
. . . . . . 7
β’ (({π₯} β β β§
(βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))) β β) β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) β (β Γ
β)) |
104 | 101, 102,
103 | syl2an2 684 |
. . . . . 6
β’ ((π β§ π₯ β β) β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) β (β Γ
β)) |
105 | 104 | ralrimiva 3141 |
. . . . 5
β’ (π β βπ₯ β β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) β (β Γ
β)) |
106 | | iunss 5003 |
. . . . 5
β’ (βͺ π₯ β β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) β (β Γ β)
β βπ₯ β
β ({π₯} Γ
(βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) β (β Γ
β)) |
107 | 105, 106 | sylibr 233 |
. . . 4
β’ (π β βͺ π₯ β β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) β (β Γ
β)) |
108 | 21, 21 | xpex 7679 |
. . . . 5
β’ (β
Γ β) β V |
109 | 108 | ssex 5276 |
. . . 4
β’ (βͺ π₯ β β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) β (β Γ β)
β βͺ π₯ β β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) β V) |
110 | 107, 109 | syl 17 |
. . 3
β’ (π β βͺ π₯ β β ({π₯} Γ (βfld tsums (π β ((0[,]π) β© β€) β¦ (((((π Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ))))) β V) |
111 | 61, 74, 79, 86, 100, 110 | ovmpodx 7500 |
. 2
β’ (π β (π(π Tayl πΉ)π΅) = βͺ
π₯ β β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))))) |
112 | 1, 111 | eqtrid 2789 |
1
β’ (π β π = βͺ π₯ β β ({π₯} Γ (βfld
tsums (π β ((0[,]π) β© β€) β¦
(((((π
Dπ πΉ)βπ)βπ΅) / (!βπ)) Β· ((π₯ β π΅)βπ)))))) |