Proof of Theorem dvfsumlem1
| Step | Hyp | Ref
| Expression |
| 1 | | dvfsum.s |
. . . . . . . . . 10
⊢ 𝑆 = (𝑇(,)+∞) |
| 2 | | ioossre 13448 |
. . . . . . . . . 10
⊢ (𝑇(,)+∞) ⊆
ℝ |
| 3 | 1, 2 | eqsstri 4030 |
. . . . . . . . 9
⊢ 𝑆 ⊆
ℝ |
| 4 | | dvfsumlem1.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ 𝑆) |
| 5 | 3, 4 | sselid 3981 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ ℝ) |
| 6 | | dvfsumlem1.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝑆) |
| 7 | 3, 6 | sselid 3981 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 8 | 7 | flcld 13838 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘𝑋) ∈
ℤ) |
| 9 | | reflcl 13836 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℝ →
(⌊‘𝑋) ∈
ℝ) |
| 10 | 7, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘𝑋) ∈
ℝ) |
| 11 | | flle 13839 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℝ →
(⌊‘𝑋) ≤
𝑋) |
| 12 | 7, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘𝑋) ≤ 𝑋) |
| 13 | | dvfsumlem1.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ≤ 𝑌) |
| 14 | 10, 7, 5, 12, 13 | letrd 11418 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘𝑋) ≤ 𝑌) |
| 15 | | flbi 13856 |
. . . . . . . . 9
⊢ ((𝑌 ∈ ℝ ∧
(⌊‘𝑋) ∈
ℤ) → ((⌊‘𝑌) = (⌊‘𝑋) ↔ ((⌊‘𝑋) ≤ 𝑌 ∧ 𝑌 < ((⌊‘𝑋) + 1)))) |
| 16 | 15 | baibd 539 |
. . . . . . . 8
⊢ (((𝑌 ∈ ℝ ∧
(⌊‘𝑋) ∈
ℤ) ∧ (⌊‘𝑋) ≤ 𝑌) → ((⌊‘𝑌) = (⌊‘𝑋) ↔ 𝑌 < ((⌊‘𝑋) + 1))) |
| 17 | 5, 8, 14, 16 | syl21anc 838 |
. . . . . . 7
⊢ (𝜑 → ((⌊‘𝑌) = (⌊‘𝑋) ↔ 𝑌 < ((⌊‘𝑋) + 1))) |
| 18 | 17 | biimpar 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 < ((⌊‘𝑋) + 1)) → (⌊‘𝑌) = (⌊‘𝑋)) |
| 19 | 18 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 < ((⌊‘𝑋) + 1)) → (𝑌 − (⌊‘𝑌)) = (𝑌 − (⌊‘𝑋))) |
| 20 | 19 | oveq1d 7446 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 < ((⌊‘𝑋) + 1)) → ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) = ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵)) |
| 21 | 18 | oveq2d 7447 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 < ((⌊‘𝑋) + 1)) → (𝑀...(⌊‘𝑌)) = (𝑀...(⌊‘𝑋))) |
| 22 | 21 | sumeq1d 15736 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 < ((⌊‘𝑋) + 1)) → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) |
| 23 | 22 | oveq1d 7446 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 < ((⌊‘𝑋) + 1)) → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) |
| 24 | 20, 23 | oveq12d 7449 |
. . 3
⊢ ((𝜑 ∧ 𝑌 < ((⌊‘𝑋) + 1)) → (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) |
| 25 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → 𝑌 = ((⌊‘𝑋) + 1)) |
| 26 | 7 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → 𝑋 ∈ ℝ) |
| 27 | 26 | flcld 13838 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → (⌊‘𝑋) ∈
ℤ) |
| 28 | 27 | peano2zd 12725 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → ((⌊‘𝑋) + 1) ∈
ℤ) |
| 29 | 25, 28 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → 𝑌 ∈ ℤ) |
| 30 | | flid 13848 |
. . . . . . . . . 10
⊢ (𝑌 ∈ ℤ →
(⌊‘𝑌) = 𝑌) |
| 31 | 29, 30 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → (⌊‘𝑌) = 𝑌) |
| 32 | 31, 25 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → (⌊‘𝑌) = ((⌊‘𝑋) + 1)) |
| 33 | 32 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → (𝑌 − (⌊‘𝑌)) = (𝑌 − ((⌊‘𝑋) + 1))) |
| 34 | 33 | oveq1d 7446 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) = ((𝑌 − ((⌊‘𝑋) + 1)) · ⦋𝑌 / 𝑥⦌𝐵)) |
| 35 | 5 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ℂ) |
| 36 | 10 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝜑 → (⌊‘𝑋) ∈
ℂ) |
| 37 | 35, 36 | subcld 11620 |
. . . . . . . . 9
⊢ (𝜑 → (𝑌 − (⌊‘𝑋)) ∈ ℂ) |
| 38 | | 1cnd 11256 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) |
| 39 | 3 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ⊆ ℝ) |
| 40 | | dvfsum.a |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℝ) |
| 41 | | dvfsum.b1 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ 𝑉) |
| 42 | | dvfsum.b3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D (𝑥 ∈ 𝑆 ↦ 𝐴)) = (𝑥 ∈ 𝑆 ↦ 𝐵)) |
| 43 | 39, 40, 41, 42 | dvmptrecl 26064 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℝ) |
| 44 | 43 | recnd 11289 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ ℂ) |
| 45 | 44 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐵 ∈ ℂ) |
| 46 | | nfcsb1v 3923 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥⦋𝑌 / 𝑥⦌𝐵 |
| 47 | 46 | nfel1 2922 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ |
| 48 | | csbeq1a 3913 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑌 → 𝐵 = ⦋𝑌 / 𝑥⦌𝐵) |
| 49 | 48 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑌 → (𝐵 ∈ ℂ ↔ ⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ)) |
| 50 | 47, 49 | rspc 3610 |
. . . . . . . . . 10
⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐵 ∈ ℂ → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ)) |
| 51 | 4, 45, 50 | sylc 65 |
. . . . . . . . 9
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ) |
| 52 | 37, 38, 51 | subdird 11720 |
. . . . . . . 8
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (1 · ⦋𝑌 / 𝑥⦌𝐵))) |
| 53 | 35, 36, 38 | subsub4d 11651 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) − 1) = (𝑌 − ((⌊‘𝑋) + 1))) |
| 54 | 53 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) − 1) · ⦋𝑌 / 𝑥⦌𝐵) = ((𝑌 − ((⌊‘𝑋) + 1)) · ⦋𝑌 / 𝑥⦌𝐵)) |
| 55 | 51 | mullidd 11279 |
. . . . . . . . 9
⊢ (𝜑 → (1 ·
⦋𝑌 / 𝑥⦌𝐵) = ⦋𝑌 / 𝑥⦌𝐵) |
| 56 | 55 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝜑 → (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − (1 · ⦋𝑌 / 𝑥⦌𝐵)) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵)) |
| 57 | 52, 54, 56 | 3eqtr3d 2785 |
. . . . . . 7
⊢ (𝜑 → ((𝑌 − ((⌊‘𝑋) + 1)) · ⦋𝑌 / 𝑥⦌𝐵) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵)) |
| 58 | 57 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → ((𝑌 − ((⌊‘𝑋) + 1)) · ⦋𝑌 / 𝑥⦌𝐵) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵)) |
| 59 | 34, 58 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵)) |
| 60 | | dvfsum.m |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 61 | 8 | peano2zd 12725 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((⌊‘𝑋) + 1) ∈
ℤ) |
| 62 | 60 | zred 12722 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 63 | | peano2rem 11576 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℝ → (𝑀 − 1) ∈
ℝ) |
| 64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 − 1) ∈ ℝ) |
| 65 | | dvfsum.d |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐷 ∈ ℝ) |
| 66 | | dvfsum.md |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ≤ (𝐷 + 1)) |
| 67 | | 1red 11262 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈
ℝ) |
| 68 | 62, 67, 65 | lesubaddd 11860 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑀 − 1) ≤ 𝐷 ↔ 𝑀 ≤ (𝐷 + 1))) |
| 69 | 66, 68 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 − 1) ≤ 𝐷) |
| 70 | | dvfsumlem1.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐷 ≤ 𝑋) |
| 71 | 64, 65, 7, 69, 70 | letrd 11418 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 − 1) ≤ 𝑋) |
| 72 | | peano2zm 12660 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
| 73 | 60, 72 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 − 1) ∈ ℤ) |
| 74 | | flge 13845 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ ℝ ∧ (𝑀 − 1) ∈ ℤ)
→ ((𝑀 − 1) ≤
𝑋 ↔ (𝑀 − 1) ≤ (⌊‘𝑋))) |
| 75 | 7, 73, 74 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑀 − 1) ≤ 𝑋 ↔ (𝑀 − 1) ≤ (⌊‘𝑋))) |
| 76 | 71, 75 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀 − 1) ≤ (⌊‘𝑋)) |
| 77 | 62, 67, 10 | lesubaddd 11860 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑀 − 1) ≤ (⌊‘𝑋) ↔ 𝑀 ≤ ((⌊‘𝑋) + 1))) |
| 78 | 76, 77 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ≤ ((⌊‘𝑋) + 1)) |
| 79 | | eluz2 12884 |
. . . . . . . . . . . 12
⊢
(((⌊‘𝑋)
+ 1) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ ((⌊‘𝑋) + 1) ∈ ℤ ∧
𝑀 ≤
((⌊‘𝑋) +
1))) |
| 80 | 60, 61, 78, 79 | syl3anbrc 1344 |
. . . . . . . . . . 11
⊢ (𝜑 → ((⌊‘𝑋) + 1) ∈
(ℤ≥‘𝑀)) |
| 81 | | dvfsum.b2 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℝ) |
| 82 | 81 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ ℂ) |
| 83 | 82 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ 𝑍 𝐵 ∈ ℂ) |
| 84 | | elfzuz 13560 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑀...((⌊‘𝑋) + 1)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 85 | | dvfsum.z |
. . . . . . . . . . . . 13
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 86 | 84, 85 | eleqtrrdi 2852 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑀...((⌊‘𝑋) + 1)) → 𝑘 ∈ 𝑍) |
| 87 | | dvfsum.c |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑘 → 𝐵 = 𝐶) |
| 88 | 87 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑘 → (𝐵 ∈ ℂ ↔ 𝐶 ∈ ℂ)) |
| 89 | 88 | rspccva 3621 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
𝑍 𝐵 ∈ ℂ ∧ 𝑘 ∈ 𝑍) → 𝐶 ∈ ℂ) |
| 90 | 83, 86, 89 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...((⌊‘𝑋) + 1))) → 𝐶 ∈ ℂ) |
| 91 | | eqvisset 3500 |
. . . . . . . . . . . . 13
⊢ (𝑘 = ((⌊‘𝑋) + 1) →
((⌊‘𝑋) + 1)
∈ V) |
| 92 | | eqeq2 2749 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = ((⌊‘𝑋) + 1) → (𝑥 = 𝑘 ↔ 𝑥 = ((⌊‘𝑋) + 1))) |
| 93 | 92 | biimpar 477 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 = ((⌊‘𝑋) + 1) ∧ 𝑥 = ((⌊‘𝑋) + 1)) → 𝑥 = 𝑘) |
| 94 | 93, 87 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑘 = ((⌊‘𝑋) + 1) ∧ 𝑥 = ((⌊‘𝑋) + 1)) → 𝐵 = 𝐶) |
| 95 | 91, 94 | csbied 3935 |
. . . . . . . . . . . 12
⊢ (𝑘 = ((⌊‘𝑋) + 1) →
⦋((⌊‘𝑋) + 1) / 𝑥⦌𝐵 = 𝐶) |
| 96 | 95 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝑘 = ((⌊‘𝑋) + 1) → 𝐶 = ⦋((⌊‘𝑋) + 1) / 𝑥⦌𝐵) |
| 97 | 80, 90, 96 | fsumm1 15787 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...((⌊‘𝑋) + 1))𝐶 = (Σ𝑘 ∈ (𝑀...(((⌊‘𝑋) + 1) − 1))𝐶 + ⦋((⌊‘𝑋) + 1) / 𝑥⦌𝐵)) |
| 98 | | ax-1cn 11213 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
| 99 | | pncan 11514 |
. . . . . . . . . . . . . 14
⊢
(((⌊‘𝑋)
∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝑋) + 1) − 1) =
(⌊‘𝑋)) |
| 100 | 36, 98, 99 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((⌊‘𝑋) + 1) − 1) =
(⌊‘𝑋)) |
| 101 | 100 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀...(((⌊‘𝑋) + 1) − 1)) = (𝑀...(⌊‘𝑋))) |
| 102 | 101 | sumeq1d 15736 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(((⌊‘𝑋) + 1) − 1))𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) |
| 103 | 102 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(((⌊‘𝑋) + 1) − 1))𝐶 + ⦋((⌊‘𝑋) + 1) / 𝑥⦌𝐵) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 + ⦋((⌊‘𝑋) + 1) / 𝑥⦌𝐵)) |
| 104 | 97, 103 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...((⌊‘𝑋) + 1))𝐶 = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 + ⦋((⌊‘𝑋) + 1) / 𝑥⦌𝐵)) |
| 105 | 104 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → Σ𝑘 ∈ (𝑀...((⌊‘𝑋) + 1))𝐶 = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 + ⦋((⌊‘𝑋) + 1) / 𝑥⦌𝐵)) |
| 106 | 32 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → (𝑀...(⌊‘𝑌)) = (𝑀...((⌊‘𝑋) + 1))) |
| 107 | 106 | sumeq1d 15736 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 = Σ𝑘 ∈ (𝑀...((⌊‘𝑋) + 1))𝐶) |
| 108 | 25 | csbeq1d 3903 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → ⦋𝑌 / 𝑥⦌𝐵 = ⦋((⌊‘𝑋) + 1) / 𝑥⦌𝐵) |
| 109 | 108 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 + ⦋𝑌 / 𝑥⦌𝐵) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 + ⦋((⌊‘𝑋) + 1) / 𝑥⦌𝐵)) |
| 110 | 105, 107,
109 | 3eqtr4d 2787 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 = (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 + ⦋𝑌 / 𝑥⦌𝐵)) |
| 111 | 110 | oveq1d 7446 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 + ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴)) |
| 112 | | fzfid 14014 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀...(⌊‘𝑋)) ∈ Fin) |
| 113 | | elfzuz 13560 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
| 114 | 113, 85 | eleqtrrdi 2852 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝑀...(⌊‘𝑋)) → 𝑘 ∈ 𝑍) |
| 115 | 83, 114, 89 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(⌊‘𝑋))) → 𝐶 ∈ ℂ) |
| 116 | 112, 115 | fsumcl 15769 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 ∈ ℂ) |
| 117 | 40 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ ℂ) |
| 118 | 117 | ralrimiva 3146 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 𝐴 ∈ ℂ) |
| 119 | | nfcsb1v 3923 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥⦋𝑌 / 𝑥⦌𝐴 |
| 120 | 119 | nfel1 2922 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⦋𝑌 / 𝑥⦌𝐴 ∈ ℂ |
| 121 | | csbeq1a 3913 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑌 → 𝐴 = ⦋𝑌 / 𝑥⦌𝐴) |
| 122 | 121 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑌 → (𝐴 ∈ ℂ ↔ ⦋𝑌 / 𝑥⦌𝐴 ∈ ℂ)) |
| 123 | 120, 122 | rspc 3610 |
. . . . . . . . 9
⊢ (𝑌 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 𝐴 ∈ ℂ → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℂ)) |
| 124 | 4, 118, 123 | sylc 65 |
. . . . . . . 8
⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐴 ∈ ℂ) |
| 125 | 116, 51, 124 | addsubd 11641 |
. . . . . . 7
⊢ (𝜑 → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 + ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + ⦋𝑌 / 𝑥⦌𝐵)) |
| 126 | 125 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → ((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 + ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + ⦋𝑌 / 𝑥⦌𝐵)) |
| 127 | 111, 126 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) = ((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + ⦋𝑌 / 𝑥⦌𝐵)) |
| 128 | 59, 127 | oveq12d 7449 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵) + ((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + ⦋𝑌 / 𝑥⦌𝐵))) |
| 129 | 37, 51 | mulcld 11281 |
. . . . . 6
⊢ (𝜑 → ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℂ) |
| 130 | 129 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → ((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) ∈ ℂ) |
| 131 | 51 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → ⦋𝑌 / 𝑥⦌𝐵 ∈ ℂ) |
| 132 | 116, 124 | subcld 11620 |
. . . . . 6
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℂ) |
| 133 | 132 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) ∈ ℂ) |
| 134 | 130, 131,
133 | nppcan3d 11647 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐵) + ((Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) + ⦋𝑌 / 𝑥⦌𝐵)) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) |
| 135 | 128, 134 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑌 = ((⌊‘𝑋) + 1)) → (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) |
| 136 | | dvfsumlem1.6 |
. . . 4
⊢ (𝜑 → 𝑌 ≤ ((⌊‘𝑋) + 1)) |
| 137 | | peano2re 11434 |
. . . . . 6
⊢
((⌊‘𝑋)
∈ ℝ → ((⌊‘𝑋) + 1) ∈ ℝ) |
| 138 | 10, 137 | syl 17 |
. . . . 5
⊢ (𝜑 → ((⌊‘𝑋) + 1) ∈
ℝ) |
| 139 | 5, 138 | leloed 11404 |
. . . 4
⊢ (𝜑 → (𝑌 ≤ ((⌊‘𝑋) + 1) ↔ (𝑌 < ((⌊‘𝑋) + 1) ∨ 𝑌 = ((⌊‘𝑋) + 1)))) |
| 140 | 136, 139 | mpbid 232 |
. . 3
⊢ (𝜑 → (𝑌 < ((⌊‘𝑋) + 1) ∨ 𝑌 = ((⌊‘𝑋) + 1))) |
| 141 | 24, 135, 140 | mpjaodan 961 |
. 2
⊢ (𝜑 → (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) |
| 142 | | ovex 7464 |
. . 3
⊢ (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ V |
| 143 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑥𝑌 |
| 144 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥(𝑌 − (⌊‘𝑌)) |
| 145 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥
· |
| 146 | 144, 145,
46 | nfov 7461 |
. . . . 5
⊢
Ⅎ𝑥((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) |
| 147 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑥
+ |
| 148 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 |
| 149 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑥
− |
| 150 | 148, 149,
119 | nfov 7461 |
. . . . 5
⊢
Ⅎ𝑥(Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴) |
| 151 | 146, 147,
150 | nfov 7461 |
. . . 4
⊢
Ⅎ𝑥(((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) |
| 152 | | id 22 |
. . . . . . 7
⊢ (𝑥 = 𝑌 → 𝑥 = 𝑌) |
| 153 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑥 = 𝑌 → (⌊‘𝑥) = (⌊‘𝑌)) |
| 154 | 152, 153 | oveq12d 7449 |
. . . . . 6
⊢ (𝑥 = 𝑌 → (𝑥 − (⌊‘𝑥)) = (𝑌 − (⌊‘𝑌))) |
| 155 | 154, 48 | oveq12d 7449 |
. . . . 5
⊢ (𝑥 = 𝑌 → ((𝑥 − (⌊‘𝑥)) · 𝐵) = ((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵)) |
| 156 | 153 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑥 = 𝑌 → (𝑀...(⌊‘𝑥)) = (𝑀...(⌊‘𝑌))) |
| 157 | 156 | sumeq1d 15736 |
. . . . . 6
⊢ (𝑥 = 𝑌 → Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 = Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶) |
| 158 | 157, 121 | oveq12d 7449 |
. . . . 5
⊢ (𝑥 = 𝑌 → (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴) = (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) |
| 159 | 155, 158 | oveq12d 7449 |
. . . 4
⊢ (𝑥 = 𝑌 → (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴)) = (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) |
| 160 | | dvfsum.h |
. . . 4
⊢ 𝐻 = (𝑥 ∈ 𝑆 ↦ (((𝑥 − (⌊‘𝑥)) · 𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶 − 𝐴))) |
| 161 | 143, 151,
159, 160 | fvmptf 7037 |
. . 3
⊢ ((𝑌 ∈ 𝑆 ∧ (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴)) ∈ V) → (𝐻‘𝑌) = (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) |
| 162 | 4, 142, 161 | sylancl 586 |
. 2
⊢ (𝜑 → (𝐻‘𝑌) = (((𝑌 − (⌊‘𝑌)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑌))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) |
| 163 | 129, 124,
116 | subadd23d 11642 |
. 2
⊢ (𝜑 → ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶) = (((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) + (Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶 − ⦋𝑌 / 𝑥⦌𝐴))) |
| 164 | 141, 162,
163 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (𝐻‘𝑌) = ((((𝑌 − (⌊‘𝑋)) · ⦋𝑌 / 𝑥⦌𝐵) − ⦋𝑌 / 𝑥⦌𝐴) + Σ𝑘 ∈ (𝑀...(⌊‘𝑋))𝐶)) |