| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fzofi 14016 | . . . 4
⊢ (𝑀..^𝑁) ∈ Fin | 
| 2 | 1 | a1i 11 | . . 3
⊢ (𝜑 → (𝑀..^𝑁) ∈ Fin) | 
| 3 |  | dvfsumleOLD.x | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℝ) | 
| 4 |  | dvfsumleOLD.m | . . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) | 
| 5 |  | eluzel2 12884 | . . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | 
| 6 | 4, 5 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 7 |  | eluzelz 12889 | . . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) | 
| 8 | 4, 7 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 9 |  | fzval2 13551 | . . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ)) | 
| 10 | 6, 8, 9 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ)) | 
| 11 |  | inss1 4236 | . . . . . . . . 9
⊢ ((𝑀[,]𝑁) ∩ ℤ) ⊆ (𝑀[,]𝑁) | 
| 12 | 10, 11 | eqsstrdi 4027 | . . . . . . . 8
⊢ (𝜑 → (𝑀...𝑁) ⊆ (𝑀[,]𝑁)) | 
| 13 | 12 | sselda 3982 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀...𝑁)) → 𝑦 ∈ (𝑀[,]𝑁)) | 
| 14 |  | dvfsumleOLD.a | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ)) | 
| 15 |  | cncff 24920 | . . . . . . . . . 10
⊢ ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) | 
| 16 | 14, 15 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) | 
| 17 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) = (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) | 
| 18 | 17 | fmpt 7129 | . . . . . . . . 9
⊢
(∀𝑥 ∈
(𝑀[,]𝑁)𝐴 ∈ ℝ ↔ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) | 
| 19 | 16, 18 | sylibr 234 | . . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ) | 
| 20 |  | nfcsb1v 3922 | . . . . . . . . . 10
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐴 | 
| 21 | 20 | nfel1 2921 | . . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ | 
| 22 |  | csbeq1a 3912 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → 𝐴 = ⦋𝑦 / 𝑥⦌𝐴) | 
| 23 | 22 | eleq1d 2825 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐴 ∈ ℝ ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ)) | 
| 24 | 21, 23 | rspc 3609 | . . . . . . . 8
⊢ (𝑦 ∈ (𝑀[,]𝑁) → (∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ)) | 
| 25 | 19, 24 | mpan9 506 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀[,]𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ) | 
| 26 | 13, 25 | syldan 591 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀...𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ) | 
| 27 | 26 | ralrimiva 3145 | . . . . 5
⊢ (𝜑 → ∀𝑦 ∈ (𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ) | 
| 28 |  | fzofzp1 13804 | . . . . 5
⊢ (𝑘 ∈ (𝑀..^𝑁) → (𝑘 + 1) ∈ (𝑀...𝑁)) | 
| 29 |  | csbeq1 3901 | . . . . . . 7
⊢ (𝑦 = (𝑘 + 1) → ⦋𝑦 / 𝑥⦌𝐴 = ⦋(𝑘 + 1) / 𝑥⦌𝐴) | 
| 30 | 29 | eleq1d 2825 | . . . . . 6
⊢ (𝑦 = (𝑘 + 1) → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℝ)) | 
| 31 | 30 | rspccva 3620 | . . . . 5
⊢
((∀𝑦 ∈
(𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℝ) | 
| 32 | 27, 28, 31 | syl2an 596 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℝ) | 
| 33 |  | elfzofz 13716 | . . . . 5
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ (𝑀...𝑁)) | 
| 34 |  | csbeq1 3901 | . . . . . . 7
⊢ (𝑦 = 𝑘 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑘 / 𝑥⦌𝐴) | 
| 35 | 34 | eleq1d 2825 | . . . . . 6
⊢ (𝑦 = 𝑘 → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ ⦋𝑘 / 𝑥⦌𝐴 ∈ ℝ)) | 
| 36 | 35 | rspccva 3620 | . . . . 5
⊢
((∀𝑦 ∈
(𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ∧ 𝑘 ∈ (𝑀...𝑁)) → ⦋𝑘 / 𝑥⦌𝐴 ∈ ℝ) | 
| 37 | 27, 33, 36 | syl2an 596 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ⦋𝑘 / 𝑥⦌𝐴 ∈ ℝ) | 
| 38 | 32, 37 | resubcld 11692 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴) ∈ ℝ) | 
| 39 |  | elfzoelz 13700 | . . . . . . . . . 10
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ ℤ) | 
| 40 | 39 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℤ) | 
| 41 | 40 | zred 12724 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℝ) | 
| 42 | 41 | recnd 11290 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℂ) | 
| 43 |  | ax-1cn 11214 | . . . . . . 7
⊢ 1 ∈
ℂ | 
| 44 |  | pncan2 11516 | . . . . . . 7
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 + 1)
− 𝑘) =
1) | 
| 45 | 42, 43, 44 | sylancl 586 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑘 + 1) − 𝑘) = 1) | 
| 46 | 45 | oveq2d 7448 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · ((𝑘 + 1) − 𝑘)) = (𝑋 · 1)) | 
| 47 | 3 | recnd 11290 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℂ) | 
| 48 |  | peano2re 11435 | . . . . . . . 8
⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈
ℝ) | 
| 49 | 41, 48 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ ℝ) | 
| 50 | 49 | recnd 11290 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ ℂ) | 
| 51 | 47, 50, 42 | subdid 11720 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · ((𝑘 + 1) − 𝑘)) = ((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘))) | 
| 52 | 47 | mulridd 11279 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · 1) = 𝑋) | 
| 53 | 46, 51, 52 | 3eqtr3d 2784 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘)) = 𝑋) | 
| 54 |  | eqid 2736 | . . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 55 | 54 | mulcn 24890 | . . . . . 6
⊢  ·
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) | 
| 56 | 6 | zred 12724 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 57 | 56 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ) | 
| 58 | 8 | zred 12724 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 59 | 58 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈ ℝ) | 
| 60 |  | elfzole1 13708 | . . . . . . . . . . 11
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝑘) | 
| 61 | 60 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ≤ 𝑘) | 
| 62 | 28 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁)) | 
| 63 |  | elfzle2 13569 | . . . . . . . . . . 11
⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → (𝑘 + 1) ≤ 𝑁) | 
| 64 | 62, 63 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ≤ 𝑁) | 
| 65 |  | iccss 13456 | . . . . . . . . . 10
⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ (𝑀 ≤ 𝑘 ∧ (𝑘 + 1) ≤ 𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁)) | 
| 66 | 57, 59, 61, 64, 65 | syl22anc 838 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁)) | 
| 67 |  | iccssre 13470 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀[,]𝑁) ⊆ ℝ) | 
| 68 | 56, 58, 67 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ) | 
| 69 | 68 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀[,]𝑁) ⊆ ℝ) | 
| 70 | 66, 69 | sstrd 3993 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ ℝ) | 
| 71 |  | ax-resscn 11213 | . . . . . . . 8
⊢ ℝ
⊆ ℂ | 
| 72 | 70, 71 | sstrdi 3995 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ ℂ) | 
| 73 | 71 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ℝ ⊆
ℂ) | 
| 74 |  | cncfmptc 24939 | . . . . . . 7
⊢ ((𝑋 ∈ ℝ ∧ (𝑘[,](𝑘 + 1)) ⊆ ℂ ∧ ℝ ⊆
ℂ) → (𝑦 ∈
(𝑘[,](𝑘 + 1)) ↦ 𝑋) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ)) | 
| 75 | 3, 72, 73, 74 | syl3anc 1372 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝑋) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ)) | 
| 76 |  | cncfmptid 24940 | . . . . . . 7
⊢ (((𝑘[,](𝑘 + 1)) ⊆ ℝ ∧ ℝ ⊆
ℂ) → (𝑦 ∈
(𝑘[,](𝑘 + 1)) ↦ 𝑦) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ)) | 
| 77 | 70, 71, 76 | sylancl 586 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝑦) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ)) | 
| 78 |  | remulcl 11241 | . . . . . 6
⊢ ((𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑋 · 𝑦) ∈ ℝ) | 
| 79 | 54, 55, 75, 77, 71, 78 | cncfmpt2ss 24943 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ (𝑋 · 𝑦)) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ)) | 
| 80 |  | reelprrecn 11248 | . . . . . . . 8
⊢ ℝ
∈ {ℝ, ℂ} | 
| 81 | 80 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ℝ ∈ {ℝ,
ℂ}) | 
| 82 | 57 | rexrd 11312 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈
ℝ*) | 
| 83 |  | iooss1 13423 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℝ*
∧ 𝑀 ≤ 𝑘) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1))) | 
| 84 | 82, 61, 83 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1))) | 
| 85 | 59 | rexrd 11312 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈
ℝ*) | 
| 86 |  | iooss2 13424 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ*
∧ (𝑘 + 1) ≤ 𝑁) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) | 
| 87 | 85, 64, 86 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) | 
| 88 | 84, 87 | sstrd 3993 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) | 
| 89 |  | ioossicc 13474 | . . . . . . . . . 10
⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) | 
| 90 | 69, 71 | sstrdi 3995 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀[,]𝑁) ⊆ ℂ) | 
| 91 | 89, 90 | sstrid 3994 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)𝑁) ⊆ ℂ) | 
| 92 | 88, 91 | sstrd 3993 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ ℂ) | 
| 93 | 92 | sselda 3982 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘(,)(𝑘 + 1))) → 𝑦 ∈ ℂ) | 
| 94 |  | 1cnd 11257 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘(,)(𝑘 + 1))) → 1 ∈
ℂ) | 
| 95 | 73 | sselda 3982 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ) | 
| 96 |  | 1cnd 11257 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ ℝ) → 1 ∈
ℂ) | 
| 97 | 81 | dvmptid 25996 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1)) | 
| 98 |  | ioossre 13449 | . . . . . . . . 9
⊢ (𝑘(,)(𝑘 + 1)) ⊆ ℝ | 
| 99 | 98 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ ℝ) | 
| 100 | 54 | tgioo2 24825 | . . . . . . . 8
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) | 
| 101 |  | iooretop 24787 | . . . . . . . . 9
⊢ (𝑘(,)(𝑘 + 1)) ∈ (topGen‘ran
(,)) | 
| 102 | 101 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ∈ (topGen‘ran
(,))) | 
| 103 | 81, 95, 96, 97, 99, 100, 54, 102 | dvmptres 26002 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ 𝑦)) = (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ 1)) | 
| 104 | 81, 93, 94, 103, 47 | dvmptcmul 26003 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 · 𝑦))) = (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 · 1))) | 
| 105 | 52 | mpteq2dv 5243 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 · 1)) = (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ 𝑋)) | 
| 106 | 104, 105 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 · 𝑦))) = (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ 𝑋)) | 
| 107 |  | nfcv 2904 | . . . . . . 7
⊢
Ⅎ𝑦𝐴 | 
| 108 | 107, 20, 22 | cbvmpt 5252 | . . . . . 6
⊢ (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝐴) = (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ ⦋𝑦 / 𝑥⦌𝐴) | 
| 109 | 66 | resmptd 6057 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ↾ (𝑘[,](𝑘 + 1))) = (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝐴)) | 
| 110 | 14 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ)) | 
| 111 |  | rescncf 24924 | . . . . . . . 8
⊢ ((𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ↾ (𝑘[,](𝑘 + 1))) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))) | 
| 112 | 66, 110, 111 | sylc 65 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ↾ (𝑘[,](𝑘 + 1))) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ)) | 
| 113 | 109, 112 | eqeltrrd 2841 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝐴) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ)) | 
| 114 | 108, 113 | eqeltrrid 2845 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ ⦋𝑦 / 𝑥⦌𝐴) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ)) | 
| 115 | 16 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) | 
| 116 | 115, 18 | sylibr 234 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ) | 
| 117 | 89 | sseli 3978 | . . . . . . . 8
⊢ (𝑦 ∈ (𝑀(,)𝑁) → 𝑦 ∈ (𝑀[,]𝑁)) | 
| 118 | 24 | impcom 407 | . . . . . . . 8
⊢
((∀𝑥 ∈
(𝑀[,]𝑁)𝐴 ∈ ℝ ∧ 𝑦 ∈ (𝑀[,]𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ) | 
| 119 | 116, 117,
118 | syl2an 596 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑀(,)𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ) | 
| 120 | 119 | recnd 11290 | . . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑀(,)𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ) | 
| 121 | 89 | sseli 3978 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝑀(,)𝑁) → 𝑥 ∈ (𝑀[,]𝑁)) | 
| 122 | 16 | fvmptelcdm 7132 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℝ) | 
| 123 | 122 | adantlr 715 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℝ) | 
| 124 | 121, 123 | sylan2 593 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℝ) | 
| 125 | 124 | fmpttd 7134 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)⟶ℝ) | 
| 126 |  | ioossre 13449 | . . . . . . . . . 10
⊢ (𝑀(,)𝑁) ⊆ ℝ | 
| 127 |  | dvfre 25990 | . . . . . . . . . 10
⊢ (((𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)⟶ℝ ∧ (𝑀(,)𝑁) ⊆ ℝ) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ) | 
| 128 | 125, 126,
127 | sylancl 586 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ) | 
| 129 |  | dvfsumleOLD.b | . . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) | 
| 130 | 129 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) | 
| 131 | 130 | dmeqd 5915 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) | 
| 132 |  | dvfsumleOLD.v | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉) | 
| 133 | 132 | adantlr 715 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉) | 
| 134 | 133 | ralrimiva 3145 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ 𝑉) | 
| 135 |  | dmmptg 6261 | . . . . . . . . . . . 12
⊢
(∀𝑥 ∈
(𝑀(,)𝑁)𝐵 ∈ 𝑉 → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑀(,)𝑁)) | 
| 136 | 134, 135 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑀(,)𝑁)) | 
| 137 | 131, 136 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑀(,)𝑁)) | 
| 138 | 130, 137 | feq12d 6723 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ)) | 
| 139 | 128, 138 | mpbid 232 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ) | 
| 140 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) | 
| 141 | 140 | fmpt 7129 | . . . . . . . 8
⊢
(∀𝑥 ∈
(𝑀(,)𝑁)𝐵 ∈ ℝ ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ) | 
| 142 | 139, 141 | sylibr 234 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ ℝ) | 
| 143 |  | nfcsb1v 3922 | . . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 | 
| 144 | 143 | nfel1 2921 | . . . . . . . 8
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ | 
| 145 |  | csbeq1a 3912 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) | 
| 146 | 145 | eleq1d 2825 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐵 ∈ ℝ ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ)) | 
| 147 | 144, 146 | rspc 3609 | . . . . . . 7
⊢ (𝑦 ∈ (𝑀(,)𝑁) → (∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ ℝ → ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ)) | 
| 148 | 142, 147 | mpan9 506 | . . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑀(,)𝑁)) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ) | 
| 149 | 107, 20, 22 | cbvmpt 5252 | . . . . . . . 8
⊢ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴) = (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / 𝑥⦌𝐴) | 
| 150 | 149 | oveq2i 7443 | . . . . . . 7
⊢ (ℝ
D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (ℝ D (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / 𝑥⦌𝐴)) | 
| 151 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑦𝐵 | 
| 152 | 151, 143,
145 | cbvmpt 5252 | . . . . . . 7
⊢ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / 𝑥⦌𝐵) | 
| 153 | 130, 150,
152 | 3eqtr3g 2799 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / 𝑥⦌𝐴)) = (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / 𝑥⦌𝐵)) | 
| 154 | 81, 120, 148, 153, 88, 100, 54, 102 | dvmptres 26002 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ ⦋𝑦 / 𝑥⦌𝐴)) = (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ ⦋𝑦 / 𝑥⦌𝐵)) | 
| 155 |  | dvfsumleOLD.l | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → 𝑋 ≤ 𝐵) | 
| 156 | 155 | anassrs 467 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → 𝑋 ≤ 𝐵) | 
| 157 | 156 | ralrimiva 3145 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑘(,)(𝑘 + 1))𝑋 ≤ 𝐵) | 
| 158 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑥𝑋 | 
| 159 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑥
≤ | 
| 160 | 158, 159,
143 | nfbr 5189 | . . . . . . 7
⊢
Ⅎ𝑥 𝑋 ≤ ⦋𝑦 / 𝑥⦌𝐵 | 
| 161 | 145 | breq2d 5154 | . . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑋 ≤ 𝐵 ↔ 𝑋 ≤ ⦋𝑦 / 𝑥⦌𝐵)) | 
| 162 | 160, 161 | rspc 3609 | . . . . . 6
⊢ (𝑦 ∈ (𝑘(,)(𝑘 + 1)) → (∀𝑥 ∈ (𝑘(,)(𝑘 + 1))𝑋 ≤ 𝐵 → 𝑋 ≤ ⦋𝑦 / 𝑥⦌𝐵)) | 
| 163 | 157, 162 | mpan9 506 | . . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘(,)(𝑘 + 1))) → 𝑋 ≤ ⦋𝑦 / 𝑥⦌𝐵) | 
| 164 | 41 | rexrd 11312 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℝ*) | 
| 165 | 49 | rexrd 11312 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈
ℝ*) | 
| 166 | 41 | lep1d 12200 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ≤ (𝑘 + 1)) | 
| 167 |  | lbicc2 13505 | . . . . . 6
⊢ ((𝑘 ∈ ℝ*
∧ (𝑘 + 1) ∈
ℝ* ∧ 𝑘
≤ (𝑘 + 1)) → 𝑘 ∈ (𝑘[,](𝑘 + 1))) | 
| 168 | 164, 165,
166, 167 | syl3anc 1372 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ (𝑘[,](𝑘 + 1))) | 
| 169 |  | ubicc2 13506 | . . . . . 6
⊢ ((𝑘 ∈ ℝ*
∧ (𝑘 + 1) ∈
ℝ* ∧ 𝑘
≤ (𝑘 + 1)) → (𝑘 + 1) ∈ (𝑘[,](𝑘 + 1))) | 
| 170 | 164, 165,
166, 169 | syl3anc 1372 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑘[,](𝑘 + 1))) | 
| 171 |  | oveq2 7440 | . . . . 5
⊢ (𝑦 = 𝑘 → (𝑋 · 𝑦) = (𝑋 · 𝑘)) | 
| 172 |  | oveq2 7440 | . . . . 5
⊢ (𝑦 = (𝑘 + 1) → (𝑋 · 𝑦) = (𝑋 · (𝑘 + 1))) | 
| 173 | 41, 49, 79, 106, 114, 154, 163, 168, 170, 166, 171, 34, 172, 29 | dvle 26047 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘)) ≤ (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) | 
| 174 | 53, 173 | eqbrtrrd 5166 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ≤ (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) | 
| 175 | 2, 3, 38, 174 | fsumle 15836 | . 2
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ Σ𝑘 ∈ (𝑀..^𝑁)(⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴)) | 
| 176 |  | vex 3483 | . . . . 5
⊢ 𝑦 ∈ V | 
| 177 | 176 | a1i 11 | . . . 4
⊢ (𝑦 = 𝑀 → 𝑦 ∈ V) | 
| 178 |  | eqeq2 2748 | . . . . . 6
⊢ (𝑦 = 𝑀 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑀)) | 
| 179 | 178 | biimpa 476 | . . . . 5
⊢ ((𝑦 = 𝑀 ∧ 𝑥 = 𝑦) → 𝑥 = 𝑀) | 
| 180 |  | dvfsumleOLD.c | . . . . 5
⊢ (𝑥 = 𝑀 → 𝐴 = 𝐶) | 
| 181 | 179, 180 | syl 17 | . . . 4
⊢ ((𝑦 = 𝑀 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐶) | 
| 182 | 177, 181 | csbied 3934 | . . 3
⊢ (𝑦 = 𝑀 → ⦋𝑦 / 𝑥⦌𝐴 = 𝐶) | 
| 183 | 176 | a1i 11 | . . . 4
⊢ (𝑦 = 𝑁 → 𝑦 ∈ V) | 
| 184 |  | eqeq2 2748 | . . . . . 6
⊢ (𝑦 = 𝑁 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑁)) | 
| 185 | 184 | biimpa 476 | . . . . 5
⊢ ((𝑦 = 𝑁 ∧ 𝑥 = 𝑦) → 𝑥 = 𝑁) | 
| 186 |  | dvfsumleOLD.d | . . . . 5
⊢ (𝑥 = 𝑁 → 𝐴 = 𝐷) | 
| 187 | 185, 186 | syl 17 | . . . 4
⊢ ((𝑦 = 𝑁 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐷) | 
| 188 | 183, 187 | csbied 3934 | . . 3
⊢ (𝑦 = 𝑁 → ⦋𝑦 / 𝑥⦌𝐴 = 𝐷) | 
| 189 | 26 | recnd 11290 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀...𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ) | 
| 190 | 34, 29, 182, 188, 4, 189 | telfsumo2 15840 | . 2
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴) = (𝐷 − 𝐶)) | 
| 191 | 175, 190 | breqtrd 5168 | 1
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ (𝐷 − 𝐶)) |