ftc1cnnclem

Description: Lemma for ftc1cnnc ; cf. ftc1lem4 . The stronger assumptions of ftc1cn are exploited to make use of weaker theorems. (Contributed by Brendan Leahy, 19-Nov-2017)

	Ref	Expression
Hypotheses	ftc1cnnc.g	$⊢ G = (x \in [A, B] ⟼ \int_{(A, x)} F (t) d t)$
	ftc1cnnc.a	$⊢ φ \to A \in ℝ$
	ftc1cnnc.b	$⊢ φ \to B \in ℝ$
	ftc1cnnc.le	$⊢ φ \to A \leq B$
	ftc1cnnc.f	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
	ftc1cnnc.i	$⊢ φ \to F \in 𝐿^{1}$
	ftc1cnnclem.c	$⊢ φ \to c \in (A, B)$
	ftc1cnnclem.h	$⊢ H = (z \in ([A, B] ∖ \{c\}) ⟼ \frac{G (z) - G (c)}{z - c})$
	ftc1cnnclem.e	$⊢ φ \to E \in ℝ^{+}$
	ftc1cnnclem.r	$⊢ φ \to R \in ℝ^{+}$
	ftc1cnnclem.fc	$⊢ (φ \land y \in (A, B)) \to (\|y - c\| < R \to \|F (y) - F (c)\| < E)$
	ftc1cnnclem.x1	$⊢ φ \to X \in [A, B]$
	ftc1cnnclem.x2	$⊢ φ \to \|X - c\| < R$
	ftc1cnnclem.y1	$⊢ φ \to Y \in [A, B]$
	ftc1cnnclem.y2	$⊢ φ \to \|Y - c\| < R$
Assertion	ftc1cnnclem	$⊢ (φ \land X < Y) \to \|(\frac{G (Y) - G (X)}{Y - X}) - F (c)\| < E$

Proof

Step	Hyp	Ref	Expression
1		ftc1cnnc.g	$⊢ G = (x \in [A, B] ⟼ \int_{(A, x)} F (t) d t)$
2		ftc1cnnc.a	$⊢ φ \to A \in ℝ$
3		ftc1cnnc.b	$⊢ φ \to B \in ℝ$
4		ftc1cnnc.le	$⊢ φ \to A \leq B$
5		ftc1cnnc.f	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
6		ftc1cnnc.i	$⊢ φ \to F \in 𝐿^{1}$
7		ftc1cnnclem.c	$⊢ φ \to c \in (A, B)$
8		ftc1cnnclem.h	$⊢ H = (z \in ([A, B] ∖ \{c\}) ⟼ \frac{G (z) - G (c)}{z - c})$
9		ftc1cnnclem.e	$⊢ φ \to E \in ℝ^{+}$
10		ftc1cnnclem.r	$⊢ φ \to R \in ℝ^{+}$
11		ftc1cnnclem.fc	$⊢ (φ \land y \in (A, B)) \to (\|y - c\| < R \to \|F (y) - F (c)\| < E)$
12		ftc1cnnclem.x1	$⊢ φ \to X \in [A, B]$
13		ftc1cnnclem.x2	$⊢ φ \to \|X - c\| < R$
14		ftc1cnnclem.y1	$⊢ φ \to Y \in [A, B]$
15		ftc1cnnclem.y2	$⊢ φ \to \|Y - c\| < R$
16		ovexd	$⊢ (φ \land t \in (X, Y)) \to F (t) - F (c) \in V$
17	2	rexrd	$⊢ φ \to A \in ℝ^{*}$
18	3	rexrd	$⊢ φ \to B \in ℝ^{*}$
19		elicc1	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to (X \in [A, B] \leftrightarrow (X \in ℝ^{*} \land A \leq X \land X \leq B))$
20	19	biimpa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land X \in [A, B]) \to (X \in ℝ^{*} \land A \leq X \land X \leq B)$
21	20	simp2d	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land X \in [A, B]) \to A \leq X$
22	17 18 12 21	syl21anc	$⊢ φ \to A \leq X$
23		iccleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land Y \in [A, B]) \to Y \leq B$
24	17 18 14 23	syl3anc	$⊢ φ \to Y \leq B$
25		ioossioo	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A \leq X \land Y \leq B)) \to (X, Y) \subseteq (A, B)$
26	17 18 22 24 25	syl22anc	$⊢ φ \to (X, Y) \subseteq (A, B)$
27	26	sselda	$⊢ (φ \land t \in (X, Y)) \to t \in (A, B)$
28		cncff	$⊢ F : (A, B) \underset{cn}{⟶} ℂ \to F : (A, B) ⟶ ℂ$
29	5 28	syl	$⊢ φ \to F : (A, B) ⟶ ℂ$
30	29	ffvelrnda	$⊢ (φ \land t \in (A, B)) \to F (t) \in ℂ$
31	27 30	syldan	$⊢ (φ \land t \in (X, Y)) \to F (t) \in ℂ$
32		ioombl	$⊢ (X, Y) \in dom vol$
33	32	a1i	$⊢ φ \to (X, Y) \in dom vol$
34		fvexd	$⊢ (φ \land t \in (A, B)) \to F (t) \in V$
35	29	feqmptd	$⊢ φ \to F = (t \in (A, B) ⟼ F (t))$
36	35 6	eqeltrrd	$⊢ φ \to (t \in (A, B) ⟼ F (t)) \in 𝐿^{1}$
37	26 33 34 36	iblss	$⊢ φ \to (t \in (X, Y) ⟼ F (t)) \in 𝐿^{1}$
38	29 7	ffvelrnd	$⊢ φ \to F (c) \in ℂ$
39	38	adantr	$⊢ (φ \land t \in (X, Y)) \to F (c) \in ℂ$
40		fconstmpt	$⊢ (X, Y) \times \{F (c)\} = (t \in (X, Y) ⟼ F (c))$
41		mblvol	$⊢ (X, Y) \in dom vol \to vol ((X, Y)) = {vol}^{*} ((X, Y))$
42	32 41	ax-mp	$⊢ vol ((X, Y)) = {vol}^{*} ((X, Y))$
43		ioossicc	$⊢ (X, Y) \subseteq [X, Y]$
44	43	a1i	$⊢ φ \to (X, Y) \subseteq [X, Y]$
45		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
46	2 3 45	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
47	46 12	sseldd	$⊢ φ \to X \in ℝ$
48	46 14	sseldd	$⊢ φ \to Y \in ℝ$
49		iccmbl	$⊢ (X \in ℝ \land Y \in ℝ) \to [X, Y] \in dom vol$
50	47 48 49	syl2anc	$⊢ φ \to [X, Y] \in dom vol$
51		mblss	$⊢ [X, Y] \in dom vol \to [X, Y] \subseteq ℝ$
52	50 51	syl	$⊢ φ \to [X, Y] \subseteq ℝ$
53		mblvol	$⊢ [X, Y] \in dom vol \to vol ([X, Y]) = {vol}^{*} ([X, Y])$
54	50 53	syl	$⊢ φ \to vol ([X, Y]) = {vol}^{*} ([X, Y])$
55		iccvolcl	$⊢ (X \in ℝ \land Y \in ℝ) \to vol ([X, Y]) \in ℝ$
56	47 48 55	syl2anc	$⊢ φ \to vol ([X, Y]) \in ℝ$
57	54 56	eqeltrrd	$⊢ φ \to {vol}^{*} ([X, Y]) \in ℝ$
58		ovolsscl	$⊢ ((X, Y) \subseteq [X, Y] \land [X, Y] \subseteq ℝ \land {vol}^{} ([X, Y]) \in ℝ) \to {vol}^{} ((X, Y)) \in ℝ$
59	44 52 57 58	syl3anc	$⊢ φ \to {vol}^{*} ((X, Y)) \in ℝ$
60	42 59	eqeltrid	$⊢ φ \to vol ((X, Y)) \in ℝ$
61		iblconst	$⊢ ((X, Y) \in dom vol \land vol ((X, Y)) \in ℝ \land F (c) \in ℂ) \to (X, Y) \times \{F (c)\} \in 𝐿^{1}$
62	33 60 38 61	syl3anc	$⊢ φ \to (X, Y) \times \{F (c)\} \in 𝐿^{1}$
63	40 62	eqeltrrid	$⊢ φ \to (t \in (X, Y) ⟼ F (c)) \in 𝐿^{1}$
64		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
65	64	subcn	$⊢ - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
66	65	a1i	$⊢ φ \to - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
67	29 26	feqresmpt	$⊢ φ \to {F ↾}_{(X, Y)} = (t \in (X, Y) ⟼ F (t))$
68		rescncf	$⊢ (X, Y) \subseteq (A, B) \to (F : (A, B) \underset{cn}{⟶} ℂ \to ({F ↾}_{(X, Y)}) : (X, Y) \underset{cn}{⟶} ℂ)$
69	26 5 68	sylc	$⊢ φ \to ({F ↾}_{(X, Y)}) : (X, Y) \underset{cn}{⟶} ℂ$
70	67 69	eqeltrrd	$⊢ φ \to (t \in (X, Y) ⟼ F (t)) : (X, Y) \underset{cn}{⟶} ℂ$
71		ioossre	$⊢ (X, Y) \subseteq ℝ$
72		ax-resscn	$⊢ ℝ \subseteq ℂ$
73	71 72	sstri	$⊢ (X, Y) \subseteq ℂ$
74		ssid	$⊢ ℂ \subseteq ℂ$
75		cncfmptc	$⊢ (F (c) \in ℂ \land (X, Y) \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in (X, Y) ⟼ F (c)) : (X, Y) \underset{cn}{⟶} ℂ$
76	73 74 75	mp3an23	$⊢ F (c) \in ℂ \to (t \in (X, Y) ⟼ F (c)) : (X, Y) \underset{cn}{⟶} ℂ$
77	38 76	syl	$⊢ φ \to (t \in (X, Y) ⟼ F (c)) : (X, Y) \underset{cn}{⟶} ℂ$
78	64 66 70 77	cncfmpt2f	$⊢ φ \to (t \in (X, Y) ⟼ F (t) - F (c)) : (X, Y) \underset{cn}{⟶} ℂ$
79		cnmbf	$⊢ ((X, Y) \in dom vol \land (t \in (X, Y) ⟼ F (t) - F (c)) : (X, Y) \underset{cn}{⟶} ℂ) \to (t \in (X, Y) ⟼ F (t) - F (c)) \in MblFn$
80	32 78 79	sylancr	$⊢ φ \to (t \in (X, Y) ⟼ F (t) - F (c)) \in MblFn$
81	31 37 39 63 80	iblsubnc	$⊢ φ \to (t \in (X, Y) ⟼ F (t) - F (c)) \in 𝐿^{1}$
82	16 81	itgcl	$⊢ φ \to \int_{(X, Y)} (F (t) - F (c)) d t \in ℂ$
83	82	adantr	$⊢ (φ \land X < Y) \to \int_{(X, Y)} (F (t) - F (c)) d t \in ℂ$
84	48 47	resubcld	$⊢ φ \to Y - X \in ℝ$
85	84	recnd	$⊢ φ \to Y - X \in ℂ$
86	85	adantr	$⊢ (φ \land X < Y) \to Y - X \in ℂ$
87	47 48	posdifd	$⊢ φ \to (X < Y \leftrightarrow 0 < Y - X)$
88	87	biimpa	$⊢ (φ \land X < Y) \to 0 < Y - X$
89	88	gt0ne0d	$⊢ (φ \land X < Y) \to Y - X \neq 0$
90	83 86 89	divcld	$⊢ (φ \land X < Y) \to \frac{\int_{(X, Y)} (F (t) - F (c)) d t}{Y - X} \in ℂ$
91	38	adantr	$⊢ (φ \land X < Y) \to F (c) \in ℂ$
92		ltle	$⊢ (X \in ℝ \land Y \in ℝ) \to (X < Y \to X \leq Y)$
93	47 48 92	syl2anc	$⊢ φ \to (X < Y \to X \leq Y)$
94	93	imp	$⊢ (φ \land X < Y) \to X \leq Y$
95		ssidd	$⊢ φ \to (A, B) \subseteq (A, B)$
96		ioossre	$⊢ (A, B) \subseteq ℝ$
97	96	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
98	1 2 3 4 95 97 6 29 12 14	ftc1lem1	$⊢ (φ \land X \leq Y) \to G (Y) - G (X) = \int_{(X, Y)} F (t) d t$
99	94 98	syldan	$⊢ (φ \land X < Y) \to G (Y) - G (X) = \int_{(X, Y)} F (t) d t$
100	31 39	npcand	$⊢ (φ \land t \in (X, Y)) \to F (t) - F (c) + F (c) = F (t)$
101	100	itgeq2dv	$⊢ φ \to \int_{(X, Y)} (F (t) - F (c) + F (c)) d t = \int_{(X, Y)} F (t) d t$
102	31 39	subcld	$⊢ (φ \land t \in (X, Y)) \to F (t) - F (c) \in ℂ$
103	100	mpteq2dva	$⊢ φ \to (t \in (X, Y) ⟼ F (t) - F (c) + F (c)) = (t \in (X, Y) ⟼ F (t))$
104	103 67	eqtr4d	$⊢ φ \to (t \in (X, Y) ⟼ F (t) - F (c) + F (c)) = {F ↾}_{(X, Y)}$
105		iblmbf	$⊢ F \in 𝐿^{1} \to F \in MblFn$
106	6 105	syl	$⊢ φ \to F \in MblFn$
107		mbfres	$⊢ (F \in MblFn \land (X, Y) \in dom vol) \to {F ↾}_{(X, Y)} \in MblFn$
108	106 32 107	sylancl	$⊢ φ \to {F ↾}_{(X, Y)} \in MblFn$
109	104 108	eqeltrd	$⊢ φ \to (t \in (X, Y) ⟼ F (t) - F (c) + F (c)) \in MblFn$
110	102 81 39 63 109	itgaddnc	$⊢ φ \to \int_{(X, Y)} (F (t) - F (c) + F (c)) d t = \int_{(X, Y)} (F (t) - F (c)) d t + \int_{(X, Y)} F (c) d t$
111	101 110	eqtr3d	$⊢ φ \to \int_{(X, Y)} F (t) d t = \int_{(X, Y)} (F (t) - F (c)) d t + \int_{(X, Y)} F (c) d t$
112	111	adantr	$⊢ (φ \land X < Y) \to \int_{(X, Y)} F (t) d t = \int_{(X, Y)} (F (t) - F (c)) d t + \int_{(X, Y)} F (c) d t$
113		itgconst	$⊢ ((X, Y) \in dom vol \land vol ((X, Y)) \in ℝ \land F (c) \in ℂ) \to \int_{(X, Y)} F (c) d t = F (c) vol ((X, Y))$
114	33 60 38 113	syl3anc	$⊢ φ \to \int_{(X, Y)} F (c) d t = F (c) vol ((X, Y))$
115	114	adantr	$⊢ (φ \land X < Y) \to \int_{(X, Y)} F (c) d t = F (c) vol ((X, Y))$
116	47	adantr	$⊢ (φ \land X < Y) \to X \in ℝ$
117	48	adantr	$⊢ (φ \land X < Y) \to Y \in ℝ$
118		ovolioo	$⊢ (X \in ℝ \land Y \in ℝ \land X \leq Y) \to {vol}^{*} ((X, Y)) = Y - X$
119	116 117 94 118	syl3anc	$⊢ (φ \land X < Y) \to {vol}^{*} ((X, Y)) = Y - X$
120	42 119	syl5eq	$⊢ (φ \land X < Y) \to vol ((X, Y)) = Y - X$
121	120	oveq2d	$⊢ (φ \land X < Y) \to F (c) vol ((X, Y)) = F (c) (Y - X)$
122	115 121	eqtrd	$⊢ (φ \land X < Y) \to \int_{(X, Y)} F (c) d t = F (c) (Y - X)$
123	122	oveq2d	$⊢ (φ \land X < Y) \to \int_{(X, Y)} (F (t) - F (c)) d t + \int_{(X, Y)} F (c) d t = \int_{(X, Y)} (F (t) - F (c)) d t + F (c) (Y - X)$
124	99 112 123	3eqtrd	$⊢ (φ \land X < Y) \to G (Y) - G (X) = \int_{(X, Y)} (F (t) - F (c)) d t + F (c) (Y - X)$
125	124	oveq1d	$⊢ (φ \land X < Y) \to \frac{G (Y) - G (X)}{Y - X} = \frac{\int_{(X, Y)} (F (t) - F (c)) d t + F (c) (Y - X)}{Y - X}$
126	91 86	mulcld	$⊢ (φ \land X < Y) \to F (c) (Y - X) \in ℂ$
127	83 126 86 89	divdird	$⊢ (φ \land X < Y) \to \frac{\int_{(X, Y)} (F (t) - F (c)) d t + F (c) (Y - X)}{Y - X} = (\frac{\int_{(X, Y)} (F (t) - F (c)) d t}{Y - X}) + (\frac{F (c) (Y - X)}{Y - X})$
128	91 86 89	divcan4d	$⊢ (φ \land X < Y) \to \frac{F (c) (Y - X)}{Y - X} = F (c)$
129	128	oveq2d	$⊢ (φ \land X < Y) \to (\frac{\int_{(X, Y)} (F (t) - F (c)) d t}{Y - X}) + (\frac{F (c) (Y - X)}{Y - X}) = (\frac{\int_{(X, Y)} (F (t) - F (c)) d t}{Y - X}) + F (c)$
130	125 127 129	3eqtrd	$⊢ (φ \land X < Y) \to \frac{G (Y) - G (X)}{Y - X} = (\frac{\int_{(X, Y)} (F (t) - F (c)) d t}{Y - X}) + F (c)$
131	90 91 130	mvrraddd	$⊢ (φ \land X < Y) \to (\frac{G (Y) - G (X)}{Y - X}) - F (c) = \frac{\int_{(X, Y)} (F (t) - F (c)) d t}{Y - X}$
132	131	fveq2d	$⊢ (φ \land X < Y) \to \|(\frac{G (Y) - G (X)}{Y - X}) - F (c)\| = \|\frac{\int_{(X, Y)} (F (t) - F (c)) d t}{Y - X}\|$
133	83 86 89	absdivd	$⊢ (φ \land X < Y) \to \|\frac{\int_{(X, Y)} (F (t) - F (c)) d t}{Y - X}\| = \frac{\|\int_{(X, Y)} (F (t) - F (c)) d t\|}{\|Y - X\|}$
134	84	adantr	$⊢ (φ \land X < Y) \to Y - X \in ℝ$
135		0re	$⊢ 0 \in ℝ$
136		ltle	$⊢ (0 \in ℝ \land Y - X \in ℝ) \to (0 < Y - X \to 0 \leq Y - X)$
137	135 134 136	sylancr	$⊢ (φ \land X < Y) \to (0 < Y - X \to 0 \leq Y - X)$
138	88 137	mpd	$⊢ (φ \land X < Y) \to 0 \leq Y - X$
139	134 138	absidd	$⊢ (φ \land X < Y) \to \|Y - X\| = Y - X$
140	139	oveq2d	$⊢ (φ \land X < Y) \to \frac{\|\int_{(X, Y)} (F (t) - F (c)) d t\|}{\|Y - X\|} = \frac{\|\int_{(X, Y)} (F (t) - F (c)) d t\|}{Y - X}$
141	132 133 140	3eqtrd	$⊢ (φ \land X < Y) \to \|(\frac{G (Y) - G (X)}{Y - X}) - F (c)\| = \frac{\|\int_{(X, Y)} (F (t) - F (c)) d t\|}{Y - X}$
142	83	abscld	$⊢ (φ \land X < Y) \to \|\int_{(X, Y)} (F (t) - F (c)) d t\| \in ℝ$
143	102	abscld	$⊢ (φ \land t \in (X, Y)) \to \|F (t) - F (c)\| \in ℝ$
144		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to ℂ \underset{cn}{⟶} ℝ \subseteq ℂ \underset{cn}{⟶} ℂ$
145	72 74 144	mp2an	$⊢ ℂ \underset{cn}{⟶} ℝ \subseteq ℂ \underset{cn}{⟶} ℂ$
146		abscncf	$⊢ abs : ℂ \underset{cn}{⟶} ℝ$
147	145 146	sselii	$⊢ abs : ℂ \underset{cn}{⟶} ℂ$
148	147	a1i	$⊢ φ \to abs : ℂ \underset{cn}{⟶} ℂ$
149	148 78	cncfmpt1f	$⊢ φ \to (t \in (X, Y) ⟼ \|F (t) - F (c)\|) : (X, Y) \underset{cn}{⟶} ℂ$
150		cnmbf	$⊢ ((X, Y) \in dom vol \land (t \in (X, Y) ⟼ \|F (t) - F (c)\|) : (X, Y) \underset{cn}{⟶} ℂ) \to (t \in (X, Y) ⟼ \|F (t) - F (c)\|) \in MblFn$
151	32 149 150	sylancr	$⊢ φ \to (t \in (X, Y) ⟼ \|F (t) - F (c)\|) \in MblFn$
152	16 81 151	iblabsnc	$⊢ φ \to (t \in (X, Y) ⟼ \|F (t) - F (c)\|) \in 𝐿^{1}$
153	143 152	itgrecl	$⊢ φ \to \int_{(X, Y)} \|F (t) - F (c)\| d t \in ℝ$
154	153	adantr	$⊢ (φ \land X < Y) \to \int_{(X, Y)} \|F (t) - F (c)\| d t \in ℝ$
155	9	rpred	$⊢ φ \to E \in ℝ$
156	84 155	remulcld	$⊢ φ \to (Y - X) E \in ℝ$
157	156	adantr	$⊢ (φ \land X < Y) \to (Y - X) E \in ℝ$
158	82	cjcld	$⊢ φ \to \overline{\int_{(X, Y)} (F (t) - F (c)) d t} \in ℂ$
159		cncfmptc	$⊢ (\overline{\int_{(X, Y)} (F (t) - F (c)) d t} \in ℂ \land (X, Y) \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in (X, Y) ⟼ \overline{\int_{(X, Y)} (F (t) - F (c)) d t}) : (X, Y) \underset{cn}{⟶} ℂ$
160	73 74 159	mp3an23	$⊢ \overline{\int_{(X, Y)} (F (t) - F (c)) d t} \in ℂ \to (x \in (X, Y) ⟼ \overline{\int_{(X, Y)} (F (t) - F (c)) d t}) : (X, Y) \underset{cn}{⟶} ℂ$
161	158 160	syl	$⊢ φ \to (x \in (X, Y) ⟼ \overline{\int_{(X, Y)} (F (t) - F (c)) d t}) : (X, Y) \underset{cn}{⟶} ℂ$
162		nfcv	$⊢ \underline{Ⅎ} x (F (t) - F (c))$
163		nfcsb1v	$⊢ \underline{Ⅎ} t ⦋ x / t ⦌ (F (t) - F (c))$
164		csbeq1a	$⊢ t = x \to F (t) - F (c) = ⦋ x / t ⦌ (F (t) - F (c))$
165	162 163 164	cbvmpt	$⊢ (t \in (X, Y) ⟼ F (t) - F (c)) = (x \in (X, Y) ⟼ ⦋ x / t ⦌ (F (t) - F (c)))$
166	165 78	eqeltrrid	$⊢ φ \to (x \in (X, Y) ⟼ ⦋ x / t ⦌ (F (t) - F (c))) : (X, Y) \underset{cn}{⟶} ℂ$
167	161 166	mulcncf	$⊢ φ \to (x \in (X, Y) ⟼ \overline{\int_{(X, Y)} (F (t) - F (c)) d t} ⦋ x / t ⦌ (F (t) - F (c))) : (X, Y) \underset{cn}{⟶} ℂ$
168		cnmbf	$⊢ ((X, Y) \in dom vol \land (x \in (X, Y) ⟼ \overline{\int_{(X, Y)} (F (t) - F (c)) d t} ⦋ x / t ⦌ (F (t) - F (c))) : (X, Y) \underset{cn}{⟶} ℂ) \to (x \in (X, Y) ⟼ \overline{\int_{(X, Y)} (F (t) - F (c)) d t} ⦋ x / t ⦌ (F (t) - F (c))) \in MblFn$
169	32 167 168	sylancr	$⊢ φ \to (x \in (X, Y) ⟼ \overline{\int_{(X, Y)} (F (t) - F (c)) d t} ⦋ x / t ⦌ (F (t) - F (c))) \in MblFn$
170	102 81 151 169	itgabsnc	$⊢ φ \to \|\int_{(X, Y)} (F (t) - F (c)) d t\| \leq \int_{(X, Y)} \|F (t) - F (c)\| d t$
171	170	adantr	$⊢ (φ \land X < Y) \to \|\int_{(X, Y)} (F (t) - F (c)) d t\| \leq \int_{(X, Y)} \|F (t) - F (c)\| d t$
172		simpr	$⊢ (φ \land X < Y) \to X < Y$
173	155	adantr	$⊢ (φ \land t \in (X, Y)) \to E \in ℝ$
174		fconstmpt	$⊢ (X, Y) \times \{E\} = (t \in (X, Y) ⟼ E)$
175	9	rpcnd	$⊢ φ \to E \in ℂ$
176		iblconst	$⊢ ((X, Y) \in dom vol \land vol ((X, Y)) \in ℝ \land E \in ℂ) \to (X, Y) \times \{E\} \in 𝐿^{1}$
177	33 60 175 176	syl3anc	$⊢ φ \to (X, Y) \times \{E\} \in 𝐿^{1}$
178	174 177	eqeltrrid	$⊢ φ \to (t \in (X, Y) ⟼ E) \in 𝐿^{1}$
179		cncfmptc	$⊢ (E \in ℂ \land (X, Y) \subseteq ℂ \land ℂ \subseteq ℂ) \to (t \in (X, Y) ⟼ E) : (X, Y) \underset{cn}{⟶} ℂ$
180	73 74 179	mp3an23	$⊢ E \in ℂ \to (t \in (X, Y) ⟼ E) : (X, Y) \underset{cn}{⟶} ℂ$
181	175 180	syl	$⊢ φ \to (t \in (X, Y) ⟼ E) : (X, Y) \underset{cn}{⟶} ℂ$
182	64 66 181 149	cncfmpt2f	$⊢ φ \to (t \in (X, Y) ⟼ E - \|F (t) - F (c)\|) : (X, Y) \underset{cn}{⟶} ℂ$
183		cnmbf	$⊢ ((X, Y) \in dom vol \land (t \in (X, Y) ⟼ E - \|F (t) - F (c)\|) : (X, Y) \underset{cn}{⟶} ℂ) \to (t \in (X, Y) ⟼ E - \|F (t) - F (c)\|) \in MblFn$
184	32 182 183	sylancr	$⊢ φ \to (t \in (X, Y) ⟼ E - \|F (t) - F (c)\|) \in MblFn$
185	173 178 143 152 184	iblsubnc	$⊢ φ \to (t \in (X, Y) ⟼ E - \|F (t) - F (c)\|) \in 𝐿^{1}$
186	185	adantr	$⊢ (φ \land X < Y) \to (t \in (X, Y) ⟼ E - \|F (t) - F (c)\|) \in 𝐿^{1}$
187	11	ralrimiva	$⊢ φ \to \forall y \in (A, B) (\|y - c\| < R \to \|F (y) - F (c)\| < E)$
188	187	adantr	$⊢ (φ \land t \in (X, Y)) \to \forall y \in (A, B) (\|y - c\| < R \to \|F (y) - F (c)\| < E)$
189	96 7	sselid	$⊢ φ \to c \in ℝ$
190	10	rpred	$⊢ φ \to R \in ℝ$
191	189 190	resubcld	$⊢ φ \to c - R \in ℝ$
192	191	adantr	$⊢ (φ \land t \in (X, Y)) \to c - R \in ℝ$
193	47	adantr	$⊢ (φ \land t \in (X, Y)) \to X \in ℝ$
194		elioore	$⊢ t \in (X, Y) \to t \in ℝ$
195	194	adantl	$⊢ (φ \land t \in (X, Y)) \to t \in ℝ$
196	47 189 190	absdifltd	$⊢ φ \to (\|X - c\| < R \leftrightarrow (c - R < X \land X < c + R))$
197	13 196	mpbid	$⊢ φ \to (c - R < X \land X < c + R)$
198	197	simpld	$⊢ φ \to c - R < X$
199	198	adantr	$⊢ (φ \land t \in (X, Y)) \to c - R < X$
200		eliooord	$⊢ t \in (X, Y) \to (X < t \land t < Y)$
201	200	adantl	$⊢ (φ \land t \in (X, Y)) \to (X < t \land t < Y)$
202	201	simpld	$⊢ (φ \land t \in (X, Y)) \to X < t$
203	192 193 195 199 202	lttrd	$⊢ (φ \land t \in (X, Y)) \to c - R < t$
204	48	adantr	$⊢ (φ \land t \in (X, Y)) \to Y \in ℝ$
205	189 190	readdcld	$⊢ φ \to c + R \in ℝ$
206	205	adantr	$⊢ (φ \land t \in (X, Y)) \to c + R \in ℝ$
207	201	simprd	$⊢ (φ \land t \in (X, Y)) \to t < Y$
208	48 189 190	absdifltd	$⊢ φ \to (\|Y - c\| < R \leftrightarrow (c - R < Y \land Y < c + R))$
209	15 208	mpbid	$⊢ φ \to (c - R < Y \land Y < c + R)$
210	209	simprd	$⊢ φ \to Y < c + R$
211	210	adantr	$⊢ (φ \land t \in (X, Y)) \to Y < c + R$
212	195 204 206 207 211	lttrd	$⊢ (φ \land t \in (X, Y)) \to t < c + R$
213	189	adantr	$⊢ (φ \land t \in (X, Y)) \to c \in ℝ$
214	190	adantr	$⊢ (φ \land t \in (X, Y)) \to R \in ℝ$
215	195 213 214	absdifltd	$⊢ (φ \land t \in (X, Y)) \to (\|t - c\| < R \leftrightarrow (c - R < t \land t < c + R))$
216	203 212 215	mpbir2and	$⊢ (φ \land t \in (X, Y)) \to \|t - c\| < R$
217		fvoveq1	$⊢ y = t \to \|y - c\| = \|t - c\|$
218	217	breq1d	$⊢ y = t \to (\|y - c\| < R \leftrightarrow \|t - c\| < R)$
219	218	imbrov2fvoveq	$⊢ y = t \to ((\|y - c\| < R \to \|F (y) - F (c)\| < E) \leftrightarrow (\|t - c\| < R \to \|F (t) - F (c)\| < E))$
220	219	rspcv	$⊢ t \in (A, B) \to (\forall y \in (A, B) (\|y - c\| < R \to \|F (y) - F (c)\| < E) \to (\|t - c\| < R \to \|F (t) - F (c)\| < E))$
221	27 188 216 220	syl3c	$⊢ (φ \land t \in (X, Y)) \to \|F (t) - F (c)\| < E$
222		difrp	$⊢ (\|F (t) - F (c)\| \in ℝ \land E \in ℝ) \to (\|F (t) - F (c)\| < E \leftrightarrow E - \|F (t) - F (c)\| \in ℝ^{+})$
223	143 173 222	syl2anc	$⊢ (φ \land t \in (X, Y)) \to (\|F (t) - F (c)\| < E \leftrightarrow E - \|F (t) - F (c)\| \in ℝ^{+})$
224	221 223	mpbid	$⊢ (φ \land t \in (X, Y)) \to E - \|F (t) - F (c)\| \in ℝ^{+}$
225	224	adantlr	$⊢ ((φ \land X < Y) \land t \in (X, Y)) \to E - \|F (t) - F (c)\| \in ℝ^{+}$
226	182	adantr	$⊢ (φ \land X < Y) \to (t \in (X, Y) ⟼ E - \|F (t) - F (c)\|) : (X, Y) \underset{cn}{⟶} ℂ$
227	172 186 225 226	itggt0cn	$⊢ (φ \land X < Y) \to 0 < \int_{(X, Y)} (E - \|F (t) - F (c)\|) d t$
228	173 178 143 152 184	itgsubnc	$⊢ φ \to \int_{(X, Y)} (E - \|F (t) - F (c)\|) d t = \int_{(X, Y)} E d t - \int_{(X, Y)} \|F (t) - F (c)\| d t$
229	228	adantr	$⊢ (φ \land X < Y) \to \int_{(X, Y)} (E - \|F (t) - F (c)\|) d t = \int_{(X, Y)} E d t - \int_{(X, Y)} \|F (t) - F (c)\| d t$
230		itgconst	$⊢ ((X, Y) \in dom vol \land vol ((X, Y)) \in ℝ \land E \in ℂ) \to \int_{(X, Y)} E d t = E vol ((X, Y))$
231	33 60 175 230	syl3anc	$⊢ φ \to \int_{(X, Y)} E d t = E vol ((X, Y))$
232	231	adantr	$⊢ (φ \land X < Y) \to \int_{(X, Y)} E d t = E vol ((X, Y))$
233	120	oveq2d	$⊢ (φ \land X < Y) \to E vol ((X, Y)) = E (Y - X)$
234	175 85	mulcomd	$⊢ φ \to E (Y - X) = (Y - X) E$
235	234	adantr	$⊢ (φ \land X < Y) \to E (Y - X) = (Y - X) E$
236	232 233 235	3eqtrd	$⊢ (φ \land X < Y) \to \int_{(X, Y)} E d t = (Y - X) E$
237	236	oveq1d	$⊢ (φ \land X < Y) \to \int_{(X, Y)} E d t - \int_{(X, Y)} \|F (t) - F (c)\| d t = (Y - X) E - \int_{(X, Y)} \|F (t) - F (c)\| d t$
238	229 237	eqtrd	$⊢ (φ \land X < Y) \to \int_{(X, Y)} (E - \|F (t) - F (c)\|) d t = (Y - X) E - \int_{(X, Y)} \|F (t) - F (c)\| d t$
239	227 238	breqtrd	$⊢ (φ \land X < Y) \to 0 < (Y - X) E - \int_{(X, Y)} \|F (t) - F (c)\| d t$
240	153 156	posdifd	$⊢ φ \to (\int_{(X, Y)} \|F (t) - F (c)\| d t < (Y - X) E \leftrightarrow 0 < (Y - X) E - \int_{(X, Y)} \|F (t) - F (c)\| d t)$
241	240	biimpar	$⊢ (φ \land 0 < (Y - X) E - \int_{(X, Y)} \|F (t) - F (c)\| d t) \to \int_{(X, Y)} \|F (t) - F (c)\| d t < (Y - X) E$
242	239 241	syldan	$⊢ (φ \land X < Y) \to \int_{(X, Y)} \|F (t) - F (c)\| d t < (Y - X) E$
243	142 154 157 171 242	lelttrd	$⊢ (φ \land X < Y) \to \|\int_{(X, Y)} (F (t) - F (c)) d t\| < (Y - X) E$
244	155	adantr	$⊢ (φ \land X < Y) \to E \in ℝ$
245		ltdivmul	$⊢ (\|\int_{(X, Y)} (F (t) - F (c)) d t\| \in ℝ \land E \in ℝ \land (Y - X \in ℝ \land 0 < Y - X)) \to (\frac{\|\int_{(X, Y)} (F (t) - F (c)) d t\|}{Y - X} < E \leftrightarrow \|\int_{(X, Y)} (F (t) - F (c)) d t\| < (Y - X) E)$
246	142 244 134 88 245	syl112anc	$⊢ (φ \land X < Y) \to (\frac{\|\int_{(X, Y)} (F (t) - F (c)) d t\|}{Y - X} < E \leftrightarrow \|\int_{(X, Y)} (F (t) - F (c)) d t\| < (Y - X) E)$
247	243 246	mpbird	$⊢ (φ \land X < Y) \to \frac{\|\int_{(X, Y)} (F (t) - F (c)) d t\|}{Y - X} < E$
248	141 247	eqbrtrd	$⊢ (φ \land X < Y) \to \|(\frac{G (Y) - G (X)}{Y - X}) - F (c)\| < E$

Metamath Proof Explorer

Theorem ftc1cnnclem

Proof