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

Theorem pntrlog2bndlem2 22802
Description: Lemma for pntrlog2bnd 22808. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
Hypotheses
Ref Expression
pntsval.1  |-  S  =  ( a  e.  RR  |->  sum_ i  e.  ( 1 ... ( |_ `  a ) ) ( (Λ `  i )  x.  ( ( log `  i
)  +  (ψ `  ( a  /  i
) ) ) ) )
pntrlog2bnd.r  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
pntrlog2bndlem2.1  |-  ( ph  ->  A  e.  RR+ )
pntrlog2bndlem2.2  |-  ( ph  ->  A. y  e.  RR+  (ψ `  y )  <_ 
( A  x.  y
) )
Assertion
Ref Expression
pntrlog2bndlem2  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( n  x.  ( abs `  ( ( R `
 ( x  / 
( n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) ) )  / 
( x  x.  ( log `  x ) ) ) )  e.  O(1) )
Distinct variable groups:    i, a, n, x, y, A    ph, n, x    S, n, x, y    R, n, x, y
Allowed substitution hints:    ph( y, i, a)    R( i, a)    S( i, a)

Proof of Theorem pntrlog2bndlem2
Dummy variable  m is distinct from all other variables.
StepHypRef Expression
1 1red 9393 . 2  |-  ( ph  ->  1  e.  RR )
2 elioore 11322 . . . . . . . 8  |-  ( x  e.  ( 1 (,) +oo )  ->  x  e.  RR )
32adantl 466 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  RR )
4 chpcl 22437 . . . . . . 7  |-  ( x  e.  RR  ->  (ψ `  x )  e.  RR )
53, 4syl 16 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (ψ `  x )  e.  RR )
65recnd 9404 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (ψ `  x )  e.  CC )
7 fzfid 11787 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
83adantr 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
9 elfznn 11470 . . . . . . . . . . . 12  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
109adantl 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
1110peano2nnd 10331 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  e.  NN )
128, 11nndivred 10362 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  e.  RR )
13 chpcl 22437 . . . . . . . . 9  |-  ( ( x  /  ( n  +  1 ) )  e.  RR  ->  (ψ `  ( x  /  (
n  +  1 ) ) )  e.  RR )
1412, 13syl 16 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  ( n  +  1 ) ) )  e.  RR )
1514, 12readdcld 9405 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  e.  RR )
167, 15fsumrecl 13203 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  e.  RR )
1716recnd 9404 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  e.  CC )
183recnd 9404 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  CC )
19 eliooord 11347 . . . . . . . . . 10  |-  ( x  e.  ( 1 (,) +oo )  ->  ( 1  <  x  /\  x  < +oo ) )
2019adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  <  x  /\  x  < +oo ) )
2120simpld 459 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <  x )
223, 21rplogcld 22053 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  RR+ )
2322rpcnd 11021 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  CC )
2418, 23mulcld 9398 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  x.  ( log `  x ) )  e.  CC )
25 1rp 10987 . . . . . . . . 9  |-  1  e.  RR+
2625a1i 11 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  RR+ )
27 1red 9393 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  RR )
2827, 3, 21ltled 9514 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <_  x )
293, 26, 28rpgecld 11054 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  RR+ )
3029rpne0d 11024 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  =/=  0 )
3122rpne0d 11024 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  =/=  0 )
3218, 23, 30, 31mulne0d 9980 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  x.  ( log `  x ) )  =/=  0 )
336, 17, 24, 32divdird 10137 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( (ψ `  x
)  +  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) ) )  /  ( x  x.  ( log `  x
) ) )  =  ( ( (ψ `  x )  /  (
x  x.  ( log `  x ) ) )  +  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  /  ( x  x.  ( log `  x
) ) ) ) )
3433mpteq2dva 4373 . . 3  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( (ψ `  x )  +  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) )  /  (
x  x.  ( log `  x ) ) ) )  =  ( x  e.  ( 1 (,) +oo )  |->  ( ( (ψ `  x )  /  ( x  x.  ( log `  x
) ) )  +  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  /  ( x  x.  ( log `  x
) ) ) ) ) )
3529, 22rpmulcld 11035 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  x.  ( log `  x ) )  e.  RR+ )
365, 35rerpdivcld 11046 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  x )  /  ( x  x.  ( log `  x
) ) )  e.  RR )
3716, 35rerpdivcld 11046 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) )  / 
( x  x.  ( log `  x ) ) )  e.  RR )
386, 18, 23, 30, 31divdiv1d 10130 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( (ψ `  x
)  /  x )  /  ( log `  x
) )  =  ( (ψ `  x )  /  ( x  x.  ( log `  x
) ) ) )
395, 29rerpdivcld 11046 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  x )  /  x )  e.  RR )
4039recnd 9404 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  x )  /  x )  e.  CC )
4140, 23, 31divrecd 10102 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( (ψ `  x
)  /  x )  /  ( log `  x
) )  =  ( ( (ψ `  x
)  /  x )  x.  ( 1  / 
( log `  x
) ) ) )
4238, 41eqtr3d 2472 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  x )  /  ( x  x.  ( log `  x
) ) )  =  ( ( (ψ `  x )  /  x
)  x.  ( 1  /  ( log `  x
) ) ) )
4342mpteq2dva 4373 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( (ψ `  x
)  /  ( x  x.  ( log `  x
) ) ) )  =  ( x  e.  ( 1 (,) +oo )  |->  ( ( (ψ `  x )  /  x
)  x.  ( 1  /  ( log `  x
) ) ) ) )
4422rprecred 11030 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  /  ( log `  x ) )  e.  RR )
4529ex 434 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  ->  x  e.  RR+ )
)
4645ssrdv 3357 . . . . . . 7  |-  ( ph  ->  ( 1 (,) +oo )  C_  RR+ )
47 chpo1ub 22704 . . . . . . . 8  |-  ( x  e.  RR+  |->  ( (ψ `  x )  /  x
) )  e.  O(1)
4847a1i 11 . . . . . . 7  |-  ( ph  ->  ( x  e.  RR+  |->  ( (ψ `  x )  /  x ) )  e.  O(1) )
4946, 48o1res2 13033 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( (ψ `  x
)  /  x ) )  e.  O(1) )
50 divlogrlim 22055 . . . . . . 7  |-  ( x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x
) ) )  ~~> r  0
51 rlimo1 13086 . . . . . . 7  |-  ( ( x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x ) ) )  ~~> r  0  ->  (
x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  O(1) )
5250, 51mp1i 12 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  O(1) )
5339, 44, 49, 52o1mul2 13094 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( (ψ `  x )  /  x
)  x.  ( 1  /  ( log `  x
) ) ) )  e.  O(1) )
5443, 53eqeltrd 2512 . . . 4  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( (ψ `  x
)  /  ( x  x.  ( log `  x
) ) ) )  e.  O(1) )
55 pntrlog2bndlem2.1 . . . . . . . . 9  |-  ( ph  ->  A  e.  RR+ )
5655rpred 11019 . . . . . . . 8  |-  ( ph  ->  A  e.  RR )
5756, 1readdcld 9405 . . . . . . 7  |-  ( ph  ->  ( A  +  1 )  e.  RR )
5857adantr 465 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( A  +  1 )  e.  RR )
5927, 44readdcld 9405 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  e.  RR )
60 ioossre 11349 . . . . . . 7  |-  ( 1 (,) +oo )  C_  RR
6157recnd 9404 . . . . . . 7  |-  ( ph  ->  ( A  +  1 )  e.  CC )
62 o1const 13089 . . . . . . 7  |-  ( ( ( 1 (,) +oo )  C_  RR  /\  ( A  +  1 )  e.  CC )  -> 
( x  e.  ( 1 (,) +oo )  |->  ( A  +  1 ) )  e.  O(1) )
6360, 61, 62sylancr 663 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( A  +  1 ) )  e.  O(1) )
64 1cnd 9394 . . . . . . . 8  |-  ( ph  ->  1  e.  CC )
65 o1const 13089 . . . . . . . 8  |-  ( ( ( 1 (,) +oo )  C_  RR  /\  1  e.  CC )  ->  (
x  e.  ( 1 (,) +oo )  |->  1 )  e.  O(1) )
6660, 64, 65sylancr 663 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  1 )  e.  O(1) )
6727, 44, 66, 52o1add2 13093 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( 1  +  ( 1  /  ( log `  x ) ) ) )  e.  O(1) )
6858, 59, 63, 67o1mul2 13094 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( A  + 
1 )  x.  (
1  +  ( 1  /  ( log `  x
) ) ) ) )  e.  O(1) )
6958, 59remulcld 9406 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  e.  RR )
7037recnd 9404 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) )  / 
( x  x.  ( log `  x ) ) )  e.  CC )
71 chpge0 22439 . . . . . . . . . . . 12  |-  ( ( x  /  ( n  +  1 ) )  e.  RR  ->  0  <_  (ψ `  ( x  /  ( n  + 
1 ) ) ) )
7212, 71syl 16 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (ψ `  ( x  /  (
n  +  1 ) ) ) )
7310nnrpd 11018 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
7425a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR+ )
7573, 74rpaddcld 11034 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  e.  RR+ )
7629adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
7776rpge0d 11023 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  x )
788, 75, 77divge0d 11055 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( x  /  ( n  +  1 ) ) )
7914, 12, 72, 78addge0d 9907 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )
807, 15, 79fsumge0 13250 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_ 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )
8116, 35, 80divge0d 11055 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  /  ( x  x.  ( log `  x
) ) ) )
8237, 81absidd 12901 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  /  ( x  x.  ( log `  x
) ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  /  ( x  x.  ( log `  x
) ) ) )
8369recnd 9404 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  e.  CC )
8483abscld 12914 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( ( A  +  1 )  x.  ( 1  +  ( 1  /  ( log `  x ) ) ) ) )  e.  RR )
8516, 29rerpdivcld 11046 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) )  /  x )  e.  RR )
8629relogcld 22047 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  RR )
8786, 27readdcld 9405 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( log `  x
)  +  1 )  e.  RR )
8858, 87remulcld 9406 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( A  +  1 )  x.  ( ( log `  x )  +  1 ) )  e.  RR )
8958, 3remulcld 9406 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( A  +  1 )  x.  x )  e.  RR )
9010nnrecred 10359 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  n )  e.  RR )
917, 90fsumrecl 13203 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
)  e.  RR )
9289, 91remulcld 9406 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( A  + 
1 )  x.  x
)  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
) )  e.  RR )
9389, 87remulcld 9406 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( A  + 
1 )  x.  x
)  x.  ( ( log `  x )  +  1 ) )  e.  RR )
9456ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A  e.  RR )
95 1red 9393 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
9694, 95readdcld 9405 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( A  +  1 )  e.  RR )
9796, 8remulcld 9406 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( A  +  1 )  x.  x )  e.  RR )
9897, 90remulcld 9406 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  x.  ( 1  /  n ) )  e.  RR )
9997, 11nndivred 10362 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  ( n  + 
1 ) )  e.  RR )
10097, 10nndivred 10362 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  n )  e.  RR )
10194, 12remulcld 9406 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( A  x.  ( x  /  (
n  +  1 ) ) )  e.  RR )
10276, 75rpdivcld 11036 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  e.  RR+ )
103 pntrlog2bndlem2.2 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A. y  e.  RR+  (ψ `  y )  <_ 
( A  x.  y
) )
104103ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A. y  e.  RR+  (ψ `  y
)  <_  ( A  x.  y ) )
105 fveq2 5686 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x  / 
( n  +  1 ) )  ->  (ψ `  y )  =  (ψ `  ( x  /  (
n  +  1 ) ) ) )
106 oveq2 6094 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x  / 
( n  +  1 ) )  ->  ( A  x.  y )  =  ( A  x.  ( x  /  (
n  +  1 ) ) ) )
107105, 106breq12d 4300 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( x  / 
( n  +  1 ) )  ->  (
(ψ `  y )  <_  ( A  x.  y
)  <->  (ψ `  ( x  /  ( n  + 
1 ) ) )  <_  ( A  x.  ( x  /  (
n  +  1 ) ) ) ) )
108107rspcv 3064 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  /  ( n  +  1 ) )  e.  RR+  ->  ( A. y  e.  RR+  (ψ `  y )  <_  ( A  x.  y )  ->  (ψ `  ( x  /  ( n  + 
1 ) ) )  <_  ( A  x.  ( x  /  (
n  +  1 ) ) ) ) )
109102, 104, 108sylc 60 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  ( n  +  1 ) ) )  <_  ( A  x.  ( x  /  (
n  +  1 ) ) ) )
11014, 101, 12, 109leadd1dd 9945 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  <_  ( ( A  x.  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )
11161ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( A  +  1 )  e.  CC )
11218adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  CC )
11310nncnd 10330 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
114 1cnd 9394 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  CC )
115113, 114addcld 9397 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  e.  CC )
11611nnne0d 10358 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  =/=  0 )
117111, 112, 115, 116divassd 10134 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  ( n  + 
1 ) )  =  ( ( A  + 
1 )  x.  (
x  /  ( n  +  1 ) ) ) )
11894recnd 9404 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A  e.  CC )
119112, 115, 116divcld 10099 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  e.  CC )
120118, 114, 119adddird 9403 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( A  +  1 )  x.  ( x  / 
( n  +  1 ) ) )  =  ( ( A  x.  ( x  /  (
n  +  1 ) ) )  +  ( 1  x.  ( x  /  ( n  + 
1 ) ) ) ) )
121119mulid2d 9396 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  ( x  / 
( n  +  1 ) ) )  =  ( x  /  (
n  +  1 ) ) )
122121oveq2d 6102 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( A  x.  ( x  /  ( n  + 
1 ) ) )  +  ( 1  x.  ( x  /  (
n  +  1 ) ) ) )  =  ( ( A  x.  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) )
123117, 120, 1223eqtrd 2474 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  ( n  + 
1 ) )  =  ( ( A  x.  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) )
124110, 123breqtrrd 4313 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  <_  ( (
( A  +  1 )  x.  x )  /  ( n  + 
1 ) ) )
12556adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  A  e.  RR )
12655adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  A  e.  RR+ )
127126rpge0d 11023 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  A )
12826rpge0d 11023 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  1 )
129125, 27, 127, 128addge0d 9907 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  ( A  +  1 ) )
13029rpge0d 11023 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  x )
13158, 3, 129, 130mulge0d 9908 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  ( ( A  + 
1 )  x.  x
) )
132131adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( A  +  1 )  x.  x ) )
13310nnred 10329 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
134133lep1d 10256 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  <_  ( n  +  1 ) )
13573, 75, 97, 132, 134lediv2ad 11041 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  ( n  + 
1 ) )  <_ 
( ( ( A  +  1 )  x.  x )  /  n
) )
13615, 99, 100, 124, 135letrd 9520 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  <_  ( (
( A  +  1 )  x.  x )  /  n ) )
13797recnd 9404 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( A  +  1 )  x.  x )  e.  CC )
13810nnne0d 10358 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0 )
139137, 113, 138divrecd 10102 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  n )  =  ( ( ( A  +  1 )  x.  x )  x.  (
1  /  n ) ) )
140136, 139breqtrd 4311 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  <_  ( (
( A  +  1 )  x.  x )  x.  ( 1  /  n ) ) )
1417, 15, 98, 140fsumle 13254 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  <_  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( ( A  +  1 )  x.  x )  x.  (
1  /  n ) ) )
14289recnd 9404 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( A  +  1 )  x.  x )  e.  CC )
143113, 138reccld 10092 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  n )  e.  CC )
1447, 142, 143fsummulc2 13243 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( A  + 
1 )  x.  x
)  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
) )  =  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( ( A  +  1 )  x.  x )  x.  ( 1  /  n ) ) )
145141, 144breqtrrd 4313 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  <_  ( ( ( A  +  1 )  x.  x )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( 1  /  n ) ) )
146 harmonicubnd 22378 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR  /\  1  <_  x )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n )  <_  ( ( log `  x )  +  1 ) )
1473, 28, 146syl2anc 661 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
)  <_  ( ( log `  x )  +  1 ) )
14891, 87, 89, 131, 147lemul2ad 10265 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( A  + 
1 )  x.  x
)  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
) )  <_  (
( ( A  + 
1 )  x.  x
)  x.  ( ( log `  x )  +  1 ) ) )
14916, 92, 93, 145, 148letrd 9520 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  <_  ( ( ( A  +  1 )  x.  x )  x.  ( ( log `  x
)  +  1 ) ) )
15061adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( A  +  1 )  e.  CC )
15187recnd 9404 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( log `  x
)  +  1 )  e.  CC )
152150, 18, 151mul32d 9571 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( A  + 
1 )  x.  x
)  x.  ( ( log `  x )  +  1 ) )  =  ( ( ( A  +  1 )  x.  ( ( log `  x )  +  1 ) )  x.  x
) )
153149, 152breqtrd 4311 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  <_  ( ( ( A  +  1 )  x.  ( ( log `  x )  +  1 ) )  x.  x
) )
15416, 88, 29ledivmul2d 11069 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  /  x )  <_ 
( ( A  + 
1 )  x.  (
( log `  x
)  +  1 ) )  <->  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  <_  ( ( ( A  +  1 )  x.  ( ( log `  x )  +  1 ) )  x.  x
) ) )
155153, 154mpbird 232 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) )  /  x )  <_  (
( A  +  1 )  x.  ( ( log `  x )  +  1 ) ) )
15685, 88, 22, 155lediv1dd 11073 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  /  x )  / 
( log `  x
) )  <_  (
( ( A  + 
1 )  x.  (
( log `  x
)  +  1 ) )  /  ( log `  x ) ) )
15717, 18, 23, 30, 31divdiv1d 10130 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  /  x )  / 
( log `  x
) )  =  (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) )  / 
( x  x.  ( log `  x ) ) ) )
158 1cnd 9394 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  CC )
15923, 158addcld 9397 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( log `  x
)  +  1 )  e.  CC )
160150, 159, 23, 31divassd 10134 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( A  + 
1 )  x.  (
( log `  x
)  +  1 ) )  /  ( log `  x ) )  =  ( ( A  + 
1 )  x.  (
( ( log `  x
)  +  1 )  /  ( log `  x
) ) ) )
16123, 158, 23, 31divdird 10137 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( log `  x
)  +  1 )  /  ( log `  x
) )  =  ( ( ( log `  x
)  /  ( log `  x ) )  +  ( 1  /  ( log `  x ) ) ) )
16223, 31dividd 10097 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( log `  x
)  /  ( log `  x ) )  =  1 )
163162oveq1d 6101 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( log `  x
)  /  ( log `  x ) )  +  ( 1  /  ( log `  x ) ) )  =  ( 1  +  ( 1  / 
( log `  x
) ) ) )
164161, 163eqtr2d 2471 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  =  ( ( ( log `  x )  +  1 )  /  ( log `  x ) ) )
165164oveq2d 6102 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( ( A  +  1 )  x.  ( ( ( log `  x )  +  1 )  /  ( log `  x ) ) ) )
166160, 165eqtr4d 2473 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( A  + 
1 )  x.  (
( log `  x
)  +  1 ) )  /  ( log `  x ) )  =  ( ( A  + 
1 )  x.  (
1  +  ( 1  /  ( log `  x
) ) ) ) )
167156, 157, 1663brtr3d 4316 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) )  / 
( x  x.  ( log `  x ) ) )  <_  ( ( A  +  1 )  x.  ( 1  +  ( 1  /  ( log `  x ) ) ) ) )
16869leabsd 12893 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  <_  ( abs `  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) ) ) )
16937, 69, 84, 167, 168letrd 9520 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) )  / 
( x  x.  ( log `  x ) ) )  <_  ( abs `  ( ( A  + 
1 )  x.  (
1  +  ( 1  /  ( log `  x
) ) ) ) ) )
17082, 169eqbrtrd 4307 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  /  ( x  x.  ( log `  x
) ) ) )  <_  ( abs `  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) ) ) )
171170adantrr 716 . . . . 5  |-  ( (
ph  /\  ( x  e.  ( 1 (,) +oo )  /\  1  <_  x
) )  ->  ( abs `  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  /  ( x  x.  ( log `  x
) ) ) )  <_  ( abs `  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) ) ) )
1721, 68, 69, 70, 171o1le 13122 . . . 4  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  /  ( x  x.  ( log `  x
) ) ) )  e.  O(1) )
17336, 37, 54, 172o1add2 13093 . . 3  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( (ψ `  x )  /  (
x  x.  ( log `  x ) ) )  +  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  /  ( x  x.  ( log `  x
) ) ) ) )  e.  O(1) )
17434, 173eqeltrd 2512 . 2  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( (ψ `  x )  +  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) )  /  (
x  x.  ( log `  x ) ) ) )  e.  O(1) )
1755, 16readdcld 9405 . . 3  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  x )  +  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) ) )  e.  RR )
176175, 35rerpdivcld 11046 . 2  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( (ψ `  x
)  +  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) ) )  /  ( x  x.  ( log `  x
) ) )  e.  RR )
177 pntrlog2bnd.r . . . . . . . . . . . 12  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
178177pntrf 22787 . . . . . . . . . . 11  |-  R : RR+
--> RR
179178ffvelrni 5837 . . . . . . . . . 10  |-  ( ( x  /  ( n  +  1 ) )  e.  RR+  ->  ( R `
 ( x  / 
( n  +  1 ) ) )  e.  RR )
180102, 179syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  (
n  +  1 ) ) )  e.  RR )
181180recnd 9404 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  (
n  +  1 ) ) )  e.  CC )
18276, 73rpdivcld 11036 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
183178ffvelrni 5837 . . . . . . . . . 10  |-  ( ( x  /  n )  e.  RR+  ->  ( R `
 ( x  /  n ) )  e.  RR )
184182, 183syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  RR )
185184recnd 9404 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  CC )
186181, 185subcld 9711 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( R `  ( x  /  ( n  + 
1 ) ) )  -  ( R `  ( x  /  n
) ) )  e.  CC )
187186abscld 12914 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  (
n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) )  e.  RR )
188133, 187remulcld 9406 . . . . 5  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  x.  ( abs `  (
( R `  (
x  /  ( n  +  1 ) ) )  -  ( R `
 ( x  /  n ) ) ) ) )  e.  RR )
1897, 188fsumrecl 13203 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( n  x.  ( abs `  ( ( R `
 ( x  / 
( n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) ) )  e.  RR )
190189, 35rerpdivcld 11046 . . 3  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( n  x.  ( abs `  ( ( R `  ( x  /  (
n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) ) )  /  (
x  x.  ( log `  x ) ) )  e.  RR )
191190recnd 9404 . 2  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( n  x.  ( abs `  ( ( R `  ( x  /  (
n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) ) )  /  (
x  x.  ( log `  x ) ) )  e.  CC )
19273rpge0d 11023 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  n )
193186absge0d 12922 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( abs `  ( ( R `  ( x  /  ( n  + 
1 ) ) )  -  ( R `  ( x  /  n
) ) ) ) )
194133, 187, 192, 193mulge0d 9908 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( n  x.  ( abs `  ( ( R `  ( x  /  (
n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) ) ) )
1957, 188, 194fsumge0 13250 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_ 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( n  x.  ( abs `  ( ( R `  ( x  /  (
n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) ) ) )
196189, 35, 195divge0d 11055 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( n  x.  ( abs `  ( ( R `
 ( x  / 
( n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) ) )  / 
( x  x.  ( log `  x ) ) ) )
197190, 196absidd 12901 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( n  x.  ( abs `  ( ( R `
 ( x  / 
( n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) ) )  / 
( x  x.  ( log `  x ) ) ) )  =  (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( n  x.  ( abs `  ( ( R `  ( x  /  (
n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) ) )  /  (
x  x.  ( log `  x ) ) ) )
1986, 17addcld 9397 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  x )  +  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) ) )  e.  CC )
199198, 24, 32divcld 10099 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( (ψ `  x
)  +  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) ) )  /  ( x  x.  ( log `  x
) ) )  e.  CC )
200199abscld 12914 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( ( (ψ `  x )  +  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) )  /  (
x  x.  ( log `  x ) ) ) )  e.  RR )
2018, 10nndivred 10362 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
202 chpcl 22437 . . . . . . . . . . . 12  |-  ( ( x  /  n )  e.  RR  ->  (ψ `  ( x  /  n
) )  e.  RR )
203201, 202syl 16 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  n ) )  e.  RR )
204203, 201readdcld 9405 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) )  e.  RR )
205204, 15resubcld 9768 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(ψ `  ( x  /  n ) )  +  ( x  /  n
) )  -  (
(ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )  e.  RR )
206133, 205remulcld 9406 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  x.  ( ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) )  -  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) ) )  e.  RR )
207177pntrval 22786 . . . . . . . . . . . . . . 15  |-  ( ( x  /  ( n  +  1 ) )  e.  RR+  ->  ( R `
 ( x  / 
( n  +  1 ) ) )  =  ( (ψ `  (
x  /  ( n  +  1 ) ) )  -  ( x  /  ( n  + 
1 ) ) ) )
208102, 207syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  (
n  +  1 ) ) )  =  ( (ψ `  ( x  /  ( n  + 
1 ) ) )  -  ( x  / 
( n  +  1 ) ) ) )
209177pntrval 22786 . . . . . . . . . . . . . . 15  |-  ( ( x  /  n )  e.  RR+  ->  ( R `
 ( x  /  n ) )  =  ( (ψ `  (
x  /  n ) )  -  ( x  /  n ) ) )
210182, 209syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  =  ( (ψ `  ( x  /  n ) )  -  ( x  /  n
) ) )
211208, 210oveq12d 6104 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( R `  ( x  /  ( n  + 
1 ) ) )  -  ( R `  ( x  /  n
) ) )  =  ( ( (ψ `  ( x  /  (
n  +  1 ) ) )  -  (
x  /  ( n  +  1 ) ) )  -  ( (ψ `  ( x  /  n
) )  -  (
x  /  n ) ) ) )
21214recnd 9404 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  ( n  +  1 ) ) )  e.  CC )
213203recnd 9404 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  n ) )  e.  CC )
214112, 113, 138divcld 10099 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  CC )
215212, 119, 213, 214sub4d 9760 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(ψ `  ( x  /  ( n  + 
1 ) ) )  -  ( x  / 
( n  +  1 ) ) )  -  ( (ψ `  ( x  /  n ) )  -  ( x  /  n
) ) )  =  ( ( (ψ `  ( x  /  (
n  +  1 ) ) )  -  (ψ `  ( x  /  n
) ) )  -  ( ( x  / 
( n  +  1 ) )  -  (
x  /  n ) ) ) )
216211, 215eqtrd 2470 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( R `  ( x  /  ( n  + 
1 ) ) )  -  ( R `  ( x  /  n
) ) )  =  ( ( (ψ `  ( x  /  (
n  +  1 ) ) )  -  (ψ `  ( x  /  n
) ) )  -  ( ( x  / 
( n  +  1 ) )  -  (
x  /  n ) ) ) )
217216fveq2d 5690 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  (
n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) )  =  ( abs `  ( ( (ψ `  ( x  /  (
n  +  1 ) ) )  -  (ψ `  ( x  /  n
) ) )  -  ( ( x  / 
( n  +  1 ) )  -  (
x  /  n ) ) ) ) )
218212, 213subcld 9711 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  -  (ψ `  ( x  /  n
) ) )  e.  CC )
219119, 214subcld 9711 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
x  /  ( n  +  1 ) )  -  ( x  /  n ) )  e.  CC )
220218, 219abs2dif2d 12936 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( (ψ `  ( x  /  (
n  +  1 ) ) )  -  (ψ `  ( x  /  n
) ) )  -  ( ( x  / 
( n  +  1 ) )  -  (
x  /  n ) ) ) )  <_ 
( ( abs `  (
(ψ `  ( x  /  ( n  + 
1 ) ) )  -  (ψ `  (
x  /  n ) ) ) )  +  ( abs `  (
( x  /  (
n  +  1 ) )  -  ( x  /  n ) ) ) ) )
221217, 220eqbrtrd 4307 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  (
n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) )  <_  ( ( abs `  ( (ψ `  ( x  /  (
n  +  1 ) ) )  -  (ψ `  ( x  /  n
) ) ) )  +  ( abs `  (
( x  /  (
n  +  1 ) )  -  ( x  /  n ) ) ) ) )
22273, 75, 8, 77, 134lediv2ad 11041 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  <_ 
( x  /  n
) )
223 chpwordi 22470 . . . . . . . . . . . . . 14  |-  ( ( ( x  /  (
n  +  1 ) )  e.  RR  /\  ( x  /  n
)  e.  RR  /\  ( x  /  (
n  +  1 ) )  <_  ( x  /  n ) )  -> 
(ψ `  ( x  /  ( n  + 
1 ) ) )  <_  (ψ `  (
x  /  n ) ) )
22412, 201, 222, 223syl3anc 1218 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  ( n  +  1 ) ) )  <_  (ψ `  (
x  /  n ) ) )
22514, 203, 224abssuble0d 12911 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( (ψ `  (
x  /  ( n  +  1 ) ) )  -  (ψ `  ( x  /  n
) ) ) )  =  ( (ψ `  ( x  /  n
) )  -  (ψ `  ( x  /  (
n  +  1 ) ) ) ) )
22612, 201, 222abssuble0d 12911 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( x  / 
( n  +  1 ) )  -  (
x  /  n ) ) )  =  ( ( x  /  n
)  -  ( x  /  ( n  + 
1 ) ) ) )
227225, 226oveq12d 6104 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( (ψ `  ( x  /  (
n  +  1 ) ) )  -  (ψ `  ( x  /  n
) ) ) )  +  ( abs `  (
( x  /  (
n  +  1 ) )  -  ( x  /  n ) ) ) )  =  ( ( (ψ `  (
x  /  n ) )  -  (ψ `  ( x  /  (
n  +  1 ) ) ) )  +  ( ( x  /  n )  -  (
x  /  ( n  +  1 ) ) ) ) )
228213, 214, 212, 119addsub4d 9758 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(ψ `  ( x  /  n ) )  +  ( x  /  n
) )  -  (
(ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )  =  ( ( (ψ `  ( x  /  n
) )  -  (ψ `  ( x  /  (
n  +  1 ) ) ) )  +  ( ( x  /  n )  -  (
x  /  ( n  +  1 ) ) ) ) )
229227, 228eqtr4d 2473 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( (ψ `  ( x  /  (
n  +  1 ) ) )  -  (ψ `  ( x  /  n
) ) ) )  +  ( abs `  (
( x  /  (
n  +  1 ) )  -  ( x  /  n ) ) ) )  =  ( ( (ψ `  (
x  /  n ) )  +  ( x  /  n ) )  -  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) ) )
230221, 229breqtrd 4311 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  (
n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) )  <_  ( (
(ψ `  ( x  /  n ) )  +  ( x  /  n
) )  -  (
(ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) ) )
231187, 205, 133, 192, 230lemul2ad 10265 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  x.  ( abs `  (
( R `  (
x  /  ( n  +  1 ) ) )  -  ( R `
 ( x  /  n ) ) ) ) )  <_  (
n  x.  ( ( (ψ `  ( x  /  n ) )  +  ( x  /  n
) )  -  (
(ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) ) ) )
2327, 188, 206, 231fsumle 13254 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( n  x.  ( abs `  ( ( R `
 ( x  / 
( n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) ) )  <_  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( n  x.  ( ( (ψ `  ( x  /  n ) )  +  ( x  /  n
) )  -  (
(ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) ) ) )
233205recnd 9404 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(ψ `  ( x  /  n ) )  +  ( x  /  n
) )  -  (
(ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )  e.  CC )
234113, 233mulcld 9398 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  x.  ( ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) )  -  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) ) )  e.  CC )
2357, 234fsumcl 13202 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( n  x.  (
( (ψ `  (
x  /  n ) )  +  ( x  /  n ) )  -  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) ) )  e.  CC )
2366, 17negdi2d 9725 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  -u (
(ψ `  x )  +  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) ) )  =  ( -u (ψ `  x )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) ) )
23729rprege0d 11026 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  e.  RR  /\  0  <_  x ) )
238 flge0nn0 11658 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( |_ `  x
)  e.  NN0 )
239 nn0p1nn 10611 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( |_ `  x )  e.  NN0  ->  ( ( |_ `  x )  +  1 )  e.  NN )
240237, 238, 2393syl 20 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  NN )
2413, 240nndivred 10362 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  RR )
242 2re 10383 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
243242a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  2  e.  RR )
244 flltp1 11642 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  x  <  ( ( |_ `  x )  +  1 ) )
2453, 244syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  <  ( ( |_ `  x )  +  1 ) )
246240nncnd 10330 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  CC )
247246mulid1d 9395 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  1 )  =  ( ( |_
`  x )  +  1 ) )
248245, 247breqtrrd 4313 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  <  ( ( ( |_
`  x )  +  1 )  x.  1 ) )
249240nnrpd 11018 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  RR+ )
2503, 27, 249ltdivmuld 11066 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  <  1  <->  x  <  ( ( ( |_
`  x )  +  1 )  x.  1 ) ) )
251248, 250mpbird 232 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  <  1 )
252 1lt2 10480 . . . . . . . . . . . . . . . . . . . 20  |-  1  <  2
253252a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <  2 )
254241, 27, 243, 251, 253lttrd 9524 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  <  2 )
255 chpeq0 22522 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  /  ( ( |_ `  x )  +  1 ) )  e.  RR  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  0  <->  ( x  /  ( ( |_
`  x )  +  1 ) )  <  2 ) )
256241, 255syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  0  <->  ( x  /  ( ( |_
`  x )  +  1 ) )  <  2 ) )
257254, 256mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  =  0 )
258257oveq1d 6101 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) )  =  ( 0  +  ( x  /  ( ( |_ `  x )  +  1 ) ) ) )
259241recnd 9404 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  CC )
260259addid2d 9562 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
0  +  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  ( x  / 
( ( |_ `  x )  +  1 ) ) )
261258, 260eqtrd 2470 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) )  =  ( x  /  (
( |_ `  x
)  +  1 ) ) )
262261oveq2d 6102 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  ( (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  +  ( x  /  ( ( |_ `  x )  +  1 ) ) ) )  =  ( ( ( |_ `  x )  +  1 )  x.  ( x  /  ( ( |_
`  x )  +  1 ) ) ) )
263240nnne0d 10358 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  =/=  0 )
26418, 246, 263divcan2d 10101 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  x )
265262, 264eqtrd 2470 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  ( (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  +  ( x  /  ( ( |_ `  x )  +  1 ) ) ) )  =  x )
26618div1d 10091 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  1 )  =  x )
267266fveq2d 5690 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (ψ `  ( x  /  1
) )  =  (ψ `  x ) )
268267, 266oveq12d 6104 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  ( x  /  1 ) )  +  ( x  / 
1 ) )  =  ( (ψ `  x
)  +  x ) )
269268oveq2d 6102 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  x.  ( (ψ `  ( x  /  1
) )  +  ( x  /  1 ) ) )  =  ( 1  x.  ( (ψ `  x )  +  x
) ) )
2705, 3readdcld 9405 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  x )  +  x )  e.  RR )
271270recnd 9404 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  x )  +  x )  e.  CC )
272271mulid2d 9396 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  x.  ( (ψ `  x )  +  x
) )  =  ( (ψ `  x )  +  x ) )
273269, 272eqtrd 2470 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  x.  ( (ψ `  ( x  /  1
) )  +  ( x  /  1 ) ) )  =  ( (ψ `  x )  +  x ) )
274265, 273oveq12d 6104 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( |_
`  x )  +  1 )  x.  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) ) )  -  ( 1  x.  ( (ψ `  (
x  /  1 ) )  +  ( x  /  1 ) ) ) )  =  ( x  -  ( (ψ `  x )  +  x
) ) )
275271, 18negsubdi2d 9727 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  -u (
( (ψ `  x
)  +  x )  -  x )  =  ( x  -  (
(ψ `  x )  +  x ) ) )
2766, 18pncand 9712 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( (ψ `  x
)  +  x )  -  x )  =  (ψ `  x )
)
277276negeqd 9596 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  -u (
( (ψ `  x
)  +  x )  -  x )  = 
-u (ψ `  x
) )
278274, 275, 2773eqtr2d 2476 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( |_
`  x )  +  1 )  x.  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) ) )  -  ( 1  x.  ( (ψ `  (
x  /  1 ) )  +  ( x  /  1 ) ) ) )  =  -u (ψ `  x ) )
2793flcld 11640 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( |_ `  x )  e.  ZZ )
280 fzval3 11597 . . . . . . . . . . . . . 14  |-  ( ( |_ `  x )  e.  ZZ  ->  (
1 ... ( |_ `  x ) )  =  ( 1..^ ( ( |_ `  x )  +  1 ) ) )
281279, 280syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1 ... ( |_ `  x ) )  =  ( 1..^ ( ( |_ `  x )  +  1 ) ) )
282281eqcomd 2443 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1..^ ( ( |_
`  x )  +  1 ) )  =  ( 1 ... ( |_ `  x ) ) )
283113, 114pncan2d 9713 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
n  +  1 )  -  n )  =  1 )
284283oveq1d 6101 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( n  +  1 )  -  n )  x.  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) )  =  ( 1  x.  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) ) )
28515recnd 9404 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  e.  CC )
286285mulid2d 9396 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) )  =  ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )
287284, 286eqtrd 2470 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( n  +  1 )  -  n )  x.  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) )  =  ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )
288282, 287sumeq12rdv 13176 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1..^ ( ( |_ `  x )  +  1 ) ) ( ( ( n  +  1 )  -  n )  x.  (
(ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) ) )
289278, 288oveq12d 6104 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( ( |_ `  x )  +  1 )  x.  ( (ψ `  (
x  /  ( ( |_ `  x )  +  1 ) ) )  +  ( x  /  ( ( |_
`  x )  +  1 ) ) ) )  -  ( 1  x.  ( (ψ `  ( x  /  1
) )  +  ( x  /  1 ) ) ) )  -  sum_ n  e.  ( 1..^ ( ( |_ `  x )  +  1 ) ) ( ( ( n  +  1 )  -  n )  x.  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) ) )  =  ( -u (ψ `  x )  -  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) ) )
290 oveq2 6094 . . . . . . . . . . . . . . 15  |-  ( m  =  n  ->  (
x  /  m )  =  ( x  /  n ) )
291290fveq2d 5690 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  (ψ `  ( x  /  m
) )  =  (ψ `  ( x  /  n
) ) )
292291, 290oveq12d 6104 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  n ) )  +  ( x  /  n
) ) )
293292ancli 551 . . . . . . . . . . . 12  |-  ( m  =  n  ->  (
m  =  n  /\  ( (ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  n ) )  +  ( x  /  n
) ) ) )
294 oveq2 6094 . . . . . . . . . . . . . . 15  |-  ( m  =  ( n  + 
1 )  ->  (
x  /  m )  =  ( x  / 
( n  +  1 ) ) )
295294fveq2d 5690 . . . . . . . . . . . . . 14  |-  ( m  =  ( n  + 
1 )  ->  (ψ `  ( x  /  m
) )  =  (ψ `  ( x  /  (
n  +  1 ) ) ) )
296295, 294oveq12d 6104 . . . . . . . . . . . . 13  |-  ( m  =  ( n  + 
1 )  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )
297296ancli 551 . . . . . . . . . . . 12  |-  ( m  =  ( n  + 
1 )  ->  (
m  =  ( n  +  1 )  /\  ( (ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) ) )
298 oveq2 6094 . . . . . . . . . . . . . . 15  |-  ( m  =  1  ->  (
x  /  m )  =  ( x  / 
1 ) )
299298fveq2d 5690 . . . . . . . . . . . . . 14  |-  ( m  =  1  ->  (ψ `  ( x  /  m
) )  =  (ψ `  ( x  /  1
) ) )
300299, 298oveq12d 6104 . . . . . . . . . . . . 13  |-  ( m  =  1  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  1 ) )  +  ( x  / 
1 ) ) )
301300ancli 551 . . . . . . . . . . . 12  |-  ( m  =  1  ->  (
m  =  1  /\  ( (ψ `  (
x  /  m ) )  +  ( x  /  m ) )  =  ( (ψ `  ( x  /  1
) )  +  ( x  /  1 ) ) ) )
302 oveq2 6094 . . . . . . . . . . . . . . 15  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
x  /  m )  =  ( x  / 
( ( |_ `  x )  +  1 ) ) )
303302fveq2d 5690 . . . . . . . . . . . . . 14  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (ψ `  ( x  /  m
) )  =  (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )
304303, 302oveq12d 6104 . . . . . . . . . . . . 13  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) ) )
305304ancli 551 . . . . . . . . . . . 12  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
m  =  ( ( |_ `  x )  +  1 )  /\  ( (ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) ) ) )
306 nnuz 10888 . . . . . . . . . . . . 13  |-  NN  =  ( ZZ>= `  1 )
307240, 306syl6eleq 2528 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  ( ZZ>= `  1
) )
308 elfznn 11470 . . . . . . . . . . . . . 14  |-  ( m  e.  ( 1 ... ( ( |_ `  x )  +  1 ) )  ->  m  e.  NN )
309308adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  NN )
310309nncnd 10330 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  CC )
3113adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  x  e.  RR )
312311, 309nndivred 10362 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
x  /  m )  e.  RR )
313 chpcl 22437 . . . . . . . . . . . . . . 15  |-  ( ( x  /  m )  e.  RR  ->  (ψ `  ( x  /  m
) )  e.  RR )
314312, 313syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (ψ `  ( x  /  m
) )  e.  RR )
315314, 312readdcld 9405 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  e.  RR )
316315recnd 9404 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  e.  CC )
317293, 297, 301, 305, 307, 310, 316fsumparts 13261 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1..^ ( ( |_ `  x )  +  1 ) ) ( n  x.  (
( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  -  ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) ) ) )  =  ( ( ( ( ( |_ `  x
)  +  1 )  x.  ( (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  +  ( x  /  ( ( |_ `  x )  +  1 ) ) ) )  -  (
1  x.  ( (ψ `  ( x  /  1
) )  +  ( x  /  1 ) ) ) )  -  sum_ n  e.  ( 1..^ ( ( |_ `  x )  +  1 ) ) ( ( ( n  +  1 )  -  n )  x.  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) ) ) )
318213, 214addcld 9397 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) )  e.  CC )
319212, 119addcld 9397 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  e.  CC )
320318, 319negsubdi2d 9727 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  -u ( ( (ψ `  ( x  /  n ) )  +  ( x  /  n
) )  -  (
(ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )  =  ( ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  -  ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) ) ) )
321320oveq2d 6102 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  x.  -u ( ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) )  -  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) ) )  =  ( n  x.  (
( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  -  ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) ) ) ) )
322113, 233mulneg2d 9790 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  x.  -u ( ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) )  -  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) ) )  = 
-u ( n  x.  ( ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) )  -  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) ) ) )
323321, 322eqtr3d 2472 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  x.  ( ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  -  ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) ) ) )  = 
-u ( n  x.  ( ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) )  -  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) ) ) )
324282, 323sumeq12rdv 13176 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1..^ ( ( |_ `  x )  +  1 ) ) ( n  x.  (
( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  -  ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) ) ) )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) -u ( n  x.  (
( (ψ `  (
x  /  n ) )  +  ( x  /  n ) )  -  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) ) ) )
325317, 324eqtr3d 2472 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( ( |_ `  x )  +  1 )  x.  ( (ψ `  (
x  /  ( ( |_ `  x )  +  1 ) ) )  +  ( x  /  ( ( |_
`  x )  +  1 ) ) ) )  -  ( 1  x.  ( (ψ `  ( x  /  1
) )  +  ( x  /  1 ) ) ) )  -  sum_ n  e.  ( 1..^ ( ( |_ `  x )  +  1 ) ) ( ( ( n  +  1 )  -  n )  x.  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) ) )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) -u ( n  x.  (
( (ψ `  (
x  /  n ) )  +  ( x  /  n ) )  -  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) ) ) )
326236, 289, 3253eqtr2d 2476 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  -u (
(ψ `  x )  +  sum_ n  e.  ( 1 ...