MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrisum0lem1 Unicode version

Theorem dchrisum0lem1 20681
Description: Lemma for dchrisum0 20685. (Contributed by Mario Carneiro, 12-May-2016.) (Revised by Mario Carneiro, 7-Jun-2016.)
Hypotheses
Ref Expression
rpvmasum.z  |-  Z  =  (ℤ/n `  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 ) )  /  ( sqr `  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  /  ( sqr `  y ) ) )
Assertion
Ref Expression
dchrisum0lem1  |-  ( ph  ->  ( x  e.  RR+  |->  sum_
m  e.  ( ( ( |_ `  x
)  +  1 ) ... ( |_ `  ( x ^ 2 ) ) ) sum_ d  e.  ( 1 ... ( |_ `  ( ( x ^
2 )  /  m
) ) ) ( ( ( X `  ( L `  m ) )  /  ( sqr `  m ) )  / 
( sqr `  d
) ) )  e.  O ( 1 ) )
Distinct variable groups:    x, m, y,  .1.    m, d, x, y, C    F, d, x, y   
a, d, m, x, y    m, N, x, y    ph, d, m, x    S, d, m, x, y   
x, W    m, Z, x, y    D, m, x, y    L, a, d, m, x, y    X, a, d, m, x, y   
m, F
Allowed substitution hints:    ph( y, a)    C( a)    D( a, d)    S( a)    .1. ( a, d)    F( a)    G( x, y, m, a, d)    N( a, d)    W( y, m, a, d)    Z( a, d)

Proof of Theorem dchrisum0lem1
StepHypRef Expression
1 fzfid 11051 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1 ... ( |_ `  x ) )  e. 
Fin )
2 fzfid 11051 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
( |_ `  x
)  +  1 ) ... ( |_ `  ( x ^ 2 ) ) )  e. 
Fin )
3 fzfid 11051 . . . 4  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( |_ `  x
)  +  1 ) ... ( |_ `  ( ( x ^
2 )  /  d
) ) )  e. 
Fin )
4 elfznn 10835 . . . . . . 7  |-  ( d  e.  ( 1 ... ( |_ `  x
) )  ->  d  e.  NN )
5 elfzuz 10810 . . . . . . 7  |-  ( m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_ `  (
( x ^ 2 )  /  d ) ) )  ->  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) )
64, 5anim12i 549 . . . . . 6  |-  ( ( d  e.  ( 1 ... ( |_ `  x ) )  /\  m  e.  ( (
( |_ `  x
)  +  1 ) ... ( |_ `  ( ( x ^
2 )  /  d
) ) ) )  ->  ( d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )
76a1i 10 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
d  e.  ( 1 ... ( |_ `  x ) )  /\  m  e.  ( (
( |_ `  x
)  +  1 ) ... ( |_ `  ( ( x ^
2 )  /  d
) ) ) )  ->  ( d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) ) )
8 elfzuz 10810 . . . . . . 7  |-  ( m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_ `  (
x ^ 2 ) ) )  ->  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) )
9 elfznn 10835 . . . . . . 7  |-  ( d  e.  ( 1 ... ( |_ `  (
( x ^ 2 )  /  m ) ) )  ->  d  e.  NN )
108, 9anim12ci 550 . . . . . 6  |-  ( ( m  e.  ( ( ( |_ `  x
)  +  1 ) ... ( |_ `  ( x ^ 2 ) ) )  /\  d  e.  ( 1 ... ( |_ `  ( ( x ^
2 )  /  m
) ) ) )  ->  ( d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )
1110a1i 10 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
m  e.  ( ( ( |_ `  x
)  +  1 ) ... ( |_ `  ( x ^ 2 ) ) )  /\  d  e.  ( 1 ... ( |_ `  ( ( x ^
2 )  /  m
) ) ) )  ->  ( d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) ) )
12 eluzelz 10254 . . . . . . . . . . . 12  |-  ( m  e.  ( ZZ>= `  (
( |_ `  x
)  +  1 ) )  ->  m  e.  ZZ )
1312ad2antll 709 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  m  e.  ZZ )
1413zred 10133 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  m  e.  RR )
15 simpr 447 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  RR+ )
16 2z 10070 . . . . . . . . . . . . 13  |-  2  e.  ZZ
17 rpexpcl 11138 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR+  /\  2  e.  ZZ )  ->  (
x ^ 2 )  e.  RR+ )
1815, 16, 17sylancl 643 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x ^ 2 )  e.  RR+ )
1918rpred 10406 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x ^ 2 )  e.  RR )
2019adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( x ^
2 )  e.  RR )
21 simprl 732 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  d  e.  NN )
2221nnrpd 10405 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  d  e.  RR+ )
2314, 20, 22lemuldivd 10451 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( m  x.  d )  <_ 
( x ^ 2 )  <->  m  <_  ( ( x ^ 2 )  /  d ) ) )
2421nnred 9777 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  d  e.  RR )
2515rprege0d 10413 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x  e.  RR  /\  0  <_  x ) )
26 flge0nn0 10964 . . . . . . . . . . . . . 14  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( |_ `  x
)  e.  NN0 )
27 nn0p1nn 10019 . . . . . . . . . . . . . 14  |-  ( ( |_ `  x )  e.  NN0  ->  ( ( |_ `  x )  +  1 )  e.  NN )
2825, 26, 273syl 18 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( |_ `  x )  +  1 )  e.  NN )
2928adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( |_
`  x )  +  1 )  e.  NN )
30 simprr 733 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  m  e.  (
ZZ>= `  ( ( |_
`  x )  +  1 ) ) )
31 nnuz 10279 . . . . . . . . . . . . 13  |-  NN  =  ( ZZ>= `  1 )
3231uztrn2 10261 . . . . . . . . . . . 12  |-  ( ( ( ( |_ `  x )  +  1 )  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) )  ->  m  e.  NN )
3329, 30, 32syl2anc 642 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  m  e.  NN )
3433nnrpd 10405 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  m  e.  RR+ )
3524, 20, 34lemuldiv2d 10452 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( m  x.  d )  <_ 
( x ^ 2 )  <->  d  <_  (
( x ^ 2 )  /  m ) ) )
3623, 35bitr3d 246 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( m  <_ 
( ( x ^
2 )  /  d
)  <->  d  <_  (
( x ^ 2 )  /  m ) ) )
37 rpcn 10378 . . . . . . . . . . . . . . . 16  |-  ( x  e.  RR+  ->  x  e.  CC )
3837adantl 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  x  e.  CC )
3938sqvald 11258 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( x ^ 2 )  =  ( x  x.  x
) )
4039adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( x ^
2 )  =  ( x  x.  x ) )
41 simplr 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  x  e.  RR+ )
4241rpred 10406 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  x  e.  RR )
43 reflcl 10944 . . . . . . . . . . . . . . . 16  |-  ( x  e.  RR  ->  ( |_ `  x )  e.  RR )
44 peano2re 9001 . . . . . . . . . . . . . . . 16  |-  ( ( |_ `  x )  e.  RR  ->  (
( |_ `  x
)  +  1 )  e.  RR )
4542, 43, 443syl 18 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( |_
`  x )  +  1 )  e.  RR )
46 fllep1 10949 . . . . . . . . . . . . . . . 16  |-  ( x  e.  RR  ->  x  <_  ( ( |_ `  x )  +  1 ) )
4742, 46syl 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  x  <_  (
( |_ `  x
)  +  1 ) )
48 eluzle 10256 . . . . . . . . . . . . . . . 16  |-  ( m  e.  ( ZZ>= `  (
( |_ `  x
)  +  1 ) )  ->  ( ( |_ `  x )  +  1 )  <_  m
)
4948ad2antll 709 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( |_
`  x )  +  1 )  <_  m
)
5042, 45, 14, 47, 49letrd 8989 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  x  <_  m
)
5142, 14, 41lemul1d 10445 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( x  <_  m 
<->  ( x  x.  x
)  <_  ( m  x.  x ) ) )
5250, 51mpbid 201 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( x  x.  x )  <_  (
m  x.  x ) )
5340, 52eqbrtrd 4059 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( x ^
2 )  <_  (
m  x.  x ) )
5420, 42, 34ledivmuld 10455 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( ( x ^ 2 )  /  m )  <_  x 
<->  ( x ^ 2 )  <_  ( m  x.  x ) ) )
5553, 54mpbird 223 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( x ^ 2 )  /  m )  <_  x
)
56 nnre 9769 . . . . . . . . . . . . 13  |-  ( d  e.  NN  ->  d  e.  RR )
5756ad2antrl 708 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  d  e.  RR )
5820, 33nndivred 9810 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( x ^ 2 )  /  m )  e.  RR )
59 letr 8930 . . . . . . . . . . . 12  |-  ( ( d  e.  RR  /\  ( ( x ^
2 )  /  m
)  e.  RR  /\  x  e.  RR )  ->  ( ( d  <_ 
( ( x ^
2 )  /  m
)  /\  ( (
x ^ 2 )  /  m )  <_  x )  ->  d  <_  x ) )
6057, 58, 42, 59syl3anc 1182 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( d  <_  ( ( x ^ 2 )  /  m )  /\  (
( x ^ 2 )  /  m )  <_  x )  -> 
d  <_  x )
)
6155, 60mpan2d 655 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( d  <_ 
( ( x ^
2 )  /  m
)  ->  d  <_  x ) )
6236, 61sylbid 206 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( m  <_ 
( ( x ^
2 )  /  d
)  ->  d  <_  x ) )
6362pm4.71rd 616 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( m  <_ 
( ( x ^
2 )  /  d
)  <->  ( d  <_  x  /\  m  <_  (
( x ^ 2 )  /  d ) ) ) )
64 nnge1 9788 . . . . . . . . . . . . . 14  |-  ( d  e.  NN  ->  1  <_  d )
6564ad2antrl 708 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  1  <_  d
)
66 1re 8853 . . . . . . . . . . . . . . . 16  |-  1  e.  RR
67 0lt1 9312 . . . . . . . . . . . . . . . 16  |-  0  <  1
6866, 67pm3.2i 441 . . . . . . . . . . . . . . 15  |-  ( 1  e.  RR  /\  0  <  1 )
6968a1i 10 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( 1  e.  RR  /\  0  <  1 ) )
7022rpregt0d 10412 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( d  e.  RR  /\  0  < 
d ) )
7118adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( x ^
2 )  e.  RR+ )
7271rpregt0d 10412 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( x ^ 2 )  e.  RR  /\  0  < 
( x ^ 2 ) ) )
73 lediv2 9662 . . . . . . . . . . . . . 14  |-  ( ( ( 1  e.  RR  /\  0  <  1 )  /\  ( d  e.  RR  /\  0  < 
d )  /\  (
( x ^ 2 )  e.  RR  /\  0  <  ( x ^
2 ) ) )  ->  ( 1  <_ 
d  <->  ( ( x ^ 2 )  / 
d )  <_  (
( x ^ 2 )  /  1 ) ) )
7469, 70, 72, 73syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( 1  <_ 
d  <->  ( ( x ^ 2 )  / 
d )  <_  (
( x ^ 2 )  /  1 ) ) )
7565, 74mpbid 201 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( x ^ 2 )  / 
d )  <_  (
( x ^ 2 )  /  1 ) )
7620recnd 8877 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( x ^
2 )  e.  CC )
7776div1d 9544 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( x ^ 2 )  / 
1 )  =  ( x ^ 2 ) )
7875, 77breqtrd 4063 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( x ^ 2 )  / 
d )  <_  (
x ^ 2 ) )
79 simpl 443 . . . . . . . . . . . . 13  |-  ( ( d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) )  -> 
d  e.  NN )
80 nndivre 9797 . . . . . . . . . . . . 13  |-  ( ( ( x ^ 2 )  e.  RR  /\  d  e.  NN )  ->  ( ( x ^
2 )  /  d
)  e.  RR )
8119, 79, 80syl2an 463 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( x ^ 2 )  / 
d )  e.  RR )
82 letr 8930 . . . . . . . . . . . 12  |-  ( ( m  e.  RR  /\  ( ( x ^
2 )  /  d
)  e.  RR  /\  ( x ^ 2 )  e.  RR )  ->  ( ( m  <_  ( ( x ^ 2 )  / 
d )  /\  (
( x ^ 2 )  /  d )  <_  ( x ^
2 ) )  ->  m  <_  ( x ^
2 ) ) )
8314, 81, 20, 82syl3anc 1182 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( m  <_  ( ( x ^ 2 )  / 
d )  /\  (
( x ^ 2 )  /  d )  <_  ( x ^
2 ) )  ->  m  <_  ( x ^
2 ) ) )
8478, 83mpan2d 655 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( m  <_ 
( ( x ^
2 )  /  d
)  ->  m  <_  ( x ^ 2 ) ) )
8536, 84sylbird 226 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( d  <_ 
( ( x ^
2 )  /  m
)  ->  m  <_  ( x ^ 2 ) ) )
8685pm4.71rd 616 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( d  <_ 
( ( x ^
2 )  /  m
)  <->  ( m  <_ 
( x ^ 2 )  /\  d  <_ 
( ( x ^
2 )  /  m
) ) ) )
8736, 63, 863bitr3d 274 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( d  <_  x  /\  m  <_  ( ( x ^
2 )  /  d
) )  <->  ( m  <_  ( x ^ 2 )  /\  d  <_ 
( ( x ^
2 )  /  m
) ) ) )
88 fznnfl 10982 . . . . . . . . . 10  |-  ( x  e.  RR  ->  (
d  e.  ( 1 ... ( |_ `  x ) )  <->  ( d  e.  NN  /\  d  <_  x ) ) )
8988baibd 875 . . . . . . . . 9  |-  ( ( x  e.  RR  /\  d  e.  NN )  ->  ( d  e.  ( 1 ... ( |_
`  x ) )  <-> 
d  <_  x )
)
9042, 21, 89syl2anc 642 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( d  e.  ( 1 ... ( |_ `  x ) )  <-> 
d  <_  x )
)
9181flcld 10946 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( |_ `  ( ( x ^
2 )  /  d
) )  e.  ZZ )
92 elfz5 10806 . . . . . . . . . 10  |-  ( ( m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) )  /\  ( |_ `  ( ( x ^ 2 )  / 
d ) )  e.  ZZ )  ->  (
m  e.  ( ( ( |_ `  x
)  +  1 ) ... ( |_ `  ( ( x ^
2 )  /  d
) ) )  <->  m  <_  ( |_ `  ( ( x ^ 2 )  /  d ) ) ) )
9330, 91, 92syl2anc 642 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( m  e.  ( ( ( |_
`  x )  +  1 ) ... ( |_ `  ( ( x ^ 2 )  / 
d ) ) )  <-> 
m  <_  ( |_ `  ( ( x ^
2 )  /  d
) ) ) )
94 flge 10953 . . . . . . . . . 10  |-  ( ( ( ( x ^
2 )  /  d
)  e.  RR  /\  m  e.  ZZ )  ->  ( m  <_  (
( x ^ 2 )  /  d )  <-> 
m  <_  ( |_ `  ( ( x ^
2 )  /  d
) ) ) )
9581, 13, 94syl2anc 642 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( m  <_ 
( ( x ^
2 )  /  d
)  <->  m  <_  ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )
9693, 95bitr4d 247 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( m  e.  ( ( ( |_
`  x )  +  1 ) ... ( |_ `  ( ( x ^ 2 )  / 
d ) ) )  <-> 
m  <_  ( (
x ^ 2 )  /  d ) ) )
9790, 96anbi12d 691 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( d  e.  ( 1 ... ( |_ `  x
) )  /\  m  e.  ( ( ( |_
`  x )  +  1 ) ... ( |_ `  ( ( x ^ 2 )  / 
d ) ) ) )  <->  ( d  <_  x  /\  m  <_  (
( x ^ 2 )  /  d ) ) ) )
9820flcld 10946 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( |_ `  ( x ^ 2 ) )  e.  ZZ )
99 elfz5 10806 . . . . . . . . . 10  |-  ( ( m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) )  /\  ( |_ `  ( x ^
2 ) )  e.  ZZ )  ->  (
m  e.  ( ( ( |_ `  x
)  +  1 ) ... ( |_ `  ( x ^ 2 ) ) )  <->  m  <_  ( |_ `  ( x ^ 2 ) ) ) )
10030, 98, 99syl2anc 642 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( m  e.  ( ( ( |_
`  x )  +  1 ) ... ( |_ `  ( x ^
2 ) ) )  <-> 
m  <_  ( |_ `  ( x ^ 2 ) ) ) )
101 flge 10953 . . . . . . . . . 10  |-  ( ( ( x ^ 2 )  e.  RR  /\  m  e.  ZZ )  ->  ( m  <_  (
x ^ 2 )  <-> 
m  <_  ( |_ `  ( x ^ 2 ) ) ) )
10220, 13, 101syl2anc 642 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( m  <_ 
( x ^ 2 )  <->  m  <_  ( |_
`  ( x ^
2 ) ) ) )
103100, 102bitr4d 247 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( m  e.  ( ( ( |_
`  x )  +  1 ) ... ( |_ `  ( x ^
2 ) ) )  <-> 
m  <_  ( x ^ 2 ) ) )
104 fznnfl 10982 . . . . . . . . . 10  |-  ( ( ( x ^ 2 )  /  m )  e.  RR  ->  (
d  e.  ( 1 ... ( |_ `  ( ( x ^
2 )  /  m
) ) )  <->  ( d  e.  NN  /\  d  <_ 
( ( x ^
2 )  /  m
) ) ) )
105104baibd 875 . . . . . . . . 9  |-  ( ( ( ( x ^
2 )  /  m
)  e.  RR  /\  d  e.  NN )  ->  ( d  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  /  m ) ) )  <-> 
d  <_  ( (
x ^ 2 )  /  m ) ) )
10658, 21, 105syl2anc 642 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( d  e.  ( 1 ... ( |_ `  ( ( x ^ 2 )  /  m ) ) )  <-> 
d  <_  ( (
x ^ 2 )  /  m ) ) )
107103, 106anbi12d 691 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_ `  (
x ^ 2 ) ) )  /\  d  e.  ( 1 ... ( |_ `  ( ( x ^ 2 )  /  m ) ) ) )  <->  ( m  <_ 
( x ^ 2 )  /\  d  <_ 
( ( x ^
2 )  /  m
) ) ) )
10887, 97, 1073bitr4d 276 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) ) )  ->  ( ( d  e.  ( 1 ... ( |_ `  x
) )  /\  m  e.  ( ( ( |_
`  x )  +  1 ) ... ( |_ `  ( ( x ^ 2 )  / 
d ) ) ) )  <->  ( m  e.  ( ( ( |_
`  x )  +  1 ) ... ( |_ `  ( x ^
2 ) ) )  /\  d  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  /  m ) ) ) ) ) )
109108ex 423 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
d  e.  NN  /\  m  e.  ( ZZ>= `  ( ( |_ `  x )  +  1 ) ) )  -> 
( ( d  e.  ( 1 ... ( |_ `  x ) )  /\  m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )  <->  ( m  e.  ( ( ( |_
`  x )  +  1 ) ... ( |_ `  ( x ^
2 ) ) )  /\  d  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  /  m ) ) ) ) ) ) )
1107, 11, 109pm5.21ndd 343 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
d  e.  ( 1 ... ( |_ `  x ) )  /\  m  e.  ( (
( |_ `  x
)  +  1 ) ... ( |_ `  ( ( x ^
2 )  /  d
) ) ) )  <-> 
( m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_
`  ( x ^
2 ) ) )  /\  d  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  /  m ) ) ) ) ) )
111 ssun2 3352 . . . . . . . 8  |-  ( ( ( |_ `  x
)  +  1 ) ... ( |_ `  ( ( x ^
2 )  /  d
) ) )  C_  ( ( 1 ... ( |_ `  x
) )  u.  (
( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )
11228adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( |_ `  x )  +  1 )  e.  NN )
113112, 31syl6eleq 2386 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( |_ `  x )  +  1 )  e.  (
ZZ>= `  1 ) )
114 dchrisum0lem1a 20651 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  <_  ( ( x ^
2 )  /  d
)  /\  ( |_ `  ( ( x ^
2 )  /  d
) )  e.  (
ZZ>= `  ( |_ `  x ) ) ) )
115114simprd 449 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( |_ `  ( ( x ^
2 )  /  d
) )  e.  (
ZZ>= `  ( |_ `  x ) ) )
116 fzsplit2 10831 . . . . . . . . 9  |-  ( ( ( ( |_ `  x )  +  1 )  e.  ( ZZ>= ` 
1 )  /\  ( |_ `  ( ( x ^ 2 )  / 
d ) )  e.  ( ZZ>= `  ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  (
( x ^ 2 )  /  d ) ) )  =  ( ( 1 ... ( |_ `  x ) )  u.  ( ( ( |_ `  x )  +  1 ) ... ( |_ `  (
( x ^ 2 )  /  d ) ) ) ) )
117113, 115, 116syl2anc 642 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  ( ( x ^
2 )  /  d
) ) )  =  ( ( 1 ... ( |_ `  x
) )  u.  (
( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) ) )
118111, 117syl5sseqr 3240 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( |_ `  x
)  +  1 ) ... ( |_ `  ( ( x ^
2 )  /  d
) ) )  C_  ( 1 ... ( |_ `  ( ( x ^ 2 )  / 
d ) ) ) )
119118sselda 3193 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )  ->  m  e.  ( 1 ... ( |_ `  ( ( x ^ 2 )  / 
d ) ) ) )
120 rpvmasum2.g . . . . . . . . 9  |-  G  =  (DChr `  N )
121 rpvmasum.z . . . . . . . . 9  |-  Z  =  (ℤ/n `  N )
122 rpvmasum2.d . . . . . . . . 9  |-  D  =  ( Base `  G
)
123 rpvmasum.l . . . . . . . . 9  |-  L  =  ( ZRHom `  Z
)
124 rpvmasum2.w . . . . . . . . . . . . 13  |-  W  =  { y  e.  ( D  \  {  .1.  } )  |  sum_ m  e.  NN  ( ( y `
 ( L `  m ) )  /  m )  =  0 }
125 ssrab2 3271 . . . . . . . . . . . . 13  |-  { y  e.  ( D  \  {  .1.  } )  | 
sum_ m  e.  NN  ( ( y `  ( L `  m ) )  /  m )  =  0 }  C_  ( D  \  {  .1.  } )
126124, 125eqsstri 3221 . . . . . . . . . . . 12  |-  W  C_  ( D  \  {  .1.  } )
127 dchrisum0.b . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  W )
128126, 127sseldi 3191 . . . . . . . . . . 11  |-  ( ph  ->  X  e.  ( D 
\  {  .1.  }
) )
129 eldifi 3311 . . . . . . . . . . 11  |-  ( X  e.  ( D  \  {  .1.  } )  ->  X  e.  D )
130128, 129syl 15 . . . . . . . . . 10  |-  ( ph  ->  X  e.  D )
131130ad3antrrr 710 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )  ->  X  e.  D )
132 elfzelz 10814 . . . . . . . . . 10  |-  ( m  e.  ( 1 ... ( |_ `  (
( x ^ 2 )  /  d ) ) )  ->  m  e.  ZZ )
133132adantl 452 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )  ->  m  e.  ZZ )
134120, 121, 122, 123, 131, 133dchrzrhcl 20500 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )  ->  ( X `  ( L `  m
) )  e.  CC )
135 elfznn 10835 . . . . . . . . . . . 12  |-  ( m  e.  ( 1 ... ( |_ `  (
( x ^ 2 )  /  d ) ) )  ->  m  e.  NN )
136135adantl 452 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )  ->  m  e.  NN )
137136nnrpd 10405 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )  ->  m  e.  RR+ )
138137rpsqrcld 11910 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )  ->  ( sqr `  m )  e.  RR+ )
139138rpcnd 10408 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )  ->  ( sqr `  m )  e.  CC )
140138rpne0d 10411 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )  ->  ( sqr `  m )  =/=  0
)
141134, 139, 140divcld 9552 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )  ->  ( ( X `  ( L `  m ) )  / 
( sqr `  m
) )  e.  CC )
1424adantl 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  d  e.  NN )
143142nnrpd 10405 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  d  e.  RR+ )
144143rpsqrcld 11910 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sqr `  d )  e.  RR+ )
145144rpcnne0d 10415 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( sqr `  d )  e.  CC  /\  ( sqr `  d )  =/=  0
) )
146145adantr 451 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )  ->  ( ( sqr `  d )  e.  CC  /\  ( sqr `  d )  =/=  0
) )
147146simpld 445 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )  ->  ( sqr `  d )  e.  CC )
148146simprd 449 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )  ->  ( sqr `  d )  =/=  0
)
149141, 147, 148divcld 9552 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )  ->  ( (
( X `  ( L `  m )
)  /  ( sqr `  m ) )  / 
( sqr `  d
) )  e.  CC )
150119, 149syldan 456 . . . . 5  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )  ->  ( (
( X `  ( L `  m )
)  /  ( sqr `  m ) )  / 
( sqr `  d
) )  e.  CC )
151150anasss 628 . . . 4  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
d  e.  ( 1 ... ( |_ `  x ) )  /\  m  e.  ( (
( |_ `  x
)  +  1 ) ... ( |_ `  ( ( x ^
2 )  /  d
) ) ) ) )  ->  ( (
( X `  ( L `  m )
)  /  ( sqr `  m ) )  / 
( sqr `  d
) )  e.  CC )
1521, 2, 3, 110, 151fsumcom2 12253 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) )
sum_ m  e.  (
( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) ( ( ( X `
 ( L `  m ) )  / 
( sqr `  m
) )  /  ( sqr `  d ) )  =  sum_ m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_
`  ( x ^
2 ) ) )
sum_ d  e.  ( 1 ... ( |_
`  ( ( x ^ 2 )  /  m ) ) ) ( ( ( X `
 ( L `  m ) )  / 
( sqr `  m
) )  /  ( sqr `  d ) ) )
153152mpteq2dva 4122 . 2  |-  ( ph  ->  ( x  e.  RR+  |->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) sum_ m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_ `  (
( x ^ 2 )  /  d ) ) ) ( ( ( X `  ( L `  m )
)  /  ( sqr `  m ) )  / 
( sqr `  d
) ) )  =  ( x  e.  RR+  |->  sum_
m  e.  ( ( ( |_ `  x
)  +  1 ) ... ( |_ `  ( x ^ 2 ) ) ) sum_ d  e.  ( 1 ... ( |_ `  ( ( x ^
2 )  /  m
) ) ) ( ( ( X `  ( L `  m ) )  /  ( sqr `  m ) )  / 
( sqr `  d
) ) ) )
15466a1i 10 . . 3  |-  ( ph  ->  1  e.  RR )
155 2cn 9832 . . . . . . . 8  |-  2  e.  CC
15615rpsqrcld 11910 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sqr `  x )  e.  RR+ )
157156rpcnd 10408 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sqr `  x )  e.  CC )
158 mulcl 8837 . . . . . . . 8  |-  ( ( 2  e.  CC  /\  ( sqr `  x )  e.  CC )  -> 
( 2  x.  ( sqr `  x ) )  e.  CC )
159155, 157, 158sylancr 644 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 2  x.  ( sqr `  x
) )  e.  CC )
160144rprecred 10417 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  ( sqr `  d
) )  e.  RR )
1611, 160fsumrecl 12223 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  e.  RR )
162161recnd 8877 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  e.  CC )
163162, 159subcld 9173 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x ) ) )  e.  CC )
164 2re 9831 . . . . . . . . . . 11  |-  2  e.  RR
165 dchrisum0.c . . . . . . . . . . . . 13  |-  ( ph  ->  C  e.  ( 0 [,)  +oo ) )
166 elrege0 10762 . . . . . . . . . . . . 13  |-  ( C  e.  ( 0 [,) 
+oo )  <->  ( C  e.  RR  /\  0  <_  C ) )
167165, 166sylib 188 . . . . . . . . . . . 12  |-  ( ph  ->  ( C  e.  RR  /\  0  <_  C )
)
168167simpld 445 . . . . . . . . . . 11  |-  ( ph  ->  C  e.  RR )
169 remulcl 8838 . . . . . . . . . . 11  |-  ( ( 2  e.  RR  /\  C  e.  RR )  ->  ( 2  x.  C
)  e.  RR )
170164, 168, 169sylancr 644 . . . . . . . . . 10  |-  ( ph  ->  ( 2  x.  C
)  e.  RR )
171170adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 2  x.  C )  e.  RR )
172171, 156rerpdivcld 10433 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
2  x.  C )  /  ( sqr `  x
) )  e.  RR )
173172recnd 8877 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
2  x.  C )  /  ( sqr `  x
) )  e.  CC )
174159, 163, 173adddird 8876 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
( 2  x.  ( sqr `  x ) )  +  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x
) ) ) )  x.  ( ( 2  x.  C )  / 
( sqr `  x
) ) )  =  ( ( ( 2  x.  ( sqr `  x
) )  x.  (
( 2  x.  C
)  /  ( sqr `  x ) ) )  +  ( ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x ) ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x
) ) ) ) )
175159, 162pncan3d 9176 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
2  x.  ( sqr `  x ) )  +  ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x
) ) ) )  =  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( 1  /  ( sqr `  d ) ) )
176175oveq1d 5889 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
( 2  x.  ( sqr `  x ) )  +  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x
) ) ) )  x.  ( ( 2  x.  C )  / 
( sqr `  x
) ) )  =  ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( 1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  / 
( sqr `  x
) ) ) )
177155a1i 10 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  2  e.  CC )
178177, 157, 173mulassd 8874 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
2  x.  ( sqr `  x ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x ) ) )  =  ( 2  x.  ( ( sqr `  x )  x.  (
( 2  x.  C
)  /  ( sqr `  x ) ) ) ) )
179171recnd 8877 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 2  x.  C )  e.  CC )
180156rpne0d 10411 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sqr `  x )  =/=  0
)
181179, 157, 180divcan2d 9554 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( sqr `  x )  x.  ( ( 2  x.  C )  /  ( sqr `  x ) ) )  =  ( 2  x.  C ) )
182181oveq2d 5890 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 2  x.  ( ( sqr `  x )  x.  (
( 2  x.  C
)  /  ( sqr `  x ) ) ) )  =  ( 2  x.  ( 2  x.  C ) ) )
183178, 182eqtrd 2328 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
2  x.  ( sqr `  x ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x ) ) )  =  ( 2  x.  ( 2  x.  C ) ) )
184183oveq1d 5889 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
( 2  x.  ( sqr `  x ) )  x.  ( ( 2  x.  C )  / 
( sqr `  x
) ) )  +  ( ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x
) ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x ) ) ) )  =  ( ( 2  x.  (
2  x.  C ) )  +  ( (
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x
) ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x ) ) ) ) )
185174, 176, 1843eqtr3d 2336 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x ) ) )  =  ( ( 2  x.  ( 2  x.  C ) )  +  ( ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x ) ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x
) ) ) ) )
186185mpteq2dva 4122 . . . 4  |-  ( ph  ->  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( 1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  / 
( sqr `  x
) ) ) )  =  ( x  e.  RR+  |->  ( ( 2  x.  ( 2  x.  C ) )  +  ( ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x
) ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x ) ) ) ) ) )
187 remulcl 8838 . . . . . . . 8  |-  ( ( 2  e.  RR  /\  ( 2  x.  C
)  e.  RR )  ->  ( 2  x.  ( 2  x.  C
) )  e.  RR )
188164, 170, 187sylancr 644 . . . . . . 7  |-  ( ph  ->  ( 2  x.  (
2  x.  C ) )  e.  RR )
189188recnd 8877 . . . . . 6  |-  ( ph  ->  ( 2  x.  (
2  x.  C ) )  e.  CC )
190189adantr 451 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 2  x.  ( 2  x.  C ) )  e.  CC )
191163, 173mulcld 8871 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x ) ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x
) ) )  e.  CC )
192 rpssre 10380 . . . . . 6  |-  RR+  C_  RR
193 o1const 12109 . . . . . 6  |-  ( (
RR+  C_  RR  /\  (
2  x.  ( 2  x.  C ) )  e.  CC )  -> 
( x  e.  RR+  |->  ( 2  x.  (
2  x.  C ) ) )  e.  O
( 1 ) )
194192, 189, 193sylancr 644 . . . . 5  |-  ( ph  ->  ( x  e.  RR+  |->  ( 2  x.  (
2  x.  C ) ) )  e.  O
( 1 ) )
195 eqid 2296 . . . . . . . 8  |-  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x ) ) ) )  =  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x ) ) ) )
196195divsqrsum 20292 . . . . . . 7  |-  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x ) ) ) )  e.  dom  ~~> r
197 rlimdmo1 12107 . . . . . . 7  |-  ( ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x ) ) ) )  e.  dom  ~~> r  ->  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x
) ) ) )  e.  O ( 1 ) )
198196, 197mp1i 11 . . . . . 6  |-  ( ph  ->  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x
) ) ) )  e.  O ( 1 ) )
199179, 157, 180divrecd 9555 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
2  x.  C )  /  ( sqr `  x
) )  =  ( ( 2  x.  C
)  x.  ( 1  /  ( sqr `  x
) ) ) )
200199mpteq2dva 4122 . . . . . . . 8  |-  ( ph  ->  ( x  e.  RR+  |->  ( ( 2  x.  C )  /  ( sqr `  x ) ) )  =  ( x  e.  RR+  |->  ( ( 2  x.  C )  x.  ( 1  / 
( sqr `  x
) ) ) ) )
201156rprecred 10417 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1  /  ( sqr `  x
) )  e.  RR )
202170recnd 8877 . . . . . . . . . 10  |-  ( ph  ->  ( 2  x.  C
)  e.  CC )
203 rlimconst 12034 . . . . . . . . . 10  |-  ( (
RR+  C_  RR  /\  (
2  x.  C )  e.  CC )  -> 
( x  e.  RR+  |->  ( 2  x.  C
) )  ~~> r  ( 2  x.  C ) )
204192, 202, 203sylancr 644 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  RR+  |->  ( 2  x.  C
) )  ~~> r  ( 2  x.  C ) )
205 sqrlim 20283 . . . . . . . . . 10  |-  ( x  e.  RR+  |->  ( 1  /  ( sqr `  x
) ) )  ~~> r  0
206205a1i 10 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  RR+  |->  ( 1  /  ( sqr `  x ) ) )  ~~> r  0 )
207171, 201, 204, 206rlimmul 12134 . . . . . . . 8  |-  ( ph  ->  ( x  e.  RR+  |->  ( ( 2  x.  C )  x.  (
1  /  ( sqr `  x ) ) ) )  ~~> r  ( ( 2  x.  C )  x.  0 ) )
208200, 207eqbrtrd 4059 . . . . . . 7  |-  ( ph  ->  ( x  e.  RR+  |->  ( ( 2  x.  C )  /  ( sqr `  x ) ) )  ~~> r  ( ( 2  x.  C )  x.  0 ) )
209 rlimo1 12106 . . . . . . 7  |-  ( ( x  e.  RR+  |->  ( ( 2  x.  C )  /  ( sqr `  x
) ) )  ~~> r  ( ( 2  x.  C
)  x.  0 )  ->  ( x  e.  RR+  |->  ( ( 2  x.  C )  / 
( sqr `  x
) ) )  e.  O ( 1 ) )
210208, 209syl 15 . . . . . 6  |-  ( ph  ->  ( x  e.  RR+  |->  ( ( 2  x.  C )  /  ( sqr `  x ) ) )  e.  O ( 1 ) )
211163, 173, 198, 210o1mul2 12114 . . . . 5  |-  ( ph  ->  ( x  e.  RR+  |->  ( ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x
) ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x ) ) ) )  e.  O
( 1 ) )
212190, 191, 194, 211o1add2 12113 . . . 4  |-  ( ph  ->  ( x  e.  RR+  |->  ( ( 2  x.  ( 2  x.  C
) )  +  ( ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( 1  /  ( sqr `  d ) )  -  ( 2  x.  ( sqr `  x
) ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x ) ) ) ) )  e.  O ( 1 ) )
213186, 212eqeltrd 2370 . . 3  |-  ( ph  ->  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( 1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  / 
( sqr `  x
) ) ) )  e.  O ( 1 ) )
214161, 172remulcld 8879 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x ) ) )  e.  RR )
2153, 150fsumcl 12222 . . . 4  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( ( ( |_
`  x )  +  1 ) ... ( |_ `  ( ( x ^ 2 )  / 
d ) ) ) ( ( ( X `
 ( L `  m ) )  / 
( sqr `  m
) )  /  ( sqr `  d ) )  e.  CC )
2161, 215fsumcl 12222 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) )
sum_ m  e.  (
( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) ( ( ( X `
 ( L `  m ) )  / 
( sqr `  m
) )  /  ( sqr `  d ) )  e.  CC )
217216abscld 11934 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( abs ` 
sum_ d  e.  ( 1 ... ( |_
`  x ) )
sum_ m  e.  (
( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) ( ( ( X `
 ( L `  m ) )  / 
( sqr `  m
) )  /  ( sqr `  d ) ) )  e.  RR )
218214recnd 8877 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x ) ) )  e.  CC )
219218abscld 11934 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( abs `  ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( 1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  / 
( sqr `  x
) ) ) )  e.  RR )
220215abscld 11934 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs ` 
sum_ m  e.  (
( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) ( ( ( X `
 ( L `  m ) )  / 
( sqr `  m
) )  /  ( sqr `  d ) ) )  e.  RR )
2211, 220fsumrecl 12223 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( abs `  sum_ m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_ `  (
( x ^ 2 )  /  d ) ) ) ( ( ( X `  ( L `  m )
)  /  ( sqr `  m ) )  / 
( sqr `  d
) ) )  e.  RR )
2221, 215fsumabs 12275 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( abs ` 
sum_ d  e.  ( 1 ... ( |_
`  x ) )
sum_ m  e.  (
( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) ( ( ( X `
 ( L `  m ) )  / 
( sqr `  m
) )  /  ( sqr `  d ) ) )  <_  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( abs `  sum_ m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_ `  (
( x ^ 2 )  /  d ) ) ) ( ( ( X `  ( L `  m )
)  /  ( sqr `  m ) )  / 
( sqr `  d
) ) ) )
223172adantr 451 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
2  x.  C )  /  ( sqr `  x
) )  e.  RR )
224160, 223remulcld 8879 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x ) ) )  e.  RR )
225119, 141syldan 456 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) )  ->  ( ( X `  ( L `  m ) )  / 
( sqr `  m
) )  e.  CC )
2263, 225fsumcl 12222 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( ( ( |_
`  x )  +  1 ) ... ( |_ `  ( ( x ^ 2 )  / 
d ) ) ) ( ( X `  ( L `  m ) )  /  ( sqr `  m ) )  e.  CC )
227226abscld 11934 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs ` 
sum_ m  e.  (
( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) ( ( X `  ( L `  m ) )  /  ( sqr `  m ) ) )  e.  RR )
228 rpvmasum.a . . . . . . . . . . 11  |-  ( ph  ->  N  e.  NN )
229 rpvmasum2.1 . . . . . . . . . . 11  |-  .1.  =  ( 0g `  G )
230 dchrisum0lem1.f . . . . . . . . . . 11  |-  F  =  ( a  e.  NN  |->  ( ( X `  ( L `  a ) )  /  ( sqr `  a ) ) )
231 dchrisum0.s . . . . . . . . . . 11  |-  ( ph  ->  seq  1 (  +  ,  F )  ~~>  S )
232 dchrisum0.1 . . . . . . . . . . 11  |-  ( ph  ->  A. y  e.  ( 1 [,)  +oo )
( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  y ) )  -  S ) )  <_ 
( C  /  ( sqr `  y ) ) )
233121, 123, 228, 120, 122, 229, 124, 127, 230, 165, 231, 232dchrisum0lem1b 20680 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs ` 
sum_ m  e.  (
( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) ( ( X `  ( L `  m ) )  /  ( sqr `  m ) ) )  <_  ( ( 2  x.  C )  / 
( sqr `  x
) ) )
234227, 223, 144, 233lediv1dd 10460 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  sum_ m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) ( ( X `  ( L `  m ) )  /  ( sqr `  m ) ) )  /  ( sqr `  d
) )  <_  (
( ( 2  x.  C )  /  ( sqr `  x ) )  /  ( sqr `  d
) ) )
235144rpcnd 10408 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sqr `  d )  e.  CC )
236144rpne0d 10411 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sqr `  d )  =/=  0
)
237226, 235, 236absdivd 11953 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( sum_ m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) ( ( X `  ( L `  m ) )  /  ( sqr `  m ) )  / 
( sqr `  d
) ) )  =  ( ( abs `  sum_ m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_ `  (
( x ^ 2 )  /  d ) ) ) ( ( X `  ( L `
 m ) )  /  ( sqr `  m
) ) )  / 
( abs `  ( sqr `  d ) ) ) )
2383, 235, 225, 236fsumdivc 12264 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_ `  (
( x ^ 2 )  /  d ) ) ) ( ( X `  ( L `
 m ) )  /  ( sqr `  m
) )  /  ( sqr `  d ) )  =  sum_ m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) ( ( ( X `
 ( L `  m ) )  / 
( sqr `  m
) )  /  ( sqr `  d ) ) )
239238fveq2d 5545 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( sum_ m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) ( ( X `  ( L `  m ) )  /  ( sqr `  m ) )  / 
( sqr `  d
) ) )  =  ( abs `  sum_ m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_ `  (
( x ^ 2 )  /  d ) ) ) ( ( ( X `  ( L `  m )
)  /  ( sqr `  m ) )  / 
( sqr `  d
) ) ) )
240144rprege0d 10413 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( sqr `  d )  e.  RR  /\  0  <_ 
( sqr `  d
) ) )
241 absid 11797 . . . . . . . . . . . 12  |-  ( ( ( sqr `  d
)  e.  RR  /\  0  <_  ( sqr `  d
) )  ->  ( abs `  ( sqr `  d
) )  =  ( sqr `  d ) )
242240, 241syl 15 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( sqr `  d
) )  =  ( sqr `  d ) )
243242oveq2d 5890 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  sum_ m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) ( ( X `  ( L `  m ) )  /  ( sqr `  m ) ) )  /  ( abs `  ( sqr `  d ) ) )  =  ( ( abs `  sum_ m  e.  ( ( ( |_
`  x )  +  1 ) ... ( |_ `  ( ( x ^ 2 )  / 
d ) ) ) ( ( X `  ( L `  m ) )  /  ( sqr `  m ) ) )  /  ( sqr `  d
) ) )
244237, 239, 2433eqtr3rd 2337 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  sum_ m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) ( ( X `  ( L `  m ) )  /  ( sqr `  m ) ) )  /  ( sqr `  d
) )  =  ( abs `  sum_ m  e.  ( ( ( |_
`  x )  +  1 ) ... ( |_ `  ( ( x ^ 2 )  / 
d ) ) ) ( ( ( X `
 ( L `  m ) )  / 
( sqr `  m
) )  /  ( sqr `  d ) ) ) )
245173adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
2  x.  C )  /  ( sqr `  x
) )  e.  CC )
246245, 235, 236divrec2d 9556 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( 2  x.  C
)  /  ( sqr `  x ) )  / 
( sqr `  d
) )  =  ( ( 1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  / 
( sqr `  x
) ) ) )
247234, 244, 2463brtr3d 4068 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs ` 
sum_ m  e.  (
( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) ( ( ( X `
 ( L `  m ) )  / 
( sqr `  m
) )  /  ( sqr `  d ) ) )  <_  ( (
1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x ) ) ) )
2481, 220, 224, 247fsumle 12273 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( abs `  sum_ m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_ `  (
( x ^ 2 )  /  d ) ) ) ( ( ( X `  ( L `  m )
)  /  ( sqr `  m ) )  / 
( sqr `  d
) ) )  <_  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  / 
( sqr `  x
) ) ) )
249160recnd 8877 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  ( sqr `  d
) )  e.  CC )
2501, 173, 249fsummulc1 12263 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x ) ) )  =  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  / 
( sqr `  d
) )  x.  (
( 2  x.  C
)  /  ( sqr `  x ) ) ) )
251248, 250breqtrrd 4065 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( abs `  sum_ m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_ `  (
( x ^ 2 )  /  d ) ) ) ( ( ( X `  ( L `  m )
)  /  ( sqr `  m ) )  / 
( sqr `  d
) ) )  <_ 
( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( 1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  / 
( sqr `  x
) ) ) )
252217, 221, 214, 222, 251letrd 8989 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( abs ` 
sum_ d  e.  ( 1 ... ( |_
`  x ) )
sum_ m  e.  (
( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) ( ( ( X `
 ( L `  m ) )  / 
( sqr `  m
) )  /  ( sqr `  d ) ) )  <_  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x ) ) ) )
253214leabsd 11913 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x ) ) )  <_  ( abs `  ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( 1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  / 
( sqr `  x
) ) ) ) )
254217, 214, 219, 252, 253letrd 8989 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( abs ` 
sum_ d  e.  ( 1 ... ( |_
`  x ) )
sum_ m  e.  (
( ( |_ `  x )  +  1 ) ... ( |_
`  ( ( x ^ 2 )  / 
d ) ) ) ( ( ( X `
 ( L `  m ) )  / 
( sqr `  m
) )  /  ( sqr `  d ) ) )  <_  ( abs `  ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( 1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  / 
( sqr `  x
) ) ) ) )
255254adantrr 697 . . 3  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  sum_ d  e.  ( 1 ... ( |_ `  x ) ) sum_ m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_ `  (
( x ^ 2 )  /  d ) ) ) ( ( ( X `  ( L `  m )
)  /  ( sqr `  m ) )  / 
( sqr `  d
) ) )  <_ 
( abs `  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  ( sqr `  d ) )  x.  ( ( 2  x.  C )  /  ( sqr `  x ) ) ) ) )
256154, 213, 214, 216, 255o1le 12142 . 2  |-  ( ph  ->  ( x  e.  RR+  |->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) sum_ m  e.  ( ( ( |_ `  x )  +  1 ) ... ( |_ `  (
( x ^ 2 )  /  d ) ) ) ( ( ( X `  ( L `  m )
)  /  ( sqr `  m ) )  / 
( sqr `  d
) ) )  e.  O ( 1 ) )
257153, 256eqeltrrd 2371 1  |-  ( ph  ->  ( x  e.  RR+  |->  sum_
m  e.  ( ( ( |_ `  x
)  +  1 ) ... ( |_ `  ( x ^ 2 ) ) ) sum_ d  e.  ( 1 ... ( |_ `  ( ( x ^
2 )  /  m
) ) ) ( ( ( X `  ( L `  m ) )  /  ( sqr `  m ) )  / 
( sqr `  d
) ) )  e.  O ( 1 ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632    e. wcel 1696    =/= wne 2459   A.wral 2556   {crab 2560    \ cdif 3162    u. cun 3163    C_ wss 3165   {csn 3653   class class class wbr 4039    e. cmpt 4093   dom cdm 4705   ` cfv 5271  (class class class)co 5874   CCcc 8751   RRcr 8752   0cc0 8753   1c1 8754    + caddc 8756    x. cmul 8758    +oocpnf 8880    < clt 8883    <_ cle 8884    - cmin 9053    / cdiv 9439   NNcn 9762   2c2 9811   NN0cn0 9981   ZZcz 10040   ZZ>=cuz 10246   RR+crp 10370   [,)cico 10674   ...cfz 10798   |_cfl 10940    seq cseq 11062   ^cexp 11120   sqrcsqr 11734   abscabs 11735    ~~> cli 11974    ~~> r crli 11975   O (
1 )co1 11976   sum_csu 12174   Basecbs 13164   0gc0g 13416   ZRHomczrh 16467  ℤ/nczn 16470  DChrcdchr 20487
This theorem is referenced by:  dchrisum0lem3  20684
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-inf2 7358  ax-cnex 8809  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-mulcom 8817  ax-addass 8818  ax-mulass 8819  ax-distr 8820  ax-i2m1 8821  ax-1ne0 8822  ax-1rid 8823  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826  ax-pre-lttri 8827  ax-pre-lttrn 8828  ax-pre-ltadd 8829  ax-pre-mulgt0 8830  ax-pre-sup 8831  ax-addf 8832  ax-mulf 8833
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rmo 2564  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-int 3879  df-iun 3923  df-iin 3924  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-se 4369  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-isom 5280  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-of 6094  df-1st 6138  df-2nd 6139  df-tpos 6250  df-riota 6320  df-recs 6404  df-rdg 6439  df-1o 6495  df-2o 6496  df-oadd 6499  df-er 6676  df-ec 6678  df-qs 6682  df-map 6790  df-pm 6791  df-ixp 6834  df-en 6880  df-dom 6881  df-sdom 6882  df-fin 6883  df-fi 7181  df-sup 7210  df-oi 7241  df-card 7588  df-cda 7810  df-pnf 8885  df-mnf 8886  df-xr 8887  df-ltxr 8888  df-le 8889  df-sub 9055  df-neg 9056  df-div 9440  df-nn 9763  df-2 9820  df-3 9821  df-4 9822  df-5 9823  df-6 9824  df-7 9825  df-8 9826  df-9 9827  df-10 9828  df-n0 9982  df-z 10041  df-dec 10141  df-uz 10247  df-q 10333  df-rp 10371  df-xneg 10468  df-xadd 10469  df-xmul 10470  df-ioo 10676  df-ioc 10677  df-ico 10678  df-icc 10679  df-fz 10799  df-fzo 10887  df-fl 10941  df-mod 10990  df-seq 11063  df-exp 11121  df-fac 11305  df-bc 11332  df-hash 11354  df-shft 11578  df-cj 11600  df-re 11601  df-im 11602  df-sqr 11736  df-abs 11737  df-limsup 11961  df-clim 11978  df-rlim 11979  df-o1 11980  df-lo1 11981  df-sum 12175  df-ef 12365  df-sin 12367  df-cos 12368  df-pi 12370  df-struct 13166  df-ndx 13167  df-slot 13168  df-base 13169  df-sets 13170  df-ress 13171  df-plusg 13237  df-mulr 13238  df-starv 13239  df-sca 13240  df-vsca 13241  df-tset 13243  df-ple 13244  df-ds 13246  df-hom 13248  df-cco 13249  df-rest 13343  df-topn 13344  df-topgen 13360  df-pt 13361  df-prds 13364  df-xrs 13419  df-0g 13420  df-gsum 13421  df-qtop 13426  df-imas 13427  df-divs 13428  df-xps 13429  df-mre 13504  df-mrc 13505  df-acs 13507  df-mnd 14383  df-mhm 14431  df-submnd 14432  df-grp 14505  df-minusg 14506  df-sbg 14507  df-mulg 14508  df-subg 14634  df-nsg 14635  df-eqg 14636  df-ghm 14697  df-cntz 14809  df-cmn 15107  df-abl 15108  df-mgp 15342  df-rng 15356  df-cring 15357  df-ur 15358  df-oppr 15421  df-dvdsr 15439  df-unit 15440  df-rnghom 15512  df-subrg 15559  df-lmod 15645  df-lss 15706  df-lsp 15745  df-sra 15941  df-rgmod 15942  df-lidl 15943  df-rsp 15944  df-2idl 16000  df-xmet 16389  df-met 16390  df-bl 16391  df-mopn 16392  df-cnfld 16394  df-zrh 16471  df-zn 16474  df-top 16652  df-bases 16654  df-topon 16655  df-topsp 16656  df-cld 16772  df-ntr 16773  df-cls 16774  df-nei 16851  df-lp 16884  df-perf 16885  df-cn 16973  df-cnp 16974  df-haus 17059  df-cmp 17130  df-tx 17273  df-hmeo 17462  df-fbas 17536  df-fg 17537  df-fil 17557  df-fm 17649  df-flim 17650  df-flf 17651  df-xms 17901  df-ms 17902  df-tms 17903  df-cncf 18398  df-limc 19232  df-dv 19233  df-log 19930  df-cxp 19931  df-dchr 20488
  Copyright terms: Public domain W3C validator