Theorem gg-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) Use mpomulcn instead of mulcn as direct dependency. (Revised by GG, 16-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		gg-dvfsumle.m	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		gg-dvfsumle.a	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑀 [,] 𝑁 ) ↦ 𝐴 ) ∈ ( ( 𝑀 [,] 𝑁 ) –cn→ ℝ ) )
3		gg-dvfsumle.v	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ) → 𝐵 ∈ 𝑉 )
4		gg-dvfsumle.b	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑀 (,) 𝑁 ) ↦ 𝐵 ) )
5		gg-dvfsumle.c	⊢ ( 𝑥 = 𝑀 → 𝐴 = 𝐶 )
6		gg-dvfsumle.d	⊢ ( 𝑥 = 𝑁 → 𝐴 = 𝐷 )
7		gg-dvfsumle.x	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑋 ∈ ℝ )
8		gg-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		ovmul	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑋 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( 𝑋 · 𝑦 ) )
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	72	tgioo2	⊢ ( 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	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝑋 ≤ ( 𝐷 − 𝐶 ) )