Metamath Proof Explorer

Theorem mudivsum

Description: Asymptotic formula for sum_ n <_ x , mmu ( n ) / n = O(1) . Equation 10.2.1 of Shapiro, p. 405. (Contributed by Mario Carneiro, 14-May-2016)

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

Proof

Step Hyp Ref Expression
1 1red 
 |-  ( T. -> 1 e. RR )
2 reex 
 |-  RR e. _V
3 rpssre 
 |-  RR+ C_ RR
4 2 3 ssexi 
 |-  RR+ e. _V
5 4 a1i 
 |-  ( T. -> RR+ e. _V )
6 fzfid 
 |-  ( x e. RR+ -> ( 1 ... ( |_ ` x ) ) e. Fin )
7 rpre 
 |-  ( x e. RR+ -> x e. RR )
8 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
9 nndivre 
 |-  ( ( x e. RR /\ n e. NN ) -> ( x / n ) e. RR )
10 7 8 9 syl2an 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
11 10 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. CC )
12 reflcl 
 |-  ( ( x / n ) e. RR -> ( |_ ` ( x / n ) ) e. RR )
13 10 12 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( x / n ) ) e. RR )
14 13 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( x / n ) ) e. CC )
15 11 14 subcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x / n ) - ( |_ ` ( x / n ) ) ) e. CC )
16 8 adantl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
17 mucl 
 |-  ( n e. NN -> ( mmu ` n ) e. ZZ )
18 16 17 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. ZZ )
19 18 zcnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. CC )
20 15 19 mulcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) e. CC )
21 6 20 fsumcl 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) e. CC )
22 rpcn 
 |-  ( x e. RR+ -> x e. CC )
23 rpne0 
 |-  ( x e. RR+ -> x =/= 0 )
24 21 22 23 divcld 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) e. CC )
25 24 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) e. CC )
26 ovexd 
 |-  ( ( T. /\ x e. RR+ ) -> ( 1 / x ) e. _V )
27 eqidd 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) ) )
28 eqidd 
 |-  ( T. -> ( x e. RR+ |-> ( 1 / x ) ) = ( x e. RR+ |-> ( 1 / x ) ) )
29 5 25 26 27 28 offval2 
 |-  ( T. -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) ) oF + ( x e. RR+ |-> ( 1 / x ) ) ) = ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) + ( 1 / x ) ) ) )
30 3 a1i 
 |-  ( T. -> RR+ C_ RR )
31 21 adantr 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) e. CC )
32 22 adantr 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> x e. CC )
33 23 adantr 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> x =/= 0 )
34 31 32 33 absdivd 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) ) = ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) / ( abs ` x ) ) )
35 rprege0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 <_ x ) )
36 absid 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( abs ` x ) = x )
37 35 36 syl 
 |-  ( x e. RR+ -> ( abs ` x ) = x )
38 37 adantr 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( abs ` x ) = x )
39 38 oveq2d 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) / ( abs ` x ) ) = ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) / x ) )
40 34 39 eqtrd 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) ) = ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) / x ) )
41 31 abscld 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) e. RR )
42 fzfid 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
43 20 adantlr 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) e. CC )
44 43 abscld 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) e. RR )
45 42 44 fsumrecl 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) e. RR )
46 7 adantr 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> x e. RR )
47 42 43 fsumabs 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) )
48 reflcl 
 |-  ( x e. RR -> ( |_ ` x ) e. RR )
49 46 48 syl 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( |_ ` x ) e. RR )
50 1red 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
51 15 adantlr 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x / n ) - ( |_ ` ( x / n ) ) ) e. CC )
52 fz1ssnn 
 |-  ( 1 ... ( |_ ` x ) ) C_ NN
53 52 a1i 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( 1 ... ( |_ ` x ) ) C_ NN )
54 53 sselda 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
55 54 17 syl 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. ZZ )
56 55 zcnd 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. CC )
57 51 56 absmuld 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) = ( ( abs ` ( ( x / n ) - ( |_ ` ( x / n ) ) ) ) x. ( abs ` ( mmu ` n ) ) ) )
58 51 abscld 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( x / n ) - ( |_ ` ( x / n ) ) ) ) e. RR )
59 56 abscld 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( mmu ` n ) ) e. RR )
60 51 absge0d 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( ( x / n ) - ( |_ ` ( x / n ) ) ) ) )
61 56 absge0d 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( mmu ` n ) ) )
62 simpl 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> x e. RR+ )
63 8 nnrpd 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. RR+ )
64 rpdivcl 
 |-  ( ( x e. RR+ /\ n e. RR+ ) -> ( x / n ) e. RR+ )
65 62 63 64 syl2an 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
66 3 65 sselid 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
67 66 12 syl 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( x / n ) ) e. RR )
68 flle 
 |-  ( ( x / n ) e. RR -> ( |_ ` ( x / n ) ) <_ ( x / n ) )
69 66 68 syl 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( x / n ) ) <_ ( x / n ) )
70 67 66 69 abssubge0d 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( x / n ) - ( |_ ` ( x / n ) ) ) ) = ( ( x / n ) - ( |_ ` ( x / n ) ) ) )
71 fracle1 
 |-  ( ( x / n ) e. RR -> ( ( x / n ) - ( |_ ` ( x / n ) ) ) <_ 1 )
72 66 71 syl 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x / n ) - ( |_ ` ( x / n ) ) ) <_ 1 )
73 70 72 eqbrtrd 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( x / n ) - ( |_ ` ( x / n ) ) ) ) <_ 1 )
74 mule1 
 |-  ( n e. NN -> ( abs ` ( mmu ` n ) ) <_ 1 )
75 54 74 syl 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( mmu ` n ) ) <_ 1 )
76 58 50 59 50 60 61 73 75 lemul12ad 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( x / n ) - ( |_ ` ( x / n ) ) ) ) x. ( abs ` ( mmu ` n ) ) ) <_ ( 1 x. 1 ) )
77 1t1e1 
 |-  ( 1 x. 1 ) = 1
78 76 77 breqtrdi 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( x / n ) - ( |_ ` ( x / n ) ) ) ) x. ( abs ` ( mmu ` n ) ) ) <_ 1 )
79 57 78 eqbrtrd 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) <_ 1 )
80 42 44 50 79 fsumle 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) 1 )
81 1cnd 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> 1 e. CC )
82 fsumconst 
 |-  ( ( ( 1 ... ( |_ ` x ) ) e. Fin /\ 1 e. CC ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) 1 = ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. 1 ) )
83 42 81 82 syl2anc 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) 1 = ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. 1 ) )
84 flge1nn 
 |-  ( ( x e. RR /\ 1 <_ x ) -> ( |_ ` x ) e. NN )
85 7 84 sylan 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( |_ ` x ) e. NN )
86 85 nnnn0d 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( |_ ` x ) e. NN0 )
87 hashfz1 
 |-  ( ( |_ ` x ) e. NN0 -> ( # ` ( 1 ... ( |_ ` x ) ) ) = ( |_ ` x ) )
88 86 87 syl 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( # ` ( 1 ... ( |_ ` x ) ) ) = ( |_ ` x ) )
89 88 oveq1d 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. 1 ) = ( ( |_ ` x ) x. 1 ) )
90 49 recnd 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( |_ ` x ) e. CC )
91 90 mulid1d 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( ( |_ ` x ) x. 1 ) = ( |_ ` x ) )
92 83 89 91 3eqtrd 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) 1 = ( |_ ` x ) )
93 80 92 breqtrd 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) <_ ( |_ ` x ) )
94 flle 
 |-  ( x e. RR -> ( |_ ` x ) <_ x )
95 46 94 syl 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( |_ ` x ) <_ x )
96 45 49 46 93 95 letrd 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) <_ x )
97 41 45 46 47 96 letrd 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) <_ x )
98 32 mulid1d 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( x x. 1 ) = x )
99 97 98 breqtrrd 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) <_ ( x x. 1 ) )
100 1red 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> 1 e. RR )
101 41 100 62 ledivmuld 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) / x ) <_ 1 <-> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) <_ ( x x. 1 ) ) )
102 99 101 mpbird 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) ) / x ) <_ 1 )
103 40 102 eqbrtrd 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) ) <_ 1 )
104 103 adantl 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) ) <_ 1 )
105 30 25 1 1 104 elo1d 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) ) e. O(1) )
106 ax-1cn 
 |-  1 e. CC
107 divrcnv 
 |-  ( 1 e. CC -> ( x e. RR+ |-> ( 1 / x ) ) ~~>r 0 )
108 106 107 ax-mp 
 |-  ( x e. RR+ |-> ( 1 / x ) ) ~~>r 0
109 rlimo1 
 |-  ( ( x e. RR+ |-> ( 1 / x ) ) ~~>r 0 -> ( x e. RR+ |-> ( 1 / x ) ) e. O(1) )
110 108 109 mp1i 
 |-  ( T. -> ( x e. RR+ |-> ( 1 / x ) ) e. O(1) )
111 o1add 
 |-  ( ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) ) e. O(1) /\ ( x e. RR+ |-> ( 1 / x ) ) e. O(1) ) -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) ) oF + ( x e. RR+ |-> ( 1 / x ) ) ) e. O(1) )
112 105 110 111 syl2anc 
 |-  ( T. -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) ) oF + ( x e. RR+ |-> ( 1 / x ) ) ) e. O(1) )
113 29 112 eqeltrrd 
 |-  ( T. -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) + ( 1 / x ) ) ) e. O(1) )
114 ovexd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) + ( 1 / x ) ) e. _V )
115 18 zred 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. RR )
116 115 16 nndivred 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. RR )
117 116 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. CC )
118 6 117 fsumcl 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) e. CC )
119 118 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) e. CC )
120 118 adantr 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) e. CC )
121 120 abscld 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) e. RR )
122 117 adantlr 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. CC )
123 42 32 122 fsummulc2 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( x x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( x x. ( ( mmu ` n ) / n ) ) )
124 14 19 mulcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( |_ ` ( x / n ) ) x. ( mmu ` n ) ) e. CC )
125 124 adantlr 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( |_ ` ( x / n ) ) x. ( mmu ` n ) ) e. CC )
126 42 43 125 fsumadd 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) + ( ( |_ ` ( x / n ) ) x. ( mmu ` n ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( |_ ` ( x / n ) ) x. ( mmu ` n ) ) ) )
127 11 adantlr 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. CC )
128 14 adantlr 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( x / n ) ) e. CC )
129 127 128 npcand 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) + ( |_ ` ( x / n ) ) ) = ( x / n ) )
130 129 oveq1d 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) + ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) = ( ( x / n ) x. ( mmu ` n ) ) )
131 51 128 56 adddird 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) + ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) = ( ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) + ( ( |_ ` ( x / n ) ) x. ( mmu ` n ) ) ) )
132 32 adantr 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
133 54 nnrpd 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
134 rpcnne0 
 |-  ( n e. RR+ -> ( n e. CC /\ n =/= 0 ) )
135 133 134 syl 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. CC /\ n =/= 0 ) )
136 div23 
 |-  ( ( x e. CC /\ ( mmu ` n ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( x x. ( mmu ` n ) ) / n ) = ( ( x / n ) x. ( mmu ` n ) ) )
137 divass 
 |-  ( ( x e. CC /\ ( mmu ` n ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( x x. ( mmu ` n ) ) / n ) = ( x x. ( ( mmu ` n ) / n ) ) )
138 136 137 eqtr3d 
 |-  ( ( x e. CC /\ ( mmu ` n ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( x / n ) x. ( mmu ` n ) ) = ( x x. ( ( mmu ` n ) / n ) ) )
139 132 56 135 138 syl3anc 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x / n ) x. ( mmu ` n ) ) = ( x x. ( ( mmu ` n ) / n ) ) )
140 130 131 139 3eqtr3d 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) + ( ( |_ ` ( x / n ) ) x. ( mmu ` n ) ) ) = ( x x. ( ( mmu ` n ) / n ) ) )
141 140 sumeq2dv 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) + ( ( |_ ` ( x / n ) ) x. ( mmu ` n ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( x x. ( ( mmu ` n ) / n ) ) )
142 eqidd 
 |-  ( k = ( n x. m ) -> ( mmu ` n ) = ( mmu ` n ) )
143 ssrab2 
 |-  { y e. NN | y || k } C_ NN
144 simprr 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> n e. { y e. NN | y || k } )
145 143 144 sselid 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> n e. NN )
146 145 17 syl 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( mmu ` n ) e. ZZ )
147 146 zcnd 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( mmu ` n ) e. CC )
148 142 46 147 dvdsflsumcom 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ n e. { y e. NN | y || k } ( mmu ` n ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( mmu ` n ) )
149 147 3impb 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) -> ( mmu ` n ) e. CC )
150 149 mulid1d 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) -> ( ( mmu ` n ) x. 1 ) = ( mmu ` n ) )
151 150 2sumeq2dv 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ n e. { y e. NN | y || k } ( ( mmu ` n ) x. 1 ) = sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ n e. { y e. NN | y || k } ( mmu ` n ) )
152 eqidd 
 |-  ( k = 1 -> 1 = 1 )
153 nnuz 
 |-  NN = ( ZZ>= ` 1 )
154 85 153 eleqtrdi 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( |_ ` x ) e. ( ZZ>= ` 1 ) )
155 eluzfz1 
 |-  ( ( |_ ` x ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( |_ ` x ) ) )
156 154 155 syl 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> 1 e. ( 1 ... ( |_ ` x ) ) )
157 1cnd 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. CC )
158 152 42 53 156 157 musumsum 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ n e. { y e. NN | y || k } ( ( mmu ` n ) x. 1 ) = 1 )
159 151 158 eqtr3d 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ n e. { y e. NN | y || k } ( mmu ` n ) = 1 )
160 fzfid 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / n ) ) ) e. Fin )
161 fsumconst 
 |-  ( ( ( 1 ... ( |_ ` ( x / n ) ) ) e. Fin /\ ( mmu ` n ) e. CC ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( mmu ` n ) = ( ( # ` ( 1 ... ( |_ ` ( x / n ) ) ) ) x. ( mmu ` n ) ) )
162 160 56 161 syl2anc 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( mmu ` n ) = ( ( # ` ( 1 ... ( |_ ` ( x / n ) ) ) ) x. ( mmu ` n ) ) )
163 rprege0 
 |-  ( ( x / n ) e. RR+ -> ( ( x / n ) e. RR /\ 0 <_ ( x / n ) ) )
164 flge0nn0 
 |-  ( ( ( x / n ) e. RR /\ 0 <_ ( x / n ) ) -> ( |_ ` ( x / n ) ) e. NN0 )
165 hashfz1 
 |-  ( ( |_ ` ( x / n ) ) e. NN0 -> ( # ` ( 1 ... ( |_ ` ( x / n ) ) ) ) = ( |_ ` ( x / n ) ) )
166 65 163 164 165 4syl 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( # ` ( 1 ... ( |_ ` ( x / n ) ) ) ) = ( |_ ` ( x / n ) ) )
167 166 oveq1d 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( # ` ( 1 ... ( |_ ` ( x / n ) ) ) ) x. ( mmu ` n ) ) = ( ( |_ ` ( x / n ) ) x. ( mmu ` n ) ) )
168 162 167 eqtrd 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( mmu ` n ) = ( ( |_ ` ( x / n ) ) x. ( mmu ` n ) ) )
169 168 sumeq2dv 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( mmu ` n ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( |_ ` ( x / n ) ) x. ( mmu ` n ) ) )
170 148 159 169 3eqtr3rd 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( |_ ` ( x / n ) ) x. ( mmu ` n ) ) = 1 )
171 170 oveq2d 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( |_ ` ( x / n ) ) x. ( mmu ` n ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) + 1 ) )
172 126 141 171 3eqtr3d 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( x x. ( ( mmu ` n ) / n ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) + 1 ) )
173 123 172 eqtrd 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( x x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) + 1 ) )
174 173 oveq1d 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( ( x x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) / x ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) + 1 ) / x ) )
175 120 32 33 divcan3d 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( ( x x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) / x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) )
176 rpcnne0 
 |-  ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) )
177 176 adantr 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( x e. CC /\ x =/= 0 ) )
178 divdir 
 |-  ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) e. CC /\ 1 e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) + 1 ) / x ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) + ( 1 / x ) ) )
179 31 81 177 178 syl3anc 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) + 1 ) / x ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) + ( 1 / x ) ) )
180 174 175 179 3eqtr3d 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) + ( 1 / x ) ) )
181 180 fveq2d 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) = ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) + ( 1 / x ) ) ) )
182 121 181 eqled 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) <_ ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) + ( 1 / x ) ) ) )
183 182 adantl 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) <_ ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( x / n ) - ( |_ ` ( x / n ) ) ) x. ( mmu ` n ) ) / x ) + ( 1 / x ) ) ) )
184 1 113 114 119 183 o1le 
 |-  ( T. -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) e. O(1) )
185 184 mptru 
 |-  ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) e. O(1)