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

Metamath Proof Explorer

Theorem dvfsumabs

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 dvfsumabs.m ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
dvfsumabs.a ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) )
dvfsumabs.v ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐵 ∈ 𝑉 )
dvfsumabs.b ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) )
dvfsumabs.c ⊢ ( 𝑥 = 𝑀 → 𝐴 = 𝐶 )
dvfsumabs.d ⊢ ( 𝑥 = 𝑁 → 𝐴 = 𝐷 )
dvfsumabs.x ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑋 ∈ ℂ )
dvfsumabs.y ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑌 ∈ ℝ )
dvfsumabs.l ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) ) → ( abs ‘ ( 𝑋 − 𝐵 ) ) ≤ 𝑌 )
Assertion dvfsumabs ( 𝜑 → ( abs ‘ ( Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 − ( 𝐷 − 𝐶 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑌 )

Proof

Step Hyp Ref Expression
1 dvfsumabs.m ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 dvfsumabs.a ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) )
3 dvfsumabs.v ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐵 ∈ 𝑉 )
4 dvfsumabs.b ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) )
5 dvfsumabs.c ⊢ ( 𝑥 = 𝑀 → 𝐴 = 𝐶 )
6 dvfsumabs.d ⊢ ( 𝑥 = 𝑁 → 𝐴 = 𝐷 )
7 dvfsumabs.x ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑋 ∈ ℂ )
8 dvfsumabs.y ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑌 ∈ ℝ )
9 dvfsumabs.l ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) ) → ( abs ‘ ( 𝑋 − 𝐵 ) ) ≤ 𝑌 )
10 fzofi ⊢ ( 𝑀 ..^ 𝑁 ) ∈ Fin
11 10 a1i ⊢ ( 𝜑 → ( 𝑀 ..^ 𝑁 ) ∈ Fin )
12 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
13 1 12 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
14 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
15 1 14 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
16 fzval2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 [,] 𝑁 ) ∩ ℤ ) )
17 13 15 16 syl2anc ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 [,] 𝑁 ) ∩ ℤ ) )
18 inss1 ⊢ ( ( 𝑀 [,] 𝑁 ) ∩ ℤ ) ⊆ ( 𝑀 [,] 𝑁 )
19 17 18 eqsstrdi ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ⊆ ( 𝑀 [,] 𝑁 ) )
20 19 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑦 ∈ ( 𝑀 [,] 𝑁 ) )
21 cncff ⊢ ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) : ( 𝑀 [,] 𝑁 ) ⟶ ℂ )
22 2 21 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) : ( 𝑀 [,] 𝑁 ) ⟶ ℂ )
23 eqid ⊢ ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) = ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 )
24 23 fmpt ⊢ ( ∀ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) 𝐴 ∈ ℂ ↔ ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) : ( 𝑀 [,] 𝑁 ) ⟶ ℂ )
25 22 24 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) 𝐴 ∈ ℂ )
26 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐴
27 26 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ
28 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
29 28 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ ℂ ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ ) )
30 27 29 rspc ⊢ ( 𝑦 ∈ ( 𝑀 [,] 𝑁 ) → ( ∀ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) 𝐴 ∈ ℂ → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ ) )
31 25 30 mpan9 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑀 [,] 𝑁 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ )
32 20 31 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ )
33 32 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ )
34 fzofzp1 ⊢ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
35 csbeq1 ⊢ ( 𝑦 = ( 𝑘 + 1 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 )
36 35 eleq1d ⊢ ( 𝑦 = ( 𝑘 + 1 ) → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ ↔ ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 ∈ ℂ ) )
37 36 rspccva ⊢ ( ( ∀ 𝑦 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ ∧ ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 ∈ ℂ )
38 33 34 37 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 ∈ ℂ )
39 elfzofz ⊢ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
40 csbeq1 ⊢ ( 𝑦 = 𝑘 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑘 / 𝑥 ⦌ 𝐴 )
41 40 eleq1d ⊢ ( 𝑦 = 𝑘 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ ↔ ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ∈ ℂ ) )
42 41 rspccva ⊢ ( ( ∀ 𝑦 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ∈ ℂ )
43 33 39 42 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ∈ ℂ )
44 38 43 subcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ∈ ℂ )
45 11 7 44 fsumsub ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑋 − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) = ( Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 − Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) )
46 vex ⊢ 𝑦 ∈ V
47 46 a1i ⊢ ( 𝑦 = 𝑀 → 𝑦 ∈ V )
48 eqeq2 ⊢ ( 𝑦 = 𝑀 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑀 ) )
49 48 biimpa ⊢ ( ( 𝑦 = 𝑀 ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝑀 )
50 49 5 syl ⊢ ( ( 𝑦 = 𝑀 ∧ 𝑥 = 𝑦 ) → 𝐴 = 𝐶 )
51 47 50 csbied ⊢ ( 𝑦 = 𝑀 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = 𝐶 )
52 46 a1i ⊢ ( 𝑦 = 𝑁 → 𝑦 ∈ V )
53 eqeq2 ⊢ ( 𝑦 = 𝑁 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑁 ) )
54 53 biimpa ⊢ ( ( 𝑦 = 𝑁 ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝑁 )
55 54 6 syl ⊢ ( ( 𝑦 = 𝑁 ∧ 𝑥 = 𝑦 ) → 𝐴 = 𝐷 )
56 52 55 csbied ⊢ ( 𝑦 = 𝑁 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = 𝐷 )
57 40 35 51 56 1 32 telfsumo2 ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) = ( 𝐷 − 𝐶 ) )
58 57 oveq2d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 − Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) = ( Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 − ( 𝐷 − 𝐶 ) ) )
59 45 58 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑋 − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) = ( Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 − ( 𝐷 − 𝐶 ) ) )
60 59 fveq2d ⊢ ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑋 − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) ) = ( abs ‘ ( Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 − ( 𝐷 − 𝐶 ) ) ) )
61 7 44 subcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑋 − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) ∈ ℂ )
62 11 61 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑋 − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) ∈ ℂ )
63 62 abscld ⊢ ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑋 − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) ) ∈ ℝ )
64 61 abscld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( abs ‘ ( 𝑋 − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) ) ∈ ℝ )
65 11 64 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( abs ‘ ( 𝑋 − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) ) ∈ ℝ )
66 11 8 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑌 ∈ ℝ )
67 11 61 fsumabs ⊢ ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑋 − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( abs ‘ ( 𝑋 − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) ) )
68 elfzoelz ⊢ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑘 ∈ ℤ )
69 68 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑘 ∈ ℤ )
70 69 zred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑘 ∈ ℝ )
71 70 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑘 ∈ ℝ* )
72 peano2re ⊢ ( 𝑘 ∈ ℝ → ( 𝑘 + 1 ) ∈ ℝ )
73 70 72 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ℝ )
74 73 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ℝ* )
75 70 lep1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑘 ≤ ( 𝑘 + 1 ) )
76 ubicc2 ⊢ ( ( 𝑘 ∈ ℝ* ∧ ( 𝑘 + 1 ) ∈ ℝ* ∧ 𝑘 ≤ ( 𝑘 + 1 ) ) → ( 𝑘 + 1 ) ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) )
77 71 74 75 76 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) )
78 lbicc2 ⊢ ( ( 𝑘 ∈ ℝ* ∧ ( 𝑘 + 1 ) ∈ ℝ* ∧ 𝑘 ≤ ( 𝑘 + 1 ) ) → 𝑘 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) )
79 71 74 75 78 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑘 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) )
80 13 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
81 80 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ℝ )
82 15 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
83 82 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑁 ∈ ℝ )
84 elfzole1 ⊢ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ≤ 𝑘 )
85 84 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ≤ 𝑘 )
86 34 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
87 elfzle2 ⊢ ( ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝑘 + 1 ) ≤ 𝑁 )
88 86 87 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ≤ 𝑁 )
89 iccss ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ ( 𝑀 ≤ 𝑘 ∧ ( 𝑘 + 1 ) ≤ 𝑁 ) ) → ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ( 𝑀 [,] 𝑁 ) )
90 81 83 85 88 89 syl22anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ( 𝑀 [,] 𝑁 ) )
91 90 resmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ↾ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) = ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) )
92 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
93 92 subcn ⊢ − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
94 93 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
95 iccssre ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 [,] 𝑁 ) ⊆ ℝ )
96 80 82 95 syl2anc ⊢ ( 𝜑 → ( 𝑀 [,] 𝑁 ) ⊆ ℝ )
97 96 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 [,] 𝑁 ) ⊆ ℝ )
98 ax-resscn ⊢ ℝ ⊆ ℂ
99 97 98 sstrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 [,] 𝑁 ) ⊆ ℂ )
100 ssid ⊢ ℂ ⊆ ℂ
101 100 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ℂ ⊆ ℂ )
102 cncfmptc ⊢ ( ( 𝑋 ∈ ℂ ∧ ( 𝑀 [,] 𝑁 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝑋 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) )
103 7 99 101 102 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝑋 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) )
104 cncfmptid ⊢ ( ( ( 𝑀 [,] 𝑁 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝑥 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) )
105 99 100 104 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝑥 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) )
106 103 105 mulcncf ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( 𝑋 · 𝑥 ) ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) )
107 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) )
108 92 94 106 107 cncfmpt2f ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) )
109 rescncf ⊢ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ( 𝑀 [,] 𝑁 ) → ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℂ ) → ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ↾ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℂ ) ) )
110 90 108 109 sylc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ↾ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℂ ) )
111 91 110 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℂ ) )
112 98 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ℝ ⊆ ℂ )
113 90 97 sstrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ℝ )
114 90 sselda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) → 𝑥 ∈ ( 𝑀 [,] 𝑁 ) )
115 7 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝑋 ∈ ℂ )
116 99 sselda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝑥 ∈ ℂ )
117 115 116 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( 𝑋 · 𝑥 ) ∈ ℂ )
118 25 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝐴 ∈ ℂ )
119 118 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝐴 ∈ ℂ )
120 117 119 subcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → ( ( 𝑋 · 𝑥 ) − 𝐴 ) ∈ ℂ )
121 114 120 syldan ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) → ( ( 𝑋 · 𝑥 ) − 𝐴 ) ∈ ℂ )
122 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
123 iccntr ⊢ ( ( 𝑘 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) = ( 𝑘 (,) ( 𝑘 + 1 ) ) )
124 70 73 123 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) = ( 𝑘 (,) ( 𝑘 + 1 ) ) )
125 112 113 121 122 92 124 dvmptntr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) = ( ℝ D ( 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) )
126 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
127 126 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ℝ ∈ { ℝ , ℂ } )
128 ioossicc ⊢ ( 𝑀 (,) 𝑁 ) ⊆ ( 𝑀 [,] 𝑁 )
129 128 sseli ⊢ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) → 𝑥 ∈ ( 𝑀 [,] 𝑁 ) )
130 129 120 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → ( ( 𝑋 · 𝑥 ) − 𝐴 ) ∈ ℂ )
131 ovex ⊢ ( 𝑋 − 𝐵 ) ∈ V
132 131 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → ( 𝑋 − 𝐵 ) ∈ V )
133 129 117 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → ( 𝑋 · 𝑥 ) ∈ ℂ )
134 7 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝑋 ∈ ℂ )
135 128 99 sstrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 (,) 𝑁 ) ⊆ ℂ )
136 135 sselda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝑥 ∈ ℂ )
137 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 1 ∈ ℂ )
138 112 sselda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
139 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ℝ ) → 1 ∈ ℂ )
140 127 dvmptid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ℝ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℝ ↦ 1 ) )
141 128 97 sstrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 (,) 𝑁 ) ⊆ ℝ )
142 iooretop ⊢ ( 𝑀 (,) 𝑁 ) ∈ ( topGen ‘ ran (,) )
143 142 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 (,) 𝑁 ) ∈ ( topGen ‘ ran (,) ) )
144 127 138 139 140 141 122 92 143 dvmptres ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝑥 ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 1 ) )
145 127 136 137 144 7 dvmptcmul ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ ( 𝑋 · 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ ( 𝑋 · 1 ) ) )
146 7 mulridd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑋 · 1 ) = 𝑋 )
147 146 mpteq2dv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ ( 𝑋 · 1 ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝑋 ) )
148 145 147 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ ( 𝑋 · 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝑋 ) )
149 129 119 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐴 ∈ ℂ )
150 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐵 ∈ 𝑉 )
151 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) )
152 127 133 134 148 149 150 151 dvmptsub ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ ( 𝑋 − 𝐵 ) ) )
153 81 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ℝ* )
154 iooss1 ⊢ ( ( 𝑀 ∈ ℝ* ∧ 𝑀 ≤ 𝑘 ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) ( 𝑘 + 1 ) ) )
155 153 85 154 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) ( 𝑘 + 1 ) ) )
156 83 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑁 ∈ ℝ* )
157 iooss2 ⊢ ( ( 𝑁 ∈ ℝ* ∧ ( 𝑘 + 1 ) ≤ 𝑁 ) → ( 𝑀 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) 𝑁 ) )
158 156 88 157 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) 𝑁 ) )
159 155 158 sstrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) 𝑁 ) )
160 iooretop ⊢ ( 𝑘 (,) ( 𝑘 + 1 ) ) ∈ ( topGen ‘ ran (,) )
161 160 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ∈ ( topGen ‘ ran (,) ) )
162 127 130 132 152 159 122 92 161 dvmptres ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) = ( 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 − 𝐵 ) ) )
163 125 162 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) = ( 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 − 𝐵 ) ) )
164 163 dmeqd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → dom ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) = dom ( 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 − 𝐵 ) ) )
165 eqid ⊢ ( 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 − 𝐵 ) ) = ( 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 − 𝐵 ) )
166 131 165 dmmpti ⊢ dom ( 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 − 𝐵 ) ) = ( 𝑘 (,) ( 𝑘 + 1 ) )
167 164 166 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → dom ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) = ( 𝑘 (,) ( 𝑘 + 1 ) ) )
168 163 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) = ( 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 − 𝐵 ) ) )
169 168 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → ( ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 − 𝐵 ) ) ‘ 𝑥 ) )
170 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) )
171 165 fvmpt2 ⊢ ( ( 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ∧ ( 𝑋 − 𝐵 ) ∈ V ) → ( ( 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 − 𝐵 ) ) ‘ 𝑥 ) = ( 𝑋 − 𝐵 ) )
172 170 131 171 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → ( ( 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 − 𝐵 ) ) ‘ 𝑥 ) = ( 𝑋 − 𝐵 ) )
173 169 172 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → ( ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) ‘ 𝑥 ) = ( 𝑋 − 𝐵 ) )
174 173 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → ( abs ‘ ( ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) ‘ 𝑥 ) ) = ( abs ‘ ( 𝑋 − 𝐵 ) ) )
175 9 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → ( abs ‘ ( 𝑋 − 𝐵 ) ) ≤ 𝑌 )
176 174 175 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → ( abs ‘ ( ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) ‘ 𝑥 ) ) ≤ 𝑌 )
177 176 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∀ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ( abs ‘ ( ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) ‘ 𝑥 ) ) ≤ 𝑌 )
178 nfcv ⊢ Ⅎ 𝑥 abs
179 nfcv ⊢ Ⅎ 𝑥 ℝ
180 nfcv ⊢ Ⅎ 𝑥 D
181 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) )
182 179 180 181 nfov ⊢ Ⅎ 𝑥 ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) )
183 nfcv ⊢ Ⅎ 𝑥 𝑦
184 182 183 nffv ⊢ Ⅎ 𝑥 ( ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) ‘ 𝑦 )
185 178 184 nffv ⊢ Ⅎ 𝑥 ( abs ‘ ( ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) ‘ 𝑦 ) )
186 nfcv ⊢ Ⅎ 𝑥 ≤
187 nfcv ⊢ Ⅎ 𝑥 𝑌
188 185 186 187 nfbr ⊢ Ⅎ 𝑥 ( abs ‘ ( ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) ‘ 𝑦 ) ) ≤ 𝑌
189 2fveq3 ⊢ ( 𝑥 = 𝑦 → ( abs ‘ ( ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) ‘ 𝑥 ) ) = ( abs ‘ ( ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) ‘ 𝑦 ) ) )
190 189 breq1d ⊢ ( 𝑥 = 𝑦 → ( ( abs ‘ ( ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) ‘ 𝑥 ) ) ≤ 𝑌 ↔ ( abs ‘ ( ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) ‘ 𝑦 ) ) ≤ 𝑌 ) )
191 188 190 rspc ⊢ ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) → ( ∀ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ( abs ‘ ( ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) ‘ 𝑥 ) ) ≤ 𝑌 → ( abs ‘ ( ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) ‘ 𝑦 ) ) ≤ 𝑌 ) )
192 177 191 mpan9 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → ( abs ‘ ( ( ℝ D ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ) ‘ 𝑦 ) ) ≤ 𝑌 )
193 70 73 111 167 8 192 dvlip ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ ( ( 𝑘 + 1 ) ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ∧ 𝑘 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) ) → ( abs ‘ ( ( ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ‘ ( 𝑘 + 1 ) ) − ( ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ‘ 𝑘 ) ) ) ≤ ( 𝑌 · ( abs ‘ ( ( 𝑘 + 1 ) − 𝑘 ) ) ) )
194 193 ex ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( 𝑘 + 1 ) ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ∧ 𝑘 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) → ( abs ‘ ( ( ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ‘ ( 𝑘 + 1 ) ) − ( ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ‘ 𝑘 ) ) ) ≤ ( 𝑌 · ( abs ‘ ( ( 𝑘 + 1 ) − 𝑘 ) ) ) ) )
195 77 79 194 mp2and ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( abs ‘ ( ( ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ‘ ( 𝑘 + 1 ) ) − ( ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ‘ 𝑘 ) ) ) ≤ ( 𝑌 · ( abs ‘ ( ( 𝑘 + 1 ) − 𝑘 ) ) ) )
196 ovex ⊢ ( ( 𝑋 · ( 𝑘 + 1 ) ) − ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 ) ∈ V
197 nfcv ⊢ Ⅎ 𝑥 ( 𝑘 + 1 )
198 nfcv ⊢ Ⅎ 𝑥 ( 𝑋 · ( 𝑘 + 1 ) )
199 nfcv ⊢ Ⅎ 𝑥 −
200 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴
201 198 199 200 nfov ⊢ Ⅎ 𝑥 ( ( 𝑋 · ( 𝑘 + 1 ) ) − ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 )
202 oveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑋 · 𝑥 ) = ( 𝑋 · ( 𝑘 + 1 ) ) )
203 csbeq1a ⊢ ( 𝑥 = ( 𝑘 + 1 ) → 𝐴 = ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 )
204 202 203 oveq12d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝑋 · 𝑥 ) − 𝐴 ) = ( ( 𝑋 · ( 𝑘 + 1 ) ) − ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 ) )
205 eqid ⊢ ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) = ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) )
206 197 201 204 205 fvmptf ⊢ ( ( ( 𝑘 + 1 ) ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ∧ ( ( 𝑋 · ( 𝑘 + 1 ) ) − ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 ) ∈ V ) → ( ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑋 · ( 𝑘 + 1 ) ) − ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 ) )
207 77 196 206 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝑋 · ( 𝑘 + 1 ) ) − ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 ) )
208 70 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑘 ∈ ℂ )
209 7 208 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑋 · 𝑘 ) ∈ ℂ )
210 209 43 subcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑋 · 𝑘 ) − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ∈ ℂ )
211 nfcv ⊢ Ⅎ 𝑥 𝑘
212 nfcv ⊢ Ⅎ 𝑥 ( 𝑋 · 𝑘 )
213 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑘 / 𝑥 ⦌ 𝐴
214 212 199 213 nfov ⊢ Ⅎ 𝑥 ( ( 𝑋 · 𝑘 ) − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 )
215 oveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑋 · 𝑥 ) = ( 𝑋 · 𝑘 ) )
216 csbeq1a ⊢ ( 𝑥 = 𝑘 → 𝐴 = ⦋ 𝑘 / 𝑥 ⦌ 𝐴 )
217 215 216 oveq12d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑋 · 𝑥 ) − 𝐴 ) = ( ( 𝑋 · 𝑘 ) − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) )
218 211 214 217 205 fvmptf ⊢ ( ( 𝑘 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ∧ ( ( 𝑋 · 𝑘 ) − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ∈ ℂ ) → ( ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ‘ 𝑘 ) = ( ( 𝑋 · 𝑘 ) − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) )
219 79 210 218 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ‘ 𝑘 ) = ( ( 𝑋 · 𝑘 ) − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) )
220 207 219 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ‘ ( 𝑘 + 1 ) ) − ( ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ‘ 𝑘 ) ) = ( ( ( 𝑋 · ( 𝑘 + 1 ) ) − ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 ) − ( ( 𝑋 · 𝑘 ) − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) )
221 peano2cn ⊢ ( 𝑘 ∈ ℂ → ( 𝑘 + 1 ) ∈ ℂ )
222 208 221 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ℂ )
223 7 222 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑋 · ( 𝑘 + 1 ) ) ∈ ℂ )
224 223 209 38 43 sub4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( 𝑋 · ( 𝑘 + 1 ) ) − ( 𝑋 · 𝑘 ) ) − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) = ( ( ( 𝑋 · ( 𝑘 + 1 ) ) − ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 ) − ( ( 𝑋 · 𝑘 ) − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) )
225 1cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 1 ∈ ℂ )
226 208 225 pncan2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑘 + 1 ) − 𝑘 ) = 1 )
227 226 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑋 · ( ( 𝑘 + 1 ) − 𝑘 ) ) = ( 𝑋 · 1 ) )
228 7 222 208 subdid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑋 · ( ( 𝑘 + 1 ) − 𝑘 ) ) = ( ( 𝑋 · ( 𝑘 + 1 ) ) − ( 𝑋 · 𝑘 ) ) )
229 227 228 146 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑋 · ( 𝑘 + 1 ) ) − ( 𝑋 · 𝑘 ) ) = 𝑋 )
230 229 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ( 𝑋 · ( 𝑘 + 1 ) ) − ( 𝑋 · 𝑘 ) ) − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑋 − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) )
231 220 224 230 3eqtr2rd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑋 − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) = ( ( ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ‘ ( 𝑘 + 1 ) ) − ( ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ‘ 𝑘 ) ) )
232 231 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( abs ‘ ( 𝑋 − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) ) = ( abs ‘ ( ( ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ‘ ( 𝑘 + 1 ) ) − ( ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( ( 𝑋 · 𝑥 ) − 𝐴 ) ) ‘ 𝑘 ) ) ) )
233 226 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( abs ‘ ( ( 𝑘 + 1 ) − 𝑘 ) ) = ( abs ‘ 1 ) )
234 abs1 ⊢ ( abs ‘ 1 ) = 1
235 233 234 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( abs ‘ ( ( 𝑘 + 1 ) − 𝑘 ) ) = 1 )
236 235 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑌 · ( abs ‘ ( ( 𝑘 + 1 ) − 𝑘 ) ) ) = ( 𝑌 · 1 ) )
237 8 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑌 ∈ ℂ )
238 237 mulridd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑌 · 1 ) = 𝑌 )
239 236 238 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑌 = ( 𝑌 · ( abs ‘ ( ( 𝑘 + 1 ) − 𝑘 ) ) ) )
240 195 232 239 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( abs ‘ ( 𝑋 − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) ) ≤ 𝑌 )
241 11 64 8 240 fsumle ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( abs ‘ ( 𝑋 − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑌 )
242 63 65 66 67 241 letrd ⊢ ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝑋 − ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑌 )
243 60 242 eqbrtrrd ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 − ( 𝐷 − 𝐶 ) ) ) ≤ Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑌 )