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	⊢ 𝑅 = ( 𝑎 ∈ ℝ⁺ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
	Assertion	pntrsumbnd2	⊢ ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑘 ∈ ℕ ∀ 𝑚 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 𝑘 ... 𝑚 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑐

Proof

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

Metamath Proof Explorer

Theorem pntrsumbnd2

Proof