Metamath Proof Explorer


Theorem chtppilimlem1

Description: Lemma for chtppilim . (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Hypotheses chtppilim.1 φA+
chtppilim.2 φA<1
chtppilim.3 φN2+∞
chtppilim.4 φNAπ_N<1A
Assertion chtppilimlem1 φA2π_NlogN<θN

Proof

Step Hyp Ref Expression
1 chtppilim.1 φA+
2 chtppilim.2 φA<1
3 chtppilim.3 φN2+∞
4 chtppilim.4 φNAπ_N<1A
5 1 rpred φA
6 5 recnd φA
7 6 sqvald φA2=AA
8 7 oveq1d φA2π_NlogN=AAπ_NlogN
9 2re 2
10 elicopnf 2N2+∞N2N
11 9 10 ax-mp N2+∞N2N
12 3 11 sylib φN2N
13 12 simpld φN
14 ppicl Nπ_N0
15 13 14 syl φπ_N0
16 15 nn0red φπ_N
17 16 recnd φπ_N
18 0red φ0
19 9 a1i φ2
20 2pos 0<2
21 20 a1i φ0<2
22 12 simprd φ2N
23 18 19 13 21 22 ltletrd φ0<N
24 13 23 elrpd φN+
25 24 relogcld φlogN
26 25 recnd φlogN
27 6 6 17 26 mul4d φAAπ_NlogN=Aπ_NAlogN
28 8 27 eqtrd φA2π_NlogN=Aπ_NAlogN
29 5 16 remulcld φAπ_N
30 5 25 remulcld φAlogN
31 29 30 remulcld φAπ_NAlogN
32 24 5 rpcxpcld φNA+
33 32 rpred φNA
34 ppicl NAπ_NA0
35 33 34 syl φπ_NA0
36 35 nn0red φπ_NA
37 16 36 resubcld φπ_Nπ_NA
38 37 30 remulcld φπ_Nπ_NAAlogN
39 chtcl NθN
40 13 39 syl φθN
41 1red φ1
42 1lt2 1<2
43 42 a1i φ1<2
44 41 19 13 43 22 ltletrd φ1<N
45 13 44 rplogcld φlogN+
46 1 45 rpmulcld φAlogN+
47 16 33 resubcld φπ_NNA
48 ppinncl N2Nπ_N
49 12 48 syl φπ_N
50 33 49 nndivred φNAπ_N
51 50 41 5 4 ltsub13d φA<1NAπ_N
52 33 recnd φNA
53 49 nnrpd φπ_N+
54 53 rpcnne0d φπ_Nπ_N0
55 divsubdir π_NNAπ_Nπ_N0π_NNAπ_N=π_Nπ_NNAπ_N
56 17 52 54 55 syl3anc φπ_NNAπ_N=π_Nπ_NNAπ_N
57 divid π_Nπ_N0π_Nπ_N=1
58 54 57 syl φπ_Nπ_N=1
59 58 oveq1d φπ_Nπ_NNAπ_N=1NAπ_N
60 56 59 eqtrd φπ_NNAπ_N=1NAπ_N
61 51 60 breqtrrd φA<π_NNAπ_N
62 5 47 53 ltmuldivd φAπ_N<π_NNAA<π_NNAπ_N
63 61 62 mpbird φAπ_N<π_NNA
64 ppiltx NA+π_NA<NA
65 32 64 syl φπ_NA<NA
66 36 33 16 65 ltsub2dd φπ_NNA<π_Nπ_NA
67 29 47 37 63 66 lttrd φAπ_N<π_Nπ_NA
68 29 37 46 67 ltmul1dd φAπ_NAlogN<π_Nπ_NAAlogN
69 fzfid φNA+1NFin
70 inss1 NA+1NNA+1N
71 ssfi NA+1NFinNA+1NNA+1NNA+1NFin
72 69 70 71 sylancl φNA+1NFin
73 simpr φpNA+1NpNA+1N
74 73 elin2d φpNA+1Np
75 prmnn pp
76 75 nnrpd pp+
77 74 76 syl φpNA+1Np+
78 77 relogcld φpNA+1Nlogp
79 72 78 fsumrecl φpNA+1Nlogp
80 30 recnd φAlogN
81 fsumconst NA+1NFinAlogNpNA+1NAlogN=NA+1NAlogN
82 72 80 81 syl2anc φpNA+1NAlogN=NA+1NAlogN
83 ppifl Nπ_N=π_N
84 13 83 syl φπ_N=π_N
85 ppifl NAπ_NA=π_NA
86 33 85 syl φπ_NA=π_NA
87 84 86 oveq12d φπ_Nπ_NA=π_Nπ_NA
88 41 13 44 ltled φ1N
89 1re 1
90 ltle A1A<1A1
91 5 89 90 sylancl φA<1A1
92 2 91 mpd φA1
93 13 88 5 41 92 cxplead φNAN1
94 13 recnd φN
95 94 cxp1d φN1=N
96 93 95 breqtrd φNAN
97 flword2 NANNANNNA
98 33 13 96 97 syl3anc φNNA
99 ppidif NNAπ_Nπ_NA=NA+1N
100 98 99 syl φπ_Nπ_NA=NA+1N
101 87 100 eqtr3d φπ_Nπ_NA=NA+1N
102 101 oveq1d φπ_Nπ_NAAlogN=NA+1NAlogN
103 82 102 eqtr4d φpNA+1NAlogN=π_Nπ_NAAlogN
104 30 adantr φpNA+1NAlogN
105 33 adantr φpNA+1NNA
106 reflcl NANA
107 peano2re NANA+1
108 33 106 107 3syl φNA+1
109 108 adantr φpNA+1NNA+1
110 77 rpred φpNA+1Np
111 fllep1 NANANA+1
112 33 111 syl φNANA+1
113 112 adantr φpNA+1NNANA+1
114 73 elin1d φpNA+1NpNA+1N
115 elfzle1 pNA+1NNA+1p
116 114 115 syl φpNA+1NNA+1p
117 105 109 110 113 116 letrd φpNA+1NNAp
118 24 rpne0d φN0
119 94 118 6 cxpefd φNA=eAlogN
120 119 eqcomd φeAlogN=NA
121 120 adantr φpNA+1NeAlogN=NA
122 77 reeflogd φpNA+1Nelogp=p
123 117 121 122 3brtr4d φpNA+1NeAlogNelogp
124 efle AlogNlogpAlogNlogpeAlogNelogp
125 104 78 124 syl2anc φpNA+1NAlogNlogpeAlogNelogp
126 123 125 mpbird φpNA+1NAlogNlogp
127 72 104 78 126 fsumle φpNA+1NAlogNpNA+1Nlogp
128 103 127 eqbrtrrd φπ_Nπ_NAAlogNpNA+1Nlogp
129 fzfid φ1NFin
130 inss1 1N1N
131 ssfi 1NFin1N1N1NFin
132 129 130 131 sylancl φ1NFin
133 simpr φp1Np1N
134 133 elin2d φp1Np
135 prmuz2 pp2
136 134 135 syl φp1Np2
137 eluz2b2 p2p1<p
138 136 137 sylib φp1Np1<p
139 138 simpld φp1Np
140 139 nnred φp1Np
141 138 simprd φp1N1<p
142 140 141 rplogcld φp1Nlogp+
143 142 rpred φp1Nlogp
144 142 rpge0d φp1N0logp
145 32 rpge0d φ0NA
146 flge0nn0 NA0NANA0
147 33 145 146 syl2anc φNA0
148 nn0p1nn NA0NA+1
149 147 148 syl φNA+1
150 nnuz =1
151 149 150 eleqtrdi φNA+11
152 fzss1 NA+11NA+1N1N
153 ssrin NA+1N1NNA+1N1N
154 151 152 153 3syl φNA+1N1N
155 132 143 144 154 fsumless φpNA+1Nlogpp1Nlogp
156 chtval NθN=p0Nlogp
157 13 156 syl φθN=p0Nlogp
158 2eluzge1 21
159 ppisval2 N210N=1N
160 13 158 159 sylancl φ0N=1N
161 160 sumeq1d φp0Nlogp=p1Nlogp
162 157 161 eqtrd φθN=p1Nlogp
163 155 162 breqtrrd φpNA+1NlogpθN
164 38 79 40 128 163 letrd φπ_Nπ_NAAlogNθN
165 31 38 40 68 164 ltletrd φAπ_NAlogN<θN
166 28 165 eqbrtrd φA2π_NlogN<θN