Step | Hyp | Ref
| Expression |
1 | | dvfcn 25424 |
. . . . 5
β’ (β
D πΉ):dom (β D πΉ)βΆβ |
2 | | ssidd 4005 |
. . . . . . . 8
β’ (π β β β
β) |
3 | | pserf.g |
. . . . . . . . . 10
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) |
4 | | pserf.f |
. . . . . . . . . 10
β’ πΉ = (π¦ β π β¦ Ξ£π β β0 ((πΊβπ¦)βπ)) |
5 | | pserf.a |
. . . . . . . . . 10
β’ (π β π΄:β0βΆβ) |
6 | | pserf.r |
. . . . . . . . . 10
β’ π
= sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*,
< ) |
7 | | psercn.s |
. . . . . . . . . 10
β’ π = (β‘abs β (0[,)π
)) |
8 | | psercn.m |
. . . . . . . . . 10
β’ π = if(π
β β, (((absβπ) + π
) / 2), ((absβπ) + 1)) |
9 | 3, 4, 5, 6, 7, 8 | psercn 25937 |
. . . . . . . . 9
β’ (π β πΉ β (πβcnββ)) |
10 | | cncff 24408 |
. . . . . . . . 9
β’ (πΉ β (πβcnββ) β πΉ:πβΆβ) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
β’ (π β πΉ:πβΆβ) |
12 | | cnvimass 6080 |
. . . . . . . . . . 11
β’ (β‘abs β (0[,)π
)) β dom abs |
13 | | absf 15283 |
. . . . . . . . . . . 12
β’
abs:ββΆβ |
14 | 13 | fdmi 6729 |
. . . . . . . . . . 11
β’ dom abs =
β |
15 | 12, 14 | sseqtri 4018 |
. . . . . . . . . 10
β’ (β‘abs β (0[,)π
)) β β |
16 | 7, 15 | eqsstri 4016 |
. . . . . . . . 9
β’ π β
β |
17 | 16 | a1i 11 |
. . . . . . . 8
β’ (π β π β β) |
18 | 2, 11, 17 | dvbss 25417 |
. . . . . . 7
β’ (π β dom (β D πΉ) β π) |
19 | | ssidd 4005 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β β β
β) |
20 | 11 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β πΉ:πβΆβ) |
21 | 16 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β π β β) |
22 | | pserdv.b |
. . . . . . . . . . . 12
β’ π΅ = (0(ballβ(abs β
β ))(((absβπ) +
π) / 2)) |
23 | | cnxmet 24288 |
. . . . . . . . . . . . 13
β’ (abs
β β ) β (βMetββ) |
24 | | 0cnd 11206 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β 0 β β) |
25 | 17 | sselda 3982 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π) β π β β) |
26 | 25 | abscld 15382 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β (absβπ) β β) |
27 | 3, 4, 5, 6, 7, 8 | psercnlem1 25936 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π) β (π β β+ β§
(absβπ) < π β§ π < π
)) |
28 | 27 | simp1d 1142 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π) β π β
β+) |
29 | 28 | rpred 13015 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β π β β) |
30 | 26, 29 | readdcld 11242 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β ((absβπ) + π) β β) |
31 | | 0red 11216 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β 0 β β) |
32 | 25 | absge0d 15390 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β 0 β€ (absβπ)) |
33 | 26, 28 | ltaddrpd 13048 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β (absβπ) < ((absβπ) + π)) |
34 | 31, 26, 30, 32, 33 | lelttrd 11371 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β 0 < ((absβπ) + π)) |
35 | 30, 34 | elrpd 13012 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β ((absβπ) + π) β
β+) |
36 | 35 | rphalfcld 13027 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β (((absβπ) + π) / 2) β
β+) |
37 | 36 | rpxrd 13016 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (((absβπ) + π) / 2) β
β*) |
38 | | blssm 23923 |
. . . . . . . . . . . . 13
β’ (((abs
β β ) β (βMetββ) β§ 0 β β
β§ (((absβπ) +
π) / 2) β
β*) β (0(ballβ(abs β β
))(((absβπ) + π) / 2)) β
β) |
39 | 23, 24, 37, 38 | mp3an2i 1466 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (0(ballβ(abs β β
))(((absβπ) + π) / 2)) β
β) |
40 | 22, 39 | eqsstrid 4030 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β π΅ β β) |
41 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(TopOpenββfld) =
(TopOpenββfld) |
42 | 41 | cnfldtopon 24298 |
. . . . . . . . . . . . 13
β’
(TopOpenββfld) β
(TopOnββ) |
43 | 42 | toponrestid 22422 |
. . . . . . . . . . . 12
β’
(TopOpenββfld) =
((TopOpenββfld) βΎt
β) |
44 | 41, 43 | dvres 25427 |
. . . . . . . . . . 11
β’
(((β β β β§ πΉ:πβΆβ) β§ (π β β β§ π΅ β β)) β (β D (πΉ βΎ π΅)) = ((β D πΉ) βΎ
((intβ(TopOpenββfld))βπ΅))) |
45 | 19, 20, 21, 40, 44 | syl22anc 837 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (β D (πΉ βΎ π΅)) = ((β D πΉ) βΎ
((intβ(TopOpenββfld))βπ΅))) |
46 | | resss 6006 |
. . . . . . . . . 10
β’ ((β
D πΉ) βΎ
((intβ(TopOpenββfld))βπ΅)) β (β D πΉ) |
47 | 45, 46 | eqsstrdi 4036 |
. . . . . . . . 9
β’ ((π β§ π β π) β (β D (πΉ βΎ π΅)) β (β D πΉ)) |
48 | | dmss 5902 |
. . . . . . . . 9
β’ ((β
D (πΉ βΎ π΅)) β (β D πΉ) β dom (β D (πΉ βΎ π΅)) β dom (β D πΉ)) |
49 | 47, 48 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β π) β dom (β D (πΉ βΎ π΅)) β dom (β D πΉ)) |
50 | 3, 4, 5, 6, 7, 8 | pserdvlem1 25938 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β ((((absβπ) + π) / 2) β β+ β§
(absβπ) <
(((absβπ) + π) / 2) β§ (((absβπ) + π) / 2) < π
)) |
51 | 3, 4, 5, 6, 7, 50 | psercnlem2 25935 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (π β (0(ballβ(abs β β
))(((absβπ) + π) / 2)) β§ (0(ballβ(abs
β β ))(((absβπ) + π) / 2)) β (β‘abs β (0[,](((absβπ) + π) / 2))) β§ (β‘abs β (0[,](((absβπ) + π) / 2))) β π)) |
52 | 51 | simp1d 1142 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β (0(ballβ(abs β β
))(((absβπ) + π) / 2))) |
53 | 52, 22 | eleqtrrdi 2844 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β π΅) |
54 | 3, 4, 5, 6, 7, 8, 22 | pserdvlem2 25939 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (β D (πΉ βΎ π΅)) = (π¦ β π΅ β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ)))) |
55 | 54 | dmeqd 5905 |
. . . . . . . . . 10
β’ ((π β§ π β π) β dom (β D (πΉ βΎ π΅)) = dom (π¦ β π΅ β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ)))) |
56 | | dmmptg 6241 |
. . . . . . . . . . 11
β’
(βπ¦ β
π΅ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ)) β V β dom (π¦ β π΅ β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ))) = π΅) |
57 | | sumex 15633 |
. . . . . . . . . . . 12
β’
Ξ£π β
β0 (((π +
1) Β· (π΄β(π + 1))) Β· (π¦βπ)) β V |
58 | 57 | a1i 11 |
. . . . . . . . . . 11
β’ (π¦ β π΅ β Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ)) β V) |
59 | 56, 58 | mprg 3067 |
. . . . . . . . . 10
β’ dom
(π¦ β π΅ β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ))) = π΅ |
60 | 55, 59 | eqtrdi 2788 |
. . . . . . . . 9
β’ ((π β§ π β π) β dom (β D (πΉ βΎ π΅)) = π΅) |
61 | 53, 60 | eleqtrrd 2836 |
. . . . . . . 8
β’ ((π β§ π β π) β π β dom (β D (πΉ βΎ π΅))) |
62 | 49, 61 | sseldd 3983 |
. . . . . . 7
β’ ((π β§ π β π) β π β dom (β D πΉ)) |
63 | 18, 62 | eqelssd 4003 |
. . . . . 6
β’ (π β dom (β D πΉ) = π) |
64 | 63 | feq2d 6703 |
. . . . 5
β’ (π β ((β D πΉ):dom (β D πΉ)βΆβ β (β
D πΉ):πβΆβ)) |
65 | 1, 64 | mpbii 232 |
. . . 4
β’ (π β (β D πΉ):πβΆβ) |
66 | 65 | feqmptd 6960 |
. . 3
β’ (π β (β D πΉ) = (π β π β¦ ((β D πΉ)βπ))) |
67 | | ffun 6720 |
. . . . . . 7
β’ ((β
D πΉ):dom (β D πΉ)βΆβ β Fun
(β D πΉ)) |
68 | 1, 67 | mp1i 13 |
. . . . . 6
β’ ((π β§ π β π) β Fun (β D πΉ)) |
69 | | funssfv 6912 |
. . . . . 6
β’ ((Fun
(β D πΉ) β§
(β D (πΉ βΎ π΅)) β (β D πΉ) β§ π β dom (β D (πΉ βΎ π΅))) β ((β D πΉ)βπ) = ((β D (πΉ βΎ π΅))βπ)) |
70 | 68, 47, 61, 69 | syl3anc 1371 |
. . . . 5
β’ ((π β§ π β π) β ((β D πΉ)βπ) = ((β D (πΉ βΎ π΅))βπ)) |
71 | 54 | fveq1d 6893 |
. . . . 5
β’ ((π β§ π β π) β ((β D (πΉ βΎ π΅))βπ) = ((π¦ β π΅ β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ)))βπ)) |
72 | | oveq1 7415 |
. . . . . . . . 9
β’ (π¦ = π β (π¦βπ) = (πβπ)) |
73 | 72 | oveq2d 7424 |
. . . . . . . 8
β’ (π¦ = π β (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ)) = (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ))) |
74 | 73 | sumeq2sdv 15649 |
. . . . . . 7
β’ (π¦ = π β Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ)) = Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ))) |
75 | | eqid 2732 |
. . . . . . 7
β’ (π¦ β π΅ β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ))) = (π¦ β π΅ β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ))) |
76 | | sumex 15633 |
. . . . . . 7
β’
Ξ£π β
β0 (((π +
1) Β· (π΄β(π + 1))) Β· (πβπ)) β V |
77 | 74, 75, 76 | fvmpt 6998 |
. . . . . 6
β’ (π β π΅ β ((π¦ β π΅ β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ)))βπ) = Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ))) |
78 | 53, 77 | syl 17 |
. . . . 5
β’ ((π β§ π β π) β ((π¦ β π΅ β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ)))βπ) = Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ))) |
79 | 70, 71, 78 | 3eqtrd 2776 |
. . . 4
β’ ((π β§ π β π) β ((β D πΉ)βπ) = Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ))) |
80 | 79 | mpteq2dva 5248 |
. . 3
β’ (π β (π β π β¦ ((β D πΉ)βπ)) = (π β π β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ)))) |
81 | 66, 80 | eqtrd 2772 |
. 2
β’ (π β (β D πΉ) = (π β π β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ)))) |
82 | | oveq1 7415 |
. . . . 5
β’ (π = π¦ β (πβπ) = (π¦βπ)) |
83 | 82 | oveq2d 7424 |
. . . 4
β’ (π = π¦ β (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ)) = (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ))) |
84 | 83 | sumeq2sdv 15649 |
. . 3
β’ (π = π¦ β Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ)) = Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ))) |
85 | 84 | cbvmptv 5261 |
. 2
β’ (π β π β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (πβπ))) = (π¦ β π β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ))) |
86 | 81, 85 | eqtrdi 2788 |
1
β’ (π β (β D πΉ) = (π¦ β π β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ)))) |