Metamath Proof Explorer

Theorem ulmcaulem

Description: Lemma for ulmcau and ulmcau2 : show the equivalence of the four- and five-quantifier forms of the Cauchy convergence condition. Compare cau3 . (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 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 ) )

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 breq2 
 |-  ( x = w -> ( ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x <-> ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < w ) )
6 5 ralbidv 
 |-  ( x = w -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x <-> A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < w ) )
7 6 rexralbidv 
 |-  ( x = w -> ( 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 ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < w ) )
8 7 cbvralvw 
 |-  ( 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. w e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < w )
9 rphalfcl 
 |-  ( x e. RR+ -> ( x / 2 ) e. RR+ )
10 breq2 
 |-  ( w = ( x / 2 ) -> ( ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < w <-> ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) )
11 10 ralbidv 
 |-  ( w = ( x / 2 ) -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < w <-> A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) )
12 11 rexralbidv 
 |-  ( w = ( x / 2 ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < w <-> E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) )
13 12 rspcv 
 |-  ( ( x / 2 ) e. RR+ -> ( A. w e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < w -> E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) )
14 9 13 syl 
 |-  ( x e. RR+ -> ( A. w e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < w -> E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) )
15 14 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( A. w e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < w -> E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) )
16 fveq2 
 |-  ( k = m -> ( F ` k ) = ( F ` m ) )
17 16 fveq1d 
 |-  ( k = m -> ( ( F ` k ) ` z ) = ( ( F ` m ) ` z ) )
18 17 fvoveq1d 
 |-  ( k = m -> ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) = ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) )
19 18 breq1d 
 |-  ( k = m -> ( ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) <-> ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) )
20 19 ralbidv 
 |-  ( k = m -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) <-> A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) )
21 20 cbvralvw 
 |-  ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) <-> A. m e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) )
22 21 biimpi 
 |-  ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) -> A. m e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) )
23 uzss 
 |-  ( k e. ( ZZ>= ` j ) -> ( ZZ>= ` k ) C_ ( ZZ>= ` j ) )
24 23 ad2antlr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) -> ( ZZ>= ` k ) C_ ( ZZ>= ` j ) )
25 ssralv 
 |-  ( ( ZZ>= ` k ) C_ ( ZZ>= ` j ) -> ( A. m e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) -> A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) )
26 24 25 syl 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) -> ( A. m e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) -> A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) )
27 r19.26 
 |-  ( A. z e. S ( ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) /\ ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) <-> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) /\ A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) )
28 4 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> F : Z --> ( CC ^m S ) )
29 28 ad3antrrr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) -> F : Z --> ( CC ^m S ) )
30 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
31 30 adantll 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
32 1 uztrn2 
 |-  ( ( k e. Z /\ m e. ( ZZ>= ` k ) ) -> m e. Z )
33 31 32 sylan 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) -> m e. Z )
34 29 33 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) -> ( F ` m ) e. ( CC ^m S ) )
35 elmapi 
 |-  ( ( F ` m ) e. ( CC ^m S ) -> ( F ` m ) : S --> CC )
36 34 35 syl 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) -> ( F ` m ) : S --> CC )
37 36 ffvelcdmda 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) /\ z e. S ) -> ( ( F ` m ) ` z ) e. CC )
38 28 ffvelcdmda 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) -> ( F ` j ) e. ( CC ^m S ) )
39 38 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) -> ( F ` j ) e. ( CC ^m S ) )
40 elmapi 
 |-  ( ( F ` j ) e. ( CC ^m S ) -> ( F ` j ) : S --> CC )
41 39 40 syl 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) -> ( F ` j ) : S --> CC )
42 41 ffvelcdmda 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) /\ z e. S ) -> ( ( F ` j ) ` z ) e. CC )
43 37 42 abssubd 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) /\ z e. S ) -> ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) = ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` m ) ` z ) ) ) )
44 43 breq1d 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) /\ z e. S ) -> ( ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) <-> ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( x / 2 ) ) )
45 44 biimpd 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) /\ z e. S ) -> ( ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) -> ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( x / 2 ) ) )
46 ffvelcdm 
 |-  ( ( F : Z --> ( CC ^m S ) /\ k e. Z ) -> ( F ` k ) e. ( CC ^m S ) )
47 28 30 46 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( F ` k ) e. ( CC ^m S ) )
48 47 anassrs 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. ( CC ^m S ) )
49 48 adantr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) -> ( F ` k ) e. ( CC ^m S ) )
50 elmapi 
 |-  ( ( F ` k ) e. ( CC ^m S ) -> ( F ` k ) : S --> CC )
51 49 50 syl 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) -> ( F ` k ) : S --> CC )
52 51 ffvelcdmda 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) /\ z e. S ) -> ( ( F ` k ) ` z ) e. CC )
53 rpre 
 |-  ( x e. RR+ -> x e. RR )
54 53 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) -> x e. RR )
55 54 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) /\ z e. S ) -> x e. RR )
56 abs3lem 
 |-  ( ( ( ( ( F ` k ) ` z ) e. CC /\ ( ( F ` m ) ` z ) e. CC ) /\ ( ( ( F ` j ) ` z ) e. CC /\ x e. RR ) ) -> ( ( ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) /\ ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( x / 2 ) ) -> ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
57 52 37 42 55 56 syl22anc 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) /\ z e. S ) -> ( ( ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) /\ ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` m ) ` z ) ) ) < ( x / 2 ) ) -> ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
58 45 57 sylan2d 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) /\ z e. S ) -> ( ( ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) /\ ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) -> ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
59 58 ralimdva 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) -> ( A. z e. S ( ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) /\ ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) -> A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
60 27 59 biimtrrid 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) -> ( ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) /\ A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) -> A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
61 60 expdimp 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ m e. ( ZZ>= ` k ) ) /\ A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) -> ( A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) -> A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
62 61 an32s 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) /\ m e. ( ZZ>= ` k ) ) -> ( A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) -> A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
63 62 ralimdva 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) -> ( A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) -> A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
64 26 63 syld 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) -> ( A. m e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) -> A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
65 64 impancom 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ A. m e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) -> A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
66 65 an32s 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ A. m e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) /\ k e. ( ZZ>= ` j ) ) -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) -> A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
67 66 ralimdva 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) /\ A. m e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) ) -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) -> A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
68 67 ex 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) -> ( A. m e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) -> A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) ) )
69 68 com23 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) -> ( A. m e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` m ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) -> A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) ) )
70 22 69 mpdi 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 2 ) -> A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
71 70 reximdva 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < ( x / 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 ) )
72 15 71 syld 
 |-  ( ( ph /\ x e. RR+ ) -> ( A. w e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < w -> 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 ) )
73 72 ralrimdva 
 |-  ( ph -> ( A. w e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < w -> 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 ) )
74 8 73 biimtrid 
 |-  ( 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 ) )
75 eluzelz 
 |-  ( j e. ( ZZ>= ` M ) -> j e. ZZ )
76 75 1 eleq2s 
 |-  ( j e. Z -> j e. ZZ )
77 uzid 
 |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )
78 76 77 syl 
 |-  ( j e. Z -> j e. ( ZZ>= ` j ) )
79 78 adantl 
 |-  ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` j ) )
80 fveq2 
 |-  ( k = j -> ( ZZ>= ` k ) = ( ZZ>= ` j ) )
81 fveq2 
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
82 81 fveq1d 
 |-  ( k = j -> ( ( F ` k ) ` z ) = ( ( F ` j ) ` z ) )
83 82 fvoveq1d 
 |-  ( k = j -> ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) = ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` m ) ` z ) ) ) )
84 83 breq1d 
 |-  ( k = j -> ( ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x <-> ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
85 84 ralbidv 
 |-  ( k = j -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x <-> A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
86 80 85 raleqbidv 
 |-  ( k = j -> ( A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x <-> A. m e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
87 86 rspcv 
 |-  ( j e. ( ZZ>= ` j ) -> ( A. k e. ( ZZ>= ` j ) A. m e. ( ZZ>= ` k ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` m ) ` z ) ) ) < x -> A. m e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
88 79 87 syl 
 |-  ( ( ph /\ 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 -> A. m e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` m ) ` z ) ) ) < x ) )
89 fveq2 
 |-  ( m = k -> ( F ` m ) = ( F ` k ) )
90 89 fveq1d 
 |-  ( m = k -> ( ( F ` m ) ` z ) = ( ( F ` k ) ` z ) )
91 90 oveq2d 
 |-  ( m = k -> ( ( ( F ` j ) ` z ) - ( ( F ` m ) ` z ) ) = ( ( ( F ` j ) ` z ) - ( ( F ` k ) ` z ) ) )
92 91 fveq2d 
 |-  ( m = k -> ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` m ) ` z ) ) ) = ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` k ) ` z ) ) ) )
93 92 breq1d 
 |-  ( m = k -> ( ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` m ) ` z ) ) ) < x <-> ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` k ) ` z ) ) ) < x ) )
94 93 ralbidv 
 |-  ( m = k -> ( A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` m ) ` z ) ) ) < x <-> A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` k ) ` z ) ) ) < x ) )
95 94 cbvralvw 
 |-  ( A. m e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` m ) ` z ) ) ) < x <-> A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` k ) ` z ) ) ) < x )
96 4 ffvelcdmda 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) e. ( CC ^m S ) )
97 96 adantr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` j ) e. ( CC ^m S ) )
98 97 40 syl 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` j ) : S --> CC )
99 98 ffvelcdmda 
 |-  ( ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( ( F ` j ) ` z ) e. CC )
100 4 30 46 syl2an 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( F ` k ) e. ( CC ^m S ) )
101 100 anassrs 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. ( CC ^m S ) )
102 101 50 syl 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) : S --> CC )
103 102 ffvelcdmda 
 |-  ( ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( ( F ` k ) ` z ) e. CC )
104 99 103 abssubd 
 |-  ( ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` k ) ` z ) ) ) = ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) )
105 104 breq1d 
 |-  ( ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ z e. S ) -> ( ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` k ) ` z ) ) ) < x <-> ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
106 105 ralbidva 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` k ) ` z ) ) ) < x <-> A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
107 106 ralbidva 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` k ) ` z ) ) ) < x <-> A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
108 95 107 bitrid 
 |-  ( ( ph /\ j e. Z ) -> ( A. m e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` j ) ` z ) - ( ( F ` m ) ` z ) ) ) < x <-> A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
109 88 108 sylibd 
 |-  ( ( ph /\ 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 -> A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
110 109 reximdva 
 |-  ( ph -> ( 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. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( ( F ` j ) ` z ) ) ) < x ) )
111 110 ralimdv 
 |-  ( ph -> ( 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 -> 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 ) )
112 74 111 impbid 
 |-  ( 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 ) )