Metamath Proof Explorer


Theorem chebbnd1lem1

Description: Lemma for chebbnd1 : show a lower bound on ppi ( x ) at even integers using similar techniques to those used to prove bpos . (Note that the expression K is actually equal to 2 x. N , but proving that is not necessary for the proof, and it's too much work.) The key to the proof is bposlem1 , which shows that each term in the expansion ( ( 2 x. N )C N ) = prod p e. Prime ( p ^ ( p pCnt ( ( 2 x. N )C N ) ) ) is at most 2 x. N , so that the sum really only has nonzero elements up to 2 x. N , and since each term is at most 2 x. N , after taking logs we get the inequality ppi ( 2 x. N ) x. log ( 2 x. N ) < log ( ( 2 x. N ) _C N ) , and bclbnd finishes the proof. (Contributed by Mario Carneiro, 22-Sep-2014) (Revised by Mario Carneiro, 15-Apr-2016)

Ref Expression
Hypothesis chebbnd1lem1.1 K = if 2 N ( 2 N N) 2 N ( 2 N N)
Assertion chebbnd1lem1 N 4 log 4 N N < π _ 2 N log 2 N

Proof

Step Hyp Ref Expression
1 chebbnd1lem1.1 K = if 2 N ( 2 N N) 2 N ( 2 N N)
2 4nn 4
3 eluznn 4 N 4 N
4 2 3 mpan N 4 N
5 4 nnnn0d N 4 N 0
6 nnexpcl 4 N 0 4 N
7 2 5 6 sylancr N 4 4 N
8 7 nnrpd N 4 4 N +
9 4 nnrpd N 4 N +
10 8 9 rpdivcld N 4 4 N N +
11 10 relogcld N 4 log 4 N N
12 fzctr N 0 N 0 2 N
13 5 12 syl N 4 N 0 2 N
14 bccl2 N 0 2 N ( 2 N N)
15 13 14 syl N 4 ( 2 N N)
16 15 nnrpd N 4 ( 2 N N) +
17 16 relogcld N 4 log ( 2 N N)
18 2z 2
19 eluzelz N 4 N
20 zmulcl 2 N 2 N
21 18 19 20 sylancr N 4 2 N
22 21 zred N 4 2 N
23 ppicl 2 N π _ 2 N 0
24 22 23 syl N 4 π _ 2 N 0
25 24 nn0red N 4 π _ 2 N
26 2nn 2
27 nnmulcl 2 N 2 N
28 26 4 27 sylancr N 4 2 N
29 28 nnrpd N 4 2 N +
30 29 relogcld N 4 log 2 N
31 25 30 remulcld N 4 π _ 2 N log 2 N
32 bclbnd N 4 4 N N < ( 2 N N)
33 logltb 4 N N + ( 2 N N) + 4 N N < ( 2 N N) log 4 N N < log ( 2 N N)
34 10 16 33 syl2anc N 4 4 N N < ( 2 N N) log 4 N N < log ( 2 N N)
35 32 34 mpbid N 4 log 4 N N < log ( 2 N N)
36 28 15 ifcld N 4 if 2 N ( 2 N N) 2 N ( 2 N N)
37 1 36 eqeltrid N 4 K
38 37 nnred N 4 K
39 ppicl K π _ K 0
40 38 39 syl N 4 π _ K 0
41 40 nn0red N 4 π _ K
42 41 30 remulcld N 4 π _ K log 2 N
43 fzfid N 4 1 K Fin
44 inss1 1 K 1 K
45 ssfi 1 K Fin 1 K 1 K 1 K Fin
46 43 44 45 sylancl N 4 1 K Fin
47 37 nnzd N 4 K
48 15 nnzd N 4 ( 2 N N)
49 15 nnred N 4 ( 2 N N)
50 min2 2 N ( 2 N N) if 2 N ( 2 N N) 2 N ( 2 N N) ( 2 N N)
51 22 49 50 syl2anc N 4 if 2 N ( 2 N N) 2 N ( 2 N N) ( 2 N N)
52 1 51 eqbrtrid N 4 K ( 2 N N)
53 eluz2 ( 2 N N) K K ( 2 N N) K ( 2 N N)
54 47 48 52 53 syl3anbrc N 4 ( 2 N N) K
55 fzss2 ( 2 N N) K 1 K 1 ( 2 N N)
56 54 55 syl N 4 1 K 1 ( 2 N N)
57 56 ssrind N 4 1 K 1 ( 2 N N)
58 57 sselda N 4 k 1 K k 1 ( 2 N N)
59 simpr N 4 k 1 ( 2 N N) k 1 ( 2 N N)
60 59 elin1d N 4 k 1 ( 2 N N) k 1 ( 2 N N)
61 elfznn k 1 ( 2 N N) k
62 60 61 syl N 4 k 1 ( 2 N N) k
63 59 elin2d N 4 k 1 ( 2 N N) k
64 15 adantr N 4 k 1 ( 2 N N) ( 2 N N)
65 63 64 pccld N 4 k 1 ( 2 N N) k pCnt ( 2 N N) 0
66 62 65 nnexpcld N 4 k 1 ( 2 N N) k k pCnt ( 2 N N)
67 66 nnrpd N 4 k 1 ( 2 N N) k k pCnt ( 2 N N) +
68 67 relogcld N 4 k 1 ( 2 N N) log k k pCnt ( 2 N N)
69 58 68 syldan N 4 k 1 K log k k pCnt ( 2 N N)
70 30 adantr N 4 k 1 K log 2 N
71 elinel2 k 1 K k
72 bposlem1 N k k k pCnt ( 2 N N) 2 N
73 4 71 72 syl2an N 4 k 1 K k k pCnt ( 2 N N) 2 N
74 58 67 syldan N 4 k 1 K k k pCnt ( 2 N N) +
75 74 reeflogd N 4 k 1 K e log k k pCnt ( 2 N N) = k k pCnt ( 2 N N)
76 29 adantr N 4 k 1 K 2 N +
77 76 reeflogd N 4 k 1 K e log 2 N = 2 N
78 73 75 77 3brtr4d N 4 k 1 K e log k k pCnt ( 2 N N) e log 2 N
79 efle log k k pCnt ( 2 N N) log 2 N log k k pCnt ( 2 N N) log 2 N e log k k pCnt ( 2 N N) e log 2 N
80 69 70 79 syl2anc N 4 k 1 K log k k pCnt ( 2 N N) log 2 N e log k k pCnt ( 2 N N) e log 2 N
81 78 80 mpbird N 4 k 1 K log k k pCnt ( 2 N N) log 2 N
82 46 69 70 81 fsumle N 4 k 1 K log k k pCnt ( 2 N N) k 1 K log 2 N
83 68 recnd N 4 k 1 ( 2 N N) log k k pCnt ( 2 N N)
84 58 83 syldan N 4 k 1 K log k k pCnt ( 2 N N)
85 eldifn k 1 ( 2 N N) 1 K ¬ k 1 K
86 85 adantl N 4 k 1 ( 2 N N) 1 K ¬ k 1 K
87 simpr N 4 k 1 ( 2 N N) 1 K k 1 ( 2 N N) 1 K
88 87 eldifad N 4 k 1 ( 2 N N) 1 K k 1 ( 2 N N)
89 88 elin1d N 4 k 1 ( 2 N N) 1 K k 1 ( 2 N N)
90 89 61 syl N 4 k 1 ( 2 N N) 1 K k
91 90 adantrr N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k
92 91 nnred N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k
93 88 66 syldan N 4 k 1 ( 2 N N) 1 K k k pCnt ( 2 N N)
94 93 nnred N 4 k 1 ( 2 N N) 1 K k k pCnt ( 2 N N)
95 94 adantrr N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k k pCnt ( 2 N N)
96 22 adantr N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) 2 N
97 91 nncnd N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k
98 97 exp1d N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k 1 = k
99 91 nnge1d N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) 1 k
100 simprr N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k pCnt ( 2 N N)
101 nnuz = 1
102 100 101 eleqtrdi N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k pCnt ( 2 N N) 1
103 92 99 102 leexp2ad N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k 1 k k pCnt ( 2 N N)
104 98 103 eqbrtrrd N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k k k pCnt ( 2 N N)
105 4 adantr N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) N
106 88 elin2d N 4 k 1 ( 2 N N) 1 K k
107 106 adantrr N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k
108 105 107 72 syl2anc N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k k pCnt ( 2 N N) 2 N
109 92 95 96 104 108 letrd N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k 2 N
110 elfzle2 k 1 ( 2 N N) k ( 2 N N)
111 89 110 syl N 4 k 1 ( 2 N N) 1 K k ( 2 N N)
112 111 adantrr N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k ( 2 N N)
113 49 adantr N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) ( 2 N N)
114 lemin k 2 N ( 2 N N) k if 2 N ( 2 N N) 2 N ( 2 N N) k 2 N k ( 2 N N)
115 92 96 113 114 syl3anc N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k if 2 N ( 2 N N) 2 N ( 2 N N) k 2 N k ( 2 N N)
116 109 112 115 mpbir2and N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k if 2 N ( 2 N N) 2 N ( 2 N N)
117 116 1 breqtrrdi N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k K
118 37 adantr N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) K
119 118 nnzd N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) K
120 fznn K k 1 K k k K
121 119 120 syl N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k 1 K k k K
122 91 117 121 mpbir2and N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k 1 K
123 122 107 elind N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k 1 K
124 123 expr N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k 1 K
125 86 124 mtod N 4 k 1 ( 2 N N) 1 K ¬ k pCnt ( 2 N N)
126 88 65 syldan N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) 0
127 elnn0 k pCnt ( 2 N N) 0 k pCnt ( 2 N N) k pCnt ( 2 N N) = 0
128 126 127 sylib N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) k pCnt ( 2 N N) = 0
129 128 ord N 4 k 1 ( 2 N N) 1 K ¬ k pCnt ( 2 N N) k pCnt ( 2 N N) = 0
130 125 129 mpd N 4 k 1 ( 2 N N) 1 K k pCnt ( 2 N N) = 0
131 130 oveq2d N 4 k 1 ( 2 N N) 1 K k k pCnt ( 2 N N) = k 0
132 90 nncnd N 4 k 1 ( 2 N N) 1 K k
133 132 exp0d N 4 k 1 ( 2 N N) 1 K k 0 = 1
134 131 133 eqtrd N 4 k 1 ( 2 N N) 1 K k k pCnt ( 2 N N) = 1
135 134 fveq2d N 4 k 1 ( 2 N N) 1 K log k k pCnt ( 2 N N) = log 1
136 log1 log 1 = 0
137 135 136 eqtrdi N 4 k 1 ( 2 N N) 1 K log k k pCnt ( 2 N N) = 0
138 fzfid N 4 1 ( 2 N N) Fin
139 inss1 1 ( 2 N N) 1 ( 2 N N)
140 ssfi 1 ( 2 N N) Fin 1 ( 2 N N) 1 ( 2 N N) 1 ( 2 N N) Fin
141 138 139 140 sylancl N 4 1 ( 2 N N) Fin
142 57 84 137 141 fsumss N 4 k 1 K log k k pCnt ( 2 N N) = k 1 ( 2 N N) log k k pCnt ( 2 N N)
143 62 nnrpd N 4 k 1 ( 2 N N) k +
144 65 nn0zd N 4 k 1 ( 2 N N) k pCnt ( 2 N N)
145 relogexp k + k pCnt ( 2 N N) log k k pCnt ( 2 N N) = k pCnt ( 2 N N) log k
146 143 144 145 syl2anc N 4 k 1 ( 2 N N) log k k pCnt ( 2 N N) = k pCnt ( 2 N N) log k
147 146 sumeq2dv N 4 k 1 ( 2 N N) log k k pCnt ( 2 N N) = k 1 ( 2 N N) k pCnt ( 2 N N) log k
148 pclogsum ( 2 N N) k 1 ( 2 N N) k pCnt ( 2 N N) log k = log ( 2 N N)
149 15 148 syl N 4 k 1 ( 2 N N) k pCnt ( 2 N N) log k = log ( 2 N N)
150 142 147 149 3eqtrd N 4 k 1 K log k k pCnt ( 2 N N) = log ( 2 N N)
151 30 recnd N 4 log 2 N
152 fsumconst 1 K Fin log 2 N k 1 K log 2 N = 1 K log 2 N
153 46 151 152 syl2anc N 4 k 1 K log 2 N = 1 K log 2 N
154 2eluzge1 2 1
155 ppival2g K 2 1 π _ K = 1 K
156 47 154 155 sylancl N 4 π _ K = 1 K
157 156 oveq1d N 4 π _ K log 2 N = 1 K log 2 N
158 153 157 eqtr4d N 4 k 1 K log 2 N = π _ K log 2 N
159 82 150 158 3brtr3d N 4 log ( 2 N N) π _ K log 2 N
160 min1 2 N ( 2 N N) if 2 N ( 2 N N) 2 N ( 2 N N) 2 N
161 22 49 160 syl2anc N 4 if 2 N ( 2 N N) 2 N ( 2 N N) 2 N
162 1 161 eqbrtrid N 4 K 2 N
163 ppiwordi K 2 N K 2 N π _ K π _ 2 N
164 38 22 162 163 syl3anc N 4 π _ K π _ 2 N
165 1red N 4 1
166 2re 2
167 166 a1i N 4 2
168 1lt2 1 < 2
169 168 a1i N 4 1 < 2
170 2t1e2 2 1 = 2
171 4 nnge1d N 4 1 N
172 eluzelre N 4 N
173 2pos 0 < 2
174 166 173 pm3.2i 2 0 < 2
175 174 a1i N 4 2 0 < 2
176 lemul2 1 N 2 0 < 2 1 N 2 1 2 N
177 165 172 175 176 syl3anc N 4 1 N 2 1 2 N
178 171 177 mpbid N 4 2 1 2 N
179 170 178 eqbrtrrid N 4 2 2 N
180 165 167 22 169 179 ltletrd N 4 1 < 2 N
181 22 180 rplogcld N 4 log 2 N +
182 41 25 181 lemul1d N 4 π _ K π _ 2 N π _ K log 2 N π _ 2 N log 2 N
183 164 182 mpbid N 4 π _ K log 2 N π _ 2 N log 2 N
184 17 42 31 159 183 letrd N 4 log ( 2 N N) π _ 2 N log 2 N
185 11 17 31 35 184 ltletrd N 4 log 4 N N < π _ 2 N log 2 N