gg-dvfsumle - Mathbox for Gino Giotto

	Mathbox for Gino Giotto		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > gg-dvfsumle		Structured version Visualization version GIF version

Theorem gg-dvfsumle 35479

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

**Hypotheses**
Ref	Expression
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**
Ref	Expression
gg-dvfsumle	⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ (𝐷 − 𝐶))

Distinct variable groups: 𝐴,𝑘 𝑥,𝑘,𝑀 𝑘,𝑁,𝑥 𝜑,𝑘,𝑥 𝑥,𝑋 𝑥,𝐶 𝑥,𝐷 Allowed substitution hints: 𝐴(𝑥) 𝐵(𝑥,𝑘) 𝐶(𝑘) 𝐷(𝑘) 𝑉(𝑥,𝑘) 𝑋(𝑘)

Proof of Theorem gg-dvfsumle Dummy variables 𝑦 𝑧 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzofi 13946	. . . 4 ⊢ (𝑀..^𝑁) ∈ Fin
2	1	a1i 11	. . 3 ⊢ (𝜑 → (𝑀..^𝑁) ∈ Fin)
3		gg-dvfsumle.x	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℝ)
4		gg-dvfsumle.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
5		eluzel2 12834	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
6	4, 5	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℤ)
7		eluzelz 12839	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ ℤ)
8	4, 7	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
9		fzval2 13494	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ))
10	6, 8, 9	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ))
11		inss1 4228	. . . . . . . . 9 ⊢ ((𝑀[,]𝑁) ∩ ℤ) ⊆ (𝑀[,]𝑁)
12	10, 11	eqsstrdi 4036	. . . . . . . 8 ⊢ (𝜑 → (𝑀...𝑁) ⊆ (𝑀[,]𝑁))
13	12	sselda 3982	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀...𝑁)) → 𝑦 ∈ (𝑀[,]𝑁))
14		gg-dvfsumle.a	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ))
15		cncff 24646	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ)
16	14, 15	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ)
17		eqid 2731	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) = (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴)
18	17	fmpt 7111	. . . . . . . . 9 ⊢ (∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ ↔ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ)
19	16, 18	sylibr 233	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ)
20		nfcsb1v 3918	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐴
21	20	nfel1 2918	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ
22		csbeq1a 3907	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → 𝐴 = ⦋𝑦 / 𝑥⦌𝐴)
23	22	eleq1d 2817	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ ℝ ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ))
24	21, 23	rspc 3600	. . . . . . . 8 ⊢ (𝑦 ∈ (𝑀[,]𝑁) → (∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ))
25	19, 24	mpan9 506	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀[,]𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ)
26	13, 25	syldan 590	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀...𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ)
27	26	ralrimiva 3145	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ (𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ)
28		fzofzp1 13736	. . . . 5 ⊢ (𝑘 ∈ (𝑀..^𝑁) → (𝑘 + 1) ∈ (𝑀...𝑁))
29		csbeq1 3896	. . . . . . 7 ⊢ (𝑦 = (𝑘 + 1) → ⦋𝑦 / 𝑥⦌𝐴 = ⦋(𝑘 + 1) / 𝑥⦌𝐴)
30	29	eleq1d 2817	. . . . . 6 ⊢ (𝑦 = (𝑘 + 1) → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℝ))
31	30	rspccva 3611	. . . . 5 ⊢ ((∀𝑦 ∈ (𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℝ)
32	27, 28, 31	syl2an 595	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℝ)
33		elfzofz 13655	. . . . 5 ⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ (𝑀...𝑁))
34		csbeq1 3896	. . . . . . 7 ⊢ (𝑦 = 𝑘 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑘 / 𝑥⦌𝐴)
35	34	eleq1d 2817	. . . . . 6 ⊢ (𝑦 = 𝑘 → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ ⦋𝑘 / 𝑥⦌𝐴 ∈ ℝ))
36	35	rspccva 3611	. . . . 5 ⊢ ((∀𝑦 ∈ (𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ∧ 𝑘 ∈ (𝑀...𝑁)) → ⦋𝑘 / 𝑥⦌𝐴 ∈ ℝ)
37	27, 33, 36	syl2an 595	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ⦋𝑘 / 𝑥⦌𝐴 ∈ ℝ)
38	32, 37	resubcld 11649	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴) ∈ ℝ)
39		elfzoelz 13639	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ ℤ)
40	39	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℤ)
41	40	zred 12673	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℝ)
42	41	recnd 11249	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℂ)
43		ax-1cn 11174	. . . . . . 7 ⊢ 1 ∈ ℂ
44		pncan2 11474	. . . . . . 7 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 𝑘) = 1)
45	42, 43, 44	sylancl 585	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑘 + 1) − 𝑘) = 1)
46	45	oveq2d 7428	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · ((𝑘 + 1) − 𝑘)) = (𝑋 · 1))
47	3	recnd 11249	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℂ)
48		peano2re 11394	. . . . . . . 8 ⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
49	41, 48	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ ℝ)
50	49	recnd 11249	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ ℂ)
51	47, 50, 42	subdid 11677	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · ((𝑘 + 1) − 𝑘)) = ((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘)))
52	47	mulridd 11238	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · 1) = 𝑋)
53	46, 51, 52	3eqtr3d 2779	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘)) = 𝑋)
54	47	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘[,](𝑘 + 1))) → 𝑋 ∈ ℂ)
55	41, 49	iccssred 13418	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ ℝ)
56		ax-resscn 11173	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
57	55, 56	sstrdi 3994	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ ℂ)
58	57	sselda 3982	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘[,](𝑘 + 1))) → 𝑦 ∈ ℂ)
59		ovmpot 7572	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) = (𝑋 · 𝑦))
60	54, 58, 59	syl2anc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘[,](𝑘 + 1))) → (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) = (𝑋 · 𝑦))
61	60	eqeq2d 2742	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘[,](𝑘 + 1))) → (𝑧 = (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ↔ 𝑧 = (𝑋 · 𝑦)))
62	61	pm5.32da 578	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑦 ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑧 = (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ↔ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑧 = (𝑋 · 𝑦))))
63	62	opabbidv 5214	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑧 = (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑧 = (𝑋 · 𝑦))})
64		df-mpt 5232	. . . . . . 7 ⊢ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ (𝑋 · 𝑦)) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑧 = (𝑋 · 𝑦))}
65	63, 64	eqtr4di 2789	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑧 = (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ (𝑋 · 𝑦)))
66		df-mpt 5232	. . . . . . 7 ⊢ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑧 = (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))}
67		eqid 2731	. . . . . . . 8 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
68	67	mpomulcn 24618	. . . . . . . 8 ⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
69	56	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ℝ ⊆ ℂ)
70		cncfmptc 24665	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℝ ∧ (𝑘[,](𝑘 + 1)) ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝑋) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
71	3, 57, 69, 70	syl3anc 1370	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝑋) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
72		cncfmptid 24666	. . . . . . . . 9 ⊢ (((𝑘[,](𝑘 + 1)) ⊆ ℝ ∧ ℝ ⊆ ℂ) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝑦) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
73	55, 56, 72	sylancl 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝑦) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
74		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑋 ∈ ℝ)
75	74	recnd 11249	. . . . . . . . . 10 ⊢ ((𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑋 ∈ ℂ)
76		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
77	76	recnd 11249	. . . . . . . . . 10 ⊢ ((𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
78	59	eqcomd 2737	. . . . . . . . . 10 ⊢ ((𝑋 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑋 · 𝑦) = (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))
79	75, 77, 78	syl2anc 583	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑋 · 𝑦) = (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))
80		remulcl 11201	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑋 · 𝑦) ∈ ℝ)
81	79, 80	eqeltrrd 2833	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ∈ ℝ)
82	67, 68, 71, 73, 56, 81	cncfmpt2ss 24669	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
83	66, 82	eqeltrrid 2837	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑧 = (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
84	65, 83	eqeltrrd 2833	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ (𝑋 · 𝑦)) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
85		reelprrecn 11208	. . . . . . . 8 ⊢ ℝ ∈ {ℝ, ℂ}
86	85	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ℝ ∈ {ℝ, ℂ})
87	6	zred 12673	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℝ)
88	87	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ)
89	88	rexrd 11271	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ^*)
90		elfzole1 13647	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝑘)
91	90	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ≤ 𝑘)
92		iooss1 13366	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℝ^* ∧ 𝑀 ≤ 𝑘) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1)))
93	89, 91, 92	syl2anc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1)))
94	8	zred 12673	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℝ)
95	94	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈ ℝ)
96	95	rexrd 11271	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈ ℝ^*)
97	28	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁))
98		elfzle2 13512	. . . . . . . . . . . 12 ⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → (𝑘 + 1) ≤ 𝑁)
99	97, 98	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ≤ 𝑁)
100		iooss2 13367	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ^* ∧ (𝑘 + 1) ≤ 𝑁) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁))
101	96, 99, 100	syl2anc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁))
102	93, 101	sstrd 3992	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁))
103		ioossicc 13417	. . . . . . . . . 10 ⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁)
104	87, 94	iccssred 13418	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ)
105	104	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀[,]𝑁) ⊆ ℝ)
106	105, 56	sstrdi 3994	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀[,]𝑁) ⊆ ℂ)
107	103, 106	sstrid 3993	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)𝑁) ⊆ ℂ)
108	102, 107	sstrd 3992	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ ℂ)
109	108	sselda 3982	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘(,)(𝑘 + 1))) → 𝑦 ∈ ℂ)
110		1cnd 11216	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘(,)(𝑘 + 1))) → 1 ∈ ℂ)
111	69	sselda 3982	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
112		1cnd 11216	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ ℝ) → 1 ∈ ℂ)
113	86	dvmptid 25722	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1))
114		ioossre 13392	. . . . . . . . 9 ⊢ (𝑘(,)(𝑘 + 1)) ⊆ ℝ
115	114	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ ℝ)
116	67	tgioo2 24552	. . . . . . . 8 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
117		iooretop 24515	. . . . . . . . 9 ⊢ (𝑘(,)(𝑘 + 1)) ∈ (topGen‘ran (,))
118	117	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ∈ (topGen‘ran (,)))
119	86, 111, 112, 113, 115, 116, 67, 118	dvmptres 25728	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ 𝑦)) = (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ 1))
120	86, 109, 110, 119, 47	dvmptcmul 25729	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 · 𝑦))) = (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 · 1)))
121	52	mpteq2dv 5250	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 · 1)) = (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ 𝑋))
122	120, 121	eqtrd 2771	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 · 𝑦))) = (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ 𝑋))
123		nfcv 2902	. . . . . . 7 ⊢ Ⅎ𝑦𝐴
124	123, 20, 22	cbvmpt 5259	. . . . . 6 ⊢ (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝐴) = (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ ⦋𝑦 / 𝑥⦌𝐴)
125		iccss 13399	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ (𝑀 ≤ 𝑘 ∧ (𝑘 + 1) ≤ 𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁))
126	88, 95, 91, 99, 125	syl22anc 836	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁))
127	126	resmptd 6040	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ↾ (𝑘[,](𝑘 + 1))) = (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝐴))
128	14	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ))
129		rescncf 24650	. . . . . . . 8 ⊢ ((𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ↾ (𝑘[,](𝑘 + 1))) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ)))
130	126, 128, 129	sylc 65	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ↾ (𝑘[,](𝑘 + 1))) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
131	127, 130	eqeltrrd 2833	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝐴) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
132	124, 131	eqeltrrid 2837	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ ⦋𝑦 / 𝑥⦌𝐴) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
133	16	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ)
134	133, 18	sylibr 233	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ)
135	103	sseli 3978	. . . . . . . 8 ⊢ (𝑦 ∈ (𝑀(,)𝑁) → 𝑦 ∈ (𝑀[,]𝑁))
136	24	impcom 407	. . . . . . . 8 ⊢ ((∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ ∧ 𝑦 ∈ (𝑀[,]𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ)
137	134, 135, 136	syl2an 595	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑀(,)𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ)
138	137	recnd 11249	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑀(,)𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ)
139	103	sseli 3978	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑀(,)𝑁) → 𝑥 ∈ (𝑀[,]𝑁))
140	16	fvmptelcdm 7114	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℝ)
141	140	adantlr 712	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℝ)
142	139, 141	sylan2 592	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℝ)
143	142	fmpttd 7116	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)⟶ℝ)
144		ioossre 13392	. . . . . . . . . 10 ⊢ (𝑀(,)𝑁) ⊆ ℝ
145		dvfre 25716	. . . . . . . . . 10 ⊢ (((𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)⟶ℝ ∧ (𝑀(,)𝑁) ⊆ ℝ) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ)
146	143, 144, 145	sylancl 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ)
147		gg-dvfsumle.b	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵))
148	147	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵))
149	148	dmeqd 5905	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵))
150		gg-dvfsumle.v	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉)
151	150	adantlr 712	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉)
152	151	ralrimiva 3145	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ 𝑉)
153		dmmptg 6241	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ 𝑉 → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑀(,)𝑁))
154	152, 153	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑀(,)𝑁))
155	149, 154	eqtrd 2771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑀(,)𝑁))
156	148, 155	feq12d 6705	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ))
157	146, 156	mpbid 231	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ)
158		eqid 2731	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)
159	158	fmpt 7111	. . . . . . . 8 ⊢ (∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ ℝ ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ)
160	157, 159	sylibr 233	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ ℝ)
161		nfcsb1v 3918	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵
162	161	nfel1 2918	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ
163		csbeq1a 3907	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵)
164	163	eleq1d 2817	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝐵 ∈ ℝ ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ))
165	162, 164	rspc 3600	. . . . . . 7 ⊢ (𝑦 ∈ (𝑀(,)𝑁) → (∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ ℝ → ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ))
166	160, 165	mpan9 506	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑀(,)𝑁)) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ)
167	123, 20, 22	cbvmpt 5259	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴) = (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / 𝑥⦌𝐴)
168	167	oveq2i 7423	. . . . . . 7 ⊢ (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (ℝ D (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / 𝑥⦌𝐴))
169		nfcv 2902	. . . . . . . 8 ⊢ Ⅎ𝑦𝐵
170	169, 161, 163	cbvmpt 5259	. . . . . . 7 ⊢ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / 𝑥⦌𝐵)
171	148, 168, 170	3eqtr3g 2794	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / 𝑥⦌𝐴)) = (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / 𝑥⦌𝐵))
172	86, 138, 166, 171, 102, 116, 67, 118	dvmptres 25728	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ ⦋𝑦 / 𝑥⦌𝐴)) = (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ ⦋𝑦 / 𝑥⦌𝐵))
173		gg-dvfsumle.l	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → 𝑋 ≤ 𝐵)
174	173	anassrs 467	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → 𝑋 ≤ 𝐵)
175	174	ralrimiva 3145	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑘(,)(𝑘 + 1))𝑋 ≤ 𝐵)
176		nfcv 2902	. . . . . . . 8 ⊢ Ⅎ𝑥𝑋
177		nfcv 2902	. . . . . . . 8 ⊢ Ⅎ𝑥 ≤
178	176, 177, 161	nfbr 5195	. . . . . . 7 ⊢ Ⅎ𝑥 𝑋 ≤ ⦋𝑦 / 𝑥⦌𝐵
179	163	breq2d 5160	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑋 ≤ 𝐵 ↔ 𝑋 ≤ ⦋𝑦 / 𝑥⦌𝐵))
180	178, 179	rspc 3600	. . . . . 6 ⊢ (𝑦 ∈ (𝑘(,)(𝑘 + 1)) → (∀𝑥 ∈ (𝑘(,)(𝑘 + 1))𝑋 ≤ 𝐵 → 𝑋 ≤ ⦋𝑦 / 𝑥⦌𝐵))
181	175, 180	mpan9 506	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘(,)(𝑘 + 1))) → 𝑋 ≤ ⦋𝑦 / 𝑥⦌𝐵)
182	41	rexrd 11271	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℝ^*)
183	49	rexrd 11271	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ ℝ^*)
184	41	lep1d 12152	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ≤ (𝑘 + 1))
185		lbicc2 13448	. . . . . 6 ⊢ ((𝑘 ∈ ℝ^* ∧ (𝑘 + 1) ∈ ℝ^* ∧ 𝑘 ≤ (𝑘 + 1)) → 𝑘 ∈ (𝑘[,](𝑘 + 1)))
186	182, 183, 184, 185	syl3anc 1370	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ (𝑘[,](𝑘 + 1)))
187		ubicc2 13449	. . . . . 6 ⊢ ((𝑘 ∈ ℝ^* ∧ (𝑘 + 1) ∈ ℝ^* ∧ 𝑘 ≤ (𝑘 + 1)) → (𝑘 + 1) ∈ (𝑘[,](𝑘 + 1)))
188	182, 183, 184, 187	syl3anc 1370	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑘[,](𝑘 + 1)))
189		oveq2 7420	. . . . 5 ⊢ (𝑦 = 𝑘 → (𝑋 · 𝑦) = (𝑋 · 𝑘))
190		oveq2 7420	. . . . 5 ⊢ (𝑦 = (𝑘 + 1) → (𝑋 · 𝑦) = (𝑋 · (𝑘 + 1)))
191	41, 49, 84, 122, 132, 172, 181, 186, 188, 184, 189, 34, 190, 29	dvle 25773	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘)) ≤ (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))
192	53, 191	eqbrtrrd 5172	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ≤ (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))
193	2, 3, 38, 192	fsumle 15752	. 2 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ Σ𝑘 ∈ (𝑀..^𝑁)(⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))
194		vex 3477	. . . . 5 ⊢ 𝑦 ∈ V
195	194	a1i 11	. . . 4 ⊢ (𝑦 = 𝑀 → 𝑦 ∈ V)
196		eqeq2 2743	. . . . . 6 ⊢ (𝑦 = 𝑀 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑀))
197	196	biimpa 476	. . . . 5 ⊢ ((𝑦 = 𝑀 ∧ 𝑥 = 𝑦) → 𝑥 = 𝑀)
198		gg-dvfsumle.c	. . . . 5 ⊢ (𝑥 = 𝑀 → 𝐴 = 𝐶)
199	197, 198	syl 17	. . . 4 ⊢ ((𝑦 = 𝑀 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐶)
200	195, 199	csbied 3931	. . 3 ⊢ (𝑦 = 𝑀 → ⦋𝑦 / 𝑥⦌𝐴 = 𝐶)
201	194	a1i 11	. . . 4 ⊢ (𝑦 = 𝑁 → 𝑦 ∈ V)
202		eqeq2 2743	. . . . . 6 ⊢ (𝑦 = 𝑁 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑁))
203	202	biimpa 476	. . . . 5 ⊢ ((𝑦 = 𝑁 ∧ 𝑥 = 𝑦) → 𝑥 = 𝑁)
204		gg-dvfsumle.d	. . . . 5 ⊢ (𝑥 = 𝑁 → 𝐴 = 𝐷)
205	203, 204	syl 17	. . . 4 ⊢ ((𝑦 = 𝑁 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐷)
206	201, 205	csbied 3931	. . 3 ⊢ (𝑦 = 𝑁 → ⦋𝑦 / 𝑥⦌𝐴 = 𝐷)
207	26	recnd 11249	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀...𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ)
208	34, 29, 200, 206, 4, 207	telfsumo2 15756	. 2 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴) = (𝐷 − 𝐶))
209	193, 208	breqtrd 5174	1 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ (𝐷 − 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2105 ∀wral 3060 Vcvv 3473 ⦋csb 3893 ∩ cin 3947 ⊆ wss 3948 {cpr 4630 class class class wbr 5148 {copab 5210 ↦ cmpt 5231 dom cdm 5676 ran crn 5677 ↾ cres 5678 ⟶wf 6539 ‘cfv 6543 (class class class)co 7412 ∈ cmpo 7414 Fincfn 8945 ℂcc 11114 ℝcr 11115 1c1 11117 + caddc 11119 · cmul 11121 ℝ^*cxr 11254 ≤ cle 11256 − cmin 11451 ℤcz 12565 ℤ_≥cuz 12829 (,)cioo 13331 [,]cicc 13334 ...cfz 13491 ..^cfzo 13634 Σcsu 15639 TopOpenctopn 17374 topGenctg 17390 ℂ_fldccnfld 21148 –cn→ccncf 24629 D cdv 25625

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729 ax-inf2 9642 ax-cnex 11172 ax-resscn 11173 ax-1cn 11174 ax-icn 11175 ax-addcl 11176 ax-addrcl 11177 ax-mulcl 11178 ax-mulrcl 11179 ax-mulcom 11180 ax-addass 11181 ax-mulass 11182 ax-distr 11183 ax-i2m1 11184 ax-1ne0 11185 ax-1rid 11186 ax-rnegex 11187 ax-rrecex 11188 ax-cnre 11189 ax-pre-lttri 11190 ax-pre-lttrn 11191 ax-pre-ltadd 11192 ax-pre-mulgt0 11193 ax-pre-sup 11194 ax-addf 11195

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7674 df-om 7860 df-1st 7979 df-2nd 7980 df-supp 8152 df-frecs 8272 df-wrecs 8303 df-recs 8377 df-rdg 8416 df-1o 8472 df-2o 8473 df-er 8709 df-map 8828 df-pm 8829 df-ixp 8898 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-fsupp 9368 df-fi 9412 df-sup 9443 df-inf 9444 df-oi 9511 df-card 9940 df-pnf 11257 df-mnf 11258 df-xr 11259 df-ltxr 11260 df-le 11261 df-sub 11453 df-neg 11454 df-div 11879 df-nn 12220 df-2 12282 df-3 12283 df-4 12284 df-5 12285 df-6 12286 df-7 12287 df-8 12288 df-9 12289 df-n0 12480 df-z 12566 df-dec 12685 df-uz 12830 df-q 12940 df-rp 12982 df-xneg 13099 df-xadd 13100 df-xmul 13101 df-ioo 13335 df-ico 13337 df-icc 13338 df-fz 13492 df-fzo 13635 df-seq 13974 df-exp 14035 df-hash 14298 df-cj 15053 df-re 15054 df-im 15055 df-sqrt 15189 df-abs 15190 df-clim 15439 df-sum 15640 df-struct 17087 df-sets 17104 df-slot 17122 df-ndx 17134 df-base 17152 df-ress 17181 df-plusg 17217 df-mulr 17218 df-starv 17219 df-sca 17220 df-vsca 17221 df-ip 17222 df-tset 17223 df-ple 17224 df-ds 17226 df-unif 17227 df-hom 17228 df-cco 17229 df-rest 17375 df-topn 17376 df-0g 17394 df-gsum 17395 df-topgen 17396 df-pt 17397 df-prds 17400 df-xrs 17455 df-qtop 17460 df-imas 17461 df-xps 17463 df-mre 17537 df-mrc 17538 df-acs 17540 df-mgm 18568 df-sgrp 18647 df-mnd 18663 df-submnd 18709 df-mulg 18991 df-cntz 19226 df-cmn 19695 df-psmet 21140 df-xmet 21141 df-met 21142 df-bl 21143 df-mopn 21144 df-fbas 21145 df-fg 21146 df-cnfld 21149 df-top 22629 df-topon 22646 df-topsp 22668 df-bases 22682 df-cld 22756 df-ntr 22757 df-cls 22758 df-nei 22835 df-lp 22873 df-perf 22874 df-cn 22964 df-cnp 22965 df-haus 23052 df-cmp 23124 df-tx 23299 df-hmeo 23492 df-fil 23583 df-fm 23675 df-flim 23676 df-flf 23677 df-xms 24059 df-ms 24060 df-tms 24061 df-cncf 24631 df-limc 25628 df-dv 25629

This theorem is referenced by: (None)

W3C validator