Metamath Proof Explorer


Theorem pntlemk

Description: Lemma for pnt . Evaluate the naive part of the estimate. (Contributed by Mario Carneiro, 14-Apr-2016)

Ref Expression
Hypotheses pntlem1.r
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
pntlem1.a
|- ( ph -> A e. RR+ )
pntlem1.b
|- ( ph -> B e. RR+ )
pntlem1.l
|- ( ph -> L e. ( 0 (,) 1 ) )
pntlem1.d
|- D = ( A + 1 )
pntlem1.f
|- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
pntlem1.u
|- ( ph -> U e. RR+ )
pntlem1.u2
|- ( ph -> U <_ A )
pntlem1.e
|- E = ( U / D )
pntlem1.k
|- K = ( exp ` ( B / E ) )
pntlem1.y
|- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )
pntlem1.x
|- ( ph -> ( X e. RR+ /\ Y < X ) )
pntlem1.c
|- ( ph -> C e. RR+ )
pntlem1.w
|- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
pntlem1.z
|- ( ph -> Z e. ( W [,) +oo ) )
pntlem1.m
|- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )
pntlem1.n
|- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )
pntlem1.U
|- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )
pntlem1.K
|- ( ph -> A. y e. ( X (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( K x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
Assertion pntlemk
|- ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) <_ ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) )

Proof

Step Hyp Ref Expression
1 pntlem1.r
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 pntlem1.a
 |-  ( ph -> A e. RR+ )
3 pntlem1.b
 |-  ( ph -> B e. RR+ )
4 pntlem1.l
 |-  ( ph -> L e. ( 0 (,) 1 ) )
5 pntlem1.d
 |-  D = ( A + 1 )
6 pntlem1.f
 |-  F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
7 pntlem1.u
 |-  ( ph -> U e. RR+ )
8 pntlem1.u2
 |-  ( ph -> U <_ A )
9 pntlem1.e
 |-  E = ( U / D )
10 pntlem1.k
 |-  K = ( exp ` ( B / E ) )
11 pntlem1.y
 |-  ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )
12 pntlem1.x
 |-  ( ph -> ( X e. RR+ /\ Y < X ) )
13 pntlem1.c
 |-  ( ph -> C e. RR+ )
14 pntlem1.w
 |-  W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
15 pntlem1.z
 |-  ( ph -> Z e. ( W [,) +oo ) )
16 pntlem1.m
 |-  M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )
17 pntlem1.n
 |-  N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )
18 pntlem1.U
 |-  ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )
19 pntlem1.K
 |-  ( ph -> A. y e. ( X (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( K x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
20 2re
 |-  2 e. RR
21 fzfid
 |-  ( ph -> ( 1 ... ( |_ ` ( Z / Y ) ) ) e. Fin )
22 elfznn
 |-  ( n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) -> n e. NN )
23 22 adantl
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> n e. NN )
24 23 nnrpd
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> n e. RR+ )
25 24 relogcld
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( log ` n ) e. RR )
26 25 23 nndivred
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( log ` n ) / n ) e. RR )
27 21 26 fsumrecl
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) e. RR )
28 remulcl
 |-  ( ( 2 e. RR /\ sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) e. RR ) -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) e. RR )
29 20 27 28 sylancr
 |-  ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) e. RR )
30 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 pntlemb
 |-  ( ph -> ( Z e. RR+ /\ ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) /\ ( ( 4 / ( L x. E ) ) <_ ( sqrt ` Z ) /\ ( ( ( log ` X ) / ( log ` K ) ) + 2 ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) /\ ( ( U x. 3 ) + C ) <_ ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) )
31 30 simp1d
 |-  ( ph -> Z e. RR+ )
32 31 relogcld
 |-  ( ph -> ( log ` Z ) e. RR )
33 peano2re
 |-  ( ( log ` Z ) e. RR -> ( ( log ` Z ) + 1 ) e. RR )
34 32 33 syl
 |-  ( ph -> ( ( log ` Z ) + 1 ) e. RR )
35 34 resqcld
 |-  ( ph -> ( ( ( log ` Z ) + 1 ) ^ 2 ) e. RR )
36 3re
 |-  3 e. RR
37 readdcl
 |-  ( ( ( log ` Z ) e. RR /\ 3 e. RR ) -> ( ( log ` Z ) + 3 ) e. RR )
38 32 36 37 sylancl
 |-  ( ph -> ( ( log ` Z ) + 3 ) e. RR )
39 38 32 remulcld
 |-  ( ph -> ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) e. RR )
40 31 rpred
 |-  ( ph -> Z e. RR )
41 11 simpld
 |-  ( ph -> Y e. RR+ )
42 40 41 rerpdivcld
 |-  ( ph -> ( Z / Y ) e. RR )
43 1red
 |-  ( ph -> 1 e. RR )
44 31 rpsqrtcld
 |-  ( ph -> ( sqrt ` Z ) e. RR+ )
45 44 rpred
 |-  ( ph -> ( sqrt ` Z ) e. RR )
46 ere
 |-  _e e. RR
47 46 a1i
 |-  ( ph -> _e e. RR )
48 1re
 |-  1 e. RR
49 1lt2
 |-  1 < 2
50 egt2lt3
 |-  ( 2 < _e /\ _e < 3 )
51 50 simpli
 |-  2 < _e
52 48 20 46 lttri
 |-  ( ( 1 < 2 /\ 2 < _e ) -> 1 < _e )
53 49 51 52 mp2an
 |-  1 < _e
54 48 46 53 ltleii
 |-  1 <_ _e
55 54 a1i
 |-  ( ph -> 1 <_ _e )
56 30 simp2d
 |-  ( ph -> ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) )
57 56 simp2d
 |-  ( ph -> _e <_ ( sqrt ` Z ) )
58 43 47 45 55 57 letrd
 |-  ( ph -> 1 <_ ( sqrt ` Z ) )
59 56 simp3d
 |-  ( ph -> ( sqrt ` Z ) <_ ( Z / Y ) )
60 43 45 42 58 59 letrd
 |-  ( ph -> 1 <_ ( Z / Y ) )
61 flge1nn
 |-  ( ( ( Z / Y ) e. RR /\ 1 <_ ( Z / Y ) ) -> ( |_ ` ( Z / Y ) ) e. NN )
62 42 60 61 syl2anc
 |-  ( ph -> ( |_ ` ( Z / Y ) ) e. NN )
63 62 nnrpd
 |-  ( ph -> ( |_ ` ( Z / Y ) ) e. RR+ )
64 63 relogcld
 |-  ( ph -> ( log ` ( |_ ` ( Z / Y ) ) ) e. RR )
65 64 43 readdcld
 |-  ( ph -> ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) e. RR )
66 65 resqcld
 |-  ( ph -> ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) e. RR )
67 logdivbnd
 |-  ( ( |_ ` ( Z / Y ) ) e. NN -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) <_ ( ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) / 2 ) )
68 62 67 syl
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) <_ ( ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) / 2 ) )
69 20 a1i
 |-  ( ph -> 2 e. RR )
70 2pos
 |-  0 < 2
71 70 a1i
 |-  ( ph -> 0 < 2 )
72 lemuldiv2
 |-  ( ( sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) e. RR /\ ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) <-> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) <_ ( ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) / 2 ) ) )
73 27 66 69 71 72 syl112anc
 |-  ( ph -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) <-> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) <_ ( ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) / 2 ) ) )
74 68 73 mpbird
 |-  ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) )
75 reflcl
 |-  ( ( Z / Y ) e. RR -> ( |_ ` ( Z / Y ) ) e. RR )
76 42 75 syl
 |-  ( ph -> ( |_ ` ( Z / Y ) ) e. RR )
77 flle
 |-  ( ( Z / Y ) e. RR -> ( |_ ` ( Z / Y ) ) <_ ( Z / Y ) )
78 42 77 syl
 |-  ( ph -> ( |_ ` ( Z / Y ) ) <_ ( Z / Y ) )
79 11 simprd
 |-  ( ph -> 1 <_ Y )
80 1rp
 |-  1 e. RR+
81 80 a1i
 |-  ( ph -> 1 e. RR+ )
82 81 41 31 lediv2d
 |-  ( ph -> ( 1 <_ Y <-> ( Z / Y ) <_ ( Z / 1 ) ) )
83 79 82 mpbid
 |-  ( ph -> ( Z / Y ) <_ ( Z / 1 ) )
84 40 recnd
 |-  ( ph -> Z e. CC )
85 84 div1d
 |-  ( ph -> ( Z / 1 ) = Z )
86 83 85 breqtrd
 |-  ( ph -> ( Z / Y ) <_ Z )
87 76 42 40 78 86 letrd
 |-  ( ph -> ( |_ ` ( Z / Y ) ) <_ Z )
88 63 31 logled
 |-  ( ph -> ( ( |_ ` ( Z / Y ) ) <_ Z <-> ( log ` ( |_ ` ( Z / Y ) ) ) <_ ( log ` Z ) ) )
89 87 88 mpbid
 |-  ( ph -> ( log ` ( |_ ` ( Z / Y ) ) ) <_ ( log ` Z ) )
90 64 32 43 89 leadd1dd
 |-  ( ph -> ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) <_ ( ( log ` Z ) + 1 ) )
91 0red
 |-  ( ph -> 0 e. RR )
92 log1
 |-  ( log ` 1 ) = 0
93 62 nnge1d
 |-  ( ph -> 1 <_ ( |_ ` ( Z / Y ) ) )
94 logleb
 |-  ( ( 1 e. RR+ /\ ( |_ ` ( Z / Y ) ) e. RR+ ) -> ( 1 <_ ( |_ ` ( Z / Y ) ) <-> ( log ` 1 ) <_ ( log ` ( |_ ` ( Z / Y ) ) ) ) )
95 80 63 94 sylancr
 |-  ( ph -> ( 1 <_ ( |_ ` ( Z / Y ) ) <-> ( log ` 1 ) <_ ( log ` ( |_ ` ( Z / Y ) ) ) ) )
96 93 95 mpbid
 |-  ( ph -> ( log ` 1 ) <_ ( log ` ( |_ ` ( Z / Y ) ) ) )
97 92 96 eqbrtrrid
 |-  ( ph -> 0 <_ ( log ` ( |_ ` ( Z / Y ) ) ) )
98 64 lep1d
 |-  ( ph -> ( log ` ( |_ ` ( Z / Y ) ) ) <_ ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) )
99 91 64 65 97 98 letrd
 |-  ( ph -> 0 <_ ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) )
100 91 65 34 99 90 letrd
 |-  ( ph -> 0 <_ ( ( log ` Z ) + 1 ) )
101 65 34 99 100 le2sqd
 |-  ( ph -> ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) <_ ( ( log ` Z ) + 1 ) <-> ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) <_ ( ( ( log ` Z ) + 1 ) ^ 2 ) ) )
102 90 101 mpbid
 |-  ( ph -> ( ( ( log ` ( |_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) <_ ( ( ( log ` Z ) + 1 ) ^ 2 ) )
103 29 66 35 74 102 letrd
 |-  ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` Z ) + 1 ) ^ 2 ) )
104 32 resqcld
 |-  ( ph -> ( ( log ` Z ) ^ 2 ) e. RR )
105 69 32 remulcld
 |-  ( ph -> ( 2 x. ( log ` Z ) ) e. RR )
106 104 105 readdcld
 |-  ( ph -> ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) e. RR )
107 loge
 |-  ( log ` _e ) = 1
108 44 rpge0d
 |-  ( ph -> 0 <_ ( sqrt ` Z ) )
109 45 45 108 58 lemulge12d
 |-  ( ph -> ( sqrt ` Z ) <_ ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) )
110 31 rprege0d
 |-  ( ph -> ( Z e. RR /\ 0 <_ Z ) )
111 remsqsqrt
 |-  ( ( Z e. RR /\ 0 <_ Z ) -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z )
112 110 111 syl
 |-  ( ph -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z )
113 109 112 breqtrd
 |-  ( ph -> ( sqrt ` Z ) <_ Z )
114 47 45 40 57 113 letrd
 |-  ( ph -> _e <_ Z )
115 epr
 |-  _e e. RR+
116 logleb
 |-  ( ( _e e. RR+ /\ Z e. RR+ ) -> ( _e <_ Z <-> ( log ` _e ) <_ ( log ` Z ) ) )
117 115 31 116 sylancr
 |-  ( ph -> ( _e <_ Z <-> ( log ` _e ) <_ ( log ` Z ) ) )
118 114 117 mpbid
 |-  ( ph -> ( log ` _e ) <_ ( log ` Z ) )
119 107 118 eqbrtrrid
 |-  ( ph -> 1 <_ ( log ` Z ) )
120 43 32 106 119 leadd2dd
 |-  ( ph -> ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + 1 ) <_ ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + ( log ` Z ) ) )
121 32 recnd
 |-  ( ph -> ( log ` Z ) e. CC )
122 binom21
 |-  ( ( log ` Z ) e. CC -> ( ( ( log ` Z ) + 1 ) ^ 2 ) = ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + 1 ) )
123 121 122 syl
 |-  ( ph -> ( ( ( log ` Z ) + 1 ) ^ 2 ) = ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + 1 ) )
124 121 sqvald
 |-  ( ph -> ( ( log ` Z ) ^ 2 ) = ( ( log ` Z ) x. ( log ` Z ) ) )
125 df-3
 |-  3 = ( 2 + 1 )
126 125 oveq1i
 |-  ( 3 x. ( log ` Z ) ) = ( ( 2 + 1 ) x. ( log ` Z ) )
127 2cnd
 |-  ( ph -> 2 e. CC )
128 1cnd
 |-  ( ph -> 1 e. CC )
129 127 128 121 adddird
 |-  ( ph -> ( ( 2 + 1 ) x. ( log ` Z ) ) = ( ( 2 x. ( log ` Z ) ) + ( 1 x. ( log ` Z ) ) ) )
130 126 129 syl5eq
 |-  ( ph -> ( 3 x. ( log ` Z ) ) = ( ( 2 x. ( log ` Z ) ) + ( 1 x. ( log ` Z ) ) ) )
131 121 mulid2d
 |-  ( ph -> ( 1 x. ( log ` Z ) ) = ( log ` Z ) )
132 131 oveq2d
 |-  ( ph -> ( ( 2 x. ( log ` Z ) ) + ( 1 x. ( log ` Z ) ) ) = ( ( 2 x. ( log ` Z ) ) + ( log ` Z ) ) )
133 130 132 eqtr2d
 |-  ( ph -> ( ( 2 x. ( log ` Z ) ) + ( log ` Z ) ) = ( 3 x. ( log ` Z ) ) )
134 124 133 oveq12d
 |-  ( ph -> ( ( ( log ` Z ) ^ 2 ) + ( ( 2 x. ( log ` Z ) ) + ( log ` Z ) ) ) = ( ( ( log ` Z ) x. ( log ` Z ) ) + ( 3 x. ( log ` Z ) ) ) )
135 121 sqcld
 |-  ( ph -> ( ( log ` Z ) ^ 2 ) e. CC )
136 2cn
 |-  2 e. CC
137 mulcl
 |-  ( ( 2 e. CC /\ ( log ` Z ) e. CC ) -> ( 2 x. ( log ` Z ) ) e. CC )
138 136 121 137 sylancr
 |-  ( ph -> ( 2 x. ( log ` Z ) ) e. CC )
139 135 138 121 addassd
 |-  ( ph -> ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + ( log ` Z ) ) = ( ( ( log ` Z ) ^ 2 ) + ( ( 2 x. ( log ` Z ) ) + ( log ` Z ) ) ) )
140 3cn
 |-  3 e. CC
141 140 a1i
 |-  ( ph -> 3 e. CC )
142 121 141 121 adddird
 |-  ( ph -> ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) = ( ( ( log ` Z ) x. ( log ` Z ) ) + ( 3 x. ( log ` Z ) ) ) )
143 134 139 142 3eqtr4rd
 |-  ( ph -> ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) = ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + ( log ` Z ) ) )
144 120 123 143 3brtr4d
 |-  ( ph -> ( ( ( log ` Z ) + 1 ) ^ 2 ) <_ ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) )
145 29 35 39 103 144 letrd
 |-  ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) )
146 29 39 7 lemul2d
 |-  ( ph -> ( ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) <-> ( U x. ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) <_ ( U x. ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) ) ) )
147 145 146 mpbid
 |-  ( ph -> ( U x. ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) <_ ( U x. ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) ) )
148 7 rpred
 |-  ( ph -> U e. RR )
149 148 adantr
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> U e. RR )
150 149 recnd
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> U e. CC )
151 25 recnd
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( log ` n ) e. CC )
152 24 rpcnne0d
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( n e. CC /\ n =/= 0 ) )
153 div23
 |-  ( ( U e. CC /\ ( log ` n ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( U x. ( log ` n ) ) / n ) = ( ( U / n ) x. ( log ` n ) ) )
154 divass
 |-  ( ( U e. CC /\ ( log ` n ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( U x. ( log ` n ) ) / n ) = ( U x. ( ( log ` n ) / n ) ) )
155 153 154 eqtr3d
 |-  ( ( U e. CC /\ ( log ` n ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( U / n ) x. ( log ` n ) ) = ( U x. ( ( log ` n ) / n ) ) )
156 150 151 152 155 syl3anc
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( U / n ) x. ( log ` n ) ) = ( U x. ( ( log ` n ) / n ) ) )
157 156 sumeq2dv
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) = sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( U x. ( ( log ` n ) / n ) ) )
158 148 recnd
 |-  ( ph -> U e. CC )
159 26 recnd
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ) -> ( ( log ` n ) / n ) e. CC )
160 21 158 159 fsummulc2
 |-  ( ph -> ( U x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) = sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( U x. ( ( log ` n ) / n ) ) )
161 157 160 eqtr4d
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) = ( U x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) )
162 161 oveq2d
 |-  ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) = ( 2 x. ( U x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) )
163 27 recnd
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) e. CC )
164 127 158 163 mul12d
 |-  ( ph -> ( 2 x. ( U x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) = ( U x. ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) )
165 162 164 eqtrd
 |-  ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) = ( U x. ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) )
166 38 recnd
 |-  ( ph -> ( ( log ` Z ) + 3 ) e. CC )
167 158 166 121 mulassd
 |-  ( ph -> ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) = ( U x. ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) ) )
168 147 165 167 3brtr4d
 |-  ( ph -> ( 2 x. sum_ n e. ( 1 ... ( |_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) <_ ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) )