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

Metamath Proof Explorer

Theorem ulmdvlem3

Description: Lemma for ulmdv . (Contributed by Mario Carneiro, 8-May-2015) (Proof shortened by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses ulmdv.z 
|- Z = ( ZZ>= ` M )
ulmdv.s 
|- ( ph -> S e. { RR , CC } )
ulmdv.m 
|- ( ph -> M e. ZZ )
ulmdv.f 
|- ( ph -> F : Z --> ( CC ^m X ) )
ulmdv.g 
|- ( ph -> G : X --> CC )
ulmdv.l 
|- ( ( ph /\ z e. X ) -> ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) )
ulmdv.u 
|- ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~>u ` X ) H )
Assertion ulmdvlem3 
|- ( ( ph /\ z e. X ) -> z ( S _D G ) ( H ` z ) )

Proof

Step Hyp Ref Expression
1 ulmdv.z 
 |-  Z = ( ZZ>= ` M )
2 ulmdv.s 
 |-  ( ph -> S e. { RR , CC } )
3 ulmdv.m 
 |-  ( ph -> M e. ZZ )
4 ulmdv.f 
 |-  ( ph -> F : Z --> ( CC ^m X ) )
5 ulmdv.g 
 |-  ( ph -> G : X --> CC )
6 ulmdv.l 
 |-  ( ( ph /\ z e. X ) -> ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) )
7 ulmdv.u 
 |-  ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~>u ` X ) H )
8 biidd 
 |-  ( k = M -> ( X C_ ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) <-> X C_ ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) ) )
9 1 2 3 4 5 6 7 ulmdvlem2 
 |-  ( ( ph /\ k e. Z ) -> dom ( S _D ( F ` k ) ) = X )
10 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
11 2 10 syl 
 |-  ( ph -> S C_ CC )
12 11 adantr 
 |-  ( ( ph /\ k e. Z ) -> S C_ CC )
13 4 ffvelcdmda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. ( CC ^m X ) )
14 elmapi 
 |-  ( ( F ` k ) e. ( CC ^m X ) -> ( F ` k ) : X --> CC )
15 13 14 syl 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) : X --> CC )
16 dvbsss 
 |-  dom ( S _D ( F ` k ) ) C_ S
17 9 16 eqsstrrdi 
 |-  ( ( ph /\ k e. Z ) -> X C_ S )
18 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t S ) = ( ( TopOpen ` CCfld ) |`t S )
19 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
20 12 15 17 18 19 dvbssntr 
 |-  ( ( ph /\ k e. Z ) -> dom ( S _D ( F ` k ) ) C_ ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) )
21 9 20 eqsstrrd 
 |-  ( ( ph /\ k e. Z ) -> X C_ ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) )
22 21 ralrimiva 
 |-  ( ph -> A. k e. Z X C_ ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) )
23 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
24 3 23 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
25 24 1 eleqtrrdi 
 |-  ( ph -> M e. Z )
26 8 22 25 rspcdva 
 |-  ( ph -> X C_ ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) )
27 26 sselda 
 |-  ( ( ph /\ z e. X ) -> z e. ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) )
28 ulmcl 
 |-  ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~>u ` X ) H -> H : X --> CC )
29 7 28 syl 
 |-  ( ph -> H : X --> CC )
30 29 ffvelcdmda 
 |-  ( ( ph /\ z e. X ) -> ( H ` z ) e. CC )
31 breq2 
 |-  ( s = ( ( r / 2 ) / 2 ) -> ( ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < s <-> ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) ) )
32 31 2ralbidv 
 |-  ( s = ( ( r / 2 ) / 2 ) -> ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < s <-> A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) ) )
33 32 rexralbidv 
 |-  ( s = ( ( r / 2 ) / 2 ) -> ( E. j e. Z A. n e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < s <-> E. j e. Z A. n e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) ) )
34 ulmrel 
 |-  Rel ( ~~>u ` X )
35 releldm 
 |-  ( ( Rel ( ~~>u ` X ) /\ ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~>u ` X ) H ) -> ( k e. Z |-> ( S _D ( F ` k ) ) ) e. dom ( ~~>u ` X ) )
36 34 7 35 sylancr 
 |-  ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) e. dom ( ~~>u ` X ) )
37 ulmscl 
 |-  ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~>u ` X ) H -> X e. _V )
38 7 37 syl 
 |-  ( ph -> X e. _V )
39 ovex 
 |-  ( S _D ( F ` k ) ) e. _V
40 39 rgenw 
 |-  A. k e. Z ( S _D ( F ` k ) ) e. _V
41 eqid 
 |-  ( k e. Z |-> ( S _D ( F ` k ) ) ) = ( k e. Z |-> ( S _D ( F ` k ) ) )
42 41 fnmpt 
 |-  ( A. k e. Z ( S _D ( F ` k ) ) e. _V -> ( k e. Z |-> ( S _D ( F ` k ) ) ) Fn Z )
43 40 42 mp1i 
 |-  ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) Fn Z )
44 ulmf2 
 |-  ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) Fn Z /\ ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~>u ` X ) H ) -> ( k e. Z |-> ( S _D ( F ` k ) ) ) : Z --> ( CC ^m X ) )
45 43 7 44 syl2anc 
 |-  ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) : Z --> ( CC ^m X ) )
46 1 3 38 45 ulmcau2 
 |-  ( ph -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) e. dom ( ~~>u ` X ) <-> A. s e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) ` x ) - ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` m ) ` x ) ) ) < s ) )
47 36 46 mpbid 
 |-  ( ph -> A. s e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) ` x ) - ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` m ) ` x ) ) ) < s )
48 1 uztrn2 
 |-  ( ( j e. Z /\ n e. ( ZZ>= ` j ) ) -> n e. Z )
49 48 ad2ant2lr 
 |-  ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> n e. Z )
50 fveq2 
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
51 50 oveq2d 
 |-  ( k = n -> ( S _D ( F ` k ) ) = ( S _D ( F ` n ) ) )
52 ovex 
 |-  ( S _D ( F ` n ) ) e. _V
53 51 41 52 fvmpt 
 |-  ( n e. Z -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) = ( S _D ( F ` n ) ) )
54 49 53 syl 
 |-  ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) = ( S _D ( F ` n ) ) )
55 54 fveq1d 
 |-  ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) ` x ) = ( ( S _D ( F ` n ) ) ` x ) )
56 simprr 
 |-  ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> m e. ( ZZ>= ` n ) )
57 1 uztrn2 
 |-  ( ( n e. Z /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
58 49 56 57 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> m e. Z )
59 fveq2 
 |-  ( k = m -> ( F ` k ) = ( F ` m ) )
60 59 oveq2d 
 |-  ( k = m -> ( S _D ( F ` k ) ) = ( S _D ( F ` m ) ) )
61 ovex 
 |-  ( S _D ( F ` m ) ) e. _V
62 60 41 61 fvmpt 
 |-  ( m e. Z -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` m ) = ( S _D ( F ` m ) ) )
63 58 62 syl 
 |-  ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` m ) = ( S _D ( F ` m ) ) )
64 63 fveq1d 
 |-  ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` m ) ` x ) = ( ( S _D ( F ` m ) ) ` x ) )
65 55 64 oveq12d 
 |-  ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> ( ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) ` x ) - ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` m ) ` x ) ) = ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) )
66 65 fveq2d 
 |-  ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> ( abs ` ( ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) ` x ) - ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` m ) ` x ) ) ) = ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) )
67 66 breq1d 
 |-  ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> ( ( abs ` ( ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) ` x ) - ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` m ) ` x ) ) ) < s <-> ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < s ) )
68 67 ralbidv 
 |-  ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> ( A. x e. X ( abs ` ( ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) ` x ) - ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` m ) ` x ) ) ) < s <-> A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < s ) )
69 68 2ralbidva 
 |-  ( ( ph /\ j e. Z ) -> ( A. n e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) ` x ) - ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` m ) ` x ) ) ) < s <-> A. n e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < s ) )
70 69 rexbidva 
 |-  ( ph -> ( E. j e. Z A. n e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) ` x ) - ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` m ) ` x ) ) ) < s <-> E. j e. Z A. n e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < s ) )
71 70 ralbidv 
 |-  ( ph -> ( A. s e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) ` x ) - ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` m ) ` x ) ) ) < s <-> A. s e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < s ) )
72 47 71 mpbid 
 |-  ( ph -> A. s e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < s )
73 72 ad2antrr 
 |-  ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> A. s e. RR+ E. j e. Z A. n e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < s )
74 rphalfcl 
 |-  ( r e. RR+ -> ( r / 2 ) e. RR+ )
75 74 adantl 
 |-  ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( r / 2 ) e. RR+ )
76 rphalfcl 
 |-  ( ( r / 2 ) e. RR+ -> ( ( r / 2 ) / 2 ) e. RR+ )
77 75 76 syl 
 |-  ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( ( r / 2 ) / 2 ) e. RR+ )
78 33 73 77 rspcdva 
 |-  ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> E. j e. Z A. n e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) )
79 3 ad2antrr 
 |-  ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> M e. ZZ )
80 51 fveq1d 
 |-  ( k = n -> ( ( S _D ( F ` k ) ) ` z ) = ( ( S _D ( F ` n ) ) ` z ) )
81 eqid 
 |-  ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) ) = ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) )
82 fvex 
 |-  ( ( S _D ( F ` n ) ) ` z ) e. _V
83 80 81 82 fvmpt 
 |-  ( n e. Z -> ( ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) ) ` n ) = ( ( S _D ( F ` n ) ) ` z ) )
84 83 adantl 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) ) ` n ) = ( ( S _D ( F ` n ) ) ` z ) )
85 45 ad2antrr 
 |-  ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( k e. Z |-> ( S _D ( F ` k ) ) ) : Z --> ( CC ^m X ) )
86 simplr 
 |-  ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> z e. X )
87 1 fvexi 
 |-  Z e. _V
88 87 mptex 
 |-  ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) ) e. _V
89 88 a1i 
 |-  ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) ) e. _V )
90 53 adantl 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) = ( S _D ( F ` n ) ) )
91 90 fveq1d 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) ` z ) = ( ( S _D ( F ` n ) ) ` z ) )
92 91 84 eqtr4d 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) ` z ) = ( ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) ) ` n ) )
93 7 ad2antrr 
 |-  ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~>u ` X ) H )
94 1 79 85 86 89 92 93 ulmclm 
 |-  ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) ) ~~> ( H ` z ) )
95 1 79 75 84 94 climi2 
 |-  ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) )
96 1 rexanuz2 
 |-  ( E. j e. Z A. n e. ( ZZ>= ` j ) ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) <-> ( E. j e. Z A. n e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) )
97 1 r19.2uz 
 |-  ( E. j e. Z A. n e. ( ZZ>= ` j ) ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) -> E. n e. Z ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) )
98 96 97 sylbir 
 |-  ( ( E. j e. Z A. n e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) -> E. n e. Z ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) )
99 fveq2 
 |-  ( y = v -> ( ( F ` n ) ` y ) = ( ( F ` n ) ` v ) )
100 99 oveq1d 
 |-  ( y = v -> ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) = ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) )
101 oveq1 
 |-  ( y = v -> ( y - z ) = ( v - z ) )
102 100 101 oveq12d 
 |-  ( y = v -> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) = ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) )
103 eqid 
 |-  ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) = ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) )
104 ovex 
 |-  ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) e. _V
105 102 103 104 fvmpt 
 |-  ( v e. ( X \ { z } ) -> ( ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) ` v ) = ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) )
106 105 fvoveq1d 
 |-  ( v e. ( X \ { z } ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) ` v ) - ( ( S _D ( F ` n ) ) ` z ) ) ) = ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) )
107 id 
 |-  ( s = ( ( r / 2 ) / 2 ) -> s = ( ( r / 2 ) / 2 ) )
108 106 107 breqan12rd 
 |-  ( ( s = ( ( r / 2 ) / 2 ) /\ v e. ( X \ { z } ) ) -> ( ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) ` v ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < s <-> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) )
109 108 imbi2d 
 |-  ( ( s = ( ( r / 2 ) / 2 ) /\ v e. ( X \ { z } ) ) -> ( ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) ` v ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < s ) <-> ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) ) )
110 109 ralbidva 
 |-  ( s = ( ( r / 2 ) / 2 ) -> ( A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) ` v ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < s ) <-> A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) ) )
111 110 rexbidv 
 |-  ( s = ( ( r / 2 ) / 2 ) -> ( E. w e. RR+ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) ` v ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < s ) <-> E. w e. RR+ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) ) )
112 simpllr 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> z e. X )
113 85 ffvelcdmda 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) e. ( CC ^m X ) )
114 90 113 eqeltrrd 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( S _D ( F ` n ) ) e. ( CC ^m X ) )
115 elmapi 
 |-  ( ( S _D ( F ` n ) ) e. ( CC ^m X ) -> ( S _D ( F ` n ) ) : X --> CC )
116 fdm 
 |-  ( ( S _D ( F ` n ) ) : X --> CC -> dom ( S _D ( F ` n ) ) = X )
117 114 115 116 3syl 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> dom ( S _D ( F ` n ) ) = X )
118 112 117 eleqtrrd 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> z e. dom ( S _D ( F ` n ) ) )
119 2 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> S e. { RR , CC } )
120 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D ( F ` n ) ) : dom ( S _D ( F ` n ) ) --> CC )
121 ffun 
 |-  ( ( S _D ( F ` n ) ) : dom ( S _D ( F ` n ) ) --> CC -> Fun ( S _D ( F ` n ) ) )
122 funfvbrb 
 |-  ( Fun ( S _D ( F ` n ) ) -> ( z e. dom ( S _D ( F ` n ) ) <-> z ( S _D ( F ` n ) ) ( ( S _D ( F ` n ) ) ` z ) ) )
123 119 120 121 122 4syl 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( z e. dom ( S _D ( F ` n ) ) <-> z ( S _D ( F ` n ) ) ( ( S _D ( F ` n ) ) ` z ) ) )
124 118 123 mpbid 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> z ( S _D ( F ` n ) ) ( ( S _D ( F ` n ) ) ` z ) )
125 119 10 syl 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> S C_ CC )
126 4 ad2antrr 
 |-  ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> F : Z --> ( CC ^m X ) )
127 126 ffvelcdmda 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( F ` n ) e. ( CC ^m X ) )
128 elmapi 
 |-  ( ( F ` n ) e. ( CC ^m X ) -> ( F ` n ) : X --> CC )
129 127 128 syl 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( F ` n ) : X --> CC )
130 biidd 
 |-  ( k = M -> ( X C_ S <-> X C_ S ) )
131 17 ralrimiva 
 |-  ( ph -> A. k e. Z X C_ S )
132 130 131 25 rspcdva 
 |-  ( ph -> X C_ S )
133 132 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> X C_ S )
134 18 19 103 125 129 133 eldv 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( z ( S _D ( F ` n ) ) ( ( S _D ( F ` n ) ) ` z ) <-> ( z e. ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) /\ ( ( S _D ( F ` n ) ) ` z ) e. ( ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) limCC z ) ) ) )
135 124 134 mpbid 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( z e. ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) /\ ( ( S _D ( F ` n ) ) ` z ) e. ( ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) limCC z ) ) )
136 135 simprd 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( ( S _D ( F ` n ) ) ` z ) e. ( ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) limCC z ) )
137 132 adantr 
 |-  ( ( ph /\ z e. X ) -> X C_ S )
138 11 adantr 
 |-  ( ( ph /\ z e. X ) -> S C_ CC )
139 137 138 sstrd 
 |-  ( ( ph /\ z e. X ) -> X C_ CC )
140 139 ad2antrr 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> X C_ CC )
141 129 140 112 dvlem 
 |-  ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) /\ y e. ( X \ { z } ) ) -> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) e. CC )
142 141 fmpttd 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) : ( X \ { z } ) --> CC )
143 140 ssdifssd 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( X \ { z } ) C_ CC )
144 140 112 sseldd 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> z e. CC )
145 142 143 144 ellimc3 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( ( ( S _D ( F ` n ) ) ` z ) e. ( ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) limCC z ) <-> ( ( ( S _D ( F ` n ) ) ` z ) e. CC /\ A. s e. RR+ E. w e. RR+ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) ` v ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < s ) ) ) )
146 136 145 mpbid 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( ( ( S _D ( F ` n ) ) ` z ) e. CC /\ A. s e. RR+ E. w e. RR+ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) ` v ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < s ) ) )
147 146 simprd 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> A. s e. RR+ E. w e. RR+ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) ` v ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < s ) )
148 77 adantr 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( ( r / 2 ) / 2 ) e. RR+ )
149 111 147 148 rspcdva 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> E. w e. RR+ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) )
150 149 adantrr 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) -> E. w e. RR+ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) )
151 anass 
 |-  ( ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) ) /\ w e. RR+ ) <-> ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) ) )
152 df-3an 
 |-  ( ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) <-> ( ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) )
153 anass 
 |-  ( ( ( ph /\ z e. X ) /\ r e. RR+ ) <-> ( ph /\ ( z e. X /\ r e. RR+ ) ) )
154 6 ralrimiva 
 |-  ( ph -> A. z e. X ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) )
155 fveq2 
 |-  ( z = s -> ( ( F ` k ) ` z ) = ( ( F ` k ) ` s ) )
156 155 mpteq2dv 
 |-  ( z = s -> ( k e. Z |-> ( ( F ` k ) ` z ) ) = ( k e. Z |-> ( ( F ` k ) ` s ) ) )
157 fveq2 
 |-  ( z = s -> ( G ` z ) = ( G ` s ) )
158 156 157 breq12d 
 |-  ( z = s -> ( ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) <-> ( k e. Z |-> ( ( F ` k ) ` s ) ) ~~> ( G ` s ) ) )
159 158 rspccva 
 |-  ( ( A. z e. X ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) /\ s e. X ) -> ( k e. Z |-> ( ( F ` k ) ` s ) ) ~~> ( G ` s ) )
160 154 159 sylan 
 |-  ( ( ph /\ s e. X ) -> ( k e. Z |-> ( ( F ` k ) ` s ) ) ~~> ( G ` s ) )
161 simprll 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> z e. X )
162 simprlr 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> r e. RR+ )
163 simprr3 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) )
164 simplll 
 |-  ( ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) -> u e. RR+ )
165 163 164 syl 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> u e. RR+ )
166 simplr 
 |-  ( ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) -> w e. RR+ )
167 163 166 syl 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> w e. RR+ )
168 simpllr 
 |-  ( ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) -> ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) )
169 163 168 syl 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) )
170 169 simpld 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> u < w )
171 169 simprd 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X )
172 simpr3 
 |-  ( ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) -> ( v =/= z /\ ( abs ` ( v - z ) ) < u ) )
173 163 172 syl 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> ( v =/= z /\ ( abs ` ( v - z ) ) < u ) )
174 173 simprd 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> ( abs ` ( v - z ) ) < u )
175 simprr1 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> n e. Z )
176 simprr2 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) )
177 176 simpld 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) )
178 176 simprd 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) )
179 simpr1 
 |-  ( ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) -> v e. ( X \ { z } ) )
180 163 179 syl 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> v e. ( X \ { z } ) )
181 180 eldifad 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> v e. X )
182 173 simpld 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> v =/= z )
183 simpr2 
 |-  ( ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) -> ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) )
184 163 183 syl 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) )
185 182 184 mpand 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> ( ( abs ` ( v - z ) ) < w -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) )
186 1 2 3 4 5 160 7 161 162 165 167 170 171 174 175 177 178 181 182 185 ulmdvlem1 
 |-  ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> ( abs ` ( ( ( ( G ` v ) - ( G ` z ) ) / ( v - z ) ) - ( H ` z ) ) ) < r )
187 186 anassrs 
 |-  ( ( ( ph /\ ( z e. X /\ r e. RR+ ) ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) -> ( abs ` ( ( ( ( G ` v ) - ( G ` z ) ) / ( v - z ) ) - ( H ` z ) ) ) < r )
188 153 187 sylanb 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) -> ( abs ` ( ( ( ( G ` v ) - ( G ` z ) ) / ( v - z ) ) - ( H ` z ) ) ) < r )
189 152 188 sylan2br 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) -> ( abs ` ( ( ( ( G ` v ) - ( G ` z ) ) / ( v - z ) ) - ( H ` z ) ) ) < r )
190 189 anassrs 
 |-  ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) -> ( abs ` ( ( ( ( G ` v ) - ( G ` z ) ) / ( v - z ) ) - ( H ` z ) ) ) < r )
191 190 anassrs 
 |-  ( ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) -> ( abs ` ( ( ( ( G ` v ) - ( G ` z ) ) / ( v - z ) ) - ( H ` z ) ) ) < r )
192 151 191 sylanb 
 |-  ( ( ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) -> ( abs ` ( ( ( ( G ` v ) - ( G ` z ) ) / ( v - z ) ) - ( H ` z ) ) ) < r )
193 192 3exp2 
 |-  ( ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) ) /\ w e. RR+ ) -> ( v e. ( X \ { z } ) -> ( ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) -> ( ( v =/= z /\ ( abs ` ( v - z ) ) < u ) -> ( abs ` ( ( ( ( G ` v ) - ( G ` z ) ) / ( v - z ) ) - ( H ` z ) ) ) < r ) ) ) )
194 193 imp 
 |-  ( ( ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) ) /\ w e. RR+ ) /\ v e. ( X \ { z } ) ) -> ( ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) -> ( ( v =/= z /\ ( abs ` ( v - z ) ) < u ) -> ( abs ` ( ( ( ( G ` v ) - ( G ` z ) ) / ( v - z ) ) - ( H ` z ) ) ) < r ) ) )
195 fveq2 
 |-  ( y = v -> ( G ` y ) = ( G ` v ) )
196 195 oveq1d 
 |-  ( y = v -> ( ( G ` y ) - ( G ` z ) ) = ( ( G ` v ) - ( G ` z ) ) )
197 196 101 oveq12d 
 |-  ( y = v -> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) = ( ( ( G ` v ) - ( G ` z ) ) / ( v - z ) ) )
198 eqid 
 |-  ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) = ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) )
199 ovex 
 |-  ( ( ( G ` v ) - ( G ` z ) ) / ( v - z ) ) e. _V
200 197 198 199 fvmpt 
 |-  ( v e. ( X \ { z } ) -> ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) ` v ) = ( ( ( G ` v ) - ( G ` z ) ) / ( v - z ) ) )
201 200 fvoveq1d 
 |-  ( v e. ( X \ { z } ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) ` v ) - ( H ` z ) ) ) = ( abs ` ( ( ( ( G ` v ) - ( G ` z ) ) / ( v - z ) ) - ( H ` z ) ) ) )
202 201 breq1d 
 |-  ( v e. ( X \ { z } ) -> ( ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) ` v ) - ( H ` z ) ) ) < r <-> ( abs ` ( ( ( ( G ` v ) - ( G ` z ) ) / ( v - z ) ) - ( H ` z ) ) ) < r ) )
203 202 imbi2d 
 |-  ( v e. ( X \ { z } ) -> ( ( ( v =/= z /\ ( abs ` ( v - z ) ) < u ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) ` v ) - ( H ` z ) ) ) < r ) <-> ( ( v =/= z /\ ( abs ` ( v - z ) ) < u ) -> ( abs ` ( ( ( ( G ` v ) - ( G ` z ) ) / ( v - z ) ) - ( H ` z ) ) ) < r ) ) )
204 203 adantl 
 |-  ( ( ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) ) /\ w e. RR+ ) /\ v e. ( X \ { z } ) ) -> ( ( ( v =/= z /\ ( abs ` ( v - z ) ) < u ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) ` v ) - ( H ` z ) ) ) < r ) <-> ( ( v =/= z /\ ( abs ` ( v - z ) ) < u ) -> ( abs ` ( ( ( ( G ` v ) - ( G ` z ) ) / ( v - z ) ) - ( H ` z ) ) ) < r ) ) )
205 194 204 sylibrd 
 |-  ( ( ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) ) /\ w e. RR+ ) /\ v e. ( X \ { z } ) ) -> ( ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) -> ( ( v =/= z /\ ( abs ` ( v - z ) ) < u ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) ` v ) - ( H ` z ) ) ) < r ) ) )
206 205 ralimdva 
 |-  ( ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) ) /\ w e. RR+ ) -> ( A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) -> A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < u ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) ` v ) - ( H ` z ) ) ) < r ) ) )
207 206 impr 
 |-  ( ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) ) /\ ( w e. RR+ /\ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) ) ) -> A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < u ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) ` v ) - ( H ` z ) ) ) < r ) )
208 207 an32s 
 |-  ( ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( w e. RR+ /\ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) ) ) /\ ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) ) -> A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < u ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) ` v ) - ( H ` z ) ) ) < r ) )
209 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
210 xmetres2 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ S C_ CC ) -> ( ( abs o. - ) |` ( S X. S ) ) e. ( *Met ` S ) )
211 209 138 210 sylancr 
 |-  ( ( ph /\ z e. X ) -> ( ( abs o. - ) |` ( S X. S ) ) e. ( *Met ` S ) )
212 211 ad3antrrr 
 |-  ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( w e. RR+ /\ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) ) ) -> ( ( abs o. - ) |` ( S X. S ) ) e. ( *Met ` S ) )
213 19 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
214 resttop 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ S e. { RR , CC } ) -> ( ( TopOpen ` CCfld ) |`t S ) e. Top )
215 213 2 214 sylancr 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t S ) e. Top )
216 19 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
217 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) )
218 216 11 217 sylancr 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) )
219 toponuni 
 |-  ( ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) -> S = U. ( ( TopOpen ` CCfld ) |`t S ) )
220 218 219 syl 
 |-  ( ph -> S = U. ( ( TopOpen ` CCfld ) |`t S ) )
221 132 220 sseqtrd 
 |-  ( ph -> X C_ U. ( ( TopOpen ` CCfld ) |`t S ) )
222 eqid 
 |-  U. ( ( TopOpen ` CCfld ) |`t S ) = U. ( ( TopOpen ` CCfld ) |`t S )
223 222 ntrss2 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t S ) e. Top /\ X C_ U. ( ( TopOpen ` CCfld ) |`t S ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) C_ X )
224 215 221 223 syl2anc 
 |-  ( ph -> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) C_ X )
225 224 26 eqssd 
 |-  ( ph -> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) = X )
226 222 isopn3 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t S ) e. Top /\ X C_ U. ( ( TopOpen ` CCfld ) |`t S ) ) -> ( X e. ( ( TopOpen ` CCfld ) |`t S ) <-> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) = X ) )
227 215 221 226 syl2anc 
 |-  ( ph -> ( X e. ( ( TopOpen ` CCfld ) |`t S ) <-> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) = X ) )
228 225 227 mpbird 
 |-  ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
229 eqid 
 |-  ( ( abs o. - ) |` ( S X. S ) ) = ( ( abs o. - ) |` ( S X. S ) )
230 19 cnfldtopn 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
231 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) )
232 229 230 231 metrest 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` CCfld ) |`t S ) = ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) )
233 209 11 232 sylancr 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t S ) = ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) )
234 228 233 eleqtrd 
 |-  ( ph -> X e. ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) )
235 234 adantr 
 |-  ( ( ph /\ z e. X ) -> X e. ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) )
236 235 ad3antrrr 
 |-  ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( w e. RR+ /\ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) ) ) -> X e. ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) )
237 86 ad2antrr 
 |-  ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( w e. RR+ /\ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) ) ) -> z e. X )
238 simprl 
 |-  ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( w e. RR+ /\ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) ) ) -> w e. RR+ )
239 231 mopni3 
 |-  ( ( ( ( ( abs o. - ) |` ( S X. S ) ) e. ( *Met ` S ) /\ X e. ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) /\ z e. X ) /\ w e. RR+ ) -> E. u e. RR+ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) )
240 212 236 237 238 239 syl31anc 
 |-  ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( w e. RR+ /\ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) ) ) -> E. u e. RR+ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) )
241 208 240 reximddv 
 |-  ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) /\ ( w e. RR+ /\ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) ) ) -> E. u e. RR+ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < u ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) ` v ) - ( H ` z ) ) ) < r ) )
242 150 241 rexlimddv 
 |-  ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) ) ) -> E. u e. RR+ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < u ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) ` v ) - ( H ` z ) ) ) < r ) )
243 242 rexlimdvaa 
 |-  ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( E. n e. Z ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) -> E. u e. RR+ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < u ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) ` v ) - ( H ` z ) ) ) < r ) ) )
244 98 243 syl5 
 |-  ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( ( E. j e. Z A. n e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ E. j e. Z A. n e. ( ZZ>= ` j ) ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) -> E. u e. RR+ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < u ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) ` v ) - ( H ` z ) ) ) < r ) ) )
245 78 95 244 mp2and 
 |-  ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> E. u e. RR+ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < u ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) ` v ) - ( H ` z ) ) ) < r ) )
246 245 ralrimiva 
 |-  ( ( ph /\ z e. X ) -> A. r e. RR+ E. u e. RR+ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < u ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) ` v ) - ( H ` z ) ) ) < r ) )
247 5 adantr 
 |-  ( ( ph /\ z e. X ) -> G : X --> CC )
248 simpr 
 |-  ( ( ph /\ z e. X ) -> z e. X )
249 247 139 248 dvlem 
 |-  ( ( ( ph /\ z e. X ) /\ y e. ( X \ { z } ) ) -> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) e. CC )
250 249 fmpttd 
 |-  ( ( ph /\ z e. X ) -> ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) : ( X \ { z } ) --> CC )
251 139 ssdifssd 
 |-  ( ( ph /\ z e. X ) -> ( X \ { z } ) C_ CC )
252 139 248 sseldd 
 |-  ( ( ph /\ z e. X ) -> z e. CC )
253 250 251 252 ellimc3 
 |-  ( ( ph /\ z e. X ) -> ( ( H ` z ) e. ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) limCC z ) <-> ( ( H ` z ) e. CC /\ A. r e. RR+ E. u e. RR+ A. v e. ( X \ { z } ) ( ( v =/= z /\ ( abs ` ( v - z ) ) < u ) -> ( abs ` ( ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) ` v ) - ( H ` z ) ) ) < r ) ) ) )
254 30 246 253 mpbir2and 
 |-  ( ( ph /\ z e. X ) -> ( H ` z ) e. ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) limCC z ) )
255 18 19 198 138 247 137 eldv 
 |-  ( ( ph /\ z e. X ) -> ( z ( S _D G ) ( H ` z ) <-> ( z e. ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` X ) /\ ( H ` z ) e. ( ( y e. ( X \ { z } ) |-> ( ( ( G ` y ) - ( G ` z ) ) / ( y - z ) ) ) limCC z ) ) ) )
256 27 254 255 mpbir2and 
 |-  ( ( ph /\ z e. X ) -> z ( S _D G ) ( H ` z ) )