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		elfzelz	$⊢ n \in (⌊\frac{Z}{(1 + L E) V}⌋ + 1 \dots ⌊\frac{Z}{V}⌋) \to n \in ℤ$
134	128 133	syl	$⊢ (φ \land n \in I) \to n \in ℤ$
135		flge	$⊢ (\frac{Z}{V} \in ℝ \land n \in ℤ) \to (n \leq \frac{Z}{V} \leftrightarrow n \leq ⌊\frac{Z}{V}⌋)$
136	132 134 135	syl2anc	$⊢ (φ \land n \in I) \to (n \leq \frac{Z}{V} \leftrightarrow n \leq ⌊\frac{Z}{V}⌋)$
137	130 136	mpbird	$⊢ (φ \land n \in I) \to n \leq \frac{Z}{V}$
138	120	nnred	$⊢ (φ \land n \in I) \to n \in ℝ$
139		ere	$⊢ e \in ℝ$
140	139	a1i	$⊢ (φ \land n \in I) \to e \in ℝ$
141	112	rpred	$⊢ φ \to \frac{Z}{(1 + L E) V} \in ℝ$
142	141	adantr	$⊢ (φ \land n \in I) \to \frac{Z}{(1 + L E) V} \in ℝ$
143	139	a1i	$⊢ φ \to e \in ℝ$
144	38	rpsqrtcld	$⊢ φ \to \sqrt{Z} \in ℝ^{+}$
145	144	rpred	$⊢ φ \to \sqrt{Z} \in ℝ$
146	40	simp2d	$⊢ φ \to e \leq \sqrt{Z}$
147	111	rpred	$⊢ φ \to (1 + L E) V \in ℝ$
148	65	rpred	$⊢ φ \to K^{J + 1} \in ℝ$
149	22	simpld	$⊢ φ \to (K^{J} < V \land (1 + L E) V < K K^{J})$
150	149	simprd	$⊢ φ \to (1 + L E) V < K K^{J}$
151	61	rpcnd	$⊢ φ \to K \in ℂ$
152	61 63	rpexpcld	$⊢ φ \to K^{J} \in ℝ^{+}$
153	152	rpcnd	$⊢ φ \to K^{J} \in ℂ$
154	151 153	mulcomd	$⊢ φ \to K K^{J} = K^{J} K$
155	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)$
156	155	simp1d	$⊢ φ \to M \in ℕ$
157		elfzouz	$⊢ J \in (M ..^N) \to J \in ℤ_{\geq M}$
158	23 157	syl	$⊢ φ \to J \in ℤ_{\geq M}$
159		eluznn	$⊢ (M \in ℕ \land J \in ℤ_{\geq M}) \to J \in ℕ$
160	156 158 159	syl2anc	$⊢ φ \to J \in ℕ$
161	160	nnnn0d	$⊢ φ \to J \in ℕ_{0}$
162	151 161	expp1d	$⊢ φ \to K^{J + 1} = K^{J} K$
163	154 162	eqtr4d	$⊢ φ \to K K^{J} = K^{J + 1}$
164	150 163	breqtrd	$⊢ φ \to (1 + L E) V < K^{J + 1}$
165	147 148 164	ltled	$⊢ φ \to (1 + L E) V \leq K^{J + 1}$
166		fzofzp1	$⊢ J \in (M ..^N) \to J + 1 \in (M \dots N)$
167	23 166	syl	$⊢ φ \to J + 1 \in (M \dots N)$
168	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})$
169	167 168	mpdan	$⊢ φ \to (X < K^{J + 1} \land K^{J + 1} \leq \sqrt{Z})$
170	169	simprd	$⊢ φ \to K^{J + 1} \leq \sqrt{Z}$
171	147 148 145 165 170	letrd	$⊢ φ \to (1 + L E) V \leq \sqrt{Z}$
172	147 145 144	lemul2d	$⊢ φ \to ((1 + L E) V \leq \sqrt{Z} \leftrightarrow \sqrt{Z} (1 + L E) V \leq \sqrt{Z} \sqrt{Z})$
173	171 172	mpbid	$⊢ φ \to \sqrt{Z} (1 + L E) V \leq \sqrt{Z} \sqrt{Z}$
174	38	rprege0d	$⊢ φ \to (Z \in ℝ \land 0 \leq Z)$
175		remsqsqrt	$⊢ (Z \in ℝ \land 0 \leq Z) \to \sqrt{Z} \sqrt{Z} = Z$
176	174 175	syl	$⊢ φ \to \sqrt{Z} \sqrt{Z} = Z$
177	173 176	breqtrd	$⊢ φ \to \sqrt{Z} (1 + L E) V \leq Z$
178	145 39 111	lemuldivd	$⊢ φ \to (\sqrt{Z} (1 + L E) V \leq Z \leftrightarrow \sqrt{Z} \leq \frac{Z}{(1 + L E) V})$
179	177 178	mpbid	$⊢ φ \to \sqrt{Z} \leq \frac{Z}{(1 + L E) V}$
180	143 145 141 146 179	letrd	$⊢ φ \to e \leq \frac{Z}{(1 + L E) V}$
181	180	adantr	$⊢ (φ \land n \in I) \to e \leq \frac{Z}{(1 + L E) V}$
182		reflcl	$⊢ \frac{Z}{(1 + L E) V} \in ℝ \to ⌊\frac{Z}{(1 + L E) V}⌋ \in ℝ$
183		peano2re	$⊢ ⌊\frac{Z}{(1 + L E) V}⌋ \in ℝ \to ⌊\frac{Z}{(1 + L E) V}⌋ + 1 \in ℝ$
184	141 182 183	3syl	$⊢ φ \to ⌊\frac{Z}{(1 + L E) V}⌋ + 1 \in ℝ$
185	184	adantr	$⊢ (φ \land n \in I) \to ⌊\frac{Z}{(1 + L E) V}⌋ + 1 \in ℝ$
186		fllep1	$⊢ \frac{Z}{(1 + L E) V} \in ℝ \to \frac{Z}{(1 + L E) V} \leq ⌊\frac{Z}{(1 + L E) V}⌋ + 1$
187	142 186	syl	$⊢ (φ \land n \in I) \to \frac{Z}{(1 + L E) V} \leq ⌊\frac{Z}{(1 + L E) V}⌋ + 1$
188		elfzle1	$⊢ n \in (⌊\frac{Z}{(1 + L E) V}⌋ + 1 \dots ⌊\frac{Z}{V}⌋) \to ⌊\frac{Z}{(1 + L E) V}⌋ + 1 \leq n$
189	128 188	syl	$⊢ (φ \land n \in I) \to ⌊\frac{Z}{(1 + L E) V}⌋ + 1 \leq n$
190	142 185 138 187 189	letrd	$⊢ (φ \land n \in I) \to \frac{Z}{(1 + L E) V} \leq n$
191	140 142 138 181 190	letrd	$⊢ (φ \land n \in I) \to e \leq n$
192	140 138 132 191 137	letrd	$⊢ (φ \land n \in I) \to e \leq \frac{Z}{V}$
193		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})$
194	138 191 132 192 193	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})$
195	137 194	mpbid	$⊢ (φ \land n \in I) \to \frac{\log (\frac{Z}{V})}{\frac{Z}{V}} \leq \frac{\log n}{n}$
196	54	adantr	$⊢ (φ \land n \in I) \to \frac{\log (\frac{Z}{V})}{\frac{Z}{V}} \in ℝ$
197		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}))$
198	196 123 106 197	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}))$
199	195 198	mpbid	$⊢ (φ \land n \in I) \to (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}}) \leq (U - E) (\frac{\log n}{n})$
200	27	rpcnd	$⊢ φ \to U - E \in ℂ$
201	200	adantr	$⊢ (φ \land n \in I) \to U - E \in ℂ$
202	122	recnd	$⊢ (φ \land n \in I) \to \log n \in ℂ$
203	121	rpcnne0d	$⊢ (φ \land n \in I) \to (n \in ℂ \land n \neq 0)$
204		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$
205	201 202 203 204	syl3anc	$⊢ (φ \land n \in I) \to \frac{(U - E) \log n}{n} = (\frac{U - E}{n}) \log n$
206		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})$
207	201 202 203 206	syl3anc	$⊢ (φ \land n \in I) \to \frac{(U - E) \log n}{n} = (U - E) (\frac{\log n}{n})$
208	205 207	eqtr3d	$⊢ (φ \land n \in I) \to (\frac{U - E}{n}) \log n = (U - E) (\frac{\log n}{n})$
209	51	adantr	$⊢ (φ \land n \in I) \to U - E \in ℝ$
210	209 120	nndivred	$⊢ (φ \land n \in I) \to \frac{U - E}{n} \in ℝ$
211	125 85	syldan	$⊢ (φ \land n \in I) \to (\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\| \in ℝ$
212		log1	$⊢ \log 1 = 0$
213	120	nnge1d	$⊢ (φ \land n \in I) \to 1 \leq n$
214		logleb	$⊢ (1 \in ℝ^{+} \land n \in ℝ^{+}) \to (1 \leq n \leftrightarrow \log 1 \leq \log n)$
215	108 121 214	sylancr	$⊢ (φ \land n \in I) \to (1 \leq n \leftrightarrow \log 1 \leq \log n)$
216	213 215	mpbid	$⊢ (φ \land n \in I) \to \log 1 \leq \log n$
217	212 216	eqbrtrrid	$⊢ (φ \land n \in I) \to 0 \leq \log n$
218	7	rpcnd	$⊢ φ \to U \in ℂ$
219	218	adantr	$⊢ (φ \land n \in I) \to U \in ℂ$
220	30	rpred	$⊢ φ \to E \in ℝ$
221	220	adantr	$⊢ (φ \land n \in I) \to E \in ℝ$
222	221	recnd	$⊢ (φ \land n \in I) \to E \in ℂ$
223		divsubdir	$⊢ (U \in ℂ \land E \in ℂ \land (n \in ℂ \land n \neq 0)) \to \frac{U - E}{n} = (\frac{U}{n}) - (\frac{E}{n})$
224	219 222 203 223	syl3anc	$⊢ (φ \land n \in I) \to \frac{U - E}{n} = (\frac{U}{n}) - (\frac{E}{n})$
225	125 84	syldan	$⊢ (φ \land n \in I) \to \|\frac{R (\frac{Z}{n})}{Z}\| \in ℝ$
226	221 120	nndivred	$⊢ (φ \land n \in I) \to \frac{E}{n} \in ℝ$
227	125 75	syldan	$⊢ (φ \land n \in I) \to \frac{U}{n} \in ℝ$
228	125 81	syldan	$⊢ (φ \land n \in I) \to R (\frac{Z}{n}) \in ℝ$
229	228	recnd	$⊢ (φ \land n \in I) \to R (\frac{Z}{n}) \in ℂ$
230	38	adantr	$⊢ (φ \land n \in I) \to Z \in ℝ^{+}$
231	230	rpcnne0d	$⊢ (φ \land n \in I) \to (Z \in ℂ \land Z \neq 0)$
232		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}$
233	229 231 203 232	syl3anc	$⊢ (φ \land n \in I) \to \frac{R (\frac{Z}{n})}{\frac{Z}{n}} = \frac{R (\frac{Z}{n}) n}{Z}$
234	121	rpcnd	$⊢ (φ \land n \in I) \to n \in ℂ$
235		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$
236	229 234 231 235	syl3anc	$⊢ (φ \land n \in I) \to \frac{R (\frac{Z}{n}) n}{Z} = (\frac{R (\frac{Z}{n})}{Z}) n$
237	233 236	eqtrd	$⊢ (φ \land n \in I) \to \frac{R (\frac{Z}{n})}{\frac{Z}{n}} = (\frac{R (\frac{Z}{n})}{Z}) n$
238	237	fveq2d	$⊢ (φ \land n \in I) \to \|\frac{R (\frac{Z}{n})}{\frac{Z}{n}}\| = \|(\frac{R (\frac{Z}{n})}{Z}) n\|$
239	125 83	syldan	$⊢ (φ \land n \in I) \to \frac{R (\frac{Z}{n})}{Z} \in ℂ$
240	239 234	absmuld	$⊢ (φ \land n \in I) \to \|(\frac{R (\frac{Z}{n})}{Z}) n\| = \|\frac{R (\frac{Z}{n})}{Z}\| \|n\|$
241	121	rprege0d	$⊢ (φ \land n \in I) \to (n \in ℝ \land 0 \leq n)$
242		absid	$⊢ (n \in ℝ \land 0 \leq n) \to \|n\| = n$
243	241 242	syl	$⊢ (φ \land n \in I) \to \|n\| = n$
244	243	oveq2d	$⊢ (φ \land n \in I) \to \|\frac{R (\frac{Z}{n})}{Z}\| \|n\| = \|\frac{R (\frac{Z}{n})}{Z}\| n$
245	238 240 244	3eqtrd	$⊢ (φ \land n \in I) \to \|\frac{R (\frac{Z}{n})}{\frac{Z}{n}}\| = \|\frac{R (\frac{Z}{n})}{Z}\| n$
246		fveq2	$⊢ u = \frac{Z}{n} \to R (u) = R (\frac{Z}{n})$
247		id	$⊢ u = \frac{Z}{n} \to u = \frac{Z}{n}$
248	246 247	oveq12d	$⊢ u = \frac{Z}{n} \to \frac{R (u)}{u} = \frac{R (\frac{Z}{n})}{\frac{Z}{n}}$
249	248	fveq2d	$⊢ u = \frac{Z}{n} \to \|\frac{R (u)}{u}\| = \|\frac{R (\frac{Z}{n})}{\frac{Z}{n}}\|$
250	249	breq1d	$⊢ u = \frac{Z}{n} \to (\|\frac{R (u)}{u}\| \leq E \leftrightarrow \|\frac{R (\frac{Z}{n})}{\frac{Z}{n}}\| \leq E)$
251	22	simprd	$⊢ φ \to \forall u \in [V, (1 + L E) V] \|\frac{R (u)}{u}\| \leq E$
252	251	adantr	$⊢ (φ \land n \in I) \to \forall u \in [V, (1 + L E) V] \|\frac{R (u)}{u}\| \leq E$
253	39	adantr	$⊢ (φ \land n \in I) \to Z \in ℝ$
254	253 120	nndivred	$⊢ (φ \land n \in I) \to \frac{Z}{n} \in ℝ$
255	21	rpregt0d	$⊢ φ \to (V \in ℝ \land 0 < V)$
256	255	adantr	$⊢ (φ \land n \in I) \to (V \in ℝ \land 0 < V)$
257		lemuldiv2	$⊢ (n \in ℝ \land Z \in ℝ \land (V \in ℝ \land 0 < V)) \to (V n \leq Z \leftrightarrow n \leq \frac{Z}{V})$
258	138 253 256 257	syl3anc	$⊢ (φ \land n \in I) \to (V n \leq Z \leftrightarrow n \leq \frac{Z}{V})$
259	137 258	mpbird	$⊢ (φ \land n \in I) \to V n \leq Z$
260	256	simpld	$⊢ (φ \land n \in I) \to V \in ℝ$
261	260 253 121	lemuldivd	$⊢ (φ \land n \in I) \to (V n \leq Z \leftrightarrow V \leq \frac{Z}{n})$
262	259 261	mpbid	$⊢ (φ \land n \in I) \to V \leq \frac{Z}{n}$
263	111	rpregt0d	$⊢ φ \to ((1 + L E) V \in ℝ \land 0 < (1 + L E) V)$
264	263	adantr	$⊢ (φ \land n \in I) \to ((1 + L E) V \in ℝ \land 0 < (1 + L E) V)$
265	121	rpregt0d	$⊢ (φ \land n \in I) \to (n \in ℝ \land 0 < n)$
266		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)$
267	253 264 265 266	syl3anc	$⊢ (φ \land n \in I) \to (\frac{Z}{(1 + L E) V} \leq n \leftrightarrow \frac{Z}{n} \leq (1 + L E) V)$
268	190 267	mpbid	$⊢ (φ \land n \in I) \to \frac{Z}{n} \leq (1 + L E) V$
269	21	rpred	$⊢ φ \to V \in ℝ$
270	269	adantr	$⊢ (φ \land n \in I) \to V \in ℝ$
271	147	adantr	$⊢ (φ \land n \in I) \to (1 + L E) V \in ℝ$
272		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))$
273	270 271 272	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))$
274	254 262 268 273	mpbir3and	$⊢ (φ \land n \in I) \to \frac{Z}{n} \in [V, (1 + L E) V]$
275	250 252 274	rspcdva	$⊢ (φ \land n \in I) \to \|\frac{R (\frac{Z}{n})}{\frac{Z}{n}}\| \leq E$
276	245 275	eqbrtrrd	$⊢ (φ \land n \in I) \to \|\frac{R (\frac{Z}{n})}{Z}\| n \leq E$
277	225 221 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})$
278	276 277	mpbid	$⊢ (φ \land n \in I) \to \|\frac{R (\frac{Z}{n})}{Z}\| \leq \frac{E}{n}$
279	225 226 227 278	lesub2dd	$⊢ (φ \land n \in I) \to (\frac{U}{n}) - (\frac{E}{n}) \leq (\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|$
280	224 279	eqbrtrd	$⊢ (φ \land n \in I) \to \frac{U - E}{n} \leq (\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|$
281	210 211 122 217 280	lemul1ad	$⊢ (φ \land n \in I) \to (\frac{U - E}{n}) \log n \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
282	208 281	eqbrtrrd	$⊢ (φ \land n \in I) \to (U - E) (\frac{\log n}{n}) \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
283	99 124 126 199 282	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$
284	283	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$
285	74	nnred	$⊢ (φ \land n \in O) \to n \in ℝ$
286	38 152	rpdivcld	$⊢ φ \to \frac{Z}{K^{J}} \in ℝ^{+}$
287	286	rpred	$⊢ φ \to \frac{Z}{K^{J}} \in ℝ$
288	287	adantr	$⊢ (φ \land n \in O) \to \frac{Z}{K^{J}} \in ℝ$
289	11	simpld	$⊢ φ \to Y \in ℝ^{+}$
290	38 289	rpdivcld	$⊢ φ \to \frac{Z}{Y} \in ℝ^{+}$
291	290	rpred	$⊢ φ \to \frac{Z}{Y} \in ℝ$
292	291	adantr	$⊢ (φ \land n \in O) \to \frac{Z}{Y} \in ℝ$
293		simpr	$⊢ (φ \land n \in O) \to n \in O$
294	293 20	eleqtrdi	$⊢ (φ \land n \in O) \to n \in (⌊\frac{Z}{K^{J + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{J}}⌋)$
295		elfzle2	$⊢ n \in (⌊\frac{Z}{K^{J + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{J}}⌋) \to n \leq ⌊\frac{Z}{K^{J}}⌋$
296	294 295	syl	$⊢ (φ \land n \in O) \to n \leq ⌊\frac{Z}{K^{J}}⌋$
297	74	nnzd	$⊢ (φ \land n \in O) \to n \in ℤ$
298		flge	$⊢ (\frac{Z}{K^{J}} \in ℝ \land n \in ℤ) \to (n \leq \frac{Z}{K^{J}} \leftrightarrow n \leq ⌊\frac{Z}{K^{J}}⌋)$
299	288 297 298	syl2anc	$⊢ (φ \land n \in O) \to (n \leq \frac{Z}{K^{J}} \leftrightarrow n \leq ⌊\frac{Z}{K^{J}}⌋)$
300	296 299	mpbird	$⊢ (φ \land n \in O) \to n \leq \frac{Z}{K^{J}}$
301	289	rpred	$⊢ φ \to Y \in ℝ$
302	12	simpld	$⊢ φ \to X \in ℝ^{+}$
303	302	rpred	$⊢ φ \to X \in ℝ$
304	152	rpred	$⊢ φ \to K^{J} \in ℝ$
305	12	simprd	$⊢ φ \to Y < X$
306	301 303 305	ltled	$⊢ φ \to Y \leq X$
307		elfzofz	$⊢ J \in (M ..^N) \to J \in (M \dots N)$
308	23 307	syl	$⊢ φ \to J \in (M \dots N)$
309	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})$
310	308 309	mpdan	$⊢ φ \to (X < K^{J} \land K^{J} \leq \sqrt{Z})$
311	310	simpld	$⊢ φ \to X < K^{J}$
312	303 304 311	ltled	$⊢ φ \to X \leq K^{J}$
313	301 303 304 306 312	letrd	$⊢ φ \to Y \leq K^{J}$
314	289 152 38	lediv2d	$⊢ φ \to (Y \leq K^{J} \leftrightarrow \frac{Z}{K^{J}} \leq \frac{Z}{Y})$
315	313 314	mpbid	$⊢ φ \to \frac{Z}{K^{J}} \leq \frac{Z}{Y}$
316	315	adantr	$⊢ (φ \land n \in O) \to \frac{Z}{K^{J}} \leq \frac{Z}{Y}$
317	285 288 292 300 316	letrd	$⊢ (φ \land n \in O) \to n \leq \frac{Z}{Y}$
318	74 317	jca	$⊢ (φ \land n \in O) \to (n \in ℕ \land n \leq \frac{Z}{Y})$
319	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$
320	318 319	syldan	$⊢ (φ \land n \in O) \to 0 \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
321	320	adantr	$⊢ ((φ \land n \in O) \land \neg n \in I) \to 0 \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
322	103 104 284 321	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$
323	58 102 87 322	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$
324	98 323	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$
325	45 56 88 89 324	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