pntlemf

Description: Lemma for pnt . Add up the pieces in pntlemi to get an estimate slightly better than the naive lower bound 0 . (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)$
Assertion	pntlemf	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \leq \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\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	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 ℝ^{+}))$
21	20	simp3d	$⊢ φ \to (E \in (0, 1) \land 1 < K \land U - E \in ℝ^{+})$
22	21	simp3d	$⊢ φ \to U - E \in ℝ^{+}$
23	1 2 3 4 5 6	pntlemd	$⊢ φ \to (L \in ℝ^{+} \land D \in ℝ^{+} \land F \in ℝ^{+})$
24	23	simp1d	$⊢ φ \to L \in ℝ^{+}$
25	20	simp1d	$⊢ φ \to E \in ℝ^{+}$
26		2z	$⊢ 2 \in ℤ$
27		rpexpcl	$⊢ (E \in ℝ^{+} \land 2 \in ℤ) \to E^{2} \in ℝ^{+}$
28	25 26 27	sylancl	$⊢ φ \to E^{2} \in ℝ^{+}$
29	24 28	rpmulcld	$⊢ φ \to L E^{2} \in ℝ^{+}$
30		3nn0	$⊢ 3 \in ℕ_{0}$
31		2nn	$⊢ 2 \in ℕ$
32	30 31	decnncl	$⊢ 32 \in ℕ$
33		nnrp	$⊢ 32 \in ℕ \to 32 \in ℝ^{+}$
34	32 33	ax-mp	$⊢ 32 \in ℝ^{+}$
35		rpmulcl	$⊢ (32 \in ℝ^{+} \land B \in ℝ^{+}) \to 32 B \in ℝ^{+}$
36	34 3 35	sylancr	$⊢ φ \to 32 B \in ℝ^{+}$
37	29 36	rpdivcld	$⊢ φ \to \frac{L E^{2}}{32 B} \in ℝ^{+}$
38	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))$
39	38	simp1d	$⊢ φ \to Z \in ℝ^{+}$
40	39	rpred	$⊢ φ \to Z \in ℝ$
41	38	simp2d	$⊢ φ \to (1 < Z \land e \leq \sqrt{Z} \land \sqrt{Z} \leq \frac{Z}{Y})$
42	41	simp1d	$⊢ φ \to 1 < Z$
43	40 42	rplogcld	$⊢ φ \to \log Z \in ℝ^{+}$
44		rpexpcl	$⊢ (\log Z \in ℝ^{+} \land 2 \in ℤ) \to {\log Z}^{2} \in ℝ^{+}$
45	43 26 44	sylancl	$⊢ φ \to {\log Z}^{2} \in ℝ^{+}$
46	37 45	rpmulcld	$⊢ φ \to (\frac{L E^{2}}{32 B}) {\log Z}^{2} \in ℝ^{+}$
47	22 46	rpmulcld	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \in ℝ^{+}$
48	47	rpred	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \in ℝ$
49	24 25	rpmulcld	$⊢ φ \to L E \in ℝ^{+}$
50		8re	$⊢ 8 \in ℝ$
51		8pos	$⊢ 0 < 8$
52	50 51	elrpii	$⊢ 8 \in ℝ^{+}$
53		rpdivcl	$⊢ (L E \in ℝ^{+} \land 8 \in ℝ^{+}) \to \frac{L E}{8} \in ℝ^{+}$
54	49 52 53	sylancl	$⊢ φ \to \frac{L E}{8} \in ℝ^{+}$
55	54 43	rpmulcld	$⊢ φ \to (\frac{L E}{8}) \log Z \in ℝ^{+}$
56	22 55	rpmulcld	$⊢ φ \to (U - E) (\frac{L E}{8}) \log Z \in ℝ^{+}$
57	56	rpred	$⊢ φ \to (U - E) (\frac{L E}{8}) \log Z \in ℝ$
58	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)$
59	58	simp1d	$⊢ φ \to M \in ℕ$
60	58	simp2d	$⊢ φ \to N \in ℤ_{\geq M}$
61		eluznn	$⊢ (M \in ℕ \land N \in ℤ_{\geq M}) \to N \in ℕ$
62	59 60 61	syl2anc	$⊢ φ \to N \in ℕ$
63	62	nnred	$⊢ φ \to N \in ℝ$
64	59	nnred	$⊢ φ \to M \in ℝ$
65	63 64	resubcld	$⊢ φ \to N - M \in ℝ$
66	57 65	remulcld	$⊢ φ \to (U - E) (\frac{L E}{8}) \log Z (N - M) \in ℝ$
67		fzfid	$⊢ φ \to (1 \dots ⌊\frac{Z}{Y}⌋) \in Fin$
68	7	rpred	$⊢ φ \to U \in ℝ$
69		elfznn	$⊢ n \in (1 \dots ⌊\frac{Z}{Y}⌋) \to n \in ℕ$
70		nndivre	$⊢ (U \in ℝ \land n \in ℕ) \to \frac{U}{n} \in ℝ$
71	68 69 70	syl2an	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \frac{U}{n} \in ℝ$
72	39	adantr	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to Z \in ℝ^{+}$
73	69	adantl	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to n \in ℕ$
74	73	nnrpd	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to n \in ℝ^{+}$
75	72 74	rpdivcld	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \frac{Z}{n} \in ℝ^{+}$
76	1	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
77	76	ffvelrni	$⊢ \frac{Z}{n} \in ℝ^{+} \to R (\frac{Z}{n}) \in ℝ$
78	75 77	syl	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to R (\frac{Z}{n}) \in ℝ$
79	78 72	rerpdivcld	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \frac{R (\frac{Z}{n})}{Z} \in ℝ$
80	79	recnd	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \frac{R (\frac{Z}{n})}{Z} \in ℂ$
81	80	abscld	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \|\frac{R (\frac{Z}{n})}{Z}\| \in ℝ$
82	71 81	resubcld	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to (\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\| \in ℝ$
83	74	relogcld	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \log n \in ℝ$
84	82 83	remulcld	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ$
85	67 84	fsumrecl	$⊢ φ \to \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ$
86	49	rpcnd	$⊢ φ \to L E \in ℂ$
87	20	simp2d	$⊢ φ \to K \in ℝ^{+}$
88	87	rpred	$⊢ φ \to K \in ℝ$
89	21	simp2d	$⊢ φ \to 1 < K$
90	88 89	rplogcld	$⊢ φ \to \log K \in ℝ^{+}$
91	43 90	rpdivcld	$⊢ φ \to \frac{\log Z}{\log K} \in ℝ^{+}$
92	91	rpcnd	$⊢ φ \to \frac{\log Z}{\log K} \in ℂ$
93		rpcnne0	$⊢ 8 \in ℝ^{+} \to (8 \in ℂ \land 8 \neq 0)$
94	52 93	mp1i	$⊢ φ \to (8 \in ℂ \land 8 \neq 0)$
95		4re	$⊢ 4 \in ℝ$
96		4pos	$⊢ 0 < 4$
97	95 96	elrpii	$⊢ 4 \in ℝ^{+}$
98		rpcnne0	$⊢ 4 \in ℝ^{+} \to (4 \in ℂ \land 4 \neq 0)$
99	97 98	mp1i	$⊢ φ \to (4 \in ℂ \land 4 \neq 0)$
100		divmuldiv	$⊢ ((L E \in ℂ \land \frac{\log Z}{\log K} \in ℂ) \land ((8 \in ℂ \land 8 \neq 0) \land (4 \in ℂ \land 4 \neq 0))) \to (\frac{L E}{8}) (\frac{\frac{\log Z}{\log K}}{4}) = \frac{L E (\frac{\log Z}{\log K})}{8 \cdot 4}$
101	86 92 94 99 100	syl22anc	$⊢ φ \to (\frac{L E}{8}) (\frac{\frac{\log Z}{\log K}}{4}) = \frac{L E (\frac{\log Z}{\log K})}{8 \cdot 4}$
102	10	fveq2i	$⊢ \log K = \log e^{\frac{B}{E}}$
103	3 25	rpdivcld	$⊢ φ \to \frac{B}{E} \in ℝ^{+}$
104	103	rpred	$⊢ φ \to \frac{B}{E} \in ℝ$
105	104	relogefd	$⊢ φ \to \log e^{\frac{B}{E}} = \frac{B}{E}$
106	102 105	eqtrid	$⊢ φ \to \log K = \frac{B}{E}$
107	106	oveq2d	$⊢ φ \to \frac{\log Z}{\log K} = \frac{\log Z}{\frac{B}{E}}$
108	43	rpcnd	$⊢ φ \to \log Z \in ℂ$
109	3	rpcnne0d	$⊢ φ \to (B \in ℂ \land B \neq 0)$
110	25	rpcnne0d	$⊢ φ \to (E \in ℂ \land E \neq 0)$
111		divdiv2	$⊢ (\log Z \in ℂ \land (B \in ℂ \land B \neq 0) \land (E \in ℂ \land E \neq 0)) \to \frac{\log Z}{\frac{B}{E}} = \frac{\log Z E}{B}$
112	108 109 110 111	syl3anc	$⊢ φ \to \frac{\log Z}{\frac{B}{E}} = \frac{\log Z E}{B}$
113	107 112	eqtrd	$⊢ φ \to \frac{\log Z}{\log K} = \frac{\log Z E}{B}$
114	113	oveq2d	$⊢ φ \to L E (\frac{\log Z}{\log K}) = L E (\frac{\log Z E}{B})$
115	25	rpcnd	$⊢ φ \to E \in ℂ$
116	108 115	mulcld	$⊢ φ \to \log Z E \in ℂ$
117		divass	$⊢ (L E \in ℂ \land \log Z E \in ℂ \land (B \in ℂ \land B \neq 0)) \to \frac{L E \log Z E}{B} = L E (\frac{\log Z E}{B})$
118	86 116 109 117	syl3anc	$⊢ φ \to \frac{L E \log Z E}{B} = L E (\frac{\log Z E}{B})$
119	24	rpcnd	$⊢ φ \to L \in ℂ$
120	119 115 108 115	mul4d	$⊢ φ \to L E \log Z E = L \log Z E E$
121	115	sqvald	$⊢ φ \to E^{2} = E E$
122	121	oveq2d	$⊢ φ \to L \log Z E^{2} = L \log Z E E$
123	115	sqcld	$⊢ φ \to E^{2} \in ℂ$
124	119 108 123	mul32d	$⊢ φ \to L \log Z E^{2} = L E^{2} \log Z$
125	120 122 124	3eqtr2d	$⊢ φ \to L E \log Z E = L E^{2} \log Z$
126	125	oveq1d	$⊢ φ \to \frac{L E \log Z E}{B} = \frac{L E^{2} \log Z}{B}$
127	114 118 126	3eqtr2d	$⊢ φ \to L E (\frac{\log Z}{\log K}) = \frac{L E^{2} \log Z}{B}$
128		8t4e32	$⊢ 8 \cdot 4 = 32$
129	128	a1i	$⊢ φ \to 8 \cdot 4 = 32$
130	127 129	oveq12d	$⊢ φ \to \frac{L E (\frac{\log Z}{\log K})}{8 \cdot 4} = \frac{\frac{L E^{2} \log Z}{B}}{32}$
131	29	rpcnd	$⊢ φ \to L E^{2} \in ℂ$
132	131 108	mulcld	$⊢ φ \to L E^{2} \log Z \in ℂ$
133		rpcnne0	$⊢ 32 \in ℝ^{+} \to (32 \in ℂ \land 32 \neq 0)$
134	34 133	mp1i	$⊢ φ \to (32 \in ℂ \land 32 \neq 0)$
135		divdiv1	$⊢ (L E^{2} \log Z \in ℂ \land (B \in ℂ \land B \neq 0) \land (32 \in ℂ \land 32 \neq 0)) \to \frac{\frac{L E^{2} \log Z}{B}}{32} = \frac{L E^{2} \log Z}{B \cdot 32}$
136	132 109 134 135	syl3anc	$⊢ φ \to \frac{\frac{L E^{2} \log Z}{B}}{32} = \frac{L E^{2} \log Z}{B \cdot 32}$
137	32	nncni	$⊢ 32 \in ℂ$
138	3	rpcnd	$⊢ φ \to B \in ℂ$
139		mulcom	$⊢ (32 \in ℂ \land B \in ℂ) \to 32 B = B \cdot 32$
140	137 138 139	sylancr	$⊢ φ \to 32 B = B \cdot 32$
141	140	oveq2d	$⊢ φ \to \frac{L E^{2} \log Z}{32 B} = \frac{L E^{2} \log Z}{B \cdot 32}$
142	36	rpcnne0d	$⊢ φ \to (32 B \in ℂ \land 32 B \neq 0)$
143		div23	$⊢ (L E^{2} \in ℂ \land \log Z \in ℂ \land (32 B \in ℂ \land 32 B \neq 0)) \to \frac{L E^{2} \log Z}{32 B} = (\frac{L E^{2}}{32 B}) \log Z$
144	131 108 142 143	syl3anc	$⊢ φ \to \frac{L E^{2} \log Z}{32 B} = (\frac{L E^{2}}{32 B}) \log Z$
145	136 141 144	3eqtr2d	$⊢ φ \to \frac{\frac{L E^{2} \log Z}{B}}{32} = (\frac{L E^{2}}{32 B}) \log Z$
146	101 130 145	3eqtrd	$⊢ φ \to (\frac{L E}{8}) (\frac{\frac{\log Z}{\log K}}{4}) = (\frac{L E^{2}}{32 B}) \log Z$
147	146	oveq1d	$⊢ φ \to (\frac{L E}{8}) (\frac{\frac{\log Z}{\log K}}{4}) \log Z = (\frac{L E^{2}}{32 B}) \log Z \log Z$
148	54	rpcnd	$⊢ φ \to \frac{L E}{8} \in ℂ$
149	91	rpred	$⊢ φ \to \frac{\log Z}{\log K} \in ℝ$
150		4nn	$⊢ 4 \in ℕ$
151		nndivre	$⊢ (\frac{\log Z}{\log K} \in ℝ \land 4 \in ℕ) \to \frac{\frac{\log Z}{\log K}}{4} \in ℝ$
152	149 150 151	sylancl	$⊢ φ \to \frac{\frac{\log Z}{\log K}}{4} \in ℝ$
153	152	recnd	$⊢ φ \to \frac{\frac{\log Z}{\log K}}{4} \in ℂ$
154	148 108 153	mul32d	$⊢ φ \to (\frac{L E}{8}) \log Z (\frac{\frac{\log Z}{\log K}}{4}) = (\frac{L E}{8}) (\frac{\frac{\log Z}{\log K}}{4}) \log Z$
155	108	sqvald	$⊢ φ \to {\log Z}^{2} = \log Z \log Z$
156	155	oveq2d	$⊢ φ \to (\frac{L E^{2}}{32 B}) {\log Z}^{2} = (\frac{L E^{2}}{32 B}) \log Z \log Z$
157	37	rpcnd	$⊢ φ \to \frac{L E^{2}}{32 B} \in ℂ$
158	157 108 108	mulassd	$⊢ φ \to (\frac{L E^{2}}{32 B}) \log Z \log Z = (\frac{L E^{2}}{32 B}) \log Z \log Z$
159	156 158	eqtr4d	$⊢ φ \to (\frac{L E^{2}}{32 B}) {\log Z}^{2} = (\frac{L E^{2}}{32 B}) \log Z \log Z$
160	147 154 159	3eqtr4d	$⊢ φ \to (\frac{L E}{8}) \log Z (\frac{\frac{\log Z}{\log K}}{4}) = (\frac{L E^{2}}{32 B}) {\log Z}^{2}$
161	58	simp3d	$⊢ φ \to \frac{\frac{\log Z}{\log K}}{4} \leq N - M$
162	152 65 55	lemul2d	$⊢ φ \to (\frac{\frac{\log Z}{\log K}}{4} \leq N - M \leftrightarrow (\frac{L E}{8}) \log Z (\frac{\frac{\log Z}{\log K}}{4}) \leq (\frac{L E}{8}) \log Z (N - M))$
163	161 162	mpbid	$⊢ φ \to (\frac{L E}{8}) \log Z (\frac{\frac{\log Z}{\log K}}{4}) \leq (\frac{L E}{8}) \log Z (N - M)$
164	160 163	eqbrtrrd	$⊢ φ \to (\frac{L E^{2}}{32 B}) {\log Z}^{2} \leq (\frac{L E}{8}) \log Z (N - M)$
165	46	rpred	$⊢ φ \to (\frac{L E^{2}}{32 B}) {\log Z}^{2} \in ℝ$
166	55	rpred	$⊢ φ \to (\frac{L E}{8}) \log Z \in ℝ$
167	166 65	remulcld	$⊢ φ \to (\frac{L E}{8}) \log Z (N - M) \in ℝ$
168	165 167 22	lemul2d	$⊢ φ \to ((\frac{L E^{2}}{32 B}) {\log Z}^{2} \leq (\frac{L E}{8}) \log Z (N - M) \leftrightarrow (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \leq (U - E) (\frac{L E}{8}) \log Z (N - M))$
169	164 168	mpbid	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \leq (U - E) (\frac{L E}{8}) \log Z (N - M)$
170	22	rpcnd	$⊢ φ \to U - E \in ℂ$
171	55	rpcnd	$⊢ φ \to (\frac{L E}{8}) \log Z \in ℂ$
172	65	recnd	$⊢ φ \to N - M \in ℂ$
173	170 171 172	mulassd	$⊢ φ \to (U - E) (\frac{L E}{8}) \log Z (N - M) = (U - E) (\frac{L E}{8}) \log Z (N - M)$
174	169 173	breqtrrd	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \leq (U - E) (\frac{L E}{8}) \log Z (N - M)$
175		fzfid	$⊢ φ \to (⌊\frac{Z}{K^{N}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) \in Fin$
176	62	nnzd	$⊢ φ \to N \in ℤ$
177	87 176	rpexpcld	$⊢ φ \to K^{N} \in ℝ^{+}$
178	39 177	rpdivcld	$⊢ φ \to \frac{Z}{K^{N}} \in ℝ^{+}$
179	178	rprege0d	$⊢ φ \to (\frac{Z}{K^{N}} \in ℝ \land 0 \leq \frac{Z}{K^{N}})$
180		flge0nn0	$⊢ (\frac{Z}{K^{N}} \in ℝ \land 0 \leq \frac{Z}{K^{N}}) \to ⌊\frac{Z}{K^{N}}⌋ \in ℕ_{0}$
181		nn0p1nn	$⊢ ⌊\frac{Z}{K^{N}}⌋ \in ℕ_{0} \to ⌊\frac{Z}{K^{N}}⌋ + 1 \in ℕ$
182	179 180 181	3syl	$⊢ φ \to ⌊\frac{Z}{K^{N}}⌋ + 1 \in ℕ$
183		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
184	182 183	eleqtrdi	$⊢ φ \to ⌊\frac{Z}{K^{N}}⌋ + 1 \in ℤ_{\geq 1}$
185		fzss1	$⊢ ⌊\frac{Z}{K^{N}}⌋ + 1 \in ℤ_{\geq 1} \to (⌊\frac{Z}{K^{N}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) \subseteq (1 \dots ⌊\frac{Z}{Y}⌋)$
186	184 185	syl	$⊢ φ \to (⌊\frac{Z}{K^{N}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) \subseteq (1 \dots ⌊\frac{Z}{Y}⌋)$
187	186	sselda	$⊢ (φ \land n \in (⌊\frac{Z}{K^{N}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)) \to n \in (1 \dots ⌊\frac{Z}{Y}⌋)$
188	187 84	syldan	$⊢ (φ \land n \in (⌊\frac{Z}{K^{N}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)) \to ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ$
189	175 188	fsumrecl	$⊢ φ \to \sum_{n = ⌊\frac{Z}{K^{N}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ$
190		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
191	60 190	syl	$⊢ φ \to N \in (M \dots N)$
192		oveq1	$⊢ m = M \to m - M = M - M$
193	192	oveq2d	$⊢ m = M \to (U - E) (\frac{L E}{8}) \log Z (m - M) = (U - E) (\frac{L E}{8}) \log Z (M - M)$
194		oveq2	$⊢ m = M \to K^{m} = K^{M}$
195	194	oveq2d	$⊢ m = M \to \frac{Z}{K^{m}} = \frac{Z}{K^{M}}$
196	195	fveq2d	$⊢ m = M \to ⌊\frac{Z}{K^{m}}⌋ = ⌊\frac{Z}{K^{M}}⌋$
197	196	oveq1d	$⊢ m = M \to ⌊\frac{Z}{K^{m}}⌋ + 1 = ⌊\frac{Z}{K^{M}}⌋ + 1$
198	197	oveq1d	$⊢ m = M \to (⌊\frac{Z}{K^{m}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) = (⌊\frac{Z}{K^{M}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)$
199	198	sumeq1d	$⊢ m = M \to \sum_{n = ⌊\frac{Z}{K^{m}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n = \sum_{n = ⌊\frac{Z}{K^{M}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
200	193 199	breq12d	$⊢ m = M \to ((U - E) (\frac{L E}{8}) \log Z (m - M) \leq \sum_{n = ⌊\frac{Z}{K^{m}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \leftrightarrow (U - E) (\frac{L E}{8}) \log Z (M - M) \leq \sum_{n = ⌊\frac{Z}{K^{M}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n)$
201	200	imbi2d	$⊢ m = M \to ((φ \to (U - E) (\frac{L E}{8}) \log Z (m - M) \leq \sum_{n = ⌊\frac{Z}{K^{m}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n) \leftrightarrow (φ \to (U - E) (\frac{L E}{8}) \log Z (M - M) \leq \sum_{n = ⌊\frac{Z}{K^{M}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n))$
202		oveq1	$⊢ m = j \to m - M = j - M$
203	202	oveq2d	$⊢ m = j \to (U - E) (\frac{L E}{8}) \log Z (m - M) = (U - E) (\frac{L E}{8}) \log Z (j - M)$
204		oveq2	$⊢ m = j \to K^{m} = K^{j}$
205	204	oveq2d	$⊢ m = j \to \frac{Z}{K^{m}} = \frac{Z}{K^{j}}$
206	205	fveq2d	$⊢ m = j \to ⌊\frac{Z}{K^{m}}⌋ = ⌊\frac{Z}{K^{j}}⌋$
207	206	oveq1d	$⊢ m = j \to ⌊\frac{Z}{K^{m}}⌋ + 1 = ⌊\frac{Z}{K^{j}}⌋ + 1$
208	207	oveq1d	$⊢ m = j \to (⌊\frac{Z}{K^{m}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) = (⌊\frac{Z}{K^{j}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)$
209	208	sumeq1d	$⊢ m = j \to \sum_{n = ⌊\frac{Z}{K^{m}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n = \sum_{n = ⌊\frac{Z}{K^{j}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
210	203 209	breq12d	$⊢ m = j \to ((U - E) (\frac{L E}{8}) \log Z (m - M) \leq \sum_{n = ⌊\frac{Z}{K^{m}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \leftrightarrow (U - E) (\frac{L E}{8}) \log Z (j - M) \leq \sum_{n = ⌊\frac{Z}{K^{j}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n)$
211	210	imbi2d	$⊢ m = j \to ((φ \to (U - E) (\frac{L E}{8}) \log Z (m - M) \leq \sum_{n = ⌊\frac{Z}{K^{m}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n) \leftrightarrow (φ \to (U - E) (\frac{L E}{8}) \log Z (j - M) \leq \sum_{n = ⌊\frac{Z}{K^{j}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n))$
212		oveq1	$⊢ m = j + 1 \to m - M = j + 1 - M$
213	212	oveq2d	$⊢ m = j + 1 \to (U - E) (\frac{L E}{8}) \log Z (m - M) = (U - E) (\frac{L E}{8}) \log Z (j + 1 - M)$
214		oveq2	$⊢ m = j + 1 \to K^{m} = K^{j + 1}$
215	214	oveq2d	$⊢ m = j + 1 \to \frac{Z}{K^{m}} = \frac{Z}{K^{j + 1}}$
216	215	fveq2d	$⊢ m = j + 1 \to ⌊\frac{Z}{K^{m}}⌋ = ⌊\frac{Z}{K^{j + 1}}⌋$
217	216	oveq1d	$⊢ m = j + 1 \to ⌊\frac{Z}{K^{m}}⌋ + 1 = ⌊\frac{Z}{K^{j + 1}}⌋ + 1$
218	217	oveq1d	$⊢ m = j + 1 \to (⌊\frac{Z}{K^{m}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) = (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)$
219	218	sumeq1d	$⊢ m = j + 1 \to \sum_{n = ⌊\frac{Z}{K^{m}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n = \sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
220	213 219	breq12d	$⊢ m = j + 1 \to ((U - E) (\frac{L E}{8}) \log Z (m - M) \leq \sum_{n = ⌊\frac{Z}{K^{m}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \leftrightarrow (U - E) (\frac{L E}{8}) \log Z (j + 1 - M) \leq \sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n)$
221	220	imbi2d	$⊢ m = j + 1 \to ((φ \to (U - E) (\frac{L E}{8}) \log Z (m - M) \leq \sum_{n = ⌊\frac{Z}{K^{m}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n) \leftrightarrow (φ \to (U - E) (\frac{L E}{8}) \log Z (j + 1 - M) \leq \sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n))$
222		oveq1	$⊢ m = N \to m - M = N - M$
223	222	oveq2d	$⊢ m = N \to (U - E) (\frac{L E}{8}) \log Z (m - M) = (U - E) (\frac{L E}{8}) \log Z (N - M)$
224		oveq2	$⊢ m = N \to K^{m} = K^{N}$
225	224	oveq2d	$⊢ m = N \to \frac{Z}{K^{m}} = \frac{Z}{K^{N}}$
226	225	fveq2d	$⊢ m = N \to ⌊\frac{Z}{K^{m}}⌋ = ⌊\frac{Z}{K^{N}}⌋$
227	226	oveq1d	$⊢ m = N \to ⌊\frac{Z}{K^{m}}⌋ + 1 = ⌊\frac{Z}{K^{N}}⌋ + 1$
228	227	oveq1d	$⊢ m = N \to (⌊\frac{Z}{K^{m}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) = (⌊\frac{Z}{K^{N}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)$
229	228	sumeq1d	$⊢ m = N \to \sum_{n = ⌊\frac{Z}{K^{m}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n = \sum_{n = ⌊\frac{Z}{K^{N}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
230	223 229	breq12d	$⊢ m = N \to ((U - E) (\frac{L E}{8}) \log Z (m - M) \leq \sum_{n = ⌊\frac{Z}{K^{m}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \leftrightarrow (U - E) (\frac{L E}{8}) \log Z (N - M) \leq \sum_{n = ⌊\frac{Z}{K^{N}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n)$
231	230	imbi2d	$⊢ m = N \to ((φ \to (U - E) (\frac{L E}{8}) \log Z (m - M) \leq \sum_{n = ⌊\frac{Z}{K^{m}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n) \leftrightarrow (φ \to (U - E) (\frac{L E}{8}) \log Z (N - M) \leq \sum_{n = ⌊\frac{Z}{K^{N}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n))$
232	59	nncnd	$⊢ φ \to M \in ℂ$
233	232	subidd	$⊢ φ \to M - M = 0$
234	233	oveq2d	$⊢ φ \to (U - E) (\frac{L E}{8}) \log Z (M - M) = (U - E) (\frac{L E}{8}) \log Z \cdot 0$
235	56	rpcnd	$⊢ φ \to (U - E) (\frac{L E}{8}) \log Z \in ℂ$
236	235	mul01d	$⊢ φ \to (U - E) (\frac{L E}{8}) \log Z \cdot 0 = 0$
237	234 236	eqtrd	$⊢ φ \to (U - E) (\frac{L E}{8}) \log Z (M - M) = 0$
238		fzfid	$⊢ φ \to (⌊\frac{Z}{K^{M}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) \in Fin$
239	59	nnzd	$⊢ φ \to M \in ℤ$
240	87 239	rpexpcld	$⊢ φ \to K^{M} \in ℝ^{+}$
241	39 240	rpdivcld	$⊢ φ \to \frac{Z}{K^{M}} \in ℝ^{+}$
242	241	rprege0d	$⊢ φ \to (\frac{Z}{K^{M}} \in ℝ \land 0 \leq \frac{Z}{K^{M}})$
243		flge0nn0	$⊢ (\frac{Z}{K^{M}} \in ℝ \land 0 \leq \frac{Z}{K^{M}}) \to ⌊\frac{Z}{K^{M}}⌋ \in ℕ_{0}$
244		nn0p1nn	$⊢ ⌊\frac{Z}{K^{M}}⌋ \in ℕ_{0} \to ⌊\frac{Z}{K^{M}}⌋ + 1 \in ℕ$
245	242 243 244	3syl	$⊢ φ \to ⌊\frac{Z}{K^{M}}⌋ + 1 \in ℕ$
246	245 183	eleqtrdi	$⊢ φ \to ⌊\frac{Z}{K^{M}}⌋ + 1 \in ℤ_{\geq 1}$
247		fzss1	$⊢ ⌊\frac{Z}{K^{M}}⌋ + 1 \in ℤ_{\geq 1} \to (⌊\frac{Z}{K^{M}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) \subseteq (1 \dots ⌊\frac{Z}{Y}⌋)$
248	246 247	syl	$⊢ φ \to (⌊\frac{Z}{K^{M}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) \subseteq (1 \dots ⌊\frac{Z}{Y}⌋)$
249	248	sselda	$⊢ (φ \land n \in (⌊\frac{Z}{K^{M}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)) \to n \in (1 \dots ⌊\frac{Z}{Y}⌋)$
250	249 84	syldan	$⊢ (φ \land n \in (⌊\frac{Z}{K^{M}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)) \to ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ$
251		elfzle2	$⊢ n \in (1 \dots ⌊\frac{Z}{Y}⌋) \to n \leq ⌊\frac{Z}{Y}⌋$
252	251	adantl	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to n \leq ⌊\frac{Z}{Y}⌋$
253	11	simpld	$⊢ φ \to Y \in ℝ^{+}$
254	39 253	rpdivcld	$⊢ φ \to \frac{Z}{Y} \in ℝ^{+}$
255	254	rpred	$⊢ φ \to \frac{Z}{Y} \in ℝ$
256		elfzelz	$⊢ n \in (1 \dots ⌊\frac{Z}{Y}⌋) \to n \in ℤ$
257		flge	$⊢ (\frac{Z}{Y} \in ℝ \land n \in ℤ) \to (n \leq \frac{Z}{Y} \leftrightarrow n \leq ⌊\frac{Z}{Y}⌋)$
258	255 256 257	syl2an	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to (n \leq \frac{Z}{Y} \leftrightarrow n \leq ⌊\frac{Z}{Y}⌋)$
259	252 258	mpbird	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to n \leq \frac{Z}{Y}$
260	73 259	jca	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to (n \in ℕ \land n \leq \frac{Z}{Y})$
261	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$
262	260 261	syldan	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to 0 \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
263	249 262	syldan	$⊢ (φ \land n \in (⌊\frac{Z}{K^{M}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)) \to 0 \leq ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
264	238 250 263	fsumge0	$⊢ φ \to 0 \leq \sum_{n = ⌊\frac{Z}{K^{M}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
265	237 264	eqbrtrd	$⊢ φ \to (U - E) (\frac{L E}{8}) \log Z (M - M) \leq \sum_{n = ⌊\frac{Z}{K^{M}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
266	265	a1i	$⊢ N \in ℤ_{\geq M} \to (φ \to (U - E) (\frac{L E}{8}) \log Z (M - M) \leq \sum_{n = ⌊\frac{Z}{K^{M}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n)$
267		eqid	$⊢ (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{j}}⌋) = (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{j}}⌋)$
268	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 267	pntlemi	$⊢ (φ \land j \in (M ..^N)) \to (U - E) (\frac{L E}{8}) \log Z \leq \sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{K^{j}}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
269	56	adantr	$⊢ (φ \land j \in (M ..^N)) \to (U - E) (\frac{L E}{8}) \log Z \in ℝ^{+}$
270	269	rpred	$⊢ (φ \land j \in (M ..^N)) \to (U - E) (\frac{L E}{8}) \log Z \in ℝ$
271		elfzoelz	$⊢ j \in (M ..^N) \to j \in ℤ$
272	271	adantl	$⊢ (φ \land j \in (M ..^N)) \to j \in ℤ$
273	272	zred	$⊢ (φ \land j \in (M ..^N)) \to j \in ℝ$
274	59	adantr	$⊢ (φ \land j \in (M ..^N)) \to M \in ℕ$
275	274	nnred	$⊢ (φ \land j \in (M ..^N)) \to M \in ℝ$
276	273 275	resubcld	$⊢ (φ \land j \in (M ..^N)) \to j - M \in ℝ$
277	270 276	remulcld	$⊢ (φ \land j \in (M ..^N)) \to (U - E) (\frac{L E}{8}) \log Z (j - M) \in ℝ$
278		fzfid	$⊢ (φ \land j \in (M ..^N)) \to (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{j}}⌋) \in Fin$
279		ssun1	$⊢ (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{j}}⌋) \subseteq (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{j}}⌋) \cup (⌊\frac{Z}{K^{j}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)$
280	40	adantr	$⊢ (φ \land j \in (M ..^N)) \to Z \in ℝ$
281	87	adantr	$⊢ (φ \land j \in (M ..^N)) \to K \in ℝ^{+}$
282	272	peano2zd	$⊢ (φ \land j \in (M ..^N)) \to j + 1 \in ℤ$
283	281 282	rpexpcld	$⊢ (φ \land j \in (M ..^N)) \to K^{j + 1} \in ℝ^{+}$
284	280 283	rerpdivcld	$⊢ (φ \land j \in (M ..^N)) \to \frac{Z}{K^{j + 1}} \in ℝ$
285	281 272	rpexpcld	$⊢ (φ \land j \in (M ..^N)) \to K^{j} \in ℝ^{+}$
286	280 285	rerpdivcld	$⊢ (φ \land j \in (M ..^N)) \to \frac{Z}{K^{j}} \in ℝ$
287	88	adantr	$⊢ (φ \land j \in (M ..^N)) \to K \in ℝ$
288		1re	$⊢ 1 \in ℝ$
289		ltle	$⊢ (1 \in ℝ \land K \in ℝ) \to (1 < K \to 1 \leq K)$
290	288 88 289	sylancr	$⊢ φ \to (1 < K \to 1 \leq K)$
291	89 290	mpd	$⊢ φ \to 1 \leq K$
292	291	adantr	$⊢ (φ \land j \in (M ..^N)) \to 1 \leq K$
293		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
294		peano2uz	$⊢ j \in ℤ_{\geq j} \to j + 1 \in ℤ_{\geq j}$
295	272 293 294	3syl	$⊢ (φ \land j \in (M ..^N)) \to j + 1 \in ℤ_{\geq j}$
296	287 292 295	leexp2ad	$⊢ (φ \land j \in (M ..^N)) \to K^{j} \leq K^{j + 1}$
297	39	adantr	$⊢ (φ \land j \in (M ..^N)) \to Z \in ℝ^{+}$
298	285 283 297	lediv2d	$⊢ (φ \land j \in (M ..^N)) \to (K^{j} \leq K^{j + 1} \leftrightarrow \frac{Z}{K^{j + 1}} \leq \frac{Z}{K^{j}})$
299	296 298	mpbid	$⊢ (φ \land j \in (M ..^N)) \to \frac{Z}{K^{j + 1}} \leq \frac{Z}{K^{j}}$
300		flword2	$⊢ (\frac{Z}{K^{j + 1}} \in ℝ \land \frac{Z}{K^{j}} \in ℝ \land \frac{Z}{K^{j + 1}} \leq \frac{Z}{K^{j}}) \to ⌊\frac{Z}{K^{j}}⌋ \in ℤ_{\geq ⌊\frac{Z}{K^{j + 1}}⌋}$
301	284 286 299 300	syl3anc	$⊢ (φ \land j \in (M ..^N)) \to ⌊\frac{Z}{K^{j}}⌋ \in ℤ_{\geq ⌊\frac{Z}{K^{j + 1}}⌋}$
302		eluzp1p1	$⊢ ⌊\frac{Z}{K^{j}}⌋ \in ℤ_{\geq ⌊\frac{Z}{K^{j + 1}}⌋} \to ⌊\frac{Z}{K^{j}}⌋ + 1 \in ℤ_{\geq (⌊\frac{Z}{K^{j + 1}}⌋ + 1)}$
303	301 302	syl	$⊢ (φ \land j \in (M ..^N)) \to ⌊\frac{Z}{K^{j}}⌋ + 1 \in ℤ_{\geq (⌊\frac{Z}{K^{j + 1}}⌋ + 1)}$
304	286	flcld	$⊢ (φ \land j \in (M ..^N)) \to ⌊\frac{Z}{K^{j}}⌋ \in ℤ$
305	254	adantr	$⊢ (φ \land j \in (M ..^N)) \to \frac{Z}{Y} \in ℝ^{+}$
306	305	rpred	$⊢ (φ \land j \in (M ..^N)) \to \frac{Z}{Y} \in ℝ$
307	306	flcld	$⊢ (φ \land j \in (M ..^N)) \to ⌊\frac{Z}{Y}⌋ \in ℤ$
308	253	adantr	$⊢ (φ \land j \in (M ..^N)) \to Y \in ℝ^{+}$
309	308	rpred	$⊢ (φ \land j \in (M ..^N)) \to Y \in ℝ$
310	285	rpred	$⊢ (φ \land j \in (M ..^N)) \to K^{j} \in ℝ$
311	12	simpld	$⊢ φ \to X \in ℝ^{+}$
312	311	rpred	$⊢ φ \to X \in ℝ$
313	312	adantr	$⊢ (φ \land j \in (M ..^N)) \to X \in ℝ$
314	12	simprd	$⊢ φ \to Y < X$
315	314	adantr	$⊢ (φ \land j \in (M ..^N)) \to Y < X$
316		elfzofz	$⊢ j \in (M ..^N) \to j \in (M \dots N)$
317	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})$
318	316 317	sylan2	$⊢ (φ \land j \in (M ..^N)) \to (X < K^{j} \land K^{j} \leq \sqrt{Z})$
319	318	simpld	$⊢ (φ \land j \in (M ..^N)) \to X < K^{j}$
320	309 313 310 315 319	lttrd	$⊢ (φ \land j \in (M ..^N)) \to Y < K^{j}$
321	309 310 320	ltled	$⊢ (φ \land j \in (M ..^N)) \to Y \leq K^{j}$
322	308 285 297	lediv2d	$⊢ (φ \land j \in (M ..^N)) \to (Y \leq K^{j} \leftrightarrow \frac{Z}{K^{j}} \leq \frac{Z}{Y})$
323	321 322	mpbid	$⊢ (φ \land j \in (M ..^N)) \to \frac{Z}{K^{j}} \leq \frac{Z}{Y}$
324		flwordi	$⊢ (\frac{Z}{K^{j}} \in ℝ \land \frac{Z}{Y} \in ℝ \land \frac{Z}{K^{j}} \leq \frac{Z}{Y}) \to ⌊\frac{Z}{K^{j}}⌋ \leq ⌊\frac{Z}{Y}⌋$
325	286 306 323 324	syl3anc	$⊢ (φ \land j \in (M ..^N)) \to ⌊\frac{Z}{K^{j}}⌋ \leq ⌊\frac{Z}{Y}⌋$
326		eluz2	$⊢ ⌊\frac{Z}{Y}⌋ \in ℤ_{\geq ⌊\frac{Z}{K^{j}}⌋} \leftrightarrow (⌊\frac{Z}{K^{j}}⌋ \in ℤ \land ⌊\frac{Z}{Y}⌋ \in ℤ \land ⌊\frac{Z}{K^{j}}⌋ \leq ⌊\frac{Z}{Y}⌋)$
327	304 307 325 326	syl3anbrc	$⊢ (φ \land j \in (M ..^N)) \to ⌊\frac{Z}{Y}⌋ \in ℤ_{\geq ⌊\frac{Z}{K^{j}}⌋}$
328		fzsplit2	$⊢ (⌊\frac{Z}{K^{j}}⌋ + 1 \in ℤ_{\geq (⌊\frac{Z}{K^{j + 1}}⌋ + 1)} \land ⌊\frac{Z}{Y}⌋ \in ℤ_{\geq ⌊\frac{Z}{K^{j}}⌋}) \to (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) = (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{j}}⌋) \cup (⌊\frac{Z}{K^{j}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)$
329	303 327 328	syl2anc	$⊢ (φ \land j \in (M ..^N)) \to (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) = (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{j}}⌋) \cup (⌊\frac{Z}{K^{j}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)$
330	279 329	sseqtrrid	$⊢ (φ \land j \in (M ..^N)) \to (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{j}}⌋) \subseteq (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)$
331	297 283	rpdivcld	$⊢ (φ \land j \in (M ..^N)) \to \frac{Z}{K^{j + 1}} \in ℝ^{+}$
332	331	rprege0d	$⊢ (φ \land j \in (M ..^N)) \to (\frac{Z}{K^{j + 1}} \in ℝ \land 0 \leq \frac{Z}{K^{j + 1}})$
333		flge0nn0	$⊢ (\frac{Z}{K^{j + 1}} \in ℝ \land 0 \leq \frac{Z}{K^{j + 1}}) \to ⌊\frac{Z}{K^{j + 1}}⌋ \in ℕ_{0}$
334		nn0p1nn	$⊢ ⌊\frac{Z}{K^{j + 1}}⌋ \in ℕ_{0} \to ⌊\frac{Z}{K^{j + 1}}⌋ + 1 \in ℕ$
335	332 333 334	3syl	$⊢ (φ \land j \in (M ..^N)) \to ⌊\frac{Z}{K^{j + 1}}⌋ + 1 \in ℕ$
336	335 183	eleqtrdi	$⊢ (φ \land j \in (M ..^N)) \to ⌊\frac{Z}{K^{j + 1}}⌋ + 1 \in ℤ_{\geq 1}$
337		fzss1	$⊢ ⌊\frac{Z}{K^{j + 1}}⌋ + 1 \in ℤ_{\geq 1} \to (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) \subseteq (1 \dots ⌊\frac{Z}{Y}⌋)$
338	336 337	syl	$⊢ (φ \land j \in (M ..^N)) \to (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) \subseteq (1 \dots ⌊\frac{Z}{Y}⌋)$
339	330 338	sstrd	$⊢ (φ \land j \in (M ..^N)) \to (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{j}}⌋) \subseteq (1 \dots ⌊\frac{Z}{Y}⌋)$
340	339	sselda	$⊢ ((φ \land j \in (M ..^N)) \land n \in (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{j}}⌋)) \to n \in (1 \dots ⌊\frac{Z}{Y}⌋)$
341	84	adantlr	$⊢ ((φ \land j \in (M ..^N)) \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ$
342	340 341	syldan	$⊢ ((φ \land j \in (M ..^N)) \land n \in (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{j}}⌋)) \to ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ$
343	278 342	fsumrecl	$⊢ (φ \land j \in (M ..^N)) \to \sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{K^{j}}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ$
344		fzfid	$⊢ (φ \land j \in (M ..^N)) \to (⌊\frac{Z}{K^{j}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) \in Fin$
345		ssun2	$⊢ (⌊\frac{Z}{K^{j}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) \subseteq (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{j}}⌋) \cup (⌊\frac{Z}{K^{j}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)$
346	345 329	sseqtrrid	$⊢ (φ \land j \in (M ..^N)) \to (⌊\frac{Z}{K^{j}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) \subseteq (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)$
347	346 338	sstrd	$⊢ (φ \land j \in (M ..^N)) \to (⌊\frac{Z}{K^{j}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) \subseteq (1 \dots ⌊\frac{Z}{Y}⌋)$
348	347	sselda	$⊢ ((φ \land j \in (M ..^N)) \land n \in (⌊\frac{Z}{K^{j}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)) \to n \in (1 \dots ⌊\frac{Z}{Y}⌋)$
349	348 341	syldan	$⊢ ((φ \land j \in (M ..^N)) \land n \in (⌊\frac{Z}{K^{j}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)) \to ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ$
350	344 349	fsumrecl	$⊢ (φ \land j \in (M ..^N)) \to \sum_{n = ⌊\frac{Z}{K^{j}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ$
351		le2add	$⊢ (((U - E) (\frac{L E}{8}) \log Z \in ℝ \land (U - E) (\frac{L E}{8}) \log Z (j - M) \in ℝ) \land (\sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{K^{j}}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ \land \sum_{n = ⌊\frac{Z}{K^{j}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ)) \to (((U - E) (\frac{L E}{8}) \log Z \leq \sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{K^{j}}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \land (U - E) (\frac{L E}{8}) \log Z (j - M) \leq \sum_{n = ⌊\frac{Z}{K^{j}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n) \to (U - E) (\frac{L E}{8}) \log Z + (U - E) (\frac{L E}{8}) \log Z (j - M) \leq \sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{K^{j}}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n + \sum_{n = ⌊\frac{Z}{K^{j}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n)$
352	270 277 343 350 351	syl22anc	$⊢ (φ \land j \in (M ..^N)) \to (((U - E) (\frac{L E}{8}) \log Z \leq \sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{K^{j}}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \land (U - E) (\frac{L E}{8}) \log Z (j - M) \leq \sum_{n = ⌊\frac{Z}{K^{j}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n) \to (U - E) (\frac{L E}{8}) \log Z + (U - E) (\frac{L E}{8}) \log Z (j - M) \leq \sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{K^{j}}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n + \sum_{n = ⌊\frac{Z}{K^{j}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n)$
353	268 352	mpand	$⊢ (φ \land j \in (M ..^N)) \to ((U - E) (\frac{L E}{8}) \log Z (j - M) \leq \sum_{n = ⌊\frac{Z}{K^{j}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \to (U - E) (\frac{L E}{8}) \log Z + (U - E) (\frac{L E}{8}) \log Z (j - M) \leq \sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{K^{j}}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n + \sum_{n = ⌊\frac{Z}{K^{j}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n)$
354	235	adantr	$⊢ (φ \land j \in (M ..^N)) \to (U - E) (\frac{L E}{8}) \log Z \in ℂ$
355		1cnd	$⊢ (φ \land j \in (M ..^N)) \to 1 \in ℂ$
356	272	zcnd	$⊢ (φ \land j \in (M ..^N)) \to j \in ℂ$
357	232	adantr	$⊢ (φ \land j \in (M ..^N)) \to M \in ℂ$
358	356 357	subcld	$⊢ (φ \land j \in (M ..^N)) \to j - M \in ℂ$
359	354 355 358	adddid	$⊢ (φ \land j \in (M ..^N)) \to (U - E) (\frac{L E}{8}) \log Z (1 + j - M) = (U - E) (\frac{L E}{8}) \log Z \cdot 1 + (U - E) (\frac{L E}{8}) \log Z (j - M)$
360	355 358	addcomd	$⊢ (φ \land j \in (M ..^N)) \to 1 + j - M = j - M + 1$
361	356 355 357	addsubd	$⊢ (φ \land j \in (M ..^N)) \to j + 1 - M = j - M + 1$
362	360 361	eqtr4d	$⊢ (φ \land j \in (M ..^N)) \to 1 + j - M = j + 1 - M$
363	362	oveq2d	$⊢ (φ \land j \in (M ..^N)) \to (U - E) (\frac{L E}{8}) \log Z (1 + j - M) = (U - E) (\frac{L E}{8}) \log Z (j + 1 - M)$
364	354	mulid1d	$⊢ (φ \land j \in (M ..^N)) \to (U - E) (\frac{L E}{8}) \log Z \cdot 1 = (U - E) (\frac{L E}{8}) \log Z$
365	364	oveq1d	$⊢ (φ \land j \in (M ..^N)) \to (U - E) (\frac{L E}{8}) \log Z \cdot 1 + (U - E) (\frac{L E}{8}) \log Z (j - M) = (U - E) (\frac{L E}{8}) \log Z + (U - E) (\frac{L E}{8}) \log Z (j - M)$
366	359 363 365	3eqtr3d	$⊢ (φ \land j \in (M ..^N)) \to (U - E) (\frac{L E}{8}) \log Z (j + 1 - M) = (U - E) (\frac{L E}{8}) \log Z + (U - E) (\frac{L E}{8}) \log Z (j - M)$
367		reflcl	$⊢ \frac{Z}{K^{j}} \in ℝ \to ⌊\frac{Z}{K^{j}}⌋ \in ℝ$
368	286 367	syl	$⊢ (φ \land j \in (M ..^N)) \to ⌊\frac{Z}{K^{j}}⌋ \in ℝ$
369	368	ltp1d	$⊢ (φ \land j \in (M ..^N)) \to ⌊\frac{Z}{K^{j}}⌋ < ⌊\frac{Z}{K^{j}}⌋ + 1$
370		fzdisj	$⊢ ⌊\frac{Z}{K^{j}}⌋ < ⌊\frac{Z}{K^{j}}⌋ + 1 \to (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{j}}⌋) \cap (⌊\frac{Z}{K^{j}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) = \emptyset$
371	369 370	syl	$⊢ (φ \land j \in (M ..^N)) \to (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{j}}⌋) \cap (⌊\frac{Z}{K^{j}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) = \emptyset$
372		fzfid	$⊢ (φ \land j \in (M ..^N)) \to (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋) \in Fin$
373	338	sselda	$⊢ ((φ \land j \in (M ..^N)) \land n \in (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)) \to n \in (1 \dots ⌊\frac{Z}{Y}⌋)$
374	373 341	syldan	$⊢ ((φ \land j \in (M ..^N)) \land n \in (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)) \to ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ$
375	374	recnd	$⊢ ((φ \land j \in (M ..^N)) \land n \in (⌊\frac{Z}{K^{j + 1}}⌋ + 1 \dots ⌊\frac{Z}{Y}⌋)) \to ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℂ$
376	371 329 372 375	fsumsplit	$⊢ (φ \land j \in (M ..^N)) \to \sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n = \sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{K^{j}}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n + \sum_{n = ⌊\frac{Z}{K^{j}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
377	366 376	breq12d	$⊢ (φ \land j \in (M ..^N)) \to ((U - E) (\frac{L E}{8}) \log Z (j + 1 - M) \leq \sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \leftrightarrow (U - E) (\frac{L E}{8}) \log Z + (U - E) (\frac{L E}{8}) \log Z (j - M) \leq \sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{K^{j}}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n + \sum_{n = ⌊\frac{Z}{K^{j}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n)$
378	353 377	sylibrd	$⊢ (φ \land j \in (M ..^N)) \to ((U - E) (\frac{L E}{8}) \log Z (j - M) \leq \sum_{n = ⌊\frac{Z}{K^{j}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \to (U - E) (\frac{L E}{8}) \log Z (j + 1 - M) \leq \sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n)$
379	378	expcom	$⊢ j \in (M ..^N) \to (φ \to ((U - E) (\frac{L E}{8}) \log Z (j - M) \leq \sum_{n = ⌊\frac{Z}{K^{j}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \to (U - E) (\frac{L E}{8}) \log Z (j + 1 - M) \leq \sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n))$
380	379	a2d	$⊢ j \in (M ..^N) \to ((φ \to (U - E) (\frac{L E}{8}) \log Z (j - M) \leq \sum_{n = ⌊\frac{Z}{K^{j}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n) \to (φ \to (U - E) (\frac{L E}{8}) \log Z (j + 1 - M) \leq \sum_{n = ⌊\frac{Z}{K^{j + 1}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n))$
381	201 211 221 231 266 380	fzind2	$⊢ N \in (M \dots N) \to (φ \to (U - E) (\frac{L E}{8}) \log Z (N - M) \leq \sum_{n = ⌊\frac{Z}{K^{N}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n)$
382	191 381	mpcom	$⊢ φ \to (U - E) (\frac{L E}{8}) \log Z (N - M) \leq \sum_{n = ⌊\frac{Z}{K^{N}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
383	67 84 262 186	fsumless	$⊢ φ \to \sum_{n = ⌊\frac{Z}{K^{N}}⌋ + 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \leq \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
384	66 189 85 382 383	letrd	$⊢ φ \to (U - E) (\frac{L E}{8}) \log Z (N - M) \leq \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
385	48 66 85 174 384	letrd	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \leq \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$

Metamath Proof Explorer

Theorem pntlemf

Proof