Metamath Proof Explorer

Theorem dvfsumle

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

Proof

Step Hyp Ref Expression
1 dvfsumle.m ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 dvfsumle.a ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) )
3 dvfsumle.v ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐵 ∈ 𝑉 )
4 dvfsumle.b ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) )
5 dvfsumle.c ⊢ ( 𝑥 = 𝑀 → 𝐴 = 𝐶 )
6 dvfsumle.d ⊢ ( 𝑥 = 𝑁 → 𝐴 = 𝐷 )
7 dvfsumle.x ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑋 ∈ ℝ )
8 dvfsumle.l ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) ) → 𝑋 ≤ 𝐵 )
9 fzofi ⊢ ( 𝑀 ..^ 𝑁 ) ∈ Fin
10 9 a1i ⊢ ( 𝜑 → ( 𝑀 ..^ 𝑁 ) ∈ Fin )
11 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
12 1 11 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
13 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
14 1 13 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
15 fzval2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 [,] 𝑁 ) ∩ ℤ ) )
16 12 14 15 syl2anc ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 [,] 𝑁 ) ∩ ℤ ) )
17 inss1 ⊢ ( ( 𝑀 [,] 𝑁 ) ∩ ℤ ) ⊆ ( 𝑀 [,] 𝑁 )
18 16 17 eqsstrdi ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ⊆ ( 𝑀 [,] 𝑁 ) )
19 18 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑦 ∈ ( 𝑀 [,] 𝑁 ) )
20 cncff ⊢ ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) : ( 𝑀 [,] 𝑁 ) ⟶ ℝ )
21 2 20 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) : ( 𝑀 [,] 𝑁 ) ⟶ ℝ )
22 eqid ⊢ ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) = ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 )
23 22 fmpt ⊢ ( ∀ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) 𝐴 ∈ ℝ ↔ ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) : ( 𝑀 [,] 𝑁 ) ⟶ ℝ )
24 21 23 sylibr ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) 𝐴 ∈ ℝ )
25 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐴
26 25 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ
27 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
28 27 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ ℝ ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ ) )
29 26 28 rspc ⊢ ( 𝑦 ∈ ( 𝑀 [,] 𝑁 ) → ( ∀ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) 𝐴 ∈ ℝ → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ ) )
30 24 29 mpan9 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑀 [,] 𝑁 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ )
31 19 30 syldan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ )
32 31 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ )
33 fzofzp1 ⊢ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
34 csbeq1 ⊢ ( 𝑦 = ( 𝑘 + 1 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 )
35 34 eleq1d ⊢ ( 𝑦 = ( 𝑘 + 1 ) → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ ↔ ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 ∈ ℝ ) )
36 35 rspccva ⊢ ( ( ∀ 𝑦 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ ∧ ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 ∈ ℝ )
37 32 33 36 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 ∈ ℝ )
38 elfzofz ⊢ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
39 csbeq1 ⊢ ( 𝑦 = 𝑘 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑘 / 𝑥 ⦌ 𝐴 )
40 39 eleq1d ⊢ ( 𝑦 = 𝑘 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ ↔ ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ∈ ℝ ) )
41 40 rspccva ⊢ ( ( ∀ 𝑦 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ∈ ℝ )
42 32 38 41 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ∈ ℝ )
43 37 42 resubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) ∈ ℝ )
44 elfzoelz ⊢ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑘 ∈ ℤ )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑘 ∈ ℤ )
46 45 zred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑘 ∈ ℝ )
47 46 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑘 ∈ ℂ )
48 ax-1cn ⊢ 1 ∈ ℂ
49 pncan2 ⊢ ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑘 + 1 ) − 𝑘 ) = 1 )
50 47 48 49 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑘 + 1 ) − 𝑘 ) = 1 )
51 50 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑋 · ( ( 𝑘 + 1 ) − 𝑘 ) ) = ( 𝑋 · 1 ) )
52 7 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑋 ∈ ℂ )
53 peano2re ⊢ ( 𝑘 ∈ ℝ → ( 𝑘 + 1 ) ∈ ℝ )
54 46 53 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ℝ )
55 54 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ℂ )
56 52 55 47 subdid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑋 · ( ( 𝑘 + 1 ) − 𝑘 ) ) = ( ( 𝑋 · ( 𝑘 + 1 ) ) − ( 𝑋 · 𝑘 ) ) )
57 52 mulridd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑋 · 1 ) = 𝑋 )
58 51 56 57 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑋 · ( 𝑘 + 1 ) ) − ( 𝑋 · 𝑘 ) ) = 𝑋 )
59 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
60 59 mulcn ⊢ · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
61 12 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
62 61 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ℝ )
63 14 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑁 ∈ ℝ )
65 elfzole1 ⊢ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ≤ 𝑘 )
66 65 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ≤ 𝑘 )
67 33 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
68 elfzle2 ⊢ ( ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝑘 + 1 ) ≤ 𝑁 )
69 67 68 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ≤ 𝑁 )
70 iccss ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ ( 𝑀 ≤ 𝑘 ∧ ( 𝑘 + 1 ) ≤ 𝑁 ) ) → ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ( 𝑀 [,] 𝑁 ) )
71 62 64 66 69 70 syl22anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ( 𝑀 [,] 𝑁 ) )
72 iccssre ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 [,] 𝑁 ) ⊆ ℝ )
73 61 63 72 syl2anc ⊢ ( 𝜑 → ( 𝑀 [,] 𝑁 ) ⊆ ℝ )
74 73 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 [,] 𝑁 ) ⊆ ℝ )
75 71 74 sstrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ℝ )
76 ax-resscn ⊢ ℝ ⊆ ℂ
77 75 76 sstrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ℂ )
78 76 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ℝ ⊆ ℂ )
79 cncfmptc ⊢ ( ( 𝑋 ∈ ℝ ∧ ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ 𝑋 ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
80 7 77 78 79 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ 𝑋 ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
81 cncfmptid ⊢ ( ( ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ 𝑦 ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
82 75 76 81 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ 𝑦 ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
83 remulcl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑋 · 𝑦 ) ∈ ℝ )
84 59 60 80 82 76 83 cncfmpt2ss ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( 𝑋 · 𝑦 ) ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
85 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
86 85 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ℝ ∈ { ℝ , ℂ } )
87 62 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ℝ* )
88 iooss1 ⊢ ( ( 𝑀 ∈ ℝ* ∧ 𝑀 ≤ 𝑘 ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) ( 𝑘 + 1 ) ) )
89 87 66 88 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) ( 𝑘 + 1 ) ) )
90 64 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑁 ∈ ℝ* )
91 iooss2 ⊢ ( ( 𝑁 ∈ ℝ* ∧ ( 𝑘 + 1 ) ≤ 𝑁 ) → ( 𝑀 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) 𝑁 ) )
92 90 69 91 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) 𝑁 ) )
93 89 92 sstrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) 𝑁 ) )
94 ioossicc ⊢ ( 𝑀 (,) 𝑁 ) ⊆ ( 𝑀 [,] 𝑁 )
95 74 76 sstrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 [,] 𝑁 ) ⊆ ℂ )
96 94 95 sstrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 (,) 𝑁 ) ⊆ ℂ )
97 93 96 sstrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ℂ )
98 97 sselda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → 𝑦 ∈ ℂ )
99 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → 1 ∈ ℂ )
100 78 sselda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
101 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℝ ) → 1 ∈ ℂ )
102 86 dvmptid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑦 ∈ ℝ ↦ 𝑦 ) ) = ( 𝑦 ∈ ℝ ↦ 1 ) )
103 ioossre ⊢ ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ℝ
104 103 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ℝ )
105 59 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
106 iooretop ⊢ ( 𝑘 (,) ( 𝑘 + 1 ) ) ∈ ( topGen ‘ ran (,) )
107 106 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ∈ ( topGen ‘ ran (,) ) )
108 86 100 101 102 104 105 59 107 dvmptres ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ 𝑦 ) ) = ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ 1 ) )
109 86 98 99 108 52 dvmptcmul ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 · 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 · 1 ) ) )
110 57 mpteq2dv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 · 1 ) ) = ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ 𝑋 ) )
111 109 110 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 · 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ 𝑋 ) )
112 nfcv ⊢ Ⅎ 𝑦 𝐴
113 112 25 27 cbvmpt ⊢ ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ 𝐴 ) = ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
114 71 resmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ↾ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) = ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ 𝐴 ) )
115 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) )
116 rescncf ⊢ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ( 𝑀 [,] 𝑁 ) → ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) → ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ↾ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) ) )
117 71 115 116 sylc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ↾ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
118 114 117 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ 𝐴 ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
119 113 118 eqeltrrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
120 21 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) : ( 𝑀 [,] 𝑁 ) ⟶ ℝ )
121 120 23 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∀ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) 𝐴 ∈ ℝ )
122 94 sseli ⊢ ( 𝑦 ∈ ( 𝑀 (,) 𝑁 ) → 𝑦 ∈ ( 𝑀 [,] 𝑁 ) )
123 29 impcom ⊢ ( ( ∀ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) 𝐴 ∈ ℝ ∧ 𝑦 ∈ ( 𝑀 [,] 𝑁 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ )
124 121 122 123 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝑀 (,) 𝑁 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ )
125 124 recnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝑀 (,) 𝑁 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ )
126 94 sseli ⊢ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) → 𝑥 ∈ ( 𝑀 [,] 𝑁 ) )
127 21 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝐴 ∈ ℝ )
128 127 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝐴 ∈ ℝ )
129 126 128 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐴 ∈ ℝ )
130 129 fmpttd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ )
131 ioossre ⊢ ( 𝑀 (,) 𝑁 ) ⊆ ℝ
132 dvfre ⊢ ( ( ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ ∧ ( 𝑀 (,) 𝑁 ) ⊆ ℝ ) → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) : dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) ⟶ ℝ )
133 130 131 132 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) : dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) ⟶ ℝ )
134 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) )
135 134 dmeqd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = dom ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) )
136 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐵 ∈ 𝑉 )
137 136 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∀ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) 𝐵 ∈ 𝑉 )
138 dmmptg ⊢ ( ∀ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) = ( 𝑀 (,) 𝑁 ) )
139 137 138 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → dom ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) = ( 𝑀 (,) 𝑁 ) )
140 135 139 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( 𝑀 (,) 𝑁 ) )
141 134 140 feq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) : dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) ⟶ ℝ ↔ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ ) )
142 133 141 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ )
143 eqid ⊢ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 )
144 143 fmpt ⊢ ( ∀ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) 𝐵 ∈ ℝ ↔ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ )
145 142 144 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∀ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) 𝐵 ∈ ℝ )
146 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
147 146 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ
148 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
149 148 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∈ ℝ ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
150 147 149 rspc ⊢ ( 𝑦 ∈ ( 𝑀 (,) 𝑁 ) → ( ∀ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) 𝐵 ∈ ℝ → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
151 145 150 mpan9 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝑀 (,) 𝑁 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ )
152 112 25 27 cbvmpt ⊢ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) = ( 𝑦 ∈ ( 𝑀 (,) 𝑁 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
153 152 oveq2i ⊢ ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( ℝ D ( 𝑦 ∈ ( 𝑀 (,) 𝑁 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) )
154 nfcv ⊢ Ⅎ 𝑦 𝐵
155 154 146 148 cbvmpt ⊢ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) = ( 𝑦 ∈ ( 𝑀 (,) 𝑁 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
156 134 153 155 3eqtr3g ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑦 ∈ ( 𝑀 (,) 𝑁 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑦 ∈ ( 𝑀 (,) 𝑁 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
157 86 125 151 156 93 105 59 107 dvmptres ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
158 8 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → 𝑋 ≤ 𝐵 )
159 158 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∀ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) 𝑋 ≤ 𝐵 )
160 nfcv ⊢ Ⅎ 𝑥 𝑋
161 nfcv ⊢ Ⅎ 𝑥 ≤
162 160 161 146 nfbr ⊢ Ⅎ 𝑥 𝑋 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵
163 148 breq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑋 ≤ 𝐵 ↔ 𝑋 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
164 162 163 rspc ⊢ ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) → ( ∀ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) 𝑋 ≤ 𝐵 → 𝑋 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
165 159 164 mpan9 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → 𝑋 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
166 46 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑘 ∈ ℝ* )
167 54 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ℝ* )
168 46 lep1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑘 ≤ ( 𝑘 + 1 ) )
169 lbicc2 ⊢ ( ( 𝑘 ∈ ℝ* ∧ ( 𝑘 + 1 ) ∈ ℝ* ∧ 𝑘 ≤ ( 𝑘 + 1 ) ) → 𝑘 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) )
170 166 167 168 169 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑘 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) )
171 ubicc2 ⊢ ( ( 𝑘 ∈ ℝ* ∧ ( 𝑘 + 1 ) ∈ ℝ* ∧ 𝑘 ≤ ( 𝑘 + 1 ) ) → ( 𝑘 + 1 ) ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) )
172 166 167 168 171 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) )
173 oveq2 ⊢ ( 𝑦 = 𝑘 → ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑘 ) )
174 oveq2 ⊢ ( 𝑦 = ( 𝑘 + 1 ) → ( 𝑋 · 𝑦 ) = ( 𝑋 · ( 𝑘 + 1 ) ) )
175 46 54 84 111 119 157 165 170 172 168 173 39 174 34 dvle ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑋 · ( 𝑘 + 1 ) ) − ( 𝑋 · 𝑘 ) ) ≤ ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) )
176 58 175 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑋 ≤ ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) )
177 10 7 43 176 fsumle ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 ≤ Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) )
178 vex ⊢ 𝑦 ∈ V
179 178 a1i ⊢ ( 𝑦 = 𝑀 → 𝑦 ∈ V )
180 eqeq2 ⊢ ( 𝑦 = 𝑀 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑀 ) )
181 180 biimpa ⊢ ( ( 𝑦 = 𝑀 ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝑀 )
182 181 5 syl ⊢ ( ( 𝑦 = 𝑀 ∧ 𝑥 = 𝑦 ) → 𝐴 = 𝐶 )
183 179 182 csbied ⊢ ( 𝑦 = 𝑀 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = 𝐶 )
184 178 a1i ⊢ ( 𝑦 = 𝑁 → 𝑦 ∈ V )
185 eqeq2 ⊢ ( 𝑦 = 𝑁 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑁 ) )
186 185 biimpa ⊢ ( ( 𝑦 = 𝑁 ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝑁 )
187 186 6 syl ⊢ ( ( 𝑦 = 𝑁 ∧ 𝑥 = 𝑦 ) → 𝐴 = 𝐷 )
188 184 187 csbied ⊢ ( 𝑦 = 𝑁 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = 𝐷 )
189 31 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ )
190 39 34 183 188 1 189 telfsumo2 ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) = ( 𝐷 − 𝐶 ) )
191 177 190 breqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 ≤ ( 𝐷 − 𝐶 ) )