Step |
Hyp |
Ref |
Expression |
1 |
|
reex |
|- RR e. _V |
2 |
|
rpssre |
|- RR+ C_ RR |
3 |
1 2
|
ssexi |
|- RR+ e. _V |
4 |
3
|
a1i |
|- ( T. -> RR+ e. _V ) |
5 |
|
ovexd |
|- ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) e. _V ) |
6 |
|
ovexd |
|- ( ( T. /\ x e. RR+ ) -> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) e. _V ) |
7 |
|
eqidd |
|- ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ) |
8 |
|
eqidd |
|- ( T. -> ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) = ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ) |
9 |
4 5 6 7 8
|
offval2 |
|- ( T. -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) oF - ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ) = ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) - ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ) ) |
10 |
9
|
mptru |
|- ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) oF - ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ) = ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) - ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ) |
11 |
|
fzfid |
|- ( x e. RR+ -> ( 1 ... ( |_ ` x ) ) e. Fin ) |
12 |
|
elfznn |
|- ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN ) |
13 |
12
|
adantl |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN ) |
14 |
|
vmacl |
|- ( n e. NN -> ( Lam ` n ) e. RR ) |
15 |
13 14
|
syl |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR ) |
16 |
15 13
|
nndivred |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR ) |
17 |
11 16
|
fsumrecl |
|- ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. RR ) |
18 |
17
|
recnd |
|- ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. CC ) |
19 |
|
relogcl |
|- ( x e. RR+ -> ( log ` x ) e. RR ) |
20 |
19
|
recnd |
|- ( x e. RR+ -> ( log ` x ) e. CC ) |
21 |
|
rprege0 |
|- ( x e. RR+ -> ( x e. RR /\ 0 <_ x ) ) |
22 |
|
flge0nn0 |
|- ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 ) |
23 |
|
faccl |
|- ( ( |_ ` x ) e. NN0 -> ( ! ` ( |_ ` x ) ) e. NN ) |
24 |
21 22 23
|
3syl |
|- ( x e. RR+ -> ( ! ` ( |_ ` x ) ) e. NN ) |
25 |
24
|
nnrpd |
|- ( x e. RR+ -> ( ! ` ( |_ ` x ) ) e. RR+ ) |
26 |
25
|
relogcld |
|- ( x e. RR+ -> ( log ` ( ! ` ( |_ ` x ) ) ) e. RR ) |
27 |
|
rerpdivcl |
|- ( ( ( log ` ( ! ` ( |_ ` x ) ) ) e. RR /\ x e. RR+ ) -> ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) e. RR ) |
28 |
26 27
|
mpancom |
|- ( x e. RR+ -> ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) e. RR ) |
29 |
28
|
recnd |
|- ( x e. RR+ -> ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) e. CC ) |
30 |
18 20 29
|
nnncan2d |
|- ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) - ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) |
31 |
30
|
mpteq2ia |
|- ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) - ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) |
32 |
10 31
|
eqtri |
|- ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) oF - ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) |
33 |
|
1red |
|- ( T. -> 1 e. RR ) |
34 |
|
chpo1ub |
|- ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1) |
35 |
34
|
a1i |
|- ( T. -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1) ) |
36 |
|
rpre |
|- ( x e. RR+ -> x e. RR ) |
37 |
|
chpcl |
|- ( x e. RR -> ( psi ` x ) e. RR ) |
38 |
36 37
|
syl |
|- ( x e. RR+ -> ( psi ` x ) e. RR ) |
39 |
|
rerpdivcl |
|- ( ( ( psi ` x ) e. RR /\ x e. RR+ ) -> ( ( psi ` x ) / x ) e. RR ) |
40 |
38 39
|
mpancom |
|- ( x e. RR+ -> ( ( psi ` x ) / x ) e. RR ) |
41 |
40
|
recnd |
|- ( x e. RR+ -> ( ( psi ` x ) / x ) e. CC ) |
42 |
41
|
adantl |
|- ( ( T. /\ x e. RR+ ) -> ( ( psi ` x ) / x ) e. CC ) |
43 |
18 29
|
subcld |
|- ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) e. CC ) |
44 |
43
|
adantl |
|- ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) e. CC ) |
45 |
36
|
adantr |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR ) |
46 |
16 45
|
remulcld |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. x ) e. RR ) |
47 |
|
nndivre |
|- ( ( x e. RR /\ n e. NN ) -> ( x / n ) e. RR ) |
48 |
36 12 47
|
syl2an |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR ) |
49 |
|
reflcl |
|- ( ( x / n ) e. RR -> ( |_ ` ( x / n ) ) e. RR ) |
50 |
48 49
|
syl |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( x / n ) ) e. RR ) |
51 |
15 50
|
remulcld |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) e. RR ) |
52 |
46 51
|
resubcld |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) e. RR ) |
53 |
48 50
|
resubcld |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x / n ) - ( |_ ` ( x / n ) ) ) e. RR ) |
54 |
|
1red |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR ) |
55 |
|
vmage0 |
|- ( n e. NN -> 0 <_ ( Lam ` n ) ) |
56 |
13 55
|
syl |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( Lam ` n ) ) |
57 |
|
fracle1 |
|- ( ( x / n ) e. RR -> ( ( x / n ) - ( |_ ` ( x / n ) ) ) <_ 1 ) |
58 |
48 57
|
syl |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x / n ) - ( |_ ` ( x / n ) ) ) <_ 1 ) |
59 |
53 54 15 56 58
|
lemul2ad |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( x / n ) - ( |_ ` ( x / n ) ) ) ) <_ ( ( Lam ` n ) x. 1 ) ) |
60 |
15
|
recnd |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. CC ) |
61 |
48
|
recnd |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. CC ) |
62 |
50
|
recnd |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( x / n ) ) e. CC ) |
63 |
60 61 62
|
subdid |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( x / n ) - ( |_ ` ( x / n ) ) ) ) = ( ( ( Lam ` n ) x. ( x / n ) ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) ) |
64 |
|
rpcn |
|- ( x e. RR+ -> x e. CC ) |
65 |
64
|
adantr |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC ) |
66 |
13
|
nnrpd |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ ) |
67 |
|
rpcnne0 |
|- ( n e. RR+ -> ( n e. CC /\ n =/= 0 ) ) |
68 |
66 67
|
syl |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. CC /\ n =/= 0 ) ) |
69 |
|
div23 |
|- ( ( ( Lam ` n ) e. CC /\ x e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( ( Lam ` n ) x. x ) / n ) = ( ( ( Lam ` n ) / n ) x. x ) ) |
70 |
|
divass |
|- ( ( ( Lam ` n ) e. CC /\ x e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( ( Lam ` n ) x. x ) / n ) = ( ( Lam ` n ) x. ( x / n ) ) ) |
71 |
69 70
|
eqtr3d |
|- ( ( ( Lam ` n ) e. CC /\ x e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( ( Lam ` n ) / n ) x. x ) = ( ( Lam ` n ) x. ( x / n ) ) ) |
72 |
60 65 68 71
|
syl3anc |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. x ) = ( ( Lam ` n ) x. ( x / n ) ) ) |
73 |
72
|
oveq1d |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) = ( ( ( Lam ` n ) x. ( x / n ) ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) ) |
74 |
63 73
|
eqtr4d |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( ( x / n ) - ( |_ ` ( x / n ) ) ) ) = ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) ) |
75 |
60
|
mulid1d |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. 1 ) = ( Lam ` n ) ) |
76 |
59 74 75
|
3brtr3d |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) <_ ( Lam ` n ) ) |
77 |
11 52 15 76
|
fsumle |
|- ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( Lam ` n ) ) |
78 |
16
|
recnd |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. CC ) |
79 |
11 64 78
|
fsummulc1 |
|- ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. x ) ) |
80 |
|
logfac2 |
|- ( ( x e. RR /\ 0 <_ x ) -> ( log ` ( ! ` ( |_ ` x ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) |
81 |
21 80
|
syl |
|- ( x e. RR+ -> ( log ` ( ! ` ( |_ ` x ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) |
82 |
79 81
|
oveq12d |
|- ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. x ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) ) |
83 |
46
|
recnd |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) x. x ) e. CC ) |
84 |
51
|
recnd |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) e. CC ) |
85 |
11 83 84
|
fsumsub |
|- ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. x ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) ) |
86 |
82 85
|
eqtr4d |
|- ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) ) |
87 |
|
chpval |
|- ( x e. RR -> ( psi ` x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( Lam ` n ) ) |
88 |
36 87
|
syl |
|- ( x e. RR+ -> ( psi ` x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( Lam ` n ) ) |
89 |
77 86 88
|
3brtr4d |
|- ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) <_ ( psi ` x ) ) |
90 |
17 36
|
remulcld |
|- ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) e. RR ) |
91 |
90 26
|
resubcld |
|- ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) e. RR ) |
92 |
|
rpregt0 |
|- ( x e. RR+ -> ( x e. RR /\ 0 < x ) ) |
93 |
|
lediv1 |
|- ( ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) e. RR /\ ( psi ` x ) e. RR /\ ( x e. RR /\ 0 < x ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) <_ ( psi ` x ) <-> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) <_ ( ( psi ` x ) / x ) ) ) |
94 |
91 38 92 93
|
syl3anc |
|- ( x e. RR+ -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) <_ ( psi ` x ) <-> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) <_ ( ( psi ` x ) / x ) ) ) |
95 |
89 94
|
mpbid |
|- ( x e. RR+ -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) <_ ( ( psi ` x ) / x ) ) |
96 |
90
|
recnd |
|- ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) e. CC ) |
97 |
26
|
recnd |
|- ( x e. RR+ -> ( log ` ( ! ` ( |_ ` x ) ) ) e. CC ) |
98 |
|
rpcnne0 |
|- ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) ) |
99 |
|
divsubdir |
|- ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) e. CC /\ ( log ` ( ! ` ( |_ ` x ) ) ) e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) = ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) / x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) |
100 |
96 97 98 99
|
syl3anc |
|- ( x e. RR+ -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) = ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) / x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) |
101 |
|
rpne0 |
|- ( x e. RR+ -> x =/= 0 ) |
102 |
18 64 101
|
divcan4d |
|- ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) / x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) ) |
103 |
102
|
oveq1d |
|- ( x e. RR+ -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) / x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) |
104 |
100 103
|
eqtr2d |
|- ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) = ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) ) |
105 |
104
|
fveq2d |
|- ( x e. RR+ -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) = ( abs ` ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) ) ) |
106 |
|
rerpdivcl |
|- ( ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) e. RR /\ x e. RR+ ) -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) e. RR ) |
107 |
91 106
|
mpancom |
|- ( x e. RR+ -> ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) e. RR ) |
108 |
|
flle |
|- ( ( x / n ) e. RR -> ( |_ ` ( x / n ) ) <_ ( x / n ) ) |
109 |
48 108
|
syl |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( x / n ) ) <_ ( x / n ) ) |
110 |
48 50
|
subge0d |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 0 <_ ( ( x / n ) - ( |_ ` ( x / n ) ) ) <-> ( |_ ` ( x / n ) ) <_ ( x / n ) ) ) |
111 |
109 110
|
mpbird |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( x / n ) - ( |_ ` ( x / n ) ) ) ) |
112 |
15 53 56 111
|
mulge0d |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( Lam ` n ) x. ( ( x / n ) - ( |_ ` ( x / n ) ) ) ) ) |
113 |
112 74
|
breqtrd |
|- ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) ) |
114 |
11 52 113
|
fsumge0 |
|- ( x e. RR+ -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( Lam ` n ) / n ) x. x ) - ( ( Lam ` n ) x. ( |_ ` ( x / n ) ) ) ) ) |
115 |
114 86
|
breqtrrd |
|- ( x e. RR+ -> 0 <_ ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) ) |
116 |
|
divge0 |
|- ( ( ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) e. RR /\ 0 <_ ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) ) /\ ( x e. RR /\ 0 < x ) ) -> 0 <_ ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) ) |
117 |
91 115 92 116
|
syl21anc |
|- ( x e. RR+ -> 0 <_ ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) ) |
118 |
107 117
|
absidd |
|- ( x e. RR+ -> ( abs ` ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) ) = ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) ) |
119 |
105 118
|
eqtrd |
|- ( x e. RR+ -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) = ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) x. x ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) ) |
120 |
|
chpge0 |
|- ( x e. RR -> 0 <_ ( psi ` x ) ) |
121 |
36 120
|
syl |
|- ( x e. RR+ -> 0 <_ ( psi ` x ) ) |
122 |
|
divge0 |
|- ( ( ( ( psi ` x ) e. RR /\ 0 <_ ( psi ` x ) ) /\ ( x e. RR /\ 0 < x ) ) -> 0 <_ ( ( psi ` x ) / x ) ) |
123 |
38 121 92 122
|
syl21anc |
|- ( x e. RR+ -> 0 <_ ( ( psi ` x ) / x ) ) |
124 |
40 123
|
absidd |
|- ( x e. RR+ -> ( abs ` ( ( psi ` x ) / x ) ) = ( ( psi ` x ) / x ) ) |
125 |
95 119 124
|
3brtr4d |
|- ( x e. RR+ -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) <_ ( abs ` ( ( psi ` x ) / x ) ) ) |
126 |
125
|
ad2antrl |
|- ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) <_ ( abs ` ( ( psi ` x ) / x ) ) ) |
127 |
33 35 42 44 126
|
o1le |
|- ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) e. O(1) ) |
128 |
127
|
mptru |
|- ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) e. O(1) |
129 |
|
logfacrlim |
|- ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ~~>r 1 |
130 |
|
rlimo1 |
|- ( ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ~~>r 1 -> ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) e. O(1) ) |
131 |
129 130
|
ax-mp |
|- ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) e. O(1) |
132 |
|
o1sub |
|- ( ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) e. O(1) /\ ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) e. O(1) ) -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) oF - ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ) e. O(1) ) |
133 |
128 131 132
|
mp2an |
|- ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) oF - ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ) e. O(1) |
134 |
32 133
|
eqeltrri |
|- ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) |