pntrsumbnd

Description: A bound on a sum over R . Equation 10.1.16 of Shapiro, p. 403. (Contributed by Mario Carneiro, 25-May-2016)

		Ref	Expression
	Hypothesis	pntrval.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	Assertion	pntrsumbnd	$⊢ \exists c \in ℝ^{+} \forall m \in ℤ \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq c$

Proof

Step	Hyp	Ref	Expression
1		pntrval.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2		ssidd	$⊢ ⊤ \to ℝ \subseteq ℝ$
3		1red	$⊢ ⊤ \to 1 \in ℝ$
4		fzfid	$⊢ (⊤ \land m \in ℝ) \to (1 \dots ⌊m⌋) \in Fin$
5		elfznn	$⊢ n \in (1 \dots ⌊m⌋) \to n \in ℕ$
6	5	adantl	$⊢ ((⊤ \land m \in ℝ) \land n \in (1 \dots ⌊m⌋)) \to n \in ℕ$
7		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
8	1	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
9	8	ffvelcdmi	$⊢ n \in ℝ^{+} \to R (n) \in ℝ$
10	7 9	syl	$⊢ n \in ℕ \to R (n) \in ℝ$
11		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
12		nnmulcl	$⊢ (n \in ℕ \land n + 1 \in ℕ) \to n (n + 1) \in ℕ$
13	11 12	mpdan	$⊢ n \in ℕ \to n (n + 1) \in ℕ$
14	10 13	nndivred	$⊢ n \in ℕ \to \frac{R (n)}{n (n + 1)} \in ℝ$
15	14	recnd	$⊢ n \in ℕ \to \frac{R (n)}{n (n + 1)} \in ℂ$
16	6 15	syl	$⊢ ((⊤ \land m \in ℝ) \land n \in (1 \dots ⌊m⌋)) \to \frac{R (n)}{n (n + 1)} \in ℂ$
17	4 16	fsumcl	$⊢ (⊤ \land m \in ℝ) \to \sum_{n = 1}^{⌊m⌋} (\frac{R (n)}{n (n + 1)}) \in ℂ$
18	1	pntrsumo1	$⊢ (m \in ℝ ⟼ \sum_{n = 1}^{⌊m⌋} (\frac{R (n)}{n (n + 1)})) \in 𝑂 (1)$
19	18	a1i	$⊢ ⊤ \to (m \in ℝ ⟼ \sum_{n = 1}^{⌊m⌋} (\frac{R (n)}{n (n + 1)})) \in 𝑂 (1)$
20		fzfid	$⊢ (⊤ \land (x \in ℝ \land 1 \leq x)) \to (1 \dots ⌊x⌋) \in Fin$
21		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
22	21	adantl	$⊢ ((⊤ \land (x \in ℝ \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
23	22 15	syl	$⊢ ((⊤ \land (x \in ℝ \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to \frac{R (n)}{n (n + 1)} \in ℂ$
24	23	abscld	$⊢ ((⊤ \land (x \in ℝ \land 1 \leq x)) \land n \in (1 \dots ⌊x⌋)) \to \|\frac{R (n)}{n (n + 1)}\| \in ℝ$
25	20 24	fsumrecl	$⊢ (⊤ \land (x \in ℝ \land 1 \leq x)) \to \sum_{n = 1}^{⌊x⌋} \|\frac{R (n)}{n (n + 1)}\| \in ℝ$
26	17	adantr	$⊢ ((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \to \sum_{n = 1}^{⌊m⌋} (\frac{R (n)}{n (n + 1)}) \in ℂ$
27	26	abscld	$⊢ ((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \to \|\sum_{n = 1}^{⌊m⌋} (\frac{R (n)}{n (n + 1)})\| \in ℝ$
28		fzfid	$⊢ ((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \to (1 \dots ⌊m⌋) \in Fin$
29	16	adantlr	$⊢ (((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \land n \in (1 \dots ⌊m⌋)) \to \frac{R (n)}{n (n + 1)} \in ℂ$
30	29	abscld	$⊢ (((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \land n \in (1 \dots ⌊m⌋)) \to \|\frac{R (n)}{n (n + 1)}\| \in ℝ$
31	28 30	fsumrecl	$⊢ ((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \to \sum_{n = 1}^{⌊m⌋} \|\frac{R (n)}{n (n + 1)}\| \in ℝ$
32	25	ad2ant2r	$⊢ ((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \to \sum_{n = 1}^{⌊x⌋} \|\frac{R (n)}{n (n + 1)}\| \in ℝ$
33	28 29	fsumabs	$⊢ ((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \to \|\sum_{n = 1}^{⌊m⌋} (\frac{R (n)}{n (n + 1)})\| \leq \sum_{n = 1}^{⌊m⌋} \|\frac{R (n)}{n (n + 1)}\|$
34		fzfid	$⊢ ((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \to (1 \dots ⌊x⌋) \in Fin$
35	21	adantl	$⊢ (((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
36	35 15	syl	$⊢ (((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \land n \in (1 \dots ⌊x⌋)) \to \frac{R (n)}{n (n + 1)} \in ℂ$
37	36	abscld	$⊢ (((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \land n \in (1 \dots ⌊x⌋)) \to \|\frac{R (n)}{n (n + 1)}\| \in ℝ$
38	36	absge0d	$⊢ (((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \land n \in (1 \dots ⌊x⌋)) \to 0 \leq \|\frac{R (n)}{n (n + 1)}\|$
39		simplr	$⊢ ((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \to m \in ℝ$
40		simprll	$⊢ ((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \to x \in ℝ$
41		simprr	$⊢ ((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \to m < x$
42	39 40 41	ltled	$⊢ ((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \to m \leq x$
43		flword2	$⊢ (m \in ℝ \land x \in ℝ \land m \leq x) \to ⌊x⌋ \in ℤ_{\geq ⌊m⌋}$
44	39 40 42 43	syl3anc	$⊢ ((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \to ⌊x⌋ \in ℤ_{\geq ⌊m⌋}$
45		fzss2	$⊢ ⌊x⌋ \in ℤ_{\geq ⌊m⌋} \to (1 \dots ⌊m⌋) \subseteq (1 \dots ⌊x⌋)$
46	44 45	syl	$⊢ ((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \to (1 \dots ⌊m⌋) \subseteq (1 \dots ⌊x⌋)$
47	34 37 38 46	fsumless	$⊢ ((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \to \sum_{n = 1}^{⌊m⌋} \|\frac{R (n)}{n (n + 1)}\| \leq \sum_{n = 1}^{⌊x⌋} \|\frac{R (n)}{n (n + 1)}\|$
48	27 31 32 33 47	letrd	$⊢ ((⊤ \land m \in ℝ) \land ((x \in ℝ \land 1 \leq x) \land m < x)) \to \|\sum_{n = 1}^{⌊m⌋} (\frac{R (n)}{n (n + 1)})\| \leq \sum_{n = 1}^{⌊x⌋} \|\frac{R (n)}{n (n + 1)}\|$
49	2 3 17 19 25 48	o1bddrp	$⊢ ⊤ \to \exists c \in ℝ^{+} \forall m \in ℝ \|\sum_{n = 1}^{⌊m⌋} (\frac{R (n)}{n (n + 1)})\| \leq c$
50	49	mptru	$⊢ \exists c \in ℝ^{+} \forall m \in ℝ \|\sum_{n = 1}^{⌊m⌋} (\frac{R (n)}{n (n + 1)})\| \leq c$
51		zre	$⊢ m \in ℤ \to m \in ℝ$
52	51	imim1i	$⊢ (m \in ℝ \to \|\sum_{n = 1}^{⌊m⌋} (\frac{R (n)}{n (n + 1)})\| \leq c) \to (m \in ℤ \to \|\sum_{n = 1}^{⌊m⌋} (\frac{R (n)}{n (n + 1)})\| \leq c)$
53		flid	$⊢ m \in ℤ \to ⌊m⌋ = m$
54	53	oveq2d	$⊢ m \in ℤ \to (1 \dots ⌊m⌋) = (1 \dots m)$
55	54	sumeq1d	$⊢ m \in ℤ \to \sum_{n = 1}^{⌊m⌋} (\frac{R (n)}{n (n + 1)}) = \sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})$
56	55	fveq2d	$⊢ m \in ℤ \to \|\sum_{n = 1}^{⌊m⌋} (\frac{R (n)}{n (n + 1)})\| = \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\|$
57	56	breq1d	$⊢ m \in ℤ \to (\|\sum_{n = 1}^{⌊m⌋} (\frac{R (n)}{n (n + 1)})\| \leq c \leftrightarrow \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq c)$
58	52 57	mpbidi	$⊢ (m \in ℝ \to \|\sum_{n = 1}^{⌊m⌋} (\frac{R (n)}{n (n + 1)})\| \leq c) \to (m \in ℤ \to \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq c)$
59	58	ralimi2	$⊢ \forall m \in ℝ \|\sum_{n = 1}^{⌊m⌋} (\frac{R (n)}{n (n + 1)})\| \leq c \to \forall m \in ℤ \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq c$
60	59	reximi	$⊢ \exists c \in ℝ^{+} \forall m \in ℝ \|\sum_{n = 1}^{⌊m⌋} (\frac{R (n)}{n (n + 1)})\| \leq c \to \exists c \in ℝ^{+} \forall m \in ℤ \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq c$
61	50 60	ax-mp	$⊢ \exists c \in ℝ^{+} \forall m \in ℤ \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq c$

Metamath Proof Explorer

Theorem pntrsumbnd

Proof