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

Theorem selberg4lem1 22768
Description: Lemma for selberg4 22769. 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 2cnd 10390 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  2  e.  CC )
2 fzfid 11791 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
3 elfznn 11474 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
43adantl 463 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
5 vmacl 22415 . . . . . . . . . . . 12  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
64, 5syl 16 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  RR )
76, 4nndivred 10366 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  RR )
8 elioore 11326 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( 1 (,) +oo )  ->  x  e.  RR )
98adantl 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  RR )
10 1rp 10991 . . . . . . . . . . . . . . 15  |-  1  e.  RR+
1110a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  RR+ )
12 1red 9397 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  RR )
13 eliooord 11351 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( 1 (,) +oo )  ->  ( 1  <  x  /\  x  < +oo ) )
1413adantl 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  <  x  /\  x  < +oo ) )
1514simpld 456 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <  x )
1612, 9, 15ltled 9518 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  <_  x )
179, 11, 16rpgecld 11058 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  RR+ )
1817adantr 462 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
194nnrpd 11022 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
2018, 19rpdivcld 11040 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
2120relogcld 22031 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  RR )
227, 21remulcld 9410 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) )  e.  RR )
232, 22fsumrecl 13207 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  e.  RR )
249, 15rplogcld 22037 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  RR+ )
2523, 24rerpdivcld 11050 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  e.  RR )
2625recnd 9408 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  e.  CC )
2717relogcld 22031 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  RR )
2827rehalfcld 10567 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( log `  x
)  /  2 )  e.  RR )
2928recnd 9408 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( log `  x
)  /  2 )  e.  CC )
301, 26, 29subdid 9796 . . . . 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
) ) ) )
3127recnd 9408 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  e.  CC )
32 2ne0 10410 . . . . . . . 8  |-  2  =/=  0
3332a1i 11 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  2  =/=  0 )
3431, 1, 33divcan2d 10105 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  ( ( log `  x )  /  2 ) )  =  ( log `  x
) )
3534oveq2d 6106 . . . . 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 ) ) )
3630, 35eqtrd 2473 . . . 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 ) ) )
3736mpteq2dva 4375 . . 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 ) ) ) )
38 2re 10387 . . . . 5  |-  2  e.  RR
3938a1i 11 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  2  e.  RR )
4025, 28resubcld 9772 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  -  ( ( log `  x )  /  2
) )  e.  RR )
41 ioossre 11353 . . . . . 6  |-  ( 1 (,) +oo )  C_  RR
42 2cn 10388 . . . . . 6  |-  2  e.  CC
43 o1const 13093 . . . . . 6  |-  ( ( ( 1 (,) +oo )  C_  RR  /\  2  e.  CC )  ->  (
x  e.  ( 1 (,) +oo )  |->  2 )  e.  O(1) )
4441, 42, 43mp2an 667 . . . . 5  |-  ( x  e.  ( 1 (,) +oo )  |->  2 )  e.  O(1)
4544a1i 11 . . . 4  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  2 )  e.  O(1) )
46 vmalogdivsum2 22746 . . . . 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 11 . . . 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) )
4839, 40, 45, 47o1mul2 13098 . . 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) )
4937, 48eqeltrrd 2516 . 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 11791 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  ( x  /  n
) ) )  e. 
Fin )
51 elfznn 11474 . . . . . . . . . . . 12  |-  ( m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) )  ->  m  e.  NN )
5251adantl 463 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) )  ->  m  e.  NN )
53 vmacl 22415 . . . . . . . . . . 11  |-  ( m  e.  NN  ->  (Λ `  m )  e.  RR )
5452, 53syl 16 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) )  ->  (Λ `  m
)  e.  RR )
5552nnrpd 11022 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) )  ->  m  e.  RR+ )
5655relogcld 22031 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) )  ->  ( log `  m )  e.  RR )
579adantr 462 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
5857, 4nndivred 10366 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
5958adantr 462 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) )  ->  ( x  /  n )  e.  RR )
6059, 52nndivred 10366 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) )  ->  ( (
x  /  n )  /  m )  e.  RR )
61 chpcl 22421 . . . . . . . . . . . 12  |-  ( ( ( x  /  n
)  /  m )  e.  RR  ->  (ψ `  ( ( x  /  n )  /  m
) )  e.  RR )
6260, 61syl 16 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) )  ->  (ψ `  (
( x  /  n
)  /  m ) )  e.  RR )
6356, 62readdcld 9409 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_
`  x ) ) )  /\  m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) )  ->  ( ( log `  m )  +  (ψ `  ( (
x  /  n )  /  m ) ) )  e.  RR )
6454, 63remulcld 9410 . . . . . . . . 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 13207 . . . . . . . 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 )
666, 65remulcld 9410 . . . . . . 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 )
672, 66fsumrecl 13207 . . . . . 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 )
6817, 24rpmulcld 11039 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
x  x.  ( log `  x ) )  e.  RR+ )
6967, 68rerpdivcld 11050 . . . . 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, 27resubcld 9772 . . . 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 9408 . . 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 )
7223recnd 9408 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  e.  CC )
7324rpne0d 11028 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( log `  x )  =/=  0 )
7472, 31, 73divcld 10103 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) )  /  ( log `  x ) )  e.  CC )
751, 74mulcld 9402 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) )  /  ( log `  x
) ) )  e.  CC )
7675, 31subcld 9715 . . 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 9408 . . . . . . 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, 31nnncan2d 9750 . . . . . 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 9408 . . . . . . . 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 )
809recnd 9408 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  e.  CC )
8117rpne0d 11028 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  x  =/=  0 )
8279, 80, 31, 81, 73divdiv1d 10134 . . . . . . 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
) ) ) )
831, 72, 31, 73divassd 10138 . . . . . . 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 6108 . . . . . 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, 17rerpdivcld 11050 . . . . . . . . 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 9408 . . . . . . . 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 )
871, 72mulcld 9402 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( log `  (
x  /  n ) ) ) )  e.  CC )
8886, 87, 31, 73divsubdird 10142 . . . . . . 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 462 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  =/=  0 )
9066, 57, 89redivcld 10155 . . . . . . . . . . 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 9408 . . . . . . . . . 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 )
9238a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  RR )
9392, 22remulcld 9410 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( (Λ `  n )  /  n
)  x.  ( log `  ( x  /  n
) ) ) )  e.  RR )
9493recnd 9408 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( (Λ `  n )  /  n
)  x.  ( log `  ( x  /  n
) ) ) )  e.  CC )
952, 91, 94fsumsub 13251 . . . . . . . . 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 ) ) ) ) ) )
966recnd 9408 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  CC )
9765, 57, 89redivcld 10155 . . . . . . . . . . . . 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 9408 . . . . . . . . . . . 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 )
99 2cnd 10390 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  2  e.  CC )
10021recnd 9408 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  CC )
1014nncnd 10334 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
1024nnne0d 10362 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0 )
103100, 101, 102divcld 10103 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  /  n )  e.  CC )
10499, 103mulcld 9402 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( log `  ( x  /  n
) )  /  n
) )  e.  CC )
10596, 98, 104subdid 9796 . . . . . . . . . . 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 9408 . . . . . . . . . . . . 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 462 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  CC )
10896, 106, 107, 89divassd 10138 . . . . . . . . . . . 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 10126 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) )  =  ( (Λ `  n
)  x.  ( ( log `  ( x  /  n ) )  /  n ) ) )
110109oveq2d 6106 . . . . . . . . . . . . 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 9574 . . . . . . . . . . . . 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 2473 . . . . . . . . . . . 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 6108 . . . . . . . . . . 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 2476 . . . . . . . . . 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 13176 . . . . . . . . 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 9408 . . . . . . . . . . 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 )
1172, 80, 116, 81fsumdivc 13249 . . . . . . . . . 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 ) )
11822recnd 9408 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  x.  ( log `  ( x  /  n ) ) )  e.  CC )
1192, 1, 118fsummulc2 13247 . . . . . . . . . 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 6108 . . . . . . . . 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 2484 . . . . . . . 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 6105 . . . . . . 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 2475 . . . . . 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 2479 . . . . 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 4375 . . . 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 1red 9397 . . . . 5  |-  ( ph  ->  1  e.  RR )
127 selberg4lem1.1 . . . . . . . 8  |-  ( ph  ->  A  e.  RR+ )
128127adantr 462 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  A  e.  RR+ )
129128rpred 11023 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  A  e.  RR )
1302, 7fsumrecl 13207 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  e.  RR )
131130, 24rerpdivcld 11050 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  /  ( log `  x ) )  e.  RR )
132127rpcnd 11025 . . . . . . 7  |-  ( ph  ->  A  e.  CC )
133 o1const 13093 . . . . . . 7  |-  ( ( ( 1 (,) +oo )  C_  RR  /\  A  e.  CC )  ->  (
x  e.  ( 1 (,) +oo )  |->  A )  e.  O(1) )
13441, 132, 133sylancr 658 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  A )  e.  O(1) )
135 1cnd 9398 . . . . . . . 8  |-  ( ph  ->  1  e.  CC )
136 o1const 13093 . . . . . . . 8  |-  ( ( ( 1 (,) +oo )  C_  RR  /\  1  e.  CC )  ->  (
x  e.  ( 1 (,) +oo )  |->  1 )  e.  O(1) )
13741, 135, 136sylancr 658 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  1 )  e.  O(1) )
138131recnd 9408 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  /  ( log `  x ) )  e.  CC )
139 1cnd 9398 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  1  e.  CC )
140130recnd 9408 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  e.  CC )
141140, 31, 31, 73divsubdird 10142 . . . . . . . . . . 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 ) ) ) )
142140, 31subcld 9715 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  -  ( log `  x ) )  e.  CC )
143142, 31, 73divrecd 10106 . . . . . . . . . . 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 ) ) ) )
14431, 73dividd 10101 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
( log `  x
)  /  ( log `  x ) )  =  1 )
145144oveq2d 6106 . . . . . . . . . . 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 ) )
146141, 143, 1453eqtr3d 2481 . . . . . . . . . 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 ) )
147146mpteq2dva 4375 . . . . . . . . 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 ) ) )
148130, 27resubcld 9772 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  -  ( log `  x ) )  e.  RR )
14912, 24rerpdivcld 11050 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
1  /  ( log `  x ) )  e.  RR )
15017ex 434 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  ->  x  e.  RR+ )
)
151150ssrdv 3359 . . . . . . . . . . 11  |-  ( ph  ->  ( 1 (,) +oo )  C_  RR+ )
152 vmadivsum 22690 . . . . . . . . . . . 12  |-  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  -  ( log `  x ) ) )  e.  O(1)
153152a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) ) )  e.  O(1) )
154151, 153o1res2 13037 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) ) )  e.  O(1) )
155 divlogrlim 22039 . . . . . . . . . . 11  |-  ( x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x
) ) )  ~~> r  0
156 rlimo1 13090 . . . . . . . . . . 11  |-  ( ( x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x ) ) )  ~~> r  0  ->  (
x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  O(1) )
157155, 156mp1i 12 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( 1  /  ( log `  x ) ) )  e.  O(1) )
158148, 149, 154, 157o1mul2 13098 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) )  x.  (
1  /  ( log `  x ) ) ) )  e.  O(1) )
159147, 158eqeltrrd 2516 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  /  ( log `  x
) )  -  1 ) )  e.  O(1) )
160138, 139, 159o1dif 13103 . . . . . . 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) ) )
161137, 160mpbird 232 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  /  ( log `  x
) ) )  e.  O(1) )
162129, 131, 134, 161o1mul2 13098 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,) +oo )  |->  ( A  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  /  ( log `  x ) ) ) )  e.  O(1) )
163129, 131remulcld 9410 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( A  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  /  ( log `  x ) ) )  e.  RR )
16421, 4nndivred 10366 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( log `  ( x  /  n ) )  /  n )  e.  RR )
16592, 164remulcld 9410 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( log `  ( x  /  n
) )  /  n
) )  e.  RR )
16697, 165resubcld 9772 . . . . . . . . 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 )
1676, 166remulcld 9410 . . . . . . . 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 )
1682, 167fsumrecl 13207 . . . . . . 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 )
169168, 24rerpdivcld 11050 . . . . . 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 )
170169recnd 9408 . . . . 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 )
171168recnd 9408 . . . . . . . . . 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 )
172171abscld 12918 . . . . . . . . 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 )
173129, 130remulcld 9410 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  ( A  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n ) )  e.  RR )
17498, 104subcld 9715 . . . . . . . . . . . . 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 )
17596, 174mulcld 9402 . . . . . . . . . . . 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 )
176175abscld 12918 . . . . . . . . . . 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 )
1772, 176fsumrecl 13207 . . . . . . . . . 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 )
178167recnd 9408 . . . . . . . . . . 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 )
1792, 178fsumabs 13260 . . . . . . . . . 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 ) ) ) ) ) )
180129adantr 462 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A  e.  RR )
181180, 7remulcld 9410 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( A  x.  ( (Λ `  n
)  /  n ) )  e.  RR )
182174abscld 12918 . . . . . . . . . . . . . 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 )
183180, 4nndivred 10366 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( A  /  n )  e.  RR )
184 vmage0 22418 . . . . . . . . . . . . . . 15  |-  ( n  e.  NN  ->  0  <_  (Λ `  n )
)
1854, 184syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (Λ `  n ) )
186106, 107, 101, 89, 102divdiv2d 10135 . . . . . . . . . . . . . . . . . . . . 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
) )
187106, 101, 107, 89div23d 10140 . . . . . . . . . . . . . . . . . . . . 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
) )
188186, 187eqtrd 2473 . . . . . . . . . . . . . . . . . . . 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
) )
18999, 103, 101mulassd 9405 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
190100, 101, 102divcan1d 10104 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( log `  (
x  /  n ) )  /  n )  x.  n )  =  ( log `  (
x  /  n ) ) )
191190oveq2d 6106 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( ( ( log `  ( x  /  n ) )  /  n )  x.  n ) )  =  ( 2  x.  ( log `  ( x  /  n ) ) ) )
192189, 191eqtr2d 2474 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 2  x.  ( log `  (
x  /  n ) ) )  =  ( ( 2  x.  (
( log `  (
x  /  n ) )  /  n ) )  x.  n ) )
193188, 192oveq12d 6108 . . . . . . . . . . . . . . . . . . 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 ) ) )
19498, 104, 101subdird 9797 . . . . . . . . . . . . . . . . . . 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 ) ) )
195193, 194eqtr4d 2476 . . . . . . . . . . . . . . . . . 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 ) )
196195fveq2d 5692 . . . . . . . . . . . . . . . . 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
) ) )
197174, 101absmuld 12936 . . . . . . . . . . . . . . . . 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 ) ) )
1984nnred 10333 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
19919rpge0d 11027 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  n )
200198, 199absidd 12905 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  n )  =  n )
201200oveq2d 6106 . . . . . . . . . . . . . . . . 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
) )
202196, 197, 2013eqtrd 2477 . . . . . . . . . . . . . . . 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 ) )
203101mulid2d 9400 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  =  n )
204 fznnfl 11697 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  (
n  e.  ( 1 ... ( |_ `  x ) )  <->  ( n  e.  NN  /\  n  <_  x ) ) )
2059, 204syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,) +oo ) )  ->  (
n  e.  ( 1 ... ( |_ `  x ) )  <->  ( n  e.  NN  /\  n  <_  x ) ) )
206205simplbda 621 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  <_  x )
207203, 206eqbrtrd 4309 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  <_  x )
208 1red 9397 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
209208, 57, 19lemuldivd 11068 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  x.  n )  <_  x  <->  1  <_  ( x  /  n ) ) )
210207, 209mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  ( x  /  n ) )
211 1re 9381 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  RR
212 elicopnf 11381 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  e.  RR  ->  (
( x  /  n
)  e.  ( 1 [,) +oo )  <->  ( (
x  /  n )  e.  RR  /\  1  <_  ( x  /  n
) ) ) )
213211, 212ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  /  n )  e.  ( 1 [,) +oo )  <->  ( ( x  /  n )  e.  RR  /\  1  <_ 
( x  /  n
) ) )
21458, 210, 213sylanbrc 659 . . . . . . . . . . . . . . . . 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 720 . . . . . . . . . . . . . . . . 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 5688 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  =  m  ->  (Λ `  i )  =  (Λ `  m ) )
218 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  =  m  ->  ( log `  i )  =  ( log `  m
) )
219 oveq2 6098 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  =  m  ->  (
y  /  i )  =  ( y  /  m ) )
220219fveq2d 5692 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  =  m  ->  (ψ `  ( y  /  i
) )  =  (ψ `  ( y  /  m
) ) )
221218, 220oveq12d 6108 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  =  m  ->  (
( log `  i
)  +  (ψ `  ( y  /  i
) ) )  =  ( ( log `  m
)  +  (ψ `  ( y  /  m
) ) ) )
222217, 221oveq12d 6108 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  =  m  ->  (
(Λ `  i )  x.  ( ( log `  i
)  +  (ψ `  ( y  /  i
) ) ) )  =  ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
y  /  m ) ) ) ) )
223222cbvsumv 13169 . . . . . . . . . . . . . . . . . . . . . . 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 5688 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( x  /  n )  ->  ( |_ `  y )  =  ( |_ `  (
x  /  n ) ) )
225224oveq2d 6106 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( x  /  n )  ->  (
1 ... ( |_ `  y ) )  =  ( 1 ... ( |_ `  ( x  /  n ) ) ) )
226 oveq1 6097 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  =  ( x  /  n )  ->  (
y  /  m )  =  ( ( x  /  n )  /  m ) )
227226fveq2d 5692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  =  ( x  /  n )  ->  (ψ `  ( y  /  m
) )  =  (ψ `  ( ( x  /  n )  /  m
) ) )
228227oveq2d 6106 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  ( x  /  n )  ->  (
( log `  m
)  +  (ψ `  ( y  /  m
) ) )  =  ( ( log `  m
)  +  (ψ `  ( ( x  /  n )  /  m
) ) ) )
229228oveq2d 6106 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( x  /  n )  ->  (
(Λ `  m )  x.  ( ( log `  m
)  +  (ψ `  ( y  /  m
) ) ) )  =  ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )
230229adantr 462 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( y  =  ( x  /  n )  /\  m  e.  ( 1 ... ( |_ `  y ) ) )  ->  ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
y  /  m ) ) ) )  =  ( (Λ `  m
)  x.  ( ( log `  m )  +  (ψ `  (
( x  /  n
)  /  m ) ) ) ) )
231225, 230sumeq12dv 13179 . . . . . . . . . . . . . . . . . . . . . . 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 2485 . . . . . . . . . . . . . . . . . . . . . 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 22 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x  /  n )  ->  y  =  ( x  /  n ) )
234232, 233oveq12d 6108 . . . . . . . . . . . . . . . . . . . . 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 5688 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x  /  n )  ->  ( log `  y )  =  ( log `  (
x  /  n ) ) )
236235oveq2d 6106 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( x  /  n )  ->  (
2  x.  ( log `  y ) )  =  ( 2  x.  ( log `  ( x  /  n ) ) ) )
237234, 236oveq12d 6108 . . . . . . . . . . . . . . . . . . . 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 5692 . . . . . . . . . . . . . . . . . . 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 4299 . . . . . . . . . . . . . . . . . 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 )
)
240239rspcv 3066 . . . . . . . . . . . . . . . . 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 60 . . . . . . . . . . . . . . . 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 )
242202, 241eqbrtrrd 4311 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,) +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) )