This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dchrisum0lem1

Description: Lemma for dchrisum0 . (Contributed by Mario Carneiro, 12-May-2016) (Revised 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 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) )

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+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
14 fzfid 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) e. Fin )
15 fzfid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) e. Fin )
16 elfznn 
 |-  ( d e. ( 1 ... ( |_ ` x ) ) -> d e. NN )
17 elfzuz 
 |-  ( m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) -> m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) )
18 16 17 anim12i 
 |-  ( ( d e. ( 1 ... ( |_ ` x ) ) /\ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) )
19 18 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( d e. ( 1 ... ( |_ ` x ) ) /\ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) )
20 elfzuz 
 |-  ( m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) -> m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) )
21 elfznn 
 |-  ( d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) -> d e. NN )
22 20 21 anim12ci 
 |-  ( ( m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) )
23 22 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) /\ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ) -> ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) )
24 eluzelz 
 |-  ( m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) -> m e. ZZ )
25 24 ad2antll 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> m e. ZZ )
26 25 zred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> m e. RR )
27 simpr 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
28 2z 
 |-  2 e. ZZ
29 rpexpcl 
 |-  ( ( x e. RR+ /\ 2 e. ZZ ) -> ( x ^ 2 ) e. RR+ )
30 27 28 29 sylancl 
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^ 2 ) e. RR+ )
31 30 rpred 
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^ 2 ) e. RR )
32 31 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( x ^ 2 ) e. RR )
33 simprl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> d e. NN )
34 33 nnrpd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> d e. RR+ )
35 26 32 34 lemuldivd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( ( m x. d ) <_ ( x ^ 2 ) <-> m <_ ( ( x ^ 2 ) / d ) ) )
36 33 nnred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> d e. RR )
37 27 rprege0d 
 |-  ( ( ph /\ x e. RR+ ) -> ( x e. RR /\ 0 <_ x ) )
38 flge0nn0 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 )
39 nn0p1nn 
 |-  ( ( |_ ` x ) e. NN0 -> ( ( |_ ` x ) + 1 ) e. NN )
40 37 38 39 3syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( |_ ` x ) + 1 ) e. NN )
41 40 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( ( |_ ` x ) + 1 ) e. NN )
42 simprr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) )
43 eluznn 
 |-  ( ( ( ( |_ ` x ) + 1 ) e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) -> m e. NN )
44 41 42 43 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> m e. NN )
45 44 nnrpd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> m e. RR+ )
46 36 32 45 lemuldiv2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( ( m x. d ) <_ ( x ^ 2 ) <-> d <_ ( ( x ^ 2 ) / m ) ) )
47 35 46 bitr3d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( m <_ ( ( x ^ 2 ) / d ) <-> d <_ ( ( x ^ 2 ) / m ) ) )
48 rpcn 
 |-  ( x e. RR+ -> x e. CC )
49 48 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x e. CC )
50 49 sqvald 
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^ 2 ) = ( x x. x ) )
51 50 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( x ^ 2 ) = ( x x. x ) )
52 simplr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> x e. RR+ )
53 52 rpred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> x e. RR )
54 reflcl 
 |-  ( x e. RR -> ( |_ ` x ) e. RR )
55 peano2re 
 |-  ( ( |_ ` x ) e. RR -> ( ( |_ ` x ) + 1 ) e. RR )
56 53 54 55 3syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( ( |_ ` x ) + 1 ) e. RR )
57 fllep1 
 |-  ( x e. RR -> x <_ ( ( |_ ` x ) + 1 ) )
58 53 57 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> x <_ ( ( |_ ` x ) + 1 ) )
59 eluzle 
 |-  ( m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) -> ( ( |_ ` x ) + 1 ) <_ m )
60 59 ad2antll 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( ( |_ ` x ) + 1 ) <_ m )
61 53 56 26 58 60 letrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> x <_ m )
62 53 26 52 lemul1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( x <_ m <-> ( x x. x ) <_ ( m x. x ) ) )
63 61 62 mpbid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( x x. x ) <_ ( m x. x ) )
64 51 63 eqbrtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( x ^ 2 ) <_ ( m x. x ) )
65 32 53 45 ledivmuld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( ( ( x ^ 2 ) / m ) <_ x <-> ( x ^ 2 ) <_ ( m x. x ) ) )
66 64 65 mpbird 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( ( x ^ 2 ) / m ) <_ x )
67 nnre 
 |-  ( d e. NN -> d e. RR )
68 67 ad2antrl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> d e. RR )
69 32 44 nndivred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( ( x ^ 2 ) / m ) e. RR )
70 letr 
 |-  ( ( d e. RR /\ ( ( x ^ 2 ) / m ) e. RR /\ x e. RR ) -> ( ( d <_ ( ( x ^ 2 ) / m ) /\ ( ( x ^ 2 ) / m ) <_ x ) -> d <_ x ) )
71 68 69 53 70 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( ( d <_ ( ( x ^ 2 ) / m ) /\ ( ( x ^ 2 ) / m ) <_ x ) -> d <_ x ) )
72 66 71 mpan2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( d <_ ( ( x ^ 2 ) / m ) -> d <_ x ) )
73 47 72 sylbid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( m <_ ( ( x ^ 2 ) / d ) -> d <_ x ) )
74 73 pm4.71rd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( m <_ ( ( x ^ 2 ) / d ) <-> ( d <_ x /\ m <_ ( ( x ^ 2 ) / d ) ) ) )
75 nnge1 
 |-  ( d e. NN -> 1 <_ d )
76 75 ad2antrl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> 1 <_ d )
77 1re 
 |-  1 e. RR
78 0lt1 
 |-  0 < 1
79 77 78 pm3.2i 
 |-  ( 1 e. RR /\ 0 < 1 )
80 34 rpregt0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( d e. RR /\ 0 < d ) )
81 30 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( x ^ 2 ) e. RR+ )
82 81 rpregt0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( ( x ^ 2 ) e. RR /\ 0 < ( x ^ 2 ) ) )
83 lediv2 
 |-  ( ( ( 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 ) ) )
84 79 80 82 83 mp3an2i 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( 1 <_ d <-> ( ( x ^ 2 ) / d ) <_ ( ( x ^ 2 ) / 1 ) ) )
85 76 84 mpbid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( ( x ^ 2 ) / d ) <_ ( ( x ^ 2 ) / 1 ) )
86 32 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( x ^ 2 ) e. CC )
87 86 div1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( ( x ^ 2 ) / 1 ) = ( x ^ 2 ) )
88 85 87 breqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( ( x ^ 2 ) / d ) <_ ( x ^ 2 ) )
89 simpl 
 |-  ( ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) -> d e. NN )
90 nndivre 
 |-  ( ( ( x ^ 2 ) e. RR /\ d e. NN ) -> ( ( x ^ 2 ) / d ) e. RR )
91 31 89 90 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( ( x ^ 2 ) / d ) e. RR )
92 letr 
 |-  ( ( m e. RR /\ ( ( x ^ 2 ) / d ) e. RR /\ ( x ^ 2 ) e. RR ) -> ( ( m <_ ( ( x ^ 2 ) / d ) /\ ( ( x ^ 2 ) / d ) <_ ( x ^ 2 ) ) -> m <_ ( x ^ 2 ) ) )
93 26 91 32 92 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( ( m <_ ( ( x ^ 2 ) / d ) /\ ( ( x ^ 2 ) / d ) <_ ( x ^ 2 ) ) -> m <_ ( x ^ 2 ) ) )
94 88 93 mpan2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( m <_ ( ( x ^ 2 ) / d ) -> m <_ ( x ^ 2 ) ) )
95 47 94 sylbird 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( d <_ ( ( x ^ 2 ) / m ) -> m <_ ( x ^ 2 ) ) )
96 95 pm4.71rd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( d <_ ( ( x ^ 2 ) / m ) <-> ( m <_ ( x ^ 2 ) /\ d <_ ( ( x ^ 2 ) / m ) ) ) )
97 47 74 96 3bitr3d 
 |-  ( ( ( 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 ) ) ) )
98 fznnfl 
 |-  ( x e. RR -> ( d e. ( 1 ... ( |_ ` x ) ) <-> ( d e. NN /\ d <_ x ) ) )
99 98 baibd 
 |-  ( ( x e. RR /\ d e. NN ) -> ( d e. ( 1 ... ( |_ ` x ) ) <-> d <_ x ) )
100 53 33 99 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( d e. ( 1 ... ( |_ ` x ) ) <-> d <_ x ) )
101 91 flcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( |_ ` ( ( x ^ 2 ) / d ) ) e. ZZ )
102 elfz5 
 |-  ( ( m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) /\ ( |_ ` ( ( x ^ 2 ) / d ) ) e. ZZ ) -> ( m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) <-> m <_ ( |_ ` ( ( x ^ 2 ) / d ) ) ) )
103 42 101 102 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) <-> m <_ ( |_ ` ( ( x ^ 2 ) / d ) ) ) )
104 flge 
 |-  ( ( ( ( x ^ 2 ) / d ) e. RR /\ m e. ZZ ) -> ( m <_ ( ( x ^ 2 ) / d ) <-> m <_ ( |_ ` ( ( x ^ 2 ) / d ) ) ) )
105 91 25 104 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( m <_ ( ( x ^ 2 ) / d ) <-> m <_ ( |_ ` ( ( x ^ 2 ) / d ) ) ) )
106 103 105 bitr4d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) <-> m <_ ( ( x ^ 2 ) / d ) ) )
107 100 106 anbi12d 
 |-  ( ( ( 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 ) ) ) )
108 32 flcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( |_ ` ( x ^ 2 ) ) e. ZZ )
109 elfz5 
 |-  ( ( m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) /\ ( |_ ` ( x ^ 2 ) ) e. ZZ ) -> ( m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) <-> m <_ ( |_ ` ( x ^ 2 ) ) ) )
110 42 108 109 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) <-> m <_ ( |_ ` ( x ^ 2 ) ) ) )
111 flge 
 |-  ( ( ( x ^ 2 ) e. RR /\ m e. ZZ ) -> ( m <_ ( x ^ 2 ) <-> m <_ ( |_ ` ( x ^ 2 ) ) ) )
112 32 25 111 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( m <_ ( x ^ 2 ) <-> m <_ ( |_ ` ( x ^ 2 ) ) ) )
113 110 112 bitr4d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) <-> m <_ ( x ^ 2 ) ) )
114 fznnfl 
 |-  ( ( ( x ^ 2 ) / m ) e. RR -> ( d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) <-> ( d e. NN /\ d <_ ( ( x ^ 2 ) / m ) ) ) )
115 114 baibd 
 |-  ( ( ( ( x ^ 2 ) / m ) e. RR /\ d e. NN ) -> ( d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) <-> d <_ ( ( x ^ 2 ) / m ) ) )
116 69 33 115 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. NN /\ m e. ( ZZ>= ` ( ( |_ ` x ) + 1 ) ) ) ) -> ( d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) <-> d <_ ( ( x ^ 2 ) / m ) ) )
117 113 116 anbi12d 
 |-  ( ( ( 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 ) ) ) )
118 97 107 117 3bitr4d 
 |-  ( ( ( 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 ) ) ) ) ) )
119 118 ex 
 |-  ( ( 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 ) ) ) ) ) ) )
120 19 23 119 pm5.21ndd 
 |-  ( ( 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 ) ) ) ) ) )
121 ssun2 
 |-  ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) C_ ( ( 1 ... ( |_ ` x ) ) u. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) )
122 40 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( |_ ` x ) + 1 ) e. NN )
123 nnuz 
 |-  NN = ( ZZ>= ` 1 )
124 122 123 eleqtrdi 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` 1 ) )
125 dchrisum0lem1a 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x <_ ( ( x ^ 2 ) / d ) /\ ( |_ ` ( ( x ^ 2 ) / d ) ) e. ( ZZ>= ` ( |_ ` x ) ) ) )
126 125 simprd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( ( x ^ 2 ) / d ) ) e. ( ZZ>= ` ( |_ ` x ) ) )
127 fzsplit2 
 |-  ( ( ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` 1 ) /\ ( |_ ` ( ( x ^ 2 ) / d ) ) e. ( ZZ>= ` ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) = ( ( 1 ... ( |_ ` x ) ) u. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) )
128 124 126 127 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) = ( ( 1 ... ( |_ ` x ) ) u. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) )
129 121 128 sseqtrrid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) C_ ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) )
130 129 sselda 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) )
131 7 ssrab3 
 |-  W C_ ( D \ { .1. } )
132 131 8 sselid 
 |-  ( ph -> X e. ( D \ { .1. } ) )
133 132 eldifad 
 |-  ( ph -> X e. D )
134 133 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> X e. D )
135 elfzelz 
 |-  ( m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) -> m e. ZZ )
136 135 adantl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> m e. ZZ )
137 4 1 5 2 134 136 dchrzrhcl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( X ` ( L ` m ) ) e. CC )
138 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) -> m e. NN )
139 138 adantl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> m e. NN )
140 139 nnrpd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> m e. RR+ )
141 140 rpsqrtcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( sqrt ` m ) e. RR+ )
142 141 rpcnd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( sqrt ` m ) e. CC )
143 141 rpne0d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( sqrt ` m ) =/= 0 )
144 137 142 143 divcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) e. CC )
145 16 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. NN )
146 145 nnrpd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. RR+ )
147 146 rpsqrtcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` d ) e. RR+ )
148 147 rpcnne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqrt ` d ) e. CC /\ ( sqrt ` d ) =/= 0 ) )
149 148 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( ( sqrt ` d ) e. CC /\ ( sqrt ` d ) =/= 0 ) )
150 149 simpld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( sqrt ` d ) e. CC )
151 149 simprd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( sqrt ` d ) =/= 0 )
152 144 150 151 divcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) e. CC )
153 130 152 syldan 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) e. CC )
154 153 anasss 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( d e. ( 1 ... ( |_ ` x ) ) /\ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) e. CC )
155 13 14 15 120 154 fsumcom2 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( 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 ) ) )
156 155 mpteq2dva 
 |-  ( ph -> ( x e. RR+ |-> sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) = ( x e. RR+ |-> sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( x ^ 2 ) ) ) sum_ d e. ( 1 ... ( |_ ` ( ( x ^ 2 ) / m ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) )
157 77 a1i 
 |-  ( ph -> 1 e. RR )
158 2cn 
 |-  2 e. CC
159 27 rpsqrtcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( sqrt ` x ) e. RR+ )
160 159 rpcnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( sqrt ` x ) e. CC )
161 mulcl 
 |-  ( ( 2 e. CC /\ ( sqrt ` x ) e. CC ) -> ( 2 x. ( sqrt ` x ) ) e. CC )
162 158 160 161 sylancr 
 |-  ( ( ph /\ x e. RR+ ) -> ( 2 x. ( sqrt ` x ) ) e. CC )
163 147 rprecred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / ( sqrt ` d ) ) e. RR )
164 13 163 fsumrecl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) e. RR )
165 164 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) e. CC )
166 165 162 subcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) e. CC )
167 2re 
 |-  2 e. RR
168 elrege0 
 |-  ( C e. ( 0 [,) +oo ) <-> ( C e. RR /\ 0 <_ C ) )
169 10 168 sylib 
 |-  ( ph -> ( C e. RR /\ 0 <_ C ) )
170 169 simpld 
 |-  ( ph -> C e. RR )
171 remulcl 
 |-  ( ( 2 e. RR /\ C e. RR ) -> ( 2 x. C ) e. RR )
172 167 170 171 sylancr 
 |-  ( ph -> ( 2 x. C ) e. RR )
173 172 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( 2 x. C ) e. RR )
174 173 159 rerpdivcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 2 x. C ) / ( sqrt ` x ) ) e. RR )
175 174 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 2 x. C ) / ( sqrt ` x ) ) e. CC )
176 162 166 175 adddird 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( ( 2 x. ( sqrt ` x ) ) + ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) = ( ( ( 2 x. ( sqrt ` x ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) + ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) ) )
177 162 165 pncan3d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 2 x. ( sqrt ` x ) ) + ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) )
178 177 oveq1d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( ( 2 x. ( sqrt ` x ) ) + ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) = ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) )
179 2cnd 
 |-  ( ( ph /\ x e. RR+ ) -> 2 e. CC )
180 179 160 175 mulassd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 2 x. ( sqrt ` x ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) = ( 2 x. ( ( sqrt ` x ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) ) )
181 173 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( 2 x. C ) e. CC )
182 159 rpne0d 
 |-  ( ( ph /\ x e. RR+ ) -> ( sqrt ` x ) =/= 0 )
183 181 160 182 divcan2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( sqrt ` x ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) = ( 2 x. C ) )
184 183 oveq2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( 2 x. ( ( sqrt ` x ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) ) = ( 2 x. ( 2 x. C ) ) )
185 180 184 eqtrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 2 x. ( sqrt ` x ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) = ( 2 x. ( 2 x. C ) ) )
186 185 oveq1d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( ( 2 x. ( sqrt ` x ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) + ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) ) = ( ( 2 x. ( 2 x. C ) ) + ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) ) )
187 176 178 186 3eqtr3d 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) = ( ( 2 x. ( 2 x. C ) ) + ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) ) )
188 187 mpteq2dva 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) ) = ( x e. RR+ |-> ( ( 2 x. ( 2 x. C ) ) + ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) ) ) )
189 remulcl 
 |-  ( ( 2 e. RR /\ ( 2 x. C ) e. RR ) -> ( 2 x. ( 2 x. C ) ) e. RR )
190 167 172 189 sylancr 
 |-  ( ph -> ( 2 x. ( 2 x. C ) ) e. RR )
191 190 recnd 
 |-  ( ph -> ( 2 x. ( 2 x. C ) ) e. CC )
192 191 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( 2 x. ( 2 x. C ) ) e. CC )
193 166 175 mulcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) e. CC )
194 rpssre 
 |-  RR+ C_ RR
195 o1const 
 |-  ( ( RR+ C_ RR /\ ( 2 x. ( 2 x. C ) ) e. CC ) -> ( x e. RR+ |-> ( 2 x. ( 2 x. C ) ) ) e. O(1) )
196 194 191 195 sylancr 
 |-  ( ph -> ( x e. RR+ |-> ( 2 x. ( 2 x. C ) ) ) e. O(1) )
197 eqid 
 |-  ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) ) = ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) )
198 197 divsqrsum 
 |-  ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) ) e. dom ~~>r
199 rlimdmo1 
 |-  ( ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) ) e. dom ~~>r -> ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) ) e. O(1) )
200 198 199 mp1i 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) ) e. O(1) )
201 181 160 182 divrecd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 2 x. C ) / ( sqrt ` x ) ) = ( ( 2 x. C ) x. ( 1 / ( sqrt ` x ) ) ) )
202 201 mpteq2dva 
 |-  ( ph -> ( x e. RR+ |-> ( ( 2 x. C ) / ( sqrt ` x ) ) ) = ( x e. RR+ |-> ( ( 2 x. C ) x. ( 1 / ( sqrt ` x ) ) ) ) )
203 159 rprecred 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 / ( sqrt ` x ) ) e. RR )
204 172 recnd 
 |-  ( ph -> ( 2 x. C ) e. CC )
205 rlimconst 
 |-  ( ( RR+ C_ RR /\ ( 2 x. C ) e. CC ) -> ( x e. RR+ |-> ( 2 x. C ) ) ~~>r ( 2 x. C ) )
206 194 204 205 sylancr 
 |-  ( ph -> ( x e. RR+ |-> ( 2 x. C ) ) ~~>r ( 2 x. C ) )
207 sqrtlim 
 |-  ( x e. RR+ |-> ( 1 / ( sqrt ` x ) ) ) ~~>r 0
208 207 a1i 
 |-  ( ph -> ( x e. RR+ |-> ( 1 / ( sqrt ` x ) ) ) ~~>r 0 )
209 173 203 206 208 rlimmul 
 |-  ( ph -> ( x e. RR+ |-> ( ( 2 x. C ) x. ( 1 / ( sqrt ` x ) ) ) ) ~~>r ( ( 2 x. C ) x. 0 ) )
210 202 209 eqbrtrd 
 |-  ( ph -> ( x e. RR+ |-> ( ( 2 x. C ) / ( sqrt ` x ) ) ) ~~>r ( ( 2 x. C ) x. 0 ) )
211 rlimo1 
 |-  ( ( x e. RR+ |-> ( ( 2 x. C ) / ( sqrt ` x ) ) ) ~~>r ( ( 2 x. C ) x. 0 ) -> ( x e. RR+ |-> ( ( 2 x. C ) / ( sqrt ` x ) ) ) e. O(1) )
212 210 211 syl 
 |-  ( ph -> ( x e. RR+ |-> ( ( 2 x. C ) / ( sqrt ` x ) ) ) e. O(1) )
213 166 175 200 212 o1mul2 
 |-  ( ph -> ( x e. RR+ |-> ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) ) e. O(1) )
214 192 193 196 213 o1add2 
 |-  ( ph -> ( x e. RR+ |-> ( ( 2 x. ( 2 x. C ) ) + ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` x ) ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) ) ) e. O(1) )
215 188 214 eqeltrd 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) ) e. O(1) )
216 164 174 remulcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) e. RR )
217 15 153 fsumcl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) e. CC )
218 13 217 fsumcl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) e. CC )
219 218 abscld 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) e. RR )
220 216 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) e. CC )
221 220 abscld 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) ) e. RR )
222 217 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) e. RR )
223 13 222 fsumrecl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) e. RR )
224 13 217 fsumabs 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) <_ sum_ d e. ( 1 ... ( |_ ` x ) ) ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) )
225 174 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. C ) / ( sqrt ` x ) ) e. RR )
226 163 225 remulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) e. RR )
227 130 144 syldan 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ) -> ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) e. CC )
228 15 227 fsumcl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) e. CC )
229 228 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 )
230 1 2 3 4 5 6 7 8 9 10 11 12 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 ) ) )
231 229 225 147 230 lediv1dd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) / ( sqrt ` d ) ) <_ ( ( ( 2 x. C ) / ( sqrt ` x ) ) / ( sqrt ` d ) ) )
232 147 rpcnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` d ) e. CC )
233 147 rpne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` d ) =/= 0 )
234 228 232 233 absdivd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) = ( ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) / ( abs ` ( sqrt ` d ) ) ) )
235 15 232 227 233 fsumdivc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) = sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) )
236 235 fveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) = ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) )
237 147 rprege0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqrt ` d ) e. RR /\ 0 <_ ( sqrt ` d ) ) )
238 absid 
 |-  ( ( ( sqrt ` d ) e. RR /\ 0 <_ ( sqrt ` d ) ) -> ( abs ` ( sqrt ` d ) ) = ( sqrt ` d ) )
239 237 238 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( sqrt ` d ) ) = ( sqrt ` d ) )
240 239 oveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) / ( abs ` ( sqrt ` d ) ) ) = ( ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) / ( sqrt ` d ) ) )
241 234 236 240 3eqtr3rd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) / ( sqrt ` d ) ) = ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) )
242 175 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. C ) / ( sqrt ` x ) ) e. CC )
243 242 232 233 divrec2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( 2 x. C ) / ( sqrt ` x ) ) / ( sqrt ` d ) ) = ( ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) )
244 231 241 243 3brtr3d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) <_ ( ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) )
245 13 222 226 244 fsumle 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) <_ sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) )
246 163 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / ( sqrt ` d ) ) e. CC )
247 13 175 246 fsummulc1 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) )
248 245 247 breqtrrd 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( abs ` sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) <_ ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) )
249 219 223 216 224 248 letrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) <_ ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) )
250 216 leabsd 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) <_ ( abs ` ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) ) )
251 219 216 221 249 250 letrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) <_ ( abs ` ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) ) )
252 251 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) <_ ( abs ` ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` d ) ) x. ( ( 2 x. C ) / ( sqrt ` x ) ) ) ) )
253 157 215 216 218 252 o1le 
 |-  ( ph -> ( x e. RR+ |-> sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( ( ( |_ ` x ) + 1 ) ... ( |_ ` ( ( x ^ 2 ) / d ) ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) / ( sqrt ` d ) ) ) e. O(1) )
254 156 253 eqeltrrd 
 |-  ( 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) )