Metamath Proof Explorer

Theorem mulog2sumlem2

Description: Lemma for mulog2sum . (Contributed by Mario Carneiro, 19-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 )
mulog2sumlem2.t 
|- T = ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) )
mulog2sumlem2.r 
|- R = ( ( ( 1 / 2 ) + ( gamma + ( abs ` L ) ) ) + sum_ m e. ( 1 ... 2 ) ( ( log ` ( _e / m ) ) / m ) )
Assertion mulog2sumlem2 
|- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. T ) - ( 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 mulog2sumlem2.t 
 |-  T = ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) )
4 mulog2sumlem2.r 
 |-  R = ( ( ( 1 / 2 ) + ( gamma + ( abs ` L ) ) ) + sum_ m e. ( 1 ... 2 ) ( ( log ` ( _e / m ) ) / m ) )
5 1red 
 |-  ( ph -> 1 e. RR )
6 2re 
 |-  2 e. RR
7 fzfid 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
8 simpr 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
9 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
10 9 nnrpd 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. RR+ )
11 rpdivcl 
 |-  ( ( x e. RR+ /\ n e. RR+ ) -> ( x / n ) e. RR+ )
12 8 10 11 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
13 12 relogcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR )
14 simplr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
15 13 14 rerpdivcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) / x ) e. RR )
16 7 15 fsumrecl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) e. RR )
17 remulcl 
 |-  ( ( 2 e. RR /\ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) e. RR ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) e. RR )
18 6 16 17 sylancr 
 |-  ( ( ph /\ x e. RR+ ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) e. RR )
19 halfre 
 |-  ( 1 / 2 ) e. RR
20 emre 
 |-  gamma e. RR
21 rlimcl 
 |-  ( F ~~>r L -> L e. CC )
22 2 21 syl 
 |-  ( ph -> L e. CC )
23 22 abscld 
 |-  ( ph -> ( abs ` L ) e. RR )
24 readdcl 
 |-  ( ( gamma e. RR /\ ( abs ` L ) e. RR ) -> ( gamma + ( abs ` L ) ) e. RR )
25 20 23 24 sylancr 
 |-  ( ph -> ( gamma + ( abs ` L ) ) e. RR )
26 readdcl 
 |-  ( ( ( 1 / 2 ) e. RR /\ ( gamma + ( abs ` L ) ) e. RR ) -> ( ( 1 / 2 ) + ( gamma + ( abs ` L ) ) ) e. RR )
27 19 25 26 sylancr 
 |-  ( ph -> ( ( 1 / 2 ) + ( gamma + ( abs ` L ) ) ) e. RR )
28 fzfid 
 |-  ( ph -> ( 1 ... 2 ) e. Fin )
29 epr 
 |-  _e e. RR+
30 elfznn 
 |-  ( m e. ( 1 ... 2 ) -> m e. NN )
31 30 adantl 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> m e. NN )
32 31 nnrpd 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> m e. RR+ )
33 rpdivcl 
 |-  ( ( _e e. RR+ /\ m e. RR+ ) -> ( _e / m ) e. RR+ )
34 29 32 33 sylancr 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> ( _e / m ) e. RR+ )
35 34 relogcld 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> ( log ` ( _e / m ) ) e. RR )
36 35 31 nndivred 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> ( ( log ` ( _e / m ) ) / m ) e. RR )
37 28 36 fsumrecl 
 |-  ( ph -> sum_ m e. ( 1 ... 2 ) ( ( log ` ( _e / m ) ) / m ) e. RR )
38 27 37 readdcld 
 |-  ( ph -> ( ( ( 1 / 2 ) + ( gamma + ( abs ` L ) ) ) + sum_ m e. ( 1 ... 2 ) ( ( log ` ( _e / m ) ) / m ) ) e. RR )
39 4 38 eqeltrid 
 |-  ( ph -> R e. RR )
40 remulcl 
 |-  ( ( R e. RR /\ 2 e. RR ) -> ( R x. 2 ) e. RR )
41 39 6 40 sylancl 
 |-  ( ph -> ( R x. 2 ) e. RR )
42 41 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( R x. 2 ) e. RR )
43 6 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> 2 e. RR )
44 rpssre 
 |-  RR+ C_ RR
45 2cnd 
 |-  ( ph -> 2 e. CC )
46 o1const 
 |-  ( ( RR+ C_ RR /\ 2 e. CC ) -> ( x e. RR+ |-> 2 ) e. O(1) )
47 44 45 46 sylancr 
 |-  ( ph -> ( x e. RR+ |-> 2 ) e. O(1) )
48 logfacrlim2 
 |-  ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) ~~>r 1
49 rlimo1 
 |-  ( ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) ~~>r 1 -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) e. O(1) )
50 48 49 mp1i 
 |-  ( ph -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) e. O(1) )
51 43 16 47 50 o1mul2 
 |-  ( ph -> ( x e. RR+ |-> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) ) e. O(1) )
52 41 recnd 
 |-  ( ph -> ( R x. 2 ) e. CC )
53 o1const 
 |-  ( ( RR+ C_ RR /\ ( R x. 2 ) e. CC ) -> ( x e. RR+ |-> ( R x. 2 ) ) e. O(1) )
54 44 52 53 sylancr 
 |-  ( ph -> ( x e. RR+ |-> ( R x. 2 ) ) e. O(1) )
55 18 42 51 54 o1add2 
 |-  ( ph -> ( x e. RR+ |-> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) + ( R x. 2 ) ) ) e. O(1) )
56 18 42 readdcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) + ( R x. 2 ) ) e. RR )
57 9 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
58 mucl 
 |-  ( n e. NN -> ( mmu ` n ) e. ZZ )
59 57 58 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. ZZ )
60 59 zred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. RR )
61 60 57 nndivred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. RR )
62 61 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. CC )
63 13 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. CC )
64 63 sqcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) ^ 2 ) e. CC )
65 64 halfcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) e. CC )
66 remulcl 
 |-  ( ( gamma e. RR /\ ( log ` ( x / n ) ) e. RR ) -> ( gamma x. ( log ` ( x / n ) ) ) e. RR )
67 20 13 66 sylancr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( gamma x. ( log ` ( x / n ) ) ) e. RR )
68 67 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( gamma x. ( log ` ( x / n ) ) ) e. CC )
69 22 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> L e. CC )
70 68 69 subcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( gamma x. ( log ` ( x / n ) ) ) - L ) e. CC )
71 65 70 addcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) e. CC )
72 3 71 eqeltrid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> T e. CC )
73 62 72 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. T ) e. CC )
74 7 73 fsumcl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. T ) e. CC )
75 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
76 75 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR )
77 76 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC )
78 74 77 subcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. T ) - ( log ` x ) ) e. CC )
79 78 abscld 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. T ) - ( log ` x ) ) ) e. RR )
80 79 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. T ) - ( log ` x ) ) ) e. RR )
81 56 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) + ( R x. 2 ) ) e. RR )
82 56 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) + ( R x. 2 ) ) e. CC )
83 82 abscld 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) + ( R x. 2 ) ) ) e. RR )
84 83 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) + ( R x. 2 ) ) ) e. RR )
85 59 zcnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. CC )
86 fzfid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / n ) ) ) e. Fin )
87 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` ( x / n ) ) ) -> m e. NN )
88 nnrp 
 |-  ( m e. NN -> m e. RR+ )
89 rpdivcl 
 |-  ( ( ( x / n ) e. RR+ /\ m e. RR+ ) -> ( ( x / n ) / m ) e. RR+ )
90 12 88 89 syl2an 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( ( x / n ) / m ) e. RR+ )
91 90 relogcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( log ` ( ( x / n ) / m ) ) e. RR )
92 simpr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> m e. NN )
93 91 92 nndivred 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( ( log ` ( ( x / n ) / m ) ) / m ) e. RR )
94 93 recnd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( ( log ` ( ( x / n ) / m ) ) / m ) e. CC )
95 87 94 sylan2 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( log ` ( ( x / n ) / m ) ) / m ) e. CC )
96 86 95 fsumcl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) e. CC )
97 72 96 subcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) e. CC )
98 57 nncnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
99 57 nnne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
100 85 97 98 99 div23d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) / n ) = ( ( ( mmu ` n ) / n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) )
101 62 72 96 subdid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) = ( ( ( ( mmu ` n ) / n ) x. T ) - ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) )
102 100 101 eqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) / n ) = ( ( ( ( mmu ` n ) / n ) x. T ) - ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) )
103 102 sumeq2dv 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) / n ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( mmu ` n ) / n ) x. T ) - ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) )
104 62 96 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) e. CC )
105 7 73 104 fsumsub 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( ( mmu ` n ) / n ) x. T ) - ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. T ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) )
106 103 105 eqtrd 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) / n ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. T ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) )
107 106 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) / n ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. T ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) )
108 86 62 95 fsummulc2 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( ( x / n ) / m ) ) / m ) ) )
109 85 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( mmu ` n ) e. CC )
110 98 99 jca 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n e. CC /\ n =/= 0 ) )
111 110 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( n e. CC /\ n =/= 0 ) )
112 div23 
 |-  ( ( ( mmu ` n ) e. CC /\ ( ( log ` ( ( x / n ) / m ) ) / m ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( ( mmu ` n ) x. ( ( log ` ( ( x / n ) / m ) ) / m ) ) / n ) = ( ( ( mmu ` n ) / n ) x. ( ( log ` ( ( x / n ) / m ) ) / m ) ) )
113 divass 
 |-  ( ( ( mmu ` n ) e. CC /\ ( ( log ` ( ( x / n ) / m ) ) / m ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( ( mmu ` n ) x. ( ( log ` ( ( x / n ) / m ) ) / m ) ) / n ) = ( ( mmu ` n ) x. ( ( ( log ` ( ( x / n ) / m ) ) / m ) / n ) ) )
114 112 113 eqtr3d 
 |-  ( ( ( mmu ` n ) e. CC /\ ( ( log ` ( ( x / n ) / m ) ) / m ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( log ` ( ( x / n ) / m ) ) / m ) ) = ( ( mmu ` n ) x. ( ( ( log ` ( ( x / n ) / m ) ) / m ) / n ) ) )
115 109 94 111 114 syl3anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( ( ( mmu ` n ) / n ) x. ( ( log ` ( ( x / n ) / m ) ) / m ) ) = ( ( mmu ` n ) x. ( ( ( log ` ( ( x / n ) / m ) ) / m ) / n ) ) )
116 91 recnd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( log ` ( ( x / n ) / m ) ) e. CC )
117 92 nnrpd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> m e. RR+ )
118 rpcnne0 
 |-  ( m e. RR+ -> ( m e. CC /\ m =/= 0 ) )
119 117 118 syl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( m e. CC /\ m =/= 0 ) )
120 divdiv1 
 |-  ( ( ( log ` ( ( x / n ) / m ) ) e. CC /\ ( m e. CC /\ m =/= 0 ) /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( ( log ` ( ( x / n ) / m ) ) / m ) / n ) = ( ( log ` ( ( x / n ) / m ) ) / ( m x. n ) ) )
121 116 119 111 120 syl3anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( ( ( log ` ( ( x / n ) / m ) ) / m ) / n ) = ( ( log ` ( ( x / n ) / m ) ) / ( m x. n ) ) )
122 rpre 
 |-  ( x e. RR+ -> x e. RR )
123 122 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR )
124 123 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
125 124 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. CC )
126 125 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> x e. CC )
127 divdiv1 
 |-  ( ( x e. CC /\ ( n e. CC /\ n =/= 0 ) /\ ( m e. CC /\ m =/= 0 ) ) -> ( ( x / n ) / m ) = ( x / ( n x. m ) ) )
128 126 111 119 127 syl3anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( ( x / n ) / m ) = ( x / ( n x. m ) ) )
129 128 fveq2d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( log ` ( ( x / n ) / m ) ) = ( log ` ( x / ( n x. m ) ) ) )
130 92 nncnd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> m e. CC )
131 98 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> n e. CC )
132 130 131 mulcomd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( m x. n ) = ( n x. m ) )
133 129 132 oveq12d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( ( log ` ( ( x / n ) / m ) ) / ( m x. n ) ) = ( ( log ` ( x / ( n x. m ) ) ) / ( n x. m ) ) )
134 121 133 eqtrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( ( ( log ` ( ( x / n ) / m ) ) / m ) / n ) = ( ( log ` ( x / ( n x. m ) ) ) / ( n x. m ) ) )
135 134 oveq2d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( ( mmu ` n ) x. ( ( ( log ` ( ( x / n ) / m ) ) / m ) / n ) ) = ( ( mmu ` n ) x. ( ( log ` ( x / ( n x. m ) ) ) / ( n x. m ) ) ) )
136 115 135 eqtrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( ( ( mmu ` n ) / n ) x. ( ( log ` ( ( x / n ) / m ) ) / m ) ) = ( ( mmu ` n ) x. ( ( log ` ( x / ( n x. m ) ) ) / ( n x. m ) ) ) )
137 87 136 sylan2 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( ( mmu ` n ) / n ) x. ( ( log ` ( ( x / n ) / m ) ) / m ) ) = ( ( mmu ` n ) x. ( ( log ` ( x / ( n x. m ) ) ) / ( n x. m ) ) ) )
138 137 sumeq2dv 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( ( mmu ` n ) / n ) x. ( ( log ` ( ( x / n ) / m ) ) / m ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` ( x / ( n x. m ) ) ) / ( n x. m ) ) ) )
139 108 138 eqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` ( x / ( n x. m ) ) ) / ( n x. m ) ) ) )
140 139 sumeq2dv 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` ( x / ( n x. m ) ) ) / ( n x. m ) ) ) )
141 oveq2 
 |-  ( k = ( n x. m ) -> ( x / k ) = ( x / ( n x. m ) ) )
142 141 fveq2d 
 |-  ( k = ( n x. m ) -> ( log ` ( x / k ) ) = ( log ` ( x / ( n x. m ) ) ) )
143 id 
 |-  ( k = ( n x. m ) -> k = ( n x. m ) )
144 142 143 oveq12d 
 |-  ( k = ( n x. m ) -> ( ( log ` ( x / k ) ) / k ) = ( ( log ` ( x / ( n x. m ) ) ) / ( n x. m ) ) )
145 144 oveq2d 
 |-  ( k = ( n x. m ) -> ( ( mmu ` n ) x. ( ( log ` ( x / k ) ) / k ) ) = ( ( mmu ` n ) x. ( ( log ` ( x / ( n x. m ) ) ) / ( n x. m ) ) ) )
146 8 rpred 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR )
147 ssrab2 
 |-  { y e. NN | y || k } C_ NN
148 simprr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> n e. { y e. NN | y || k } )
149 147 148 sselid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> n e. NN )
150 149 58 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( mmu ` n ) e. ZZ )
151 150 zred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( mmu ` n ) e. RR )
152 elfznn 
 |-  ( k e. ( 1 ... ( |_ ` x ) ) -> k e. NN )
153 152 adantr 
 |-  ( ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) -> k e. NN )
154 153 nnrpd 
 |-  ( ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) -> k e. RR+ )
155 rpdivcl 
 |-  ( ( x e. RR+ /\ k e. RR+ ) -> ( x / k ) e. RR+ )
156 8 154 155 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( x / k ) e. RR+ )
157 156 relogcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( log ` ( x / k ) ) e. RR )
158 152 ad2antrl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> k e. NN )
159 157 158 nndivred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( ( log ` ( x / k ) ) / k ) e. RR )
160 151 159 remulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( ( mmu ` n ) x. ( ( log ` ( x / k ) ) / k ) ) e. RR )
161 160 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( k e. ( 1 ... ( |_ ` x ) ) /\ n e. { y e. NN | y || k } ) ) -> ( ( mmu ` n ) x. ( ( log ` ( x / k ) ) / k ) ) e. CC )
162 145 146 161 dvdsflsumcom 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ n e. { y e. NN | y || k } ( ( mmu ` n ) x. ( ( log ` ( x / k ) ) / k ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( mmu ` n ) x. ( ( log ` ( x / ( n x. m ) ) ) / ( n x. m ) ) ) )
163 140 162 eqtr4d 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) = sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ n e. { y e. NN | y || k } ( ( mmu ` n ) x. ( ( log ` ( x / k ) ) / k ) ) )
164 163 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) = sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ n e. { y e. NN | y || k } ( ( mmu ` n ) x. ( ( log ` ( x / k ) ) / k ) ) )
165 oveq2 
 |-  ( k = 1 -> ( x / k ) = ( x / 1 ) )
166 165 fveq2d 
 |-  ( k = 1 -> ( log ` ( x / k ) ) = ( log ` ( x / 1 ) ) )
167 id 
 |-  ( k = 1 -> k = 1 )
168 166 167 oveq12d 
 |-  ( k = 1 -> ( ( log ` ( x / k ) ) / k ) = ( ( log ` ( x / 1 ) ) / 1 ) )
169 fzfid 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
170 fz1ssnn 
 |-  ( 1 ... ( |_ ` x ) ) C_ NN
171 170 a1i 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 ... ( |_ ` x ) ) C_ NN )
172 123 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR )
173 simprr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 <_ x )
174 flge1nn 
 |-  ( ( x e. RR /\ 1 <_ x ) -> ( |_ ` x ) e. NN )
175 172 173 174 syl2anc 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) e. NN )
176 nnuz 
 |-  NN = ( ZZ>= ` 1 )
177 175 176 eleqtrdi 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) e. ( ZZ>= ` 1 ) )
178 eluzfz1 
 |-  ( ( |_ ` x ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( |_ ` x ) ) )
179 177 178 syl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 e. ( 1 ... ( |_ ` x ) ) )
180 152 nnrpd 
 |-  ( k e. ( 1 ... ( |_ ` x ) ) -> k e. RR+ )
181 8 180 155 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( x / k ) e. RR+ )
182 181 relogcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / k ) ) e. RR )
183 170 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) C_ NN )
184 183 sselda 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> k e. NN )
185 182 184 nndivred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / k ) ) / k ) e. RR )
186 185 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / k ) ) / k ) e. CC )
187 186 adantlrr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ k e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / k ) ) / k ) e. CC )
188 168 169 171 179 187 musumsum 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ k e. ( 1 ... ( |_ ` x ) ) sum_ n e. { y e. NN | y || k } ( ( mmu ` n ) x. ( ( log ` ( x / k ) ) / k ) ) = ( ( log ` ( x / 1 ) ) / 1 ) )
189 8 rpcnd 
 |-  ( ( ph /\ x e. RR+ ) -> x e. CC )
190 189 div1d 
 |-  ( ( ph /\ x e. RR+ ) -> ( x / 1 ) = x )
191 190 fveq2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` ( x / 1 ) ) = ( log ` x ) )
192 191 oveq1d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` ( x / 1 ) ) / 1 ) = ( ( log ` x ) / 1 ) )
193 77 div1d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) / 1 ) = ( log ` x ) )
194 192 193 eqtrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` ( x / 1 ) ) / 1 ) = ( log ` x ) )
195 194 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` ( x / 1 ) ) / 1 ) = ( log ` x ) )
196 164 188 195 3eqtrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) = ( log ` x ) )
197 196 oveq2d 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. T ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. T ) - ( log ` x ) ) )
198 107 197 eqtrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) / n ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. T ) - ( log ` x ) ) )
199 198 fveq2d 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) / n ) ) = ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. T ) - ( log ` x ) ) ) )
200 ere 
 |-  _e e. RR
201 200 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> _e e. RR )
202 1re 
 |-  1 e. RR
203 1lt2 
 |-  1 < 2
204 egt2lt3 
 |-  ( 2 < _e /\ _e < 3 )
205 204 simpli 
 |-  2 < _e
206 202 6 200 lttri 
 |-  ( ( 1 < 2 /\ 2 < _e ) -> 1 < _e )
207 203 205 206 mp2an 
 |-  1 < _e
208 202 200 207 ltleii 
 |-  1 <_ _e
209 201 208 jctir 
 |-  ( ( ph /\ x e. RR+ ) -> ( _e e. RR /\ 1 <_ _e ) )
210 39 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> R e. RR )
211 19 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
212 1rp 
 |-  1 e. RR+
213 rphalfcl 
 |-  ( 1 e. RR+ -> ( 1 / 2 ) e. RR+ )
214 212 213 ax-mp 
 |-  ( 1 / 2 ) e. RR+
215 rpge0 
 |-  ( ( 1 / 2 ) e. RR+ -> 0 <_ ( 1 / 2 ) )
216 214 215 mp1i 
 |-  ( ph -> 0 <_ ( 1 / 2 ) )
217 20 a1i 
 |-  ( ph -> gamma e. RR )
218 0re 
 |-  0 e. RR
219 emgt0 
 |-  0 < gamma
220 218 20 219 ltleii 
 |-  0 <_ gamma
221 220 a1i 
 |-  ( ph -> 0 <_ gamma )
222 22 absge0d 
 |-  ( ph -> 0 <_ ( abs ` L ) )
223 217 23 221 222 addge0d 
 |-  ( ph -> 0 <_ ( gamma + ( abs ` L ) ) )
224 211 25 216 223 addge0d 
 |-  ( ph -> 0 <_ ( ( 1 / 2 ) + ( gamma + ( abs ` L ) ) ) )
225 log1 
 |-  ( log ` 1 ) = 0
226 31 nncnd 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> m e. CC )
227 226 mulid2d 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> ( 1 x. m ) = m )
228 32 rpred 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> m e. RR )
229 6 a1i 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> 2 e. RR )
230 200 a1i 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> _e e. RR )
231 elfzle2 
 |-  ( m e. ( 1 ... 2 ) -> m <_ 2 )
232 231 adantl 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> m <_ 2 )
233 6 200 205 ltleii 
 |-  2 <_ _e
234 233 a1i 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> 2 <_ _e )
235 228 229 230 232 234 letrd 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> m <_ _e )
236 227 235 eqbrtrd 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> ( 1 x. m ) <_ _e )
237 1red 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> 1 e. RR )
238 237 230 32 lemuldivd 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> ( ( 1 x. m ) <_ _e <-> 1 <_ ( _e / m ) ) )
239 236 238 mpbid 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> 1 <_ ( _e / m ) )
240 logleb 
 |-  ( ( 1 e. RR+ /\ ( _e / m ) e. RR+ ) -> ( 1 <_ ( _e / m ) <-> ( log ` 1 ) <_ ( log ` ( _e / m ) ) ) )
241 212 34 240 sylancr 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> ( 1 <_ ( _e / m ) <-> ( log ` 1 ) <_ ( log ` ( _e / m ) ) ) )
242 239 241 mpbid 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> ( log ` 1 ) <_ ( log ` ( _e / m ) ) )
243 225 242 eqbrtrrid 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> 0 <_ ( log ` ( _e / m ) ) )
244 35 32 243 divge0d 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> 0 <_ ( ( log ` ( _e / m ) ) / m ) )
245 28 36 244 fsumge0 
 |-  ( ph -> 0 <_ sum_ m e. ( 1 ... 2 ) ( ( log ` ( _e / m ) ) / m ) )
246 27 37 224 245 addge0d 
 |-  ( ph -> 0 <_ ( ( ( 1 / 2 ) + ( gamma + ( abs ` L ) ) ) + sum_ m e. ( 1 ... 2 ) ( ( log ` ( _e / m ) ) / m ) ) )
247 246 4 breqtrrdi 
 |-  ( ph -> 0 <_ R )
248 247 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> 0 <_ R )
249 210 248 jca 
 |-  ( ( ph /\ x e. RR+ ) -> ( R e. RR /\ 0 <_ R ) )
250 85 97 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) e. CC )
251 remulcl 
 |-  ( ( 2 e. RR /\ ( ( log ` ( x / n ) ) / x ) e. RR ) -> ( 2 x. ( ( log ` ( x / n ) ) / x ) ) e. RR )
252 6 15 251 sylancr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( log ` ( x / n ) ) / x ) ) e. RR )
253 6 a1i 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. RR )
254 0le2 
 |-  0 <_ 2
255 254 a1i 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ 2 )
256 98 mulid2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) = n )
257 fznnfl 
 |-  ( x e. RR -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) )
258 123 257 syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( n e. ( 1 ... ( |_ ` x ) ) <-> ( n e. NN /\ n <_ x ) ) )
259 258 simplbda 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n <_ x )
260 256 259 eqbrtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. n ) <_ x )
261 1red 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
262 57 nnrpd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
263 261 124 262 lemuldivd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 x. n ) <_ x <-> 1 <_ ( x / n ) ) )
264 260 263 mpbid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ ( x / n ) )
265 logleb 
 |-  ( ( 1 e. RR+ /\ ( x / n ) e. RR+ ) -> ( 1 <_ ( x / n ) <-> ( log ` 1 ) <_ ( log ` ( x / n ) ) ) )
266 212 12 265 sylancr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 <_ ( x / n ) <-> ( log ` 1 ) <_ ( log ` ( x / n ) ) ) )
267 264 266 mpbid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` 1 ) <_ ( log ` ( x / n ) ) )
268 225 267 eqbrtrrid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( log ` ( x / n ) ) )
269 rpregt0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 < x ) )
270 269 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x e. RR /\ 0 < x ) )
271 divge0 
 |-  ( ( ( ( log ` ( x / n ) ) e. RR /\ 0 <_ ( log ` ( x / n ) ) ) /\ ( x e. RR /\ 0 < x ) ) -> 0 <_ ( ( log ` ( x / n ) ) / x ) )
272 13 268 270 271 syl21anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( log ` ( x / n ) ) / x ) )
273 253 15 255 272 mulge0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( 2 x. ( ( log ` ( x / n ) ) / x ) ) )
274 250 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) ) e. RR )
275 274 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ _e <_ ( x / n ) ) -> ( abs ` ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) ) e. RR )
276 97 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ _e <_ ( x / n ) ) -> ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) e. CC )
277 276 abscld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ _e <_ ( x / n ) ) -> ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) e. RR )
278 262 rpred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR )
279 252 278 remulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. ( ( log ` ( x / n ) ) / x ) ) x. n ) e. RR )
280 279 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ _e <_ ( x / n ) ) -> ( ( 2 x. ( ( log ` ( x / n ) ) / x ) ) x. n ) e. RR )
281 85 97 absmuld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) ) = ( ( abs ` ( mmu ` n ) ) x. ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) ) )
282 85 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( mmu ` n ) ) e. RR )
283 97 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) e. RR )
284 97 absge0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) )
285 mule1 
 |-  ( n e. NN -> ( abs ` ( mmu ` n ) ) <_ 1 )
286 57 285 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( mmu ` n ) ) <_ 1 )
287 282 261 283 284 286 lemul1ad 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( mmu ` n ) ) x. ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) ) <_ ( 1 x. ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) ) )
288 283 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) e. CC )
289 288 mulid2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) ) = ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) )
290 287 289 breqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( mmu ` n ) ) x. ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) ) <_ ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) )
291 281 290 eqbrtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) ) <_ ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) )
292 291 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ _e <_ ( x / n ) ) -> ( abs ` ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) ) <_ ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) )
293 2 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ _e <_ ( x / n ) ) -> F ~~>r L )
294 12 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ _e <_ ( x / n ) ) -> ( x / n ) e. RR+ )
295 simpr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ _e <_ ( x / n ) ) -> _e <_ ( x / n ) )
296 1 293 294 295 mulog2sumlem1 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ _e <_ ( x / n ) ) -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) - ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) ) <_ ( 2 x. ( ( log ` ( x / n ) ) / ( x / n ) ) ) )
297 72 96 abssubd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) = ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) - T ) ) )
298 297 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ _e <_ ( x / n ) ) -> ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) = ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) - T ) ) )
299 3 oveq2i 
 |-  ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) - T ) = ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) - ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) )
300 299 fveq2i 
 |-  ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) - T ) ) = ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) - ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) )
301 298 300 eqtrdi 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ _e <_ ( x / n ) ) -> ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) = ( abs ` ( sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) - ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) ) )
302 2cnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 2 e. CC )
303 15 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) / x ) e. CC )
304 302 303 98 mulassd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. ( ( log ` ( x / n ) ) / x ) ) x. n ) = ( 2 x. ( ( ( log ` ( x / n ) ) / x ) x. n ) ) )
305 rpcnne0 
 |-  ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) )
306 305 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x e. CC /\ x =/= 0 ) )
307 divdiv2 
 |-  ( ( ( log ` ( x / n ) ) e. CC /\ ( x e. CC /\ x =/= 0 ) /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( log ` ( x / n ) ) / ( x / n ) ) = ( ( ( log ` ( x / n ) ) x. n ) / x ) )
308 63 306 110 307 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) / ( x / n ) ) = ( ( ( log ` ( x / n ) ) x. n ) / x ) )
309 div23 
 |-  ( ( ( log ` ( x / n ) ) e. CC /\ n e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( log ` ( x / n ) ) x. n ) / x ) = ( ( ( log ` ( x / n ) ) / x ) x. n ) )
310 63 98 306 309 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` ( x / n ) ) x. n ) / x ) = ( ( ( log ` ( x / n ) ) / x ) x. n ) )
311 308 310 eqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) / ( x / n ) ) = ( ( ( log ` ( x / n ) ) / x ) x. n ) )
312 311 oveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 x. ( ( log ` ( x / n ) ) / ( x / n ) ) ) = ( 2 x. ( ( ( log ` ( x / n ) ) / x ) x. n ) ) )
313 304 312 eqtr4d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 2 x. ( ( log ` ( x / n ) ) / x ) ) x. n ) = ( 2 x. ( ( log ` ( x / n ) ) / ( x / n ) ) ) )
314 313 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ _e <_ ( x / n ) ) -> ( ( 2 x. ( ( log ` ( x / n ) ) / x ) ) x. n ) = ( 2 x. ( ( log ` ( x / n ) ) / ( x / n ) ) ) )
315 296 301 314 3brtr4d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ _e <_ ( x / n ) ) -> ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) <_ ( ( 2 x. ( ( log ` ( x / n ) ) / x ) ) x. n ) )
316 275 277 280 292 315 letrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ _e <_ ( x / n ) ) -> ( abs ` ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) ) <_ ( ( 2 x. ( ( log ` ( x / n ) ) / x ) ) x. n ) )
317 274 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) ) e. RR )
318 283 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) e. RR )
319 39 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> R e. RR )
320 291 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) ) <_ ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) )
321 72 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> T e. CC )
322 321 abscld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` T ) e. RR )
323 96 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) e. CC )
324 323 abscld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) e. RR )
325 322 324 readdcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( abs ` T ) + ( abs ` sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) e. RR )
326 321 323 abs2dif2d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) <_ ( ( abs ` T ) + ( abs ` sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) )
327 27 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( 1 / 2 ) + ( gamma + ( abs ` L ) ) ) e. RR )
328 37 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> sum_ m e. ( 1 ... 2 ) ( ( log ` ( _e / m ) ) / m ) e. RR )
329 3 fveq2i 
 |-  ( abs ` T ) = ( abs ` ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) )
330 329 322 eqeltrrid 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) e. RR )
331 65 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) e. CC )
332 331 abscld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) e. RR )
333 70 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( gamma x. ( log ` ( x / n ) ) ) - L ) e. CC )
334 333 abscld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) e. RR )
335 332 334 readdcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( abs ` ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) + ( abs ` ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) e. RR )
336 331 333 abstrid 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) <_ ( ( abs ` ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) + ( abs ` ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) )
337 19 a1i 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( 1 / 2 ) e. RR )
338 25 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( gamma + ( abs ` L ) ) e. RR )
339 13 resqcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) ^ 2 ) e. RR )
340 339 rehalfcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) e. RR )
341 13 sqge0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( log ` ( x / n ) ) ^ 2 ) )
342 2pos 
 |-  0 < 2
343 6 342 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
344 343 a1i 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 2 e. RR /\ 0 < 2 ) )
345 divge0 
 |-  ( ( ( ( ( log ` ( x / n ) ) ^ 2 ) e. RR /\ 0 <_ ( ( log ` ( x / n ) ) ^ 2 ) ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 <_ ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) )
346 339 341 344 345 syl21anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) )
347 340 346 absidd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) = ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) )
348 347 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) = ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) )
349 12 rpred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR )
350 ltle 
 |-  ( ( ( x / n ) e. RR /\ _e e. RR ) -> ( ( x / n ) < _e -> ( x / n ) <_ _e ) )
351 349 200 350 sylancl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( x / n ) < _e -> ( x / n ) <_ _e ) )
352 351 imp 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( x / n ) <_ _e )
353 12 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( x / n ) e. RR+ )
354 logleb 
 |-  ( ( ( x / n ) e. RR+ /\ _e e. RR+ ) -> ( ( x / n ) <_ _e <-> ( log ` ( x / n ) ) <_ ( log ` _e ) ) )
355 353 29 354 sylancl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( x / n ) <_ _e <-> ( log ` ( x / n ) ) <_ ( log ` _e ) ) )
356 352 355 mpbid 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( log ` ( x / n ) ) <_ ( log ` _e ) )
357 loge 
 |-  ( log ` _e ) = 1
358 356 357 breqtrdi 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( log ` ( x / n ) ) <_ 1 )
359 0le1 
 |-  0 <_ 1
360 359 a1i 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ 1 )
361 13 261 268 360 le2sqd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) <_ 1 <-> ( ( log ` ( x / n ) ) ^ 2 ) <_ ( 1 ^ 2 ) ) )
362 361 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( log ` ( x / n ) ) <_ 1 <-> ( ( log ` ( x / n ) ) ^ 2 ) <_ ( 1 ^ 2 ) ) )
363 358 362 mpbid 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( log ` ( x / n ) ) ^ 2 ) <_ ( 1 ^ 2 ) )
364 sq1 
 |-  ( 1 ^ 2 ) = 1
365 363 364 breqtrdi 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( log ` ( x / n ) ) ^ 2 ) <_ 1 )
366 339 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( log ` ( x / n ) ) ^ 2 ) e. RR )
367 1red 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> 1 e. RR )
368 343 a1i 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( 2 e. RR /\ 0 < 2 ) )
369 lediv1 
 |-  ( ( ( ( log ` ( x / n ) ) ^ 2 ) e. RR /\ 1 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( log ` ( x / n ) ) ^ 2 ) <_ 1 <-> ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) <_ ( 1 / 2 ) ) )
370 366 367 368 369 syl3anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( ( log ` ( x / n ) ) ^ 2 ) <_ 1 <-> ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) <_ ( 1 / 2 ) ) )
371 365 370 mpbid 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) <_ ( 1 / 2 ) )
372 348 371 eqbrtrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) <_ ( 1 / 2 ) )
373 69 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` L ) e. RR )
374 67 373 readdcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( gamma x. ( log ` ( x / n ) ) ) + ( abs ` L ) ) e. RR )
375 374 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( gamma x. ( log ` ( x / n ) ) ) + ( abs ` L ) ) e. RR )
376 68 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( gamma x. ( log ` ( x / n ) ) ) e. CC )
377 22 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> L e. CC )
378 376 377 abs2dif2d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) <_ ( ( abs ` ( gamma x. ( log ` ( x / n ) ) ) ) + ( abs ` L ) ) )
379 20 a1i 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> gamma e. RR )
380 220 a1i 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ gamma )
381 379 13 380 268 mulge0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( gamma x. ( log ` ( x / n ) ) ) )
382 67 381 absidd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( gamma x. ( log ` ( x / n ) ) ) ) = ( gamma x. ( log ` ( x / n ) ) ) )
383 382 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` ( gamma x. ( log ` ( x / n ) ) ) ) = ( gamma x. ( log ` ( x / n ) ) ) )
384 383 oveq1d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( abs ` ( gamma x. ( log ` ( x / n ) ) ) ) + ( abs ` L ) ) = ( ( gamma x. ( log ` ( x / n ) ) ) + ( abs ` L ) ) )
385 378 384 breqtrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) <_ ( ( gamma x. ( log ` ( x / n ) ) ) + ( abs ` L ) ) )
386 67 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( gamma x. ( log ` ( x / n ) ) ) e. RR )
387 20 a1i 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> gamma e. RR )
388 377 abscld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` L ) e. RR )
389 13 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( log ` ( x / n ) ) e. RR )
390 387 219 jctir 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( gamma e. RR /\ 0 < gamma ) )
391 lemul2 
 |-  ( ( ( log ` ( x / n ) ) e. RR /\ 1 e. RR /\ ( gamma e. RR /\ 0 < gamma ) ) -> ( ( log ` ( x / n ) ) <_ 1 <-> ( gamma x. ( log ` ( x / n ) ) ) <_ ( gamma x. 1 ) ) )
392 389 367 390 391 syl3anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( log ` ( x / n ) ) <_ 1 <-> ( gamma x. ( log ` ( x / n ) ) ) <_ ( gamma x. 1 ) ) )
393 358 392 mpbid 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( gamma x. ( log ` ( x / n ) ) ) <_ ( gamma x. 1 ) )
394 20 recni 
 |-  gamma e. CC
395 394 mulid1i 
 |-  ( gamma x. 1 ) = gamma
396 393 395 breqtrdi 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( gamma x. ( log ` ( x / n ) ) ) <_ gamma )
397 386 387 388 396 leadd1dd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( gamma x. ( log ` ( x / n ) ) ) + ( abs ` L ) ) <_ ( gamma + ( abs ` L ) ) )
398 334 375 338 385 397 letrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) <_ ( gamma + ( abs ` L ) ) )
399 332 334 337 338 372 398 le2addd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( abs ` ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) ) + ( abs ` ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) <_ ( ( 1 / 2 ) + ( gamma + ( abs ` L ) ) ) )
400 330 335 327 336 399 letrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` ( ( ( ( log ` ( x / n ) ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` ( x / n ) ) ) - L ) ) ) <_ ( ( 1 / 2 ) + ( gamma + ( abs ` L ) ) ) )
401 329 400 eqbrtrid 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` T ) <_ ( ( 1 / 2 ) + ( gamma + ( abs ` L ) ) ) )
402 87 93 sylan2 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( log ` ( ( x / n ) / m ) ) / m ) e. RR )
403 86 402 fsumrecl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) e. RR )
404 403 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) e. RR )
405 87 91 sylan2 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( log ` ( ( x / n ) / m ) ) e. RR )
406 87 130 sylan2 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. CC )
407 406 mulid2d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( 1 x. m ) = m )
408 fznnfl 
 |-  ( ( x / n ) e. RR -> ( m e. ( 1 ... ( |_ ` ( x / n ) ) ) <-> ( m e. NN /\ m <_ ( x / n ) ) ) )
409 349 408 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( m e. ( 1 ... ( |_ ` ( x / n ) ) ) <-> ( m e. NN /\ m <_ ( x / n ) ) ) )
410 409 simplbda 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m <_ ( x / n ) )
411 407 410 eqbrtrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( 1 x. m ) <_ ( x / n ) )
412 1red 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> 1 e. RR )
413 349 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( x / n ) e. RR )
414 117 rpregt0d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. NN ) -> ( m e. RR /\ 0 < m ) )
415 87 414 sylan2 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( m e. RR /\ 0 < m ) )
416 lemuldiv 
 |-  ( ( 1 e. RR /\ ( x / n ) e. RR /\ ( m e. RR /\ 0 < m ) ) -> ( ( 1 x. m ) <_ ( x / n ) <-> 1 <_ ( ( x / n ) / m ) ) )
417 412 413 415 416 syl3anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( 1 x. m ) <_ ( x / n ) <-> 1 <_ ( ( x / n ) / m ) ) )
418 411 417 mpbid 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> 1 <_ ( ( x / n ) / m ) )
419 87 90 sylan2 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( x / n ) / m ) e. RR+ )
420 logleb 
 |-  ( ( 1 e. RR+ /\ ( ( x / n ) / m ) e. RR+ ) -> ( 1 <_ ( ( x / n ) / m ) <-> ( log ` 1 ) <_ ( log ` ( ( x / n ) / m ) ) ) )
421 212 419 420 sylancr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( 1 <_ ( ( x / n ) / m ) <-> ( log ` 1 ) <_ ( log ` ( ( x / n ) / m ) ) ) )
422 418 421 mpbid 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( log ` 1 ) <_ ( log ` ( ( x / n ) / m ) ) )
423 225 422 eqbrtrrid 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> 0 <_ ( log ` ( ( x / n ) / m ) ) )
424 divge0 
 |-  ( ( ( ( log ` ( ( x / n ) / m ) ) e. RR /\ 0 <_ ( log ` ( ( x / n ) / m ) ) ) /\ ( m e. RR /\ 0 < m ) ) -> 0 <_ ( ( log ` ( ( x / n ) / m ) ) / m ) )
425 405 423 415 424 syl21anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> 0 <_ ( ( log ` ( ( x / n ) / m ) ) / m ) )
426 86 402 425 fsumge0 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) )
427 426 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> 0 <_ sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) )
428 404 427 absidd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) )
429 fzfid 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( 1 ... ( |_ ` ( x / n ) ) ) e. Fin )
430 349 flcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( x / n ) ) e. ZZ )
431 430 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( |_ ` ( x / n ) ) e. ZZ )
432 2z 
 |-  2 e. ZZ
433 432 a1i 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> 2 e. ZZ )
434 349 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( x / n ) e. RR )
435 200 a1i 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> _e e. RR )
436 3re 
 |-  3 e. RR
437 436 a1i 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> 3 e. RR )
438 simpr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( x / n ) < _e )
439 204 simpri 
 |-  _e < 3
440 439 a1i 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> _e < 3 )
441 434 435 437 438 440 lttrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( x / n ) < 3 )
442 3z 
 |-  3 e. ZZ
443 fllt 
 |-  ( ( ( x / n ) e. RR /\ 3 e. ZZ ) -> ( ( x / n ) < 3 <-> ( |_ ` ( x / n ) ) < 3 ) )
444 434 442 443 sylancl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( x / n ) < 3 <-> ( |_ ` ( x / n ) ) < 3 ) )
445 441 444 mpbid 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( |_ ` ( x / n ) ) < 3 )
446 df-3 
 |-  3 = ( 2 + 1 )
447 445 446 breqtrdi 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( |_ ` ( x / n ) ) < ( 2 + 1 ) )
448 zleltp1 
 |-  ( ( ( |_ ` ( x / n ) ) e. ZZ /\ 2 e. ZZ ) -> ( ( |_ ` ( x / n ) ) <_ 2 <-> ( |_ ` ( x / n ) ) < ( 2 + 1 ) ) )
449 431 432 448 sylancl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( |_ ` ( x / n ) ) <_ 2 <-> ( |_ ` ( x / n ) ) < ( 2 + 1 ) ) )
450 447 449 mpbird 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( |_ ` ( x / n ) ) <_ 2 )
451 eluz2 
 |-  ( 2 e. ( ZZ>= ` ( |_ ` ( x / n ) ) ) <-> ( ( |_ ` ( x / n ) ) e. ZZ /\ 2 e. ZZ /\ ( |_ ` ( x / n ) ) <_ 2 ) )
452 431 433 450 451 syl3anbrc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> 2 e. ( ZZ>= ` ( |_ ` ( x / n ) ) ) )
453 fzss2 
 |-  ( 2 e. ( ZZ>= ` ( |_ ` ( x / n ) ) ) -> ( 1 ... ( |_ ` ( x / n ) ) ) C_ ( 1 ... 2 ) )
454 452 453 syl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( 1 ... ( |_ ` ( x / n ) ) ) C_ ( 1 ... 2 ) )
455 454 sselda 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> m e. ( 1 ... 2 ) )
456 36 ad5ant15 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... 2 ) ) -> ( ( log ` ( _e / m ) ) / m ) e. RR )
457 455 456 syldan 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( log ` ( _e / m ) ) / m ) e. RR )
458 429 457 fsumrecl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( _e / m ) ) / m ) e. RR )
459 93 adantlr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. NN ) -> ( ( log ` ( ( x / n ) / m ) ) / m ) e. RR )
460 87 459 sylan2 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( log ` ( ( x / n ) / m ) ) / m ) e. RR )
461 352 adantr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... 2 ) ) -> ( x / n ) <_ _e )
462 434 adantr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... 2 ) ) -> ( x / n ) e. RR )
463 200 a1i 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... 2 ) ) -> _e e. RR )
464 32 rpregt0d 
 |-  ( ( ph /\ m e. ( 1 ... 2 ) ) -> ( m e. RR /\ 0 < m ) )
465 464 ad5ant15 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... 2 ) ) -> ( m e. RR /\ 0 < m ) )
466 lediv1 
 |-  ( ( ( x / n ) e. RR /\ _e e. RR /\ ( m e. RR /\ 0 < m ) ) -> ( ( x / n ) <_ _e <-> ( ( x / n ) / m ) <_ ( _e / m ) ) )
467 462 463 465 466 syl3anc 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... 2 ) ) -> ( ( x / n ) <_ _e <-> ( ( x / n ) / m ) <_ ( _e / m ) ) )
468 461 467 mpbid 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... 2 ) ) -> ( ( x / n ) / m ) <_ ( _e / m ) )
469 90 adantlr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. NN ) -> ( ( x / n ) / m ) e. RR+ )
470 30 469 sylan2 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... 2 ) ) -> ( ( x / n ) / m ) e. RR+ )
471 34 ad5ant15 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... 2 ) ) -> ( _e / m ) e. RR+ )
472 470 471 logled 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... 2 ) ) -> ( ( ( x / n ) / m ) <_ ( _e / m ) <-> ( log ` ( ( x / n ) / m ) ) <_ ( log ` ( _e / m ) ) ) )
473 468 472 mpbid 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... 2 ) ) -> ( log ` ( ( x / n ) / m ) ) <_ ( log ` ( _e / m ) ) )
474 91 adantlr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. NN ) -> ( log ` ( ( x / n ) / m ) ) e. RR )
475 30 474 sylan2 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... 2 ) ) -> ( log ` ( ( x / n ) / m ) ) e. RR )
476 35 ad5ant15 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... 2 ) ) -> ( log ` ( _e / m ) ) e. RR )
477 lediv1 
 |-  ( ( ( log ` ( ( x / n ) / m ) ) e. RR /\ ( log ` ( _e / m ) ) e. RR /\ ( m e. RR /\ 0 < m ) ) -> ( ( log ` ( ( x / n ) / m ) ) <_ ( log ` ( _e / m ) ) <-> ( ( log ` ( ( x / n ) / m ) ) / m ) <_ ( ( log ` ( _e / m ) ) / m ) ) )
478 475 476 465 477 syl3anc 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... 2 ) ) -> ( ( log ` ( ( x / n ) / m ) ) <_ ( log ` ( _e / m ) ) <-> ( ( log ` ( ( x / n ) / m ) ) / m ) <_ ( ( log ` ( _e / m ) ) / m ) ) )
479 473 478 mpbid 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... 2 ) ) -> ( ( log ` ( ( x / n ) / m ) ) / m ) <_ ( ( log ` ( _e / m ) ) / m ) )
480 455 479 syldan 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ) -> ( ( log ` ( ( x / n ) / m ) ) / m ) <_ ( ( log ` ( _e / m ) ) / m ) )
481 429 460 457 480 fsumle 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) <_ sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( _e / m ) ) / m ) )
482 fzfid 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( 1 ... 2 ) e. Fin )
483 244 ad5ant15 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) /\ m e. ( 1 ... 2 ) ) -> 0 <_ ( ( log ` ( _e / m ) ) / m ) )
484 482 456 483 454 fsumless 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( _e / m ) ) / m ) <_ sum_ m e. ( 1 ... 2 ) ( ( log ` ( _e / m ) ) / m ) )
485 404 458 328 481 484 letrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) <_ sum_ m e. ( 1 ... 2 ) ( ( log ` ( _e / m ) ) / m ) )
486 428 485 eqbrtrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) <_ sum_ m e. ( 1 ... 2 ) ( ( log ` ( _e / m ) ) / m ) )
487 322 324 327 328 401 486 le2addd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( abs ` T ) + ( abs ` sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) <_ ( ( ( 1 / 2 ) + ( gamma + ( abs ` L ) ) ) + sum_ m e. ( 1 ... 2 ) ( ( log ` ( _e / m ) ) / m ) ) )
488 487 4 breqtrrdi 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( ( abs ` T ) + ( abs ` sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) <_ R )
489 318 325 319 326 488 letrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) <_ R )
490 317 318 319 320 489 letrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / n ) < _e ) -> ( abs ` ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) ) <_ R )
491 8 209 249 250 252 273 316 490 fsumharmonic 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) / n ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( log ` ( x / n ) ) / x ) ) + ( R x. ( ( log ` _e ) + 1 ) ) ) )
492 2cnd 
 |-  ( ( ph /\ x e. RR+ ) -> 2 e. CC )
493 7 492 303 fsummulc2 
 |-  ( ( ph /\ x e. RR+ ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( log ` ( x / n ) ) / x ) ) )
494 df-2 
 |-  2 = ( 1 + 1 )
495 357 oveq1i 
 |-  ( ( log ` _e ) + 1 ) = ( 1 + 1 )
496 494 495 eqtr4i 
 |-  2 = ( ( log ` _e ) + 1 )
497 496 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> 2 = ( ( log ` _e ) + 1 ) )
498 497 oveq2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( R x. 2 ) = ( R x. ( ( log ` _e ) + 1 ) ) )
499 493 498 oveq12d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) + ( R x. 2 ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 2 x. ( ( log ` ( x / n ) ) / x ) ) + ( R x. ( ( log ` _e ) + 1 ) ) ) )
500 491 499 breqtrrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) / n ) ) <_ ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) + ( R x. 2 ) ) )
501 500 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) x. ( T - sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( log ` ( ( x / n ) / m ) ) / m ) ) ) / n ) ) <_ ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) + ( R x. 2 ) ) )
502 199 501 eqbrtrrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. T ) - ( log ` x ) ) ) <_ ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) + ( R x. 2 ) ) )
503 56 leabsd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) + ( R x. 2 ) ) <_ ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) + ( R x. 2 ) ) ) )
504 503 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) + ( R x. 2 ) ) <_ ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) + ( R x. 2 ) ) ) )
505 80 81 84 502 504 letrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. T ) - ( log ` x ) ) ) <_ ( abs ` ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) + ( R x. 2 ) ) ) )
506 5 55 56 78 505 o1le 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( mmu ` n ) / n ) x. T ) - ( log ` x ) ) ) e. O(1) )