Metamath Proof Explorer

Theorem mulog2sumlem3

Description: Lemma for mulog2sum . (Contributed by Mario Carneiro, 13-May-2016)

Ref Expression
Hypotheses logdivsum.1 
|- F = ( y e. RR+ |-> ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( log ` i ) / i ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) )
mulog2sumlem.1 
|- ( ph -> F ~~>r L )
Assertion mulog2sumlem3 
|- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) )

Proof

Step Hyp Ref Expression
1 logdivsum.1 
 |-  F = ( y e. RR+ |-> ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( log ` i ) / i ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) )
2 mulog2sumlem.1 
 |-  ( ph -> F ~~>r L )
3 2cn 
 |-  2 e. CC
4 3 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> 2 e. CC )
5 fzfid 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
6 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
7 6 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
8 mucl 
 |-  ( n e. NN -> ( mmu ` n ) e. ZZ )
9 7 8 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. ZZ )
10 9 zred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. RR )
11 10 7 nndivred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. RR )
12 11 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. CC )
13 simpr 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
14 6 nnrpd 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. RR+ )
15 rpdivcl 
 |-  ( ( x e. RR+ /\ n e. RR+ ) -> ( x / n ) e. RR+ )
16 13 14 15 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
17 16 relogcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR )
18 17 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. CC )
19 18 sqcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) ^ 2 ) e. CC )
20 19 halfcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) e. CC )
21 12 20 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) e. CC )
22 5 21 fsumcl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) e. CC )
23 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
24 23 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR )
25 24 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC )
26 4 22 25 subdid 
 |-  ( ( ph /\ x e. RR+ ) -> ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) ) = ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) - ( 2 x. ( log ` x ) ) ) )
27 5 4 21 fsummulc2 
 |-  ( ( ph /\ x e. RR+ ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) )
28 3 a1i 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. CC )
29 28 12 20 mul12d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) = ( ( ( mmu ` n ) / n ) x. ( 2 x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) )
30 2ne0 
 |-  2 =/= 0
31 30 a1i 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 =/= 0 )
32 19 28 31 divcan2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) = ( ( log ` ( x / n ) ) ^ 2 ) )
33 32 oveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( 2 x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) = ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) )
34 29 33 eqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) = ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) )
35 34 sumeq2dv 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) )
36 27 35 eqtrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) )
37 36 oveq1d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) ) - ( 2 x. ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) )
38 26 37 eqtrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) )
39 38 mpteq2dva 
 |-  ( ph -> ( x e. RR+ |-> ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) ) )
40 22 25 subcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) e. CC )
41 rpssre 
 |-  RR+ C_ RR
42 o1const 
 |-  ( ( RR+ C_ RR /\ 2 e. CC ) -> ( x e. RR+ |-> 2 ) e. O(1) )
43 41 3 42 mp2an 
 |-  ( x e. RR+ |-> 2 ) e. O(1)
44 43 a1i 
 |-  ( ph -> ( x e. RR+ |-> 2 ) e. O(1) )
45 emre 
 |-  gamma e. RR
46 45 recni 
 |-  gamma e. CC
47 mulcl 
 |-  ( ( gamma e. CC /\ ( log ` ( x / n ) ) e. CC ) -> ( gamma x. ( log ` ( x / n ) ) ) e. CC )
48 46 18 47 sylancr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( gamma x. ( log ` ( x / n ) ) ) e. CC )
49 rlimcl 
 |-  ( F ~~>r L -> L e. CC )
50 2 49 syl 
 |-  ( ph -> L e. CC )
51 50 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> L e. CC )
52 48 51 subcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( gamma x. ( log ` ( x / n ) ) ) - L ) e. CC )
53 20 52 addcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) e. CC )
54 12 53 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) e. CC )
55 5 54 fsumcl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) e. CC )
56 12 52 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) e. CC )
57 5 56 fsumcl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) e. CC )
58 55 25 57 sub32d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( log ` x ) ) )
59 5 54 56 fsumsub 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) )
60 12 53 52 subdid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) - ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) = ( ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) )
61 20 52 pncand 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) - ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) = ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) )
62 61 oveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) - ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) = ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) )
63 60 62 eqtr3d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) = ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) )
64 63 sumeq2dv 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) )
65 59 64 eqtr3d 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) )
66 65 oveq1d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( log ` x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) )
67 58 66 eqtrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) )
68 67 mpteq2dva 
 |-  ( ph -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) ) )
69 55 25 subcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( log ` x ) ) e. CC )
70 eqid 
 |-  ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) = ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) )
71 eqid 
 |-  ( ( ( 1 / 2 ) + ( gamma + ( abs ` L ) ) ) + sum_ m e. ( 1 ... 2 ) ( ( log ` ( _e / m ) ) / m ) ) = ( ( ( 1 / 2 ) + ( gamma + ( abs ` L ) ) ) + sum_ m e. ( 1 ... 2 ) ( ( log ` ( _e / m ) ) / m ) )
72 1 2 70 71 mulog2sumlem2 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( log ` x ) ) ) e. O(1) )
73 46 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> gamma e. CC )
74 12 18 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
75 5 73 74 fsummulc2 
 |-  ( ( ph /\ x e. RR+ ) -> ( gamma x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) )
76 50 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> L e. CC )
77 5 76 12 fsummulc1 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. L ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. L ) )
78 75 77 oveq12d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( gamma x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. L ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. L ) ) )
79 mulcl 
 |-  ( ( gamma e. CC /\ ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC ) -> ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. CC )
80 46 74 79 sylancr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. CC )
81 12 51 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. L ) e. CC )
82 5 80 81 fsumsub 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - ( ( ( mmu ` n ) / n ) x. L ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. L ) ) )
83 46 a1i 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> gamma e. CC )
84 83 12 18 mul12d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) = ( ( ( mmu ` n ) / n ) x. ( gamma x. ( log ` ( x / n ) ) ) ) )
85 84 oveq1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - ( ( ( mmu ` n ) / n ) x. L ) ) = ( ( ( ( mmu ` n ) / n ) x. ( gamma x. ( log ` ( x / n ) ) ) ) - ( ( ( mmu ` n ) / n ) x. L ) ) )
86 12 48 51 subdid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) = ( ( ( ( mmu ` n ) / n ) x. ( gamma x. ( log ` ( x / n ) ) ) ) - ( ( ( mmu ` n ) / n ) x. L ) ) )
87 85 86 eqtr4d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - ( ( ( mmu ` n ) / n ) x. L ) ) = ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) )
88 87 sumeq2dv 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( gamma x. ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - ( ( ( mmu ` n ) / n ) x. L ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) )
89 78 82 88 3eqtr2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( gamma x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. L ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) )
90 89 mpteq2dva 
 |-  ( ph -> ( x e. RR+ |-> ( ( gamma x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. L ) ) ) = ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) )
91 5 74 fsumcl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC )
92 mulcl 
 |-  ( ( gamma e. CC /\ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) e. CC ) -> ( gamma x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. CC )
93 46 91 92 sylancr 
 |-  ( ( ph /\ x e. RR+ ) -> ( gamma x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. CC )
94 5 12 fsumcl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) e. CC )
95 94 76 mulcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. L ) e. CC )
96 46 a1i 
 |-  ( ph -> gamma e. CC )
97 o1const 
 |-  ( ( RR+ C_ RR /\ gamma e. CC ) -> ( x e. RR+ |-> gamma ) e. O(1) )
98 41 96 97 sylancr 
 |-  ( ph -> ( x e. RR+ |-> gamma ) e. O(1) )
99 mulogsum 
 |-  ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. O(1)
100 99 a1i 
 |-  ( ph -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) e. O(1) )
101 73 91 98 100 o1mul2 
 |-  ( ph -> ( x e. RR+ |-> ( gamma x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) ) e. O(1) )
102 mudivsum 
 |-  ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) e. O(1)
103 102 a1i 
 |-  ( ph -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) ) e. O(1) )
104 o1const 
 |-  ( ( RR+ C_ RR /\ L e. CC ) -> ( x e. RR+ |-> L ) e. O(1) )
105 41 50 104 sylancr 
 |-  ( ph -> ( x e. RR+ |-> L ) e. O(1) )
106 94 76 103 105 o1mul2 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. L ) ) e. O(1) )
107 93 95 101 106 o1sub2 
 |-  ( ph -> ( x e. RR+ |-> ( ( gamma x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( log ` ( x / n ) ) ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( mmu ` n ) / n ) x. L ) ) ) e. O(1) )
108 90 107 eqeltrrd 
 |-  ( ph -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) e. O(1) )
109 69 57 72 108 o1sub2 
 |-  ( ph -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) - ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) ) e. O(1) )
110 68 109 eqeltrrd 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) ) e. O(1) )
111 4 40 44 110 o1mul2 
 |-  ( ph -> ( x e. RR+ |-> ( 2 x. ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) - ( log ` x ) ) ) ) e. O(1) )
112 39 111 eqeltrrd 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( x / n ) ) ^ 2 ) ) - ( 2 x. ( log ` x ) ) ) ) e. O(1) )