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 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 ) ) )