Step | Hyp | Ref
| Expression |
1 | | etransclem2.g |
. . 3
β’ πΊ = (π₯ β β β¦ Ξ£π β (0...π
)(((β Dπ πΉ)βπ)βπ₯)) |
2 | 1 | oveq2i 7416 |
. 2
β’ (β
D πΊ) = (β D (π₯ β β β¦
Ξ£π β (0...π
)(((β
Dπ πΉ)βπ)βπ₯))) |
3 | | eqid 2732 |
. . . 4
β’
(TopOpenββfld) =
(TopOpenββfld) |
4 | 3 | tgioo2 24310 |
. . 3
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
5 | | reelprrecn 11198 |
. . . 4
β’ β
β {β, β} |
6 | 5 | a1i 11 |
. . 3
β’ (π β β β {β,
β}) |
7 | | reopn 43985 |
. . . 4
β’ β
β (topGenβran (,)) |
8 | 7 | a1i 11 |
. . 3
β’ (π β β β
(topGenβran (,))) |
9 | | fzfid 13934 |
. . 3
β’ (π β (0...π
) β Fin) |
10 | | fzelp1 13549 |
. . . . . 6
β’ (π β (0...π
) β π β (0...(π
+ 1))) |
11 | | etransclem2.dvnf |
. . . . . 6
β’ ((π β§ π β (0...(π
+ 1))) β ((β
Dπ πΉ)βπ):ββΆβ) |
12 | 10, 11 | sylan2 593 |
. . . . 5
β’ ((π β§ π β (0...π
)) β ((β Dπ
πΉ)βπ):ββΆβ) |
13 | 12 | 3adant3 1132 |
. . . 4
β’ ((π β§ π β (0...π
) β§ π₯ β β) β ((β
Dπ πΉ)βπ):ββΆβ) |
14 | | simp3 1138 |
. . . 4
β’ ((π β§ π β (0...π
) β§ π₯ β β) β π₯ β β) |
15 | 13, 14 | ffvelcdmd 7084 |
. . 3
β’ ((π β§ π β (0...π
) β§ π₯ β β) β (((β
Dπ πΉ)βπ)βπ₯) β β) |
16 | | fzp1elp1 13550 |
. . . . . 6
β’ (π β (0...π
) β (π + 1) β (0...(π
+ 1))) |
17 | | ovex 7438 |
. . . . . . 7
β’ (π + 1) β V |
18 | | eleq1 2821 |
. . . . . . . . 9
β’ (π = (π + 1) β (π β (0...(π
+ 1)) β (π + 1) β (0...(π
+ 1)))) |
19 | 18 | anbi2d 629 |
. . . . . . . 8
β’ (π = (π + 1) β ((π β§ π β (0...(π
+ 1))) β (π β§ (π + 1) β (0...(π
+ 1))))) |
20 | | fveq2 6888 |
. . . . . . . . 9
β’ (π = (π + 1) β ((β Dπ
πΉ)βπ) = ((β Dπ πΉ)β(π + 1))) |
21 | 20 | feq1d 6699 |
. . . . . . . 8
β’ (π = (π + 1) β (((β Dπ
πΉ)βπ):ββΆβ β ((β
Dπ πΉ)β(π +
1)):ββΆβ)) |
22 | 19, 21 | imbi12d 344 |
. . . . . . 7
β’ (π = (π + 1) β (((π β§ π β (0...(π
+ 1))) β ((β
Dπ πΉ)βπ):ββΆβ) β ((π β§ (π + 1) β (0...(π
+ 1))) β ((β
Dπ πΉ)β(π +
1)):ββΆβ))) |
23 | | eleq1 2821 |
. . . . . . . . . 10
β’ (π = π β (π β (0...(π
+ 1)) β π β (0...(π
+ 1)))) |
24 | 23 | anbi2d 629 |
. . . . . . . . 9
β’ (π = π β ((π β§ π β (0...(π
+ 1))) β (π β§ π β (0...(π
+ 1))))) |
25 | | fveq2 6888 |
. . . . . . . . . 10
β’ (π = π β ((β Dπ πΉ)βπ) = ((β Dπ πΉ)βπ)) |
26 | 25 | feq1d 6699 |
. . . . . . . . 9
β’ (π = π β (((β Dπ
πΉ)βπ):ββΆβ β ((β
Dπ πΉ)βπ):ββΆβ)) |
27 | 24, 26 | imbi12d 344 |
. . . . . . . 8
β’ (π = π β (((π β§ π β (0...(π
+ 1))) β ((β
Dπ πΉ)βπ):ββΆβ) β ((π β§ π β (0...(π
+ 1))) β ((β
Dπ πΉ)βπ):ββΆβ))) |
28 | 27, 11 | chvarvv 2002 |
. . . . . . 7
β’ ((π β§ π β (0...(π
+ 1))) β ((β
Dπ πΉ)βπ):ββΆβ) |
29 | 17, 22, 28 | vtocl 3549 |
. . . . . 6
β’ ((π β§ (π + 1) β (0...(π
+ 1))) β ((β
Dπ πΉ)β(π +
1)):ββΆβ) |
30 | 16, 29 | sylan2 593 |
. . . . 5
β’ ((π β§ π β (0...π
)) β ((β Dπ
πΉ)β(π +
1)):ββΆβ) |
31 | 30 | 3adant3 1132 |
. . . 4
β’ ((π β§ π β (0...π
) β§ π₯ β β) β ((β
Dπ πΉ)β(π +
1)):ββΆβ) |
32 | 31, 14 | ffvelcdmd 7084 |
. . 3
β’ ((π β§ π β (0...π
) β§ π₯ β β) β (((β
Dπ πΉ)β(π + 1))βπ₯) β β) |
33 | 12 | ffnd 6715 |
. . . . . . 7
β’ ((π β§ π β (0...π
)) β ((β Dπ
πΉ)βπ) Fn β) |
34 | | nfcv 2903 |
. . . . . . . . . 10
β’
β²π₯β |
35 | | nfcv 2903 |
. . . . . . . . . 10
β’
β²π₯
Dπ |
36 | | etransclem2.xf |
. . . . . . . . . 10
β’
β²π₯πΉ |
37 | 34, 35, 36 | nfov 7435 |
. . . . . . . . 9
β’
β²π₯(β Dπ πΉ) |
38 | | nfcv 2903 |
. . . . . . . . 9
β’
β²π₯π |
39 | 37, 38 | nffv 6898 |
. . . . . . . 8
β’
β²π₯((β Dπ πΉ)βπ) |
40 | 39 | dffn5f 6960 |
. . . . . . 7
β’
(((β Dπ πΉ)βπ) Fn β β ((β
Dπ πΉ)βπ) = (π₯ β β β¦ (((β
Dπ πΉ)βπ)βπ₯))) |
41 | 33, 40 | sylib 217 |
. . . . . 6
β’ ((π β§ π β (0...π
)) β ((β Dπ
πΉ)βπ) = (π₯ β β β¦ (((β
Dπ πΉ)βπ)βπ₯))) |
42 | 41 | eqcomd 2738 |
. . . . 5
β’ ((π β§ π β (0...π
)) β (π₯ β β β¦ (((β
Dπ πΉ)βπ)βπ₯)) = ((β Dπ πΉ)βπ)) |
43 | 42 | oveq2d 7421 |
. . . 4
β’ ((π β§ π β (0...π
)) β (β D (π₯ β β β¦ (((β
Dπ πΉ)βπ)βπ₯))) = (β D ((β
Dπ πΉ)βπ))) |
44 | | ax-resscn 11163 |
. . . . . 6
β’ β
β β |
45 | 44 | a1i 11 |
. . . . 5
β’ ((π β§ π β (0...π
)) β β β
β) |
46 | | etransclem2.f |
. . . . . . . 8
β’ (π β πΉ:ββΆβ) |
47 | | ffdm 6744 |
. . . . . . . 8
β’ (πΉ:ββΆβ β
(πΉ:dom πΉβΆβ β§ dom πΉ β β)) |
48 | 46, 47 | syl 17 |
. . . . . . 7
β’ (π β (πΉ:dom πΉβΆβ β§ dom πΉ β β)) |
49 | | cnex 11187 |
. . . . . . . . 9
β’ β
β V |
50 | 49 | a1i 11 |
. . . . . . . 8
β’ (π β β β
V) |
51 | | reex 11197 |
. . . . . . . 8
β’ β
β V |
52 | | elpm2g 8834 |
. . . . . . . 8
β’ ((β
β V β§ β β V) β (πΉ β (β βpm
β) β (πΉ:dom
πΉβΆβ β§ dom
πΉ β
β))) |
53 | 50, 51, 52 | sylancl 586 |
. . . . . . 7
β’ (π β (πΉ β (β βpm
β) β (πΉ:dom
πΉβΆβ β§ dom
πΉ β
β))) |
54 | 48, 53 | mpbird 256 |
. . . . . 6
β’ (π β πΉ β (β βpm
β)) |
55 | 54 | adantr 481 |
. . . . 5
β’ ((π β§ π β (0...π
)) β πΉ β (β βpm
β)) |
56 | | elfznn0 13590 |
. . . . . 6
β’ (π β (0...π
) β π β β0) |
57 | 56 | adantl 482 |
. . . . 5
β’ ((π β§ π β (0...π
)) β π β β0) |
58 | | dvnp1 25433 |
. . . . 5
β’ ((β
β β β§ πΉ
β (β βpm β) β§ π β β0) β ((β
Dπ πΉ)β(π + 1)) = (β D ((β
Dπ πΉ)βπ))) |
59 | 45, 55, 57, 58 | syl3anc 1371 |
. . . 4
β’ ((π β§ π β (0...π
)) β ((β Dπ
πΉ)β(π + 1)) = (β D ((β
Dπ πΉ)βπ))) |
60 | 30 | ffnd 6715 |
. . . . 5
β’ ((π β§ π β (0...π
)) β ((β Dπ
πΉ)β(π + 1)) Fn
β) |
61 | | nfcv 2903 |
. . . . . . 7
β’
β²π₯(π + 1) |
62 | 37, 61 | nffv 6898 |
. . . . . 6
β’
β²π₯((β Dπ πΉ)β(π + 1)) |
63 | 62 | dffn5f 6960 |
. . . . 5
β’
(((β Dπ πΉ)β(π + 1)) Fn β β ((β
Dπ πΉ)β(π + 1)) = (π₯ β β β¦ (((β
Dπ πΉ)β(π + 1))βπ₯))) |
64 | 60, 63 | sylib 217 |
. . . 4
β’ ((π β§ π β (0...π
)) β ((β Dπ
πΉ)β(π + 1)) = (π₯ β β β¦ (((β
Dπ πΉ)β(π + 1))βπ₯))) |
65 | 43, 59, 64 | 3eqtr2d 2778 |
. . 3
β’ ((π β§ π β (0...π
)) β (β D (π₯ β β β¦ (((β
Dπ πΉ)βπ)βπ₯))) = (π₯ β β β¦ (((β
Dπ πΉ)β(π + 1))βπ₯))) |
66 | 4, 3, 6, 8, 9, 15,
32, 65 | dvmptfsum 25483 |
. 2
β’ (π β (β D (π₯ β β β¦
Ξ£π β (0...π
)(((β
Dπ πΉ)βπ)βπ₯))) = (π₯ β β β¦ Ξ£π β (0...π
)(((β Dπ πΉ)β(π + 1))βπ₯))) |
67 | 2, 66 | eqtrid 2784 |
1
β’ (π β (β D πΊ) = (π₯ β β β¦ Ξ£π β (0...π
)(((β Dπ πΉ)β(π + 1))βπ₯))) |