Step | Hyp | Ref
| Expression |
1 | | pntrval.r |
. . 3
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
2 | 1 | pntrsumbnd 25606 |
. 2
⊢
∃𝑏 ∈
ℝ+ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 |
3 | | 2rp 12078 |
. . . . . 6
⊢ 2 ∈
ℝ+ |
4 | | rpmulcl 12098 |
. . . . . 6
⊢ ((2
∈ ℝ+ ∧ 𝑏 ∈ ℝ+) → (2
· 𝑏) ∈
ℝ+) |
5 | 3, 4 | mpan 682 |
. . . . 5
⊢ (𝑏 ∈ ℝ+
→ (2 · 𝑏)
∈ ℝ+) |
6 | 5 | adantr 473 |
. . . 4
⊢ ((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → (2 · 𝑏) ∈
ℝ+) |
7 | | oveq2 6887 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑘 − 1) → (1...𝑚) = (1...(𝑘 − 1))) |
8 | 7 | sumeq1d 14771 |
. . . . . . . . 9
⊢ (𝑚 = (𝑘 − 1) → Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
9 | 8 | fveq2d 6416 |
. . . . . . . 8
⊢ (𝑚 = (𝑘 − 1) → (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
10 | 9 | breq1d 4854 |
. . . . . . 7
⊢ (𝑚 = (𝑘 − 1) → ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ↔ (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏)) |
11 | | simplr 786 |
. . . . . . 7
⊢ (((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) ∧ 𝑘 ∈ ℕ) → ∀𝑚 ∈ ℤ
(abs‘Σ𝑛 ∈
(1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) |
12 | | nnz 11688 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
13 | 12 | adantl 474 |
. . . . . . . 8
⊢ (((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ) |
14 | | peano2zm 11709 |
. . . . . . . 8
⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈
ℤ) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ (((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) ∧ 𝑘 ∈ ℕ) → (𝑘 − 1) ∈ ℤ) |
16 | 10, 11, 15 | rspcdva 3504 |
. . . . . 6
⊢ (((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) ∧ 𝑘 ∈ ℕ) →
(abs‘Σ𝑛 ∈
(1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) |
17 | 5 | ad2antrr 718 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ (2 · 𝑏)
∈ ℝ+) |
18 | 17 | rpge0d 12120 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ 0 ≤ (2 · 𝑏)) |
19 | | sumeq1 14759 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘...𝑚) = ∅ → Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = Σ𝑛 ∈ ∅ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
20 | | sum0 14792 |
. . . . . . . . . . . . . . . . . . 19
⊢
Σ𝑛 ∈
∅ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = 0 |
21 | 19, 20 | syl6eq 2850 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘...𝑚) = ∅ → Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = 0) |
22 | 21 | abs00bd 14371 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘...𝑚) = ∅ → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = 0) |
23 | 22 | breq1d 4854 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘...𝑚) = ∅ → ((abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏) ↔ 0 ≤ (2 · 𝑏))) |
24 | 18, 23 | syl5ibrcom 239 |
. . . . . . . . . . . . . . 15
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ ((𝑘...𝑚) = ∅ →
(abs‘Σ𝑛 ∈
(𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
25 | 24 | imp 396 |
. . . . . . . . . . . . . 14
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ (𝑘...𝑚) = ∅) →
(abs‘Σ𝑛 ∈
(𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏)) |
26 | 25 | a1d 25 |
. . . . . . . . . . . . 13
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ (𝑘...𝑚) = ∅) →
(((abs‘Σ𝑛
∈ (1...(𝑘 −
1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ∧ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
27 | | fzn0 12608 |
. . . . . . . . . . . . . 14
⊢ ((𝑘...𝑚) ≠ ∅ ↔ 𝑚 ∈ (ℤ≥‘𝑘)) |
28 | | fzfid 13026 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (1...𝑚) ∈ Fin) |
29 | | elfznn 12623 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ (1...𝑚) → 𝑛 ∈ ℕ) |
30 | | simpr 478 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
31 | 30 | nnrpd 12114 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ+) |
32 | 1 | pntrf 25603 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑅:ℝ+⟶ℝ |
33 | 32 | ffvelrni 6585 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ ℝ+
→ (𝑅‘𝑛) ∈
ℝ) |
34 | 31, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ ℕ) → (𝑅‘𝑛) ∈ ℝ) |
35 | 30 | peano2nnd 11332 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ) |
36 | 30, 35 | nnmulcld 11365 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ ℕ) → (𝑛 · (𝑛 + 1)) ∈ ℕ) |
37 | 34, 36 | nndivred 11366 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ ℕ) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
38 | 29, 37 | sylan2 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ (1...𝑚)) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
39 | 28, 38 | fsumrecl 14805 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
40 | 39 | recnd 10358 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
41 | 40 | abscld 14515 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
42 | | fzfid 13026 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (1...(𝑘 − 1)) ∈ Fin) |
43 | | elfznn 12623 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ (1...(𝑘 − 1)) → 𝑛 ∈ ℕ) |
44 | 43, 37 | sylan2 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ (1...(𝑘 − 1))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
45 | 42, 44 | fsumrecl 14805 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
46 | 45 | recnd 10358 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
47 | 46 | abscld 14515 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
48 | | simplll 792 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑏 ∈ ℝ+) |
49 | 48 | rpred 12116 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑏 ∈ ℝ) |
50 | | le2add 10803 |
. . . . . . . . . . . . . . . . 17
⊢
((((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ ∧
(abs‘Σ𝑛 ∈
(1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) ∧ (𝑏 ∈ ℝ ∧ 𝑏 ∈ ℝ)) →
(((abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ∧ (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ≤ (𝑏 + 𝑏))) |
51 | 41, 47, 49, 49, 50 | syl22anc 868 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ∧ (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ≤ (𝑏 + 𝑏))) |
52 | 49 | recnd 10358 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑏 ∈ ℂ) |
53 | 52 | 2timesd 11562 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (2 · 𝑏) = (𝑏 + 𝑏)) |
54 | 53 | breq2d 4856 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ≤ (2 · 𝑏) ↔ ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ≤ (𝑏 + 𝑏))) |
55 | | simpllr 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑘 ∈ ℕ) |
56 | 55 | nnred 11330 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑘 ∈ ℝ) |
57 | 56 | ltm1d 11249 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (𝑘 − 1) < 𝑘) |
58 | | fzdisj 12621 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 − 1) < 𝑘 → ((1...(𝑘 − 1)) ∩ (𝑘...𝑚)) = ∅) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → ((1...(𝑘 − 1)) ∩ (𝑘...𝑚)) = ∅) |
60 | 55 | nncnd 11331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑘 ∈ ℂ) |
61 | | ax-1cn 10283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 1 ∈
ℂ |
62 | | npcan 10583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 −
1) + 1) = 𝑘) |
63 | 60, 61, 62 | sylancl 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → ((𝑘 − 1) + 1) = 𝑘) |
64 | 63, 55 | eqeltrd 2879 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → ((𝑘 − 1) + 1) ∈
ℕ) |
65 | | nnuz 11966 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ℕ =
(ℤ≥‘1) |
66 | 64, 65 | syl6eleq 2889 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → ((𝑘 − 1) + 1) ∈
(ℤ≥‘1)) |
67 | 55 | nnzd 11770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑘 ∈ ℤ) |
68 | 67, 14 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (𝑘 − 1) ∈ ℤ) |
69 | | simplr 786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ 𝑘 ∈
ℕ) |
70 | 69 | nncnd 11331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ 𝑘 ∈
ℂ) |
71 | 70, 61, 62 | sylancl 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ ((𝑘 − 1) + 1)
= 𝑘) |
72 | 71 | fveq2d 6416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ (ℤ≥‘((𝑘 − 1) + 1)) =
(ℤ≥‘𝑘)) |
73 | 72 | eleq2d 2865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ (𝑚 ∈
(ℤ≥‘((𝑘 − 1) + 1)) ↔ 𝑚 ∈ (ℤ≥‘𝑘))) |
74 | 73 | biimpar 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑚 ∈ (ℤ≥‘((𝑘 − 1) +
1))) |
75 | | peano2uzr 11986 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑘 − 1) ∈ ℤ ∧
𝑚 ∈
(ℤ≥‘((𝑘 − 1) + 1))) → 𝑚 ∈ (ℤ≥‘(𝑘 − 1))) |
76 | 68, 74, 75 | syl2anc 580 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑚 ∈ (ℤ≥‘(𝑘 − 1))) |
77 | | fzsplit2 12619 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑘 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑚 ∈ (ℤ≥‘(𝑘 − 1))) → (1...𝑚) = ((1...(𝑘 − 1)) ∪ (((𝑘 − 1) + 1)...𝑚))) |
78 | 66, 76, 77 | syl2anc 580 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (1...𝑚) = ((1...(𝑘 − 1)) ∪ (((𝑘 − 1) + 1)...𝑚))) |
79 | 63 | oveq1d 6894 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (((𝑘 − 1) + 1)...𝑚) = (𝑘...𝑚)) |
80 | 79 | uneq2d 3966 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → ((1...(𝑘 − 1)) ∪ (((𝑘 − 1) + 1)...𝑚)) = ((1...(𝑘 − 1)) ∪ (𝑘...𝑚))) |
81 | 78, 80 | eqtrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (1...𝑚) = ((1...(𝑘 − 1)) ∪ (𝑘...𝑚))) |
82 | 38 | recnd 10358 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ (1...𝑚)) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
83 | 59, 81, 28, 82 | fsumsplit 14811 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = (Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) + Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
84 | 83 | oveq1d 6894 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) − Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = ((Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) + Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) − Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
85 | | fzfid 13026 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (𝑘...𝑚) ∈ Fin) |
86 | | elfzuz 12591 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ (𝑘...𝑚) → 𝑛 ∈ (ℤ≥‘𝑘)) |
87 | | eluznn 12002 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 ∈
(ℤ≥‘𝑘)) → 𝑛 ∈ ℕ) |
88 | 55, 86, 87 | syl2an 590 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ (𝑘...𝑚)) → 𝑛 ∈ ℕ) |
89 | 88, 37 | syldan 586 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ (𝑘...𝑚)) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
90 | 85, 89 | fsumrecl 14805 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
91 | 90 | recnd 10358 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
92 | 46, 91 | pncan2d 10687 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → ((Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) + Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) − Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
93 | 84, 92 | eqtrd 2834 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) − Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
94 | 93 | fveq2d 6416 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (abs‘(Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) − Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) = (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
95 | 40, 46 | abs2dif2d 14537 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (abs‘(Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) − Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ≤ ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))))) |
96 | 94, 95 | eqbrtrrd 4868 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))))) |
97 | 91 | abscld 14515 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
98 | 41, 47 | readdcld 10359 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ∈ ℝ) |
99 | | 2re 11386 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℝ |
100 | 99 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 2 ∈ ℝ) |
101 | 100, 49 | remulcld 10360 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (2 · 𝑏) ∈ ℝ) |
102 | | letr 10422 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((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 · 𝑏))) |
103 | 97, 98, 101, 102 | syl3anc 1491 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (((abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ∧ ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ≤ (2 · 𝑏)) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
104 | 96, 103 | mpand 687 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ≤ (2 · 𝑏) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
105 | 54, 104 | sylbird 252 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ≤ (𝑏 + 𝑏) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
106 | 51, 105 | syld 47 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ∧ (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
107 | 106 | ancomsd 458 |
. . . . . . . . . . . . . 14
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (((abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ∧ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
108 | 27, 107 | sylan2b 588 |
. . . . . . . . . . . . 13
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ (𝑘...𝑚) ≠ ∅) →
(((abs‘Σ𝑛
∈ (1...(𝑘 −
1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ∧ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
109 | 26, 108 | pm2.61dane 3059 |
. . . . . . . . . . . 12
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ (((abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ∧ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
110 | 109 | imp 396 |
. . . . . . . . . . 11
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ ((abs‘Σ𝑛
∈ (1...(𝑘 −
1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ∧ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏)) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏)) |
111 | 110 | an4s 651 |
. . . . . . . . . 10
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ (abs‘Σ𝑛
∈ (1...(𝑘 −
1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) ∧ (𝑚 ∈ ℤ ∧ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏)) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏)) |
112 | 111 | expr 449 |
. . . . . . . . 9
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ (abs‘Σ𝑛
∈ (1...(𝑘 −
1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) ∧ 𝑚 ∈ ℤ) →
((abs‘Σ𝑛 ∈
(1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
113 | 112 | ralimdva 3144 |
. . . . . . . 8
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ (abs‘Σ𝑛
∈ (1...(𝑘 −
1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → (∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 → ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
114 | 113 | impancom 444 |
. . . . . . 7
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → ((abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 → ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
115 | 114 | an32s 643 |
. . . . . 6
⊢ (((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) ∧ 𝑘 ∈ ℕ) →
((abs‘Σ𝑛 ∈
(1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 → ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
116 | 16, 115 | mpd 15 |
. . . . 5
⊢ (((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) ∧ 𝑘 ∈ ℕ) → ∀𝑚 ∈ ℤ
(abs‘Σ𝑛 ∈
(𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏)) |
117 | 116 | ralrimiva 3148 |
. . . 4
⊢ ((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → ∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏)) |
118 | | breq2 4848 |
. . . . . 6
⊢ (𝑐 = (2 · 𝑏) →
((abs‘Σ𝑛 ∈
(𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 ↔ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
119 | 118 | 2ralbidv 3171 |
. . . . 5
⊢ (𝑐 = (2 · 𝑏) → (∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ
(abs‘Σ𝑛 ∈
(𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 ↔ ∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
120 | 119 | rspcev 3498 |
. . . 4
⊢ (((2
· 𝑏) ∈
ℝ+ ∧ ∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏)) → ∃𝑐 ∈ ℝ+ ∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ
(abs‘Σ𝑛 ∈
(𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) |
121 | 6, 117, 120 | syl2anc 580 |
. . 3
⊢ ((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → ∃𝑐 ∈ ℝ+ ∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ
(abs‘Σ𝑛 ∈
(𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) |
122 | 121 | rexlimiva 3210 |
. 2
⊢
(∃𝑏 ∈
ℝ+ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 → ∃𝑐 ∈ ℝ+ ∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ
(abs‘Σ𝑛 ∈
(𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) |
123 | 2, 122 | ax-mp 5 |
1
⊢
∃𝑐 ∈
ℝ+ ∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 |