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

Theorem pntrlog2bndlem2 20727
Description: Lemma for pntrlog2bnd 20733. 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 8837 . . 3  |-  1  e.  RR
21a1i 10 . 2  |-  ( ph  ->  1  e.  RR )
3 elioore 10686 . . . . . . . 8  |-  ( x  e.  ( 1 (,) 
+oo )  ->  x  e.  RR )
43adantl 452 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR )
5 chpcl 20362 . . . . . . 7  |-  ( x  e.  RR  ->  (ψ `  x )  e.  RR )
64, 5syl 15 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (ψ `  x )  e.  RR )
76recnd 8861 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (ψ `  x )  e.  CC )
8 fzfid 11035 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
94adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
10 elfznn 10819 . . . . . . . . . . . 12  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
1110adantl 452 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
1211peano2nnd 9763 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  e.  NN )
139, 12nndivred 9794 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  e.  RR )
14 chpcl 20362 . . . . . . . . 9  |-  ( ( x  /  ( n  +  1 ) )  e.  RR  ->  (ψ `  ( x  /  (
n  +  1 ) ) )  e.  RR )
1513, 14syl 15 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  ( n  +  1 ) ) )  e.  RR )
1615, 13readdcld 8862 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  e.  RR )
178, 16fsumrecl 12207 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  e.  RR )
1817recnd 8861 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  e.  CC )
194recnd 8861 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  CC )
20 eliooord 10710 . . . . . . . . . 10  |-  ( x  e.  ( 1 (,) 
+oo )  ->  (
1  <  x  /\  x  <  +oo ) )
2120adantl 452 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  <  x  /\  x  <  +oo ) )
2221simpld 445 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <  x )
234, 22rplogcld 19980 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR+ )
2423rpcnd 10392 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  CC )
2519, 24mulcld 8855 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  x.  ( log `  x ) )  e.  CC )
26 1rp 10358 . . . . . . . . 9  |-  1  e.  RR+
2726a1i 10 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR+ )
281a1i 10 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR )
2928, 4, 22ltled 8967 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <_  x )
304, 27, 29rpgecld 10425 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR+ )
3130rpne0d 10395 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  =/=  0 )
3223rpne0d 10395 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  =/=  0 )
3319, 24, 31, 32mulne0d 9420 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  x.  ( log `  x ) )  =/=  0 )
347, 18, 25, 33divdird 9574 . . . 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 4106 . . 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 10406 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  x.  ( log `  x ) )  e.  RR+ )
376, 36rerpdivcld 10417 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  /  ( x  x.  ( log `  x
) ) )  e.  RR )
3817, 36rerpdivcld 10417 . . . 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 9567 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( (ψ `  x
)  /  x )  /  ( log `  x
) )  =  ( (ψ `  x )  /  ( x  x.  ( log `  x
) ) ) )
406, 30rerpdivcld 10417 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  /  x )  e.  RR )
4140recnd 8861 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  /  x )  e.  CC )
4241, 24, 32divrecd 9539 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( (ψ `  x
)  /  x )  /  ( log `  x
) )  =  ( ( (ψ `  x
)  /  x )  x.  ( 1  / 
( log `  x
) ) ) )
4339, 42eqtr3d 2317 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  /  ( x  x.  ( log `  x
) ) )  =  ( ( (ψ `  x )  /  x
)  x.  ( 1  /  ( log `  x
) ) ) )
4443mpteq2dva 4106 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( (ψ `  x
)  /  ( x  x.  ( log `  x
) ) ) )  =  ( x  e.  ( 1 (,)  +oo )  |->  ( ( (ψ `  x )  /  x
)  x.  ( 1  /  ( log `  x
) ) ) ) )
4523rprecred 10401 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  /  ( log `  x ) )  e.  RR )
4630ex 423 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  ->  x  e.  RR+ )
)
4746ssrdv 3185 . . . . . . 7  |-  ( ph  ->  ( 1 (,)  +oo )  C_  RR+ )
48 chpo1ub 20629 . . . . . . . 8  |-  ( x  e.  RR+  |->  ( (ψ `  x )  /  x
) )  e.  O
( 1 )
4948a1i 10 . . . . . . 7  |-  ( ph  ->  ( x  e.  RR+  |->  ( (ψ `  x )  /  x ) )  e.  O ( 1 ) )
5047, 49o1res2 12037 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( (ψ `  x
)  /  x ) )  e.  O ( 1 ) )
51 divlogrlim 19982 . . . . . . 7  |-  ( x  e.  ( 1 (,) 
+oo )  |->  ( 1  /  ( log `  x
) ) )  ~~> r  0
52 rlimo1 12090 . . . . . . 7  |-  ( ( x  e.  ( 1 (,)  +oo )  |->  ( 1  /  ( log `  x
) ) )  ~~> r  0  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  / 
( log `  x
) ) )  e.  O ( 1 ) )
5351, 52mp1i 11 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  O ( 1 ) )
5440, 45, 50, 53o1mul2 12098 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( (ψ `  x )  /  x
)  x.  ( 1  /  ( log `  x
) ) ) )  e.  O ( 1 ) )
5544, 54eqeltrd 2357 . . . 4  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( (ψ `  x
)  /  ( x  x.  ( log `  x
) ) ) )  e.  O ( 1 ) )
56 pntrlog2bndlem2.1 . . . . . . . . 9  |-  ( ph  ->  A  e.  RR+ )
5756rpred 10390 . . . . . . . 8  |-  ( ph  ->  A  e.  RR )
5857, 2readdcld 8862 . . . . . . 7  |-  ( ph  ->  ( A  +  1 )  e.  RR )
5958adantr 451 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( A  +  1 )  e.  RR )
6028, 45readdcld 8862 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  e.  RR )
61 ioossre 10712 . . . . . . 7  |-  ( 1 (,)  +oo )  C_  RR
6258recnd 8861 . . . . . . 7  |-  ( ph  ->  ( A  +  1 )  e.  CC )
63 o1const 12093 . . . . . . 7  |-  ( ( ( 1 (,)  +oo )  C_  RR  /\  ( A  +  1 )  e.  CC )  -> 
( x  e.  ( 1 (,)  +oo )  |->  ( A  +  1 ) )  e.  O
( 1 ) )
6461, 62, 63sylancr 644 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( A  +  1 ) )  e.  O
( 1 ) )
65 ax-1cn 8795 . . . . . . . . 9  |-  1  e.  CC
6665a1i 10 . . . . . . . 8  |-  ( ph  ->  1  e.  CC )
67 o1const 12093 . . . . . . . 8  |-  ( ( ( 1 (,)  +oo )  C_  RR  /\  1  e.  CC )  ->  (
x  e.  ( 1 (,)  +oo )  |->  1 )  e.  O ( 1 ) )
6861, 66, 67sylancr 644 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  1 )  e.  O
( 1 ) )
6928, 45, 68, 53o1add2 12097 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  +  ( 1  /  ( log `  x ) ) ) )  e.  O ( 1 ) )
7059, 60, 64, 69o1mul2 12098 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( A  + 
1 )  x.  (
1  +  ( 1  /  ( log `  x
) ) ) ) )  e.  O ( 1 ) )
7159, 60remulcld 8863 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  e.  RR )
7238recnd 8861 . . . . 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 20364 . . . . . . . . . . . 12  |-  ( ( x  /  ( n  +  1 ) )  e.  RR  ->  0  <_  (ψ `  ( x  /  ( n  + 
1 ) ) ) )
7413, 73syl 15 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (ψ `  ( x  /  (
n  +  1 ) ) ) )
7511nnrpd 10389 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
7626a1i 10 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR+ )
7775, 76rpaddcld 10405 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  e.  RR+ )
7830adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
7978rpge0d 10394 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  x )
809, 77, 79divge0d 10426 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( x  /  ( n  +  1 ) ) )
8115, 13, 74, 80addge0d 9348 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )
828, 16, 81fsumge0 12253 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_ 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )
8317, 36, 82divge0d 10426 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) )  /  ( x  x.  ( log `  x
) ) ) )
8438, 83absidd 11905 . . . . . . 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 8861 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  e.  CC )
8685abscld 11918 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( abs `  ( ( A  +  1 )  x.  ( 1  +  ( 1  /  ( log `  x ) ) ) ) )  e.  RR )
8717, 30rerpdivcld 10417 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) )  /  x )  e.  RR )
8830relogcld 19974 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR )
8988, 28readdcld 8862 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  +  1 )  e.  RR )
9059, 89remulcld 8863 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( A  +  1 )  x.  ( ( log `  x )  +  1 ) )  e.  RR )
9159, 4remulcld 8863 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( A  +  1 )  x.  x )  e.  RR )
9211nnrecred 9791 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  n )  e.  RR )
938, 92fsumrecl 12207 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
)  e.  RR )
9491, 93remulcld 8863 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( A  + 
1 )  x.  x
)  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
) )  e.  RR )
9591, 89remulcld 8863 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( A  + 
1 )  x.  x
)  x.  ( ( log `  x )  +  1 ) )  e.  RR )
9657ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A  e.  RR )
971a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
9896, 97readdcld 8862 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( A  +  1 )  e.  RR )
9998, 9remulcld 8863 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( A  +  1 )  x.  x )  e.  RR )
10099, 92remulcld 8863 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  x.  ( 1  /  n ) )  e.  RR )
10199, 12nndivred 9794 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  ( n  + 
1 ) )  e.  RR )
10299, 11nndivred 9794 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  n )  e.  RR )
10396, 13remulcld 8863 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( A  x.  ( x  /  (
n  +  1 ) ) )  e.  RR )
10478, 77rpdivcld 10407 . . . . . . . . . . . . . . . . . . . 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 706 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A. y  e.  RR+  (ψ `  y
)  <_  ( A  x.  y ) )
107 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x  / 
( n  +  1 ) )  ->  (ψ `  y )  =  (ψ `  ( x  /  (
n  +  1 ) ) ) )
108 oveq2 5866 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x  / 
( n  +  1 ) )  ->  ( A  x.  y )  =  ( A  x.  ( x  /  (
n  +  1 ) ) ) )
109107, 108breq12d 4036 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( x  / 
( n  +  1 ) )  ->  (
(ψ `  y )  <_  ( A  x.  y
)  <->  (ψ `  ( x  /  ( n  + 
1 ) ) )  <_  ( A  x.  ( x  /  (
n  +  1 ) ) ) ) )
110109rspcv 2880 . . . . . . . . . . . . . . . . . . . 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 56 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  ( n  +  1 ) ) )  <_  ( A  x.  ( x  /  (
n  +  1 ) ) ) )
11215, 103, 13, 111leadd1dd 9386 . . . . . . . . . . . . . . . . . 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 706 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( A  +  1 )  e.  CC )
11419adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  CC )
11511nncnd 9762 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
11665a1i 10 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  CC )
117115, 116addcld 8854 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  e.  CC )
11812nnne0d 9790 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  +  1 )  =/=  0 )
119113, 114, 117, 118divassd 9571 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  ( n  + 
1 ) )  =  ( ( A  + 
1 )  x.  (
x  /  ( n  +  1 ) ) ) )
12096recnd 8861 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A  e.  CC )
121114, 117, 118divcld 9536 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  e.  CC )
122120, 116, 121adddird 8860 . . . . . . . . . . . . . . . . . . 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 8853 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  ( x  / 
( n  +  1 ) ) )  =  ( x  /  (
n  +  1 ) ) )
124123oveq2d 5874 . . . . . . . . . . . . . . . . . . 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 2319 . . . . . . . . . . . . . . . . . 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 4049 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  <_  ( (
( A  +  1 )  x.  x )  /  ( n  + 
1 ) ) )
12757adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  A  e.  RR )
12856adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  A  e.  RR+ )
129128rpge0d 10394 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  A )
13027rpge0d 10394 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  1 )
131127, 28, 129, 130addge0d 9348 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  ( A  +  1 ) )
13230rpge0d 10394 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  x )
13359, 4, 131, 132mulge0d 9349 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <_  ( ( A  + 
1 )  x.  x
) )
134133adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( ( A  +  1 )  x.  x ) )
13511nnred 9761 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
136135lep1d 9688 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  <_  ( n  +  1 ) )
13775, 77, 99, 134, 136lediv2ad 10412 . . . . . . . . . . . . . . . . 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 8973 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  <_  ( (
( A  +  1 )  x.  x )  /  n ) )
13999recnd 8861 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( A  +  1 )  x.  x )  e.  CC )
14011nnne0d 9790 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0 )
141139, 115, 140divrecd 9539 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( A  +  1 )  x.  x )  /  n )  =  ( ( ( A  +  1 )  x.  x )  x.  (
1  /  n ) ) )
142138, 141breqtrd 4047 . . . . . . . . . . . . . . 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 12257 . . . . . . . . . . . . . 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 8861 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( A  +  1 )  x.  x )  e.  CC )
145115, 140reccld 9529 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  /  n )  e.  CC )
1468, 144, 145fsummulc2 12246 . . . . . . . . . . . . . 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 4049 . . . . . . . . . . . . 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 20303 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  RR  /\  1  <_  x )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n )  <_  ( ( log `  x )  +  1 ) )
1494, 29, 148syl2anc 642 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 1  /  n
)  <_  ( ( log `  x )  +  1 ) )
15093, 89, 91, 133, 149lemul2ad 9697 . . . . . . . . . . . . 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 8973 . . . . . . . . . . . 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 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( A  +  1 )  e.  CC )
15389recnd 8861 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  +  1 )  e.  CC )
154152, 19, 153mul32d 9022 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( A  + 
1 )  x.  x
)  x.  ( ( log `  x )  +  1 ) )  =  ( ( ( A  +  1 )  x.  ( ( log `  x )  +  1 ) )  x.  x
) )
155151, 154breqtrd 4047 . . . . . . . . . . 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 10440 . . . . . . . . . . 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 223 . . . . . . . . . 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 10444 . . . . . . . . 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 9567 . . . . . . . . 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 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  CC )
16124, 160addcld 8854 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  +  1 )  e.  CC )
162152, 161, 24, 32divassd 9571 . . . . . . . . . 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 9574 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( log `  x
)  +  1 )  /  ( log `  x
) )  =  ( ( ( log `  x
)  /  ( log `  x ) )  +  ( 1  /  ( log `  x ) ) ) )
16424, 32dividd 9534 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  /  ( log `  x ) )  =  1 )
165164oveq1d 5873 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( log `  x
)  /  ( log `  x ) )  +  ( 1  /  ( log `  x ) ) )  =  ( 1  +  ( 1  / 
( log `  x
) ) ) )
166163, 165eqtr2d 2316 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  +  ( 1  /  ( log `  x
) ) )  =  ( ( ( log `  x )  +  1 )  /  ( log `  x ) ) )
167166oveq2d 5874 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( A  +  1 )  x.  ( 1  +  ( 1  / 
( log `  x
) ) ) )  =  ( ( A  +  1 )  x.  ( ( ( log `  x )  +  1 )  /  ( log `  x ) ) ) )
168162, 167eqtr4d 2318 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( A  + 
1 )  x.  (
( log `  x
)  +  1 ) )  /  ( log `  x ) )  =  ( ( A  + 
1 )  x.  (
1  +  ( 1  /  ( log `  x
) ) ) ) )
169158, 159, 1683brtr3d 4052 . . . . . . . 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 11897 . . . . . . . 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 8973 . . . . . . 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 4043 . . . . . 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 697 . . . . 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 12126 . . . 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 12097 . . 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 2357 . 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 8862 . . 3  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  +  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) ) )  e.  RR )
178177, 36rerpdivcld 10417 . 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 20712 . . . . . . . . . . 11  |-  R : RR+
--> RR
181180ffvelrni 5664 . . . . . . . . . 10  |-  ( ( x  /  ( n  +  1 ) )  e.  RR+  ->  ( R `
 ( x  / 
( n  +  1 ) ) )  e.  RR )
182104, 181syl 15 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  (
n  +  1 ) ) )  e.  RR )
183182recnd 8861 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  (
n  +  1 ) ) )  e.  CC )
18478, 75rpdivcld 10407 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
185180ffvelrni 5664 . . . . . . . . . 10  |-  ( ( x  /  n )  e.  RR+  ->  ( R `
 ( x  /  n ) )  e.  RR )
186184, 185syl 15 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  RR )
187186recnd 8861 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  e.  CC )
188183, 187subcld 9157 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( R `  ( x  /  ( n  + 
1 ) ) )  -  ( R `  ( x  /  n
) ) )  e.  CC )
189188abscld 11918 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( R `  ( x  /  (
n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) )  e.  RR )
190135, 189remulcld 8863 . . . . 5  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  x.  ( abs `  (
( R `  (
x  /  ( n  +  1 ) ) )  -  ( R `
 ( x  /  n ) ) ) ) )  e.  RR )
1918, 190fsumrecl 12207 . . . 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 10417 . . 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 8861 . 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 10394 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  n )
195188absge0d 11926 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( abs `  ( ( R `  ( x  /  ( n  + 
1 ) ) )  -  ( R `  ( x  /  n
) ) ) ) )
196135, 189, 194, 195mulge0d 9349 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( n  x.  ( abs `  ( ( R `  ( x  /  (
n  +  1 ) ) )  -  ( R `  ( x  /  n ) ) ) ) ) )
1978, 190, 196fsumge0 12253 . . . . . 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 10426 . . . . 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 11905 . . . 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 8854 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  +  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (ψ `  (
x  /  ( n  +  1 ) ) )  +  ( x  /  ( n  + 
1 ) ) ) )  e.  CC )
201200, 25, 33divcld 9536 . . . . . 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 11918 . . . . 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 9794 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
204 chpcl 20362 . . . . . . . . . . . 12  |-  ( ( x  /  n )  e.  RR  ->  (ψ `  ( x  /  n
) )  e.  RR )
205203, 204syl 15 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  n ) )  e.  RR )
206205, 203readdcld 8862 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) )  e.  RR )
207206, 16resubcld 9211 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(ψ `  ( x  /  n ) )  +  ( x  /  n
) )  -  (
(ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )  e.  RR )
208135, 207remulcld 8863 . . . . . . . 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 20711 . . . . . . . . . . . . . . 15  |-  ( ( x  /  ( n  +  1 ) )  e.  RR+  ->  ( R `
 ( x  / 
( n  +  1 ) ) )  =  ( (ψ `  (
x  /  ( n  +  1 ) ) )  -  ( x  /  ( n  + 
1 ) ) ) )
210104, 209syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  (
n  +  1 ) ) )  =  ( (ψ `  ( x  /  ( n  + 
1 ) ) )  -  ( x  / 
( n  +  1 ) ) ) )
211179pntrval 20711 . . . . . . . . . . . . . . 15  |-  ( ( x  /  n )  e.  RR+  ->  ( R `
 ( x  /  n ) )  =  ( (ψ `  (
x  /  n ) )  -  ( x  /  n ) ) )
212184, 211syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( R `  ( x  /  n
) )  =  ( (ψ `  ( x  /  n ) )  -  ( x  /  n
) ) )
213210, 212oveq12d 5876 . . . . . . . . . . . . 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 8861 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  ( n  +  1 ) ) )  e.  CC )
215205recnd 8861 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  n ) )  e.  CC )
216114, 115, 140divcld 9536 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  CC )
217214, 121, 215, 216sub4d 9206 . . . . . . . . . . . . 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 2315 . . . . . . . . . . . 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 5529 . . . . . . . . . . 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 9157 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  -  (ψ `  ( x  /  n
) ) )  e.  CC )
221121, 216subcld 9157 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
x  /  ( n  +  1 ) )  -  ( x  /  n ) )  e.  CC )
222220, 221abs2dif2d 11940 . . . . . . . . . . 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 4043 . . . . . . . . . 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 10412 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  ( n  + 
1 ) )  <_ 
( x  /  n
) )
225 chpwordi 20395 . . . . . . . . . . . . . 14  |-  ( ( ( x  /  (
n  +  1 ) )  e.  RR  /\  ( x  /  n
)  e.  RR  /\  ( x  /  (
n  +  1 ) )  <_  ( x  /  n ) )  -> 
(ψ `  ( x  /  ( n  + 
1 ) ) )  <_  (ψ `  (
x  /  n ) ) )
22613, 203, 224, 225syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  ( n  +  1 ) ) )  <_  (ψ `  (
x  /  n ) ) )
22715, 205, 226abssuble0d 11915 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( (ψ `  (
x  /  ( n  +  1 ) ) )  -  (ψ `  ( x  /  n
) ) ) )  =  ( (ψ `  ( x  /  n
) )  -  (ψ `  ( x  /  (
n  +  1 ) ) ) ) )
22813, 203, 224abssuble0d 11915 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( x  / 
( n  +  1 ) )  -  (
x  /  n ) ) )  =  ( ( x  /  n
)  -  ( x  /  ( n  + 
1 ) ) ) )
229227, 228oveq12d 5876 . . . . . . . . . . 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 9204 . . . . . . . . . . 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 2318 . . . . . . . . . 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 4047 . . . . . . . . 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 9697 . . . . . . . 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 12257 . . . . . . 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 8861 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(ψ `  ( x  /  n ) )  +  ( x  /  n
) )  -  (
(ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )  e.  CC )
236115, 235mulcld 8855 . . . . . . . . 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 12206 . . . . . . . 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 9171 . . . . . . . . . 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 10397 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  e.  RR  /\  0  <_  x ) )
240 flge0nn0 10948 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  0  <_  x )  -> 
( |_ `  x
)  e.  NN0 )
241 nn0p1nn 10003 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( |_ `  x )  e.  NN0  ->  ( ( |_ `  x )  +  1 )  e.  NN )
242239, 240, 2413syl 18 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  NN )
2434, 242nndivred 9794 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  RR )
244 2re 9815 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
245244a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  RR )
246 flltp1 10932 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  x  <  ( ( |_ `  x )  +  1 ) )
2474, 246syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  <  ( ( |_ `  x )  +  1 ) )
248242nncnd 9762 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  CC )
249248mulid1d 8852 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  1 )  =  ( ( |_
`  x )  +  1 ) )
250247, 249breqtrrd 4049 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  <  ( ( ( |_
`  x )  +  1 )  x.  1 ) )
251242nnrpd 10389 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  RR+ )
2524, 28, 251ltdivmuld 10437 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( x  /  (
( |_ `  x
)  +  1 ) )  <  1  <->  x  <  ( ( ( |_
`  x )  +  1 )  x.  1 ) ) )
253250, 252mpbird 223 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  <  1 )
254 1lt2 9886 . . . . . . . . . . . . . . . . . . . 20  |-  1  <  2
255254a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <  2 )
256243, 28, 245, 253, 255lttrd 8977 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  <  2 )
257 chpeq0 20447 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  /  ( ( |_ `  x )  +  1 ) )  e.  RR  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  0  <->  ( x  /  ( ( |_
`  x )  +  1 ) )  <  2 ) )
258243, 257syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  0  <->  ( x  /  ( ( |_
`  x )  +  1 ) )  <  2 ) )
259256, 258mpbird 223 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  =  0 )
260259oveq1d 5873 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) )  =  ( 0  +  ( x  /  ( ( |_ `  x )  +  1 ) ) ) )
261243recnd 8861 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  /  ( ( |_ `  x )  +  1 ) )  e.  CC )
262261addid2d 9013 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
0  +  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  ( x  / 
( ( |_ `  x )  +  1 ) ) )
263260, 262eqtrd 2315 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) )  =  ( x  /  (
( |_ `  x
)  +  1 ) ) )
264263oveq2d 5874 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  ( (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  +  ( x  /  ( ( |_ `  x )  +  1 ) ) ) )  =  ( ( ( |_ `  x )  +  1 )  x.  ( x  /  ( ( |_
`  x )  +  1 ) ) ) )
265242nnne0d 9790 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( |_ `  x
)  +  1 )  =/=  0 )
26619, 248, 265divcan2d 9538 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  ( x  /  ( ( |_
`  x )  +  1 ) ) )  =  x )
267264, 266eqtrd 2315 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( |_ `  x )  +  1 )  x.  ( (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) )  +  ( x  /  ( ( |_ `  x )  +  1 ) ) ) )  =  x )
26819div1d 9528 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  /  1 )  =  x )
269268fveq2d 5529 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (ψ `  ( x  /  1
) )  =  (ψ `  x ) )
270269, 268oveq12d 5876 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  ( x  /  1 ) )  +  ( x  / 
1 ) )  =  ( (ψ `  x
)  +  x ) )
271270oveq2d 5874 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  x.  ( (ψ `  ( x  /  1
) )  +  ( x  /  1 ) ) )  =  ( 1  x.  ( (ψ `  x )  +  x
) ) )
2726, 4readdcld 8862 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  +  x )  e.  RR )
273272recnd 8861 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
(ψ `  x )  +  x )  e.  CC )
274273mulid2d 8853 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  x.  ( (ψ `  x )  +  x
) )  =  ( (ψ `  x )  +  x ) )
275271, 274eqtrd 2315 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  x.  ( (ψ `  ( x  /  1
) )  +  ( x  /  1 ) ) )  =  ( (ψ `  x )  +  x ) )
276267, 275oveq12d 5876 . . . . . . . . . . . 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 9173 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  -u (
( (ψ `  x
)  +  x )  -  x )  =  ( x  -  (
(ψ `  x )  +  x ) ) )
2787, 19pncand 9158 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( (ψ `  x
)  +  x )  -  x )  =  (ψ `  x )
)
279278negeqd 9046 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  -u (
( (ψ `  x
)  +  x )  -  x )  = 
-u (ψ `  x
) )
280276, 277, 2793eqtr2d 2321 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( |_
`  x )  +  1 )  x.  (
(ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) ) )  -  ( 1  x.  ( (ψ `  (
x  /  1 ) )  +  ( x  /  1 ) ) ) )  =  -u (ψ `  x ) )
2814flcld 10930 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( |_ `  x )  e.  ZZ )
282 fzval3 10911 . . . . . . . . . . . . . 14  |-  ( ( |_ `  x )  e.  ZZ  ->  (
1 ... ( |_ `  x ) )  =  ( 1..^ ( ( |_ `  x )  +  1 ) ) )
283281, 282syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1 ... ( |_ `  x ) )  =  ( 1..^ ( ( |_ `  x )  +  1 ) ) )
284283eqcomd 2288 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1..^ ( ( |_
`  x )  +  1 ) )  =  ( 1 ... ( |_ `  x ) ) )
285115, 116pncan2d 9159 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
n  +  1 )  -  n )  =  1 )
286285oveq1d 5873 . . . . . . . . . . . . 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 8861 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  e.  CC )
288287mulid2d 8853 . . . . . . . . . . . . 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 2315 . . . . . . . . . . . 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 12180 . . . . . . . . . . 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 5876 . . . . . . . . . 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 5866 . . . . . . . . . . . . . . 15  |-  ( m  =  n  ->  (
x  /  m )  =  ( x  /  n ) )
293292fveq2d 5529 . . . . . . . . . . . . . 14  |-  ( m  =  n  ->  (ψ `  ( x  /  m
) )  =  (ψ `  ( x  /  n
) ) )
294293, 292oveq12d 5876 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  n ) )  +  ( x  /  n
) ) )
295294ancli 534 . . . . . . . . . . . 12  |-  ( m  =  n  ->  (
m  =  n  /\  ( (ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  n ) )  +  ( x  /  n
) ) ) )
296 oveq2 5866 . . . . . . . . . . . . . . 15  |-  ( m  =  ( n  + 
1 )  ->  (
x  /  m )  =  ( x  / 
( n  +  1 ) ) )
297296fveq2d 5529 . . . . . . . . . . . . . 14  |-  ( m  =  ( n  + 
1 )  ->  (ψ `  ( x  /  m
) )  =  (ψ `  ( x  /  (
n  +  1 ) ) ) )
298297, 296oveq12d 5876 . . . . . . . . . . . . 13  |-  ( m  =  ( n  + 
1 )  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) )
299298ancli 534 . . . . . . . . . . . 12  |-  ( m  =  ( n  + 
1 )  ->  (
m  =  ( n  +  1 )  /\  ( (ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  ( n  + 
1 ) ) )  +  ( x  / 
( n  +  1 ) ) ) ) )
300 oveq2 5866 . . . . . . . . . . . . . . 15  |-  ( m  =  1  ->  (
x  /  m )  =  ( x  / 
1 ) )
301300fveq2d 5529 . . . . . . . . . . . . . 14  |-  ( m  =  1  ->  (ψ `  ( x  /  m
) )  =  (ψ `  ( x  /  1
) ) )
302301, 300oveq12d 5876 . . . . . . . . . . . . 13  |-  ( m  =  1  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  1 ) )  +  ( x  / 
1 ) ) )
303302ancli 534 . . . . . . . . . . . 12  |-  ( m  =  1  ->  (
m  =  1  /\  ( (ψ `  (
x  /  m ) )  +  ( x  /  m ) )  =  ( (ψ `  ( x  /  1
) )  +  ( x  /  1 ) ) ) )
304 oveq2 5866 . . . . . . . . . . . . . . 15  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
x  /  m )  =  ( x  / 
( ( |_ `  x )  +  1 ) ) )
305304fveq2d 5529 . . . . . . . . . . . . . 14  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (ψ `  ( x  /  m
) )  =  (ψ `  ( x  /  (
( |_ `  x
)  +  1 ) ) ) )
306305, 304oveq12d 5876 . . . . . . . . . . . . 13  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) ) )
307306ancli 534 . . . . . . . . . . . 12  |-  ( m  =  ( ( |_
`  x )  +  1 )  ->  (
m  =  ( ( |_ `  x )  +  1 )  /\  ( (ψ `  ( x  /  m ) )  +  ( x  /  m
) )  =  ( (ψ `  ( x  /  ( ( |_
`  x )  +  1 ) ) )  +  ( x  / 
( ( |_ `  x )  +  1 ) ) ) ) )
308 nnuz 10263 . . . . . . . . . . . . 13  |-  NN  =  ( ZZ>= `  1 )
309242, 308syl6eleq 2373 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( |_ `  x
)  +  1 )  e.  ( ZZ>= `  1
) )
310 elfznn 10819 . . . . . . . . . . . . . 14  |-  ( m  e.  ( 1 ... ( ( |_ `  x )  +  1 ) )  ->  m  e.  NN )
311310adantl 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  NN )
312311nncnd 9762 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  m  e.  CC )
3134adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  x  e.  RR )
314313, 311nndivred 9794 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
x  /  m )  e.  RR )
315 chpcl 20362 . . . . . . . . . . . . . . 15  |-  ( ( x  /  m )  e.  RR  ->  (ψ `  ( x  /  m
) )  e.  RR )
316314, 315syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (ψ `  ( x  /  m
) )  e.  RR )
317316, 314readdcld 8862 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  e.  RR )
318317recnd 8861 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... (
( |_ `  x
)  +  1 ) ) )  ->  (
(ψ `  ( x  /  m ) )  +  ( x  /  m
) )  e.  CC )
319295, 299, 303, 307, 309, 312, 318fsumparts 12264 . . . . . . . . . . 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 8854 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  n
) )  +  ( x  /  n ) )  e.  CC )
321214, 121addcld 8854 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  (
n  +  1 ) ) )  +  ( x  /  ( n  +  1 ) ) )  e.  CC )
322320, 321negsubdi2d 9173 . . . . . . . . . . . . . 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 5874 . . . . . . . . . . . . 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 9233 . . . . . . . . . . . . 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 2317 . . . . . . . . . . . 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 12180 . . . . . . . . . . 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 2317 . . . . . . . . . 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 ) ) )