This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvfsumge

Description: Compare a finite sum to an integral (the integral here is given as a function with a known derivative). (Contributed by Mario Carneiro, 14-May-2016)

Ref Expression
Hypotheses dvfsumleOLD.m ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
dvfsumleOLD.a ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) )
dvfsumleOLD.v ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐵 ∈ 𝑉 )
dvfsumleOLD.b ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) )
dvfsumleOLD.c ⊢ ( 𝑥 = 𝑀 → 𝐴 = 𝐶 )
dvfsumleOLD.d ⊢ ( 𝑥 = 𝑁 → 𝐴 = 𝐷 )
dvfsumleOLD.x ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑋 ∈ ℝ )
dvfsumge.l ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) ) → 𝐵 ≤ 𝑋 )
Assertion dvfsumge ( 𝜑 → ( 𝐷 − 𝐶 ) ≤ Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 )

Proof

Step Hyp Ref Expression
1 dvfsumleOLD.m ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 dvfsumleOLD.a ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) )
3 dvfsumleOLD.v ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐵 ∈ 𝑉 )
4 dvfsumleOLD.b ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) )
5 dvfsumleOLD.c ⊢ ( 𝑥 = 𝑀 → 𝐴 = 𝐶 )
6 dvfsumleOLD.d ⊢ ( 𝑥 = 𝑁 → 𝐴 = 𝐷 )
7 dvfsumleOLD.x ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑋 ∈ ℝ )
8 dvfsumge.l ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) ) → 𝐵 ≤ 𝑋 )
9 df-neg ⊢ - 𝐴 = ( 0 − 𝐴 )
10 9 mpteq2i ⊢ ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ - 𝐴 ) = ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( 0 − 𝐴 ) )
11 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
12 11 subcn ⊢ − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
13 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
14 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
15 1 14 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
16 15 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
17 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
18 1 17 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
19 18 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
20 iccssre ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 [,] 𝑁 ) ⊆ ℝ )
21 16 19 20 syl2anc ⊢ ( 𝜑 → ( 𝑀 [,] 𝑁 ) ⊆ ℝ )
22 ax-resscn ⊢ ℝ ⊆ ℂ
23 21 22 sstrdi ⊢ ( 𝜑 → ( 𝑀 [,] 𝑁 ) ⊆ ℂ )
24 22 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
25 cncfmptc ⊢ ( ( 0 ∈ ℝ ∧ ( 𝑀 [,] 𝑁 ) ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 0 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) )
26 13 23 24 25 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 0 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) )
27 resubcl ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 − 𝐴 ) ∈ ℝ )
28 11 12 26 2 22 27 cncfmpt2ss ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( 0 − 𝐴 ) ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) )
29 10 28 eqeltrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ - 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) )
30 negex ⊢ - 𝐵 ∈ V
31 30 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → - 𝐵 ∈ V )
32 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
33 32 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
34 ioossicc ⊢ ( 𝑀 (,) 𝑁 ) ⊆ ( 𝑀 [,] 𝑁 )
35 34 sseli ⊢ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) → 𝑥 ∈ ( 𝑀 [,] 𝑁 ) )
36 cncff ⊢ ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) : ( 𝑀 [,] 𝑁 ) ⟶ ℝ )
37 2 36 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) : ( 𝑀 [,] 𝑁 ) ⟶ ℝ )
38 37 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝐴 ∈ ℝ )
39 35 38 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐴 ∈ ℝ )
40 39 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐴 ∈ ℂ )
41 33 40 3 4 dvmptneg ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ - 𝐴 ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ - 𝐵 ) )
42 5 negeqd ⊢ ( 𝑥 = 𝑀 → - 𝐴 = - 𝐶 )
43 6 negeqd ⊢ ( 𝑥 = 𝑁 → - 𝐴 = - 𝐷 )
44 7 renegcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → - 𝑋 ∈ ℝ )
45 16 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ℝ )
46 45 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ℝ* )
47 elfzole1 ⊢ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ≤ 𝑘 )
48 47 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ≤ 𝑘 )
49 iooss1 ⊢ ( ( 𝑀 ∈ ℝ* ∧ 𝑀 ≤ 𝑘 ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) ( 𝑘 + 1 ) ) )
50 46 48 49 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) ( 𝑘 + 1 ) ) )
51 19 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑁 ∈ ℝ )
52 51 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑁 ∈ ℝ* )
53 fzofzp1 ⊢ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
54 53 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
55 elfzle2 ⊢ ( ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝑘 + 1 ) ≤ 𝑁 )
56 54 55 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ≤ 𝑁 )
57 iooss2 ⊢ ( ( 𝑁 ∈ ℝ* ∧ ( 𝑘 + 1 ) ≤ 𝑁 ) → ( 𝑀 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) 𝑁 ) )
58 52 56 57 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) 𝑁 ) )
59 50 58 sstrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) 𝑁 ) )
60 59 sselda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → 𝑥 ∈ ( 𝑀 (,) 𝑁 ) )
61 38 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝐴 ∈ ℝ )
62 35 61 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐴 ∈ ℝ )
63 62 fmpttd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ )
64 ioossre ⊢ ( 𝑀 (,) 𝑁 ) ⊆ ℝ
65 dvfre ⊢ ( ( ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ ∧ ( 𝑀 (,) 𝑁 ) ⊆ ℝ ) → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) : dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) ⟶ ℝ )
66 63 64 65 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) : dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) ⟶ ℝ )
67 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) )
68 67 dmeqd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = dom ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) )
69 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐵 ∈ 𝑉 )
70 69 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∀ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) 𝐵 ∈ 𝑉 )
71 dmmptg ⊢ ( ∀ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) = ( 𝑀 (,) 𝑁 ) )
72 70 71 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → dom ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) = ( 𝑀 (,) 𝑁 ) )
73 68 72 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( 𝑀 (,) 𝑁 ) )
74 67 73 feq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) : dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) ⟶ ℝ ↔ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ ) )
75 66 74 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ )
76 75 fvmptelcdm ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐵 ∈ ℝ )
77 60 76 syldan ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → 𝐵 ∈ ℝ )
78 77 anasss ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) ) → 𝐵 ∈ ℝ )
79 7 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) ) → 𝑋 ∈ ℝ )
80 78 79 lenegd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) ) → ( 𝐵 ≤ 𝑋 ↔ - 𝑋 ≤ - 𝐵 ) )
81 8 80 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) ) → - 𝑋 ≤ - 𝐵 )
82 1 29 31 41 42 43 44 81 dvfsumle ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) - 𝑋 ≤ ( - 𝐷 − - 𝐶 ) )
83 fzofi ⊢ ( 𝑀 ..^ 𝑁 ) ∈ Fin
84 83 a1i ⊢ ( 𝜑 → ( 𝑀 ..^ 𝑁 ) ∈ Fin )
85 7 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑋 ∈ ℂ )
86 84 85 fsumneg ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) - 𝑋 = - Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 )
87 6 eleq1d ⊢ ( 𝑥 = 𝑁 → ( 𝐴 ∈ ℝ ↔ 𝐷 ∈ ℝ ) )
88 eqid ⊢ ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) = ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 )
89 88 fmpt ⊢ ( ∀ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) 𝐴 ∈ ℝ ↔ ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) : ( 𝑀 [,] 𝑁 ) ⟶ ℝ )
90 37 89 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) 𝐴 ∈ ℝ )
91 16 rexrd ⊢ ( 𝜑 → 𝑀 ∈ ℝ* )
92 19 rexrd ⊢ ( 𝜑 → 𝑁 ∈ ℝ* )
93 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑁 )
94 1 93 syl ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
95 ubicc2 ⊢ ( ( 𝑀 ∈ ℝ* ∧ 𝑁 ∈ ℝ* ∧ 𝑀 ≤ 𝑁 ) → 𝑁 ∈ ( 𝑀 [,] 𝑁 ) )
96 91 92 94 95 syl3anc ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 [,] 𝑁 ) )
97 87 90 96 rspcdva ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
98 97 recnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
99 5 eleq1d ⊢ ( 𝑥 = 𝑀 → ( 𝐴 ∈ ℝ ↔ 𝐶 ∈ ℝ ) )
100 lbicc2 ⊢ ( ( 𝑀 ∈ ℝ* ∧ 𝑁 ∈ ℝ* ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ∈ ( 𝑀 [,] 𝑁 ) )
101 91 92 94 100 syl3anc ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 [,] 𝑁 ) )
102 99 90 101 rspcdva ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
103 102 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
104 98 103 neg2subd ⊢ ( 𝜑 → ( - 𝐷 − - 𝐶 ) = ( 𝐶 − 𝐷 ) )
105 98 103 negsubdi2d ⊢ ( 𝜑 → - ( 𝐷 − 𝐶 ) = ( 𝐶 − 𝐷 ) )
106 104 105 eqtr4d ⊢ ( 𝜑 → ( - 𝐷 − - 𝐶 ) = - ( 𝐷 − 𝐶 ) )
107 82 86 106 3brtr3d ⊢ ( 𝜑 → - Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 ≤ - ( 𝐷 − 𝐶 ) )
108 97 102 resubcld ⊢ ( 𝜑 → ( 𝐷 − 𝐶 ) ∈ ℝ )
109 84 7 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 ∈ ℝ )
110 108 109 lenegd ⊢ ( 𝜑 → ( ( 𝐷 − 𝐶 ) ≤ Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 ↔ - Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 ≤ - ( 𝐷 − 𝐶 ) ) )
111 107 110 mpbird ⊢ ( 𝜑 → ( 𝐷 − 𝐶 ) ≤ Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 )