Metamath Proof Explorer

Theorem 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 ) ) ) ) ≤ 𝑐