Step | Hyp | Ref
| Expression |
1 | | pntrval.r |
. . 3
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
2 | 1 | pntrsumbnd 25255 |
. 2
⊢
∃𝑏 ∈
ℝ+ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 |
3 | | 2rp 11837 |
. . . . . 6
⊢ 2 ∈
ℝ+ |
4 | | rpmulcl 11855 |
. . . . . 6
⊢ ((2
∈ ℝ+ ∧ 𝑏 ∈ ℝ+) → (2
· 𝑏) ∈
ℝ+) |
5 | 3, 4 | mpan 706 |
. . . . 5
⊢ (𝑏 ∈ ℝ+
→ (2 · 𝑏)
∈ ℝ+) |
6 | 5 | adantr 481 |
. . . 4
⊢ ((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → (2 · 𝑏) ∈
ℝ+) |
7 | | nnz 11399 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
8 | 7 | adantl 482 |
. . . . . . . 8
⊢ (((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ) |
9 | | peano2zm 11420 |
. . . . . . . 8
⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈
ℤ) |
10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) ∧ 𝑘 ∈ ℕ) → (𝑘 − 1) ∈ ℤ) |
11 | | simplr 792 |
. . . . . . 7
⊢ (((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) ∧ 𝑘 ∈ ℕ) → ∀𝑚 ∈ ℤ
(abs‘Σ𝑛 ∈
(1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) |
12 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑘 − 1) → (1...𝑚) = (1...(𝑘 − 1))) |
13 | 12 | sumeq1d 14431 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑘 − 1) → Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
14 | 13 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑚 = (𝑘 − 1) → (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
15 | 14 | breq1d 4663 |
. . . . . . . 8
⊢ (𝑚 = (𝑘 − 1) → ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ↔ (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏)) |
16 | 15 | rspcv 3305 |
. . . . . . 7
⊢ ((𝑘 − 1) ∈ ℤ
→ (∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 → (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏)) |
17 | 10, 11, 16 | sylc 65 |
. . . . . 6
⊢ (((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) ∧ 𝑘 ∈ ℕ) →
(abs‘Σ𝑛 ∈
(1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) |
18 | 5 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ (2 · 𝑏)
∈ ℝ+) |
19 | 18 | rpge0d 11876 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ 0 ≤ (2 · 𝑏)) |
20 | | sumeq1 14419 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘...𝑚) = ∅ → Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = Σ𝑛 ∈ ∅ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
21 | | sum0 14452 |
. . . . . . . . . . . . . . . . . . 19
⊢
Σ𝑛 ∈
∅ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = 0 |
22 | 20, 21 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘...𝑚) = ∅ → Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = 0) |
23 | 22 | abs00bd 14031 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘...𝑚) = ∅ → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = 0) |
24 | 23 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘...𝑚) = ∅ → ((abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏) ↔ 0 ≤ (2 · 𝑏))) |
25 | 19, 24 | syl5ibrcom 237 |
. . . . . . . . . . . . . . 15
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ ((𝑘...𝑚) = ∅ →
(abs‘Σ𝑛 ∈
(𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
26 | 25 | imp 445 |
. . . . . . . . . . . . . 14
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ (𝑘...𝑚) = ∅) →
(abs‘Σ𝑛 ∈
(𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏)) |
27 | 26 | a1d 25 |
. . . . . . . . . . . . 13
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ (𝑘...𝑚) = ∅) →
(((abs‘Σ𝑛
∈ (1...(𝑘 −
1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ∧ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
28 | | fzn0 12355 |
. . . . . . . . . . . . . 14
⊢ ((𝑘...𝑚) ≠ ∅ ↔ 𝑚 ∈ (ℤ≥‘𝑘)) |
29 | | fzfid 12772 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (1...𝑚) ∈ Fin) |
30 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ (1...𝑚) → 𝑛 ∈ ℕ) |
31 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
32 | 31 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ+) |
33 | 1 | pntrf 25252 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑅:ℝ+⟶ℝ |
34 | 33 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ ℝ+
→ (𝑅‘𝑛) ∈
ℝ) |
35 | 32, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ ℕ) → (𝑅‘𝑛) ∈ ℝ) |
36 | 31 | peano2nnd 11037 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ) |
37 | 31, 36 | nnmulcld 11068 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ ℕ) → (𝑛 · (𝑛 + 1)) ∈ ℕ) |
38 | 35, 37 | nndivred 11069 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ ℕ) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
39 | 30, 38 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ (1...𝑚)) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
40 | 29, 39 | fsumrecl 14465 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
41 | 40 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
42 | 41 | abscld 14175 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
43 | | fzfid 12772 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (1...(𝑘 − 1)) ∈ Fin) |
44 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ (1...(𝑘 − 1)) → 𝑛 ∈ ℕ) |
45 | 44, 38 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ (1...(𝑘 − 1))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
46 | 43, 45 | fsumrecl 14465 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
47 | 46 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
48 | 47 | abscld 14175 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
49 | | simplll 798 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑏 ∈ ℝ+) |
50 | 49 | rpred 11872 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑏 ∈ ℝ) |
51 | | le2add 10510 |
. . . . . . . . . . . . . . . . 17
⊢
((((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ ∧
(abs‘Σ𝑛 ∈
(1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) ∧ (𝑏 ∈ ℝ ∧ 𝑏 ∈ ℝ)) →
(((abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ∧ (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ≤ (𝑏 + 𝑏))) |
52 | 42, 48, 50, 50, 51 | syl22anc 1327 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ∧ (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ≤ (𝑏 + 𝑏))) |
53 | 50 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑏 ∈ ℂ) |
54 | 53 | 2timesd 11275 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (2 · 𝑏) = (𝑏 + 𝑏)) |
55 | 54 | breq2d 4665 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ≤ (2 · 𝑏) ↔ ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ≤ (𝑏 + 𝑏))) |
56 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑘 ∈ ℕ) |
57 | 56 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑘 ∈ ℝ) |
58 | 57 | ltm1d 10956 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (𝑘 − 1) < 𝑘) |
59 | | fzdisj 12368 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 − 1) < 𝑘 → ((1...(𝑘 − 1)) ∩ (𝑘...𝑚)) = ∅) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → ((1...(𝑘 − 1)) ∩ (𝑘...𝑚)) = ∅) |
61 | 56 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑘 ∈ ℂ) |
62 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 1 ∈
ℂ |
63 | | npcan 10290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 −
1) + 1) = 𝑘) |
64 | 61, 62, 63 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → ((𝑘 − 1) + 1) = 𝑘) |
65 | 64, 56 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → ((𝑘 − 1) + 1) ∈
ℕ) |
66 | | nnuz 11723 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ℕ =
(ℤ≥‘1) |
67 | 65, 66 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → ((𝑘 − 1) + 1) ∈
(ℤ≥‘1)) |
68 | 56 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑘 ∈ ℤ) |
69 | 68, 9 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (𝑘 − 1) ∈ ℤ) |
70 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ 𝑘 ∈
ℕ) |
71 | 70 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ 𝑘 ∈
ℂ) |
72 | 71, 62, 63 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ ((𝑘 − 1) + 1)
= 𝑘) |
73 | 72 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ (ℤ≥‘((𝑘 − 1) + 1)) =
(ℤ≥‘𝑘)) |
74 | 73 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ (𝑚 ∈
(ℤ≥‘((𝑘 − 1) + 1)) ↔ 𝑚 ∈ (ℤ≥‘𝑘))) |
75 | 74 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑚 ∈ (ℤ≥‘((𝑘 − 1) +
1))) |
76 | | peano2uzr 11743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑘 − 1) ∈ ℤ ∧
𝑚 ∈
(ℤ≥‘((𝑘 − 1) + 1))) → 𝑚 ∈ (ℤ≥‘(𝑘 − 1))) |
77 | 69, 75, 76 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 𝑚 ∈ (ℤ≥‘(𝑘 − 1))) |
78 | | fzsplit2 12366 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑘 − 1) + 1) ∈
(ℤ≥‘1) ∧ 𝑚 ∈ (ℤ≥‘(𝑘 − 1))) → (1...𝑚) = ((1...(𝑘 − 1)) ∪ (((𝑘 − 1) + 1)...𝑚))) |
79 | 67, 77, 78 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (1...𝑚) = ((1...(𝑘 − 1)) ∪ (((𝑘 − 1) + 1)...𝑚))) |
80 | 64 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (((𝑘 − 1) + 1)...𝑚) = (𝑘...𝑚)) |
81 | 80 | uneq2d 3767 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → ((1...(𝑘 − 1)) ∪ (((𝑘 − 1) + 1)...𝑚)) = ((1...(𝑘 − 1)) ∪ (𝑘...𝑚))) |
82 | 79, 81 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (1...𝑚) = ((1...(𝑘 − 1)) ∪ (𝑘...𝑚))) |
83 | 39 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ (1...𝑚)) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
84 | 60, 82, 29, 83 | fsumsplit 14471 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = (Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) + Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
85 | 84 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) − Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = ((Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) + Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) − Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
86 | | fzfid 12772 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (𝑘...𝑚) ∈ Fin) |
87 | | elfzuz 12338 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ (𝑘...𝑚) → 𝑛 ∈ (ℤ≥‘𝑘)) |
88 | | eluznn 11758 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑘 ∈ ℕ ∧ 𝑛 ∈
(ℤ≥‘𝑘)) → 𝑛 ∈ ℕ) |
89 | 56, 87, 88 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ (𝑘...𝑚)) → 𝑛 ∈ ℕ) |
90 | 89, 38 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑏 ∈
ℝ+ ∧ 𝑘
∈ ℕ) ∧ 𝑚
∈ ℤ) ∧ 𝑚
∈ (ℤ≥‘𝑘)) ∧ 𝑛 ∈ (𝑘...𝑚)) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
91 | 86, 90 | fsumrecl 14465 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
92 | 91 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
93 | 47, 92 | pncan2d 10394 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → ((Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) + Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) − Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
94 | 85, 93 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) − Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
95 | 94 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (abs‘(Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) − Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) = (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
96 | 41, 47 | abs2dif2d 14197 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (abs‘(Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) − Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ≤ ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))))) |
97 | 95, 96 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))))) |
98 | 92 | abscld 14175 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
99 | 42, 48 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ∈ ℝ) |
100 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℝ |
101 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → 2 ∈ ℝ) |
102 | 101, 50 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (2 · 𝑏) ∈ ℝ) |
103 | | letr 10131 |
. . . . . . . . . . . . . . . . . . 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 · 𝑏))) |
104 | 98, 99, 102, 103 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (((abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ∧ ((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ≤ (2 · 𝑏)) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
105 | 97, 104 | mpand 711 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ≤ (2 · 𝑏) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
106 | 55, 105 | sylbird 250 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) + (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) ≤ (𝑏 + 𝑏) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
107 | 52, 106 | syld 47 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (((abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ∧ (abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
108 | 107 | ancomsd 470 |
. . . . . . . . . . . . . 14
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ 𝑚 ∈
(ℤ≥‘𝑘)) → (((abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ∧ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
109 | 28, 108 | sylan2b 492 |
. . . . . . . . . . . . 13
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ (𝑘...𝑚) ≠ ∅) →
(((abs‘Σ𝑛
∈ (1...(𝑘 −
1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ∧ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
110 | 27, 109 | pm2.61dane 2881 |
. . . . . . . . . . . 12
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
→ (((abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ∧ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
111 | 110 | imp 445 |
. . . . . . . . . . 11
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ 𝑚 ∈ ℤ)
∧ ((abs‘Σ𝑛
∈ (1...(𝑘 −
1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 ∧ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏)) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏)) |
112 | 111 | an4s 869 |
. . . . . . . . . 10
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ (abs‘Σ𝑛
∈ (1...(𝑘 −
1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) ∧ (𝑚 ∈ ℤ ∧ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏)) → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏)) |
113 | 112 | expr 643 |
. . . . . . . . 9
⊢ ((((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ (abs‘Σ𝑛
∈ (1...(𝑘 −
1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) ∧ 𝑚 ∈ ℤ) →
((abs‘Σ𝑛 ∈
(1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 → (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
114 | 113 | ralimdva 2962 |
. . . . . . . 8
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ (abs‘Σ𝑛
∈ (1...(𝑘 −
1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → (∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 → ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
115 | 114 | impancom 456 |
. . . . . . 7
⊢ (((𝑏 ∈ ℝ+
∧ 𝑘 ∈ ℕ)
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → ((abs‘Σ𝑛 ∈ (1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 → ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
116 | 115 | an32s 846 |
. . . . . 6
⊢ (((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) ∧ 𝑘 ∈ ℕ) →
((abs‘Σ𝑛 ∈
(1...(𝑘 − 1))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 → ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
117 | 17, 116 | mpd 15 |
. . . . 5
⊢ (((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) ∧ 𝑘 ∈ ℕ) → ∀𝑚 ∈ ℤ
(abs‘Σ𝑛 ∈
(𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏)) |
118 | 117 | ralrimiva 2966 |
. . . 4
⊢ ((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → ∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏)) |
119 | | breq2 4657 |
. . . . . 6
⊢ (𝑐 = (2 · 𝑏) →
((abs‘Σ𝑛 ∈
(𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 ↔ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
120 | 119 | 2ralbidv 2989 |
. . . . 5
⊢ (𝑐 = (2 · 𝑏) → (∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ
(abs‘Σ𝑛 ∈
(𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 ↔ ∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏))) |
121 | 120 | rspcev 3309 |
. . . 4
⊢ (((2
· 𝑏) ∈
ℝ+ ∧ ∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ (2 · 𝑏)) → ∃𝑐 ∈ ℝ+ ∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ
(abs‘Σ𝑛 ∈
(𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) |
122 | 6, 118, 121 | syl2anc 693 |
. . 3
⊢ ((𝑏 ∈ ℝ+
∧ ∀𝑚 ∈
ℤ (abs‘Σ𝑛
∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏) → ∃𝑐 ∈ ℝ+ ∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ
(abs‘Σ𝑛 ∈
(𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) |
123 | 122 | rexlimiva 3028 |
. 2
⊢
(∃𝑏 ∈
ℝ+ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑏 → ∃𝑐 ∈ ℝ+ ∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ
(abs‘Σ𝑛 ∈
(𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) |
124 | 2, 123 | ax-mp 5 |
1
⊢
∃𝑐 ∈
ℝ+ ∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 |