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

Metamath Proof Explorer

Theorem dchrisum0lem2a

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 ) ) )
dchrisum0lem2.h 
|- H = ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) )
dchrisum0lem2.u 
|- ( ph -> H ~~>r U )
Assertion dchrisum0lem2a 
|- ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) ) 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 dchrisum0lem2.h 
 |-  H = ( y e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` y ) ) ( 1 / ( sqrt ` d ) ) - ( 2 x. ( sqrt ` y ) ) ) )
14 dchrisum0lem2.u 
 |-  ( ph -> H ~~>r U )
15 fzfid 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
16 simpl 
 |-  ( ( ph /\ x e. RR+ ) -> ph )
17 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` x ) ) -> m e. NN )
18 7 ssrab3 
 |-  W C_ ( D \ { .1. } )
19 18 8 sselid 
 |-  ( ph -> X e. ( D \ { .1. } ) )
20 19 eldifad 
 |-  ( ph -> X e. D )
21 20 adantr 
 |-  ( ( ph /\ m e. NN ) -> X e. D )
22 nnz 
 |-  ( m e. NN -> m e. ZZ )
23 22 adantl 
 |-  ( ( ph /\ m e. NN ) -> m e. ZZ )
24 4 1 5 2 21 23 dchrzrhcl 
 |-  ( ( ph /\ m e. NN ) -> ( X ` ( L ` m ) ) e. CC )
25 nnrp 
 |-  ( m e. NN -> m e. RR+ )
26 25 adantl 
 |-  ( ( ph /\ m e. NN ) -> m e. RR+ )
27 26 rpsqrtcld 
 |-  ( ( ph /\ m e. NN ) -> ( sqrt ` m ) e. RR+ )
28 27 rpcnd 
 |-  ( ( ph /\ m e. NN ) -> ( sqrt ` m ) e. CC )
29 27 rpne0d 
 |-  ( ( ph /\ m e. NN ) -> ( sqrt ` m ) =/= 0 )
30 24 28 29 divcld 
 |-  ( ( ph /\ m e. NN ) -> ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) e. CC )
31 16 17 30 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) e. CC )
32 15 31 fsumcl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) e. CC )
33 rlimcl 
 |-  ( H ~~>r U -> U e. CC )
34 14 33 syl 
 |-  ( ph -> U e. CC )
35 34 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> U e. CC )
36 0xr 
 |-  0 e. RR*
37 0lt1 
 |-  0 < 1
38 df-ioo 
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
39 df-ico 
 |-  [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
40 xrltletr 
 |-  ( ( 0 e. RR* /\ 1 e. RR* /\ w e. RR* ) -> ( ( 0 < 1 /\ 1 <_ w ) -> 0 < w ) )
41 38 39 40 ixxss1 
 |-  ( ( 0 e. RR* /\ 0 < 1 ) -> ( 1 [,) +oo ) C_ ( 0 (,) +oo ) )
42 36 37 41 mp2an 
 |-  ( 1 [,) +oo ) C_ ( 0 (,) +oo )
43 ioorp 
 |-  ( 0 (,) +oo ) = RR+
44 42 43 sseqtri 
 |-  ( 1 [,) +oo ) C_ RR+
45 resmpt 
 |-  ( ( 1 [,) +oo ) C_ RR+ -> ( ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) |` ( 1 [,) +oo ) ) = ( x e. ( 1 [,) +oo ) |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) )
46 44 45 ax-mp 
 |-  ( ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) |` ( 1 [,) +oo ) ) = ( x e. ( 1 [,) +oo ) |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) )
47 44 sseli 
 |-  ( x e. ( 1 [,) +oo ) -> x e. RR+ )
48 17 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m e. NN )
49 2fveq3 
 |-  ( a = m -> ( X ` ( L ` a ) ) = ( X ` ( L ` m ) ) )
50 fveq2 
 |-  ( a = m -> ( sqrt ` a ) = ( sqrt ` m ) )
51 49 50 oveq12d 
 |-  ( a = m -> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) = ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) )
52 ovex 
 |-  ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) e. _V
53 51 9 52 fvmpt3i 
 |-  ( m e. NN -> ( F ` m ) = ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) )
54 48 53 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( F ` m ) = ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) )
55 47 54 sylanl2 
 |-  ( ( ( ph /\ x e. ( 1 [,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( F ` m ) = ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) )
56 1re 
 |-  1 e. RR
57 elicopnf 
 |-  ( 1 e. RR -> ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) ) )
58 56 57 ax-mp 
 |-  ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) )
59 flge1nn 
 |-  ( ( x e. RR /\ 1 <_ x ) -> ( |_ ` x ) e. NN )
60 58 59 sylbi 
 |-  ( x e. ( 1 [,) +oo ) -> ( |_ ` x ) e. NN )
61 60 adantl 
 |-  ( ( ph /\ x e. ( 1 [,) +oo ) ) -> ( |_ ` x ) e. NN )
62 nnuz 
 |-  NN = ( ZZ>= ` 1 )
63 61 62 eleqtrdi 
 |-  ( ( ph /\ x e. ( 1 [,) +oo ) ) -> ( |_ ` x ) e. ( ZZ>= ` 1 ) )
64 47 31 sylanl2 
 |-  ( ( ( ph /\ x e. ( 1 [,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) e. CC )
65 55 63 64 fsumser 
 |-  ( ( ph /\ x e. ( 1 [,) +oo ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) = ( seq 1 ( + , F ) ` ( |_ ` x ) ) )
66 65 mpteq2dva 
 |-  ( ph -> ( x e. ( 1 [,) +oo ) |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) = ( x e. ( 1 [,) +oo ) |-> ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) )
67 46 66 eqtrid 
 |-  ( ph -> ( ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) |` ( 1 [,) +oo ) ) = ( x e. ( 1 [,) +oo ) |-> ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) )
68 fveq2 
 |-  ( m = ( |_ ` x ) -> ( seq 1 ( + , F ) ` m ) = ( seq 1 ( + , F ) ` ( |_ ` x ) ) )
69 rpssre 
 |-  RR+ C_ RR
70 69 a1i 
 |-  ( ph -> RR+ C_ RR )
71 44 70 sstrid 
 |-  ( ph -> ( 1 [,) +oo ) C_ RR )
72 1zzd 
 |-  ( ph -> 1 e. ZZ )
73 51 cbvmptv 
 |-  ( a e. NN |-> ( ( X ` ( L ` a ) ) / ( sqrt ` a ) ) ) = ( m e. NN |-> ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) )
74 9 73 eqtri 
 |-  F = ( m e. NN |-> ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) )
75 30 74 fmptd 
 |-  ( ph -> F : NN --> CC )
76 75 ffvelcdmda 
 |-  ( ( ph /\ m e. NN ) -> ( F ` m ) e. CC )
77 62 72 76 serf 
 |-  ( ph -> seq 1 ( + , F ) : NN --> CC )
78 77 feqmptd 
 |-  ( ph -> seq 1 ( + , F ) = ( m e. NN |-> ( seq 1 ( + , F ) ` m ) ) )
79 78 11 eqbrtrrd 
 |-  ( ph -> ( m e. NN |-> ( seq 1 ( + , F ) ` m ) ) ~~> S )
80 77 ffvelcdmda 
 |-  ( ( ph /\ m e. NN ) -> ( seq 1 ( + , F ) ` m ) e. CC )
81 58 simprbi 
 |-  ( x e. ( 1 [,) +oo ) -> 1 <_ x )
82 81 adantl 
 |-  ( ( ph /\ x e. ( 1 [,) +oo ) ) -> 1 <_ x )
83 62 68 71 72 79 80 82 climrlim2 
 |-  ( ph -> ( x e. ( 1 [,) +oo ) |-> ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) ~~>r S )
84 rlimo1 
 |-  ( ( x e. ( 1 [,) +oo ) |-> ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) ~~>r S -> ( x e. ( 1 [,) +oo ) |-> ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) e. O(1) )
85 83 84 syl 
 |-  ( ph -> ( x e. ( 1 [,) +oo ) |-> ( seq 1 ( + , F ) ` ( |_ ` x ) ) ) e. O(1) )
86 67 85 eqeltrd 
 |-  ( ph -> ( ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) |` ( 1 [,) +oo ) ) e. O(1) )
87 32 fmpttd 
 |-  ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) : RR+ --> CC )
88 1red 
 |-  ( ph -> 1 e. RR )
89 87 70 88 o1resb 
 |-  ( ph -> ( ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) e. O(1) <-> ( ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) |` ( 1 [,) +oo ) ) e. O(1) ) )
90 86 89 mpbird 
 |-  ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) e. O(1) )
91 o1const 
 |-  ( ( RR+ C_ RR /\ U e. CC ) -> ( x e. RR+ |-> U ) e. O(1) )
92 69 34 91 sylancr 
 |-  ( ph -> ( x e. RR+ |-> U ) e. O(1) )
93 32 35 90 92 o1mul2 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. U ) ) e. O(1) )
94 simpr 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
95 2z 
 |-  2 e. ZZ
96 rpexpcl 
 |-  ( ( x e. RR+ /\ 2 e. ZZ ) -> ( x ^ 2 ) e. RR+ )
97 94 95 96 sylancl 
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^ 2 ) e. RR+ )
98 17 nnrpd 
 |-  ( m e. ( 1 ... ( |_ ` x ) ) -> m e. RR+ )
99 rpdivcl 
 |-  ( ( ( x ^ 2 ) e. RR+ /\ m e. RR+ ) -> ( ( x ^ 2 ) / m ) e. RR+ )
100 97 98 99 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x ^ 2 ) / m ) e. RR+ )
101 13 divsqrsumf 
 |-  H : RR+ --> RR
102 101 ffvelcdmi 
 |-  ( ( ( x ^ 2 ) / m ) e. RR+ -> ( H ` ( ( x ^ 2 ) / m ) ) e. RR )
103 100 102 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( H ` ( ( x ^ 2 ) / m ) ) e. RR )
104 103 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( H ` ( ( x ^ 2 ) / m ) ) e. CC )
105 31 104 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) e. CC )
106 15 105 fsumcl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) e. CC )
107 32 35 mulcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. U ) e. CC )
108 14 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> H ~~>r U )
109 108 33 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> U e. CC )
110 31 109 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. U ) e. CC )
111 15 105 110 fsumsub 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) - ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. U ) ) = ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. U ) ) )
112 31 104 109 subdid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) = ( ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) - ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. U ) ) )
113 112 sumeq2dv 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) = sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) - ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. U ) ) )
114 15 35 31 fsummulc1 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. U ) = sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. U ) )
115 114 oveq2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) - ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. U ) ) = ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) - sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. U ) ) )
116 111 113 115 3eqtr4d 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) = ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) - ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. U ) ) )
117 116 mpteq2dva 
 |-  ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) ) = ( x e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) - ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. U ) ) ) )
118 104 109 subcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) e. CC )
119 31 118 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) e. CC )
120 15 119 fsumcl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) e. CC )
121 120 abscld 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) ) e. RR )
122 119 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) ) e. RR )
123 15 122 fsumrecl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) ) e. RR )
124 1red 
 |-  ( ( ph /\ x e. RR+ ) -> 1 e. RR )
125 15 119 fsumabs 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) ) <_ sum_ m e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) ) )
126 rprege0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 <_ x ) )
127 126 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( x e. RR /\ 0 <_ x ) )
128 127 simpld 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR )
129 reflcl 
 |-  ( x e. RR -> ( |_ ` x ) e. RR )
130 128 129 syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( |_ ` x ) e. RR )
131 130 94 rerpdivcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( |_ ` x ) / x ) e. RR )
132 simplr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
133 132 rprecred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / x ) e. RR )
134 31 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) e. RR )
135 98 rpsqrtcld 
 |-  ( m e. ( 1 ... ( |_ ` x ) ) -> ( sqrt ` m ) e. RR+ )
136 135 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` m ) e. RR+ )
137 136 rprecred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / ( sqrt ` m ) ) e. RR )
138 118 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) e. RR )
139 136 132 rpdivcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqrt ` m ) / x ) e. RR+ )
140 69 139 sselid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqrt ` m ) / x ) e. RR )
141 31 absge0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) )
142 118 absge0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) )
143 16 17 24 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( X ` ( L ` m ) ) e. CC )
144 136 rpcnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` m ) e. CC )
145 136 rpne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` m ) =/= 0 )
146 143 144 145 absdivd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) = ( ( abs ` ( X ` ( L ` m ) ) ) / ( abs ` ( sqrt ` m ) ) ) )
147 136 rprege0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqrt ` m ) e. RR /\ 0 <_ ( sqrt ` m ) ) )
148 absid 
 |-  ( ( ( sqrt ` m ) e. RR /\ 0 <_ ( sqrt ` m ) ) -> ( abs ` ( sqrt ` m ) ) = ( sqrt ` m ) )
149 147 148 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( sqrt ` m ) ) = ( sqrt ` m ) )
150 149 oveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( X ` ( L ` m ) ) ) / ( abs ` ( sqrt ` m ) ) ) = ( ( abs ` ( X ` ( L ` m ) ) ) / ( sqrt ` m ) ) )
151 146 150 eqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) = ( ( abs ` ( X ` ( L ` m ) ) ) / ( sqrt ` m ) ) )
152 143 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( X ` ( L ` m ) ) ) e. RR )
153 1red 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
154 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
155 20 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> X e. D )
156 3 nnnn0d 
 |-  ( ph -> N e. NN0 )
157 1 154 2 znzrhfo 
 |-  ( N e. NN0 -> L : ZZ -onto-> ( Base ` Z ) )
158 fof 
 |-  ( L : ZZ -onto-> ( Base ` Z ) -> L : ZZ --> ( Base ` Z ) )
159 156 157 158 3syl 
 |-  ( ph -> L : ZZ --> ( Base ` Z ) )
160 159 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> L : ZZ --> ( Base ` Z ) )
161 elfzelz 
 |-  ( m e. ( 1 ... ( |_ ` x ) ) -> m e. ZZ )
162 ffvelcdm 
 |-  ( ( L : ZZ --> ( Base ` Z ) /\ m e. ZZ ) -> ( L ` m ) e. ( Base ` Z ) )
163 160 161 162 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( L ` m ) e. ( Base ` Z ) )
164 4 5 1 154 155 163 dchrabs2 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( X ` ( L ` m ) ) ) <_ 1 )
165 152 153 136 164 lediv1dd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( X ` ( L ` m ) ) ) / ( sqrt ` m ) ) <_ ( 1 / ( sqrt ` m ) ) )
166 151 165 eqbrtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) <_ ( 1 / ( sqrt ` m ) ) )
167 13 108 divsqrtsum2 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ ( ( x ^ 2 ) / m ) e. RR+ ) -> ( abs ` ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) <_ ( 1 / ( sqrt ` ( ( x ^ 2 ) / m ) ) ) )
168 100 167 mpdan 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) <_ ( 1 / ( sqrt ` ( ( x ^ 2 ) / m ) ) ) )
169 97 rprege0d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( x ^ 2 ) e. RR /\ 0 <_ ( x ^ 2 ) ) )
170 sqrtdiv 
 |-  ( ( ( ( x ^ 2 ) e. RR /\ 0 <_ ( x ^ 2 ) ) /\ m e. RR+ ) -> ( sqrt ` ( ( x ^ 2 ) / m ) ) = ( ( sqrt ` ( x ^ 2 ) ) / ( sqrt ` m ) ) )
171 169 98 170 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` ( ( x ^ 2 ) / m ) ) = ( ( sqrt ` ( x ^ 2 ) ) / ( sqrt ` m ) ) )
172 126 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( x e. RR /\ 0 <_ x ) )
173 sqrtsq 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( sqrt ` ( x ^ 2 ) ) = x )
174 172 173 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` ( x ^ 2 ) ) = x )
175 174 oveq1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqrt ` ( x ^ 2 ) ) / ( sqrt ` m ) ) = ( x / ( sqrt ` m ) ) )
176 171 175 eqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` ( ( x ^ 2 ) / m ) ) = ( x / ( sqrt ` m ) ) )
177 176 oveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / ( sqrt ` ( ( x ^ 2 ) / m ) ) ) = ( 1 / ( x / ( sqrt ` m ) ) ) )
178 rpcnne0 
 |-  ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) )
179 178 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( x e. CC /\ x =/= 0 ) )
180 136 rpcnne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqrt ` m ) e. CC /\ ( sqrt ` m ) =/= 0 ) )
181 recdiv 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( ( sqrt ` m ) e. CC /\ ( sqrt ` m ) =/= 0 ) ) -> ( 1 / ( x / ( sqrt ` m ) ) ) = ( ( sqrt ` m ) / x ) )
182 179 180 181 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / ( x / ( sqrt ` m ) ) ) = ( ( sqrt ` m ) / x ) )
183 177 182 eqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / ( sqrt ` ( ( x ^ 2 ) / m ) ) ) = ( ( sqrt ` m ) / x ) )
184 168 183 breqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) <_ ( ( sqrt ` m ) / x ) )
185 134 137 138 140 141 142 166 184 lemul12ad 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) x. ( abs ` ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) ) <_ ( ( 1 / ( sqrt ` m ) ) x. ( ( sqrt ` m ) / x ) ) )
186 31 118 absmuld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) ) = ( ( abs ` ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) ) x. ( abs ` ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) ) )
187 1cnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. CC )
188 dmdcan 
 |-  ( ( ( ( sqrt ` m ) e. CC /\ ( sqrt ` m ) =/= 0 ) /\ ( x e. CC /\ x =/= 0 ) /\ 1 e. CC ) -> ( ( ( sqrt ` m ) / x ) x. ( 1 / ( sqrt ` m ) ) ) = ( 1 / x ) )
189 180 179 187 188 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( sqrt ` m ) / x ) x. ( 1 / ( sqrt ` m ) ) ) = ( 1 / x ) )
190 139 rpcnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqrt ` m ) / x ) e. CC )
191 reccl 
 |-  ( ( ( sqrt ` m ) e. CC /\ ( sqrt ` m ) =/= 0 ) -> ( 1 / ( sqrt ` m ) ) e. CC )
192 180 191 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / ( sqrt ` m ) ) e. CC )
193 190 192 mulcomd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( sqrt ` m ) / x ) x. ( 1 / ( sqrt ` m ) ) ) = ( ( 1 / ( sqrt ` m ) ) x. ( ( sqrt ` m ) / x ) ) )
194 189 193 eqtr3d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / x ) = ( ( 1 / ( sqrt ` m ) ) x. ( ( sqrt ` m ) / x ) ) )
195 185 186 194 3brtr4d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) ) <_ ( 1 / x ) )
196 15 122 133 195 fsumle 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) ) <_ sum_ m e. ( 1 ... ( |_ ` x ) ) ( 1 / x ) )
197 flge0nn0 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 )
198 hashfz1 
 |-  ( ( |_ ` x ) e. NN0 -> ( # ` ( 1 ... ( |_ ` x ) ) ) = ( |_ ` x ) )
199 127 197 198 3syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( # ` ( 1 ... ( |_ ` x ) ) ) = ( |_ ` x ) )
200 199 oveq1d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. ( 1 / x ) ) = ( ( |_ ` x ) x. ( 1 / x ) ) )
201 94 rpreccld 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 / x ) e. RR+ )
202 201 rpcnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 / x ) e. CC )
203 fsumconst 
 |-  ( ( ( 1 ... ( |_ ` x ) ) e. Fin /\ ( 1 / x ) e. CC ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( 1 / x ) = ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. ( 1 / x ) ) )
204 15 202 203 syl2anc 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( 1 / x ) = ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. ( 1 / x ) ) )
205 130 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( |_ ` x ) e. CC )
206 178 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( x e. CC /\ x =/= 0 ) )
207 206 simpld 
 |-  ( ( ph /\ x e. RR+ ) -> x e. CC )
208 206 simprd 
 |-  ( ( ph /\ x e. RR+ ) -> x =/= 0 )
209 205 207 208 divrecd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( |_ ` x ) / x ) = ( ( |_ ` x ) x. ( 1 / x ) ) )
210 200 204 209 3eqtr4d 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( 1 / x ) = ( ( |_ ` x ) / x ) )
211 196 210 breqtrd 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) ) <_ ( ( |_ ` x ) / x ) )
212 flle 
 |-  ( x e. RR -> ( |_ ` x ) <_ x )
213 128 212 syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( |_ ` x ) <_ x )
214 128 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> x e. CC )
215 214 mulridd 
 |-  ( ( ph /\ x e. RR+ ) -> ( x x. 1 ) = x )
216 213 215 breqtrrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( |_ ` x ) <_ ( x x. 1 ) )
217 rpregt0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 < x ) )
218 217 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( x e. RR /\ 0 < x ) )
219 ledivmul 
 |-  ( ( ( |_ ` x ) e. RR /\ 1 e. RR /\ ( x e. RR /\ 0 < x ) ) -> ( ( ( |_ ` x ) / x ) <_ 1 <-> ( |_ ` x ) <_ ( x x. 1 ) ) )
220 130 124 218 219 syl3anc 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( ( |_ ` x ) / x ) <_ 1 <-> ( |_ ` x ) <_ ( x x. 1 ) ) )
221 216 220 mpbird 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( |_ ` x ) / x ) <_ 1 )
222 123 131 124 211 221 letrd 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) ) <_ 1 )
223 121 123 124 125 222 letrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) ) <_ 1 )
224 223 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) ) <_ 1 )
225 70 120 88 88 224 elo1d 
 |-  ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( ( H ` ( ( x ^ 2 ) / m ) ) - U ) ) ) e. O(1) )
226 117 225 eqeltrrd 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) - ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. U ) ) ) e. O(1) )
227 106 107 226 o1dif 
 |-  ( ph -> ( ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) ) e. O(1) <-> ( x e. RR+ |-> ( sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. U ) ) e. O(1) ) )
228 93 227 mpbird 
 |-  ( ph -> ( x e. RR+ |-> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` m ) ) / ( sqrt ` m ) ) x. ( H ` ( ( x ^ 2 ) / m ) ) ) ) e. O(1) )