Metamath Proof Explorer

Theorem dchrisum0fno1

Description: The sum sum_ k <_ x , F ( x ) / sqrt k is divergent (i.e. not eventually bounded). Equation 9.4.30 of Shapiro, p. 383. (Contributed by Mario Carneiro, 5-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 )
dchrisum0f.f 
|- F = ( b e. NN |-> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) )
dchrisum0f.x 
|- ( ph -> X e. D )
dchrisum0flb.r 
|- ( ph -> X : ( Base ` Z ) --> RR )
dchrisum0fno1.a 
|- ( ph -> ( x e. RR+ |-> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( F ` k ) / ( sqrt ` k ) ) ) e. O(1) )
Assertion dchrisum0fno1 
|- -. ph

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 dchrisum0f.f 
 |-  F = ( b e. NN |-> sum_ v e. { q e. NN | q || b } ( X ` ( L ` v ) ) )
8 dchrisum0f.x 
 |-  ( ph -> X e. D )
9 dchrisum0flb.r 
 |-  ( ph -> X : ( Base ` Z ) --> RR )
10 dchrisum0fno1.a 
 |-  ( ph -> ( x e. RR+ |-> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( F ` k ) / ( sqrt ` k ) ) ) e. O(1) )
11 logno1 
 |-  -. ( x e. RR+ |-> ( log ` x ) ) e. O(1)
12 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
13 12 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR )
14 13 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC )
15 2cnd 
 |-  ( ( ph /\ x e. RR+ ) -> 2 e. CC )
16 2ne0 
 |-  2 =/= 0
17 16 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> 2 =/= 0 )
18 14 15 17 divcan2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( 2 x. ( ( log ` x ) / 2 ) ) = ( log ` x ) )
19 18 mpteq2dva 
 |-  ( ph -> ( x e. RR+ |-> ( 2 x. ( ( log ` x ) / 2 ) ) ) = ( x e. RR+ |-> ( log ` x ) ) )
20 13 rehalfcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) / 2 ) e. RR )
21 20 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) / 2 ) e. CC )
22 rpssre 
 |-  RR+ C_ RR
23 2cn 
 |-  2 e. CC
24 o1const 
 |-  ( ( RR+ C_ RR /\ 2 e. CC ) -> ( x e. RR+ |-> 2 ) e. O(1) )
25 22 23 24 mp2an 
 |-  ( x e. RR+ |-> 2 ) e. O(1)
26 25 a1i 
 |-  ( ph -> ( x e. RR+ |-> 2 ) e. O(1) )
27 1red 
 |-  ( ph -> 1 e. RR )
28 sumex 
 |-  sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( F ` k ) / ( sqrt ` k ) ) e. _V
29 28 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( F ` k ) / ( sqrt ` k ) ) e. _V )
30 20 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) / 2 ) e. RR )
31 12 ad2antrl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` x ) e. RR )
32 log1 
 |-  ( log ` 1 ) = 0
33 simprr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 <_ x )
34 1rp 
 |-  1 e. RR+
35 simprl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR+ )
36 logleb 
 |-  ( ( 1 e. RR+ /\ x e. RR+ ) -> ( 1 <_ x <-> ( log ` 1 ) <_ ( log ` x ) ) )
37 34 35 36 sylancr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 <_ x <-> ( log ` 1 ) <_ ( log ` x ) ) )
38 33 37 mpbid 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` 1 ) <_ ( log ` x ) )
39 32 38 eqbrtrrid 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 <_ ( log ` x ) )
40 2re 
 |-  2 e. RR
41 40 a1i 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 2 e. RR )
42 2pos 
 |-  0 < 2
43 42 a1i 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 < 2 )
44 divge0 
 |-  ( ( ( ( log ` x ) e. RR /\ 0 <_ ( log ` x ) ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 <_ ( ( log ` x ) / 2 ) )
45 31 39 41 43 44 syl22anc 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 <_ ( ( log ` x ) / 2 ) )
46 30 45 absidd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( log ` x ) / 2 ) ) = ( ( log ` x ) / 2 ) )
47 fzfid 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
48 1 2 3 4 5 6 7 8 9 dchrisum0ff 
 |-  ( ph -> F : NN --> RR )
49 48 adantr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> F : NN --> RR )
50 elfznn 
 |-  ( k e. ( 1 ... ( |_ ` x ) ) -> k e. NN )
51 ffvelcdm 
 |-  ( ( F : NN --> RR /\ k e. NN ) -> ( F ` k ) e. RR )
52 49 50 51 syl2an 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( F ` k ) e. RR )
53 50 adantl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. NN )
54 53 nnrpd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. RR+ )
55 54 rpsqrtcld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( sqrt ` k ) e. RR+ )
56 52 55 rerpdivcld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( ( F ` k ) / ( sqrt ` k ) ) e. RR )
57 47 56 fsumrecl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( F ` k ) / ( sqrt ` k ) ) e. RR )
58 57 recnd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( F ` k ) / ( sqrt ` k ) ) e. CC )
59 58 abscld 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( F ` k ) / ( sqrt ` k ) ) ) e. RR )
60 fzfid 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 ... ( |_ ` ( sqrt ` x ) ) ) e. Fin )
61 elfznn 
 |-  ( i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) -> i e. NN )
62 61 adantl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> i e. NN )
63 62 nnrecred 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( 1 / i ) e. RR )
64 60 63 fsumrecl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ( 1 / i ) e. RR )
65 logsqrt 
 |-  ( x e. RR+ -> ( log ` ( sqrt ` x ) ) = ( ( log ` x ) / 2 ) )
66 65 ad2antrl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` ( sqrt ` x ) ) = ( ( log ` x ) / 2 ) )
67 rpsqrtcl 
 |-  ( x e. RR+ -> ( sqrt ` x ) e. RR+ )
68 67 ad2antrl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( sqrt ` x ) e. RR+ )
69 harmoniclbnd 
 |-  ( ( sqrt ` x ) e. RR+ -> ( log ` ( sqrt ` x ) ) <_ sum_ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ( 1 / i ) )
70 68 69 syl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` ( sqrt ` x ) ) <_ sum_ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ( 1 / i ) )
71 66 70 eqbrtrrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) / 2 ) <_ sum_ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ( 1 / i ) )
72 eqid 
 |-  ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) = ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) )
73 ovex 
 |-  ( m ^ 2 ) e. _V
74 72 73 elrnmpti 
 |-  ( k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) <-> E. m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) k = ( m ^ 2 ) )
75 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) -> m e. NN )
76 75 adantl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> m e. NN )
77 76 nnrpd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> m e. RR+ )
78 77 rprege0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( m e. RR /\ 0 <_ m ) )
79 sqrtsq 
 |-  ( ( m e. RR /\ 0 <_ m ) -> ( sqrt ` ( m ^ 2 ) ) = m )
80 78 79 syl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( sqrt ` ( m ^ 2 ) ) = m )
81 80 76 eqeltrd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( sqrt ` ( m ^ 2 ) ) e. NN )
82 fveq2 
 |-  ( k = ( m ^ 2 ) -> ( sqrt ` k ) = ( sqrt ` ( m ^ 2 ) ) )
83 82 eleq1d 
 |-  ( k = ( m ^ 2 ) -> ( ( sqrt ` k ) e. NN <-> ( sqrt ` ( m ^ 2 ) ) e. NN ) )
84 81 83 syl5ibrcom 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( k = ( m ^ 2 ) -> ( sqrt ` k ) e. NN ) )
85 84 rexlimdva 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( E. m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) k = ( m ^ 2 ) -> ( sqrt ` k ) e. NN ) )
86 74 85 biimtrid 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) -> ( sqrt ` k ) e. NN ) )
87 86 imp 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) -> ( sqrt ` k ) e. NN )
88 87 iftrued 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) -> if ( ( sqrt ` k ) e. NN , 1 , 0 ) = 1 )
89 88 oveq1d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) -> ( if ( ( sqrt ` k ) e. NN , 1 , 0 ) / ( sqrt ` k ) ) = ( 1 / ( sqrt ` k ) ) )
90 89 sumeq2dv 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ( if ( ( sqrt ` k ) e. NN , 1 , 0 ) / ( sqrt ` k ) ) = sum_ k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ( 1 / ( sqrt ` k ) ) )
91 fveq2 
 |-  ( k = ( i ^ 2 ) -> ( sqrt ` k ) = ( sqrt ` ( i ^ 2 ) ) )
92 91 oveq2d 
 |-  ( k = ( i ^ 2 ) -> ( 1 / ( sqrt ` k ) ) = ( 1 / ( sqrt ` ( i ^ 2 ) ) ) )
93 76 nnsqcld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( m ^ 2 ) e. NN )
94 68 rpred 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( sqrt ` x ) e. RR )
95 fznnfl 
 |-  ( ( sqrt ` x ) e. RR -> ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) <-> ( m e. NN /\ m <_ ( sqrt ` x ) ) ) )
96 94 95 syl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) <-> ( m e. NN /\ m <_ ( sqrt ` x ) ) ) )
97 96 simplbda 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> m <_ ( sqrt ` x ) )
98 68 adantr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( sqrt ` x ) e. RR+ )
99 98 rprege0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( ( sqrt ` x ) e. RR /\ 0 <_ ( sqrt ` x ) ) )
100 le2sq 
 |-  ( ( ( m e. RR /\ 0 <_ m ) /\ ( ( sqrt ` x ) e. RR /\ 0 <_ ( sqrt ` x ) ) ) -> ( m <_ ( sqrt ` x ) <-> ( m ^ 2 ) <_ ( ( sqrt ` x ) ^ 2 ) ) )
101 78 99 100 syl2anc 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( m <_ ( sqrt ` x ) <-> ( m ^ 2 ) <_ ( ( sqrt ` x ) ^ 2 ) ) )
102 97 101 mpbid 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( m ^ 2 ) <_ ( ( sqrt ` x ) ^ 2 ) )
103 35 rpred 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR )
104 103 adantr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> x e. RR )
105 104 recnd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> x e. CC )
106 105 sqsqrtd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( ( sqrt ` x ) ^ 2 ) = x )
107 102 106 breqtrd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( m ^ 2 ) <_ x )
108 fznnfl 
 |-  ( x e. RR -> ( ( m ^ 2 ) e. ( 1 ... ( |_ ` x ) ) <-> ( ( m ^ 2 ) e. NN /\ ( m ^ 2 ) <_ x ) ) )
109 104 108 syl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( ( m ^ 2 ) e. ( 1 ... ( |_ ` x ) ) <-> ( ( m ^ 2 ) e. NN /\ ( m ^ 2 ) <_ x ) ) )
110 93 107 109 mpbir2and 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( m ^ 2 ) e. ( 1 ... ( |_ ` x ) ) )
111 110 ex 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) -> ( m ^ 2 ) e. ( 1 ... ( |_ ` x ) ) ) )
112 75 nnrpd 
 |-  ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) -> m e. RR+ )
113 112 rprege0d 
 |-  ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) -> ( m e. RR /\ 0 <_ m ) )
114 61 nnrpd 
 |-  ( i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) -> i e. RR+ )
115 114 rprege0d 
 |-  ( i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) -> ( i e. RR /\ 0 <_ i ) )
116 sq11 
 |-  ( ( ( m e. RR /\ 0 <_ m ) /\ ( i e. RR /\ 0 <_ i ) ) -> ( ( m ^ 2 ) = ( i ^ 2 ) <-> m = i ) )
117 113 115 116 syl2an 
 |-  ( ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) /\ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( ( m ^ 2 ) = ( i ^ 2 ) <-> m = i ) )
118 117 a1i 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) /\ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( ( m ^ 2 ) = ( i ^ 2 ) <-> m = i ) ) )
119 111 118 dom2lem 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) : ( 1 ... ( |_ ` ( sqrt ` x ) ) ) -1-1-> ( 1 ... ( |_ ` x ) ) )
120 f1f1orn 
 |-  ( ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) : ( 1 ... ( |_ ` ( sqrt ` x ) ) ) -1-1-> ( 1 ... ( |_ ` x ) ) -> ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) : ( 1 ... ( |_ ` ( sqrt ` x ) ) ) -1-1-onto-> ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) )
121 119 120 syl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) : ( 1 ... ( |_ ` ( sqrt ` x ) ) ) -1-1-onto-> ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) )
122 oveq1 
 |-  ( m = i -> ( m ^ 2 ) = ( i ^ 2 ) )
123 122 72 73 fvmpt3i 
 |-  ( i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) -> ( ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ` i ) = ( i ^ 2 ) )
124 123 adantl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ` i ) = ( i ^ 2 ) )
125 f1f 
 |-  ( ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) : ( 1 ... ( |_ ` ( sqrt ` x ) ) ) -1-1-> ( 1 ... ( |_ ` x ) ) -> ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) : ( 1 ... ( |_ ` ( sqrt ` x ) ) ) --> ( 1 ... ( |_ ` x ) ) )
126 frn 
 |-  ( ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) : ( 1 ... ( |_ ` ( sqrt ` x ) ) ) --> ( 1 ... ( |_ ` x ) ) -> ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) C_ ( 1 ... ( |_ ` x ) ) )
127 119 125 126 3syl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) C_ ( 1 ... ( |_ ` x ) ) )
128 127 sselda 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) -> k e. ( 1 ... ( |_ ` x ) ) )
129 1re 
 |-  1 e. RR
130 0re 
 |-  0 e. RR
131 129 130 ifcli 
 |-  if ( ( sqrt ` k ) e. NN , 1 , 0 ) e. RR
132 rerpdivcl 
 |-  ( ( if ( ( sqrt ` k ) e. NN , 1 , 0 ) e. RR /\ ( sqrt ` k ) e. RR+ ) -> ( if ( ( sqrt ` k ) e. NN , 1 , 0 ) / ( sqrt ` k ) ) e. RR )
133 131 55 132 sylancr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( if ( ( sqrt ` k ) e. NN , 1 , 0 ) / ( sqrt ` k ) ) e. RR )
134 133 recnd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( if ( ( sqrt ` k ) e. NN , 1 , 0 ) / ( sqrt ` k ) ) e. CC )
135 128 134 syldan 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) -> ( if ( ( sqrt ` k ) e. NN , 1 , 0 ) / ( sqrt ` k ) ) e. CC )
136 89 135 eqeltrrd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) -> ( 1 / ( sqrt ` k ) ) e. CC )
137 92 60 121 124 136 fsumf1o 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ( 1 / ( sqrt ` k ) ) = sum_ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ( 1 / ( sqrt ` ( i ^ 2 ) ) ) )
138 90 137 eqtrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ( if ( ( sqrt ` k ) e. NN , 1 , 0 ) / ( sqrt ` k ) ) = sum_ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ( 1 / ( sqrt ` ( i ^ 2 ) ) ) )
139 eldif 
 |-  ( k e. ( ( 1 ... ( |_ ` x ) ) \ ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) <-> ( k e. ( 1 ... ( |_ ` x ) ) /\ -. k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) )
140 50 ad2antrl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> k e. NN )
141 140 nncnd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> k e. CC )
142 141 sqsqrtd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> ( ( sqrt ` k ) ^ 2 ) = k )
143 simprr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> ( sqrt ` k ) e. NN )
144 fznnfl 
 |-  ( x e. RR -> ( k e. ( 1 ... ( |_ ` x ) ) <-> ( k e. NN /\ k <_ x ) ) )
145 103 144 syl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( k e. ( 1 ... ( |_ ` x ) ) <-> ( k e. NN /\ k <_ x ) ) )
146 145 simplbda 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k <_ x )
147 146 adantrr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> k <_ x )
148 140 nnrpd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> k e. RR+ )
149 148 rprege0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> ( k e. RR /\ 0 <_ k ) )
150 35 adantr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> x e. RR+ )
151 150 rprege0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> ( x e. RR /\ 0 <_ x ) )
152 sqrtle 
 |-  ( ( ( k e. RR /\ 0 <_ k ) /\ ( x e. RR /\ 0 <_ x ) ) -> ( k <_ x <-> ( sqrt ` k ) <_ ( sqrt ` x ) ) )
153 149 151 152 syl2anc 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> ( k <_ x <-> ( sqrt ` k ) <_ ( sqrt ` x ) ) )
154 147 153 mpbid 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> ( sqrt ` k ) <_ ( sqrt ` x ) )
155 68 adantr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> ( sqrt ` x ) e. RR+ )
156 155 rpred 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> ( sqrt ` x ) e. RR )
157 fznnfl 
 |-  ( ( sqrt ` x ) e. RR -> ( ( sqrt ` k ) e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) <-> ( ( sqrt ` k ) e. NN /\ ( sqrt ` k ) <_ ( sqrt ` x ) ) ) )
158 156 157 syl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> ( ( sqrt ` k ) e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) <-> ( ( sqrt ` k ) e. NN /\ ( sqrt ` k ) <_ ( sqrt ` x ) ) ) )
159 143 154 158 mpbir2and 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> ( sqrt ` k ) e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) )
160 142 140 eqeltrd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> ( ( sqrt ` k ) ^ 2 ) e. NN )
161 oveq1 
 |-  ( m = ( sqrt ` k ) -> ( m ^ 2 ) = ( ( sqrt ` k ) ^ 2 ) )
162 72 161 elrnmpt1s 
 |-  ( ( ( sqrt ` k ) e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) /\ ( ( sqrt ` k ) ^ 2 ) e. NN ) -> ( ( sqrt ` k ) ^ 2 ) e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) )
163 159 160 162 syl2anc 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> ( ( sqrt ` k ) ^ 2 ) e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) )
164 142 163 eqeltrrd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ ( sqrt ` k ) e. NN ) ) -> k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) )
165 164 expr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sqrt ` k ) e. NN -> k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) )
166 165 con3d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( -. k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) -> -. ( sqrt ` k ) e. NN ) )
167 166 impr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ -. k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) ) -> -. ( sqrt ` k ) e. NN )
168 139 167 sylan2b 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( ( 1 ... ( |_ ` x ) ) \ ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) ) -> -. ( sqrt ` k ) e. NN )
169 168 iffalsed 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( ( 1 ... ( |_ ` x ) ) \ ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) ) -> if ( ( sqrt ` k ) e. NN , 1 , 0 ) = 0 )
170 169 oveq1d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( ( 1 ... ( |_ ` x ) ) \ ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) ) -> ( if ( ( sqrt ` k ) e. NN , 1 , 0 ) / ( sqrt ` k ) ) = ( 0 / ( sqrt ` k ) ) )
171 eldifi 
 |-  ( k e. ( ( 1 ... ( |_ ` x ) ) \ ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) -> k e. ( 1 ... ( |_ ` x ) ) )
172 171 55 sylan2 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( ( 1 ... ( |_ ` x ) ) \ ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) ) -> ( sqrt ` k ) e. RR+ )
173 172 rpcnne0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( ( 1 ... ( |_ ` x ) ) \ ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) ) -> ( ( sqrt ` k ) e. CC /\ ( sqrt ` k ) =/= 0 ) )
174 div0 
 |-  ( ( ( sqrt ` k ) e. CC /\ ( sqrt ` k ) =/= 0 ) -> ( 0 / ( sqrt ` k ) ) = 0 )
175 173 174 syl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( ( 1 ... ( |_ ` x ) ) \ ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) ) -> ( 0 / ( sqrt ` k ) ) = 0 )
176 170 175 eqtrd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( ( 1 ... ( |_ ` x ) ) \ ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ) ) -> ( if ( ( sqrt ` k ) e. NN , 1 , 0 ) / ( sqrt ` k ) ) = 0 )
177 127 135 176 47 fsumss 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ k e. ran ( m e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) |-> ( m ^ 2 ) ) ( if ( ( sqrt ` k ) e. NN , 1 , 0 ) / ( sqrt ` k ) ) = sum_ k e. ( 1 ... ( |_ ` x ) ) ( if ( ( sqrt ` k ) e. NN , 1 , 0 ) / ( sqrt ` k ) ) )
178 62 nnrpd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> i e. RR+ )
179 178 rprege0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( i e. RR /\ 0 <_ i ) )
180 sqrtsq 
 |-  ( ( i e. RR /\ 0 <_ i ) -> ( sqrt ` ( i ^ 2 ) ) = i )
181 179 180 syl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( sqrt ` ( i ^ 2 ) ) = i )
182 181 oveq2d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ) -> ( 1 / ( sqrt ` ( i ^ 2 ) ) ) = ( 1 / i ) )
183 182 sumeq2dv 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ( 1 / ( sqrt ` ( i ^ 2 ) ) ) = sum_ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ( 1 / i ) )
184 138 177 183 3eqtr3d 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( if ( ( sqrt ` k ) e. NN , 1 , 0 ) / ( sqrt ` k ) ) = sum_ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ( 1 / i ) )
185 131 a1i 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> if ( ( sqrt ` k ) e. NN , 1 , 0 ) e. RR )
186 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> N e. NN )
187 8 ad2antrr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> X e. D )
188 9 ad2antrr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> X : ( Base ` Z ) --> RR )
189 1 2 186 4 5 6 7 187 188 53 dchrisum0flb 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> if ( ( sqrt ` k ) e. NN , 1 , 0 ) <_ ( F ` k ) )
190 185 52 55 189 lediv1dd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( if ( ( sqrt ` k ) e. NN , 1 , 0 ) / ( sqrt ` k ) ) <_ ( ( F ` k ) / ( sqrt ` k ) ) )
191 47 133 56 190 fsumle 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( if ( ( sqrt ` k ) e. NN , 1 , 0 ) / ( sqrt ` k ) ) <_ sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( F ` k ) / ( sqrt ` k ) ) )
192 184 191 eqbrtrrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ i e. ( 1 ... ( |_ ` ( sqrt ` x ) ) ) ( 1 / i ) <_ sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( F ` k ) / ( sqrt ` k ) ) )
193 30 64 57 71 192 letrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) / 2 ) <_ sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( F ` k ) / ( sqrt ` k ) ) )
194 57 leabsd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( F ` k ) / ( sqrt ` k ) ) <_ ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( F ` k ) / ( sqrt ` k ) ) ) )
195 30 57 59 193 194 letrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) / 2 ) <_ ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( F ` k ) / ( sqrt ` k ) ) ) )
196 46 195 eqbrtrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( log ` x ) / 2 ) ) <_ ( abs ` sum_ k e. ( 1 ... ( |_ ` x ) ) ( ( F ` k ) / ( sqrt ` k ) ) ) )
197 27 10 29 21 196 o1le 
 |-  ( ph -> ( x e. RR+ |-> ( ( log ` x ) / 2 ) ) e. O(1) )
198 15 21 26 197 o1mul2 
 |-  ( ph -> ( x e. RR+ |-> ( 2 x. ( ( log ` x ) / 2 ) ) ) e. O(1) )
199 19 198 eqeltrrd 
 |-  ( ph -> ( x e. RR+ |-> ( log ` x ) ) e. O(1) )
200 11 199 mto 
 |-  -. ph