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 |
|
rpvmasum2.g |
|- G = ( DChr ` N ) |
5 |
|
rpvmasum2.d |
|- D = ( Base ` G ) |
6 |
|
rpvmasum2.1 |
|- .1. = ( 0g ` G ) |
7 |
|
rpvmasum2.w |
|- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } |
8 |
|
dchrisum0.b |
|- ( ph -> X e. W ) |
9 |
|
dchrisum0lem1.f |
|- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) |
10 |
|
dchrisum0.c |
|- ( ph -> C e. ( 0 [,) +oo ) ) |
11 |
|
dchrisum0.s |
|- ( ph -> seq 1 ( + , F ) ~~> S ) |
12 |
|
dchrisum0.1 |
|- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / ( sqrt ` y ) ) ) |
13 |
|
fzfid |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) e. Fin ) |
14 |
|
ssun2 |
|- ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) C_ ( ( 1 ... ( |_ ` x ) ) u. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) |
15 |
|
simpr |
|- ( ( ph /\ x e. RR+ ) -> x e. RR+ ) |
16 |
15
|
rprege0d |
|- ( ( ph /\ x e. RR+ ) -> ( x e. RR /\ 0 <_ x ) ) |
17 |
|
flge0nn0 |
|- ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 ) |
18 |
16 17
|
syl |
|- ( ( ph /\ x e. RR+ ) -> ( |_ ` x ) e. NN0 ) |
19 |
|
nn0p1nn |
|- ( ( |_ ` x ) e. NN0 -> ( ( |_ ` x ) + 1 ) e. NN ) |
20 |
18 19
|
syl |
|- ( ( ph /\ x e. RR+ ) -> ( ( |_ ` x ) + 1 ) e. NN ) |
21 |
20
|
adantr |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( |_ ` x ) + 1 ) e. NN ) |
22 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
23 |
21 22
|
eleqtrdi |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` 1 ) ) |
24 |
|
dchrisum0lem1a |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x <_ ( ( x ^ 2 ) / d ) /\ ( |_ ` ( ( x ^ 2 ) / d ) ) e. ( ZZ>= ` ( |_ ` x ) ) ) ) |
25 |
24
|
simprd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( ( x ^ 2 ) / d ) ) e. ( ZZ>= ` ( |_ ` x ) ) ) |
26 |
|
fzsplit2 |
|- ( ( ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` 1 ) /\ ( |_ ` ( ( x ^ 2 ) / d ) ) e. ( ZZ>= ` ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) = ( ( 1 ... ( |_ ` x ) ) u. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) ) |
27 |
23 25 26
|
syl2anc |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) = ( ( 1 ... ( |_ ` x ) ) u. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) ) |
28 |
14 27
|
sseqtrrid |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) C_ ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) |
29 |
28
|
sselda |
|- ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) |
30 |
7
|
ssrab3 |
|- W C_ ( D \ { .1. } ) |
31 |
30 8
|
sselid |
|- ( ph -> X e. ( D \ { .1. } ) ) |
32 |
31
|
eldifad |
|- ( ph -> X e. D ) |
33 |
32
|
ad3antrrr |
|- ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> X e. D ) |
34 |
|
elfzelz |
|- ( m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) -> m e. ZZ ) |
35 |
34
|
adantl |
|- ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> m e. ZZ ) |
36 |
4 1 5 2 33 35
|
dchrzrhcl |
|- ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( X ` ( L ` m ) ) e. CC ) |
37 |
|
elfznn |
|- ( m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) -> m e. NN ) |
38 |
37
|
adantl |
|- ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> m e. NN ) |
39 |
38
|
nnrpd |
|- ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> m e. RR+ ) |
40 |
39
|
rpsqrtcld |
|- ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( sqrt ` m ) e. RR+ ) |
41 |
40
|
rpcnd |
|- ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( sqrt ` m ) e. CC ) |
42 |
40
|
rpne0d |
|- ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( sqrt ` m ) =/= 0 ) |
43 |
36 41 42
|
divcld |
|- ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) e. CC ) |
44 |
29 43
|
syldan |
|- ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) e. CC ) |
45 |
13 44
|
fsumcl |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) e. CC ) |
46 |
45
|
abscld |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) e. RR ) |
47 |
|
1zzd |
|- ( ph -> 1 e. ZZ ) |
48 |
32
|
adantr |
|- ( ( ph /\ m e. NN ) -> X e. D ) |
49 |
|
nnz |
|- ( m e. NN -> m e. ZZ ) |
50 |
49
|
adantl |
|- ( ( ph /\ m e. NN ) -> m e. ZZ ) |
51 |
4 1 5 2 48 50
|
dchrzrhcl |
|- ( ( ph /\ m e. NN ) -> ( X ` ( L ` m ) ) e. CC ) |
52 |
|
nnrp |
|- ( m e. NN -> m e. RR+ ) |
53 |
52
|
adantl |
|- ( ( ph /\ m e. NN ) -> m e. RR+ ) |
54 |
53
|
rpsqrtcld |
|- ( ( ph /\ m e. NN ) -> ( sqrt ` m ) e. RR+ ) |
55 |
54
|
rpcnd |
|- ( ( ph /\ m e. NN ) -> ( sqrt ` m ) e. CC ) |
56 |
54
|
rpne0d |
|- ( ( ph /\ m e. NN ) -> ( sqrt ` m ) =/= 0 ) |
57 |
51 55 56
|
divcld |
|- ( ( ph /\ m e. NN ) -> ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) e. CC ) |
58 |
|
2fveq3 |
|- ( a = m -> ( X ` ( L ` a ) ) = ( X ` ( L ` m ) ) ) |
59 |
|
fveq2 |
|- ( a = m -> ( sqrt ` a ) = ( sqrt ` m ) ) |
60 |
58 59
|
oveq12d |
|- ( a = m -> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) = ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) |
61 |
60
|
cbvmptv |
|- ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) = ( m e. NN |-> ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) |
62 |
9 61
|
eqtri |
|- F = ( m e. NN |-> ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) |
63 |
57 62
|
fmptd |
|- ( ph -> F : NN --> CC ) |
64 |
63
|
ffvelrnda |
|- ( ( ph /\ m e. NN ) -> ( F ` m ) e. CC ) |
65 |
22 47 64
|
serf |
|- ( ph -> seq 1 ( + , F ) : NN --> CC ) |
66 |
65
|
ad2antrr |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> seq 1 ( + , F ) : NN --> CC ) |
67 |
15
|
rpregt0d |
|- ( ( ph /\ x e. RR+ ) -> ( x e. RR /\ 0 < x ) ) |
68 |
67
|
adantr |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x e. RR /\ 0 < x ) ) |
69 |
68
|
simpld |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR ) |
70 |
|
1red |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR ) |
71 |
|
elfznn |
|- ( d e. ( 1 ... ( |_ ` x ) ) -> d e. NN ) |
72 |
71
|
adantl |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. NN ) |
73 |
72
|
nnred |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. RR ) |
74 |
72
|
nnge1d |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ d ) |
75 |
15
|
rpred |
|- ( ( ph /\ x e. RR+ ) -> x e. RR ) |
76 |
|
fznnfl |
|- ( x e. RR -> ( d e. ( 1 ... ( |_ ` x ) ) <-> ( d e. NN /\ d <_ x ) ) ) |
77 |
75 76
|
syl |
|- ( ( ph /\ x e. RR+ ) -> ( d e. ( 1 ... ( |_ ` x ) ) <-> ( d e. NN /\ d <_ x ) ) ) |
78 |
77
|
simplbda |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d <_ x ) |
79 |
70 73 69 74 78
|
letrd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ x ) |
80 |
|
flge1nn |
|- ( ( x e. RR /\ 1 <_ x ) -> ( |_ ` x ) e. NN ) |
81 |
69 79 80
|
syl2anc |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` x ) e. NN ) |
82 |
|
eluznn |
|- ( ( ( |_ ` x ) e. NN /\ ( |_ ` ( ( x ^ 2 ) / d ) ) e. ( ZZ>= ` ( |_ ` x ) ) ) -> ( |_ ` ( ( x ^ 2 ) / d ) ) e. NN ) |
83 |
81 25 82
|
syl2anc |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( ( x ^ 2 ) / d ) ) e. NN ) |
84 |
66 83
|
ffvelrnd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) e. CC ) |
85 |
|
climcl |
|- ( seq 1 ( + , F ) ~~> S -> S e. CC ) |
86 |
11 85
|
syl |
|- ( ph -> S e. CC ) |
87 |
86
|
ad2antrr |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> S e. CC ) |
88 |
84 87
|
subcld |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) - S ) e. CC ) |
89 |
88
|
abscld |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) - S ) ) e. RR ) |
90 |
66 81
|
ffvelrnd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( seq 1 ( + , F ) ` ( |_ ` x ) ) e. CC ) |
91 |
87 90
|
subcld |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( S - ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) e. CC ) |
92 |
91
|
abscld |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( S - ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) ) e. RR ) |
93 |
89 92
|
readdcld |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) - S ) ) + ( abs ` ( S - ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) ) ) e. RR ) |
94 |
|
2re |
|- 2 e. RR |
95 |
|
elrege0 |
|- ( C e. ( 0 [,) +oo ) <-> ( C e. RR /\ 0 <_ C ) ) |
96 |
10 95
|
sylib |
|- ( ph -> ( C e. RR /\ 0 <_ C ) ) |
97 |
96
|
simpld |
|- ( ph -> C e. RR ) |
98 |
|
remulcl |
|- ( ( 2 e. RR /\ C e. RR ) -> ( 2 x. C ) e. RR ) |
99 |
94 97 98
|
sylancr |
|- ( ph -> ( 2 x. C ) e. RR ) |
100 |
99
|
adantr |
|- ( ( ph /\ x e. RR+ ) -> ( 2 x. C ) e. RR ) |
101 |
15
|
rpsqrtcld |
|- ( ( ph /\ x e. RR+ ) -> ( sqrt ` x ) e. RR+ ) |
102 |
100 101
|
rerpdivcld |
|- ( ( ph /\ x e. RR+ ) -> ( ( 2 x. C ) / ( sqrt ` x ) ) e. RR ) |
103 |
102
|
adantr |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. C ) / ( sqrt ` x ) ) e. RR ) |
104 |
|
ssun1 |
|- ( 1 ... ( |_ ` x ) ) C_ ( ( 1 ... ( |_ ` x ) ) u. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) |
105 |
104 27
|
sseqtrrid |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` x ) ) C_ ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) |
106 |
105
|
sselda |
|- ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) |
107 |
|
ovex |
|- ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) e. _V |
108 |
60 9 107
|
fvmpt3i |
|- ( m e. NN -> ( F ` m ) = ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) |
109 |
38 108
|
syl |
|- ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( F ` m ) = ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) |
110 |
106 109
|
syldan |
|- ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( F ` m ) = ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) |
111 |
81 22
|
eleqtrdi |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` x ) e. ( ZZ>= ` 1 ) ) |
112 |
106 43
|
syldan |
|- ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) e. CC ) |
113 |
110 111 112
|
fsumser |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) = ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) |
114 |
113 90
|
eqeltrd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) e. CC ) |
115 |
114 45
|
pncan2d |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) + sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) = sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) |
116 |
|
reflcl |
|- ( x e. RR -> ( |_ ` x ) e. RR ) |
117 |
69 116
|
syl |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` x ) e. RR ) |
118 |
117
|
ltp1d |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` x ) < ( ( |_ ` x ) + 1 ) ) |
119 |
|
fzdisj |
|- ( ( |_ ` x ) < ( ( |_ ` x ) + 1 ) -> ( ( 1 ... ( |_ ` x ) ) i^i ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) = (/) ) |
120 |
118 119
|
syl |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 ... ( |_ ` x ) ) i^i ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) = (/) ) |
121 |
|
fzfid |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) e. Fin ) |
122 |
120 27 121 43
|
fsumsplit |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) = ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) + sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) ) |
123 |
83 22
|
eleqtrdi |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( ( x ^ 2 ) / d ) ) e. ( ZZ>= ` 1 ) ) |
124 |
109 123 43
|
fsumser |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) = ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) |
125 |
122 124
|
eqtr3d |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) + sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) = ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) |
126 |
125 113
|
oveq12d |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) + sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) = ( ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) - ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) ) |
127 |
115 126
|
eqtr3d |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) = ( ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) - ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) ) |
128 |
127
|
fveq2d |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) - ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) ) ) |
129 |
84 90 87
|
abs3difd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) - ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) ) <_ ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) - S ) ) + ( abs ` ( S - ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) ) ) ) |
130 |
128 129
|
eqbrtrd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) <_ ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) - S ) ) + ( abs ` ( S - ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) ) ) ) |
131 |
97
|
ad2antrr |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> C e. RR ) |
132 |
|
simplr |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ ) |
133 |
132
|
rpsqrtcld |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` x ) e. RR+ ) |
134 |
131 133
|
rerpdivcld |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C / ( sqrt ` x ) ) e. RR ) |
135 |
|
2z |
|- 2 e. ZZ |
136 |
|
rpexpcl |
|- ( ( x e. RR+ /\ 2 e. ZZ ) -> ( x ^ 2 ) e. RR+ ) |
137 |
15 135 136
|
sylancl |
|- ( ( ph /\ x e. RR+ ) -> ( x ^ 2 ) e. RR+ ) |
138 |
137
|
adantr |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x ^ 2 ) e. RR+ ) |
139 |
72
|
nnrpd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. RR+ ) |
140 |
138 139
|
rpdivcld |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x ^ 2 ) / d ) e. RR+ ) |
141 |
140
|
rpsqrtcld |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` ( ( x ^ 2 ) / d ) ) e. RR+ ) |
142 |
131 141
|
rerpdivcld |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C / ( sqrt ` ( ( x ^ 2 ) / d ) ) ) e. RR ) |
143 |
|
2fveq3 |
|- ( y = ( ( x ^ 2 ) / d ) -> ( seq 1 ( + , F ) ` ( |_ ` y ) ) = ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) |
144 |
143
|
fvoveq1d |
|- ( y = ( ( x ^ 2 ) / d ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) - S ) ) ) |
145 |
|
fveq2 |
|- ( y = ( ( x ^ 2 ) / d ) -> ( sqrt ` y ) = ( sqrt ` ( ( x ^ 2 ) / d ) ) ) |
146 |
145
|
oveq2d |
|- ( y = ( ( x ^ 2 ) / d ) -> ( C / ( sqrt ` y ) ) = ( C / ( sqrt ` ( ( x ^ 2 ) / d ) ) ) ) |
147 |
144 146
|
breq12d |
|- ( y = ( ( x ^ 2 ) / d ) -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / ( sqrt ` y ) ) <-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) - S ) ) <_ ( C / ( sqrt ` ( ( x ^ 2 ) / d ) ) ) ) ) |
148 |
12
|
ad2antrr |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / ( sqrt ` y ) ) ) |
149 |
137
|
rpred |
|- ( ( ph /\ x e. RR+ ) -> ( x ^ 2 ) e. RR ) |
150 |
|
nndivre |
|- ( ( ( x ^ 2 ) e. RR /\ d e. NN ) -> ( ( x ^ 2 ) / d ) e. RR ) |
151 |
149 71 150
|
syl2an |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x ^ 2 ) / d ) e. RR ) |
152 |
24
|
simpld |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> x <_ ( ( x ^ 2 ) / d ) ) |
153 |
70 69 151 79 152
|
letrd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ ( ( x ^ 2 ) / d ) ) |
154 |
|
1re |
|- 1 e. RR |
155 |
|
elicopnf |
|- ( 1 e. RR -> ( ( ( x ^ 2 ) / d ) e. ( 1 [,) +oo ) <-> ( ( ( x ^ 2 ) / d ) e. RR /\ 1 <_ ( ( x ^ 2 ) / d ) ) ) ) |
156 |
154 155
|
ax-mp |
|- ( ( ( x ^ 2 ) / d ) e. ( 1 [,) +oo ) <-> ( ( ( x ^ 2 ) / d ) e. RR /\ 1 <_ ( ( x ^ 2 ) / d ) ) ) |
157 |
151 153 156
|
sylanbrc |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x ^ 2 ) / d ) e. ( 1 [,) +oo ) ) |
158 |
147 148 157
|
rspcdva |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) - S ) ) <_ ( C / ( sqrt ` ( ( x ^ 2 ) / d ) ) ) ) |
159 |
133
|
rpregt0d |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqrt ` x ) e. RR /\ 0 < ( sqrt ` x ) ) ) |
160 |
141
|
rpregt0d |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqrt ` ( ( x ^ 2 ) / d ) ) e. RR /\ 0 < ( sqrt ` ( ( x ^ 2 ) / d ) ) ) ) |
161 |
96
|
ad2antrr |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C e. RR /\ 0 <_ C ) ) |
162 |
132
|
rprege0d |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x e. RR /\ 0 <_ x ) ) |
163 |
140
|
rprege0d |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( x ^ 2 ) / d ) e. RR /\ 0 <_ ( ( x ^ 2 ) / d ) ) ) |
164 |
|
sqrtle |
|- ( ( ( x e. RR /\ 0 <_ x ) /\ ( ( ( x ^ 2 ) / d ) e. RR /\ 0 <_ ( ( x ^ 2 ) / d ) ) ) -> ( x <_ ( ( x ^ 2 ) / d ) <-> ( sqrt ` x ) <_ ( sqrt ` ( ( x ^ 2 ) / d ) ) ) ) |
165 |
162 163 164
|
syl2anc |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x <_ ( ( x ^ 2 ) / d ) <-> ( sqrt ` x ) <_ ( sqrt ` ( ( x ^ 2 ) / d ) ) ) ) |
166 |
152 165
|
mpbid |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` x ) <_ ( sqrt ` ( ( x ^ 2 ) / d ) ) ) |
167 |
|
lediv2a |
|- ( ( ( ( ( sqrt ` x ) e. RR /\ 0 < ( sqrt ` x ) ) /\ ( ( sqrt ` ( ( x ^ 2 ) / d ) ) e. RR /\ 0 < ( sqrt ` ( ( x ^ 2 ) / d ) ) ) /\ ( C e. RR /\ 0 <_ C ) ) /\ ( sqrt ` x ) <_ ( sqrt ` ( ( x ^ 2 ) / d ) ) ) -> ( C / ( sqrt ` ( ( x ^ 2 ) / d ) ) ) <_ ( C / ( sqrt ` x ) ) ) |
168 |
159 160 161 166 167
|
syl31anc |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C / ( sqrt ` ( ( x ^ 2 ) / d ) ) ) <_ ( C / ( sqrt ` x ) ) ) |
169 |
89 142 134 158 168
|
letrd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) - S ) ) <_ ( C / ( sqrt ` x ) ) ) |
170 |
87 90
|
abssubd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( S - ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - S ) ) ) |
171 |
|
2fveq3 |
|- ( y = x -> ( seq 1 ( + , F ) ` ( |_ ` y ) ) = ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) |
172 |
171
|
fvoveq1d |
|- ( y = x -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - S ) ) ) |
173 |
|
fveq2 |
|- ( y = x -> ( sqrt ` y ) = ( sqrt ` x ) ) |
174 |
173
|
oveq2d |
|- ( y = x -> ( C / ( sqrt ` y ) ) = ( C / ( sqrt ` x ) ) ) |
175 |
172 174
|
breq12d |
|- ( y = x -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / ( sqrt ` y ) ) <-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - S ) ) <_ ( C / ( sqrt ` x ) ) ) ) |
176 |
|
elicopnf |
|- ( 1 e. RR -> ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) ) ) |
177 |
154 176
|
ax-mp |
|- ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) ) |
178 |
69 79 177
|
sylanbrc |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> x e. ( 1 [,) +oo ) ) |
179 |
175 148 178
|
rspcdva |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` x ) ) - S ) ) <_ ( C / ( sqrt ` x ) ) ) |
180 |
170 179
|
eqbrtrd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( S - ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) ) <_ ( C / ( sqrt ` x ) ) ) |
181 |
89 92 134 134 169 180
|
le2addd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) - S ) ) + ( abs ` ( S - ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) ) ) <_ ( ( C / ( sqrt ` x ) ) + ( C / ( sqrt ` x ) ) ) ) |
182 |
|
2cnd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. CC ) |
183 |
97
|
adantr |
|- ( ( ph /\ x e. RR+ ) -> C e. RR ) |
184 |
183
|
recnd |
|- ( ( ph /\ x e. RR+ ) -> C e. CC ) |
185 |
184
|
adantr |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> C e. CC ) |
186 |
101
|
rpcnne0d |
|- ( ( ph /\ x e. RR+ ) -> ( ( sqrt ` x ) e. CC /\ ( sqrt ` x ) =/= 0 ) ) |
187 |
186
|
adantr |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqrt ` x ) e. CC /\ ( sqrt ` x ) =/= 0 ) ) |
188 |
|
divass |
|- ( ( 2 e. CC /\ C e. CC /\ ( ( sqrt ` x ) e. CC /\ ( sqrt ` x ) =/= 0 ) ) -> ( ( 2 x. C ) / ( sqrt ` x ) ) = ( 2 x. ( C / ( sqrt ` x ) ) ) ) |
189 |
182 185 187 188
|
syl3anc |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. C ) / ( sqrt ` x ) ) = ( 2 x. ( C / ( sqrt ` x ) ) ) ) |
190 |
134
|
recnd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C / ( sqrt ` x ) ) e. CC ) |
191 |
190
|
2timesd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( C / ( sqrt ` x ) ) ) = ( ( C / ( sqrt ` x ) ) + ( C / ( sqrt ` x ) ) ) ) |
192 |
189 191
|
eqtrd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. C ) / ( sqrt ` x ) ) = ( ( C / ( sqrt ` x ) ) + ( C / ( sqrt ` x ) ) ) ) |
193 |
181 192
|
breqtrrd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( ( x ^ 2 ) / d ) ) ) - S ) ) + ( abs ` ( S - ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) ) ) <_ ( ( 2 x. C ) / ( sqrt ` x ) ) ) |
194 |
46 93 103 130 193
|
letrd |
|- ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) <_ ( ( 2 x. C ) / ( sqrt ` x ) ) ) |