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 + ψ a a
pntlem1.a φ A +
pntlem1.b φ B +
pntlem1.l φ L 0 1
pntlem1.d D = A + 1
pntlem1.f F = 1 1 D L 32 B D 2
pntlem1.u φ U +
pntlem1.u2 φ U A
pntlem1.e E = U D
pntlem1.k K = e B E
pntlem1.y φ Y + 1 Y
pntlem1.x φ X + Y < X
pntlem1.c φ C +
pntlem1.w W = Y + 4 L E 2 + X K 2 4 + e 32 B U E L E 2 U 3 + C
pntlem1.z φ Z W +∞
pntlem1.m M = log X log K + 1
pntlem1.n N = log Z log K 2
pntlem1.U φ z Y +∞ R z z U
pntlem1.K φ y X +∞ z + y < z 1 + L E z < K y u z 1 + L E z R u u E
Assertion pntlemk φ 2 n = 1 Z Y U n log n U log Z + 3 log Z

Proof

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