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

Theorem selberg4lem1 20671
Description: Lemma for selberg4 20672. Equation 10.4.20 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
Hypotheses
Ref Expression
selberg4lem1.1  |-  ( ph  ->  A  e.  RR+ )
selberg4lem1.2  |-  ( ph  ->  A. y  e.  ( 1 [,)  +oo )
( abs `  (
( sum_ i  e.  ( 1 ... ( |_
`  y ) ) ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
y  /  i ) ) ) )  / 
y )  -  (
2  x.  ( log `  y ) ) ) )  <_  A )
Assertion
Ref Expression
selberg4lem1  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  ( x  x.  ( log `  x
) ) )  -  ( log `  x ) ) )  e.  O
( 1 ) )
Distinct variable groups:    i, m, n, x, y, A    ph, m, n, x
Allowed substitution hints:    ph( y, i)

Proof of Theorem selberg4lem1
StepHypRef Expression
1 2cn 9784 . . . . . . 7  |-  2  e.  CC
21a1i 12 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  CC )
3 fzfid 11001 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
4 elfznn 10785 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
54adantl 454 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
6 vmacl 20318 . . . . . . . . . . . 12  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
75, 6syl 17 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  RR )
87, 5nndivred 9762 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  RR )
9 elioore 10652 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 (,) 
+oo )  ->  x  e.  RR )
109adantl 454 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR )
11 1rp 10325 . . . . . . . . . . . . . . 15  |-  1  e.  RR+
1211a1i 12 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR+ )
1312rpred 10357 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR )
14 eliooord 10676 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( 1 (,) 
+oo )  ->  (
1  <  x  /\  x  <  +oo ) )
1514adantl 454 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  <  x  /\  x  <  +oo ) )
1615simpld 447 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <  x )
1713, 10, 16ltled 8935 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <_  x )
1810, 12, 17rpgecld 10392 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR+ )
1918adantr 453 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
205nnrpd 10356 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
2119, 20rpdivcld 10374 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
2221relogcld 19936 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  RR )
238, 22remulcld 8831 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) )  e.  RR )
243, 23fsumrecl 12172 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  e.  RR )
2510, 16rplogcld 19942 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR+ )
2624, 25rerpdivcld 10384 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  e.  RR )
2726recnd 8829 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  e.  CC )
2818relogcld 19936 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR )
2928rehalfcld 9925 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  /  2 )  e.  RR )
3029recnd 8829 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  /  2 )  e.  CC )
312, 27, 30subdid 9203 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  -  ( ( log `  x )  /  2
) ) )  =  ( ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) ) )  -  ( 2  x.  ( ( log `  x )  /  2
) ) ) )
3228recnd 8829 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  CC )
33 2ne0 9797 . . . . . . . 8  |-  2  =/=  0
3433a1i 12 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  =/=  0 )
3532, 2, 34divcan2d 9506 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( ( log `  x )  /  2 ) )  =  ( log `  x
) )
3635oveq2d 5808 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) ) )  -  ( 2  x.  ( ( log `  x )  /  2
) ) )  =  ( ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) ) )  -  ( log `  x ) ) )
3731, 36eqtrd 2290 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  -  ( ( log `  x )  /  2
) ) )  =  ( ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) ) )  -  ( log `  x ) ) )
3837mpteq2dva 4080 . . 3  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 2  x.  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  -  ( ( log `  x )  /  2
) ) ) )  =  ( x  e.  ( 1 (,)  +oo )  |->  ( ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) ) )  -  ( log `  x ) ) ) )
39 2re 9783 . . . . 5  |-  2  e.  RR
4039a1i 12 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  RR )
4126, 29resubcld 9179 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  -  ( ( log `  x )  /  2
) )  e.  RR )
42 ioossre 10678 . . . . . 6  |-  ( 1 (,)  +oo )  C_  RR
43 o1const 12058 . . . . . 6  |-  ( ( ( 1 (,)  +oo )  C_  RR  /\  2  e.  CC )  ->  (
x  e.  ( 1 (,)  +oo )  |->  2 )  e.  O ( 1 ) )
4442, 1, 43mp2an 656 . . . . 5  |-  ( x  e.  ( 1 (,) 
+oo )  |->  2 )  e.  O ( 1 )
4544a1i 12 . . . 4  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  2 )  e.  O
( 1 ) )
46 vmalogdivsum2 20649 . . . . 5  |-  ( x  e.  ( 1 (,) 
+oo )  |->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  -  ( ( log `  x )  /  2
) ) )  e.  O ( 1 )
4746a1i 12 . . . 4  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  -  ( ( log `  x )  /  2
) ) )  e.  O ( 1 ) )
4840, 41, 45, 47o1mul2 12063 . . 3  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 2  x.  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  -  ( ( log `  x )  /  2
) ) ) )  e.  O ( 1 ) )
4938, 48eqeltrrd 2333 . 2  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) ) )  -  ( log `  x ) ) )  e.  O ( 1 ) )
50 fzfid 11001 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  ( x  /  n
) ) )  e. 
Fin )
51 elfznn 10785 . . . . . . . . . . . 12  |-  ( m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) )  ->  m  e.  NN )
5251adantl 454 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  m  e.  NN )
53 vmacl 20318 . . . . . . . . . . 11  |-  ( m  e.  NN  ->  (Λ `  m )  e.  RR )
5452, 53syl 17 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  (Λ `  m
)  e.  RR )
5552nnrpd 10356 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  m  e.  RR+ )
5655relogcld 19936 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( log `  m )  e.  RR )
5710adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
5857, 5nndivred 9762 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
5958adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( x  /  n )  e.  RR )
6059, 52nndivred 9762 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (
x  /  n )  /  m )  e.  RR )
61 chpcl 20324 . . . . . . . . . . . 12  |-  ( ( ( x  /  n
)  /  m )  e.  RR  ->  (ψ `  ( ( x  /  n )  /  m
) )  e.  RR )
6260, 61syl 17 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  (ψ `  (
( x  /  n
)  /  m ) )  e.  RR )
6356, 62readdcld 8830 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( ( log `  m )  +  (ψ `  ( (
x  /  n )  /  m ) ) )  e.  RR )
6454, 63remulcld 8831 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  e.  RR )
6550, 64fsumrecl 12172 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  e.  RR )
667, 65remulcld 8831 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )  e.  RR )
673, 66fsumrecl 12172 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  e.  RR )
6818, 25rpmulcld 10373 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
x  x.  ( log `  x ) )  e.  RR+ )
6967, 68rerpdivcld 10384 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  ( x  x.  ( log `  x
) ) )  e.  RR )
7069, 28resubcld 9179 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  ( x  x.  ( log `  x
) ) )  -  ( log `  x ) )  e.  RR )
7170recnd 8829 . . 3  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  ( x  x.  ( log `  x
) ) )  -  ( log `  x ) )  e.  CC )
7224recnd 8829 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  e.  CC )
7325rpne0d 10362 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  =/=  0 )
7472, 32, 73divcld 9504 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  e.  CC )
752, 74mulcld 8823 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) )  /  ( log `  x
) ) )  e.  CC )
7675, 32subcld 9125 . . 3  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) ) )  -  ( log `  x ) )  e.  CC )
7769recnd 8829 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  ( x  x.  ( log `  x
) ) )  e.  CC )
7877, 75, 32nnncan2d 9160 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  ( x  x.  ( log `  x
) ) )  -  ( log `  x ) )  -  ( ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) )  /  ( log `  x
) ) )  -  ( log `  x ) ) )  =  ( ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  ( x  x.  ( log `  x
) ) )  -  ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) ) ) ) )
7967recnd 8829 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  e.  CC )
8010recnd 8829 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  CC )
8118rpne0d 10362 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  =/=  0 )
8279, 80, 32, 81, 73divdiv1d 9535 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  x )  / 
( log `  x
) )  =  (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  ( x  x.  ( log `  x
) ) ) )
832, 72, 32, 73divassd 9539 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) ) )  /  ( log `  x ) )  =  ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) ) ) )
8482, 83oveq12d 5810 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  x )  / 
( log `  x
) )  -  (
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) ) )  /  ( log `  x ) ) )  =  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )  /  ( x  x.  ( log `  x
) ) )  -  ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) ) ) ) )
8567, 18rerpdivcld 10384 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  x )  e.  RR )
8685recnd 8829 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  x )  e.  CC )
872, 72mulcld 8823 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) ) )  e.  CC )
8886, 87, 32, 73divsubdird 9543 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  x )  -  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) ) ) )  /  ( log `  x ) )  =  ( ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  x )  / 
( log `  x
) )  -  (
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) ) )  /  ( log `  x ) ) ) )
8981adantr 453 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  =/=  0 )
9066, 57, 89redivcld 9556 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  x. 
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )  /  x )  e.  RR )
9190recnd 8829 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  x. 
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )  /  x )  e.  CC )
9239a1i 12 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  RR )
9392, 23remulcld 8831 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( (Λ `  n )  /  n
)  x.  ( log `  ( x  /  n
) ) ) )  e.  RR )
9493recnd 8829 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( (Λ `  n )  /  n
)  x.  ( log `  ( x  /  n
) ) ) )  e.  CC )
953, 91, 94fsumsub 12215 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )  /  x )  -  ( 2  x.  ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  x )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 2  x.  ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) ) ) ) )
967recnd 8829 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  CC )
9765, 57, 89redivcld 9556 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  e.  RR )
9897recnd 8829 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  e.  CC )
991a1i 12 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  CC )
10022recnd 8829 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  CC )
1015nncnd 9730 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
1025nnne0d 9758 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0 )
103100, 101, 102divcld 9504 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  /  n )  e.  CC )
10499, 103mulcld 8823 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( log `  ( x  /  n
) )  /  n
) )  e.  CC )
10596, 98, 104subdid 9203 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  -  (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) ) ) )  =  ( ( (Λ `  n
)  x.  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x ) )  -  ( (Λ `  n
)  x.  ( 2  x.  ( ( log `  ( x  /  n
) )  /  n
) ) ) ) )
10665recnd 8829 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  e.  CC )
10780adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  CC )
10896, 106, 107, 89divassd 9539 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  x. 
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )  /  x )  =  ( (Λ `  n
)  x.  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x ) ) )
10996, 101, 100, 102div32d 9527 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) )  =  ( (Λ `  n
)  x.  ( ( log `  ( x  /  n ) )  /  n ) ) )
110109oveq2d 5808 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( (Λ `  n )  /  n
)  x.  ( log `  ( x  /  n
) ) ) )  =  ( 2  x.  ( (Λ `  n
)  x.  ( ( log `  ( x  /  n ) )  /  n ) ) ) )
11199, 96, 103mul12d 8989 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( (Λ `  n
)  x.  ( ( log `  ( x  /  n ) )  /  n ) ) )  =  ( (Λ `  n )  x.  (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) ) ) )
112110, 111eqtrd 2290 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( (Λ `  n )  /  n
)  x.  ( log `  ( x  /  n
) ) ) )  =  ( (Λ `  n
)  x.  ( 2  x.  ( ( log `  ( x  /  n
) )  /  n
) ) ) )
113108, 112oveq12d 5810 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  x )  -  ( 2  x.  (
( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) ) ) )  =  ( ( (Λ `  n
)  x.  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x ) )  -  ( (Λ `  n
)  x.  ( 2  x.  ( ( log `  ( x  /  n
) )  /  n
) ) ) ) )
114105, 113eqtr4d 2293 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  -  (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) ) ) )  =  ( ( ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  x )  -  ( 2  x.  (
( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) ) ) ) )
115114sumeq2dv 12141 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  -  ( 2  x.  (
( log `  (
x  /  n ) )  /  n ) ) ) )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  x )  -  ( 2  x.  (
( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) ) ) ) )
11666recnd 8829 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )  e.  CC )
1173, 80, 116, 81fsumdivc 12213 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  x )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  x ) )
11823recnd 8829 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) )  e.  CC )
1193, 2, 118fsummulc2 12211 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) ) )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( 2  x.  ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) ) ) )
120117, 119oveq12d 5810 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  x )  -  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) ) ) )  =  (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  x )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( 2  x.  ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) ) ) ) )
12195, 115, 1203eqtr4rd 2301 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  x )  -  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) ) ) )  =  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  -  (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) ) ) ) )
122121oveq1d 5807 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  x )  -  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) ) ) )  /  ( log `  x ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  -  ( 2  x.  (
( log `  (
x  /  n ) )  /  n ) ) ) )  / 
( log `  x
) ) )
12388, 122eqtr3d 2292 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  x )  / 
( log `  x
) )  -  (
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) ) )  /  ( log `  x ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  -  ( 2  x.  (
( log `  (
x  /  n ) )  /  n ) ) ) )  / 
( log `  x
) ) )
12478, 84, 1233eqtr2d 2296 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )  /  ( x  x.  ( log `  x
) ) )  -  ( log `  x ) )  -  ( ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) )  /  ( log `  x
) ) )  -  ( log `  x ) ) )  =  (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  -  (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) ) ) )  /  ( log `  x ) ) )
125124mpteq2dva 4080 . . . 4  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )  /  ( x  x.  ( log `  x
) ) )  -  ( log `  x ) )  -  ( ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) )  /  ( log `  x
) ) )  -  ( log `  x ) ) ) )  =  ( x  e.  ( 1 (,)  +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  -  ( 2  x.  (
( log `  (
x  /  n ) )  /  n ) ) ) )  / 
( log `  x
) ) ) )
126 1re 8805 . . . . . 6  |-  1  e.  RR
127126a1i 12 . . . . 5  |-  ( ph  ->  1  e.  RR )
128 selberg4lem1.1 . . . . . . . 8  |-  ( ph  ->  A  e.  RR+ )
129128adantr 453 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  A  e.  RR+ )
130129rpred 10357 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  A  e.  RR )
1313, 8fsumrecl 12172 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  e.  RR )
132131, 25rerpdivcld 10384 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  /  ( log `  x ) )  e.  RR )
133128rpcnd 10359 . . . . . . 7  |-  ( ph  ->  A  e.  CC )
134 o1const 12058 . . . . . . 7  |-  ( ( ( 1 (,)  +oo )  C_  RR  /\  A  e.  CC )  ->  (
x  e.  ( 1 (,)  +oo )  |->  A )  e.  O ( 1 ) )
13542, 133, 134sylancr 647 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  A )  e.  O
( 1 ) )
136127recnd 8829 . . . . . . . 8  |-  ( ph  ->  1  e.  CC )
137 o1const 12058 . . . . . . . 8  |-  ( ( ( 1 (,)  +oo )  C_  RR  /\  1  e.  CC )  ->  (
x  e.  ( 1 (,)  +oo )  |->  1 )  e.  O ( 1 ) )
13842, 136, 137sylancr 647 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  1 )  e.  O
( 1 ) )
139132recnd 8829 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  /  ( log `  x ) )  e.  CC )
14013recnd 8829 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  CC )
141131recnd 8829 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  e.  CC )
142141, 32, 32, 73divsubdird 9543 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) )  /  ( log `  x ) )  =  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  /  ( log `  x ) )  -  ( ( log `  x
)  /  ( log `  x ) ) ) )
143141, 32subcld 9125 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  -  ( log `  x ) )  e.  CC )
144143, 32, 73divrecd 9507 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) )  /  ( log `  x ) )  =  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  -  ( log `  x ) )  x.  ( 1  /  ( log `  x ) ) ) )
14532, 73dividd 9502 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  /  ( log `  x ) )  =  1 )
146145oveq2d 5808 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  /  ( log `  x
) )  -  (
( log `  x
)  /  ( log `  x ) ) )  =  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  /  ( log `  x ) )  - 
1 ) )
147142, 144, 1463eqtr3d 2298 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) )  x.  (
1  /  ( log `  x ) ) )  =  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  /  ( log `  x ) )  - 
1 ) )
148147mpteq2dva 4080 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) )  x.  (
1  /  ( log `  x ) ) ) )  =  ( x  e.  ( 1 (,) 
+oo )  |->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  /  ( log `  x ) )  -  1 ) ) )
149131, 28resubcld 9179 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  -  ( log `  x ) )  e.  RR )
15013, 25rerpdivcld 10384 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1  /  ( log `  x ) )  e.  RR )
15118ex 425 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  ->  x  e.  RR+ )
)
152151ssrdv 3160 . . . . . . . . . . 11  |-  ( ph  ->  ( 1 (,)  +oo )  C_  RR+ )
153 vmadivsum 20593 . . . . . . . . . . . 12  |-  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  -  ( log `  x ) ) )  e.  O ( 1 )
154153a1i 12 . . . . . . . . . . 11  |-  ( ph  ->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) ) )  e.  O ( 1 ) )
155152, 154o1res2 12002 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) ) )  e.  O ( 1 ) )
156 divlogrlim 19944 . . . . . . . . . . 11  |-  ( x  e.  ( 1 (,) 
+oo )  |->  ( 1  /  ( log `  x
) ) )  ~~> r  0
157 rlimo1 12055 . . . . . . . . . . 11  |-  ( ( x  e.  ( 1 (,)  +oo )  |->  ( 1  /  ( log `  x
) ) )  ~~> r  0  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  / 
( log `  x
) ) )  e.  O ( 1 ) )
158156, 157mp1i 13 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  O ( 1 ) )
159149, 150, 155, 158o1mul2 12063 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) )  x.  (
1  /  ( log `  x ) ) ) )  e.  O ( 1 ) )
160148, 159eqeltrrd 2333 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  /  ( log `  x
) )  -  1 ) )  e.  O
( 1 ) )
161139, 140, 160o1dif 12068 . . . . . . 7  |-  ( ph  ->  ( ( x  e.  ( 1 (,)  +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  /  ( log `  x
) ) )  e.  O ( 1 )  <-> 
( x  e.  ( 1 (,)  +oo )  |->  1 )  e.  O
( 1 ) ) )
162138, 161mpbird 225 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  /  ( log `  x
) ) )  e.  O ( 1 ) )
163130, 132, 135, 162o1mul2 12063 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( A  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  /  ( log `  x ) ) ) )  e.  O
( 1 ) )
164130, 132remulcld 8831 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( A  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  /  ( log `  x ) ) )  e.  RR )
16522, 5nndivred 9762 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  /  n )  e.  RR )
16692, 165remulcld 8831 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( log `  ( x  /  n
) )  /  n
) )  e.  RR )
16797, 166resubcld 9179 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  -  ( 2  x.  (
( log `  (
x  /  n ) )  /  n ) ) )  e.  RR )
1687, 167remulcld 8831 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  -  (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) ) ) )  e.  RR )
1693, 168fsumrecl 12172 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  -  ( 2  x.  (
( log `  (
x  /  n ) )  /  n ) ) ) )  e.  RR )
170169, 25rerpdivcld 10384 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  -  (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) ) ) )  /  ( log `  x ) )  e.  RR )
171170recnd 8829 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  -  (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) ) ) )  /  ( log `  x ) )  e.  CC )
172169recnd 8829 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  -  ( 2  x.  (
( log `  (
x  /  n ) )  /  n ) ) ) )  e.  CC )
173172abscld 11883 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( abs `  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  -  ( 2  x.  (
( log `  (
x  /  n ) )  /  n ) ) ) ) )  e.  RR )
174130, 131remulcld 8831 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( A  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n ) )  e.  RR )
17598, 104subcld 9125 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  -  ( 2  x.  (
( log `  (
x  /  n ) )  /  n ) ) )  e.  CC )
17696, 175mulcld 8823 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  -  (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) ) ) )  e.  CC )
177176abscld 11883 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( (Λ `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  -  ( 2  x.  (
( log `  (
x  /  n ) )  /  n ) ) ) ) )  e.  RR )
1783, 177fsumrecl 12172 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  (
(Λ `  n )  x.  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  -  (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) ) ) ) )  e.  RR )
179168recnd 8829 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  -  (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) ) ) )  e.  CC )
1803, 179fsumabs 12224 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( abs `  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  -  ( 2  x.  (
( log `  (
x  /  n ) )  /  n ) ) ) ) )  <_  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( abs `  (
(Λ `  n )  x.  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  -  (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) ) ) ) ) )
181130adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A  e.  RR )
182181, 8remulcld 8831 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( A  x.  ( (Λ `  n
)  /  n ) )  e.  RR )
183175abscld 11883 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  -  (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) ) ) )  e.  RR )
184181, 5nndivred 9762 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( A  /  n )  e.  RR )
185 vmage0 20321 . . . . . . . . . . . . . . 15  |-  ( n  e.  NN  ->  0  <_  (Λ `  n )
)
1865, 185syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (Λ `  n ) )
187106, 107, 101, 89, 102divdiv2d 9536 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  ( x  /  n ) )  =  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  x.  n )  /  x
) )
188106, 101, 107, 89div23d 9541 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  x.  n )  /  x )  =  ( ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  x.  n
) )
189187, 188eqtrd 2290 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  ( x  /  n ) )  =  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  x.  n
) )
19099, 103, 101mulassd 8826 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) )  x.  n )  =  ( 2  x.  (
( ( log `  (
x  /  n ) )  /  n )  x.  n ) ) )
191100, 101, 102divcan1d 9505 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) )  /  n )  x.  n )  =  ( log `  (
x  /  n ) ) )
192191oveq2d 5808 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( ( log `  ( x  /  n ) )  /  n )  x.  n ) )  =  ( 2  x.  ( log `  ( x  /  n ) ) ) )
193190, 192eqtr2d 2291 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( log `  (
x  /  n ) ) )  =  ( ( 2  x.  (
( log `  (
x  /  n ) )  /  n ) )  x.  n ) )
194189, 193oveq12d 5810 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  ( x  /  n ) )  -  ( 2  x.  ( log `  ( x  /  n ) ) ) )  =  ( ( ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  x.  n
)  -  ( ( 2  x.  ( ( log `  ( x  /  n ) )  /  n ) )  x.  n ) ) )
19598, 104, 101subdird 9204 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  -  (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) ) )  x.  n )  =  ( ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  x.  n )  -  (
( 2  x.  (
( log `  (
x  /  n ) )  /  n ) )  x.  n ) ) )
196194, 195eqtr4d 2293 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  ( x  /  n ) )  -  ( 2  x.  ( log `  ( x  /  n ) ) ) )  =  ( ( ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  -  (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) ) )  x.  n ) )
197196fveq2d 5462 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  / 
( x  /  n
) )  -  (
2  x.  ( log `  ( x  /  n
) ) ) ) )  =  ( abs `  ( ( ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  -  ( 2  x.  (
( log `  (
x  /  n ) )  /  n ) ) )  x.  n
) ) )
198175, 101absmuld 11901 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  -  ( 2  x.  (
( log `  (
x  /  n ) )  /  n ) ) )  x.  n
) )  =  ( ( abs `  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  -  (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) ) ) )  x.  ( abs `  n ) ) )
1995nnred 9729 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
20020rpge0d 10361 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  n )
201199, 200absidd 11870 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  n )  =  n )
202201oveq2d 5808 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  -  ( 2  x.  (
( log `  (
x  /  n ) )  /  n ) ) ) )  x.  ( abs `  n
) )  =  ( ( abs `  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  /  x )  -  (
2  x.  ( ( log `  ( x  /  n ) )  /  n ) ) ) )  x.  n
) )
203197, 198, 2023eqtrd 2294 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  / 
( x  /  n
) )  -  (
2  x.  ( log `  ( x  /  n
) ) ) ) )  =  ( ( abs `  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  x )  -  ( 2  x.  (
( log `  (
x  /  n ) )  /  n ) ) ) )  x.  n ) )
204101mulid2d 8821 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  =  n )
205 fznnfl 10932 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  (
n  e.  ( 1 ... ( |_ `  x ) )  <->  ( n  e.  NN  /\  n  <_  x ) ) )
20610, 205syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
n  e.  ( 1 ... ( |_ `  x ) )  <->  ( n  e.  NN  /\  n  <_  x ) ) )
207206simplbda 610 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  <_  x )
208204, 207eqbrtrd 4017 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  <_  x )
209126a1i 12 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
210209, 57, 20lemuldivd 10402 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  x.  n )  <_  x  <->  1  <_  ( x  /  n ) ) )
211208, 210mpbid 203 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  ( x  /  n ) )
212 elicopnf 10705 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  e.  RR  ->  (
( x  /  n
)  e.  ( 1 [,)  +oo )  <->  ( (
x  /  n )  e.  RR  /\  1  <_  ( x  /  n
) ) ) )
213126, 212ax-mp 10 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  /  n )  e.  ( 1 [,) 
+oo )  <->  ( (
x  /  n )  e.  RR  /\  1  <_  ( x  /  n
) ) )
21458, 211, 213sylanbrc 648 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  ( 1 [,)  +oo )
)
215 selberg4lem1.2 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A. y  e.  ( 1 [,)  +oo )
( abs `  (
( sum_ i  e.  ( 1 ... ( |_
`  y ) ) ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
y  /  i ) ) ) )  / 
y )  -  (
2  x.  ( log `  y ) ) ) )  <_  A )
216215ad2antrr 709 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A. y  e.  ( 1 [,)  +oo ) ( abs `  (
( sum_ i  e.  ( 1 ... ( |_
`  y ) ) ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
y  /  i ) ) ) )  / 
y )  -  (
2  x.  ( log `  y ) ) ) )  <_  A )
217 fveq2 5458 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  =  m  ->  (Λ `  i )  =  (Λ `  m ) )
218 fveq2 5458 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  =  m  ->  ( log `  i )  =  ( log `  m
) )
219 oveq2 5800 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  =  m  ->  (
y  /  i )  =  ( y  /  m ) )
220219fveq2d 5462 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  =  m  ->  (ψ `  ( y  /  i
) )  =  (ψ `  ( y  /  m
) ) )
221218, 220oveq12d 5810 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  =  m  ->  (
( log `  i
)  +  (ψ `  ( y  /  i
) ) )  =  ( ( log `  m
)  +  (ψ `  ( y  /  m
) ) ) )
222217, 221oveq12d 5810 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  =  m  ->  (
(Λ `  i )  x.  ( ( log `  i
)  +  (ψ `  ( y  /  i
) ) ) )  =  ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
y  /  m ) ) ) ) )
223222cbvsumv 12134 . . . . . . . . . . . . . . . . . . . . . . 23  |-  sum_ i  e.  ( 1 ... ( |_ `  y ) ) ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
y  /  i ) ) ) )  = 
sum_ m  e.  (
1 ... ( |_ `  y ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( y  /  m
) ) ) )
224 fveq2 5458 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( x  /  n )  ->  ( |_ `  y )  =  ( |_ `  (
x  /  n ) ) )
225224oveq2d 5808 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( x  /  n )  ->  (
1 ... ( |_ `  y ) )  =  ( 1 ... ( |_ `  ( x  /  n ) ) ) )
226 oveq1 5799 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  =  ( x  /  n )  ->  (
y  /  m )  =  ( ( x  /  n )  /  m ) )
227226fveq2d 5462 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  =  ( x  /  n )  ->  (ψ `  ( y  /  m
) )  =  (ψ `  ( ( x  /  n )  /  m
) ) )
228227oveq2d 5808 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  ( x  /  n )  ->  (
( log `  m
)  +  (ψ `  ( y  /  m
) ) )  =  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )
229228oveq2d 5808 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( x  /  n )  ->  (
(Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( y  /  m
) ) ) )  =  ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )
230229adantr 453 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( y  =  ( x  /  n )  /\  m  e.  ( 1 ... ( |_ `  y ) ) )  ->  ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
y  /  m ) ) ) )  =  ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )
231225, 230sumeq12dv 12144 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( x  /  n )  ->  sum_ m  e.  ( 1 ... ( |_ `  y ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
y  /  m ) ) ) )  = 
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )
232223, 231syl5eq 2302 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x  /  n )  ->  sum_ i  e.  ( 1 ... ( |_ `  y ) ) ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
y  /  i ) ) ) )  = 
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) ) )
233 id 21 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x  /  n )  ->  y  =  ( x  /  n ) )
234232, 233oveq12d 5810 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( x  /  n )  ->  ( sum_ i  e.  ( 1 ... ( |_ `  y ) ) ( (Λ `  i )  x.  ( ( log `  i
)  +  (ψ `  ( y  /  i
) ) ) )  /  y )  =  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  / 
( x  /  n
) ) )
235 fveq2 5458 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x  /  n )  ->  ( log `  y )  =  ( log `  (
x  /  n ) ) )
236235oveq2d 5808 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( x  /  n )  ->  (
2  x.  ( log `  y ) )  =  ( 2  x.  ( log `  ( x  /  n ) ) ) )
237234, 236oveq12d 5810 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( x  /  n )  ->  (
( sum_ i  e.  ( 1 ... ( |_
`  y ) ) ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
y  /  i ) ) ) )  / 
y )  -  (
2  x.  ( log `  y ) ) )  =  ( ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  (
( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  ( x  /  n ) )  -  ( 2  x.  ( log `  ( x  /  n ) ) ) ) )
238237fveq2d 5462 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  ( x  /  n )  ->  ( abs `  ( ( sum_ i  e.  ( 1 ... ( |_ `  y ) ) ( (Λ `  i )  x.  ( ( log `  i
)  +  (ψ `  ( y  /  i
) ) ) )  /  y )  -  ( 2  x.  ( log `  y ) ) ) )  =  ( abs `  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  ( x  /  n ) )  -  ( 2  x.  ( log `  ( x  /  n ) ) ) ) ) )
239238breq1d 4007 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( x  /  n )  ->  (
( abs `  (
( sum_ i  e.  ( 1 ... ( |_
`  y ) ) ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
y  /  i ) ) ) )  / 
y )  -  (
2  x.  ( log `  y ) ) ) )  <_  A  <->  ( abs `  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  / 
( x  /  n
) )  -  (
2  x.  ( log `  ( x  /  n
) ) ) ) )  <_  A )
)
240239rcla4v 2855 . . . . . . . . . . . . . . . . 17  |-  ( ( x  /  n )  e.  ( 1 [,) 
+oo )  ->  ( A. y  e.  (
1 [,)  +oo ) ( abs `  ( (
sum_ i  e.  ( 1 ... ( |_
`  y ) ) ( (Λ `  i
)  x.  ( ( log `  i )  +  (ψ `  (
y  /  i ) ) ) )  / 
y )  -  (
2  x.  ( log `  y ) ) ) )  <_  A  ->  ( abs `  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )  /  ( x  /  n ) )  -  ( 2  x.  ( log `  ( x  /  n ) ) ) ) )  <_  A
) )
241214, 216, 240sylc 58 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) )  / 
( x  /  n
) )  -  (
2  x.  ( log `  ( x  /  n
) ) ) ) )  <_  A )
242203, 241eqbrtrrd 4019 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_