pntlemi

Description: Lemma for pnt . Eliminate some assumptions from pntlemj . (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}}⌋)$
Assertion	pntlemi	$⊢ (φ \land J \in (M ..^N)) \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		breq2	$⊢ z = x \to (y < z \leftrightarrow y < x)$
22		oveq2	$⊢ z = x \to (1 + L E) z = (1 + L E) x$
23	22	breq1d	$⊢ z = x \to ((1 + L E) z < K y \leftrightarrow (1 + L E) x < K y)$
24	21 23	anbi12d	$⊢ z = x \to ((y < z \land (1 + L E) z < K y) \leftrightarrow (y < x \land (1 + L E) x < K y))$
25		id	$⊢ z = x \to z = x$
26	25 22	oveq12d	$⊢ z = x \to [z, (1 + L E) z] = [x, (1 + L E) x]$
27	26	raleqdv	$⊢ z = x \to (\forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E \leftrightarrow \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E)$
28	24 27	anbi12d	$⊢ z = x \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 < x \land (1 + L E) x < K y) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))$
29	28	cbvrexvw	$⊢ \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 ℝ^{+} ((y < x \land (1 + L E) x < K y) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E)$
30		breq1	$⊢ y = K^{J} \to (y < x \leftrightarrow K^{J} < x)$
31		oveq2	$⊢ y = K^{J} \to K y = K K^{J}$
32	31	breq2d	$⊢ y = K^{J} \to ((1 + L E) x < K y \leftrightarrow (1 + L E) x < K K^{J})$
33	30 32	anbi12d	$⊢ y = K^{J} \to ((y < x \land (1 + L E) x < K y) \leftrightarrow (K^{J} < x \land (1 + L E) x < K K^{J}))$
34	33	anbi1d	$⊢ y = K^{J} \to (((y < x \land (1 + L E) x < K y) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E) \leftrightarrow ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))$
35	34	rexbidv	$⊢ y = K^{J} \to (\exists x \in ℝ^{+} ((y < x \land (1 + L E) x < K y) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E) \leftrightarrow \exists x \in ℝ^{+} ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))$
36	29 35	bitrid	$⊢ y = K^{J} \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 x \in ℝ^{+} ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))$
37	19	adantr	$⊢ (φ \land J \in (M ..^N)) \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)$
38	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 ℝ^{+}))$
39	38	simp2d	$⊢ φ \to K \in ℝ^{+}$
40		elfzoelz	$⊢ J \in (M ..^N) \to J \in ℤ$
41		rpexpcl	$⊢ (K \in ℝ^{+} \land J \in ℤ) \to K^{J} \in ℝ^{+}$
42	39 40 41	syl2an	$⊢ (φ \land J \in (M ..^N)) \to K^{J} \in ℝ^{+}$
43	42	rpred	$⊢ (φ \land J \in (M ..^N)) \to K^{J} \in ℝ$
44		elfzofz	$⊢ J \in (M ..^N) \to J \in (M \dots N)$
45	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})$
46	44 45	sylan2	$⊢ (φ \land J \in (M ..^N)) \to (X < K^{J} \land K^{J} \leq \sqrt{Z})$
47	46	simpld	$⊢ (φ \land J \in (M ..^N)) \to X < K^{J}$
48	12	simpld	$⊢ φ \to X \in ℝ^{+}$
49	48	adantr	$⊢ (φ \land J \in (M ..^N)) \to X \in ℝ^{+}$
50		rpxr	$⊢ X \in ℝ^{+} \to X \in ℝ^{*}$
51		elioopnf	$⊢ X \in ℝ^{*} \to (K^{J} \in (X, +∞) \leftrightarrow (K^{J} \in ℝ \land X < K^{J}))$
52	49 50 51	3syl	$⊢ (φ \land J \in (M ..^N)) \to (K^{J} \in (X, +∞) \leftrightarrow (K^{J} \in ℝ \land X < K^{J}))$
53	43 47 52	mpbir2and	$⊢ (φ \land J \in (M ..^N)) \to K^{J} \in (X, +∞)$
54	36 37 53	rspcdva	$⊢ (φ \land J \in (M ..^N)) \to \exists x \in ℝ^{+} ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E)$
55	2	ad2antrr	$⊢ ((φ \land J \in (M ..^N)) \land (x \in ℝ^{+} \land ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))) \to A \in ℝ^{+}$
56	3	ad2antrr	$⊢ ((φ \land J \in (M ..^N)) \land (x \in ℝ^{+} \land ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))) \to B \in ℝ^{+}$
57	4	ad2antrr	$⊢ ((φ \land J \in (M ..^N)) \land (x \in ℝ^{+} \land ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))) \to L \in (0, 1)$
58	7	ad2antrr	$⊢ ((φ \land J \in (M ..^N)) \land (x \in ℝ^{+} \land ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))) \to U \in ℝ^{+}$
59	8	ad2antrr	$⊢ ((φ \land J \in (M ..^N)) \land (x \in ℝ^{+} \land ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))) \to U \leq A$
60	11	ad2antrr	$⊢ ((φ \land J \in (M ..^N)) \land (x \in ℝ^{+} \land ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))) \to (Y \in ℝ^{+} \land 1 \leq Y)$
61	12	ad2antrr	$⊢ ((φ \land J \in (M ..^N)) \land (x \in ℝ^{+} \land ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))) \to (X \in ℝ^{+} \land Y < X)$
62	13	ad2antrr	$⊢ ((φ \land J \in (M ..^N)) \land (x \in ℝ^{+} \land ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))) \to C \in ℝ^{+}$
63	15	ad2antrr	$⊢ ((φ \land J \in (M ..^N)) \land (x \in ℝ^{+} \land ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))) \to Z \in [W, +∞)$
64	18	ad2antrr	$⊢ ((φ \land J \in (M ..^N)) \land (x \in ℝ^{+} \land ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))) \to \forall z \in [Y, +∞) \|\frac{R (z)}{z}\| \leq U$
65	19	ad2antrr	$⊢ ((φ \land J \in (M ..^N)) \land (x \in ℝ^{+} \land ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq 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)$
66		simprl	$⊢ ((φ \land J \in (M ..^N)) \land (x \in ℝ^{+} \land ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))) \to x \in ℝ^{+}$
67		simprr	$⊢ ((φ \land J \in (M ..^N)) \land (x \in ℝ^{+} \land ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))) \to ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E)$
68		simplr	$⊢ ((φ \land J \in (M ..^N)) \land (x \in ℝ^{+} \land ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))) \to J \in (M ..^N)$
69		eqid	$⊢ (⌊\frac{Z}{(1 + L E) x}⌋ + 1 \dots ⌊\frac{Z}{x}⌋) = (⌊\frac{Z}{(1 + L E) x}⌋ + 1 \dots ⌊\frac{Z}{x}⌋)$
70	1 55 56 57 5 6 58 59 9 10 60 61 62 14 63 16 17 64 65 20 66 67 68 69	pntlemj	$⊢ ((φ \land J \in (M ..^N)) \land (x \in ℝ^{+} \land ((K^{J} < x \land (1 + L E) x < K K^{J}) \land \forall u \in [x, (1 + L E) x] \|\frac{R (u)}{u}\| \leq E))) \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$
71	54 70	rexlimddv	$⊢ (φ \land J \in (M ..^N)) \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 pntlemi

Proof