Metamath Proof Explorer

Theorem mulogsum

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

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

Proof

Step Hyp Ref Expression
1 rpssre 
 |-  RR+ C_ RR
2 ax-1cn 
 |-  1 e. CC
3 o1const 
 |-  ( ( RR+ C_ RR /\ 1 e. CC ) -> ( x e. RR+ |-> 1 ) e. O(1) )
4 1 2 3 mp2an 
 |-  ( x e. RR+ |-> 1 ) e. O(1)
5 1cnd 
 |-  ( ( T. /\ x e. RR+ ) -> 1 e. CC )
6 fzfid 
 |-  ( x e. RR+ -> ( 1 ... ( |_ ` x ) ) e. Fin )
7 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
8 7 adantl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
9 mucl 
 |-  ( n e. NN -> ( mmu ` n ) e. ZZ )
10 8 9 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. ZZ )
11 10 zred 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. RR )
12 11 8 nndivred 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. RR )
13 7 nnrpd 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. RR+ )
14 rpdivcl 
 |-  ( ( x e. RR+ /\ n e. RR+ ) -> ( x / n ) e. RR+ )
15 13 14 sylan2 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
16 15 relogcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR )
17 12 16 remulcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) e. RR )
18 17 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
19 6 18 fsumcl 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
20 19 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
21 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)
22 sumex 
 |-  sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) e. _V
23 22 a1i 
 |-  ( ( 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. _V )
24 21 a1i 
 |-  ( 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) )
25 23 24 o1mptrcl 
 |-  ( ( 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 )
26 5 20 subcld 
 |-  ( ( T. /\ x e. RR+ ) -> ( 1 - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. CC )
27 1red 
 |-  ( T. -> 1 e. RR )
28 fz1ssnn 
 |-  ( 1 ... ( |_ ` x ) ) C_ NN
29 28 a1i 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( 1 ... ( |_ ` x ) ) C_ NN )
30 29 sselda 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
31 30 9 syl 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. ZZ )
32 31 zred 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. RR )
33 32 30 nndivred 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. RR )
34 33 recnd 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. CC )
35 fzfid 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / n ) ) ) e. Fin )
36 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` ( x / n ) ) ) -> m e. NN )
37 36 adantl 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. NN )
38 37 nnrpd 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. RR+ )
39 38 rpcnne0d 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( m e. CC /\ m =/= 0 ) )
40 reccl 
 |-  ( ( m e. CC /\ m =/= 0 ) -> ( 1 / m ) e. CC )
41 39 40 syl 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( 1 / m ) e. CC )
42 35 41 fsumcl 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) e. CC )
43 simpl 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> x e. RR+ )
44 43 13 14 syl2an 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
45 44 relogcld 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR )
46 45 recnd 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. CC )
47 34 42 46 subdid 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) = ( ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) - ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
48 47 sumeq2dv 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> 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. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) - ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
49 fzfid 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
50 34 42 mulcld 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) e. CC )
51 18 adantlr 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
52 49 50 51 fsumsub 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) - ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
53 oveq2 
 |-  ( k = ( n x. m ) -> ( 1 / k ) = ( 1 / ( n x. m ) ) )
54 53 oveq2d 
 |-  ( k = ( n x. m ) -> ( ( mmu ` n ) x. ( 1 / k ) ) = ( ( mmu ` n ) x. ( 1 / ( n x. m ) ) ) )
55 rpre 
 |-  ( x e. RR+ -> x e. RR )
56 55 adantr 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> x e. RR )
57 ssrab2 
 |-  { y e. NN | y || k } C_ NN
58 simprr 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> n e. { y e. NN | y || k } )
59 57 58 sseldi 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> n e. NN )
60 59 9 syl 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( mmu ` n ) e. ZZ )
61 60 zcnd 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( mmu ` n ) e. CC )
62 elfznn 
 |-  ( k e. ( 1 ... ( |_ ` x ) ) -> k e. NN )
63 62 adantl 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. NN )
64 63 nnrecred 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / k ) e. RR )
65 64 recnd 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / k ) e. CC )
66 65 adantrr 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( 1 / k ) e. CC )
67 61 66 mulcld 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( ( mmu ` n ) x. ( 1 / k ) ) e. CC )
68 54 56 67 dvdsflsumcom 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ n e. { y e. NN | y || k } ( ( mmu ` n ) x. ( 1 / k ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( 1 / ( n x. m ) ) ) )
69 oveq2 
 |-  ( k = 1 -> ( 1 / k ) = ( 1 / 1 ) )
70 1div1e1 
 |-  ( 1 / 1 ) = 1
71 69 70 eqtrdi 
 |-  ( k = 1 -> ( 1 / k ) = 1 )
72 flge1nn 
 |-  ( ( x e. RR /\ 1 <_ x ) -> ( |_ ` x ) e. NN )
73 55 72 sylan 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( |_ ` x ) e. NN )
74 nnuz 
 |-  NN = ( ZZ>= ` 1 )
75 73 74 eleqtrdi 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( |_ ` x ) e. ( ZZ>= ` 1 ) )
76 eluzfz1 
 |-  ( ( |_ ` x ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( |_ ` x ) ) )
77 75 76 syl 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> 1 e. ( 1 ... ( |_ ` x ) ) )
78 71 49 29 77 65 musumsum 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ n e. { y e. NN | y || k } ( ( mmu ` n ) x. ( 1 / k ) ) = 1 )
79 31 zcnd 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. CC )
80 79 adantr 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( mmu ` n ) e. CC )
81 30 adantr 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n e. NN )
82 81 nnrpd 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> n e. RR+ )
83 82 rpcnne0d 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( n e. CC /\ n =/= 0 ) )
84 divdiv1 
 |-  ( ( ( mmu ` n ) e. CC /\ ( n e. CC /\ n =/= 0 ) /\ ( m e. CC /\ m =/= 0 ) ) -> ( ( ( mmu ` n ) / n ) / m ) = ( ( mmu ` n ) / ( n x. m ) ) )
85 80 83 39 84 syl3anc 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( ( mmu ` n ) / n ) / m ) = ( ( mmu ` n ) / ( n x. m ) ) )
86 34 adantr 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( mmu ` n ) / n ) e. CC )
87 37 nncnd 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. CC )
88 37 nnne0d 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m =/= 0 )
89 86 87 88 divrecd 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( ( mmu ` n ) / n ) / m ) = ( ( ( mmu ` n ) / n ) x. ( 1 / m ) ) )
90 nnmulcl 
 |-  ( ( n e. NN /\ m e. NN ) -> ( n x. m ) e. NN )
91 30 36 90 syl2an 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( n x. m ) e. NN )
92 91 nncnd 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( n x. m ) e. CC )
93 91 nnne0d 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( n x. m ) =/= 0 )
94 80 92 93 divrecd 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( mmu ` n ) / ( n x. m ) ) = ( ( mmu ` n ) x. ( 1 / ( n x. m ) ) ) )
95 85 89 94 3eqtr3rd 
 |-  ( ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( mmu ` n ) x. ( 1 / ( n x. m ) ) ) = ( ( ( mmu ` n ) / n ) x. ( 1 / m ) ) )
96 95 sumeq2dv 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( 1 / ( n x. m ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( ( mmu ` n ) / n ) x. ( 1 / m ) ) )
97 35 34 41 fsummulc2 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( ( mmu ` n ) / n ) x. ( 1 / m ) ) )
98 96 97 eqtr4d 
 |-  ( ( ( x e. RR+ /\ 1 <_ x ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( 1 / ( n x. m ) ) ) = ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) )
99 98 sumeq2dv 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( 1 / ( n x. m ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) )
100 68 78 99 3eqtr3rd 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) = 1 )
101 100 oveq1d 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( 1 - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
102 48 52 101 3eqtrd 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) = ( 1 - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
103 102 adantl 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( 1 / m ) - ( log ` ( x / n ) ) ) ) = ( 1 - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
104 25 26 27 103 o1eq 
 |-  ( 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+ |-> ( 1 - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) e. O(1) ) )
105 21 104 mpbii 
 |-  ( T. -> ( x e. RR+ |-> ( 1 - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) e. O(1) )
106 5 20 105 o1dif 
 |-  ( T. -> ( ( x e. RR+ |-> 1 ) e. O(1) <-> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. O(1) ) )
107 4 106 mpbii 
 |-  ( T. -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. O(1) )
108 107 mptru 
 |-  ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. O(1)