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) )