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	$⊢ φ \to N \in ℤ_{\geq M}$
	dvfsumle.a	$⊢ φ \to (x \in [M, N] ⟼ A) : [M, N] \underset{cn}{⟶} ℝ$
	dvfsumle.v	$⊢ (φ \land x \in (M, N)) \to B \in V$
	dvfsumle.b	$⊢ φ \to \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = (x \in (M, N) ⟼ B)$
	dvfsumle.c	$⊢ x = M \to A = C$
	dvfsumle.d	$⊢ x = N \to A = D$
	dvfsumle.x	$⊢ (φ \land k \in (M ..^N)) \to X \in ℝ$
	dvfsumle.l	$⊢ (φ \land (k \in (M ..^N) \land x \in (k, k + 1))) \to X \leq B$
Assertion	dvfsumle	$⊢ φ \to \sum_{k \in (M ..^N)} X \leq D - C$

Proof

Step	Hyp	Ref	Expression
1		dvfsumle.m	$⊢ φ \to N \in ℤ_{\geq M}$
2		dvfsumle.a	$⊢ φ \to (x \in [M, N] ⟼ A) : [M, N] \underset{cn}{⟶} ℝ$
3		dvfsumle.v	$⊢ (φ \land x \in (M, N)) \to B \in V$
4		dvfsumle.b	$⊢ φ \to \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = (x \in (M, N) ⟼ B)$
5		dvfsumle.c	$⊢ x = M \to A = C$
6		dvfsumle.d	$⊢ x = N \to A = D$
7		dvfsumle.x	$⊢ (φ \land k \in (M ..^N)) \to X \in ℝ$
8		dvfsumle.l	$⊢ (φ \land (k \in (M ..^N) \land x \in (k, k + 1))) \to X \leq B$
9		fzofi	$⊢ (M ..^N) \in Fin$
10	9	a1i	$⊢ φ \to (M ..^N) \in Fin$
11		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
12	1 11	syl	$⊢ φ \to M \in ℤ$
13		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
14	1 13	syl	$⊢ φ \to N \in ℤ$
15		fzval2	$⊢ (M \in ℤ \land N \in ℤ) \to (M \dots N) = [M, N] \cap ℤ$
16	12 14 15	syl2anc	$⊢ φ \to (M \dots N) = [M, N] \cap ℤ$
17		inss1	$⊢ [M, N] \cap ℤ \subseteq [M, N]$
18	16 17	eqsstrdi	$⊢ φ \to (M \dots N) \subseteq [M, N]$
19	18	sselda	$⊢ (φ \land y \in (M \dots N)) \to y \in [M, N]$
20		cncff	$⊢ (x \in [M, N] ⟼ A) : [M, N] \underset{cn}{⟶} ℝ \to (x \in [M, N] ⟼ A) : [M, N] ⟶ ℝ$
21	2 20	syl	$⊢ φ \to (x \in [M, N] ⟼ A) : [M, N] ⟶ ℝ$
22		eqid	$⊢ (x \in [M, N] ⟼ A) = (x \in [M, N] ⟼ A)$
23	22	fmpt	$⊢ \forall x \in [M, N] A \in ℝ \leftrightarrow (x \in [M, N] ⟼ A) : [M, N] ⟶ ℝ$
24	21 23	sylibr	$⊢ φ \to \forall x \in [M, N] A \in ℝ$
25		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ A$
26	25	nfel1	$⊢ Ⅎ x ⦋ y / x ⦌ A \in ℝ$
27		csbeq1a	$⊢ x = y \to A = ⦋ y / x ⦌ A$
28	27	eleq1d	$⊢ x = y \to (A \in ℝ \leftrightarrow ⦋ y / x ⦌ A \in ℝ)$
29	26 28	rspc	$⊢ y \in [M, N] \to (\forall x \in [M, N] A \in ℝ \to ⦋ y / x ⦌ A \in ℝ)$
30	24 29	mpan9	$⊢ (φ \land y \in [M, N]) \to ⦋ y / x ⦌ A \in ℝ$
31	19 30	syldan	$⊢ (φ \land y \in (M \dots N)) \to ⦋ y / x ⦌ A \in ℝ$
32	31	ralrimiva	$⊢ φ \to \forall y \in (M \dots N) ⦋ y / x ⦌ A \in ℝ$
33		fzofzp1	$⊢ k \in (M ..^N) \to k + 1 \in (M \dots N)$
34		csbeq1	$⊢ y = k + 1 \to ⦋ y / x ⦌ A = ⦋ (k + 1) / x ⦌ A$
35	34	eleq1d	$⊢ y = k + 1 \to (⦋ y / x ⦌ A \in ℝ \leftrightarrow ⦋ (k + 1) / x ⦌ A \in ℝ)$
36	35	rspccva	$⊢ (\forall y \in (M \dots N) ⦋ y / x ⦌ A \in ℝ \land k + 1 \in (M \dots N)) \to ⦋ (k + 1) / x ⦌ A \in ℝ$
37	32 33 36	syl2an	$⊢ (φ \land k \in (M ..^N)) \to ⦋ (k + 1) / x ⦌ A \in ℝ$
38		elfzofz	$⊢ k \in (M ..^N) \to k \in (M \dots N)$
39		csbeq1	$⊢ y = k \to ⦋ y / x ⦌ A = ⦋ k / x ⦌ A$
40	39	eleq1d	$⊢ y = k \to (⦋ y / x ⦌ A \in ℝ \leftrightarrow ⦋ k / x ⦌ A \in ℝ)$
41	40	rspccva	$⊢ (\forall y \in (M \dots N) ⦋ y / x ⦌ A \in ℝ \land k \in (M \dots N)) \to ⦋ k / x ⦌ A \in ℝ$
42	32 38 41	syl2an	$⊢ (φ \land k \in (M ..^N)) \to ⦋ k / x ⦌ A \in ℝ$
43	37 42	resubcld	$⊢ (φ \land k \in (M ..^N)) \to ⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A \in ℝ$
44		elfzoelz	$⊢ k \in (M ..^N) \to k \in ℤ$
45	44	adantl	$⊢ (φ \land k \in (M ..^N)) \to k \in ℤ$
46	45	zred	$⊢ (φ \land k \in (M ..^N)) \to k \in ℝ$
47	46	recnd	$⊢ (φ \land k \in (M ..^N)) \to k \in ℂ$
48		ax-1cn	$⊢ 1 \in ℂ$
49		pncan2	$⊢ (k \in ℂ \land 1 \in ℂ) \to k + 1 - k = 1$
50	47 48 49	sylancl	$⊢ (φ \land k \in (M ..^N)) \to k + 1 - k = 1$
51	50	oveq2d	$⊢ (φ \land k \in (M ..^N)) \to X (k + 1 - k) = X \cdot 1$
52	7	recnd	$⊢ (φ \land k \in (M ..^N)) \to X \in ℂ$
53		peano2re	$⊢ k \in ℝ \to k + 1 \in ℝ$
54	46 53	syl	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \in ℝ$
55	54	recnd	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \in ℂ$
56	52 55 47	subdid	$⊢ (φ \land k \in (M ..^N)) \to X (k + 1 - k) = X (k + 1) - X k$
57	52	mulridd	$⊢ (φ \land k \in (M ..^N)) \to X \cdot 1 = X$
58	51 56 57	3eqtr3d	$⊢ (φ \land k \in (M ..^N)) \to X (k + 1) - X k = X$
59	52	adantr	$⊢ ((φ \land k \in (M ..^N)) \land y \in [k, k + 1]) \to X \in ℂ$
60	46 54	iccssred	$⊢ (φ \land k \in (M ..^N)) \to [k, k + 1] \subseteq ℝ$
61		ax-resscn	$⊢ ℝ \subseteq ℂ$
62	60 61	sstrdi	$⊢ (φ \land k \in (M ..^N)) \to [k, k + 1] \subseteq ℂ$
63	62	sselda	$⊢ ((φ \land k \in (M ..^N)) \land y \in [k, k + 1]) \to y \in ℂ$
64		ovmpot	$⊢ (X \in ℂ \land y \in ℂ) \to X (u \in ℂ, v \in ℂ ⟼ u v) y = X y$
65	59 63 64	syl2anc	$⊢ ((φ \land k \in (M ..^N)) \land y \in [k, k + 1]) \to X (u \in ℂ, v \in ℂ ⟼ u v) y = X y$
66	65	eqeq2d	$⊢ ((φ \land k \in (M ..^N)) \land y \in [k, k + 1]) \to (z = X (u \in ℂ, v \in ℂ ⟼ u v) y \leftrightarrow z = X y)$
67	66	pm5.32da	$⊢ (φ \land k \in (M ..^N)) \to ((y \in [k, k + 1] \land z = X (u \in ℂ, v \in ℂ ⟼ u v) y) \leftrightarrow (y \in [k, k + 1] \land z = X y))$
68	67	opabbidv	$⊢ (φ \land k \in (M ..^N)) \to \{⟨y, z⟩ \| (y \in [k, k + 1] \land z = X (u \in ℂ, v \in ℂ ⟼ u v) y)\} = \{⟨y, z⟩ \| (y \in [k, k + 1] \land z = X y)\}$
69		df-mpt	$⊢ (y \in [k, k + 1] ⟼ X y) = \{⟨y, z⟩ \| (y \in [k, k + 1] \land z = X y)\}$
70	68 69	eqtr4di	$⊢ (φ \land k \in (M ..^N)) \to \{⟨y, z⟩ \| (y \in [k, k + 1] \land z = X (u \in ℂ, v \in ℂ ⟼ u v) y)\} = (y \in [k, k + 1] ⟼ X y)$
71		df-mpt	$⊢ (y \in [k, k + 1] ⟼ X (u \in ℂ, v \in ℂ ⟼ u v) y) = \{⟨y, z⟩ \| (y \in [k, k + 1] \land z = X (u \in ℂ, v \in ℂ ⟼ u v) y)\}$
72		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
73	72	mpomulcn	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
74	61	a1i	$⊢ (φ \land k \in (M ..^N)) \to ℝ \subseteq ℂ$
75		cncfmptc	$⊢ (X \in ℝ \land [k, k + 1] \subseteq ℂ \land ℝ \subseteq ℂ) \to (y \in [k, k + 1] ⟼ X) : [k, k + 1] \underset{cn}{⟶} ℝ$
76	7 62 74 75	syl3anc	$⊢ (φ \land k \in (M ..^N)) \to (y \in [k, k + 1] ⟼ X) : [k, k + 1] \underset{cn}{⟶} ℝ$
77		cncfmptid	$⊢ ([k, k + 1] \subseteq ℝ \land ℝ \subseteq ℂ) \to (y \in [k, k + 1] ⟼ y) : [k, k + 1] \underset{cn}{⟶} ℝ$
78	60 61 77	sylancl	$⊢ (φ \land k \in (M ..^N)) \to (y \in [k, k + 1] ⟼ y) : [k, k + 1] \underset{cn}{⟶} ℝ$
79		simpl	$⊢ (X \in ℝ \land y \in ℝ) \to X \in ℝ$
80	79	recnd	$⊢ (X \in ℝ \land y \in ℝ) \to X \in ℂ$
81		simpr	$⊢ (X \in ℝ \land y \in ℝ) \to y \in ℝ$
82	81	recnd	$⊢ (X \in ℝ \land y \in ℝ) \to y \in ℂ$
83	64	eqcomd	$⊢ (X \in ℂ \land y \in ℂ) \to X y = X (u \in ℂ, v \in ℂ ⟼ u v) y$
84	80 82 83	syl2anc	$⊢ (X \in ℝ \land y \in ℝ) \to X y = X (u \in ℂ, v \in ℂ ⟼ u v) y$
85		remulcl	$⊢ (X \in ℝ \land y \in ℝ) \to X y \in ℝ$
86	84 85	eqeltrrd	$⊢ (X \in ℝ \land y \in ℝ) \to X (u \in ℂ, v \in ℂ ⟼ u v) y \in ℝ$
87	72 73 76 78 61 86	cncfmpt2ss	$⊢ (φ \land k \in (M ..^N)) \to (y \in [k, k + 1] ⟼ X (u \in ℂ, v \in ℂ ⟼ u v) y) : [k, k + 1] \underset{cn}{⟶} ℝ$
88	71 87	eqeltrrid	$⊢ (φ \land k \in (M ..^N)) \to \{⟨y, z⟩ \| (y \in [k, k + 1] \land z = X (u \in ℂ, v \in ℂ ⟼ u v) y)\} : [k, k + 1] \underset{cn}{⟶} ℝ$
89	70 88	eqeltrrd	$⊢ (φ \land k \in (M ..^N)) \to (y \in [k, k + 1] ⟼ X y) : [k, k + 1] \underset{cn}{⟶} ℝ$
90		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
91	90	a1i	$⊢ (φ \land k \in (M ..^N)) \to ℝ \in \{ℝ, ℂ\}$
92	12	zred	$⊢ φ \to M \in ℝ$
93	92	adantr	$⊢ (φ \land k \in (M ..^N)) \to M \in ℝ$
94	93	rexrd	$⊢ (φ \land k \in (M ..^N)) \to M \in ℝ^{*}$
95		elfzole1	$⊢ k \in (M ..^N) \to M \leq k$
96	95	adantl	$⊢ (φ \land k \in (M ..^N)) \to M \leq k$
97		iooss1	$⊢ (M \in ℝ^{*} \land M \leq k) \to (k, k + 1) \subseteq (M, k + 1)$
98	94 96 97	syl2anc	$⊢ (φ \land k \in (M ..^N)) \to (k, k + 1) \subseteq (M, k + 1)$
99	14	zred	$⊢ φ \to N \in ℝ$
100	99	adantr	$⊢ (φ \land k \in (M ..^N)) \to N \in ℝ$
101	100	rexrd	$⊢ (φ \land k \in (M ..^N)) \to N \in ℝ^{*}$
102	33	adantl	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \in (M \dots N)$
103		elfzle2	$⊢ k + 1 \in (M \dots N) \to k + 1 \leq N$
104	102 103	syl	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \leq N$
105		iooss2	$⊢ (N \in ℝ^{*} \land k + 1 \leq N) \to (M, k + 1) \subseteq (M, N)$
106	101 104 105	syl2anc	$⊢ (φ \land k \in (M ..^N)) \to (M, k + 1) \subseteq (M, N)$
107	98 106	sstrd	$⊢ (φ \land k \in (M ..^N)) \to (k, k + 1) \subseteq (M, N)$
108		ioossicc	$⊢ (M, N) \subseteq [M, N]$
109	92 99	iccssred	$⊢ φ \to [M, N] \subseteq ℝ$
110	109	adantr	$⊢ (φ \land k \in (M ..^N)) \to [M, N] \subseteq ℝ$
111	110 61	sstrdi	$⊢ (φ \land k \in (M ..^N)) \to [M, N] \subseteq ℂ$
112	108 111	sstrid	$⊢ (φ \land k \in (M ..^N)) \to (M, N) \subseteq ℂ$
113	107 112	sstrd	$⊢ (φ \land k \in (M ..^N)) \to (k, k + 1) \subseteq ℂ$
114	113	sselda	$⊢ ((φ \land k \in (M ..^N)) \land y \in (k, k + 1)) \to y \in ℂ$
115		1cnd	$⊢ ((φ \land k \in (M ..^N)) \land y \in (k, k + 1)) \to 1 \in ℂ$
116	74	sselda	$⊢ ((φ \land k \in (M ..^N)) \land y \in ℝ) \to y \in ℂ$
117		1cnd	$⊢ ((φ \land k \in (M ..^N)) \land y \in ℝ) \to 1 \in ℂ$
118	91	dvmptid	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (y \in ℝ⟼ y)}{d_{ℝ} y} = (y \in ℝ ⟼ 1)$
119		ioossre	$⊢ (k, k + 1) \subseteq ℝ$
120	119	a1i	$⊢ (φ \land k \in (M ..^N)) \to (k, k + 1) \subseteq ℝ$
121		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
122		iooretop	$⊢ (k, k + 1) \in topGen (ran (.))$
123	122	a1i	$⊢ (φ \land k \in (M ..^N)) \to (k, k + 1) \in topGen (ran (.))$
124	91 116 117 118 120 121 72 123	dvmptres	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (y \in (k, k + 1)⟼ y)}{d_{ℝ} y} = (y \in (k, k + 1) ⟼ 1)$
125	91 114 115 124 52	dvmptcmul	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (y \in (k, k + 1)⟼ X y)}{d_{ℝ} y} = (y \in (k, k + 1) ⟼ X \cdot 1)$
126	57	mpteq2dv	$⊢ (φ \land k \in (M ..^N)) \to (y \in (k, k + 1) ⟼ X \cdot 1) = (y \in (k, k + 1) ⟼ X)$
127	125 126	eqtrd	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (y \in (k, k + 1)⟼ X y)}{d_{ℝ} y} = (y \in (k, k + 1) ⟼ X)$
128		nfcv	$⊢ \underline{Ⅎ} y A$
129	128 25 27	cbvmpt	$⊢ (x \in [k, k + 1] ⟼ A) = (y \in [k, k + 1] ⟼ ⦋ y / x ⦌ A)$
130		iccss	$⊢ ((M \in ℝ \land N \in ℝ) \land (M \leq k \land k + 1 \leq N)) \to [k, k + 1] \subseteq [M, N]$
131	93 100 96 104 130	syl22anc	$⊢ (φ \land k \in (M ..^N)) \to [k, k + 1] \subseteq [M, N]$
132	131	resmptd	$⊢ (φ \land k \in (M ..^N)) \to {(x \in [M, N] ⟼ A) ↾}_{[k, k + 1]} = (x \in [k, k + 1] ⟼ A)$
133	2	adantr	$⊢ (φ \land k \in (M ..^N)) \to (x \in [M, N] ⟼ A) : [M, N] \underset{cn}{⟶} ℝ$
134		rescncf	$⊢ [k, k + 1] \subseteq [M, N] \to ((x \in [M, N] ⟼ A) : [M, N] \underset{cn}{⟶} ℝ \to ({(x \in [M, N] ⟼ A) ↾}_{[k, k + 1]}) : [k, k + 1] \underset{cn}{⟶} ℝ)$
135	131 133 134	sylc	$⊢ (φ \land k \in (M ..^N)) \to ({(x \in [M, N] ⟼ A) ↾}_{[k, k + 1]}) : [k, k + 1] \underset{cn}{⟶} ℝ$
136	132 135	eqeltrrd	$⊢ (φ \land k \in (M ..^N)) \to (x \in [k, k + 1] ⟼ A) : [k, k + 1] \underset{cn}{⟶} ℝ$
137	129 136	eqeltrrid	$⊢ (φ \land k \in (M ..^N)) \to (y \in [k, k + 1] ⟼ ⦋ y / x ⦌ A) : [k, k + 1] \underset{cn}{⟶} ℝ$
138	21	adantr	$⊢ (φ \land k \in (M ..^N)) \to (x \in [M, N] ⟼ A) : [M, N] ⟶ ℝ$
139	138 23	sylibr	$⊢ (φ \land k \in (M ..^N)) \to \forall x \in [M, N] A \in ℝ$
140	108	sseli	$⊢ y \in (M, N) \to y \in [M, N]$
141	29	impcom	$⊢ (\forall x \in [M, N] A \in ℝ \land y \in [M, N]) \to ⦋ y / x ⦌ A \in ℝ$
142	139 140 141	syl2an	$⊢ ((φ \land k \in (M ..^N)) \land y \in (M, N)) \to ⦋ y / x ⦌ A \in ℝ$
143	142	recnd	$⊢ ((φ \land k \in (M ..^N)) \land y \in (M, N)) \to ⦋ y / x ⦌ A \in ℂ$
144	108	sseli	$⊢ x \in (M, N) \to x \in [M, N]$
145	21	fvmptelcdm	$⊢ (φ \land x \in [M, N]) \to A \in ℝ$
146	145	adantlr	$⊢ ((φ \land k \in (M ..^N)) \land x \in [M, N]) \to A \in ℝ$
147	144 146	sylan2	$⊢ ((φ \land k \in (M ..^N)) \land x \in (M, N)) \to A \in ℝ$
148	147	fmpttd	$⊢ (φ \land k \in (M ..^N)) \to (x \in (M, N) ⟼ A) : (M, N) ⟶ ℝ$
149		ioossre	$⊢ (M, N) \subseteq ℝ$
150		dvfre	$⊢ ((x \in (M, N) ⟼ A) : (M, N) ⟶ ℝ \land (M, N) \subseteq ℝ) \to \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} : dom \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} ⟶ ℝ$
151	148 149 150	sylancl	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} : dom \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} ⟶ ℝ$
152	4	adantr	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = (x \in (M, N) ⟼ B)$
153	152	dmeqd	$⊢ (φ \land k \in (M ..^N)) \to dom \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = dom (x \in (M, N) ⟼ B)$
154	3	adantlr	$⊢ ((φ \land k \in (M ..^N)) \land x \in (M, N)) \to B \in V$
155	154	ralrimiva	$⊢ (φ \land k \in (M ..^N)) \to \forall x \in (M, N) B \in V$
156		dmmptg	$⊢ \forall x \in (M, N) B \in V \to dom (x \in (M, N) ⟼ B) = (M, N)$
157	155 156	syl	$⊢ (φ \land k \in (M ..^N)) \to dom (x \in (M, N) ⟼ B) = (M, N)$
158	153 157	eqtrd	$⊢ (φ \land k \in (M ..^N)) \to dom \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = (M, N)$
159	152 158	feq12d	$⊢ (φ \land k \in (M ..^N)) \to (\frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} : dom \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} ⟶ ℝ \leftrightarrow (x \in (M, N) ⟼ B) : (M, N) ⟶ ℝ)$
160	151 159	mpbid	$⊢ (φ \land k \in (M ..^N)) \to (x \in (M, N) ⟼ B) : (M, N) ⟶ ℝ$
161		eqid	$⊢ (x \in (M, N) ⟼ B) = (x \in (M, N) ⟼ B)$
162	161	fmpt	$⊢ \forall x \in (M, N) B \in ℝ \leftrightarrow (x \in (M, N) ⟼ B) : (M, N) ⟶ ℝ$
163	160 162	sylibr	$⊢ (φ \land k \in (M ..^N)) \to \forall x \in (M, N) B \in ℝ$
164		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ B$
165	164	nfel1	$⊢ Ⅎ x ⦋ y / x ⦌ B \in ℝ$
166		csbeq1a	$⊢ x = y \to B = ⦋ y / x ⦌ B$
167	166	eleq1d	$⊢ x = y \to (B \in ℝ \leftrightarrow ⦋ y / x ⦌ B \in ℝ)$
168	165 167	rspc	$⊢ y \in (M, N) \to (\forall x \in (M, N) B \in ℝ \to ⦋ y / x ⦌ B \in ℝ)$
169	163 168	mpan9	$⊢ ((φ \land k \in (M ..^N)) \land y \in (M, N)) \to ⦋ y / x ⦌ B \in ℝ$
170	128 25 27	cbvmpt	$⊢ (x \in (M, N) ⟼ A) = (y \in (M, N) ⟼ ⦋ y / x ⦌ A)$
171	170	oveq2i	$⊢ \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = \frac{d (y \in (M, N)⟼ ⦋ y / x ⦌ A)}{d_{ℝ} y}$
172		nfcv	$⊢ \underline{Ⅎ} y B$
173	172 164 166	cbvmpt	$⊢ (x \in (M, N) ⟼ B) = (y \in (M, N) ⟼ ⦋ y / x ⦌ B)$
174	152 171 173	3eqtr3g	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (y \in (M, N)⟼ ⦋ y / x ⦌ A)}{d_{ℝ} y} = (y \in (M, N) ⟼ ⦋ y / x ⦌ B)$
175	91 143 169 174 107 121 72 123	dvmptres	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (y \in (k, k + 1)⟼ ⦋ y / x ⦌ A)}{d_{ℝ} y} = (y \in (k, k + 1) ⟼ ⦋ y / x ⦌ B)$
176	8	anassrs	$⊢ ((φ \land k \in (M ..^N)) \land x \in (k, k + 1)) \to X \leq B$
177	176	ralrimiva	$⊢ (φ \land k \in (M ..^N)) \to \forall x \in (k, k + 1) X \leq B$
178		nfcv	$⊢ \underline{Ⅎ} x X$
179		nfcv	$⊢ \underline{Ⅎ} x \leq$
180	178 179 164	nfbr	$⊢ Ⅎ x X \leq ⦋ y / x ⦌ B$
181	166	breq2d	$⊢ x = y \to (X \leq B \leftrightarrow X \leq ⦋ y / x ⦌ B)$
182	180 181	rspc	$⊢ y \in (k, k + 1) \to (\forall x \in (k, k + 1) X \leq B \to X \leq ⦋ y / x ⦌ B)$
183	177 182	mpan9	$⊢ ((φ \land k \in (M ..^N)) \land y \in (k, k + 1)) \to X \leq ⦋ y / x ⦌ B$
184	46	rexrd	$⊢ (φ \land k \in (M ..^N)) \to k \in ℝ^{*}$
185	54	rexrd	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \in ℝ^{*}$
186	46	lep1d	$⊢ (φ \land k \in (M ..^N)) \to k \leq k + 1$
187		lbicc2	$⊢ (k \in ℝ^{} \land k + 1 \in ℝ^{} \land k \leq k + 1) \to k \in [k, k + 1]$
188	184 185 186 187	syl3anc	$⊢ (φ \land k \in (M ..^N)) \to k \in [k, k + 1]$
189		ubicc2	$⊢ (k \in ℝ^{} \land k + 1 \in ℝ^{} \land k \leq k + 1) \to k + 1 \in [k, k + 1]$
190	184 185 186 189	syl3anc	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \in [k, k + 1]$
191		oveq2	$⊢ y = k \to X y = X k$
192		oveq2	$⊢ y = k + 1 \to X y = X (k + 1)$
193	46 54 89 127 137 175 183 188 190 186 191 39 192 34	dvle	$⊢ (φ \land k \in (M ..^N)) \to X (k + 1) - X k \leq ⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A$
194	58 193	eqbrtrrd	$⊢ (φ \land k \in (M ..^N)) \to X \leq ⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A$
195	10 7 43 194	fsumle	$⊢ φ \to \sum_{k \in (M ..^N)} X \leq \sum_{k \in (M ..^N)} (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A)$
196		vex	$⊢ y \in V$
197	196	a1i	$⊢ y = M \to y \in V$
198		eqeq2	$⊢ y = M \to (x = y \leftrightarrow x = M)$
199	198	biimpa	$⊢ (y = M \land x = y) \to x = M$
200	199 5	syl	$⊢ (y = M \land x = y) \to A = C$
201	197 200	csbied	$⊢ y = M \to ⦋ y / x ⦌ A = C$
202	196	a1i	$⊢ y = N \to y \in V$
203		eqeq2	$⊢ y = N \to (x = y \leftrightarrow x = N)$
204	203	biimpa	$⊢ (y = N \land x = y) \to x = N$
205	204 6	syl	$⊢ (y = N \land x = y) \to A = D$
206	202 205	csbied	$⊢ y = N \to ⦋ y / x ⦌ A = D$
207	31	recnd	$⊢ (φ \land y \in (M \dots N)) \to ⦋ y / x ⦌ A \in ℂ$
208	39 34 201 206 1 207	telfsumo2	$⊢ φ \to \sum_{k \in (M ..^N)} (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A) = D - C$
209	195 208	breqtrd	$⊢ φ \to \sum_{k \in (M ..^N)} X \leq D - C$

Metamath Proof Explorer

Theorem dvfsumle

Proof