Metamath Proof Explorer

Theorem selberg3lem1

Description: Introduce a log weighting on the summands of sum_ m x. n <_ x , Lam ( m ) Lam ( n ) , the core of selberg2 (written here as sum_ n <_ x , Lam ( n ) psi ( x / n ) ). Equation 10.4.21 of Shapiro, p. 422. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Hypotheses selberg3lem1.1 
|- ( ph -> A e. RR+ )
selberg3lem1.2 
|- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ k e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` k ) x. ( log ` k ) ) - ( ( psi ` y ) x. ( log ` y ) ) ) / y ) ) <_ A )
Assertion selberg3lem1 
|- ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) ) e. O(1) )

Proof

Step Hyp Ref Expression
1 selberg3lem1.1 
 |-  ( ph -> A e. RR+ )
2 selberg3lem1.2 
 |-  ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ k e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` k ) x. ( log ` k ) ) - ( ( psi ` y ) x. ( log ` y ) ) ) / y ) ) <_ A )
3 1red 
 |-  ( ph -> 1 e. RR )
4 ioossre 
 |-  ( 1 (,) +oo ) C_ RR
5 1 rpcnd 
 |-  ( ph -> A e. CC )
6 o1const 
 |-  ( ( ( 1 (,) +oo ) C_ RR /\ A e. CC ) -> ( x e. ( 1 (,) +oo ) |-> A ) e. O(1) )
7 4 5 6 sylancr 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> A ) e. O(1) )
8 fzfid 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
9 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
10 9 adantl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
11 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
12 10 11 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
13 12 10 nndivred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
14 8 13 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. RR )
15 elioore 
 |-  ( x e. ( 1 (,) +oo ) -> x e. RR )
16 eliooord 
 |-  ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
17 16 simpld 
 |-  ( x e. ( 1 (,) +oo ) -> 1 < x )
18 15 17 rplogcld 
 |-  ( x e. ( 1 (,) +oo ) -> ( log ` x ) e. RR+ )
19 rpdivcl 
 |-  ( ( A e. RR+ /\ ( log ` x ) e. RR+ ) -> ( A / ( log ` x ) ) e. RR+ )
20 1 18 19 syl2an 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A / ( log ` x ) ) e. RR+ )
21 20 rpred 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A / ( log ` x ) ) e. RR )
22 14 21 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A / ( log ` x ) ) ) e. RR )
23 22 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A / ( log ` x ) ) ) e. CC )
24 5 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. CC )
25 14 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. CC )
26 18 adantl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
27 26 rpcnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
28 20 rpcnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A / ( log ` x ) ) e. CC )
29 25 27 28 subdird 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) x. ( A / ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A / ( log ` x ) ) ) - ( ( log ` x ) x. ( A / ( log ` x ) ) ) ) )
30 26 rpne0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
31 24 27 30 divcan2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( log ` x ) x. ( A / ( log ` x ) ) ) = A )
32 31 oveq2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A / ( log ` x ) ) ) - ( ( log ` x ) x. ( A / ( log ` x ) ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A / ( log ` x ) ) ) - A ) )
33 29 32 eqtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) x. ( A / ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A / ( log ` x ) ) ) - A ) )
34 33 mpteq2dva 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) x. ( A / ( log ` x ) ) ) ) = ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A / ( log ` x ) ) ) - A ) ) )
35 26 rpred 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
36 14 35 resubcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. RR )
37 15 adantl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
38 0red 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 e. RR )
39 1red 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
40 0lt1 
 |-  0 < 1
41 40 a1i 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 < 1 )
42 17 adantl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
43 38 39 37 41 42 lttrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 < x )
44 37 43 elrpd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
45 44 ex 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) -> x e. RR+ ) )
46 45 ssrdv 
 |-  ( ph -> ( 1 (,) +oo ) C_ RR+ )
47 vmadivsum 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1)
48 47 a1i 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) )
49 46 48 o1res2 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) )
50 4 a1i 
 |-  ( ph -> ( 1 (,) +oo ) C_ RR )
51 ere 
 |-  _e e. RR
52 51 a1i 
 |-  ( ph -> _e e. RR )
53 1 rpred 
 |-  ( ph -> A e. RR )
54 20 adantrr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> ( A / ( log ` x ) ) e. RR+ )
55 54 rprege0d 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> ( ( A / ( log ` x ) ) e. RR /\ 0 <_ ( A / ( log ` x ) ) ) )
56 absid 
 |-  ( ( ( A / ( log ` x ) ) e. RR /\ 0 <_ ( A / ( log ` x ) ) ) -> ( abs ` ( A / ( log ` x ) ) ) = ( A / ( log ` x ) ) )
57 55 56 syl 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> ( abs ` ( A / ( log ` x ) ) ) = ( A / ( log ` x ) ) )
58 loge 
 |-  ( log ` _e ) = 1
59 simprr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> _e <_ x )
60 epr 
 |-  _e e. RR+
61 44 adantrr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> x e. RR+ )
62 logleb 
 |-  ( ( _e e. RR+ /\ x e. RR+ ) -> ( _e <_ x <-> ( log ` _e ) <_ ( log ` x ) ) )
63 60 61 62 sylancr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> ( _e <_ x <-> ( log ` _e ) <_ ( log ` x ) ) )
64 59 63 mpbid 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> ( log ` _e ) <_ ( log ` x ) )
65 58 64 eqbrtrrid 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> 1 <_ ( log ` x ) )
66 1rp 
 |-  1 e. RR+
67 rpregt0 
 |-  ( 1 e. RR+ -> ( 1 e. RR /\ 0 < 1 ) )
68 66 67 mp1i 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> ( 1 e. RR /\ 0 < 1 ) )
69 26 adantrr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> ( log ` x ) e. RR+ )
70 69 rpregt0d 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> ( ( log ` x ) e. RR /\ 0 < ( log ` x ) ) )
71 1 adantr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> A e. RR+ )
72 71 rpregt0d 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> ( A e. RR /\ 0 < A ) )
73 lediv2 
 |-  ( ( ( 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 ) ) )
74 68 70 72 73 syl3anc 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> ( 1 <_ ( log ` x ) <-> ( A / ( log ` x ) ) <_ ( A / 1 ) ) )
75 65 74 mpbid 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> ( A / ( log ` x ) ) <_ ( A / 1 ) )
76 5 adantr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> A e. CC )
77 76 div1d 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> ( A / 1 ) = A )
78 75 77 breqtrd 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> ( A / ( log ` x ) ) <_ A )
79 57 78 eqbrtrd 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ _e <_ x ) ) -> ( abs ` ( A / ( log ` x ) ) ) <_ A )
80 50 28 52 53 79 elo1d 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( A / ( log ` x ) ) ) e. O(1) )
81 36 21 49 80 o1mul2 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) x. ( A / ( log ` x ) ) ) ) e. O(1) )
82 34 81 eqeltrrd 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A / ( log ` x ) ) ) - A ) ) e. O(1) )
83 23 24 82 o1dif 
 |-  ( ph -> ( ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A / ( log ` x ) ) ) ) e. O(1) <-> ( x e. ( 1 (,) +oo ) |-> A ) e. O(1) ) )
84 7 83 mpbird 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A / ( log ` x ) ) ) ) e. O(1) )
85 2re 
 |-  2 e. RR
86 rerpdivcl 
 |-  ( ( 2 e. RR /\ ( log ` x ) e. RR+ ) -> ( 2 / ( log ` x ) ) e. RR )
87 85 26 86 sylancr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 / ( log ` x ) ) e. RR )
88 nndivre 
 |-  ( ( x e. RR /\ n e. NN ) -> ( x / n ) e. RR )
89 37 9 88 syl2an 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
90 chpcl 
 |-  ( ( x / n ) e. RR -> ( psi ` ( x / n ) ) e. RR )
91 89 90 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / n ) ) e. RR )
92 12 91 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) e. RR )
93 10 nnrpd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
94 93 relogcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
95 92 94 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) e. RR )
96 8 95 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) e. RR )
97 87 96 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) e. RR )
98 8 92 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) e. RR )
99 97 98 resubcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) e. RR )
100 99 44 rerpdivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) e. RR )
101 100 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) e. CC )
102 101 abscld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) ) e. RR )
103 23 abscld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A / ( log ` x ) ) ) ) e. RR )
104 2cnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 2 e. CC )
105 96 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) e. CC )
106 104 105 mulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) e. CC )
107 98 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) e. CC )
108 107 27 mulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) e. CC )
109 106 108 subcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) e. CC )
110 109 abscld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) ) e. RR )
111 43 gt0ne0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
112 110 37 111 redivcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) ) / x ) e. RR )
113 53 adantr 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> A e. RR )
114 14 113 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. A ) e. RR )
115 12 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. CC )
116 fzfid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / n ) ) ) e. Fin )
117 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` ( x / n ) ) ) -> m e. NN )
118 117 adantl 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. NN )
119 vmacl 
 |-  ( m e. NN -> ( Lam ` m ) e. RR )
120 118 119 syl 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( Lam ` m ) e. RR )
121 118 nnrpd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. RR+ )
122 121 relogcld 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( log ` m ) e. RR )
123 120 122 remulcld 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( log ` m ) ) e. RR )
124 116 123 fsumrecl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) e. RR )
125 9 nnrpd 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. RR+ )
126 rpdivcl 
 |-  ( ( x e. RR+ /\ n e. RR+ ) -> ( x / n ) e. RR+ )
127 44 125 126 syl2an 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
128 127 relogcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR )
129 91 128 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) e. RR )
130 124 129 resubcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) e. RR )
131 130 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) e. CC )
132 115 131 mulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) e. CC )
133 8 132 fsumcl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) e. CC )
134 133 abscld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) ) e. RR )
135 132 abscld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) ) e. RR )
136 8 135 fsumrecl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) ) e. RR )
137 113 37 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A x. x ) e. RR )
138 14 137 remulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A x. x ) ) e. RR )
139 8 132 fsumabs 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) ) )
140 53 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. RR )
141 37 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
142 140 141 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( A x. x ) e. RR )
143 13 142 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( A x. x ) ) e. RR )
144 131 abscld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) e. RR )
145 142 10 nndivred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( A x. x ) / n ) e. RR )
146 vmage0 
 |-  ( n e. NN -> 0 <_ ( Lam ` n ) )
147 10 146 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( Lam ` n ) )
148 89 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. CC )
149 127 rpne0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) =/= 0 )
150 131 148 149 absdivd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) / ( x / n ) ) ) = ( ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) / ( abs ` ( x / n ) ) ) )
151 127 rpge0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( x / n ) )
152 89 151 absidd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( x / n ) ) = ( x / n ) )
153 152 oveq2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) / ( abs ` ( x / n ) ) ) = ( ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) / ( x / n ) ) )
154 150 153 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) / ( x / n ) ) ) = ( ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) / ( x / n ) ) )
155 fveq2 
 |-  ( k = m -> ( Lam ` k ) = ( Lam ` m ) )
156 fveq2 
 |-  ( k = m -> ( log ` k ) = ( log ` m ) )
157 155 156 oveq12d 
 |-  ( k = m -> ( ( Lam ` k ) x. ( log ` k ) ) = ( ( Lam ` m ) x. ( log ` m ) ) )
158 157 cbvsumv 
 |-  sum_ k e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` k ) x. ( log ` k ) ) = sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` m ) x. ( log ` m ) )
159 fveq2 
 |-  ( y = ( x / n ) -> ( |_ ` y ) = ( |_ ` ( x / n ) ) )
160 159 oveq2d 
 |-  ( y = ( x / n ) -> ( 1 ... ( |_ ` y ) ) = ( 1 ... ( |_ ` ( x / n ) ) ) )
161 160 sumeq1d 
 |-  ( y = ( x / n ) -> sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` m ) x. ( log ` m ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) )
162 158 161 eqtrid 
 |-  ( y = ( x / n ) -> sum_ k e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` k ) x. ( log ` k ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) )
163 fveq2 
 |-  ( y = ( x / n ) -> ( psi ` y ) = ( psi ` ( x / n ) ) )
164 fveq2 
 |-  ( y = ( x / n ) -> ( log ` y ) = ( log ` ( x / n ) ) )
165 163 164 oveq12d 
 |-  ( y = ( x / n ) -> ( ( psi ` y ) x. ( log ` y ) ) = ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) )
166 162 165 oveq12d 
 |-  ( y = ( x / n ) -> ( sum_ k e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` k ) x. ( log ` k ) ) - ( ( psi ` y ) x. ( log ` y ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) )
167 id 
 |-  ( y = ( x / n ) -> y = ( x / n ) )
168 166 167 oveq12d 
 |-  ( y = ( x / n ) -> ( ( sum_ k e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` k ) x. ( log ` k ) ) - ( ( psi ` y ) x. ( log ` y ) ) ) / y ) = ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) / ( x / n ) ) )
169 168 fveq2d 
 |-  ( y = ( x / n ) -> ( abs ` ( ( sum_ k e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` k ) x. ( log ` k ) ) - ( ( psi ` y ) x. ( log ` y ) ) ) / y ) ) = ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) / ( x / n ) ) ) )
170 169 breq1d 
 |-  ( y = ( x / n ) -> ( ( abs ` ( ( sum_ k e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` k ) x. ( log ` k ) ) - ( ( psi ` y ) x. ( log ` y ) ) ) / y ) ) <_ A <-> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) / ( x / n ) ) ) <_ A ) )
171 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( sum_ k e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` k ) x. ( log ` k ) ) - ( ( psi ` y ) x. ( log ` y ) ) ) / y ) ) <_ A )
172 10 nncnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
173 172 mullidd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) = n )
174 fznnfl 
 |-  ( x e. RR -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) )
175 37 174 syl 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) )
176 175 simplbda 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n <_ x )
177 173 176 eqbrtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) <_ x )
178 1red 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
179 178 141 93 lemuldivd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 x. n ) <_ x <-> 1 <_ ( x / n ) ) )
180 177 179 mpbid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ ( x / n ) )
181 1re 
 |-  1 e. RR
182 elicopnf 
 |-  ( 1 e. RR -> ( ( x / n ) e. ( 1 [,) +oo ) <-> ( ( x / n ) e. RR /\ 1 <_ ( x / n ) ) ) )
183 181 182 ax-mp 
 |-  ( ( x / n ) e. ( 1 [,) +oo ) <-> ( ( x / n ) e. RR /\ 1 <_ ( x / n ) ) )
184 89 180 183 sylanbrc 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. ( 1 [,) +oo ) )
185 170 171 184 rspcdva 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) / ( x / n ) ) ) <_ A )
186 154 185 eqbrtrrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) / ( x / n ) ) <_ A )
187 144 140 127 ledivmul2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) / ( x / n ) ) <_ A <-> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) <_ ( A x. ( x / n ) ) ) )
188 186 187 mpbid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) <_ ( A x. ( x / n ) ) )
189 24 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> A e. CC )
190 141 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
191 10 nnne0d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
192 189 190 172 191 divassd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( A x. x ) / n ) = ( A x. ( x / n ) ) )
193 188 192 breqtrrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) <_ ( ( A x. x ) / n ) )
194 144 145 12 147 193 lemul2ad 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) ) <_ ( ( Lam ` n ) x. ( ( A x. x ) / n ) ) )
195 115 131 absmuld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) ) = ( ( abs ` ( Lam ` n ) ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) ) )
196 12 147 absidd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( Lam ` n ) ) = ( Lam ` n ) )
197 196 oveq1d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( Lam ` n ) ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) ) = ( ( Lam ` n ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) ) )
198 195 197 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) ) = ( ( Lam ` n ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) ) )
199 142 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( A x. x ) e. CC )
200 115 172 199 191 div32d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. ( A x. x ) ) = ( ( Lam ` n ) x. ( ( A x. x ) / n ) ) )
201 194 198 200 3brtr4d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) ) <_ ( ( ( Lam ` n ) / n ) x. ( A x. x ) ) )
202 8 135 143 201 fsumle 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( A x. x ) ) )
203 37 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
204 24 203 mulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( A x. x ) e. CC )
205 115 172 191 divcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. CC )
206 8 204 205 fsummulc1 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A x. x ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. ( A x. x ) ) )
207 202 206 breqtrrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A x. x ) ) )
208 134 136 138 139 207 letrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A x. x ) ) )
209 124 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) e. CC )
210 91 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / n ) ) e. CC )
211 94 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. CC )
212 210 211 mulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / n ) ) x. ( log ` n ) ) e. CC )
213 209 212 addcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) e. CC )
214 115 213 mulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) e. CC )
215 115 210 mulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) e. CC )
216 27 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` x ) e. CC )
217 215 216 mulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) e. CC )
218 8 214 217 fsumsub 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) - ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) )
219 210 216 mulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / n ) ) x. ( log ` x ) ) e. CC )
220 115 213 219 subdid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) - ( ( psi ` ( x / n ) ) x. ( log ` x ) ) ) ) = ( ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) - ( ( Lam ` n ) x. ( ( psi ` ( x / n ) ) x. ( log ` x ) ) ) ) )
221 44 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
222 221 93 relogdivd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) = ( ( log ` x ) - ( log ` n ) ) )
223 222 oveq2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) = ( ( psi ` ( x / n ) ) x. ( ( log ` x ) - ( log ` n ) ) ) )
224 210 216 211 subdid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / n ) ) x. ( ( log ` x ) - ( log ` n ) ) ) = ( ( ( psi ` ( x / n ) ) x. ( log ` x ) ) - ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) )
225 223 224 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) = ( ( ( psi ` ( x / n ) ) x. ( log ` x ) ) - ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) )
226 225 oveq2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( ( psi ` ( x / n ) ) x. ( log ` x ) ) - ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) )
227 209 219 212 subsub3d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( ( psi ` ( x / n ) ) x. ( log ` x ) ) - ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) = ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) - ( ( psi ` ( x / n ) ) x. ( log ` x ) ) ) )
228 226 227 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) = ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) - ( ( psi ` ( x / n ) ) x. ( log ` x ) ) ) )
229 228 oveq2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) = ( ( Lam ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) - ( ( psi ` ( x / n ) ) x. ( log ` x ) ) ) ) )
230 115 210 216 mulassd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) = ( ( Lam ` n ) x. ( ( psi ` ( x / n ) ) x. ( log ` x ) ) ) )
231 230 oveq2d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) - ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) = ( ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) - ( ( Lam ` n ) x. ( ( psi ` ( x / n ) ) x. ( log ` x ) ) ) ) )
232 220 229 231 3eqtr4d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) = ( ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) - ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) )
233 232 sumeq2dv 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) - ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) )
234 fveq2 
 |-  ( n = m -> ( Lam ` n ) = ( Lam ` m ) )
235 oveq2 
 |-  ( n = m -> ( x / n ) = ( x / m ) )
236 235 fveq2d 
 |-  ( n = m -> ( psi ` ( x / n ) ) = ( psi ` ( x / m ) ) )
237 234 236 oveq12d 
 |-  ( n = m -> ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) = ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) )
238 fveq2 
 |-  ( n = m -> ( log ` n ) = ( log ` m ) )
239 237 238 oveq12d 
 |-  ( n = m -> ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) = ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) )
240 239 cbvsumv 
 |-  sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) = sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) )
241 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` ( x / m ) ) ) -> n e. NN )
242 241 adantl 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> n e. NN )
243 242 11 syl 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( Lam ` n ) e. RR )
244 243 recnd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) /\ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ) -> ( Lam ` n ) e. CC )
245 244 anasss 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ ( m e. ( 1 ... ( |_ ` x ) ) /\ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ) ) -> ( Lam ` n ) e. CC )
246 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` x ) ) -> m e. NN )
247 246 adantl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m e. NN )
248 247 119 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` m ) e. RR )
249 248 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` m ) e. CC )
250 247 nnrpd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> m e. RR+ )
251 250 relogcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` m ) e. RR )
252 251 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` m ) e. CC )
253 249 252 mulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` m ) x. ( log ` m ) ) e. CC )
254 253 adantrr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ ( m e. ( 1 ... ( |_ ` x ) ) /\ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ) ) -> ( ( Lam ` m ) x. ( log ` m ) ) e. CC )
255 245 254 mulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ ( m e. ( 1 ... ( |_ ` x ) ) /\ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ) ) -> ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) e. CC )
256 37 255 fsumfldivdiag 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
257 37 adantr 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
258 257 247 nndivred 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( x / m ) e. RR )
259 chpcl 
 |-  ( ( x / m ) e. RR -> ( psi ` ( x / m ) ) e. RR )
260 258 259 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / m ) ) e. RR )
261 260 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / m ) ) e. CC )
262 249 261 252 mul32d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) = ( ( ( Lam ` m ) x. ( log ` m ) ) x. ( psi ` ( x / m ) ) ) )
263 248 251 remulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` m ) x. ( log ` m ) ) e. RR )
264 263 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` m ) x. ( log ` m ) ) e. CC )
265 264 261 mulcomd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` m ) x. ( log ` m ) ) x. ( psi ` ( x / m ) ) ) = ( ( psi ` ( x / m ) ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
266 chpval 
 |-  ( ( x / m ) e. RR -> ( psi ` ( x / m ) ) = sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( Lam ` n ) )
267 258 266 syl 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( x / m ) ) = sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( Lam ` n ) )
268 267 oveq1d 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / m ) ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
269 fzfid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / m ) ) ) e. Fin )
270 269 264 244 fsummulc1 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) = sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
271 268 270 eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( x / m ) ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) = sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
272 262 265 271 3eqtrd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ m e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) = sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
273 272 sumeq2dv 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) = sum_ m e. ( 1 ... ( |_ ` x ) ) sum_ n e. ( 1 ... ( |_ ` ( x / m ) ) ) ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
274 123 recnd 
 |-  ( ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( Lam ` m ) x. ( log ` m ) ) e. CC )
275 116 115 274 fsummulc2 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
276 275 sumeq2dv 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` n ) x. ( ( Lam ` m ) x. ( log ` m ) ) ) )
277 256 273 276 3eqtr4d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ m e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` m ) x. ( psi ` ( x / m ) ) ) x. ( log ` m ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) )
278 240 277 eqtrid 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) )
279 115 210 211 mulassd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) = ( ( Lam ` n ) x. ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) )
280 279 sumeq2dv 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) )
281 278 280 oveq12d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) )
282 105 2timesd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) )
283 115 209 mulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) e. CC )
284 115 212 mulcld 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) e. CC )
285 8 283 284 fsumadd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) + ( ( Lam ` n ) x. ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) )
286 281 282 285 3eqtr4d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) + ( ( Lam ` n ) x. ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) )
287 115 209 212 adddid 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) = ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) + ( ( Lam ` n ) x. ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) )
288 287 sumeq2dv 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) ) + ( ( Lam ` n ) x. ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) )
289 286 288 eqtr4d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) )
290 92 recnd 
 |-  ( ( ( ph /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) e. CC )
291 8 27 290 fsummulc1 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) )
292 289 291 oveq12d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) + ( ( psi ` ( x / n ) ) x. ( log ` n ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) )
293 218 233 292 3eqtr4rd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) )
294 293 fveq2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) ) = ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) x. ( log ` m ) ) - ( ( psi ` ( x / n ) ) x. ( log ` ( x / n ) ) ) ) ) ) )
295 25 24 203 mulassd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. A ) x. x ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A x. x ) ) )
296 208 294 295 3brtr4d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) ) <_ ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. A ) x. x ) )
297 110 114 44 ledivmul2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) ) / x ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. A ) <-> ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) ) <_ ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. A ) x. x ) ) )
298 296 297 mpbird 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) ) / x ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. A ) )
299 112 114 26 298 lediv1dd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) ) / x ) / ( log ` x ) ) <_ ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. A ) / ( log ` x ) ) )
300 110 recnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) ) e. CC )
301 300 203 27 111 30 divdiv1d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) ) / x ) / ( log ` x ) ) = ( ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) ) / ( x x. ( log ` x ) ) ) )
302 109 27 203 30 111 divdiv32d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) / ( log ` x ) ) / x ) = ( ( ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) / x ) / ( log ` x ) ) )
303 106 108 27 30 divsubdird 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) / ( log ` x ) ) = ( ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) / ( log ` x ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) / ( log ` x ) ) ) )
304 104 105 27 30 div23d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) / ( log ` x ) ) = ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) )
305 107 27 30 divcan4d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) / ( log ` x ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) )
306 304 305 oveq12d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) / ( log ` x ) ) - ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) / ( log ` x ) ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) )
307 303 306 eqtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) / ( log ` x ) ) = ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) )
308 307 oveq1d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) / ( log ` x ) ) / x ) = ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) )
309 109 203 27 111 30 divdiv1d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) / x ) / ( log ` x ) ) = ( ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) / ( x x. ( log ` x ) ) ) )
310 302 308 309 3eqtr3d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) = ( ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) / ( x x. ( log ` x ) ) ) )
311 310 fveq2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) ) = ( abs ` ( ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) / ( x x. ( log ` x ) ) ) ) )
312 44 26 rpmulcld 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. RR+ )
313 312 rpcnd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. CC )
314 312 rpne0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) =/= 0 )
315 109 313 314 absdivd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) / ( x x. ( log ` x ) ) ) ) = ( ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) ) / ( abs ` ( x x. ( log ` x ) ) ) ) )
316 312 rpred 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( x x. ( log ` x ) ) e. RR )
317 312 rpge0d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( x x. ( log ` x ) ) )
318 316 317 absidd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( x x. ( log ` x ) ) ) = ( x x. ( log ` x ) ) )
319 318 oveq2d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) ) / ( abs ` ( x x. ( log ` x ) ) ) ) = ( ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) ) / ( x x. ( log ` x ) ) ) )
320 311 315 319 3eqtrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) ) = ( ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) ) / ( x x. ( log ` x ) ) ) )
321 301 320 eqtr4d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` x ) ) ) ) / x ) / ( log ` x ) ) = ( abs ` ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) ) )
322 25 24 27 30 divassd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. A ) / ( log ` x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A / ( log ` x ) ) ) )
323 299 321 322 3brtr3d 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A / ( log ` x ) ) ) )
324 22 leabsd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A / ( log ` x ) ) ) <_ ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A / ( log ` x ) ) ) ) )
325 102 22 103 323 324 letrd 
 |-  ( ( ph /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) ) <_ ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A / ( log ` x ) ) ) ) )
326 325 adantrr 
 |-  ( ( ph /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( abs ` ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) ) <_ ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. ( A / ( log ` x ) ) ) ) )
327 3 84 22 101 326 o1le 
 |-  ( ph -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( 2 / ( log ` x ) ) x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) x. ( log ` n ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( psi ` ( x / n ) ) ) ) / x ) ) e. O(1) )