Metamath Proof Explorer

Theorem ftc1cnnc

Description: Choice-free proof of ftc1cn . (Contributed by Brendan Leahy, 20-Nov-2017)

Ref Expression
Hypotheses ftc1cnnc.g 
|- G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )
ftc1cnnc.a 
|- ( ph -> A e. RR )
ftc1cnnc.b 
|- ( ph -> B e. RR )
ftc1cnnc.le 
|- ( ph -> A <_ B )
ftc1cnnc.f 
|- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
ftc1cnnc.i 
|- ( ph -> F e. L^1 )
Assertion ftc1cnnc 
|- ( ph -> ( RR _D G ) = F )

Proof

Step Hyp Ref Expression
1 ftc1cnnc.g 
 |-  G = ( x e. ( A [,] B ) |-> S. ( A (,) x ) ( F ` t ) _d t )
2 ftc1cnnc.a 
 |-  ( ph -> A e. RR )
3 ftc1cnnc.b 
 |-  ( ph -> B e. RR )
4 ftc1cnnc.le 
 |-  ( ph -> A <_ B )
5 ftc1cnnc.f 
 |-  ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
6 ftc1cnnc.i 
 |-  ( ph -> F e. L^1 )
7 dvf 
 |-  ( RR _D G ) : dom ( RR _D G ) --> CC
8 7 a1i 
 |-  ( ph -> ( RR _D G ) : dom ( RR _D G ) --> CC )
9 8 ffund 
 |-  ( ph -> Fun ( RR _D G ) )
10 ax-resscn 
 |-  RR C_ CC
11 10 a1i 
 |-  ( ph -> RR C_ CC )
12 ssidd 
 |-  ( ph -> ( A (,) B ) C_ ( A (,) B ) )
13 ioossre 
 |-  ( A (,) B ) C_ RR
14 13 a1i 
 |-  ( ph -> ( A (,) B ) C_ RR )
15 cncff 
 |-  ( F e. ( ( A (,) B ) -cn-> CC ) -> F : ( A (,) B ) --> CC )
16 5 15 syl 
 |-  ( ph -> F : ( A (,) B ) --> CC )
17 1 2 3 4 12 14 6 16 ftc1lem2 
 |-  ( ph -> G : ( A [,] B ) --> CC )
18 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
19 2 3 18 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
20 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
21 20 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
22 11 17 19 21 20 dvbssntr 
 |-  ( ph -> dom ( RR _D G ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) )
23 iccntr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
24 2 3 23 syl2anc 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
25 22 24 sseqtrd 
 |-  ( ph -> dom ( RR _D G ) C_ ( A (,) B ) )
26 retop 
 |-  ( topGen ` ran (,) ) e. Top
27 21 26 eqeltrri 
 |-  ( ( TopOpen ` CCfld ) |`t RR ) e. Top
28 27 a1i 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( ( TopOpen ` CCfld ) |`t RR ) e. Top )
29 19 adantr 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( A [,] B ) C_ RR )
30 iooretop 
 |-  ( A (,) B ) e. ( topGen ` ran (,) )
31 30 21 eleqtri 
 |-  ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR )
32 31 a1i 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR ) )
33 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
34 33 a1i 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( A (,) B ) C_ ( A [,] B ) )
35 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
36 21 unieqi 
 |-  U. ( topGen ` ran (,) ) = U. ( ( TopOpen ` CCfld ) |`t RR )
37 35 36 eqtri 
 |-  RR = U. ( ( TopOpen ` CCfld ) |`t RR )
38 37 ssntr 
 |-  ( ( ( ( ( TopOpen ` CCfld ) |`t RR ) e. Top /\ ( A [,] B ) C_ RR ) /\ ( ( A (,) B ) e. ( ( TopOpen ` CCfld ) |`t RR ) /\ ( A (,) B ) C_ ( A [,] B ) ) ) -> ( A (,) B ) C_ ( ( int ` ( ( TopOpen ` CCfld ) |`t RR ) ) ` ( A [,] B ) ) )
39 28 29 32 34 38 syl22anc 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( A (,) B ) C_ ( ( int ` ( ( TopOpen ` CCfld ) |`t RR ) ) ` ( A [,] B ) ) )
40 simpr 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> c e. ( A (,) B ) )
41 39 40 sseldd 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> c e. ( ( int ` ( ( TopOpen ` CCfld ) |`t RR ) ) ` ( A [,] B ) ) )
42 16 ffvelrnda 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( F ` c ) e. CC )
43 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
44 13 10 sstri 
 |-  ( A (,) B ) C_ CC
45 xmetres2 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( A (,) B ) C_ CC ) -> ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) e. ( *Met ` ( A (,) B ) ) )
46 43 44 45 mp2an 
 |-  ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) e. ( *Met ` ( A (,) B ) )
47 46 a1i 
 |-  ( ( ( ph /\ c e. ( A (,) B ) ) /\ w e. RR+ ) -> ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) e. ( *Met ` ( A (,) B ) ) )
48 43 a1i 
 |-  ( ( ( ph /\ c e. ( A (,) B ) ) /\ w e. RR+ ) -> ( abs o. - ) e. ( *Met ` CC ) )
49 ssid 
 |-  CC C_ CC
50 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) = ( ( TopOpen ` CCfld ) |`t ( A (,) B ) )
51 20 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
52 51 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
53 20 50 52 cncfcn 
 |-  ( ( ( A (,) B ) C_ CC /\ CC C_ CC ) -> ( ( A (,) B ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
54 44 49 53 mp2an 
 |-  ( ( A (,) B ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) )
55 5 54 eleqtrdi 
 |-  ( ph -> F e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
56 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( A (,) B ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) e. ( TopOn ` ( A (,) B ) ) )
57 51 44 56 mp2an 
 |-  ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) e. ( TopOn ` ( A (,) B ) )
58 57 toponunii 
 |-  ( A (,) B ) = U. ( ( TopOpen ` CCfld ) |`t ( A (,) B ) )
59 58 eleq2i 
 |-  ( c e. ( A (,) B ) <-> c e. U. ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) )
60 59 biimpi 
 |-  ( c e. ( A (,) B ) -> c e. U. ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) )
61 eqid 
 |-  U. ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) = U. ( ( TopOpen ` CCfld ) |`t ( A (,) B ) )
62 61 cncnpi 
 |-  ( ( F e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) /\ c e. U. ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) ) -> F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` c ) )
63 55 60 62 syl2an 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` c ) )
64 eqid 
 |-  ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) = ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) )
65 20 cnfldtopn 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
66 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) )
67 64 65 66 metrest 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( A (,) B ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) ) )
68 43 44 67 mp2an 
 |-  ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) )
69 68 oveq1i 
 |-  ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) = ( ( MetOpen ` ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) ) CnP ( TopOpen ` CCfld ) )
70 69 fveq1i 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` c ) = ( ( ( MetOpen ` ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` c )
71 63 70 eleqtrdi 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> F e. ( ( ( MetOpen ` ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` c ) )
72 71 adantr 
 |-  ( ( ( ph /\ c e. ( A (,) B ) ) /\ w e. RR+ ) -> F e. ( ( ( MetOpen ` ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` c ) )
73 simpr 
 |-  ( ( ( ph /\ c e. ( A (,) B ) ) /\ w e. RR+ ) -> w e. RR+ )
74 66 65 metcnpi2 
 |-  ( ( ( ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) e. ( *Met ` ( A (,) B ) ) /\ ( abs o. - ) e. ( *Met ` CC ) ) /\ ( F e. ( ( ( MetOpen ` ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) ) CnP ( TopOpen ` CCfld ) ) ` c ) /\ w e. RR+ ) ) -> E. v e. RR+ A. u e. ( A (,) B ) ( ( u ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) c ) < v -> ( ( F ` u ) ( abs o. - ) ( F ` c ) ) < w ) )
75 47 48 72 73 74 syl22anc 
 |-  ( ( ( ph /\ c e. ( A (,) B ) ) /\ w e. RR+ ) -> E. v e. RR+ A. u e. ( A (,) B ) ( ( u ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) c ) < v -> ( ( F ` u ) ( abs o. - ) ( F ` c ) ) < w ) )
76 simpr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ u e. ( A (,) B ) ) -> u e. ( A (,) B ) )
77 simpllr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ u e. ( A (,) B ) ) -> c e. ( A (,) B ) )
78 76 77 ovresd 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ u e. ( A (,) B ) ) -> ( u ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) c ) = ( u ( abs o. - ) c ) )
79 elioore 
 |-  ( u e. ( A (,) B ) -> u e. RR )
80 79 recnd 
 |-  ( u e. ( A (,) B ) -> u e. CC )
81 44 sseli 
 |-  ( c e. ( A (,) B ) -> c e. CC )
82 81 ad3antlr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ u e. ( A (,) B ) ) -> c e. CC )
83 eqid 
 |-  ( abs o. - ) = ( abs o. - )
84 83 cnmetdval 
 |-  ( ( u e. CC /\ c e. CC ) -> ( u ( abs o. - ) c ) = ( abs ` ( u - c ) ) )
85 80 82 84 syl2an2 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ u e. ( A (,) B ) ) -> ( u ( abs o. - ) c ) = ( abs ` ( u - c ) ) )
86 78 85 eqtrd 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ u e. ( A (,) B ) ) -> ( u ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) c ) = ( abs ` ( u - c ) ) )
87 86 breq1d 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ u e. ( A (,) B ) ) -> ( ( u ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) c ) < v <-> ( abs ` ( u - c ) ) < v ) )
88 16 ad2antrr 
 |-  ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) -> F : ( A (,) B ) --> CC )
89 88 ffvelrnda 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ u e. ( A (,) B ) ) -> ( F ` u ) e. CC )
90 42 ad2antrr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ u e. ( A (,) B ) ) -> ( F ` c ) e. CC )
91 83 cnmetdval 
 |-  ( ( ( F ` u ) e. CC /\ ( F ` c ) e. CC ) -> ( ( F ` u ) ( abs o. - ) ( F ` c ) ) = ( abs ` ( ( F ` u ) - ( F ` c ) ) ) )
92 89 90 91 syl2anc 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ u e. ( A (,) B ) ) -> ( ( F ` u ) ( abs o. - ) ( F ` c ) ) = ( abs ` ( ( F ` u ) - ( F ` c ) ) ) )
93 92 breq1d 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ u e. ( A (,) B ) ) -> ( ( ( F ` u ) ( abs o. - ) ( F ` c ) ) < w <-> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) )
94 87 93 imbi12d 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ u e. ( A (,) B ) ) -> ( ( ( u ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) c ) < v -> ( ( F ` u ) ( abs o. - ) ( F ` c ) ) < w ) <-> ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) )
95 94 ralbidva 
 |-  ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) -> ( A. u e. ( A (,) B ) ( ( u ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) c ) < v -> ( ( F ` u ) ( abs o. - ) ( F ` c ) ) < w ) <-> A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) )
96 simprll 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> z e. ( ( A [,] B ) \ { c } ) )
97 eldifsni 
 |-  ( z e. ( ( A [,] B ) \ { c } ) -> z =/= c )
98 96 97 syl 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> z =/= c )
99 19 ssdifssd 
 |-  ( ph -> ( ( A [,] B ) \ { c } ) C_ RR )
100 99 sselda 
 |-  ( ( ph /\ z e. ( ( A [,] B ) \ { c } ) ) -> z e. RR )
101 100 ad2ant2r 
 |-  ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) ) -> z e. RR )
102 101 ad2ant2r 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> z e. RR )
103 elioore 
 |-  ( c e. ( A (,) B ) -> c e. RR )
104 103 ad3antlr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> c e. RR )
105 102 104 lttri2d 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> ( z =/= c <-> ( z < c \/ c < z ) ) )
106 105 biimpa 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ z =/= c ) -> ( z < c \/ c < z ) )
107 fveq2 
 |-  ( s = z -> ( G ` s ) = ( G ` z ) )
108 107 oveq1d 
 |-  ( s = z -> ( ( G ` s ) - ( G ` c ) ) = ( ( G ` z ) - ( G ` c ) ) )
109 oveq1 
 |-  ( s = z -> ( s - c ) = ( z - c ) )
110 108 109 oveq12d 
 |-  ( s = z -> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) = ( ( ( G ` z ) - ( G ` c ) ) / ( z - c ) ) )
111 eqid 
 |-  ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) = ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) )
112 ovex 
 |-  ( ( ( G ` z ) - ( G ` c ) ) / ( z - c ) ) e. _V
113 110 111 112 fvmpt 
 |-  ( z e. ( ( A [,] B ) \ { c } ) -> ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) = ( ( ( G ` z ) - ( G ` c ) ) / ( z - c ) ) )
114 113 ad2antrr 
 |-  ( ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) -> ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) = ( ( ( G ` z ) - ( G ` c ) ) / ( z - c ) ) )
115 114 ad2antlr 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ z < c ) -> ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) = ( ( ( G ` z ) - ( G ` c ) ) / ( z - c ) ) )
116 17 ad4antr 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ z < c ) -> G : ( A [,] B ) --> CC )
117 eldifi 
 |-  ( z e. ( ( A [,] B ) \ { c } ) -> z e. ( A [,] B ) )
118 117 ad2antrr 
 |-  ( ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) -> z e. ( A [,] B ) )
119 118 ad2antlr 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ z < c ) -> z e. ( A [,] B ) )
120 116 119 ffvelrnd 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ z < c ) -> ( G ` z ) e. CC )
121 33 sseli 
 |-  ( c e. ( A (,) B ) -> c e. ( A [,] B ) )
122 17 ffvelrnda 
 |-  ( ( ph /\ c e. ( A [,] B ) ) -> ( G ` c ) e. CC )
123 121 122 sylan2 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( G ` c ) e. CC )
124 123 ad3antrrr 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ z < c ) -> ( G ` c ) e. CC )
125 102 adantr 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ z < c ) -> z e. RR )
126 125 recnd 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ z < c ) -> z e. CC )
127 81 ad4antlr 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ z < c ) -> c e. CC )
128 ltne 
 |-  ( ( z e. RR /\ z < c ) -> c =/= z )
129 128 necomd 
 |-  ( ( z e. RR /\ z < c ) -> z =/= c )
130 102 129 sylan 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ z < c ) -> z =/= c )
131 120 124 126 127 130 div2subd 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ z < c ) -> ( ( ( G ` z ) - ( G ` c ) ) / ( z - c ) ) = ( ( ( G ` c ) - ( G ` z ) ) / ( c - z ) ) )
132 115 131 eqtrd 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ z < c ) -> ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) = ( ( ( G ` c ) - ( G ` z ) ) / ( c - z ) ) )
133 132 fvoveq1d 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ z < c ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) = ( abs ` ( ( ( ( G ` c ) - ( G ` z ) ) / ( c - z ) ) - ( F ` c ) ) ) )
134 2 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> A e. RR )
135 3 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> B e. RR )
136 4 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> A <_ B )
137 5 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> F e. ( ( A (,) B ) -cn-> CC ) )
138 6 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> F e. L^1 )
139 simpllr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> c e. ( A (,) B ) )
140 simplrl 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> w e. RR+ )
141 simplrr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> v e. RR+ )
142 simprlr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) )
143 fvoveq1 
 |-  ( u = y -> ( abs ` ( u - c ) ) = ( abs ` ( y - c ) ) )
144 143 breq1d 
 |-  ( u = y -> ( ( abs ` ( u - c ) ) < v <-> ( abs ` ( y - c ) ) < v ) )
145 144 imbrov2fvoveq 
 |-  ( u = y -> ( ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) <-> ( ( abs ` ( y - c ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` c ) ) ) < w ) ) )
146 145 rspccva 
 |-  ( ( A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) /\ y e. ( A (,) B ) ) -> ( ( abs ` ( y - c ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` c ) ) ) < w ) )
147 142 146 sylan 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ y e. ( A (,) B ) ) -> ( ( abs ` ( y - c ) ) < v -> ( abs ` ( ( F ` y ) - ( F ` c ) ) ) < w ) )
148 96 117 syl 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> z e. ( A [,] B ) )
149 simprr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> ( abs ` ( z - c ) ) < v )
150 121 ad3antlr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> c e. ( A [,] B ) )
151 103 recnd 
 |-  ( c e. ( A (,) B ) -> c e. CC )
152 151 subidd 
 |-  ( c e. ( A (,) B ) -> ( c - c ) = 0 )
153 152 abs00bd 
 |-  ( c e. ( A (,) B ) -> ( abs ` ( c - c ) ) = 0 )
154 153 ad3antlr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> ( abs ` ( c - c ) ) = 0 )
155 141 rpgt0d 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> 0 < v )
156 154 155 eqbrtrd 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> ( abs ` ( c - c ) ) < v )
157 1 134 135 136 137 138 139 111 140 141 147 148 149 150 156 ftc1cnnclem 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ z < c ) -> ( abs ` ( ( ( ( G ` c ) - ( G ` z ) ) / ( c - z ) ) - ( F ` c ) ) ) < w )
158 133 157 eqbrtrd 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ z < c ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) < w )
159 113 fvoveq1d 
 |-  ( z e. ( ( A [,] B ) \ { c } ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) = ( abs ` ( ( ( ( G ` z ) - ( G ` c ) ) / ( z - c ) ) - ( F ` c ) ) ) )
160 159 ad2antrr 
 |-  ( ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) = ( abs ` ( ( ( ( G ` z ) - ( G ` c ) ) / ( z - c ) ) - ( F ` c ) ) ) )
161 160 ad2antlr 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ c < z ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) = ( abs ` ( ( ( ( G ` z ) - ( G ` c ) ) / ( z - c ) ) - ( F ` c ) ) ) )
162 1 134 135 136 137 138 139 111 140 141 147 150 156 148 149 ftc1cnnclem 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ c < z ) -> ( abs ` ( ( ( ( G ` z ) - ( G ` c ) ) / ( z - c ) ) - ( F ` c ) ) ) < w )
163 161 162 eqbrtrd 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ c < z ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) < w )
164 158 163 jaodan 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ ( z < c \/ c < z ) ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) < w )
165 106 164 syldan 
 |-  ( ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) /\ z =/= c ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) < w )
166 98 165 mpdan 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) /\ ( abs ` ( z - c ) ) < v ) ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) < w )
167 166 expr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) ) -> ( ( abs ` ( z - c ) ) < v -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) < w ) )
168 167 adantld 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ ( z e. ( ( A [,] B ) \ { c } ) /\ A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) ) ) -> ( ( z =/= c /\ ( abs ` ( z - c ) ) < v ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) < w ) )
169 168 expr 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) /\ z e. ( ( A [,] B ) \ { c } ) ) -> ( A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) -> ( ( z =/= c /\ ( abs ` ( z - c ) ) < v ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) < w ) ) )
170 169 ralrimdva 
 |-  ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) -> ( A. u e. ( A (,) B ) ( ( abs ` ( u - c ) ) < v -> ( abs ` ( ( F ` u ) - ( F ` c ) ) ) < w ) -> A. z e. ( ( A [,] B ) \ { c } ) ( ( z =/= c /\ ( abs ` ( z - c ) ) < v ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) < w ) ) )
171 95 170 sylbid 
 |-  ( ( ( ph /\ c e. ( A (,) B ) ) /\ ( w e. RR+ /\ v e. RR+ ) ) -> ( A. u e. ( A (,) B ) ( ( u ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) c ) < v -> ( ( F ` u ) ( abs o. - ) ( F ` c ) ) < w ) -> A. z e. ( ( A [,] B ) \ { c } ) ( ( z =/= c /\ ( abs ` ( z - c ) ) < v ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) < w ) ) )
172 171 anassrs 
 |-  ( ( ( ( ph /\ c e. ( A (,) B ) ) /\ w e. RR+ ) /\ v e. RR+ ) -> ( A. u e. ( A (,) B ) ( ( u ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) c ) < v -> ( ( F ` u ) ( abs o. - ) ( F ` c ) ) < w ) -> A. z e. ( ( A [,] B ) \ { c } ) ( ( z =/= c /\ ( abs ` ( z - c ) ) < v ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) < w ) ) )
173 172 reximdva 
 |-  ( ( ( ph /\ c e. ( A (,) B ) ) /\ w e. RR+ ) -> ( E. v e. RR+ A. u e. ( A (,) B ) ( ( u ( ( abs o. - ) |` ( ( A (,) B ) X. ( A (,) B ) ) ) c ) < v -> ( ( F ` u ) ( abs o. - ) ( F ` c ) ) < w ) -> E. v e. RR+ A. z e. ( ( A [,] B ) \ { c } ) ( ( z =/= c /\ ( abs ` ( z - c ) ) < v ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) < w ) ) )
174 75 173 mpd 
 |-  ( ( ( ph /\ c e. ( A (,) B ) ) /\ w e. RR+ ) -> E. v e. RR+ A. z e. ( ( A [,] B ) \ { c } ) ( ( z =/= c /\ ( abs ` ( z - c ) ) < v ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) < w ) )
175 174 ralrimiva 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> A. w e. RR+ E. v e. RR+ A. z e. ( ( A [,] B ) \ { c } ) ( ( z =/= c /\ ( abs ` ( z - c ) ) < v ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) < w ) )
176 17 adantr 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> G : ( A [,] B ) --> CC )
177 19 10 sstrdi 
 |-  ( ph -> ( A [,] B ) C_ CC )
178 177 adantr 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( A [,] B ) C_ CC )
179 121 adantl 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> c e. ( A [,] B ) )
180 176 178 179 dvlem 
 |-  ( ( ( ph /\ c e. ( A (,) B ) ) /\ s e. ( ( A [,] B ) \ { c } ) ) -> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) e. CC )
181 180 fmpttd 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) : ( ( A [,] B ) \ { c } ) --> CC )
182 177 ssdifssd 
 |-  ( ph -> ( ( A [,] B ) \ { c } ) C_ CC )
183 182 adantr 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( ( A [,] B ) \ { c } ) C_ CC )
184 81 adantl 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> c e. CC )
185 181 183 184 ellimc3 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( ( F ` c ) e. ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) limCC c ) <-> ( ( F ` c ) e. CC /\ A. w e. RR+ E. v e. RR+ A. z e. ( ( A [,] B ) \ { c } ) ( ( z =/= c /\ ( abs ` ( z - c ) ) < v ) -> ( abs ` ( ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) ` z ) - ( F ` c ) ) ) < w ) ) ) )
186 42 175 185 mpbir2and 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( F ` c ) e. ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) limCC c ) )
187 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t RR ) = ( ( TopOpen ` CCfld ) |`t RR )
188 187 20 111 11 17 19 eldv 
 |-  ( ph -> ( c ( RR _D G ) ( F ` c ) <-> ( c e. ( ( int ` ( ( TopOpen ` CCfld ) |`t RR ) ) ` ( A [,] B ) ) /\ ( F ` c ) e. ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) limCC c ) ) ) )
189 188 adantr 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( c ( RR _D G ) ( F ` c ) <-> ( c e. ( ( int ` ( ( TopOpen ` CCfld ) |`t RR ) ) ` ( A [,] B ) ) /\ ( F ` c ) e. ( ( s e. ( ( A [,] B ) \ { c } ) |-> ( ( ( G ` s ) - ( G ` c ) ) / ( s - c ) ) ) limCC c ) ) ) )
190 41 186 189 mpbir2and 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> c ( RR _D G ) ( F ` c ) )
191 vex 
 |-  c e. _V
192 fvex 
 |-  ( F ` c ) e. _V
193 191 192 breldm 
 |-  ( c ( RR _D G ) ( F ` c ) -> c e. dom ( RR _D G ) )
194 190 193 syl 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> c e. dom ( RR _D G ) )
195 25 194 eqelssd 
 |-  ( ph -> dom ( RR _D G ) = ( A (,) B ) )
196 df-fn 
 |-  ( ( RR _D G ) Fn ( A (,) B ) <-> ( Fun ( RR _D G ) /\ dom ( RR _D G ) = ( A (,) B ) ) )
197 9 195 196 sylanbrc 
 |-  ( ph -> ( RR _D G ) Fn ( A (,) B ) )
198 16 ffnd 
 |-  ( ph -> F Fn ( A (,) B ) )
199 9 adantr 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> Fun ( RR _D G ) )
200 funbrfv 
 |-  ( Fun ( RR _D G ) -> ( c ( RR _D G ) ( F ` c ) -> ( ( RR _D G ) ` c ) = ( F ` c ) ) )
201 199 190 200 sylc 
 |-  ( ( ph /\ c e. ( A (,) B ) ) -> ( ( RR _D G ) ` c ) = ( F ` c ) )
202 197 198 201 eqfnfvd 
 |-  ( ph -> ( RR _D G ) = F )