Metamath Proof Explorer

Theorem dchrisum0lem3

Description: Lemma for dchrisum0 . (Contributed by Mario Carneiro, 12-May-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 dchrisum0lem3 
|- ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) e. O(1) )

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 1red 
 |-  ( ph -> 1 e. RR )
14 sumex 
 |-  sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) e. _V
15 14 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) e. _V )
16 sumex 
 |-  sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) e. _V
17 16 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) e. _V )
18 7 ssrab3 
 |-  W C_ ( D \ { .1. } )
19 difss 
 |-  ( D \ { .1. } ) C_ D
20 18 19 sstri 
 |-  W C_ D
21 20 8 sselid 
 |-  ( ph -> X e. D )
22 18 8 sselid 
 |-  ( ph -> X e. ( D \ { .1. } ) )
23 eldifsni 
 |-  ( X e. ( D \ { .1. } ) -> X =/= .1. )
24 22 23 syl 
 |-  ( ph -> X =/= .1. )
25 eqid 
 |-  ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
26 1 2 3 4 5 6 21 24 25 dchrmusumlema 
 |-  ( ph -> E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) )
27 3 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> N e. NN )
28 8 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> X e. W )
29 10 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> C e. ( 0 [,) +oo ) )
30 11 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> seq 1 ( + , F ) ~~> S )
31 12 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - S ) ) <_ ( C / ( sqrt ` y ) ) )
32 eqid 
 |-  ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) ) = ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) )
33 32 divsqrsum 
 |-  ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) ) e. dom ~~>r
34 32 divsqrsumf 
 |-  ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) ) : RR+ --> RR
35 ax-resscn 
 |-  RR C_ CC
36 fss 
 |-  ( ( ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) ) : RR+ --> RR /\ RR C_ CC ) -> ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) ) : RR+ --> CC )
37 34 35 36 mp2an 
 |-  ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) ) : RR+ --> CC
38 37 a1i 
 |-  ( ph -> ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) ) : RR+ --> CC )
39 rpsup 
 |-  sup ( RR+ , RR* , < ) = +oo
40 39 a1i 
 |-  ( ph -> sup ( RR+ , RR* , < ) = +oo )
41 38 40 rlimdm 
 |-  ( ph -> ( ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) ) e. dom ~~>r <-> ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) ) ~~>r ( ~~>r ` ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) ) ) ) )
42 33 41 mpbii 
 |-  ( ph -> ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) ) ~~>r ( ~~>r ` ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) ) ) )
43 42 adantr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) ) ~~>r ( ~~>r ` ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) ) ) )
44 simprl 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> c e. ( 0 [,) +oo ) )
45 simprrl 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t )
46 simprrr 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) )
47 1 2 27 4 5 6 7 28 9 29 30 31 32 43 25 44 45 46 dchrisum0lem2 
 |-  ( ( ph /\ ( c e. ( 0 [,) +oo ) /\ ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) ) ) -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) e. O(1) )
48 47 rexlimdvaa 
 |-  ( ph -> ( E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) e. O(1) ) )
49 48 exlimdv 
 |-  ( ph -> ( E. t E. c e. ( 0 [,) +oo ) ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ~~> t /\ A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) ) ` ( |_ ` y ) ) - t ) ) <_ ( c / y ) ) -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) e. O(1) ) )
50 26 49 mpd 
 |-  ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) e. O(1) )
51 1 2 3 4 5 6 7 8 9 10 11 12 dchrisum0lem1 
 |-  ( ph -> ( x e. RR+ |-> sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) e. O(1) )
52 15 17 50 51 o1add2 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) + sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) ) e. O(1) )
53 ovexd 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) + sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) e. _V )
54 fzfid 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` ( x ^ 2 ) ) ) e. Fin )
55 fzfid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) -> ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) e. Fin )
56 21 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) -> X e. D )
57 elfzelz 
 |-  ( m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) -> m e. ZZ )
58 57 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) -> m e. ZZ )
59 4 1 5 2 56 58 dchrzrhcl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) -> ( X ` ( L ` m ) ) e. CC )
60 59 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( X ` ( L ` m ) ) e. CC )
61 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) -> m e. NN )
62 61 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) -> m e. NN )
63 62 nnrpd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) -> m e. RR+ )
64 elfznn 
 |-  ( d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) -> d e. NN )
65 64 nnrpd 
 |-  ( d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) -> d e. RR+ )
66 rpmulcl 
 |-  ( ( m e. RR+ /\ d e. RR+ ) -> ( m x. d ) e. RR+ )
67 63 65 66 syl2an 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( m x. d ) e. RR+ )
68 67 rpsqrtcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( sqrt ` ( m x. d ) ) e. RR+ )
69 68 rpcnd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( sqrt ` ( m x. d ) ) e. CC )
70 68 rpne0d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( sqrt ` ( m x. d ) ) =/= 0 )
71 60 69 70 divcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) e. CC )
72 55 71 fsumcl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) -> sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) e. CC )
73 54 72 fsumcl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) e. CC )
74 73 abscld 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) e. RR )
75 74 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) e. RR )
76 62 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> m e. NN )
77 76 nnrpd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> m e. RR+ )
78 77 rprege0d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( m e. RR /\ 0 <_ m ) )
79 64 adantl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> d e. NN )
80 79 nnrpd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> d e. RR+ )
81 80 rprege0d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( d e. RR /\ 0 <_ d ) )
82 sqrtmul 
 |-  ( ( ( m e. RR /\ 0 <_ m ) /\ ( d e. RR /\ 0 <_ d ) ) -> ( sqrt ` ( m x. d ) ) = ( ( sqrt ` m ) x. ( sqrt ` d ) ) )
83 78 81 82 syl2anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( sqrt ` ( m x. d ) ) = ( ( sqrt ` m ) x. ( sqrt ` d ) ) )
84 83 oveq2d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) = ( ( X ` ( L ` m ) ) / ( ( sqrt ` m ) x. ( sqrt ` d ) ) ) )
85 77 rpsqrtcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( sqrt ` m ) e. RR+ )
86 85 rpcnne0d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( ( sqrt ` m ) e. CC /\ ( sqrt ` m ) =/= 0 ) )
87 80 rpsqrtcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( sqrt ` d ) e. RR+ )
88 87 rpcnne0d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( ( sqrt ` d ) e. CC /\ ( sqrt ` d ) =/= 0 ) )
89 divdiv1 
 |-  ( ( ( X ` ( L ` m ) ) e. CC /\ ( ( sqrt ` m ) e. CC /\ ( sqrt ` m ) =/= 0 ) /\ ( ( sqrt ` d ) e. CC /\ ( sqrt ` d ) =/= 0 ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) = ( ( X ` ( L ` m ) ) / ( ( sqrt ` m ) x. ( sqrt ` d ) ) ) )
90 60 86 88 89 syl3anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) = ( ( X ` ( L ` m ) ) / ( ( sqrt ` m ) x. ( sqrt ` d ) ) ) )
91 84 90 eqtr4d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) = ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) )
92 91 sumeq2dv 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) -> sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) = sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) )
93 92 sumeq2dv 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) )
94 93 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) )
95 simpr 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
96 95 rpred 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR )
97 reflcl 
 |-  ( x e. RR -> ( |_ ` x ) e. RR )
98 96 97 syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( |_ ` x ) e. RR )
99 98 ltp1d 
 |-  ( ( ph /\ x e. RR+ ) -> ( |_ ` x ) < ( ( |_ ` x ) + 1 ) )
100 fzdisj 
 |-  ( ( |_ ` x ) < ( ( |_ ` x ) + 1 ) -> ( ( 1 ... ( |_ ` x ) ) i^i ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) ) = (/) )
101 99 100 syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) i^i ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) ) = (/) )
102 101 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( 1 ... ( |_ ` x ) ) i^i ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) ) = (/) )
103 95 rprege0d 
 |-  ( ( ph /\ x e. RR+ ) -> ( x e. RR /\ 0 <_ x ) )
104 flge0nn0 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 )
105 nn0p1nn 
 |-  ( ( |_ ` x ) e. NN0 -> ( ( |_ ` x ) + 1 ) e. NN )
106 103 104 105 3syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( |_ ` x ) + 1 ) e. NN )
107 nnuz 
 |-  NN = ( ZZ>= ` 1 )
108 106 107 eleqtrdi 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` 1 ) )
109 108 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` 1 ) )
110 96 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR )
111 2z 
 |-  2 e. ZZ
112 rpexpcl 
 |-  ( ( x e. RR+ /\ 2 e. ZZ ) -> ( x ^ 2 ) e. RR+ )
113 95 111 112 sylancl 
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^ 2 ) e. RR+ )
114 113 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x ^ 2 ) e. RR+ )
115 114 rpred 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x ^ 2 ) e. RR )
116 110 recnd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. CC )
117 116 mulid1d 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x x. 1 ) = x )
118 simprr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 <_ x )
119 1red 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 e. RR )
120 rpregt0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 < x ) )
121 120 ad2antrl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x e. RR /\ 0 < x ) )
122 lemul2 
 |-  ( ( 1 e. RR /\ x e. RR /\ ( x e. RR /\ 0 < x ) ) -> ( 1 <_ x <-> ( x x. 1 ) <_ ( x x. x ) ) )
123 119 110 121 122 syl3anc 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 <_ x <-> ( x x. 1 ) <_ ( x x. x ) ) )
124 118 123 mpbid 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x x. 1 ) <_ ( x x. x ) )
125 117 124 eqbrtrrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x <_ ( x x. x ) )
126 116 sqvald 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x ^ 2 ) = ( x x. x ) )
127 125 126 breqtrrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x <_ ( x ^ 2 ) )
128 flword2 
 |-  ( ( x e. RR /\ ( x ^ 2 ) e. RR /\ x <_ ( x ^ 2 ) ) -> ( |_ ` ( x ^ 2 ) ) e. ( ZZ>= ` ( |_ ` x ) ) )
129 110 115 127 128 syl3anc 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` ( x ^ 2 ) ) e. ( ZZ>= ` ( |_ ` x ) ) )
130 fzsplit2 
 |-  ( ( ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` 1 ) /\ ( |_ ` ( x ^ 2 ) ) e. ( ZZ>= ` ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x ^ 2 ) ) ) = ( ( 1 ... ( |_ ` x ) ) u. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) ) )
131 109 129 130 syl2anc 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 ... ( |_ ` ( x ^ 2 ) ) ) = ( ( 1 ... ( |_ ` x ) ) u. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) ) )
132 fzfid 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 ... ( |_ ` ( x ^ 2 ) ) ) e. Fin )
133 92 72 eqeltrrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) -> sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) e. CC )
134 133 adantlrr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) ) -> sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) e. CC )
135 102 131 132 134 fsumsplit 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) = ( sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) + sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) )
136 94 135 eqtrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) + sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) )
137 136 fveq2d 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) = ( abs ` ( sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) + sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) ) )
138 75 137 eqled 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) <_ ( abs ` ( sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) + sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) ) )
139 13 52 53 73 138 o1le 
 |-  ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` ( m x. d ) ) ) ) e. O(1) )