Theorem ulmdvlem3 20271

Description: Lemma for ulmdv 20272. (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 10456	. . . . . 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 2495	. . . 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 20270	. . . . . 6 |- ( ( ph /\ k e. Z ) -> dom ( S _D ( F ` k ) ) = X )
12		recnprss 19744	. . . . . . . . 9 |- ( S e. { RR , CC } -> S C_ CC )
13	6, 12	syl 16	. . . . . . . 8 |- ( ph -> S C_ CC )
14	13	adantr 452	. . . . . . 7 |- ( ( ph /\ k e. Z ) -> S C_ CC )
15	7	ffvelrnda 5829	. . . . . . . 8 |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. ( CC ^m X ) )
16		elmapi 6997	. . . . . . . 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 19742	. . . . . . . 8 |- dom ( S _D ( F ` k ) ) C_ S
19	11, 18	syl6eqssr 3359	. . . . . . 7 |- ( ( ph /\ k e. Z ) -> X C_ S )
20		eqid 2404	. . . . . . 7 |- ( ( TopOpen ` ℂfld ) ↾t S ) = ( ( TopOpen ` ℂfld ) ↾t S )
21		eqid 2404	. . . . . . 7 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
22	14, 17, 19, 20, 21	dvbssntr 19740	. . . . . 6 |- ( ( ph /\ k e. Z ) -> dom ( S _D ( F ` k ) ) C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) )
23	11, 22	eqsstr3d 3343	. . . . 5 |- ( ( ph /\ k e. Z ) -> X C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) )
24	23	ralrimiva 2749	. . . 4 |- ( ph -> A. k e. Z X C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) )
25		biidd 229	. . . . 5 |- ( k = M -> ( X C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) <-> X C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) ) )
26	25	rspcv 3008	. . . 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 58	. . 3 |- ( ph -> X C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) )
28	27	sselda 3308	. 2 |- ( ( ph /\ z e. X ) -> z e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) )
29		ulmcl 20250	. . . . 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 5829	. . 3 |- ( ( ph /\ z e. X ) -> ( H ` z ) e. CC )
32		rphalfcl 10592	. . . . . . . 8 |- ( r e. RR+ -> ( r / 2 ) e. RR+ )
33	32	adantl 453	. . . . . . 7 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( r / 2 ) e. RR+ )
34		rphalfcl 10592	. . . . . . 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 20247	. . . . . . . . . 10 |- Rel ( ~~> u ` X )
37		releldm 5061	. . . . . . . . . 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 645	. . . . . . . . 9 |- ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) e. dom ( ~~> u ` X ) )
39		ulmscl 20248	. . . . . . . . . . 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 6065	. . . . . . . . . . . . 13 |- ( S _D ( F ` k ) ) e. _V
42	41	rgenw 2733	. . . . . . . . . . . 12 |- A. k e. Z ( S _D ( F ` k ) ) e. _V
43		eqid 2404	. . . . . . . . . . . . 13 |- ( k e. Z |-> ( S _D ( F ` k ) ) ) = ( k e. Z |-> ( S _D ( F ` k ) ) )
44	43	fnmpt 5530	. . . . . . . . . . . 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 20253	. . . . . . . . . . 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 643	. . . . . . . . . 10 |- ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) : Z --> ( CC ^m X ) )
48	4, 1, 40, 47	ulmcau2 20265	. . . . . . . . 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 202	. . . . . . . 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 10459	. . . . . . . . . . . . . . . . . 18 |- ( ( j e. Z /\ n e. ( ZZ>= ` j ) ) -> n e. Z )
51	50	ad2ant2lr 729	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> n e. Z )
52		fveq2 5687	. . . . . . . . . . . . . . . . . . 19 |- ( k = n -> ( F ` k ) = ( F ` n ) )
53	52	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 |- ( k = n -> ( S _D ( F ` k ) ) = ( S _D ( F ` n ) ) )
54		ovex 6065	. . . . . . . . . . . . . . . . . 18 |- ( S _D ( F ` n ) ) e. _V
55	53, 43, 54	fvmpt 5765	. . . . . . . . . . . . . . . . 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 5689	. . . . . . . . . . . . . . 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 734	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> m e. ( ZZ>= ` n ) )
59	4	uztrn2 10459	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. Z /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
60	51, 58, 59	syl2anc 643	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> m e. Z )
61		fveq2 5687	. . . . . . . . . . . . . . . . . . 19 |- ( k = m -> ( F ` k ) = ( F ` m ) )
62	61	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 |- ( k = m -> ( S _D ( F ` k ) ) = ( S _D ( F ` m ) ) )
63		ovex 6065	. . . . . . . . . . . . . . . . . 18 |- ( S _D ( F ` m ) ) e. _V
64	62, 43, 63	fvmpt 5765	. . . . . . . . . . . . . . . . 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 5689	. . . . . . . . . . . . . . 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 6058	. . . . . . . . . . . . . 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 5691	. . . . . . . . . . . . 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 4182	. . . . . . . . . . . 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 2686	. . . . . . . . . . 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 2706	. . . . . . . . . 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 2683	. . . . . . . . 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 2686	. . . . . . . 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 202	. . . . . . 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 707	. . . . . 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 4176	. . . . . . . . 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 2708	. . . . . . . 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 2710	. . . . . . 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 3008	. . . . . 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 58	. . . . 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 707	. . . . . 6 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> M e. ZZ )
82	53	fveq1d 5689	. . . . . . . 8 |- ( k = n -> ( ( S _D ( F ` k ) ) ` z ) = ( ( S _D ( F ` n ) ) ` z ) )
83		eqid 2404	. . . . . . . 8 |- ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) ) = ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) )
84		fvex 5701	. . . . . . . 8 |- ( ( S _D ( F ` n ) ) ` z ) e. _V
85	82, 83, 84	fvmpt 5765	. . . . . . 7 |- ( n e. Z -> ( ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) ) ` n ) = ( ( S _D ( F ` n ) ) ` z ) )
86	85	adantl 453	. . . . . 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 707	. . . . . . 7 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( k e. Z |-> ( S _D ( F ` k ) ) ) : Z --> ( CC ^m X ) )
88		simplr 732	. . . . . . 7 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> z e. X )
89		fvex 5701	. . . . . . . . . 10 |- ( ZZ>= ` M ) e. _V
90	4, 89	eqeltri 2474	. . . . . . . . 9 |- Z e. _V
91	90	mptex 5925	. . . . . . . 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 453	. . . . . . . . 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 5689	. . . . . . . 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 2439	. . . . . . 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 707	. . . . . . 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 20256	. . . . . 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 12260	. . . . 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 12108	. . . . . . 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 12110	. . . . . . 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 205	. . . . . 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 452	. . . . . . . . . 10 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( ( r / 2 ) / 2 ) e. RR+ )
103		simpllr 736	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> z e. X )
104	87	ffvelrnda 5829	. . . . . . . . . . . . . . . . . 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 2479	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( S _D ( F ` n ) ) e. ( CC ^m X ) )
106		elmapi 6997	. . . . . . . . . . . . . . . . 17 |- ( ( S _D ( F ` n ) ) e. ( CC ^m X ) -> ( S _D ( F ` n ) ) : X --> CC )
107		fdm 5554	. . . . . . . . . . . . . . . . 17 |- ( ( S _D ( F ` n ) ) : X --> CC -> dom ( S _D ( F ` n ) ) = X )
108	105, 106, 107	3syl 19	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> dom ( S _D ( F ` n ) ) = X )
109	103, 108	eleqtrrd 2481	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> z e. dom ( S _D ( F ` n ) ) )
110	6	ad3antrrr 711	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> S e. { RR , CC } )
111		dvfg 19746	. . . . . . . . . . . . . . . . 17 |- ( S e. { RR , CC } -> ( S _D ( F ` n ) ) : dom ( S _D ( F ` n ) ) --> CC )
112	110, 111	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( S _D ( F ` n ) ) : dom ( S _D ( F ` n ) ) --> CC )
113		ffun 5552	. . . . . . . . . . . . . . . 16 |- ( ( S _D ( F ` n ) ) : dom ( S _D ( F ` n ) ) --> CC -> Fun ( S _D ( F ` n ) ) )
114		funfvbrb 5802	. . . . . . . . . . . . . . . 16 |- ( Fun ( S _D ( F ` n ) ) -> ( z e. dom ( S _D ( F ` n ) ) <-> z ( S _D ( F ` n ) ) ( ( S _D ( F ` n ) ) ` z ) ) )
115	112, 113, 114	3syl 19	. . . . . . . . . . . . . . 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 ) ) )
116	109, 115	mpbid 202	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> z ( S _D ( F ` n ) ) ( ( S _D ( F ` n ) ) ` z ) )
117		eqid 2404	. . . . . . . . . . . . . . 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 ) ) )
118	110, 12	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> S C_ CC )
119	7	ad2antrr 707	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> F : Z --> ( CC ^m X ) )
120	119	ffvelrnda 5829	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( F ` n ) e. ( CC ^m X ) )
121		elmapi 6997	. . . . . . . . . . . . . . . 16 |- ( ( F ` n ) e. ( CC ^m X ) -> ( F ` n ) : X --> CC )
122	120, 121	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( F ` n ) : X --> CC )
123	19	ralrimiva 2749	. . . . . . . . . . . . . . . . 17 |- ( ph -> A. k e. Z X C_ S )
124		biidd 229	. . . . . . . . . . . . . . . . . 18 |- ( k = M -> ( X C_ S <-> X C_ S ) )
125	124	rspcv 3008	. . . . . . . . . . . . . . . . 17 |- ( M e. Z -> ( A. k e. Z X C_ S -> X C_ S ) )
126	5, 123, 125	sylc 58	. . . . . . . . . . . . . . . 16 |- ( ph -> X C_ S )
127	126	ad3antrrr 711	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> X C_ S )
128	20, 21, 117, 118, 122, 127	eldv 19738	. . . . . . . . . . . . . 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 ) ) ) )
129	116, 128	mpbid 202	. . . . . . . . . . . . 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 ) ) )
130	129	simprd 450	. . . . . . . . . . . 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 ) )
131	126	adantr 452	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. X ) -> X C_ S )
132	13	adantr 452	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. X ) -> S C_ CC )
133	131, 132	sstrd 3318	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ z e. X ) -> X C_ CC )
134	133	ad2antrr 707	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> X C_ CC )
135	122, 134, 103	dvlem 19736	. . . . . . . . . . . . . 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 )
136	135, 117	fmptd 5852	. . . . . . . . . . . . 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 )
137	134	ssdifssd 3445	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( X \ { z } ) C_ CC )
138	134, 103	sseldd 3309	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> z e. CC )
139	136, 137, 138	ellimc3 19719	. . . . . . . . . . . 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 ) ) ) )
140	130, 139	mpbid 202	. . . . . . . . . . 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 ) ) )
141	140	simprd 450	. . . . . . . . . 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 ) )
142		fveq2 5687	. . . . . . . . . . . . . . . . . . . 20 |- ( y = v -> ( ( F ` n ) ` y ) = ( ( F ` n ) ` v ) )
143	142	oveq1d 6055	. . . . . . . . . . . . . . . . . . 19 |- ( y = v -> ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) = ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) )
144		oveq1 6047	. . . . . . . . . . . . . . . . . . 19 |- ( y = v -> ( y - z ) = ( v - z ) )
145	143, 144	oveq12d 6058	. . . . . . . . . . . . . . . . . 18 |- ( y = v -> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) = ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) )
146		ovex 6065	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) e. _V
147	145, 117, 146	fvmpt 5765	. . . . . . . . . . . . . . . . 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 ) ) )
148	147	oveq1d 6055	. . . . . . . . . . . . . . . 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 ) ) )
149	148	fveq2d 5691	. . . . . . . . . . . . . . 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 ) ) ) )
150		id 20	. . . . . . . . . . . . . . 15 |- ( s = ( ( r / 2 ) / 2 ) -> s = ( ( r / 2 ) / 2 ) )
151	149, 150	breqan12rd 4188	. . . . . . . . . . . . . 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 ) ) )
152	151	imbi2d 308	. . . . . . . . . . . . 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 ) ) ) )
153	152	ralbidva 2682	. . . . . . . . . . . 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 ) ) ) )
154	153	rexbidv 2687	. . . . . . . . . . 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 ) ) ) )
155	154	rspcv 3008	. . . . . . . . . 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 ) ) ) )
156	102, 141, 155	sylc 58	. . . . . . . . 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 ) ) )
157	156	adantrr 698	. . . . . . . 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 ) ) )
158		cnxmet 18760	. . . . . . . . . . . 12 |- ( abs o. - ) e. ( * Met ` CC )
159		xmetres2 18344	. . . . . . . . . . . 12 |- ( ( ( abs o. - ) e. ( * Met ` CC ) /\ S C_ CC ) -> ( ( abs o. - ) |` ( S X. S ) ) e. ( * Met ` S ) )
160	158, 132, 159	sylancr 645	. . . . . . . . . . 11 |- ( ( ph /\ z e. X ) -> ( ( abs o. - ) |` ( S X. S ) ) e. ( * Met ` S ) )
161	160	ad3antrrr 711	. . . . . . . . . 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 ) )
162	21	cnfldtop 18771	. . . . . . . . . . . . . . . . 17 |- ( TopOpen ` ℂfld ) e. Top
163		resttop 17178	. . . . . . . . . . . . . . . . 17 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ S e. { RR , CC } ) -> ( ( TopOpen ` ℂfld ) ↾t S ) e. Top )
164	162, 6, 163	sylancr 645	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t S ) e. Top )
165	21	cnfldtopon 18770	. . . . . . . . . . . . . . . . . . 19 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
166		resttopon 17179	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) )
167	165, 13, 166	sylancr 645	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) )
168		toponuni 16947	. . . . . . . . . . . . . . . . . 18 |- ( ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) -> S = U. ( ( TopOpen ` ℂfld ) ↾t S ) )
169	167, 168	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> S = U. ( ( TopOpen ` ℂfld ) ↾t S ) )
170	126, 169	sseqtrd 3344	. . . . . . . . . . . . . . . 16 |- ( ph -> X C_ U. ( ( TopOpen ` ℂfld ) ↾t S ) )
171		eqid 2404	. . . . . . . . . . . . . . . . 17 |- U. ( ( TopOpen ` ℂfld ) ↾t S ) = U. ( ( TopOpen ` ℂfld ) ↾t S )
172	171	ntrss2 17076	. . . . . . . . . . . . . . . 16 |- ( ( ( ( TopOpen ` ℂfld ) ↾t S ) e. Top /\ X C_ U. ( ( TopOpen ` ℂfld ) ↾t S ) ) -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) C_ X )
173	164, 170, 172	syl2anc 643	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) C_ X )
174	173, 27	eqssd 3325	. . . . . . . . . . . . . 14 |- ( ph -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) = X )
175	171	isopn3 17085	. . . . . . . . . . . . . . 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 ) )
176	164, 170, 175	syl2anc 643	. . . . . . . . . . . . . 14 |- ( ph -> ( X e. ( ( TopOpen ` ℂfld ) ↾t S ) <-> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) = X ) )
177	174, 176	mpbird 224	. . . . . . . . . . . . 13 |- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )
178		eqid 2404	. . . . . . . . . . . . . . 15 |- ( ( abs o. - ) |` ( S X. S ) ) = ( ( abs o. - ) |` ( S X. S ) )
179	21	cnfldtopn 18769	. . . . . . . . . . . . . . 15 |- ( TopOpen ` ℂfld ) = ( MetOpen ` ( abs o. - ) )
180		eqid 2404	. . . . . . . . . . . . . . 15 |- ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) )
181	178, 179, 180	metrest 18507	. . . . . . . . . . . . . 14 |- ( ( ( abs o. - ) e. ( * Met ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t S ) = ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) )
182	158, 13, 181	sylancr 645	. . . . . . . . . . . . 13 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t S ) = ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) )
183	177, 182	eleqtrd 2480	. . . . . . . . . . . 12 |- ( ph -> X e. ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) )
184	183	adantr 452	. . . . . . . . . . 11 |- ( ( ph /\ z e. X ) -> X e. ( MetOpen ` ( ( abs o. - ) |` ( S X. S ) ) ) )
185	184	ad3antrrr 711	. . . . . . . . . 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 ) ) ) )
186	88	ad2antrr 707	. . . . . . . . . 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 )
187		simprl 733	. . . . . . . . . 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+ )
188	180	mopni3 18477	. . . . . . . . . 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 ) )
189	161, 185, 186, 187, 188	syl31anc 1187	. . . . . . . . 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 ) )
190		anass 631	. . . . . . . . . . . . . . . . . 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+ ) ) )
191		df-3an 938	. . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
192		anass 631	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) <-> ( ph /\ ( z e. X /\ r e. RR+ ) ) )
193	9	ralrimiva 2749	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> A. z e. X ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) )
194		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( z = s -> ( ( F ` k ) ` z ) = ( ( F ` k ) ` s ) )
195	194	mpteq2dv 4256	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( z = s -> ( k e. Z |-> ( ( F ` k ) ` z ) ) = ( k e. Z |-> ( ( F ` k ) ` s ) ) )
196		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( z = s -> ( G ` z ) = ( G ` s ) )
197	195, 196	breq12d 4185	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z = s -> ( ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) <-> ( k e. Z |-> ( ( F ` k ) ` s ) ) ~~> ( G ` s ) ) )
198	197	rspccva 3011	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A. z e. X ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) /\ s e. X ) -> ( k e. Z |-> ( ( F ` k ) ` s ) ) ~~> ( G ` s ) )
199	193, 198	sylan 458	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ s e. X ) -> ( k e. Z |-> ( ( F ` k ) ` s ) ) ~~> ( G ` s ) )
200		simprll 739	. . . . . . . . . . . . . . . . . . . . . . . 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 )
201		simprlr 740	. . . . . . . . . . . . . . . . . . . . . . . 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+ )
202		simprr3 1007	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
203		simplll 735	. . . . . . . . . . . . . . . . . . . . . . . . 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+ )
204	202, 203	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+ )
205		simplr 732	. . . . . . . . . . . . . . . . . . . . . . . . 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+ )
206	202, 205	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+ )
207		simpllr 736	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
208	202, 207	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 ) )
209	208	simpld 446	. . . . . . . . . . . . . . . . . . . . . . . 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 )
210	208	simprd 450	. . . . . . . . . . . . . . . . . . . . . . . 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 )
211		simpr3 965	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
212	202, 211	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 ) )
213	212	simprd 450	. . . . . . . . . . . . . . . . . . . . . . . 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 )
214		simprr1 1005	. . . . . . . . . . . . . . . . . . . . . . . 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 )
215		simprr2 1006	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
216	215	simpld 446	. . . . . . . . . . . . . . . . . . . . . . . 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 ) )
217	215	simprd 450	. . . . . . . . . . . . . . . . . . . . . . . 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 ) )
218		simpr1 963	. . . . . . . . . . . . . . . . . . . . . . . . . 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