pntleme

Description: Lemma for pnt . Package up pntlemo in quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016)

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

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		pntleme.U	$⊢ φ \to \forall z \in [Y, +∞) \|\frac{R (z)}{z}\| \leq U$
16		pntleme.K	$⊢ φ \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)$
17		pntleme.C	$⊢ φ \to \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{i = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{i})\| \log i}{z} \leq C$
18	1 2 3 4 5 6 7 8 9 10 11 12 13 14	pntlema	$⊢ φ \to W \in ℝ^{+}$
19	2	adantr	$⊢ (φ \land v \in [W, +∞)) \to A \in ℝ^{+}$
20	3	adantr	$⊢ (φ \land v \in [W, +∞)) \to B \in ℝ^{+}$
21	4	adantr	$⊢ (φ \land v \in [W, +∞)) \to L \in (0, 1)$
22	7	adantr	$⊢ (φ \land v \in [W, +∞)) \to U \in ℝ^{+}$
23	8	adantr	$⊢ (φ \land v \in [W, +∞)) \to U \leq A$
24	11	adantr	$⊢ (φ \land v \in [W, +∞)) \to (Y \in ℝ^{+} \land 1 \leq Y)$
25	12	adantr	$⊢ (φ \land v \in [W, +∞)) \to (X \in ℝ^{+} \land Y < X)$
26	13	adantr	$⊢ (φ \land v \in [W, +∞)) \to C \in ℝ^{+}$
27		simpr	$⊢ (φ \land v \in [W, +∞)) \to v \in [W, +∞)$
28		eqid	$⊢ ⌊\frac{\log X}{\log K}⌋ + 1 = ⌊\frac{\log X}{\log K}⌋ + 1$
29		eqid	$⊢ ⌊\frac{\frac{\log v}{\log K}}{2}⌋ = ⌊\frac{\frac{\log v}{\log K}}{2}⌋$
30	15	adantr	$⊢ (φ \land v \in [W, +∞)) \to \forall z \in [Y, +∞) \|\frac{R (z)}{z}\| \leq U$
31		oveq1	$⊢ k = K \to k y = K y$
32	31	breq2d	$⊢ k = K \to ((1 + L E) z < k y \leftrightarrow (1 + L E) z < K y)$
33	32	anbi2d	$⊢ k = K \to ((y < z \land (1 + L E) z < k y) \leftrightarrow (y < z \land (1 + L E) z < K y))$
34	33	anbi1d	$⊢ k = K \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))$
35	34	rexbidv	$⊢ k = K \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))$
36	35	ralbidv	$⊢ k = 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) \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))$
37	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 ℝ^{+}))$
38	37	simp2d	$⊢ φ \to K \in ℝ^{+}$
39	38	rpxrd	$⊢ φ \to K \in ℝ^{*}$
40		pnfxr	$⊢ +∞ \in ℝ^{*}$
41	40	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
42	38	rpred	$⊢ φ \to K \in ℝ$
43	42	ltpnfd	$⊢ φ \to K < +∞$
44		lbico1	$⊢ (K \in ℝ^{} \land +∞ \in ℝ^{} \land K < +∞) \to K \in [K, +∞)$
45	39 41 43 44	syl3anc	$⊢ φ \to K \in [K, +∞)$
46	36 16 45	rspcdva	$⊢ φ \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)$
47	46	adantr	$⊢ (φ \land v \in [W, +∞)) \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)$
48	17	adantr	$⊢ (φ \land v \in [W, +∞)) \to \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{i = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{i})\| \log i}{z} \leq C$
49	1 19 20 21 5 6 22 23 9 10 24 25 26 14 27 28 29 30 47 48	pntlemo	$⊢ (φ \land v \in [W, +∞)) \to \|\frac{R (v)}{v}\| \leq U - F U^{3}$
50	49	ralrimiva	$⊢ φ \to \forall v \in [W, +∞) \|\frac{R (v)}{v}\| \leq U - F U^{3}$
51		oveq1	$⊢ w = W \to [w, +∞) = [W, +∞)$
52	51	raleqdv	$⊢ w = W \to (\forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq U - F U^{3} \leftrightarrow \forall v \in [W, +∞) \|\frac{R (v)}{v}\| \leq U - F U^{3})$
53	52	rspcev	$⊢ (W \in ℝ^{+} \land \forall v \in [W, +∞) \|\frac{R (v)}{v}\| \leq U - F U^{3}) \to \exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq U - F U^{3}$
54	18 50 53	syl2anc	$⊢ φ \to \exists w \in ℝ^{+} \forall v \in [w, +∞) \|\frac{R (v)}{v}\| \leq U - F U^{3}$

Metamath Proof Explorer

Theorem pntleme

Proof