This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ftc1lem6

Description: Lemma for ftc1 . (Contributed by Mario Carneiro, 14-Aug-2014) (Proof shortened 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 ) ) )
Assertion ftc1lem6 
|- ( ph -> ( F ` C ) e. ( H limCC C ) )

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 1 2 3 4 5 6 7 8 9 10 11 12 ftc1lem3 
 |-  ( ph -> F : D --> CC )
15 5 8 sseldd 
 |-  ( ph -> C e. D )
16 14 15 ffvelcdmd 
 |-  ( ph -> ( F ` C ) e. CC )
17 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
18 ax-resscn 
 |-  RR C_ CC
19 6 18 sstrdi 
 |-  ( ph -> D C_ CC )
20 19 adantr 
 |-  ( ( ph /\ w e. RR+ ) -> D C_ CC )
21 xmetres2 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ D C_ CC ) -> ( ( abs o. - ) |` ( D X. D ) ) e. ( *Met ` D ) )
22 17 20 21 sylancr 
 |-  ( ( ph /\ w e. RR+ ) -> ( ( abs o. - ) |` ( D X. D ) ) e. ( *Met ` D ) )
23 17 a1i 
 |-  ( ( ph /\ w e. RR+ ) -> ( abs o. - ) e. ( *Met ` CC ) )
24 eqid 
 |-  ( ( abs o. - ) |` ( D X. D ) ) = ( ( abs o. - ) |` ( D X. D ) )
25 12 cnfldtopn 
 |-  L = ( MetOpen ` ( abs o. - ) )
26 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) )
27 24 25 26 metrest 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ D C_ CC ) -> ( L |`t D ) = ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) ) )
28 17 19 27 sylancr 
 |-  ( ph -> ( L |`t D ) = ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) ) )
29 11 28 eqtrid 
 |-  ( ph -> K = ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) ) )
30 29 oveq1d 
 |-  ( ph -> ( K CnP L ) = ( ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) ) CnP L ) )
31 30 fveq1d 
 |-  ( ph -> ( ( K CnP L ) ` C ) = ( ( ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) ) CnP L ) ` C ) )
32 9 31 eleqtrd 
 |-  ( ph -> F e. ( ( ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) ) CnP L ) ` C ) )
33 32 adantr 
 |-  ( ( ph /\ w e. RR+ ) -> F e. ( ( ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) ) CnP L ) ` C ) )
34 simpr 
 |-  ( ( ph /\ w e. RR+ ) -> w e. RR+ )
35 26 25 metcnpi2 
 |-  ( ( ( ( ( abs o. - ) |` ( D X. D ) ) e. ( *Met ` D ) /\ ( abs o. - ) e. ( *Met ` CC ) ) /\ ( F e. ( ( ( MetOpen ` ( ( abs o. - ) |` ( D X. D ) ) ) CnP L ) ` C ) /\ w e. RR+ ) ) -> E. v e. RR+ A. y e. D ( ( y ( ( abs o. - ) |` ( D X. D ) ) C ) < v -> ( ( F ` y ) ( abs o. - ) ( F ` C ) ) < w ) )
36 22 23 33 34 35 syl22anc 
 |-  ( ( ph /\ w e. RR+ ) -> E. v e. RR+ A. y e. D ( ( y ( ( abs o. - ) |` ( D X. D ) ) C ) < v -> ( ( F ` y ) ( abs o. - ) ( F ` C ) ) < w ) )
37 simpr 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ y e. D ) -> y e. D )
38 15 ad2antrr 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ y e. D ) -> C e. D )
39 37 38 ovresd 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ y e. D ) -> ( y ( ( abs o. - ) |` ( D X. D ) ) C ) = ( y ( abs o. - ) C ) )
40 19 adantr 
 |-  ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) -> D C_ CC )
41 40 sselda 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ y e. D ) -> y e. CC )
42 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
43 2 3 42 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
44 43 18 sstrdi 
 |-  ( ph -> ( A [,] B ) C_ CC )
45 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
46 45 8 sselid 
 |-  ( ph -> C e. ( A [,] B ) )
47 44 46 sseldd 
 |-  ( ph -> C e. CC )
48 47 ad2antrr 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ y e. D ) -> C e. CC )
49 eqid 
 |-  ( abs o. - ) = ( abs o. - )
50 49 cnmetdval 
 |-  ( ( y e. CC /\ C e. CC ) -> ( y ( abs o. - ) C ) = ( abs ` ( y - C ) ) )
51 41 48 50 syl2anc 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ y e. D ) -> ( y ( abs o. - ) C ) = ( abs ` ( y - C ) ) )
52 39 51 eqtrd 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ y e. D ) -> ( y ( ( abs o. - ) |` ( D X. D ) ) C ) = ( abs ` ( y - C ) ) )
53 52 breq1d 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ y e. D ) -> ( ( y ( ( abs o. - ) |` ( D X. D ) ) C ) < v <-> ( abs ` ( y - C ) ) < v ) )
54 14 adantr 
 |-  ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) -> F : D --> CC )
55 54 ffvelcdmda 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ y e. D ) -> ( F ` y ) e. CC )
56 16 ad2antrr 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ y e. D ) -> ( F ` C ) e. CC )
57 49 cnmetdval 
 |-  ( ( ( F ` y ) e. CC /\ ( F ` C ) e. CC ) -> ( ( F ` y ) ( abs o. - ) ( F ` C ) ) = ( abs ` ( ( F ` y ) - ( F ` C ) ) ) )
58 55 56 57 syl2anc 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ y e. D ) -> ( ( F ` y ) ( abs o. - ) ( F ` C ) ) = ( abs ` ( ( F ` y ) - ( F ` C ) ) ) )
59 58 breq1d 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ y e. D ) -> ( ( ( F ` y ) ( abs o. - ) ( F ` C ) ) < w <-> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) )
60 53 59 imbi12d 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ y e. D ) -> ( ( ( y ( ( abs o. - ) |` ( D X. D ) ) C ) < v -> ( ( F ` y ) ( abs o. - ) ( F ` C ) ) < w ) <-> ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) )
61 60 ralbidva 
 |-  ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) -> ( A. y e. D ( ( y ( ( abs o. - ) |` ( D X. D ) ) C ) < v -> ( ( F ` y ) ( abs o. - ) ( F ` C ) ) < w ) <-> A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) )
62 simprll 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) -> s e. ( ( A [,] B ) \ { C } ) )
63 eldifsni 
 |-  ( s e. ( ( A [,] B ) \ { C } ) -> s =/= C )
64 62 63 syl 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) -> s =/= C )
65 2 ad2antrr 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) -> A e. RR )
66 3 ad2antrr 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) -> B e. RR )
67 4 ad2antrr 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) -> A <_ B )
68 5 ad2antrr 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) -> ( A (,) B ) C_ D )
69 6 ad2antrr 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) -> D C_ RR )
70 7 ad2antrr 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) -> F e. L^1 )
71 8 ad2antrr 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) -> C e. ( A (,) B ) )
72 9 ad2antrr 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) -> F e. ( ( K CnP L ) ` C ) )
73 simplrl 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) -> w e. RR+ )
74 simplrr 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) -> v e. RR+ )
75 simprlr 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) -> A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) )
76 fvoveq1 
 |-  ( y = u -> ( abs ` ( y - C ) ) = ( abs ` ( u - C ) ) )
77 76 breq1d 
 |-  ( y = u -> ( ( abs ` ( y - C ) ) < v <-> ( abs ` ( u - C ) ) < v ) )
78 77 imbrov2fvoveq 
 |-  ( y = u -> ( ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) <-> ( ( abs ` ( u - C ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` C ) ) ) < w ) ) )
79 78 rspccva 
 |-  ( ( A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) /\ u e. D ) -> ( ( abs ` ( u - C ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` C ) ) ) < w ) )
80 75 79 sylan 
 |-  ( ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) /\ u e. D ) -> ( ( abs ` ( u - C ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` C ) ) ) < w ) )
81 62 eldifad 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) -> s e. ( A [,] B ) )
82 simprr 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) -> ( abs ` ( s - C ) ) < v )
83 1 65 66 67 68 69 70 71 72 10 11 12 13 73 74 80 81 82 ftc1lem5 
 |-  ( ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) /\ s =/= C ) -> ( abs ` ( ( H ` s ) - ( F ` C ) ) ) < w )
84 64 83 mpdan 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) /\ ( abs ` ( s - C ) ) < v ) ) -> ( abs ` ( ( H ` s ) - ( F ` C ) ) ) < w )
85 84 expr 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) ) -> ( ( abs ` ( s - C ) ) < v -> ( abs ` ( ( H ` s ) - ( F ` C ) ) ) < w ) )
86 85 adantld 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( s e. ( ( A [,] B ) \ { C } ) /\ A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) ) ) -> ( ( s =/= C /\ ( abs ` ( s - C ) ) < v ) -> ( abs ` ( ( H ` s ) - ( F ` C ) ) ) < w ) )
87 86 expr 
 |-  ( ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) /\ s e. ( ( A [,] B ) \ { C } ) ) -> ( A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) -> ( ( s =/= C /\ ( abs ` ( s - C ) ) < v ) -> ( abs ` ( ( H ` s ) - ( F ` C ) ) ) < w ) ) )
88 87 ralrimdva 
 |-  ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) -> ( A. y e. D ( ( abs ` ( y - C ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` C ) ) ) < w ) -> A. s e. ( ( A [,] B ) \ { C } ) ( ( s =/= C /\ ( abs ` ( s - C ) ) < v ) -> ( abs ` ( ( H ` s ) - ( F ` C ) ) ) < w ) ) )
89 61 88 sylbid 
 |-  ( ( ph /\ ( w e. RR+ /\ v e. RR+ ) ) -> ( A. y e. D ( ( y ( ( abs o. - ) |` ( D X. D ) ) C ) < v -> ( ( F ` y ) ( abs o. - ) ( F ` C ) ) < w ) -> A. s e. ( ( A [,] B ) \ { C } ) ( ( s =/= C /\ ( abs ` ( s - C ) ) < v ) -> ( abs ` ( ( H ` s ) - ( F ` C ) ) ) < w ) ) )
90 89 anassrs 
 |-  ( ( ( ph /\ w e. RR+ ) /\ v e. RR+ ) -> ( A. y e. D ( ( y ( ( abs o. - ) |` ( D X. D ) ) C ) < v -> ( ( F ` y ) ( abs o. - ) ( F ` C ) ) < w ) -> A. s e. ( ( A [,] B ) \ { C } ) ( ( s =/= C /\ ( abs ` ( s - C ) ) < v ) -> ( abs ` ( ( H ` s ) - ( F ` C ) ) ) < w ) ) )
91 90 reximdva 
 |-  ( ( ph /\ w e. RR+ ) -> ( E. v e. RR+ A. y e. D ( ( y ( ( abs o. - ) |` ( D X. D ) ) C ) < v -> ( ( F ` y ) ( abs o. - ) ( F ` C ) ) < w ) -> E. v e. RR+ A. s e. ( ( A [,] B ) \ { C } ) ( ( s =/= C /\ ( abs ` ( s - C ) ) < v ) -> ( abs ` ( ( H ` s ) - ( F ` C ) ) ) < w ) ) )
92 36 91 mpd 
 |-  ( ( ph /\ w e. RR+ ) -> E. v e. RR+ A. s e. ( ( A [,] B ) \ { C } ) ( ( s =/= C /\ ( abs ` ( s - C ) ) < v ) -> ( abs ` ( ( H ` s ) - ( F ` C ) ) ) < w ) )
93 92 ralrimiva 
 |-  ( ph -> A. w e. RR+ E. v e. RR+ A. s e. ( ( A [,] B ) \ { C } ) ( ( s =/= C /\ ( abs ` ( s - C ) ) < v ) -> ( abs ` ( ( H ` s ) - ( F ` C ) ) ) < w ) )
94 1 2 3 4 5 6 7 14 ftc1lem2 
 |-  ( ph -> G : ( A [,] B ) --> CC )
95 94 44 46 dvlem 
 |-  ( ( ph /\ z e. ( ( A [,] B ) \ { C } ) ) -> ( ( ( G ` z ) - ( G ` C ) ) / ( z - C ) ) e. CC )
96 95 13 fmptd 
 |-  ( ph -> H : ( ( A [,] B ) \ { C } ) --> CC )
97 44 ssdifssd 
 |-  ( ph -> ( ( A [,] B ) \ { C } ) C_ CC )
98 96 97 47 ellimc3 
 |-  ( ph -> ( ( F ` C ) e. ( H limCC C ) <-> ( ( F ` C ) e. CC /\ A. w e. RR+ E. v e. RR+ A. s e. ( ( A [,] B ) \ { C } ) ( ( s =/= C /\ ( abs ` ( s - C ) ) < v ) -> ( abs ` ( ( H ` s ) - ( F ` C ) ) ) < w ) ) ) )
99 16 93 98 mpbir2and 
 |-  ( ph -> ( F ` C ) e. ( H limCC C ) )