Metamath Proof Explorer

Theorem mtest

Description: The Weierstrass M-test. If F is a sequence of functions which are uniformly bounded by the convergent sequence M ( k ) , then the series generated by the sequence F converges uniformly. (Contributed by Mario Carneiro, 3-Mar-2015)

Ref Expression
Hypotheses mtest.z 
|- Z = ( ZZ>= ` N )
mtest.n 
|- ( ph -> N e. ZZ )
mtest.s 
|- ( ph -> S e. V )
mtest.f 
|- ( ph -> F : Z --> ( CC ^m S ) )
mtest.m 
|- ( ph -> M e. W )
mtest.c 
|- ( ( ph /\ k e. Z ) -> ( M ` k ) e. RR )
mtest.l 
|- ( ( ph /\ ( k e. Z /\ z e. S ) ) -> ( abs ` ( ( F ` k ) ` z ) ) <_ ( M ` k ) )
mtest.d 
|- ( ph -> seq N ( + , M ) e. dom ~~> )
Assertion mtest 
|- ( ph -> seq N ( oF + , F ) e. dom ( ~~>u ` S ) )

Proof

Step Hyp Ref Expression
1 mtest.z 
 |-  Z = ( ZZ>= ` N )
2 mtest.n 
 |-  ( ph -> N e. ZZ )
3 mtest.s 
 |-  ( ph -> S e. V )
4 mtest.f 
 |-  ( ph -> F : Z --> ( CC ^m S ) )
5 mtest.m 
 |-  ( ph -> M e. W )
6 mtest.c 
 |-  ( ( ph /\ k e. Z ) -> ( M ` k ) e. RR )
7 mtest.l 
 |-  ( ( ph /\ ( k e. Z /\ z e. S ) ) -> ( abs ` ( ( F ` k ) ` z ) ) <_ ( M ` k ) )
8 mtest.d 
 |-  ( ph -> seq N ( + , M ) e. dom ~~> )
9 1 climcau 
 |-  ( ( N e. ZZ /\ seq N ( + , M ) e. dom ~~> ) -> A. r e. RR+ E. j e. Z A. i e. ( ZZ>= ` j ) ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) < r )
10 2 8 9 syl2anc 
 |-  ( ph -> A. r e. RR+ E. j e. Z A. i e. ( ZZ>= ` j ) ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) < r )
11 seqfn 
 |-  ( N e. ZZ -> seq N ( oF + , F ) Fn ( ZZ>= ` N ) )
12 2 11 syl 
 |-  ( ph -> seq N ( oF + , F ) Fn ( ZZ>= ` N ) )
13 1 fneq2i 
 |-  ( seq N ( oF + , F ) Fn Z <-> seq N ( oF + , F ) Fn ( ZZ>= ` N ) )
14 12 13 sylibr 
 |-  ( ph -> seq N ( oF + , F ) Fn Z )
15 3 elexd 
 |-  ( ph -> S e. _V )
16 15 adantr 
 |-  ( ( ph /\ i e. Z ) -> S e. _V )
17 simpr 
 |-  ( ( ph /\ i e. Z ) -> i e. Z )
18 17 1 eleqtrdi 
 |-  ( ( ph /\ i e. Z ) -> i e. ( ZZ>= ` N ) )
19 4 adantr 
 |-  ( ( ph /\ i e. Z ) -> F : Z --> ( CC ^m S ) )
20 elfzuz 
 |-  ( k e. ( N ... i ) -> k e. ( ZZ>= ` N ) )
21 20 1 eleqtrrdi 
 |-  ( k e. ( N ... i ) -> k e. Z )
22 ffvelrn 
 |-  ( ( F : Z --> ( CC ^m S ) /\ k e. Z ) -> ( F ` k ) e. ( CC ^m S ) )
23 19 21 22 syl2an 
 |-  ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> ( F ` k ) e. ( CC ^m S ) )
24 elmapi 
 |-  ( ( F ` k ) e. ( CC ^m S ) -> ( F ` k ) : S --> CC )
25 23 24 syl 
 |-  ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> ( F ` k ) : S --> CC )
26 25 feqmptd 
 |-  ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> ( F ` k ) = ( z e. S |-> ( ( F ` k ) ` z ) ) )
27 21 adantl 
 |-  ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> k e. Z )
28 fveq2 
 |-  ( n = k -> ( F ` n ) = ( F ` k ) )
29 28 fveq1d 
 |-  ( n = k -> ( ( F ` n ) ` z ) = ( ( F ` k ) ` z ) )
30 eqid 
 |-  ( n e. Z |-> ( ( F ` n ) ` z ) ) = ( n e. Z |-> ( ( F ` n ) ` z ) )
31 fvex 
 |-  ( ( F ` k ) ` z ) e. _V
32 29 30 31 fvmpt 
 |-  ( k e. Z -> ( ( n e. Z |-> ( ( F ` n ) ` z ) ) ` k ) = ( ( F ` k ) ` z ) )
33 27 32 syl 
 |-  ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> ( ( n e. Z |-> ( ( F ` n ) ` z ) ) ` k ) = ( ( F ` k ) ` z ) )
34 33 mpteq2dv 
 |-  ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> ( z e. S |-> ( ( n e. Z |-> ( ( F ` n ) ` z ) ) ` k ) ) = ( z e. S |-> ( ( F ` k ) ` z ) ) )
35 26 34 eqtr4d 
 |-  ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> ( F ` k ) = ( z e. S |-> ( ( n e. Z |-> ( ( F ` n ) ` z ) ) ` k ) ) )
36 16 18 35 seqof 
 |-  ( ( ph /\ i e. Z ) -> ( seq N ( oF + , F ) ` i ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) )
37 2 adantr 
 |-  ( ( ph /\ z e. S ) -> N e. ZZ )
38 4 ffvelrnda 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. ( CC ^m S ) )
39 elmapi 
 |-  ( ( F ` n ) e. ( CC ^m S ) -> ( F ` n ) : S --> CC )
40 38 39 syl 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) : S --> CC )
41 40 ffvelrnda 
 |-  ( ( ( ph /\ n e. Z ) /\ z e. S ) -> ( ( F ` n ) ` z ) e. CC )
42 41 an32s 
 |-  ( ( ( ph /\ z e. S ) /\ n e. Z ) -> ( ( F ` n ) ` z ) e. CC )
43 42 fmpttd 
 |-  ( ( ph /\ z e. S ) -> ( n e. Z |-> ( ( F ` n ) ` z ) ) : Z --> CC )
44 43 ffvelrnda 
 |-  ( ( ( ph /\ z e. S ) /\ i e. Z ) -> ( ( n e. Z |-> ( ( F ` n ) ` z ) ) ` i ) e. CC )
45 1 37 44 serf 
 |-  ( ( ph /\ z e. S ) -> seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) : Z --> CC )
46 45 ffvelrnda 
 |-  ( ( ( ph /\ z e. S ) /\ i e. Z ) -> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) e. CC )
47 46 an32s 
 |-  ( ( ( ph /\ i e. Z ) /\ z e. S ) -> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) e. CC )
48 47 fmpttd 
 |-  ( ( ph /\ i e. Z ) -> ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) : S --> CC )
49 cnex 
 |-  CC e. _V
50 elmapg 
 |-  ( ( CC e. _V /\ S e. _V ) -> ( ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) e. ( CC ^m S ) <-> ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) : S --> CC ) )
51 49 16 50 sylancr 
 |-  ( ( ph /\ i e. Z ) -> ( ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) e. ( CC ^m S ) <-> ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) : S --> CC ) )
52 48 51 mpbird 
 |-  ( ( ph /\ i e. Z ) -> ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) e. ( CC ^m S ) )
53 36 52 eqeltrd 
 |-  ( ( ph /\ i e. Z ) -> ( seq N ( oF + , F ) ` i ) e. ( CC ^m S ) )
54 53 ralrimiva 
 |-  ( ph -> A. i e. Z ( seq N ( oF + , F ) ` i ) e. ( CC ^m S ) )
55 ffnfv 
 |-  ( seq N ( oF + , F ) : Z --> ( CC ^m S ) <-> ( seq N ( oF + , F ) Fn Z /\ A. i e. Z ( seq N ( oF + , F ) ` i ) e. ( CC ^m S ) ) )
56 14 54 55 sylanbrc 
 |-  ( ph -> seq N ( oF + , F ) : Z --> ( CC ^m S ) )
57 56 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> seq N ( oF + , F ) : Z --> ( CC ^m S ) )
58 1 uztrn2 
 |-  ( ( j e. Z /\ i e. ( ZZ>= ` j ) ) -> i e. Z )
59 58 adantl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> i e. Z )
60 57 59 ffvelrnd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( oF + , F ) ` i ) e. ( CC ^m S ) )
61 elmapi 
 |-  ( ( seq N ( oF + , F ) ` i ) e. ( CC ^m S ) -> ( seq N ( oF + , F ) ` i ) : S --> CC )
62 60 61 syl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( oF + , F ) ` i ) : S --> CC )
63 62 ffvelrnda 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( seq N ( oF + , F ) ` i ) ` z ) e. CC )
64 simprl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> j e. Z )
65 57 64 ffvelrnd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( oF + , F ) ` j ) e. ( CC ^m S ) )
66 elmapi 
 |-  ( ( seq N ( oF + , F ) ` j ) e. ( CC ^m S ) -> ( seq N ( oF + , F ) ` j ) : S --> CC )
67 65 66 syl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( oF + , F ) ` j ) : S --> CC )
68 67 ffvelrnda 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( seq N ( oF + , F ) ` j ) ` z ) e. CC )
69 63 68 subcld 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) e. CC )
70 69 abscld 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( abs ` ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) ) e. RR )
71 fzfid 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( j + 1 ) ... i ) e. Fin )
72 ssun2 
 |-  ( ( j + 1 ) ... i ) C_ ( ( N ... j ) u. ( ( j + 1 ) ... i ) )
73 64 1 eleqtrdi 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> j e. ( ZZ>= ` N ) )
74 simprr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> i e. ( ZZ>= ` j ) )
75 elfzuzb 
 |-  ( j e. ( N ... i ) <-> ( j e. ( ZZ>= ` N ) /\ i e. ( ZZ>= ` j ) ) )
76 73 74 75 sylanbrc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> j e. ( N ... i ) )
77 fzsplit 
 |-  ( j e. ( N ... i ) -> ( N ... i ) = ( ( N ... j ) u. ( ( j + 1 ) ... i ) ) )
78 76 77 syl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( N ... i ) = ( ( N ... j ) u. ( ( j + 1 ) ... i ) ) )
79 72 78 sseqtrrid 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( j + 1 ) ... i ) C_ ( N ... i ) )
80 79 sselda 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( ( j + 1 ) ... i ) ) -> k e. ( N ... i ) )
81 80 adantlr 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> k e. ( N ... i ) )
82 4 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> F : Z --> ( CC ^m S ) )
83 82 21 22 syl2an 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... i ) ) -> ( F ` k ) e. ( CC ^m S ) )
84 83 24 syl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... i ) ) -> ( F ` k ) : S --> CC )
85 84 ffvelrnda 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... i ) ) /\ z e. S ) -> ( ( F ` k ) ` z ) e. CC )
86 85 an32s 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( N ... i ) ) -> ( ( F ` k ) ` z ) e. CC )
87 81 86 syldan 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> ( ( F ` k ) ` z ) e. CC )
88 87 abscld 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> ( abs ` ( ( F ` k ) ` z ) ) e. RR )
89 71 88 fsumrecl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> sum_ k e. ( ( j + 1 ) ... i ) ( abs ` ( ( F ` k ) ` z ) ) e. RR )
90 1 2 6 serfre 
 |-  ( ph -> seq N ( + , M ) : Z --> RR )
91 90 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> seq N ( + , M ) : Z --> RR )
92 91 59 ffvelrnd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( + , M ) ` i ) e. RR )
93 91 64 ffvelrnd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( + , M ) ` j ) e. RR )
94 92 93 resubcld 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) e. RR )
95 94 recnd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) e. CC )
96 95 abscld 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) e. RR )
97 96 adantr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) e. RR )
98 58 36 sylan2 
 |-  ( ( ph /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( oF + , F ) ` i ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) )
99 98 adantlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( oF + , F ) ` i ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) )
100 99 fveq1d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( seq N ( oF + , F ) ` i ) ` z ) = ( ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) ` z ) )
101 fvex 
 |-  ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) e. _V
102 eqid 
 |-  ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) )
103 102 fvmpt2 
 |-  ( ( z e. S /\ ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) e. _V ) -> ( ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) ` z ) = ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) )
104 101 103 mpan2 
 |-  ( z e. S -> ( ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) ` z ) = ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) )
105 100 104 sylan9eq 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( seq N ( oF + , F ) ` i ) ` z ) = ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) )
106 fveq2 
 |-  ( i = j -> ( seq N ( oF + , F ) ` i ) = ( seq N ( oF + , F ) ` j ) )
107 fveq2 
 |-  ( i = j -> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) = ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) )
108 107 mpteq2dv 
 |-  ( i = j -> ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) ) )
109 106 108 eqeq12d 
 |-  ( i = j -> ( ( seq N ( oF + , F ) ` i ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) <-> ( seq N ( oF + , F ) ` j ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) ) ) )
110 36 ralrimiva 
 |-  ( ph -> A. i e. Z ( seq N ( oF + , F ) ` i ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) )
111 110 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> A. i e. Z ( seq N ( oF + , F ) ` i ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) )
112 109 111 64 rspcdva 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( oF + , F ) ` j ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) ) )
113 112 fveq1d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( seq N ( oF + , F ) ` j ) ` z ) = ( ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) ) ` z ) )
114 fvex 
 |-  ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) e. _V
115 eqid 
 |-  ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) )
116 115 fvmpt2 
 |-  ( ( z e. S /\ ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) e. _V ) -> ( ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) ) ` z ) = ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) )
117 114 116 mpan2 
 |-  ( z e. S -> ( ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) ) ` z ) = ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) )
118 113 117 sylan9eq 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( seq N ( oF + , F ) ` j ) ` z ) = ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) )
119 105 118 oveq12d 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) = ( ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) - ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) ) )
120 21 adantl 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( N ... i ) ) -> k e. Z )
121 120 32 syl 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( N ... i ) ) -> ( ( n e. Z |-> ( ( F ` n ) ` z ) ) ` k ) = ( ( F ` k ) ` z ) )
122 59 adantr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> i e. Z )
123 122 1 eleqtrdi 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> i e. ( ZZ>= ` N ) )
124 121 123 86 fsumser 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> sum_ k e. ( N ... i ) ( ( F ` k ) ` z ) = ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) )
125 elfzuz 
 |-  ( k e. ( N ... j ) -> k e. ( ZZ>= ` N ) )
126 125 1 eleqtrrdi 
 |-  ( k e. ( N ... j ) -> k e. Z )
127 126 adantl 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( N ... j ) ) -> k e. Z )
128 127 32 syl 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( N ... j ) ) -> ( ( n e. Z |-> ( ( F ` n ) ` z ) ) ` k ) = ( ( F ` k ) ` z ) )
129 64 adantr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> j e. Z )
130 129 1 eleqtrdi 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> j e. ( ZZ>= ` N ) )
131 82 126 22 syl2an 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... j ) ) -> ( F ` k ) e. ( CC ^m S ) )
132 131 24 syl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... j ) ) -> ( F ` k ) : S --> CC )
133 132 ffvelrnda 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... j ) ) /\ z e. S ) -> ( ( F ` k ) ` z ) e. CC )
134 133 an32s 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( N ... j ) ) -> ( ( F ` k ) ` z ) e. CC )
135 128 130 134 fsumser 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> sum_ k e. ( N ... j ) ( ( F ` k ) ` z ) = ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) )
136 124 135 oveq12d 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( sum_ k e. ( N ... i ) ( ( F ` k ) ` z ) - sum_ k e. ( N ... j ) ( ( F ` k ) ` z ) ) = ( ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) - ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) ) )
137 fzfid 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( N ... j ) e. Fin )
138 137 134 fsumcl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> sum_ k e. ( N ... j ) ( ( F ` k ) ` z ) e. CC )
139 71 87 fsumcl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> sum_ k e. ( ( j + 1 ) ... i ) ( ( F ` k ) ` z ) e. CC )
140 eluzelre 
 |-  ( j e. ( ZZ>= ` N ) -> j e. RR )
141 73 140 syl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> j e. RR )
142 141 ltp1d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> j < ( j + 1 ) )
143 fzdisj 
 |-  ( j < ( j + 1 ) -> ( ( N ... j ) i^i ( ( j + 1 ) ... i ) ) = (/) )
144 142 143 syl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( N ... j ) i^i ( ( j + 1 ) ... i ) ) = (/) )
145 144 adantr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( N ... j ) i^i ( ( j + 1 ) ... i ) ) = (/) )
146 78 adantr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( N ... i ) = ( ( N ... j ) u. ( ( j + 1 ) ... i ) ) )
147 fzfid 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( N ... i ) e. Fin )
148 145 146 147 86 fsumsplit 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> sum_ k e. ( N ... i ) ( ( F ` k ) ` z ) = ( sum_ k e. ( N ... j ) ( ( F ` k ) ` z ) + sum_ k e. ( ( j + 1 ) ... i ) ( ( F ` k ) ` z ) ) )
149 138 139 148 mvrladdd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( sum_ k e. ( N ... i ) ( ( F ` k ) ` z ) - sum_ k e. ( N ... j ) ( ( F ` k ) ` z ) ) = sum_ k e. ( ( j + 1 ) ... i ) ( ( F ` k ) ` z ) )
150 119 136 149 3eqtr2d 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) = sum_ k e. ( ( j + 1 ) ... i ) ( ( F ` k ) ` z ) )
151 150 fveq2d 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( abs ` ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) ) = ( abs ` sum_ k e. ( ( j + 1 ) ... i ) ( ( F ` k ) ` z ) ) )
152 71 87 fsumabs 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( abs ` sum_ k e. ( ( j + 1 ) ... i ) ( ( F ` k ) ` z ) ) <_ sum_ k e. ( ( j + 1 ) ... i ) ( abs ` ( ( F ` k ) ` z ) ) )
153 151 152 eqbrtrd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( abs ` ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) ) <_ sum_ k e. ( ( j + 1 ) ... i ) ( abs ` ( ( F ` k ) ` z ) ) )
154 simpll 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ph )
155 154 21 6 syl2an 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... i ) ) -> ( M ` k ) e. RR )
156 80 155 syldan 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( ( j + 1 ) ... i ) ) -> ( M ` k ) e. RR )
157 156 adantlr 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> ( M ` k ) e. RR )
158 81 21 syl 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> k e. Z )
159 7 ad4ant14 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ ( k e. Z /\ z e. S ) ) -> ( abs ` ( ( F ` k ) ` z ) ) <_ ( M ` k ) )
160 159 anass1rs 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. Z ) -> ( abs ` ( ( F ` k ) ` z ) ) <_ ( M ` k ) )
161 158 160 syldan 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> ( abs ` ( ( F ` k ) ` z ) ) <_ ( M ` k ) )
162 71 88 157 161 fsumle 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> sum_ k e. ( ( j + 1 ) ... i ) ( abs ` ( ( F ` k ) ` z ) ) <_ sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) )
163 eqidd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... i ) ) -> ( M ` k ) = ( M ` k ) )
164 59 1 eleqtrdi 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> i e. ( ZZ>= ` N ) )
165 155 recnd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... i ) ) -> ( M ` k ) e. CC )
166 163 164 165 fsumser 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( N ... i ) ( M ` k ) = ( seq N ( + , M ) ` i ) )
167 eqidd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... j ) ) -> ( M ` k ) = ( M ` k ) )
168 154 126 6 syl2an 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... j ) ) -> ( M ` k ) e. RR )
169 168 recnd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... j ) ) -> ( M ` k ) e. CC )
170 167 73 169 fsumser 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( N ... j ) ( M ` k ) = ( seq N ( + , M ) ` j ) )
171 166 170 oveq12d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( sum_ k e. ( N ... i ) ( M ` k ) - sum_ k e. ( N ... j ) ( M ` k ) ) = ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) )
172 fzfid 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( N ... j ) e. Fin )
173 172 169 fsumcl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( N ... j ) ( M ` k ) e. CC )
174 fzfid 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( j + 1 ) ... i ) e. Fin )
175 80 165 syldan 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( ( j + 1 ) ... i ) ) -> ( M ` k ) e. CC )
176 174 175 fsumcl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) e. CC )
177 fzfid 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( N ... i ) e. Fin )
178 144 78 177 165 fsumsplit 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( N ... i ) ( M ` k ) = ( sum_ k e. ( N ... j ) ( M ` k ) + sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) ) )
179 173 176 178 mvrladdd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( sum_ k e. ( N ... i ) ( M ` k ) - sum_ k e. ( N ... j ) ( M ` k ) ) = sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) )
180 171 179 eqtr3d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) = sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) )
181 180 fveq2d 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) = ( abs ` sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) ) )
182 181 adantr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) = ( abs ` sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) ) )
183 180 94 eqeltrrd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) e. RR )
184 183 adantr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) e. RR )
185 0red 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> 0 e. RR )
186 87 absge0d 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> 0 <_ ( abs ` ( ( F ` k ) ` z ) ) )
187 185 88 157 186 161 letrd 
 |-  ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> 0 <_ ( M ` k ) )
188 71 157 187 fsumge0 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> 0 <_ sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) )
189 184 188 absidd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( abs ` sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) ) = sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) )
190 182 189 eqtrd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) = sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) )
191 162 190 breqtrrd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> sum_ k e. ( ( j + 1 ) ... i ) ( abs ` ( ( F ` k ) ` z ) ) <_ ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) )
192 70 89 97 153 191 letrd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( abs ` ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) ) <_ ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) )
193 simpllr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> r e. RR+ )
194 193 rpred 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> r e. RR )
195 lelttr 
 |-  ( ( ( abs ` ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) ) e. RR /\ ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) e. RR /\ r e. RR ) -> ( ( ( abs ` ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) ) <_ ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) /\ ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) < r ) -> ( abs ` ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) ) < r ) )
196 70 97 194 195 syl3anc 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( ( abs ` ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) ) <_ ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) /\ ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) < r ) -> ( abs ` ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) ) < r ) )
197 192 196 mpand 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) < r -> ( abs ` ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) ) < r ) )
198 197 ralrimdva 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) < r -> A. z e. S ( abs ` ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) ) < r ) )
199 198 anassrs 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ j e. Z ) /\ i e. ( ZZ>= ` j ) ) -> ( ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) < r -> A. z e. S ( abs ` ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) ) < r ) )
200 199 ralimdva 
 |-  ( ( ( ph /\ r e. RR+ ) /\ j e. Z ) -> ( A. i e. ( ZZ>= ` j ) ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) < r -> A. i e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) ) < r ) )
201 200 reximdva 
 |-  ( ( ph /\ r e. RR+ ) -> ( E. j e. Z A. i e. ( ZZ>= ` j ) ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) < r -> E. j e. Z A. i e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) ) < r ) )
202 201 ralimdva 
 |-  ( ph -> ( A. r e. RR+ E. j e. Z A. i e. ( ZZ>= ` j ) ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) < r -> A. r e. RR+ E. j e. Z A. i e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) ) < r ) )
203 10 202 mpd 
 |-  ( ph -> A. r e. RR+ E. j e. Z A. i e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) ) < r )
204 1 2 3 56 ulmcau 
 |-  ( ph -> ( seq N ( oF + , F ) e. dom ( ~~>u ` S ) <-> A. r e. RR+ E. j e. Z A. i e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( seq N ( oF + , F ) ` i ) ` z ) - ( ( seq N ( oF + , F ) ` j ) ` z ) ) ) < r ) )
205 203 204 mpbird 
 |-  ( ph -> seq N ( oF + , F ) e. dom ( ~~>u ` S ) )