| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ssidd 4006 | . . . 4
⊢ (⊤
→ ℝ ⊆ ℝ) | 
| 2 |  | 1red 11263 | . . . 4
⊢ (⊤
→ 1 ∈ ℝ) | 
| 3 |  | fzfid 14015 | . . . . 5
⊢
((⊤ ∧ 𝑚
∈ ℝ) → (1...(⌊‘𝑚)) ∈ Fin) | 
| 4 |  | elfznn 13594 | . . . . . . 7
⊢ (𝑛 ∈
(1...(⌊‘𝑚))
→ 𝑛 ∈
ℕ) | 
| 5 | 4 | adantl 481 | . . . . . 6
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ 𝑛
∈ (1...(⌊‘𝑚))) → 𝑛 ∈ ℕ) | 
| 6 |  | nnrp 13047 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) | 
| 7 |  | pntrval.r | . . . . . . . . . . 11
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) | 
| 8 | 7 | pntrf 27608 | . . . . . . . . . 10
⊢ 𝑅:ℝ+⟶ℝ | 
| 9 | 8 | ffvelcdmi 7102 | . . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ (𝑅‘𝑛) ∈
ℝ) | 
| 10 | 6, 9 | syl 17 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝑅‘𝑛) ∈ ℝ) | 
| 11 |  | peano2nn 12279 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) | 
| 12 |  | nnmulcl 12291 | . . . . . . . . 9
⊢ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ) →
(𝑛 · (𝑛 + 1)) ∈
ℕ) | 
| 13 | 11, 12 | mpdan 687 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ → (𝑛 · (𝑛 + 1)) ∈ ℕ) | 
| 14 | 10, 13 | nndivred 12321 | . . . . . . 7
⊢ (𝑛 ∈ ℕ → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) | 
| 15 | 14 | recnd 11290 | . . . . . 6
⊢ (𝑛 ∈ ℕ → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) | 
| 16 | 5, 15 | syl 17 | . . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ 𝑛
∈ (1...(⌊‘𝑚))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) | 
| 17 | 3, 16 | fsumcl 15770 | . . . 4
⊢
((⊤ ∧ 𝑚
∈ ℝ) → Σ𝑛 ∈ (1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) | 
| 18 | 7 | pntrsumo1 27610 | . . . . 5
⊢ (𝑚 ∈ ℝ ↦
Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1) | 
| 19 | 18 | a1i 11 | . . . 4
⊢ (⊤
→ (𝑚 ∈ ℝ
↦ Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈
𝑂(1)) | 
| 20 |  | fzfid 14015 | . . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin) | 
| 21 |  | elfznn 13594 | . . . . . . . 8
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) | 
| 22 | 21 | adantl 481 | . . . . . . 7
⊢
(((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) | 
| 23 | 22, 15 | syl 17 | . . . . . 6
⊢
(((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) | 
| 24 | 23 | abscld 15476 | . . . . 5
⊢
(((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) | 
| 25 | 20, 24 | fsumrecl 15771 | . . . 4
⊢
((⊤ ∧ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) | 
| 26 | 17 | adantr 480 | . . . . . 6
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) | 
| 27 | 26 | abscld 15476 | . . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) | 
| 28 |  | fzfid 14015 | . . . . . 6
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (1...(⌊‘𝑚)) ∈ Fin) | 
| 29 | 16 | adantlr 715 | . . . . . . 7
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑚))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) | 
| 30 | 29 | abscld 15476 | . . . . . 6
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑚))) → (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) | 
| 31 | 28, 30 | fsumrecl 15771 | . . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑚))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) | 
| 32 | 25 | ad2ant2r 747 | . . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) | 
| 33 | 28, 29 | fsumabs 15838 | . . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑚))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) | 
| 34 |  | fzfid 14015 | . . . . . 6
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin) | 
| 35 | 21 | adantl 481 | . . . . . . . 8
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) | 
| 36 | 35, 15 | syl 17 | . . . . . . 7
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) | 
| 37 | 36 | abscld 15476 | . . . . . 6
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ ℝ) | 
| 38 | 36 | absge0d 15484 | . . . . . 6
⊢
((((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) | 
| 39 |  | simplr 768 | . . . . . . . 8
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → 𝑚 ∈ ℝ) | 
| 40 |  | simprll 778 | . . . . . . . 8
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → 𝑥 ∈ ℝ) | 
| 41 |  | simprr 772 | . . . . . . . . 9
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → 𝑚 < 𝑥) | 
| 42 | 39, 40, 41 | ltled 11410 | . . . . . . . 8
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → 𝑚 ≤ 𝑥) | 
| 43 |  | flword2 13854 | . . . . . . . 8
⊢ ((𝑚 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑚 ≤ 𝑥) → (⌊‘𝑥) ∈
(ℤ≥‘(⌊‘𝑚))) | 
| 44 | 39, 40, 42, 43 | syl3anc 1372 | . . . . . . 7
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (⌊‘𝑥) ∈
(ℤ≥‘(⌊‘𝑚))) | 
| 45 |  | fzss2 13605 | . . . . . . 7
⊢
((⌊‘𝑥)
∈ (ℤ≥‘(⌊‘𝑚)) → (1...(⌊‘𝑚)) ⊆
(1...(⌊‘𝑥))) | 
| 46 | 44, 45 | syl 17 | . . . . . 6
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (1...(⌊‘𝑚)) ⊆
(1...(⌊‘𝑥))) | 
| 47 | 34, 37, 38, 46 | fsumless 15833 | . . . . 5
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑚))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) | 
| 48 | 27, 31, 32, 33, 47 | letrd 11419 | . . . 4
⊢
(((⊤ ∧ 𝑚
∈ ℝ) ∧ ((𝑥
∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑚 < 𝑥)) → (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) | 
| 49 | 1, 2, 17, 19, 25, 48 | o1bddrp 15579 | . . 3
⊢ (⊤
→ ∃𝑐 ∈
ℝ+ ∀𝑚 ∈ ℝ (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) | 
| 50 | 49 | mptru 1546 | . 2
⊢
∃𝑐 ∈
ℝ+ ∀𝑚 ∈ ℝ (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 | 
| 51 |  | zre 12619 | . . . . . 6
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
ℝ) | 
| 52 | 51 | imim1i 63 | . . . . 5
⊢ ((𝑚 ∈ ℝ →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) → (𝑚 ∈ ℤ →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐)) | 
| 53 |  | flid 13849 | . . . . . . . . 9
⊢ (𝑚 ∈ ℤ →
(⌊‘𝑚) = 𝑚) | 
| 54 | 53 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑚 ∈ ℤ →
(1...(⌊‘𝑚)) =
(1...𝑚)) | 
| 55 | 54 | sumeq1d 15737 | . . . . . . 7
⊢ (𝑚 ∈ ℤ →
Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) | 
| 56 | 55 | fveq2d 6909 | . . . . . 6
⊢ (𝑚 ∈ ℤ →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) | 
| 57 | 56 | breq1d 5152 | . . . . 5
⊢ (𝑚 ∈ ℤ →
((abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 ↔ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐)) | 
| 58 | 52, 57 | mpbidi 241 | . . . 4
⊢ ((𝑚 ∈ ℝ →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) → (𝑚 ∈ ℤ →
(abs‘Σ𝑛 ∈
(1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐)) | 
| 59 | 58 | ralimi2 3077 | . . 3
⊢
(∀𝑚 ∈
ℝ (abs‘Σ𝑛
∈ (1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 → ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) | 
| 60 | 59 | reximi 3083 | . 2
⊢
(∃𝑐 ∈
ℝ+ ∀𝑚 ∈ ℝ (abs‘Σ𝑛 ∈
(1...(⌊‘𝑚))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 → ∃𝑐 ∈ ℝ+ ∀𝑚 ∈ ℤ
(abs‘Σ𝑛 ∈
(1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐) | 
| 61 | 50, 60 | ax-mp 5 | 1
⊢
∃𝑐 ∈
ℝ+ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 |