ftc1lem4

	Ref	Expression
Hypotheses	ftc1.g	$⊢ G = (x \in [A, B] ⟼ \int_{(A, x)} F (t) d t)$
	ftc1.a	$⊢ φ \to A \in ℝ$
	ftc1.b	$⊢ φ \to B \in ℝ$
	ftc1.le	$⊢ φ \to A \leq B$
	ftc1.s	$⊢ φ \to (A, B) \subseteq D$
	ftc1.d	$⊢ φ \to D \subseteq ℝ$
	ftc1.i	$⊢ φ \to F \in 𝐿^{1}$
	ftc1.c	$⊢ φ \to C \in (A, B)$
	ftc1.f	$⊢ φ \to F \in (K CnP L) (C)$
	ftc1.j	$⊢ J = L ↾_{𝑡} ℝ$
	ftc1.k	$⊢ K = L ↾_{𝑡} D$
	ftc1.l	$⊢ L = TopOpen (ℂ_{fld})$
	ftc1.h	$⊢ H = (z \in ([A, B] ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C})$
	ftc1.e	$⊢ φ \to E \in ℝ^{+}$
	ftc1.r	$⊢ φ \to R \in ℝ^{+}$
	ftc1.fc	$⊢ (φ \land y \in D) \to (\|y - C\| < R \to \|F (y) - F (C)\| < E)$
	ftc1.x1	$⊢ φ \to X \in [A, B]$
	ftc1.x2	$⊢ φ \to \|X - C\| < R$
	ftc1.y1	$⊢ φ \to Y \in [A, B]$
	ftc1.y2	$⊢ φ \to \|Y - C\| < R$
Assertion	ftc1lem4	$⊢ (φ \land X < Y) \to \|(\frac{G (Y) - G (X)}{Y - X}) - F (C)\| < E$

Proof

Step	Hyp	Ref	Expression
1		ftc1.g	$⊢ G = (x \in [A, B] ⟼ \int_{(A, x)} F (t) d t)$
2		ftc1.a	$⊢ φ \to A \in ℝ$
3		ftc1.b	$⊢ φ \to B \in ℝ$
4		ftc1.le	$⊢ φ \to A \leq B$
5		ftc1.s	$⊢ φ \to (A, B) \subseteq D$
6		ftc1.d	$⊢ φ \to D \subseteq ℝ$
7		ftc1.i	$⊢ φ \to F \in 𝐿^{1}$
8		ftc1.c	$⊢ φ \to C \in (A, B)$
9		ftc1.f	$⊢ φ \to F \in (K CnP L) (C)$
10		ftc1.j	$⊢ J = L ↾_{𝑡} ℝ$
11		ftc1.k	$⊢ K = L ↾_{𝑡} D$
12		ftc1.l	$⊢ L = TopOpen (ℂ_{fld})$
13		ftc1.h	$⊢ H = (z \in ([A, B] ∖ \{C\}) ⟼ \frac{G (z) - G (C)}{z - C})$
14		ftc1.e	$⊢ φ \to E \in ℝ^{+}$
15		ftc1.r	$⊢ φ \to R \in ℝ^{+}$
16		ftc1.fc	$⊢ (φ \land y \in D) \to (\|y - C\| < R \to \|F (y) - F (C)\| < E)$
17		ftc1.x1	$⊢ φ \to X \in [A, B]$
18		ftc1.x2	$⊢ φ \to \|X - C\| < R$
19		ftc1.y1	$⊢ φ \to Y \in [A, B]$
20		ftc1.y2	$⊢ φ \to \|Y - C\| < R$
21		ovexd	$⊢ (φ \land t \in (X, Y)) \to F (t) - F (C) \in V$
22	2	rexrd	$⊢ φ \to A \in ℝ^{*}$
23		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (X \in [A, B] \leftrightarrow (X \in ℝ \land A \leq X \land X \leq B))$
24	2 3 23	syl2anc	$⊢ φ \to (X \in [A, B] \leftrightarrow (X \in ℝ \land A \leq X \land X \leq B))$
25	17 24	mpbid	$⊢ φ \to (X \in ℝ \land A \leq X \land X \leq B)$
26	25	simp2d	$⊢ φ \to A \leq X$
27		iooss1	$⊢ (A \in ℝ^{*} \land A \leq X) \to (X, Y) \subseteq (A, Y)$
28	22 26 27	syl2anc	$⊢ φ \to (X, Y) \subseteq (A, Y)$
29	3	rexrd	$⊢ φ \to B \in ℝ^{*}$
30		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (Y \in [A, B] \leftrightarrow (Y \in ℝ \land A \leq Y \land Y \leq B))$
31	2 3 30	syl2anc	$⊢ φ \to (Y \in [A, B] \leftrightarrow (Y \in ℝ \land A \leq Y \land Y \leq B))$
32	19 31	mpbid	$⊢ φ \to (Y \in ℝ \land A \leq Y \land Y \leq B)$
33	32	simp3d	$⊢ φ \to Y \leq B$
34		iooss2	$⊢ (B \in ℝ^{*} \land Y \leq B) \to (A, Y) \subseteq (A, B)$
35	29 33 34	syl2anc	$⊢ φ \to (A, Y) \subseteq (A, B)$
36	28 35	sstrd	$⊢ φ \to (X, Y) \subseteq (A, B)$
37	36 5	sstrd	$⊢ φ \to (X, Y) \subseteq D$
38	37	sselda	$⊢ (φ \land t \in (X, Y)) \to t \in D$
39	1 2 3 4 5 6 7 8 9 10 11 12	ftc1lem3	$⊢ φ \to F : D ⟶ ℂ$
40	39	ffvelcdmda	$⊢ (φ \land t \in D) \to F (t) \in ℂ$
41	38 40	syldan	$⊢ (φ \land t \in (X, Y)) \to F (t) \in ℂ$
42		ioombl	$⊢ (X, Y) \in dom vol$
43	42	a1i	$⊢ φ \to (X, Y) \in dom vol$
44		fvexd	$⊢ (φ \land t \in D) \to F (t) \in V$
45	39	feqmptd	$⊢ φ \to F = (t \in D ⟼ F (t))$
46	45 7	eqeltrrd	$⊢ φ \to (t \in D ⟼ F (t)) \in 𝐿^{1}$
47	37 43 44 46	iblss	$⊢ φ \to (t \in (X, Y) ⟼ F (t)) \in 𝐿^{1}$
48	5 8	sseldd	$⊢ φ \to C \in D$
49	39 48	ffvelcdmd	$⊢ φ \to F (C) \in ℂ$
50	49	adantr	$⊢ (φ \land t \in (X, Y)) \to F (C) \in ℂ$
51		fconstmpt	$⊢ (X, Y) \times \{F (C)\} = (t \in (X, Y) ⟼ F (C))$
52		mblvol	$⊢ (X, Y) \in dom vol \to vol ((X, Y)) = {vol}^{*} ((X, Y))$
53	42 52	ax-mp	$⊢ vol ((X, Y)) = {vol}^{*} ((X, Y))$
54		ioossicc	$⊢ (X, Y) \subseteq [X, Y]$
55	54	a1i	$⊢ φ \to (X, Y) \subseteq [X, Y]$
56		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
57	2 3 56	syl2anc	$⊢ φ \to [A, B] \subseteq ℝ$
58	57 17	sseldd	$⊢ φ \to X \in ℝ$
59	57 19	sseldd	$⊢ φ \to Y \in ℝ$
60		iccmbl	$⊢ (X \in ℝ \land Y \in ℝ) \to [X, Y] \in dom vol$
61	58 59 60	syl2anc	$⊢ φ \to [X, Y] \in dom vol$
62		mblss	$⊢ [X, Y] \in dom vol \to [X, Y] \subseteq ℝ$
63	61 62	syl	$⊢ φ \to [X, Y] \subseteq ℝ$
64		mblvol	$⊢ [X, Y] \in dom vol \to vol ([X, Y]) = {vol}^{*} ([X, Y])$
65	61 64	syl	$⊢ φ \to vol ([X, Y]) = {vol}^{*} ([X, Y])$
66		iccvolcl	$⊢ (X \in ℝ \land Y \in ℝ) \to vol ([X, Y]) \in ℝ$
67	58 59 66	syl2anc	$⊢ φ \to vol ([X, Y]) \in ℝ$
68	65 67	eqeltrrd	$⊢ φ \to {vol}^{*} ([X, Y]) \in ℝ$
69		ovolsscl	$⊢ ((X, Y) \subseteq [X, Y] \land [X, Y] \subseteq ℝ \land {vol}^{} ([X, Y]) \in ℝ) \to {vol}^{} ((X, Y)) \in ℝ$
70	55 63 68 69	syl3anc	$⊢ φ \to {vol}^{*} ((X, Y)) \in ℝ$
71	53 70	eqeltrid	$⊢ φ \to vol ((X, Y)) \in ℝ$
72		iblconst	$⊢ ((X, Y) \in dom vol \land vol ((X, Y)) \in ℝ \land F (C) \in ℂ) \to (X, Y) \times \{F (C)\} \in 𝐿^{1}$
73	43 71 49 72	syl3anc	$⊢ φ \to (X, Y) \times \{F (C)\} \in 𝐿^{1}$
74	51 73	eqeltrrid	$⊢ φ \to (t \in (X, Y) ⟼ F (C)) \in 𝐿^{1}$
75	41 47 50 74	iblsub	$⊢ φ \to (t \in (X, Y) ⟼ F (t) - F (C)) \in 𝐿^{1}$
76	21 75	itgcl	$⊢ φ \to \int_{(X, Y)} (F (t) - F (C)) d t \in ℂ$
77	76	adantr	$⊢ (φ \land X < Y) \to \int_{(X, Y)} (F (t) - F (C)) d t \in ℂ$
78	59 58	resubcld	$⊢ φ \to Y - X \in ℝ$
79	78	adantr	$⊢ (φ \land X < Y) \to Y - X \in ℝ$
80	79	recnd	$⊢ (φ \land X < Y) \to Y - X \in ℂ$
81	58 59	posdifd	$⊢ φ \to (X < Y \leftrightarrow 0 < Y - X)$
82	81	biimpa	$⊢ (φ \land X < Y) \to 0 < Y - X$
83	82	gt0ne0d	$⊢ (φ \land X < Y) \to Y - X \neq 0$
84	77 80 83	divcld	$⊢ (φ \land X < Y) \to \frac{\int_{(X, Y)} (F (t) - F (C)) d t}{Y - X} \in ℂ$
85	49	adantr	$⊢ (φ \land X < Y) \to F (C) \in ℂ$
86		ltle	$⊢ (X \in ℝ \land Y \in ℝ) \to (X < Y \to X \leq Y)$
87	58 59 86	syl2anc	$⊢ φ \to (X < Y \to X \leq Y)$
88	87	imp	$⊢ (φ \land X < Y) \to X \leq Y$
89	1 2 3 4 5 6 7 39 17 19	ftc1lem1	$⊢ (φ \land X \leq Y) \to G (Y) - G (X) = \int_{(X, Y)} F (t) d t$
90	88 89	syldan	$⊢ (φ \land X < Y) \to G (Y) - G (X) = \int_{(X, Y)} F (t) d t$
91	41 50	npcand	$⊢ (φ \land t \in (X, Y)) \to F (t) - F (C) + F (C) = F (t)$
92	91	itgeq2dv	$⊢ φ \to \int_{(X, Y)} (F (t) - F (C) + F (C)) d t = \int_{(X, Y)} F (t) d t$
93	41 50	subcld	$⊢ (φ \land t \in (X, Y)) \to F (t) - F (C) \in ℂ$
94	93 75 50 74	itgadd	$⊢ φ \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$
95	92 94	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$
96	95	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$
97		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))$
98	43 71 49 97	syl3anc	$⊢ φ \to \int_{(X, Y)} F (C) d t = F (C) vol ((X, Y))$
99	98	adantr	$⊢ (φ \land X < Y) \to \int_{(X, Y)} F (C) d t = F (C) vol ((X, Y))$
100	58	adantr	$⊢ (φ \land X < Y) \to X \in ℝ$
101	59	adantr	$⊢ (φ \land X < Y) \to Y \in ℝ$
102		ovolioo	$⊢ (X \in ℝ \land Y \in ℝ \land X \leq Y) \to {vol}^{*} ((X, Y)) = Y - X$
103	100 101 88 102	syl3anc	$⊢ (φ \land X < Y) \to {vol}^{*} ((X, Y)) = Y - X$
104	53 103	eqtrid	$⊢ (φ \land X < Y) \to vol ((X, Y)) = Y - X$
105	104	oveq2d	$⊢ (φ \land X < Y) \to F (C) vol ((X, Y)) = F (C) (Y - X)$
106	99 105	eqtrd	$⊢ (φ \land X < Y) \to \int_{(X, Y)} F (C) d t = F (C) (Y - X)$
107	106	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)$
108	90 96 107	3eqtrd	$⊢ (φ \land X < Y) \to G (Y) - G (X) = \int_{(X, Y)} (F (t) - F (C)) d t + F (C) (Y - X)$
109	108	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}$
110	85 80	mulcld	$⊢ (φ \land X < Y) \to F (C) (Y - X) \in ℂ$
111	77 110 80 83	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})$
112	85 80 83	divcan4d	$⊢ (φ \land X < Y) \to \frac{F (C) (Y - X)}{Y - X} = F (C)$
113	112	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)$
114	109 111 113	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)$
115	84 85 114	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}$
116	115	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}\|$
117	77 80 83	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\|}$
118		0re	$⊢ 0 \in ℝ$
119		ltle	$⊢ (0 \in ℝ \land Y - X \in ℝ) \to (0 < Y - X \to 0 \leq Y - X)$
120	118 79 119	sylancr	$⊢ (φ \land X < Y) \to (0 < Y - X \to 0 \leq Y - X)$
121	82 120	mpd	$⊢ (φ \land X < Y) \to 0 \leq Y - X$
122	79 121	absidd	$⊢ (φ \land X < Y) \to \|Y - X\| = Y - X$
123	122	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}$
124	116 117 123	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}$
125	76	abscld	$⊢ φ \to \|\int_{(X, Y)} (F (t) - F (C)) d t\| \in ℝ$
126	125	adantr	$⊢ (φ \land X < Y) \to \|\int_{(X, Y)} (F (t) - F (C)) d t\| \in ℝ$
127	93	abscld	$⊢ (φ \land t \in (X, Y)) \to \|F (t) - F (C)\| \in ℝ$
128	21 75	iblabs	$⊢ φ \to (t \in (X, Y) ⟼ \|F (t) - F (C)\|) \in 𝐿^{1}$
129	127 128	itgrecl	$⊢ φ \to \int_{(X, Y)} \|F (t) - F (C)\| d t \in ℝ$
130	129	adantr	$⊢ (φ \land X < Y) \to \int_{(X, Y)} \|F (t) - F (C)\| d t \in ℝ$
131	14	rpred	$⊢ φ \to E \in ℝ$
132	78 131	remulcld	$⊢ φ \to (Y - X) E \in ℝ$
133	132	adantr	$⊢ (φ \land X < Y) \to (Y - X) E \in ℝ$
134	93 75	itgabs	$⊢ φ \to \|\int_{(X, Y)} (F (t) - F (C)) d t\| \leq \int_{(X, Y)} \|F (t) - F (C)\| d t$
135	134	adantr	$⊢ (φ \land X < Y) \to \|\int_{(X, Y)} (F (t) - F (C)) d t\| \leq \int_{(X, Y)} \|F (t) - F (C)\| d t$
136	82 104	breqtrrd	$⊢ (φ \land X < Y) \to 0 < vol ((X, Y))$
137	131	adantr	$⊢ (φ \land t \in (X, Y)) \to E \in ℝ$
138		fconstmpt	$⊢ (X, Y) \times \{E\} = (t \in (X, Y) ⟼ E)$
139	131	recnd	$⊢ φ \to E \in ℂ$
140		iblconst	$⊢ ((X, Y) \in dom vol \land vol ((X, Y)) \in ℝ \land E \in ℂ) \to (X, Y) \times \{E\} \in 𝐿^{1}$
141	43 71 139 140	syl3anc	$⊢ φ \to (X, Y) \times \{E\} \in 𝐿^{1}$
142	138 141	eqeltrrid	$⊢ φ \to (t \in (X, Y) ⟼ E) \in 𝐿^{1}$
143	137 142 127 128	iblsub	$⊢ φ \to (t \in (X, Y) ⟼ E - \|F (t) - F (C)\|) \in 𝐿^{1}$
144	143	adantr	$⊢ (φ \land X < Y) \to (t \in (X, Y) ⟼ E - \|F (t) - F (C)\|) \in 𝐿^{1}$
145	6 48	sseldd	$⊢ φ \to C \in ℝ$
146	15	rpred	$⊢ φ \to R \in ℝ$
147	145 146	resubcld	$⊢ φ \to C - R \in ℝ$
148	147	adantr	$⊢ (φ \land t \in (X, Y)) \to C - R \in ℝ$
149	58	adantr	$⊢ (φ \land t \in (X, Y)) \to X \in ℝ$
150	37 6	sstrd	$⊢ φ \to (X, Y) \subseteq ℝ$
151	150	sselda	$⊢ (φ \land t \in (X, Y)) \to t \in ℝ$
152	58 145 146	absdifltd	$⊢ φ \to (\|X - C\| < R \leftrightarrow (C - R < X \land X < C + R))$
153	18 152	mpbid	$⊢ φ \to (C - R < X \land X < C + R)$
154	153	simpld	$⊢ φ \to C - R < X$
155	154	adantr	$⊢ (φ \land t \in (X, Y)) \to C - R < X$
156		eliooord	$⊢ t \in (X, Y) \to (X < t \land t < Y)$
157	156	adantl	$⊢ (φ \land t \in (X, Y)) \to (X < t \land t < Y)$
158	157	simpld	$⊢ (φ \land t \in (X, Y)) \to X < t$
159	148 149 151 155 158	lttrd	$⊢ (φ \land t \in (X, Y)) \to C - R < t$
160	59	adantr	$⊢ (φ \land t \in (X, Y)) \to Y \in ℝ$
161	145 146	readdcld	$⊢ φ \to C + R \in ℝ$
162	161	adantr	$⊢ (φ \land t \in (X, Y)) \to C + R \in ℝ$
163	157	simprd	$⊢ (φ \land t \in (X, Y)) \to t < Y$
164	59 145 146	absdifltd	$⊢ φ \to (\|Y - C\| < R \leftrightarrow (C - R < Y \land Y < C + R))$
165	20 164	mpbid	$⊢ φ \to (C - R < Y \land Y < C + R)$
166	165	simprd	$⊢ φ \to Y < C + R$
167	166	adantr	$⊢ (φ \land t \in (X, Y)) \to Y < C + R$
168	151 160 162 163 167	lttrd	$⊢ (φ \land t \in (X, Y)) \to t < C + R$
169	145	adantr	$⊢ (φ \land t \in (X, Y)) \to C \in ℝ$
170	146	adantr	$⊢ (φ \land t \in (X, Y)) \to R \in ℝ$
171	151 169 170	absdifltd	$⊢ (φ \land t \in (X, Y)) \to (\|t - C\| < R \leftrightarrow (C - R < t \land t < C + R))$
172	159 168 171	mpbir2and	$⊢ (φ \land t \in (X, Y)) \to \|t - C\| < R$
173		fvoveq1	$⊢ y = t \to \|y - C\| = \|t - C\|$
174	173	breq1d	$⊢ y = t \to (\|y - C\| < R \leftrightarrow \|t - C\| < R)$
175	174	imbrov2fvoveq	$⊢ y = t \to ((\|y - C\| < R \to \|F (y) - F (C)\| < E) \leftrightarrow (\|t - C\| < R \to \|F (t) - F (C)\| < E))$
176	16	ralrimiva	$⊢ φ \to \forall y \in D (\|y - C\| < R \to \|F (y) - F (C)\| < E)$
177	176	adantr	$⊢ (φ \land t \in (X, Y)) \to \forall y \in D (\|y - C\| < R \to \|F (y) - F (C)\| < E)$
178	175 177 38	rspcdva	$⊢ (φ \land t \in (X, Y)) \to (\|t - C\| < R \to \|F (t) - F (C)\| < E)$
179	172 178	mpd	$⊢ (φ \land t \in (X, Y)) \to \|F (t) - F (C)\| < E$
180		difrp	$⊢ (\|F (t) - F (C)\| \in ℝ \land E \in ℝ) \to (\|F (t) - F (C)\| < E \leftrightarrow E - \|F (t) - F (C)\| \in ℝ^{+})$
181	127 137 180	syl2anc	$⊢ (φ \land t \in (X, Y)) \to (\|F (t) - F (C)\| < E \leftrightarrow E - \|F (t) - F (C)\| \in ℝ^{+})$
182	179 181	mpbid	$⊢ (φ \land t \in (X, Y)) \to E - \|F (t) - F (C)\| \in ℝ^{+}$
183	182	adantlr	$⊢ ((φ \land X < Y) \land t \in (X, Y)) \to E - \|F (t) - F (C)\| \in ℝ^{+}$
184	136 144 183	itggt0	$⊢ (φ \land X < Y) \to 0 < \int_{(X, Y)} (E - \|F (t) - F (C)\|) d t$
185	137 142 127 128	itgsub	$⊢ φ \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$
186	185	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$
187		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))$
188	43 71 139 187	syl3anc	$⊢ φ \to \int_{(X, Y)} E d t = E vol ((X, Y))$
189	188	adantr	$⊢ (φ \land X < Y) \to \int_{(X, Y)} E d t = E vol ((X, Y))$
190	104	oveq2d	$⊢ (φ \land X < Y) \to E vol ((X, Y)) = E (Y - X)$
191	78	recnd	$⊢ φ \to Y - X \in ℂ$
192	139 191	mulcomd	$⊢ φ \to E (Y - X) = (Y - X) E$
193	192	adantr	$⊢ (φ \land X < Y) \to E (Y - X) = (Y - X) E$
194	189 190 193	3eqtrd	$⊢ (φ \land X < Y) \to \int_{(X, Y)} E d t = (Y - X) E$
195	194	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$
196	186 195	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$
197	184 196	breqtrd	$⊢ (φ \land X < Y) \to 0 < (Y - X) E - \int_{(X, Y)} \|F (t) - F (C)\| d t$
198	129 132	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)$
199	198	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$
200	197 199	syldan	$⊢ (φ \land X < Y) \to \int_{(X, Y)} \|F (t) - F (C)\| d t < (Y - X) E$
201	126 130 133 135 200	lelttrd	$⊢ (φ \land X < Y) \to \|\int_{(X, Y)} (F (t) - F (C)) d t\| < (Y - X) E$
202	77	abscld	$⊢ (φ \land X < Y) \to \|\int_{(X, Y)} (F (t) - F (C)) d t\| \in ℝ$
203	131	adantr	$⊢ (φ \land X < Y) \to E \in ℝ$
204		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)$
205	202 203 79 82 204	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)$
206	201 205	mpbird	$⊢ (φ \land X < Y) \to \frac{\|\int_{(X, Y)} (F (t) - F (C)) d t\|}{Y - X} < E$
207	124 206	eqbrtrd	$⊢ (φ \land X < Y) \to \|(\frac{G (Y) - G (X)}{Y - X}) - F (C)\| < E$

Metamath Proof Explorer

Theorem ftc1lem4

Proof