pntlemj

Description: Lemma for pnt . The induction step. Using pntibnd , we find an interval in K ^ J ... K ^ ( J + 1 ) which is sufficiently large and has a much smaller value, R ( z ) / z <_ E (instead of our original bound R ( z ) / z <_ U ). (Contributed by Mario Carneiro, 13-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)$
	pntlem1.o	$⊢ O = (⌊\frac{Z}{K^{J + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{J}}⌋)$
	pntlem1.v	$⊢ φ \to V \in ℝ^{+}$
	pntlem1.V	$⊢ φ \to ((K^{J} < V \land (1 + L E) V < K K^{J}) \land \forall u \in [V, (1 + L E) V] \|\frac{R (u)}{u}\| \leq E)$
	pntlem1.j	$⊢ φ \to J \in (M ..^N)$
	pntlem1.i	$⊢ I = (⌊\frac{Z}{(1 + L E) V}⌋ + 1 \dots ⌊\frac{Z}{V}⌋)$
Assertion	pntlemj	$⊢ φ \to (U - E) (\frac{L E}{8}) \log Z \leq \sum_{n \in O} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$

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		pntlem1.o	$⊢ O = (⌊\frac{Z}{K^{J + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{J}}⌋)$
21		pntlem1.v	$⊢ φ \to V \in ℝ^{+}$
22		pntlem1.V	$⊢ φ \to ((K^{J} < V \land (1 + L E) V < K K^{J}) \land \forall u \in [V, (1 + L E) V] \|\frac{R (u)}{u}\| \leq E)$
23		pntlem1.j	$⊢ φ \to J \in (M ..^N)$
24		pntlem1.i	$⊢ I = (⌊\frac{Z}{(1 + L E) V}⌋ + 1 \dots ⌊\frac{Z}{V}⌋)$
25	1 2 3 4 5 6 7 8 9 10	pntlemc	$⊢ φ \to (E \in ℝ^{+} \land K \in ℝ^{+} \land (E \in (0, 1) \land 1 < K \land U - E \in ℝ^{+}))$
26	25	simp3d	$⊢ φ \to (E \in (0, 1) \land 1 < K \land U - E \in ℝ^{+})$
27	26	simp3d	$⊢ φ \to U - E \in ℝ^{+}$
28	1 2 3 4 5 6	pntlemd	$⊢ φ \to (L \in ℝ^{+} \land D \in ℝ^{+} \land F \in ℝ^{+})$
29	28	simp1d	$⊢ φ \to L \in ℝ^{+}$
30	25	simp1d	$⊢ φ \to E \in ℝ^{+}$
31	29 30	rpmulcld	$⊢ φ \to L E \in ℝ^{+}$
32		8nn	$⊢ 8 \in ℕ$
33		nnrp	$⊢ 8 \in ℕ \to 8 \in ℝ^{+}$
34	32 33	ax-mp	$⊢ 8 \in ℝ^{+}$
35		rpdivcl	$⊢ (L E \in ℝ^{+} \land 8 \in ℝ^{+}) \to \frac{L E}{8} \in ℝ^{+}$
36	31 34 35	sylancl	$⊢ φ \to \frac{L E}{8} \in ℝ^{+}$
37	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))$
38	37	simp1d	$⊢ φ \to Z \in ℝ^{+}$
39	38	rpred	$⊢ φ \to Z \in ℝ$
40	37	simp2d	$⊢ φ \to (1 < Z \land e \leq \sqrt{Z} \land \sqrt{Z} \leq \frac{Z}{Y})$
41	40	simp1d	$⊢ φ \to 1 < Z$
42	39 41	rplogcld	$⊢ φ \to \log Z \in ℝ^{+}$
43	36 42	rpmulcld	$⊢ φ \to (\frac{L E}{8}) \log Z \in ℝ^{+}$
44	27 43	rpmulcld	$⊢ φ \to (U - E) (\frac{L E}{8}) \log Z \in ℝ^{+}$
45	44	rpred	$⊢ φ \to (U - E) (\frac{L E}{8}) \log Z \in ℝ$
46		fzfid	$⊢ φ \to (⌊\frac{Z}{(1 + L E) V}⌋ + 1 \dots ⌊\frac{Z}{V}⌋) \in Fin$
47	24 46	eqeltrid	$⊢ φ \to I \in Fin$
48		hashcl	$⊢ I \in Fin \to \|I\| \in ℕ_{0}$
49	47 48	syl	$⊢ φ \to \|I\| \in ℕ_{0}$
50	49	nn0red	$⊢ φ \to \|I\| \in ℝ$
51	27	rpred	$⊢ φ \to U - E \in ℝ$
52	38 21	rpdivcld	$⊢ φ \to \frac{Z}{V} \in ℝ^{+}$
53	52	relogcld	$⊢ φ \to \log (\frac{Z}{V}) \in ℝ$
54	53 52	rerpdivcld	$⊢ φ \to \frac{\log (\frac{Z}{V})}{\frac{Z}{V}} \in ℝ$
55	51 54	remulcld	$⊢ φ \to (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) \in ℝ$
56	50 55	remulcld	$⊢ φ \to \|I\| (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) \in ℝ$
57		fzfid	$⊢ φ \to (⌊\frac{Z}{K^{J + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{J}}⌋) \in Fin$
58	20 57	eqeltrid	$⊢ φ \to O \in Fin$
59	7	rpred	$⊢ φ \to U \in ℝ$
60	59	adantr	$⊢ (φ \land n \in O) \to U \in ℝ$
61	25	simp2d	$⊢ φ \to K \in ℝ^{+}$
62		elfzoelz	$⊢ J \in (M ..^N) \to J \in ℤ$
63	23 62	syl	$⊢ φ \to J \in ℤ$
64	63	peano2zd	$⊢ φ \to J + 1 \in ℤ$
65	61 64	rpexpcld	$⊢ φ \to K^{J + 1} \in ℝ^{+}$
66	38 65	rpdivcld	$⊢ φ \to \frac{Z}{K^{J + 1}} \in ℝ^{+}$
67	66	rprege0d	$⊢ φ \to (\frac{Z}{K^{J + 1}} \in ℝ \land 0 \leq \frac{Z}{K^{J + 1}})$
68		flge0nn0	$⊢ (\frac{Z}{K^{J + 1}} \in ℝ \land 0 \leq \frac{Z}{K^{J + 1}}) \to ⌊\frac{Z}{K^{J + 1}}⌋ \in ℕ_{0}$
69		nn0p1nn	$⊢ ⌊\frac{Z}{K^{J + 1}}⌋ \in ℕ_{0} \to ⌊\frac{Z}{K^{J + 1}}⌋ + 1 \in ℕ$
70	67 68 69	3syl	$⊢ φ \to ⌊\frac{Z}{K^{J + 1}}⌋ + 1 \in ℕ$
71		elfzuz	$⊢ n \in (⌊\frac{Z}{K^{J + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{J}}⌋) \to n \in ℤ_{\geq (⌊\frac{Z}{K^{J + 1}}⌋ + 1)}$
72	71 20	eleq2s	$⊢ n \in O \to n \in ℤ_{\geq (⌊\frac{Z}{K^{J + 1}}⌋ + 1)}$
73		eluznn	$⊢ (⌊\frac{Z}{K^{J + 1}}⌋ + 1 \in ℕ \land n \in ℤ_{\geq (⌊\frac{Z}{K^{J + 1}}⌋ + 1)}) \to n \in ℕ$
74	70 72 73	syl2an	$⊢ (φ \land n \in O) \to n \in ℕ$
75	60 74	nndivred	$⊢ (φ \land n \in O) \to \frac{U}{n} \in ℝ$
76	38	adantr	$⊢ (φ \land n \in O) \to Z \in ℝ^{+}$
77	74	nnrpd	$⊢ (φ \land n \in O) \to n \in ℝ^{+}$
78	76 77	rpdivcld	$⊢ (φ \land n \in O) \to \frac{Z}{n} \in ℝ^{+}$
79	1	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
80	79	ffvelrni	$⊢ \frac{Z}{n} \in ℝ^{+} \to R (\frac{Z}{n}) \in ℝ$
81	78 80	syl	$⊢ (φ \land n \in O) \to R (\frac{Z}{n}) \in ℝ$
82	81 76	rerpdivcld	$⊢ (φ \land n \in O) \to \frac{R (\frac{Z}{n})}{Z} \in ℝ$
83	82	recnd	$⊢ (φ \land n \in O) \to \frac{R (\frac{Z}{n})}{Z} \in ℂ$
84	83	abscld	$⊢ (φ \land n \in O) \to \|\frac{R (\frac{Z}{n})}{Z}\| \in ℝ$
85	75 84	resubcld	$⊢ (φ \land n \in O) \to (\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\| \in ℝ$
86	77	relogcld	$⊢ (φ \land n \in O) \to \log n \in ℝ$
87	85 86	remulcld	$⊢ (φ \land n \in O) \to ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ$
88	58 87	fsumrecl	$⊢ φ \to \sum_{n \in O} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ$
89	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24	pntlemr	$⊢ φ \to (U - E) (\frac{L E}{8}) \log Z \leq \|I\| (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}})$
90	55	recnd	$⊢ φ \to (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) \in ℂ$
91		fsumconst	$⊢ (I \in Fin \land (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) \in ℂ) \to \sum_{n \in I} (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) = \|I\| (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}})$
92	47 90 91	syl2anc	$⊢ φ \to \sum_{n \in I} (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) = \|I\| (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}})$
93	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24	pntlemq	$⊢ φ \to I \subseteq O$
94	90	ralrimivw	$⊢ φ \to \forall n \in I (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) \in ℂ$
95	58	olcd	$⊢ φ \to (O \subseteq ℤ_{\geq 1} \lor O \in Fin)$
96		sumss2	$⊢ ((I \subseteq O \land \forall n \in I (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) \in ℂ) \land (O \subseteq ℤ_{\geq 1} \lor O \in Fin)) \to \sum_{n \in I} (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) = \sum_{n \in O} if (n \in I, (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}), 0)$
97	93 94 95 96	syl21anc	$⊢ φ \to \sum_{n \in I} (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) = \sum_{n \in O} if (n \in I, (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}), 0)$
98	92 97	eqtr3d	$⊢ φ \to \|I\| (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) = \sum_{n \in O} if (n \in I, (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}), 0)$
99	55	adantr	$⊢ (φ \land n \in I) \to (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) \in ℝ$
100	99	adantlr	$⊢ ((φ \land n \in O) \land n \in I) \to (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) \in ℝ$
101		0red	$⊢ ((φ \land n \in O) \land \neg n \in I) \to 0 \in ℝ$
102	100 101	ifclda	$⊢ (φ \land n \in O) \to if (n \in I, (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}), 0) \in ℝ$
103		breq1	$⊢ (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) = if (n \in I, (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}), 0) \to ((U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \leftrightarrow if (n \in I, (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}), 0) \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n)$
104		breq1	$⊢ 0 = if (n \in I, (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}), 0) \to (0 \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \leftrightarrow if (n \in I, (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}), 0) \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n)$
105	27	rpregt0d	$⊢ φ \to (U - E \in ℝ \land 0 < U - E)$
106	105	adantr	$⊢ (φ \land n \in I) \to (U - E \in ℝ \land 0 < U - E)$
107	106	simpld	$⊢ (φ \land n \in I) \to U - E \in ℝ$
108		1rp	$⊢ 1 \in ℝ^{+}$
109		rpaddcl	$⊢ (1 \in ℝ^{+} \land L E \in ℝ^{+}) \to 1 + L E \in ℝ^{+}$
110	108 31 109	sylancr	$⊢ φ \to 1 + L E \in ℝ^{+}$
111	110 21	rpmulcld	$⊢ φ \to (1 + L E) V \in ℝ^{+}$
112	38 111	rpdivcld	$⊢ φ \to \frac{Z}{(1 + L E) V} \in ℝ^{+}$
113	112	rprege0d	$⊢ φ \to (\frac{Z}{(1 + L E) V} \in ℝ \land 0 \leq \frac{Z}{(1 + L E) V})$
114		flge0nn0	$⊢ (\frac{Z}{(1 + L E) V} \in ℝ \land 0 \leq \frac{Z}{(1 + L E) V}) \to ⌊\frac{Z}{(1 + L E) V}⌋ \in ℕ_{0}$
115		nn0p1nn	$⊢ ⌊\frac{Z}{(1 + L E) V}⌋ \in ℕ_{0} \to ⌊\frac{Z}{(1 + L E) V}⌋ + 1 \in ℕ$
116	113 114 115	3syl	$⊢ φ \to ⌊\frac{Z}{(1 + L E) V}⌋ + 1 \in ℕ$
117		elfzuz	$⊢ n \in (⌊\frac{Z}{(1 + L E) V}⌋ + 1 \dots ⌊\frac{Z}{V}⌋) \to n \in ℤ_{\geq (⌊\frac{Z}{(1 + L E) V}⌋ + 1)}$
118	117 24	eleq2s	$⊢ n \in I \to n \in ℤ_{\geq (⌊\frac{Z}{(1 + L E) V}⌋ + 1)}$
119		eluznn	$⊢ (⌊\frac{Z}{(1 + L E) V}⌋ + 1 \in ℕ \land n \in ℤ_{\geq (⌊\frac{Z}{(1 + L E) V}⌋ + 1)}) \to n \in ℕ$
120	116 118 119	syl2an	$⊢ (φ \land n \in I) \to n \in ℕ$
121	120	nnrpd	$⊢ (φ \land n \in I) \to n \in ℝ^{+}$
122	121	relogcld	$⊢ (φ \land n \in I) \to \log n \in ℝ$
123	122 120	nndivred	$⊢ (φ \land n \in I) \to \frac{\log n}{n} \in ℝ$
124	107 123	remulcld	$⊢ (φ \land n \in I) \to (U - E) (\frac{\log n}{n}) \in ℝ$
125	93	sselda	$⊢ (φ \land n \in I) \to n \in O$
126	125 87	syldan	$⊢ (φ \land n \in I) \to ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ$
127		simpr	$⊢ (φ \land n \in I) \to n \in I$
128	127 24	eleqtrdi	$⊢ (φ \land n \in I) \to n \in (⌊\frac{Z}{(1 + L E) V}⌋ + 1 \dots ⌊\frac{Z}{V}⌋)$
129		elfzle2	$⊢ n \in (⌊\frac{Z}{(1 + L E) V}⌋ + 1 \dots ⌊\frac{Z}{V}⌋) \to n \leq ⌊\frac{Z}{V}⌋$
130	128 129	syl	$⊢ (φ \land n \in I) \to n \leq ⌊\frac{Z}{V}⌋$
131	52	rpred	$⊢ φ \to \frac{Z}{V} \in ℝ$
132	131	adantr	$⊢ (φ \land n \in I) \to \frac{Z}{V} \in ℝ$
133	128	elfzelzd	$⊢ (φ \land n \in I) \to n \in ℤ$
134		flge	$⊢ (\frac{Z}{V} \in ℝ \land n \in ℤ) \to (n \leq \frac{Z}{V} \leftrightarrow n \leq ⌊\frac{Z}{V}⌋)$
135	132 133 134	syl2anc	$⊢ (φ \land n \in I) \to (n \leq \frac{Z}{V} \leftrightarrow n \leq ⌊\frac{Z}{V}⌋)$
136	130 135	mpbird	$⊢ (φ \land n \in I) \to n \leq \frac{Z}{V}$
137	120	nnred	$⊢ (φ \land n \in I) \to n \in ℝ$
138		ere	$⊢ e \in ℝ$
139	138	a1i	$⊢ (φ \land n \in I) \to e \in ℝ$
140	112	rpred	$⊢ φ \to \frac{Z}{(1 + L E) V} \in ℝ$
141	140	adantr	$⊢ (φ \land n \in I) \to \frac{Z}{(1 + L E) V} \in ℝ$
142	138	a1i	$⊢ φ \to e \in ℝ$
143	38	rpsqrtcld	$⊢ φ \to \sqrt{Z} \in ℝ^{+}$
144	143	rpred	$⊢ φ \to \sqrt{Z} \in ℝ$
145	40	simp2d	$⊢ φ \to e \leq \sqrt{Z}$
146	111	rpred	$⊢ φ \to (1 + L E) V \in ℝ$
147	65	rpred	$⊢ φ \to K^{J + 1} \in ℝ$
148	22	simpld	$⊢ φ \to (K^{J} < V \land (1 + L E) V < K K^{J})$
149	148	simprd	$⊢ φ \to (1 + L E) V < K K^{J}$
150	61	rpcnd	$⊢ φ \to K \in ℂ$
151	61 63	rpexpcld	$⊢ φ \to K^{J} \in ℝ^{+}$
152	151	rpcnd	$⊢ φ \to K^{J} \in ℂ$
153	150 152	mulcomd	$⊢ φ \to K K^{J} = K^{J} K$
154	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	pntlemg	$⊢ φ \to (M \in ℕ \land N \in ℤ_{\geq M} \land \frac{\frac{\log Z}{\log K}}{4} \leq N - M)$
155	154	simp1d	$⊢ φ \to M \in ℕ$
156		elfzouz	$⊢ J \in (M ..^N) \to J \in ℤ_{\geq M}$
157	23 156	syl	$⊢ φ \to J \in ℤ_{\geq M}$
158		eluznn	$⊢ (M \in ℕ \land J \in ℤ_{\geq M}) \to J \in ℕ$
159	155 157 158	syl2anc	$⊢ φ \to J \in ℕ$
160	159	nnnn0d	$⊢ φ \to J \in ℕ_{0}$
161	150 160	expp1d	$⊢ φ \to K^{J + 1} = K^{J} K$
162	153 161	eqtr4d	$⊢ φ \to K K^{J} = K^{J + 1}$
163	149 162	breqtrd	$⊢ φ \to (1 + L E) V < K^{J + 1}$
164	146 147 163	ltled	$⊢ φ \to (1 + L E) V \leq K^{J + 1}$
165		fzofzp1	$⊢ J \in (M ..^N) \to J + 1 \in (M \dots N)$
166	23 165	syl	$⊢ φ \to J + 1 \in (M \dots N)$
167	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	pntlemh	$⊢ (φ \land J + 1 \in (M \dots N)) \to (X < K^{J + 1} \land K^{J + 1} \leq \sqrt{Z})$
168	166 167	mpdan	$⊢ φ \to (X < K^{J + 1} \land K^{J + 1} \leq \sqrt{Z})$
169	168	simprd	$⊢ φ \to K^{J + 1} \leq \sqrt{Z}$
170	146 147 144 164 169	letrd	$⊢ φ \to (1 + L E) V \leq \sqrt{Z}$
171	146 144 143	lemul2d	$⊢ φ \to ((1 + L E) V \leq \sqrt{Z} \leftrightarrow \sqrt{Z} (1 + L E) V \leq \sqrt{Z} \sqrt{Z})$
172	170 171	mpbid	$⊢ φ \to \sqrt{Z} (1 + L E) V \leq \sqrt{Z} \sqrt{Z}$
173	38	rprege0d	$⊢ φ \to (Z \in ℝ \land 0 \leq Z)$
174		remsqsqrt	$⊢ (Z \in ℝ \land 0 \leq Z) \to \sqrt{Z} \sqrt{Z} = Z$
175	173 174	syl	$⊢ φ \to \sqrt{Z} \sqrt{Z} = Z$
176	172 175	breqtrd	$⊢ φ \to \sqrt{Z} (1 + L E) V \leq Z$
177	144 39 111	lemuldivd	$⊢ φ \to (\sqrt{Z} (1 + L E) V \leq Z \leftrightarrow \sqrt{Z} \leq \frac{Z}{(1 + L E) V})$
178	176 177	mpbid	$⊢ φ \to \sqrt{Z} \leq \frac{Z}{(1 + L E) V}$
179	142 144 140 145 178	letrd	$⊢ φ \to e \leq \frac{Z}{(1 + L E) V}$
180	179	adantr	$⊢ (φ \land n \in I) \to e \leq \frac{Z}{(1 + L E) V}$
181		reflcl	$⊢ \frac{Z}{(1 + L E) V} \in ℝ \to ⌊\frac{Z}{(1 + L E) V}⌋ \in ℝ$
182		peano2re	$⊢ ⌊\frac{Z}{(1 + L E) V}⌋ \in ℝ \to ⌊\frac{Z}{(1 + L E) V}⌋ + 1 \in ℝ$
183	140 181 182	3syl	$⊢ φ \to ⌊\frac{Z}{(1 + L E) V}⌋ + 1 \in ℝ$
184	183	adantr	$⊢ (φ \land n \in I) \to ⌊\frac{Z}{(1 + L E) V}⌋ + 1 \in ℝ$
185		fllep1	$⊢ \frac{Z}{(1 + L E) V} \in ℝ \to \frac{Z}{(1 + L E) V} \leq ⌊\frac{Z}{(1 + L E) V}⌋ + 1$
186	141 185	syl	$⊢ (φ \land n \in I) \to \frac{Z}{(1 + L E) V} \leq ⌊\frac{Z}{(1 + L E) V}⌋ + 1$
187		elfzle1	$⊢ n \in (⌊\frac{Z}{(1 + L E) V}⌋ + 1 \dots ⌊\frac{Z}{V}⌋) \to ⌊\frac{Z}{(1 + L E) V}⌋ + 1 \leq n$
188	128 187	syl	$⊢ (φ \land n \in I) \to ⌊\frac{Z}{(1 + L E) V}⌋ + 1 \leq n$
189	141 184 137 186 188	letrd	$⊢ (φ \land n \in I) \to \frac{Z}{(1 + L E) V} \leq n$
190	139 141 137 180 189	letrd	$⊢ (φ \land n \in I) \to e \leq n$
191	139 137 132 190 136	letrd	$⊢ (φ \land n \in I) \to e \leq \frac{Z}{V}$
192		logdivle	$⊢ ((n \in ℝ \land e \leq n) \land (\frac{Z}{V} \in ℝ \land e \leq \frac{Z}{V})) \to (n \leq \frac{Z}{V} \leftrightarrow \frac{\log (\frac{Z}{V})}{\frac{Z}{V}} \leq \frac{\log n}{n})$
193	137 190 132 191 192	syl22anc	$⊢ (φ \land n \in I) \to (n \leq \frac{Z}{V} \leftrightarrow \frac{\log (\frac{Z}{V})}{\frac{Z}{V}} \leq \frac{\log n}{n})$
194	136 193	mpbid	$⊢ (φ \land n \in I) \to \frac{\log (\frac{Z}{V})}{\frac{Z}{V}} \leq \frac{\log n}{n}$
195	54	adantr	$⊢ (φ \land n \in I) \to \frac{\log (\frac{Z}{V})}{\frac{Z}{V}} \in ℝ$
196		lemul2	$⊢ (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}} \in ℝ \land \frac{\log n}{n} \in ℝ \land (U - E \in ℝ \land 0 < U - E)) \to (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}} \leq \frac{\log n}{n} \leftrightarrow (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) \leq (U - E) (\frac{\log n}{n}))$
197	195 123 106 196	syl3anc	$⊢ (φ \land n \in I) \to (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}} \leq \frac{\log n}{n} \leftrightarrow (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) \leq (U - E) (\frac{\log n}{n}))$
198	194 197	mpbid	$⊢ (φ \land n \in I) \to (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) \leq (U - E) (\frac{\log n}{n})$
199	27	rpcnd	$⊢ φ \to U - E \in ℂ$
200	199	adantr	$⊢ (φ \land n \in I) \to U - E \in ℂ$
201	122	recnd	$⊢ (φ \land n \in I) \to \log n \in ℂ$
202	121	rpcnne0d	$⊢ (φ \land n \in I) \to (n \in ℂ \land n \neq 0)$
203		div23	$⊢ (U - E \in ℂ \land \log n \in ℂ \land (n \in ℂ \land n \neq 0)) \to \frac{(U - E) \log n}{n} = (\frac{U - E}{n}) \log n$
204	200 201 202 203	syl3anc	$⊢ (φ \land n \in I) \to \frac{(U - E) \log n}{n} = (\frac{U - E}{n}) \log n$
205		divass	$⊢ (U - E \in ℂ \land \log n \in ℂ \land (n \in ℂ \land n \neq 0)) \to \frac{(U - E) \log n}{n} = (U - E) (\frac{\log n}{n})$
206	200 201 202 205	syl3anc	$⊢ (φ \land n \in I) \to \frac{(U - E) \log n}{n} = (U - E) (\frac{\log n}{n})$
207	204 206	eqtr3d	$⊢ (φ \land n \in I) \to (\frac{U - E}{n}) \log n = (U - E) (\frac{\log n}{n})$
208	51	adantr	$⊢ (φ \land n \in I) \to U - E \in ℝ$
209	208 120	nndivred	$⊢ (φ \land n \in I) \to \frac{U - E}{n} \in ℝ$
210	125 85	syldan	$⊢ (φ \land n \in I) \to (\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\| \in ℝ$
211		log1	$⊢ \log 1 = 0$
212	120	nnge1d	$⊢ (φ \land n \in I) \to 1 \leq n$
213		logleb	$⊢ (1 \in ℝ^{+} \land n \in ℝ^{+}) \to (1 \leq n \leftrightarrow \log 1 \leq \log n)$
214	108 121 213	sylancr	$⊢ (φ \land n \in I) \to (1 \leq n \leftrightarrow \log 1 \leq \log n)$
215	212 214	mpbid	$⊢ (φ \land n \in I) \to \log 1 \leq \log n$
216	211 215	eqbrtrrid	$⊢ (φ \land n \in I) \to 0 \leq \log n$
217	7	rpcnd	$⊢ φ \to U \in ℂ$
218	217	adantr	$⊢ (φ \land n \in I) \to U \in ℂ$
219	30	rpred	$⊢ φ \to E \in ℝ$
220	219	adantr	$⊢ (φ \land n \in I) \to E \in ℝ$
221	220	recnd	$⊢ (φ \land n \in I) \to E \in ℂ$
222		divsubdir	$⊢ (U \in ℂ \land E \in ℂ \land (n \in ℂ \land n \neq 0)) \to \frac{U - E}{n} = (\frac{U}{n}) - (\frac{E}{n})$
223	218 221 202 222	syl3anc	$⊢ (φ \land n \in I) \to \frac{U - E}{n} = (\frac{U}{n}) - (\frac{E}{n})$
224	125 84	syldan	$⊢ (φ \land n \in I) \to \|\frac{R (\frac{Z}{n})}{Z}\| \in ℝ$
225	220 120	nndivred	$⊢ (φ \land n \in I) \to \frac{E}{n} \in ℝ$
226	125 75	syldan	$⊢ (φ \land n \in I) \to \frac{U}{n} \in ℝ$
227	125 81	syldan	$⊢ (φ \land n \in I) \to R (\frac{Z}{n}) \in ℝ$
228	227	recnd	$⊢ (φ \land n \in I) \to R (\frac{Z}{n}) \in ℂ$
229	38	adantr	$⊢ (φ \land n \in I) \to Z \in ℝ^{+}$
230	229	rpcnne0d	$⊢ (φ \land n \in I) \to (Z \in ℂ \land Z \neq 0)$
231		divdiv2	$⊢ (R (\frac{Z}{n}) \in ℂ \land (Z \in ℂ \land Z \neq 0) \land (n \in ℂ \land n \neq 0)) \to \frac{R (\frac{Z}{n})}{\frac{Z}{n}} = \frac{R (\frac{Z}{n}) n}{Z}$
232	228 230 202 231	syl3anc	$⊢ (φ \land n \in I) \to \frac{R (\frac{Z}{n})}{\frac{Z}{n}} = \frac{R (\frac{Z}{n}) n}{Z}$
233	121	rpcnd	$⊢ (φ \land n \in I) \to n \in ℂ$
234		div23	$⊢ (R (\frac{Z}{n}) \in ℂ \land n \in ℂ \land (Z \in ℂ \land Z \neq 0)) \to \frac{R (\frac{Z}{n}) n}{Z} = (\frac{R (\frac{Z}{n})}{Z}) n$
235	228 233 230 234	syl3anc	$⊢ (φ \land n \in I) \to \frac{R (\frac{Z}{n}) n}{Z} = (\frac{R (\frac{Z}{n})}{Z}) n$
236	232 235	eqtrd	$⊢ (φ \land n \in I) \to \frac{R (\frac{Z}{n})}{\frac{Z}{n}} = (\frac{R (\frac{Z}{n})}{Z}) n$
237	236	fveq2d	$⊢ (φ \land n \in I) \to \|\frac{R (\frac{Z}{n})}{\frac{Z}{n}}\| = \|(\frac{R (\frac{Z}{n})}{Z}) n\|$
238	125 83	syldan	$⊢ (φ \land n \in I) \to \frac{R (\frac{Z}{n})}{Z} \in ℂ$
239	238 233	absmuld	$⊢ (φ \land n \in I) \to \|(\frac{R (\frac{Z}{n})}{Z}) n\| = \|\frac{R (\frac{Z}{n})}{Z}\| \|n\|$
240	121	rprege0d	$⊢ (φ \land n \in I) \to (n \in ℝ \land 0 \leq n)$
241		absid	$⊢ (n \in ℝ \land 0 \leq n) \to \|n\| = n$
242	240 241	syl	$⊢ (φ \land n \in I) \to \|n\| = n$
243	242	oveq2d	$⊢ (φ \land n \in I) \to \|\frac{R (\frac{Z}{n})}{Z}\| \|n\| = \|\frac{R (\frac{Z}{n})}{Z}\| n$
244	237 239 243	3eqtrd	$⊢ (φ \land n \in I) \to \|\frac{R (\frac{Z}{n})}{\frac{Z}{n}}\| = \|\frac{R (\frac{Z}{n})}{Z}\| n$
245		fveq2	$⊢ u = \frac{Z}{n} \to R (u) = R (\frac{Z}{n})$
246		id	$⊢ u = \frac{Z}{n} \to u = \frac{Z}{n}$
247	245 246	oveq12d	$⊢ u = \frac{Z}{n} \to \frac{R (u)}{u} = \frac{R (\frac{Z}{n})}{\frac{Z}{n}}$
248	247	fveq2d	$⊢ u = \frac{Z}{n} \to \|\frac{R (u)}{u}\| = \|\frac{R (\frac{Z}{n})}{\frac{Z}{n}}\|$
249	248	breq1d	$⊢ u = \frac{Z}{n} \to (\|\frac{R (u)}{u}\| \leq E \leftrightarrow \|\frac{R (\frac{Z}{n})}{\frac{Z}{n}}\| \leq E)$
250	22	simprd	$⊢ φ \to \forall u \in [V, (1 + L E) V] \|\frac{R (u)}{u}\| \leq E$
251	250	adantr	$⊢ (φ \land n \in I) \to \forall u \in [V, (1 + L E) V] \|\frac{R (u)}{u}\| \leq E$
252	39	adantr	$⊢ (φ \land n \in I) \to Z \in ℝ$
253	252 120	nndivred	$⊢ (φ \land n \in I) \to \frac{Z}{n} \in ℝ$
254	21	rpregt0d	$⊢ φ \to (V \in ℝ \land 0 < V)$
255	254	adantr	$⊢ (φ \land n \in I) \to (V \in ℝ \land 0 < V)$
256		lemuldiv2	$⊢ (n \in ℝ \land Z \in ℝ \land (V \in ℝ \land 0 < V)) \to (V n \leq Z \leftrightarrow n \leq \frac{Z}{V})$
257	137 252 255 256	syl3anc	$⊢ (φ \land n \in I) \to (V n \leq Z \leftrightarrow n \leq \frac{Z}{V})$
258	136 257	mpbird	$⊢ (φ \land n \in I) \to V n \leq Z$
259	255	simpld	$⊢ (φ \land n \in I) \to V \in ℝ$
260	259 252 121	lemuldivd	$⊢ (φ \land n \in I) \to (V n \leq Z \leftrightarrow V \leq \frac{Z}{n})$
261	258 260	mpbid	$⊢ (φ \land n \in I) \to V \leq \frac{Z}{n}$
262	111	rpregt0d	$⊢ φ \to ((1 + L E) V \in ℝ \land 0 < (1 + L E) V)$
263	262	adantr	$⊢ (φ \land n \in I) \to ((1 + L E) V \in ℝ \land 0 < (1 + L E) V)$
264	121	rpregt0d	$⊢ (φ \land n \in I) \to (n \in ℝ \land 0 < n)$
265		lediv23	$⊢ (Z \in ℝ \land ((1 + L E) V \in ℝ \land 0 < (1 + L E) V) \land (n \in ℝ \land 0 < n)) \to (\frac{Z}{(1 + L E) V} \leq n \leftrightarrow \frac{Z}{n} \leq (1 + L E) V)$
266	252 263 264 265	syl3anc	$⊢ (φ \land n \in I) \to (\frac{Z}{(1 + L E) V} \leq n \leftrightarrow \frac{Z}{n} \leq (1 + L E) V)$
267	189 266	mpbid	$⊢ (φ \land n \in I) \to \frac{Z}{n} \leq (1 + L E) V$
268	21	rpred	$⊢ φ \to V \in ℝ$
269	268	adantr	$⊢ (φ \land n \in I) \to V \in ℝ$
270	146	adantr	$⊢ (φ \land n \in I) \to (1 + L E) V \in ℝ$
271		elicc2	$⊢ (V \in ℝ \land (1 + L E) V \in ℝ) \to (\frac{Z}{n} \in [V, (1 + L E) V] \leftrightarrow (\frac{Z}{n} \in ℝ \land V \leq \frac{Z}{n} \land \frac{Z}{n} \leq (1 + L E) V))$
272	269 270 271	syl2anc	$⊢ (φ \land n \in I) \to (\frac{Z}{n} \in [V, (1 + L E) V] \leftrightarrow (\frac{Z}{n} \in ℝ \land V \leq \frac{Z}{n} \land \frac{Z}{n} \leq (1 + L E) V))$
273	253 261 267 272	mpbir3and	$⊢ (φ \land n \in I) \to \frac{Z}{n} \in [V, (1 + L E) V]$
274	249 251 273	rspcdva	$⊢ (φ \land n \in I) \to \|\frac{R (\frac{Z}{n})}{\frac{Z}{n}}\| \leq E$
275	244 274	eqbrtrrd	$⊢ (φ \land n \in I) \to \|\frac{R (\frac{Z}{n})}{Z}\| n \leq E$
276	224 220 121	lemuldivd	$⊢ (φ \land n \in I) \to (\|\frac{R (\frac{Z}{n})}{Z}\| n \leq E \leftrightarrow \|\frac{R (\frac{Z}{n})}{Z}\| \leq \frac{E}{n})$
277	275 276	mpbid	$⊢ (φ \land n \in I) \to \|\frac{R (\frac{Z}{n})}{Z}\| \leq \frac{E}{n}$
278	224 225 226 277	lesub2dd	$⊢ (φ \land n \in I) \to (\frac{U}{n}) - (\frac{E}{n}) \leq (\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|$
279	223 278	eqbrtrd	$⊢ (φ \land n \in I) \to \frac{U - E}{n} \leq (\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|$
280	209 210 122 216 279	lemul1ad	$⊢ (φ \land n \in I) \to (\frac{U - E}{n}) \log n \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
281	207 280	eqbrtrrd	$⊢ (φ \land n \in I) \to (U - E) (\frac{\log n}{n}) \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
282	99 124 126 198 281	letrd	$⊢ (φ \land n \in I) \to (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
283	282	adantlr	$⊢ ((φ \land n \in O) \land n \in I) \to (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
284	74	nnred	$⊢ (φ \land n \in O) \to n \in ℝ$
285	38 151	rpdivcld	$⊢ φ \to \frac{Z}{K^{J}} \in ℝ^{+}$
286	285	rpred	$⊢ φ \to \frac{Z}{K^{J}} \in ℝ$
287	286	adantr	$⊢ (φ \land n \in O) \to \frac{Z}{K^{J}} \in ℝ$
288	11	simpld	$⊢ φ \to Y \in ℝ^{+}$
289	38 288	rpdivcld	$⊢ φ \to \frac{Z}{Y} \in ℝ^{+}$
290	289	rpred	$⊢ φ \to \frac{Z}{Y} \in ℝ$
291	290	adantr	$⊢ (φ \land n \in O) \to \frac{Z}{Y} \in ℝ$
292		simpr	$⊢ (φ \land n \in O) \to n \in O$
293	292 20	eleqtrdi	$⊢ (φ \land n \in O) \to n \in (⌊\frac{Z}{K^{J + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{J}}⌋)$
294		elfzle2	$⊢ n \in (⌊\frac{Z}{K^{J + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{J}}⌋) \to n \leq ⌊\frac{Z}{K^{J}}⌋$
295	293 294	syl	$⊢ (φ \land n \in O) \to n \leq ⌊\frac{Z}{K^{J}}⌋$
296	74	nnzd	$⊢ (φ \land n \in O) \to n \in ℤ$
297		flge	$⊢ (\frac{Z}{K^{J}} \in ℝ \land n \in ℤ) \to (n \leq \frac{Z}{K^{J}} \leftrightarrow n \leq ⌊\frac{Z}{K^{J}}⌋)$
298	287 296 297	syl2anc	$⊢ (φ \land n \in O) \to (n \leq \frac{Z}{K^{J}} \leftrightarrow n \leq ⌊\frac{Z}{K^{J}}⌋)$
299	295 298	mpbird	$⊢ (φ \land n \in O) \to n \leq \frac{Z}{K^{J}}$
300	288	rpred	$⊢ φ \to Y \in ℝ$
301	12	simpld	$⊢ φ \to X \in ℝ^{+}$
302	301	rpred	$⊢ φ \to X \in ℝ$
303	151	rpred	$⊢ φ \to K^{J} \in ℝ$
304	12	simprd	$⊢ φ \to Y < X$
305	300 302 304	ltled	$⊢ φ \to Y \leq X$
306		elfzofz	$⊢ J \in (M ..^N) \to J \in (M \dots N)$
307	23 306	syl	$⊢ φ \to J \in (M \dots N)$
308	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	pntlemh	$⊢ (φ \land J \in (M \dots N)) \to (X < K^{J} \land K^{J} \leq \sqrt{Z})$
309	307 308	mpdan	$⊢ φ \to (X < K^{J} \land K^{J} \leq \sqrt{Z})$
310	309	simpld	$⊢ φ \to X < K^{J}$
311	302 303 310	ltled	$⊢ φ \to X \leq K^{J}$
312	300 302 303 305 311	letrd	$⊢ φ \to Y \leq K^{J}$
313	288 151 38	lediv2d	$⊢ φ \to (Y \leq K^{J} \leftrightarrow \frac{Z}{K^{J}} \leq \frac{Z}{Y})$
314	312 313	mpbid	$⊢ φ \to \frac{Z}{K^{J}} \leq \frac{Z}{Y}$
315	314	adantr	$⊢ (φ \land n \in O) \to \frac{Z}{K^{J}} \leq \frac{Z}{Y}$
316	284 287 291 299 315	letrd	$⊢ (φ \land n \in O) \to n \leq \frac{Z}{Y}$
317	74 316	jca	$⊢ (φ \land n \in O) \to (n \in ℕ \land n \leq \frac{Z}{Y})$
318	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	pntlemn	$⊢ (φ \land (n \in ℕ \land n \leq \frac{Z}{Y})) \to 0 \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
319	317 318	syldan	$⊢ (φ \land n \in O) \to 0 \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
320	319	adantr	$⊢ ((φ \land n \in O) \land \neg n \in I) \to 0 \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
321	103 104 283 320	ifbothda	$⊢ (φ \land n \in O) \to if (n \in I, (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}), 0) \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
322	58 102 87 321	fsumle	$⊢ φ \to \sum_{n \in O} if (n \in I, (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}), 0) \leq \sum_{n \in O} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
323	98 322	eqbrtrd	$⊢ φ \to \|I\| (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) \leq \sum_{n \in O} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
324	45 56 88 89 323	letrd	$⊢ φ \to (U - E) (\frac{L E}{8}) \log Z \leq \sum_{n \in O} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$

Metamath Proof Explorer

Theorem pntlemj

Proof