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

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) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

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 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) → 𝑋 ∈ ℂ )
60 46 54 iccssred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ℝ )
61 ax-resscn ⊢ ℝ ⊆ ℂ
62 60 61 sstrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ℂ )
63 62 sselda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) → 𝑦 ∈ ℂ )
64 ovmpot ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑋 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( 𝑋 · 𝑦 ) )
65 59 63 64 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) → ( 𝑋 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( 𝑋 · 𝑦 ) )
66 65 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) → ( 𝑧 = ( 𝑋 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ↔ 𝑧 = ( 𝑋 · 𝑦 ) ) )
67 66 pm5.32da ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ∧ 𝑧 = ( 𝑋 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) ↔ ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ∧ 𝑧 = ( 𝑋 · 𝑦 ) ) ) )
68 67 opabbidv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ∧ 𝑧 = ( 𝑋 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ∧ 𝑧 = ( 𝑋 · 𝑦 ) ) } )
69 df-mpt ⊢ ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( 𝑋 · 𝑦 ) ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ∧ 𝑧 = ( 𝑋 · 𝑦 ) ) }
70 68 69 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ∧ 𝑧 = ( 𝑋 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } = ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( 𝑋 · 𝑦 ) ) )
71 df-mpt ⊢ ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( 𝑋 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ∧ 𝑧 = ( 𝑋 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) }
72 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
73 72 mpomulcn ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
74 61 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ℝ ⊆ ℂ )
75 cncfmptc ⊢ ( ( 𝑋 ∈ ℝ ∧ ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ 𝑋 ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
76 7 62 74 75 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ 𝑋 ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
77 cncfmptid ⊢ ( ( ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ 𝑦 ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
78 60 61 77 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ 𝑦 ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
79 simpl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑋 ∈ ℝ )
80 79 recnd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑋 ∈ ℂ )
81 simpr ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
82 81 recnd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
83 64 eqcomd ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑋 · 𝑦 ) = ( 𝑋 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) )
84 80 82 83 syl2anc ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑋 · 𝑦 ) = ( 𝑋 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) )
85 remulcl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑋 · 𝑦 ) ∈ ℝ )
86 84 85 eqeltrrd ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑋 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ∈ ℝ )
87 72 73 76 78 61 86 cncfmpt2ss ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( 𝑋 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
88 71 87 eqeltrrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ∧ 𝑧 = ( 𝑋 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ) } ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
89 70 88 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ( 𝑋 · 𝑦 ) ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
90 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
91 90 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ℝ ∈ { ℝ , ℂ } )
92 12 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
93 92 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ℝ )
94 93 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ℝ* )
95 elfzole1 ⊢ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ≤ 𝑘 )
96 95 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ≤ 𝑘 )
97 iooss1 ⊢ ( ( 𝑀 ∈ ℝ* ∧ 𝑀 ≤ 𝑘 ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) ( 𝑘 + 1 ) ) )
98 94 96 97 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) ( 𝑘 + 1 ) ) )
99 14 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
100 99 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑁 ∈ ℝ )
101 100 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑁 ∈ ℝ* )
102 33 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
103 elfzle2 ⊢ ( ( 𝑘 + 1 ) ∈ ( 𝑀 ... 𝑁 ) → ( 𝑘 + 1 ) ≤ 𝑁 )
104 102 103 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ≤ 𝑁 )
105 iooss2 ⊢ ( ( 𝑁 ∈ ℝ* ∧ ( 𝑘 + 1 ) ≤ 𝑁 ) → ( 𝑀 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) 𝑁 ) )
106 101 104 105 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) 𝑁 ) )
107 98 106 sstrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ( 𝑀 (,) 𝑁 ) )
108 ioossicc ⊢ ( 𝑀 (,) 𝑁 ) ⊆ ( 𝑀 [,] 𝑁 )
109 92 99 iccssred ⊢ ( 𝜑 → ( 𝑀 [,] 𝑁 ) ⊆ ℝ )
110 109 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 [,] 𝑁 ) ⊆ ℝ )
111 110 61 sstrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 [,] 𝑁 ) ⊆ ℂ )
112 108 111 sstrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 (,) 𝑁 ) ⊆ ℂ )
113 107 112 sstrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ℂ )
114 113 sselda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → 𝑦 ∈ ℂ )
115 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → 1 ∈ ℂ )
116 74 sselda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℂ )
117 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℝ ) → 1 ∈ ℂ )
118 91 dvmptid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑦 ∈ ℝ ↦ 𝑦 ) ) = ( 𝑦 ∈ ℝ ↦ 1 ) )
119 ioossre ⊢ ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ℝ
120 119 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ⊆ ℝ )
121 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
122 iooretop ⊢ ( 𝑘 (,) ( 𝑘 + 1 ) ) ∈ ( topGen ‘ ran (,) )
123 122 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 (,) ( 𝑘 + 1 ) ) ∈ ( topGen ‘ ran (,) ) )
124 91 116 117 118 120 121 72 123 dvmptres ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ 𝑦 ) ) = ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ 1 ) )
125 91 114 115 124 52 dvmptcmul ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 · 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 · 1 ) ) )
126 57 mpteq2dv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 · 1 ) ) = ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ 𝑋 ) )
127 125 126 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ( 𝑋 · 𝑦 ) ) ) = ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ 𝑋 ) )
128 nfcv ⊢ Ⅎ 𝑦 𝐴
129 128 25 27 cbvmpt ⊢ ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ 𝐴 ) = ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
130 iccss ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ ( 𝑀 ≤ 𝑘 ∧ ( 𝑘 + 1 ) ≤ 𝑁 ) ) → ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ( 𝑀 [,] 𝑁 ) )
131 93 100 96 104 130 syl22anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ( 𝑀 [,] 𝑁 ) )
132 131 resmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ↾ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) = ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ 𝐴 ) )
133 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) )
134 rescncf ⊢ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) ⊆ ( 𝑀 [,] 𝑁 ) → ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) → ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ↾ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) ) )
135 131 133 134 sylc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ↾ ( 𝑘 [,] ( 𝑘 + 1 ) ) ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
136 132 135 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ 𝐴 ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
137 129 136 eqeltrrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑦 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ∈ ( ( 𝑘 [,] ( 𝑘 + 1 ) ) –cn→ ℝ ) )
138 21 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) : ( 𝑀 [,] 𝑁 ) ⟶ ℝ )
139 138 23 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∀ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) 𝐴 ∈ ℝ )
140 108 sseli ⊢ ( 𝑦 ∈ ( 𝑀 (,) 𝑁 ) → 𝑦 ∈ ( 𝑀 [,] 𝑁 ) )
141 29 impcom ⊢ ( ( ∀ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) 𝐴 ∈ ℝ ∧ 𝑦 ∈ ( 𝑀 [,] 𝑁 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ )
142 139 140 141 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝑀 (,) 𝑁 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℝ )
143 142 recnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝑀 (,) 𝑁 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ )
144 108 sseli ⊢ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) → 𝑥 ∈ ( 𝑀 [,] 𝑁 ) )
145 21 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝐴 ∈ ℝ )
146 145 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ) → 𝐴 ∈ ℝ )
147 144 146 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐴 ∈ ℝ )
148 147 fmpttd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ )
149 ioossre ⊢ ( 𝑀 (,) 𝑁 ) ⊆ ℝ
150 dvfre ⊢ ( ( ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ ∧ ( 𝑀 (,) 𝑁 ) ⊆ ℝ ) → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) : dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) ⟶ ℝ )
151 148 149 150 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) : dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) ⟶ ℝ )
152 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) )
153 152 dmeqd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = dom ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) )
154 3 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐵 ∈ 𝑉 )
155 154 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∀ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) 𝐵 ∈ 𝑉 )
156 dmmptg ⊢ ( ∀ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) = ( 𝑀 (,) 𝑁 ) )
157 155 156 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → dom ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) = ( 𝑀 (,) 𝑁 ) )
158 153 157 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( 𝑀 (,) 𝑁 ) )
159 152 158 feq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) : dom ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) ⟶ ℝ ↔ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ ) )
160 151 159 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ )
161 eqid ⊢ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 )
162 161 fmpt ⊢ ( ∀ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) 𝐵 ∈ ℝ ↔ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) : ( 𝑀 (,) 𝑁 ) ⟶ ℝ )
163 160 162 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∀ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) 𝐵 ∈ ℝ )
164 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
165 164 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ
166 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
167 166 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∈ ℝ ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
168 165 167 rspc ⊢ ( 𝑦 ∈ ( 𝑀 (,) 𝑁 ) → ( ∀ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) 𝐵 ∈ ℝ → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
169 163 168 mpan9 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝑀 (,) 𝑁 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℝ )
170 128 25 27 cbvmpt ⊢ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) = ( 𝑦 ∈ ( 𝑀 (,) 𝑁 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
171 170 oveq2i ⊢ ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( ℝ D ( 𝑦 ∈ ( 𝑀 (,) 𝑁 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) )
172 nfcv ⊢ Ⅎ 𝑦 𝐵
173 172 164 166 cbvmpt ⊢ ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) = ( 𝑦 ∈ ( 𝑀 (,) 𝑁 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
174 152 171 173 3eqtr3g ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑦 ∈ ( 𝑀 (,) 𝑁 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑦 ∈ ( 𝑀 (,) 𝑁 ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
175 91 143 169 174 107 121 72 123 dvmptres ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ℝ D ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
176 8 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → 𝑋 ≤ 𝐵 )
177 176 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∀ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) 𝑋 ≤ 𝐵 )
178 nfcv ⊢ Ⅎ 𝑥 𝑋
179 nfcv ⊢ Ⅎ 𝑥 ≤
180 178 179 164 nfbr ⊢ Ⅎ 𝑥 𝑋 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵
181 166 breq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑋 ≤ 𝐵 ↔ 𝑋 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
182 180 181 rspc ⊢ ( 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) → ( ∀ 𝑥 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) 𝑋 ≤ 𝐵 → 𝑋 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
183 177 182 mpan9 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝑘 (,) ( 𝑘 + 1 ) ) ) → 𝑋 ≤ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
184 46 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑘 ∈ ℝ* )
185 54 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ℝ* )
186 46 lep1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑘 ≤ ( 𝑘 + 1 ) )
187 lbicc2 ⊢ ( ( 𝑘 ∈ ℝ* ∧ ( 𝑘 + 1 ) ∈ ℝ* ∧ 𝑘 ≤ ( 𝑘 + 1 ) ) → 𝑘 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) )
188 184 185 186 187 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑘 ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) )
189 ubicc2 ⊢ ( ( 𝑘 ∈ ℝ* ∧ ( 𝑘 + 1 ) ∈ ℝ* ∧ 𝑘 ≤ ( 𝑘 + 1 ) ) → ( 𝑘 + 1 ) ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) )
190 184 185 186 189 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( 𝑘 [,] ( 𝑘 + 1 ) ) )
191 oveq2 ⊢ ( 𝑦 = 𝑘 → ( 𝑋 · 𝑦 ) = ( 𝑋 · 𝑘 ) )
192 oveq2 ⊢ ( 𝑦 = ( 𝑘 + 1 ) → ( 𝑋 · 𝑦 ) = ( 𝑋 · ( 𝑘 + 1 ) ) )
193 46 54 89 127 137 175 183 188 190 186 191 39 192 34 dvle ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑋 · ( 𝑘 + 1 ) ) − ( 𝑋 · 𝑘 ) ) ≤ ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) )
194 58 193 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑋 ≤ ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) )
195 10 7 43 194 fsumle ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 ≤ Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) )
196 vex ⊢ 𝑦 ∈ V
197 196 a1i ⊢ ( 𝑦 = 𝑀 → 𝑦 ∈ V )
198 eqeq2 ⊢ ( 𝑦 = 𝑀 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑀 ) )
199 198 biimpa ⊢ ( ( 𝑦 = 𝑀 ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝑀 )
200 199 5 syl ⊢ ( ( 𝑦 = 𝑀 ∧ 𝑥 = 𝑦 ) → 𝐴 = 𝐶 )
201 197 200 csbied ⊢ ( 𝑦 = 𝑀 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = 𝐶 )
202 196 a1i ⊢ ( 𝑦 = 𝑁 → 𝑦 ∈ V )
203 eqeq2 ⊢ ( 𝑦 = 𝑁 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑁 ) )
204 203 biimpa ⊢ ( ( 𝑦 = 𝑁 ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝑁 )
205 204 6 syl ⊢ ( ( 𝑦 = 𝑁 ∧ 𝑥 = 𝑦 ) → 𝐴 = 𝐷 )
206 202 205 csbied ⊢ ( 𝑦 = 𝑁 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = 𝐷 )
207 31 recnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ )
208 39 34 201 206 1 207 telfsumo2 ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( ⦋ ( 𝑘 + 1 ) / 𝑥 ⦌ 𝐴 − ⦋ 𝑘 / 𝑥 ⦌ 𝐴 ) = ( 𝐷 − 𝐶 ) )
209 195 208 breqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 ≤ ( 𝐷 − 𝐶 ) )