Proof of Theorem dvfsumge
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dvfsumleOLD.m | . . . 4
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) | 
| 2 |  | df-neg 11496 | . . . . . 6
⊢ -𝐴 = (0 − 𝐴) | 
| 3 | 2 | mpteq2i 5246 | . . . . 5
⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ -𝐴) = (𝑥 ∈ (𝑀[,]𝑁) ↦ (0 − 𝐴)) | 
| 4 |  | eqid 2736 | . . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 5 | 4 | subcn 24889 | . . . . . 6
⊢  −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) | 
| 6 |  | 0red 11265 | . . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ) | 
| 7 |  | eluzel2 12884 | . . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | 
| 8 | 1, 7 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 9 | 8 | zred 12724 | . . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 10 |  | eluzelz 12889 | . . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) | 
| 11 | 1, 10 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 12 | 11 | zred 12724 | . . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 13 |  | iccssre 13470 | . . . . . . . . 9
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀[,]𝑁) ⊆ ℝ) | 
| 14 | 9, 12, 13 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ) | 
| 15 |  | ax-resscn 11213 | . . . . . . . 8
⊢ ℝ
⊆ ℂ | 
| 16 | 14, 15 | sstrdi 3995 | . . . . . . 7
⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℂ) | 
| 17 | 15 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ℝ ⊆
ℂ) | 
| 18 |  | cncfmptc 24939 | . . . . . . 7
⊢ ((0
∈ ℝ ∧ (𝑀[,]𝑁) ⊆ ℂ ∧ ℝ ⊆
ℂ) → (𝑥 ∈
(𝑀[,]𝑁) ↦ 0) ∈ ((𝑀[,]𝑁)–cn→ℝ)) | 
| 19 | 6, 16, 17, 18 | syl3anc 1372 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 0) ∈ ((𝑀[,]𝑁)–cn→ℝ)) | 
| 20 |  | dvfsumleOLD.a | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ)) | 
| 21 |  | resubcl 11574 | . . . . . 6
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 − 𝐴) ∈ ℝ) | 
| 22 | 4, 5, 19, 20, 15, 21 | cncfmpt2ss 24943 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ (0 − 𝐴)) ∈ ((𝑀[,]𝑁)–cn→ℝ)) | 
| 23 | 3, 22 | eqeltrid 2844 | . . . 4
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ -𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ)) | 
| 24 |  | negex 11507 | . . . . 5
⊢ -𝐵 ∈ V | 
| 25 | 24 | a1i 11 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → -𝐵 ∈ V) | 
| 26 |  | reelprrecn 11248 | . . . . . 6
⊢ ℝ
∈ {ℝ, ℂ} | 
| 27 | 26 | a1i 11 | . . . . 5
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) | 
| 28 |  | ioossicc 13474 | . . . . . . . 8
⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁) | 
| 29 | 28 | sseli 3978 | . . . . . . 7
⊢ (𝑥 ∈ (𝑀(,)𝑁) → 𝑥 ∈ (𝑀[,]𝑁)) | 
| 30 |  | cncff 24920 | . . . . . . . . 9
⊢ ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) | 
| 31 | 20, 30 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) | 
| 32 | 31 | fvmptelcdm 7132 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℝ) | 
| 33 | 29, 32 | sylan2 593 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℝ) | 
| 34 | 33 | recnd 11290 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℂ) | 
| 35 |  | dvfsumleOLD.v | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉) | 
| 36 |  | dvfsumleOLD.b | . . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) | 
| 37 | 27, 34, 35, 36 | dvmptneg 26005 | . . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ -𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ -𝐵)) | 
| 38 |  | dvfsumleOLD.c | . . . . 5
⊢ (𝑥 = 𝑀 → 𝐴 = 𝐶) | 
| 39 | 38 | negeqd 11503 | . . . 4
⊢ (𝑥 = 𝑀 → -𝐴 = -𝐶) | 
| 40 |  | dvfsumleOLD.d | . . . . 5
⊢ (𝑥 = 𝑁 → 𝐴 = 𝐷) | 
| 41 | 40 | negeqd 11503 | . . . 4
⊢ (𝑥 = 𝑁 → -𝐴 = -𝐷) | 
| 42 |  | dvfsumleOLD.x | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℝ) | 
| 43 | 42 | renegcld 11691 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → -𝑋 ∈ ℝ) | 
| 44 |  | dvfsumge.l | . . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → 𝐵 ≤ 𝑋) | 
| 45 | 9 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ) | 
| 46 | 45 | rexrd 11312 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈
ℝ*) | 
| 47 |  | elfzole1 13708 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝑘) | 
| 48 | 47 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ≤ 𝑘) | 
| 49 |  | iooss1 13423 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℝ*
∧ 𝑀 ≤ 𝑘) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1))) | 
| 50 | 46, 48, 49 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1))) | 
| 51 | 12 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈ ℝ) | 
| 52 | 51 | rexrd 11312 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈
ℝ*) | 
| 53 |  | fzofzp1 13804 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝑀..^𝑁) → (𝑘 + 1) ∈ (𝑀...𝑁)) | 
| 54 | 53 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁)) | 
| 55 |  | elfzle2 13569 | . . . . . . . . . . . 12
⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → (𝑘 + 1) ≤ 𝑁) | 
| 56 | 54, 55 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ≤ 𝑁) | 
| 57 |  | iooss2 13424 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ*
∧ (𝑘 + 1) ≤ 𝑁) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) | 
| 58 | 52, 56, 57 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) | 
| 59 | 50, 58 | sstrd 3993 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁)) | 
| 60 | 59 | sselda 3982 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → 𝑥 ∈ (𝑀(,)𝑁)) | 
| 61 | 32 | adantlr 715 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℝ) | 
| 62 | 29, 61 | sylan2 593 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℝ) | 
| 63 | 62 | fmpttd 7134 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)⟶ℝ) | 
| 64 |  | ioossre 13449 | . . . . . . . . . . 11
⊢ (𝑀(,)𝑁) ⊆ ℝ | 
| 65 |  | dvfre 25990 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)⟶ℝ ∧ (𝑀(,)𝑁) ⊆ ℝ) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ) | 
| 66 | 63, 64, 65 | sylancl 586 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ) | 
| 67 | 36 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) | 
| 68 | 67 | dmeqd 5915 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)) | 
| 69 | 35 | adantlr 715 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉) | 
| 70 | 69 | ralrimiva 3145 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ 𝑉) | 
| 71 |  | dmmptg 6261 | . . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
(𝑀(,)𝑁)𝐵 ∈ 𝑉 → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑀(,)𝑁)) | 
| 72 | 70, 71 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑀(,)𝑁)) | 
| 73 | 68, 72 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑀(,)𝑁)) | 
| 74 | 67, 73 | feq12d 6723 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ)) | 
| 75 | 66, 74 | mpbid 232 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ) | 
| 76 | 75 | fvmptelcdm 7132 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ ℝ) | 
| 77 | 60, 76 | syldan 591 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → 𝐵 ∈ ℝ) | 
| 78 | 77 | anasss 466 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → 𝐵 ∈ ℝ) | 
| 79 | 42 | adantrr 717 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → 𝑋 ∈ ℝ) | 
| 80 | 78, 79 | lenegd 11843 | . . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → (𝐵 ≤ 𝑋 ↔ -𝑋 ≤ -𝐵)) | 
| 81 | 44, 80 | mpbid 232 | . . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → -𝑋 ≤ -𝐵) | 
| 82 | 1, 23, 25, 37, 39, 41, 43, 81 | dvfsumle 26061 | . . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)-𝑋 ≤ (-𝐷 − -𝐶)) | 
| 83 |  | fzofi 14016 | . . . . 5
⊢ (𝑀..^𝑁) ∈ Fin | 
| 84 | 83 | a1i 11 | . . . 4
⊢ (𝜑 → (𝑀..^𝑁) ∈ Fin) | 
| 85 | 42 | recnd 11290 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℂ) | 
| 86 | 84, 85 | fsumneg 15824 | . . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)-𝑋 = -Σ𝑘 ∈ (𝑀..^𝑁)𝑋) | 
| 87 | 40 | eleq1d 2825 | . . . . . . 7
⊢ (𝑥 = 𝑁 → (𝐴 ∈ ℝ ↔ 𝐷 ∈ ℝ)) | 
| 88 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) = (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) | 
| 89 | 88 | fmpt 7129 | . . . . . . . 8
⊢
(∀𝑥 ∈
(𝑀[,]𝑁)𝐴 ∈ ℝ ↔ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ) | 
| 90 | 31, 89 | sylibr 234 | . . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ) | 
| 91 | 9 | rexrd 11312 | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈
ℝ*) | 
| 92 | 12 | rexrd 11312 | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
ℝ*) | 
| 93 |  | eluzle 12892 | . . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) | 
| 94 | 1, 93 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑀 ≤ 𝑁) | 
| 95 |  | ubicc2 13506 | . . . . . . . 8
⊢ ((𝑀 ∈ ℝ*
∧ 𝑁 ∈
ℝ* ∧ 𝑀
≤ 𝑁) → 𝑁 ∈ (𝑀[,]𝑁)) | 
| 96 | 91, 92, 94, 95 | syl3anc 1372 | . . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (𝑀[,]𝑁)) | 
| 97 | 87, 90, 96 | rspcdva 3622 | . . . . . 6
⊢ (𝜑 → 𝐷 ∈ ℝ) | 
| 98 | 97 | recnd 11290 | . . . . 5
⊢ (𝜑 → 𝐷 ∈ ℂ) | 
| 99 | 38 | eleq1d 2825 | . . . . . . 7
⊢ (𝑥 = 𝑀 → (𝐴 ∈ ℝ ↔ 𝐶 ∈ ℝ)) | 
| 100 |  | lbicc2 13505 | . . . . . . . 8
⊢ ((𝑀 ∈ ℝ*
∧ 𝑁 ∈
ℝ* ∧ 𝑀
≤ 𝑁) → 𝑀 ∈ (𝑀[,]𝑁)) | 
| 101 | 91, 92, 94, 100 | syl3anc 1372 | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (𝑀[,]𝑁)) | 
| 102 | 99, 90, 101 | rspcdva 3622 | . . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 103 | 102 | recnd 11290 | . . . . 5
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 104 | 98, 103 | neg2subd 11638 | . . . 4
⊢ (𝜑 → (-𝐷 − -𝐶) = (𝐶 − 𝐷)) | 
| 105 | 98, 103 | negsubdi2d 11637 | . . . 4
⊢ (𝜑 → -(𝐷 − 𝐶) = (𝐶 − 𝐷)) | 
| 106 | 104, 105 | eqtr4d 2779 | . . 3
⊢ (𝜑 → (-𝐷 − -𝐶) = -(𝐷 − 𝐶)) | 
| 107 | 82, 86, 106 | 3brtr3d 5173 | . 2
⊢ (𝜑 → -Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ -(𝐷 − 𝐶)) | 
| 108 | 97, 102 | resubcld 11692 | . . 3
⊢ (𝜑 → (𝐷 − 𝐶) ∈ ℝ) | 
| 109 | 84, 42 | fsumrecl 15771 | . . 3
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ∈ ℝ) | 
| 110 | 108, 109 | lenegd 11843 | . 2
⊢ (𝜑 → ((𝐷 − 𝐶) ≤ Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ↔ -Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ -(𝐷 − 𝐶))) | 
| 111 | 107, 110 | mpbird 257 | 1
⊢ (𝜑 → (𝐷 − 𝐶) ≤ Σ𝑘 ∈ (𝑀..^𝑁)𝑋) |