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 \in ℝ^{+} ⟼ ψ (a) - a)$
	pntlem1.a	$⊢ φ \to A \in ℝ^{+}$
	pntlem1.b	$⊢ φ \to B \in ℝ^{+}$
	pntlem1.l	$⊢ φ \to L \in (0, 1)$
	pntlem1.d	$⊢ D = A + 1$
	pntlem1.f	$⊢ F = (1 - (\frac{1}{D})) (\frac{\frac{L}{32 B}}{D^{2}})$
	pntlem1.u	$⊢ φ \to U \in ℝ^{+}$
	pntlem1.u2	$⊢ φ \to U \leq A$
	pntlem1.e	$⊢ E = \frac{U}{D}$
	pntlem1.k	$⊢ K = e^{\frac{B}{E}}$
	pntlem1.y	$⊢ φ \to (Y \in ℝ^{+} \land 1 \leq Y)$
	pntlem1.x	$⊢ φ \to (X \in ℝ^{+} \land Y < X)$
	pntlem1.c	$⊢ φ \to C \in ℝ^{+}$
	pntlem1.w	$⊢ W = {(Y + (\frac{4}{L E}))}^{2} + {X K^{2}}^{4} + e^{(\frac{32 B}{(U - E) L E^{2}}) (U \cdot 3 + C)}$
	pntlem1.z	$⊢ φ \to Z \in [W, +∞)$
	pntlem1.m	$⊢ M = ⌊\frac{\log X}{\log K}⌋ + 1$
	pntlem1.n	$⊢ N = ⌊\frac{\frac{\log Z}{\log K}}{2}⌋$
	pntlem1.U	$⊢ φ \to \forall z \in [Y, +∞) \|\frac{R (z)}{z}\| \leq U$
	pntlem1.K	$⊢ φ \to \forall y \in (X, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + L E) z < K y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E)$
Assertion	pntlemk	$⊢ φ \to 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} (\frac{U}{n}) \log n \leq U (\log Z + 3) \log Z$

Proof

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

Metamath Proof Explorer

Theorem pntlemk

Proof