Theorem ulmdvlem3 22559

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

Hypotheses

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

Assertion

Ref	Expression
ulmdvlem3	|- ( ( ph /\ z e. X ) -> z ( S _D G ) ( H ` z ) )

Distinct variable groups:   z, k, F   z, G   z, H   k, M   ph, k, z   S, k, z   k, X, z   k, Z, z

Allowed substitution hints:   G( k)   H( k)   M( z)

Proof of Theorem ulmdvlem3

Dummy variables j m n s u v w x y r are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ulmdv.m	. . . . . 6 |- ( ph -> M e. ZZ )
2		uzid 11096	. . . . . 6 |- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
3	1, 2	syl 16	. . . . 5 |- ( ph -> M e. ( ZZ>= ` M ) )
4		ulmdv.z	. . . . 5 |- Z = ( ZZ>= ` M )
5	3, 4	syl6eleqr 2566	. . . 4 |- ( ph -> M e. Z )
6		ulmdv.s	. . . . . . 7 |- ( ph -> S e. { RR , CC } )
7		ulmdv.f	. . . . . . 7 |- ( ph -> F : Z --> ( CC ^m X ) )
8		ulmdv.g	. . . . . . 7 |- ( ph -> G : X --> CC )
9		ulmdv.l	. . . . . . 7 |- ( ( ph /\ z e. X ) -> ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) )
10		ulmdv.u	. . . . . . 7 |- ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~> u ` X ) H )
11	4, 6, 1, 7, 8, 9, 10	ulmdvlem2 22558	. . . . . 6 |- ( ( ph /\ k e. Z ) -> dom ( S _D ( F ` k ) ) = X )
12		recnprss 22071	. . . . . . . . 9 |- ( S e. { RR , CC } -> S C_ CC )
13	6, 12	syl 16	. . . . . . . 8 |- ( ph -> S C_ CC )
14	13	adantr 465	. . . . . . 7 |- ( ( ph /\ k e. Z ) -> S C_ CC )
15	7	ffvelrnda 6021	. . . . . . . 8 |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. ( CC ^m X ) )
16		elmapi 7440	. . . . . . . 8 |- ( ( F ` k ) e. ( CC ^m X ) -> ( F ` k ) : X --> CC )
17	15, 16	syl 16	. . . . . . 7 |- ( ( ph /\ k e. Z ) -> ( F ` k ) : X --> CC )
18		dvbsss 22069	. . . . . . . 8 |- dom ( S _D ( F ` k ) ) C_ S
19	11, 18	syl6eqssr 3555	. . . . . . 7 |- ( ( ph /\ k e. Z ) -> X C_ S )
20		eqid 2467	. . . . . . 7 |- ( ( TopOpen ` ℂfld ) ↾t S ) = ( ( TopOpen ` ℂfld ) ↾t S )
21		eqid 2467	. . . . . . 7 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
22	14, 17, 19, 20, 21	dvbssntr 22067	. . . . . 6 |- ( ( ph /\ k e. Z ) -> dom ( S _D ( F ` k ) ) C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) )
23	11, 22	eqsstr3d 3539	. . . . 5 |- ( ( ph /\ k e. Z ) -> X C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) )
24	23	ralrimiva 2878	. . . 4 |- ( ph -> A. k e. Z X C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) )
25		biidd 237	. . . . 5 |- ( k = M -> ( X C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) <-> X C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) ) )
26	25	rspcv 3210	. . . 4 |- ( M e. Z -> ( A. k e. Z X C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) -> X C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) ) )
27	5, 24, 26	sylc 60	. . 3 |- ( ph -> X C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) )
28	27	sselda 3504	. 2 |- ( ( ph /\ z e. X ) -> z e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) )
29		ulmcl 22538	. . . . 5 |- ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~> u ` X ) H -> H : X --> CC )
30	10, 29	syl 16	. . . 4 |- ( ph -> H : X --> CC )
31	30	ffvelrnda 6021	. . 3 |- ( ( ph /\ z e. X ) -> ( H ` z ) e. CC )
32		rphalfcl 11244	. . . . . . . 8 |- ( r e. RR+ -> ( r / 2 ) e. RR+ )
33	32	adantl 466	. . . . . . 7 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( r / 2 ) e. RR+ )
34		rphalfcl 11244	. . . . . . 7 |- ( ( r / 2 ) e. RR+ -> ( ( r / 2 ) / 2 ) e. RR+ )
35	33, 34	syl 16	. . . . . 6 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( ( r / 2 ) / 2 ) e. RR+ )
36		ulmrel 22535	. . . . . . . . . 10 |- Rel ( ~~> u ` X )
37		releldm 5235	. . . . . . . . . 10 |- ( ( Rel ( ~~> u ` X ) /\ ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~> u ` X ) H ) -> ( k e. Z |-> ( S _D ( F ` k ) ) ) e. dom ( ~~> u ` X ) )
38	36, 10, 37	sylancr 663	. . . . . . . . 9 |- ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) e. dom ( ~~> u ` X ) )
39		ulmscl 22536	. . . . . . . . . . 11 |- ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~> u ` X ) H -> X e. _V )
40	10, 39	syl 16	. . . . . . . . . 10 |- ( ph -> X e. _V )
41		ovex 6309	. . . . . . . . . . . . 13 |- ( S _D ( F ` k ) ) e. _V
42	41	rgenw 2825	. . . . . . . . . . . 12 |- A. k e. Z ( S _D ( F ` k ) ) e. _V
43		eqid 2467	. . . . . . . . . . . . 13 |- ( k e. Z |-> ( S _D ( F ` k ) ) ) = ( k e. Z |-> ( S _D ( F ` k ) ) )
44	43	fnmpt 5707	. . . . . . . . . . . 12 |- ( A. k e. Z ( S _D ( F ` k ) ) e. _V -> ( k e. Z |-> ( S _D ( F ` k ) ) ) Fn Z )
45	42, 44	mp1i 12	. . . . . . . . . . 11 |- ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) Fn Z )
46		ulmf2 22541	. . . . . . . . . . 11 |- ( ( ( 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 ) )
47	45, 10, 46	syl2anc 661	. . . . . . . . . 10 |- ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) : Z --> ( CC ^m X ) )
48	4, 1, 40, 47	ulmcau2 22553	. . . . . . . . 9 |- ( 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 ) )
49	38, 48	mpbid 210	. . . . . . . 8 |- ( 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 )
50	4	uztrn2 11099	. . . . . . . . . . . . . . . . . 18 |- ( ( j e. Z /\ n e. ( ZZ>= ` j ) ) -> n e. Z )
51	50	ad2ant2lr 747	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> n e. Z )
52		fveq2 5866	. . . . . . . . . . . . . . . . . . 19 |- ( k = n -> ( F ` k ) = ( F ` n ) )
53	52	oveq2d 6300	. . . . . . . . . . . . . . . . . 18 |- ( k = n -> ( S _D ( F ` k ) ) = ( S _D ( F ` n ) ) )
54		ovex 6309	. . . . . . . . . . . . . . . . . 18 |- ( S _D ( F ` n ) ) e. _V
55	53, 43, 54	fvmpt 5950	. . . . . . . . . . . . . . . . 17 |- ( n e. Z -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) = ( S _D ( F ` n ) ) )
56	51, 55	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) = ( S _D ( F ` n ) ) )
57	56	fveq1d 5868	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) )
58		simprr 756	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> m e. ( ZZ>= ` n ) )
59	4	uztrn2 11099	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. Z /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
60	51, 58, 59	syl2anc 661	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> m e. Z )
61		fveq2 5866	. . . . . . . . . . . . . . . . . . 19 |- ( k = m -> ( F ` k ) = ( F ` m ) )
62	61	oveq2d 6300	. . . . . . . . . . . . . . . . . 18 |- ( k = m -> ( S _D ( F ` k ) ) = ( S _D ( F ` m ) ) )
63		ovex 6309	. . . . . . . . . . . . . . . . . 18 |- ( S _D ( F ` m ) ) e. _V
64	62, 43, 63	fvmpt 5950	. . . . . . . . . . . . . . . . 17 |- ( m e. Z -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` m ) = ( S _D ( F ` m ) ) )
65	60, 64	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` m ) = ( S _D ( F ` m ) ) )
66	65	fveq1d 5868	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) )
67	57, 66	oveq12d 6302	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) )
68	67	fveq2d 5870	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) ) )
69	68	breq1d 4457	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
70	69	ralbidv 2903	. . . . . . . . . . 11 |- ( ( ( 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 ) )
71	70	2ralbidva 2906	. . . . . . . . . 10 |- ( ( 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 ) )
72	71	rexbidva 2970	. . . . . . . . 9 |- ( 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 ) )
73	72	ralbidv 2903	. . . . . . . 8 |- ( 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 ) )
74	49, 73	mpbid 210	. . . . . . 7 |- ( 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 )
75	74	ad2antrr 725	. . . . . 6 |- ( ( ( 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 )
76		breq2 4451	. . . . . . . . 9 |- ( 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 ) ) )
77	76	2ralbidv 2908	. . . . . . . 8 |- ( 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 ) ) )
78	77	rexralbidv 2981	. . . . . . 7 |- ( 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 ) ) )
79	78	rspcv 3210	. . . . . 6 |- ( ( ( r / 2 ) / 2 ) 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 -> 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 ) ) )
80	35, 75, 79	sylc 60	. . . . 5 |- ( ( ( 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 ) )
81	1	ad2antrr 725	. . . . . 6 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> M e. ZZ )
82	53	fveq1d 5868	. . . . . . . 8 |- ( k = n -> ( ( S _D ( F ` k ) ) ` z ) = ( ( S _D ( F ` n ) ) ` z ) )
83		eqid 2467	. . . . . . . 8 |- ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) ) = ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) )
84		fvex 5876	. . . . . . . 8 |- ( ( S _D ( F ` n ) ) ` z ) e. _V
85	82, 83, 84	fvmpt 5950	. . . . . . 7 |- ( n e. Z -> ( ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) ) ` n ) = ( ( S _D ( F ` n ) ) ` z ) )
86	85	adantl 466	. . . . . 6 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) ) ` n ) = ( ( S _D ( F ` n ) ) ` z ) )
87	47	ad2antrr 725	. . . . . . 7 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( k e. Z |-> ( S _D ( F ` k ) ) ) : Z --> ( CC ^m X ) )
88		simplr 754	. . . . . . 7 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> z e. X )
89		fvex 5876	. . . . . . . . . 10 |- ( ZZ>= ` M ) e. _V
90	4, 89	eqeltri 2551	. . . . . . . . 9 |- Z e. _V
91	90	mptex 6131	. . . . . . . 8 |- ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) ) e. _V
92	91	a1i 11	. . . . . . 7 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) ) e. _V )
93	55	adantl 466	. . . . . . . . 9 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) = ( S _D ( F ` n ) ) )
94	93	fveq1d 5868	. . . . . . . 8 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) ` z ) = ( ( S _D ( F ` n ) ) ` z ) )
95	94, 86	eqtr4d 2511	. . . . . . 7 |- ( ( ( ( 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 ) )
96	10	ad2antrr 725	. . . . . . 7 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~> u ` X ) H )
97	4, 81, 87, 88, 92, 95, 96	ulmclm 22544	. . . . . 6 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) ) ~~> ( H ` z ) )
98	4, 81, 33, 86, 97	climi2 13297	. . . . 5 |- ( ( ( 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 ) )
99	4	rexanuz2 13145	. . . . . . 7 |- ( 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 ) ) )
100	4	r19.2uz 13147	. . . . . . 7 |- ( 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 ) ) )
101	99, 100	sylbir 213	. . . . . 6 |- ( ( 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 ) ) )
102	35	adantr 465	. . . . . . . . . 10 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( ( r / 2 ) / 2 ) e. RR+ )
103		simpllr 758	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> z e. X )
104	87	ffvelrnda 6021	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) e. ( CC ^m X ) )
105	93, 104	eqeltrrd 2556	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( S _D ( F ` n ) ) e. ( CC ^m X ) )
106		elmapi 7440	. . . . . . . . . . . . . . . . 17 |- ( ( S _D ( F ` n ) ) e. ( CC ^m X ) -> ( S _D ( F ` n ) ) : X --> CC )
107		fdm 5735	. . . . . . . . . . . . . . . . 17 |- ( ( S _D ( F ` n ) ) : X --> CC -> dom ( S _D ( F ` n ) ) = X )
108	105, 106, 107	3syl 20	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> dom ( S _D ( F ` n ) ) = X )
109	103, 108	eleqtrrd 2558	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> z e. dom ( S _D ( F ` n ) ) )
110	6	ad3antrrr 729	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> S e. { RR , CC } )
111		dvfg 22073	. . . . . . . . . . . . . . . 16 |- ( S e. { RR , CC } -> ( S _D ( F ` n ) ) : dom ( S _D ( F ` n ) ) --> CC )
112		ffun 5733	. . . . . . . . . . . . . . . 16 |- ( ( S _D ( F ` n ) ) : dom ( S _D ( F ` n ) ) --> CC -> Fun ( S _D ( F ` n ) ) )
113		funfvbrb 5994	. . . . . . . . . . . . . . . 16 |- ( Fun ( S _D ( F ` n ) ) -> ( z e. dom ( S _D ( F ` n ) ) <-> z ( S _D ( F ` n ) ) ( ( S _D ( F ` n ) ) ` z ) ) )
114	110, 111, 112, 113	4syl 21	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) )
115	109, 114	mpbid 210	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> z ( S _D ( F ` n ) ) ( ( S _D ( F ` n ) ) ` z ) )
116		eqid 2467	. . . . . . . . . . . . . . 15 |- ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) = ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) )
117	110, 12	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> S C_ CC )
118	7	ad2antrr 725	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> F : Z --> ( CC ^m X ) )
119	118	ffvelrnda 6021	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( F ` n ) e. ( CC ^m X ) )
120		elmapi 7440	. . . . . . . . . . . . . . . 16 |- ( ( F ` n ) e. ( CC ^m X ) -> ( F ` n ) : X --> CC )
121	119, 120	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( F ` n ) : X --> CC )
122	19	ralrimiva 2878	. . . . . . . . . . . . . . . . 17 |- ( ph -> A. k e. Z X C_ S )
123		biidd 237	. . . . . . . . . . . . . . . . . 18 |- ( k = M -> ( X C_ S <-> X C_ S ) )
124	123	rspcv 3210	. . . . . . . . . . . . . . . . 17 |- ( M e. Z -> ( A. k e. Z X C_ S -> X C_ S ) )
125	5, 122, 124	sylc 60	. . . . . . . . . . . . . . . 16 |- ( ph -> X C_ S )
126	125	ad3antrrr 729	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> X C_ S )
127	20, 21, 116, 117, 121, 126	eldv 22065	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( z ( S _D ( F ` n ) ) ( ( S _D ( F ` n ) ) ` z ) <-> ( z e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) /\ ( ( S _D ( F ` n ) ) ` z ) e. ( ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) lim CC z ) ) ) )
128	115, 127	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( z e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) /\ ( ( S _D ( F ` n ) ) ` z ) e. ( ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) lim CC z ) ) )
129	128	simprd 463	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) ) lim CC z ) )
130	125	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. X ) -> X C_ S )
131	13	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. X ) -> S C_ CC )
132	130, 131	sstrd 3514	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ z e. X ) -> X C_ CC )
133	132	ad2antrr 725	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> X C_ CC )
134	121, 133, 103	dvlem 22063	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) /\ y e. ( X \ { z } ) ) -> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) e. CC )
135	134, 116	fmptd 6045	. . . . . . . . . . . . 13 |- ( ( ( ( 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 )
136	133	ssdifssd 3642	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( X \ { z } ) C_ CC )
137	133, 103	sseldd 3505	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> z e. CC )
138	135, 136, 137	ellimc3 22046	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) ) lim CC 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 ) ) ) )
139	129, 138	mpbid 210	. . . . . . . . . . 11 |- ( ( ( ( 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 ) ) )
140	139	simprd 463	. . . . . . . . . 10 |- ( ( ( ( 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 ) )
141		fveq2 5866	. . . . . . . . . . . . . . . . . . . 20 |- ( y = v -> ( ( F ` n ) ` y ) = ( ( F ` n ) ` v ) )
142	141	oveq1d 6299	. . . . . . . . . . . . . . . . . . 19 |- ( y = v -> ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) = ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) )
143		oveq1 6291	. . . . . . . . . . . . . . . . . . 19 |- ( y = v -> ( y - z ) = ( v - z ) )
144	142, 143	oveq12d 6302	. . . . . . . . . . . . . . . . . 18 |- ( y = v -> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) = ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) )
145		ovex 6309	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) e. _V
146	144, 116, 145	fvmpt 5950	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) )
147	146	oveq1d 6299	. . . . . . . . . . . . . . . 16 |- ( v e. ( X \ { z } ) -> ( ( ( y e. ( X \ { z } ) |-> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) ) ` v ) - ( ( S _D ( F ` n ) ) ` z ) ) = ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) )
148	147	fveq2d 5870	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) )
149		id 22	. . . . . . . . . . . . . . 15 |- ( s = ( ( r / 2 ) / 2 ) -> s = ( ( r / 2 ) / 2 ) )
150	148, 149	breqan12rd 4463	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) )
151	150	imbi2d 316	. . . . . . . . . . . . 13 |- ( ( 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 ) ) ) )
152	151	ralbidva 2900	. . . . . . . . . . . 12 |- ( 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 ) ) ) )
153	152	rexbidv 2973	. . . . . . . . . . 11 |- ( 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 ) ) ) )
154	153	rspcv 3210	. . . . . . . . . 10 |- ( ( ( r / 2 ) / 2 ) e. RR+ -> ( 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 ) -> 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 ) ) ) )
155	102, 140, 154	sylc 60	. . . . . . . . 9 |- ( ( ( ( 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 ) ) )
156	155	adantrr 716	. . . . . . . 8 |- ( ( ( ( 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 ) ) )
157		cnxmet 21043	. . . . . . . . . . . 12 |- ( abs o. - ) e. ( *Met ` CC )
158		xmetres2 20627	. . . . . . . . . . . 12 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ S C_ CC ) -> ( ( abs o. - ) |` ( S X. S ) ) e. ( *Met ` S ) )
159	157, 131, 158	sylancr 663	. . . . . . . . . . 11 |- ( ( ph /\ z e. X ) -> ( ( abs o. - ) |` ( S X. S ) ) e. ( *Met ` S ) )
160	159	ad3antrrr 729	. . . . . . . . . 10 |- ( ( ( ( ( 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 ) )
161	21	cnfldtop 21054	. . . . . . . . . . . . . . . . 17 |- ( TopOpen ` ℂfld ) e. Top
162		resttop 19455	. . . . . . . . . . . . . . . . 17 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ S e. { RR , CC } ) -> ( ( TopOpen ` ℂfld ) ↾t S ) e. Top )
163	161, 6, 162	sylancr 663	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t S ) e. Top )
164	21	cnfldtopon 21053	. . . . . . . . . . . . . . . . . . 19 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
165		resttopon 19456	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) )
166	164, 13, 165	sylancr 663	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) )
167		toponuni 19223	. . . . . . . . . . . . . . . . . 18 |- ( ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) -> S = U. ( ( TopOpen ` ℂfld ) ↾t S ) )
168	166, 167	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> S = U. ( ( TopOpen ` ℂfld ) ↾t S ) )
169	125, 168	sseqtrd 3540	. . . . . . . . . . . . . . . 16 |- ( ph -> X C_ U. ( ( TopOpen ` ℂfld ) ↾t S ) )
170		eqid 2467	. . . . . . . . . . . . . . . . 17 |- U. ( ( TopOpen ` ℂfld ) ↾t S ) = U. ( ( TopOpen ` ℂfld ) ↾t S )
171	170	ntrss2 19352	. . . . . . . . . . . . . . . 16 |- ( ( ( ( TopOpen ` ℂfld ) ↾t S ) e. Top /\ X C_ U. ( ( TopOpen ` ℂfld ) ↾t S ) ) -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) C_ X )
172	163, 169, 171	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) C_ X )
173	172, 27	eqssd 3521	. . . . . . . . . . . . . 14 |- ( ph -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) = X )
174	170	isopn3 19361	. . . . . . . . . . . . . . 15 |- ( ( ( ( TopOpen ` ℂfld ) ↾t S ) e. Top /\ X C_ U. ( ( TopOpen ` ℂfld ) ↾t S ) ) -> ( X e. ( ( TopOpen ` ℂfld ) ↾t S ) <-> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) = X ) )
175	163, 169, 174	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ph -> ( X e. ( ( TopOpen ` ℂfld ) ↾t S ) <-> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) = X ) )
176	173, 175	mpbird 232	. . . . . . . . . . . . 13 |- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )
177		eqid 2467	. . . . . . . . . . . . . . 15 |- ( ( abs o. - ) |` ( S X. S ) ) = ( ( abs o. - ) |` ( S X. S ) )
178	21	cnfldtopn 21052	. . . . . . . . . . . . . . 15 |- ( TopOpen ` ℂfld ) = ( MetOpen ` ( abs o. - ) )
179		eqid 2467	. . . . . . . . . . . . . . 15 |- ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) )
180	177, 178, 179	metrest 20790	. . . . . . . . . . . . . 14 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t S ) = ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) )
181	157, 13, 180	sylancr 663	. . . . . . . . . . . . 13 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t S ) = ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) )
182	176, 181	eleqtrd 2557	. . . . . . . . . . . 12 |- ( ph -> X e. ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) )
183	182	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ z e. X ) -> X e. ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) )
184	183	ad3antrrr 729	. . . . . . . . . 10 |- ( ( ( ( ( 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 ) ) ) )
185	88	ad2antrr 725	. . . . . . . . . 10 |- ( ( ( ( ( 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 )
186		simprl 755	. . . . . . . . . 10 |- ( ( ( ( ( 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+ )
187	179	mopni3 20760	. . . . . . . . . 10 |- ( ( ( ( ( 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 ) )
188	160, 184, 185, 186, 187	syl31anc 1231	. . . . . . . . 9 |- ( ( ( ( ( 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 ) )
189		anass 649	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( 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+ ) ) )
190		df-3an 975	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 ) ) ) ) )
191		anass 649	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) <-> ( ph /\ ( z e. X /\ r e. RR+ ) ) )
192	9	ralrimiva 2878	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> A. z e. X ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) )
193		fveq2 5866	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( z = s -> ( ( F ` k ) ` z ) = ( ( F ` k ) ` s ) )
194	193	mpteq2dv 4534	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( z = s -> ( k e. Z |-> ( ( F ` k ) ` z ) ) = ( k e. Z |-> ( ( F ` k ) ` s ) ) )
195		fveq2 5866	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( z = s -> ( G ` z ) = ( G ` s ) )
196	194, 195	breq12d 4460	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z = s -> ( ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) <-> ( k e. Z |-> ( ( F ` k ) ` s ) ) ~~> ( G ` s ) ) )
197	196	rspccva 3213	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A. z e. X ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) /\ s e. X ) -> ( k e. Z |-> ( ( F ` k ) ` s ) ) ~~> ( G ` s ) )
198	192, 197	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ s e. X ) -> ( k e. Z |-> ( ( F ` k ) ` s ) ) ~~> ( G ` s ) )
199		simprll 761	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 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 )
200		simprlr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 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+ )
201		simprr3 1046	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 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 ) ) ) )
202		simplll 757	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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+ )
203	201, 202	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 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+ )
204		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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+ )
205	201, 204	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 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+ )
206		simpllr 758	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( 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 ) )
207	201, 206	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 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 ) )
208	207	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 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 )
209	207	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 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 )
210		simpr3 1004	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( 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 ) )
211	201, 210	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 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 ) )
212	211	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 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 )
213		simprr1 1044	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 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 )
214		simprr2 1045	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( 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 ) ) )
215	214	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 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 ) )
216	214	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 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 ) )
217		simpr1 1002	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( 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 =/=