Metamath Proof Explorer


Theorem ulmcau

Description: A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < x there is a j such that for all j <_ k the functions F ( k ) and F ( j ) are uniformly within x of each other on S . This is the four-quantifier version, see ulmcau2 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015)

Ref Expression
Hypotheses ulmcau.z
|- Z = ( ZZ>= ` M )
ulmcau.m
|- ( ph -> M e. ZZ )
ulmcau.s
|- ( ph -> S e. V )
ulmcau.f
|- ( ph -> F : Z --> ( CC ^m S ) )
Assertion ulmcau
|- ( ph -> ( F e. dom ( ~~>u ` S ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )

Proof

Step Hyp Ref Expression
1 ulmcau.z
 |-  Z = ( ZZ>= ` M )
2 ulmcau.m
 |-  ( ph -> M e. ZZ )
3 ulmcau.s
 |-  ( ph -> S e. V )
4 ulmcau.f
 |-  ( ph -> F : Z --> ( CC ^m S ) )
5 eldmg
 |-  ( F e. dom ( ~~>u ` S ) -> ( F e. dom ( ~~>u ` S ) <-> E. g F ( ~~>u ` S ) g ) )
6 5 ibi
 |-  ( F e. dom ( ~~>u ` S ) -> E. g F ( ~~>u ` S ) g )
7 2 ad2antrr
 |-  ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) -> M e. ZZ )
8 4 ad2antrr
 |-  ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) -> F : Z --> ( CC ^m S ) )
9 eqidd
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ ( k e. Z /\ z e. S ) ) -> ( ( F ` k ) ` z ) = ( ( F ` k ) ` z ) )
10 eqidd
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ z e. S ) -> ( g ` z ) = ( g ` z ) )
11 simplr
 |-  ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) -> F ( ~~>u ` S ) g )
12 rphalfcl
 |-  ( x e. RR+ -> ( x / 2 ) e. RR+ )
13 12 adantl
 |-  ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) -> ( x / 2 ) e. RR+ )
14 1 7 8 9 10 11 13 ulmi
 |-  ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) )
15 simpr
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) -> j e. Z )
16 15 1 eleqtrdi
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) -> j e. ( ZZ>= ` M ) )
17 eluzelz
 |-  ( j e. ( ZZ>= ` M ) -> j e. ZZ )
18 uzid
 |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )
19 fveq2
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
20 19 fveq1d
 |-  ( k = j -> ( ( F ` k ) ` z ) = ( ( F ` j ) ` z ) )
21 20 fvoveq1d
 |-  ( k = j -> ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) = ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) )
22 21 breq1d
 |-  ( k = j -> ( ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) <-> ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) ) )
23 22 ralbidv
 |-  ( k = j -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) <-> A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) ) )
24 23 rspcv
 |-  ( j e. ( ZZ>= ` j ) -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) -> A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) ) )
25 16 17 18 24 4syl
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) -> A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) ) )
26 r19.26
 |-  ( A. z e. S ( ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) /\ ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) ) <-> ( A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) /\ A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) ) )
27 8 ffvelrnda
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) -> ( F ` j ) e. ( CC ^m S ) )
28 27 adantr
 |-  ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` j ) e. ( CC ^m S ) )
29 elmapi
 |-  ( ( F ` j ) e. ( CC ^m S ) -> ( F ` j ) : S --> CC )
30 28 29 syl
 |-  ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` j ) : S --> CC )
31 30 ffvelrnda
 |-  ( ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( ( F ` j ) ` z ) e. CC )
32 ulmcl
 |-  ( F ( ~~>u ` S ) g -> g : S --> CC )
33 32 ad4antlr
 |-  ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> g : S --> CC )
34 33 ffvelrnda
 |-  ( ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( g ` z ) e. CC )
35 31 34 abssubd
 |-  ( ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) = ( abs ` ( ( g ` z ) - ( ( F ` j ) ` z ) ) ) )
36 35 breq1d
 |-  ( ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) <-> ( abs ` ( ( g ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) )
37 36 biimpd
 |-  ( ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) -> ( abs ` ( ( g ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) )
38 1 uztrn2
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
39 ffvelrn
 |-  ( ( F : Z --> ( CC ^m S ) /\ k e. Z ) -> ( F ` k ) e. ( CC ^m S ) )
40 8 38 39 syl2an
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( F ` k ) e. ( CC ^m S ) )
41 40 anassrs
 |-  ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. ( CC ^m S ) )
42 elmapi
 |-  ( ( F ` k ) e. ( CC ^m S ) -> ( F ` k ) : S --> CC )
43 41 42 syl
 |-  ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) : S --> CC )
44 43 ffvelrnda
 |-  ( ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( ( F ` k ) ` z ) e. CC )
45 rpre
 |-  ( x e. RR+ -> x e. RR )
46 45 ad4antlr
 |-  ( ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> x e. RR )
47 abs3lem
 |-  ( ( ( ( ( F ` k ) ` z ) e. CC /\ ( ( F ` j ) ` z ) e. CC ) /\ ( ( g ` z ) e. CC /\ x e. RR ) ) -> ( ( ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) /\ ( abs ` ( ( g ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) -> ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
48 44 31 34 46 47 syl22anc
 |-  ( ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( ( ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) /\ ( abs ` ( ( g ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) -> ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
49 37 48 sylan2d
 |-  ( ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( ( ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) /\ ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) ) -> ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
50 49 ancomsd
 |-  ( ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( ( ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) /\ ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) ) -> ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
51 50 ralimdva
 |-  ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( A. z e. S ( ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) /\ ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) ) -> A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
52 26 51 syl5bir
 |-  ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) /\ A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) ) -> A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
53 52 expdimp
 |-  ( ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) ) -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) -> A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
54 53 an32s
 |-  ( ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) ) /\ k e. ( ZZ>= ` j ) ) -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) -> A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
55 54 ralimdva
 |-  ( ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) /\ A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) ) -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) -> A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
56 55 ex
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) -> ( A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) -> A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) ) )
57 56 com23
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) -> ( A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) -> A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) ) )
58 25 57 mpdd
 |-  ( ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) -> A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
59 58 reximdva
 |-  ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( g ` z ) ) ) < ( x / 2 ) -> E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
60 14 59 mpd
 |-  ( ( ( ph /\ F ( ~~>u ` S ) g ) /\ x e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x )
61 60 ralrimiva
 |-  ( ( ph /\ F ( ~~>u ` S ) g ) -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x )
62 61 ex
 |-  ( ph -> ( F ( ~~>u ` S ) g -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
63 62 exlimdv
 |-  ( ph -> ( E. g F ( ~~>u ` S ) g -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
64 6 63 syl5
 |-  ( ph -> ( F e. dom ( ~~>u ` S ) -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
65 ulmrel
 |-  Rel ( ~~>u ` S )
66 1 2 3 4 ulmcaulem
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
67 66 biimpa
 |-  ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x )
68 rphalfcl
 |-  ( r e. RR+ -> ( r / 2 ) e. RR+ )
69 breq2
 |-  ( x = ( r / 2 ) -> ( ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x <-> ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) ) )
70 69 ralbidv
 |-  ( x = ( r / 2 ) -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x <-> A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) ) )
71 70 2ralbidv
 |-  ( x = ( r / 2 ) -> ( A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x <-> A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) ) )
72 71 rexbidv
 |-  ( x = ( r / 2 ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x <-> E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) ) )
73 ralcom
 |-  ( A. w e. S A. m e. ( ZZ>= ` q ) ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) <-> A. m e. ( ZZ>= ` q ) A. w e. S ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) )
74 fveq2
 |-  ( q = k -> ( ZZ>= ` q ) = ( ZZ>= ` k ) )
75 fveq2
 |-  ( w = z -> ( ( F ` q ) ` w ) = ( ( F ` q ) ` z ) )
76 fveq2
 |-  ( w = z -> ( ( F ` m ) ` w ) = ( ( F ` m ) ` z ) )
77 75 76 oveq12d
 |-  ( w = z -> ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) = ( ( ( F ` q ) ` z ) - ( ( F ` m ) ` z ) ) )
78 77 fveq2d
 |-  ( w = z -> ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) = ( abs ` ( ( ( F ` q ) ` z ) - ( ( F ` m ) ` z ) ) ) )
79 78 breq1d
 |-  ( w = z -> ( ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) <-> ( abs ` ( ( ( F ` q ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) ) )
80 79 cbvralvw
 |-  ( A. w e. S ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) <-> A. z e. S ( abs ` ( ( ( F ` q ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) )
81 fveq2
 |-  ( q = k -> ( F ` q ) = ( F ` k ) )
82 81 fveq1d
 |-  ( q = k -> ( ( F ` q ) ` z ) = ( ( F ` k ) ` z ) )
83 82 fvoveq1d
 |-  ( q = k -> ( abs ` ( ( ( F ` q ) ` z ) - ( ( F ` m ) ` z ) ) ) = ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) )
84 83 breq1d
 |-  ( q = k -> ( ( abs ` ( ( ( F ` q ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) <-> ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) ) )
85 84 ralbidv
 |-  ( q = k -> ( A. z e. S ( abs ` ( ( ( F ` q ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) <-> A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) ) )
86 80 85 syl5bb
 |-  ( q = k -> ( A. w e. S ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) <-> A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) ) )
87 74 86 raleqbidv
 |-  ( q = k -> ( A. m e. ( ZZ>= ` q ) A. w e. S ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) <-> A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) ) )
88 73 87 syl5bb
 |-  ( q = k -> ( A. w e. S A. m e. ( ZZ>= ` q ) ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) <-> A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) ) )
89 88 cbvralvw
 |-  ( A. q e. ( ZZ>= ` p ) A. w e. S A. m e. ( ZZ>= ` q ) ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) <-> A. k e. ( ZZ>= ` p ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) )
90 fveq2
 |-  ( p = j -> ( ZZ>= ` p ) = ( ZZ>= ` j ) )
91 90 raleqdv
 |-  ( p = j -> ( A. k e. ( ZZ>= ` p ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) <-> A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) ) )
92 89 91 syl5bb
 |-  ( p = j -> ( A. q e. ( ZZ>= ` p ) A. w e. S A. m e. ( ZZ>= ` q ) ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) <-> A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) ) )
93 92 cbvrexvw
 |-  ( E. p e. Z A. q e. ( ZZ>= ` p ) A. w e. S A. m e. ( ZZ>= ` q ) ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( r / 2 ) )
94 72 93 bitr4di
 |-  ( x = ( r / 2 ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x <-> E. p e. Z A. q e. ( ZZ>= ` p ) A. w e. S A. m e. ( ZZ>= ` q ) ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) ) )
95 94 rspccva
 |-  ( ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x /\ ( r / 2 ) e. RR+ ) -> E. p e. Z A. q e. ( ZZ>= ` p ) A. w e. S A. m e. ( ZZ>= ` q ) ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) )
96 67 68 95 syl2an
 |-  ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) -> E. p e. Z A. q e. ( ZZ>= ` p ) A. w e. S A. m e. ( ZZ>= ` q ) ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) )
97 1 uztrn2
 |-  ( ( p e. Z /\ q e. ( ZZ>= ` p ) ) -> q e. Z )
98 eqid
 |-  ( ZZ>= ` q ) = ( ZZ>= ` q )
99 eluzelz
 |-  ( q e. ( ZZ>= ` M ) -> q e. ZZ )
100 99 1 eleq2s
 |-  ( q e. Z -> q e. ZZ )
101 100 ad2antlr
 |-  ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) -> q e. ZZ )
102 68 adantl
 |-  ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) -> ( r / 2 ) e. RR+ )
103 102 ad2antrr
 |-  ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) -> ( r / 2 ) e. RR+ )
104 simplr
 |-  ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) -> q e. Z )
105 1 uztrn2
 |-  ( ( q e. Z /\ m e. ( ZZ>= ` q ) ) -> m e. Z )
106 104 105 sylan
 |-  ( ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) /\ m e. ( ZZ>= ` q ) ) -> m e. Z )
107 fveq2
 |-  ( n = m -> ( F ` n ) = ( F ` m ) )
108 107 fveq1d
 |-  ( n = m -> ( ( F ` n ) ` w ) = ( ( F ` m ) ` w ) )
109 eqid
 |-  ( n e. Z |-> ( ( F ` n ) ` w ) ) = ( n e. Z |-> ( ( F ` n ) ` w ) )
110 fvex
 |-  ( ( F ` m ) ` w ) e. _V
111 108 109 110 fvmpt
 |-  ( m e. Z -> ( ( n e. Z |-> ( ( F ` n ) ` w ) ) ` m ) = ( ( F ` m ) ` w ) )
112 106 111 syl
 |-  ( ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) /\ m e. ( ZZ>= ` q ) ) -> ( ( n e. Z |-> ( ( F ` n ) ` w ) ) ` m ) = ( ( F ` m ) ` w ) )
113 4 adantr
 |-  ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) -> F : Z --> ( CC ^m S ) )
114 113 ffvelrnda
 |-  ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ n e. Z ) -> ( F ` n ) e. ( CC ^m S ) )
115 elmapi
 |-  ( ( F ` n ) e. ( CC ^m S ) -> ( F ` n ) : S --> CC )
116 114 115 syl
 |-  ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ n e. Z ) -> ( F ` n ) : S --> CC )
117 116 ffvelrnda
 |-  ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ n e. Z ) /\ y e. S ) -> ( ( F ` n ) ` y ) e. CC )
118 117 an32s
 |-  ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ y e. S ) /\ n e. Z ) -> ( ( F ` n ) ` y ) e. CC )
119 118 fmpttd
 |-  ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ y e. S ) -> ( n e. Z |-> ( ( F ` n ) ` y ) ) : Z --> CC )
120 119 ffvelrnda
 |-  ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ y e. S ) /\ q e. Z ) -> ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` q ) e. CC )
121 fveq2
 |-  ( z = y -> ( ( F ` k ) ` z ) = ( ( F ` k ) ` y ) )
122 fveq2
 |-  ( z = y -> ( ( F ` j ) ` z ) = ( ( F ` j ) ` y ) )
123 121 122 oveq12d
 |-  ( z = y -> ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) = ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) )
124 123 fveq2d
 |-  ( z = y -> ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) = ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) )
125 124 breq1d
 |-  ( z = y -> ( ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x <-> ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < x ) )
126 125 rspcv
 |-  ( y e. S -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x -> ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < x ) )
127 126 ralimdv
 |-  ( y e. S -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < x ) )
128 127 reximdv
 |-  ( y e. S -> ( E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < x ) )
129 128 ralimdv
 |-  ( y e. S -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < x ) )
130 129 impcom
 |-  ( ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x /\ y e. S ) -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < x )
131 130 adantll
 |-  ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ y e. S ) -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < x )
132 fveq2
 |-  ( q = k -> ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` q ) = ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) )
133 132 fvoveq1d
 |-  ( q = k -> ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` q ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` p ) ) ) = ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` p ) ) ) )
134 133 breq1d
 |-  ( q = k -> ( ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` q ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` p ) ) ) < r <-> ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` p ) ) ) < r ) )
135 134 cbvralvw
 |-  ( A. q e. ( ZZ>= ` p ) ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` q ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` p ) ) ) < r <-> A. k e. ( ZZ>= ` p ) ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` p ) ) ) < r )
136 fveq2
 |-  ( p = j -> ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` p ) = ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` j ) )
137 136 oveq2d
 |-  ( p = j -> ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` p ) ) = ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` j ) ) )
138 137 fveq2d
 |-  ( p = j -> ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` p ) ) ) = ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` j ) ) ) )
139 138 breq1d
 |-  ( p = j -> ( ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` p ) ) ) < r <-> ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` j ) ) ) < r ) )
140 90 139 raleqbidv
 |-  ( p = j -> ( A. k e. ( ZZ>= ` p ) ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` p ) ) ) < r <-> A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` j ) ) ) < r ) )
141 135 140 syl5bb
 |-  ( p = j -> ( A. q e. ( ZZ>= ` p ) ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` q ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` p ) ) ) < r <-> A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` j ) ) ) < r ) )
142 141 cbvrexvw
 |-  ( E. p e. Z A. q e. ( ZZ>= ` p ) ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` q ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` p ) ) ) < r <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` j ) ) ) < r )
143 fveq2
 |-  ( n = k -> ( F ` n ) = ( F ` k ) )
144 143 fveq1d
 |-  ( n = k -> ( ( F ` n ) ` y ) = ( ( F ` k ) ` y ) )
145 eqid
 |-  ( n e. Z |-> ( ( F ` n ) ` y ) ) = ( n e. Z |-> ( ( F ` n ) ` y ) )
146 fvex
 |-  ( ( F ` k ) ` y ) e. _V
147 144 145 146 fvmpt
 |-  ( k e. Z -> ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) = ( ( F ` k ) ` y ) )
148 38 147 syl
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) = ( ( F ` k ) ` y ) )
149 fveq2
 |-  ( n = j -> ( F ` n ) = ( F ` j ) )
150 149 fveq1d
 |-  ( n = j -> ( ( F ` n ) ` y ) = ( ( F ` j ) ` y ) )
151 fvex
 |-  ( ( F ` j ) ` y ) e. _V
152 150 145 151 fvmpt
 |-  ( j e. Z -> ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` j ) = ( ( F ` j ) ` y ) )
153 152 adantr
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` j ) = ( ( F ` j ) ` y ) )
154 148 153 oveq12d
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` j ) ) = ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) )
155 154 fveq2d
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` j ) ) ) = ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) )
156 155 breq1d
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> ( ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` j ) ) ) < r <-> ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < r ) )
157 156 ralbidva
 |-  ( j e. Z -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` j ) ) ) < r <-> A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < r ) )
158 157 rexbiia
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` k ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` j ) ) ) < r <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < r )
159 142 158 bitri
 |-  ( E. p e. Z A. q e. ( ZZ>= ` p ) ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` q ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` p ) ) ) < r <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < r )
160 breq2
 |-  ( r = x -> ( ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < r <-> ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < x ) )
161 160 ralbidv
 |-  ( r = x -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < r <-> A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < x ) )
162 161 rexbidv
 |-  ( r = x -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < r <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < x ) )
163 159 162 syl5bb
 |-  ( r = x -> ( E. p e. Z A. q e. ( ZZ>= ` p ) ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` q ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` p ) ) ) < r <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < x ) )
164 163 cbvralvw
 |-  ( A. r e. RR+ E. p e. Z A. q e. ( ZZ>= ` p ) ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` q ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` p ) ) ) < r <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` y ) - ( ( F ` j ) ` y ) ) ) < x )
165 131 164 sylibr
 |-  ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ y e. S ) -> A. r e. RR+ E. p e. Z A. q e. ( ZZ>= ` p ) ( abs ` ( ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` q ) - ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ` p ) ) ) < r )
166 1 fvexi
 |-  Z e. _V
167 166 mptex
 |-  ( n e. Z |-> ( ( F ` n ) ` y ) ) e. _V
168 167 a1i
 |-  ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ y e. S ) -> ( n e. Z |-> ( ( F ` n ) ` y ) ) e. _V )
169 1 120 165 168 caucvg
 |-  ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ y e. S ) -> ( n e. Z |-> ( ( F ` n ) ` y ) ) e. dom ~~> )
170 169 ralrimiva
 |-  ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) -> A. y e. S ( n e. Z |-> ( ( F ` n ) ` y ) ) e. dom ~~> )
171 170 ad2antrr
 |-  ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) -> A. y e. S ( n e. Z |-> ( ( F ` n ) ` y ) ) e. dom ~~> )
172 fveq2
 |-  ( y = w -> ( ( F ` n ) ` y ) = ( ( F ` n ) ` w ) )
173 172 mpteq2dv
 |-  ( y = w -> ( n e. Z |-> ( ( F ` n ) ` y ) ) = ( n e. Z |-> ( ( F ` n ) ` w ) ) )
174 173 eleq1d
 |-  ( y = w -> ( ( n e. Z |-> ( ( F ` n ) ` y ) ) e. dom ~~> <-> ( n e. Z |-> ( ( F ` n ) ` w ) ) e. dom ~~> ) )
175 174 rspccva
 |-  ( ( A. y e. S ( n e. Z |-> ( ( F ` n ) ` y ) ) e. dom ~~> /\ w e. S ) -> ( n e. Z |-> ( ( F ` n ) ` w ) ) e. dom ~~> )
176 171 175 sylan
 |-  ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) -> ( n e. Z |-> ( ( F ` n ) ` w ) ) e. dom ~~> )
177 climdm
 |-  ( ( n e. Z |-> ( ( F ` n ) ` w ) ) e. dom ~~> <-> ( n e. Z |-> ( ( F ` n ) ` w ) ) ~~> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) )
178 176 177 sylib
 |-  ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) -> ( n e. Z |-> ( ( F ` n ) ` w ) ) ~~> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) )
179 98 101 103 112 178 climi2
 |-  ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) -> E. v e. ( ZZ>= ` q ) A. m e. ( ZZ>= ` v ) ( abs ` ( ( ( F ` m ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < ( r / 2 ) )
180 98 r19.29uz
 |-  ( ( A. m e. ( ZZ>= ` q ) ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) /\ E. v e. ( ZZ>= ` q ) A. m e. ( ZZ>= ` v ) ( abs ` ( ( ( F ` m ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < ( r / 2 ) ) -> E. v e. ( ZZ>= ` q ) A. m e. ( ZZ>= ` v ) ( ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) /\ ( abs ` ( ( ( F ` m ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < ( r / 2 ) ) )
181 98 r19.2uz
 |-  ( E. v e. ( ZZ>= ` q ) A. m e. ( ZZ>= ` v ) ( ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) /\ ( abs ` ( ( ( F ` m ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < ( r / 2 ) ) -> E. m e. ( ZZ>= ` q ) ( ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) /\ ( abs ` ( ( ( F ` m ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < ( r / 2 ) ) )
182 180 181 syl
 |-  ( ( A. m e. ( ZZ>= ` q ) ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) /\ E. v e. ( ZZ>= ` q ) A. m e. ( ZZ>= ` v ) ( abs ` ( ( ( F ` m ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < ( r / 2 ) ) -> E. m e. ( ZZ>= ` q ) ( ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) /\ ( abs ` ( ( ( F ` m ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < ( r / 2 ) ) )
183 4 ad2antrr
 |-  ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) -> F : Z --> ( CC ^m S ) )
184 183 ffvelrnda
 |-  ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) -> ( F ` q ) e. ( CC ^m S ) )
185 elmapi
 |-  ( ( F ` q ) e. ( CC ^m S ) -> ( F ` q ) : S --> CC )
186 184 185 syl
 |-  ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) -> ( F ` q ) : S --> CC )
187 186 ffvelrnda
 |-  ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) -> ( ( F ` q ) ` w ) e. CC )
188 187 adantr
 |-  ( ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) /\ m e. ( ZZ>= ` q ) ) -> ( ( F ` q ) ` w ) e. CC )
189 climcl
 |-  ( ( n e. Z |-> ( ( F ` n ) ` w ) ) ~~> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) -> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) e. CC )
190 178 189 syl
 |-  ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) -> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) e. CC )
191 190 adantr
 |-  ( ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) /\ m e. ( ZZ>= ` q ) ) -> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) e. CC )
192 4 ad5antr
 |-  ( ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) /\ m e. ( ZZ>= ` q ) ) -> F : Z --> ( CC ^m S ) )
193 192 106 ffvelrnd
 |-  ( ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) /\ m e. ( ZZ>= ` q ) ) -> ( F ` m ) e. ( CC ^m S ) )
194 elmapi
 |-  ( ( F ` m ) e. ( CC ^m S ) -> ( F ` m ) : S --> CC )
195 193 194 syl
 |-  ( ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) /\ m e. ( ZZ>= ` q ) ) -> ( F ` m ) : S --> CC )
196 simplr
 |-  ( ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) /\ m e. ( ZZ>= ` q ) ) -> w e. S )
197 195 196 ffvelrnd
 |-  ( ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) /\ m e. ( ZZ>= ` q ) ) -> ( ( F ` m ) ` w ) e. CC )
198 rpre
 |-  ( r e. RR+ -> r e. RR )
199 198 ad4antlr
 |-  ( ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) /\ m e. ( ZZ>= ` q ) ) -> r e. RR )
200 abs3lem
 |-  ( ( ( ( ( F ` q ) ` w ) e. CC /\ ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) e. CC ) /\ ( ( ( F ` m ) ` w ) e. CC /\ r e. RR ) ) -> ( ( ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) /\ ( abs ` ( ( ( F ` m ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < ( r / 2 ) ) -> ( abs ` ( ( ( F ` q ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < r ) )
201 188 191 197 199 200 syl22anc
 |-  ( ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) /\ m e. ( ZZ>= ` q ) ) -> ( ( ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) /\ ( abs ` ( ( ( F ` m ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < ( r / 2 ) ) -> ( abs ` ( ( ( F ` q ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < r ) )
202 201 rexlimdva
 |-  ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) -> ( E. m e. ( ZZ>= ` q ) ( ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) /\ ( abs ` ( ( ( F ` m ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < ( r / 2 ) ) -> ( abs ` ( ( ( F ` q ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < r ) )
203 182 202 syl5
 |-  ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) -> ( ( A. m e. ( ZZ>= ` q ) ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) /\ E. v e. ( ZZ>= ` q ) A. m e. ( ZZ>= ` v ) ( abs ` ( ( ( F ` m ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < ( r / 2 ) ) -> ( abs ` ( ( ( F ` q ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < r ) )
204 179 203 mpan2d
 |-  ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) /\ w e. S ) -> ( A. m e. ( ZZ>= ` q ) ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) -> ( abs ` ( ( ( F ` q ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < r ) )
205 204 ralimdva
 |-  ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ q e. Z ) -> ( A. w e. S A. m e. ( ZZ>= ` q ) ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) -> A. w e. S ( abs ` ( ( ( F ` q ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < r ) )
206 97 205 sylan2
 |-  ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ ( p e. Z /\ q e. ( ZZ>= ` p ) ) ) -> ( A. w e. S A. m e. ( ZZ>= ` q ) ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) -> A. w e. S ( abs ` ( ( ( F ` q ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < r ) )
207 206 anassrs
 |-  ( ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ p e. Z ) /\ q e. ( ZZ>= ` p ) ) -> ( A. w e. S A. m e. ( ZZ>= ` q ) ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) -> A. w e. S ( abs ` ( ( ( F ` q ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < r ) )
208 207 ralimdva
 |-  ( ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) /\ p e. Z ) -> ( A. q e. ( ZZ>= ` p ) A. w e. S A. m e. ( ZZ>= ` q ) ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) -> A. q e. ( ZZ>= ` p ) A. w e. S ( abs ` ( ( ( F ` q ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < r ) )
209 208 reximdva
 |-  ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) -> ( E. p e. Z A. q e. ( ZZ>= ` p ) A. w e. S A. m e. ( ZZ>= ` q ) ( abs ` ( ( ( F ` q ) ` w ) - ( ( F ` m ) ` w ) ) ) < ( r / 2 ) -> E. p e. Z A. q e. ( ZZ>= ` p ) A. w e. S ( abs ` ( ( ( F ` q ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < r ) )
210 96 209 mpd
 |-  ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ r e. RR+ ) -> E. p e. Z A. q e. ( ZZ>= ` p ) A. w e. S ( abs ` ( ( ( F ` q ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < r )
211 210 ralrimiva
 |-  ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) -> A. r e. RR+ E. p e. Z A. q e. ( ZZ>= ` p ) A. w e. S ( abs ` ( ( ( F ` q ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < r )
212 2 adantr
 |-  ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) -> M e. ZZ )
213 eqidd
 |-  ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ ( q e. Z /\ w e. S ) ) -> ( ( F ` q ) ` w ) = ( ( F ` q ) ` w ) )
214 173 fveq2d
 |-  ( y = w -> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` y ) ) ) = ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) )
215 eqid
 |-  ( y e. S |-> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` y ) ) ) ) = ( y e. S |-> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` y ) ) ) )
216 fvex
 |-  ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) e. _V
217 214 215 216 fvmpt
 |-  ( w e. S -> ( ( y e. S |-> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` y ) ) ) ) ` w ) = ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) )
218 217 adantl
 |-  ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ w e. S ) -> ( ( y e. S |-> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` y ) ) ) ) ` w ) = ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) )
219 climdm
 |-  ( ( n e. Z |-> ( ( F ` n ) ` y ) ) e. dom ~~> <-> ( n e. Z |-> ( ( F ` n ) ` y ) ) ~~> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` y ) ) ) )
220 169 219 sylib
 |-  ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ y e. S ) -> ( n e. Z |-> ( ( F ` n ) ` y ) ) ~~> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` y ) ) ) )
221 climcl
 |-  ( ( n e. Z |-> ( ( F ` n ) ` y ) ) ~~> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` y ) ) ) -> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` y ) ) ) e. CC )
222 220 221 syl
 |-  ( ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) /\ y e. S ) -> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` y ) ) ) e. CC )
223 222 fmpttd
 |-  ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) -> ( y e. S |-> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` y ) ) ) ) : S --> CC )
224 3 adantr
 |-  ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) -> S e. V )
225 1 212 113 213 218 223 224 ulm2
 |-  ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) -> ( F ( ~~>u ` S ) ( y e. S |-> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` y ) ) ) ) <-> A. r e. RR+ E. p e. Z A. q e. ( ZZ>= ` p ) A. w e. S ( abs ` ( ( ( F ` q ) ` w ) - ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` w ) ) ) ) ) < r ) )
226 211 225 mpbird
 |-  ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) -> F ( ~~>u ` S ) ( y e. S |-> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` y ) ) ) ) )
227 releldm
 |-  ( ( Rel ( ~~>u ` S ) /\ F ( ~~>u ` S ) ( y e. S |-> ( ~~> ` ( n e. Z |-> ( ( F ` n ) ` y ) ) ) ) ) -> F e. dom ( ~~>u ` S ) )
228 65 226 227 sylancr
 |-  ( ( ph /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) -> F e. dom ( ~~>u ` S ) )
229 228 ex
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x -> F e. dom ( ~~>u ` S ) ) )
230 64 229 impbid
 |-  ( ph -> ( F e. dom ( ~~>u ` S ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )