Theorem ulmdvlem3 23357

Description: Lemma for ulmdv 23358. (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 11173	. . . . . 6 |- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
3	1, 2	syl 17	. . . . 5 |- ( ph -> M e. ( ZZ>= ` M ) )
4		ulmdv.z	. . . . 5 |- Z = ( ZZ>= ` M )
5	3, 4	syl6eleqr 2540	. . . 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 23356	. . . . . 6 |- ( ( ph /\ k e. Z ) -> dom ( S _D ( F ` k ) ) = X )
12		recnprss 22859	. . . . . . . . 9 |- ( S e. { RR , CC } -> S C_ CC )
13	6, 12	syl 17	. . . . . . . 8 |- ( ph -> S C_ CC )
14	13	adantr 467	. . . . . . 7 |- ( ( ph /\ k e. Z ) -> S C_ CC )
15	7	ffvelrnda 6022	. . . . . . . 8 |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. ( CC ^m X ) )
16		elmapi 7493	. . . . . . . 8 |- ( ( F ` k ) e. ( CC ^m X ) -> ( F ` k ) : X --> CC )
17	15, 16	syl 17	. . . . . . 7 |- ( ( ph /\ k e. Z ) -> ( F ` k ) : X --> CC )
18		dvbsss 22857	. . . . . . . 8 |- dom ( S _D ( F ` k ) ) C_ S
19	11, 18	syl6eqssr 3483	. . . . . . 7 |- ( ( ph /\ k e. Z ) -> X C_ S )
20		eqid 2451	. . . . . . 7 |- ( ( TopOpen ` ℂfld ) ↾t S ) = ( ( TopOpen ` ℂfld ) ↾t S )
21		eqid 2451	. . . . . . 7 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
22	14, 17, 19, 20, 21	dvbssntr 22855	. . . . . 6 |- ( ( ph /\ k e. Z ) -> dom ( S _D ( F ` k ) ) C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) )
23	11, 22	eqsstr3d 3467	. . . . 5 |- ( ( ph /\ k e. Z ) -> X C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) )
24	23	ralrimiva 2802	. . . 4 |- ( ph -> A. k e. Z X C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) )
25		biidd 241	. . . . 5 |- ( k = M -> ( X C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) <-> X C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) ) )
26	25	rspcv 3146	. . . 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 62	. . 3 |- ( ph -> X C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) )
28	27	sselda 3432	. 2 |- ( ( ph /\ z e. X ) -> z e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` X ) )
29		ulmcl 23336	. . . . 5 |- ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~> u ` X ) H -> H : X --> CC )
30	10, 29	syl 17	. . . 4 |- ( ph -> H : X --> CC )
31	30	ffvelrnda 6022	. . 3 |- ( ( ph /\ z e. X ) -> ( H ` z ) e. CC )
32		rphalfcl 11327	. . . . . . . 8 |- ( r e. RR+ -> ( r / 2 ) e. RR+ )
33	32	adantl 468	. . . . . . 7 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( r / 2 ) e. RR+ )
34		rphalfcl 11327	. . . . . . 7 |- ( ( r / 2 ) e. RR+ -> ( ( r / 2 ) / 2 ) e. RR+ )
35	33, 34	syl 17	. . . . . 6 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( ( r / 2 ) / 2 ) e. RR+ )
36		ulmrel 23333	. . . . . . . . . 10 |- Rel ( ~~> u ` X )
37		releldm 5067	. . . . . . . . . 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 669	. . . . . . . . 9 |- ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) e. dom ( ~~> u ` X ) )
39		ulmscl 23334	. . . . . . . . . . 11 |- ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~> u ` X ) H -> X e. _V )
40	10, 39	syl 17	. . . . . . . . . 10 |- ( ph -> X e. _V )
41		ovex 6318	. . . . . . . . . . . . 13 |- ( S _D ( F ` k ) ) e. _V
42	41	rgenw 2749	. . . . . . . . . . . 12 |- A. k e. Z ( S _D ( F ` k ) ) e. _V
43		eqid 2451	. . . . . . . . . . . . 13 |- ( k e. Z |-> ( S _D ( F ` k ) ) ) = ( k e. Z |-> ( S _D ( F ` k ) ) )
44	43	fnmpt 5704	. . . . . . . . . . . 12 |- ( A. k e. Z ( S _D ( F ` k ) ) e. _V -> ( k e. Z |-> ( S _D ( F ` k ) ) ) Fn Z )
45	42, 44	mp1i 13	. . . . . . . . . . 11 |- ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) Fn Z )
46		ulmf2 23339	. . . . . . . . . . 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 667	. . . . . . . . . 10 |- ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) : Z --> ( CC ^m X ) )
48	4, 1, 40, 47	ulmcau2 23351	. . . . . . . . 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 214	. . . . . . . 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 11176	. . . . . . . . . . . . . . . . . 18 |- ( ( j e. Z /\ n e. ( ZZ>= ` j ) ) -> n e. Z )
51	50	ad2ant2lr 754	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> n e. Z )
52		fveq2 5865	. . . . . . . . . . . . . . . . . . 19 |- ( k = n -> ( F ` k ) = ( F ` n ) )
53	52	oveq2d 6306	. . . . . . . . . . . . . . . . . 18 |- ( k = n -> ( S _D ( F ` k ) ) = ( S _D ( F ` n ) ) )
54		ovex 6318	. . . . . . . . . . . . . . . . . 18 |- ( S _D ( F ` n ) ) e. _V
55	53, 43, 54	fvmpt 5948	. . . . . . . . . . . . . . . . 17 |- ( n e. Z -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` n ) = ( S _D ( F ` n ) ) )
56	51, 55	syl 17	. . . . . . . . . . . . . . . 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 5867	. . . . . . . . . . . . . . 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 766	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> m e. ( ZZ>= ` n ) )
59	4	uztrn2 11176	. . . . . . . . . . . . . . . . . 18 |- ( ( n e. Z /\ m e. ( ZZ>= ` n ) ) -> m e. Z )
60	51, 58, 59	syl2anc 667	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. Z ) /\ ( n e. ( ZZ>= ` j ) /\ m e. ( ZZ>= ` n ) ) ) -> m e. Z )
61		fveq2 5865	. . . . . . . . . . . . . . . . . . 19 |- ( k = m -> ( F ` k ) = ( F ` m ) )
62	61	oveq2d 6306	. . . . . . . . . . . . . . . . . 18 |- ( k = m -> ( S _D ( F ` k ) ) = ( S _D ( F ` m ) ) )
63		ovex 6318	. . . . . . . . . . . . . . . . . 18 |- ( S _D ( F ` m ) ) e. _V
64	62, 43, 63	fvmpt 5948	. . . . . . . . . . . . . . . . 17 |- ( m e. Z -> ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ` m ) = ( S _D ( F ` m ) ) )
65	60, 64	syl 17	. . . . . . . . . . . . . . . 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 5867	. . . . . . . . . . . . . . 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 6308	. . . . . . . . . . . . . 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 5869	. . . . . . . . . . . . 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 4412	. . . . . . . . . . . 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 2827	. . . . . . . . . . 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 2830	. . . . . . . . . 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 2898	. . . . . . . . 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 2827	. . . . . . . 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 214	. . . . . . 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 732	. . . . . 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 4406	. . . . . . . . 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 2832	. . . . . . . 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 2909	. . . . . . 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 3146	. . . . . 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 62	. . . . 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 732	. . . . . 6 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> M e. ZZ )
82	53	fveq1d 5867	. . . . . . . 8 |- ( k = n -> ( ( S _D ( F ` k ) ) ` z ) = ( ( S _D ( F ` n ) ) ` z ) )
83		eqid 2451	. . . . . . . 8 |- ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) ) = ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) )
84		fvex 5875	. . . . . . . 8 |- ( ( S _D ( F ` n ) ) ` z ) e. _V
85	82, 83, 84	fvmpt 5948	. . . . . . 7 |- ( n e. Z -> ( ( k e. Z |-> ( ( S _D ( F ` k ) ) ` z ) ) ` n ) = ( ( S _D ( F ` n ) ) ` z ) )
86	85	adantl 468	. . . . . 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 732	. . . . . . 7 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> ( k e. Z |-> ( S _D ( F ` k ) ) ) : Z --> ( CC ^m X ) )
88		simplr 762	. . . . . . 7 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> z e. X )
89		fvex 5875	. . . . . . . . . 10 |- ( ZZ>= ` M ) e. _V
90	4, 89	eqeltri 2525	. . . . . . . . 9 |- Z e. _V
91	90	mptex 6136	. . . . . . . 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 468	. . . . . . . . 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 5867	. . . . . . . 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 2488	. . . . . . 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 732	. . . . . . 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 23342	. . . . . 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 13575	. . . . 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 13412	. . . . . . 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 13414	. . . . . . 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 217	. . . . . 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 467	. . . . . . . . . 10 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( ( r / 2 ) / 2 ) e. RR+ )
103		simpllr 769	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> z e. X )
104	87	ffvelrnda 6022	. . . . . . . . . . . . . . . . . 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 2530	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( S _D ( F ` n ) ) e. ( CC ^m X ) )
106		elmapi 7493	. . . . . . . . . . . . . . . . 17 |- ( ( S _D ( F ` n ) ) e. ( CC ^m X ) -> ( S _D ( F ` n ) ) : X --> CC )
107		fdm 5733	. . . . . . . . . . . . . . . . 17 |- ( ( S _D ( F ` n ) ) : X --> CC -> dom ( S _D ( F ` n ) ) = X )
108	105, 106, 107	3syl 18	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> dom ( S _D ( F ` n ) ) = X )
109	103, 108	eleqtrrd 2532	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> z e. dom ( S _D ( F ` n ) ) )
110	6	ad3antrrr 736	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> S e. { RR , CC } )
111		dvfg 22861	. . . . . . . . . . . . . . . 16 |- ( S e. { RR , CC } -> ( S _D ( F ` n ) ) : dom ( S _D ( F ` n ) ) --> CC )
112		ffun 5731	. . . . . . . . . . . . . . . 16 |- ( ( S _D ( F ` n ) ) : dom ( S _D ( F ` n ) ) --> CC -> Fun ( S _D ( F ` n ) ) )
113		funfvbrb 5995	. . . . . . . . . . . . . . . 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 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 ) ) )
115	109, 114	mpbid 214	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> z ( S _D ( F ` n ) ) ( ( S _D ( F ` n ) ) ` z ) )
116		eqid 2451	. . . . . . . . . . . . . . 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 17	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> S C_ CC )
118	7	ad2antrr 732	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) -> F : Z --> ( CC ^m X ) )
119	118	ffvelrnda 6022	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( F ` n ) e. ( CC ^m X ) )
120		elmapi 7493	. . . . . . . . . . . . . . . 16 |- ( ( F ` n ) e. ( CC ^m X ) -> ( F ` n ) : X --> CC )
121	119, 120	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( F ` n ) : X --> CC )
122	19	ralrimiva 2802	. . . . . . . . . . . . . . . . 17 |- ( ph -> A. k e. Z X C_ S )
123		biidd 241	. . . . . . . . . . . . . . . . . 18 |- ( k = M -> ( X C_ S <-> X C_ S ) )
124	123	rspcv 3146	. . . . . . . . . . . . . . . . 17 |- ( M e. Z -> ( A. k e. Z X C_ S -> X C_ S ) )
125	5, 122, 124	sylc 62	. . . . . . . . . . . . . . . 16 |- ( ph -> X C_ S )
126	125	ad3antrrr 736	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> X C_ S )
127	20, 21, 116, 117, 121, 126	eldv 22853	. . . . . . . . . . . . . 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 214	. . . . . . . . . . . . 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 465	. . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. X ) -> X C_ S )
131	13	adantr 467	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. X ) -> S C_ CC )
132	130, 131	sstrd 3442	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ z e. X ) -> X C_ CC )
133	132	ad2antrr 732	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> X C_ CC )
134	121, 133, 103	dvlem 22851	. . . . . . . . . . . . . 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 6046	. . . . . . . . . . . . 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 3571	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> ( X \ { z } ) C_ CC )
137	133, 103	sseldd 3433	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ z e. X ) /\ r e. RR+ ) /\ n e. Z ) -> z e. CC )
138	135, 136, 137	ellimc3 22834	. . . . . . . . . . . 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 214	. . . . . . . . . . 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 465	. . . . . . . . . 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 5865	. . . . . . . . . . . . . . . . . . . 20 |- ( y = v -> ( ( F ` n ) ` y ) = ( ( F ` n ) ` v ) )
142	141	oveq1d 6305	. . . . . . . . . . . . . . . . . . 19 |- ( y = v -> ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) = ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) )
143		oveq1 6297	. . . . . . . . . . . . . . . . . . 19 |- ( y = v -> ( y - z ) = ( v - z ) )
144	142, 143	oveq12d 6308	. . . . . . . . . . . . . . . . . 18 |- ( y = v -> ( ( ( ( F ` n ) ` y ) - ( ( F ` n ) ` z ) ) / ( y - z ) ) = ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) )
145		ovex 6318	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) e. _V
146	144, 116, 145	fvmpt 5948	. . . . . . . . . . . . . . . . 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 6305	. . . . . . . . . . . . . . . 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 5869	. . . . . . . . . . . . . . 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 4419	. . . . . . . . . . . . . 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 318	. . . . . . . . . . . . 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 2824	. . . . . . . . . . . 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 2901	. . . . . . . . . . 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 3146	. . . . . . . . . 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 62	. . . . . . . . 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 723	. . . . . . . 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		anass 655	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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+ ) ) )
158		df-3an 987	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) ) ) ) )
159		anass 655	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ z e. X ) /\ r e. RR+ ) <-> ( ph /\ ( z e. X /\ r e. RR+ ) ) )
160	9	ralrimiva 2802	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> A. z e. X ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) )
161		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z = s -> ( ( F ` k ) ` z ) = ( ( F ` k ) ` s ) )
162	161	mpteq2dv 4490	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z = s -> ( k e. Z |-> ( ( F ` k ) ` z ) ) = ( k e. Z |-> ( ( F ` k ) ` s ) ) )
163		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z = s -> ( G ` z ) = ( G ` s ) )
164	162, 163	breq12d 4415	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( z = s -> ( ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) <-> ( k e. Z |-> ( ( F ` k ) ` s ) ) ~~> ( G ` s ) ) )
165	164	rspccva 3149	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A. z e. X ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) /\ s e. X ) -> ( k e. Z |-> ( ( F ` k ) ` s ) ) ~~> ( G ` s ) )
166	160, 165	sylan 474	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ s e. X ) -> ( k e. Z |-> ( ( F ` k ) ` s ) ) ~~> ( G ` s ) )
167		simprll 772	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 )
168		simprlr 773	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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+ )
169		simprr3 1058	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 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 ) ) ) )
170		simplll 768	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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+ )
171	169, 170	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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+ )
172		simplr 762	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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+ )
173	169, 172	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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+ )
174		simpllr 769	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 ) )
175	169, 174	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 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 ) )
176	175	simpld 461	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 )
177	175	simprd 465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 )
178		simpr3 1016	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 ) )
179	169, 178	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 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 ) )
180	179	simprd 465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 )
181		simprr1 1056	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 )
182		simprr2 1057	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 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 ) ) )
183	182	simpld 461	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 ) )
184	182	simprd 465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 ) )
185		simpr1 1014	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) -> v e. ( X \ { z } ) )
186	169, 185	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> v e. ( X \ { z } ) )
187	186	eldifad 3416	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> v e. X )
188	179	simpld 461	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 )
189		simpr2 1015	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) -> ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) )
190	169, 189	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) )
191	188, 190	mpand 681	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> ( ( abs ` ( v - z ) ) < w -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) )
192	4, 6, 1, 7, 8, 166, 10, 167, 168, 171, 173, 176, 177, 180, 181, 183, 184, 187, 188, 191	ulmdvlem1 23355	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( ( z e. X /\ r e. RR+ ) /\ ( n e. Z /\ ( A. m e. ( ZZ>= ` n ) A. x e. X ( abs ` ( ( ( S _D ( F ` n ) ) ` x ) - ( ( S _D ( F ` m ) ) ` x ) ) ) < ( ( r / 2 ) / 2 ) /\ ( abs ` ( ( ( S _D ( F ` n ) ) ` z ) - ( H ` z ) ) ) < ( r / 2 ) ) /\ ( ( ( u e. RR+ /\ ( u < w /\ ( z ( ball ` ( ( abs o. - ) |` ( S X. S ) ) ) u ) C_ X ) ) /\ w e. RR+ ) /\ ( v e. ( X \ { z } ) /\ ( ( v =/= z /\ ( abs ` ( v - z ) ) < w ) -> ( abs ` ( ( ( ( ( F ` n ) ` v ) - ( ( F ` n ) ` z ) ) / ( v - z ) ) - ( ( S _D ( F ` n ) ) ` z ) ) ) < ( ( r / 2 ) / 2 ) ) /\ ( v =/= z /\ ( abs ` ( v - z ) ) < u ) ) ) ) ) ) -> ( abs ` ( ( ( ( G ` v ) - ( G ` z ) ) / ( v - z ) ) - ( H ` z ) ) ) <