Theorem ftc1lem5

Description: Lemma for ftc1 . (Contributed by Mario Carneiro, 14-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016)

	Ref	Expression
Hypotheses	ftc1.g	$$⊢G=\left(x\in \left[A,B\right]⟼{\int }_{\left(A,x\right)}F\left(t\right)dt\right)$$
	ftc1.a	$$⊢\phi \to A\in ℝ$$
	ftc1.b	$$⊢\phi \to B\in ℝ$$
	ftc1.le	$$⊢\phi \to A\le B$$
	ftc1.s	$$⊢\phi \to \left(A,B\right)\subseteq D$$
	ftc1.d	$$⊢\phi \to D\subseteq ℝ$$
	ftc1.i	$$⊢\phi \to F\in {𝐿}^1$$
	ftc1.c	$$⊢\phi \to C\in \left(A,B\right)$$
	ftc1.f	$$⊢\phi \to F\in \left(K\mathrm{CnP}L\right)\left(C\right)$$
	ftc1.j	$$⊢J=L{\upharpoonright }_{𝑡}ℝ$$
	ftc1.k	$$⊢K=L{\upharpoonright }_{𝑡}D$$
	ftc1.l	$$⊢L=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	ftc1.h	$$⊢H=\left(z\in \left(\left[A,B\right]\setminus \left\{C\right\}\right)⟼\frac{G\left(z\right)-G\left(C\right)}{z-C}\right)$$
	ftc1.e	$$⊢\phi \to E\in {ℝ}^{+}$$
	ftc1.r	$$⊢\phi \to R\in {ℝ}^{+}$$
	ftc1.fc	$$⊢\left(\phi \wedge y\in D\right)\to \left(\left|y-C\right|<R\to \left|F\left(y\right)-F\left(C\right)\right|<E\right)$$
	ftc1.x1	$$⊢\phi \to X\in \left[A,B\right]$$
	ftc1.x2	$$⊢\phi \to \left|X-C\right|<R$$
Assertion	ftc1lem5	$$⊢\left(\phi \wedge X\ne C\right)\to \left|H\left(X\right)-F\left(C\right)\right|<E$$

Proof

Step	Hyp	Ref	Expression
1		ftc1.g	$$⊢G=\left(x\in \left[A,B\right]⟼{\int }_{\left(A,x\right)}F\left(t\right)dt\right)$$
2		ftc1.a	$$⊢\phi \to A\in ℝ$$
3		ftc1.b	$$⊢\phi \to B\in ℝ$$
4		ftc1.le	$$⊢\phi \to A\le B$$
5		ftc1.s	$$⊢\phi \to \left(A,B\right)\subseteq D$$
6		ftc1.d	$$⊢\phi \to D\subseteq ℝ$$
7		ftc1.i	$$⊢\phi \to F\in {𝐿}^1$$
8		ftc1.c	$$⊢\phi \to C\in \left(A,B\right)$$
9		ftc1.f	$$⊢\phi \to F\in \left(K\mathrm{CnP}L\right)\left(C\right)$$
10		ftc1.j	$$⊢J=L{\upharpoonright }_{𝑡}ℝ$$
11		ftc1.k	$$⊢K=L{\upharpoonright }_{𝑡}D$$
12		ftc1.l	$$⊢L=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
13		ftc1.h	$$⊢H=\left(z\in \left(\left[A,B\right]\setminus \left\{C\right\}\right)⟼\frac{G\left(z\right)-G\left(C\right)}{z-C}\right)$$
14		ftc1.e	$$⊢\phi \to E\in {ℝ}^{+}$$
15		ftc1.r	$$⊢\phi \to R\in {ℝ}^{+}$$
16		ftc1.fc	$$⊢\left(\phi \wedge y\in D\right)\to \left(\left|y-C\right|<R\to \left|F\left(y\right)-F\left(C\right)\right|<E\right)$$
17		ftc1.x1	$$⊢\phi \to X\in \left[A,B\right]$$
18		ftc1.x2	$$⊢\phi \to \left|X-C\right|<R$$
19		iccssre	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left[A,B\right]\subseteq ℝ$$
20	2 3 19	syl2anc	$$⊢\phi \to \left[A,B\right]\subseteq ℝ$$
21	20 17	sseldd	$$⊢\phi \to X\in ℝ$$
22		ioossicc	$$⊢\left(A,B\right)\subseteq \left[A,B\right]$$
23	22 8	sselid	$$⊢\phi \to C\in \left[A,B\right]$$
24	20 23	sseldd	$$⊢\phi \to C\in ℝ$$
25	21 24	lttri2d	$$⊢\phi \to \left(X\ne C\leftrightarrow \left(X<C\vee C<X\right)\right)$$
26	25	biimpa	$$⊢\left(\phi \wedge X\ne C\right)\to \left(X<C\vee C<X\right)$$
27	17	adantr	$$⊢\left(\phi \wedge X<C\right)\to X\in \left[A,B\right]$$
28	21	adantr	$$⊢\left(\phi \wedge X<C\right)\to X\in ℝ$$
29		simpr	$$⊢\left(\phi \wedge X<C\right)\to X<C$$
30	28 29	ltned	$$⊢\left(\phi \wedge X<C\right)\to X\ne C$$
31		eldifsn	$$⊢X\in \left(\left[A,B\right]\setminus \left\{C\right\}\right)\leftrightarrow \left(X\in \left[A,B\right]\wedge X\ne C\right)$$
32	27 30 31	sylanbrc	$$⊢\left(\phi \wedge X<C\right)\to X\in \left(\left[A,B\right]\setminus \left\{C\right\}\right)$$
33		fveq2	$$⊢z=X\to G\left(z\right)=G\left(X\right)$$
34	33	oveq1d	$$⊢z=X\to G\left(z\right)-G\left(C\right)=G\left(X\right)-G\left(C\right)$$
35		oveq1	$$⊢z=X\to z-C=X-C$$
36	34 35	oveq12d	$$⊢z=X\to \frac{G\left(z\right)-G\left(C\right)}{z-C}=\frac{G\left(X\right)-G\left(C\right)}{X-C}$$
37		ovex	$$⊢\frac{G\left(X\right)-G\left(C\right)}{X-C}\in \mathrm{V}$$
38	36 13 37	fvmpt	$$⊢X\in \left(\left[A,B\right]\setminus \left\{C\right\}\right)\to H\left(X\right)=\frac{G\left(X\right)-G\left(C\right)}{X-C}$$
39	32 38	syl	$$⊢\left(\phi \wedge X<C\right)\to H\left(X\right)=\frac{G\left(X\right)-G\left(C\right)}{X-C}$$
40	1 2 3 4 5 6 7 8 9 10 11 12	ftc1lem3	$$⊢\phi \to F:D⟶ℂ$$
41	1 2 3 4 5 6 7 40	ftc1lem2	$$⊢\phi \to G:\left[A,B\right]⟶ℂ$$
42	41 17	ffvelcdmd	$$⊢\phi \to G\left(X\right)\in ℂ$$
43	41 23	ffvelcdmd	$$⊢\phi \to G\left(C\right)\in ℂ$$
44	42 43	subcld	$$⊢\phi \to G\left(X\right)-G\left(C\right)\in ℂ$$
45	44	adantr	$$⊢\left(\phi \wedge X<C\right)\to G\left(X\right)-G\left(C\right)\in ℂ$$
46	21	recnd	$$⊢\phi \to X\in ℂ$$
47	24	recnd	$$⊢\phi \to C\in ℂ$$
48	46 47	subcld	$$⊢\phi \to X-C\in ℂ$$
49	48	adantr	$$⊢\left(\phi \wedge X<C\right)\to X-C\in ℂ$$
50	46 47	subeq0ad	$$⊢\phi \to \left(X-C=0\leftrightarrow X=C\right)$$
51	50	necon3bid	$$⊢\phi \to \left(X-C\ne 0\leftrightarrow X\ne C\right)$$
52	51	biimpar	$$⊢\left(\phi \wedge X\ne C\right)\to X-C\ne 0$$
53	30 52	syldan	$$⊢\left(\phi \wedge X<C\right)\to X-C\ne 0$$
54	45 49 53	div2negd	$$⊢\left(\phi \wedge X<C\right)\to \frac{-\left(G\left(X\right)-G\left(C\right)\right)}{-\left(X-C\right)}=\frac{G\left(X\right)-G\left(C\right)}{X-C}$$
55	42 43	negsubdi2d	$$⊢\phi \to -\left(G\left(X\right)-G\left(C\right)\right)=G\left(C\right)-G\left(X\right)$$
56	46 47	negsubdi2d	$$⊢\phi \to -\left(X-C\right)=C-X$$
57	55 56	oveq12d	$$⊢\phi \to \frac{-\left(G\left(X\right)-G\left(C\right)\right)}{-\left(X-C\right)}=\frac{G\left(C\right)-G\left(X\right)}{C-X}$$
58	57	adantr	$$⊢\left(\phi \wedge X<C\right)\to \frac{-\left(G\left(X\right)-G\left(C\right)\right)}{-\left(X-C\right)}=\frac{G\left(C\right)-G\left(X\right)}{C-X}$$
59	39 54 58	3eqtr2d	$$⊢\left(\phi \wedge X<C\right)\to H\left(X\right)=\frac{G\left(C\right)-G\left(X\right)}{C-X}$$
60	59	fvoveq1d	$$⊢\left(\phi \wedge X<C\right)\to \left|H\left(X\right)-F\left(C\right)\right|=\left|\left(\frac{G\left(C\right)-G\left(X\right)}{C-X}\right)-F\left(C\right)\right|$$
61	47	subidd	$$⊢\phi \to C-C=0$$
62	61	abs00bd	$$⊢\phi \to \left|C-C\right|=0$$
63	15	rpgt0d	$$⊢\phi \to 0<R$$
64	62 63	eqbrtrd	$$⊢\phi \to \left|C-C\right|<R$$
65	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 23 64	ftc1lem4	$$⊢\left(\phi \wedge X<C\right)\to \left|\left(\frac{G\left(C\right)-G\left(X\right)}{C-X}\right)-F\left(C\right)\right|<E$$
66	60 65	eqbrtrd	$$⊢\left(\phi \wedge X<C\right)\to \left|H\left(X\right)-F\left(C\right)\right|<E$$
67	17	adantr	$$⊢\left(\phi \wedge C<X\right)\to X\in \left[A,B\right]$$
68	24	adantr	$$⊢\left(\phi \wedge C<X\right)\to C\in ℝ$$
69		simpr	$$⊢\left(\phi \wedge C<X\right)\to C<X$$
70	68 69	gtned	$$⊢\left(\phi \wedge C<X\right)\to X\ne C$$
71	67 70 31	sylanbrc	$$⊢\left(\phi \wedge C<X\right)\to X\in \left(\left[A,B\right]\setminus \left\{C\right\}\right)$$
72	71 38	syl	$$⊢\left(\phi \wedge C<X\right)\to H\left(X\right)=\frac{G\left(X\right)-G\left(C\right)}{X-C}$$
73	72	fvoveq1d	$$⊢\left(\phi \wedge C<X\right)\to \left|H\left(X\right)-F\left(C\right)\right|=\left|\left(\frac{G\left(X\right)-G\left(C\right)}{X-C}\right)-F\left(C\right)\right|$$
74	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 23 64 17 18	ftc1lem4	$$⊢\left(\phi \wedge C<X\right)\to \left|\left(\frac{G\left(X\right)-G\left(C\right)}{X-C}\right)-F\left(C\right)\right|<E$$
75	73 74	eqbrtrd	$$⊢\left(\phi \wedge C<X\right)\to \left|H\left(X\right)-F\left(C\right)\right|<E$$
76	66 75	jaodan	$$⊢\left(\phi \wedge \left(X<C\vee C<X\right)\right)\to \left|H\left(X\right)-F\left(C\right)\right|<E$$
77	26 76	syldan	$$⊢\left(\phi \wedge X\ne C\right)\to \left|H\left(X\right)-F\left(C\right)\right|<E$$