pntrsumbnd2

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

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

Proof

Step	Hyp	Ref	Expression
1		pntrval.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2	1	pntrsumbnd	$⊢ \exists b \in ℝ^{+} \forall m \in ℤ \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b$
3		2rp	$⊢ 2 \in ℝ^{+}$
4		rpmulcl	$⊢ (2 \in ℝ^{+} \land b \in ℝ^{+}) \to 2 b \in ℝ^{+}$
5	3 4	mpan	$⊢ b \in ℝ^{+} \to 2 b \in ℝ^{+}$
6		oveq2	$⊢ m = k - 1 \to (1 \dots m) = (1 \dots k - 1)$
7	6	sumeq1d	$⊢ m = k - 1 \to \sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)}) = \sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})$
8	7	fveq2d	$⊢ m = k - 1 \to \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| = \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\|$
9	8	breq1d	$⊢ m = k - 1 \to (\|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b \leftrightarrow \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b)$
10		simplr	$⊢ ((b \in ℝ^{+} \land \forall m \in ℤ \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b) \land k \in ℕ) \to \forall m \in ℤ \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b$
11		nnz	$⊢ k \in ℕ \to k \in ℤ$
12	11	adantl	$⊢ ((b \in ℝ^{+} \land \forall m \in ℤ \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b) \land k \in ℕ) \to k \in ℤ$
13		peano2zm	$⊢ k \in ℤ \to k - 1 \in ℤ$
14	12 13	syl	$⊢ ((b \in ℝ^{+} \land \forall m \in ℤ \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b) \land k \in ℕ) \to k - 1 \in ℤ$
15	9 10 14	rspcdva	$⊢ ((b \in ℝ^{+} \land \forall m \in ℤ \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b) \land k \in ℕ) \to \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b$
16	5	ad2antrr	$⊢ ((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \to 2 b \in ℝ^{+}$
17	16	rpge0d	$⊢ ((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \to 0 \leq 2 b$
18		sumeq1	$⊢ (k \dots m) = \emptyset \to \sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)}) = \sum_{n \in \emptyset} (\frac{R (n)}{n (n + 1)})$
19		sum0	$⊢ \sum_{n \in \emptyset} (\frac{R (n)}{n (n + 1)}) = 0$
20	18 19	eqtrdi	$⊢ (k \dots m) = \emptyset \to \sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)}) = 0$
21	20	abs00bd	$⊢ (k \dots m) = \emptyset \to \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| = 0$
22	21	breq1d	$⊢ (k \dots m) = \emptyset \to (\|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b \leftrightarrow 0 \leq 2 b)$
23	17 22	syl5ibrcom	$⊢ ((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \to ((k \dots m) = \emptyset \to \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b)$
24	23	imp	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land (k \dots m) = \emptyset) \to \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b$
25	24	a1d	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land (k \dots m) = \emptyset) \to ((\|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b \land \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b) \to \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b)$
26		fzn0	$⊢ (k \dots m) \neq \emptyset \leftrightarrow m \in ℤ_{\geq k}$
27		fzfid	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to (1 \dots m) \in Fin$
28		elfznn	$⊢ n \in (1 \dots m) \to n \in ℕ$
29		simpr	$⊢ ((((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \land n \in ℕ) \to n \in ℕ$
30	29	nnrpd	$⊢ ((((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \land n \in ℕ) \to n \in ℝ^{+}$
31	1	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
32	31	ffvelcdmi	$⊢ n \in ℝ^{+} \to R (n) \in ℝ$
33	30 32	syl	$⊢ ((((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \land n \in ℕ) \to R (n) \in ℝ$
34	29	peano2nnd	$⊢ ((((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \land n \in ℕ) \to n + 1 \in ℕ$
35	29 34	nnmulcld	$⊢ ((((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \land n \in ℕ) \to n (n + 1) \in ℕ$
36	33 35	nndivred	$⊢ ((((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \land n \in ℕ) \to \frac{R (n)}{n (n + 1)} \in ℝ$
37	28 36	sylan2	$⊢ ((((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \land n \in (1 \dots m)) \to \frac{R (n)}{n (n + 1)} \in ℝ$
38	27 37	fsumrecl	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to \sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)}) \in ℝ$
39	38	recnd	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to \sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)}) \in ℂ$
40	39	abscld	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \in ℝ$
41		fzfid	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to (1 \dots k - 1) \in Fin$
42		elfznn	$⊢ n \in (1 \dots k - 1) \to n \in ℕ$
43	42 36	sylan2	$⊢ ((((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \land n \in (1 \dots k - 1)) \to \frac{R (n)}{n (n + 1)} \in ℝ$
44	41 43	fsumrecl	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to \sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)}) \in ℝ$
45	44	recnd	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to \sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)}) \in ℂ$
46	45	abscld	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \in ℝ$
47		simplll	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to b \in ℝ^{+}$
48	47	rpred	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to b \in ℝ$
49		le2add	$⊢ ((\|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \in ℝ \land \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \in ℝ) \land (b \in ℝ \land b \in ℝ)) \to ((\|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b \land \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b) \to \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| + \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b + b)$
50	40 46 48 48 49	syl22anc	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to ((\|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b \land \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b) \to \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| + \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b + b)$
51	48	recnd	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to b \in ℂ$
52	51	2timesd	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to 2 b = b + b$
53	52	breq2d	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to (\|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| + \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq 2 b \leftrightarrow \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| + \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b + b)$
54		fzfid	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to (k \dots m) \in Fin$
55		simpllr	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to k \in ℕ$
56		elfzuz	$⊢ n \in (k \dots m) \to n \in ℤ_{\geq k}$
57		eluznn	$⊢ (k \in ℕ \land n \in ℤ_{\geq k}) \to n \in ℕ$
58	55 56 57	syl2an	$⊢ ((((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \land n \in (k \dots m)) \to n \in ℕ$
59	58 36	syldan	$⊢ ((((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \land n \in (k \dots m)) \to \frac{R (n)}{n (n + 1)} \in ℝ$
60	54 59	fsumrecl	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to \sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)}) \in ℝ$
61	60	recnd	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to \sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)}) \in ℂ$
62	55	nnred	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to k \in ℝ$
63	62	ltm1d	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to k - 1 < k$
64		fzdisj	$⊢ k - 1 < k \to (1 \dots k - 1) \cap (k \dots m) = \emptyset$
65	63 64	syl	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to (1 \dots k - 1) \cap (k \dots m) = \emptyset$
66	55	nncnd	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to k \in ℂ$
67		ax-1cn	$⊢ 1 \in ℂ$
68		npcan	$⊢ (k \in ℂ \land 1 \in ℂ) \to k - 1 + 1 = k$
69	66 67 68	sylancl	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to k - 1 + 1 = k$
70	69 55	eqeltrd	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to k - 1 + 1 \in ℕ$
71		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
72	70 71	eleqtrdi	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to k - 1 + 1 \in ℤ_{\geq 1}$
73	55	nnzd	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to k \in ℤ$
74	73 13	syl	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to k - 1 \in ℤ$
75		simplr	$⊢ ((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \to k \in ℕ$
76	75	nncnd	$⊢ ((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \to k \in ℂ$
77	76 67 68	sylancl	$⊢ ((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \to k - 1 + 1 = k$
78	77	fveq2d	$⊢ ((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \to ℤ_{\geq (k - 1 + 1)} = ℤ_{\geq k}$
79	78	eleq2d	$⊢ ((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \to (m \in ℤ_{\geq (k - 1 + 1)} \leftrightarrow m \in ℤ_{\geq k})$
80	79	biimpar	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to m \in ℤ_{\geq (k - 1 + 1)}$
81		peano2uzr	$⊢ (k - 1 \in ℤ \land m \in ℤ_{\geq (k - 1 + 1)}) \to m \in ℤ_{\geq (k - 1)}$
82	74 80 81	syl2anc	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to m \in ℤ_{\geq (k - 1)}$
83		fzsplit2	$⊢ (k - 1 + 1 \in ℤ_{\geq 1} \land m \in ℤ_{\geq (k - 1)}) \to (1 \dots m) = (1 \dots k - 1) \cup (k - 1 + 1 \dots m)$
84	72 82 83	syl2anc	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to (1 \dots m) = (1 \dots k - 1) \cup (k - 1 + 1 \dots m)$
85	69	oveq1d	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to (k - 1 + 1 \dots m) = (k \dots m)$
86	85	uneq2d	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to (1 \dots k - 1) \cup (k - 1 + 1 \dots m) = (1 \dots k - 1) \cup (k \dots m)$
87	84 86	eqtrd	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to (1 \dots m) = (1 \dots k - 1) \cup (k \dots m)$
88	37	recnd	$⊢ ((((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \land n \in (1 \dots m)) \to \frac{R (n)}{n (n + 1)} \in ℂ$
89	65 87 27 88	fsumsplit	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to \sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)}) = \sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)}) + \sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})$
90	45 61 89	mvrladdd	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to \sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)}) - \sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)}) = \sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})$
91	90	fveq2d	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)}) - \sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| = \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\|$
92	39 45	abs2dif2d	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)}) - \sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| + \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\|$
93	91 92	eqbrtrrd	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| + \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\|$
94	61	abscld	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \in ℝ$
95	40 46	readdcld	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| + \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \in ℝ$
96		2re	$⊢ 2 \in ℝ$
97	96	a1i	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to 2 \in ℝ$
98	97 48	remulcld	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to 2 b \in ℝ$
99		letr	$⊢ (\|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \in ℝ \land \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| + \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \in ℝ \land 2 b \in ℝ) \to ((\|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| + \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \land \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| + \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq 2 b) \to \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b)$
100	94 95 98 99	syl3anc	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to ((\|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| + \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \land \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| + \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq 2 b) \to \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b)$
101	93 100	mpand	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to (\|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| + \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq 2 b \to \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b)$
102	53 101	sylbird	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to (\|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| + \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b + b \to \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b)$
103	50 102	syld	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to ((\|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b \land \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b) \to \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b)$
104	103	ancomsd	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land m \in ℤ_{\geq k}) \to ((\|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b \land \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b) \to \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b)$
105	26 104	sylan2b	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land (k \dots m) \neq \emptyset) \to ((\|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b \land \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b) \to \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b)$
106	25 105	pm2.61dane	$⊢ ((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \to ((\|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b \land \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b) \to \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b)$
107	106	imp	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land m \in ℤ) \land (\|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b \land \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b)) \to \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b$
108	107	an4s	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b) \land (m \in ℤ \land \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b)) \to \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b$
109	108	expr	$⊢ (((b \in ℝ^{+} \land k \in ℕ) \land \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b) \land m \in ℤ) \to (\|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b \to \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b)$
110	109	ralimdva	$⊢ ((b \in ℝ^{+} \land k \in ℕ) \land \|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b) \to (\forall m \in ℤ \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b \to \forall m \in ℤ \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b)$
111	110	impancom	$⊢ ((b \in ℝ^{+} \land k \in ℕ) \land \forall m \in ℤ \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b) \to (\|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b \to \forall m \in ℤ \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b)$
112	111	an32s	$⊢ ((b \in ℝ^{+} \land \forall m \in ℤ \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b) \land k \in ℕ) \to (\|\sum_{n = 1}^{k - 1} (\frac{R (n)}{n (n + 1)})\| \leq b \to \forall m \in ℤ \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b)$
113	15 112	mpd	$⊢ ((b \in ℝ^{+} \land \forall m \in ℤ \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b) \land k \in ℕ) \to \forall m \in ℤ \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b$
114	113	ralrimiva	$⊢ (b \in ℝ^{+} \land \forall m \in ℤ \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b) \to \forall k \in ℕ \forall m \in ℤ \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b$
115		breq2	$⊢ c = 2 b \to (\|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq c \leftrightarrow \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b)$
116	115	2ralbidv	$⊢ c = 2 b \to (\forall k \in ℕ \forall m \in ℤ \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq c \leftrightarrow \forall k \in ℕ \forall m \in ℤ \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b)$
117	116	rspcev	$⊢ (2 b \in ℝ^{+} \land \forall k \in ℕ \forall m \in ℤ \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq 2 b) \to \exists c \in ℝ^{+} \forall k \in ℕ \forall m \in ℤ \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq c$
118	5 114 117	syl2an2r	$⊢ (b \in ℝ^{+} \land \forall m \in ℤ \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b) \to \exists c \in ℝ^{+} \forall k \in ℕ \forall m \in ℤ \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq c$
119	118	rexlimiva	$⊢ \exists b \in ℝ^{+} \forall m \in ℤ \|\sum_{n = 1}^{m} (\frac{R (n)}{n (n + 1)})\| \leq b \to \exists c \in ℝ^{+} \forall k \in ℕ \forall m \in ℤ \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq c$
120	2 119	ax-mp	$⊢ \exists c \in ℝ^{+} \forall k \in ℕ \forall m \in ℤ \|\sum_{n = k}^{m} (\frac{R (n)}{n (n + 1)})\| \leq c$

Metamath Proof Explorer

Theorem pntrsumbnd2

Proof