pntlemp

Description: Lemma for pnt . Wrapping up more quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016)

	Ref	Expression
Hypotheses	pntlem3.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	pntlem3.a	$⊢ φ \to A \in ℝ^{+}$
	pntlem3.A	$⊢ φ \to \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq A$
	pntlemp.b	$⊢ φ \to B \in ℝ^{+}$
	pntlemp.l	$⊢ φ \to L \in (0, 1)$
	pntlemp.d	$⊢ D = A + 1$
	pntlemp.f	$⊢ F = (1 - (\frac{1}{D})) (\frac{\frac{L}{32 B}}{D^{2}})$
	pntlemp.K	$⊢ φ \to \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{B}{e}}, +∞) \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)$
	pntlemp.u	$⊢ φ \to U \in ℝ^{+}$
	pntlemp.u2	$⊢ φ \to U \leq A$
	pntlemp.e	$⊢ E = \frac{U}{D}$
	pntlemp.k	$⊢ K = e^{\frac{B}{E}}$
	pntlemp.y	$⊢ φ \to (Y \in ℝ^{+} \land 1 \leq Y)$
	pntlemp.U	$⊢ φ \to \forall z \in [Y, +∞) \|\frac{R (z)}{z}\| \leq U$
Assertion	pntlemp	$⊢ φ \to \exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq U - F U^{3}$

Proof

Step	Hyp	Ref	Expression
1		pntlem3.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2		pntlem3.a	$⊢ φ \to A \in ℝ^{+}$
3		pntlem3.A	$⊢ φ \to \forall x \in ℝ^{+} \|\frac{R (x)}{x}\| \leq A$
4		pntlemp.b	$⊢ φ \to B \in ℝ^{+}$
5		pntlemp.l	$⊢ φ \to L \in (0, 1)$
6		pntlemp.d	$⊢ D = A + 1$
7		pntlemp.f	$⊢ F = (1 - (\frac{1}{D})) (\frac{\frac{L}{32 B}}{D^{2}})$
8		pntlemp.K	$⊢ φ \to \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{B}{e}}, +∞) \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)$
9		pntlemp.u	$⊢ φ \to U \in ℝ^{+}$
10		pntlemp.u2	$⊢ φ \to U \leq A$
11		pntlemp.e	$⊢ E = \frac{U}{D}$
12		pntlemp.k	$⊢ K = e^{\frac{B}{E}}$
13		pntlemp.y	$⊢ φ \to (Y \in ℝ^{+} \land 1 \leq Y)$
14		pntlemp.U	$⊢ φ \to \forall z \in [Y, +∞) \|\frac{R (z)}{z}\| \leq U$
15		oveq2	$⊢ e = E \to \frac{B}{e} = \frac{B}{E}$
16	15	fveq2d	$⊢ e = E \to e^{\frac{B}{e}} = e^{\frac{B}{E}}$
17	16 12	eqtr4di	$⊢ e = E \to e^{\frac{B}{e}} = K$
18	17	oveq1d	$⊢ e = E \to [e^{\frac{B}{e}}, +∞) = [K, +∞)$
19		oveq2	$⊢ e = E \to L e = L E$
20	19	oveq2d	$⊢ e = E \to 1 + L e = 1 + L E$
21	20	oveq1d	$⊢ e = E \to (1 + L e) z = (1 + L E) z$
22	21	breq1d	$⊢ e = E \to ((1 + L e) z < k y \leftrightarrow (1 + L E) z < k y)$
23	22	anbi2d	$⊢ e = E \to ((y < z \land (1 + L e) z < k y) \leftrightarrow (y < z \land (1 + L E) z < k y))$
24	21	oveq2d	$⊢ e = E \to [z, (1 + L e) z] = [z, (1 + L E) z]$
25		breq2	$⊢ e = E \to (\|\frac{R (u)}{u}\| \leq e \leftrightarrow \|\frac{R (u)}{u}\| \leq E)$
26	24 25	raleqbidv	$⊢ e = E \to (\forall u \in [z, (1 + L e) z] \|\frac{R (u)}{u}\| \leq e \leftrightarrow \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E)$
27	23 26	anbi12d	$⊢ e = E \to (((y < z \land (1 + L e) z < k y) \land \forall u \in [z, (1 + L e) z] \|\frac{R (u)}{u}\| \leq e) \leftrightarrow ((y < z \land (1 + L E) z < k y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E))$
28	27	rexbidv	$⊢ e = E \to (\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) \leftrightarrow \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))$
29	28	ralbidv	$⊢ e = E \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) \leftrightarrow \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))$
30	18 29	raleqbidv	$⊢ e = E \to (\forall k \in [e^{\frac{B}{e}}, +∞) \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) \leftrightarrow \forall k \in [K, +∞) \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))$
31	30	rexbidv	$⊢ e = E \to (\exists x \in ℝ^{+} \forall k \in [e^{\frac{B}{e}}, +∞) \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) \leftrightarrow \exists x \in ℝ^{+} \forall k \in [K, +∞) \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))$
32		oveq1	$⊢ x = t \to (x, +∞) = (t, +∞)$
33	32	raleqdv	$⊢ x = t \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) \leftrightarrow \forall y \in (t, +∞) \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))$
34	33	ralbidv	$⊢ x = t \to (\forall k \in [K, +∞) \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) \leftrightarrow \forall k \in [K, +∞) \forall y \in (t, +∞) \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))$
35	34	cbvrexvw	$⊢ \exists x \in ℝ^{+} \forall k \in [K, +∞) \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) \leftrightarrow \exists t \in ℝ^{+} \forall k \in [K, +∞) \forall y \in (t, +∞) \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)$
36	31 35	bitrdi	$⊢ e = E \to (\exists x \in ℝ^{+} \forall k \in [e^{\frac{B}{e}}, +∞) \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) \leftrightarrow \exists t \in ℝ^{+} \forall k \in [K, +∞) \forall y \in (t, +∞) \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))$
37	1 2 4 5 6 7 9 10 11 12	pntlemc	$⊢ φ \to (E \in ℝ^{+} \land K \in ℝ^{+} \land (E \in (0, 1) \land 1 < K \land U - E \in ℝ^{+}))$
38	37	simp3d	$⊢ φ \to (E \in (0, 1) \land 1 < K \land U - E \in ℝ^{+})$
39	38	simp1d	$⊢ φ \to E \in (0, 1)$
40	36 8 39	rspcdva	$⊢ φ \to \exists t \in ℝ^{+} \forall k \in [K, +∞) \forall y \in (t, +∞) \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)$
41	13	simpld	$⊢ φ \to Y \in ℝ^{+}$
42	41	rpred	$⊢ φ \to Y \in ℝ$
43	13	simprd	$⊢ φ \to 1 \leq Y$
44	1	pntrlog2bnd	$⊢ (Y \in ℝ \land 1 \leq Y) \to \exists c \in ℝ^{+} \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c$
45	42 43 44	syl2anc	$⊢ φ \to \exists c \in ℝ^{+} \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c$
46		reeanv	$⊢ \exists t \in ℝ^{+} \exists c \in ℝ^{+} (\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c) \leftrightarrow (\exists t \in ℝ^{+} \forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \exists c \in ℝ^{+} \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c)$
47	2	adantr	$⊢ (φ \land ((t \in ℝ^{+} \land c \in ℝ^{+}) \land (\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c))) \to A \in ℝ^{+}$
48	4	adantr	$⊢ (φ \land ((t \in ℝ^{+} \land c \in ℝ^{+}) \land (\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c))) \to B \in ℝ^{+}$
49	5	adantr	$⊢ (φ \land ((t \in ℝ^{+} \land c \in ℝ^{+}) \land (\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c))) \to L \in (0, 1)$
50	9	adantr	$⊢ (φ \land ((t \in ℝ^{+} \land c \in ℝ^{+}) \land (\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c))) \to U \in ℝ^{+}$
51	10	adantr	$⊢ (φ \land ((t \in ℝ^{+} \land c \in ℝ^{+}) \land (\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c))) \to U \leq A$
52	13	adantr	$⊢ (φ \land ((t \in ℝ^{+} \land c \in ℝ^{+}) \land (\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c))) \to (Y \in ℝ^{+} \land 1 \leq Y)$
53		simpl	$⊢ (t \in ℝ^{+} \land c \in ℝ^{+}) \to t \in ℝ^{+}$
54		rpaddcl	$⊢ (Y \in ℝ^{+} \land t \in ℝ^{+}) \to Y + t \in ℝ^{+}$
55	41 53 54	syl2an	$⊢ (φ \land (t \in ℝ^{+} \land c \in ℝ^{+})) \to Y + t \in ℝ^{+}$
56		ltaddrp	$⊢ (Y \in ℝ \land t \in ℝ^{+}) \to Y < Y + t$
57	42 53 56	syl2an	$⊢ (φ \land (t \in ℝ^{+} \land c \in ℝ^{+})) \to Y < Y + t$
58	55 57	jca	$⊢ (φ \land (t \in ℝ^{+} \land c \in ℝ^{+})) \to (Y + t \in ℝ^{+} \land Y < Y + t)$
59	58	adantrr	$⊢ (φ \land ((t \in ℝ^{+} \land c \in ℝ^{+}) \land (\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c))) \to (Y + t \in ℝ^{+} \land Y < Y + t)$
60		simprlr	$⊢ (φ \land ((t \in ℝ^{+} \land c \in ℝ^{+}) \land (\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c))) \to c \in ℝ^{+}$
61		eqid	$⊢ {(Y + (\frac{4}{L E}))}^{2} + {(Y + t) K^{2}}^{4} + e^{(\frac{32 B}{(U - E) L E^{2}}) (U \cdot 3 + c)} = {(Y + (\frac{4}{L E}))}^{2} + {(Y + t) K^{2}}^{4} + e^{(\frac{32 B}{(U - E) L E^{2}}) (U \cdot 3 + c)}$
62	14	adantr	$⊢ (φ \land ((t \in ℝ^{+} \land c \in ℝ^{+}) \land (\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c))) \to \forall z \in [Y, +∞) \|\frac{R (z)}{z}\| \leq U$
63		rpxr	$⊢ t \in ℝ^{+} \to t \in ℝ^{*}$
64	63	ad2antrl	$⊢ (φ \land (t \in ℝ^{+} \land c \in ℝ^{+})) \to t \in ℝ^{*}$
65		rpre	$⊢ t \in ℝ^{+} \to t \in ℝ$
66	65	ad2antrl	$⊢ (φ \land (t \in ℝ^{+} \land c \in ℝ^{+})) \to t \in ℝ$
67	55	rpred	$⊢ (φ \land (t \in ℝ^{+} \land c \in ℝ^{+})) \to Y + t \in ℝ$
68	41	adantr	$⊢ (φ \land (t \in ℝ^{+} \land c \in ℝ^{+})) \to Y \in ℝ^{+}$
69	66 68	ltaddrp2d	$⊢ (φ \land (t \in ℝ^{+} \land c \in ℝ^{+})) \to t < Y + t$
70	66 67 69	ltled	$⊢ (φ \land (t \in ℝ^{+} \land c \in ℝ^{+})) \to t \leq Y + t$
71		iooss1	$⊢ (t \in ℝ^{*} \land t \leq Y + t) \to (Y + t, +∞) \subseteq (t, +∞)$
72	64 70 71	syl2anc	$⊢ (φ \land (t \in ℝ^{+} \land c \in ℝ^{+})) \to (Y + t, +∞) \subseteq (t, +∞)$
73	72	adantrr	$⊢ (φ \land ((t \in ℝ^{+} \land c \in ℝ^{+}) \land (\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c))) \to (Y + t, +∞) \subseteq (t, +∞)$
74		simprrl	$⊢ (φ \land ((t \in ℝ^{+} \land c \in ℝ^{+}) \land (\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c))) \to \forall k \in [K, +∞) \forall y \in (t, +∞) \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)$
75		ssralv	$⊢ (Y + t, +∞) \subseteq (t, +∞) \to (\forall y \in (t, +∞) \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) \to \forall y \in (Y + t, +∞) \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))$
76	75	ralimdv	$⊢ (Y + t, +∞) \subseteq (t, +∞) \to (\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \to \forall k \in [K, +∞) \forall y \in (Y + t, +∞) \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))$
77	73 74 76	sylc	$⊢ (φ \land ((t \in ℝ^{+} \land c \in ℝ^{+}) \land (\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c))) \to \forall k \in [K, +∞) \forall y \in (Y + t, +∞) \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)$
78		simprrr	$⊢ (φ \land ((t \in ℝ^{+} \land c \in ℝ^{+}) \land (\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c))) \to \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c$
79	1 47 48 49 6 7 50 51 11 12 52 59 60 61 62 77 78	pntleme	$⊢ (φ \land ((t \in ℝ^{+} \land c \in ℝ^{+}) \land (\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c))) \to \exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq U - F U^{3}$
80	79	expr	$⊢ (φ \land (t \in ℝ^{+} \land c \in ℝ^{+})) \to ((\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c) \to \exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq U - F U^{3})$
81	80	rexlimdvva	$⊢ φ \to (\exists t \in ℝ^{+} \exists c \in ℝ^{+} (\forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c) \to \exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq U - F U^{3})$
82	46 81	syl5bir	$⊢ φ \to ((\exists t \in ℝ^{+} \forall k \in [K, +∞) \forall y \in (t, +∞) \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) \land \exists c \in ℝ^{+} \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n}{z} \leq c) \to \exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq U - F U^{3})$
83	40 45 82	mp2and	$⊢ φ \to \exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq U - F U^{3}$

Metamath Proof Explorer

Theorem pntlemp

Proof