Metamath Proof Explorer

Theorem selberglem1

Description: Lemma for selberg . Estimation of the asymptotic part of selberglem3 . (Contributed by Mario Carneiro, 20-May-2016)

Ref Expression
Hypothesis selberglem1.t 
|- T = ( ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) / n )
Assertion selberglem1 
|- ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)

Proof

Step Hyp Ref Expression
1 selberglem1.t 
 |-  T = ( ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) / n )
2 fzfid 
 |-  ( x e. RR+ -> ( 1 ... ( |_ ` x ) ) e. Fin )
3 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
4 3 adantl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
5 mucl 
 |-  ( n e. NN -> ( mmu ` n ) e. ZZ )
6 4 5 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. ZZ )
7 6 zred 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. RR )
8 7 4 nndivred 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. RR )
9 8 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. CC )
10 3 nnrpd 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. RR+ )
11 rpdivcl 
 |-  ( ( x e. RR+ /\ n e. RR+ ) -> ( x / n ) e. RR+ )
12 10 11 sylan2 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
13 relogcl 
 |-  ( ( x / n ) e. RR+ -> ( log ` ( x / n ) ) e. RR )
14 12 13 syl 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR )
15 14 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. CC )
16 15 sqcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) ^ 2 ) e. CC )
17 9 16 mulcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) e. CC )
18 2 17 fsumcl 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) e. CC )
19 2cn 
 |-  2 e. CC
20 19 a1i 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. CC )
21 20 15 mulcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( log ` ( x / n ) ) ) e. CC )
22 20 21 subcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) e. CC )
23 9 22 mulcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) e. CC )
24 2 23 fsumcl 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) e. CC )
25 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
26 25 recnd 
 |-  ( x e. RR+ -> ( log ` x ) e. CC )
27 mulcl 
 |-  ( ( 2 e. CC /\ ( log ` x ) e. CC ) -> ( 2 x. ( log ` x ) ) e. CC )
28 19 26 27 sylancr 
 |-  ( x e. RR+ -> ( 2 x. ( log ` x ) ) e. CC )
29 18 24 28 addsubd 
 |-  ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) - ( 2 x. ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) )
30 1 oveq2i 
 |-  ( ( mmu ` n ) x. T ) = ( ( mmu ` n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) / n ) )
31 6 zcnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. CC )
32 16 22 addcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) e. CC )
33 4 nnrpd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
34 33 rpcnne0d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. CC /\ n =/= 0 ) )
35 divass 
 |-  ( ( ( mmu ` n ) e. CC /\ ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( ( mmu ` n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) / n ) = ( ( mmu ` n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) / n ) ) )
36 div23 
 |-  ( ( ( mmu ` n ) e. CC /\ ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( ( mmu ` n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) / n ) = ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) )
37 35 36 eqtr3d 
 |-  ( ( ( mmu ` n ) e. CC /\ ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( mmu ` n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) / n ) ) = ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) )
38 31 32 34 37 syl3anc 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) / n ) ) = ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) )
39 9 16 22 adddid 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) = ( ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) + ( ( ( mmu ` n ) / n ) x. ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) )
40 38 39 eqtrd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) / n ) ) = ( ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) + ( ( ( mmu ` n ) / n ) x. ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) )
41 30 40 syl5eq 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) x. T ) = ( ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) + ( ( ( mmu ` n ) / n ) x. ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) )
42 41 sumeq2dv 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) + ( ( ( mmu ` n ) / n ) x. ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) )
43 2 17 23 fsumadd 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) + ( ( ( mmu ` n ) / n ) x. ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) )
44 42 43 eqtrd 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) )
45 44 oveq1d 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) - ( 2 x. ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) - ( 2 x. ( log ` x ) ) ) )
46 19 a1i 
 |-  ( x e. RR+ -> 2 e. CC )
47 9 15 mulcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
48 9 47 subcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) - ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. CC )
49 2 46 48 fsummulc2 
 |-  ( x e. RR+ -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) - ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( ( mmu ` n ) / n ) - ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) )
50 2 9 47 fsumsub 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) - ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
51 50 oveq2d 
 |-  ( x e. RR+ -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) - ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) = ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) )
52 20 9 mulcomd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( mmu ` n ) / n ) ) = ( ( ( mmu ` n ) / n ) x. 2 ) )
53 20 9 15 mul12d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( ( ( mmu ` n ) / n ) x. ( 2 x. ( log ` ( x / n ) ) ) ) )
54 52 53 oveq12d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. ( ( mmu ` n ) / n ) ) - ( 2 x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) = ( ( ( ( mmu ` n ) / n ) x. 2 ) - ( ( ( mmu ` n ) / n ) x. ( 2 x. ( log ` ( x / n ) ) ) ) ) )
55 20 9 47 subdid 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( ( mmu ` n ) / n ) - ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) = ( ( 2 x. ( ( mmu ` n ) / n ) ) - ( 2 x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) )
56 9 20 21 subdid 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) = ( ( ( ( mmu ` n ) / n ) x. 2 ) - ( ( ( mmu ` n ) / n ) x. ( 2 x. ( log ` ( x / n ) ) ) ) ) )
57 54 55 56 3eqtr4d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( ( mmu ` n ) / n ) - ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) = ( ( ( mmu ` n ) / n ) x. ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) )
58 57 sumeq2dv 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( ( mmu ` n ) / n ) - ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) )
59 49 51 58 3eqtr3d 
 |-  ( x e. RR+ -> ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) )
60 59 oveq2d 
 |-  ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) + ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) )
61 29 45 60 3eqtr4d 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) - ( 2 x. ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) + ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) ) )
62 61 mpteq2ia 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) - ( 2 x. ( log ` x ) ) ) ) = ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) + ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) ) )
63 ovexd 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) e. _V )
64 ovexd 
 |-  ( ( T. /\ x e. RR+ ) -> ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) e. _V )
65 mulog2sum 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
66 65 a1i 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) )
67 2ex 
 |-  2 e. _V
68 67 a1i 
 |-  ( ( T. /\ x e. RR+ ) -> 2 e. _V )
69 ovexd 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. _V )
70 rpssre 
 |-  RR+ C_ RR
71 o1const 
 |-  ( ( RR+ C_ RR /\ 2 e. CC ) -> ( x e. RR+ |-> 2 ) e. O(1) )
72 70 19 71 mp2an 
 |-  ( x e. RR+ |-> 2 ) e. O(1)
73 72 a1i 
 |-  ( T. -> ( x e. RR+ |-> 2 ) e. O(1) )
74 reex 
 |-  RR e. _V
75 74 70 ssexi 
 |-  RR+ e. _V
76 75 a1i 
 |-  ( T. -> RR+ e. _V )
77 sumex 
 |-  sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) e. _V
78 77 a1i 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) e. _V )
79 sumex 
 |-  sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) e. _V
80 79 a1i 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) e. _V )
81 eqidd 
 |-  ( T. -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) = ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) )
82 eqidd 
 |-  ( T. -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
83 76 78 80 81 82 offval2 
 |-  ( T. -> ( ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) oF - ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) )
84 mudivsum 
 |-  ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) e. O(1)
85 mulogsum 
 |-  ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. O(1)
86 o1sub 
 |-  ( ( ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) e. O(1) /\ ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. O(1) ) -> ( ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) oF - ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) e. O(1) )
87 84 85 86 mp2an 
 |-  ( ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) oF - ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) e. O(1)
88 83 87 eqeltrrdi 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) e. O(1) )
89 68 69 73 88 o1mul2 
 |-  ( T. -> ( x e. RR+ |-> ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) ) e. O(1) )
90 63 64 66 89 o1add2 
 |-  ( T. -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) + ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) ) ) e. O(1) )
91 90 mptru 
 |-  ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) + ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) ) ) e. O(1)
92 62 91 eqeltri 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)