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

Theorem selberg3lem1 20700
Description: Introduce a log weighting on the summands of  sum_ m  x.  n  <_  x , Λ ( m )Λ ( n ), the core of selberg2 20694 (written here as  sum_ n  <_  x , Λ ( n )ψ (
x  /  n )). Equation 10.4.21 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
Hypotheses
Ref Expression
selberg3lem1.1  |-  ( ph  ->  A  e.  RR+ )
selberg3lem1.2  |-  ( ph  ->  A. y  e.  ( 1 [,)  +oo )
( abs `  (
( sum_ k  e.  ( 1 ... ( |_
`  y ) ) ( (Λ `  k
)  x.  ( log `  k ) )  -  ( (ψ `  y )  x.  ( log `  y
) ) )  / 
y ) )  <_  A )
Assertion
Ref Expression
selberg3lem1  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( ( ( 2  /  ( log `  x ) )  x. 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  n
) ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) ) )  /  x ) )  e.  O ( 1 ) )
Distinct variable groups:    k, n, x, y, A    ph, n, x
Dummy variable  m is distinct from all other variables.
Allowed substitution hints:    ph( y, k)

Proof of Theorem selberg3lem1
StepHypRef Expression
1 1re 8832 . . 3  |-  1  e.  RR
21a1i 12 . 2  |-  ( ph  ->  1  e.  RR )
3 ioossre 10706 . . . 4  |-  ( 1 (,)  +oo )  C_  RR
4 selberg3lem1.1 . . . . 5  |-  ( ph  ->  A  e.  RR+ )
54rpcnd 10387 . . . 4  |-  ( ph  ->  A  e.  CC )
6 o1const 12087 . . . 4  |-  ( ( ( 1 (,)  +oo )  C_  RR  /\  A  e.  CC )  ->  (
x  e.  ( 1 (,)  +oo )  |->  A )  e.  O ( 1 ) )
73, 5, 6sylancr 646 . . 3  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  A )  e.  O
( 1 ) )
8 fzfid 11029 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
9 elfznn 10813 . . . . . . . . . 10  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
109adantl 454 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
11 vmacl 20350 . . . . . . . . 9  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
1210, 11syl 17 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  RR )
1312, 10nndivred 9789 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  RR )
148, 13fsumrecl 12201 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  e.  RR )
15 elioore 10680 . . . . . . . . 9  |-  ( x  e.  ( 1 (,) 
+oo )  ->  x  e.  RR )
16 eliooord 10704 . . . . . . . . . 10  |-  ( x  e.  ( 1 (,) 
+oo )  ->  (
1  <  x  /\  x  <  +oo ) )
1716simpld 447 . . . . . . . . 9  |-  ( x  e.  ( 1 (,) 
+oo )  ->  1  <  x )
1815, 17rplogcld 19974 . . . . . . . 8  |-  ( x  e.  ( 1 (,) 
+oo )  ->  ( log `  x )  e.  RR+ )
19 rpdivcl 10371 . . . . . . . 8  |-  ( ( A  e.  RR+  /\  ( log `  x )  e.  RR+ )  ->  ( A  /  ( log `  x
) )  e.  RR+ )
204, 18, 19syl2an 465 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( A  /  ( log `  x
) )  e.  RR+ )
2120rpred 10385 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( A  /  ( log `  x
) )  e.  RR )
2214, 21remulcld 8858 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  x.  ( A  /  ( log `  x
) ) )  e.  RR )
2322recnd 8856 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  x.  ( A  /  ( log `  x
) ) )  e.  CC )
245adantr 453 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  A  e.  CC )
2514recnd 8856 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  e.  CC )
2618adantl 454 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR+ )
2726rpcnd 10387 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  CC )
2820rpcnd 10387 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( A  /  ( log `  x
) )  e.  CC )
2925, 27, 28subdird 9231 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) )  x.  ( A  /  ( log `  x
) ) )  =  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  x.  ( A  / 
( log `  x
) ) )  -  ( ( log `  x
)  x.  ( A  /  ( log `  x
) ) ) ) )
3026rpne0d 10390 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  =/=  0 )
3124, 27, 30divcan2d 9533 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( log `  x
)  x.  ( A  /  ( log `  x
) ) )  =  A )
3231oveq2d 5835 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  x.  ( A  / 
( log `  x
) ) )  -  ( ( log `  x
)  x.  ( A  /  ( log `  x
) ) ) )  =  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  x.  ( A  /  ( log `  x
) ) )  -  A ) )
3329, 32eqtrd 2316 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) )  x.  ( A  /  ( log `  x
) ) )  =  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  x.  ( A  / 
( log `  x
) ) )  -  A ) )
3433mpteq2dva 4107 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) )  x.  ( A  /  ( log `  x
) ) ) )  =  ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  x.  ( A  /  ( log `  x
) ) )  -  A ) ) )
3526rpred 10385 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( log `  x )  e.  RR )
3614, 35resubcld 9206 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  -  ( log `  x ) )  e.  RR )
3715adantl 454 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR )
38 0re 8833 . . . . . . . . . . . 12  |-  0  e.  RR
3938a1i 12 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  e.  RR )
401a1i 12 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  e.  RR )
41 0lt1 9291 . . . . . . . . . . . 12  |-  0  <  1
4241a1i 12 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <  1 )
4317adantl 454 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  1  <  x )
4439, 40, 37, 42, 43lttrd 8972 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  0  <  x )
4537, 44elrpd 10383 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  RR+ )
4645ex 425 . . . . . . . 8  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  ->  x  e.  RR+ )
)
4746ssrdv 3186 . . . . . . 7  |-  ( ph  ->  ( 1 (,)  +oo )  C_  RR+ )
48 vmadivsum 20625 . . . . . . . 8  |-  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  -  ( log `  x ) ) )  e.  O ( 1 )
4948a1i 12 . . . . . . 7  |-  ( ph  ->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) ) )  e.  O ( 1 ) )
5047, 49o1res2 12031 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) ) )  e.  O ( 1 ) )
513a1i 12 . . . . . . 7  |-  ( ph  ->  ( 1 (,)  +oo )  C_  RR )
52 ere 12364 . . . . . . . 8  |-  _e  e.  RR
5352a1i 12 . . . . . . 7  |-  ( ph  ->  _e  e.  RR )
544rpred 10385 . . . . . . 7  |-  ( ph  ->  A  e.  RR )
5520adantrr 699 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  ( A  /  ( log `  x
) )  e.  RR+ )
5655rprege0d 10392 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  (
( A  /  ( log `  x ) )  e.  RR  /\  0  <_  ( A  /  ( log `  x ) ) ) )
57 absid 11775 . . . . . . . . 9  |-  ( ( ( A  /  ( log `  x ) )  e.  RR  /\  0  <_  ( A  /  ( log `  x ) ) )  ->  ( abs `  ( A  /  ( log `  x ) ) )  =  ( A  /  ( log `  x
) ) )
5856, 57syl 17 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  ( abs `  ( A  / 
( log `  x
) ) )  =  ( A  /  ( log `  x ) ) )
59 loge 19934 . . . . . . . . . . 11  |-  ( log `  _e )  =  1
60 simprr 735 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  _e  <_  x )
61 epr 12480 . . . . . . . . . . . . 13  |-  _e  e.  RR+
6245adantrr 699 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  x  e.  RR+ )
63 logleb 19951 . . . . . . . . . . . . 13  |-  ( ( _e  e.  RR+  /\  x  e.  RR+ )  ->  (
_e  <_  x  <->  ( log `  _e )  <_  ( log `  x ) ) )
6461, 62, 63sylancr 646 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  (
_e  <_  x  <->  ( log `  _e )  <_  ( log `  x ) ) )
6560, 64mpbid 203 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  ( log `  _e )  <_ 
( log `  x
) )
6659, 65syl5eqbrr 4058 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  1  <_  ( log `  x
) )
67 1rp 10353 . . . . . . . . . . . 12  |-  1  e.  RR+
68 rpregt0 10362 . . . . . . . . . . . 12  |-  ( 1  e.  RR+  ->  ( 1  e.  RR  /\  0  <  1 ) )
6967, 68mp1i 13 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  (
1  e.  RR  /\  0  <  1 ) )
7026adantrr 699 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  ( log `  x )  e.  RR+ )
7170rpregt0d 10391 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  (
( log `  x
)  e.  RR  /\  0  <  ( log `  x
) ) )
724adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  A  e.  RR+ )
7372rpregt0d 10391 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  ( A  e.  RR  /\  0  <  A ) )
74 lediv2 9641 . . . . . . . . . . 11  |-  ( ( ( 1  e.  RR  /\  0  <  1 )  /\  ( ( log `  x )  e.  RR  /\  0  <  ( log `  x ) )  /\  ( A  e.  RR  /\  0  <  A ) )  ->  ( 1  <_  ( log `  x
)  <->  ( A  / 
( log `  x
) )  <_  ( A  /  1 ) ) )
7569, 71, 73, 74syl3anc 1184 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  (
1  <_  ( log `  x )  <->  ( A  /  ( log `  x
) )  <_  ( A  /  1 ) ) )
7666, 75mpbid 203 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  ( A  /  ( log `  x
) )  <_  ( A  /  1 ) )
775adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  A  e.  CC )
7877div1d 9523 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  ( A  /  1 )  =  A )
7976, 78breqtrd 4048 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  ( A  /  ( log `  x
) )  <_  A
)
8058, 79eqbrtrd 4044 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  ( 1 (,)  +oo )  /\  _e  <_  x
) )  ->  ( abs `  ( A  / 
( log `  x
) ) )  <_  A )
8151, 28, 53, 54, 80elo1d 12004 . . . . . 6  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( A  /  ( log `  x ) ) )  e.  O ( 1 ) )
8236, 21, 50, 81o1mul2 12092 . . . . 5  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) )  x.  ( A  /  ( log `  x
) ) ) )  e.  O ( 1 ) )
8334, 82eqeltrrd 2359 . . . 4  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  x.  ( A  / 
( log `  x
) ) )  -  A ) )  e.  O ( 1 ) )
8423, 24, 83o1dif 12097 . . 3  |-  ( ph  ->  ( ( x  e.  ( 1 (,)  +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  x.  ( A  / 
( log `  x
) ) ) )  e.  O ( 1 )  <->  ( x  e.  ( 1 (,)  +oo )  |->  A )  e.  O ( 1 ) ) )
857, 84mpbird 225 . 2  |-  ( ph  ->  ( x  e.  ( 1 (,)  +oo )  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  x.  ( A  / 
( log `  x
) ) ) )  e.  O ( 1 ) )
86 2re 9810 . . . . . . 7  |-  2  e.  RR
87 rerpdivcl 10376 . . . . . . 7  |-  ( ( 2  e.  RR  /\  ( log `  x )  e.  RR+ )  ->  (
2  /  ( log `  x ) )  e.  RR )
8886, 26, 87sylancr 646 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  /  ( log `  x ) )  e.  RR )
89 nndivre 9776 . . . . . . . . . . 11  |-  ( ( x  e.  RR  /\  n  e.  NN )  ->  ( x  /  n
)  e.  RR )
9037, 9, 89syl2an 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR )
91 chpcl 20356 . . . . . . . . . 10  |-  ( ( x  /  n )  e.  RR  ->  (ψ `  ( x  /  n
) )  e.  RR )
9290, 91syl 17 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  n ) )  e.  RR )
9312, 92remulcld 8858 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  (ψ `  ( x  /  n
) ) )  e.  RR )
9410nnrpd 10384 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR+ )
9594relogcld 19968 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  RR )
9693, 95remulcld 8858 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  x.  ( log `  n
) )  e.  RR )
978, 96fsumrecl 12201 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  n
) )  e.  RR )
9888, 97remulcld 8858 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  n
) ) )  e.  RR )
998, 93fsumrecl 12201 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  e.  RR )
10098, 99resubcld 9206 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( 2  / 
( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  x.  ( log `  n
) ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) ) )  e.  RR )
101100, 45rerpdivcld 10412 . . 3  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  x.  ( log `  n
) ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) ) )  /  x )  e.  RR )
102101recnd 8856 . 2  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( ( ( 2  /  ( log `  x
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  x.  ( log `  n
) ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) ) )  /  x )  e.  CC )
103102abscld 11912 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( abs `  ( ( ( ( 2  /  ( log `  x ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  n
) ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) ) )  /  x ) )  e.  RR )
10423abscld 11912 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( abs `  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  x.  ( A  / 
( log `  x
) ) ) )  e.  RR )
105 2cn 9811 . . . . . . . . . . 11  |-  2  e.  CC
106105a1i 12 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  2  e.  CC )
10797recnd 8856 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  n
) )  e.  CC )
108106, 107mulcld 8850 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  n
) ) )  e.  CC )
10999recnd 8856 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  e.  CC )
110109, 27mulcld 8850 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  x.  ( log `  x
) )  e.  CC )
111108, 110subcld 9152 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  x.  ( log `  n
) ) )  -  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  x
) ) )  e.  CC )
112111abscld 11912 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( abs `  ( ( 2  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  n
) ) )  -  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  x
) ) ) )  e.  RR )
11344gt0ne0d 9332 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  =/=  0 )
114112, 37, 113redivcld 9583 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
( abs `  (
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  x.  ( log `  n
) ) )  -  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  x
) ) ) )  /  x )  e.  RR )
11554adantr 453 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  A  e.  RR )
11614, 115remulcld 8858 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  x.  A
)  e.  RR )
11712recnd 8856 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  CC )
118 fzfid 11029 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  ( x  /  n
) ) )  e. 
Fin )
119 elfznn 10813 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) )  ->  m  e.  NN )
120119adantl 454 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  m  e.  NN )
121 vmacl 20350 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  NN  ->  (Λ `  m )  e.  RR )
122120, 121syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  (Λ `  m
)  e.  RR )
123120nnrpd 10384 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  m  e.  RR+ )
124123relogcld 19968 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( log `  m )  e.  RR )
125122, 124remulcld 8858 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (Λ `  m )  x.  ( log `  m ) )  e.  RR )
126118, 125fsumrecl 12201 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  e.  RR )
1279nnrpd 10384 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  RR+ )
128 rpdivcl 10371 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  RR+  /\  n  e.  RR+ )  ->  (
x  /  n )  e.  RR+ )
12945, 127, 128syl2an 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  RR+ )
130129relogcld 19968 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  e.  RR )
13192, 130remulcld 8858 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  n
) )  x.  ( log `  ( x  /  n ) ) )  e.  RR )
132126, 131resubcld 9206 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n
) )  x.  ( log `  ( x  /  n ) ) ) )  e.  RR )
133132recnd 8856 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n
) )  x.  ( log `  ( x  /  n ) ) ) )  e.  CC )
134117, 133mulcld 8850 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) )  -  (
(ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) )  e.  CC )
1358, 134fsumcl 12200 . . . . . . . . . 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
) )  x.  ( log `  ( x  /  n ) ) ) ) )  e.  CC )
136135abscld 11912 . . . . . . . . 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
) )  x.  ( log `  ( x  /  n ) ) ) ) ) )  e.  RR )
137134abscld 11912 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( (Λ `  n
)  x.  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n
) )  x.  ( log `  ( x  /  n ) ) ) ) ) )  e.  RR )
1388, 137fsumrecl 12201 . . . . . . . . 9  |-  ( (
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 ) )  x.  ( log `  (
x  /  n ) ) ) ) ) )  e.  RR )
139115, 37remulcld 8858 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( A  x.  x )  e.  RR )
14014, 139remulcld 8858 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  x.  ( A  x.  x )
)  e.  RR )
1418, 134fsumabs 12253 . . . . . . . . 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
) )  x.  ( log `  ( x  /  n ) ) ) ) ) )  <_  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( (Λ `  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) )  -  (
(ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) ) ) )
14254ad2antrr 708 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A  e.  RR )
14337adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
144142, 143remulcld 8858 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( A  x.  x )  e.  RR )
14513, 144remulcld 8858 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  x.  ( A  x.  x )
)  e.  RR )
146133abscld 11912 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) )  e.  RR )
147144, 10nndivred 9789 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( A  x.  x )  /  n )  e.  RR )
148 vmage0 20353 . . . . . . . . . . . . . 14  |-  ( n  e.  NN  ->  0  <_  (Λ `  n )
)
14910, 148syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (Λ `  n ) )
15090recnd 8856 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  CC )
151129rpne0d 10390 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  =/=  0
)
152133, 150, 151absdivd 11931 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) )  / 
( x  /  n
) ) )  =  ( ( abs `  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) )  -  (
(ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) )  /  ( abs `  (
x  /  n ) ) ) )
153129rpge0d 10389 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( x  /  n ) )
15490, 153absidd 11899 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( x  /  n
) )  =  ( x  /  n ) )
155154oveq2d 5835 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) )  /  ( abs `  (
x  /  n ) ) )  =  ( ( abs `  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) )  -  (
(ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) )  /  ( x  /  n ) ) )
156152, 155eqtrd 2316 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) )  / 
( x  /  n
) ) )  =  ( ( abs `  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) )  -  (
(ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) )  /  ( x  /  n ) ) )
15710nncnd 9757 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
158157mulid2d 8848 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  =  n )
159 fznnfl 10960 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  (
n  e.  ( 1 ... ( |_ `  x ) )  <->  ( n  e.  NN  /\  n  <_  x ) ) )
16037, 159syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
n  e.  ( 1 ... ( |_ `  x ) )  <->  ( n  e.  NN  /\  n  <_  x ) ) )
161160simplbda 609 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  <_  x )
162158, 161eqbrtrd 4044 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  n )  <_  x )
1631a1i 12 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
164163, 143, 94lemuldivd 10430 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  x.  n )  <_  x  <->  1  <_  ( x  /  n ) ) )
165162, 164mpbid 203 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  ( x  /  n ) )
166 elicopnf 10733 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  e.  RR  ->  (
( x  /  n
)  e.  ( 1 [,)  +oo )  <->  ( (
x  /  n )  e.  RR  /\  1  <_  ( x  /  n
) ) ) )
1671, 166ax-mp 10 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  /  n )  e.  ( 1 [,) 
+oo )  <->  ( (
x  /  n )  e.  RR  /\  1  <_  ( x  /  n
) ) )
16890, 165, 167sylanbrc 647 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  n )  e.  ( 1 [,)  +oo )
)
169 selberg3lem1.2 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A. y  e.  ( 1 [,)  +oo )
( abs `  (
( sum_ k  e.  ( 1 ... ( |_
`  y ) ) ( (Λ `  k
)  x.  ( log `  k ) )  -  ( (ψ `  y )  x.  ( log `  y
) ) )  / 
y ) )  <_  A )
170169ad2antrr 708 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A. y  e.  ( 1 [,)  +oo ) ( abs `  (
( sum_ k  e.  ( 1 ... ( |_
`  y ) ) ( (Λ `  k
)  x.  ( log `  k ) )  -  ( (ψ `  y )  x.  ( log `  y
) ) )  / 
y ) )  <_  A )
171 fveq2 5485 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  m  ->  (Λ `  k )  =  (Λ `  m ) )
172 fveq2 5485 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  m  ->  ( log `  k )  =  ( log `  m
) )
173171, 172oveq12d 5837 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  m  ->  (
(Λ `  k )  x.  ( log `  k
) )  =  ( (Λ `  m )  x.  ( log `  m
) ) )
174173cbvsumv 12163 . . . . . . . . . . . . . . . . . . . . . . 23  |-  sum_ k  e.  ( 1 ... ( |_ `  y ) ) ( (Λ `  k
)  x.  ( log `  k ) )  = 
sum_ m  e.  (
1 ... ( |_ `  y ) ) ( (Λ `  m )  x.  ( log `  m
) )
175 fveq2 5485 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( x  /  n )  ->  ( |_ `  y )  =  ( |_ `  (
x  /  n ) ) )
176175oveq2d 5835 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( x  /  n )  ->  (
1 ... ( |_ `  y ) )  =  ( 1 ... ( |_ `  ( x  /  n ) ) ) )
177176sumeq1d 12168 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( x  /  n )  ->  sum_ m  e.  ( 1 ... ( |_ `  y ) ) ( (Λ `  m
)  x.  ( log `  m ) )  = 
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) ) )
178174, 177syl5eq 2328 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x  /  n )  ->  sum_ k  e.  ( 1 ... ( |_ `  y ) ) ( (Λ `  k
)  x.  ( log `  k ) )  = 
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) ) )
179 fveq2 5485 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( x  /  n )  ->  (ψ `  y )  =  (ψ `  ( x  /  n
) ) )
180 fveq2 5485 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( x  /  n )  ->  ( log `  y )  =  ( log `  (
x  /  n ) ) )
181179, 180oveq12d 5837 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x  /  n )  ->  (
(ψ `  y )  x.  ( log `  y
) )  =  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) )
182178, 181oveq12d 5837 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( x  /  n )  ->  ( sum_ k  e.  ( 1 ... ( |_ `  y ) ) ( (Λ `  k )  x.  ( log `  k
) )  -  (
(ψ `  y )  x.  ( log `  y
) ) )  =  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) )
183 id 21 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( x  /  n )  ->  y  =  ( x  /  n ) )
184182, 183oveq12d 5837 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( x  /  n )  ->  (
( sum_ k  e.  ( 1 ... ( |_
`  y ) ) ( (Λ `  k
)  x.  ( log `  k ) )  -  ( (ψ `  y )  x.  ( log `  y
) ) )  / 
y )  =  ( ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) )  / 
( x  /  n
) ) )
185184fveq2d 5489 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  ( x  /  n )  ->  ( abs `  ( ( sum_ k  e.  ( 1 ... ( |_ `  y ) ) ( (Λ `  k )  x.  ( log `  k
) )  -  (
(ψ `  y )  x.  ( log `  y
) ) )  / 
y ) )  =  ( abs `  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) )  / 
( x  /  n
) ) ) )
186185breq1d 4034 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( x  /  n )  ->  (
( abs `  (
( sum_ k  e.  ( 1 ... ( |_
`  y ) ) ( (Λ `  k
)  x.  ( log `  k ) )  -  ( (ψ `  y )  x.  ( log `  y
) ) )  / 
y ) )  <_  A 
<->  ( abs `  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) )  / 
( x  /  n
) ) )  <_  A ) )
187186rspcv 2881 . . . . . . . . . . . . . . . . 17  |-  ( ( x  /  n )  e.  ( 1 [,) 
+oo )  ->  ( A. y  e.  (
1 [,)  +oo ) ( abs `  ( (
sum_ k  e.  ( 1 ... ( |_
`  y ) ) ( (Λ `  k
)  x.  ( log `  k ) )  -  ( (ψ `  y )  x.  ( log `  y
) ) )  / 
y ) )  <_  A  ->  ( abs `  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) )  / 
( x  /  n
) ) )  <_  A ) )
188168, 170, 187sylc 58 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) )  / 
( x  /  n
) ) )  <_  A )
189156, 188eqbrtrrd 4046 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) )  /  ( x  /  n ) )  <_  A )
190146, 142, 129ledivmul2d 10435 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
( abs `  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) )  -  (
(ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) )  /  ( x  /  n ) )  <_  A 
<->  ( abs `  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) )  -  (
(ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) )  <_  ( A  x.  ( x  /  n
) ) ) )
191189, 190mpbid 203 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) )  <_  ( A  x.  ( x  /  n
) ) )
19224adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A  e.  CC )
193143recnd 8856 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  CC )
19410nnne0d 9785 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0 )
195192, 193, 157, 194divassd 9566 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( A  x.  x )  /  n )  =  ( A  x.  ( x  /  n ) ) )
196191, 195breqtrrd 4050 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) )  <_  ( ( A  x.  x )  /  n ) )
197146, 147, 12, 149, 196lemul2ad 9692 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( abs `  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) ) )  <_  ( (Λ `  n )  x.  (
( A  x.  x
)  /  n ) ) )
198117, 133absmuld 11930 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( (Λ `  n
)  x.  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n
) )  x.  ( log `  ( x  /  n ) ) ) ) ) )  =  ( ( abs `  (Λ `  n ) )  x.  ( abs `  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) )  -  (
(ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) ) ) )
19912, 149absidd 11899 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  (Λ `  n )
)  =  (Λ `  n
) )
200199oveq1d 5834 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  (Λ `  n
) )  x.  ( abs `  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) ) )  =  ( (Λ `  n )  x.  ( abs `  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) ) ) )
201198, 200eqtrd 2316 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( (Λ `  n
)  x.  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n
) )  x.  ( log `  ( x  /  n ) ) ) ) ) )  =  ( (Λ `  n
)  x.  ( abs `  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) ) ) )
202144recnd 8856 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( A  x.  x )  e.  CC )
203117, 157, 202, 194div32d 9554 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  x.  ( A  x.  x )
)  =  ( (Λ `  n )  x.  (
( A  x.  x
)  /  n ) ) )
204197, 201, 2033brtr4d 4054 . . . . . . . . . . 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
) )  x.  ( log `  ( x  /  n ) ) ) ) ) )  <_ 
( ( (Λ `  n
)  /  n )  x.  ( A  x.  x ) ) )
2058, 137, 145, 204fsumle 12251 . . . . . . . . . 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 ) )  x.  ( log `  (
x  /  n ) ) ) ) ) )  <_  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( A  x.  x ) ) )
20637recnd 8856 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  x  e.  CC )
20724, 206mulcld 8850 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( A  x.  x )  e.  CC )
208117, 157, 194divcld 9531 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  CC )
2098, 207, 208fsummulc1 12241 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  x.  ( A  x.  x )
)  =  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  x.  ( A  x.  x ) ) )
210205, 209breqtrrd 4050 . . . . . . . . 9  |-  ( (
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 ) )  x.  ( log `  (
x  /  n ) ) ) ) ) )  <_  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  x.  ( A  x.  x ) ) )
211136, 138, 140, 141, 210letrd 8968 . . . . . . . 8  |-  ( (
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
) )  x.  ( log `  ( x  /  n ) ) ) ) ) )  <_ 
( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  x.  ( A  x.  x ) ) )
212126recnd 8856 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  e.  CC )
21392recnd 8856 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  n ) )  e.  CC )
21495recnd 8856 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  n )  e.  CC )
215213, 214mulcld 8850 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  n
) )  x.  ( log `  n ) )  e.  CC )
216212, 215addcld 8849 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) )  +  ( (ψ `  ( x  /  n
) )  x.  ( log `  n ) ) )  e.  CC )
217117, 216mulcld 8850 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) )  +  ( (ψ `  ( x  /  n ) )  x.  ( log `  n
) ) ) )  e.  CC )
218117, 213mulcld 8850 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  (ψ `  ( x  /  n
) ) )  e.  CC )
21927adantr 453 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  x )  e.  CC )
220218, 219mulcld 8850 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  x.  ( log `  x
) )  e.  CC )
2218, 217, 220fsumsub 12244 . . . . . . . . . 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
) )  x.  ( log `  n ) ) ) )  -  (
( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  x.  ( log `  x
) ) )  =  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) )  +  ( (ψ `  ( x  /  n
) )  x.  ( log `  n ) ) ) )  -  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  x.  ( log `  x
) ) ) )
222213, 219mulcld 8850 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  n
) )  x.  ( log `  x ) )  e.  CC )
223117, 216, 222subdid 9230 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  (
( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  +  ( (ψ `  (
x  /  n ) )  x.  ( log `  n ) ) )  -  ( (ψ `  ( x  /  n
) )  x.  ( log `  x ) ) ) )  =  ( ( (Λ `  n
)  x.  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) )  +  ( (ψ `  ( x  /  n
) )  x.  ( log `  n ) ) ) )  -  (
(Λ `  n )  x.  ( (ψ `  (
x  /  n ) )  x.  ( log `  x ) ) ) ) )
22445adantr 453 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR+ )
225224, 94relogdivd 19971 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  ( x  /  n
) )  =  ( ( log `  x
)  -  ( log `  n ) ) )
226225oveq2d 5835 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  n
) )  x.  ( log `  ( x  /  n ) ) )  =  ( (ψ `  ( x  /  n
) )  x.  (
( log `  x
)  -  ( log `  n ) ) ) )
227213, 219, 214subdid 9230 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  n
) )  x.  (
( log `  x
)  -  ( log `  n ) ) )  =  ( ( (ψ `  ( x  /  n
) )  x.  ( log `  x ) )  -  ( (ψ `  ( x  /  n
) )  x.  ( log `  n ) ) ) )
228226, 227eqtrd 2316 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  n
) )  x.  ( log `  ( x  /  n ) ) )  =  ( ( (ψ `  ( x  /  n
) )  x.  ( log `  x ) )  -  ( (ψ `  ( x  /  n
) )  x.  ( log `  n ) ) ) )
229228oveq2d 5835 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n
) )  x.  ( log `  ( x  /  n ) ) ) )  =  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) )  -  ( ( (ψ `  ( x  /  n
) )  x.  ( log `  x ) )  -  ( (ψ `  ( x  /  n
) )  x.  ( log `  n ) ) ) ) )
230212, 222, 215subsub3d 9182 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) )  -  ( ( (ψ `  ( x  /  n
) )  x.  ( log `  x ) )  -  ( (ψ `  ( x  /  n
) )  x.  ( log `  n ) ) ) )  =  ( ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  +  ( (ψ `  (
x  /  n ) )  x.  ( log `  n ) ) )  -  ( (ψ `  ( x  /  n
) )  x.  ( log `  x ) ) ) )
231229, 230eqtrd 2316 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) )  -  ( (ψ `  ( x  /  n
) )  x.  ( log `  ( x  /  n ) ) ) )  =  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) )  +  ( (ψ `  ( x  /  n ) )  x.  ( log `  n
) ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  x
) ) ) )
232231oveq2d 5835 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) )  -  (
(ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) )  =  ( (Λ `  n
)  x.  ( (
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) )  +  ( (ψ `  ( x  /  n ) )  x.  ( log `  n
) ) )  -  ( (ψ `  ( x  /  n ) )  x.  ( log `  x
) ) ) ) )
233117, 213, 219mulassd 8853 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  x.  ( log `  x
) )  =  ( (Λ `  n )  x.  ( (ψ `  (
x  /  n ) )  x.  ( log `  x ) ) ) )
234233oveq2d 5835 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  x.  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  +  ( (ψ `  (
x  /  n ) )  x.  ( log `  n ) ) ) )  -  ( ( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  x.  ( log `  x
) ) )  =  ( ( (Λ `  n
)  x.  ( sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) )  +  ( (ψ `  ( x  /  n
) )  x.  ( log `  n ) ) ) )  -  (
(Λ `  n )  x.  ( (ψ `  (
x  /  n ) )  x.  ( log `  x ) ) ) ) )
235223, 232, 2343eqtr4d 2326 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) )  -  (
(ψ `  ( x  /  n ) )  x.  ( log `  (
x  /  n ) ) ) ) )  =  ( ( (Λ `  n )  x.  ( sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  m )  x.  ( log `  m
) )  +  ( (ψ `  ( x  /  n ) )  x.  ( log `  n
) ) ) )  -  ( ( (Λ `  n )  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  x
) ) ) )
236235sumeq2dv 12170 . . . . . . . . . 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
) )  x.  ( log `  ( x  /  n ) ) ) ) )  =  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  ( sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) )  +  ( (ψ `  (
x  /  n ) )  x.  ( log `  n ) ) ) )  -  ( ( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  x.  ( log `  x
) ) ) )
237 fveq2 5485 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  m  ->  (Λ `  n )  =  (Λ `  m ) )
238 oveq2 5827 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  m  ->  (
x  /  n )  =  ( x  /  m ) )
239238fveq2d 5489 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  m  ->  (ψ `  ( x  /  n
) )  =  (ψ `  ( x  /  m
) ) )
240237, 239oveq12d 5837 . . . . . . . . . . . . . . . . 17  |-  ( n  =  m  ->  (
(Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  =  ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) ) )
241 fveq2 5485 . . . . . . . . . . . . . . . . 17  |-  ( n  =  m  ->  ( log `  n )  =  ( log `  m
) )
242240, 241oveq12d 5837 . . . . . . . . . . . . . . . 16  |-  ( n  =  m  ->  (
( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  x.  ( log `  n
) )  =  ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) ) )
243242cbvsumv 12163 . . . . . . . . . . . . . . 15  |-  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  n
) )  =  sum_ m  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  m )  x.  (ψ `  ( x  /  m ) ) )  x.  ( log `  m
) )
244 elfznn 10813 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  ( 1 ... ( |_ `  (
x  /  m ) ) )  ->  n  e.  NN )
245244adantl 454 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  n  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  n  e.  NN )
246245, 11syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  n  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  (Λ `  n
)  e.  RR )
247246recnd 8856 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  /\  n  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) )  ->  (Λ `  n
)  e.  CC )
248247anasss 630 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
m  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ) )  ->  (Λ `  n
)  e.  CC )
249 elfznn 10813 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  e.  ( 1 ... ( |_ `  x
) )  ->  m  e.  NN )
250249adantl 454 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  m  e.  NN )
251250, 121syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  m
)  e.  RR )
252251recnd 8856 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  m
)  e.  CC )
253250nnrpd 10384 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  m  e.  RR+ )
254253relogcld 19968 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  m )  e.  RR )
255254recnd 8856 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( log `  m )  e.  CC )
256252, 255mulcld 8850 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  m )  x.  ( log `  m ) )  e.  CC )
257256adantrr 699 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
m  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ) )  ->  ( (Λ `  m )  x.  ( log `  m ) )  e.  CC )
258248, 257mulcld 8850 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  (
m  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  ( 1 ... ( |_ `  ( x  /  m
) ) ) ) )  ->  ( (Λ `  n )  x.  (
(Λ `  m )  x.  ( log `  m
) ) )  e.  CC )
25937, 258fsumfldivdiag 20424 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  x ) )
sum_ n  e.  (
1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  n )  x.  ( (Λ `  m
)  x.  ( log `  m ) ) )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) )
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  n )  x.  ( (Λ `  m
)  x.  ( log `  m ) ) ) )
26037adantr 453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
261260, 250nndivred 9789 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  /  m )  e.  RR )
262 chpcl 20356 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  /  m )  e.  RR  ->  (ψ `  ( x  /  m
) )  e.  RR )
263261, 262syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  m ) )  e.  RR )
264263recnd 8856 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  m ) )  e.  CC )
265252, 264, 255mul32d 9017 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  m )  x.  (ψ `  ( x  /  m ) ) )  x.  ( log `  m
) )  =  ( ( (Λ `  m
)  x.  ( log `  m ) )  x.  (ψ `  ( x  /  m ) ) ) )
266251, 254remulcld 8858 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  m )  x.  ( log `  m ) )  e.  RR )
267266recnd 8856 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  m )  x.  ( log `  m ) )  e.  CC )
268267, 264mulcomd 8851 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  m )  x.  ( log `  m
) )  x.  (ψ `  ( x  /  m
) ) )  =  ( (ψ `  (
x  /  m ) )  x.  ( (Λ `  m )  x.  ( log `  m ) ) ) )
269 chpval 20354 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  /  m )  e.  RR  ->  (ψ `  ( x  /  m
) )  =  sum_ n  e.  ( 1 ... ( |_ `  (
x  /  m ) ) ) (Λ `  n
) )
270261, 269syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  (ψ `  (
x  /  m ) )  =  sum_ n  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) (Λ `  n )
)
271270oveq1d 5834 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  m
) )  x.  (
(Λ `  m )  x.  ( log `  m
) ) )  =  ( sum_ n  e.  ( 1 ... ( |_
`  ( x  /  m ) ) ) (Λ `  n )  x.  ( (Λ `  m
)  x.  ( log `  m ) ) ) )
272 fzfid 11029 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  ( x  /  m
) ) )  e. 
Fin )
273272, 267, 247fsummulc1 12241 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  (
x  /  m ) ) ) (Λ `  n
)  x.  ( (Λ `  m )  x.  ( log `  m ) ) )  =  sum_ n  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  n
)  x.  ( (Λ `  m )  x.  ( log `  m ) ) ) )
274271, 273eqtrd 2316 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (ψ `  ( x  /  m
) )  x.  (
(Λ `  m )  x.  ( log `  m
) ) )  = 
sum_ n  e.  (
1 ... ( |_ `  ( x  /  m
) ) ) ( (Λ `  n )  x.  ( (Λ `  m
)  x.  ( log `  m ) ) ) )
275265, 268, 2743eqtrd 2320 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  m  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  m )  x.  (ψ `  ( x  /  m ) ) )  x.  ( log `  m
) )  =  sum_ n  e.  ( 1 ... ( |_ `  (
x  /  m ) ) ) ( (Λ `  n )  x.  (
(Λ `  m )  x.  ( log `  m
) ) ) )
276275sumeq2dv 12170 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) )  =  sum_ m  e.  ( 1 ... ( |_ `  x
) ) sum_ n  e.  ( 1 ... ( |_ `  ( x  /  m ) ) ) ( (Λ `  n
)  x.  ( (Λ `  m )  x.  ( log `  m ) ) ) )
277125recnd 8856 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) )  ->  ( (Λ `  m )  x.  ( log `  m ) )  e.  CC )
278118, 117, 277fsummulc2 12240 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) )  =  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  n
)  x.  ( (Λ `  m )  x.  ( log `  m ) ) ) )
279278sumeq2dv 12170 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) )
sum_ m  e.  (
1 ... ( |_ `  ( x  /  n
) ) ) ( (Λ `  n )  x.  ( (Λ `  m
)  x.  ( log `  m ) ) ) )
280259, 276, 2793eqtr4d 2326 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ m  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  m
)  x.  (ψ `  ( x  /  m
) ) )  x.  ( log `  m
) )  =  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) )
281243, 280syl5eq 2328 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  n
) )  =  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) ) )
282117, 213, 214mulassd 8853 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  x.  ( log `  n
) )  =  ( (Λ `  n )  x.  ( (ψ `  (
x  /  n ) )  x.  ( log `  n ) ) ) )
283282sumeq2dv 12170 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  n
) )  =  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  x.  (
(ψ `  ( x  /  n ) )  x.  ( log `  n
) ) ) )
284281, 283oveq12d 5837 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  n
) )  +  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  x.  ( log `  n
) ) )  =  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) )  +  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  ( (ψ `  ( x  /  n
) )  x.  ( log `  n ) ) ) ) )
2851072timesd 9949 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  n
) ) )  =  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  n
) )  +  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( (Λ `  n )  x.  (ψ `  ( x  /  n ) ) )  x.  ( log `  n
) ) ) )
286117, 212mulcld 8850 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  n ) ) ) ( (Λ `  m )  x.  ( log `  m ) ) )  e.  CC )
287117, 215mulcld 8850 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  x.  (
(ψ `  ( x  /  n ) )  x.  ( log `  n
) ) )  e.  CC )
2888, 286, 287fsumadd 12205 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) )  +  ( (Λ `  n
)  x.  ( (ψ `  ( x  /  n
) )  x.  ( log `  n ) ) ) )  =  (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  x.  sum_ m  e.  ( 1 ... ( |_
`  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) )  +  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  x.  ( (ψ `  ( x  /  n
) )  x.  ( log `  n ) ) ) ) )
289284, 285, 2883eqtr4d 2326 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ( 1 (,)  +oo ) )  ->  (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  (ψ `  ( x  /  n
) ) )  x.  ( log `  n
) ) )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  x.  sum_ m  e.  ( 1 ... ( |_ `  ( x  /  n ) ) ) ( (Λ `  m
)  x.  ( log `  m ) ) )  +  ( (Λ `  n
)  x.  ( (ψ `  ( x  /  n
) )  x.  ( log `  n ) ) ) ) )
290117, 212, 215adddid 8854 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  ( 1 (,)  +oo ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (&La