Step | Hyp | Ref
| Expression |
1 | | fzfid 13693 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) → (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) ∈ Fin) |
2 | | ioossre 13140 |
. . . . . . . . . . . . . 14
⊢ (𝑋(,)+∞) ⊆
ℝ |
3 | | pntpbnd1.y |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ∈ (𝑋(,)+∞)) |
4 | 2, 3 | sselid 3919 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ∈ ℝ) |
5 | | 0red 10978 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ∈
ℝ) |
6 | | pntpbnd1.x |
. . . . . . . . . . . . . . . 16
⊢ 𝑋 = (exp‘(2 / 𝐸)) |
7 | | 2re 12047 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
8 | | ioossre 13140 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0(,)1)
⊆ ℝ |
9 | | pntpbnd1.e |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐸 ∈ (0(,)1)) |
10 | 8, 9 | sselid 3919 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐸 ∈ ℝ) |
11 | | eliooord 13138 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐸 ∈ (0(,)1) → (0 <
𝐸 ∧ 𝐸 < 1)) |
12 | 9, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (0 < 𝐸 ∧ 𝐸 < 1)) |
13 | 12 | simpld 495 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 < 𝐸) |
14 | 10, 13 | elrpd 12769 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
15 | | rerpdivcl 12760 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℝ ∧ 𝐸
∈ ℝ+) → (2 / 𝐸) ∈ ℝ) |
16 | 7, 14, 15 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 / 𝐸) ∈ ℝ) |
17 | 16 | reefcld 15797 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (exp‘(2 / 𝐸)) ∈
ℝ) |
18 | 6, 17 | eqeltrid 2843 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ∈ ℝ) |
19 | | efgt0 15812 |
. . . . . . . . . . . . . . . . 17
⊢ ((2 /
𝐸) ∈ ℝ → 0
< (exp‘(2 / 𝐸))) |
20 | 16, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 < (exp‘(2 /
𝐸))) |
21 | 20, 6 | breqtrrdi 5116 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 < 𝑋) |
22 | | eliooord 13138 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑌 ∈ (𝑋(,)+∞) → (𝑋 < 𝑌 ∧ 𝑌 < +∞)) |
23 | 3, 22 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑋 < 𝑌 ∧ 𝑌 < +∞)) |
24 | 23 | simpld 495 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 < 𝑌) |
25 | 5, 18, 4, 21, 24 | lttrd 11136 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝑌) |
26 | 5, 4, 25 | ltled 11123 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ 𝑌) |
27 | | flge0nn0 13540 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ∈ ℝ ∧ 0 ≤
𝑌) →
(⌊‘𝑌) ∈
ℕ0) |
28 | 4, 26, 27 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (⌊‘𝑌) ∈
ℕ0) |
29 | | nn0p1nn 12272 |
. . . . . . . . . . . 12
⊢
((⌊‘𝑌)
∈ ℕ0 → ((⌊‘𝑌) + 1) ∈ ℕ) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((⌊‘𝑌) + 1) ∈
ℕ) |
31 | | elfzuz 13252 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → 𝑛 ∈
(ℤ≥‘((⌊‘𝑌) + 1))) |
32 | | eluznn 12658 |
. . . . . . . . . . 11
⊢
((((⌊‘𝑌)
+ 1) ∈ ℕ ∧ 𝑛
∈ (ℤ≥‘((⌊‘𝑌) + 1))) → 𝑛 ∈ ℕ) |
33 | 30, 31, 32 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℕ) |
34 | 33 | nnrpd 12770 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑛 ∈ ℝ+) |
35 | | pntpbnd.r |
. . . . . . . . . . 11
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
36 | 35 | pntrf 26711 |
. . . . . . . . . 10
⊢ 𝑅:ℝ+⟶ℝ |
37 | 36 | ffvelrni 6960 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℝ+
→ (𝑅‘𝑛) ∈
ℝ) |
38 | 34, 37 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑛) ∈ ℝ) |
39 | 33 | peano2nnd 11990 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 + 1) ∈ ℕ) |
40 | 33, 39 | nnmulcld 12026 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ∈ ℕ) |
41 | 38, 40 | nndivred 12027 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
42 | 41 | adantlr 712 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
43 | 1, 42 | fsumrecl 15446 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
44 | 38 | adantlr 712 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑛) ∈ ℝ) |
45 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑛 → (𝑅‘𝑖) = (𝑅‘𝑛)) |
46 | 45 | breq2d 5086 |
. . . . . . . . 9
⊢ (𝑖 = 𝑛 → (0 ≤ (𝑅‘𝑖) ↔ 0 ≤ (𝑅‘𝑛))) |
47 | 46 | rspccva 3560 |
. . . . . . . 8
⊢
((∀𝑖 ∈
(((⌊‘𝑌) +
1)...(⌊‘(𝐾
· 𝑌)))0 ≤ (𝑅‘𝑖) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 0 ≤ (𝑅‘𝑛)) |
48 | 47 | adantll 711 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 0 ≤ (𝑅‘𝑛)) |
49 | 40 | adantlr 712 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ∈ ℕ) |
50 | 49 | nnred 11988 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ∈ ℝ) |
51 | 49 | nngt0d 12022 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 0 < (𝑛 · (𝑛 + 1))) |
52 | | divge0 11844 |
. . . . . . 7
⊢ ((((𝑅‘𝑛) ∈ ℝ ∧ 0 ≤ (𝑅‘𝑛)) ∧ ((𝑛 · (𝑛 + 1)) ∈ ℝ ∧ 0 < (𝑛 · (𝑛 + 1)))) → 0 ≤ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
53 | 44, 48, 50, 51, 52 | syl22anc 836 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 0 ≤ ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
54 | 1, 42, 53 | fsumge0 15507 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) → 0 ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
55 | 43, 54 | absidd 15134 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) → (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
56 | 42, 53 | absidd 15134 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
57 | 56 | sumeq2dv 15415 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
58 | 55, 57 | eqtr4d 2781 |
. . 3
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖)) → (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
59 | | fzfid 13693 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) ∈ Fin) |
60 | 41 | adantlr 712 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
61 | 60 | recnd 11003 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ) |
62 | 59, 61 | fsumneg 15499 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))-((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = -Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
63 | 38 | adantlr 712 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑛) ∈ ℝ) |
64 | 63 | renegcld 11402 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → -(𝑅‘𝑛) ∈ ℝ) |
65 | 45 | breq1d 5084 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑛 → ((𝑅‘𝑖) ≤ 0 ↔ (𝑅‘𝑛) ≤ 0)) |
66 | 65 | rspccva 3560 |
. . . . . . . . . . 11
⊢
((∀𝑖 ∈
(((⌊‘𝑌) +
1)...(⌊‘(𝐾
· 𝑌)))(𝑅‘𝑖) ≤ 0 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑛) ≤ 0) |
67 | 66 | adantll 711 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑛) ≤ 0) |
68 | 63 | le0neg1d 11546 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) ≤ 0 ↔ 0 ≤ -(𝑅‘𝑛))) |
69 | 67, 68 | mpbid 231 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 0 ≤ -(𝑅‘𝑛)) |
70 | 40 | adantlr 712 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ∈ ℕ) |
71 | 70 | nnred 11988 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ∈ ℝ) |
72 | 70 | nngt0d 12022 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 0 < (𝑛 · (𝑛 + 1))) |
73 | | divge0 11844 |
. . . . . . . . 9
⊢
(((-(𝑅‘𝑛) ∈ ℝ ∧ 0 ≤
-(𝑅‘𝑛)) ∧ ((𝑛 · (𝑛 + 1)) ∈ ℝ ∧ 0 < (𝑛 · (𝑛 + 1)))) → 0 ≤ (-(𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
74 | 64, 69, 71, 72, 73 | syl22anc 836 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 0 ≤ (-(𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
75 | 38 | recnd 11003 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑛) ∈ ℂ) |
76 | 40 | nncnd 11989 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ∈ ℂ) |
77 | 40 | nnne0d 12023 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑛 · (𝑛 + 1)) ≠ 0) |
78 | 75, 76, 77 | divnegd 11764 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = (-(𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
79 | 78 | adantlr 712 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = (-(𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
80 | 74, 79 | breqtrrd 5102 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 0 ≤ -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
81 | 60 | le0neg1d 11546 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ≤ 0 ↔ 0 ≤ -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
82 | 80, 81 | mpbird 256 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ≤ 0) |
83 | 60, 82 | absnidd 15125 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
84 | 83 | sumeq2dv 15415 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))-((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
85 | 59, 60 | fsumrecl 15446 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
86 | 60 | renegcld 11402 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) ∧ 𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → -((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ) |
87 | 59, 86, 80 | fsumge0 15507 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → 0 ≤ Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))-((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
88 | 87, 62 | breqtrd 5100 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → 0 ≤ -Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
89 | 85 | le0neg1d 11546 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → (Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ≤ 0 ↔ 0 ≤ -Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
90 | 88, 89 | mpbird 256 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) ≤ 0) |
91 | 85, 90 | absnidd 15125 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = -Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
92 | 62, 84, 91 | 3eqtr4rd 2789 |
. . 3
⊢ ((𝜑 ∧ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0) → (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
93 | | pntpbnd1.c |
. . . . . . . . . . . . 13
⊢ 𝐶 = (𝐴 + 2) |
94 | | pntpbnd1.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
95 | | 2rp 12735 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ+ |
96 | | rpaddcl 12752 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ+
∧ 2 ∈ ℝ+) → (𝐴 + 2) ∈
ℝ+) |
97 | 94, 95, 96 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 + 2) ∈
ℝ+) |
98 | 93, 97 | eqeltrid 2843 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
99 | 98, 14 | rpdivcld 12789 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶 / 𝐸) ∈
ℝ+) |
100 | 99 | rpred 12772 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 / 𝐸) ∈ ℝ) |
101 | 100 | reefcld 15797 |
. . . . . . . . 9
⊢ (𝜑 → (exp‘(𝐶 / 𝐸)) ∈ ℝ) |
102 | | pnfxr 11029 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
103 | | icossre 13160 |
. . . . . . . . 9
⊢
(((exp‘(𝐶 /
𝐸)) ∈ ℝ ∧
+∞ ∈ ℝ*) → ((exp‘(𝐶 / 𝐸))[,)+∞) ⊆
ℝ) |
104 | 101, 102,
103 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → ((exp‘(𝐶 / 𝐸))[,)+∞) ⊆
ℝ) |
105 | | pntpbnd1.k |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) |
106 | 104, 105 | sseldd 3922 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℝ) |
107 | 106, 4 | remulcld 11005 |
. . . . . 6
⊢ (𝜑 → (𝐾 · 𝑌) ∈ ℝ) |
108 | 4 | recnd 11003 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ ℂ) |
109 | 108 | mulid2d 10993 |
. . . . . . . 8
⊢ (𝜑 → (1 · 𝑌) = 𝑌) |
110 | | 1red 10976 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
111 | | efgt1 15825 |
. . . . . . . . . . 11
⊢ ((𝐶 / 𝐸) ∈ ℝ+ → 1 <
(exp‘(𝐶 / 𝐸))) |
112 | 99, 111 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 1 < (exp‘(𝐶 / 𝐸))) |
113 | | elicopnf 13177 |
. . . . . . . . . . . . 13
⊢
((exp‘(𝐶 /
𝐸)) ∈ ℝ →
(𝐾 ∈
((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝐾 ∈ ℝ ∧
(exp‘(𝐶 / 𝐸)) ≤ 𝐾))) |
114 | 101, 113 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞) ↔ (𝐾 ∈ ℝ ∧ (exp‘(𝐶 / 𝐸)) ≤ 𝐾))) |
115 | 114 | simplbda 500 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) → (exp‘(𝐶 / 𝐸)) ≤ 𝐾) |
116 | 105, 115 | mpdan 684 |
. . . . . . . . . 10
⊢ (𝜑 → (exp‘(𝐶 / 𝐸)) ≤ 𝐾) |
117 | 110, 101,
106, 112, 116 | ltletrd 11135 |
. . . . . . . . 9
⊢ (𝜑 → 1 < 𝐾) |
118 | | ltmul1 11825 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ 𝐾
∈ ℝ ∧ (𝑌
∈ ℝ ∧ 0 < 𝑌)) → (1 < 𝐾 ↔ (1 · 𝑌) < (𝐾 · 𝑌))) |
119 | 110, 106,
4, 25, 118 | syl112anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → (1 < 𝐾 ↔ (1 · 𝑌) < (𝐾 · 𝑌))) |
120 | 117, 119 | mpbid 231 |
. . . . . . . 8
⊢ (𝜑 → (1 · 𝑌) < (𝐾 · 𝑌)) |
121 | 109, 120 | eqbrtrrd 5098 |
. . . . . . 7
⊢ (𝜑 → 𝑌 < (𝐾 · 𝑌)) |
122 | 4, 107, 121 | ltled 11123 |
. . . . . 6
⊢ (𝜑 → 𝑌 ≤ (𝐾 · 𝑌)) |
123 | | flword2 13533 |
. . . . . 6
⊢ ((𝑌 ∈ ℝ ∧ (𝐾 · 𝑌) ∈ ℝ ∧ 𝑌 ≤ (𝐾 · 𝑌)) → (⌊‘(𝐾 · 𝑌)) ∈
(ℤ≥‘(⌊‘𝑌))) |
124 | 4, 107, 122, 123 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈
(ℤ≥‘(⌊‘𝑌))) |
125 | 107 | flcld 13518 |
. . . . . 6
⊢ (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈ ℤ) |
126 | | uzid 12597 |
. . . . . 6
⊢
((⌊‘(𝐾
· 𝑌)) ∈ ℤ
→ (⌊‘(𝐾
· 𝑌)) ∈
(ℤ≥‘(⌊‘(𝐾 · 𝑌)))) |
127 | 125, 126 | syl 17 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈
(ℤ≥‘(⌊‘(𝐾 · 𝑌)))) |
128 | | elfzuzb 13250 |
. . . . 5
⊢
((⌊‘(𝐾
· 𝑌)) ∈
((⌊‘𝑌)...(⌊‘(𝐾 · 𝑌))) ↔ ((⌊‘(𝐾 · 𝑌)) ∈
(ℤ≥‘(⌊‘𝑌)) ∧ (⌊‘(𝐾 · 𝑌)) ∈
(ℤ≥‘(⌊‘(𝐾 · 𝑌))))) |
129 | 124, 127,
128 | sylanbrc 583 |
. . . 4
⊢ (𝜑 → (⌊‘(𝐾 · 𝑌)) ∈ ((⌊‘𝑌)...(⌊‘(𝐾 · 𝑌)))) |
130 | | oveq2 7283 |
. . . . . . . 8
⊢ (𝑥 = (⌊‘𝑌) → (((⌊‘𝑌) + 1)...𝑥) = (((⌊‘𝑌) + 1)...(⌊‘𝑌))) |
131 | 130 | raleqdv 3348 |
. . . . . . 7
⊢ (𝑥 = (⌊‘𝑌) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ↔ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))0 ≤ (𝑅‘𝑖))) |
132 | 130 | raleqdv 3348 |
. . . . . . 7
⊢ (𝑥 = (⌊‘𝑌) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0 ↔ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))(𝑅‘𝑖) ≤ 0)) |
133 | 131, 132 | orbi12d 916 |
. . . . . 6
⊢ (𝑥 = (⌊‘𝑌) → ((∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0) ↔ (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))(𝑅‘𝑖) ≤ 0))) |
134 | 133 | imbi2d 341 |
. . . . 5
⊢ (𝑥 = (⌊‘𝑌) → ((𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0)) ↔ (𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))(𝑅‘𝑖) ≤ 0)))) |
135 | | oveq2 7283 |
. . . . . . . 8
⊢ (𝑥 = 𝑚 → (((⌊‘𝑌) + 1)...𝑥) = (((⌊‘𝑌) + 1)...𝑚)) |
136 | 135 | raleqdv 3348 |
. . . . . . 7
⊢ (𝑥 = 𝑚 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ↔ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖))) |
137 | 135 | raleqdv 3348 |
. . . . . . 7
⊢ (𝑥 = 𝑚 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0 ↔ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0)) |
138 | 136, 137 | orbi12d 916 |
. . . . . 6
⊢ (𝑥 = 𝑚 → ((∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0) ↔ (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0))) |
139 | 138 | imbi2d 341 |
. . . . 5
⊢ (𝑥 = 𝑚 → ((𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0)) ↔ (𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0)))) |
140 | | oveq2 7283 |
. . . . . . . 8
⊢ (𝑥 = (𝑚 + 1) → (((⌊‘𝑌) + 1)...𝑥) = (((⌊‘𝑌) + 1)...(𝑚 + 1))) |
141 | 140 | raleqdv 3348 |
. . . . . . 7
⊢ (𝑥 = (𝑚 + 1) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ↔ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖))) |
142 | 140 | raleqdv 3348 |
. . . . . . 7
⊢ (𝑥 = (𝑚 + 1) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0 ↔ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0)) |
143 | 141, 142 | orbi12d 916 |
. . . . . 6
⊢ (𝑥 = (𝑚 + 1) → ((∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0) ↔ (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0))) |
144 | 143 | imbi2d 341 |
. . . . 5
⊢ (𝑥 = (𝑚 + 1) → ((𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0)) ↔ (𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0)))) |
145 | | oveq2 7283 |
. . . . . . . 8
⊢ (𝑥 = (⌊‘(𝐾 · 𝑌)) → (((⌊‘𝑌) + 1)...𝑥) = (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) |
146 | 145 | raleqdv 3348 |
. . . . . . 7
⊢ (𝑥 = (⌊‘(𝐾 · 𝑌)) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ↔ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖))) |
147 | 145 | raleqdv 3348 |
. . . . . . 7
⊢ (𝑥 = (⌊‘(𝐾 · 𝑌)) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0 ↔ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0)) |
148 | 146, 147 | orbi12d 916 |
. . . . . 6
⊢ (𝑥 = (⌊‘(𝐾 · 𝑌)) → ((∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0) ↔ (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0))) |
149 | 148 | imbi2d 341 |
. . . . 5
⊢ (𝑥 = (⌊‘(𝐾 · 𝑌)) → ((𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑥)(𝑅‘𝑖) ≤ 0)) ↔ (𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0)))) |
150 | | elfzle3 13262 |
. . . . . . . . 9
⊢ (𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌)) → ((⌊‘𝑌) + 1) ≤ (⌊‘𝑌)) |
151 | | elfzel2 13254 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌)) → (⌊‘𝑌) ∈
ℤ) |
152 | 151 | zred 12426 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌)) → (⌊‘𝑌) ∈
ℝ) |
153 | 152 | ltp1d 11905 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌)) → (⌊‘𝑌) < ((⌊‘𝑌) + 1)) |
154 | | peano2re 11148 |
. . . . . . . . . . . 12
⊢
((⌊‘𝑌)
∈ ℝ → ((⌊‘𝑌) + 1) ∈ ℝ) |
155 | 152, 154 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌)) → ((⌊‘𝑌) + 1) ∈
ℝ) |
156 | 152, 155 | ltnled 11122 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌)) → ((⌊‘𝑌) < ((⌊‘𝑌) + 1) ↔ ¬
((⌊‘𝑌) + 1)
≤ (⌊‘𝑌))) |
157 | 153, 156 | mpbid 231 |
. . . . . . . . 9
⊢ (𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌)) → ¬
((⌊‘𝑌) + 1)
≤ (⌊‘𝑌)) |
158 | 150, 157 | pm2.21dd 194 |
. . . . . . . 8
⊢ (𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌)) → (𝑅‘𝑖) ≤ 0) |
159 | 158 | rgen 3074 |
. . . . . . 7
⊢
∀𝑖 ∈
(((⌊‘𝑌) +
1)...(⌊‘𝑌))(𝑅‘𝑖) ≤ 0 |
160 | 159 | olci 863 |
. . . . . 6
⊢
(∀𝑖 ∈
(((⌊‘𝑌) +
1)...(⌊‘𝑌))0
≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))(𝑅‘𝑖) ≤ 0) |
161 | 160 | 2a1i 12 |
. . . . 5
⊢
((⌊‘(𝐾
· 𝑌)) ∈
(ℤ≥‘(⌊‘𝑌)) → (𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘𝑌))(𝑅‘𝑖) ≤ 0))) |
162 | | elfzofz 13403 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ((⌊‘𝑌)..^(⌊‘(𝐾 · 𝑌))) → 𝑚 ∈ ((⌊‘𝑌)...(⌊‘(𝐾 · 𝑌)))) |
163 | | elfzp12 13335 |
. . . . . . . . . . 11
⊢
((⌊‘(𝐾
· 𝑌)) ∈
(ℤ≥‘(⌊‘𝑌)) → (𝑚 ∈ ((⌊‘𝑌)...(⌊‘(𝐾 · 𝑌))) ↔ (𝑚 = (⌊‘𝑌) ∨ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))))) |
164 | 124, 163 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑚 ∈ ((⌊‘𝑌)...(⌊‘(𝐾 · 𝑌))) ↔ (𝑚 = (⌊‘𝑌) ∨ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))))) |
165 | 162, 164 | syl5ib 243 |
. . . . . . . . 9
⊢ (𝜑 → (𝑚 ∈ ((⌊‘𝑌)..^(⌊‘(𝐾 · 𝑌))) → (𝑚 = (⌊‘𝑌) ∨ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))))) |
166 | 165 | imp 407 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ((⌊‘𝑌)..^(⌊‘(𝐾 · 𝑌)))) → (𝑚 = (⌊‘𝑌) ∨ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))))) |
167 | 30 | nnrpd 12770 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((⌊‘𝑌) + 1) ∈
ℝ+) |
168 | 36 | ffvelrni 6960 |
. . . . . . . . . . . . . 14
⊢
(((⌊‘𝑌)
+ 1) ∈ ℝ+ → (𝑅‘((⌊‘𝑌) + 1)) ∈ ℝ) |
169 | 167, 168 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑅‘((⌊‘𝑌) + 1)) ∈ ℝ) |
170 | 5, 169 | letrid 11127 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 ≤ (𝑅‘((⌊‘𝑌) + 1)) ∨ (𝑅‘((⌊‘𝑌) + 1)) ≤ 0)) |
171 | 170 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → (0 ≤ (𝑅‘((⌊‘𝑌) + 1)) ∨ (𝑅‘((⌊‘𝑌) + 1)) ≤ 0)) |
172 | | oveq1 7282 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = (⌊‘𝑌) → (𝑚 + 1) = ((⌊‘𝑌) + 1)) |
173 | 172 | oveq2d 7291 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (⌊‘𝑌) → (((⌊‘𝑌) + 1)...(𝑚 + 1)) = (((⌊‘𝑌) + 1)...((⌊‘𝑌) + 1))) |
174 | 4 | flcld 13518 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (⌊‘𝑌) ∈
ℤ) |
175 | 174 | peano2zd 12429 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((⌊‘𝑌) + 1) ∈
ℤ) |
176 | | fzsn 13298 |
. . . . . . . . . . . . . . . 16
⊢
(((⌊‘𝑌)
+ 1) ∈ ℤ → (((⌊‘𝑌) + 1)...((⌊‘𝑌) + 1)) = {((⌊‘𝑌) + 1)}) |
177 | 175, 176 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((⌊‘𝑌) + 1)...((⌊‘𝑌) + 1)) = {((⌊‘𝑌) + 1)}) |
178 | 173, 177 | sylan9eqr 2800 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → (((⌊‘𝑌) + 1)...(𝑚 + 1)) = {((⌊‘𝑌) + 1)}) |
179 | 178 | raleqdv 3348 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ↔ ∀𝑖 ∈ {((⌊‘𝑌) + 1)}0 ≤ (𝑅‘𝑖))) |
180 | | ovex 7308 |
. . . . . . . . . . . . . 14
⊢
((⌊‘𝑌) +
1) ∈ V |
181 | | fveq2 6774 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = ((⌊‘𝑌) + 1) → (𝑅‘𝑖) = (𝑅‘((⌊‘𝑌) + 1))) |
182 | 181 | breq2d 5086 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = ((⌊‘𝑌) + 1) → (0 ≤ (𝑅‘𝑖) ↔ 0 ≤ (𝑅‘((⌊‘𝑌) + 1)))) |
183 | 180, 182 | ralsn 4617 |
. . . . . . . . . . . . 13
⊢
(∀𝑖 ∈
{((⌊‘𝑌) + 1)}0
≤ (𝑅‘𝑖) ↔ 0 ≤ (𝑅‘((⌊‘𝑌) + 1))) |
184 | 179, 183 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ↔ 0 ≤ (𝑅‘((⌊‘𝑌) + 1)))) |
185 | 178 | raleqdv 3348 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0 ↔ ∀𝑖 ∈ {((⌊‘𝑌) + 1)} (𝑅‘𝑖) ≤ 0)) |
186 | 181 | breq1d 5084 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = ((⌊‘𝑌) + 1) → ((𝑅‘𝑖) ≤ 0 ↔ (𝑅‘((⌊‘𝑌) + 1)) ≤ 0)) |
187 | 180, 186 | ralsn 4617 |
. . . . . . . . . . . . 13
⊢
(∀𝑖 ∈
{((⌊‘𝑌) + 1)}
(𝑅‘𝑖) ≤ 0 ↔ (𝑅‘((⌊‘𝑌) + 1)) ≤ 0) |
188 | 185, 187 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0 ↔ (𝑅‘((⌊‘𝑌) + 1)) ≤ 0)) |
189 | 184, 188 | orbi12d 916 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → ((∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0) ↔ (0 ≤ (𝑅‘((⌊‘𝑌) + 1)) ∨ (𝑅‘((⌊‘𝑌) + 1)) ≤ 0))) |
190 | 171, 189 | mpbird 256 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0)) |
191 | 190 | a1d 25 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 = (⌊‘𝑌)) → ((∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0))) |
192 | | elfzuz 13252 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → 𝑚 ∈
(ℤ≥‘((⌊‘𝑌) + 1))) |
193 | 192 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑚 ∈
(ℤ≥‘((⌊‘𝑌) + 1))) |
194 | | eluzfz2 13264 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈
(ℤ≥‘((⌊‘𝑌) + 1)) → 𝑚 ∈ (((⌊‘𝑌) + 1)...𝑚)) |
195 | 193, 194 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑚 ∈ (((⌊‘𝑌) + 1)...𝑚)) |
196 | | fveq2 6774 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝑚 → (𝑅‘𝑖) = (𝑅‘𝑚)) |
197 | 196 | breq2d 5086 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑚 → (0 ≤ (𝑅‘𝑖) ↔ 0 ≤ (𝑅‘𝑚))) |
198 | 197 | rspcv 3557 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ (((⌊‘𝑌) + 1)...𝑚) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) → 0 ≤ (𝑅‘𝑚))) |
199 | 195, 198 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) → 0 ≤ (𝑅‘𝑚))) |
200 | | pntpbnd1.3 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) |
201 | 200 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) |
202 | | eluznn 12658 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((⌊‘𝑌)
+ 1) ∈ ℕ ∧ 𝑚
∈ (ℤ≥‘((⌊‘𝑌) + 1))) → 𝑚 ∈ ℕ) |
203 | 30, 192, 202 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑚 ∈ ℕ) |
204 | 203 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) → 𝑚 ∈ ℕ) |
205 | | elfzle1 13259 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → ((⌊‘𝑌) + 1) ≤ 𝑚) |
206 | 205 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((⌊‘𝑌) + 1) ≤ 𝑚) |
207 | | elfzelz 13256 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → 𝑚 ∈ ℤ) |
208 | | zltp1le 12370 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((⌊‘𝑌)
∈ ℤ ∧ 𝑚
∈ ℤ) → ((⌊‘𝑌) < 𝑚 ↔ ((⌊‘𝑌) + 1) ≤ 𝑚)) |
209 | 174, 207,
208 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((⌊‘𝑌) < 𝑚 ↔ ((⌊‘𝑌) + 1) ≤ 𝑚)) |
210 | 206, 209 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (⌊‘𝑌) < 𝑚) |
211 | | fllt 13526 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑌 ∈ ℝ ∧ 𝑚 ∈ ℤ) → (𝑌 < 𝑚 ↔ (⌊‘𝑌) < 𝑚)) |
212 | 4, 207, 211 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑌 < 𝑚 ↔ (⌊‘𝑌) < 𝑚)) |
213 | 210, 212 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑌 < 𝑚) |
214 | | elfzle2 13260 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌))) → 𝑚 ≤ (⌊‘(𝐾 · 𝑌))) |
215 | 214 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑚 ≤ (⌊‘(𝐾 · 𝑌))) |
216 | | flge 13525 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐾 · 𝑌) ∈ ℝ ∧ 𝑚 ∈ ℤ) → (𝑚 ≤ (𝐾 · 𝑌) ↔ 𝑚 ≤ (⌊‘(𝐾 · 𝑌)))) |
217 | 107, 207,
216 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑚 ≤ (𝐾 · 𝑌) ↔ 𝑚 ≤ (⌊‘(𝐾 · 𝑌)))) |
218 | 215, 217 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑚 ≤ (𝐾 · 𝑌)) |
219 | 213, 218 | jca 512 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑌 < 𝑚 ∧ 𝑚 ≤ (𝐾 · 𝑌))) |
220 | 219 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) → (𝑌 < 𝑚 ∧ 𝑚 ≤ (𝐾 · 𝑌))) |
221 | 9 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) → 𝐸 ∈ (0(,)1)) |
222 | 3 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) → 𝑌 ∈ (𝑋(,)+∞)) |
223 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) → (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) |
224 | 35, 221, 6, 222, 204, 220, 223 | pntpbnd1a 26733 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) → (abs‘((𝑅‘𝑚) / 𝑚)) ≤ 𝐸) |
225 | | breq2 5078 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑚 → (𝑌 < 𝑦 ↔ 𝑌 < 𝑚)) |
226 | | breq1 5077 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑚 → (𝑦 ≤ (𝐾 · 𝑌) ↔ 𝑚 ≤ (𝐾 · 𝑌))) |
227 | 225, 226 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑚 → ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ↔ (𝑌 < 𝑚 ∧ 𝑚 ≤ (𝐾 · 𝑌)))) |
228 | | fveq2 6774 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 𝑚 → (𝑅‘𝑦) = (𝑅‘𝑚)) |
229 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 𝑚 → 𝑦 = 𝑚) |
230 | 228, 229 | oveq12d 7293 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 𝑚 → ((𝑅‘𝑦) / 𝑦) = ((𝑅‘𝑚) / 𝑚)) |
231 | 230 | fveq2d 6778 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑚 → (abs‘((𝑅‘𝑦) / 𝑦)) = (abs‘((𝑅‘𝑚) / 𝑚))) |
232 | 231 | breq1d 5084 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑚 → ((abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸 ↔ (abs‘((𝑅‘𝑚) / 𝑚)) ≤ 𝐸)) |
233 | 227, 232 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑚 → (((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸) ↔ ((𝑌 < 𝑚 ∧ 𝑚 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑚) / 𝑚)) ≤ 𝐸))) |
234 | 233 | rspcev 3561 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈ ℕ ∧ ((𝑌 < 𝑚 ∧ 𝑚 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑚) / 𝑚)) ≤ 𝐸)) → ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) |
235 | 204, 220,
224, 234 | syl12anc 834 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) → ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) |
236 | 201, 235 | mtand 813 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ¬ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) |
237 | 236 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ 0 ≤ (𝑅‘𝑚)) → ¬ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) |
238 | 203 | nnrpd 12770 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → 𝑚 ∈ ℝ+) |
239 | 36 | ffvelrni 6960 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈ ℝ+
→ (𝑅‘𝑚) ∈
ℝ) |
240 | 238, 239 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘𝑚) ∈ ℝ) |
241 | 240 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (𝑅‘𝑚) ∈ ℝ) |
242 | 241 | recnd 11003 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (𝑅‘𝑚) ∈ ℂ) |
243 | 242 | subid1d 11321 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → ((𝑅‘𝑚) − 0) = (𝑅‘𝑚)) |
244 | 203 | peano2nnd 11990 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑚 + 1) ∈ ℕ) |
245 | 244 | nnrpd 12770 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑚 + 1) ∈
ℝ+) |
246 | 36 | ffvelrni 6960 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑚 + 1) ∈ ℝ+
→ (𝑅‘(𝑚 + 1)) ∈
ℝ) |
247 | 245, 246 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (𝑅‘(𝑚 + 1)) ∈ ℝ) |
248 | 247 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (𝑅‘(𝑚 + 1)) ∈ ℝ) |
249 | | 0red 10978 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → 0 ∈
ℝ) |
250 | | 0re 10977 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
ℝ |
251 | | letric 11075 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((0
∈ ℝ ∧ (𝑅‘(𝑚 + 1)) ∈ ℝ) → (0 ≤ (𝑅‘(𝑚 + 1)) ∨ (𝑅‘(𝑚 + 1)) ≤ 0)) |
252 | 250, 247,
251 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (0 ≤ (𝑅‘(𝑚 + 1)) ∨ (𝑅‘(𝑚 + 1)) ≤ 0)) |
253 | 252 | ord 861 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (¬ 0 ≤ (𝑅‘(𝑚 + 1)) → (𝑅‘(𝑚 + 1)) ≤ 0)) |
254 | 253 | imp 407 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1))) → (𝑅‘(𝑚 + 1)) ≤ 0) |
255 | 254 | adantrl 713 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (𝑅‘(𝑚 + 1)) ≤ 0) |
256 | 248, 249,
241, 255 | lesub2dd 11592 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → ((𝑅‘𝑚) − 0) ≤ ((𝑅‘𝑚) − (𝑅‘(𝑚 + 1)))) |
257 | 243, 256 | eqbrtrrd 5098 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (𝑅‘𝑚) ≤ ((𝑅‘𝑚) − (𝑅‘(𝑚 + 1)))) |
258 | | simprl 768 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → 0 ≤ (𝑅‘𝑚)) |
259 | 241, 258 | absidd 15134 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (abs‘(𝑅‘𝑚)) = (𝑅‘𝑚)) |
260 | 248, 249,
241, 255, 258 | letrd 11132 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (𝑅‘(𝑚 + 1)) ≤ (𝑅‘𝑚)) |
261 | 248, 241,
260 | abssuble0d 15144 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚))) = ((𝑅‘𝑚) − (𝑅‘(𝑚 + 1)))) |
262 | 257, 259,
261 | 3brtr4d 5106 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (0 ≤ (𝑅‘𝑚) ∧ ¬ 0 ≤ (𝑅‘(𝑚 + 1)))) → (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) |
263 | 262 | expr 457 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ 0 ≤ (𝑅‘𝑚)) → (¬ 0 ≤ (𝑅‘(𝑚 + 1)) → (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚))))) |
264 | 237, 263 | mt3d 148 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ 0 ≤ (𝑅‘𝑚)) → 0 ≤ (𝑅‘(𝑚 + 1))) |
265 | 264 | ex 413 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (0 ≤ (𝑅‘𝑚) → 0 ≤ (𝑅‘(𝑚 + 1)))) |
266 | 199, 265 | syld 47 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) → 0 ≤ (𝑅‘(𝑚 + 1)))) |
267 | | ovex 7308 |
. . . . . . . . . . . . . 14
⊢ (𝑚 + 1) ∈ V |
268 | | fveq2 6774 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑚 + 1) → (𝑅‘𝑖) = (𝑅‘(𝑚 + 1))) |
269 | 268 | breq2d 5086 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑚 + 1) → (0 ≤ (𝑅‘𝑖) ↔ 0 ≤ (𝑅‘(𝑚 + 1)))) |
270 | 267, 269 | ralsn 4617 |
. . . . . . . . . . . . 13
⊢
(∀𝑖 ∈
{(𝑚 + 1)}0 ≤ (𝑅‘𝑖) ↔ 0 ≤ (𝑅‘(𝑚 + 1))) |
271 | 266, 270 | syl6ibr 251 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) → ∀𝑖 ∈ {(𝑚 + 1)}0 ≤ (𝑅‘𝑖))) |
272 | 271 | ancld 551 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) ∧ ∀𝑖 ∈ {(𝑚 + 1)}0 ≤ (𝑅‘𝑖)))) |
273 | | fzsuc 13303 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈
(ℤ≥‘((⌊‘𝑌) + 1)) → (((⌊‘𝑌) + 1)...(𝑚 + 1)) = ((((⌊‘𝑌) + 1)...𝑚) ∪ {(𝑚 + 1)})) |
274 | 193, 273 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (((⌊‘𝑌) + 1)...(𝑚 + 1)) = ((((⌊‘𝑌) + 1)...𝑚) ∪ {(𝑚 + 1)})) |
275 | 274 | raleqdv 3348 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ↔ ∀𝑖 ∈ ((((⌊‘𝑌) + 1)...𝑚) ∪ {(𝑚 + 1)})0 ≤ (𝑅‘𝑖))) |
276 | | ralunb 4125 |
. . . . . . . . . . . 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 258 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) → ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖))) |
279 | 196 | breq1d 5084 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑚 → ((𝑅‘𝑖) ≤ 0 ↔ (𝑅‘𝑚) ≤ 0)) |
280 | 279 | rspcv 3557 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ (((⌊‘𝑌) + 1)...𝑚) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0 → (𝑅‘𝑚) ≤ 0)) |
281 | 195, 280 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0 → (𝑅‘𝑚) ≤ 0)) |
282 | 236 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (𝑅‘𝑚) ≤ 0) → ¬ (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) |
283 | 253 | con1d 145 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (¬ (𝑅‘(𝑚 + 1)) ≤ 0 → 0 ≤ (𝑅‘(𝑚 + 1)))) |
284 | 283 | imp 407 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0) → 0 ≤ (𝑅‘(𝑚 + 1))) |
285 | 284 | adantrl 713 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → 0 ≤ (𝑅‘(𝑚 + 1))) |
286 | 240 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (𝑅‘𝑚) ∈ ℝ) |
287 | 286 | renegcld 11402 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → -(𝑅‘𝑚) ∈ ℝ) |
288 | 247 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (𝑅‘(𝑚 + 1)) ∈ ℝ) |
289 | 287, 288 | addge02d 11564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (0 ≤ (𝑅‘(𝑚 + 1)) ↔ -(𝑅‘𝑚) ≤ ((𝑅‘(𝑚 + 1)) + -(𝑅‘𝑚)))) |
290 | 285, 289 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → -(𝑅‘𝑚) ≤ ((𝑅‘(𝑚 + 1)) + -(𝑅‘𝑚))) |
291 | 288 | recnd 11003 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (𝑅‘(𝑚 + 1)) ∈ ℂ) |
292 | 286 | recnd 11003 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (𝑅‘𝑚) ∈ ℂ) |
293 | 291, 292 | negsubd 11338 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → ((𝑅‘(𝑚 + 1)) + -(𝑅‘𝑚)) = ((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚))) |
294 | 290, 293 | breqtrd 5100 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → -(𝑅‘𝑚) ≤ ((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚))) |
295 | | simprl 768 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (𝑅‘𝑚) ≤ 0) |
296 | 286, 295 | absnidd 15125 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (abs‘(𝑅‘𝑚)) = -(𝑅‘𝑚)) |
297 | | 0red 10978 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → 0 ∈
ℝ) |
298 | 286, 297,
288, 295, 285 | letrd 11132 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (𝑅‘𝑚) ≤ (𝑅‘(𝑚 + 1))) |
299 | 286, 288,
298 | abssubge0d 15143 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚))) = ((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚))) |
300 | 294, 296,
299 | 3brtr4d 5106 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ ((𝑅‘𝑚) ≤ 0 ∧ ¬ (𝑅‘(𝑚 + 1)) ≤ 0)) → (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚)))) |
301 | 300 | expr 457 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (𝑅‘𝑚) ≤ 0) → (¬ (𝑅‘(𝑚 + 1)) ≤ 0 → (abs‘(𝑅‘𝑚)) ≤ (abs‘((𝑅‘(𝑚 + 1)) − (𝑅‘𝑚))))) |
302 | 282, 301 | mt3d 148 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) ∧ (𝑅‘𝑚) ≤ 0) → (𝑅‘(𝑚 + 1)) ≤ 0) |
303 | 302 | ex 413 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((𝑅‘𝑚) ≤ 0 → (𝑅‘(𝑚 + 1)) ≤ 0)) |
304 | 281, 303 | syld 47 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0 → (𝑅‘(𝑚 + 1)) ≤ 0)) |
305 | 268 | breq1d 5084 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑚 + 1) → ((𝑅‘𝑖) ≤ 0 ↔ (𝑅‘(𝑚 + 1)) ≤ 0)) |
306 | 267, 305 | ralsn 4617 |
. . . . . . . . . . . . 13
⊢
(∀𝑖 ∈
{(𝑚 + 1)} (𝑅‘𝑖) ≤ 0 ↔ (𝑅‘(𝑚 + 1)) ≤ 0) |
307 | 304, 306 | syl6ibr 251 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0 → ∀𝑖 ∈ {(𝑚 + 1)} (𝑅‘𝑖) ≤ 0)) |
308 | 307 | ancld 551 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0 ∧ ∀𝑖 ∈ {(𝑚 + 1)} (𝑅‘𝑖) ≤ 0))) |
309 | 274 | raleqdv 3348 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0 ↔ ∀𝑖 ∈ ((((⌊‘𝑌) + 1)...𝑚) ∪ {(𝑚 + 1)})(𝑅‘𝑖) ≤ 0)) |
310 | | ralunb 4125 |
. . . . . . . . . . . 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 258 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0 → ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0)) |
313 | 278, 312 | orim12d 962 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) → ((∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...𝑚)(𝑅‘𝑖) ≤ 0) → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(𝑚 + 1))(𝑅‘𝑖) ≤ 0))) |
314 | 191, 313 | jaodan 955 |
. . . . . . . 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 414 |
. . . . . 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 13505 |
. . . 4
⊢
((⌊‘(𝐾
· 𝑌)) ∈
((⌊‘𝑌)...(⌊‘(𝐾 · 𝑌))) → (𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0))) |
319 | 129, 318 | mpcom 38 |
. . 3
⊢ (𝜑 → (∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))0 ≤ (𝑅‘𝑖) ∨ ∀𝑖 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(𝑅‘𝑖) ≤ 0)) |
320 | 58, 92, 319 | mpjaodan 956 |
. 2
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
321 | | pntpbnd1.2 |
. . 3
⊢ (𝜑 → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℤ (abs‘Σ𝑦 ∈ (𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴) |
322 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑦 = 𝑛 → (𝑅‘𝑦) = (𝑅‘𝑛)) |
323 | | id 22 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑛 → 𝑦 = 𝑛) |
324 | | oveq1 7282 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑛 → (𝑦 + 1) = (𝑛 + 1)) |
325 | 323, 324 | oveq12d 7293 |
. . . . . . . . 9
⊢ (𝑦 = 𝑛 → (𝑦 · (𝑦 + 1)) = (𝑛 · (𝑛 + 1))) |
326 | 322, 325 | oveq12d 7293 |
. . . . . . . 8
⊢ (𝑦 = 𝑛 → ((𝑅‘𝑦) / (𝑦 · (𝑦 + 1))) = ((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
327 | 326 | cbvsumv 15408 |
. . . . . . 7
⊢
Σ𝑦 ∈
(𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1))) = Σ𝑛 ∈ (𝑖...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) |
328 | | oveq1 7282 |
. . . . . . . 8
⊢ (𝑖 = ((⌊‘𝑌) + 1) → (𝑖...𝑗) = (((⌊‘𝑌) + 1)...𝑗)) |
329 | 328 | sumeq1d 15413 |
. . . . . . 7
⊢ (𝑖 = ((⌊‘𝑌) + 1) → Σ𝑛 ∈ (𝑖...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
330 | 327, 329 | eqtrid 2790 |
. . . . . 6
⊢ (𝑖 = ((⌊‘𝑌) + 1) → Σ𝑦 ∈ (𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
331 | 330 | fveq2d 6778 |
. . . . 5
⊢ (𝑖 = ((⌊‘𝑌) + 1) →
(abs‘Σ𝑦 ∈
(𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) = (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
332 | 331 | breq1d 5084 |
. . . 4
⊢ (𝑖 = ((⌊‘𝑌) + 1) →
((abs‘Σ𝑦 ∈
(𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴 ↔ (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴)) |
333 | | oveq2 7283 |
. . . . . . 7
⊢ (𝑗 = (⌊‘(𝐾 · 𝑌)) → (((⌊‘𝑌) + 1)...𝑗) = (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))) |
334 | 333 | sumeq1d 15413 |
. . . . . 6
⊢ (𝑗 = (⌊‘(𝐾 · 𝑌)) → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))) = Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) |
335 | 334 | fveq2d 6778 |
. . . . 5
⊢ (𝑗 = (⌊‘(𝐾 · 𝑌)) → (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) = (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1))))) |
336 | 335 | breq1d 5084 |
. . . 4
⊢ (𝑗 = (⌊‘(𝐾 · 𝑌)) → ((abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...𝑗)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴 ↔ (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴)) |
337 | 332, 336 | rspc2va 3571 |
. . 3
⊢
(((((⌊‘𝑌) + 1) ∈ ℕ ∧
(⌊‘(𝐾 ·
𝑌)) ∈ ℤ) ∧
∀𝑖 ∈ ℕ
∀𝑗 ∈ ℤ
(abs‘Σ𝑦 ∈
(𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴) → (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴) |
338 | 30, 125, 321, 337 | syl21anc 835 |
. 2
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴) |
339 | 320, 338 | eqbrtrrd 5098 |
1
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴) |