pntlemq

	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	pntlemq	$⊢ φ \to I \subseteq O$

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 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))$
26	25	simp1d	$⊢ φ \to Z \in ℝ^{+}$
27	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 ℝ^{+}))$
28	27	simp2d	$⊢ φ \to K \in ℝ^{+}$
29		elfzoelz	$⊢ J \in (M ..^N) \to J \in ℤ$
30	23 29	syl	$⊢ φ \to J \in ℤ$
31	30	peano2zd	$⊢ φ \to J + 1 \in ℤ$
32	28 31	rpexpcld	$⊢ φ \to K^{J + 1} \in ℝ^{+}$
33	26 32	rpdivcld	$⊢ φ \to \frac{Z}{K^{J + 1}} \in ℝ^{+}$
34	33	rpred	$⊢ φ \to \frac{Z}{K^{J + 1}} \in ℝ$
35	34	flcld	$⊢ φ \to ⌊\frac{Z}{K^{J + 1}}⌋ \in ℤ$
36		1rp	$⊢ 1 \in ℝ^{+}$
37	1 2 3 4 5 6	pntlemd	$⊢ φ \to (L \in ℝ^{+} \land D \in ℝ^{+} \land F \in ℝ^{+})$
38	37	simp1d	$⊢ φ \to L \in ℝ^{+}$
39	27	simp1d	$⊢ φ \to E \in ℝ^{+}$
40	38 39	rpmulcld	$⊢ φ \to L E \in ℝ^{+}$
41		rpaddcl	$⊢ (1 \in ℝ^{+} \land L E \in ℝ^{+}) \to 1 + L E \in ℝ^{+}$
42	36 40 41	sylancr	$⊢ φ \to 1 + L E \in ℝ^{+}$
43	42 21	rpmulcld	$⊢ φ \to (1 + L E) V \in ℝ^{+}$
44	26 43	rpdivcld	$⊢ φ \to \frac{Z}{(1 + L E) V} \in ℝ^{+}$
45	44	rpred	$⊢ φ \to \frac{Z}{(1 + L E) V} \in ℝ$
46	45	flcld	$⊢ φ \to ⌊\frac{Z}{(1 + L E) V}⌋ \in ℤ$
47	43	rpred	$⊢ φ \to (1 + L E) V \in ℝ$
48	32	rpred	$⊢ φ \to K^{J + 1} \in ℝ$
49	22	simpld	$⊢ φ \to (K^{J} < V \land (1 + L E) V < K K^{J})$
50	49	simprd	$⊢ φ \to (1 + L E) V < K K^{J}$
51	28	rpcnd	$⊢ φ \to K \in ℂ$
52	28 30	rpexpcld	$⊢ φ \to K^{J} \in ℝ^{+}$
53	52	rpcnd	$⊢ φ \to K^{J} \in ℂ$
54	51 53	mulcomd	$⊢ φ \to K K^{J} = K^{J} K$
55	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)$
56	55	simp1d	$⊢ φ \to M \in ℕ$
57		elfzouz	$⊢ J \in (M ..^N) \to J \in ℤ_{\geq M}$
58	23 57	syl	$⊢ φ \to J \in ℤ_{\geq M}$
59		eluznn	$⊢ (M \in ℕ \land J \in ℤ_{\geq M}) \to J \in ℕ$
60	56 58 59	syl2anc	$⊢ φ \to J \in ℕ$
61	60	nnnn0d	$⊢ φ \to J \in ℕ_{0}$
62	51 61	expp1d	$⊢ φ \to K^{J + 1} = K^{J} K$
63	54 62	eqtr4d	$⊢ φ \to K K^{J} = K^{J + 1}$
64	50 63	breqtrd	$⊢ φ \to (1 + L E) V < K^{J + 1}$
65	47 48 64	ltled	$⊢ φ \to (1 + L E) V \leq K^{J + 1}$
66	43 32 26	lediv2d	$⊢ φ \to ((1 + L E) V \leq K^{J + 1} \leftrightarrow \frac{Z}{K^{J + 1}} \leq \frac{Z}{(1 + L E) V})$
67	65 66	mpbid	$⊢ φ \to \frac{Z}{K^{J + 1}} \leq \frac{Z}{(1 + L E) V}$
68		flwordi	$⊢ (\frac{Z}{K^{J + 1}} \in ℝ \land \frac{Z}{(1 + L E) V} \in ℝ \land \frac{Z}{K^{J + 1}} \leq \frac{Z}{(1 + L E) V}) \to ⌊\frac{Z}{K^{J + 1}}⌋ \leq ⌊\frac{Z}{(1 + L E) V}⌋$
69	34 45 67 68	syl3anc	$⊢ φ \to ⌊\frac{Z}{K^{J + 1}}⌋ \leq ⌊\frac{Z}{(1 + L E) V}⌋$
70		eluz2	$⊢ ⌊\frac{Z}{(1 + L E) V}⌋ \in ℤ_{\geq ⌊\frac{Z}{K^{J + 1}}⌋} \leftrightarrow (⌊\frac{Z}{K^{J + 1}}⌋ \in ℤ \land ⌊\frac{Z}{(1 + L E) V}⌋ \in ℤ \land ⌊\frac{Z}{K^{J + 1}}⌋ \leq ⌊\frac{Z}{(1 + L E) V}⌋)$
71	35 46 69 70	syl3anbrc	$⊢ φ \to ⌊\frac{Z}{(1 + L E) V}⌋ \in ℤ_{\geq ⌊\frac{Z}{K^{J + 1}}⌋}$
72		eluzp1p1	$⊢ ⌊\frac{Z}{(1 + L E) V}⌋ \in ℤ_{\geq ⌊\frac{Z}{K^{J + 1}}⌋} \to ⌊\frac{Z}{(1 + L E) V}⌋ + 1 \in ℤ_{\geq (⌊\frac{Z}{K^{J + 1}}⌋ + 1)}$
73		fzss1	$⊢ ⌊\frac{Z}{(1 + L E) V}⌋ + 1 \in ℤ_{\geq (⌊\frac{Z}{K^{J + 1}}⌋ + 1)} \to (⌊\frac{Z}{(1 + L E) V}⌋ + 1 \dots ⌊\frac{Z}{V}⌋) \subseteq (⌊\frac{Z}{K^{J + 1}}⌋ + 1 \dots ⌊\frac{Z}{V}⌋)$
74	71 72 73	3syl	$⊢ φ \to (⌊\frac{Z}{(1 + L E) V}⌋ + 1 \dots ⌊\frac{Z}{V}⌋) \subseteq (⌊\frac{Z}{K^{J + 1}}⌋ + 1 \dots ⌊\frac{Z}{V}⌋)$
75	26 21	rpdivcld	$⊢ φ \to \frac{Z}{V} \in ℝ^{+}$
76	75	rpred	$⊢ φ \to \frac{Z}{V} \in ℝ$
77	76	flcld	$⊢ φ \to ⌊\frac{Z}{V}⌋ \in ℤ$
78	26 52	rpdivcld	$⊢ φ \to \frac{Z}{K^{J}} \in ℝ^{+}$
79	78	rpred	$⊢ φ \to \frac{Z}{K^{J}} \in ℝ$
80	79	flcld	$⊢ φ \to ⌊\frac{Z}{K^{J}}⌋ \in ℤ$
81	52	rpred	$⊢ φ \to K^{J} \in ℝ$
82	21	rpred	$⊢ φ \to V \in ℝ$
83	49	simpld	$⊢ φ \to K^{J} < V$
84	81 82 83	ltled	$⊢ φ \to K^{J} \leq V$
85	52 21 26	lediv2d	$⊢ φ \to (K^{J} \leq V \leftrightarrow \frac{Z}{V} \leq \frac{Z}{K^{J}})$
86	84 85	mpbid	$⊢ φ \to \frac{Z}{V} \leq \frac{Z}{K^{J}}$
87		flwordi	$⊢ (\frac{Z}{V} \in ℝ \land \frac{Z}{K^{J}} \in ℝ \land \frac{Z}{V} \leq \frac{Z}{K^{J}}) \to ⌊\frac{Z}{V}⌋ \leq ⌊\frac{Z}{K^{J}}⌋$
88	76 79 86 87	syl3anc	$⊢ φ \to ⌊\frac{Z}{V}⌋ \leq ⌊\frac{Z}{K^{J}}⌋$
89		eluz2	$⊢ ⌊\frac{Z}{K^{J}}⌋ \in ℤ_{\geq ⌊\frac{Z}{V}⌋} \leftrightarrow (⌊\frac{Z}{V}⌋ \in ℤ \land ⌊\frac{Z}{K^{J}}⌋ \in ℤ \land ⌊\frac{Z}{V}⌋ \leq ⌊\frac{Z}{K^{J}}⌋)$
90	77 80 88 89	syl3anbrc	$⊢ φ \to ⌊\frac{Z}{K^{J}}⌋ \in ℤ_{\geq ⌊\frac{Z}{V}⌋}$
91		fzss2	$⊢ ⌊\frac{Z}{K^{J}}⌋ \in ℤ_{\geq ⌊\frac{Z}{V}⌋} \to (⌊\frac{Z}{K^{J + 1}}⌋ + 1 \dots ⌊\frac{Z}{V}⌋) \subseteq (⌊\frac{Z}{K^{J + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{J}}⌋)$
92	90 91	syl	$⊢ φ \to (⌊\frac{Z}{K^{J + 1}}⌋ + 1 \dots ⌊\frac{Z}{V}⌋) \subseteq (⌊\frac{Z}{K^{J + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{J}}⌋)$
93	74 92	sstrd	$⊢ φ \to (⌊\frac{Z}{(1 + L E) V}⌋ + 1 \dots ⌊\frac{Z}{V}⌋) \subseteq (⌊\frac{Z}{K^{J + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{J}}⌋)$
94	93 24 20	3sstr4g	$⊢ φ \to I \subseteq O$

Metamath Proof Explorer

Theorem pntlemq

Proof