ftc1lem5

	Ref	Expression
Hypotheses	ftc1.g	\|- G = ( x e. ( A [,] B ) \|-> S. ( A (,) x ) ( F ` t ) _d t )
	ftc1.a	\|- ( ph -> A e. RR )
	ftc1.b	\|- ( ph -> B e. RR )
	ftc1.le	\|- ( ph -> A <_ B )
	ftc1.s	\|- ( ph -> ( A (,) B ) C_ D )
	ftc1.d	\|- ( ph -> D C_ RR )
	ftc1.i	\|- ( ph -> F e. L^1 )
	ftc1.c	\|- ( ph -> C e. ( A (,) B ) )
	ftc1.f	\|- ( ph -> F e. ( ( K CnP L ) ` C ) )
	ftc1.j	\|- J = ( L \|`t RR )
	ftc1.k	\|- K = ( L \|`t D )
	ftc1.l	\|- L = ( TopOpen ` CCfld )
	ftc1.h	\|- H = ( z e. ( ( A [,] B ) \ { C } ) \|-> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) )
	ftc1.e	\|- ( ph -> E e. RR+ )
	ftc1.r	\|- ( ph -> R e. RR+ )
	ftc1.fc	\|- ( ( ph /\ y e. D ) -> ( ( abs ` ( y - C ) ) < R -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < E ) )
	ftc1.x1	\|- ( ph -> X e. ( A [,] B ) )
	ftc1.x2	\|- ( ph -> ( abs ` ( X - C ) ) < R )
Assertion	ftc1lem5	\|- ( ( ph /\ X =/= C ) -> ( abs ` ( ( H ` X ) - ( F ` C ) ) ) < E )

Proof

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

Metamath Proof Explorer

Theorem ftc1lem5

Proof