Metamath Proof Explorer

Theorem mtestbdd

Description: Given the hypotheses of the Weierstrass M-test, the convergent function of the sequence is uniformly bounded. (Contributed by Mario Carneiro, 9-Jul-2017)

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 ~~> )
mtest.t 
|- ( ph -> seq N ( oF + , F ) ( ~~>u ` S ) T )
Assertion mtestbdd 
|- ( ph -> E. x e. RR A. z e. S ( abs ` ( T ` z ) ) <_ x )

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 mtest.t 
 |-  ( ph -> seq N ( oF + , F ) ( ~~>u ` S ) T )
10 6 recnd 
 |-  ( ( ph /\ k e. Z ) -> ( M ` k ) e. CC )
11 1 2 10 serf 
 |-  ( ph -> seq N ( + , M ) : Z --> CC )
12 11 ffvelrnda 
 |-  ( ( ph /\ m e. Z ) -> ( seq N ( + , M ) ` m ) e. CC )
13 12 ralrimiva 
 |-  ( ph -> A. m e. Z ( seq N ( + , M ) ` m ) e. CC )
14 1 climbdd 
 |-  ( ( N e. ZZ /\ seq N ( + , M ) e. dom ~~> /\ A. m e. Z ( seq N ( + , M ) ` m ) e. CC ) -> E. y e. RR A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y )
15 2 8 13 14 syl3anc 
 |-  ( ph -> E. y e. RR A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y )
16 2 adantr 
 |-  ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) -> N e. ZZ )
17 seqfn 
 |-  ( N e. ZZ -> seq N ( oF + , F ) Fn ( ZZ>= ` N ) )
18 2 17 syl 
 |-  ( ph -> seq N ( oF + , F ) Fn ( ZZ>= ` N ) )
19 1 fneq2i 
 |-  ( seq N ( oF + , F ) Fn Z <-> seq N ( oF + , F ) Fn ( ZZ>= ` N ) )
20 18 19 sylibr 
 |-  ( ph -> seq N ( oF + , F ) Fn Z )
21 ulmf2 
 |-  ( ( seq N ( oF + , F ) Fn Z /\ seq N ( oF + , F ) ( ~~>u ` S ) T ) -> seq N ( oF + , F ) : Z --> ( CC ^m S ) )
22 20 9 21 syl2anc 
 |-  ( ph -> seq N ( oF + , F ) : Z --> ( CC ^m S ) )
23 22 adantr 
 |-  ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) -> seq N ( oF + , F ) : Z --> ( CC ^m S ) )
24 simplrl 
 |-  ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) -> y e. RR )
25 fveq2 
 |-  ( x = z -> ( ( F ` j ) ` x ) = ( ( F ` j ) ` z ) )
26 25 mpteq2dv 
 |-  ( x = z -> ( j e. Z |-> ( ( F ` j ) ` x ) ) = ( j e. Z |-> ( ( F ` j ) ` z ) ) )
27 26 seqeq3d 
 |-  ( x = z -> seq N ( + , ( j e. Z |-> ( ( F ` j ) ` x ) ) ) = seq N ( + , ( j e. Z |-> ( ( F ` j ) ` z ) ) ) )
28 27 fveq1d 
 |-  ( x = z -> ( seq N ( + , ( j e. Z |-> ( ( F ` j ) ` x ) ) ) ` n ) = ( seq N ( + , ( j e. Z |-> ( ( F ` j ) ` z ) ) ) ` n ) )
29 eqid 
 |-  ( x e. S |-> ( seq N ( + , ( j e. Z |-> ( ( F ` j ) ` x ) ) ) ` n ) ) = ( x e. S |-> ( seq N ( + , ( j e. Z |-> ( ( F ` j ) ` x ) ) ) ` n ) )
30 fvex 
 |-  ( seq N ( + , ( j e. Z |-> ( ( F ` j ) ` z ) ) ) ` n ) e. _V
31 28 29 30 fvmpt 
 |-  ( z e. S -> ( ( x e. S |-> ( seq N ( + , ( j e. Z |-> ( ( F ` j ) ` x ) ) ) ` n ) ) ` z ) = ( seq N ( + , ( j e. Z |-> ( ( F ` j ) ` z ) ) ) ` n ) )
32 31 adantl 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( ( x e. S |-> ( seq N ( + , ( j e. Z |-> ( ( F ` j ) ` x ) ) ) ` n ) ) ` z ) = ( seq N ( + , ( j e. Z |-> ( ( F ` j ) ` z ) ) ) ` n ) )
33 4 ad3antrrr 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> F : Z --> ( CC ^m S ) )
34 33 feqmptd 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> F = ( j e. Z |-> ( F ` j ) ) )
35 33 ffvelrnda 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ j e. Z ) -> ( F ` j ) e. ( CC ^m S ) )
36 elmapi 
 |-  ( ( F ` j ) e. ( CC ^m S ) -> ( F ` j ) : S --> CC )
37 35 36 syl 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ j e. Z ) -> ( F ` j ) : S --> CC )
38 37 feqmptd 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ j e. Z ) -> ( F ` j ) = ( x e. S |-> ( ( F ` j ) ` x ) ) )
39 38 mpteq2dva 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( j e. Z |-> ( F ` j ) ) = ( j e. Z |-> ( x e. S |-> ( ( F ` j ) ` x ) ) ) )
40 34 39 eqtrd 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> F = ( j e. Z |-> ( x e. S |-> ( ( F ` j ) ` x ) ) ) )
41 40 seqeq3d 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> seq N ( oF + , F ) = seq N ( oF + , ( j e. Z |-> ( x e. S |-> ( ( F ` j ) ` x ) ) ) ) )
42 41 fveq1d 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( seq N ( oF + , F ) ` n ) = ( seq N ( oF + , ( j e. Z |-> ( x e. S |-> ( ( F ` j ) ` x ) ) ) ) ` n ) )
43 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> S e. V )
44 simplr 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> n e. Z )
45 44 1 eleqtrdi 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> n e. ( ZZ>= ` N ) )
46 elfzuz 
 |-  ( k e. ( N ... n ) -> k e. ( ZZ>= ` N ) )
47 46 1 eleqtrrdi 
 |-  ( k e. ( N ... n ) -> k e. Z )
48 47 ssriv 
 |-  ( N ... n ) C_ Z
49 48 a1i 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( N ... n ) C_ Z )
50 37 ffvelrnda 
 |-  ( ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ j e. Z ) /\ x e. S ) -> ( ( F ` j ) ` x ) e. CC )
51 50 anasss 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ ( j e. Z /\ x e. S ) ) -> ( ( F ` j ) ` x ) e. CC )
52 43 45 49 51 seqof2 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( seq N ( oF + , ( j e. Z |-> ( x e. S |-> ( ( F ` j ) ` x ) ) ) ) ` n ) = ( x e. S |-> ( seq N ( + , ( j e. Z |-> ( ( F ` j ) ` x ) ) ) ` n ) ) )
53 42 52 eqtrd 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( seq N ( oF + , F ) ` n ) = ( x e. S |-> ( seq N ( + , ( j e. Z |-> ( ( F ` j ) ` x ) ) ) ` n ) ) )
54 53 fveq1d 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( ( seq N ( oF + , F ) ` n ) ` z ) = ( ( x e. S |-> ( seq N ( + , ( j e. Z |-> ( ( F ` j ) ` x ) ) ) ` n ) ) ` z ) )
55 47 adantl 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ k e. ( N ... n ) ) -> k e. Z )
56 fveq2 
 |-  ( j = k -> ( F ` j ) = ( F ` k ) )
57 56 fveq1d 
 |-  ( j = k -> ( ( F ` j ) ` z ) = ( ( F ` k ) ` z ) )
58 eqid 
 |-  ( j e. Z |-> ( ( F ` j ) ` z ) ) = ( j e. Z |-> ( ( F ` j ) ` z ) )
59 fvex 
 |-  ( ( F ` k ) ` z ) e. _V
60 57 58 59 fvmpt 
 |-  ( k e. Z -> ( ( j e. Z |-> ( ( F ` j ) ` z ) ) ` k ) = ( ( F ` k ) ` z ) )
61 55 60 syl 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ k e. ( N ... n ) ) -> ( ( j e. Z |-> ( ( F ` j ) ` z ) ) ` k ) = ( ( F ` k ) ` z ) )
62 simplr 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ j e. Z ) -> z e. S )
63 37 62 ffvelrnd 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ j e. Z ) -> ( ( F ` j ) ` z ) e. CC )
64 63 fmpttd 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( j e. Z |-> ( ( F ` j ) ` z ) ) : Z --> CC )
65 64 ffvelrnda 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ k e. Z ) -> ( ( j e. Z |-> ( ( F ` j ) ` z ) ) ` k ) e. CC )
66 47 65 sylan2 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ k e. ( N ... n ) ) -> ( ( j e. Z |-> ( ( F ` j ) ` z ) ) ` k ) e. CC )
67 61 66 eqeltrrd 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ k e. ( N ... n ) ) -> ( ( F ` k ) ` z ) e. CC )
68 61 45 67 fsumser 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> sum_ k e. ( N ... n ) ( ( F ` k ) ` z ) = ( seq N ( + , ( j e. Z |-> ( ( F ` j ) ` z ) ) ) ` n ) )
69 32 54 68 3eqtr4d 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( ( seq N ( oF + , F ) ` n ) ` z ) = sum_ k e. ( N ... n ) ( ( F ` k ) ` z ) )
70 69 fveq2d 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( abs ` ( ( seq N ( oF + , F ) ` n ) ` z ) ) = ( abs ` sum_ k e. ( N ... n ) ( ( F ` k ) ` z ) ) )
71 fzfid 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( N ... n ) e. Fin )
72 71 67 fsumcl 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> sum_ k e. ( N ... n ) ( ( F ` k ) ` z ) e. CC )
73 72 abscld 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( abs ` sum_ k e. ( N ... n ) ( ( F ` k ) ` z ) ) e. RR )
74 67 abscld 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ k e. ( N ... n ) ) -> ( abs ` ( ( F ` k ) ` z ) ) e. RR )
75 71 74 fsumrecl 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> sum_ k e. ( N ... n ) ( abs ` ( ( F ` k ) ` z ) ) e. RR )
76 24 adantr 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> y e. RR )
77 71 67 fsumabs 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( abs ` sum_ k e. ( N ... n ) ( ( F ` k ) ` z ) ) <_ sum_ k e. ( N ... n ) ( abs ` ( ( F ` k ) ` z ) ) )
78 simp-4l 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ k e. ( N ... n ) ) -> ph )
79 78 55 6 syl2anc 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ k e. ( N ... n ) ) -> ( M ` k ) e. RR )
80 71 79 fsumrecl 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> sum_ k e. ( N ... n ) ( M ` k ) e. RR )
81 simplr 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ k e. ( N ... n ) ) -> z e. S )
82 78 55 81 7 syl12anc 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ k e. ( N ... n ) ) -> ( abs ` ( ( F ` k ) ` z ) ) <_ ( M ` k ) )
83 71 74 79 82 fsumle 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> sum_ k e. ( N ... n ) ( abs ` ( ( F ` k ) ` z ) ) <_ sum_ k e. ( N ... n ) ( M ` k ) )
84 80 recnd 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> sum_ k e. ( N ... n ) ( M ` k ) e. CC )
85 84 abscld 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( abs ` sum_ k e. ( N ... n ) ( M ` k ) ) e. RR )
86 80 leabsd 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> sum_ k e. ( N ... n ) ( M ` k ) <_ ( abs ` sum_ k e. ( N ... n ) ( M ` k ) ) )
87 eqidd 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ k e. ( N ... n ) ) -> ( M ` k ) = ( M ` k ) )
88 78 55 10 syl2anc 
 |-  ( ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) /\ k e. ( N ... n ) ) -> ( M ` k ) e. CC )
89 87 45 88 fsumser 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> sum_ k e. ( N ... n ) ( M ` k ) = ( seq N ( + , M ) ` n ) )
90 89 fveq2d 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( abs ` sum_ k e. ( N ... n ) ( M ` k ) ) = ( abs ` ( seq N ( + , M ) ` n ) ) )
91 simprr 
 |-  ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) -> A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y )
92 fveq2 
 |-  ( m = n -> ( seq N ( + , M ) ` m ) = ( seq N ( + , M ) ` n ) )
93 92 fveq2d 
 |-  ( m = n -> ( abs ` ( seq N ( + , M ) ` m ) ) = ( abs ` ( seq N ( + , M ) ` n ) ) )
94 93 breq1d 
 |-  ( m = n -> ( ( abs ` ( seq N ( + , M ) ` m ) ) <_ y <-> ( abs ` ( seq N ( + , M ) ` n ) ) <_ y ) )
95 94 rspccva 
 |-  ( ( A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y /\ n e. Z ) -> ( abs ` ( seq N ( + , M ) ` n ) ) <_ y )
96 91 95 sylan 
 |-  ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) -> ( abs ` ( seq N ( + , M ) ` n ) ) <_ y )
97 96 adantr 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( abs ` ( seq N ( + , M ) ` n ) ) <_ y )
98 90 97 eqbrtrd 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( abs ` sum_ k e. ( N ... n ) ( M ` k ) ) <_ y )
99 80 85 76 86 98 letrd 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> sum_ k e. ( N ... n ) ( M ` k ) <_ y )
100 75 80 76 83 99 letrd 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> sum_ k e. ( N ... n ) ( abs ` ( ( F ` k ) ` z ) ) <_ y )
101 73 75 76 77 100 letrd 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( abs ` sum_ k e. ( N ... n ) ( ( F ` k ) ` z ) ) <_ y )
102 70 101 eqbrtrd 
 |-  ( ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) /\ z e. S ) -> ( abs ` ( ( seq N ( oF + , F ) ` n ) ` z ) ) <_ y )
103 102 ralrimiva 
 |-  ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) -> A. z e. S ( abs ` ( ( seq N ( oF + , F ) ` n ) ` z ) ) <_ y )
104 brralrspcev 
 |-  ( ( y e. RR /\ A. z e. S ( abs ` ( ( seq N ( oF + , F ) ` n ) ` z ) ) <_ y ) -> E. x e. RR A. z e. S ( abs ` ( ( seq N ( oF + , F ) ` n ) ` z ) ) <_ x )
105 24 103 104 syl2anc 
 |-  ( ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) /\ n e. Z ) -> E. x e. RR A. z e. S ( abs ` ( ( seq N ( oF + , F ) ` n ) ` z ) ) <_ x )
106 9 adantr 
 |-  ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) -> seq N ( oF + , F ) ( ~~>u ` S ) T )
107 1 16 23 105 106 ulmbdd 
 |-  ( ( ph /\ ( y e. RR /\ A. m e. Z ( abs ` ( seq N ( + , M ) ` m ) ) <_ y ) ) -> E. x e. RR A. z e. S ( abs ` ( T ` z ) ) <_ x )
108 15 107 rexlimddv 
 |-  ( ph -> E. x e. RR A. z e. S ( abs ` ( T ` z ) ) <_ x )