dvfsumle - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dvfsumle		Structured version Visualization version GIF version

Theorem dvfsumle 26013

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

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

**Assertion**
Ref	Expression
dvfsumle	⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ (𝐷 − 𝐶))

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

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

Step	Hyp	Ref	Expression
1		fzofi 13934	. . . 4 ⊢ (𝑀..^𝑁) ∈ Fin
2	1	a1i 11	. . 3 ⊢ (𝜑 → (𝑀..^𝑁) ∈ Fin)
3		dvfsumle.x	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℝ)
4		dvfsumle.m	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
5		eluzel2 12791	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
6	4, 5	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℤ)
7		eluzelz 12796	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ ℤ)
8	4, 7	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
9		fzval2 13462	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ))
10	6, 8, 9	syl2anc 590	. . . . . . . . 9 ⊢ (𝜑 → (𝑀...𝑁) = ((𝑀[,]𝑁) ∩ ℤ))
11		inss1 4172	. . . . . . . . 9 ⊢ ((𝑀[,]𝑁) ∩ ℤ) ⊆ (𝑀[,]𝑁)
12	10, 11	eqsstrdi 3966	. . . . . . . 8 ⊢ (𝜑 → (𝑀...𝑁) ⊆ (𝑀[,]𝑁))
13	12	sselda 3922	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀...𝑁)) → 𝑦 ∈ (𝑀[,]𝑁))
14		dvfsumle.a	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ))
15		cncff 24885	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ)
16	14, 15	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ)
17		eqid 2740	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) = (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴)
18	17	fmpt 7058	. . . . . . . . 9 ⊢ (∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ ↔ (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ)
19	16, 18	sylibr 235	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ)
20		nfcsb1v 3862	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐴
21	20	nfel1 2918	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ
22		csbeq1a 3852	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → 𝐴 = ⦋𝑦 / 𝑥⦌𝐴)
23	22	eleq1d 2825	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐴 ∈ ℝ ↔ ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ))
24	21, 23	rspc 3555	. . . . . . . 8 ⊢ (𝑦 ∈ (𝑀[,]𝑁) → (∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ))
25	19, 24	mpan9 511	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀[,]𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ)
26	13, 25	syldan 597	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀...𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ)
27	26	ralrimiva 3132	. . . . 5 ⊢ (𝜑 → ∀𝑦 ∈ (𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ)
28		fzofzp1 13717	. . . . 5 ⊢ (𝑘 ∈ (𝑀..^𝑁) → (𝑘 + 1) ∈ (𝑀...𝑁))
29		csbeq1 3841	. . . . . . 7 ⊢ (𝑦 = (𝑘 + 1) → ⦋𝑦 / 𝑥⦌𝐴 = ⦋(𝑘 + 1) / 𝑥⦌𝐴)
30	29	eleq1d 2825	. . . . . 6 ⊢ (𝑦 = (𝑘 + 1) → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℝ))
31	30	rspccva 3566	. . . . 5 ⊢ ((∀𝑦 ∈ (𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ∧ (𝑘 + 1) ∈ (𝑀...𝑁)) → ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℝ)
32	27, 28, 31	syl2an 602	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ⦋(𝑘 + 1) / 𝑥⦌𝐴 ∈ ℝ)
33		elfzofz 13628	. . . . 5 ⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ (𝑀...𝑁))
34		csbeq1 3841	. . . . . . 7 ⊢ (𝑦 = 𝑘 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑘 / 𝑥⦌𝐴)
35	34	eleq1d 2825	. . . . . 6 ⊢ (𝑦 = 𝑘 → (⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ↔ ⦋𝑘 / 𝑥⦌𝐴 ∈ ℝ))
36	35	rspccva 3566	. . . . 5 ⊢ ((∀𝑦 ∈ (𝑀...𝑁)⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ ∧ 𝑘 ∈ (𝑀...𝑁)) → ⦋𝑘 / 𝑥⦌𝐴 ∈ ℝ)
37	27, 33, 36	syl2an 602	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ⦋𝑘 / 𝑥⦌𝐴 ∈ ℝ)
38	32, 37	resubcld 11576	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴) ∈ ℝ)
39		elfzoelz 13611	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ ℤ)
40	39	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℤ)
41	40	zred 12631	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℝ)
42	41	recnd 11171	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℂ)
43		ax-1cn 11094	. . . . . . 7 ⊢ 1 ∈ ℂ
44		pncan2 11398	. . . . . . 7 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 𝑘) = 1)
45	42, 43, 44	sylancl 592	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑘 + 1) − 𝑘) = 1)
46	45	oveq2d 7379	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · ((𝑘 + 1) − 𝑘)) = (𝑋 · 1))
47	3	recnd 11171	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ∈ ℂ)
48		peano2re 11317	. . . . . . . 8 ⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
49	41, 48	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ ℝ)
50	49	recnd 11171	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ ℂ)
51	47, 50, 42	subdid 11604	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · ((𝑘 + 1) − 𝑘)) = ((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘)))
52	47	mulridd 11160	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑋 · 1) = 𝑋)
53	46, 51, 52	3eqtr3d 2783	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘)) = 𝑋)
54	47	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘[,](𝑘 + 1))) → 𝑋 ∈ ℂ)
55	41, 49	iccssred 13385	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ ℝ)
56		ax-resscn 11093	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
57	55, 56	sstrdi 3934	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ ℂ)
58	57	sselda 3922	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘[,](𝑘 + 1))) → 𝑦 ∈ ℂ)
59		ovmpot 7524	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) = (𝑋 · 𝑦))
60	54, 58, 59	syl2anc 590	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘[,](𝑘 + 1))) → (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) = (𝑋 · 𝑦))
61	60	eqeq2d 2751	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘[,](𝑘 + 1))) → (𝑧 = (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ↔ 𝑧 = (𝑋 · 𝑦)))
62	61	pm5.32da 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑦 ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑧 = (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ↔ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑧 = (𝑋 · 𝑦))))
63	62	opabbidv 5145	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑧 = (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑧 = (𝑋 · 𝑦))})
64		df-mpt 5161	. . . . . . 7 ⊢ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ (𝑋 · 𝑦)) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑧 = (𝑋 · 𝑦))}
65	63, 64	eqtr4di 2793	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑧 = (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} = (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ (𝑋 · 𝑦)))
66		df-mpt 5161	. . . . . . 7 ⊢ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑧 = (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))}
67		eqid 2740	. . . . . . . 8 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
68	67	mpomulcn 24859	. . . . . . . 8 ⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
69	56	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ℝ ⊆ ℂ)
70		cncfmptc 24904	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℝ ∧ (𝑘[,](𝑘 + 1)) ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝑋) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
71	3, 57, 69, 70	syl3anc 1379	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝑋) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
72		cncfmptid 24905	. . . . . . . . 9 ⊢ (((𝑘[,](𝑘 + 1)) ⊆ ℝ ∧ ℝ ⊆ ℂ) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝑦) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
73	55, 56, 72	sylancl 592	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝑦) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
74		simpl 483	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑋 ∈ ℝ)
75	74	recnd 11171	. . . . . . . . . 10 ⊢ ((𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑋 ∈ ℂ)
76		simpr 485	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
77	76	recnd 11171	. . . . . . . . . 10 ⊢ ((𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
78	59	eqcomd 2746	. . . . . . . . . 10 ⊢ ((𝑋 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑋 · 𝑦) = (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))
79	75, 77, 78	syl2anc 590	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑋 · 𝑦) = (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))
80		remulcl 11121	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑋 · 𝑦) ∈ ℝ)
81	79, 80	eqeltrrd 2841	. . . . . . . 8 ⊢ ((𝑋 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦) ∈ ℝ)
82	67, 68, 71, 73, 56, 81	cncfmpt2ss 24908	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦)) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
83	66, 82	eqeltrrid 2845	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ (𝑘[,](𝑘 + 1)) ∧ 𝑧 = (𝑋(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))𝑦))} ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
84	65, 83	eqeltrrd 2841	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ (𝑋 · 𝑦)) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
85		reelprrecn 11128	. . . . . . . 8 ⊢ ℝ ∈ {ℝ, ℂ}
86	85	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ℝ ∈ {ℝ, ℂ})
87	6	zred 12631	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℝ)
88	87	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ)
89	88	rexrd 11193	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ^*)
90		elfzole1 13620	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝑘)
91	90	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑀 ≤ 𝑘)
92		iooss1 13331	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℝ^* ∧ 𝑀 ≤ 𝑘) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1)))
93	89, 91, 92	syl2anc 590	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)(𝑘 + 1)))
94	8	zred 12631	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℝ)
95	94	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈ ℝ)
96	95	rexrd 11193	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑁 ∈ ℝ^*)
97	28	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑀...𝑁))
98		elfzle2 13480	. . . . . . . . . . . 12 ⊢ ((𝑘 + 1) ∈ (𝑀...𝑁) → (𝑘 + 1) ≤ 𝑁)
99	97, 98	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ≤ 𝑁)
100		iooss2 13332	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℝ^* ∧ (𝑘 + 1) ≤ 𝑁) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁))
101	96, 99, 100	syl2anc 590	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁))
102	93, 101	sstrd 3932	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ (𝑀(,)𝑁))
103		ioossicc 13384	. . . . . . . . . 10 ⊢ (𝑀(,)𝑁) ⊆ (𝑀[,]𝑁)
104	87, 94	iccssred 13385	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀[,]𝑁) ⊆ ℝ)
105	104	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀[,]𝑁) ⊆ ℝ)
106	105, 56	sstrdi 3934	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀[,]𝑁) ⊆ ℂ)
107	103, 106	sstrid 3933	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑀(,)𝑁) ⊆ ℂ)
108	102, 107	sstrd 3932	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ ℂ)
109	108	sselda 3922	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘(,)(𝑘 + 1))) → 𝑦 ∈ ℂ)
110		1cnd 11137	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘(,)(𝑘 + 1))) → 1 ∈ ℂ)
111	69	sselda 3922	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
112		1cnd 11137	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ ℝ) → 1 ∈ ℂ)
113	86	dvmptid 25949	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ ℝ ↦ 𝑦)) = (𝑦 ∈ ℝ ↦ 1))
114		ioossre 13358	. . . . . . . . 9 ⊢ (𝑘(,)(𝑘 + 1)) ⊆ ℝ
115	114	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ⊆ ℝ)
116		tgioo4 24795	. . . . . . . 8 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
117		iooretop 24755	. . . . . . . . 9 ⊢ (𝑘(,)(𝑘 + 1)) ∈ (topGen‘ran (,))
118	117	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘(,)(𝑘 + 1)) ∈ (topGen‘ran (,)))
119	86, 111, 112, 113, 115, 116, 67, 118	dvmptres 25955	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ 𝑦)) = (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ 1))
120	86, 109, 110, 119, 47	dvmptcmul 25956	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 · 𝑦))) = (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 · 1)))
121	52	mpteq2dv 5173	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 · 1)) = (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ 𝑋))
122	120, 121	eqtrd 2775	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ (𝑋 · 𝑦))) = (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ 𝑋))
123		nfcv 2902	. . . . . . 7 ⊢ Ⅎ𝑦𝐴
124	123, 20, 22	cbvmpt 5181	. . . . . 6 ⊢ (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝐴) = (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ ⦋𝑦 / 𝑥⦌𝐴)
125		iccss 13365	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ (𝑀 ≤ 𝑘 ∧ (𝑘 + 1) ≤ 𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁))
126	88, 95, 91, 99, 125	syl22anc 844	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁))
127	126	resmptd 5999	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ↾ (𝑘[,](𝑘 + 1))) = (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝐴))
128	14	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ))
129		rescncf 24889	. . . . . . . 8 ⊢ ((𝑘[,](𝑘 + 1)) ⊆ (𝑀[,]𝑁) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ∈ ((𝑀[,]𝑁)–cn→ℝ) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ↾ (𝑘[,](𝑘 + 1))) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ)))
130	126, 128, 129	sylc 65	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴) ↾ (𝑘[,](𝑘 + 1))) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
131	127, 130	eqeltrrd 2841	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑘[,](𝑘 + 1)) ↦ 𝐴) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
132	124, 131	eqeltrrid 2845	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑦 ∈ (𝑘[,](𝑘 + 1)) ↦ ⦋𝑦 / 𝑥⦌𝐴) ∈ ((𝑘[,](𝑘 + 1))–cn→ℝ))
133	16	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀[,]𝑁) ↦ 𝐴):(𝑀[,]𝑁)⟶ℝ)
134	133, 18	sylibr 235	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ)
135	103	sseli 3918	. . . . . . . 8 ⊢ (𝑦 ∈ (𝑀(,)𝑁) → 𝑦 ∈ (𝑀[,]𝑁))
136	24	impcom 408	. . . . . . . 8 ⊢ ((∀𝑥 ∈ (𝑀[,]𝑁)𝐴 ∈ ℝ ∧ 𝑦 ∈ (𝑀[,]𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ)
137	134, 135, 136	syl2an 602	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑀(,)𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℝ)
138	137	recnd 11171	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑀(,)𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ)
139	103	sseli 3918	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑀(,)𝑁) → 𝑥 ∈ (𝑀[,]𝑁))
140	16	fvmptelcdm 7061	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℝ)
141	140	adantlr 721	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀[,]𝑁)) → 𝐴 ∈ ℝ)
142	139, 141	sylan2 599	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐴 ∈ ℝ)
143	142	fmpttd 7063	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)⟶ℝ)
144		ioossre 13358	. . . . . . . . . 10 ⊢ (𝑀(,)𝑁) ⊆ ℝ
145		dvfre 25943	. . . . . . . . . 10 ⊢ (((𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴):(𝑀(,)𝑁)⟶ℝ ∧ (𝑀(,)𝑁) ⊆ ℝ) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ)
146	143, 144, 145	sylancl 592	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ)
147		dvfsumle.b	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵))
148	147	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵))
149	148	dmeqd 5854	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵))
150		dvfsumle.v	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉)
151	150	adantlr 721	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑀(,)𝑁)) → 𝐵 ∈ 𝑉)
152	151	ralrimiva 3132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ 𝑉)
153		dmmptg 6200	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ 𝑉 → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑀(,)𝑁))
154	152, 153	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑀(,)𝑁))
155	149, 154	eqtrd 2775	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (𝑀(,)𝑁))
156	148, 155	feq12d 6650	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)):dom (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴))⟶ℝ ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ))
157	146, 156	mpbid 233	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ)
158		eqid 2740	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵)
159	158	fmpt 7058	. . . . . . . 8 ⊢ (∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ ℝ ↔ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵):(𝑀(,)𝑁)⟶ℝ)
160	157, 159	sylibr 235	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ ℝ)
161		nfcsb1v 3862	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵
162	161	nfel1 2918	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ
163		csbeq1a 3852	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵)
164	163	eleq1d 2825	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝐵 ∈ ℝ ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ))
165	162, 164	rspc 3555	. . . . . . 7 ⊢ (𝑦 ∈ (𝑀(,)𝑁) → (∀𝑥 ∈ (𝑀(,)𝑁)𝐵 ∈ ℝ → ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ))
166	160, 165	mpan9 511	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑀(,)𝑁)) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ℝ)
167	123, 20, 22	cbvmpt 5181	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴) = (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / 𝑥⦌𝐴)
168	167	oveq2i 7374	. . . . . . 7 ⊢ (ℝ D (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐴)) = (ℝ D (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / 𝑥⦌𝐴))
169		nfcv 2902	. . . . . . . 8 ⊢ Ⅎ𝑦𝐵
170	169, 161, 163	cbvmpt 5181	. . . . . . 7 ⊢ (𝑥 ∈ (𝑀(,)𝑁) ↦ 𝐵) = (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / 𝑥⦌𝐵)
171	148, 168, 170	3eqtr3g 2798	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / 𝑥⦌𝐴)) = (𝑦 ∈ (𝑀(,)𝑁) ↦ ⦋𝑦 / 𝑥⦌𝐵))
172	86, 138, 166, 171, 102, 116, 67, 118	dvmptres 25955	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (ℝ D (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ ⦋𝑦 / 𝑥⦌𝐴)) = (𝑦 ∈ (𝑘(,)(𝑘 + 1)) ↦ ⦋𝑦 / 𝑥⦌𝐵))
173		dvfsumle.l	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑘 ∈ (𝑀..^𝑁) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1)))) → 𝑋 ≤ 𝐵)
174	173	anassrs 468	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑥 ∈ (𝑘(,)(𝑘 + 1))) → 𝑋 ≤ 𝐵)
175	174	ralrimiva 3132	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ∀𝑥 ∈ (𝑘(,)(𝑘 + 1))𝑋 ≤ 𝐵)
176		nfcv 2902	. . . . . . . 8 ⊢ Ⅎ𝑥𝑋
177		nfcv 2902	. . . . . . . 8 ⊢ Ⅎ𝑥 ≤
178	176, 177, 161	nfbr 5126	. . . . . . 7 ⊢ Ⅎ𝑥 𝑋 ≤ ⦋𝑦 / 𝑥⦌𝐵
179	163	breq2d 5091	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑋 ≤ 𝐵 ↔ 𝑋 ≤ ⦋𝑦 / 𝑥⦌𝐵))
180	178, 179	rspc 3555	. . . . . 6 ⊢ (𝑦 ∈ (𝑘(,)(𝑘 + 1)) → (∀𝑥 ∈ (𝑘(,)(𝑘 + 1))𝑋 ≤ 𝐵 → 𝑋 ≤ ⦋𝑦 / 𝑥⦌𝐵))
181	175, 180	mpan9 511	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) ∧ 𝑦 ∈ (𝑘(,)(𝑘 + 1))) → 𝑋 ≤ ⦋𝑦 / 𝑥⦌𝐵)
182	41	rexrd 11193	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℝ^*)
183	49	rexrd 11193	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ ℝ^*)
184	41	lep1d 12085	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ≤ (𝑘 + 1))
185		lbicc2 13415	. . . . . 6 ⊢ ((𝑘 ∈ ℝ^* ∧ (𝑘 + 1) ∈ ℝ^* ∧ 𝑘 ≤ (𝑘 + 1)) → 𝑘 ∈ (𝑘[,](𝑘 + 1)))
186	182, 183, 184, 185	syl3anc 1379	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ (𝑘[,](𝑘 + 1)))
187		ubicc2 13416	. . . . . 6 ⊢ ((𝑘 ∈ ℝ^* ∧ (𝑘 + 1) ∈ ℝ^* ∧ 𝑘 ≤ (𝑘 + 1)) → (𝑘 + 1) ∈ (𝑘[,](𝑘 + 1)))
188	182, 183, 184, 187	syl3anc 1379	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝑘 + 1) ∈ (𝑘[,](𝑘 + 1)))
189		oveq2 7371	. . . . 5 ⊢ (𝑦 = 𝑘 → (𝑋 · 𝑦) = (𝑋 · 𝑘))
190		oveq2 7371	. . . . 5 ⊢ (𝑦 = (𝑘 + 1) → (𝑋 · 𝑦) = (𝑋 · (𝑘 + 1)))
191	41, 49, 84, 122, 132, 172, 181, 186, 188, 184, 189, 34, 190, 29	dvle 25999	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝑋 · (𝑘 + 1)) − (𝑋 · 𝑘)) ≤ (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))
192	53, 191	eqbrtrrd 5103	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑋 ≤ (⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))
193	2, 3, 38, 192	fsumle 15760	. 2 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ Σ𝑘 ∈ (𝑀..^𝑁)(⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴))
194		vex 3436	. . . . 5 ⊢ 𝑦 ∈ V
195	194	a1i 11	. . . 4 ⊢ (𝑦 = 𝑀 → 𝑦 ∈ V)
196		eqeq2 2752	. . . . . 6 ⊢ (𝑦 = 𝑀 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑀))
197	196	biimpa 477	. . . . 5 ⊢ ((𝑦 = 𝑀 ∧ 𝑥 = 𝑦) → 𝑥 = 𝑀)
198		dvfsumle.c	. . . . 5 ⊢ (𝑥 = 𝑀 → 𝐴 = 𝐶)
199	197, 198	syl 17	. . . 4 ⊢ ((𝑦 = 𝑀 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐶)
200	195, 199	csbied 3874	. . 3 ⊢ (𝑦 = 𝑀 → ⦋𝑦 / 𝑥⦌𝐴 = 𝐶)
201	194	a1i 11	. . . 4 ⊢ (𝑦 = 𝑁 → 𝑦 ∈ V)
202		eqeq2 2752	. . . . . 6 ⊢ (𝑦 = 𝑁 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑁))
203	202	biimpa 477	. . . . 5 ⊢ ((𝑦 = 𝑁 ∧ 𝑥 = 𝑦) → 𝑥 = 𝑁)
204		dvfsumle.d	. . . . 5 ⊢ (𝑥 = 𝑁 → 𝐴 = 𝐷)
205	203, 204	syl 17	. . . 4 ⊢ ((𝑦 = 𝑁 ∧ 𝑥 = 𝑦) → 𝐴 = 𝐷)
206	201, 205	csbied 3874	. . 3 ⊢ (𝑦 = 𝑁 → ⦋𝑦 / 𝑥⦌𝐴 = 𝐷)
207	26	recnd 11171	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑀...𝑁)) → ⦋𝑦 / 𝑥⦌𝐴 ∈ ℂ)
208	34, 29, 200, 206, 4, 207	telfsumo2 15764	. 2 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(⦋(𝑘 + 1) / 𝑥⦌𝐴 − ⦋𝑘 / 𝑥⦌𝐴) = (𝐷 − 𝐶))
209	193, 208	breqtrd 5105	1 ⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)𝑋 ≤ (𝐷 − 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 = wceq 1547 ∈ wcel 2119 ∀wral 3054 Vcvv 3432 ⦋csb 3838 ∩ cin 3889 ⊆ wss 3890 {cpr 4564 class class class wbr 5079 {copab 5141 ↦ cmpt 5160 dom cdm 5625 ran crn 5626 ↾ cres 5627 ⟶wf 6488 ‘cfv 6492 (class class class)co 7363 ∈ cmpo 7365 Fincfn 8890 ℂcc 11034 ℝcr 11035 1c1 11037 + caddc 11039 · cmul 11041 ℝ^*cxr 11176 ≤ cle 11178 − cmin 11375 ℤcz 12522 ℤ_≥cuz 12786 (,)cioo 13296 [,]cicc 13299 ...cfz 13459 ..^cfzo 13606 Σcsu 15646 TopOpenctopn 17382 topGenctg 17398 ℂ_fldccnfld 21354 –cn→ccncf 24868 D cdv 25855

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-rep 5206 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 ax-un 7685 ax-inf2 9560 ax-cnex 11092 ax-resscn 11093 ax-1cn 11094 ax-icn 11095 ax-addcl 11096 ax-addrcl 11097 ax-mulcl 11098 ax-mulrcl 11099 ax-mulcom 11100 ax-addass 11101 ax-mulass 11102 ax-distr 11103 ax-i2m1 11104 ax-1ne0 11105 ax-1rid 11106 ax-rnegex 11107 ax-rrecex 11108 ax-cnre 11109 ax-pre-lttri 11110 ax-pre-lttrn 11111 ax-pre-ltadd 11112 ax-pre-mulgt0 11113 ax-pre-sup 11114 ax-addf 11115

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-nel 3040 df-ral 3055 df-rex 3065 df-rmo 3345 df-reu 3346 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4846 df-int 4885 df-iun 4930 df-iin 4931 df-br 5080 df-opab 5142 df-mpt 5161 df-tr 5187 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7320 df-ov 7366 df-oprab 7367 df-mpo 7368 df-of 7627 df-om 7814 df-1st 7938 df-2nd 7939 df-supp 8108 df-frecs 8228 df-wrecs 8259 df-recs 8308 df-rdg 8346 df-1o 8402 df-2o 8403 df-er 8640 df-map 8772 df-pm 8773 df-ixp 8843 df-en 8891 df-dom 8892 df-sdom 8893 df-fin 8894 df-fsupp 9272 df-fi 9321 df-sup 9352 df-inf 9353 df-oi 9422 df-card 9861 df-pnf 11179 df-mnf 11180 df-xr 11181 df-ltxr 11182 df-le 11183 df-sub 11377 df-neg 11378 df-div 11806 df-nn 12173 df-2 12242 df-3 12243 df-4 12244 df-5 12245 df-6 12246 df-7 12247 df-8 12248 df-9 12249 df-n0 12436 df-z 12523 df-dec 12643 df-uz 12787 df-q 12897 df-rp 12941 df-xneg 13061 df-xadd 13062 df-xmul 13063 df-ioo 13300 df-ico 13302 df-icc 13303 df-fz 13460 df-fzo 13607 df-seq 13962 df-exp 14022 df-hash 14291 df-cj 15059 df-re 15060 df-im 15061 df-sqrt 15195 df-abs 15196 df-clim 15448 df-sum 15647 df-struct 17115 df-sets 17132 df-slot 17150 df-ndx 17162 df-base 17178 df-ress 17199 df-plusg 17231 df-mulr 17232 df-starv 17233 df-sca 17234 df-vsca 17235 df-ip 17236 df-tset 17237 df-ple 17238 df-ds 17240 df-unif 17241 df-hom 17242 df-cco 17243 df-rest 17383 df-topn 17384 df-0g 17402 df-gsum 17403 df-topgen 17404 df-pt 17405 df-prds 17408 df-xrs 17464 df-qtop 17469 df-imas 17470 df-xps 17472 df-mre 17546 df-mrc 17547 df-acs 17549 df-mgm 18606 df-sgrp 18685 df-mnd 18701 df-submnd 18750 df-mulg 19042 df-cntz 19290 df-cmn 19755 df-psmet 21346 df-xmet 21347 df-met 21348 df-bl 21349 df-mopn 21350 df-fbas 21351 df-fg 21352 df-cnfld 21355 df-top 22884 df-topon 22901 df-topsp 22923 df-bases 22936 df-cld 23009 df-ntr 23010 df-cls 23011 df-nei 23088 df-lp 23126 df-perf 23127 df-cn 23217 df-cnp 23218 df-haus 23305 df-cmp 23377 df-tx 23552 df-hmeo 23745 df-fil 23836 df-fm 23928 df-flim 23929 df-flf 23930 df-xms 24310 df-ms 24311 df-tms 24312 df-cncf 24870 df-limc 25858 df-dv 25859

This theorem is referenced by: dvfsumge 26014

W3C validator