Step | Hyp | Ref
| Expression |
1 | | fzofi 13886 |
. . 3
β’
(0..^π) β
Fin |
2 | | fzofi 13886 |
. . . . . . 7
β’
(0..^π’) β
Fin |
3 | 2 | a1i 11 |
. . . . . 6
β’ (π β (0..^π’) β Fin) |
4 | | rpvmasum.g |
. . . . . . 7
β’ πΊ = (DChrβπ) |
5 | | rpvmasum.z |
. . . . . . 7
β’ π =
(β€/nβ€βπ) |
6 | | rpvmasum.d |
. . . . . . 7
β’ π· = (BaseβπΊ) |
7 | | rpvmasum.l |
. . . . . . 7
β’ πΏ = (β€RHomβπ) |
8 | | dchrisum.b |
. . . . . . . 8
β’ (π β π β π·) |
9 | 8 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0..^π’)) β π β π·) |
10 | | elfzoelz 13579 |
. . . . . . . 8
β’ (π β (0..^π’) β π β β€) |
11 | 10 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (0..^π’)) β π β β€) |
12 | 4, 5, 6, 7, 9, 11 | dchrzrhcl 26609 |
. . . . . 6
β’ ((π β§ π β (0..^π’)) β (πβ(πΏβπ)) β β) |
13 | 3, 12 | fsumcl 15625 |
. . . . 5
β’ (π β Ξ£π β (0..^π’)(πβ(πΏβπ)) β β) |
14 | 13 | abscld 15328 |
. . . 4
β’ (π β (absβΞ£π β (0..^π’)(πβ(πΏβπ))) β β) |
15 | 14 | ralrimivw 3148 |
. . 3
β’ (π β βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β β) |
16 | | fimaxre3 12108 |
. . 3
β’
(((0..^π) β Fin
β§ βπ’ β
(0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β β) β βπ β β βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π) |
17 | 1, 15, 16 | sylancr 588 |
. 2
β’ (π β βπ β β βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π) |
18 | | rpvmasum.a |
. . . 4
β’ (π β π β β) |
19 | 18 | adantr 482 |
. . 3
β’ ((π β§ (π β β β§ βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π)) β π β β) |
20 | | rpvmasum.1 |
. . 3
β’ 1 =
(0gβπΊ) |
21 | 8 | adantr 482 |
. . 3
β’ ((π β§ (π β β β§ βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π)) β π β π·) |
22 | | dchrisum.n1 |
. . . 4
β’ (π β π β 1 ) |
23 | 22 | adantr 482 |
. . 3
β’ ((π β§ (π β β β§ βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π)) β π β 1 ) |
24 | | dchrisum.2 |
. . 3
β’ (π = π₯ β π΄ = π΅) |
25 | | dchrisum.3 |
. . . 4
β’ (π β π β β) |
26 | 25 | adantr 482 |
. . 3
β’ ((π β§ (π β β β§ βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π)) β π β β) |
27 | | dchrisum.4 |
. . . 4
β’ ((π β§ π β β+) β π΄ β
β) |
28 | 27 | adantlr 714 |
. . 3
β’ (((π β§ (π β β β§ βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π)) β§ π β β+) β π΄ β
β) |
29 | | dchrisum.5 |
. . . 4
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (π β€ π β§ π β€ π₯)) β π΅ β€ π΄) |
30 | 29 | 3adant1r 1178 |
. . 3
β’ (((π β§ (π β β β§ βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π)) β§ (π β β+ β§ π₯ β β+)
β§ (π β€ π β§ π β€ π₯)) β π΅ β€ π΄) |
31 | | dchrisum.6 |
. . . 4
β’ (π β (π β β+ β¦ π΄) βπ
0) |
32 | 31 | adantr 482 |
. . 3
β’ ((π β§ (π β β β§ βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π)) β (π β β+ β¦ π΄) βπ
0) |
33 | | dchrisum.7 |
. . 3
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) Β· π΄)) |
34 | | simprl 770 |
. . 3
β’ ((π β§ (π β β β§ βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π)) β π β β) |
35 | | simprr 772 |
. . . 4
β’ ((π β§ (π β β β§ βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π)) β βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π) |
36 | | 2fveq3 6852 |
. . . . . . . . 9
β’ (π = π β (πβ(πΏβπ)) = (πβ(πΏβπ))) |
37 | 36 | cbvsumv 15588 |
. . . . . . . 8
β’
Ξ£π β
(0..^π’)(πβ(πΏβπ)) = Ξ£π β (0..^π’)(πβ(πΏβπ)) |
38 | | oveq2 7370 |
. . . . . . . . 9
β’ (π’ = π β (0..^π’) = (0..^π)) |
39 | 38 | sumeq1d 15593 |
. . . . . . . 8
β’ (π’ = π β Ξ£π β (0..^π’)(πβ(πΏβπ)) = Ξ£π β (0..^π)(πβ(πΏβπ))) |
40 | 37, 39 | eqtrid 2789 |
. . . . . . 7
β’ (π’ = π β Ξ£π β (0..^π’)(πβ(πΏβπ)) = Ξ£π β (0..^π)(πβ(πΏβπ))) |
41 | 40 | fveq2d 6851 |
. . . . . 6
β’ (π’ = π β (absβΞ£π β (0..^π’)(πβ(πΏβπ))) = (absβΞ£π β (0..^π)(πβ(πΏβπ)))) |
42 | 41 | breq1d 5120 |
. . . . 5
β’ (π’ = π β ((absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π β (absβΞ£π β (0..^π)(πβ(πΏβπ))) β€ π)) |
43 | 42 | cbvralvw 3228 |
. . . 4
β’
(βπ’ β
(0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π β βπ β (0..^π)(absβΞ£π β (0..^π)(πβ(πΏβπ))) β€ π) |
44 | 35, 43 | sylib 217 |
. . 3
β’ ((π β§ (π β β β§ βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π)) β βπ β (0..^π)(absβΞ£π β (0..^π)(πβ(πΏβπ))) β€ π) |
45 | 5, 7, 19, 4, 6, 20, 21, 23, 24, 26, 28, 30, 32, 33, 34, 44 | dchrisumlem3 26855 |
. 2
β’ ((π β§ (π β β β§ βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π)) β βπ‘βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ₯ β (π[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π Β· π΅))) |
46 | 17, 45 | rexlimddv 3159 |
1
β’ (π β βπ‘βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ₯ β (π[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π Β· π΅))) |