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)

	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		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
60	59	mulcn	$⊢ \times \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
61	12	zred	$⊢ φ \to M \in ℝ$
62	61	adantr	$⊢ (φ \land k \in (M ..^N)) \to M \in ℝ$
63	14	zred	$⊢ φ \to N \in ℝ$
64	63	adantr	$⊢ (φ \land k \in (M ..^N)) \to N \in ℝ$
65		elfzole1	$⊢ k \in (M ..^N) \to M \leq k$
66	65	adantl	$⊢ (φ \land k \in (M ..^N)) \to M \leq k$
67	33	adantl	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \in (M \dots N)$
68		elfzle2	$⊢ k + 1 \in (M \dots N) \to k + 1 \leq N$
69	67 68	syl	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \leq N$
70		iccss	$⊢ ((M \in ℝ \land N \in ℝ) \land (M \leq k \land k + 1 \leq N)) \to [k, k + 1] \subseteq [M, N]$
71	62 64 66 69 70	syl22anc	$⊢ (φ \land k \in (M ..^N)) \to [k, k + 1] \subseteq [M, N]$
72		iccssre	$⊢ (M \in ℝ \land N \in ℝ) \to [M, N] \subseteq ℝ$
73	61 63 72	syl2anc	$⊢ φ \to [M, N] \subseteq ℝ$
74	73	adantr	$⊢ (φ \land k \in (M ..^N)) \to [M, N] \subseteq ℝ$
75	71 74	sstrd	$⊢ (φ \land k \in (M ..^N)) \to [k, k + 1] \subseteq ℝ$
76		ax-resscn	$⊢ ℝ \subseteq ℂ$
77	75 76	sstrdi	$⊢ (φ \land k \in (M ..^N)) \to [k, k + 1] \subseteq ℂ$
78	76	a1i	$⊢ (φ \land k \in (M ..^N)) \to ℝ \subseteq ℂ$
79		cncfmptc	$⊢ (X \in ℝ \land [k, k + 1] \subseteq ℂ \land ℝ \subseteq ℂ) \to (y \in [k, k + 1] ⟼ X) : [k, k + 1] \underset{cn}{⟶} ℝ$
80	7 77 78 79	syl3anc	$⊢ (φ \land k \in (M ..^N)) \to (y \in [k, k + 1] ⟼ X) : [k, k + 1] \underset{cn}{⟶} ℝ$
81		cncfmptid	$⊢ ([k, k + 1] \subseteq ℝ \land ℝ \subseteq ℂ) \to (y \in [k, k + 1] ⟼ y) : [k, k + 1] \underset{cn}{⟶} ℝ$
82	75 76 81	sylancl	$⊢ (φ \land k \in (M ..^N)) \to (y \in [k, k + 1] ⟼ y) : [k, k + 1] \underset{cn}{⟶} ℝ$
83		remulcl	$⊢ (X \in ℝ \land y \in ℝ) \to X y \in ℝ$
84	59 60 80 82 76 83	cncfmpt2ss	$⊢ (φ \land k \in (M ..^N)) \to (y \in [k, k + 1] ⟼ X y) : [k, k + 1] \underset{cn}{⟶} ℝ$
85		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
86	85	a1i	$⊢ (φ \land k \in (M ..^N)) \to ℝ \in \{ℝ, ℂ\}$
87	62	rexrd	$⊢ (φ \land k \in (M ..^N)) \to M \in ℝ^{*}$
88		iooss1	$⊢ (M \in ℝ^{*} \land M \leq k) \to (k, k + 1) \subseteq (M, k + 1)$
89	87 66 88	syl2anc	$⊢ (φ \land k \in (M ..^N)) \to (k, k + 1) \subseteq (M, k + 1)$
90	64	rexrd	$⊢ (φ \land k \in (M ..^N)) \to N \in ℝ^{*}$
91		iooss2	$⊢ (N \in ℝ^{*} \land k + 1 \leq N) \to (M, k + 1) \subseteq (M, N)$
92	90 69 91	syl2anc	$⊢ (φ \land k \in (M ..^N)) \to (M, k + 1) \subseteq (M, N)$
93	89 92	sstrd	$⊢ (φ \land k \in (M ..^N)) \to (k, k + 1) \subseteq (M, N)$
94		ioossicc	$⊢ (M, N) \subseteq [M, N]$
95	74 76	sstrdi	$⊢ (φ \land k \in (M ..^N)) \to [M, N] \subseteq ℂ$
96	94 95	sstrid	$⊢ (φ \land k \in (M ..^N)) \to (M, N) \subseteq ℂ$
97	93 96	sstrd	$⊢ (φ \land k \in (M ..^N)) \to (k, k + 1) \subseteq ℂ$
98	97	sselda	$⊢ ((φ \land k \in (M ..^N)) \land y \in (k, k + 1)) \to y \in ℂ$
99		1cnd	$⊢ ((φ \land k \in (M ..^N)) \land y \in (k, k + 1)) \to 1 \in ℂ$
100	78	sselda	$⊢ ((φ \land k \in (M ..^N)) \land y \in ℝ) \to y \in ℂ$
101		1cnd	$⊢ ((φ \land k \in (M ..^N)) \land y \in ℝ) \to 1 \in ℂ$
102	86	dvmptid	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (y \in ℝ⟼ y)}{d_{ℝ} y} = (y \in ℝ ⟼ 1)$
103		ioossre	$⊢ (k, k + 1) \subseteq ℝ$
104	103	a1i	$⊢ (φ \land k \in (M ..^N)) \to (k, k + 1) \subseteq ℝ$
105	59	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
106		iooretop	$⊢ (k, k + 1) \in topGen (ran (.))$
107	106	a1i	$⊢ (φ \land k \in (M ..^N)) \to (k, k + 1) \in topGen (ran (.))$
108	86 100 101 102 104 105 59 107	dvmptres	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (y \in (k, k + 1)⟼ y)}{d_{ℝ} y} = (y \in (k, k + 1) ⟼ 1)$
109	86 98 99 108 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)$
110	57	mpteq2dv	$⊢ (φ \land k \in (M ..^N)) \to (y \in (k, k + 1) ⟼ X \cdot 1) = (y \in (k, k + 1) ⟼ X)$
111	109 110	eqtrd	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (y \in (k, k + 1)⟼ X y)}{d_{ℝ} y} = (y \in (k, k + 1) ⟼ X)$
112		nfcv	$⊢ \underline{Ⅎ} y A$
113	112 25 27	cbvmpt	$⊢ (x \in [k, k + 1] ⟼ A) = (y \in [k, k + 1] ⟼ ⦋ y / x ⦌ A)$
114	71	resmptd	$⊢ (φ \land k \in (M ..^N)) \to {(x \in [M, N] ⟼ A) ↾}_{[k, k + 1]} = (x \in [k, k + 1] ⟼ A)$
115	2	adantr	$⊢ (φ \land k \in (M ..^N)) \to (x \in [M, N] ⟼ A) : [M, N] \underset{cn}{⟶} ℝ$
116		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}{⟶} ℝ)$
117	71 115 116	sylc	$⊢ (φ \land k \in (M ..^N)) \to ({(x \in [M, N] ⟼ A) ↾}_{[k, k + 1]}) : [k, k + 1] \underset{cn}{⟶} ℝ$
118	114 117	eqeltrrd	$⊢ (φ \land k \in (M ..^N)) \to (x \in [k, k + 1] ⟼ A) : [k, k + 1] \underset{cn}{⟶} ℝ$
119	113 118	eqeltrrid	$⊢ (φ \land k \in (M ..^N)) \to (y \in [k, k + 1] ⟼ ⦋ y / x ⦌ A) : [k, k + 1] \underset{cn}{⟶} ℝ$
120	21	adantr	$⊢ (φ \land k \in (M ..^N)) \to (x \in [M, N] ⟼ A) : [M, N] ⟶ ℝ$
121	120 23	sylibr	$⊢ (φ \land k \in (M ..^N)) \to \forall x \in [M, N] A \in ℝ$
122	94	sseli	$⊢ y \in (M, N) \to y \in [M, N]$
123	29	impcom	$⊢ (\forall x \in [M, N] A \in ℝ \land y \in [M, N]) \to ⦋ y / x ⦌ A \in ℝ$
124	121 122 123	syl2an	$⊢ ((φ \land k \in (M ..^N)) \land y \in (M, N)) \to ⦋ y / x ⦌ A \in ℝ$
125	124	recnd	$⊢ ((φ \land k \in (M ..^N)) \land y \in (M, N)) \to ⦋ y / x ⦌ A \in ℂ$
126	94	sseli	$⊢ x \in (M, N) \to x \in [M, N]$
127	21	fvmptelcdm	$⊢ (φ \land x \in [M, N]) \to A \in ℝ$
128	127	adantlr	$⊢ ((φ \land k \in (M ..^N)) \land x \in [M, N]) \to A \in ℝ$
129	126 128	sylan2	$⊢ ((φ \land k \in (M ..^N)) \land x \in (M, N)) \to A \in ℝ$
130	129	fmpttd	$⊢ (φ \land k \in (M ..^N)) \to (x \in (M, N) ⟼ A) : (M, N) ⟶ ℝ$
131		ioossre	$⊢ (M, N) \subseteq ℝ$
132		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} ⟶ ℝ$
133	130 131 132	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} ⟶ ℝ$
134	4	adantr	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = (x \in (M, N) ⟼ B)$
135	134	dmeqd	$⊢ (φ \land k \in (M ..^N)) \to dom \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = dom (x \in (M, N) ⟼ B)$
136	3	adantlr	$⊢ ((φ \land k \in (M ..^N)) \land x \in (M, N)) \to B \in V$
137	136	ralrimiva	$⊢ (φ \land k \in (M ..^N)) \to \forall x \in (M, N) B \in V$
138		dmmptg	$⊢ \forall x \in (M, N) B \in V \to dom (x \in (M, N) ⟼ B) = (M, N)$
139	137 138	syl	$⊢ (φ \land k \in (M ..^N)) \to dom (x \in (M, N) ⟼ B) = (M, N)$
140	135 139	eqtrd	$⊢ (φ \land k \in (M ..^N)) \to dom \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = (M, N)$
141	134 140	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) ⟶ ℝ)$
142	133 141	mpbid	$⊢ (φ \land k \in (M ..^N)) \to (x \in (M, N) ⟼ B) : (M, N) ⟶ ℝ$
143		eqid	$⊢ (x \in (M, N) ⟼ B) = (x \in (M, N) ⟼ B)$
144	143	fmpt	$⊢ \forall x \in (M, N) B \in ℝ \leftrightarrow (x \in (M, N) ⟼ B) : (M, N) ⟶ ℝ$
145	142 144	sylibr	$⊢ (φ \land k \in (M ..^N)) \to \forall x \in (M, N) B \in ℝ$
146		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ B$
147	146	nfel1	$⊢ Ⅎ x ⦋ y / x ⦌ B \in ℝ$
148		csbeq1a	$⊢ x = y \to B = ⦋ y / x ⦌ B$
149	148	eleq1d	$⊢ x = y \to (B \in ℝ \leftrightarrow ⦋ y / x ⦌ B \in ℝ)$
150	147 149	rspc	$⊢ y \in (M, N) \to (\forall x \in (M, N) B \in ℝ \to ⦋ y / x ⦌ B \in ℝ)$
151	145 150	mpan9	$⊢ ((φ \land k \in (M ..^N)) \land y \in (M, N)) \to ⦋ y / x ⦌ B \in ℝ$
152	112 25 27	cbvmpt	$⊢ (x \in (M, N) ⟼ A) = (y \in (M, N) ⟼ ⦋ y / x ⦌ A)$
153	152	oveq2i	$⊢ \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = \frac{d (y \in (M, N)⟼ ⦋ y / x ⦌ A)}{d_{ℝ} y}$
154		nfcv	$⊢ \underline{Ⅎ} y B$
155	154 146 148	cbvmpt	$⊢ (x \in (M, N) ⟼ B) = (y \in (M, N) ⟼ ⦋ y / x ⦌ B)$
156	134 153 155	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)$
157	86 125 151 156 93 105 59 107	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)$
158	8	anassrs	$⊢ ((φ \land k \in (M ..^N)) \land x \in (k, k + 1)) \to X \leq B$
159	158	ralrimiva	$⊢ (φ \land k \in (M ..^N)) \to \forall x \in (k, k + 1) X \leq B$
160		nfcv	$⊢ \underline{Ⅎ} x X$
161		nfcv	$⊢ \underline{Ⅎ} x \leq$
162	160 161 146	nfbr	$⊢ Ⅎ x X \leq ⦋ y / x ⦌ B$
163	148	breq2d	$⊢ x = y \to (X \leq B \leftrightarrow X \leq ⦋ y / x ⦌ B)$
164	162 163	rspc	$⊢ y \in (k, k + 1) \to (\forall x \in (k, k + 1) X \leq B \to X \leq ⦋ y / x ⦌ B)$
165	159 164	mpan9	$⊢ ((φ \land k \in (M ..^N)) \land y \in (k, k + 1)) \to X \leq ⦋ y / x ⦌ B$
166	46	rexrd	$⊢ (φ \land k \in (M ..^N)) \to k \in ℝ^{*}$
167	54	rexrd	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \in ℝ^{*}$
168	46	lep1d	$⊢ (φ \land k \in (M ..^N)) \to k \leq k + 1$
169		lbicc2	$⊢ (k \in ℝ^{} \land k + 1 \in ℝ^{} \land k \leq k + 1) \to k \in [k, k + 1]$
170	166 167 168 169	syl3anc	$⊢ (φ \land k \in (M ..^N)) \to k \in [k, k + 1]$
171		ubicc2	$⊢ (k \in ℝ^{} \land k + 1 \in ℝ^{} \land k \leq k + 1) \to k + 1 \in [k, k + 1]$
172	166 167 168 171	syl3anc	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \in [k, k + 1]$
173		oveq2	$⊢ y = k \to X y = X k$
174		oveq2	$⊢ y = k + 1 \to X y = X (k + 1)$
175	46 54 84 111 119 157 165 170 172 168 173 39 174 34	dvle	$⊢ (φ \land k \in (M ..^N)) \to X (k + 1) - X k \leq ⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A$
176	58 175	eqbrtrrd	$⊢ (φ \land k \in (M ..^N)) \to X \leq ⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A$
177	10 7 43 176	fsumle	$⊢ φ \to \sum_{k \in (M ..^N)} X \leq \sum_{k \in (M ..^N)} (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A)$
178		vex	$⊢ y \in V$
179	178	a1i	$⊢ y = M \to y \in V$
180		eqeq2	$⊢ y = M \to (x = y \leftrightarrow x = M)$
181	180	biimpa	$⊢ (y = M \land x = y) \to x = M$
182	181 5	syl	$⊢ (y = M \land x = y) \to A = C$
183	179 182	csbied	$⊢ y = M \to ⦋ y / x ⦌ A = C$
184	178	a1i	$⊢ y = N \to y \in V$
185		eqeq2	$⊢ y = N \to (x = y \leftrightarrow x = N)$
186	185	biimpa	$⊢ (y = N \land x = y) \to x = N$
187	186 6	syl	$⊢ (y = N \land x = y) \to A = D$
188	184 187	csbied	$⊢ y = N \to ⦋ y / x ⦌ A = D$
189	31	recnd	$⊢ (φ \land y \in (M \dots N)) \to ⦋ y / x ⦌ A \in ℂ$
190	39 34 183 188 1 189	telfsumo2	$⊢ φ \to \sum_{k \in (M ..^N)} (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A) = D - C$
191	177 190	breqtrd	$⊢ φ \to \sum_{k \in (M ..^N)} X \leq D - C$

Metamath Proof Explorer

Theorem dvfsumle

Proof