Step | Hyp | Ref
| Expression |
1 | | 1red 11163 |
. 2
β’ (π β 1 β
β) |
2 | | rpvmasum.z |
. . 3
β’ π =
(β€/nβ€βπ) |
3 | | rpvmasum.l |
. . 3
β’ πΏ = (β€RHomβπ) |
4 | | rpvmasum.a |
. . 3
β’ (π β π β β) |
5 | | rpvmasum.g |
. . 3
β’ πΊ = (DChrβπ) |
6 | | rpvmasum.d |
. . 3
β’ π· = (BaseβπΊ) |
7 | | rpvmasum.1 |
. . 3
β’ 1 =
(0gβπΊ) |
8 | | dchrisum.b |
. . 3
β’ (π β π β π·) |
9 | | dchrisum.n1 |
. . 3
β’ (π β π β 1 ) |
10 | | dchrvmasum.f |
. . 3
β’ ((π β§ π β β+) β πΉ β
β) |
11 | | dchrvmasum.g |
. . 3
β’ (π = (π₯ / π) β πΉ = πΎ) |
12 | | dchrvmasum.c |
. . 3
β’ (π β πΆ β (0[,)+β)) |
13 | | dchrvmasum.t |
. . 3
β’ (π β π β β) |
14 | | dchrvmasum.1 |
. . 3
β’ ((π β§ π β (3[,)+β)) β
(absβ(πΉ β π)) β€ (πΆ Β· ((logβπ) / π))) |
15 | | dchrvmasum.r |
. . 3
β’ (π β π
β β) |
16 | | dchrvmasum.2 |
. . 3
β’ (π β βπ β (1[,)3)(absβ(πΉ β π)) β€ π
) |
17 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16 | dchrvmasumlem2 26862 |
. 2
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))((absβ(πΎ β π)) / π)) β π(1)) |
18 | | fzfid 13885 |
. . 3
β’ ((π β§ π₯ β β+) β
(1...(ββπ₯))
β Fin) |
19 | 11 | eleq1d 2823 |
. . . . . . 7
β’ (π = (π₯ / π) β (πΉ β β β πΎ β β)) |
20 | 10 | ralrimiva 3144 |
. . . . . . . 8
β’ (π β βπ β β+ πΉ β β) |
21 | 20 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β βπ β
β+ πΉ
β β) |
22 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β π₯ β
β+) |
23 | | elfznn 13477 |
. . . . . . . . 9
β’ (π β
(1...(ββπ₯))
β π β
β) |
24 | 23 | nnrpd 12962 |
. . . . . . . 8
β’ (π β
(1...(ββπ₯))
β π β
β+) |
25 | | rpdivcl 12947 |
. . . . . . . 8
β’ ((π₯ β β+
β§ π β
β+) β (π₯ / π) β
β+) |
26 | 22, 24, 25 | syl2an 597 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β+) |
27 | 19, 21, 26 | rspcdva 3585 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β πΎ β
β) |
28 | 13 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
29 | 27, 28 | subcld 11519 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (πΎ β π) β
β) |
30 | 29 | abscld 15328 |
. . . 4
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(πΎ
β π)) β
β) |
31 | 23 | adantl 483 |
. . . 4
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
32 | 30, 31 | nndivred 12214 |
. . 3
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((absβ(πΎ
β π)) / π) β
β) |
33 | 18, 32 | fsumrecl 15626 |
. 2
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))((absβ(πΎ β π)) / π) β β) |
34 | 8 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β π·) |
35 | | elfzelz 13448 |
. . . . . . 7
β’ (π β
(1...(ββπ₯))
β π β
β€) |
36 | 35 | adantl 483 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β€) |
37 | 5, 2, 6, 3, 34, 36 | dchrzrhcl 26609 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (πβ(πΏβπ)) β β) |
38 | | mucl 26506 |
. . . . . . . . 9
β’ (π β β β
(ΞΌβπ) β
β€) |
39 | 31, 38 | syl 17 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β€) |
40 | 39 | zred 12614 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β) |
41 | 40, 31 | nndivred 12214 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ΞΌβπ) /
π) β
β) |
42 | 41 | recnd 11190 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ΞΌβπ) /
π) β
β) |
43 | 37, 42 | mulcld 11182 |
. . . 4
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) β β) |
44 | 43, 29 | mulcld 11182 |
. . 3
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (πΎ β π)) β β) |
45 | 18, 44 | fsumcl 15625 |
. 2
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (πΎ β π)) β β) |
46 | 45 | abscld 15328 |
. . . 4
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (πΎ β π))) β β) |
47 | 33 | recnd 11190 |
. . . . 5
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))((absβ(πΎ β π)) / π) β β) |
48 | 47 | abscld 15328 |
. . . 4
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))((absβ(πΎ β π)) / π)) β β) |
49 | 44 | abscld 15328 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (πΎ β π))) β β) |
50 | 18, 49 | fsumrecl 15626 |
. . . . 5
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(absβ(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (πΎ β π))) β β) |
51 | 18, 44 | fsumabs 15693 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (πΎ β π))) β€ Ξ£π β (1...(ββπ₯))(absβ(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (πΎ β π)))) |
52 | 43 | abscld 15328 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π))) β β) |
53 | 31 | nnrecred 12211 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 / π) β
β) |
54 | 29 | absge0d 15336 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ (absβ(πΎ
β π))) |
55 | 37, 42 | absmuld 15346 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π))) = ((absβ(πβ(πΏβπ))) Β· (absβ((ΞΌβπ) / π)))) |
56 | 37 | abscld 15328 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(πβ(πΏβπ))) β β) |
57 | | 1red 11163 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 1 β β) |
58 | 42 | abscld 15328 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ((ΞΌβπ) / π)) β β) |
59 | 37 | absge0d 15336 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ (absβ(πβ(πΏβπ)))) |
60 | 42 | absge0d 15336 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ (absβ((ΞΌβπ) / π))) |
61 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(Baseβπ) =
(Baseβπ) |
62 | 4 | nnnn0d 12480 |
. . . . . . . . . . . . . . . 16
β’ (π β π β
β0) |
63 | 2, 61, 3 | znzrhfo 20970 |
. . . . . . . . . . . . . . . 16
β’ (π β β0
β πΏ:β€βontoβ(Baseβπ)) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β πΏ:β€βontoβ(Baseβπ)) |
65 | | fof 6761 |
. . . . . . . . . . . . . . 15
β’ (πΏ:β€βontoβ(Baseβπ) β πΏ:β€βΆ(Baseβπ)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β πΏ:β€βΆ(Baseβπ)) |
67 | 66 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β πΏ:β€βΆ(Baseβπ)) |
68 | 67, 36 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (πΏβπ) β (Baseβπ)) |
69 | 5, 6, 2, 61, 34, 68 | dchrabs2 26626 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(πβ(πΏβπ))) β€ 1) |
70 | 40 | recnd 11190 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β) |
71 | 31 | nncnd 12176 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
72 | 31 | nnne0d 12210 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
0) |
73 | 70, 71, 72 | absdivd 15347 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ((ΞΌβπ) / π)) = ((absβ(ΞΌβπ)) / (absβπ))) |
74 | 31 | nnrpd 12962 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β+) |
75 | 74 | rprege0d 12971 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π β β
β§ 0 β€ π)) |
76 | | absid 15188 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ 0 β€
π) β (absβπ) = π) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβπ) =
π) |
78 | 77 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((absβ(ΞΌβπ)) / (absβπ)) = ((absβ(ΞΌβπ)) / π)) |
79 | 73, 78 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ((ΞΌβπ) / π)) = ((absβ(ΞΌβπ)) / π)) |
80 | 70 | abscld 15328 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(ΞΌβπ)) β β) |
81 | | mule1 26513 |
. . . . . . . . . . . . . 14
β’ (π β β β
(absβ(ΞΌβπ))
β€ 1) |
82 | 31, 81 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(ΞΌβπ)) β€ 1) |
83 | 80, 57, 74, 82 | lediv1dd 13022 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((absβ(ΞΌβπ)) / π) β€ (1 / π)) |
84 | 79, 83 | eqbrtrd 5132 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ((ΞΌβπ) / π)) β€ (1 / π)) |
85 | 56, 57, 58, 53, 59, 60, 69, 84 | lemul12ad 12104 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((absβ(πβ(πΏβπ))) Β· (absβ((ΞΌβπ) / π))) β€ (1 Β· (1 / π))) |
86 | 53 | recnd 11190 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 / π) β
β) |
87 | 86 | mulid2d 11180 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 Β· (1 / π))
= (1 / π)) |
88 | 85, 87 | breqtrd 5136 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((absβ(πβ(πΏβπ))) Β· (absβ((ΞΌβπ) / π))) β€ (1 / π)) |
89 | 55, 88 | eqbrtrd 5132 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π))) β€ (1 / π)) |
90 | 52, 53, 30, 54, 89 | lemul1ad 12101 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((absβ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π))) Β· (absβ(πΎ β π))) β€ ((1 / π) Β· (absβ(πΎ β π)))) |
91 | 43, 29 | absmuld 15346 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (πΎ β π))) = ((absβ((πβ(πΏβπ)) Β· ((ΞΌβπ) / π))) Β· (absβ(πΎ β π)))) |
92 | 30 | recnd 11190 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(πΎ
β π)) β
β) |
93 | 92, 71, 72 | divrec2d 11942 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((absβ(πΎ
β π)) / π) = ((1 / π) Β· (absβ(πΎ β π)))) |
94 | 90, 91, 93 | 3brtr4d 5142 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (πΎ β π))) β€ ((absβ(πΎ β π)) / π)) |
95 | 18, 49, 32, 94 | fsumle 15691 |
. . . . 5
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(absβ(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (πΎ β π))) β€ Ξ£π β (1...(ββπ₯))((absβ(πΎ β π)) / π)) |
96 | 46, 50, 33, 51, 95 | letrd 11319 |
. . . 4
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (πΎ β π))) β€ Ξ£π β (1...(ββπ₯))((absβ(πΎ β π)) / π)) |
97 | 33 | leabsd 15306 |
. . . 4
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))((absβ(πΎ β π)) / π) β€ (absβΞ£π β (1...(ββπ₯))((absβ(πΎ β π)) / π))) |
98 | 46, 33, 48, 96, 97 | letrd 11319 |
. . 3
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (πΎ β π))) β€ (absβΞ£π β
(1...(ββπ₯))((absβ(πΎ β π)) / π))) |
99 | 98 | adantrr 716 |
. 2
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβΞ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (πΎ β π))) β€ (absβΞ£π β
(1...(ββπ₯))((absβ(πΎ β π)) / π))) |
100 | 1, 17, 33, 45, 99 | o1le 15544 |
1
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))(((πβ(πΏβπ)) Β· ((ΞΌβπ) / π)) Β· (πΎ β π))) β π(1)) |