Metamath Proof Explorer

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 = ( 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 sseldi 
 |-  ( 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 ffvelrnd 
 |-  ( ph -> ( G ` X ) e. CC )
43 41 23 ffvelrnd 
 |-  ( 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 )