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
|
ffvelrnda |
|- ( ( 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
|
ffvelrnda |
|- ( ( 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
|
ffvelrnda |
|- ( ( ( ( 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
|
ffvelrnda |
|- ( ( ( ( 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 ) ) |