Step | Hyp | Ref
| Expression |
1 | | pserf.g |
. . 3
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) |
2 | | pserf.f |
. . 3
β’ πΉ = (π¦ β π β¦ Ξ£π β β0 ((πΊβπ¦)βπ)) |
3 | | pserf.a |
. . 3
β’ (π β π΄:β0βΆβ) |
4 | | pserf.r |
. . 3
β’ π
= sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*,
< ) |
5 | | psercn.s |
. . 3
β’ π = (β‘abs β (0[,)π
)) |
6 | | psercn.m |
. . 3
β’ π = if(π
β β, (((absβπ) + π
) / 2), ((absβπ) + 1)) |
7 | | pserdv.b |
. . 3
β’ π΅ = (0(ballβ(abs β
β ))(((absβπ) +
π) / 2)) |
8 | 1, 2, 3, 4, 5, 6, 7 | pserdv 25804 |
. 2
β’ (π β (β D πΉ) = (π¦ β π β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ)))) |
9 | | nn0uz 12812 |
. . . . 5
β’
β0 = (β€β₯β0) |
10 | | nnuz 12813 |
. . . . . 6
β’ β =
(β€β₯β1) |
11 | | 1e0p1 12667 |
. . . . . . 7
β’ 1 = (0 +
1) |
12 | 11 | fveq2i 6850 |
. . . . . 6
β’
(β€β₯β1) = (β€β₯β(0 +
1)) |
13 | 10, 12 | eqtri 2765 |
. . . . 5
β’ β =
(β€β₯β(0 + 1)) |
14 | | id 22 |
. . . . . . 7
β’ (π = (1 + π) β π = (1 + π)) |
15 | | fveq2 6847 |
. . . . . . 7
β’ (π = (1 + π) β (π΄βπ) = (π΄β(1 + π))) |
16 | 14, 15 | oveq12d 7380 |
. . . . . 6
β’ (π = (1 + π) β (π Β· (π΄βπ)) = ((1 + π) Β· (π΄β(1 + π)))) |
17 | | oveq1 7369 |
. . . . . . 7
β’ (π = (1 + π) β (π β 1) = ((1 + π) β 1)) |
18 | 17 | oveq2d 7378 |
. . . . . 6
β’ (π = (1 + π) β (π¦β(π β 1)) = (π¦β((1 + π) β 1))) |
19 | 16, 18 | oveq12d 7380 |
. . . . 5
β’ (π = (1 + π) β ((π Β· (π΄βπ)) Β· (π¦β(π β 1))) = (((1 + π) Β· (π΄β(1 + π))) Β· (π¦β((1 + π) β 1)))) |
20 | | 1zzd 12541 |
. . . . 5
β’ ((π β§ π¦ β π) β 1 β β€) |
21 | | 0zd 12518 |
. . . . 5
β’ ((π β§ π¦ β π) β 0 β β€) |
22 | | nncn 12168 |
. . . . . . . 8
β’ (π β β β π β
β) |
23 | 22 | adantl 483 |
. . . . . . 7
β’ (((π β§ π¦ β π) β§ π β β) β π β β) |
24 | 3 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β π΄:β0βΆβ) |
25 | | nnnn0 12427 |
. . . . . . . 8
β’ (π β β β π β
β0) |
26 | | ffvelcdm 7037 |
. . . . . . . 8
β’ ((π΄:β0βΆβ β§
π β
β0) β (π΄βπ) β β) |
27 | 24, 25, 26 | syl2an 597 |
. . . . . . 7
β’ (((π β§ π¦ β π) β§ π β β) β (π΄βπ) β β) |
28 | 23, 27 | mulcld 11182 |
. . . . . 6
β’ (((π β§ π¦ β π) β§ π β β) β (π Β· (π΄βπ)) β β) |
29 | | cnvimass 6038 |
. . . . . . . . . . 11
β’ (β‘abs β (0[,)π
)) β dom abs |
30 | | absf 15229 |
. . . . . . . . . . . 12
β’
abs:ββΆβ |
31 | 30 | fdmi 6685 |
. . . . . . . . . . 11
β’ dom abs =
β |
32 | 29, 31 | sseqtri 3985 |
. . . . . . . . . 10
β’ (β‘abs β (0[,)π
)) β β |
33 | 5, 32 | eqsstri 3983 |
. . . . . . . . 9
β’ π β
β |
34 | 33 | a1i 11 |
. . . . . . . 8
β’ (π β π β β) |
35 | 34 | sselda 3949 |
. . . . . . 7
β’ ((π β§ π¦ β π) β π¦ β β) |
36 | | nnm1nn0 12461 |
. . . . . . 7
β’ (π β β β (π β 1) β
β0) |
37 | | expcl 13992 |
. . . . . . 7
β’ ((π¦ β β β§ (π β 1) β
β0) β (π¦β(π β 1)) β β) |
38 | 35, 36, 37 | syl2an 597 |
. . . . . 6
β’ (((π β§ π¦ β π) β§ π β β) β (π¦β(π β 1)) β β) |
39 | 28, 38 | mulcld 11182 |
. . . . 5
β’ (((π β§ π¦ β π) β§ π β β) β ((π Β· (π΄βπ)) Β· (π¦β(π β 1))) β
β) |
40 | 9, 13, 19, 20, 21, 39 | isumshft 15731 |
. . . 4
β’ ((π β§ π¦ β π) β Ξ£π β β ((π Β· (π΄βπ)) Β· (π¦β(π β 1))) = Ξ£π β β0 (((1 + π) Β· (π΄β(1 + π))) Β· (π¦β((1 + π) β 1)))) |
41 | | ax-1cn 11116 |
. . . . . . . 8
β’ 1 β
β |
42 | | nn0cn 12430 |
. . . . . . . . 9
β’ (π β β0
β π β
β) |
43 | 42 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π¦ β π) β§ π β β0) β π β
β) |
44 | | addcom 11348 |
. . . . . . . 8
β’ ((1
β β β§ π
β β) β (1 + π) = (π + 1)) |
45 | 41, 43, 44 | sylancr 588 |
. . . . . . 7
β’ (((π β§ π¦ β π) β§ π β β0) β (1 +
π) = (π + 1)) |
46 | 45 | fveq2d 6851 |
. . . . . . 7
β’ (((π β§ π¦ β π) β§ π β β0) β (π΄β(1 + π)) = (π΄β(π + 1))) |
47 | 45, 46 | oveq12d 7380 |
. . . . . 6
β’ (((π β§ π¦ β π) β§ π β β0) β ((1 +
π) Β· (π΄β(1 + π))) = ((π + 1) Β· (π΄β(π + 1)))) |
48 | | pncan2 11415 |
. . . . . . . 8
β’ ((1
β β β§ π
β β) β ((1 + π) β 1) = π) |
49 | 41, 43, 48 | sylancr 588 |
. . . . . . 7
β’ (((π β§ π¦ β π) β§ π β β0) β ((1 +
π) β 1) = π) |
50 | 49 | oveq2d 7378 |
. . . . . 6
β’ (((π β§ π¦ β π) β§ π β β0) β (π¦β((1 + π) β 1)) = (π¦βπ)) |
51 | 47, 50 | oveq12d 7380 |
. . . . 5
β’ (((π β§ π¦ β π) β§ π β β0) β (((1 +
π) Β· (π΄β(1 + π))) Β· (π¦β((1 + π) β 1))) = (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ))) |
52 | 51 | sumeq2dv 15595 |
. . . 4
β’ ((π β§ π¦ β π) β Ξ£π β β0 (((1 + π) Β· (π΄β(1 + π))) Β· (π¦β((1 + π) β 1))) = Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ))) |
53 | 40, 52 | eqtr2d 2778 |
. . 3
β’ ((π β§ π¦ β π) β Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ)) = Ξ£π β β ((π Β· (π΄βπ)) Β· (π¦β(π β 1)))) |
54 | 53 | mpteq2dva 5210 |
. 2
β’ (π β (π¦ β π β¦ Ξ£π β β0 (((π + 1) Β· (π΄β(π + 1))) Β· (π¦βπ))) = (π¦ β π β¦ Ξ£π β β ((π Β· (π΄βπ)) Β· (π¦β(π β 1))))) |
55 | 8, 54 | eqtrd 2777 |
1
β’ (π β (β D πΉ) = (π¦ β π β¦ Ξ£π β β ((π Β· (π΄βπ)) Β· (π¦β(π β 1))))) |