Step |
Hyp |
Ref |
Expression |
1 |
|
rpre |
|- ( x e. RR+ -> x e. RR ) |
2 |
|
chpcl |
|- ( x e. RR -> ( psi ` x ) e. RR ) |
3 |
1 2
|
syl |
|- ( x e. RR+ -> ( psi ` x ) e. RR ) |
4 |
3
|
recnd |
|- ( x e. RR+ -> ( psi ` x ) e. CC ) |
5 |
|
rprege0 |
|- ( x e. RR+ -> ( x e. RR /\ 0 <_ x ) ) |
6 |
|
flge0nn0 |
|- ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 ) |
7 |
5 6
|
syl |
|- ( x e. RR+ -> ( |_ ` x ) e. NN0 ) |
8 |
|
nn0p1nn |
|- ( ( |_ ` x ) e. NN0 -> ( ( |_ ` x ) + 1 ) e. NN ) |
9 |
7 8
|
syl |
|- ( x e. RR+ -> ( ( |_ ` x ) + 1 ) e. NN ) |
10 |
9
|
nnrpd |
|- ( x e. RR+ -> ( ( |_ ` x ) + 1 ) e. RR+ ) |
11 |
10
|
relogcld |
|- ( x e. RR+ -> ( log ` ( ( |_ ` x ) + 1 ) ) e. RR ) |
12 |
11
|
recnd |
|- ( x e. RR+ -> ( log ` ( ( |_ ` x ) + 1 ) ) e. CC ) |
13 |
|
relogcl |
|- ( x e. RR+ -> ( log ` x ) e. RR ) |
14 |
13
|
recnd |
|- ( x e. RR+ -> ( log ` x ) e. CC ) |
15 |
12 14
|
subcld |
|- ( x e. RR+ -> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) e. CC ) |
16 |
4 15
|
mulcld |
|- ( x e. RR+ -> ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) e. CC ) |
17 |
|
fzfid |
|- ( x e. RR+ -> ( 1 ... ( |_ ` x ) ) e. Fin ) |
18 |
|
elfznn |
|- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN ) |
19 |
18
|
adantl |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN ) |
20 |
19
|
nnrpd |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ ) |
21 |
|
1rp |
|- 1 e. RR+ |
22 |
|
rpaddcl |
|- ( ( n e. RR+ /\ 1 e. RR+ ) -> ( n + 1 ) e. RR+ ) |
23 |
21 22
|
mpan2 |
|- ( n e. RR+ -> ( n + 1 ) e. RR+ ) |
24 |
23
|
relogcld |
|- ( n e. RR+ -> ( log ` ( n + 1 ) ) e. RR ) |
25 |
|
relogcl |
|- ( n e. RR+ -> ( log ` n ) e. RR ) |
26 |
24 25
|
resubcld |
|- ( n e. RR+ -> ( ( log ` ( n + 1 ) ) - ( log ` n ) ) e. RR ) |
27 |
|
rpre |
|- ( n e. RR+ -> n e. RR ) |
28 |
|
chpcl |
|- ( n e. RR -> ( psi ` n ) e. RR ) |
29 |
27 28
|
syl |
|- ( n e. RR+ -> ( psi ` n ) e. RR ) |
30 |
26 29
|
remulcld |
|- ( n e. RR+ -> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) e. RR ) |
31 |
30
|
recnd |
|- ( n e. RR+ -> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) e. CC ) |
32 |
20 31
|
syl |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) e. CC ) |
33 |
17 32
|
fsumcl |
|- ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) e. CC ) |
34 |
|
rpcnne0 |
|- ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) ) |
35 |
|
divsubdir |
|- ( ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) e. CC /\ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) / x ) = ( ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) / x ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) ) ) |
36 |
16 33 34 35
|
syl3anc |
|- ( x e. RR+ -> ( ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) / x ) = ( ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) / x ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) ) ) |
37 |
4 12
|
mulcld |
|- ( x e. RR+ -> ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) e. CC ) |
38 |
4 14
|
mulcld |
|- ( x e. RR+ -> ( ( psi ` x ) x. ( log ` x ) ) e. CC ) |
39 |
37 38 33
|
sub32d |
|- ( x e. RR+ -> ( ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) = ( ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) ) |
40 |
4 12 14
|
subdid |
|- ( x e. RR+ -> ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) = ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) ) |
41 |
40
|
oveq1d |
|- ( x e. RR+ -> ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) = ( ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) ) |
42 |
|
fveq2 |
|- ( m = n -> ( log ` m ) = ( log ` n ) ) |
43 |
|
fvoveq1 |
|- ( m = n -> ( psi ` ( m - 1 ) ) = ( psi ` ( n - 1 ) ) ) |
44 |
42 43
|
jca |
|- ( m = n -> ( ( log ` m ) = ( log ` n ) /\ ( psi ` ( m - 1 ) ) = ( psi ` ( n - 1 ) ) ) ) |
45 |
|
fveq2 |
|- ( m = ( n + 1 ) -> ( log ` m ) = ( log ` ( n + 1 ) ) ) |
46 |
|
fvoveq1 |
|- ( m = ( n + 1 ) -> ( psi ` ( m - 1 ) ) = ( psi ` ( ( n + 1 ) - 1 ) ) ) |
47 |
45 46
|
jca |
|- ( m = ( n + 1 ) -> ( ( log ` m ) = ( log ` ( n + 1 ) ) /\ ( psi ` ( m - 1 ) ) = ( psi ` ( ( n + 1 ) - 1 ) ) ) ) |
48 |
|
fveq2 |
|- ( m = 1 -> ( log ` m ) = ( log ` 1 ) ) |
49 |
|
log1 |
|- ( log ` 1 ) = 0 |
50 |
48 49
|
eqtrdi |
|- ( m = 1 -> ( log ` m ) = 0 ) |
51 |
|
oveq1 |
|- ( m = 1 -> ( m - 1 ) = ( 1 - 1 ) ) |
52 |
|
1m1e0 |
|- ( 1 - 1 ) = 0 |
53 |
51 52
|
eqtrdi |
|- ( m = 1 -> ( m - 1 ) = 0 ) |
54 |
53
|
fveq2d |
|- ( m = 1 -> ( psi ` ( m - 1 ) ) = ( psi ` 0 ) ) |
55 |
|
2pos |
|- 0 < 2 |
56 |
|
0re |
|- 0 e. RR |
57 |
|
chpeq0 |
|- ( 0 e. RR -> ( ( psi ` 0 ) = 0 <-> 0 < 2 ) ) |
58 |
56 57
|
ax-mp |
|- ( ( psi ` 0 ) = 0 <-> 0 < 2 ) |
59 |
55 58
|
mpbir |
|- ( psi ` 0 ) = 0 |
60 |
54 59
|
eqtrdi |
|- ( m = 1 -> ( psi ` ( m - 1 ) ) = 0 ) |
61 |
50 60
|
jca |
|- ( m = 1 -> ( ( log ` m ) = 0 /\ ( psi ` ( m - 1 ) ) = 0 ) ) |
62 |
|
fveq2 |
|- ( m = ( ( |_ ` x ) + 1 ) -> ( log ` m ) = ( log ` ( ( |_ ` x ) + 1 ) ) ) |
63 |
|
fvoveq1 |
|- ( m = ( ( |_ ` x ) + 1 ) -> ( psi ` ( m - 1 ) ) = ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) |
64 |
62 63
|
jca |
|- ( m = ( ( |_ ` x ) + 1 ) -> ( ( log ` m ) = ( log ` ( ( |_ ` x ) + 1 ) ) /\ ( psi ` ( m - 1 ) ) = ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) ) |
65 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
66 |
9 65
|
eleqtrdi |
|- ( x e. RR+ -> ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` 1 ) ) |
67 |
|
elfznn |
|- ( m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) -> m e. NN ) |
68 |
67
|
adantl |
|- ( ( x e. RR+ /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. NN ) |
69 |
68
|
nnrpd |
|- ( ( x e. RR+ /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. RR+ ) |
70 |
69
|
relogcld |
|- ( ( x e. RR+ /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( log ` m ) e. RR ) |
71 |
70
|
recnd |
|- ( ( x e. RR+ /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( log ` m ) e. CC ) |
72 |
68
|
nnred |
|- ( ( x e. RR+ /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. RR ) |
73 |
|
peano2rem |
|- ( m e. RR -> ( m - 1 ) e. RR ) |
74 |
72 73
|
syl |
|- ( ( x e. RR+ /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( m - 1 ) e. RR ) |
75 |
|
chpcl |
|- ( ( m - 1 ) e. RR -> ( psi ` ( m - 1 ) ) e. RR ) |
76 |
74 75
|
syl |
|- ( ( x e. RR+ /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( psi ` ( m - 1 ) ) e. RR ) |
77 |
76
|
recnd |
|- ( ( x e. RR+ /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( psi ` ( m - 1 ) ) e. CC ) |
78 |
44 47 61 64 66 71 77
|
fsumparts |
|- ( x e. RR+ -> sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( log ` n ) x. ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( psi ` ( n - 1 ) ) ) ) = ( ( ( ( log ` ( ( |_ ` x ) + 1 ) ) x. ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) - ( 0 x. 0 ) ) - sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` ( ( n + 1 ) - 1 ) ) ) ) ) |
79 |
7
|
nn0zd |
|- ( x e. RR+ -> ( |_ ` x ) e. ZZ ) |
80 |
|
fzval3 |
|- ( ( |_ ` x ) e. ZZ -> ( 1 ... ( |_ ` x ) ) = ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ) |
81 |
79 80
|
syl |
|- ( x e. RR+ -> ( 1 ... ( |_ ` x ) ) = ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ) |
82 |
81
|
eqcomd |
|- ( x e. RR+ -> ( 1 ..^ ( ( |_ ` x ) + 1 ) ) = ( 1 ... ( |_ ` x ) ) ) |
83 |
|
nnm1nn0 |
|- ( n e. NN -> ( n - 1 ) e. NN0 ) |
84 |
19 83
|
syl |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n - 1 ) e. NN0 ) |
85 |
84
|
nn0red |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n - 1 ) e. RR ) |
86 |
|
chpcl |
|- ( ( n - 1 ) e. RR -> ( psi ` ( n - 1 ) ) e. RR ) |
87 |
85 86
|
syl |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( n - 1 ) ) e. RR ) |
88 |
87
|
recnd |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( n - 1 ) ) e. CC ) |
89 |
|
vmacl |
|- ( n e. NN -> ( Lam ` n ) e. RR ) |
90 |
19 89
|
syl |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR ) |
91 |
90
|
recnd |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. CC ) |
92 |
19
|
nncnd |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC ) |
93 |
|
ax-1cn |
|- 1 e. CC |
94 |
|
pncan |
|- ( ( n e. CC /\ 1 e. CC ) -> ( ( n + 1 ) - 1 ) = n ) |
95 |
92 93 94
|
sylancl |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) - 1 ) = n ) |
96 |
|
npcan |
|- ( ( n e. CC /\ 1 e. CC ) -> ( ( n - 1 ) + 1 ) = n ) |
97 |
92 93 96
|
sylancl |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n - 1 ) + 1 ) = n ) |
98 |
95 97
|
eqtr4d |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) - 1 ) = ( ( n - 1 ) + 1 ) ) |
99 |
98
|
fveq2d |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( ( n + 1 ) - 1 ) ) = ( psi ` ( ( n - 1 ) + 1 ) ) ) |
100 |
|
chpp1 |
|- ( ( n - 1 ) e. NN0 -> ( psi ` ( ( n - 1 ) + 1 ) ) = ( ( psi ` ( n - 1 ) ) + ( Lam ` ( ( n - 1 ) + 1 ) ) ) ) |
101 |
84 100
|
syl |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( ( n - 1 ) + 1 ) ) = ( ( psi ` ( n - 1 ) ) + ( Lam ` ( ( n - 1 ) + 1 ) ) ) ) |
102 |
97
|
fveq2d |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` ( ( n - 1 ) + 1 ) ) = ( Lam ` n ) ) |
103 |
102
|
oveq2d |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( n - 1 ) ) + ( Lam ` ( ( n - 1 ) + 1 ) ) ) = ( ( psi ` ( n - 1 ) ) + ( Lam ` n ) ) ) |
104 |
99 101 103
|
3eqtrd |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( ( n + 1 ) - 1 ) ) = ( ( psi ` ( n - 1 ) ) + ( Lam ` n ) ) ) |
105 |
88 91 104
|
mvrladdd |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( psi ` ( n - 1 ) ) ) = ( Lam ` n ) ) |
106 |
105
|
oveq2d |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` n ) x. ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( psi ` ( n - 1 ) ) ) ) = ( ( log ` n ) x. ( Lam ` n ) ) ) |
107 |
20
|
relogcld |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR ) |
108 |
107
|
recnd |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. CC ) |
109 |
91 108
|
mulcomd |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( log ` n ) ) = ( ( log ` n ) x. ( Lam ` n ) ) ) |
110 |
106 109
|
eqtr4d |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` n ) x. ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( psi ` ( n - 1 ) ) ) ) = ( ( Lam ` n ) x. ( log ` n ) ) ) |
111 |
82 110
|
sumeq12rdv |
|- ( x e. RR+ -> sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( log ` n ) x. ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( psi ` ( n - 1 ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) ) |
112 |
7
|
nn0cnd |
|- ( x e. RR+ -> ( |_ ` x ) e. CC ) |
113 |
|
pncan |
|- ( ( ( |_ ` x ) e. CC /\ 1 e. CC ) -> ( ( ( |_ ` x ) + 1 ) - 1 ) = ( |_ ` x ) ) |
114 |
112 93 113
|
sylancl |
|- ( x e. RR+ -> ( ( ( |_ ` x ) + 1 ) - 1 ) = ( |_ ` x ) ) |
115 |
114
|
fveq2d |
|- ( x e. RR+ -> ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( psi ` ( |_ ` x ) ) ) |
116 |
|
chpfl |
|- ( x e. RR -> ( psi ` ( |_ ` x ) ) = ( psi ` x ) ) |
117 |
1 116
|
syl |
|- ( x e. RR+ -> ( psi ` ( |_ ` x ) ) = ( psi ` x ) ) |
118 |
115 117
|
eqtrd |
|- ( x e. RR+ -> ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( psi ` x ) ) |
119 |
118
|
oveq2d |
|- ( x e. RR+ -> ( ( log ` ( ( |_ ` x ) + 1 ) ) x. ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) = ( ( log ` ( ( |_ ` x ) + 1 ) ) x. ( psi ` x ) ) ) |
120 |
12 4
|
mulcomd |
|- ( x e. RR+ -> ( ( log ` ( ( |_ ` x ) + 1 ) ) x. ( psi ` x ) ) = ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) ) |
121 |
119 120
|
eqtrd |
|- ( x e. RR+ -> ( ( log ` ( ( |_ ` x ) + 1 ) ) x. ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) = ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) ) |
122 |
|
0cn |
|- 0 e. CC |
123 |
122
|
mul01i |
|- ( 0 x. 0 ) = 0 |
124 |
123
|
a1i |
|- ( x e. RR+ -> ( 0 x. 0 ) = 0 ) |
125 |
121 124
|
oveq12d |
|- ( x e. RR+ -> ( ( ( log ` ( ( |_ ` x ) + 1 ) ) x. ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) - ( 0 x. 0 ) ) = ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - 0 ) ) |
126 |
37
|
subid1d |
|- ( x e. RR+ -> ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - 0 ) = ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) ) |
127 |
125 126
|
eqtrd |
|- ( x e. RR+ -> ( ( ( log ` ( ( |_ ` x ) + 1 ) ) x. ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) - ( 0 x. 0 ) ) = ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) ) |
128 |
95
|
fveq2d |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( ( n + 1 ) - 1 ) ) = ( psi ` n ) ) |
129 |
128
|
oveq2d |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` ( ( n + 1 ) - 1 ) ) ) = ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) |
130 |
82 129
|
sumeq12rdv |
|- ( x e. RR+ -> sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` ( ( n + 1 ) - 1 ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) |
131 |
127 130
|
oveq12d |
|- ( x e. RR+ -> ( ( ( ( log ` ( ( |_ ` x ) + 1 ) ) x. ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) - ( 0 x. 0 ) ) - sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` ( ( n + 1 ) - 1 ) ) ) ) = ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) ) |
132 |
78 111 131
|
3eqtr3d |
|- ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) = ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) ) |
133 |
132
|
oveq1d |
|- ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) = ( ( ( ( psi ` x ) x. ( log ` ( ( |_ ` x ) + 1 ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) ) |
134 |
39 41 133
|
3eqtr4d |
|- ( x e. RR+ -> ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) ) |
135 |
134
|
oveq1d |
|- ( x e. RR+ -> ( ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) / x ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) |
136 |
|
div23 |
|- ( ( ( psi ` x ) e. CC /\ ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) / x ) = ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) ) |
137 |
4 15 34 136
|
syl3anc |
|- ( x e. RR+ -> ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) / x ) = ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) ) |
138 |
137
|
oveq1d |
|- ( x e. RR+ -> ( ( ( ( psi ` x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) / x ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) ) = ( ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) ) ) |
139 |
36 135 138
|
3eqtr3rd |
|- ( x e. RR+ -> ( ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) |
140 |
139
|
mpteq2ia |
|- ( x e. RR+ |-> ( ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) ) ) = ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) |
141 |
|
ovexd |
|- ( ( T. /\ x e. RR+ ) -> ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) e. _V ) |
142 |
|
ovexd |
|- ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) e. _V ) |
143 |
|
reex |
|- RR e. _V |
144 |
|
rpssre |
|- RR+ C_ RR |
145 |
143 144
|
ssexi |
|- RR+ e. _V |
146 |
145
|
a1i |
|- ( T. -> RR+ e. _V ) |
147 |
|
ovexd |
|- ( ( T. /\ x e. RR+ ) -> ( ( psi ` x ) / x ) e. _V ) |
148 |
15
|
adantl |
|- ( ( T. /\ x e. RR+ ) -> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) e. CC ) |
149 |
|
eqidd |
|- ( T. -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) = ( x e. RR+ |-> ( ( psi ` x ) / x ) ) ) |
150 |
|
eqidd |
|- ( T. -> ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) = ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) ) |
151 |
146 147 148 149 150
|
offval2 |
|- ( T. -> ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) oF x. ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) ) = ( x e. RR+ |-> ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) ) ) |
152 |
|
chpo1ub |
|- ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1) |
153 |
|
0red |
|- ( T. -> 0 e. RR ) |
154 |
|
1red |
|- ( T. -> 1 e. RR ) |
155 |
|
divrcnv |
|- ( 1 e. CC -> ( x e. RR+ |-> ( 1 / x ) ) ~~>r 0 ) |
156 |
93 155
|
mp1i |
|- ( T. -> ( x e. RR+ |-> ( 1 / x ) ) ~~>r 0 ) |
157 |
|
rpreccl |
|- ( x e. RR+ -> ( 1 / x ) e. RR+ ) |
158 |
157
|
rpred |
|- ( x e. RR+ -> ( 1 / x ) e. RR ) |
159 |
158
|
adantl |
|- ( ( T. /\ x e. RR+ ) -> ( 1 / x ) e. RR ) |
160 |
11 13
|
resubcld |
|- ( x e. RR+ -> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) e. RR ) |
161 |
160
|
adantl |
|- ( ( T. /\ x e. RR+ ) -> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) e. RR ) |
162 |
|
rpaddcl |
|- ( ( x e. RR+ /\ 1 e. RR+ ) -> ( x + 1 ) e. RR+ ) |
163 |
21 162
|
mpan2 |
|- ( x e. RR+ -> ( x + 1 ) e. RR+ ) |
164 |
163
|
relogcld |
|- ( x e. RR+ -> ( log ` ( x + 1 ) ) e. RR ) |
165 |
164 13
|
resubcld |
|- ( x e. RR+ -> ( ( log ` ( x + 1 ) ) - ( log ` x ) ) e. RR ) |
166 |
7
|
nn0red |
|- ( x e. RR+ -> ( |_ ` x ) e. RR ) |
167 |
|
1red |
|- ( x e. RR+ -> 1 e. RR ) |
168 |
|
flle |
|- ( x e. RR -> ( |_ ` x ) <_ x ) |
169 |
1 168
|
syl |
|- ( x e. RR+ -> ( |_ ` x ) <_ x ) |
170 |
166 1 167 169
|
leadd1dd |
|- ( x e. RR+ -> ( ( |_ ` x ) + 1 ) <_ ( x + 1 ) ) |
171 |
10 163
|
logled |
|- ( x e. RR+ -> ( ( ( |_ ` x ) + 1 ) <_ ( x + 1 ) <-> ( log ` ( ( |_ ` x ) + 1 ) ) <_ ( log ` ( x + 1 ) ) ) ) |
172 |
170 171
|
mpbid |
|- ( x e. RR+ -> ( log ` ( ( |_ ` x ) + 1 ) ) <_ ( log ` ( x + 1 ) ) ) |
173 |
11 164 13 172
|
lesub1dd |
|- ( x e. RR+ -> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) <_ ( ( log ` ( x + 1 ) ) - ( log ` x ) ) ) |
174 |
|
logdifbnd |
|- ( x e. RR+ -> ( ( log ` ( x + 1 ) ) - ( log ` x ) ) <_ ( 1 / x ) ) |
175 |
160 165 158 173 174
|
letrd |
|- ( x e. RR+ -> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) <_ ( 1 / x ) ) |
176 |
175
|
ad2antrl |
|- ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) <_ ( 1 / x ) ) |
177 |
|
fllep1 |
|- ( x e. RR -> x <_ ( ( |_ ` x ) + 1 ) ) |
178 |
1 177
|
syl |
|- ( x e. RR+ -> x <_ ( ( |_ ` x ) + 1 ) ) |
179 |
|
logleb |
|- ( ( x e. RR+ /\ ( ( |_ ` x ) + 1 ) e. RR+ ) -> ( x <_ ( ( |_ ` x ) + 1 ) <-> ( log ` x ) <_ ( log ` ( ( |_ ` x ) + 1 ) ) ) ) |
180 |
10 179
|
mpdan |
|- ( x e. RR+ -> ( x <_ ( ( |_ ` x ) + 1 ) <-> ( log ` x ) <_ ( log ` ( ( |_ ` x ) + 1 ) ) ) ) |
181 |
178 180
|
mpbid |
|- ( x e. RR+ -> ( log ` x ) <_ ( log ` ( ( |_ ` x ) + 1 ) ) ) |
182 |
11 13
|
subge0d |
|- ( x e. RR+ -> ( 0 <_ ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) <-> ( log ` x ) <_ ( log ` ( ( |_ ` x ) + 1 ) ) ) ) |
183 |
181 182
|
mpbird |
|- ( x e. RR+ -> 0 <_ ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) |
184 |
183
|
ad2antrl |
|- ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 <_ ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) |
185 |
153 154 156 159 161 176 184
|
rlimsqz2 |
|- ( T. -> ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) ~~>r 0 ) |
186 |
|
rlimo1 |
|- ( ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) ~~>r 0 -> ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) e. O(1) ) |
187 |
185 186
|
syl |
|- ( T. -> ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) e. O(1) ) |
188 |
|
o1mul |
|- ( ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1) /\ ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) e. O(1) ) -> ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) oF x. ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) ) e. O(1) ) |
189 |
152 187 188
|
sylancr |
|- ( T. -> ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) oF x. ( x e. RR+ |-> ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) ) e. O(1) ) |
190 |
151 189
|
eqeltrrd |
|- ( T. -> ( x e. RR+ |-> ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) ) e. O(1) ) |
191 |
|
nnrp |
|- ( m e. NN -> m e. RR+ ) |
192 |
191
|
ssriv |
|- NN C_ RR+ |
193 |
192
|
a1i |
|- ( T. -> NN C_ RR+ ) |
194 |
193
|
sselda |
|- ( ( T. /\ n e. NN ) -> n e. RR+ ) |
195 |
194 31
|
syl |
|- ( ( T. /\ n e. NN ) -> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) e. CC ) |
196 |
|
chpo1ub |
|- ( n e. RR+ |-> ( ( psi ` n ) / n ) ) e. O(1) |
197 |
196
|
a1i |
|- ( T. -> ( n e. RR+ |-> ( ( psi ` n ) / n ) ) e. O(1) ) |
198 |
|
rerpdivcl |
|- ( ( ( psi ` n ) e. RR /\ n e. RR+ ) -> ( ( psi ` n ) / n ) e. RR ) |
199 |
29 198
|
mpancom |
|- ( n e. RR+ -> ( ( psi ` n ) / n ) e. RR ) |
200 |
199
|
adantl |
|- ( ( T. /\ n e. RR+ ) -> ( ( psi ` n ) / n ) e. RR ) |
201 |
31
|
adantl |
|- ( ( T. /\ n e. RR+ ) -> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) e. CC ) |
202 |
|
rpreccl |
|- ( n e. RR+ -> ( 1 / n ) e. RR+ ) |
203 |
202
|
rpred |
|- ( n e. RR+ -> ( 1 / n ) e. RR ) |
204 |
|
chpge0 |
|- ( n e. RR -> 0 <_ ( psi ` n ) ) |
205 |
27 204
|
syl |
|- ( n e. RR+ -> 0 <_ ( psi ` n ) ) |
206 |
|
logdifbnd |
|- ( n e. RR+ -> ( ( log ` ( n + 1 ) ) - ( log ` n ) ) <_ ( 1 / n ) ) |
207 |
26 203 29 205 206
|
lemul1ad |
|- ( n e. RR+ -> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) <_ ( ( 1 / n ) x. ( psi ` n ) ) ) |
208 |
27
|
lep1d |
|- ( n e. RR+ -> n <_ ( n + 1 ) ) |
209 |
|
logleb |
|- ( ( n e. RR+ /\ ( n + 1 ) e. RR+ ) -> ( n <_ ( n + 1 ) <-> ( log ` n ) <_ ( log ` ( n + 1 ) ) ) ) |
210 |
23 209
|
mpdan |
|- ( n e. RR+ -> ( n <_ ( n + 1 ) <-> ( log ` n ) <_ ( log ` ( n + 1 ) ) ) ) |
211 |
208 210
|
mpbid |
|- ( n e. RR+ -> ( log ` n ) <_ ( log ` ( n + 1 ) ) ) |
212 |
24 25
|
subge0d |
|- ( n e. RR+ -> ( 0 <_ ( ( log ` ( n + 1 ) ) - ( log ` n ) ) <-> ( log ` n ) <_ ( log ` ( n + 1 ) ) ) ) |
213 |
211 212
|
mpbird |
|- ( n e. RR+ -> 0 <_ ( ( log ` ( n + 1 ) ) - ( log ` n ) ) ) |
214 |
26 29 213 205
|
mulge0d |
|- ( n e. RR+ -> 0 <_ ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) |
215 |
30 214
|
absidd |
|- ( n e. RR+ -> ( abs ` ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) = ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) |
216 |
|
rpregt0 |
|- ( n e. RR+ -> ( n e. RR /\ 0 < n ) ) |
217 |
|
divge0 |
|- ( ( ( ( psi ` n ) e. RR /\ 0 <_ ( psi ` n ) ) /\ ( n e. RR /\ 0 < n ) ) -> 0 <_ ( ( psi ` n ) / n ) ) |
218 |
29 205 216 217
|
syl21anc |
|- ( n e. RR+ -> 0 <_ ( ( psi ` n ) / n ) ) |
219 |
199 218
|
absidd |
|- ( n e. RR+ -> ( abs ` ( ( psi ` n ) / n ) ) = ( ( psi ` n ) / n ) ) |
220 |
29
|
recnd |
|- ( n e. RR+ -> ( psi ` n ) e. CC ) |
221 |
|
rpcn |
|- ( n e. RR+ -> n e. CC ) |
222 |
|
rpne0 |
|- ( n e. RR+ -> n =/= 0 ) |
223 |
220 221 222
|
divrec2d |
|- ( n e. RR+ -> ( ( psi ` n ) / n ) = ( ( 1 / n ) x. ( psi ` n ) ) ) |
224 |
219 223
|
eqtrd |
|- ( n e. RR+ -> ( abs ` ( ( psi ` n ) / n ) ) = ( ( 1 / n ) x. ( psi ` n ) ) ) |
225 |
207 215 224
|
3brtr4d |
|- ( n e. RR+ -> ( abs ` ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) <_ ( abs ` ( ( psi ` n ) / n ) ) ) |
226 |
225
|
ad2antrl |
|- ( ( T. /\ ( n e. RR+ /\ 1 <_ n ) ) -> ( abs ` ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) <_ ( abs ` ( ( psi ` n ) / n ) ) ) |
227 |
154 197 200 201 226
|
o1le |
|- ( T. -> ( n e. RR+ |-> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) e. O(1) ) |
228 |
193 227
|
o1res2 |
|- ( T. -> ( n e. NN |-> ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) ) e. O(1) ) |
229 |
195 228
|
o1fsum |
|- ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) ) e. O(1) ) |
230 |
141 142 190 229
|
o1sub2 |
|- ( T. -> ( x e. RR+ |-> ( ( ( ( psi ` x ) / x ) x. ( ( log ` ( ( |_ ` x ) + 1 ) ) - ( log ` x ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( n + 1 ) ) - ( log ` n ) ) x. ( psi ` n ) ) / x ) ) ) e. O(1) ) |
231 |
140 230
|
eqeltrrid |
|- ( T. -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) e. O(1) ) |
232 |
231
|
mptru |
|- ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( log ` n ) ) - ( ( psi ` x ) x. ( log ` x ) ) ) / x ) ) e. O(1) |