Step | Hyp | Ref
| Expression |
1 | | ssidd 3898 |
. . . 4
⊢ (⊤
→ ℝ ⊆ ℝ) |
2 | | 1red 10713 |
. . . 4
⊢ (⊤
→ 1 ∈ ℝ) |
3 | | fzfid 13425 |
. . . . 5
⊢
((⊤ ∧ 𝑚
∈ ℝ) → (1...(⌊‘𝑚)) ∈ Fin) |
4 | | elfznn 13020 |
. . . . . . 7
⊢ (𝑛 ∈
(1...(⌊‘𝑚))
→ 𝑛 ∈
ℕ) |
5 | 4 | adantl 485 |
. . . . . 6
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ 𝑛
∈ (1...(⌊‘𝑚))) → 𝑛 ∈ ℕ) |
6 | | nnrp 12476 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
7 | | pntrval.r |
. . . . . . . . . . 11
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
8 | 7 | pntrf 26291 |
. . . . . . . . . 10
⊢ 𝑅:ℝ+⟶ℝ |
9 | 8 | ffvelrni 6854 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ (𝑅‘𝑛) ∈
ℝ) |
10 | 6, 9 | syl 17 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝑅‘𝑛) ∈ ℝ) |
11 | | peano2nn 11721 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
12 | | nnmulcl 11733 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ) →
(𝑛 · (𝑛 + 1)) ∈
ℕ) |
13 | 11, 12 | mpdan 687 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝑛 · (𝑛 + 1)) ∈ ℕ) |
14 | 10, 13 | nndivred 11763 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
15 | 14 | recnd 10740 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
16 | 5, 15 | syl 17 |
. . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ 𝑛
∈ (1...(⌊‘𝑚))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
17 | 3, 16 | fsumcl 15176 |
. . . 4
⊢
((⊤ ∧ 𝑚
∈ ℝ) → Σ𝑛 ∈ (1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
18 | 7 | pntrsumo1 26293 |
. . . . 5
⊢ (𝑚 ∈ ℝ ↦
Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1) |
19 | 18 | a1i 11 |
. . . 4
⊢ (⊤
→ (𝑚 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈
𝑂(1)) |
20 | | fzfid 13425 |
. . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin) |
21 | | elfznn 13020 |
. . . . . . . 8
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
22 | 21 | adantl 485 |
. . . . . . 7
⊢
(((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
23 | 22, 15 | syl 17 |
. . . . . 6
⊢
(((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
24 | 23 | abscld 14879 |
. . . . 5
⊢
(((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
25 | 20, 24 | fsumrecl 15177 |
. . . 4
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
26 | 17 | adantr 484 |
. . . . . 6
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
27 | 26 | abscld 14879 |
. . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
28 | | fzfid 13425 |
. . . . . 6
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (1...(⌊‘𝑚)) ∈ Fin) |
29 | 16 | adantlr 715 |
. . . . . . 7
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑚))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
30 | 29 | abscld 14879 |
. . . . . 6
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑚))) → (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
31 | 28, 30 | fsumrecl 15177 |
. . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑚))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
32 | 25 | ad2ant2r 747 |
. . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
33 | 28, 29 | fsumabs 15242 |
. . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑚))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
34 | | fzfid 13425 |
. . . . . 6
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin) |
35 | 21 | adantl 485 |
. . . . . . . 8
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
36 | 35, 15 | syl 17 |
. . . . . . 7
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
37 | 36 | abscld 14879 |
. . . . . 6
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
38 | 36 | absge0d 14887 |
. . . . . 6
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
39 | | simplr 769 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → 𝑚 ∈ ℝ) |
40 | | simprll 779 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → 𝑥 ∈ ℝ) |
41 | | simprr 773 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → 𝑚 < 𝑥) |
42 | 39, 40, 41 | ltled 10859 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → 𝑚 ≤ 𝑥) |
43 | | flword2 13267 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑚 ≤ 𝑥) → (⌊‘𝑥) ∈
(ℤ≥‘(⌊‘𝑚))) |
44 | 39, 40, 42, 43 | syl3anc 1372 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (⌊‘𝑥) ∈
(ℤ≥‘(⌊‘𝑚))) |
45 | | fzss2 13031 |
. . . . . . 7
⊢
((⌊‘𝑥)
∈ (ℤ≥‘(⌊‘𝑚)) → (1...(⌊‘𝑚)) ⊆
(1...(⌊‘𝑥))) |
46 | 44, 45 | syl 17 |
. . . . . 6
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (1...(⌊‘𝑚)) ⊆
(1...(⌊‘𝑥))) |
47 | 34, 37, 38, 46 | fsumless 15237 |
. . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑚))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
48 | 27, 31, 32, 33, 47 | letrd 10868 |
. . . 4
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
49 | 1, 2, 17, 19, 25, 48 | o1bddrp 14982 |
. . 3
⊢ (⊤
→ ∃𝑐 ∈
ℝ+ ∀𝑚 ∈ ℝ (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) |
50 | 49 | mptru 1549 |
. 2
⊢
∃𝑐 ∈
ℝ+ ∀𝑚 ∈ ℝ (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 |
51 | | zre 12059 |
. . . . . 6
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
ℝ) |
52 | 51 | imim1i 63 |
. . . . 5
⊢ ((𝑚 ∈ ℝ →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) → (𝑚 ∈ ℤ →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐)) |
53 | | flid 13262 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℤ →
(⌊‘𝑚) = 𝑚) |
54 | 53 | oveq2d 7180 |
. . . . . . . 8
⊢ (𝑚 ∈ ℤ →
(1...(⌊‘𝑚)) =
(1...𝑚)) |
55 | 54 | sumeq1d 15144 |
. . . . . . 7
⊢ (𝑚 ∈ ℤ →
Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
56 | 55 | fveq2d 6672 |
. . . . . 6
⊢ (𝑚 ∈ ℤ →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
57 | 56 | breq1d 5037 |
. . . . 5
⊢ (𝑚 ∈ ℤ →
((abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 ↔ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐)) |
58 | 52, 57 | mpbidi 244 |
. . . 4
⊢ ((𝑚 ∈ ℝ →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) → (𝑚 ∈ ℤ →
(abs‘Σ𝑛 ∈
(1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐)) |
59 | 58 | ralimi2 3072 |
. . 3
⊢
(∀𝑚 ∈
ℝ (abs‘Σ𝑛
∈ (1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 → ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) |
60 | 59 | reximi 3156 |
. 2
⊢
(∃𝑐 ∈
ℝ+ ∀𝑚 ∈ ℝ (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 → ∃𝑐 ∈ ℝ+ ∀𝑚 ∈ ℤ
(abs‘Σ𝑛 ∈
(1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) |
61 | 50, 60 | ax-mp 5 |
1
⊢
∃𝑐 ∈
ℝ+ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 |