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

Proof

Step	Hyp	Ref	Expression
1		pntrval.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ⁺ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2		ssidd	⊢ ( ⊤ → ℝ ⊆ ℝ )
3		1red	⊢ ( ⊤ → 1 ∈ ℝ )
4		fzfid	⊢ ( ( ⊤ ∧ 𝑚 ∈ ℝ ) → ( 1 ... ( ⌊ ‘ 𝑚 ) ) ∈ Fin )
5		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) → 𝑛 ∈ ℕ )
6	5	adantl	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → 𝑛 ∈ ℕ )
7		nnrp	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ⁺ )
8	1	pntrf	⊢ 𝑅 : ℝ⁺ ⟶ ℝ
9	8	ffvelcdmi	⊢ ( 𝑛 ∈ ℝ⁺ → ( 𝑅 ‘ 𝑛 ) ∈ ℝ )
10	7 9	syl	⊢ ( 𝑛 ∈ ℕ → ( 𝑅 ‘ 𝑛 ) ∈ ℝ )
11		peano2nn	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℕ )
12		nnmulcl	⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 + 1 ) ∈ ℕ ) → ( 𝑛 · ( 𝑛 + 1 ) ) ∈ ℕ )
13	11 12	mpdan	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 · ( 𝑛 + 1 ) ) ∈ ℕ )
14	10 13	nndivred	⊢ ( 𝑛 ∈ ℕ → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℝ )
15	14	recnd	⊢ ( 𝑛 ∈ ℕ → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℂ )
16	6 15	syl	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℂ )
17	4 16	fsumcl	⊢ ( ( ⊤ ∧ 𝑚 ∈ ℝ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℂ )
18	1	pntrsumo1	⊢ ( 𝑚 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ∈ 𝑂(1)
19	18	a1i	⊢ ( ⊤ → ( 𝑚 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ∈ 𝑂(1) )
20		fzfid	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
21		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
22	21	adantl	⊢ ( ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
23	22 15	syl	⊢ ( ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℂ )
24	23	abscld	⊢ ( ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ∈ ℝ )
25	20 24	fsumrecl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ∈ ℝ )
26	17	adantr	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℂ )
27	26	abscld	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ∈ ℝ )
28		fzfid	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑚 ) ) ∈ Fin )
29	16	adantlr	⊢ ( ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℂ )
30	29	abscld	⊢ ( ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ∈ ℝ )
31	28 30	fsumrecl	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ∈ ℝ )
32	25	ad2ant2r	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ∈ ℝ )
33	28 29	fsumabs	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
34		fzfid	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
35	21	adantl	⊢ ( ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
36	35 15	syl	⊢ ( ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℂ )
37	36	abscld	⊢ ( ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ∈ ℝ )
38	36	absge0d	⊢ ( ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
39		simplr	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) → 𝑚 ∈ ℝ )
40		simprll	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) → 𝑥 ∈ ℝ )
41		simprr	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) → 𝑚 < 𝑥 )
42	39 40 41	ltled	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) → 𝑚 ≤ 𝑥 )
43		flword2	⊢ ( ( 𝑚 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑚 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ( ℤ_≥ ‘ ( ⌊ ‘ 𝑚 ) ) )
44	39 40 42 43	syl3anc	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) → ( ⌊ ‘ 𝑥 ) ∈ ( ℤ_≥ ‘ ( ⌊ ‘ 𝑚 ) ) )
45		fzss2	⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ( ℤ_≥ ‘ ( ⌊ ‘ 𝑚 ) ) → ( 1 ... ( ⌊ ‘ 𝑚 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
46	44 45	syl	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑚 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
47	34 37 38 46	fsumless	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
48	27 31 32 33 47	letrd	⊢ ( ( ( ⊤ ∧ 𝑚 ∈ ℝ ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑚 < 𝑥 ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
49	2 3 17 19 25 48	o1bddrp	⊢ ( ⊤ → ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑚 ∈ ℝ ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑐 )
50	49	mptru	⊢ ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑚 ∈ ℝ ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑐
51		zre	⊢ ( 𝑚 ∈ ℤ → 𝑚 ∈ ℝ )
52	51	imim1i	⊢ ( ( 𝑚 ∈ ℝ → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑐 ) → ( 𝑚 ∈ ℤ → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑐 ) )
53		flid	⊢ ( 𝑚 ∈ ℤ → ( ⌊ ‘ 𝑚 ) = 𝑚 )
54	53	oveq2d	⊢ ( 𝑚 ∈ ℤ → ( 1 ... ( ⌊ ‘ 𝑚 ) ) = ( 1 ... 𝑚 ) )
55	54	sumeq1d	⊢ ( 𝑚 ∈ ℤ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) = Σ 𝑛 ∈ ( 1 ... 𝑚 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
56	55	fveq2d	⊢ ( 𝑚 ∈ ℤ → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) = ( abs ‘ Σ 𝑛 ∈ ( 1 ... 𝑚 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
57	56	breq1d	⊢ ( 𝑚 ∈ ℤ → ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑐 ↔ ( abs ‘ Σ 𝑛 ∈ ( 1 ... 𝑚 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑐 ) )
58	52 57	mpbidi	⊢ ( ( 𝑚 ∈ ℝ → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑐 ) → ( 𝑚 ∈ ℤ → ( abs ‘ Σ 𝑛 ∈ ( 1 ... 𝑚 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑐 ) )
59	58	ralimi2	⊢ ( ∀ 𝑚 ∈ ℝ ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑐 → ∀ 𝑚 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 1 ... 𝑚 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑐 )
60	59	reximi	⊢ ( ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑚 ∈ ℝ ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑚 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑐 → ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑚 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 1 ... 𝑚 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑐 )
61	50 60	ax-mp	⊢ ∃ 𝑐 ∈ ℝ⁺ ∀ 𝑚 ∈ ℤ ( abs ‘ Σ 𝑛 ∈ ( 1 ... 𝑚 ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ≤ 𝑐

Metamath Proof Explorer

Theorem pntrsumbnd

Proof