pntpbnd

Description: Lemma for pnt . Establish smallness of R at a point. Lemma 10.6.1 in Shapiro, p. 436. (Contributed by Mario Carneiro, 10-Apr-2016)

		Ref	Expression
	Hypothesis	pntibnd.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	Assertion	pntpbnd	$⊢ \exists c \in ℝ^{+} \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (x, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)$

Proof

Step	Hyp	Ref	Expression
1		pntibnd.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2	1	pntrsumbnd2	$⊢ \exists d \in ℝ^{+} \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d$
3		simpl	$⊢ (d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \to d \in ℝ^{+}$
4		2rp	$⊢ 2 \in ℝ^{+}$
5		rpaddcl	$⊢ (d \in ℝ^{+} \land 2 \in ℝ^{+}) \to d + 2 \in ℝ^{+}$
6	3 4 5	sylancl	$⊢ (d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \to d + 2 \in ℝ^{+}$
7		2re	$⊢ 2 \in ℝ$
8		elioore	$⊢ e \in (0, 1) \to e \in ℝ$
9	8	adantl	$⊢ ((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \to e \in ℝ$
10		eliooord	$⊢ e \in (0, 1) \to (0 < e \land e < 1)$
11	10	adantl	$⊢ ((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \to (0 < e \land e < 1)$
12	11	simpld	$⊢ ((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \to 0 < e$
13	9 12	elrpd	$⊢ ((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \to e \in ℝ^{+}$
14		rerpdivcl	$⊢ (2 \in ℝ \land e \in ℝ^{+}) \to \frac{2}{e} \in ℝ$
15	7 13 14	sylancr	$⊢ ((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \to \frac{2}{e} \in ℝ$
16	15	rpefcld	$⊢ ((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \to e^{\frac{2}{e}} \in ℝ^{+}$
17		simpllr	$⊢ ((((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \land (k \in [e^{\frac{d + 2}{e}}, +∞) \land y \in (e^{\frac{2}{e}}, +∞))) \land \neg \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)) \to e \in (0, 1)$
18		eqid	$⊢ e^{\frac{2}{e}} = e^{\frac{2}{e}}$
19		simplrr	$⊢ ((((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \land (k \in [e^{\frac{d + 2}{e}}, +∞) \land y \in (e^{\frac{2}{e}}, +∞))) \land \neg \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)) \to y \in (e^{\frac{2}{e}}, +∞)$
20		simp-4l	$⊢ ((((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \land (k \in [e^{\frac{d + 2}{e}}, +∞) \land y \in (e^{\frac{2}{e}}, +∞))) \land \neg \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)) \to d \in ℝ^{+}$
21		simp-4r	$⊢ ((((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \land (k \in [e^{\frac{d + 2}{e}}, +∞) \land y \in (e^{\frac{2}{e}}, +∞))) \land \neg \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)) \to \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d$
22		eqid	$⊢ d + 2 = d + 2$
23		simplrl	$⊢ ((((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \land (k \in [e^{\frac{d + 2}{e}}, +∞) \land y \in (e^{\frac{2}{e}}, +∞))) \land \neg \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)) \to k \in [e^{\frac{d + 2}{e}}, +∞)$
24		simpr	$⊢ ((((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \land (k \in [e^{\frac{d + 2}{e}}, +∞) \land y \in (e^{\frac{2}{e}}, +∞))) \land \neg \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)) \to \neg \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)$
25	1 17 18 19 20 21 22 23 24	pntpbnd2	$⊢ \neg ((((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \land (k \in [e^{\frac{d + 2}{e}}, +∞) \land y \in (e^{\frac{2}{e}}, +∞))) \land \neg \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e))$
26		iman	$⊢ ((((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \land (k \in [e^{\frac{d + 2}{e}}, +∞) \land y \in (e^{\frac{2}{e}}, +∞))) \to \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)) \leftrightarrow \neg ((((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \land (k \in [e^{\frac{d + 2}{e}}, +∞) \land y \in (e^{\frac{2}{e}}, +∞))) \land \neg \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e))$
27	25 26	mpbir	$⊢ (((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \land (k \in [e^{\frac{d + 2}{e}}, +∞) \land y \in (e^{\frac{2}{e}}, +∞))) \to \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)$
28	27	ralrimivva	$⊢ ((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \to \forall k \in [e^{\frac{d + 2}{e}}, +∞) \forall y \in (e^{\frac{2}{e}}, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)$
29		oveq1	$⊢ x = e^{\frac{2}{e}} \to (x, +∞) = (e^{\frac{2}{e}}, +∞)$
30	29	raleqdv	$⊢ x = e^{\frac{2}{e}} \to (\forall y \in (x, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e) \leftrightarrow \forall y \in (e^{\frac{2}{e}}, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e))$
31	30	ralbidv	$⊢ x = e^{\frac{2}{e}} \to (\forall k \in [e^{\frac{d + 2}{e}}, +∞) \forall y \in (x, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e) \leftrightarrow \forall k \in [e^{\frac{d + 2}{e}}, +∞) \forall y \in (e^{\frac{2}{e}}, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e))$
32	31	rspcev	$⊢ (e^{\frac{2}{e}} \in ℝ^{+} \land \forall k \in [e^{\frac{d + 2}{e}}, +∞) \forall y \in (e^{\frac{2}{e}}, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)) \to \exists x \in ℝ^{+} \forall k \in [e^{\frac{d + 2}{e}}, +∞) \forall y \in (x, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)$
33	16 28 32	syl2anc	$⊢ ((d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \land e \in (0, 1)) \to \exists x \in ℝ^{+} \forall k \in [e^{\frac{d + 2}{e}}, +∞) \forall y \in (x, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)$
34	33	ralrimiva	$⊢ (d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \to \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{d + 2}{e}}, +∞) \forall y \in (x, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)$
35		fvoveq1	$⊢ c = d + 2 \to e^{\frac{c}{e}} = e^{\frac{d + 2}{e}}$
36	35	oveq1d	$⊢ c = d + 2 \to [e^{\frac{c}{e}}, +∞) = [e^{\frac{d + 2}{e}}, +∞)$
37	36	raleqdv	$⊢ c = d + 2 \to (\forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (x, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e) \leftrightarrow \forall k \in [e^{\frac{d + 2}{e}}, +∞) \forall y \in (x, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e))$
38	37	rexbidv	$⊢ c = d + 2 \to (\exists x \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (x, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e) \leftrightarrow \exists x \in ℝ^{+} \forall k \in [e^{\frac{d + 2}{e}}, +∞) \forall y \in (x, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e))$
39	38	ralbidv	$⊢ c = d + 2 \to (\forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (x, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e) \leftrightarrow \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{d + 2}{e}}, +∞) \forall y \in (x, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e))$
40	39	rspcev	$⊢ (d + 2 \in ℝ^{+} \land \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{d + 2}{e}}, +∞) \forall y \in (x, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)) \to \exists c \in ℝ^{+} \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (x, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)$
41	6 34 40	syl2anc	$⊢ (d \in ℝ^{+} \land \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d) \to \exists c \in ℝ^{+} \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (x, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)$
42	41	rexlimiva	$⊢ \exists d \in ℝ^{+} \forall i \in ℕ \forall j \in ℤ \|\sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})\| \leq d \to \exists c \in ℝ^{+} \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (x, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)$
43	2 42	ax-mp	$⊢ \exists c \in ℝ^{+} \forall e \in (0, 1) \exists x \in ℝ^{+} \forall k \in [e^{\frac{c}{e}}, +∞) \forall y \in (x, +∞) \exists n \in ℕ ((y < n \land n \leq k y) \land \|\frac{R (n)}{n}\| \leq e)$

Metamath Proof Explorer

Theorem pntpbnd

Proof