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

Theorem pntrlog2bndlem2 21264
Description: Lemma for pntrlog2bnd 21270. 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 1re 9082 . . 3  |-  1  e.  RR
21a1i 11 . 2  |-  ( ph  ->  1  e.  RR )
3 elioore 10938 . . . . . . . 8  |-  ( x  e.  ( 1 (,) 
+oo )  ->  x  e.  RR )
43adantl 453 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR )
5 chpcl 20899 . . . . . . 7  |-  ( x  e.  RR  ->  (ψ `  x )  e.  RR )
64, 5syl 16 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (ψ `  x )  e.  RR )
76recnd 9106 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (ψ `  x )  e.  CC )
8 fzfid 11304 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
94adantr 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
10 elfznn 11072 . . . . . . . . . . . 12  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
1110adantl 453 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
1211peano2nnd 10009 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  e.  NN )
139, 12nndivred 10040 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  e.  RR )
14 chpcl 20899 . . . . . . . . 9  |-  ( ( x  /  ( n  +  1 ) )  e.  RR  ->  (ψ `  ( x  /  (
n  +  1 ) ) )  e.  RR )
1513, 14syl 16 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  ( n  +  1 ) ) )  e.  RR )
1615, 13readdcld 9107 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  e.  RR )
178, 16fsumrecl 12520 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  e.  RR )
1817recnd 9106 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  e.  CC )
194recnd 9106 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  CC )
20 eliooord 10962 . . . . . . . . . 10  |-  ( x  e.  ( 1 (,) 
+oo )  ->  (
1  <  x  /\  x  <  +oo ) )
2120adantl 453 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  <  x  /\  x  <  +oo ) )
2221simpld 446 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <  x )
234, 22rplogcld 20516 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR+ )
2423rpcnd 10642 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  CC )
2519, 24mulcld 9100 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  x.  ( log `  x ) )  e.  CC )
26 1rp 10608 . . . . . . . . 9  |-  1  e.  RR+
2726a1i 11 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR+ )
281a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR )
2928, 4, 22ltled 9213 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <_  x )
304, 27, 29rpgecld 10675 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR+ )
3130rpne0d 10645 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  =/=  0 )
3223rpne0d 10645 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  =/=  0 )
3319, 24, 31, 32mulne0d 9666 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  x.  ( log `  x ) )  =/=  0 )
347, 18, 25, 33divdird 9820 . . . 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
) ) ) ) )
3534mpteq2dva 4287 . . 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
) ) ) ) ) )
3630, 23rpmulcld 10656 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  x.  ( log `  x ) )  e.  RR+ )
376, 36rerpdivcld 10667 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  /  ( x  x.  ( log `  x
) ) )  e.  RR )
3817, 36rerpdivcld 10667 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) )  / 
( x  x.  ( log `  x ) ) )  e.  RR )
397, 19, 24, 31, 32divdiv1d 9813 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( (ψ `  x
)  /  x )  /  ( log `  x
) )  =  ( (ψ `  x )  /  ( x  x.  ( log `  x
) ) ) )
406, 30rerpdivcld 10667 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  /  x )  e.  RR )
4140recnd 9106 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  /  x )  e.  CC )
4241, 24, 32divrecd 9785 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( (ψ `  x
)  /  x )  /  ( log `  x
) )  =  ( ( (ψ `  x
)  /  x )  x.  ( 1  / 
( log `  x
) ) ) )
4339, 42eqtr3d 2469 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  /  ( x  x.  ( log `  x
) ) )  =  ( ( (ψ `  x )  /  x
)  x.  ( 1  /  ( log `  x
) ) ) )
4443mpteq2dva 4287 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( (ψ `  x
)  /  ( x  x.  ( log `  x
) ) ) )  =  ( x  e.  ( 1 (,)  +oo )  |->  ( ( (ψ `  x )  /  x
)  x.  ( 1  /  ( log `  x
) ) ) ) )
4523rprecred 10651 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  /  ( log `  x ) )  e.  RR )
4630ex 424 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  ->  x  e.  RR+ )
)
4746ssrdv 3346 . . . . . . 7  |-  ( ph  ->  ( 1 (,)  +oo )  C_  RR+ )
48 chpo1ub 21166 . . . . . . . 8  |-  ( x  e.  RR+  |->  ( (ψ `  x )  /  x
) )  e.  O
( 1 )
4948a1i 11 . . . . . . 7  |-  ( ph  ->  ( x  e.  RR+  |->  ( (ψ `  x )  /  x ) )  e.  O ( 1 ) )
5047, 49o1res2 12349 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( (ψ `  x
)  /  x ) )  e.  O ( 1 ) )
51 divlogrlim 20518 . . . . . . 7  |-  ( x  e.  ( 1 (,) 
+oo )  |->  ( 1  /  ( log `  x
) ) )  ~~> r  0
52 rlimo1 12402 . . . . . . 7  |-  ( ( x  e.  ( 1 (,)  +oo )  |->  ( 1  /  ( log `  x
) ) )  ~~> r  0  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  / 
( log `  x
) ) )  e.  O ( 1 ) )
5351, 52mp1i 12 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  O ( 1 ) )
5440, 45, 50, 53o1mul2 12410 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( (ψ `  x )  /  x
)  x.  ( 1  /  ( log `  x
) ) ) )  e.  O ( 1 ) )
5544, 54eqeltrd 2509 . . . 4  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( (ψ `  x
)  /  ( x  x.  ( log `  x
) ) ) )  e.  O ( 1 ) )
56 pntrlog2bndlem2.1 . . . . . . . . 9  |-  ( ph  ->  A  e.  RR+ )
5756rpred 10640 . . . . . . . 8  |-  ( ph  ->  A  e.  RR )
5857, 2readdcld 9107 . . . . . . 7  |-  ( ph  ->  ( A  +  1 )  e.  RR )
5958adantr 452 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( A  +  1 )  e.  RR )
6028, 45readdcld 9107 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  e.  RR )
61 ioossre 10964 . . . . . . 7  |-  ( 1 (,)  +oo )  C_  RR
6258recnd 9106 . . . . . . 7  |-  ( ph  ->  ( A  +  1 )  e.  CC )
63 o1const 12405 . . . . . . 7  |-  ( ( ( 1 (,)  +oo )  C_  RR  /\  ( A  +  1 )  e.  CC )  -> 
( x  e.  ( 1 (,)  +oo )  |->  ( A  +  1 ) )  e.  O
( 1 ) )
6461, 62, 63sylancr 645 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( A  +  1 ) )  e.  O
( 1 ) )
65 ax-1cn 9040 . . . . . . . . 9  |-  1  e.  CC
6665a1i 11 . . . . . . . 8  |-  ( ph  ->  1  e.  CC )
67 o1const 12405 . . . . . . . 8  |-  ( ( ( 1 (,)  +oo )  C_  RR  /\  1  e.  CC )  ->  (
x  e.  ( 1 (,)  +oo )  |->  1 )  e.  O ( 1 ) )
6861, 66, 67sylancr 645 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  1 )  e.  O
( 1 ) )
6928, 45, 68, 53o1add2 12409 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  +  ( 1  /  ( log `  x ) ) ) )  e.  O ( 1 ) )
7059, 60, 64, 69o1mul2 12410 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( A  + 
1 )  x.  (
1  +  ( 1  /  ( log `  x
) ) ) ) )  e.  O ( 1 ) )
7159, 60remulcld 9108 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  e.  RR )
7238recnd 9106 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) )  / 
( x  x.  ( log `  x ) ) )  e.  CC )
73 chpge0 20901 . . . . . . . . . . . 12  |-  ( ( x  /  ( n  +  1 ) )  e.  RR  ->  0  <_  (ψ `  ( x  /  ( n  + 
1 ) ) ) )
7413, 73syl 16 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (ψ `  ( x  /  (
n  +  1 ) ) ) )
7511nnrpd 10639 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
7626a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR+ )
7775, 76rpaddcld 10655 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  e.  RR+ )
7830adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
7978rpge0d 10644 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  x )
809, 77, 79divge0d 10676 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( x  /  ( n  +  1 ) ) )
8115, 13, 74, 80addge0d 9594 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )
828, 16, 81fsumge0 12566 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_ 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )
8317, 36, 82divge0d 10676 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  /  ( x  x.  ( log `  x
) ) ) )
8438, 83absidd 12217 . . . . . . 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
) ) ) )
8571recnd 9106 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  e.  CC )
8685abscld 12230 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( abs `  ( ( A  +  1 )  x.  ( 1  +  ( 1  /  ( log `  x ) ) ) ) )  e.  RR )
8717, 30rerpdivcld 10667 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) )  /  x )  e.  RR )
8830relogcld 20510 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR )
8988, 28readdcld 9107 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  +  1 )  e.  RR )
9059, 89remulcld 9108 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( A  +  1 )  x.  ( ( log `  x )  +  1 ) )  e.  RR )
9159, 4remulcld 9108 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( A  +  1 )  x.  x )  e.  RR )
9211nnrecred 10037 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  n )  e.  RR )
938, 92fsumrecl 12520 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
)  e.  RR )
9491, 93remulcld 9108 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( A  + 
1 )  x.  x
)  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
) )  e.  RR )
9591, 89remulcld 9108 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( A  + 
1 )  x.  x
)  x.  ( ( log `  x )  +  1 ) )  e.  RR )
9657ad2antrr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A  e.  RR )
971a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
9896, 97readdcld 9107 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( A  +  1 )  e.  RR )
9998, 9remulcld 9108 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( A  +  1 )  x.  x )  e.  RR )
10099, 92remulcld 9108 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  x.  ( 1  /  n ) )  e.  RR )
10199, 12nndivred 10040 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  ( n  + 
1 ) )  e.  RR )
10299, 11nndivred 10040 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  n )  e.  RR )
10396, 13remulcld 9108 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( A  x.  ( x  /  (
n  +  1 ) ) )  e.  RR )
10478, 77rpdivcld 10657 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  e.  RR+ )
105 pntrlog2bndlem2.2 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A. y  e.  RR+  (ψ `  y )  <_ 
( A  x.  y
) )
106105ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A. y  e.  RR+  (ψ `  y
)  <_  ( A  x.  y ) )
107 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x  / 
( n  +  1 ) )  ->  (ψ `  y )  =  (ψ `  ( x  /  (
n  +  1 ) ) ) )
108 oveq2 6081 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x  / 
( n  +  1 ) )  ->  ( A  x.  y )  =  ( A  x.  ( x  /  (
n  +  1 ) ) ) )
109107, 108breq12d 4217 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( x  / 
( n  +  1 ) )  ->  (
(ψ `  y )  <_  ( A  x.  y
)  <->  (ψ `  ( x  /  ( n  + 
1 ) ) )  <_  ( A  x.  ( x  /  (
n  +  1 ) ) ) ) )
110109rspcv 3040 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  /  ( n  +  1 ) )  e.  RR+  ->  ( A. y  e.  RR+  (ψ `  y )  <_  ( A  x.  y )  ->  (ψ `  ( x  /  ( n  + 
1 ) ) )  <_  ( A  x.  ( x  /  (
n  +  1 ) ) ) ) )
111104, 106, 110sylc 58 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  ( n  +  1 ) ) )  <_  ( A  x.  ( x  /  (
n  +  1 ) ) ) )
11215, 103, 13, 111leadd1dd 9632 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  <_  ( ( A  x.  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )
11362ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( A  +  1 )  e.  CC )
11419adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  CC )
11511nncnd 10008 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
11665a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  CC )
117115, 116addcld 9099 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  e.  CC )
11812nnne0d 10036 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  =/=  0 )
119113, 114, 117, 118divassd 9817 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  ( n  + 
1 ) )  =  ( ( A  + 
1 )  x.  (
x  /  ( n  +  1 ) ) ) )
12096recnd 9106 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A  e.  CC )
121114, 117, 118divcld 9782 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  e.  CC )
122120, 116, 121adddird 9105 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
123121mulid2d 9098 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  ( x  / 
( n  +  1 ) ) )  =  ( x  /  (
n  +  1 ) ) )
124123oveq2d 6089 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
125119, 122, 1243eqtrd 2471 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  ( n  + 
1 ) )  =  ( ( A  x.  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) )
126112, 125breqtrrd 4230 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  <_  ( (
( A  +  1 )  x.  x )  /  ( n  + 
1 ) ) )
12757adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  A  e.  RR )
12856adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  A  e.  RR+ )
129128rpge0d 10644 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  A )
13027rpge0d 10644 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  1 )
131127, 28, 129, 130addge0d 9594 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  ( A  +  1 ) )
13230rpge0d 10644 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  x )
13359, 4, 131, 132mulge0d 9595 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  ( ( A  + 
1 )  x.  x
) )
134133adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( A  +  1 )  x.  x ) )
13511nnred 10007 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
136135lep1d 9934 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  <_  ( n  +  1 ) )
13775, 77, 99, 134, 136lediv2ad 10662 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  ( n  + 
1 ) )  <_ 
( ( ( A  +  1 )  x.  x )  /  n
) )
13816, 101, 102, 126, 137letrd 9219 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  <_  ( (
( A  +  1 )  x.  x )  /  n ) )
13999recnd 9106 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( A  +  1 )  x.  x )  e.  CC )
14011nnne0d 10036 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0 )
141139, 115, 140divrecd 9785 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  n )  =  ( ( ( A  +  1 )  x.  x )  x.  (
1  /  n ) ) )
142138, 141breqtrd 4228 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  <_  ( (
( A  +  1 )  x.  x )  x.  ( 1  /  n ) ) )
1438, 16, 100, 142fsumle 12570 . . . . . . . . . . . . . 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 ) ) )
14491recnd 9106 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( A  +  1 )  x.  x )  e.  CC )
145115, 140reccld 9775 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  n )  e.  CC )
1468, 144, 145fsummulc2 12559 . . . . . . . . . . . . . 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 ) ) )
147143, 146breqtrrd 4230 . . . . . . . . . . . . 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 ) ) )
148 harmonicubnd 20840 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR  /\  1  <_  x )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n )  <_  ( ( log `  x )  +  1 ) )
1494, 29, 148syl2anc 643 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
)  <_  ( ( log `  x )  +  1 ) )
15093, 89, 91, 133, 149lemul2ad 9943 . . . . . . . . . . . . 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 ) ) )
15117, 94, 95, 147, 150letrd 9219 . . . . . . . . . . . 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 ) ) )
15262adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( A  +  1 )  e.  CC )
15389recnd 9106 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  +  1 )  e.  CC )
154152, 19, 153mul32d 9268 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( A  + 
1 )  x.  x
)  x.  ( ( log `  x )  +  1 ) )  =  ( ( ( A  +  1 )  x.  ( ( log `  x )  +  1 ) )  x.  x
) )
155151, 154breqtrd 4228 . . . . . . . . . . 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
) )
15617, 90, 30ledivmul2d 10690 . . . . . . . . . . 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
) ) )
157155, 156mpbird 224 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) )  /  x )  <_  (
( A  +  1 )  x.  ( ( log `  x )  +  1 ) ) )
15887, 90, 23, 157lediv1dd 10694 . . . . . . . . 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 ) ) )
15918, 19, 24, 31, 32divdiv1d 9813 . . . . . . . . 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 ) ) ) )
16065a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  CC )
16124, 160addcld 9099 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  +  1 )  e.  CC )
162152, 161, 24, 32divassd 9817 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( A  + 
1 )  x.  (
( log `  x
)  +  1 ) )  /  ( log `  x ) )  =  ( ( A  + 
1 )  x.  (
( ( log `  x
)  +  1 )  /  ( log `  x
) ) ) )
16324, 160, 24, 32divdird 9820 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( log `  x
)  +  1 )  /  ( log `  x
) )  =  ( ( ( log `  x
)  /  ( log `  x ) )  +  ( 1  /  ( log `  x ) ) ) )
16424, 32dividd 9780 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  /  ( log `  x ) )  =  1 )
165164oveq1d 6088 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( log `  x
)  /  ( log `  x ) )  +  ( 1  /  ( log `  x ) ) )  =  ( 1  +  ( 1  / 
( log `  x
) ) ) )
166163, 165eqtr2d 2468 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  =  ( ( ( log `  x )  +  1 )  /  ( log `  x ) ) )
167166oveq2d 6089 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( ( A  +  1 )  x.  ( ( ( log `  x )  +  1 )  /  ( log `  x ) ) ) )
168162, 167eqtr4d 2470 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( A  + 
1 )  x.  (
( log `  x
)  +  1 ) )  /  ( log `  x ) )  =  ( ( A  + 
1 )  x.  (
1  +  ( 1  /  ( log `  x
) ) ) ) )
169158, 159, 1683brtr3d 4233 . . . . . . . 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 ) ) ) ) )
17071leabsd 12209 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  <_  ( abs `  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) ) ) )
17138, 71, 86, 169, 170letrd 9219 . . . . . . 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
) ) ) ) ) )
17284, 171eqbrtrd 4224 . . . . . 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
) ) ) ) ) )
173172adantrr 698 . . . . 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
) ) ) ) ) )
1742, 70, 71, 72, 173o1le 12438 . . . 4  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  /  ( x  x.  ( log `  x
) ) ) )  e.  O ( 1 ) )
17537, 38, 55, 174o1add2 12409 . . 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 ) )
17635, 175eqeltrd 2509 . 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 ) )
1776, 17readdcld 9107 . . 3  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  +  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) ) )  e.  RR )
178177, 36rerpdivcld 10667 . 2  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( (ψ `  x
)  +  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) ) )  /  ( x  x.  ( log `  x
) ) )  e.  RR )
179 pntrlog2bnd.r . . . . . . . . . . . 12  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
180179pntrf 21249 . . . . . . . . . . 11  |-  R : RR+
--> RR
181180ffvelrni 5861 . . . . . . . . . 10  |-  ( ( x  /  ( n  +  1 ) )  e.  RR+  ->  ( R `
 ( x  / 
( n  +  1 ) ) )  e.  RR )
182104, 181syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  (
n  +  1 ) ) )  e.  RR )
183182recnd 9106 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  (
n  +  1 ) ) )  e.  CC )
18478, 75rpdivcld 10657 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
185180ffvelrni 5861 . . . . . . . . . 10  |-  ( ( x  /  n )  e.  RR+  ->  ( R `
 ( x  /  n ) )  e.  RR )
186184, 185syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  RR )
187186recnd 9106 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  CC )
188183, 187subcld 9403 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( R `  ( x  /  ( n  + 
1 ) ) )  -  ( R `  ( x  /  n
) ) )  e.  CC )
189188abscld 12230 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  (
n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) )  e.  RR )
190135, 189remulcld 9108 . . . . 5  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  x.  ( abs `  (
( R `  (
x  /  ( n  +  1 ) ) )  -  ( R `
 ( x  /  n ) ) ) ) )  e.  RR )
1918, 190fsumrecl 12520 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( n  x.  ( abs `  ( ( R `
 ( x  / 
( n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) ) )  e.  RR )
192191, 36rerpdivcld 10667 . . 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 )
193192recnd 9106 . 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 )
19475rpge0d 10644 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  n )
195188absge0d 12238 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( abs `  ( ( R `  ( x  /  ( n  + 
1 ) ) )  -  ( R `  ( x  /  n
) ) ) ) )
196135, 189, 194, 195mulge0d 9595 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( n  x.  ( abs `  ( ( R `  ( x  /  (
n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) ) ) )
1978, 190, 196fsumge0 12566 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_ 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( n  x.  ( abs `  ( ( R `  ( x  /  (
n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) ) ) )
198191, 36, 197divge0d 10676 . . . . 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 ) ) ) )
199192, 198absidd 12217 . . . 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 ) ) ) )
2007, 18addcld 9099 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  +  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) ) )  e.  CC )
201200, 25, 33divcld 9782 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( (ψ `  x
)  +  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) ) )  /  ( x  x.  ( log `  x
) ) )  e.  CC )
202201abscld 12230 . . . . 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 )
2039, 11nndivred 10040 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
204 chpcl 20899 . . . . . . . . . . . 12  |-  ( ( x  /  n )  e.  RR  ->  (ψ `  ( x  /  n
) )  e.  RR )
205203, 204syl 16 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  n ) )  e.  RR )
206205, 203readdcld 9107 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) )  e.  RR )
207206, 16resubcld 9457 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(ψ `  ( x  /  n ) )  +  ( x  /  n
) )  -  (
(ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )  e.  RR )
208135, 207remulcld 9108 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  x.  ( ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) )  -  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) ) )  e.  RR )
209179pntrval 21248 . . . . . . . . . . . . . . 15  |-  ( ( x  /  ( n  +  1 ) )  e.  RR+  ->  ( R `
 ( x  / 
( n  +  1 ) ) )  =  ( (ψ `  (
x  /  ( n  +  1 ) ) )  -  ( x  /  ( n  + 
1 ) ) ) )
210104, 209syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  (
n  +  1 ) ) )  =  ( (ψ `  ( x  /  ( n  + 
1 ) ) )  -  ( x  / 
( n  +  1 ) ) ) )
211179pntrval 21248 . . . . . . . . . . . . . . 15  |-  ( ( x  /  n )  e.  RR+  ->  ( R `
 ( x  /  n ) )  =  ( (ψ `  (
x  /  n ) )  -  ( x  /  n ) ) )
212184, 211syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  =  ( (ψ `  ( x  /  n ) )  -  ( x  /  n
) ) )
213210, 212oveq12d 6091 . . . . . . . . . . . . 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 ) ) ) )
21415recnd 9106 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  ( n  +  1 ) ) )  e.  CC )
215205recnd 9106 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  n ) )  e.  CC )
216114, 115, 140divcld 9782 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  CC )
217214, 121, 215, 216sub4d 9452 . . . . . . . . . . . . 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 ) ) ) )
218213, 217eqtrd 2467 . . . . . . . . . . . 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 ) ) ) )
219218fveq2d 5724 . . . . . . . . . . 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 ) ) ) ) )
220214, 215subcld 9403 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  -  (ψ `  ( x  /  n
) ) )  e.  CC )
221121, 216subcld 9403 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
x  /  ( n  +  1 ) )  -  ( x  /  n ) )  e.  CC )
222220, 221abs2dif2d 12252 . . . . . . . . . . 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 ) ) ) ) )
223219, 222eqbrtrd 4224 . . . . . . . . . 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 ) ) ) ) )
22475, 77, 9, 79, 136lediv2ad 10662 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  <_ 
( x  /  n
) )
225 chpwordi 20932 . . . . . . . . . . . . . 14  |-  ( ( ( x  /  (
n  +  1 ) )  e.  RR  /\  ( x  /  n
)  e.  RR  /\  ( x  /  (
n  +  1 ) )  <_  ( x  /  n ) )  -> 
(ψ `  ( x  /  ( n  + 
1 ) ) )  <_  (ψ `  (
x  /  n ) ) )
22613, 203, 224, 225syl3anc 1184 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  ( n  +  1 ) ) )  <_  (ψ `  (
x  /  n ) ) )
22715, 205, 226abssuble0d 12227 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( (ψ `  (
x  /  ( n  +  1 ) ) )  -  (ψ `  ( x  /  n
) ) ) )  =  ( (ψ `  ( x  /  n
) )  -  (ψ `  ( x  /  (
n  +  1 ) ) ) ) )
22813, 203, 224abssuble0d 12227 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( x  / 
( n  +  1 ) )  -  (
x  /  n ) ) )  =  ( ( x  /  n
)  -  ( x  /  ( n  + 
1 ) ) ) )
229227, 228oveq12d 6091 . . . . . . . . . . 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 ) ) ) ) )
230215, 216, 214, 121addsub4d 9450 . . . . . . . . . . 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 ) ) ) ) )
231229, 230eqtr4d 2470 . . . . . . . . . 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 ) ) ) ) )
232223, 231breqtrd 4228 . . . . . . . . 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 ) ) ) ) )
233189, 207, 135, 194, 232lemul2ad 9943 . . . . . . . 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 ) ) ) ) ) )
2348, 190, 208, 233fsumle 12570 . . . . . . 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 ) ) ) ) ) )
235207recnd 9106 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(ψ `  ( x  /  n ) )  +  ( x  /  n
) )  -  (
(ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )  e.  CC )
236115, 235mulcld 9100 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  x.  ( ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) )  -  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) ) )  e.  CC )
2378, 236fsumcl 12519 . . . . . . . 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 )
2387, 18negdi2d 9417 . . . . . . . . . 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 ) ) ) ) )
23930rprege0d 10647 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  e.  RR  /\  0  <_  x ) )
240 flge0nn0 11217 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( |_ `  x
)  e.  NN0 )
241 nn0p1nn 10251 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( |_ `  x )  e.  NN0  ->  ( ( |_ `  x )  +  1 )  e.  NN )
242239, 240, 2413syl 19 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  NN )
2434, 242nndivred 10040 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  RR )
244 2re 10061 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
245244a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  RR )
246 flltp1 11201 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  x  <  ( ( |_ `  x )  +  1 ) )
2474, 246syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  <  ( ( |_ `  x )  +  1 ) )
248242nncnd 10008 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  CC )
249248mulid1d 9097 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  1 )  =  ( ( |_
`  x )  +  1 ) )
250247, 249breqtrrd 4230 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  <  ( ( ( |_
`  x )  +  1 )  x.  1 ) )
251242nnrpd 10639 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  RR+ )
2524, 28, 251ltdivmuld 10687 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  <  1  <->  x  <  ( ( ( |_
`  x )  +  1 )  x.  1 ) ) )
253250, 252mpbird 224 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  <  1 )
254 1lt2 10134 . . . . . . . . . . . . . . . . . . . 20  |-  1  <  2
255254a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <  2 )
256243, 28, 245, 253, 255lttrd 9223 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  <  2 )
257 chpeq0 20984 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  /  ( ( |_ `  x )  +  1 ) )  e.  RR  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  0  <->  ( x  /  ( ( |_
`  x )  +  1 ) )  <  2 ) )
258243, 257syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  0  <->  ( x  /  ( ( |_
`  x )  +  1 ) )  <  2 ) )
259256, 258mpbird 224 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  =  0 )
260259oveq1d 6088 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) )  =  ( 0  +  ( x  /  ( ( |_ `  x )  +  1 ) ) ) )
261243recnd 9106 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  CC )
262261addid2d 9259 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
0  +  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  ( x  / 
( ( |_ `  x )  +  1 ) ) )
263260, 262eqtrd 2467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) )  =  ( x  /  (
( |_ `  x
)  +  1 ) ) )
264263oveq2d 6089 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  ( (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  +  ( x  /  ( ( |_ `  x )  +  1 ) ) ) )  =  ( ( ( |_ `  x )  +  1 )  x.  ( x  /  ( ( |_
`  x )  +  1 ) ) ) )
265242nnne0d 10036 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( |_ `  x
)  +  1 )  =/=  0 )
26619, 248, 265divcan2d 9784 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  x )
267264, 266eqtrd 2467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  ( (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  +  ( x  /  ( ( |_ `  x )  +  1 ) ) ) )  =  x )
26819div1d 9774 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  /  1 )  =  x )
269268fveq2d 5724 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (ψ `  ( x  /  1
) )  =  (ψ `  x ) )
270269, 268oveq12d 6091 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  ( x  /  1 ) )  +  ( x  / 
1 ) )  =  ( (ψ `  x
)  +  x ) )
271270oveq2d 6089 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  x.  ( (ψ `  ( x  /  1
) )  +  ( x  /  1 ) ) )  =  ( 1  x.  ( (ψ `  x )  +  x
) ) )
2726, 4readdcld 9107 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  +  x )  e.  RR )
273272recnd 9106 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  +  x )  e.  CC )
274273mulid2d 9098 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  x.  ( (ψ `  x )  +  x
) )  =  ( (ψ `  x )  +  x ) )
275271, 274eqtrd 2467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  x.  ( (ψ `  ( x  /  1
) )  +  ( x  /  1 ) ) )  =  ( (ψ `  x )  +  x ) )
276267, 275oveq12d 6091 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( |_
`  x )  +  1 )  x.  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) ) )  -  ( 1  x.  ( (ψ `  (
x  /  1 ) )  +  ( x  /  1 ) ) ) )  =  ( x  -  ( (ψ `  x )  +  x
) ) )
277273, 19negsubdi2d 9419 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  -u (
( (ψ `  x
)  +  x )  -  x )  =  ( x  -  (
(ψ `  x )  +  x ) ) )
2787, 19pncand 9404 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( (ψ `  x
)  +  x )  -  x )  =  (ψ `  x )
)
279278negeqd 9292 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  -u (
( (ψ `  x
)  +  x )  -  x )  = 
-u (ψ `  x
) )
280276, 277, 2793eqtr2d 2473 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( |_
`  x )  +  1 )  x.  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) ) )  -  ( 1  x.  ( (ψ `  (
x  /  1 ) )  +  ( x  /  1 ) ) ) )  =  -u (ψ `  x ) )
2814flcld 11199 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( |_ `  x )  e.  ZZ )
282 fzval3 11172 . . . . . . . . . . . . . 14  |-  ( ( |_ `  x )  e.  ZZ  ->  (
1 ... ( |_ `  x ) )  =  ( 1..^ ( ( |_ `  x )  +  1 ) ) )
283281, 282syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1 ... ( |_ `  x ) )  =  ( 1..^ ( ( |_ `  x )  +  1 ) ) )
284283eqcomd 2440 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1..^ ( ( |_
`  x )  +  1 ) )  =  ( 1 ... ( |_ `  x ) ) )
285115, 116pncan2d 9405 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
n  +  1 )  -  n )  =  1 )
286285oveq1d 6088 . . . . . . . . . . . . 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 ) ) ) ) )
28716recnd 9106 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  e.  CC )
288287mulid2d 9098 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) ) )  =  ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )
289286, 288eqtrd 2467 . . . . . . . . . . . 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 ) ) ) )
290284, 289sumeq12rdv 12493 . . . . . . . . . . 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 ) ) ) )
291280, 290oveq12d 6091 . . . . . . . . . 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 ) ) ) ) )
292 oveq2 6081 . . . . . . . . . . . . . . 15  |-  ( m  =  n  ->  (
x  /  m )  =  ( x  /  n ) )
293292fveq2d 5724 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  (ψ `  ( x  /  m
) )  =  (ψ `  ( x  /  n
) ) )
294293, 292oveq12d 6091 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  n ) )  +  ( x  /  n
) ) )
295294ancli 535 . . . . . . . . . . . 12  |-  ( m  =  n  ->  (
m  =  n  /\  ( (ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  n ) )  +  ( x  /  n
) ) ) )
296 oveq2 6081 . . . . . . . . . . . . . . 15  |-  ( m  =  ( n  + 
1 )  ->  (
x  /  m )  =  ( x  / 
( n  +  1 ) ) )
297296fveq2d 5724 . . . . . . . . . . . . . 14  |-  ( m  =  ( n  + 
1 )  ->  (ψ `  ( x  /  m
) )  =  (ψ `  ( x  /  (
n  +  1 ) ) ) )
298297, 296oveq12d 6091 . . . . . . . . . . . . 13  |-  ( m  =  ( n  + 
1 )  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )
299298ancli 535 . . . . . . . . . . . 12  |-  ( m  =  ( n  + 
1 )  ->  (
m  =  ( n  +  1 )  /\  ( (ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) ) )
300 oveq2 6081 . . . . . . . . . . . . . . 15  |-  ( m  =  1  ->  (
x  /  m )  =  ( x  / 
1 ) )
301300fveq2d 5724 . . . . . . . . . . . . . 14  |-  ( m  =  1  ->  (ψ `  ( x  /  m
) )  =  (ψ `  ( x  /  1
) ) )
302301, 300oveq12d 6091 . . . . . . . . . . . . 13  |-  ( m  =  1  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  1 ) )  +  ( x  / 
1 ) ) )
303302ancli 535 . . . . . . . . . . . 12  |-  ( m  =  1  ->  (
m  =  1  /\  ( (ψ `  (
x  /  m ) )  +  ( x  /  m ) )  =  ( (ψ `  ( x  /  1
) )  +  ( x  /  1 ) ) ) )
304 oveq2 6081 . . . . . . . . . . . . . . 15  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
x  /  m )  =  ( x  / 
( ( |_ `  x )  +  1 ) ) )
305304fveq2d 5724 . . . . . . . . . . . . . 14  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (ψ `  ( x  /  m
) )  =  (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )
306305, 304oveq12d 6091 . . . . . . . . . . . . 13  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) ) )
307306ancli 535 . . . . . . . . . . . 12  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
m  =  ( ( |_ `  x )  +  1 )  /\  ( (ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) ) ) )
308 nnuz 10513 . . . . . . . . . . . . 13  |-  NN  =  ( ZZ>= `  1 )
309242, 308syl6eleq 2525 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  ( ZZ>= `  1
) )
310 elfznn 11072 . . . . . . . . . . . . . 14  |-  ( m  e.  ( 1 ... ( ( |_ `  x )  +  1 ) )  ->  m  e.  NN )
311310adantl 453 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  NN )
312311nncnd 10008 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  CC )
3134adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  x  e.  RR )
314313, 311nndivred 10040 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
x  /  m )  e.  RR )
315 chpcl 20899 . . . . . . . . . . . . . . 15  |-  ( ( x  /  m )  e.  RR  ->  (ψ `  ( x  /  m
) )  e.  RR )
316314, 315syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (ψ `  ( x  /  m
) )  e.  RR )
317316, 314readdcld 9107 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  e.  RR )
318317recnd 9106 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  e.  CC )
319295, 299, 303, 307, 309, 312, 318fsumparts 12577 . . . . . . . . . . 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 ) ) ) ) ) )
320215, 216addcld 9099 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) )  e.  CC )
321214, 121addcld 9099 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  e.  CC )
322320, 321negsubdi2d 9419 . . . . . . . . . . . . . 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 ) ) ) )
323322oveq2d 6089 . . . . . . . . . . . . 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 ) ) ) ) )
324115, 235mulneg2d 9479 . . . . . . . . . . . . 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 ) ) ) ) ) )
325323, 324eqtr3d 2469 . . . . . . . . . . . 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 ) ) ) ) ) )
326284, 325sumeq12rdv 12493 . . . . . . . . . . 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 ) ) ) ) ) )
327319, 326eqtr3d 2469 . . . . . . . . . 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 ) ) ) ) ) )
328238, 291, 3273eqtr2d 2473 . . . . . . . . 9  |-  ( (
ph