Metamath Proof Explorer

Theorem ulmdvlem1

Description: Lemma for ulmdv . (Contributed by Mario Carneiro, 3-Mar-2015)

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 )
ulmdvlem1.c 
|- ( ( ph /\ ps ) -> C e. X )
ulmdvlem1.r 
|- ( ( ph /\ ps ) -> R e. RR+ )
ulmdvlem1.u 
|- ( ( ph /\ ps ) -> U e. RR+ )
ulmdvlem1.v 
|- ( ( ph /\ ps ) -> W e. RR+ )
ulmdvlem1.l 
|- ( ( ph /\ ps ) -> U < W )
ulmdvlem1.b 
|- ( ( ph /\ ps ) -> ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) C_ X )
ulmdvlem1.a 
|- ( ( ph /\ ps ) -> ( abs ` ( Y - C ) ) < U )
ulmdvlem1.n 
|- ( ( ph /\ ps ) -> N e. Z )
ulmdvlem1.1 
|- ( ( ph /\ ps ) -> A. m e. ( ZZ>= ` N ) A. x e. X ( abs ` ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( R / 2 ) / 2 ) )
ulmdvlem1.2 
|- ( ( ph /\ ps ) -> ( abs ` ( ( ( S _D ( F ` N ) ) ` C ) - ( H ` C ) ) ) < ( R / 2 ) )
ulmdvlem1.y 
|- ( ( ph /\ ps ) -> Y e. X )
ulmdvlem1.3 
|- ( ( ph /\ ps ) -> Y =/= C )
ulmdvlem1.4 
|- ( ( ph /\ ps ) -> ( ( abs ` ( Y - C ) ) < W -> ( abs ` ( ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) - ( ( S _D ( F ` N ) ) ` C ) ) ) < ( ( R / 2 ) / 2 ) ) )
Assertion ulmdvlem1 
|- ( ( ph /\ ps ) -> ( abs ` ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( H ` C ) ) ) < R )

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 ulmdvlem1.c 
 |-  ( ( ph /\ ps ) -> C e. X )
9 ulmdvlem1.r 
 |-  ( ( ph /\ ps ) -> R e. RR+ )
10 ulmdvlem1.u 
 |-  ( ( ph /\ ps ) -> U e. RR+ )
11 ulmdvlem1.v 
 |-  ( ( ph /\ ps ) -> W e. RR+ )
12 ulmdvlem1.l 
 |-  ( ( ph /\ ps ) -> U < W )
13 ulmdvlem1.b 
 |-  ( ( ph /\ ps ) -> ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) C_ X )
14 ulmdvlem1.a 
 |-  ( ( ph /\ ps ) -> ( abs ` ( Y - C ) ) < U )
15 ulmdvlem1.n 
 |-  ( ( ph /\ ps ) -> N e. Z )
16 ulmdvlem1.1 
 |-  ( ( ph /\ ps ) -> A. m e. ( ZZ>= ` N ) A. x e. X ( abs ` ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( R / 2 ) / 2 ) )
17 ulmdvlem1.2 
 |-  ( ( ph /\ ps ) -> ( abs ` ( ( ( S _D ( F ` N ) ) ` C ) - ( H ` C ) ) ) < ( R / 2 ) )
18 ulmdvlem1.y 
 |-  ( ( ph /\ ps ) -> Y e. X )
19 ulmdvlem1.3 
 |-  ( ( ph /\ ps ) -> Y =/= C )
20 ulmdvlem1.4 
 |-  ( ( ph /\ ps ) -> ( ( abs ` ( Y - C ) ) < W -> ( abs ` ( ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) - ( ( S _D ( F ` N ) ) ` C ) ) ) < ( ( R / 2 ) / 2 ) ) )
21 5 adantr 
 |-  ( ( ph /\ ps ) -> G : X --> CC )
22 21 18 ffvelcdmd 
 |-  ( ( ph /\ ps ) -> ( G ` Y ) e. CC )
23 21 8 ffvelcdmd 
 |-  ( ( ph /\ ps ) -> ( G ` C ) e. CC )
24 22 23 subcld 
 |-  ( ( ph /\ ps ) -> ( ( G ` Y ) - ( G ` C ) ) e. CC )
25 fveq2 
 |-  ( k = N -> ( F ` k ) = ( F ` N ) )
26 25 oveq2d 
 |-  ( k = N -> ( S _D ( F ` k ) ) = ( S _D ( F ` N ) ) )
27 eqid 
 |-  ( k e. Z |-> ( S _D ( F ` k ) ) ) = ( k e. Z |-> ( S _D ( F ` k ) ) )
28 ovex 
 |-  ( S _D ( F ` N ) ) e. _V
29 26 27 28 fvmpt 
 |-  ( N e. Z -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` N ) = ( S _D ( F ` N ) ) )
30 15 29 syl 
 |-  ( ( ph /\ ps ) -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` N ) = ( S _D ( F ` N ) ) )
31 ovex 
 |-  ( S _D ( F ` k ) ) e. _V
32 31 rgenw 
 |-  A. k e. Z ( S _D ( F ` k ) ) e. _V
33 27 fnmpt 
 |-  ( A. k e. Z ( S _D ( F ` k ) ) e. _V -> ( k e. Z |-> ( S _D ( F ` k ) ) ) Fn Z )
34 32 33 mp1i 
 |-  ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) Fn Z )
35 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 ) )
36 34 7 35 syl2anc 
 |-  ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) : Z --> ( CC ^m X ) )
37 36 adantr 
 |-  ( ( ph /\ ps ) -> ( k e. Z |-> ( S _D ( F ` k ) ) ) : Z --> ( CC ^m X ) )
38 37 15 ffvelcdmd 
 |-  ( ( ph /\ ps ) -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` N ) e. ( CC ^m X ) )
39 30 38 eqeltrrd 
 |-  ( ( ph /\ ps ) -> ( S _D ( F ` N ) ) e. ( CC ^m X ) )
40 elmapi 
 |-  ( ( S _D ( F ` N ) ) e. ( CC ^m X ) -> ( S _D ( F ` N ) ) : X --> CC )
41 39 40 syl 
 |-  ( ( ph /\ ps ) -> ( S _D ( F ` N ) ) : X --> CC )
42 41 fdmd 
 |-  ( ( ph /\ ps ) -> dom ( S _D ( F ` N ) ) = X )
43 dvbsss 
 |-  dom ( S _D ( F ` N ) ) C_ S
44 42 43 eqsstrrdi 
 |-  ( ( ph /\ ps ) -> X C_ S )
45 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
46 2 45 syl 
 |-  ( ph -> S C_ CC )
47 46 adantr 
 |-  ( ( ph /\ ps ) -> S C_ CC )
48 44 47 sstrd 
 |-  ( ( ph /\ ps ) -> X C_ CC )
49 48 18 sseldd 
 |-  ( ( ph /\ ps ) -> Y e. CC )
50 48 8 sseldd 
 |-  ( ( ph /\ ps ) -> C e. CC )
51 49 50 subcld 
 |-  ( ( ph /\ ps ) -> ( Y - C ) e. CC )
52 49 50 19 subne0d 
 |-  ( ( ph /\ ps ) -> ( Y - C ) =/= 0 )
53 24 51 52 divcld 
 |-  ( ( ph /\ ps ) -> ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) e. CC )
54 ulmcl 
 |-  ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~>u ` X ) H -> H : X --> CC )
55 7 54 syl 
 |-  ( ph -> H : X --> CC )
56 55 adantr 
 |-  ( ( ph /\ ps ) -> H : X --> CC )
57 56 8 ffvelcdmd 
 |-  ( ( ph /\ ps ) -> ( H ` C ) e. CC )
58 41 8 ffvelcdmd 
 |-  ( ( ph /\ ps ) -> ( ( S _D ( F ` N ) ) ` C ) e. CC )
59 9 rpred 
 |-  ( ( ph /\ ps ) -> R e. RR )
60 53 58 subcld 
 |-  ( ( ph /\ ps ) -> ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( ( S _D ( F ` N ) ) ` C ) ) e. CC )
61 60 abscld 
 |-  ( ( ph /\ ps ) -> ( abs ` ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( ( S _D ( F ` N ) ) ` C ) ) ) e. RR )
62 4 adantr 
 |-  ( ( ph /\ ps ) -> F : Z --> ( CC ^m X ) )
63 62 15 ffvelcdmd 
 |-  ( ( ph /\ ps ) -> ( F ` N ) e. ( CC ^m X ) )
64 elmapi 
 |-  ( ( F ` N ) e. ( CC ^m X ) -> ( F ` N ) : X --> CC )
65 63 64 syl 
 |-  ( ( ph /\ ps ) -> ( F ` N ) : X --> CC )
66 65 18 ffvelcdmd 
 |-  ( ( ph /\ ps ) -> ( ( F ` N ) ` Y ) e. CC )
67 65 8 ffvelcdmd 
 |-  ( ( ph /\ ps ) -> ( ( F ` N ) ` C ) e. CC )
68 66 67 subcld 
 |-  ( ( ph /\ ps ) -> ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) e. CC )
69 68 51 52 divcld 
 |-  ( ( ph /\ ps ) -> ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) e. CC )
70 53 69 subcld 
 |-  ( ( ph /\ ps ) -> ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) ) e. CC )
71 70 abscld 
 |-  ( ( ph /\ ps ) -> ( abs ` ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) ) ) e. RR )
72 69 58 subcld 
 |-  ( ( ph /\ ps ) -> ( ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) - ( ( S _D ( F ` N ) ) ` C ) ) e. CC )
73 72 abscld 
 |-  ( ( ph /\ ps ) -> ( abs ` ( ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) - ( ( S _D ( F ` N ) ) ` C ) ) ) e. RR )
74 71 73 readdcld 
 |-  ( ( ph /\ ps ) -> ( ( abs ` ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) ) ) + ( abs ` ( ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) - ( ( S _D ( F ` N ) ) ` C ) ) ) ) e. RR )
75 59 rehalfcld 
 |-  ( ( ph /\ ps ) -> ( R / 2 ) e. RR )
76 53 58 69 abs3difd 
 |-  ( ( ph /\ ps ) -> ( abs ` ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( ( S _D ( F ` N ) ) ` C ) ) ) <_ ( ( abs ` ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) ) ) + ( abs ` ( ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) - ( ( S _D ( F ` N ) ) ` C ) ) ) ) )
77 75 rehalfcld 
 |-  ( ( ph /\ ps ) -> ( ( R / 2 ) / 2 ) e. RR )
78 22 66 23 67 sub4d 
 |-  ( ( ph /\ ps ) -> ( ( ( G ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( G ` C ) - ( ( F ` N ) ` C ) ) ) = ( ( ( G ` Y ) - ( G ` C ) ) - ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) ) )
79 78 oveq1d 
 |-  ( ( ph /\ ps ) -> ( ( ( ( G ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( G ` C ) - ( ( F ` N ) ` C ) ) ) / ( Y - C ) ) = ( ( ( ( G ` Y ) - ( G ` C ) ) - ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) ) / ( Y - C ) ) )
80 24 68 51 52 divsubdird 
 |-  ( ( ph /\ ps ) -> ( ( ( ( G ` Y ) - ( G ` C ) ) - ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) ) / ( Y - C ) ) = ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) ) )
81 79 80 eqtrd 
 |-  ( ( ph /\ ps ) -> ( ( ( ( G ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( G ` C ) - ( ( F ` N ) ` C ) ) ) / ( Y - C ) ) = ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) ) )
82 81 fveq2d 
 |-  ( ( ph /\ ps ) -> ( abs ` ( ( ( ( G ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( G ` C ) - ( ( F ` N ) ` C ) ) ) / ( Y - C ) ) ) = ( abs ` ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) ) ) )
83 22 66 subcld 
 |-  ( ( ph /\ ps ) -> ( ( G ` Y ) - ( ( F ` N ) ` Y ) ) e. CC )
84 23 67 subcld 
 |-  ( ( ph /\ ps ) -> ( ( G ` C ) - ( ( F ` N ) ` C ) ) e. CC )
85 83 84 subcld 
 |-  ( ( ph /\ ps ) -> ( ( ( G ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( G ` C ) - ( ( F ` N ) ` C ) ) ) e. CC )
86 85 51 52 absdivd 
 |-  ( ( ph /\ ps ) -> ( abs ` ( ( ( ( G ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( G ` C ) - ( ( F ` N ) ` C ) ) ) / ( Y - C ) ) ) = ( ( abs ` ( ( ( G ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( G ` C ) - ( ( F ` N ) ` C ) ) ) ) / ( abs ` ( Y - C ) ) ) )
87 82 86 eqtr3d 
 |-  ( ( ph /\ ps ) -> ( abs ` ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) ) ) = ( ( abs ` ( ( ( G ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( G ` C ) - ( ( F ` N ) ` C ) ) ) ) / ( abs ` ( Y - C ) ) ) )
88 eqid 
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
89 15 1 eleqtrdi 
 |-  ( ( ph /\ ps ) -> N e. ( ZZ>= ` M ) )
90 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
91 89 90 syl 
 |-  ( ( ph /\ ps ) -> N e. ZZ )
92 3 adantr 
 |-  ( ( ph /\ ps ) -> M e. ZZ )
93 fveq2 
 |-  ( z = Y -> ( ( F ` k ) ` z ) = ( ( F ` k ) ` Y ) )
94 93 mpteq2dv 
 |-  ( z = Y -> ( k e. Z |-> ( ( F ` k ) ` z ) ) = ( k e. Z |-> ( ( F ` k ) ` Y ) ) )
95 fveq2 
 |-  ( z = Y -> ( G ` z ) = ( G ` Y ) )
96 94 95 breq12d 
 |-  ( z = Y -> ( ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) <-> ( k e. Z |-> ( ( F ` k ) ` Y ) ) ~~> ( G ` Y ) ) )
97 6 ralrimiva 
 |-  ( ph -> A. z e. X ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) )
98 97 adantr 
 |-  ( ( ph /\ ps ) -> A. z e. X ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) )
99 96 98 18 rspcdva 
 |-  ( ( ph /\ ps ) -> ( k e. Z |-> ( ( F ` k ) ` Y ) ) ~~> ( G ` Y ) )
100 1 fvexi 
 |-  Z e. _V
101 100 mptex 
 |-  ( k e. Z |-> ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) ) e. _V
102 101 a1i 
 |-  ( ( ph /\ ps ) -> ( k e. Z |-> ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) ) e. _V )
103 fveq2 
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
104 103 fveq1d 
 |-  ( k = n -> ( ( F ` k ) ` Y ) = ( ( F ` n ) ` Y ) )
105 eqid 
 |-  ( k e. Z |-> ( ( F ` k ) ` Y ) ) = ( k e. Z |-> ( ( F ` k ) ` Y ) )
106 fvex 
 |-  ( ( F ` n ) ` Y ) e. _V
107 104 105 106 fvmpt 
 |-  ( n e. Z -> ( ( k e. Z |-> ( ( F ` k ) ` Y ) ) ` n ) = ( ( F ` n ) ` Y ) )
108 107 adantl 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( k e. Z |-> ( ( F ` k ) ` Y ) ) ` n ) = ( ( F ` n ) ` Y ) )
109 62 ffvelcdmda 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( F ` n ) e. ( CC ^m X ) )
110 elmapi 
 |-  ( ( F ` n ) e. ( CC ^m X ) -> ( F ` n ) : X --> CC )
111 109 110 syl 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( F ` n ) : X --> CC )
112 18 adantr 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> Y e. X )
113 111 112 ffvelcdmd 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( F ` n ) ` Y ) e. CC )
114 108 113 eqeltrd 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( k e. Z |-> ( ( F ` k ) ` Y ) ) ` n ) e. CC )
115 104 oveq1d 
 |-  ( k = n -> ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) = ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) )
116 eqid 
 |-  ( k e. Z |-> ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) ) = ( k e. Z |-> ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) )
117 ovex 
 |-  ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) e. _V
118 115 116 117 fvmpt 
 |-  ( n e. Z -> ( ( k e. Z |-> ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) ) ` n ) = ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) )
119 118 adantl 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( k e. Z |-> ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) ) ` n ) = ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) )
120 108 oveq1d 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( ( k e. Z |-> ( ( F ` k ) ` Y ) ) ` n ) - ( ( F ` N ) ` Y ) ) = ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) )
121 119 120 eqtr4d 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( k e. Z |-> ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) ) ` n ) = ( ( ( k e. Z |-> ( ( F ` k ) ` Y ) ) ` n ) - ( ( F ` N ) ` Y ) ) )
122 1 92 99 66 102 114 121 climsubc1 
 |-  ( ( ph /\ ps ) -> ( k e. Z |-> ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) ) ~~> ( ( G ` Y ) - ( ( F ` N ) ` Y ) ) )
123 100 mptex 
 |-  ( k e. Z |-> ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) e. _V
124 123 a1i 
 |-  ( ( ph /\ ps ) -> ( k e. Z |-> ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) e. _V )
125 fveq2 
 |-  ( z = C -> ( ( F ` k ) ` z ) = ( ( F ` k ) ` C ) )
126 125 mpteq2dv 
 |-  ( z = C -> ( k e. Z |-> ( ( F ` k ) ` z ) ) = ( k e. Z |-> ( ( F ` k ) ` C ) ) )
127 fveq2 
 |-  ( z = C -> ( G ` z ) = ( G ` C ) )
128 126 127 breq12d 
 |-  ( z = C -> ( ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) <-> ( k e. Z |-> ( ( F ` k ) ` C ) ) ~~> ( G ` C ) ) )
129 128 98 8 rspcdva 
 |-  ( ( ph /\ ps ) -> ( k e. Z |-> ( ( F ` k ) ` C ) ) ~~> ( G ` C ) )
130 100 mptex 
 |-  ( k e. Z |-> ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) e. _V
131 130 a1i 
 |-  ( ( ph /\ ps ) -> ( k e. Z |-> ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) e. _V )
132 103 fveq1d 
 |-  ( k = n -> ( ( F ` k ) ` C ) = ( ( F ` n ) ` C ) )
133 eqid 
 |-  ( k e. Z |-> ( ( F ` k ) ` C ) ) = ( k e. Z |-> ( ( F ` k ) ` C ) )
134 fvex 
 |-  ( ( F ` n ) ` C ) e. _V
135 132 133 134 fvmpt 
 |-  ( n e. Z -> ( ( k e. Z |-> ( ( F ` k ) ` C ) ) ` n ) = ( ( F ` n ) ` C ) )
136 135 adantl 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( k e. Z |-> ( ( F ` k ) ` C ) ) ` n ) = ( ( F ` n ) ` C ) )
137 8 adantr 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> C e. X )
138 111 137 ffvelcdmd 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( F ` n ) ` C ) e. CC )
139 136 138 eqeltrd 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( k e. Z |-> ( ( F ` k ) ` C ) ) ` n ) e. CC )
140 132 oveq1d 
 |-  ( k = n -> ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) = ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) )
141 eqid 
 |-  ( k e. Z |-> ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) = ( k e. Z |-> ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) )
142 ovex 
 |-  ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) e. _V
143 140 141 142 fvmpt 
 |-  ( n e. Z -> ( ( k e. Z |-> ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ` n ) = ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) )
144 143 adantl 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( k e. Z |-> ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ` n ) = ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) )
145 136 oveq1d 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( ( k e. Z |-> ( ( F ` k ) ` C ) ) ` n ) - ( ( F ` N ) ` C ) ) = ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) )
146 144 145 eqtr4d 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( k e. Z |-> ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ` n ) = ( ( ( k e. Z |-> ( ( F ` k ) ` C ) ) ` n ) - ( ( F ` N ) ` C ) ) )
147 1 92 129 67 131 139 146 climsubc1 
 |-  ( ( ph /\ ps ) -> ( k e. Z |-> ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ~~> ( ( G ` C ) - ( ( F ` N ) ` C ) ) )
148 66 adantr 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( F ` N ) ` Y ) e. CC )
149 113 148 subcld 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) e. CC )
150 119 149 eqeltrd 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( k e. Z |-> ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) ) ` n ) e. CC )
151 67 adantr 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( F ` N ) ` C ) e. CC )
152 138 151 subcld 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) e. CC )
153 144 152 eqeltrd 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( k e. Z |-> ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ` n ) e. CC )
154 115 140 oveq12d 
 |-  ( k = n -> ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) = ( ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) ) )
155 eqid 
 |-  ( k e. Z |-> ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) = ( k e. Z |-> ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) )
156 ovex 
 |-  ( ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) ) e. _V
157 154 155 156 fvmpt 
 |-  ( n e. Z -> ( ( k e. Z |-> ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) ` n ) = ( ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) ) )
158 157 adantl 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( k e. Z |-> ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) ` n ) = ( ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) ) )
159 119 144 oveq12d 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( ( k e. Z |-> ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) ) ` n ) - ( ( k e. Z |-> ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ` n ) ) = ( ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) ) )
160 158 159 eqtr4d 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( k e. Z |-> ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) ` n ) = ( ( ( k e. Z |-> ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) ) ` n ) - ( ( k e. Z |-> ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ` n ) ) )
161 1 92 122 124 147 150 153 160 climsub 
 |-  ( ( ph /\ ps ) -> ( k e. Z |-> ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) ~~> ( ( ( G ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( G ` C ) - ( ( F ` N ) ` C ) ) ) )
162 100 mptex 
 |-  ( k e. Z |-> ( abs ` ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) ) e. _V
163 162 a1i 
 |-  ( ( ph /\ ps ) -> ( k e. Z |-> ( abs ` ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) ) e. _V )
164 149 152 subcld 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) ) e. CC )
165 158 164 eqeltrd 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( k e. Z |-> ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) ` n ) e. CC )
166 154 fveq2d 
 |-  ( k = n -> ( abs ` ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) = ( abs ` ( ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) ) ) )
167 eqid 
 |-  ( k e. Z |-> ( abs ` ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) ) = ( k e. Z |-> ( abs ` ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) )
168 fvex 
 |-  ( abs ` ( ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) ) ) e. _V
169 166 167 168 fvmpt 
 |-  ( n e. Z -> ( ( k e. Z |-> ( abs ` ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) ) ` n ) = ( abs ` ( ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) ) ) )
170 169 adantl 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( k e. Z |-> ( abs ` ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) ) ` n ) = ( abs ` ( ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) ) ) )
171 158 fveq2d 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( abs ` ( ( k e. Z |-> ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) ` n ) ) = ( abs ` ( ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) ) ) )
172 170 171 eqtr4d 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( ( k e. Z |-> ( abs ` ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) ) ` n ) = ( abs ` ( ( k e. Z |-> ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) ` n ) ) )
173 1 161 163 92 165 172 climabs 
 |-  ( ( ph /\ ps ) -> ( k e. Z |-> ( abs ` ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) ) ~~> ( abs ` ( ( ( G ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( G ` C ) - ( ( F ` N ) ` C ) ) ) ) )
174 51 abscld 
 |-  ( ( ph /\ ps ) -> ( abs ` ( Y - C ) ) e. RR )
175 77 174 remulcld 
 |-  ( ( ph /\ ps ) -> ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) e. RR )
176 175 recnd 
 |-  ( ( ph /\ ps ) -> ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) e. CC )
177 1 eqimss2i 
 |-  ( ZZ>= ` M ) C_ Z
178 177 100 climconst2 
 |-  ( ( ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) e. CC /\ M e. ZZ ) -> ( Z X. { ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) } ) ~~> ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) )
179 176 92 178 syl2anc 
 |-  ( ( ph /\ ps ) -> ( Z X. { ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) } ) ~~> ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) )
180 1 uztrn2 
 |-  ( ( N e. Z /\ n e. ( ZZ>= ` N ) ) -> n e. Z )
181 15 180 sylan 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> n e. Z )
182 181 169 syl 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. Z |-> ( abs ` ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) ) ` n ) = ( abs ` ( ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) ) ) )
183 164 abscld 
 |-  ( ( ( ph /\ ps ) /\ n e. Z ) -> ( abs ` ( ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) ) ) e. RR )
184 181 183 syldan 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( abs ` ( ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) ) ) e. RR )
185 182 184 eqeltrd 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. Z |-> ( abs ` ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) ) ` n ) e. RR )
186 ovex 
 |-  ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) e. _V
187 186 fvconst2 
 |-  ( n e. Z -> ( ( Z X. { ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) } ) ` n ) = ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) )
188 181 187 syl 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( ( Z X. { ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) } ) ` n ) = ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) )
189 175 adantr 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) e. RR )
190 188 189 eqeltrd 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( ( Z X. { ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) } ) ` n ) e. RR )
191 181 111 syldan 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( F ` n ) : X --> CC )
192 191 ffnd 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( F ` n ) Fn X )
193 65 adantr 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( F ` N ) : X --> CC )
194 193 ffnd 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( F ` N ) Fn X )
195 ulmscl 
 |-  ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~>u ` X ) H -> X e. _V )
196 7 195 syl 
 |-  ( ph -> X e. _V )
197 196 ad2antrr 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> X e. _V )
198 18 adantr 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> Y e. X )
199 fnfvof 
 |-  ( ( ( ( F ` n ) Fn X /\ ( F ` N ) Fn X ) /\ ( X e. _V /\ Y e. X ) ) -> ( ( ( F ` n ) oF - ( F ` N ) ) ` Y ) = ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) )
200 192 194 197 198 199 syl22anc 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( ( ( F ` n ) oF - ( F ` N ) ) ` Y ) = ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) )
201 8 adantr 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> C e. X )
202 fnfvof 
 |-  ( ( ( ( F ` n ) Fn X /\ ( F ` N ) Fn X ) /\ ( X e. _V /\ C e. X ) ) -> ( ( ( F ` n ) oF - ( F ` N ) ) ` C ) = ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) )
203 192 194 197 201 202 syl22anc 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( ( ( F ` n ) oF - ( F ` N ) ) ` C ) = ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) )
204 200 203 oveq12d 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( ( ( ( F ` n ) oF - ( F ` N ) ) ` Y ) - ( ( ( F ` n ) oF - ( F ` N ) ) ` C ) ) = ( ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) ) )
205 204 fveq2d 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( abs ` ( ( ( ( F ` n ) oF - ( F ` N ) ) ` Y ) - ( ( ( F ` n ) oF - ( F ` N ) ) ` C ) ) ) = ( abs ` ( ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) ) ) )
206 44 18 sseldd 
 |-  ( ( ph /\ ps ) -> Y e. S )
207 44 8 sseldd 
 |-  ( ( ph /\ ps ) -> C e. S )
208 206 207 ovresd 
 |-  ( ( ph /\ ps ) -> ( Y ( ( abs o. - ) |` ( S X. S ) ) C ) = ( Y ( abs o. - ) C ) )
209 eqid 
 |-  ( abs o. - ) = ( abs o. - )
210 209 cnmetdval 
 |-  ( ( Y e. CC /\ C e. CC ) -> ( Y ( abs o. - ) C ) = ( abs ` ( Y - C ) ) )
211 49 50 210 syl2anc 
 |-  ( ( ph /\ ps ) -> ( Y ( abs o. - ) C ) = ( abs ` ( Y - C ) ) )
212 208 211 eqtrd 
 |-  ( ( ph /\ ps ) -> ( Y ( ( abs o. - ) |` ( S X. S ) ) C ) = ( abs ` ( Y - C ) ) )
213 212 14 eqbrtrd 
 |-  ( ( ph /\ ps ) -> ( Y ( ( abs o. - ) |` ( S X. S ) ) C ) < U )
214 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
215 xmetres2 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ S C_ CC ) -> ( ( abs o. - ) |` ( S X. S ) ) e. ( *Met ` S ) )
216 214 47 215 sylancr 
 |-  ( ( ph /\ ps ) -> ( ( abs o. - ) |` ( S X. S ) ) e. ( *Met ` S ) )
217 10 rpxrd 
 |-  ( ( ph /\ ps ) -> U e. RR* )
218 elbl3 
 |-  ( ( ( ( ( abs o. - ) |` ( S X. S ) ) e. ( *Met ` S ) /\ U e. RR* ) /\ ( C e. S /\ Y e. S ) ) -> ( Y e. ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) <-> ( Y ( ( abs o. - ) |` ( S X. S ) ) C ) < U ) )
219 216 217 207 206 218 syl22anc 
 |-  ( ( ph /\ ps ) -> ( Y e. ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) <-> ( Y ( ( abs o. - ) |` ( S X. S ) ) C ) < U ) )
220 213 219 mpbird 
 |-  ( ( ph /\ ps ) -> Y e. ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) )
221 220 adantr 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> Y e. ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) )
222 blcntr 
 |-  ( ( ( ( abs o. - ) |` ( S X. S ) ) e. ( *Met ` S ) /\ C e. S /\ U e. RR+ ) -> C e. ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) )
223 216 207 10 222 syl3anc 
 |-  ( ( ph /\ ps ) -> C e. ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) )
224 223 adantr 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> C e. ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) )
225 221 224 jca 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( Y e. ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) /\ C e. ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) ) )
226 2 ad2antrr 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> S e. { RR , CC } )
227 eqid 
 |-  ( ( abs o. - ) |` ( S X. S ) ) = ( ( abs o. - ) |` ( S X. S ) )
228 44 adantr 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> X C_ S )
229 fvexd 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( ( F ` n ) ` y ) e. _V )
230 fvexd 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( ( F ` N ) ` y ) e. _V )
231 191 feqmptd 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( F ` n ) = ( y e. X |-> ( ( F ` n ) ` y ) ) )
232 193 feqmptd 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( F ` N ) = ( y e. X |-> ( ( F ` N ) ` y ) ) )
233 197 229 230 231 232 offval2 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( ( F ` n ) oF - ( F ` N ) ) = ( y e. X |-> ( ( ( F ` n ) ` y ) - ( ( F ` N ) ` y ) ) ) )
234 191 ffvelcdmda 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( ( F ` n ) ` y ) e. CC )
235 193 ffvelcdmda 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( ( F ` N ) ` y ) e. CC )
236 234 235 subcld 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( ( ( F ` n ) ` y ) - ( ( F ` N ) ` y ) ) e. CC )
237 233 236 fmpt3d 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( ( F ` n ) oF - ( F ` N ) ) : X --> CC )
238 207 adantr 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> C e. S )
239 217 adantr 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> U e. RR* )
240 eqid 
 |-  ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) = ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U )
241 13 adantr 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) C_ X )
242 233 oveq2d 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( S _D ( ( F ` n ) oF - ( F ` N ) ) ) = ( S _D ( y e. X |-> ( ( ( F ` n ) ` y ) - ( ( F ` N ) ` y ) ) ) ) )
243 fvexd 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( ( S _D ( F ` n ) ) ` y ) e. _V )
244 231 oveq2d 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( S _D ( F ` n ) ) = ( S _D ( y e. X |-> ( ( F ` n ) ` y ) ) ) )
245 103 oveq2d 
 |-  ( k = n -> ( S _D ( F ` k ) ) = ( S _D ( F ` n ) ) )
246 ovex 
 |-  ( S _D ( F ` n ) ) e. _V
247 245 27 246 fvmpt 
 |-  ( n e. Z -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) = ( S _D ( F ` n ) ) )
248 181 247 syl 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) = ( S _D ( F ` n ) ) )
249 36 ad2antrr 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( k e. Z |-> ( S _D ( F ` k ) ) ) : Z --> ( CC ^m X ) )
250 249 181 ffvelcdmd 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) e. ( CC ^m X ) )
251 248 250 eqeltrrd 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( S _D ( F ` n ) ) e. ( CC ^m X ) )
252 elmapi 
 |-  ( ( S _D ( F ` n ) ) e. ( CC ^m X ) -> ( S _D ( F ` n ) ) : X --> CC )
253 251 252 syl 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( S _D ( F ` n ) ) : X --> CC )
254 253 feqmptd 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( S _D ( F ` n ) ) = ( y e. X |-> ( ( S _D ( F ` n ) ) ` y ) ) )
255 244 254 eqtr3d 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( S _D ( y e. X |-> ( ( F ` n ) ` y ) ) ) = ( y e. X |-> ( ( S _D ( F ` n ) ) ` y ) ) )
256 fvexd 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( ( S _D ( F ` N ) ) ` y ) e. _V )
257 232 oveq2d 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( S _D ( F ` N ) ) = ( S _D ( y e. X |-> ( ( F ` N ) ` y ) ) ) )
258 41 adantr 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( S _D ( F ` N ) ) : X --> CC )
259 258 feqmptd 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( S _D ( F ` N ) ) = ( y e. X |-> ( ( S _D ( F ` N ) ) ` y ) ) )
260 257 259 eqtr3d 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( S _D ( y e. X |-> ( ( F ` N ) ` y ) ) ) = ( y e. X |-> ( ( S _D ( F ` N ) ) ` y ) ) )
261 226 234 243 255 235 256 260 dvmptsub 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( S _D ( y e. X |-> ( ( ( F ` n ) ` y ) - ( ( F ` N ) ` y ) ) ) ) = ( y e. X |-> ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) ) )
262 242 261 eqtrd 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( S _D ( ( F ` n ) oF - ( F ` N ) ) ) = ( y e. X |-> ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) ) )
263 262 dmeqd 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> dom ( S _D ( ( F ` n ) oF - ( F ` N ) ) ) = dom ( y e. X |-> ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) ) )
264 ovex 
 |-  ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) e. _V
265 eqid 
 |-  ( y e. X |-> ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) ) = ( y e. X |-> ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) )
266 264 265 dmmpti 
 |-  dom ( y e. X |-> ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) ) = X
267 263 266 eqtrdi 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> dom ( S _D ( ( F ` n ) oF - ( F ` N ) ) ) = X )
268 241 267 sseqtrrd 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) C_ dom ( S _D ( ( F ` n ) oF - ( F ` N ) ) ) )
269 77 adantr 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( ( R / 2 ) / 2 ) e. RR )
270 241 sselda 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) ) -> y e. X )
271 262 fveq1d 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( ( S _D ( ( F ` n ) oF - ( F ` N ) ) ) ` y ) = ( ( y e. X |-> ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) ) ` y ) )
272 265 fvmpt2 
 |-  ( ( y e. X /\ ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) e. _V ) -> ( ( y e. X |-> ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) ) ` y ) = ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) )
273 264 272 mpan2 
 |-  ( y e. X -> ( ( y e. X |-> ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) ) ` y ) = ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) )
274 271 273 sylan9eq 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( ( S _D ( ( F ` n ) oF - ( F ` N ) ) ) ` y ) = ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) )
275 274 fveq2d 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( abs ` ( ( S _D ( ( F ` n ) oF - ( F ` N ) ) ) ` y ) ) = ( abs ` ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) ) )
276 264 a1i 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) e. _V )
277 226 236 276 261 dvmptcl 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) e. CC )
278 277 abscld 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( abs ` ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) ) e. RR )
279 77 ad2antrr 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( ( R / 2 ) / 2 ) e. RR )
280 253 ffvelcdmda 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( ( S _D ( F ` n ) ) ` y ) e. CC )
281 258 ffvelcdmda 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( ( S _D ( F ` N ) ) ` y ) e. CC )
282 280 281 abssubd 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( abs ` ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) ) = ( abs ` ( ( ( S _D ( F ` N ) ) ` y ) - ( ( S _D ( F ` n ) ) ` y ) ) ) )
283 fveq2 
 |-  ( m = n -> ( F ` m ) = ( F ` n ) )
284 283 oveq2d 
 |-  ( m = n -> ( S _D ( F ` m ) ) = ( S _D ( F ` n ) ) )
285 284 fveq1d 
 |-  ( m = n -> ( ( S _D ( F ` m ) ) ` x ) = ( ( S _D ( F ` n ) ) ` x ) )
286 285 oveq2d 
 |-  ( m = n -> ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) = ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` n ) ) ` x ) ) )
287 286 fveq2d 
 |-  ( m = n -> ( abs ` ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) = ( abs ` ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` n ) ) ` x ) ) ) )
288 287 breq1d 
 |-  ( m = n -> ( ( abs ` ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( R / 2 ) / 2 ) <-> ( abs ` ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` n ) ) ` x ) ) ) < ( ( R / 2 ) / 2 ) ) )
289 288 ralbidv 
 |-  ( m = n -> ( A. x e. X ( abs ` ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( R / 2 ) / 2 ) <-> A. x e. X ( abs ` ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` n ) ) ` x ) ) ) < ( ( R / 2 ) / 2 ) ) )
290 289 rspccva 
 |-  ( ( A. m e. ( ZZ>= ` N ) A. x e. X ( abs ` ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( R / 2 ) / 2 ) /\ n e. ( ZZ>= ` N ) ) -> A. x e. X ( abs ` ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` n ) ) ` x ) ) ) < ( ( R / 2 ) / 2 ) )
291 16 290 sylan 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> A. x e. X ( abs ` ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` n ) ) ` x ) ) ) < ( ( R / 2 ) / 2 ) )
292 fveq2 
 |-  ( x = y -> ( ( S _D ( F ` N ) ) ` x ) = ( ( S _D ( F ` N ) ) ` y ) )
293 fveq2 
 |-  ( x = y -> ( ( S _D ( F ` n ) ) ` x ) = ( ( S _D ( F ` n ) ) ` y ) )
294 292 293 oveq12d 
 |-  ( x = y -> ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` n ) ) ` x ) ) = ( ( ( S _D ( F ` N ) ) ` y ) - ( ( S _D ( F ` n ) ) ` y ) ) )
295 294 fveq2d 
 |-  ( x = y -> ( abs ` ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` n ) ) ` x ) ) ) = ( abs ` ( ( ( S _D ( F ` N ) ) ` y ) - ( ( S _D ( F ` n ) ) ` y ) ) ) )
296 295 breq1d 
 |-  ( x = y -> ( ( abs ` ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` n ) ) ` x ) ) ) < ( ( R / 2 ) / 2 ) <-> ( abs ` ( ( ( S _D ( F ` N ) ) ` y ) - ( ( S _D ( F ` n ) ) ` y ) ) ) < ( ( R / 2 ) / 2 ) ) )
297 296 rspccva 
 |-  ( ( A. x e. X ( abs ` ( ( ( S _D ( F ` N ) ) ` x ) - ( ( S _D ( F ` n ) ) ` x ) ) ) < ( ( R / 2 ) / 2 ) /\ y e. X ) -> ( abs ` ( ( ( S _D ( F ` N ) ) ` y ) - ( ( S _D ( F ` n ) ) ` y ) ) ) < ( ( R / 2 ) / 2 ) )
298 291 297 sylan 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( abs ` ( ( ( S _D ( F ` N ) ) ` y ) - ( ( S _D ( F ` n ) ) ` y ) ) ) < ( ( R / 2 ) / 2 ) )
299 282 298 eqbrtrd 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( abs ` ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) ) < ( ( R / 2 ) / 2 ) )
300 278 279 299 ltled 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( abs ` ( ( ( S _D ( F ` n ) ) ` y ) - ( ( S _D ( F ` N ) ) ` y ) ) ) <_ ( ( R / 2 ) / 2 ) )
301 275 300 eqbrtrd 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. X ) -> ( abs ` ( ( S _D ( ( F ` n ) oF - ( F ` N ) ) ) ` y ) ) <_ ( ( R / 2 ) / 2 ) )
302 270 301 syldan 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ y e. ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) ) -> ( abs ` ( ( S _D ( ( F ` n ) oF - ( F ` N ) ) ) ` y ) ) <_ ( ( R / 2 ) / 2 ) )
303 226 227 228 237 238 239 240 268 269 302 dvlip2 
 |-  ( ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) /\ ( Y e. ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) /\ C e. ( C ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) U ) ) ) -> ( abs ` ( ( ( ( F ` n ) oF - ( F ` N ) ) ` Y ) - ( ( ( F ` n ) oF - ( F ` N ) ) ` C ) ) ) <_ ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) )
304 225 303 mpdan 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( abs ` ( ( ( ( F ` n ) oF - ( F ` N ) ) ` Y ) - ( ( ( F ` n ) oF - ( F ` N ) ) ` C ) ) ) <_ ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) )
305 205 304 eqbrtrrd 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( abs ` ( ( ( ( F ` n ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` n ) ` C ) - ( ( F ` N ) ` C ) ) ) ) <_ ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) )
306 305 182 188 3brtr4d 
 |-  ( ( ( ph /\ ps ) /\ n e. ( ZZ>= ` N ) ) -> ( ( k e. Z |-> ( abs ` ( ( ( ( F ` k ) ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( ( F ` k ) ` C ) - ( ( F ` N ) ` C ) ) ) ) ) ` n ) <_ ( ( Z X. { ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) } ) ` n ) )
307 88 91 173 179 185 190 306 climle 
 |-  ( ( ph /\ ps ) -> ( abs ` ( ( ( G ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( G ` C ) - ( ( F ` N ) ` C ) ) ) ) <_ ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) )
308 85 abscld 
 |-  ( ( ph /\ ps ) -> ( abs ` ( ( ( G ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( G ` C ) - ( ( F ` N ) ` C ) ) ) ) e. RR )
309 51 52 absrpcld 
 |-  ( ( ph /\ ps ) -> ( abs ` ( Y - C ) ) e. RR+ )
310 308 77 309 ledivmul2d 
 |-  ( ( ph /\ ps ) -> ( ( ( abs ` ( ( ( G ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( G ` C ) - ( ( F ` N ) ` C ) ) ) ) / ( abs ` ( Y - C ) ) ) <_ ( ( R / 2 ) / 2 ) <-> ( abs ` ( ( ( G ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( G ` C ) - ( ( F ` N ) ` C ) ) ) ) <_ ( ( ( R / 2 ) / 2 ) x. ( abs ` ( Y - C ) ) ) ) )
311 307 310 mpbird 
 |-  ( ( ph /\ ps ) -> ( ( abs ` ( ( ( G ` Y ) - ( ( F ` N ) ` Y ) ) - ( ( G ` C ) - ( ( F ` N ) ` C ) ) ) ) / ( abs ` ( Y - C ) ) ) <_ ( ( R / 2 ) / 2 ) )
312 87 311 eqbrtrd 
 |-  ( ( ph /\ ps ) -> ( abs ` ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) ) ) <_ ( ( R / 2 ) / 2 ) )
313 10 rpred 
 |-  ( ( ph /\ ps ) -> U e. RR )
314 11 rpred 
 |-  ( ( ph /\ ps ) -> W e. RR )
315 174 313 314 14 12 lttrd 
 |-  ( ( ph /\ ps ) -> ( abs ` ( Y - C ) ) < W )
316 315 20 mpd 
 |-  ( ( ph /\ ps ) -> ( abs ` ( ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) - ( ( S _D ( F ` N ) ) ` C ) ) ) < ( ( R / 2 ) / 2 ) )
317 71 73 77 77 312 316 leltaddd 
 |-  ( ( ph /\ ps ) -> ( ( abs ` ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) ) ) + ( abs ` ( ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) - ( ( S _D ( F ` N ) ) ` C ) ) ) ) < ( ( ( R / 2 ) / 2 ) + ( ( R / 2 ) / 2 ) ) )
318 75 recnd 
 |-  ( ( ph /\ ps ) -> ( R / 2 ) e. CC )
319 318 2halvesd 
 |-  ( ( ph /\ ps ) -> ( ( ( R / 2 ) / 2 ) + ( ( R / 2 ) / 2 ) ) = ( R / 2 ) )
320 317 319 breqtrd 
 |-  ( ( ph /\ ps ) -> ( ( abs ` ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) ) ) + ( abs ` ( ( ( ( ( F ` N ) ` Y ) - ( ( F ` N ) ` C ) ) / ( Y - C ) ) - ( ( S _D ( F ` N ) ) ` C ) ) ) ) < ( R / 2 ) )
321 61 74 75 76 320 lelttrd 
 |-  ( ( ph /\ ps ) -> ( abs ` ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( ( S _D ( F ` N ) ) ` C ) ) ) < ( R / 2 ) )
322 53 57 58 59 321 17 abs3lemd 
 |-  ( ( ph /\ ps ) -> ( abs ` ( ( ( ( G ` Y ) - ( G ` C ) ) / ( Y - C ) ) - ( H ` C ) ) ) < R )