| Step | Hyp | Ref
| Expression |
| 1 | | fzfid 14014 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) → (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) ∈ Fin) |
| 2 | | ioossre 13448 |
. . . . . . . . . . . . . 14
⊢ (𝑋(,)+∞) ⊆
ℝ |
| 3 | | pntpbnd1.y |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ∈ (𝑋(,)+∞)) |
| 4 | 2, 3 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ∈ ℝ) |
| 5 | | 0red 11264 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ∈
ℝ) |
| 6 | | pntpbnd1.x |
. . . . . . . . . . . . . . . 16
⊢ 𝑋 = (exp‘(2 / 𝐸)) |
| 7 | | 2re 12340 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
| 8 | | ioossre 13448 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0(,)1)
⊆ ℝ |
| 9 | | pntpbnd1.e |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐸 ∈ (0(,)1)) |
| 10 | 8, 9 | sselid 3981 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐸 ∈ ℝ) |
| 11 | | eliooord 13446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐸 ∈ (0(,)1) → (0 <
𝐸 ∧ 𝐸 < 1)) |
| 12 | 9, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1)) |
| 13 | 12 | simpld 494 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 < 𝐸) |
| 14 | 10, 13 | elrpd 13074 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
| 15 | | rerpdivcl 13065 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℝ ∧ 𝐸
∈ ℝ+) → (2 / 𝐸) ∈ ℝ) |
| 16 | 7, 14, 15 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 / 𝐸) ∈ ℝ) |
| 17 | 16 | reefcld 16124 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (exp‘(2 / 𝐸)) ∈
ℝ) |
| 18 | 6, 17 | eqeltrid 2845 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 19 | | efgt0 16139 |
. . . . . . . . . . . . . . . . 17
⊢ ((2 /
𝐸) ∈ ℝ → 0
< (exp‘(2 / 𝐸))) |
| 20 | 16, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 < (exp‘(2 /
𝐸))) |
| 21 | 20, 6 | breqtrrdi 5185 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 < 𝑋) |
| 22 | | eliooord 13446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑌 ∈ (𝑋(,)+∞) → (𝑋 < 𝑌 ∧ 𝑌 < +∞)) |
| 23 | 3, 22 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑋 < 𝑌 ∧ 𝑌 < +∞)) |
| 24 | 23 | simpld 494 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 < 𝑌) |
| 25 | 5, 18, 4, 21, 24 | lttrd 11422 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝑌) |
| 26 | 5, 4, 25 | ltled 11409 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ 𝑌) |
| 27 | | flge0nn0 13860 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ∈ ℝ ∧ 0 ≤
𝑌) →
(⌊‘𝑌) ∈
ℕ0) |
| 28 | 4, 26, 27 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⌊‘𝑌) ∈
ℕ0) |
| 29 | | nn0p1nn 12565 |
. . . . . . . . . . . 12
⊢
((⌊‘𝑌)
∈ ℕ0 → ((⌊‘𝑌) + 1) ∈ ℕ) |
| 30 | 28, 29 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((⌊‘𝑌) + 1) ∈
ℕ) |
| 31 | | elfzuz 13560 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → 𝑛 ∈
(ℤ≥‘((⌊‘𝑌) + 1))) |
| 32 | | eluznn 12960 |
. . . . . . . . . . 11
⊢
((((⌊‘𝑌)
+ 1) ∈ ℕ ∧ 𝑛
∈ (ℤ≥‘((⌊‘𝑌) + 1))) → 𝑛 ∈ ℕ) |
| 33 | 30, 31, 32 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℕ) |
| 34 | 33 | nnrpd 13075 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℝ+) |
| 35 | | pntpbnd.r |
. . . . . . . . . . 11
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
| 36 | 35 | pntrf 27607 |
. . . . . . . . . 10
⊢ 𝑅:ℝ+⟶ℝ |
| 37 | 36 | ffvelcdmi 7103 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ (𝑅‘𝑛) ∈
ℝ) |
| 38 | 34, 37 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑛) ∈ ℝ) |
| 39 | 33 | peano2nnd 12283 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈ ℕ) |
| 40 | 33, 39 | nnmulcld 12319 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ∈ ℕ) |
| 41 | 38, 40 | nndivred 12320 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
| 42 | 41 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
| 43 | 1, 42 | fsumrecl 15770 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
| 44 | 38 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑛) ∈ ℝ) |
| 45 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑛 → (𝑅‘𝑖) = (𝑅‘𝑛)) |
| 46 | 45 | breq2d 5155 |
. . . . . . . . 9
⊢ (𝑖 = 𝑛 → (0 ≤ (𝑅‘𝑖) ↔ 0 ≤ (𝑅‘𝑛))) |
| 47 | 46 | rspccva 3621 |
. . . . . . . 8
⊢
((∀𝑖 ∈
(((⌊‘𝑌) +
1)...(⌊‘(𝐾
· 𝑌)))0 ≤ (𝑅‘𝑖) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 0 ≤ (𝑅‘𝑛)) |
| 48 | 47 | adantll 714 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 0 ≤ (𝑅‘𝑛)) |
| 49 | 40 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ∈ ℕ) |
| 50 | 49 | nnred 12281 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ∈ ℝ) |
| 51 | 49 | nngt0d 12315 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 0 < (𝑛 · (𝑛 + 1))) |
| 52 | | divge0 12137 |
. . . . . . 7
⊢ ((((𝑅‘𝑛) ∈ ℝ ∧ 0 ≤ (𝑅‘𝑛)) ∧ ((𝑛 · (𝑛 + 1)) ∈ ℝ ∧ 0 < (𝑛 · (𝑛 + 1)))) → 0 ≤ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 53 | 44, 48, 50, 51, 52 | syl22anc 839 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 0 ≤ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 54 | 1, 42, 53 | fsumge0 15831 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) → 0 ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 55 | 43, 54 | absidd 15461 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) → (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 56 | 42, 53 | absidd 15461 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 57 | 56 | sumeq2dv 15738 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 58 | 55, 57 | eqtr4d 2780 |
. . 3
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) → (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
| 59 | | fzfid 14014 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) ∈ Fin) |
| 60 | 41 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
| 61 | 60 | recnd 11289 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
| 62 | 59, 61 | fsumneg 15823 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))-((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = -Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 63 | 38 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑛) ∈ ℝ) |
| 64 | 63 | renegcld 11690 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → -(𝑅‘𝑛) ∈ ℝ) |
| 65 | 45 | breq1d 5153 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑛 → ((𝑅‘𝑖) ≤ 0 ↔ (𝑅‘𝑛) ≤ 0)) |
| 66 | 65 | rspccva 3621 |
. . . . . . . . . . 11
⊢
((∀𝑖 ∈
(((⌊‘𝑌) +
1)...(⌊‘(𝐾
· 𝑌)))(𝑅‘𝑖) ≤ 0 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑛) ≤ 0) |
| 67 | 66 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑛) ≤ 0) |
| 68 | 63 | le0neg1d 11834 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) ≤ 0 ↔ 0 ≤ -(𝑅‘𝑛))) |
| 69 | 67, 68 | mpbid 232 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 0 ≤ -(𝑅‘𝑛)) |
| 70 | 40 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ∈ ℕ) |
| 71 | 70 | nnred 12281 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ∈ ℝ) |
| 72 | 70 | nngt0d 12315 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 0 < (𝑛 · (𝑛 + 1))) |
| 73 | | divge0 12137 |
. . . . . . . . 9
⊢
(((-(𝑅‘𝑛) ∈ ℝ ∧ 0 ≤
-(𝑅‘𝑛)) ∧ ((𝑛 · (𝑛 + 1)) ∈ ℝ ∧ 0 < (𝑛 · (𝑛 + 1)))) → 0 ≤ (-(𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 74 | 64, 69, 71, 72, 73 | syl22anc 839 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 0 ≤ (-(𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 75 | 38 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑛) ∈ ℂ) |
| 76 | 40 | nncnd 12282 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ∈ ℂ) |
| 77 | 40 | nnne0d 12316 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ≠ 0) |
| 78 | 75, 76, 77 | divnegd 12056 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = (-(𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 79 | 78 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = (-(𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 80 | 74, 79 | breqtrrd 5171 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 0 ≤ -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 81 | 60 | le0neg1d 11834 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ≤ 0 ↔ 0 ≤ -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
| 82 | 80, 81 | mpbird 257 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ≤ 0) |
| 83 | 60, 82 | absnidd 15452 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 84 | 83 | sumeq2dv 15738 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))-((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 85 | 59, 60 | fsumrecl 15770 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
| 86 | 60 | renegcld 11690 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
| 87 | 59, 86, 80 | fsumge0 15831 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → 0 ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))-((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 88 | 87, 62 | breqtrd 5169 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → 0 ≤ -Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 89 | 85 | le0neg1d 11834 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → (Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ≤ 0 ↔ 0 ≤ -Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
| 90 | 88, 89 | mpbird 257 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ≤ 0) |
| 91 | 85, 90 | absnidd 15452 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = -Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 92 | 62, 84, 91 | 3eqtr4rd 2788 |
. . 3
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
| 93 | | pntpbnd1.c |
. . . . . . . . . . . . 13
⊢ 𝐶 = (𝐴 + 2) |
| 94 | | pntpbnd1.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
| 95 | | 2rp 13039 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ+ |
| 96 | | rpaddcl 13057 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ+
∧ 2 ∈ ℝ+) → (𝐴 + 2) ∈
ℝ+) |
| 97 | 94, 95, 96 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 + 2) ∈
ℝ+) |
| 98 | 93, 97 | eqeltrid 2845 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
| 99 | 98, 14 | rpdivcld 13094 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶 / 𝐸) ∈
ℝ+) |
| 100 | 99 | rpred 13077 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 / 𝐸) ∈ ℝ) |
| 101 | 100 | reefcld 16124 |
. . . . . . . . 9
⊢ (𝜑 → (exp‘(𝐶 / 𝐸)) ∈ ℝ) |
| 102 | | pnfxr 11315 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
| 103 | | icossre 13468 |
. . . . . . . . 9
⊢
(((exp‘(𝐶 /
𝐸)) ∈ ℝ ∧
+∞ ∈ ℝ*) → ((exp‘(𝐶 / 𝐸))[,)+∞) ⊆
ℝ) |
| 104 | 101, 102,
103 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → ((exp‘(𝐶 / 𝐸))[,)+∞) ⊆
ℝ) |
| 105 | | pntpbnd1.k |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) |
| 106 | 104, 105 | sseldd 3984 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℝ) |
| 107 | 106, 4 | remulcld 11291 |
. . . . . 6
⊢ (𝜑 → (𝐾 · 𝑌) ∈ ℝ) |
| 108 | 4 | recnd 11289 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ ℂ) |
| 109 | 108 | mullidd 11279 |
. . . . . . . 8
⊢ (𝜑 → (1 · 𝑌) = 𝑌) |
| 110 | | 1red 11262 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
| 111 | | efgt1 16152 |
. . . . . . . . . . 11
⊢ ((𝐶 / 𝐸) ∈ ℝ+ → 1 <
(exp‘(𝐶 / 𝐸))) |
| 112 | 99, 111 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 1 < (exp‘(𝐶 / 𝐸))) |
| 113 | | elicopnf 13485 |
. . . . . . . . . . . . 13
⊢
((exp‘(𝐶 /
𝐸)) ∈ ℝ →
(𝐾 ∈
((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝐾 ∈ ℝ ∧
(exp‘(𝐶 / 𝐸)) ≤ 𝐾))) |
| 114 | 101, 113 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝐾 ∈ ℝ ∧ (exp‘(𝐶 / 𝐸)) ≤ 𝐾))) |
| 115 | 114 | simplbda 499 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (exp‘(𝐶 / 𝐸)) ≤ 𝐾) |
| 116 | 105, 115 | mpdan 687 |
. . . . . . . . . 10
⊢ (𝜑 → (exp‘(𝐶 / 𝐸)) ≤ 𝐾) |
| 117 | 110, 101,
106, 112, 116 | ltletrd 11421 |
. . . . . . . . 9
⊢ (𝜑 → 1 < 𝐾) |
| 118 | | ltmul1 12117 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ 𝐾
∈ ℝ ∧ (𝑌
∈ ℝ ∧ 0 < 𝑌)) → (1 < 𝐾 ↔ (1 · 𝑌) < (𝐾 · 𝑌))) |
| 119 | 110, 106,
4, 25, 118 | syl112anc 1376 |
. . . . . . . . 9
⊢ (𝜑 → (1 < 𝐾 ↔ (1 · 𝑌) < (𝐾 · 𝑌))) |
| 120 | 117, 119 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → (1 · 𝑌) < (𝐾 · 𝑌)) |
| 121 | 109, 120 | eqbrtrrd 5167 |
. . . . . . 7
⊢ (𝜑 → 𝑌 < (𝐾 · 𝑌)) |
| 122 | 4, 107, 121 | ltled 11409 |
. . . . . 6
⊢ (𝜑 → 𝑌 ≤ (𝐾 · 𝑌)) |
| 123 | | flword2 13853 |
. . . . . 6
⊢ ((𝑌 ∈ ℝ ∧ (𝐾 · 𝑌) ∈ ℝ ∧ 𝑌 ≤ (𝐾 · 𝑌)) → (⌊‘(𝐾 · 𝑌)) ∈
(ℤ≥‘(⌊‘𝑌))) |
| 124 | 4, 107, 122, 123 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈
(ℤ≥‘(⌊‘𝑌))) |
| 125 | 107 | flcld 13838 |
. . . . . 6
⊢ (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈ ℤ) |
| 126 | | uzid 12893 |
. . . . . 6
⊢
((⌊‘(𝐾
· 𝑌)) ∈ ℤ
→ (⌊‘(𝐾
· 𝑌)) ∈
(ℤ≥‘(⌊‘(𝐾 · 𝑌)))) |
| 127 | 125, 126 | syl 17 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈
(ℤ≥‘(⌊‘(𝐾 · 𝑌)))) |
| 128 | | elfzuzb 13558 |
. . . . 5
⊢
((⌊‘(𝐾
· 𝑌)) ∈
((⌊‘𝑌)...(⌊‘(𝐾 · 𝑌))) ↔ ((⌊‘(𝐾 · 𝑌)) ∈
(ℤ≥‘(⌊‘𝑌)) ∧ (⌊‘(𝐾 · 𝑌)) ∈
(ℤ≥‘(⌊‘(𝐾 · 𝑌))))) |
| 129 | 124, 127,
128 | sylanbrc 583 |
. . . 4
⊢ (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈ ((⌊‘𝑌)...(⌊‘(𝐾 · 𝑌)))) |
| 130 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = (⌊‘𝑌) → (((⌊‘𝑌) + 1)...𝑥) = (((⌊‘𝑌) + 1)...(⌊‘𝑌))) |
| 131 | 130 | raleqdv 3326 |
. . . . . . 7
⊢ (𝑥 = (⌊‘𝑌) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ↔ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))0 ≤ (𝑅‘𝑖))) |
| 132 | 130 | raleqdv 3326 |
. . . . . . 7
⊢ (𝑥 = (⌊‘𝑌) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0 ↔ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))(𝑅‘𝑖) ≤ 0)) |
| 133 | 131, 132 | orbi12d 919 |
. . . . . 6
⊢ (𝑥 = (⌊‘𝑌) → ((∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0) ↔ (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))(𝑅‘𝑖) ≤ 0))) |
| 134 | 133 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = (⌊‘𝑌) → ((𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0)) ↔ (𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))(𝑅‘𝑖) ≤ 0)))) |
| 135 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝑚 → (((⌊‘𝑌) + 1)...𝑥) = (((⌊‘𝑌) + 1)...𝑚)) |
| 136 | 135 | raleqdv 3326 |
. . . . . . 7
⊢ (𝑥 = 𝑚 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ↔ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖))) |
| 137 | 135 | raleqdv 3326 |
. . . . . . 7
⊢ (𝑥 = 𝑚 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0 ↔ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0)) |
| 138 | 136, 137 | orbi12d 919 |
. . . . . 6
⊢ (𝑥 = 𝑚 → ((∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0) ↔ (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0))) |
| 139 | 138 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = 𝑚 → ((𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0)) ↔ (𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0)))) |
| 140 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = (𝑚 + 1) → (((⌊‘𝑌) + 1)...𝑥) = (((⌊‘𝑌) + 1)...(𝑚 + 1))) |
| 141 | 140 | raleqdv 3326 |
. . . . . . 7
⊢ (𝑥 = (𝑚 + 1) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ↔ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖))) |
| 142 | 140 | raleqdv 3326 |
. . . . . . 7
⊢ (𝑥 = (𝑚 + 1) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0 ↔ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0)) |
| 143 | 141, 142 | orbi12d 919 |
. . . . . 6
⊢ (𝑥 = (𝑚 + 1) → ((∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0) ↔ (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0))) |
| 144 | 143 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = (𝑚 + 1) → ((𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0)) ↔ (𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0)))) |
| 145 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = (⌊‘(𝐾 · 𝑌)) → (((⌊‘𝑌) + 1)...𝑥) = (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) |
| 146 | 145 | raleqdv 3326 |
. . . . . . 7
⊢ (𝑥 = (⌊‘(𝐾 · 𝑌)) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ↔ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖))) |
| 147 | 145 | raleqdv 3326 |
. . . . . . 7
⊢ (𝑥 = (⌊‘(𝐾 · 𝑌)) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0 ↔ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0)) |
| 148 | 146, 147 | orbi12d 919 |
. . . . . 6
⊢ (𝑥 = (⌊‘(𝐾 · 𝑌)) → ((∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0) ↔ (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0))) |
| 149 | 148 | imbi2d 340 |
. . . . 5
⊢ (𝑥 = (⌊‘(𝐾 · 𝑌)) → ((𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0)) ↔ (𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0)))) |
| 150 | | elfzle3 13570 |
. . . . . . . . 9
⊢ (𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌)) → ((⌊‘𝑌) + 1) ≤ (⌊‘𝑌)) |
| 151 | | elfzel2 13562 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌)) → (⌊‘𝑌) ∈
ℤ) |
| 152 | 151 | zred 12722 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌)) → (⌊‘𝑌) ∈
ℝ) |
| 153 | 152 | ltp1d 12198 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌)) → (⌊‘𝑌) < ((⌊‘𝑌) + 1)) |
| 154 | | peano2re 11434 |
. . . . . . . . . . . 12
⊢
((⌊‘𝑌)
∈ ℝ → ((⌊‘𝑌) + 1) ∈ ℝ) |
| 155 | 152, 154 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌)) → ((⌊‘𝑌) + 1) ∈
ℝ) |
| 156 | 152, 155 | ltnled 11408 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌)) → ((⌊‘𝑌) < ((⌊‘𝑌) + 1) ↔ ¬
((⌊‘𝑌) + 1)
≤ (⌊‘𝑌))) |
| 157 | 153, 156 | mpbid 232 |
. . . . . . . . 9
⊢ (𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌)) → ¬
((⌊‘𝑌) + 1)
≤ (⌊‘𝑌)) |
| 158 | 150, 157 | pm2.21dd 195 |
. . . . . . . 8
⊢ (𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌)) → (𝑅‘𝑖) ≤ 0) |
| 159 | 158 | rgen 3063 |
. . . . . . 7
⊢
∀𝑖 ∈
(((⌊‘𝑌) +
1)...(⌊‘𝑌))(𝑅‘𝑖) ≤ 0 |
| 160 | 159 | olci 867 |
. . . . . 6
⊢
(∀𝑖 ∈
(((⌊‘𝑌) +
1)...(⌊‘𝑌))0
≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))(𝑅‘𝑖) ≤ 0) |
| 161 | 160 | 2a1i 12 |
. . . . 5
⊢
((⌊‘(𝐾
· 𝑌)) ∈
(ℤ≥‘(⌊‘𝑌)) → (𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))(𝑅‘𝑖) ≤ 0))) |
| 162 | | elfzofz 13715 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ((⌊‘𝑌)..^(⌊‘(𝐾 · 𝑌))) → 𝑚 ∈ ((⌊‘𝑌)...(⌊‘(𝐾 · 𝑌)))) |
| 163 | | elfzp12 13643 |
. . . . . . . . . . 11
⊢
((⌊‘(𝐾
· 𝑌)) ∈
(ℤ≥‘(⌊‘𝑌)) → (𝑚 ∈ ((⌊‘𝑌)...(⌊‘(𝐾 · 𝑌))) ↔ (𝑚 = (⌊‘𝑌) ∨ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))))) |
| 164 | 124, 163 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑚 ∈ ((⌊‘𝑌)...(⌊‘(𝐾 · 𝑌))) ↔ (𝑚 = (⌊‘𝑌) ∨ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))))) |
| 165 | 162, 164 | imbitrid 244 |
. . . . . . . . 9
⊢ (𝜑 → (𝑚 ∈ ((⌊‘𝑌)..^(⌊‘(𝐾 · 𝑌))) → (𝑚 = (⌊‘𝑌) ∨ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))))) |
| 166 | 165 | imp 406 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ((⌊‘𝑌)..^(⌊‘(𝐾 · 𝑌)))) → (𝑚 = (⌊‘𝑌) ∨ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))))) |
| 167 | 30 | nnrpd 13075 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((⌊‘𝑌) + 1) ∈
ℝ+) |
| 168 | 36 | ffvelcdmi 7103 |
. . . . . . . . . . . . . 14
⊢
(((⌊‘𝑌)
+ 1) ∈ ℝ+ → (𝑅‘((⌊‘𝑌) + 1)) ∈ ℝ) |
| 169 | 167, 168 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑅‘((⌊‘𝑌) + 1)) ∈ ℝ) |
| 170 | 5, 169 | letrid 11413 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 ≤ (𝑅‘((⌊‘𝑌) + 1)) ∨ (𝑅‘((⌊‘𝑌) + 1)) ≤ 0)) |
| 171 | 170 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → (0 ≤ (𝑅‘((⌊‘𝑌) + 1)) ∨ (𝑅‘((⌊‘𝑌) + 1)) ≤ 0)) |
| 172 | | oveq1 7438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = (⌊‘𝑌) → (𝑚 + 1) = ((⌊‘𝑌) + 1)) |
| 173 | 172 | oveq2d 7447 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (⌊‘𝑌) → (((⌊‘𝑌) + 1)...(𝑚 + 1)) = (((⌊‘𝑌) + 1)...((⌊‘𝑌) + 1))) |
| 174 | 4 | flcld 13838 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (⌊‘𝑌) ∈
ℤ) |
| 175 | 174 | peano2zd 12725 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((⌊‘𝑌) + 1) ∈
ℤ) |
| 176 | | fzsn 13606 |
. . . . . . . . . . . . . . . 16
⊢
(((⌊‘𝑌)
+ 1) ∈ ℤ → (((⌊‘𝑌) + 1)...((⌊‘𝑌) + 1)) = {((⌊‘𝑌) + 1)}) |
| 177 | 175, 176 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((⌊‘𝑌) + 1)...((⌊‘𝑌) + 1)) = {((⌊‘𝑌) + 1)}) |
| 178 | 173, 177 | sylan9eqr 2799 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → (((⌊‘𝑌) + 1)...(𝑚 + 1)) = {((⌊‘𝑌) + 1)}) |
| 179 | 178 | raleqdv 3326 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ↔ ∀𝑖 ∈ {((⌊‘𝑌) + 1)}0 ≤ (𝑅‘𝑖))) |
| 180 | | ovex 7464 |
. . . . . . . . . . . . . 14
⊢
((⌊‘𝑌) +
1) ∈ V |
| 181 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = ((⌊‘𝑌) + 1) → (𝑅‘𝑖) = (𝑅‘((⌊‘𝑌) + 1))) |
| 182 | 181 | breq2d 5155 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = ((⌊‘𝑌) + 1) → (0 ≤ (𝑅‘𝑖) ↔ 0 ≤ (𝑅‘((⌊‘𝑌) + 1)))) |
| 183 | 180, 182 | ralsn 4681 |
. . . . . . . . . . . . 13
⊢
(∀𝑖 ∈
{((⌊‘𝑌) + 1)}0
≤ (𝑅‘𝑖) ↔ 0 ≤ (𝑅‘((⌊‘𝑌) + 1))) |
| 184 | 179, 183 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ↔ 0 ≤ (𝑅‘((⌊‘𝑌) + 1)))) |
| 185 | 178 | raleqdv 3326 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0 ↔ ∀𝑖 ∈ {((⌊‘𝑌) + 1)} (𝑅‘𝑖) ≤ 0)) |
| 186 | 181 | breq1d 5153 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = ((⌊‘𝑌) + 1) → ((𝑅‘𝑖) ≤ 0 ↔ (𝑅‘((⌊‘𝑌) + 1)) ≤ 0)) |
| 187 | 180, 186 | ralsn 4681 |
. . . . . . . . . . . . 13
⊢
(∀𝑖 ∈
{((⌊‘𝑌) + 1)}
(𝑅‘𝑖) ≤ 0 ↔ (𝑅‘((⌊‘𝑌) + 1)) ≤ 0) |
| 188 | 185, 187 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0 ↔ (𝑅‘((⌊‘𝑌) + 1)) ≤ 0)) |
| 189 | 184, 188 | orbi12d 919 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → ((∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0) ↔ (0 ≤ (𝑅‘((⌊‘𝑌) + 1)) ∨ (𝑅‘((⌊‘𝑌) + 1)) ≤ 0))) |
| 190 | 171, 189 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0)) |
| 191 | 190 | a1d 25 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → ((∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0))) |
| 192 | | elfzuz 13560 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → 𝑚 ∈
(ℤ≥‘((⌊‘𝑌) + 1))) |
| 193 | 192 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑚 ∈
(ℤ≥‘((⌊‘𝑌) + 1))) |
| 194 | | eluzfz2 13572 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈
(ℤ≥‘((⌊‘𝑌) + 1)) → 𝑚 ∈ (((⌊‘𝑌) + 1)...𝑚)) |
| 195 | 193, 194 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑚 ∈ (((⌊‘𝑌) + 1)...𝑚)) |
| 196 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝑚 → (𝑅‘𝑖) = (𝑅‘𝑚)) |
| 197 | 196 | breq2d 5155 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑚 → (0 ≤ (𝑅‘𝑖) ↔ 0 ≤ (𝑅‘𝑚))) |
| 198 | 197 | rspcv 3618 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ (((⌊‘𝑌) + 1)...𝑚) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) → 0 ≤ (𝑅‘𝑚))) |
| 199 | 195, 198 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) → 0 ≤ (𝑅‘𝑚))) |
| 200 | | pntpbnd1.3 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) |
| 201 | 200 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) |
| 202 | | eluznn 12960 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((⌊‘𝑌)
+ 1) ∈ ℕ ∧ 𝑚
∈ (ℤ≥‘((⌊‘𝑌) + 1))) → 𝑚 ∈ ℕ) |
| 203 | 30, 192, 202 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑚 ∈ ℕ) |
| 204 | 203 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) → 𝑚 ∈ ℕ) |
| 205 | | elfzle1 13567 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → ((⌊‘𝑌) + 1) ≤ 𝑚) |
| 206 | 205 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((⌊‘𝑌) + 1) ≤ 𝑚) |
| 207 | | elfzelz 13564 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → 𝑚 ∈ ℤ) |
| 208 | | zltp1le 12667 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((⌊‘𝑌)
∈ ℤ ∧ 𝑚
∈ ℤ) → ((⌊‘𝑌) < 𝑚 ↔ ((⌊‘𝑌) + 1) ≤ 𝑚)) |
| 209 | 174, 207,
208 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((⌊‘𝑌) < 𝑚 ↔ ((⌊‘𝑌) + 1) ≤ 𝑚)) |
| 210 | 206, 209 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (⌊‘𝑌) < 𝑚) |
| 211 | | fllt 13846 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑌 ∈ ℝ ∧ 𝑚 ∈ ℤ) → (𝑌 < 𝑚 ↔ (⌊‘𝑌) < 𝑚)) |
| 212 | 4, 207, 211 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑌 < 𝑚 ↔ (⌊‘𝑌) < 𝑚)) |
| 213 | 210, 212 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑌 < 𝑚) |
| 214 | | elfzle2 13568 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → 𝑚 ≤ (⌊‘(𝐾 · 𝑌))) |
| 215 | 214 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑚 ≤ (⌊‘(𝐾 · 𝑌))) |
| 216 | | flge 13845 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐾 · 𝑌) ∈ ℝ ∧ 𝑚 ∈ ℤ) → (𝑚 ≤ (𝐾 · 𝑌) ↔ 𝑚 ≤ (⌊‘(𝐾 · 𝑌)))) |
| 217 | 107, 207,
216 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑚 ≤ (𝐾 · 𝑌) ↔ 𝑚 ≤ (⌊‘(𝐾 · 𝑌)))) |
| 218 | 215, 217 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑚 ≤ (𝐾 · 𝑌)) |
| 219 | 213, 218 | jca 511 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑌 < 𝑚 ∧ 𝑚 ≤ (𝐾 · 𝑌))) |
| 220 | 219 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) → (𝑌 < 𝑚 ∧ 𝑚 ≤ (𝐾 · 𝑌))) |
| 221 | 9 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) → 𝐸 ∈ (0(,)1)) |
| 222 | 3 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) → 𝑌 ∈ (𝑋(,)+∞)) |
| 223 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) → (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) |
| 224 | 35, 221, 6, 222, 204, 220, 223 | pntpbnd1a 27629 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) → (abs‘((𝑅‘𝑚) / 𝑚)) ≤ 𝐸) |
| 225 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑚 → (𝑌 < 𝑦 ↔ 𝑌 < 𝑚)) |
| 226 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑚 → (𝑦 ≤ (𝐾 · 𝑌) ↔ 𝑚 ≤ (𝐾 · 𝑌))) |
| 227 | 225, 226 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑚 → ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ↔ (𝑌 < 𝑚 ∧ 𝑚 ≤ (𝐾 · 𝑌)))) |
| 228 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 𝑚 → (𝑅‘𝑦) = (𝑅‘𝑚)) |
| 229 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 𝑚 → 𝑦 = 𝑚) |
| 230 | 228, 229 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 𝑚 → ((𝑅‘𝑦) / 𝑦) = ((𝑅‘𝑚) / 𝑚)) |
| 231 | 230 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑚 → (abs‘((𝑅‘𝑦) / 𝑦)) = (abs‘((𝑅‘𝑚) / 𝑚))) |
| 232 | 231 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑚 → ((abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸 ↔ (abs‘((𝑅‘𝑚) / 𝑚)) ≤ 𝐸)) |
| 233 | 227, 232 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑚 → (((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸) ↔ ((𝑌 < 𝑚 ∧ 𝑚 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑚) / 𝑚)) ≤ 𝐸))) |
| 234 | 233 | rspcev 3622 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈ ℕ ∧ ((𝑌 < 𝑚 ∧ 𝑚 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑚) / 𝑚)) ≤ 𝐸)) → ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) |
| 235 | 204, 220,
224, 234 | syl12anc 837 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) → ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) |
| 236 | 201, 235 | mtand 816 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ¬ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) |
| 237 | 236 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ 0 ≤ (𝑅‘𝑚)) → ¬ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) |
| 238 | 203 | nnrpd 13075 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑚 ∈ ℝ+) |
| 239 | 36 | ffvelcdmi 7103 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ℝ+
→ (𝑅‘𝑚) ∈
ℝ) |
| 240 | 238, 239 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑚) ∈ ℝ) |
| 241 | 240 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (𝑅‘𝑚) ∈ ℝ) |
| 242 | 241 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (𝑅‘𝑚) ∈ ℂ) |
| 243 | 242 | subid1d 11609 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → ((𝑅‘𝑚) − 0) = (𝑅‘𝑚)) |
| 244 | 203 | peano2nnd 12283 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑚 + 1) ∈ ℕ) |
| 245 | 244 | nnrpd 13075 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑚 + 1) ∈
ℝ+) |
| 246 | 36 | ffvelcdmi 7103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑚 + 1) ∈ ℝ+
→ (𝑅‘(𝑚 + 1)) ∈
ℝ) |
| 247 | 245, 246 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘(𝑚 + 1)) ∈ ℝ) |
| 248 | 247 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (𝑅‘(𝑚 + 1)) ∈ ℝ) |
| 249 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → 0 ∈
ℝ) |
| 250 | | 0re 11263 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
ℝ |
| 251 | | letric 11361 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((0
∈ ℝ ∧ (𝑅‘(𝑚 + 1)) ∈ ℝ) → (0 ≤ (𝑅‘(𝑚 + 1)) ∨ (𝑅‘(𝑚 + 1)) ≤ 0)) |
| 252 | 250, 247,
251 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (0 ≤ (𝑅‘(𝑚 + 1)) ∨ (𝑅‘(𝑚 + 1)) ≤ 0)) |
| 253 | 252 | ord 865 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (¬ 0 ≤ (𝑅‘(𝑚 + 1)) → (𝑅‘(𝑚 + 1)) ≤ 0)) |
| 254 | 253 | imp 406 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1))) → (𝑅‘(𝑚 + 1)) ≤ 0) |
| 255 | 254 | adantrl 716 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (𝑅‘(𝑚 + 1)) ≤ 0) |
| 256 | 248, 249,
241, 255 | lesub2dd 11880 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → ((𝑅‘𝑚) − 0) ≤ ((𝑅‘𝑚) − (𝑅‘(𝑚 + 1)))) |
| 257 | 243, 256 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (𝑅‘𝑚) ≤ ((𝑅‘𝑚) − (𝑅‘(𝑚 + 1)))) |
| 258 | | simprl 771 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → 0 ≤ (𝑅‘𝑚)) |
| 259 | 241, 258 | absidd 15461 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (abs‘(𝑅‘𝑚)) = (𝑅‘𝑚)) |
| 260 | 248, 249,
241, 255, 258 | letrd 11418 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (𝑅‘(𝑚 + 1)) ≤ (𝑅‘𝑚)) |
| 261 | 248, 241,
260 | abssuble0d 15471 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚))) = ((𝑅‘𝑚) − (𝑅‘(𝑚 + 1)))) |
| 262 | 257, 259,
261 | 3brtr4d 5175 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) |
| 263 | 262 | expr 456 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ 0 ≤ (𝑅‘𝑚)) → (¬ 0 ≤ (𝑅‘(𝑚 + 1)) → (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚))))) |
| 264 | 237, 263 | mt3d 148 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ 0 ≤ (𝑅‘𝑚)) → 0 ≤ (𝑅‘(𝑚 + 1))) |
| 265 | 264 | ex 412 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (0 ≤ (𝑅‘𝑚) → 0 ≤ (𝑅‘(𝑚 + 1)))) |
| 266 | 199, 265 | syld 47 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) → 0 ≤ (𝑅‘(𝑚 + 1)))) |
| 267 | | ovex 7464 |
. . . . . . . . . . . . . 14
⊢ (𝑚 + 1) ∈ V |
| 268 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑚 + 1) → (𝑅‘𝑖) = (𝑅‘(𝑚 + 1))) |
| 269 | 268 | breq2d 5155 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑚 + 1) → (0 ≤ (𝑅‘𝑖) ↔ 0 ≤ (𝑅‘(𝑚 + 1)))) |
| 270 | 267, 269 | ralsn 4681 |
. . . . . . . . . . . . 13
⊢
(∀𝑖 ∈
{(𝑚 + 1)}0 ≤ (𝑅‘𝑖) ↔ 0 ≤ (𝑅‘(𝑚 + 1))) |
| 271 | 266, 270 | imbitrrdi 252 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) → ∀𝑖 ∈ {(𝑚 + 1)}0 ≤ (𝑅‘𝑖))) |
| 272 | 271 | ancld 550 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) ∧ ∀𝑖 ∈ {(𝑚 + 1)}0 ≤ (𝑅‘𝑖)))) |
| 273 | | fzsuc 13611 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈
(ℤ≥‘((⌊‘𝑌) + 1)) → (((⌊‘𝑌) + 1)...(𝑚 + 1)) = ((((⌊‘𝑌) + 1)...𝑚) ∪ {(𝑚 + 1)})) |
| 274 | 193, 273 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (((⌊‘𝑌) + 1)...(𝑚 + 1)) = ((((⌊‘𝑌) + 1)...𝑚) ∪ {(𝑚 + 1)})) |
| 275 | 274 | raleqdv 3326 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ↔ ∀𝑖 ∈ ((((⌊‘𝑌) + 1)...𝑚) ∪ {(𝑚 + 1)})0 ≤ (𝑅‘𝑖))) |
| 276 | | ralunb 4197 |
. . . . . . . . . . . 12
⊢
(∀𝑖 ∈
((((⌊‘𝑌) +
1)...𝑚) ∪ {(𝑚 + 1)})0 ≤ (𝑅‘𝑖) ↔ (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) ∧ ∀𝑖 ∈ {(𝑚 + 1)}0 ≤ (𝑅‘𝑖))) |
| 277 | 275, 276 | bitrdi 287 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ↔ (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) ∧ ∀𝑖 ∈ {(𝑚 + 1)}0 ≤ (𝑅‘𝑖)))) |
| 278 | 272, 277 | sylibrd 259 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) → ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖))) |
| 279 | 196 | breq1d 5153 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑚 → ((𝑅‘𝑖) ≤ 0 ↔ (𝑅‘𝑚) ≤ 0)) |
| 280 | 279 | rspcv 3618 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ (((⌊‘𝑌) + 1)...𝑚) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0 → (𝑅‘𝑚) ≤ 0)) |
| 281 | 195, 280 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0 → (𝑅‘𝑚) ≤ 0)) |
| 282 | 236 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (𝑅‘𝑚) ≤ 0) → ¬ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) |
| 283 | 253 | con1d 145 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (¬ (𝑅‘(𝑚 + 1)) ≤ 0 → 0 ≤ (𝑅‘(𝑚 + 1)))) |
| 284 | 283 | imp 406 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0) → 0 ≤ (𝑅‘(𝑚 + 1))) |
| 285 | 284 | adantrl 716 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → 0 ≤ (𝑅‘(𝑚 + 1))) |
| 286 | 240 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (𝑅‘𝑚) ∈ ℝ) |
| 287 | 286 | renegcld 11690 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → -(𝑅‘𝑚) ∈ ℝ) |
| 288 | 247 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (𝑅‘(𝑚 + 1)) ∈ ℝ) |
| 289 | 287, 288 | addge02d 11852 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (0 ≤ (𝑅‘(𝑚 + 1)) ↔ -(𝑅‘𝑚) ≤ ((𝑅‘(𝑚 + 1)) + -(𝑅‘𝑚)))) |
| 290 | 285, 289 | mpbid 232 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → -(𝑅‘𝑚) ≤ ((𝑅‘(𝑚 + 1)) + -(𝑅‘𝑚))) |
| 291 | 288 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (𝑅‘(𝑚 + 1)) ∈ ℂ) |
| 292 | 286 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (𝑅‘𝑚) ∈ ℂ) |
| 293 | 291, 292 | negsubd 11626 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → ((𝑅‘(𝑚 + 1)) + -(𝑅‘𝑚)) = ((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚))) |
| 294 | 290, 293 | breqtrd 5169 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → -(𝑅‘𝑚) ≤ ((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚))) |
| 295 | | simprl 771 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (𝑅‘𝑚) ≤ 0) |
| 296 | 286, 295 | absnidd 15452 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (abs‘(𝑅‘𝑚)) = -(𝑅‘𝑚)) |
| 297 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → 0 ∈
ℝ) |
| 298 | 286, 297,
288, 295, 285 | letrd 11418 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (𝑅‘𝑚) ≤ (𝑅‘(𝑚 + 1))) |
| 299 | 286, 288,
298 | abssubge0d 15470 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚))) = ((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚))) |
| 300 | 294, 296,
299 | 3brtr4d 5175 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) |
| 301 | 300 | expr 456 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (𝑅‘𝑚) ≤ 0) → (¬ (𝑅‘(𝑚 + 1)) ≤ 0 → (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚))))) |
| 302 | 282, 301 | mt3d 148 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (𝑅‘𝑚) ≤ 0) → (𝑅‘(𝑚 + 1)) ≤ 0) |
| 303 | 302 | ex 412 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑚) ≤ 0 → (𝑅‘(𝑚 + 1)) ≤ 0)) |
| 304 | 281, 303 | syld 47 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0 → (𝑅‘(𝑚 + 1)) ≤ 0)) |
| 305 | 268 | breq1d 5153 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑚 + 1) → ((𝑅‘𝑖) ≤ 0 ↔ (𝑅‘(𝑚 + 1)) ≤ 0)) |
| 306 | 267, 305 | ralsn 4681 |
. . . . . . . . . . . . 13
⊢
(∀𝑖 ∈
{(𝑚 + 1)} (𝑅‘𝑖) ≤ 0 ↔ (𝑅‘(𝑚 + 1)) ≤ 0) |
| 307 | 304, 306 | imbitrrdi 252 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0 → ∀𝑖 ∈ {(𝑚 + 1)} (𝑅‘𝑖) ≤ 0)) |
| 308 | 307 | ancld 550 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0 ∧ ∀𝑖 ∈ {(𝑚 + 1)} (𝑅‘𝑖) ≤ 0))) |
| 309 | 274 | raleqdv 3326 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0 ↔ ∀𝑖 ∈ ((((⌊‘𝑌) + 1)...𝑚) ∪ {(𝑚 + 1)})(𝑅‘𝑖) ≤ 0)) |
| 310 | | ralunb 4197 |
. . . . . . . . . . . 12
⊢
(∀𝑖 ∈
((((⌊‘𝑌) +
1)...𝑚) ∪ {(𝑚 + 1)})(𝑅‘𝑖) ≤ 0 ↔ (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0 ∧ ∀𝑖 ∈ {(𝑚 + 1)} (𝑅‘𝑖) ≤ 0)) |
| 311 | 309, 310 | bitrdi 287 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0 ↔ (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0 ∧ ∀𝑖 ∈ {(𝑚 + 1)} (𝑅‘𝑖) ≤ 0))) |
| 312 | 308, 311 | sylibrd 259 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0 → ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0)) |
| 313 | 278, 312 | orim12d 967 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0))) |
| 314 | 191, 313 | jaodan 960 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 = (⌊‘𝑌) ∨ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))))) → ((∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0))) |
| 315 | 166, 314 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ((⌊‘𝑌)..^(⌊‘(𝐾 · 𝑌)))) → ((∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0))) |
| 316 | 315 | expcom 413 |
. . . . . 6
⊢ (𝑚 ∈ ((⌊‘𝑌)..^(⌊‘(𝐾 · 𝑌))) → (𝜑 → ((∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0)))) |
| 317 | 316 | a2d 29 |
. . . . 5
⊢ (𝑚 ∈ ((⌊‘𝑌)..^(⌊‘(𝐾 · 𝑌))) → ((𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0)) → (𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0)))) |
| 318 | 134, 139,
144, 149, 161, 317 | fzind2 13824 |
. . . 4
⊢
((⌊‘(𝐾
· 𝑌)) ∈
((⌊‘𝑌)...(⌊‘(𝐾 · 𝑌))) → (𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0))) |
| 319 | 129, 318 | mpcom 38 |
. . 3
⊢ (𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0)) |
| 320 | 58, 92, 319 | mpjaodan 961 |
. 2
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
| 321 | | pntpbnd1.2 |
. . 3
⊢ (𝜑 → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℤ (abs‘Σ𝑦 ∈ (𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴) |
| 322 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = 𝑛 → (𝑅‘𝑦) = (𝑅‘𝑛)) |
| 323 | | id 22 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑛 → 𝑦 = 𝑛) |
| 324 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑛 → (𝑦 + 1) = (𝑛 + 1)) |
| 325 | 323, 324 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑦 = 𝑛 → (𝑦 · (𝑦 + 1)) = (𝑛 · (𝑛 + 1))) |
| 326 | 322, 325 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑦 = 𝑛 → ((𝑅‘𝑦) / (𝑦 · (𝑦 + 1))) = ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 327 | 326 | cbvsumv 15732 |
. . . . . . 7
⊢
Σ𝑦 ∈
(𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1))) = Σ𝑛 ∈ (𝑖...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) |
| 328 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑖 = ((⌊‘𝑌) + 1) → (𝑖...𝑗) = (((⌊‘𝑌) + 1)...𝑗)) |
| 329 | 328 | sumeq1d 15736 |
. . . . . . 7
⊢ (𝑖 = ((⌊‘𝑌) + 1) → Σ𝑛 ∈ (𝑖...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 330 | 327, 329 | eqtrid 2789 |
. . . . . 6
⊢ (𝑖 = ((⌊‘𝑌) + 1) → Σ𝑦 ∈ (𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 331 | 330 | fveq2d 6910 |
. . . . 5
⊢ (𝑖 = ((⌊‘𝑌) + 1) →
(abs‘Σ𝑦 ∈
(𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) = (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
| 332 | 331 | breq1d 5153 |
. . . 4
⊢ (𝑖 = ((⌊‘𝑌) + 1) →
((abs‘Σ𝑦 ∈
(𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴 ↔ (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴)) |
| 333 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑗 = (⌊‘(𝐾 · 𝑌)) → (((⌊‘𝑌) + 1)...𝑗) = (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) |
| 334 | 333 | sumeq1d 15736 |
. . . . . 6
⊢ (𝑗 = (⌊‘(𝐾 · 𝑌)) → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
| 335 | 334 | fveq2d 6910 |
. . . . 5
⊢ (𝑗 = (⌊‘(𝐾 · 𝑌)) → (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
| 336 | 335 | breq1d 5153 |
. . . 4
⊢ (𝑗 = (⌊‘(𝐾 · 𝑌)) → ((abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴 ↔ (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴)) |
| 337 | 332, 336 | rspc2va 3634 |
. . 3
⊢
(((((⌊‘𝑌) + 1) ∈ ℕ ∧
(⌊‘(𝐾 ·
𝑌)) ∈ ℤ) ∧
∀𝑖 ∈ ℕ
∀𝑗 ∈ ℤ
(abs‘Σ𝑦 ∈
(𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴) → (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴) |
| 338 | 30, 125, 321, 337 | syl21anc 838 |
. 2
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴) |
| 339 | 320, 338 | eqbrtrrd 5167 |
1
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴) |