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 ) )