Metamath Proof Explorer

Theorem selberglem2

Description: Lemma for selberg . (Contributed by Mario Carneiro, 23-May-2016)

Ref Expression
Hypothesis selberglem1.t 
|- T = ( ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) / n )
Assertion selberglem2 
|- ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) / x ) - ( 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 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 
 |-  ( ( T. /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
7 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
8 7 adantl 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
9 mucl 
 |-  ( n e. NN -> ( mmu ` n ) e. ZZ )
10 8 9 syl 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. ZZ )
11 10 zred 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. RR )
12 11 recnd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. CC )
13 fzfid 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / n ) ) ) e. Fin )
14 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` ( x / n ) ) ) -> m e. NN )
15 14 adantl 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. NN )
16 15 nnrpd 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. RR+ )
17 16 relogcld 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( log ` m ) e. RR )
18 17 resqcld 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( log ` m ) ^ 2 ) e. RR )
19 13 18 fsumrecl 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) e. RR )
20 simplr 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
21 19 20 rerpdivcld 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) e. RR )
22 21 recnd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) e. CC )
23 simpr 
 |-  ( ( T. /\ x e. RR+ ) -> x e. RR+ )
24 7 nnrpd 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. RR+ )
25 rpdivcl 
 |-  ( ( x e. RR+ /\ n e. RR+ ) -> ( x / n ) e. RR+ )
26 23 24 25 syl2an 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
27 26 relogcld 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR )
28 27 resqcld 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) ^ 2 ) e. RR )
29 2re 
 |-  2 e. RR
30 remulcl 
 |-  ( ( 2 e. RR /\ ( log ` ( x / n ) ) e. RR ) -> ( 2 x. ( log ` ( x / n ) ) ) e. RR )
31 29 27 30 sylancr 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( log ` ( x / n ) ) ) e. RR )
32 resubcl 
 |-  ( ( 2 e. RR /\ ( 2 x. ( log ` ( x / n ) ) ) e. RR ) -> ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) e. RR )
33 29 31 32 sylancr 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) e. RR )
34 28 33 readdcld 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) e. RR )
35 34 8 nndivred 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) / n ) e. RR )
36 1 35 eqeltrid 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> T e. RR )
37 36 recnd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> T e. CC )
38 22 37 subcld 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) e. CC )
39 12 38 mulcld 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) e. CC )
40 6 39 fsumcl 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) e. CC )
41 12 37 mulcld 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) x. T ) e. CC )
42 6 41 fsumcl 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) e. CC )
43 2cn 
 |-  2 e. CC
44 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
45 44 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( log ` x ) e. RR )
46 45 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> ( log ` x ) e. CC )
47 mulcl 
 |-  ( ( 2 e. CC /\ ( log ` x ) e. CC ) -> ( 2 x. ( log ` x ) ) e. CC )
48 43 46 47 sylancr 
 |-  ( ( T. /\ x e. RR+ ) -> ( 2 x. ( log ` x ) ) e. CC )
49 42 48 subcld 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) - ( 2 x. ( log ` x ) ) ) e. CC )
50 eqidd 
 |-  ( T. -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) = ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) )
51 eqidd 
 |-  ( T. -> ( 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 ) x. T ) - ( 2 x. ( log ` x ) ) ) ) )
52 5 40 49 50 51 offval2 
 |-  ( T. -> ( ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) oF + ( 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 ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) - ( 2 x. ( log ` x ) ) ) ) ) )
53 40 42 48 addsubassd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) ) - ( 2 x. ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) - ( 2 x. ( log ` x ) ) ) ) )
54 rpcnne0 
 |-  ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) )
55 54 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( x e. CC /\ x =/= 0 ) )
56 55 simpld 
 |-  ( ( T. /\ x e. RR+ ) -> x e. CC )
57 11 adantr 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( mmu ` n ) e. RR )
58 57 18 remulcld 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) e. RR )
59 13 58 fsumrecl 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) e. RR )
60 59 recnd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) e. CC )
61 55 simprd 
 |-  ( ( T. /\ x e. RR+ ) -> x =/= 0 )
62 6 56 60 61 fsumdivc 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) / x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) / x ) )
63 18 recnd 
 |-  ( ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( log ` m ) ^ 2 ) e. CC )
64 13 63 fsumcl 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) e. CC )
65 55 adantr 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x e. CC /\ x =/= 0 ) )
66 divass 
 |-  ( ( ( mmu ` n ) e. CC /\ sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( mmu ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) ) / x ) = ( ( mmu ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) ) )
67 12 64 65 66 syl3anc 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) ) / x ) = ( ( mmu ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) ) )
68 13 12 63 fsummulc2 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) )
69 68 oveq1d 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) ) / x ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) / x ) )
70 22 37 npcand 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) + T ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) )
71 70 oveq2d 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) x. ( ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) + T ) ) = ( ( mmu ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) ) )
72 12 38 37 adddid 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) x. ( ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) + T ) ) = ( ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) + ( ( mmu ` n ) x. T ) ) )
73 71 72 eqtr3d 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) ) = ( ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) + ( ( mmu ` n ) x. T ) ) )
74 67 69 73 3eqtr3d 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) / x ) = ( ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) + ( ( mmu ` n ) x. T ) ) )
75 74 sumeq2dv 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) / x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) + ( ( mmu ` n ) x. T ) ) )
76 6 39 41 fsumadd 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) + ( ( mmu ` n ) x. T ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) ) )
77 62 75 76 3eqtrrd 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) / x ) )
78 77 oveq1d 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) ) - ( 2 x. ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) )
79 53 78 eqtr3d 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) - ( 2 x. ( log ` x ) ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) )
80 79 mpteq2dva 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) + ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) - ( 2 x. ( log ` x ) ) ) ) ) = ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) )
81 52 80 eqtrd 
 |-  ( T. -> ( ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) oF + ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) - ( 2 x. ( log ` x ) ) ) ) ) = ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) )
82 1red 
 |-  ( T. -> 1 e. RR )
83 6 28 fsumrecl 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) e. RR )
84 83 23 rerpdivcld 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) e. RR )
85 84 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) e. CC )
86 2cnd 
 |-  ( ( T. /\ x e. RR+ ) -> 2 e. CC )
87 2nn0 
 |-  2 e. NN0
88 logexprlim 
 |-  ( 2 e. NN0 -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) ) ~~>r ( ! ` 2 ) )
89 87 88 mp1i 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) ) ~~>r ( ! ` 2 ) )
90 2cnd 
 |-  ( T. -> 2 e. CC )
91 rlimconst 
 |-  ( ( RR+ C_ RR /\ 2 e. CC ) -> ( x e. RR+ |-> 2 ) ~~>r 2 )
92 3 90 91 sylancr 
 |-  ( T. -> ( x e. RR+ |-> 2 ) ~~>r 2 )
93 85 86 89 92 rlimadd 
 |-  ( T. -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + 2 ) ) ~~>r ( ( ! ` 2 ) + 2 ) )
94 rlimo1 
 |-  ( ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + 2 ) ) ~~>r ( ( ! ` 2 ) + 2 ) -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + 2 ) ) e. O(1) )
95 93 94 syl 
 |-  ( T. -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + 2 ) ) e. O(1) )
96 readdcl 
 |-  ( ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) e. RR /\ 2 e. RR ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + 2 ) e. RR )
97 84 29 96 sylancl 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + 2 ) e. RR )
98 40 abscld 
 |-  ( ( T. /\ x e. RR+ ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) e. RR )
99 97 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + 2 ) e. CC )
100 99 abscld 
 |-  ( ( T. /\ x e. RR+ ) -> ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + 2 ) ) e. RR )
101 39 abscld 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) e. RR )
102 6 101 fsumrecl 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) e. RR )
103 6 39 fsumabs 
 |-  ( ( T. /\ x e. RR+ ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) )
104 readdcl 
 |-  ( ( ( ( log ` ( x / n ) ) ^ 2 ) e. RR /\ 2 e. RR ) -> ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) e. RR )
105 28 29 104 sylancl 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) e. RR )
106 105 20 rerpdivcld 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) / x ) e. RR )
107 6 106 fsumrecl 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) / x ) e. RR )
108 38 abscld 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) e. RR )
109 12 38 absmuld 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) = ( ( abs ` ( mmu ` n ) ) x. ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) )
110 12 abscld 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( mmu ` n ) ) e. RR )
111 1red 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
112 38 absge0d 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) )
113 mule1 
 |-  ( n e. NN -> ( abs ` ( mmu ` n ) ) <_ 1 )
114 8 113 syl 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( mmu ` n ) ) <_ 1 )
115 110 111 108 112 114 lemul1ad 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( mmu ` n ) ) x. ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) <_ ( 1 x. ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) )
116 108 recnd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) e. CC )
117 116 mullidd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) = ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) )
118 115 117 breqtrd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( mmu ` n ) ) x. ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) <_ ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) )
119 109 118 eqbrtrd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) <_ ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) )
120 65 simpld 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
121 120 38 absmuld 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( x x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) = ( ( abs ` x ) x. ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) )
122 120 22 37 subdid 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) = ( ( x x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) ) - ( x x. T ) ) )
123 65 simprd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x =/= 0 )
124 64 120 123 divcan2d 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) )
125 34 recnd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) e. CC )
126 8 nnrpd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
127 rpcnne0 
 |-  ( n e. RR+ -> ( n e. CC /\ n =/= 0 ) )
128 126 127 syl 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. CC /\ n =/= 0 ) )
129 divass 
 |-  ( ( x e. CC /\ ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( x x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) / n ) = ( x x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) / n ) ) )
130 1 oveq2i 
 |-  ( x x. T ) = ( x x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) / n ) )
131 129 130 eqtr4di 
 |-  ( ( x e. CC /\ ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( x x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) / n ) = ( x x. T ) )
132 div23 
 |-  ( ( x e. CC /\ ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( x x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) / n ) = ( ( x / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) )
133 131 132 eqtr3d 
 |-  ( ( x e. CC /\ ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( x x. T ) = ( ( x / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) )
134 120 125 128 133 syl3anc 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x x. T ) = ( ( x / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) )
135 124 134 oveq12d 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x x. ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) ) - ( x x. T ) ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) - ( ( x / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) ) )
136 122 135 eqtrd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) - ( ( x / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) ) )
137 136 fveq2d 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( x x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) = ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) - ( ( x / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) ) ) )
138 rprege0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 <_ x ) )
139 absid 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( abs ` x ) = x )
140 20 138 139 3syl 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` x ) = x )
141 140 oveq1d 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` x ) x. ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) = ( x x. ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) )
142 121 137 141 3eqtr3d 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) - ( ( x / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) ) ) = ( x x. ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) )
143 8 nncnd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
144 143 mullidd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) = n )
145 rpre 
 |-  ( x e. RR+ -> x e. RR )
146 145 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> x e. RR )
147 fznnfl 
 |-  ( x e. RR -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) )
148 146 147 syl 
 |-  ( ( T. /\ x e. RR+ ) -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) )
149 148 simplbda 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n <_ x )
150 144 149 eqbrtrd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) <_ x )
151 20 rpred 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
152 111 151 126 lemuldivd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 x. n ) <_ x <-> 1 <_ ( x / n ) ) )
153 150 152 mpbid 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ ( x / n ) )
154 log2sumbnd 
 |-  ( ( ( x / n ) e. RR+ /\ 1 <_ ( x / n ) ) -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) - ( ( x / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) ) ) <_ ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) )
155 26 153 154 syl2anc 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) - ( ( x / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / n ) ) ) ) ) ) ) ) <_ ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) )
156 142 155 eqbrtrrd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x x. ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) <_ ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) )
157 108 105 20 lemuldiv2d 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x x. ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) <_ ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) <-> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) <_ ( ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) / x ) ) )
158 156 157 mpbid 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) <_ ( ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) / x ) )
159 101 108 106 119 158 letrd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) <_ ( ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) / x ) )
160 6 101 106 159 fsumle 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) / x ) )
161 6 105 fsumrecl 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) e. RR )
162 remulcl 
 |-  ( ( x e. RR /\ 2 e. RR ) -> ( x x. 2 ) e. RR )
163 146 29 162 sylancl 
 |-  ( ( T. /\ x e. RR+ ) -> ( x x. 2 ) e. RR )
164 83 163 readdcld 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) + ( x x. 2 ) ) e. RR )
165 28 recnd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) ^ 2 ) e. CC )
166 2cnd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. CC )
167 6 165 166 fsumadd 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) + sum_ n e. ( 1 ... ( |_ ` x ) ) 2 ) )
168 fsumconst 
 |-  ( ( ( 1 ... ( |_ ` x ) ) e. Fin /\ 2 e. CC ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) 2 = ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. 2 ) )
169 6 43 168 sylancl 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) 2 = ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. 2 ) )
170 138 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( x e. RR /\ 0 <_ x ) )
171 flge0nn0 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 )
172 hashfz1 
 |-  ( ( |_ ` x ) e. NN0 -> ( # ` ( 1 ... ( |_ ` x ) ) ) = ( |_ ` x ) )
173 170 171 172 3syl 
 |-  ( ( T. /\ x e. RR+ ) -> ( # ` ( 1 ... ( |_ ` x ) ) ) = ( |_ ` x ) )
174 173 oveq1d 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. 2 ) = ( ( |_ ` x ) x. 2 ) )
175 169 174 eqtrd 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) 2 = ( ( |_ ` x ) x. 2 ) )
176 175 oveq2d 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) + sum_ n e. ( 1 ... ( |_ ` x ) ) 2 ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) + ( ( |_ ` x ) x. 2 ) ) )
177 167 176 eqtrd 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) + ( ( |_ ` x ) x. 2 ) ) )
178 reflcl 
 |-  ( x e. RR -> ( |_ ` x ) e. RR )
179 146 178 syl 
 |-  ( ( T. /\ x e. RR+ ) -> ( |_ ` x ) e. RR )
180 29 a1i 
 |-  ( ( T. /\ x e. RR+ ) -> 2 e. RR )
181 179 180 remulcld 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( |_ ` x ) x. 2 ) e. RR )
182 flle 
 |-  ( x e. RR -> ( |_ ` x ) <_ x )
183 146 182 syl 
 |-  ( ( T. /\ x e. RR+ ) -> ( |_ ` x ) <_ x )
184 2pos 
 |-  0 < 2
185 29 184 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
186 185 a1i 
 |-  ( ( T. /\ x e. RR+ ) -> ( 2 e. RR /\ 0 < 2 ) )
187 lemul1 
 |-  ( ( ( |_ ` x ) e. RR /\ x e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( |_ ` x ) <_ x <-> ( ( |_ ` x ) x. 2 ) <_ ( x x. 2 ) ) )
188 179 146 186 187 syl3anc 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( |_ ` x ) <_ x <-> ( ( |_ ` x ) x. 2 ) <_ ( x x. 2 ) ) )
189 183 188 mpbid 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( |_ ` x ) x. 2 ) <_ ( x x. 2 ) )
190 181 163 83 189 leadd2dd 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) + ( ( |_ ` x ) x. 2 ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) + ( x x. 2 ) ) )
191 177 190 eqbrtrd 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) + ( x x. 2 ) ) )
192 161 164 23 191 lediv1dd 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) / x ) <_ ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) + ( x x. 2 ) ) / x ) )
193 105 recnd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) e. CC )
194 6 56 193 61 fsumdivc 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) / x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) / x ) )
195 83 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) e. CC )
196 56 86 mulcld 
 |-  ( ( T. /\ x e. RR+ ) -> ( x x. 2 ) e. CC )
197 divdir 
 |-  ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) e. CC /\ ( x x. 2 ) e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) + ( x x. 2 ) ) / x ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + ( ( x x. 2 ) / x ) ) )
198 195 196 55 197 syl3anc 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) + ( x x. 2 ) ) / x ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + ( ( x x. 2 ) / x ) ) )
199 86 56 61 divcan3d 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( x x. 2 ) / x ) = 2 )
200 199 oveq2d 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + ( ( x x. 2 ) / x ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + 2 ) )
201 198 200 eqtrd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) + ( x x. 2 ) ) / x ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + 2 ) )
202 192 194 201 3brtr3d 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( log ` ( x / n ) ) ^ 2 ) + 2 ) / x ) <_ ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + 2 ) )
203 102 107 97 160 202 letrd 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) <_ ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + 2 ) )
204 98 102 97 103 203 letrd 
 |-  ( ( T. /\ x e. RR+ ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) <_ ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + 2 ) )
205 97 leabsd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + 2 ) <_ ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + 2 ) ) )
206 98 97 100 204 205 letrd 
 |-  ( ( T. /\ x e. RR+ ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) <_ ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + 2 ) ) )
207 206 adantrr 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) <_ ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 2 ) / x ) + 2 ) ) )
208 82 95 97 40 207 o1le 
 |-  ( T. -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) e. O(1) )
209 1 selberglem1 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
210 o1add 
 |-  ( ( ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) e. O(1) /\ ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) ) -> ( ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) oF + ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) - ( 2 x. ( log ` x ) ) ) ) ) e. O(1) )
211 208 209 210 sylancl 
 |-  ( T. -> ( ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. ( ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` m ) ^ 2 ) / x ) - T ) ) ) oF + ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) x. T ) - ( 2 x. ( log ` x ) ) ) ) ) e. O(1) )
212 81 211 eqeltrrd 
 |-  ( T. -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) )
213 212 mptru 
 |-  ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` m ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)