Metamath Proof Explorer


Theorem chebbnd1lem3

Description: Lemma for chebbnd1 : get a lower bound on ppi ( N ) / ( N / log ( N ) ) that is independent of N . (Contributed by Mario Carneiro, 21-Sep-2014)

Ref Expression
Hypothesis chebbnd1lem2.1 M = N 2
Assertion chebbnd1lem3 N 8 N log 2 1 2 e 2 < π _ N log N N

Proof

Step Hyp Ref Expression
1 chebbnd1lem2.1 M = N 2
2 2rp 2 +
3 relogcl 2 + log 2
4 2 3 ax-mp log 2
5 1re 1
6 2re 2
7 ere e
8 6 7 remulcli 2 e
9 2pos 0 < 2
10 epos 0 < e
11 6 7 9 10 mulgt0ii 0 < 2 e
12 8 11 gt0ne0ii 2 e 0
13 5 8 12 redivcli 1 2 e
14 4 13 resubcli log 2 1 2 e
15 2ne0 2 0
16 14 6 15 redivcli log 2 1 2 e 2
17 16 a1i N 8 N log 2 1 2 e 2
18 6 a1i N 8 N 2
19 8re 8
20 19 a1i N 8 N 8
21 simpl N 8 N N
22 2lt8 2 < 8
23 6 19 22 ltleii 2 8
24 23 a1i N 8 N 2 8
25 simpr N 8 N 8 N
26 18 20 21 24 25 letrd N 8 N 2 N
27 ppinncl N 2 N π _ N
28 26 27 syldan N 8 N π _ N
29 28 nnred N 8 N π _ N
30 rehalfcl N N 2
31 30 adantr N 8 N N 2
32 31 flcld N 8 N N 2
33 1 32 eqeltrid N 8 N M
34 33 zred N 8 N M
35 remulcl 2 M 2 M
36 6 34 35 sylancr N 8 N 2 M
37 5 a1i N 8 N 1
38 1lt2 1 < 2
39 38 a1i N 8 N 1 < 2
40 2t1e2 2 1 = 2
41 4nn 4
42 4z 4
43 42 a1i N 8 N 4
44 4t2e8 4 2 = 8
45 44 25 eqbrtrid N 8 N 4 2 N
46 4re 4
47 46 a1i N 8 N 4
48 9 a1i N 8 N 0 < 2
49 lemuldiv 4 N 2 0 < 2 4 2 N 4 N 2
50 47 21 18 48 49 syl112anc N 8 N 4 2 N 4 N 2
51 45 50 mpbid N 8 N 4 N 2
52 flge N 2 4 4 N 2 4 N 2
53 31 42 52 sylancl N 8 N 4 N 2 4 N 2
54 51 53 mpbid N 8 N 4 N 2
55 54 1 breqtrrdi N 8 N 4 M
56 eluz2 M 4 4 M 4 M
57 43 33 55 56 syl3anbrc N 8 N M 4
58 eluznn 4 M 4 M
59 41 57 58 sylancr N 8 N M
60 59 nnge1d N 8 N 1 M
61 lemul2 1 M 2 0 < 2 1 M 2 1 2 M
62 37 34 18 48 61 syl112anc N 8 N 1 M 2 1 2 M
63 60 62 mpbid N 8 N 2 1 2 M
64 40 63 eqbrtrrid N 8 N 2 2 M
65 37 18 36 39 64 ltletrd N 8 N 1 < 2 M
66 36 65 rplogcld N 8 N log 2 M +
67 66 rpred N 8 N log 2 M
68 2nn 2
69 nnmulcl 2 M 2 M
70 68 59 69 sylancr N 8 N 2 M
71 67 70 nndivred N 8 N log 2 M 2 M
72 29 71 remulcld N 8 N π _ N log 2 M 2 M
73 rehalfcl π _ N log 2 M 2 M π _ N log 2 M 2 M 2
74 72 73 syl N 8 N π _ N log 2 M 2 M 2
75 0red N 8 N 0
76 8pos 0 < 8
77 76 a1i N 8 N 0 < 8
78 75 20 21 77 25 ltletrd N 8 N 0 < N
79 21 78 elrpd N 8 N N +
80 79 relogcld N 8 N log N
81 80 79 rerpdivcld N 8 N log N N
82 29 81 remulcld N 8 N π _ N log N N
83 14 a1i N 8 N log 2 1 2 e
84 ppinncl 2 M 2 2 M π _ 2 M
85 36 64 84 syl2anc N 8 N π _ 2 M
86 85 nnred N 8 N π _ 2 M
87 86 71 remulcld N 8 N π _ 2 M log 2 M 2 M
88 remulcl log 2 1 2 e 2 M log 2 1 2 e 2 M
89 14 36 88 sylancr N 8 N log 2 1 2 e 2 M
90 4pos 0 < 4
91 46 90 elrpii 4 +
92 rpexpcl 4 + M 4 M +
93 91 33 92 sylancr N 8 N 4 M +
94 59 nnrpd N 8 N M +
95 93 94 rpdivcld N 8 N 4 M M +
96 95 relogcld N 8 N log 4 M M
97 86 67 remulcld N 8 N π _ 2 M log 2 M
98 94 relogcld N 8 N log M
99 epr e +
100 rerpdivcl M e + M e
101 34 99 100 sylancl N 8 N M e
102 93 relogcld N 8 N log 4 M
103 7 a1i N 8 N e
104 egt2lt3 2 < e e < 3
105 104 simpri e < 3
106 3lt4 3 < 4
107 3re 3
108 7 107 46 lttri e < 3 3 < 4 e < 4
109 105 106 108 mp2an e < 4
110 109 a1i N 8 N e < 4
111 103 47 34 110 55 ltletrd N 8 N e < M
112 103 34 111 ltled N 8 N e M
113 7 leidi e e
114 logdivlt e e e M e M e < M log M M < log e e
115 7 113 114 mpanl12 M e M e < M log M M < log e e
116 34 112 115 syl2anc N 8 N e < M log M M < log e e
117 111 116 mpbid N 8 N log M M < log e e
118 loge log e = 1
119 118 oveq1i log e e = 1 e
120 117 119 breqtrdi N 8 N log M M < 1 e
121 7 10 pm3.2i e 0 < e
122 121 a1i N 8 N e 0 < e
123 59 nngt0d N 8 N 0 < M
124 34 123 jca N 8 N M 0 < M
125 lt2mul2div log M e 0 < e 1 M 0 < M log M e < 1 M log M M < 1 e
126 98 122 37 124 125 syl22anc N 8 N log M e < 1 M log M M < 1 e
127 120 126 mpbird N 8 N log M e < 1 M
128 34 recnd N 8 N M
129 128 mulid2d N 8 N 1 M = M
130 127 129 breqtrd N 8 N log M e < M
131 ltmuldiv log M M e 0 < e log M e < M log M < M e
132 98 34 122 131 syl3anc N 8 N log M e < M log M < M e
133 130 132 mpbid N 8 N log M < M e
134 98 101 102 133 ltsub2dd N 8 N log 4 M M e < log 4 M log M
135 4 recni log 2
136 135 a1i N 8 N log 2
137 13 recni 1 2 e
138 137 a1i N 8 N 1 2 e
139 70 nnrpd N 8 N 2 M +
140 139 rpcnd N 8 N 2 M
141 136 138 140 subdird N 8 N log 2 1 2 e 2 M = log 2 2 M 1 2 e 2 M
142 136 140 mulcomd N 8 N log 2 2 M = 2 M log 2
143 2z 2
144 zmulcl 2 M 2 M
145 143 33 144 sylancr N 8 N 2 M
146 relogexp 2 + 2 M log 2 2 M = 2 M log 2
147 2 145 146 sylancr N 8 N log 2 2 M = 2 M log 2
148 2cnd N 8 N 2
149 59 nnnn0d N 8 N M 0
150 2nn0 2 0
151 150 a1i N 8 N 2 0
152 148 149 151 expmuld N 8 N 2 2 M = 2 2 M
153 sq2 2 2 = 4
154 153 oveq1i 2 2 M = 4 M
155 152 154 eqtrdi N 8 N 2 2 M = 4 M
156 155 fveq2d N 8 N log 2 2 M = log 4 M
157 142 147 156 3eqtr2d N 8 N log 2 2 M = log 4 M
158 8 recni 2 e
159 158 a1i N 8 N 2 e
160 12 a1i N 8 N 2 e 0
161 140 159 160 divrec2d N 8 N 2 M 2 e = 1 2 e 2 M
162 7 recni e
163 162 a1i N 8 N e
164 7 10 gt0ne0ii e 0
165 164 a1i N 8 N e 0
166 15 a1i N 8 N 2 0
167 128 163 148 165 166 divcan5d N 8 N 2 M 2 e = M e
168 161 167 eqtr3d N 8 N 1 2 e 2 M = M e
169 157 168 oveq12d N 8 N log 2 2 M 1 2 e 2 M = log 4 M M e
170 141 169 eqtrd N 8 N log 2 1 2 e 2 M = log 4 M M e
171 93 94 relogdivd N 8 N log 4 M M = log 4 M log M
172 134 170 171 3brtr4d N 8 N log 2 1 2 e 2 M < log 4 M M
173 eqid if 2 M ( 2 M M) 2 M ( 2 M M) = if 2 M ( 2 M M) 2 M ( 2 M M)
174 173 chebbnd1lem1 M 4 log 4 M M < π _ 2 M log 2 M
175 57 174 syl N 8 N log 4 M M < π _ 2 M log 2 M
176 89 96 97 172 175 lttrd N 8 N log 2 1 2 e 2 M < π _ 2 M log 2 M
177 83 97 139 ltmuldivd N 8 N log 2 1 2 e 2 M < π _ 2 M log 2 M log 2 1 2 e < π _ 2 M log 2 M 2 M
178 176 177 mpbid N 8 N log 2 1 2 e < π _ 2 M log 2 M 2 M
179 86 recnd N 8 N π _ 2 M
180 66 rpcnd N 8 N log 2 M
181 139 rpcnne0d N 8 N 2 M 2 M 0
182 divass π _ 2 M log 2 M 2 M 2 M 0 π _ 2 M log 2 M 2 M = π _ 2 M log 2 M 2 M
183 179 180 181 182 syl3anc N 8 N π _ 2 M log 2 M 2 M = π _ 2 M log 2 M 2 M
184 178 183 breqtrd N 8 N log 2 1 2 e < π _ 2 M log 2 M 2 M
185 flle N 2 N 2 N 2
186 31 185 syl N 8 N N 2 N 2
187 1 186 eqbrtrid N 8 N M N 2
188 lemuldiv2 M N 2 0 < 2 2 M N M N 2
189 34 21 18 48 188 syl112anc N 8 N 2 M N M N 2
190 187 189 mpbird N 8 N 2 M N
191 ppiwordi 2 M N 2 M N π _ 2 M π _ N
192 36 21 190 191 syl3anc N 8 N π _ 2 M π _ N
193 66 139 rpdivcld N 8 N log 2 M 2 M +
194 86 29 193 lemul1d N 8 N π _ 2 M π _ N π _ 2 M log 2 M 2 M π _ N log 2 M 2 M
195 192 194 mpbid N 8 N π _ 2 M log 2 M 2 M π _ N log 2 M 2 M
196 83 87 72 184 195 ltletrd N 8 N log 2 1 2 e < π _ N log 2 M 2 M
197 ltdiv1 log 2 1 2 e π _ N log 2 M 2 M 2 0 < 2 log 2 1 2 e < π _ N log 2 M 2 M log 2 1 2 e 2 < π _ N log 2 M 2 M 2
198 83 72 18 48 197 syl112anc N 8 N log 2 1 2 e < π _ N log 2 M 2 M log 2 1 2 e 2 < π _ N log 2 M 2 M 2
199 196 198 mpbid N 8 N log 2 1 2 e 2 < π _ N log 2 M 2 M 2
200 1 chebbnd1lem2 N 8 N log 2 M 2 M < 2 log N N
201 remulcl 2 log N N 2 log N N
202 6 81 201 sylancr N 8 N 2 log N N
203 28 nngt0d N 8 N 0 < π _ N
204 ltmul2 log 2 M 2 M 2 log N N π _ N 0 < π _ N log 2 M 2 M < 2 log N N π _ N log 2 M 2 M < π _ N 2 log N N
205 71 202 29 203 204 syl112anc N 8 N log 2 M 2 M < 2 log N N π _ N log 2 M 2 M < π _ N 2 log N N
206 200 205 mpbid N 8 N π _ N log 2 M 2 M < π _ N 2 log N N
207 29 recnd N 8 N π _ N
208 81 recnd N 8 N log N N
209 207 148 208 mul12d N 8 N π _ N 2 log N N = 2 π _ N log N N
210 206 209 breqtrd N 8 N π _ N log 2 M 2 M < 2 π _ N log N N
211 ltdivmul π _ N log 2 M 2 M π _ N log N N 2 0 < 2 π _ N log 2 M 2 M 2 < π _ N log N N π _ N log 2 M 2 M < 2 π _ N log N N
212 72 82 18 48 211 syl112anc N 8 N π _ N log 2 M 2 M 2 < π _ N log N N π _ N log 2 M 2 M < 2 π _ N log N N
213 210 212 mpbird N 8 N π _ N log 2 M 2 M 2 < π _ N log N N
214 17 74 82 199 213 lttrd N 8 N log 2 1 2 e 2 < π _ N log N N