Metamath Proof Explorer

Theorem dchrisum0lem1b

Description: Lemma for dchrisum0lem1 . (Contributed by Mario Carneiro, 7-Jun-2016)

Ref Expression
Hypotheses rpvmasum.z 
|- Z = ( Z/nZ ` N )
rpvmasum.l 
|- L = ( ZRHom ` Z )
rpvmasum.a 
|- ( ph -> N e. NN )
rpvmasum2.g 
|- G = ( DChr ` N )
rpvmasum2.d 
|- D = ( Base ` G )
rpvmasum2.1 
|- .1. = ( 0g ` G )
rpvmasum2.w 
|- W = { y e. ( D \ { .1. } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }
dchrisum0.b 
|- ( ph -> X e. W )
dchrisum0lem1.f 
|- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) )
dchrisum0.c 
|- ( ph -> C e. ( 0 [,) +oo ) )
dchrisum0.s 
|- ( ph -> seq 1 ( + , F ) ~~> S )
dchrisum0.1 
|- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / ( sqrt ` y ) ) )
Assertion dchrisum0lem1b 
|- ( ( ( 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 ) ) )

Proof

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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ) ) )