Metamath Proof Explorer

Theorem mulogsumlem

Description: Lemma for mulogsum . (Contributed by Mario Carneiro, 14-May-2016)

Ref Expression
Assertion mulogsumlem 
|- ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) ) e. O(1)

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( x e. RR+ -> ( 1 ... ( |_ ` x ) ) e. Fin )
2 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
3 2 adantl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
4 mucl 
 |-  ( n e. NN -> ( mmu ` n ) e. ZZ )
5 3 4 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. ZZ )
6 5 zred 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. RR )
7 6 3 nndivred 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. RR )
8 7 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. CC )
9 1 8 fsumcl 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) e. CC )
10 9 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) e. CC )
11 emre 
 |-  gamma e. RR
12 11 recni 
 |-  gamma e. CC
13 12 a1i 
 |-  ( ( T. /\ x e. RR+ ) -> gamma e. CC )
14 mudivsum 
 |-  ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) e. O(1)
15 14 a1i 
 |-  ( T. -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) e. O(1) )
16 rpssre 
 |-  RR+ C_ RR
17 o1const 
 |-  ( ( RR+ C_ RR /\ gamma e. CC ) -> ( x e. RR+ |-> gamma ) e. O(1) )
18 16 12 17 mp2an 
 |-  ( x e. RR+ |-> gamma ) e. O(1)
19 18 a1i 
 |-  ( T. -> ( x e. RR+ |-> gamma ) e. O(1) )
20 10 13 15 19 o1mul2 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. gamma ) ) e. O(1) )
21 fzfid 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / n ) ) ) e. Fin )
22 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` ( x / n ) ) ) -> m e. NN )
23 22 adantl 
 |-  ( ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. NN )
24 23 nnrecred 
 |-  ( ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( 1 / m ) e. RR )
25 21 24 fsumrecl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) e. RR )
26 2 nnrpd 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. RR+ )
27 rpdivcl 
 |-  ( ( x e. RR+ /\ n e. RR+ ) -> ( x / n ) e. RR+ )
28 26 27 sylan2 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
29 28 relogcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR )
30 25 29 resubcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) e. RR )
31 7 30 remulcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) e. RR )
32 1 31 fsumrecl 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) e. RR )
33 32 recnd 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) e. CC )
34 33 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) e. CC )
35 mulcl 
 |-  ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) e. CC /\ gamma e. CC ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. gamma ) e. CC )
36 9 12 35 sylancl 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. gamma ) e. CC )
37 36 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. gamma ) e. CC )
38 nnrecre 
 |-  ( m e. NN -> ( 1 / m ) e. RR )
39 38 recnd 
 |-  ( m e. NN -> ( 1 / m ) e. CC )
40 23 39 syl 
 |-  ( ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( 1 / m ) e. CC )
41 21 40 fsumcl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) e. CC )
42 29 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. CC )
43 41 42 subcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) e. CC )
44 8 43 mulcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) e. CC )
45 mulcl 
 |-  ( ( ( ( mmu ` n ) / n ) e. CC /\ gamma e. CC ) -> ( ( ( mmu ` n ) / n ) x. gamma ) e. CC )
46 8 12 45 sylancl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. gamma ) e. CC )
47 1 44 46 fsumsub 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) - ( ( ( mmu ` n ) / n ) x. gamma ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. gamma ) ) )
48 12 a1i 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> gamma e. CC )
49 41 42 48 subsub4d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) - gamma ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) )
50 49 oveq2d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) - gamma ) ) = ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) )
51 8 43 48 subdid 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) - gamma ) ) = ( ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) - ( ( ( mmu ` n ) / n ) x. gamma ) ) )
52 50 51 eqtr3d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) = ( ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) - ( ( ( mmu ` n ) / n ) x. gamma ) ) )
53 52 sumeq2dv 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) - ( ( ( mmu ` n ) / n ) x. gamma ) ) )
54 12 a1i 
 |-  ( x e. RR+ -> gamma e. CC )
55 1 54 8 fsummulc1 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. gamma ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. gamma ) )
56 55 oveq2d 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. gamma ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. gamma ) ) )
57 47 53 56 3eqtr4d 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. gamma ) ) )
58 57 mpteq2ia 
 |-  ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. gamma ) ) )
59 16 a1i 
 |-  ( T. -> RR+ C_ RR )
60 42 48 addcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) + gamma ) e. CC )
61 41 60 subcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) e. CC )
62 8 61 mulcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) e. CC )
63 1 62 fsumcl 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) e. CC )
64 63 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) e. CC )
65 1red 
 |-  ( T. -> 1 e. RR )
66 63 abscld 
 |-  ( x e. RR+ -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) ) e. RR )
67 62 abscld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) ) e. RR )
68 1 67 fsumrecl 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) ) e. RR )
69 1red 
 |-  ( x e. RR+ -> 1 e. RR )
70 1 62 fsumabs 
 |-  ( x e. RR+ -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) ) )
71 rprege0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 <_ x ) )
72 flge0nn0 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 )
73 71 72 syl 
 |-  ( x e. RR+ -> ( |_ ` x ) e. NN0 )
74 73 nn0red 
 |-  ( x e. RR+ -> ( |_ ` x ) e. RR )
75 rerpdivcl 
 |-  ( ( ( |_ ` x ) e. RR /\ x e. RR+ ) -> ( ( |_ ` x ) / x ) e. RR )
76 74 75 mpancom 
 |-  ( x e. RR+ -> ( ( |_ ` x ) / x ) e. RR )
77 rpreccl 
 |-  ( x e. RR+ -> ( 1 / x ) e. RR+ )
78 77 adantr 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / x ) e. RR+ )
79 78 rpred 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / x ) e. RR )
80 8 abscld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` n ) / n ) ) e. RR )
81 3 nnrecred 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. RR )
82 61 abscld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) e. RR )
83 id 
 |-  ( x e. RR+ -> x e. RR+ )
84 rpdivcl 
 |-  ( ( n e. RR+ /\ x e. RR+ ) -> ( n / x ) e. RR+ )
85 26 83 84 syl2anr 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n / x ) e. RR+ )
86 85 rpred 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n / x ) e. RR )
87 8 absge0d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( ( mmu ` n ) / n ) ) )
88 61 absge0d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) )
89 6 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. CC )
90 3 nncnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
91 3 nnne0d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
92 89 90 91 absdivd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` n ) / n ) ) = ( ( abs ` ( mmu ` n ) ) / ( abs ` n ) ) )
93 3 nnrpd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
94 rprege0 
 |-  ( n e. RR+ -> ( n e. RR /\ 0 <_ n ) )
95 93 94 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. RR /\ 0 <_ n ) )
96 absid 
 |-  ( ( n e. RR /\ 0 <_ n ) -> ( abs ` n ) = n )
97 95 96 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` n ) = n )
98 97 oveq2d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( mmu ` n ) ) / ( abs ` n ) ) = ( ( abs ` ( mmu ` n ) ) / n ) )
99 92 98 eqtrd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` n ) / n ) ) = ( ( abs ` ( mmu ` n ) ) / n ) )
100 89 abscld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( mmu ` n ) ) e. RR )
101 1red 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
102 mule1 
 |-  ( n e. NN -> ( abs ` ( mmu ` n ) ) <_ 1 )
103 3 102 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( mmu ` n ) ) <_ 1 )
104 100 101 93 103 lediv1dd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( mmu ` n ) ) / n ) <_ ( 1 / n ) )
105 99 104 eqbrtrd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` n ) / n ) ) <_ ( 1 / n ) )
106 harmonicbnd4 
 |-  ( ( x / n ) e. RR+ -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) <_ ( 1 / ( x / n ) ) )
107 28 106 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) <_ ( 1 / ( x / n ) ) )
108 rpcnne0 
 |-  ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) )
109 108 adantr 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x e. CC /\ x =/= 0 ) )
110 rpcnne0 
 |-  ( n e. RR+ -> ( n e. CC /\ n =/= 0 ) )
111 93 110 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. CC /\ n =/= 0 ) )
112 recdiv 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( n e. CC /\ n =/= 0 ) ) -> ( 1 / ( x / n ) ) = ( n / x ) )
113 109 111 112 syl2anc 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / ( x / n ) ) = ( n / x ) )
114 107 113 breqtrd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) <_ ( n / x ) )
115 80 81 82 86 87 88 105 114 lemul12ad 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( mmu ` n ) / n ) ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) ) <_ ( ( 1 / n ) x. ( n / x ) ) )
116 8 61 absmuld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) ) = ( ( abs ` ( ( mmu ` n ) / n ) ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) ) )
117 1cnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. CC )
118 dmdcan 
 |-  ( ( ( n e. CC /\ n =/= 0 ) /\ ( x e. CC /\ x =/= 0 ) /\ 1 e. CC ) -> ( ( n / x ) x. ( 1 / n ) ) = ( 1 / x ) )
119 111 109 117 118 syl3anc 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n / x ) x. ( 1 / n ) ) = ( 1 / x ) )
120 85 rpcnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n / x ) e. CC )
121 81 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. CC )
122 120 121 mulcomd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n / x ) x. ( 1 / n ) ) = ( ( 1 / n ) x. ( n / x ) ) )
123 119 122 eqtr3d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / x ) = ( ( 1 / n ) x. ( n / x ) ) )
124 115 116 123 3brtr4d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) ) <_ ( 1 / x ) )
125 1 67 79 124 fsumle 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / x ) )
126 hashfz1 
 |-  ( ( |_ ` x ) e. NN0 -> ( # ` ( 1 ... ( |_ ` x ) ) ) = ( |_ ` x ) )
127 73 126 syl 
 |-  ( x e. RR+ -> ( # ` ( 1 ... ( |_ ` x ) ) ) = ( |_ ` x ) )
128 127 oveq1d 
 |-  ( x e. RR+ -> ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. ( 1 / x ) ) = ( ( |_ ` x ) x. ( 1 / x ) ) )
129 77 rpcnd 
 |-  ( x e. RR+ -> ( 1 / x ) e. CC )
130 fsumconst 
 |-  ( ( ( 1 ... ( |_ ` x ) ) e. Fin /\ ( 1 / x ) e. CC ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / x ) = ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. ( 1 / x ) ) )
131 1 129 130 syl2anc 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / x ) = ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. ( 1 / x ) ) )
132 73 nn0cnd 
 |-  ( x e. RR+ -> ( |_ ` x ) e. CC )
133 rpcn 
 |-  ( x e. RR+ -> x e. CC )
134 rpne0 
 |-  ( x e. RR+ -> x =/= 0 )
135 132 133 134 divrecd 
 |-  ( x e. RR+ -> ( ( |_ ` x ) / x ) = ( ( |_ ` x ) x. ( 1 / x ) ) )
136 128 131 135 3eqtr4d 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / x ) = ( ( |_ ` x ) / x ) )
137 125 136 breqtrd 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) ) <_ ( ( |_ ` x ) / x ) )
138 rpre 
 |-  ( x e. RR+ -> x e. RR )
139 flle 
 |-  ( x e. RR -> ( |_ ` x ) <_ x )
140 138 139 syl 
 |-  ( x e. RR+ -> ( |_ ` x ) <_ x )
141 133 mulridd 
 |-  ( x e. RR+ -> ( x x. 1 ) = x )
142 140 141 breqtrrd 
 |-  ( x e. RR+ -> ( |_ ` x ) <_ ( x x. 1 ) )
143 reflcl 
 |-  ( x e. RR -> ( |_ ` x ) e. RR )
144 138 143 syl 
 |-  ( x e. RR+ -> ( |_ ` x ) e. RR )
145 rpregt0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 < x ) )
146 ledivmul 
 |-  ( ( ( |_ ` x ) e. RR /\ 1 e. RR /\ ( x e. RR /\ 0 < x ) ) -> ( ( ( |_ ` x ) / x ) <_ 1 <-> ( |_ ` x ) <_ ( x x. 1 ) ) )
147 144 69 145 146 syl3anc 
 |-  ( x e. RR+ -> ( ( ( |_ ` x ) / x ) <_ 1 <-> ( |_ ` x ) <_ ( x x. 1 ) ) )
148 142 147 mpbird 
 |-  ( x e. RR+ -> ( ( |_ ` x ) / x ) <_ 1 )
149 68 76 69 137 148 letrd 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) ) <_ 1 )
150 66 68 69 70 149 letrd 
 |-  ( x e. RR+ -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) ) <_ 1 )
151 150 ad2antrl 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) ) <_ 1 )
152 59 64 65 65 151 elo1d 
 |-  ( T. -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( ( log ` ( x / n ) ) + gamma ) ) ) ) e. O(1) )
153 58 152 eqeltrrid 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. gamma ) ) ) e. O(1) )
154 34 37 153 o1dif 
 |-  ( T. -> ( ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) ) e. O(1) <-> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. gamma ) ) e. O(1) ) )
155 20 154 mpbird 
 |-  ( T. -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) ) e. O(1) )
156 155 mptru 
 |-  ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) ) e. O(1)