pntpbnd1a

Description: Lemma for pntpbnd . (Contributed by Mario Carneiro, 11-Apr-2016) Replace reference to OLD theorem. (Revised by Wolf Lammen, 8-Sep-2020)

	Ref	Expression
Hypotheses	pntpbnd.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	pntpbnd1.e	$⊢ φ \to E \in (0, 1)$
	pntpbnd1.x	$⊢ X = e^{\frac{2}{E}}$
	pntpbnd1.y	$⊢ φ \to Y \in (X, +∞)$
	pntpbnd1a.1	$⊢ φ \to N \in ℕ$
	pntpbnd1a.2	$⊢ φ \to (Y < N \land N \leq K Y)$
	pntpbnd1a.3	$⊢ φ \to \|R (N)\| \leq \|R (N + 1) - R (N)\|$
Assertion	pntpbnd1a	$⊢ φ \to \|\frac{R (N)}{N}\| \leq E$

Proof

Step	Hyp	Ref	Expression
1		pntpbnd.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2		pntpbnd1.e	$⊢ φ \to E \in (0, 1)$
3		pntpbnd1.x	$⊢ X = e^{\frac{2}{E}}$
4		pntpbnd1.y	$⊢ φ \to Y \in (X, +∞)$
5		pntpbnd1a.1	$⊢ φ \to N \in ℕ$
6		pntpbnd1a.2	$⊢ φ \to (Y < N \land N \leq K Y)$
7		pntpbnd1a.3	$⊢ φ \to \|R (N)\| \leq \|R (N + 1) - R (N)\|$
8	5	nnrpd	$⊢ φ \to N \in ℝ^{+}$
9	1	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
10	9	ffvelrni	$⊢ N \in ℝ^{+} \to R (N) \in ℝ$
11	8 10	syl	$⊢ φ \to R (N) \in ℝ$
12	11 8	rerpdivcld	$⊢ φ \to \frac{R (N)}{N} \in ℝ$
13	12	recnd	$⊢ φ \to \frac{R (N)}{N} \in ℂ$
14	13	abscld	$⊢ φ \to \|\frac{R (N)}{N}\| \in ℝ$
15	8	relogcld	$⊢ φ \to \log N \in ℝ$
16	15 8	rerpdivcld	$⊢ φ \to \frac{\log N}{N} \in ℝ$
17		ioossre	$⊢ (0, 1) \subseteq ℝ$
18	17 2	sseldi	$⊢ φ \to E \in ℝ$
19	11	recnd	$⊢ φ \to R (N) \in ℂ$
20	5	nnred	$⊢ φ \to N \in ℝ$
21	20	recnd	$⊢ φ \to N \in ℂ$
22	5	nnne0d	$⊢ φ \to N \neq 0$
23	19 21 22	absdivd	$⊢ φ \to \|\frac{R (N)}{N}\| = \frac{\|R (N)\|}{\|N\|}$
24	5	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
25	24	nn0ge0d	$⊢ φ \to 0 \leq N$
26	20 25	absidd	$⊢ φ \to \|N\| = N$
27	26	oveq2d	$⊢ φ \to \frac{\|R (N)\|}{\|N\|} = \frac{\|R (N)\|}{N}$
28	23 27	eqtrd	$⊢ φ \to \|\frac{R (N)}{N}\| = \frac{\|R (N)\|}{N}$
29	19	abscld	$⊢ φ \to \|R (N)\| \in ℝ$
30	5	peano2nnd	$⊢ φ \to N + 1 \in ℕ$
31		vmacl	$⊢ N + 1 \in ℕ \to Λ (N + 1) \in ℝ$
32	30 31	syl	$⊢ φ \to Λ (N + 1) \in ℝ$
33		peano2rem	$⊢ Λ (N + 1) \in ℝ \to Λ (N + 1) - 1 \in ℝ$
34	32 33	syl	$⊢ φ \to Λ (N + 1) - 1 \in ℝ$
35	34	recnd	$⊢ φ \to Λ (N + 1) - 1 \in ℂ$
36	35	abscld	$⊢ φ \to \|Λ (N + 1) - 1\| \in ℝ$
37	30	nnrpd	$⊢ φ \to N + 1 \in ℝ^{+}$
38	1	pntrval	$⊢ N + 1 \in ℝ^{+} \to R (N + 1) = ψ (N + 1) - (N + 1)$
39	37 38	syl	$⊢ φ \to R (N + 1) = ψ (N + 1) - (N + 1)$
40	1	pntrval	$⊢ N \in ℝ^{+} \to R (N) = ψ (N) - N$
41	8 40	syl	$⊢ φ \to R (N) = ψ (N) - N$
42	39 41	oveq12d	$⊢ φ \to R (N + 1) - R (N) = ψ (N + 1) - (N + 1) - (ψ (N) - N)$
43		peano2re	$⊢ N \in ℝ \to N + 1 \in ℝ$
44	20 43	syl	$⊢ φ \to N + 1 \in ℝ$
45		chpcl	$⊢ N + 1 \in ℝ \to ψ (N + 1) \in ℝ$
46	44 45	syl	$⊢ φ \to ψ (N + 1) \in ℝ$
47	46	recnd	$⊢ φ \to ψ (N + 1) \in ℂ$
48	44	recnd	$⊢ φ \to N + 1 \in ℂ$
49		chpcl	$⊢ N \in ℝ \to ψ (N) \in ℝ$
50	20 49	syl	$⊢ φ \to ψ (N) \in ℝ$
51	50	recnd	$⊢ φ \to ψ (N) \in ℂ$
52	47 48 51 21	sub4d	$⊢ φ \to ψ (N + 1) - (N + 1) - (ψ (N) - N) = ψ (N + 1) - ψ (N) - (N + 1 - N)$
53	32	recnd	$⊢ φ \to Λ (N + 1) \in ℂ$
54		chpp1	$⊢ N \in ℕ_{0} \to ψ (N + 1) = ψ (N) + Λ (N + 1)$
55	24 54	syl	$⊢ φ \to ψ (N + 1) = ψ (N) + Λ (N + 1)$
56	51 53 55	mvrladdd	$⊢ φ \to ψ (N + 1) - ψ (N) = Λ (N + 1)$
57		ax-1cn	$⊢ 1 \in ℂ$
58		pncan2	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - N = 1$
59	21 57 58	sylancl	$⊢ φ \to N + 1 - N = 1$
60	56 59	oveq12d	$⊢ φ \to ψ (N + 1) - ψ (N) - (N + 1 - N) = Λ (N + 1) - 1$
61	42 52 60	3eqtrd	$⊢ φ \to R (N + 1) - R (N) = Λ (N + 1) - 1$
62	61	fveq2d	$⊢ φ \to \|R (N + 1) - R (N)\| = \|Λ (N + 1) - 1\|$
63	7 62	breqtrd	$⊢ φ \to \|R (N)\| \leq \|Λ (N + 1) - 1\|$
64		1red	$⊢ φ \to 1 \in ℝ$
65	64 15	resubcld	$⊢ φ \to 1 - \log N \in ℝ$
66		0red	$⊢ φ \to 0 \in ℝ$
67		2re	$⊢ 2 \in ℝ$
68		eliooord	$⊢ E \in (0, 1) \to (0 < E \land E < 1)$
69	2 68	syl	$⊢ φ \to (0 < E \land E < 1)$
70	69	simpld	$⊢ φ \to 0 < E$
71	18 70	elrpd	$⊢ φ \to E \in ℝ^{+}$
72		rerpdivcl	$⊢ (2 \in ℝ \land E \in ℝ^{+}) \to \frac{2}{E} \in ℝ$
73	67 71 72	sylancr	$⊢ φ \to \frac{2}{E} \in ℝ$
74	67	a1i	$⊢ φ \to 2 \in ℝ$
75		1lt2	$⊢ 1 < 2$
76	75	a1i	$⊢ φ \to 1 < 2$
77		2cn	$⊢ 2 \in ℂ$
78	77	div1i	$⊢ \frac{2}{1} = 2$
79	69	simprd	$⊢ φ \to E < 1$
80		0lt1	$⊢ 0 < 1$
81	80	a1i	$⊢ φ \to 0 < 1$
82		2pos	$⊢ 0 < 2$
83	82	a1i	$⊢ φ \to 0 < 2$
84		ltdiv2	$⊢ ((E \in ℝ \land 0 < E) \land (1 \in ℝ \land 0 < 1) \land (2 \in ℝ \land 0 < 2)) \to (E < 1 \leftrightarrow \frac{2}{1} < \frac{2}{E})$
85	18 70 64 81 74 83 84	syl222anc	$⊢ φ \to (E < 1 \leftrightarrow \frac{2}{1} < \frac{2}{E})$
86	79 85	mpbid	$⊢ φ \to \frac{2}{1} < \frac{2}{E}$
87	78 86	eqbrtrrid	$⊢ φ \to 2 < \frac{2}{E}$
88	64 74 73 76 87	lttrd	$⊢ φ \to 1 < \frac{2}{E}$
89	73	rpefcld	$⊢ φ \to e^{\frac{2}{E}} \in ℝ^{+}$
90	3 89	eqeltrid	$⊢ φ \to X \in ℝ^{+}$
91	90	rpred	$⊢ φ \to X \in ℝ$
92	90	rpxrd	$⊢ φ \to X \in ℝ^{*}$
93		elioopnf	$⊢ X \in ℝ^{*} \to (Y \in (X, +∞) \leftrightarrow (Y \in ℝ \land X < Y))$
94	92 93	syl	$⊢ φ \to (Y \in (X, +∞) \leftrightarrow (Y \in ℝ \land X < Y))$
95	4 94	mpbid	$⊢ φ \to (Y \in ℝ \land X < Y)$
96	95	simpld	$⊢ φ \to Y \in ℝ$
97	95	simprd	$⊢ φ \to X < Y$
98	6	simpld	$⊢ φ \to Y < N$
99	91 96 20 97 98	lttrd	$⊢ φ \to X < N$
100	3 99	eqbrtrrid	$⊢ φ \to e^{\frac{2}{E}} < N$
101	8	reeflogd	$⊢ φ \to e^{\log N} = N$
102	100 101	breqtrrd	$⊢ φ \to e^{\frac{2}{E}} < e^{\log N}$
103		eflt	$⊢ (\frac{2}{E} \in ℝ \land \log N \in ℝ) \to (\frac{2}{E} < \log N \leftrightarrow e^{\frac{2}{E}} < e^{\log N})$
104	73 15 103	syl2anc	$⊢ φ \to (\frac{2}{E} < \log N \leftrightarrow e^{\frac{2}{E}} < e^{\log N})$
105	102 104	mpbird	$⊢ φ \to \frac{2}{E} < \log N$
106	64 73 15 88 105	lttrd	$⊢ φ \to 1 < \log N$
107	64 15 106	ltled	$⊢ φ \to 1 \leq \log N$
108		1re	$⊢ 1 \in ℝ$
109		suble0	$⊢ (1 \in ℝ \land \log N \in ℝ) \to (1 - \log N \leq 0 \leftrightarrow 1 \leq \log N)$
110	108 15 109	sylancr	$⊢ φ \to (1 - \log N \leq 0 \leftrightarrow 1 \leq \log N)$
111	107 110	mpbird	$⊢ φ \to 1 - \log N \leq 0$
112		vmage0	$⊢ N + 1 \in ℕ \to 0 \leq Λ (N + 1)$
113	30 112	syl	$⊢ φ \to 0 \leq Λ (N + 1)$
114	65 66 32 111 113	letrd	$⊢ φ \to 1 - \log N \leq Λ (N + 1)$
115	37	relogcld	$⊢ φ \to \log (N + 1) \in ℝ$
116		readdcl	$⊢ (1 \in ℝ \land \log N \in ℝ) \to 1 + \log N \in ℝ$
117	108 15 116	sylancr	$⊢ φ \to 1 + \log N \in ℝ$
118		vmalelog	$⊢ N + 1 \in ℕ \to Λ (N + 1) \leq \log (N + 1)$
119	30 118	syl	$⊢ φ \to Λ (N + 1) \leq \log (N + 1)$
120	74 20	remulcld	$⊢ φ \to 2 \cdot N \in ℝ$
121		epr	$⊢ e \in ℝ^{+}$
122		rpmulcl	$⊢ (e \in ℝ^{+} \land N \in ℝ^{+}) \to e \cdot N \in ℝ^{+}$
123	121 8 122	sylancr	$⊢ φ \to e \cdot N \in ℝ^{+}$
124	123	rpred	$⊢ φ \to e \cdot N \in ℝ$
125	5	nnge1d	$⊢ φ \to 1 \leq N$
126	64 20 20 125	leadd2dd	$⊢ φ \to N + 1 \leq N + N$
127	21	2timesd	$⊢ φ \to 2 \cdot N = N + N$
128	126 127	breqtrrd	$⊢ φ \to N + 1 \leq 2 \cdot N$
129		ere	$⊢ e \in ℝ$
130		egt2lt3	$⊢ (2 < e \land e < 3)$
131	130	simpli	$⊢ 2 < e$
132	67 129 131	ltleii	$⊢ 2 \leq e$
133	132	a1i	$⊢ φ \to 2 \leq e$
134	129	a1i	$⊢ φ \to e \in ℝ$
135	5	nngt0d	$⊢ φ \to 0 < N$
136		lemul1	$⊢ (2 \in ℝ \land e \in ℝ \land (N \in ℝ \land 0 < N)) \to (2 \leq e \leftrightarrow 2 \cdot N \leq e \cdot N)$
137	74 134 20 135 136	syl112anc	$⊢ φ \to (2 \leq e \leftrightarrow 2 \cdot N \leq e \cdot N)$
138	133 137	mpbid	$⊢ φ \to 2 \cdot N \leq e \cdot N$
139	44 120 124 128 138	letrd	$⊢ φ \to N + 1 \leq e \cdot N$
140	37 123	logled	$⊢ φ \to (N + 1 \leq e \cdot N \leftrightarrow \log (N + 1) \leq \log e \cdot N)$
141	139 140	mpbid	$⊢ φ \to \log (N + 1) \leq \log e \cdot N$
142		relogmul	$⊢ (e \in ℝ^{+} \land N \in ℝ^{+}) \to \log e \cdot N = \log e + \log N$
143	121 8 142	sylancr	$⊢ φ \to \log e \cdot N = \log e + \log N$
144		loge	$⊢ \log e = 1$
145	144	oveq1i	$⊢ \log e + \log N = 1 + \log N$
146	143 145	eqtrdi	$⊢ φ \to \log e \cdot N = 1 + \log N$
147	141 146	breqtrd	$⊢ φ \to \log (N + 1) \leq 1 + \log N$
148	32 115 117 119 147	letrd	$⊢ φ \to Λ (N + 1) \leq 1 + \log N$
149	32 64 15	absdifled	$⊢ φ \to (\|Λ (N + 1) - 1\| \leq \log N \leftrightarrow (1 - \log N \leq Λ (N + 1) \land Λ (N + 1) \leq 1 + \log N))$
150	114 148 149	mpbir2and	$⊢ φ \to \|Λ (N + 1) - 1\| \leq \log N$
151	29 36 15 63 150	letrd	$⊢ φ \to \|R (N)\| \leq \log N$
152	29 15 8 151	lediv1dd	$⊢ φ \to \frac{\|R (N)\|}{N} \leq \frac{\log N}{N}$
153	28 152	eqbrtrd	$⊢ φ \to \|\frac{R (N)}{N}\| \leq \frac{\log N}{N}$
154	90	relogcld	$⊢ φ \to \log X \in ℝ$
155	154 90	rerpdivcld	$⊢ φ \to \frac{\log X}{X} \in ℝ$
156	64 73 88	ltled	$⊢ φ \to 1 \leq \frac{2}{E}$
157		efle	$⊢ (1 \in ℝ \land \frac{2}{E} \in ℝ) \to (1 \leq \frac{2}{E} \leftrightarrow e^{1} \leq e^{\frac{2}{E}})$
158	108 73 157	sylancr	$⊢ φ \to (1 \leq \frac{2}{E} \leftrightarrow e^{1} \leq e^{\frac{2}{E}})$
159	156 158	mpbid	$⊢ φ \to e^{1} \leq e^{\frac{2}{E}}$
160		df-e	$⊢ e = e^{1}$
161	159 160 3	3brtr4g	$⊢ φ \to e \leq X$
162	144 107	eqbrtrid	$⊢ φ \to \log e \leq \log N$
163		logleb	$⊢ (e \in ℝ^{+} \land N \in ℝ^{+}) \to (e \leq N \leftrightarrow \log e \leq \log N)$
164	121 8 163	sylancr	$⊢ φ \to (e \leq N \leftrightarrow \log e \leq \log N)$
165	162 164	mpbird	$⊢ φ \to e \leq N$
166		logdivlt	$⊢ ((X \in ℝ \land e \leq X) \land (N \in ℝ \land e \leq N)) \to (X < N \leftrightarrow \frac{\log N}{N} < \frac{\log X}{X})$
167	91 161 20 165 166	syl22anc	$⊢ φ \to (X < N \leftrightarrow \frac{\log N}{N} < \frac{\log X}{X})$
168	99 167	mpbid	$⊢ φ \to \frac{\log N}{N} < \frac{\log X}{X}$
169	3	fveq2i	$⊢ \log X = \log e^{\frac{2}{E}}$
170	73	relogefd	$⊢ φ \to \log e^{\frac{2}{E}} = \frac{2}{E}$
171	169 170	syl5eq	$⊢ φ \to \log X = \frac{2}{E}$
172	171	oveq1d	$⊢ φ \to \frac{\log X}{X} = \frac{\frac{2}{E}}{X}$
173		2rp	$⊢ 2 \in ℝ^{+}$
174		rpdivcl	$⊢ (2 \in ℝ^{+} \land E \in ℝ^{+}) \to \frac{2}{E} \in ℝ^{+}$
175	173 71 174	sylancr	$⊢ φ \to \frac{2}{E} \in ℝ^{+}$
176	175	rpcnd	$⊢ φ \to \frac{2}{E} \in ℂ$
177	176	sqvald	$⊢ φ \to {(\frac{2}{E})}^{2} = (\frac{2}{E}) (\frac{2}{E})$
178		2cnd	$⊢ φ \to 2 \in ℂ$
179	71	rpcnne0d	$⊢ φ \to (E \in ℂ \land E \neq 0)$
180		div12	$⊢ (\frac{2}{E} \in ℂ \land 2 \in ℂ \land (E \in ℂ \land E \neq 0)) \to (\frac{2}{E}) (\frac{2}{E}) = 2 (\frac{\frac{2}{E}}{E})$
181	176 178 179 180	syl3anc	$⊢ φ \to (\frac{2}{E}) (\frac{2}{E}) = 2 (\frac{\frac{2}{E}}{E})$
182	177 181	eqtrd	$⊢ φ \to {(\frac{2}{E})}^{2} = 2 (\frac{\frac{2}{E}}{E})$
183	182	oveq1d	$⊢ φ \to \frac{{(\frac{2}{E})}^{2}}{2} = \frac{2 (\frac{\frac{2}{E}}{E})}{2}$
184	175 71	rpdivcld	$⊢ φ \to \frac{\frac{2}{E}}{E} \in ℝ^{+}$
185	184	rpcnd	$⊢ φ \to \frac{\frac{2}{E}}{E} \in ℂ$
186		2ne0	$⊢ 2 \neq 0$
187	186	a1i	$⊢ φ \to 2 \neq 0$
188	185 178 187	divcan3d	$⊢ φ \to \frac{2 (\frac{\frac{2}{E}}{E})}{2} = \frac{\frac{2}{E}}{E}$
189	183 188	eqtrd	$⊢ φ \to \frac{{(\frac{2}{E})}^{2}}{2} = \frac{\frac{2}{E}}{E}$
190	73	resqcld	$⊢ φ \to {(\frac{2}{E})}^{2} \in ℝ$
191	190	rehalfcld	$⊢ φ \to \frac{{(\frac{2}{E})}^{2}}{2} \in ℝ$
192		1rp	$⊢ 1 \in ℝ^{+}$
193		rpaddcl	$⊢ (1 \in ℝ^{+} \land \frac{2}{E} \in ℝ^{+}) \to 1 + (\frac{2}{E}) \in ℝ^{+}$
194	192 175 193	sylancr	$⊢ φ \to 1 + (\frac{2}{E}) \in ℝ^{+}$
195	194	rpred	$⊢ φ \to 1 + (\frac{2}{E}) \in ℝ$
196	195 191	readdcld	$⊢ φ \to 1 + (\frac{2}{E}) + (\frac{{(\frac{2}{E})}^{2}}{2}) \in ℝ$
197	191 194	ltaddrp2d	$⊢ φ \to \frac{{(\frac{2}{E})}^{2}}{2} < 1 + (\frac{2}{E}) + (\frac{{(\frac{2}{E})}^{2}}{2})$
198		efgt1p2	$⊢ \frac{2}{E} \in ℝ^{+} \to 1 + (\frac{2}{E}) + (\frac{{(\frac{2}{E})}^{2}}{2}) < e^{\frac{2}{E}}$
199	175 198	syl	$⊢ φ \to 1 + (\frac{2}{E}) + (\frac{{(\frac{2}{E})}^{2}}{2}) < e^{\frac{2}{E}}$
200	199 3	breqtrrdi	$⊢ φ \to 1 + (\frac{2}{E}) + (\frac{{(\frac{2}{E})}^{2}}{2}) < X$
201	191 196 91 197 200	lttrd	$⊢ φ \to \frac{{(\frac{2}{E})}^{2}}{2} < X$
202	189 201	eqbrtrrd	$⊢ φ \to \frac{\frac{2}{E}}{E} < X$
203	73 71 90 202	ltdiv23d	$⊢ φ \to \frac{\frac{2}{E}}{X} < E$
204	172 203	eqbrtrd	$⊢ φ \to \frac{\log X}{X} < E$
205	16 155 18 168 204	lttrd	$⊢ φ \to \frac{\log N}{N} < E$
206	16 18 205	ltled	$⊢ φ \to \frac{\log N}{N} \leq E$
207	14 16 18 153 206	letrd	$⊢ φ \to \|\frac{R (N)}{N}\| \leq E$

Metamath Proof Explorer

Theorem pntpbnd1a

Proof