Step |
Hyp |
Ref |
Expression |
1 |
|
rpvmasum.z |
|- Z = ( Z/nZ ` N ) |
2 |
|
rpvmasum.l |
|- L = ( ZRHom ` Z ) |
3 |
|
rpvmasum.a |
|- ( ph -> N e. NN ) |
4 |
|
rpvmasum.g |
|- G = ( DChr ` N ) |
5 |
|
rpvmasum.d |
|- D = ( Base ` G ) |
6 |
|
rpvmasum.1 |
|- .1. = ( 0g ` G ) |
7 |
|
dchrisum.b |
|- ( ph -> X e. D ) |
8 |
|
dchrisum.n1 |
|- ( ph -> X =/= .1. ) |
9 |
|
dchrisumn0.f |
|- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) |
10 |
|
dchrisumn0.c |
|- ( ph -> C e. ( 0 [,) +oo ) ) |
11 |
|
dchrisumn0.t |
|- ( ph -> seq 1 ( + , F ) ~~> T ) |
12 |
|
dchrisumn0.1 |
|- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - T ) ) <_ ( C / y ) ) |
13 |
|
rpssre |
|- RR+ C_ RR |
14 |
|
ax-1cn |
|- 1 e. CC |
15 |
|
o1const |
|- ( ( RR+ C_ RR /\ 1 e. CC ) -> ( x e. RR+ |-> 1 ) e. O(1) ) |
16 |
13 14 15
|
mp2an |
|- ( x e. RR+ |-> 1 ) e. O(1) |
17 |
16
|
a1i |
|- ( ph -> ( x e. RR+ |-> 1 ) e. O(1) ) |
18 |
14
|
a1i |
|- ( ( ph /\ x e. RR+ ) -> 1 e. CC ) |
19 |
|
fzfid |
|- ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin ) |
20 |
7
|
ad2antrr |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> X e. D ) |
21 |
|
elfzelz |
|- ( d e. ( 1 ... ( |_ ` x ) ) -> d e. ZZ ) |
22 |
21
|
adantl |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. ZZ ) |
23 |
4 1 5 2 20 22
|
dchrzrhcl |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( X ` ( L ` d ) ) e. CC ) |
24 |
|
elfznn |
|- ( d e. ( 1 ... ( |_ ` x ) ) -> d e. NN ) |
25 |
24
|
adantl |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. NN ) |
26 |
|
mucl |
|- ( d e. NN -> ( mmu ` d ) e. ZZ ) |
27 |
26
|
zred |
|- ( d e. NN -> ( mmu ` d ) e. RR ) |
28 |
|
nndivre |
|- ( ( ( mmu ` d ) e. RR /\ d e. NN ) -> ( ( mmu ` d ) / d ) e. RR ) |
29 |
27 28
|
mpancom |
|- ( d e. NN -> ( ( mmu ` d ) / d ) e. RR ) |
30 |
25 29
|
syl |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` d ) / d ) e. RR ) |
31 |
30
|
recnd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` d ) / d ) e. CC ) |
32 |
23 31
|
mulcld |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) e. CC ) |
33 |
19 32
|
fsumcl |
|- ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) e. CC ) |
34 |
|
climcl |
|- ( seq 1 ( + , F ) ~~> T -> T e. CC ) |
35 |
11 34
|
syl |
|- ( ph -> T e. CC ) |
36 |
35
|
adantr |
|- ( ( ph /\ x e. RR+ ) -> T e. CC ) |
37 |
33 36
|
mulcld |
|- ( ( ph /\ x e. RR+ ) -> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) e. CC ) |
38 |
13
|
a1i |
|- ( ph -> RR+ C_ RR ) |
39 |
|
subcl |
|- ( ( 1 e. CC /\ ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) e. CC ) -> ( 1 - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) e. CC ) |
40 |
14 37 39
|
sylancr |
|- ( ( ph /\ x e. RR+ ) -> ( 1 - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) e. CC ) |
41 |
|
1red |
|- ( ph -> 1 e. RR ) |
42 |
|
elrege0 |
|- ( C e. ( 0 [,) +oo ) <-> ( C e. RR /\ 0 <_ C ) ) |
43 |
10 42
|
sylib |
|- ( ph -> ( C e. RR /\ 0 <_ C ) ) |
44 |
43
|
simpld |
|- ( ph -> C e. RR ) |
45 |
|
fzfid |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin ) |
46 |
32
|
adantlrr |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) e. CC ) |
47 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
48 |
|
1zzd |
|- ( ph -> 1 e. ZZ ) |
49 |
7
|
adantr |
|- ( ( ph /\ m e. NN ) -> X e. D ) |
50 |
|
nnz |
|- ( m e. NN -> m e. ZZ ) |
51 |
50
|
adantl |
|- ( ( ph /\ m e. NN ) -> m e. ZZ ) |
52 |
4 1 5 2 49 51
|
dchrzrhcl |
|- ( ( ph /\ m e. NN ) -> ( X ` ( L ` m ) ) e. CC ) |
53 |
|
nncn |
|- ( m e. NN -> m e. CC ) |
54 |
53
|
adantl |
|- ( ( ph /\ m e. NN ) -> m e. CC ) |
55 |
|
nnne0 |
|- ( m e. NN -> m =/= 0 ) |
56 |
55
|
adantl |
|- ( ( ph /\ m e. NN ) -> m =/= 0 ) |
57 |
52 54 56
|
divcld |
|- ( ( ph /\ m e. NN ) -> ( ( X ` ( L ` m ) ) / m ) e. CC ) |
58 |
|
2fveq3 |
|- ( a = m -> ( X ` ( L ` a ) ) = ( X ` ( L ` m ) ) ) |
59 |
|
id |
|- ( a = m -> a = m ) |
60 |
58 59
|
oveq12d |
|- ( a = m -> ( ( X ` ( L ` a ) ) / a ) = ( ( X ` ( L ` m ) ) / m ) ) |
61 |
60
|
cbvmptv |
|- ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) = ( m e. NN |-> ( ( X ` ( L ` m ) ) / m ) ) |
62 |
9 61
|
eqtri |
|- F = ( m e. NN |-> ( ( X ` ( L ` m ) ) / m ) ) |
63 |
57 62
|
fmptd |
|- ( ph -> F : NN --> CC ) |
64 |
63
|
ffvelrnda |
|- ( ( ph /\ m e. NN ) -> ( F ` m ) e. CC ) |
65 |
47 48 64
|
serf |
|- ( ph -> seq 1 ( + , F ) : NN --> CC ) |
66 |
65
|
ad2antrr |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> seq 1 ( + , F ) : NN --> CC ) |
67 |
|
simprl |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR+ ) |
68 |
67
|
rpred |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR ) |
69 |
|
nndivre |
|- ( ( x e. RR /\ d e. NN ) -> ( x / d ) e. RR ) |
70 |
68 24 69
|
syl2an |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x / d ) e. RR ) |
71 |
24
|
adantl |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. NN ) |
72 |
71
|
nncnd |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. CC ) |
73 |
72
|
mulid2d |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. d ) = d ) |
74 |
|
fznnfl |
|- ( x e. RR -> ( d e. ( 1 ... ( |_ ` x ) ) <-> ( d e. NN /\ d <_ x ) ) ) |
75 |
68 74
|
syl |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( d e. ( 1 ... ( |_ ` x ) ) <-> ( d e. NN /\ d <_ x ) ) ) |
76 |
75
|
simplbda |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d <_ x ) |
77 |
73 76
|
eqbrtrd |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. d ) <_ x ) |
78 |
|
1red |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR ) |
79 |
68
|
adantr |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR ) |
80 |
71
|
nnrpd |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. RR+ ) |
81 |
78 79 80
|
lemuldivd |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 x. d ) <_ x <-> 1 <_ ( x / d ) ) ) |
82 |
77 81
|
mpbid |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ ( x / d ) ) |
83 |
|
flge1nn |
|- ( ( ( x / d ) e. RR /\ 1 <_ ( x / d ) ) -> ( |_ ` ( x / d ) ) e. NN ) |
84 |
70 82 83
|
syl2anc |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( x / d ) ) e. NN ) |
85 |
66 84
|
ffvelrnd |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) e. CC ) |
86 |
46 85
|
mulcld |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) e. CC ) |
87 |
35
|
ad2antrr |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> T e. CC ) |
88 |
46 87
|
mulcld |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) e. CC ) |
89 |
45 86 88
|
fsumsub |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) - ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) = ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) - sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) ) |
90 |
46 85 87
|
subdid |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) = ( ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) - ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) ) |
91 |
90
|
sumeq2dv |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) - ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) ) |
92 |
7
|
ad3antrrr |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> X e. D ) |
93 |
21
|
ad2antlr |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> d e. ZZ ) |
94 |
|
elfzelz |
|- ( m e. ( 1 ... ( |_ ` ( x / d ) ) ) -> m e. ZZ ) |
95 |
94
|
adantl |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> m e. ZZ ) |
96 |
4 1 5 2 92 93 95
|
dchrzrhmul |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( X ` ( L ` ( d x. m ) ) ) = ( ( X ` ( L ` d ) ) x. ( X ` ( L ` m ) ) ) ) |
97 |
96
|
oveq1d |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) = ( ( ( X ` ( L ` d ) ) x. ( X ` ( L ` m ) ) ) / ( d x. m ) ) ) |
98 |
23
|
adantlrr |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( X ` ( L ` d ) ) e. CC ) |
99 |
98
|
adantr |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( X ` ( L ` d ) ) e. CC ) |
100 |
72
|
adantr |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> d e. CC ) |
101 |
4 1 5 2 92 95
|
dchrzrhcl |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( X ` ( L ` m ) ) e. CC ) |
102 |
|
elfznn |
|- ( m e. ( 1 ... ( |_ ` ( x / d ) ) ) -> m e. NN ) |
103 |
102
|
adantl |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> m e. NN ) |
104 |
103
|
nncnd |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> m e. CC ) |
105 |
71
|
nnne0d |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d =/= 0 ) |
106 |
105
|
adantr |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> d =/= 0 ) |
107 |
103
|
nnne0d |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> m =/= 0 ) |
108 |
99 100 101 104 106 107
|
divmuldivd |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) = ( ( ( X ` ( L ` d ) ) x. ( X ` ( L ` m ) ) ) / ( d x. m ) ) ) |
109 |
97 108
|
eqtr4d |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) = ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) ) |
110 |
109
|
oveq2d |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( mmu ` d ) x. ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) ) = ( ( mmu ` d ) x. ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) ) ) |
111 |
71 26
|
syl |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` d ) e. ZZ ) |
112 |
111
|
zcnd |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` d ) e. CC ) |
113 |
112
|
adantr |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( mmu ` d ) e. CC ) |
114 |
99 100 106
|
divcld |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( X ` ( L ` d ) ) / d ) e. CC ) |
115 |
101 104 107
|
divcld |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( X ` ( L ` m ) ) / m ) e. CC ) |
116 |
113 114 115
|
mulassd |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( ( mmu ` d ) x. ( ( X ` ( L ` d ) ) / d ) ) x. ( ( X ` ( L ` m ) ) / m ) ) = ( ( mmu ` d ) x. ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) ) ) |
117 |
113 99 100 106
|
div12d |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( mmu ` d ) x. ( ( X ` ( L ` d ) ) / d ) ) = ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) |
118 |
117
|
oveq1d |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( ( mmu ` d ) x. ( ( X ` ( L ` d ) ) / d ) ) x. ( ( X ` ( L ` m ) ) / m ) ) = ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( X ` ( L ` m ) ) / m ) ) ) |
119 |
110 116 118
|
3eqtr2d |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( mmu ` d ) x. ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) ) = ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( X ` ( L ` m ) ) / m ) ) ) |
120 |
119
|
sumeq2dv |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( X ` ( L ` m ) ) / m ) ) ) |
121 |
|
fzfid |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / d ) ) ) e. Fin ) |
122 |
|
simpll |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ph ) |
123 |
122 102 57
|
syl2an |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( X ` ( L ` m ) ) / m ) e. CC ) |
124 |
121 46 123
|
fsummulc2 |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( X ` ( L ` m ) ) / m ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( X ` ( L ` m ) ) / m ) ) ) |
125 |
|
ovex |
|- ( ( X ` ( L ` m ) ) / m ) e. _V |
126 |
60 9 125
|
fvmpt |
|- ( m e. NN -> ( F ` m ) = ( ( X ` ( L ` m ) ) / m ) ) |
127 |
103 126
|
syl |
|- ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( F ` m ) = ( ( X ` ( L ` m ) ) / m ) ) |
128 |
84 47
|
eleqtrdi |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( x / d ) ) e. ( ZZ>= ` 1 ) ) |
129 |
127 128 123
|
fsumser |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( X ` ( L ` m ) ) / m ) = ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) |
130 |
129
|
oveq2d |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( X ` ( L ` m ) ) / m ) ) = ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) ) |
131 |
120 124 130
|
3eqtr2rd |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) ) ) |
132 |
131
|
sumeq2dv |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) ) ) |
133 |
|
2fveq3 |
|- ( n = ( d x. m ) -> ( X ` ( L ` n ) ) = ( X ` ( L ` ( d x. m ) ) ) ) |
134 |
|
id |
|- ( n = ( d x. m ) -> n = ( d x. m ) ) |
135 |
133 134
|
oveq12d |
|- ( n = ( d x. m ) -> ( ( X ` ( L ` n ) ) / n ) = ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) ) |
136 |
135
|
oveq2d |
|- ( n = ( d x. m ) -> ( ( mmu ` d ) x. ( ( X ` ( L ` n ) ) / n ) ) = ( ( mmu ` d ) x. ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) ) ) |
137 |
|
elrabi |
|- ( d e. { y e. NN | y || n } -> d e. NN ) |
138 |
137
|
ad2antll |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> d e. NN ) |
139 |
138 26
|
syl |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( mmu ` d ) e. ZZ ) |
140 |
139
|
zcnd |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( mmu ` d ) e. CC ) |
141 |
7
|
ad2antrr |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> X e. D ) |
142 |
|
elfzelz |
|- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. ZZ ) |
143 |
142
|
adantl |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. ZZ ) |
144 |
4 1 5 2 141 143
|
dchrzrhcl |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( X ` ( L ` n ) ) e. CC ) |
145 |
|
fz1ssnn |
|- ( 1 ... ( |_ ` x ) ) C_ NN |
146 |
145
|
a1i |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 ... ( |_ ` x ) ) C_ NN ) |
147 |
146
|
sselda |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN ) |
148 |
147
|
nncnd |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC ) |
149 |
147
|
nnne0d |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 ) |
150 |
144 148 149
|
divcld |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` n ) ) / n ) e. CC ) |
151 |
150
|
adantrr |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( ( X ` ( L ` n ) ) / n ) e. CC ) |
152 |
140 151
|
mulcld |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( ( mmu ` d ) x. ( ( X ` ( L ` n ) ) / n ) ) e. CC ) |
153 |
136 68 152
|
dvdsflsumcom |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( mmu ` d ) x. ( ( X ` ( L ` n ) ) / n ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) ) ) |
154 |
|
2fveq3 |
|- ( n = 1 -> ( X ` ( L ` n ) ) = ( X ` ( L ` 1 ) ) ) |
155 |
|
id |
|- ( n = 1 -> n = 1 ) |
156 |
154 155
|
oveq12d |
|- ( n = 1 -> ( ( X ` ( L ` n ) ) / n ) = ( ( X ` ( L ` 1 ) ) / 1 ) ) |
157 |
|
simprr |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 <_ x ) |
158 |
|
flge1nn |
|- ( ( x e. RR /\ 1 <_ x ) -> ( |_ ` x ) e. NN ) |
159 |
68 157 158
|
syl2anc |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) e. NN ) |
160 |
159 47
|
eleqtrdi |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) e. ( ZZ>= ` 1 ) ) |
161 |
|
eluzfz1 |
|- ( ( |_ ` x ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( |_ ` x ) ) ) |
162 |
160 161
|
syl |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 e. ( 1 ... ( |_ ` x ) ) ) |
163 |
156 45 146 162 150
|
musumsum |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( mmu ` d ) x. ( ( X ` ( L ` n ) ) / n ) ) = ( ( X ` ( L ` 1 ) ) / 1 ) ) |
164 |
132 153 163
|
3eqtr2d |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) = ( ( X ` ( L ` 1 ) ) / 1 ) ) |
165 |
4 1 5 2 7
|
dchrzrh1 |
|- ( ph -> ( X ` ( L ` 1 ) ) = 1 ) |
166 |
165
|
adantr |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( X ` ( L ` 1 ) ) = 1 ) |
167 |
166
|
oveq1d |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( X ` ( L ` 1 ) ) / 1 ) = ( 1 / 1 ) ) |
168 |
|
1div1e1 |
|- ( 1 / 1 ) = 1 |
169 |
167 168
|
eqtrdi |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( X ` ( L ` 1 ) ) / 1 ) = 1 ) |
170 |
164 169
|
eqtr2d |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 = sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) ) |
171 |
35
|
adantr |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> T e. CC ) |
172 |
45 171 46
|
fsummulc1 |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) = sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) |
173 |
170 172
|
oveq12d |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) = ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) - sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) ) |
174 |
89 91 173
|
3eqtr4rd |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) |
175 |
174
|
fveq2d |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( 1 - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) ) = ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) ) |
176 |
85 87
|
subcld |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) e. CC ) |
177 |
46 176
|
mulcld |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) e. CC ) |
178 |
45 177
|
fsumcl |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) e. CC ) |
179 |
178
|
abscld |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) e. RR ) |
180 |
177
|
abscld |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) e. RR ) |
181 |
45 180
|
fsumrecl |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) e. RR ) |
182 |
44
|
adantr |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> C e. RR ) |
183 |
45 177
|
fsumabs |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) <_ sum_ d e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) ) |
184 |
|
reflcl |
|- ( x e. RR -> ( |_ ` x ) e. RR ) |
185 |
68 184
|
syl |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) e. RR ) |
186 |
185 182
|
remulcld |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( |_ ` x ) x. C ) e. RR ) |
187 |
186 67
|
rerpdivcld |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( |_ ` x ) x. C ) / x ) e. RR ) |
188 |
182 67
|
rerpdivcld |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( C / x ) e. RR ) |
189 |
188
|
adantr |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C / x ) e. RR ) |
190 |
46
|
abscld |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) e. RR ) |
191 |
71
|
nnrecred |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / d ) e. RR ) |
192 |
176
|
abscld |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) e. RR ) |
193 |
80
|
rpred |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. RR ) |
194 |
189 193
|
remulcld |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( C / x ) x. d ) e. RR ) |
195 |
46
|
absge0d |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) ) |
196 |
176
|
absge0d |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) |
197 |
98
|
abscld |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( X ` ( L ` d ) ) ) e. RR ) |
198 |
31
|
adantlrr |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` d ) / d ) e. CC ) |
199 |
198
|
abscld |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` d ) / d ) ) e. RR ) |
200 |
98
|
absge0d |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( X ` ( L ` d ) ) ) ) |
201 |
198
|
absge0d |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( ( mmu ` d ) / d ) ) ) |
202 |
|
eqid |
|- ( Base ` Z ) = ( Base ` Z ) |
203 |
7
|
ad2antrr |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> X e. D ) |
204 |
3
|
nnnn0d |
|- ( ph -> N e. NN0 ) |
205 |
1 202 2
|
znzrhfo |
|- ( N e. NN0 -> L : ZZ -onto-> ( Base ` Z ) ) |
206 |
|
fof |
|- ( L : ZZ -onto-> ( Base ` Z ) -> L : ZZ --> ( Base ` Z ) ) |
207 |
204 205 206
|
3syl |
|- ( ph -> L : ZZ --> ( Base ` Z ) ) |
208 |
207
|
adantr |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> L : ZZ --> ( Base ` Z ) ) |
209 |
|
ffvelrn |
|- ( ( L : ZZ --> ( Base ` Z ) /\ d e. ZZ ) -> ( L ` d ) e. ( Base ` Z ) ) |
210 |
208 21 209
|
syl2an |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( L ` d ) e. ( Base ` Z ) ) |
211 |
4 5 1 202 203 210
|
dchrabs2 |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( X ` ( L ` d ) ) ) <_ 1 ) |
212 |
112 72 105
|
absdivd |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` d ) / d ) ) = ( ( abs ` ( mmu ` d ) ) / ( abs ` d ) ) ) |
213 |
80
|
rprege0d |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( d e. RR /\ 0 <_ d ) ) |
214 |
|
absid |
|- ( ( d e. RR /\ 0 <_ d ) -> ( abs ` d ) = d ) |
215 |
213 214
|
syl |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` d ) = d ) |
216 |
215
|
oveq2d |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( mmu ` d ) ) / ( abs ` d ) ) = ( ( abs ` ( mmu ` d ) ) / d ) ) |
217 |
212 216
|
eqtrd |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` d ) / d ) ) = ( ( abs ` ( mmu ` d ) ) / d ) ) |
218 |
112
|
abscld |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( mmu ` d ) ) e. RR ) |
219 |
|
mule1 |
|- ( d e. NN -> ( abs ` ( mmu ` d ) ) <_ 1 ) |
220 |
71 219
|
syl |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( mmu ` d ) ) <_ 1 ) |
221 |
218 78 80 220
|
lediv1dd |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( mmu ` d ) ) / d ) <_ ( 1 / d ) ) |
222 |
217 221
|
eqbrtrd |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` d ) / d ) ) <_ ( 1 / d ) ) |
223 |
197 78 199 191 200 201 211 222
|
lemul12ad |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( X ` ( L ` d ) ) ) x. ( abs ` ( ( mmu ` d ) / d ) ) ) <_ ( 1 x. ( 1 / d ) ) ) |
224 |
98 198
|
absmuld |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) = ( ( abs ` ( X ` ( L ` d ) ) ) x. ( abs ` ( ( mmu ` d ) / d ) ) ) ) |
225 |
191
|
recnd |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / d ) e. CC ) |
226 |
225
|
mulid2d |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. ( 1 / d ) ) = ( 1 / d ) ) |
227 |
226
|
eqcomd |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / d ) = ( 1 x. ( 1 / d ) ) ) |
228 |
223 224 227
|
3brtr4d |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) <_ ( 1 / d ) ) |
229 |
|
2fveq3 |
|- ( y = ( x / d ) -> ( seq 1 ( + , F ) ` ( |_ ` y ) ) = ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) |
230 |
229
|
fvoveq1d |
|- ( y = ( x / d ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - T ) ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) |
231 |
|
oveq2 |
|- ( y = ( x / d ) -> ( C / y ) = ( C / ( x / d ) ) ) |
232 |
230 231
|
breq12d |
|- ( y = ( x / d ) -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - T ) ) <_ ( C / y ) <-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) <_ ( C / ( x / d ) ) ) ) |
233 |
12
|
ad2antrr |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - T ) ) <_ ( C / y ) ) |
234 |
|
1re |
|- 1 e. RR |
235 |
|
elicopnf |
|- ( 1 e. RR -> ( ( x / d ) e. ( 1 [,) +oo ) <-> ( ( x / d ) e. RR /\ 1 <_ ( x / d ) ) ) ) |
236 |
234 235
|
ax-mp |
|- ( ( x / d ) e. ( 1 [,) +oo ) <-> ( ( x / d ) e. RR /\ 1 <_ ( x / d ) ) ) |
237 |
70 82 236
|
sylanbrc |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x / d ) e. ( 1 [,) +oo ) ) |
238 |
232 233 237
|
rspcdva |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) <_ ( C / ( x / d ) ) ) |
239 |
182
|
recnd |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> C e. CC ) |
240 |
239
|
adantr |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> C e. CC ) |
241 |
|
rpcnne0 |
|- ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) ) |
242 |
241
|
ad2antrl |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x e. CC /\ x =/= 0 ) ) |
243 |
242
|
adantr |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x e. CC /\ x =/= 0 ) ) |
244 |
|
divdiv2 |
|- ( ( C e. CC /\ ( x e. CC /\ x =/= 0 ) /\ ( d e. CC /\ d =/= 0 ) ) -> ( C / ( x / d ) ) = ( ( C x. d ) / x ) ) |
245 |
240 243 72 105 244
|
syl112anc |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C / ( x / d ) ) = ( ( C x. d ) / x ) ) |
246 |
|
div23 |
|- ( ( C e. CC /\ d e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( C x. d ) / x ) = ( ( C / x ) x. d ) ) |
247 |
240 72 243 246
|
syl3anc |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( C x. d ) / x ) = ( ( C / x ) x. d ) ) |
248 |
245 247
|
eqtrd |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C / ( x / d ) ) = ( ( C / x ) x. d ) ) |
249 |
238 248
|
breqtrd |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) <_ ( ( C / x ) x. d ) ) |
250 |
190 191 192 194 195 196 228 249
|
lemul12ad |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) x. ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) <_ ( ( 1 / d ) x. ( ( C / x ) x. d ) ) ) |
251 |
46 176
|
absmuld |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) = ( ( abs ` ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) x. ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) ) |
252 |
188
|
recnd |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( C / x ) e. CC ) |
253 |
252
|
adantr |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C / x ) e. CC ) |
254 |
253 72 105
|
divcan4d |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( C / x ) x. d ) / d ) = ( C / x ) ) |
255 |
253 72
|
mulcld |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( C / x ) x. d ) e. CC ) |
256 |
255 72 105
|
divrec2d |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( C / x ) x. d ) / d ) = ( ( 1 / d ) x. ( ( C / x ) x. d ) ) ) |
257 |
254 256
|
eqtr3d |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C / x ) = ( ( 1 / d ) x. ( ( C / x ) x. d ) ) ) |
258 |
250 251 257
|
3brtr4d |
|- ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) <_ ( C / x ) ) |
259 |
45 180 189 258
|
fsumle |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) <_ sum_ d e. ( 1 ... ( |_ ` x ) ) ( C / x ) ) |
260 |
159
|
nnnn0d |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) e. NN0 ) |
261 |
|
hashfz1 |
|- ( ( |_ ` x ) e. NN0 -> ( # ` ( 1 ... ( |_ ` x ) ) ) = ( |_ ` x ) ) |
262 |
260 261
|
syl |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( # ` ( 1 ... ( |_ ` x ) ) ) = ( |_ ` x ) ) |
263 |
262
|
oveq1d |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. ( C / x ) ) = ( ( |_ ` x ) x. ( C / x ) ) ) |
264 |
|
fsumconst |
|- ( ( ( 1 ... ( |_ ` x ) ) e. Fin /\ ( C / x ) e. CC ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( C / x ) = ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. ( C / x ) ) ) |
265 |
45 252 264
|
syl2anc |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( C / x ) = ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. ( C / x ) ) ) |
266 |
159
|
nncnd |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) e. CC ) |
267 |
|
divass |
|- ( ( ( |_ ` x ) e. CC /\ C e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( |_ ` x ) x. C ) / x ) = ( ( |_ ` x ) x. ( C / x ) ) ) |
268 |
266 239 242 267
|
syl3anc |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( |_ ` x ) x. C ) / x ) = ( ( |_ ` x ) x. ( C / x ) ) ) |
269 |
263 265 268
|
3eqtr4d |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( C / x ) = ( ( ( |_ ` x ) x. C ) / x ) ) |
270 |
259 269
|
breqtrd |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) <_ ( ( ( |_ ` x ) x. C ) / x ) ) |
271 |
43
|
adantr |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( C e. RR /\ 0 <_ C ) ) |
272 |
|
flle |
|- ( x e. RR -> ( |_ ` x ) <_ x ) |
273 |
68 272
|
syl |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) <_ x ) |
274 |
|
lemul1a |
|- ( ( ( ( |_ ` x ) e. RR /\ x e. RR /\ ( C e. RR /\ 0 <_ C ) ) /\ ( |_ ` x ) <_ x ) -> ( ( |_ ` x ) x. C ) <_ ( x x. C ) ) |
275 |
185 68 271 273 274
|
syl31anc |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( |_ ` x ) x. C ) <_ ( x x. C ) ) |
276 |
186 182 67
|
ledivmuld |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( ( |_ ` x ) x. C ) / x ) <_ C <-> ( ( |_ ` x ) x. C ) <_ ( x x. C ) ) ) |
277 |
275 276
|
mpbird |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( |_ ` x ) x. C ) / x ) <_ C ) |
278 |
181 187 182 270 277
|
letrd |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) <_ C ) |
279 |
179 181 182 183 278
|
letrd |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) <_ C ) |
280 |
175 279
|
eqbrtrd |
|- ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( 1 - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) ) <_ C ) |
281 |
38 40 41 44 280
|
elo1d |
|- ( ph -> ( x e. RR+ |-> ( 1 - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) ) e. O(1) ) |
282 |
18 37 281
|
o1dif |
|- ( ph -> ( ( x e. RR+ |-> 1 ) e. O(1) <-> ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) e. O(1) ) ) |
283 |
17 282
|
mpbid |
|- ( ph -> ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) e. O(1) ) |