dvfsumabs

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

Proof

Step	Hyp	Ref	Expression
1		dvfsumabs.m	$⊢ φ \to N \in ℤ_{\geq M}$
2		dvfsumabs.a	$⊢ φ \to (x \in [M, N] ⟼ A) : [M, N] \underset{cn}{⟶} ℂ$
3		dvfsumabs.v	$⊢ (φ \land x \in (M, N)) \to B \in V$
4		dvfsumabs.b	$⊢ φ \to \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = (x \in (M, N) ⟼ B)$
5		dvfsumabs.c	$⊢ x = M \to A = C$
6		dvfsumabs.d	$⊢ x = N \to A = D$
7		dvfsumabs.x	$⊢ (φ \land k \in (M ..^N)) \to X \in ℂ$
8		dvfsumabs.y	$⊢ (φ \land k \in (M ..^N)) \to Y \in ℝ$
9		dvfsumabs.l	$⊢ (φ \land (k \in (M ..^N) \land x \in (k, k + 1))) \to \|X - B\| \leq Y$
10		fzofi	$⊢ (M ..^N) \in Fin$
11	10	a1i	$⊢ φ \to (M ..^N) \in Fin$
12		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
13	1 12	syl	$⊢ φ \to M \in ℤ$
14		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
15	1 14	syl	$⊢ φ \to N \in ℤ$
16		fzval2	$⊢ (M \in ℤ \land N \in ℤ) \to (M \dots N) = [M, N] \cap ℤ$
17	13 15 16	syl2anc	$⊢ φ \to (M \dots N) = [M, N] \cap ℤ$
18		inss1	$⊢ [M, N] \cap ℤ \subseteq [M, N]$
19	17 18	eqsstrdi	$⊢ φ \to (M \dots N) \subseteq [M, N]$
20	19	sselda	$⊢ (φ \land y \in (M \dots N)) \to y \in [M, N]$
21		cncff	$⊢ (x \in [M, N] ⟼ A) : [M, N] \underset{cn}{⟶} ℂ \to (x \in [M, N] ⟼ A) : [M, N] ⟶ ℂ$
22	2 21	syl	$⊢ φ \to (x \in [M, N] ⟼ A) : [M, N] ⟶ ℂ$
23		eqid	$⊢ (x \in [M, N] ⟼ A) = (x \in [M, N] ⟼ A)$
24	23	fmpt	$⊢ \forall x \in [M, N] A \in ℂ \leftrightarrow (x \in [M, N] ⟼ A) : [M, N] ⟶ ℂ$
25	22 24	sylibr	$⊢ φ \to \forall x \in [M, N] A \in ℂ$
26		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ A$
27	26	nfel1	$⊢ Ⅎ x ⦋ y / x ⦌ A \in ℂ$
28		csbeq1a	$⊢ x = y \to A = ⦋ y / x ⦌ A$
29	28	eleq1d	$⊢ x = y \to (A \in ℂ \leftrightarrow ⦋ y / x ⦌ A \in ℂ)$
30	27 29	rspc	$⊢ y \in [M, N] \to (\forall x \in [M, N] A \in ℂ \to ⦋ y / x ⦌ A \in ℂ)$
31	25 30	mpan9	$⊢ (φ \land y \in [M, N]) \to ⦋ y / x ⦌ A \in ℂ$
32	20 31	syldan	$⊢ (φ \land y \in (M \dots N)) \to ⦋ y / x ⦌ A \in ℂ$
33	32	ralrimiva	$⊢ φ \to \forall y \in (M \dots N) ⦋ y / x ⦌ A \in ℂ$
34		fzofzp1	$⊢ k \in (M ..^N) \to k + 1 \in (M \dots N)$
35		csbeq1	$⊢ y = k + 1 \to ⦋ y / x ⦌ A = ⦋ (k + 1) / x ⦌ A$
36	35	eleq1d	$⊢ y = k + 1 \to (⦋ y / x ⦌ A \in ℂ \leftrightarrow ⦋ (k + 1) / x ⦌ A \in ℂ)$
37	36	rspccva	$⊢ (\forall y \in (M \dots N) ⦋ y / x ⦌ A \in ℂ \land k + 1 \in (M \dots N)) \to ⦋ (k + 1) / x ⦌ A \in ℂ$
38	33 34 37	syl2an	$⊢ (φ \land k \in (M ..^N)) \to ⦋ (k + 1) / x ⦌ A \in ℂ$
39		elfzofz	$⊢ k \in (M ..^N) \to k \in (M \dots N)$
40		csbeq1	$⊢ y = k \to ⦋ y / x ⦌ A = ⦋ k / x ⦌ A$
41	40	eleq1d	$⊢ y = k \to (⦋ y / x ⦌ A \in ℂ \leftrightarrow ⦋ k / x ⦌ A \in ℂ)$
42	41	rspccva	$⊢ (\forall y \in (M \dots N) ⦋ y / x ⦌ A \in ℂ \land k \in (M \dots N)) \to ⦋ k / x ⦌ A \in ℂ$
43	33 39 42	syl2an	$⊢ (φ \land k \in (M ..^N)) \to ⦋ k / x ⦌ A \in ℂ$
44	38 43	subcld	$⊢ (φ \land k \in (M ..^N)) \to ⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A \in ℂ$
45	11 7 44	fsumsub	$⊢ φ \to \sum_{k \in (M ..^N)} (X - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A)) = \sum_{k \in (M ..^N)} X - \sum_{k \in (M ..^N)} (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A)$
46		vex	$⊢ y \in V$
47	46	a1i	$⊢ y = M \to y \in V$
48		eqeq2	$⊢ y = M \to (x = y \leftrightarrow x = M)$
49	48	biimpa	$⊢ (y = M \land x = y) \to x = M$
50	49 5	syl	$⊢ (y = M \land x = y) \to A = C$
51	47 50	csbied	$⊢ y = M \to ⦋ y / x ⦌ A = C$
52	46	a1i	$⊢ y = N \to y \in V$
53		eqeq2	$⊢ y = N \to (x = y \leftrightarrow x = N)$
54	53	biimpa	$⊢ (y = N \land x = y) \to x = N$
55	54 6	syl	$⊢ (y = N \land x = y) \to A = D$
56	52 55	csbied	$⊢ y = N \to ⦋ y / x ⦌ A = D$
57	40 35 51 56 1 32	telfsumo2	$⊢ φ \to \sum_{k \in (M ..^N)} (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A) = D - C$
58	57	oveq2d	$⊢ φ \to \sum_{k \in (M ..^N)} X - \sum_{k \in (M ..^N)} (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A) = \sum_{k \in (M ..^N)} X - (D - C)$
59	45 58	eqtrd	$⊢ φ \to \sum_{k \in (M ..^N)} (X - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A)) = \sum_{k \in (M ..^N)} X - (D - C)$
60	59	fveq2d	$⊢ φ \to \|\sum_{k \in (M ..^N)} (X - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A))\| = \|\sum_{k \in (M ..^N)} X - (D - C)\|$
61	7 44	subcld	$⊢ (φ \land k \in (M ..^N)) \to X - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A) \in ℂ$
62	11 61	fsumcl	$⊢ φ \to \sum_{k \in (M ..^N)} (X - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A)) \in ℂ$
63	62	abscld	$⊢ φ \to \|\sum_{k \in (M ..^N)} (X - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A))\| \in ℝ$
64	61	abscld	$⊢ (φ \land k \in (M ..^N)) \to \|X - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A)\| \in ℝ$
65	11 64	fsumrecl	$⊢ φ \to \sum_{k \in (M ..^N)} \|X - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A)\| \in ℝ$
66	11 8	fsumrecl	$⊢ φ \to \sum_{k \in (M ..^N)} Y \in ℝ$
67	11 61	fsumabs	$⊢ φ \to \|\sum_{k \in (M ..^N)} (X - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A))\| \leq \sum_{k \in (M ..^N)} \|X - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A)\|$
68		elfzoelz	$⊢ k \in (M ..^N) \to k \in ℤ$
69	68	adantl	$⊢ (φ \land k \in (M ..^N)) \to k \in ℤ$
70	69	zred	$⊢ (φ \land k \in (M ..^N)) \to k \in ℝ$
71	70	rexrd	$⊢ (φ \land k \in (M ..^N)) \to k \in ℝ^{*}$
72		peano2re	$⊢ k \in ℝ \to k + 1 \in ℝ$
73	70 72	syl	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \in ℝ$
74	73	rexrd	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \in ℝ^{*}$
75	70	lep1d	$⊢ (φ \land k \in (M ..^N)) \to k \leq k + 1$
76		ubicc2	$⊢ (k \in ℝ^{} \land k + 1 \in ℝ^{} \land k \leq k + 1) \to k + 1 \in [k, k + 1]$
77	71 74 75 76	syl3anc	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \in [k, k + 1]$
78		lbicc2	$⊢ (k \in ℝ^{} \land k + 1 \in ℝ^{} \land k \leq k + 1) \to k \in [k, k + 1]$
79	71 74 75 78	syl3anc	$⊢ (φ \land k \in (M ..^N)) \to k \in [k, k + 1]$
80	13	zred	$⊢ φ \to M \in ℝ$
81	80	adantr	$⊢ (φ \land k \in (M ..^N)) \to M \in ℝ$
82	15	zred	$⊢ φ \to N \in ℝ$
83	82	adantr	$⊢ (φ \land k \in (M ..^N)) \to N \in ℝ$
84		elfzole1	$⊢ k \in (M ..^N) \to M \leq k$
85	84	adantl	$⊢ (φ \land k \in (M ..^N)) \to M \leq k$
86	34	adantl	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \in (M \dots N)$
87		elfzle2	$⊢ k + 1 \in (M \dots N) \to k + 1 \leq N$
88	86 87	syl	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \leq N$
89		iccss	$⊢ ((M \in ℝ \land N \in ℝ) \land (M \leq k \land k + 1 \leq N)) \to [k, k + 1] \subseteq [M, N]$
90	81 83 85 88 89	syl22anc	$⊢ (φ \land k \in (M ..^N)) \to [k, k + 1] \subseteq [M, N]$
91	90	resmptd	$⊢ (φ \land k \in (M ..^N)) \to {(x \in [M, N] ⟼ X x - A) ↾}_{[k, k + 1]} = (x \in [k, k + 1] ⟼ X x - A)$
92		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
93	92	subcn	$⊢ - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
94	93	a1i	$⊢ (φ \land k \in (M ..^N)) \to - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
95		iccssre	$⊢ (M \in ℝ \land N \in ℝ) \to [M, N] \subseteq ℝ$
96	80 82 95	syl2anc	$⊢ φ \to [M, N] \subseteq ℝ$
97	96	adantr	$⊢ (φ \land k \in (M ..^N)) \to [M, N] \subseteq ℝ$
98		ax-resscn	$⊢ ℝ \subseteq ℂ$
99	97 98	sstrdi	$⊢ (φ \land k \in (M ..^N)) \to [M, N] \subseteq ℂ$
100		ssid	$⊢ ℂ \subseteq ℂ$
101	100	a1i	$⊢ (φ \land k \in (M ..^N)) \to ℂ \subseteq ℂ$
102		cncfmptc	$⊢ (X \in ℂ \land [M, N] \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in [M, N] ⟼ X) : [M, N] \underset{cn}{⟶} ℂ$
103	7 99 101 102	syl3anc	$⊢ (φ \land k \in (M ..^N)) \to (x \in [M, N] ⟼ X) : [M, N] \underset{cn}{⟶} ℂ$
104		cncfmptid	$⊢ ([M, N] \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in [M, N] ⟼ x) : [M, N] \underset{cn}{⟶} ℂ$
105	99 100 104	sylancl	$⊢ (φ \land k \in (M ..^N)) \to (x \in [M, N] ⟼ x) : [M, N] \underset{cn}{⟶} ℂ$
106	103 105	mulcncf	$⊢ (φ \land k \in (M ..^N)) \to (x \in [M, N] ⟼ X x) : [M, N] \underset{cn}{⟶} ℂ$
107	2	adantr	$⊢ (φ \land k \in (M ..^N)) \to (x \in [M, N] ⟼ A) : [M, N] \underset{cn}{⟶} ℂ$
108	92 94 106 107	cncfmpt2f	$⊢ (φ \land k \in (M ..^N)) \to (x \in [M, N] ⟼ X x - A) : [M, N] \underset{cn}{⟶} ℂ$
109		rescncf	$⊢ [k, k + 1] \subseteq [M, N] \to ((x \in [M, N] ⟼ X x - A) : [M, N] \underset{cn}{⟶} ℂ \to ({(x \in [M, N] ⟼ X x - A) ↾}_{[k, k + 1]}) : [k, k + 1] \underset{cn}{⟶} ℂ)$
110	90 108 109	sylc	$⊢ (φ \land k \in (M ..^N)) \to ({(x \in [M, N] ⟼ X x - A) ↾}_{[k, k + 1]}) : [k, k + 1] \underset{cn}{⟶} ℂ$
111	91 110	eqeltrrd	$⊢ (φ \land k \in (M ..^N)) \to (x \in [k, k + 1] ⟼ X x - A) : [k, k + 1] \underset{cn}{⟶} ℂ$
112	98	a1i	$⊢ (φ \land k \in (M ..^N)) \to ℝ \subseteq ℂ$
113	90 97	sstrd	$⊢ (φ \land k \in (M ..^N)) \to [k, k + 1] \subseteq ℝ$
114	90	sselda	$⊢ ((φ \land k \in (M ..^N)) \land x \in [k, k + 1]) \to x \in [M, N]$
115	7	adantr	$⊢ ((φ \land k \in (M ..^N)) \land x \in [M, N]) \to X \in ℂ$
116	99	sselda	$⊢ ((φ \land k \in (M ..^N)) \land x \in [M, N]) \to x \in ℂ$
117	115 116	mulcld	$⊢ ((φ \land k \in (M ..^N)) \land x \in [M, N]) \to X x \in ℂ$
118	25	r19.21bi	$⊢ (φ \land x \in [M, N]) \to A \in ℂ$
119	118	adantlr	$⊢ ((φ \land k \in (M ..^N)) \land x \in [M, N]) \to A \in ℂ$
120	117 119	subcld	$⊢ ((φ \land k \in (M ..^N)) \land x \in [M, N]) \to X x - A \in ℂ$
121	114 120	syldan	$⊢ ((φ \land k \in (M ..^N)) \land x \in [k, k + 1]) \to X x - A \in ℂ$
122		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
123		iccntr	$⊢ (k \in ℝ \land k + 1 \in ℝ) \to int (topGen (ran (.))) ([k, k + 1]) = (k, k + 1)$
124	70 73 123	syl2anc	$⊢ (φ \land k \in (M ..^N)) \to int (topGen (ran (.))) ([k, k + 1]) = (k, k + 1)$
125	112 113 121 122 92 124	dvmptntr	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} = \frac{d (x \in (k, k + 1)⟼ X x - A)}{d_{ℝ} x}$
126		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
127	126	a1i	$⊢ (φ \land k \in (M ..^N)) \to ℝ \in \{ℝ, ℂ\}$
128		ioossicc	$⊢ (M, N) \subseteq [M, N]$
129	128	sseli	$⊢ x \in (M, N) \to x \in [M, N]$
130	129 120	sylan2	$⊢ ((φ \land k \in (M ..^N)) \land x \in (M, N)) \to X x - A \in ℂ$
131		ovex	$⊢ X - B \in V$
132	131	a1i	$⊢ ((φ \land k \in (M ..^N)) \land x \in (M, N)) \to X - B \in V$
133	129 117	sylan2	$⊢ ((φ \land k \in (M ..^N)) \land x \in (M, N)) \to X x \in ℂ$
134	7	adantr	$⊢ ((φ \land k \in (M ..^N)) \land x \in (M, N)) \to X \in ℂ$
135	128 99	sstrid	$⊢ (φ \land k \in (M ..^N)) \to (M, N) \subseteq ℂ$
136	135	sselda	$⊢ ((φ \land k \in (M ..^N)) \land x \in (M, N)) \to x \in ℂ$
137		1cnd	$⊢ ((φ \land k \in (M ..^N)) \land x \in (M, N)) \to 1 \in ℂ$
138	112	sselda	$⊢ ((φ \land k \in (M ..^N)) \land x \in ℝ) \to x \in ℂ$
139		1cnd	$⊢ ((φ \land k \in (M ..^N)) \land x \in ℝ) \to 1 \in ℂ$
140	127	dvmptid	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (x \in ℝ⟼ x)}{d_{ℝ} x} = (x \in ℝ ⟼ 1)$
141	128 97	sstrid	$⊢ (φ \land k \in (M ..^N)) \to (M, N) \subseteq ℝ$
142		iooretop	$⊢ (M, N) \in topGen (ran (.))$
143	142	a1i	$⊢ (φ \land k \in (M ..^N)) \to (M, N) \in topGen (ran (.))$
144	127 138 139 140 141 122 92 143	dvmptres	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (x \in (M, N)⟼ x)}{d_{ℝ} x} = (x \in (M, N) ⟼ 1)$
145	127 136 137 144 7	dvmptcmul	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (x \in (M, N)⟼ X x)}{d_{ℝ} x} = (x \in (M, N) ⟼ X \cdot 1)$
146	7	mulridd	$⊢ (φ \land k \in (M ..^N)) \to X \cdot 1 = X$
147	146	mpteq2dv	$⊢ (φ \land k \in (M ..^N)) \to (x \in (M, N) ⟼ X \cdot 1) = (x \in (M, N) ⟼ X)$
148	145 147	eqtrd	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (x \in (M, N)⟼ X x)}{d_{ℝ} x} = (x \in (M, N) ⟼ X)$
149	129 119	sylan2	$⊢ ((φ \land k \in (M ..^N)) \land x \in (M, N)) \to A \in ℂ$
150	3	adantlr	$⊢ ((φ \land k \in (M ..^N)) \land x \in (M, N)) \to B \in V$
151	4	adantr	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (x \in (M, N)⟼ A)}{d_{ℝ} x} = (x \in (M, N) ⟼ B)$
152	127 133 134 148 149 150 151	dvmptsub	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (x \in (M, N)⟼ X x - A)}{d_{ℝ} x} = (x \in (M, N) ⟼ X - B)$
153	81	rexrd	$⊢ (φ \land k \in (M ..^N)) \to M \in ℝ^{*}$
154		iooss1	$⊢ (M \in ℝ^{*} \land M \leq k) \to (k, k + 1) \subseteq (M, k + 1)$
155	153 85 154	syl2anc	$⊢ (φ \land k \in (M ..^N)) \to (k, k + 1) \subseteq (M, k + 1)$
156	83	rexrd	$⊢ (φ \land k \in (M ..^N)) \to N \in ℝ^{*}$
157		iooss2	$⊢ (N \in ℝ^{*} \land k + 1 \leq N) \to (M, k + 1) \subseteq (M, N)$
158	156 88 157	syl2anc	$⊢ (φ \land k \in (M ..^N)) \to (M, k + 1) \subseteq (M, N)$
159	155 158	sstrd	$⊢ (φ \land k \in (M ..^N)) \to (k, k + 1) \subseteq (M, N)$
160		iooretop	$⊢ (k, k + 1) \in topGen (ran (.))$
161	160	a1i	$⊢ (φ \land k \in (M ..^N)) \to (k, k + 1) \in topGen (ran (.))$
162	127 130 132 152 159 122 92 161	dvmptres	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (x \in (k, k + 1)⟼ X x - A)}{d_{ℝ} x} = (x \in (k, k + 1) ⟼ X - B)$
163	125 162	eqtrd	$⊢ (φ \land k \in (M ..^N)) \to \frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} = (x \in (k, k + 1) ⟼ X - B)$
164	163	dmeqd	$⊢ (φ \land k \in (M ..^N)) \to dom \frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} = dom (x \in (k, k + 1) ⟼ X - B)$
165		eqid	$⊢ (x \in (k, k + 1) ⟼ X - B) = (x \in (k, k + 1) ⟼ X - B)$
166	131 165	dmmpti	$⊢ dom (x \in (k, k + 1) ⟼ X - B) = (k, k + 1)$
167	164 166	eqtrdi	$⊢ (φ \land k \in (M ..^N)) \to dom \frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} = (k, k + 1)$
168	163	adantr	$⊢ ((φ \land k \in (M ..^N)) \land x \in (k, k + 1)) \to \frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} = (x \in (k, k + 1) ⟼ X - B)$
169	168	fveq1d	$⊢ ((φ \land k \in (M ..^N)) \land x \in (k, k + 1)) \to \frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} (x) = (x \in (k, k + 1) ⟼ X - B) (x)$
170		simpr	$⊢ ((φ \land k \in (M ..^N)) \land x \in (k, k + 1)) \to x \in (k, k + 1)$
171	165	fvmpt2	$⊢ (x \in (k, k + 1) \land X - B \in V) \to (x \in (k, k + 1) ⟼ X - B) (x) = X - B$
172	170 131 171	sylancl	$⊢ ((φ \land k \in (M ..^N)) \land x \in (k, k + 1)) \to (x \in (k, k + 1) ⟼ X - B) (x) = X - B$
173	169 172	eqtrd	$⊢ ((φ \land k \in (M ..^N)) \land x \in (k, k + 1)) \to \frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} (x) = X - B$
174	173	fveq2d	$⊢ ((φ \land k \in (M ..^N)) \land x \in (k, k + 1)) \to \|\frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} (x)\| = \|X - B\|$
175	9	anassrs	$⊢ ((φ \land k \in (M ..^N)) \land x \in (k, k + 1)) \to \|X - B\| \leq Y$
176	174 175	eqbrtrd	$⊢ ((φ \land k \in (M ..^N)) \land x \in (k, k + 1)) \to \|\frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} (x)\| \leq Y$
177	176	ralrimiva	$⊢ (φ \land k \in (M ..^N)) \to \forall x \in (k, k + 1) \|\frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} (x)\| \leq Y$
178		nfcv	$⊢ \underline{Ⅎ} x abs$
179		nfcv	$⊢ \underline{Ⅎ} x ℝ$
180		nfcv	$⊢ \underline{Ⅎ} x D$
181		nfmpt1	$⊢ \underline{Ⅎ} x (x \in [k, k + 1] ⟼ X x - A)$
182	179 180 181	nfov	$⊢ \underline{Ⅎ} x \frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x}$
183		nfcv	$⊢ \underline{Ⅎ} x y$
184	182 183	nffv	$⊢ \underline{Ⅎ} x \frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} (y)$
185	178 184	nffv	$⊢ \underline{Ⅎ} x \|\frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} (y)\|$
186		nfcv	$⊢ \underline{Ⅎ} x \leq$
187		nfcv	$⊢ \underline{Ⅎ} x Y$
188	185 186 187	nfbr	$⊢ Ⅎ x \|\frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} (y)\| \leq Y$
189		2fveq3	$⊢ x = y \to \|\frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} (x)\| = \|\frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} (y)\|$
190	189	breq1d	$⊢ x = y \to (\|\frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} (x)\| \leq Y \leftrightarrow \|\frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} (y)\| \leq Y)$
191	188 190	rspc	$⊢ y \in (k, k + 1) \to (\forall x \in (k, k + 1) \|\frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} (x)\| \leq Y \to \|\frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} (y)\| \leq Y)$
192	177 191	mpan9	$⊢ ((φ \land k \in (M ..^N)) \land y \in (k, k + 1)) \to \|\frac{d (x \in [k, k + 1]⟼ X x - A)}{d_{ℝ} x} (y)\| \leq Y$
193	70 73 111 167 8 192	dvlip	$⊢ ((φ \land k \in (M ..^N)) \land (k + 1 \in [k, k + 1] \land k \in [k, k + 1])) \to \|(x \in [k, k + 1] ⟼ X x - A) (k + 1) - (x \in [k, k + 1] ⟼ X x - A) (k)\| \leq Y \|k + 1 - k\|$
194	193	ex	$⊢ (φ \land k \in (M ..^N)) \to ((k + 1 \in [k, k + 1] \land k \in [k, k + 1]) \to \|(x \in [k, k + 1] ⟼ X x - A) (k + 1) - (x \in [k, k + 1] ⟼ X x - A) (k)\| \leq Y \|k + 1 - k\|)$
195	77 79 194	mp2and	$⊢ (φ \land k \in (M ..^N)) \to \|(x \in [k, k + 1] ⟼ X x - A) (k + 1) - (x \in [k, k + 1] ⟼ X x - A) (k)\| \leq Y \|k + 1 - k\|$
196		ovex	$⊢ X (k + 1) - ⦋ (k + 1) / x ⦌ A \in V$
197		nfcv	$⊢ \underline{Ⅎ} x (k + 1)$
198		nfcv	$⊢ \underline{Ⅎ} x X (k + 1)$
199		nfcv	$⊢ \underline{Ⅎ} x -$
200		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ (k + 1) / x ⦌ A$
201	198 199 200	nfov	$⊢ \underline{Ⅎ} x (X (k + 1) - ⦋ (k + 1) / x ⦌ A)$
202		oveq2	$⊢ x = k + 1 \to X x = X (k + 1)$
203		csbeq1a	$⊢ x = k + 1 \to A = ⦋ (k + 1) / x ⦌ A$
204	202 203	oveq12d	$⊢ x = k + 1 \to X x - A = X (k + 1) - ⦋ (k + 1) / x ⦌ A$
205		eqid	$⊢ (x \in [k, k + 1] ⟼ X x - A) = (x \in [k, k + 1] ⟼ X x - A)$
206	197 201 204 205	fvmptf	$⊢ (k + 1 \in [k, k + 1] \land X (k + 1) - ⦋ (k + 1) / x ⦌ A \in V) \to (x \in [k, k + 1] ⟼ X x - A) (k + 1) = X (k + 1) - ⦋ (k + 1) / x ⦌ A$
207	77 196 206	sylancl	$⊢ (φ \land k \in (M ..^N)) \to (x \in [k, k + 1] ⟼ X x - A) (k + 1) = X (k + 1) - ⦋ (k + 1) / x ⦌ A$
208	70	recnd	$⊢ (φ \land k \in (M ..^N)) \to k \in ℂ$
209	7 208	mulcld	$⊢ (φ \land k \in (M ..^N)) \to X k \in ℂ$
210	209 43	subcld	$⊢ (φ \land k \in (M ..^N)) \to X k - ⦋ k / x ⦌ A \in ℂ$
211		nfcv	$⊢ \underline{Ⅎ} x k$
212		nfcv	$⊢ \underline{Ⅎ} x X k$
213		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ k / x ⦌ A$
214	212 199 213	nfov	$⊢ \underline{Ⅎ} x (X k - ⦋ k / x ⦌ A)$
215		oveq2	$⊢ x = k \to X x = X k$
216		csbeq1a	$⊢ x = k \to A = ⦋ k / x ⦌ A$
217	215 216	oveq12d	$⊢ x = k \to X x - A = X k - ⦋ k / x ⦌ A$
218	211 214 217 205	fvmptf	$⊢ (k \in [k, k + 1] \land X k - ⦋ k / x ⦌ A \in ℂ) \to (x \in [k, k + 1] ⟼ X x - A) (k) = X k - ⦋ k / x ⦌ A$
219	79 210 218	syl2anc	$⊢ (φ \land k \in (M ..^N)) \to (x \in [k, k + 1] ⟼ X x - A) (k) = X k - ⦋ k / x ⦌ A$
220	207 219	oveq12d	$⊢ (φ \land k \in (M ..^N)) \to (x \in [k, k + 1] ⟼ X x - A) (k + 1) - (x \in [k, k + 1] ⟼ X x - A) (k) = X (k + 1) - ⦋ (k + 1) / x ⦌ A - (X k - ⦋ k / x ⦌ A)$
221		peano2cn	$⊢ k \in ℂ \to k + 1 \in ℂ$
222	208 221	syl	$⊢ (φ \land k \in (M ..^N)) \to k + 1 \in ℂ$
223	7 222	mulcld	$⊢ (φ \land k \in (M ..^N)) \to X (k + 1) \in ℂ$
224	223 209 38 43	sub4d	$⊢ (φ \land k \in (M ..^N)) \to X (k + 1) - X k - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A) = X (k + 1) - ⦋ (k + 1) / x ⦌ A - (X k - ⦋ k / x ⦌ A)$
225		1cnd	$⊢ (φ \land k \in (M ..^N)) \to 1 \in ℂ$
226	208 225	pncan2d	$⊢ (φ \land k \in (M ..^N)) \to k + 1 - k = 1$
227	226	oveq2d	$⊢ (φ \land k \in (M ..^N)) \to X (k + 1 - k) = X \cdot 1$
228	7 222 208	subdid	$⊢ (φ \land k \in (M ..^N)) \to X (k + 1 - k) = X (k + 1) - X k$
229	227 228 146	3eqtr3d	$⊢ (φ \land k \in (M ..^N)) \to X (k + 1) - X k = X$
230	229	oveq1d	$⊢ (φ \land k \in (M ..^N)) \to X (k + 1) - X k - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A) = X - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A)$
231	220 224 230	3eqtr2rd	$⊢ (φ \land k \in (M ..^N)) \to X - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A) = (x \in [k, k + 1] ⟼ X x - A) (k + 1) - (x \in [k, k + 1] ⟼ X x - A) (k)$
232	231	fveq2d	$⊢ (φ \land k \in (M ..^N)) \to \|X - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A)\| = \|(x \in [k, k + 1] ⟼ X x - A) (k + 1) - (x \in [k, k + 1] ⟼ X x - A) (k)\|$
233	226	fveq2d	$⊢ (φ \land k \in (M ..^N)) \to \|k + 1 - k\| = \|1\|$
234		abs1	$⊢ \|1\| = 1$
235	233 234	eqtrdi	$⊢ (φ \land k \in (M ..^N)) \to \|k + 1 - k\| = 1$
236	235	oveq2d	$⊢ (φ \land k \in (M ..^N)) \to Y \|k + 1 - k\| = Y \cdot 1$
237	8	recnd	$⊢ (φ \land k \in (M ..^N)) \to Y \in ℂ$
238	237	mulridd	$⊢ (φ \land k \in (M ..^N)) \to Y \cdot 1 = Y$
239	236 238	eqtr2d	$⊢ (φ \land k \in (M ..^N)) \to Y = Y \|k + 1 - k\|$
240	195 232 239	3brtr4d	$⊢ (φ \land k \in (M ..^N)) \to \|X - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A)\| \leq Y$
241	11 64 8 240	fsumle	$⊢ φ \to \sum_{k \in (M ..^N)} \|X - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A)\| \leq \sum_{k \in (M ..^N)} Y$
242	63 65 66 67 241	letrd	$⊢ φ \to \|\sum_{k \in (M ..^N)} (X - (⦋ (k + 1) / x ⦌ A - ⦋ k / x ⦌ A))\| \leq \sum_{k \in (M ..^N)} Y$
243	60 242	eqbrtrrd	$⊢ φ \to \|\sum_{k \in (M ..^N)} X - (D - C)\| \leq \sum_{k \in (M ..^N)} Y$

Metamath Proof Explorer

Theorem dvfsumabs

Proof