Metamath Proof Explorer


Theorem chtub

Description: An upper bound on the Chebyshev function. (Contributed by Mario Carneiro, 13-Mar-2014) (Revised 22-Sep-2014.)

Ref Expression
Assertion chtub N 2 < N θ N < log 2 2 N 3

Proof

Step Hyp Ref Expression
1 2re 2
2 1lt2 1 < 2
3 rplogcl 2 1 < 2 log 2 +
4 1 2 3 mp2an log 2 +
5 elrp log 2 + log 2 0 < log 2
6 4 5 mpbi log 2 0 < log 2
7 6 simpli log 2
8 7 recni log 2
9 8 mulid1i log 2 1 = log 2
10 cht2 θ 2 = log 2
11 9 10 eqtr4i log 2 1 = θ 2
12 fveq2 N = 2 θ N = θ 2
13 11 12 eqtr4id N = 2 log 2 1 = θ N
14 chtfl N θ N = θ N
15 14 adantr N 2 < N θ N = θ N
16 13 15 sylan9eqr N 2 < N N = 2 log 2 1 = θ N
17 2t2e4 2 2 = 4
18 df-4 4 = 3 + 1
19 17 18 eqtri 2 2 = 3 + 1
20 simplr N 2 < N N = 2 2 < N
21 simpl N 2 < N N
22 2pos 0 < 2
23 1 22 pm3.2i 2 0 < 2
24 23 a1i N 2 < N N = 2 2 0 < 2
25 ltmul2 2 N 2 0 < 2 2 < N 2 2 < 2 N
26 1 21 24 25 mp3an2ani N 2 < N N = 2 2 < N 2 2 < 2 N
27 20 26 mpbid N 2 < N N = 2 2 2 < 2 N
28 19 27 eqbrtrrid N 2 < N N = 2 3 + 1 < 2 N
29 3re 3
30 29 a1i N 2 < N N = 2 3
31 1red N 2 < N N = 2 1
32 remulcl 2 N 2 N
33 1 21 32 sylancr N 2 < N 2 N
34 33 adantr N 2 < N N = 2 2 N
35 30 31 34 ltaddsub2d N 2 < N N = 2 3 + 1 < 2 N 1 < 2 N 3
36 28 35 mpbid N 2 < N N = 2 1 < 2 N 3
37 resubcl 2 N 3 2 N 3
38 33 29 37 sylancl N 2 < N 2 N 3
39 38 adantr N 2 < N N = 2 2 N 3
40 6 a1i N 2 < N N = 2 log 2 0 < log 2
41 ltmul2 1 2 N 3 log 2 0 < log 2 1 < 2 N 3 log 2 1 < log 2 2 N 3
42 31 39 40 41 syl3anc N 2 < N N = 2 1 < 2 N 3 log 2 1 < log 2 2 N 3
43 36 42 mpbid N 2 < N N = 2 log 2 1 < log 2 2 N 3
44 16 43 eqbrtrrd N 2 < N N = 2 θ N < log 2 2 N 3
45 chtcl N θ N
46 45 ad2antrr N 2 < N N 2 + 1 θ N
47 reflcl N N
48 47 ad2antrr N 2 < N N 2 + 1 N
49 remulcl 2 N 2 N
50 1 48 49 sylancr N 2 < N N 2 + 1 2 N
51 resubcl 2 N 3 2 N 3
52 50 29 51 sylancl N 2 < N N 2 + 1 2 N 3
53 remulcl log 2 2 N 3 log 2 2 N 3
54 7 52 53 sylancr N 2 < N N 2 + 1 log 2 2 N 3
55 38 adantr N 2 < N N 2 + 1 2 N 3
56 remulcl log 2 2 N 3 log 2 2 N 3
57 7 55 56 sylancr N 2 < N N 2 + 1 log 2 2 N 3
58 15 adantr N 2 < N N 2 + 1 θ N = θ N
59 simpr N 2 < N N 2 + 1 N 2 + 1
60 df-3 3 = 2 + 1
61 60 fveq2i 3 = 2 + 1
62 59 61 eleqtrrdi N 2 < N N 2 + 1 N 3
63 fveq2 k = N θ k = θ N
64 oveq2 k = N 2 k = 2 N
65 64 oveq1d k = N 2 k 3 = 2 N 3
66 65 oveq2d k = N log 2 2 k 3 = log 2 2 N 3
67 63 66 breq12d k = N θ k < log 2 2 k 3 θ N < log 2 2 N 3
68 oveq2 x = 3 3 x = 3 3
69 68 raleqdv x = 3 k 3 x θ k < log 2 2 k 3 k 3 3 θ k < log 2 2 k 3
70 oveq2 x = n 3 x = 3 n
71 70 raleqdv x = n k 3 x θ k < log 2 2 k 3 k 3 n θ k < log 2 2 k 3
72 oveq2 x = n + 1 3 x = 3 n + 1
73 72 raleqdv x = n + 1 k 3 x θ k < log 2 2 k 3 k 3 n + 1 θ k < log 2 2 k 3
74 oveq2 x = N 3 x = 3 N
75 74 raleqdv x = N k 3 x θ k < log 2 2 k 3 k 3 N θ k < log 2 2 k 3
76 6lt8 6 < 8
77 6re 6
78 6pos 0 < 6
79 77 78 elrpii 6 +
80 8re 8
81 8pos 0 < 8
82 80 81 elrpii 8 +
83 logltb 6 + 8 + 6 < 8 log 6 < log 8
84 79 82 83 mp2an 6 < 8 log 6 < log 8
85 76 84 mpbi log 6 < log 8
86 85 a1i k 3 3 log 6 < log 8
87 elfz1eq k 3 3 k = 3
88 87 fveq2d k 3 3 θ k = θ 3
89 cht3 θ 3 = log 6
90 88 89 eqtrdi k 3 3 θ k = log 6
91 87 oveq2d k 3 3 2 k = 2 3
92 91 oveq1d k 3 3 2 k 3 = 2 3 3
93 3cn 3
94 93 2timesi 2 3 = 3 + 3
95 93 93 94 mvrraddi 2 3 3 = 3
96 92 95 eqtrdi k 3 3 2 k 3 = 3
97 96 oveq2d k 3 3 log 2 2 k 3 = log 2 3
98 2rp 2 +
99 relogcl 2 + log 2
100 98 99 ax-mp log 2
101 100 recni log 2
102 101 93 mulcomi log 2 3 = 3 log 2
103 3z 3
104 relogexp 2 + 3 log 2 3 = 3 log 2
105 98 103 104 mp2an log 2 3 = 3 log 2
106 102 105 eqtr4i log 2 3 = log 2 3
107 cu2 2 3 = 8
108 107 fveq2i log 2 3 = log 8
109 106 108 eqtri log 2 3 = log 8
110 97 109 eqtrdi k 3 3 log 2 2 k 3 = log 8
111 86 90 110 3brtr4d k 3 3 θ k < log 2 2 k 3
112 111 rgen k 3 3 θ k < log 2 2 k 3
113 df-2 2 = 1 + 1
114 2div2e1 2 2 = 1
115 eluzle n 3 3 n
116 60 115 eqbrtrrid n 3 2 + 1 n
117 2z 2
118 eluzelz n 3 n
119 zltp1le 2 n 2 < n 2 + 1 n
120 117 118 119 sylancr n 3 2 < n 2 + 1 n
121 116 120 mpbird n 3 2 < n
122 eluzelre n 3 n
123 ltdiv1 2 n 2 0 < 2 2 < n 2 2 < n 2
124 1 23 123 mp3an13 n 2 < n 2 2 < n 2
125 122 124 syl n 3 2 < n 2 2 < n 2
126 121 125 mpbid n 3 2 2 < n 2
127 114 126 eqbrtrrid n 3 1 < n 2
128 122 rehalfcld n 3 n 2
129 1re 1
130 ltadd1 1 n 2 1 1 < n 2 1 + 1 < n 2 + 1
131 129 129 130 mp3an13 n 2 1 < n 2 1 + 1 < n 2 + 1
132 128 131 syl n 3 1 < n 2 1 + 1 < n 2 + 1
133 127 132 mpbid n 3 1 + 1 < n 2 + 1
134 113 133 eqbrtrid n 3 2 < n 2 + 1
135 134 adantr n 3 n 2 2 < n 2 + 1
136 peano2z n 2 n 2 + 1
137 136 adantl n 3 n 2 n 2 + 1
138 zltp1le 2 n 2 + 1 2 < n 2 + 1 2 + 1 n 2 + 1
139 117 137 138 sylancr n 3 n 2 2 < n 2 + 1 2 + 1 n 2 + 1
140 135 139 mpbid n 3 n 2 2 + 1 n 2 + 1
141 60 140 eqbrtrid n 3 n 2 3 n 2 + 1
142 1red n 3 1
143 ltle 1 n 2 1 < n 2 1 n 2
144 129 128 143 sylancr n 3 1 < n 2 1 n 2
145 127 144 mpd n 3 1 n 2
146 142 128 128 145 leadd2dd n 3 n 2 + 1 n 2 + n 2
147 122 recnd n 3 n
148 147 2halvesd n 3 n 2 + n 2 = n
149 146 148 breqtrd n 3 n 2 + 1 n
150 149 adantr n 3 n 2 n 2 + 1 n
151 elfz n 2 + 1 3 n n 2 + 1 3 n 3 n 2 + 1 n 2 + 1 n
152 103 151 mp3an2 n 2 + 1 n n 2 + 1 3 n 3 n 2 + 1 n 2 + 1 n
153 136 118 152 syl2anr n 3 n 2 n 2 + 1 3 n 3 n 2 + 1 n 2 + 1 n
154 141 150 153 mpbir2and n 3 n 2 n 2 + 1 3 n
155 fveq2 k = n 2 + 1 θ k = θ n 2 + 1
156 oveq2 k = n 2 + 1 2 k = 2 n 2 + 1
157 156 oveq1d k = n 2 + 1 2 k 3 = 2 n 2 + 1 3
158 157 oveq2d k = n 2 + 1 log 2 2 k 3 = log 2 2 n 2 + 1 3
159 155 158 breq12d k = n 2 + 1 θ k < log 2 2 k 3 θ n 2 + 1 < log 2 2 n 2 + 1 3
160 159 rspcv n 2 + 1 3 n k 3 n θ k < log 2 2 k 3 θ n 2 + 1 < log 2 2 n 2 + 1 3
161 154 160 syl n 3 n 2 k 3 n θ k < log 2 2 k 3 θ n 2 + 1 < log 2 2 n 2 + 1 3
162 128 recnd n 3 n 2
163 162 adantr n 3 n 2 n 2
164 2cn 2
165 ax-1cn 1
166 adddi 2 n 2 1 2 n 2 + 1 = 2 n 2 + 2 1
167 164 165 166 mp3an13 n 2 2 n 2 + 1 = 2 n 2 + 2 1
168 163 167 syl n 3 n 2 2 n 2 + 1 = 2 n 2 + 2 1
169 147 adantr n 3 n 2 n
170 2ne0 2 0
171 divcan2 n 2 2 0 2 n 2 = n
172 164 170 171 mp3an23 n 2 n 2 = n
173 169 172 syl n 3 n 2 2 n 2 = n
174 164 mulid1i 2 1 = 2
175 174 a1i n 3 n 2 2 1 = 2
176 173 175 oveq12d n 3 n 2 2 n 2 + 2 1 = n + 2
177 168 176 eqtrd n 3 n 2 2 n 2 + 1 = n + 2
178 177 oveq1d n 3 n 2 2 n 2 + 1 3 = n + 2 - 3
179 subsub3 n 3 2 n 3 2 = n + 2 - 3
180 93 164 179 mp3an23 n n 3 2 = n + 2 - 3
181 169 180 syl n 3 n 2 n 3 2 = n + 2 - 3
182 2p1e3 2 + 1 = 3
183 93 164 165 182 subaddrii 3 2 = 1
184 183 oveq2i n 3 2 = n 1
185 181 184 eqtr3di n 3 n 2 n + 2 - 3 = n 1
186 178 185 eqtrd n 3 n 2 2 n 2 + 1 3 = n 1
187 186 oveq2d n 3 n 2 log 2 2 n 2 + 1 3 = log 2 n 1
188 187 breq2d n 3 n 2 θ n 2 + 1 < log 2 2 n 2 + 1 3 θ n 2 + 1 < log 2 n 1
189 137 zred n 3 n 2 n 2 + 1
190 chtcl n 2 + 1 θ n 2 + 1
191 189 190 syl n 3 n 2 θ n 2 + 1
192 122 adantr n 3 n 2 n
193 peano2rem n n 1
194 192 193 syl n 3 n 2 n 1
195 remulcl log 2 n 1 log 2 n 1
196 100 194 195 sylancr n 3 n 2 log 2 n 1
197 remulcl log 2 n log 2 n
198 100 192 197 sylancr n 3 n 2 log 2 n
199 191 196 198 ltadd1d n 3 n 2 θ n 2 + 1 < log 2 n 1 θ n 2 + 1 + log 2 n < log 2 n 1 + log 2 n
200 101 a1i n 3 n 2 log 2
201 194 recnd n 3 n 2 n 1
202 200 201 169 adddid n 3 n 2 log 2 n - 1 + n = log 2 n 1 + log 2 n
203 adddi 2 n 1 2 n + 1 = 2 n + 2 1
204 164 165 203 mp3an13 n 2 n + 1 = 2 n + 2 1
205 169 204 syl n 3 n 2 2 n + 1 = 2 n + 2 1
206 174 oveq2i 2 n + 2 1 = 2 n + 2
207 205 206 eqtrdi n 3 n 2 2 n + 1 = 2 n + 2
208 207 oveq1d n 3 n 2 2 n + 1 3 = 2 n + 2 - 3
209 zmulcl 2 n 2 n
210 117 118 209 sylancr n 3 2 n
211 210 zcnd n 3 2 n
212 211 adantr n 3 n 2 2 n
213 subsub3 2 n 3 2 2 n 3 2 = 2 n + 2 - 3
214 93 164 213 mp3an23 2 n 2 n 3 2 = 2 n + 2 - 3
215 212 214 syl n 3 n 2 2 n 3 2 = 2 n + 2 - 3
216 183 oveq2i 2 n 3 2 = 2 n 1
217 169 2timesd n 3 n 2 2 n = n + n
218 217 oveq1d n 3 n 2 2 n 1 = n + n - 1
219 165 a1i n 3 n 2 1
220 169 169 219 addsubd n 3 n 2 n + n - 1 = n - 1 + n
221 218 220 eqtrd n 3 n 2 2 n 1 = n - 1 + n
222 216 221 syl5eq n 3 n 2 2 n 3 2 = n - 1 + n
223 208 215 222 3eqtr2rd n 3 n 2 n - 1 + n = 2 n + 1 3
224 223 oveq2d n 3 n 2 log 2 n - 1 + n = log 2 2 n + 1 3
225 202 224 eqtr3d n 3 n 2 log 2 n 1 + log 2 n = log 2 2 n + 1 3
226 225 breq2d n 3 n 2 θ n 2 + 1 + log 2 n < log 2 n 1 + log 2 n θ n 2 + 1 + log 2 n < log 2 2 n + 1 3
227 188 199 226 3bitrd n 3 n 2 θ n 2 + 1 < log 2 2 n 2 + 1 3 θ n 2 + 1 + log 2 n < log 2 2 n + 1 3
228 3nn 3
229 elfzuz n 2 + 1 3 n n 2 + 1 3
230 154 229 syl n 3 n 2 n 2 + 1 3
231 eluznn 3 n 2 + 1 3 n 2 + 1
232 228 230 231 sylancr n 3 n 2 n 2 + 1
233 chtublem n 2 + 1 θ 2 n 2 + 1 1 θ n 2 + 1 + log 4 n 2 + 1 - 1
234 232 233 syl n 3 n 2 θ 2 n 2 + 1 1 θ n 2 + 1 + log 4 n 2 + 1 - 1
235 177 oveq1d n 3 n 2 2 n 2 + 1 1 = n + 2 - 1
236 addsubass n 2 1 n + 2 - 1 = n + 2 - 1
237 164 165 236 mp3an23 n n + 2 - 1 = n + 2 - 1
238 169 237 syl n 3 n 2 n + 2 - 1 = n + 2 - 1
239 2m1e1 2 1 = 1
240 239 oveq2i n + 2 - 1 = n + 1
241 238 240 eqtrdi n 3 n 2 n + 2 - 1 = n + 1
242 235 241 eqtrd n 3 n 2 2 n 2 + 1 1 = n + 1
243 242 fveq2d n 3 n 2 θ 2 n 2 + 1 1 = θ n + 1
244 pncan n 2 1 n 2 + 1 - 1 = n 2
245 163 165 244 sylancl n 3 n 2 n 2 + 1 - 1 = n 2
246 245 oveq2d n 3 n 2 log 4 n 2 + 1 - 1 = log 4 n 2
247 relogexp 2 + 2 log 2 2 = 2 log 2
248 98 117 247 mp2an log 2 2 = 2 log 2
249 sq2 2 2 = 4
250 249 fveq2i log 2 2 = log 4
251 164 101 mulcomi 2 log 2 = log 2 2
252 248 250 251 3eqtr3i log 4 = log 2 2
253 252 oveq1i log 4 n 2 = log 2 2 n 2
254 164 a1i n 3 n 2 2
255 200 254 163 mulassd n 3 n 2 log 2 2 n 2 = log 2 2 n 2
256 253 255 syl5eq n 3 n 2 log 4 n 2 = log 2 2 n 2
257 173 oveq2d n 3 n 2 log 2 2 n 2 = log 2 n
258 246 256 257 3eqtrd n 3 n 2 log 4 n 2 + 1 - 1 = log 2 n
259 258 oveq2d n 3 n 2 θ n 2 + 1 + log 4 n 2 + 1 - 1 = θ n 2 + 1 + log 2 n
260 234 243 259 3brtr3d n 3 n 2 θ n + 1 θ n 2 + 1 + log 2 n
261 peano2uz n 3 n + 1 3
262 eluzelz n + 1 3 n + 1
263 261 262 syl n 3 n + 1
264 263 zred n 3 n + 1
265 264 adantr n 3 n 2 n + 1
266 chtcl n + 1 θ n + 1
267 265 266 syl n 3 n 2 θ n + 1
268 191 198 readdcld n 3 n 2 θ n 2 + 1 + log 2 n
269 zmulcl 2 n + 1 2 n + 1
270 117 263 269 sylancr n 3 2 n + 1
271 270 zred n 3 2 n + 1
272 resubcl 2 n + 1 3 2 n + 1 3
273 271 29 272 sylancl n 3 2 n + 1 3
274 273 adantr n 3 n 2 2 n + 1 3
275 remulcl log 2 2 n + 1 3 log 2 2 n + 1 3
276 100 274 275 sylancr n 3 n 2 log 2 2 n + 1 3
277 lelttr θ n + 1 θ n 2 + 1 + log 2 n log 2 2 n + 1 3 θ n + 1 θ n 2 + 1 + log 2 n θ n 2 + 1 + log 2 n < log 2 2 n + 1 3 θ n + 1 < log 2 2 n + 1 3
278 267 268 276 277 syl3anc n 3 n 2 θ n + 1 θ n 2 + 1 + log 2 n θ n 2 + 1 + log 2 n < log 2 2 n + 1 3 θ n + 1 < log 2 2 n + 1 3
279 260 278 mpand n 3 n 2 θ n 2 + 1 + log 2 n < log 2 2 n + 1 3 θ n + 1 < log 2 2 n + 1 3
280 227 279 sylbid n 3 n 2 θ n 2 + 1 < log 2 2 n 2 + 1 3 θ n + 1 < log 2 2 n + 1 3
281 161 280 syld n 3 n 2 k 3 n θ k < log 2 2 k 3 θ n + 1 < log 2 2 n + 1 3
282 eluzfz2 n 3 n 3 n
283 fveq2 k = n θ k = θ n
284 oveq2 k = n 2 k = 2 n
285 284 oveq1d k = n 2 k 3 = 2 n 3
286 285 oveq2d k = n log 2 2 k 3 = log 2 2 n 3
287 283 286 breq12d k = n θ k < log 2 2 k 3 θ n < log 2 2 n 3
288 287 rspcv n 3 n k 3 n θ k < log 2 2 k 3 θ n < log 2 2 n 3
289 282 288 syl n 3 k 3 n θ k < log 2 2 k 3 θ n < log 2 2 n 3
290 289 adantr n 3 n + 1 2 k 3 n θ k < log 2 2 k 3 θ n < log 2 2 n 3
291 210 zred n 3 2 n
292 29 a1i n 3 3
293 122 ltp1d n 3 n < n + 1
294 23 a1i n 3 2 0 < 2
295 ltmul2 n n + 1 2 0 < 2 n < n + 1 2 n < 2 n + 1
296 122 264 294 295 syl3anc n 3 n < n + 1 2 n < 2 n + 1
297 293 296 mpbid n 3 2 n < 2 n + 1
298 291 271 292 297 ltsub1dd n 3 2 n 3 < 2 n + 1 3
299 resubcl 2 n 3 2 n 3
300 291 29 299 sylancl n 3 2 n 3
301 6 a1i n 3 log 2 0 < log 2
302 ltmul2 2 n 3 2 n + 1 3 log 2 0 < log 2 2 n 3 < 2 n + 1 3 log 2 2 n 3 < log 2 2 n + 1 3
303 300 273 301 302 syl3anc n 3 2 n 3 < 2 n + 1 3 log 2 2 n 3 < log 2 2 n + 1 3
304 298 303 mpbid n 3 log 2 2 n 3 < log 2 2 n + 1 3
305 chtcl n θ n
306 122 305 syl n 3 θ n
307 remulcl log 2 2 n 3 log 2 2 n 3
308 100 300 307 sylancr n 3 log 2 2 n 3
309 100 273 275 sylancr n 3 log 2 2 n + 1 3
310 lttr θ n log 2 2 n 3 log 2 2 n + 1 3 θ n < log 2 2 n 3 log 2 2 n 3 < log 2 2 n + 1 3 θ n < log 2 2 n + 1 3
311 306 308 309 310 syl3anc n 3 θ n < log 2 2 n 3 log 2 2 n 3 < log 2 2 n + 1 3 θ n < log 2 2 n + 1 3
312 304 311 mpan2d n 3 θ n < log 2 2 n 3 θ n < log 2 2 n + 1 3
313 312 adantr n 3 n + 1 2 θ n < log 2 2 n 3 θ n < log 2 2 n + 1 3
314 evend2 n + 1 2 n + 1 n + 1 2
315 263 314 syl n 3 2 n + 1 n + 1 2
316 2lt3 2 < 3
317 1 29 ltnlei 2 < 3 ¬ 3 2
318 316 317 mpbi ¬ 3 2
319 breq2 2 = n + 1 3 2 3 n + 1
320 318 319 mtbii 2 = n + 1 ¬ 3 n + 1
321 eluzle n + 1 3 3 n + 1
322 261 321 syl n 3 3 n + 1
323 320 322 nsyl3 n 3 ¬ 2 = n + 1
324 323 adantr n 3 n + 1 ¬ 2 = n + 1
325 uzid 2 2 2
326 117 325 ax-mp 2 2
327 simpr n 3 n + 1 n + 1
328 dvdsprm 2 2 n + 1 2 n + 1 2 = n + 1
329 326 327 328 sylancr n 3 n + 1 2 n + 1 2 = n + 1
330 324 329 mtbird n 3 n + 1 ¬ 2 n + 1
331 330 ex n 3 n + 1 ¬ 2 n + 1
332 331 con2d n 3 2 n + 1 ¬ n + 1
333 315 332 sylbird n 3 n + 1 2 ¬ n + 1
334 333 imp n 3 n + 1 2 ¬ n + 1
335 chtnprm n ¬ n + 1 θ n + 1 = θ n
336 118 334 335 syl2an2r n 3 n + 1 2 θ n + 1 = θ n
337 336 breq1d n 3 n + 1 2 θ n + 1 < log 2 2 n + 1 3 θ n < log 2 2 n + 1 3
338 313 337 sylibrd n 3 n + 1 2 θ n < log 2 2 n 3 θ n + 1 < log 2 2 n + 1 3
339 290 338 syld n 3 n + 1 2 k 3 n θ k < log 2 2 k 3 θ n + 1 < log 2 2 n + 1 3
340 zeo n n 2 n + 1 2
341 118 340 syl n 3 n 2 n + 1 2
342 281 339 341 mpjaodan n 3 k 3 n θ k < log 2 2 k 3 θ n + 1 < log 2 2 n + 1 3
343 ovex n + 1 V
344 fveq2 k = n + 1 θ k = θ n + 1
345 oveq2 k = n + 1 2 k = 2 n + 1
346 345 oveq1d k = n + 1 2 k 3 = 2 n + 1 3
347 346 oveq2d k = n + 1 log 2 2 k 3 = log 2 2 n + 1 3
348 344 347 breq12d k = n + 1 θ k < log 2 2 k 3 θ n + 1 < log 2 2 n + 1 3
349 343 348 ralsn k n + 1 θ k < log 2 2 k 3 θ n + 1 < log 2 2 n + 1 3
350 342 349 syl6ibr n 3 k 3 n θ k < log 2 2 k 3 k n + 1 θ k < log 2 2 k 3
351 350 ancld n 3 k 3 n θ k < log 2 2 k 3 k 3 n θ k < log 2 2 k 3 k n + 1 θ k < log 2 2 k 3
352 ralun k 3 n θ k < log 2 2 k 3 k n + 1 θ k < log 2 2 k 3 k 3 n n + 1 θ k < log 2 2 k 3
353 fzsuc n 3 3 n + 1 = 3 n n + 1
354 353 raleqdv n 3 k 3 n + 1 θ k < log 2 2 k 3 k 3 n n + 1 θ k < log 2 2 k 3
355 352 354 syl5ibr n 3 k 3 n θ k < log 2 2 k 3 k n + 1 θ k < log 2 2 k 3 k 3 n + 1 θ k < log 2 2 k 3
356 351 355 syld n 3 k 3 n θ k < log 2 2 k 3 k 3 n + 1 θ k < log 2 2 k 3
357 69 71 73 75 112 356 uzind4i N 3 k 3 N θ k < log 2 2 k 3
358 eluzfz2 N 3 N 3 N
359 67 357 358 rspcdva N 3 θ N < log 2 2 N 3
360 62 359 syl N 2 < N N 2 + 1 θ N < log 2 2 N 3
361 58 360 eqbrtrrd N 2 < N N 2 + 1 θ N < log 2 2 N 3
362 33 adantr N 2 < N N 2 + 1 2 N
363 29 a1i N 2 < N N 2 + 1 3
364 flle N N N
365 364 ad2antrr N 2 < N N 2 + 1 N N
366 21 adantr N 2 < N N 2 + 1 N
367 23 a1i N 2 < N N 2 + 1 2 0 < 2
368 lemul2 N N 2 0 < 2 N N 2 N 2 N
369 48 366 367 368 syl3anc N 2 < N N 2 + 1 N N 2 N 2 N
370 365 369 mpbid N 2 < N N 2 + 1 2 N 2 N
371 50 362 363 370 lesub1dd N 2 < N N 2 + 1 2 N 3 2 N 3
372 6 a1i N 2 < N N 2 + 1 log 2 0 < log 2
373 lemul2 2 N 3 2 N 3 log 2 0 < log 2 2 N 3 2 N 3 log 2 2 N 3 log 2 2 N 3
374 52 55 372 373 syl3anc N 2 < N N 2 + 1 2 N 3 2 N 3 log 2 2 N 3 log 2 2 N 3
375 371 374 mpbid N 2 < N N 2 + 1 log 2 2 N 3 log 2 2 N 3
376 46 54 57 361 375 ltletrd N 2 < N N 2 + 1 θ N < log 2 2 N 3
377 117 a1i N 2 < N 2
378 flcl N N
379 378 adantr N 2 < N N
380 ltle 2 N 2 < N 2 N
381 1 380 mpan N 2 < N 2 N
382 flge N 2 2 N 2 N
383 117 382 mpan2 N 2 N 2 N
384 381 383 sylibd N 2 < N 2 N
385 384 imp N 2 < N 2 N
386 eluz2 N 2 2 N 2 N
387 377 379 385 386 syl3anbrc N 2 < N N 2
388 uzp1 N 2 N = 2 N 2 + 1
389 387 388 syl N 2 < N N = 2 N 2 + 1
390 44 376 389 mpjaodan N 2 < N θ N < log 2 2 N 3