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

Theorem pntrlog2bndlem2 22961
Description: Lemma for pntrlog2bnd 22967. 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 9513 . 2  |-  ( ph  ->  1  e.  RR )
2 elioore 11442 . . . . . . . 8  |-  ( x  e.  ( 1 (,) +oo )  ->  x  e.  RR )
32adantl 466 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  RR )
4 chpcl 22596 . . . . . . 7  |-  ( x  e.  RR  ->  (ψ `  x )  e.  RR )
53, 4syl 16 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (ψ `  x )  e.  RR )
65recnd 9524 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (ψ `  x )  e.  CC )
7 fzfid 11913 . . . . . . 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 11596 . . . . . . . . . . . 12  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
109adantl 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
1110peano2nnd 10451 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  e.  NN )
128, 11nndivred 10482 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  e.  RR )
13 chpcl 22596 . . . . . . . . 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 9525 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  e.  RR )
167, 15fsumrecl 13330 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  e.  RR )
1716recnd 9524 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  e.  CC )
183recnd 9524 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  CC )
19 eliooord 11467 . . . . . . . . . 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 22212 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  RR+ )
2322rpcnd 11141 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  CC )
2418, 23mulcld 9518 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  x.  ( log `  x ) )  e.  CC )
25 1rp 11107 . . . . . . . . 9  |-  1  e.  RR+
2625a1i 11 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  RR+ )
27 1red 9513 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  RR )
2827, 3, 21ltled 9634 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <_  x )
293, 26, 28rpgecld 11174 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  RR+ )
3029rpne0d 11144 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  =/=  0 )
3122rpne0d 11144 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  =/=  0 )
3218, 23, 30, 31mulne0d 10100 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  x.  ( log `  x ) )  =/=  0 )
336, 17, 24, 32divdird 10257 . . . 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 4487 . . 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 11155 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  x.  ( log `  x ) )  e.  RR+ )
365, 35rerpdivcld 11166 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  x )  /  ( x  x.  ( log `  x
) ) )  e.  RR )
3716, 35rerpdivcld 11166 . . . 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 10250 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( (ψ `  x
)  /  x )  /  ( log `  x
) )  =  ( (ψ `  x )  /  ( x  x.  ( log `  x
) ) ) )
395, 29rerpdivcld 11166 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  x )  /  x )  e.  RR )
4039recnd 9524 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  x )  /  x )  e.  CC )
4140, 23, 31divrecd 10222 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( (ψ `  x
)  /  x )  /  ( log `  x
) )  =  ( ( (ψ `  x
)  /  x )  x.  ( 1  / 
( log `  x
) ) ) )
4238, 41eqtr3d 2497 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  x )  /  ( x  x.  ( log `  x
) ) )  =  ( ( (ψ `  x )  /  x
)  x.  ( 1  /  ( log `  x
) ) ) )
4342mpteq2dva 4487 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( (ψ `  x
)  /  ( x  x.  ( log `  x
) ) ) )  =  ( x  e.  ( 1 (,) +oo )  |->  ( ( (ψ `  x )  /  x
)  x.  ( 1  /  ( log `  x
) ) ) ) )
4422rprecred 11150 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  /  ( log `  x ) )  e.  RR )
4529ex 434 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  ->  x  e.  RR+ )
)
4645ssrdv 3471 . . . . . . 7  |-  ( ph  ->  ( 1 (,) +oo )  C_  RR+ )
47 chpo1ub 22863 . . . . . . . 8  |-  ( x  e.  RR+  |->  ( (ψ `  x )  /  x
) )  e.  O(1)
4847a1i 11 . . . . . . 7  |-  ( ph  ->  ( x  e.  RR+  |->  ( (ψ `  x )  /  x ) )  e.  O(1) )
4946, 48o1res2 13160 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( (ψ `  x
)  /  x ) )  e.  O(1) )
50 divlogrlim 22214 . . . . . . 7  |-  ( x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x
) ) )  ~~> r  0
51 rlimo1 13213 . . . . . . 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 13221 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( (ψ `  x )  /  x
)  x.  ( 1  /  ( log `  x
) ) ) )  e.  O(1) )
5443, 53eqeltrd 2542 . . . 4  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( (ψ `  x
)  /  ( x  x.  ( log `  x
) ) ) )  e.  O(1) )
55 pntrlog2bndlem2.1 . . . . . . . . 9  |-  ( ph  ->  A  e.  RR+ )
5655rpred 11139 . . . . . . . 8  |-  ( ph  ->  A  e.  RR )
5756, 1readdcld 9525 . . . . . . 7  |-  ( ph  ->  ( A  +  1 )  e.  RR )
5857adantr 465 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( A  +  1 )  e.  RR )
5927, 44readdcld 9525 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  e.  RR )
60 ioossre 11469 . . . . . . 7  |-  ( 1 (,) +oo )  C_  RR
6157recnd 9524 . . . . . . 7  |-  ( ph  ->  ( A  +  1 )  e.  CC )
62 o1const 13216 . . . . . . 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 9514 . . . . . . . 8  |-  ( ph  ->  1  e.  CC )
65 o1const 13216 . . . . . . . 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 13220 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( 1  +  ( 1  /  ( log `  x ) ) ) )  e.  O(1) )
6858, 59, 63, 67o1mul2 13221 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( A  + 
1 )  x.  (
1  +  ( 1  /  ( log `  x
) ) ) ) )  e.  O(1) )
6958, 59remulcld 9526 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  e.  RR )
7037recnd 9524 . . . . 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 22598 . . . . . . . . . . . 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 11138 . . . . . . . . . . . . 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 11154 . . . . . . . . . . . 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 11143 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  x )
788, 75, 77divge0d 11175 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( x  /  ( n  +  1 ) ) )
7914, 12, 72, 78addge0d 10027 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )
807, 15, 79fsumge0 13377 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_ 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )
8116, 35, 80divge0d 11175 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  /  ( x  x.  ( log `  x
) ) ) )
8237, 81absidd 13028 . . . . . . 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 9524 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  e.  CC )
8483abscld 13041 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( abs `  ( ( A  +  1 )  x.  ( 1  +  ( 1  /  ( log `  x ) ) ) ) )  e.  RR )
8516, 29rerpdivcld 11166 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) )  /  x )  e.  RR )
8629relogcld 22206 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  RR )
8786, 27readdcld 9525 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( log `  x
)  +  1 )  e.  RR )
8858, 87remulcld 9526 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( A  +  1 )  x.  ( ( log `  x )  +  1 ) )  e.  RR )
8958, 3remulcld 9526 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( A  +  1 )  x.  x )  e.  RR )
9010nnrecred 10479 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  n )  e.  RR )
917, 90fsumrecl 13330 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
)  e.  RR )
9289, 91remulcld 9526 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( A  + 
1 )  x.  x
)  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
) )  e.  RR )
9389, 87remulcld 9526 . . . . . . . . . . . . 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 9513 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
9694, 95readdcld 9525 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( A  +  1 )  e.  RR )
9796, 8remulcld 9526 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( A  +  1 )  x.  x )  e.  RR )
9897, 90remulcld 9526 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  x.  ( 1  /  n ) )  e.  RR )
9997, 11nndivred 10482 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  ( n  + 
1 ) )  e.  RR )
10097, 10nndivred 10482 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  n )  e.  RR )
10194, 12remulcld 9526 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( A  x.  ( x  /  (
n  +  1 ) ) )  e.  RR )
10276, 75rpdivcld 11156 . . . . . . . . . . . . . . . . . . . 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 5800 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x  / 
( n  +  1 ) )  ->  (ψ `  y )  =  (ψ `  ( x  /  (
n  +  1 ) ) ) )
106 oveq2 6209 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x  / 
( n  +  1 ) )  ->  ( A  x.  y )  =  ( A  x.  ( x  /  (
n  +  1 ) ) ) )
107105, 106breq12d 4414 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( x  / 
( n  +  1 ) )  ->  (
(ψ `  y )  <_  ( A  x.  y
)  <->  (ψ `  ( x  /  ( n  + 
1 ) ) )  <_  ( A  x.  ( x  /  (
n  +  1 ) ) ) ) )
108107rspcv 3175 . . . . . . . . . . . . . . . . . . . 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 10065 . . . . . . . . . . . . . . . . . 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 10450 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
114 1cnd 9514 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  CC )
115113, 114addcld 9517 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  e.  CC )
11611nnne0d 10478 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  =/=  0 )
117111, 112, 115, 116divassd 10254 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  ( n  + 
1 ) )  =  ( ( A  + 
1 )  x.  (
x  /  ( n  +  1 ) ) ) )
11894recnd 9524 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A  e.  CC )
119112, 115, 116divcld 10219 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  e.  CC )
120118, 114, 119adddird 9523 . . . . . . . . . . . . . . . . . . 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 9516 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  ( x  / 
( n  +  1 ) ) )  =  ( x  /  (
n  +  1 ) ) )
122121oveq2d 6217 . . . . . . . . . . . . . . . . . . 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 2499 . . . . . . . . . . . . . . . . . 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 4427 . . . . . . . . . . . . . . . . 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 11143 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  A )
12826rpge0d 11143 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  1 )
129125, 27, 127, 128addge0d 10027 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  ( A  +  1 ) )
13029rpge0d 11143 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  0  <_  x )
13158, 3, 129, 130mulge0d 10028 . . . . . . . . . . . . . . . . . . 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 10449 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
134133lep1d 10376 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  <_  ( n  +  1 ) )
13573, 75, 97, 132, 134lediv2ad 11161 . . . . . . . . . . . . . . . . 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 9640 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  <_  ( (
( A  +  1 )  x.  x )  /  n ) )
13797recnd 9524 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( A  +  1 )  x.  x )  e.  CC )
13810nnne0d 10478 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0 )
139137, 113, 138divrecd 10222 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  n )  =  ( ( ( A  +  1 )  x.  x )  x.  (
1  /  n ) ) )
140136, 139breqtrd 4425 . . . . . . . . . . . . . . 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 13381 . . . . . . . . . . . . . 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 9524 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( A  +  1 )  x.  x )  e.  CC )
143113, 138reccld 10212 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  n )  e.  CC )
1447, 142, 143fsummulc2 13370 . . . . . . . . . . . . . 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 4427 . . . . . . . . . . . . 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 22537 . . . . . . . . . . . . . . 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 10385 . . . . . . . . . . . . 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 9640 . . . . . . . . . . . 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 9524 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( log `  x
)  +  1 )  e.  CC )
152150, 18, 151mul32d 9691 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( A  + 
1 )  x.  x
)  x.  ( ( log `  x )  +  1 ) )  =  ( ( ( A  +  1 )  x.  ( ( log `  x )  +  1 ) )  x.  x
) )
153149, 152breqtrd 4425 . . . . . . . . . . 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 11189 . . . . . . . . . . 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 11193 . . . . . . . . 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 10250 . . . . . . . . 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 9514 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  CC )
15923, 158addcld 9517 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( log `  x
)  +  1 )  e.  CC )
160150, 159, 23, 31divassd 10254 . . . . . . . . . 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 10257 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( log `  x
)  +  1 )  /  ( log `  x
) )  =  ( ( ( log `  x
)  /  ( log `  x ) )  +  ( 1  /  ( log `  x ) ) ) )
16223, 31dividd 10217 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( log `  x
)  /  ( log `  x ) )  =  1 )
163162oveq1d 6216 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( log `  x
)  /  ( log `  x ) )  +  ( 1  /  ( log `  x ) ) )  =  ( 1  +  ( 1  / 
( log `  x
) ) ) )
164161, 163eqtr2d 2496 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  =  ( ( ( log `  x )  +  1 )  /  ( log `  x ) ) )
165164oveq2d 6217 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( ( A  +  1 )  x.  ( ( ( log `  x )  +  1 )  /  ( log `  x ) ) ) )
166160, 165eqtr4d 2498 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( A  + 
1 )  x.  (
( log `  x
)  +  1 ) )  /  ( log `  x ) )  =  ( ( A  + 
1 )  x.  (
1  +  ( 1  /  ( log `  x
) ) ) ) )
167156, 157, 1663brtr3d 4430 . . . . . . . 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 13020 . . . . . . . 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 9640 . . . . . . 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 4421 . . . . . 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 13249 . . . 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 13220 . . 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 2542 . 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 9525 . . 3  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  x )  +  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) ) )  e.  RR )
176175, 35rerpdivcld 11166 . 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 22946 . . . . . . . . . . 11  |-  R : RR+
--> RR
179178ffvelrni 5952 . . . . . . . . . 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 9524 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  (
n  +  1 ) ) )  e.  CC )
18276, 73rpdivcld 11156 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
183178ffvelrni 5952 . . . . . . . . . 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 9524 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  CC )
186181, 185subcld 9831 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( R `  ( x  /  ( n  + 
1 ) ) )  -  ( R `  ( x  /  n
) ) )  e.  CC )
187186abscld 13041 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  (
n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) )  e.  RR )
188133, 187remulcld 9526 . . . . 5  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  x.  ( abs `  (
( R `  (
x  /  ( n  +  1 ) ) )  -  ( R `
 ( x  /  n ) ) ) ) )  e.  RR )
1897, 188fsumrecl 13330 . . . 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 11166 . . 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 9524 . 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 11143 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  n )
193186absge0d 13049 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( abs `  ( ( R `  ( x  /  ( n  + 
1 ) ) )  -  ( R `  ( x  /  n
) ) ) ) )
194133, 187, 192, 193mulge0d 10028 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( n  x.  ( abs `  ( ( R `  ( x  /  (
n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) ) ) )
1957, 188, 194fsumge0 13377 . . . . . 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 11175 . . . . 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 13028 . . . 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 9517 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  x )  +  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) ) )  e.  CC )
199198, 24, 32divcld 10219 . . . . . 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 13041 . . . . 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 10482 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
202 chpcl 22596 . . . . . . . . . . . 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 9525 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) )  e.  RR )
205204, 15resubcld 9888 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(ψ `  ( x  /  n ) )  +  ( x  /  n
) )  -  (
(ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )  e.  RR )
206133, 205remulcld 9526 . . . . . . . 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 22945 . . . . . . . . . . . . . . 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 22945 . . . . . . . . . . . . . . 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 6219 . . . . . . . . . . . . 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 9524 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  ( n  +  1 ) ) )  e.  CC )
213203recnd 9524 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  n ) )  e.  CC )
214112, 113, 138divcld 10219 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  CC )
215212, 119, 213, 214sub4d 9880 . . . . . . . . . . . . 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 2495 . . . . . . . . . . . 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 5804 . . . . . . . . . . 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 9831 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  -  (ψ `  ( x  /  n
) ) )  e.  CC )
219119, 214subcld 9831 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
x  /  ( n  +  1 ) )  -  ( x  /  n ) )  e.  CC )
220218, 219abs2dif2d 13063 . . . . . . . . . . 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 4421 . . . . . . . . . 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 11161 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  <_ 
( x  /  n
) )
223 chpwordi 22629 . . . . . . . . . . . . . 14  |-  ( ( ( x  /  (
n  +  1 ) )  e.  RR  /\  ( x  /  n
)  e.  RR  /\  ( x  /  (
n  +  1 ) )  <_  ( x  /  n ) )  -> 
(ψ `  ( x  /  ( n  + 
1 ) ) )  <_  (ψ `  (
x  /  n ) ) )
22412, 201, 222, 223syl3anc 1219 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  ( n  +  1 ) ) )  <_  (ψ `  (
x  /  n ) ) )
22514, 203, 224abssuble0d 13038 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( (ψ `  (
x  /  ( n  +  1 ) ) )  -  (ψ `  ( x  /  n
) ) ) )  =  ( (ψ `  ( x  /  n
) )  -  (ψ `  ( x  /  (
n  +  1 ) ) ) ) )
22612, 201, 222abssuble0d 13038 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( x  / 
( n  +  1 ) )  -  (
x  /  n ) ) )  =  ( ( x  /  n
)  -  ( x  /  ( n  + 
1 ) ) ) )
227225, 226oveq12d 6219 . . . . . . . . . . 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 9878 . . . . . . . . . . 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 2498 . . . . . . . . . 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 4425 . . . . . . . . 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 10385 . . . . . . . 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 13381 . . . . . . 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 9524 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(ψ `  ( x  /  n ) )  +  ( x  /  n
) )  -  (
(ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )  e.  CC )
234113, 233mulcld 9518 . . . . . . . . 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 13329 . . . . . . . 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 9845 . . . . . . . . . 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 11146 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  e.  RR  /\  0  <_  x ) )
238 flge0nn0 11784 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( |_ `  x
)  e.  NN0 )
239 nn0p1nn 10731 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( |_ `  x )  e.  NN0  ->  ( ( |_ `  x )  +  1 )  e.  NN )
240237, 238, 2393syl 20 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  NN )
2413, 240nndivred 10482 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  RR )
242 2re 10503 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
243242a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  2  e.  RR )
244 flltp1 11768 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  x  <  ( ( |_ `  x )  +  1 ) )
2453, 244syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  <  ( ( |_ `  x )  +  1 ) )
246240nncnd 10450 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  CC )
247246mulid1d 9515 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  1 )  =  ( ( |_
`  x )  +  1 ) )
248245, 247breqtrrd 4427 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  <  ( ( ( |_
`  x )  +  1 )  x.  1 ) )
249240nnrpd 11138 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  RR+ )
2503, 27, 249ltdivmuld 11186 . . . . . . . . . . . . . . . . . . . 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 10600 . . . . . . . . . . . . . . . . . . . 20  |-  1  <  2
253252a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <  2 )
254241, 27, 243, 251, 253lttrd 9644 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  <  2 )
255 chpeq0 22681 . . . . . . . . . . . . . . . . . . 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 6216 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) )  =  ( 0  +  ( x  /  ( ( |_ `  x )  +  1 ) ) ) )
259241recnd 9524 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  CC )
260259addid2d 9682 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
0  +  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  ( x  / 
( ( |_ `  x )  +  1 ) ) )
261258, 260eqtrd 2495 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) )  =  ( x  /  (
( |_ `  x
)  +  1 ) ) )
262261oveq2d 6217 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  ( (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  +  ( x  /  ( ( |_ `  x )  +  1 ) ) ) )  =  ( ( ( |_ `  x )  +  1 )  x.  ( x  /  ( ( |_
`  x )  +  1 ) ) ) )
263240nnne0d 10478 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  =/=  0 )
26418, 246, 263divcan2d 10221 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  x )
265262, 264eqtrd 2495 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  ( (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  +  ( x  /  ( ( |_ `  x )  +  1 ) ) ) )  =  x )
26618div1d 10211 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  /  1 )  =  x )
267266fveq2d 5804 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (ψ `  ( x  /  1
) )  =  (ψ `  x ) )
268267, 266oveq12d 6219 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  ( x  /  1 ) )  +  ( x  / 
1 ) )  =  ( (ψ `  x
)  +  x ) )
269268oveq2d 6217 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  x.  ( (ψ `  ( x  /  1
) )  +  ( x  /  1 ) ) )  =  ( 1  x.  ( (ψ `  x )  +  x
) ) )
2705, 3readdcld 9525 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  x )  +  x )  e.  RR )
271270recnd 9524 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
(ψ `  x )  +  x )  e.  CC )
272271mulid2d 9516 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  x.  ( (ψ `  x )  +  x
) )  =  ( (ψ `  x )  +  x ) )
273269, 272eqtrd 2495 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  x.  ( (ψ `  ( x  /  1
) )  +  ( x  /  1 ) ) )  =  ( (ψ `  x )  +  x ) )
274265, 273oveq12d 6219 . . . . . . . . . . . 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 9847 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  -u (
( (ψ `  x
)  +  x )  -  x )  =  ( x  -  (
(ψ `  x )  +  x ) ) )
2766, 18pncand 9832 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( (ψ `  x
)  +  x )  -  x )  =  (ψ `  x )
)
277276negeqd 9716 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  -u (
( (ψ `  x
)  +  x )  -  x )  = 
-u (ψ `  x
) )
278274, 275, 2773eqtr2d 2501 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( ( ( |_
`  x )  +  1 )  x.  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) ) )  -  ( 1  x.  ( (ψ `  (
x  /  1 ) )  +  ( x  /  1 ) ) ) )  =  -u (ψ `  x ) )
2793flcld 11766 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( |_ `  x )  e.  ZZ )
280 fzval3 11723 . . . . . . . . . . . . . 14  |-  ( ( |_ `  x )  e.  ZZ  ->  (
1 ... ( |_ `  x ) )  =  ( 1..^ ( ( |_ `  x )  +  1 ) ) )
281279, 280syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1 ... ( |_ `  x ) )  =  ( 1..^ ( ( |_ `  x )  +  1 ) ) )
282281eqcomd 2462 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1..^ ( ( |_
`  x )  +  1 ) )  =  ( 1 ... ( |_ `  x ) ) )
283113, 114pncan2d 9833 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
n  +  1 )  -  n )  =  1 )
284283oveq1d 6216 . . . . . . . . . . . . 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 9524 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  e.  CC )
286285mulid2d 9516 . . . . . . . . . . . . 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 2495 . . . . . . . . . . . 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 13303 . . . . . . . . . . 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 6219 . . . . . . . . . 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 6209 . . . . . . . . . . . . . . 15  |-  ( m  =  n  ->  (
x  /  m )  =  ( x  /  n ) )
291290fveq2d 5804 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  (ψ `  ( x  /  m
) )  =  (ψ `  ( x  /  n
) ) )
292291, 290oveq12d 6219 . . . . . . . . . . . . 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 6209 . . . . . . . . . . . . . . 15  |-  ( m  =  ( n  + 
1 )  ->  (
x  /  m )  =  ( x  / 
( n  +  1 ) ) )
295294fveq2d 5804 . . . . . . . . . . . . . 14  |-  ( m  =  ( n  + 
1 )  ->  (ψ `  ( x  /  m
) )  =  (ψ `  ( x  /  (
n  +  1 ) ) ) )
296295, 294oveq12d 6219 . . . . . . . . . . . . 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 6209 . . . . . . . . . . . . . . 15  |-  ( m  =  1  ->  (
x  /  m )  =  ( x  / 
1 ) )
299298fveq2d 5804 . . . . . . . . . . . . . 14  |-  ( m  =  1  ->  (ψ `  ( x  /  m
) )  =  (ψ `  ( x  /  1
) ) )
300299, 298oveq12d 6219 . . . . . . . . . . . . 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 6209 . . . . . . . . . . . . . . 15  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
x  /  m )  =  ( x  / 
( ( |_ `  x )  +  1 ) ) )
303302fveq2d 5804 . . . . . . . . . . . . . 14  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (ψ `  ( x  /  m
) )  =  (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )
304303, 302oveq12d 6219 . . . . . . . . . . . . 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 11008 . . . . . . . . . . . . 13  |-  NN  =  ( ZZ>= `  1 )
307240, 306syl6eleq 2552 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  ( ZZ>= `  1
) )
308 elfznn 11596 . . . . . . . . . . . . . 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 10450 . . . . . . . . . . . 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 10482 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
x  /  m )  e.  RR )
313 chpcl 22596 . . . . . . . . . . . . . . 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 9525 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  e.  RR )
316315recnd 9524 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  e.  CC )
317293, 297, 301, 305, 307, 310, 316fsumparts 13388 . . . . . . . . . . 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 9517 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) )  e.  CC )
319212, 119addcld 9517 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  e.  CC )
320318, 319negsubdi2d 9847 . . . . . . . . . . . . . 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 6217 . . . . . . . . . . . . 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 9910 . . . . . . . . . . . . 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 2497 . . . . . . . . . . . 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 13303 . . . . . . . . . . 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 2497 . . . . . . . . . 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 2501 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  -u (
(ψ `  x )  +  sum_ n  e.  ( 1 ...