Step | Hyp | Ref
| Expression |
1 | | ssid 3587 |
. . . . 5
⊢ ℝ
⊆ ℝ |
2 | 1 | a1i 11 |
. . . 4
⊢ (⊤
→ ℝ ⊆ ℝ) |
3 | | 1red 9934 |
. . . 4
⊢ (⊤
→ 1 ∈ ℝ) |
4 | | fzfid 12634 |
. . . . 5
⊢
((⊤ ∧ 𝑚
∈ ℝ) → (1...(⌊‘𝑚)) ∈ Fin) |
5 | | elfznn 12241 |
. . . . . . 7
⊢ (𝑛 ∈
(1...(⌊‘𝑚))
→ 𝑛 ∈
ℕ) |
6 | 5 | adantl 481 |
. . . . . 6
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ 𝑛
∈ (1...(⌊‘𝑚))) → 𝑛 ∈ ℕ) |
7 | | nnrp 11718 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
8 | | pntrval.r |
. . . . . . . . . . 11
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
9 | 8 | pntrf 25052 |
. . . . . . . . . 10
⊢ 𝑅:ℝ+⟶ℝ |
10 | 9 | ffvelrni 6266 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ (𝑅‘𝑛) ∈
ℝ) |
11 | 7, 10 | syl 17 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝑅‘𝑛) ∈ ℝ) |
12 | | peano2nn 10909 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
13 | | nnmulcl 10920 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ) →
(𝑛 · (𝑛 + 1)) ∈
ℕ) |
14 | 12, 13 | mpdan 699 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝑛 · (𝑛 + 1)) ∈ ℕ) |
15 | 11, 14 | nndivred 10946 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
16 | 15 | recnd 9947 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
17 | 6, 16 | syl 17 |
. . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ 𝑛
∈ (1...(⌊‘𝑚))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
18 | 4, 17 | fsumcl 14311 |
. . . 4
⊢
((⊤ ∧ 𝑚
∈ ℝ) → Σ𝑛 ∈ (1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
19 | 8 | pntrsumo1 25054 |
. . . . 5
⊢ (𝑚 ∈ ℝ ↦
Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1) |
20 | 19 | a1i 11 |
. . . 4
⊢ (⊤
→ (𝑚 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈
𝑂(1)) |
21 | | fzfid 12634 |
. . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin) |
22 | | elfznn 12241 |
. . . . . . . 8
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
23 | 22 | adantl 481 |
. . . . . . 7
⊢
(((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
24 | 23, 16 | syl 17 |
. . . . . 6
⊢
(((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
25 | 24 | abscld 14023 |
. . . . 5
⊢
(((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
26 | 21, 25 | fsumrecl 14312 |
. . . 4
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
27 | 18 | adantr 480 |
. . . . . 6
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
28 | 27 | abscld 14023 |
. . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
29 | | fzfid 12634 |
. . . . . 6
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (1...(⌊‘𝑚)) ∈ Fin) |
30 | 17 | adantlr 747 |
. . . . . . 7
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑚))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
31 | 30 | abscld 14023 |
. . . . . 6
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑚))) → (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
32 | 29, 31 | fsumrecl 14312 |
. . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑚))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
33 | 26 | ad2ant2r 779 |
. . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
34 | 29, 30 | fsumabs 14374 |
. . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑚))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
35 | | fzfid 12634 |
. . . . . 6
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin) |
36 | 22 | adantl 481 |
. . . . . . . 8
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
37 | 36, 16 | syl 17 |
. . . . . . 7
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
38 | 37 | abscld 14023 |
. . . . . 6
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) |
39 | 37 | absge0d 14031 |
. . . . . 6
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
40 | | simplr 788 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → 𝑚 ∈ ℝ) |
41 | | simprll 798 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → 𝑥 ∈ ℝ) |
42 | | simprr 792 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → 𝑚 < 𝑥) |
43 | 40, 41, 42 | ltled 10064 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → 𝑚 ≤ 𝑥) |
44 | | flword2 12476 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑚 ≤ 𝑥) → (⌊‘𝑥) ∈
(ℤ≥‘(⌊‘𝑚))) |
45 | 40, 41, 43, 44 | syl3anc 1318 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (⌊‘𝑥) ∈
(ℤ≥‘(⌊‘𝑚))) |
46 | | fzss2 12252 |
. . . . . . 7
⊢
((⌊‘𝑥)
∈ (ℤ≥‘(⌊‘𝑚)) → (1...(⌊‘𝑚)) ⊆
(1...(⌊‘𝑥))) |
47 | 45, 46 | syl 17 |
. . . . . 6
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (1...(⌊‘𝑚)) ⊆
(1...(⌊‘𝑥))) |
48 | 35, 38, 39, 47 | fsumless 14369 |
. . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑚))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
49 | 28, 32, 33, 34, 48 | letrd 10073 |
. . . 4
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
50 | 2, 3, 18, 20, 26, 49 | o1bddrp 14121 |
. . 3
⊢ (⊤
→ ∃𝑐 ∈
ℝ+ ∀𝑚 ∈ ℝ (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) |
51 | 50 | trud 1484 |
. 2
⊢
∃𝑐 ∈
ℝ+ ∀𝑚 ∈ ℝ (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 |
52 | | zre 11258 |
. . . . . 6
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
ℝ) |
53 | 52 | imim1i 61 |
. . . . 5
⊢ ((𝑚 ∈ ℝ →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) → (𝑚 ∈ ℤ →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐)) |
54 | | flid 12471 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℤ →
(⌊‘𝑚) = 𝑚) |
55 | 54 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑚 ∈ ℤ →
(1...(⌊‘𝑚)) =
(1...𝑚)) |
56 | 55 | sumeq1d 14279 |
. . . . . . 7
⊢ (𝑚 ∈ ℤ →
Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
57 | 56 | fveq2d 6107 |
. . . . . 6
⊢ (𝑚 ∈ ℤ →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
58 | 57 | breq1d 4593 |
. . . . 5
⊢ (𝑚 ∈ ℤ →
((abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 ↔ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐)) |
59 | 53, 58 | mpbidi 230 |
. . . 4
⊢ ((𝑚 ∈ ℝ →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) → (𝑚 ∈ ℤ →
(abs‘Σ𝑛 ∈
(1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐)) |
60 | 59 | ralimi2 2933 |
. . 3
⊢
(∀𝑚 ∈
ℝ (abs‘Σ𝑛
∈ (1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 → ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) |
61 | 60 | reximi 2994 |
. 2
⊢
(∃𝑐 ∈
ℝ+ ∀𝑚 ∈ ℝ (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 → ∃𝑐 ∈ ℝ+ ∀𝑚 ∈ ℤ
(abs‘Σ𝑛 ∈
(1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) |
62 | 51, 61 | ax-mp 5 |
1
⊢
∃𝑐 ∈
ℝ+ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 |