Theorem mtest 23371

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

Hypotheses

Ref	Expression
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

Ref	Expression
mtest	|- ( ph -> seq N ( oF + , F ) e. dom ( ~~> u ` S ) )

Distinct variable groups:   z, k, F   k, M, z   k, N, z   ph, k, z   k, Z, z   S, k, z

Allowed substitution hints:   V( z, k)   W( z, k)

Proof of Theorem mtest

Dummy variables i j n r are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mtest.n	. . . 4 |- ( ph -> N e. ZZ )
2		mtest.d	. . . 4 |- ( ph -> seq N ( + , M ) e. dom ~~> )
3		mtest.z	. . . . 5 |- Z = ( ZZ>= ` N )
4	3	climcau 13746	. . . 4 |- ( ( 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 )
5	1, 2, 4	syl2anc 667	. . 3 |- ( ph -> A. r e. RR+ E. j e. Z A. i e. ( ZZ>= ` j ) ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) < r )
6		seqfn 12232	. . . . . . . . . . . . . . . . . . 19 |- ( N e. ZZ -> seq N ( oF + , F ) Fn ( ZZ>= ` N ) )
7	1, 6	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> seq N ( oF + , F ) Fn ( ZZ>= ` N ) )
8	3	fneq2i 5676	. . . . . . . . . . . . . . . . . 18 |- ( seq N ( oF + , F ) Fn Z <-> seq N ( oF + , F ) Fn ( ZZ>= ` N ) )
9	7, 8	sylibr 216	. . . . . . . . . . . . . . . . 17 |- ( ph -> seq N ( oF + , F ) Fn Z )
10		mtest.s	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> S e. V )
11		elex 3056	. . . . . . . . . . . . . . . . . . . . . 22 |- ( S e. V -> S e. _V )
12	10, 11	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> S e. _V )
13	12	adantr 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. Z ) -> S e. _V )
14		simpr 463	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. Z ) -> i e. Z )
15	14, 3	syl6eleq 2541	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. Z ) -> i e. ( ZZ>= ` N ) )
16		mtest.f	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> F : Z --> ( CC ^m S ) )
17	16	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ i e. Z ) -> F : Z --> ( CC ^m S ) )
18		elfzuz 11803	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k e. ( N ... i ) -> k e. ( ZZ>= ` N ) )
19	18, 3	syl6eleqr 2542	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k e. ( N ... i ) -> k e. Z )
20		ffvelrn 6025	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( F : Z --> ( CC ^m S ) /\ k e. Z ) -> ( F ` k ) e. ( CC ^m S ) )
21	17, 19, 20	syl2an 480	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> ( F ` k ) e. ( CC ^m S ) )
22		elmapi 7498	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( F ` k ) e. ( CC ^m S ) -> ( F ` k ) : S --> CC )
23	21, 22	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> ( F ` k ) : S --> CC )
24	23	feqmptd 5923	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> ( F ` k ) = ( z e. S |-> ( ( F ` k ) ` z ) ) )
25	19	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> k e. Z )
26		fveq2 5870	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( n = k -> ( F ` n ) = ( F ` k ) )
27	26	fveq1d 5872	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = k -> ( ( F ` n ) ` z ) = ( ( F ` k ) ` z ) )
28		eqid 2453	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. Z |-> ( ( F ` n ) ` z ) ) = ( n e. Z |-> ( ( F ` n ) ` z ) )
29		fvex 5880	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( F ` k ) ` z ) e. _V
30	27, 28, 29	fvmpt 5953	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. Z -> ( ( n e. Z |-> ( ( F ` n ) ` z ) ) ` k ) = ( ( F ` k ) ` z ) )
31	25, 30	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> ( ( n e. Z |-> ( ( F ` n ) ` z ) ) ` k ) = ( ( F ` k ) ` z ) )
32	31	mpteq2dv 4493	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> ( z e. S |-> ( ( n e. Z |-> ( ( F ` n ) ` z ) ) ` k ) ) = ( z e. S |-> ( ( F ` k ) ` z ) ) )
33	24, 32	eqtr4d 2490	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> ( F ` k ) = ( z e. S |-> ( ( n e. Z |-> ( ( F ` n ) ` z ) ) ` k ) ) )
34	13, 15, 33	seqof 12277	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. Z ) -> ( seq N ( oF + , F ) ` i ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) )
35	1	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ z e. S ) -> N e. ZZ )
36	16	ffvelrnda 6027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ n e. Z ) -> ( F ` n ) e. ( CC ^m S ) )
37		elmapi 7498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( F ` n ) e. ( CC ^m S ) -> ( F ` n ) : S --> CC )
38	36, 37	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ n e. Z ) -> ( F ` n ) : S --> CC )
39	38	ffvelrnda 6027	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ n e. Z ) /\ z e. S ) -> ( ( F ` n ) ` z ) e. CC )
40	39	an32s 814	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ z e. S ) /\ n e. Z ) -> ( ( F ` n ) ` z ) e. CC )
41	40, 28	fmptd 6051	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ z e. S ) -> ( n e. Z |-> ( ( F ` n ) ` z ) ) : Z --> CC )
42	41	ffvelrnda 6027	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ z e. S ) /\ i e. Z ) -> ( ( n e. Z |-> ( ( F ` n ) ` z ) ) ` i ) e. CC )
43	3, 35, 42	serf 12248	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ z e. S ) -> seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) : Z --> CC )
44	43	ffvelrnda 6027	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ z e. S ) /\ i e. Z ) -> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) e. CC )
45	44	an32s 814	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. Z ) /\ z e. S ) -> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) e. CC )
46		eqid 2453	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) )
47	45, 46	fmptd 6051	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. Z ) -> ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) : S --> CC )
48		cnex 9625	. . . . . . . . . . . . . . . . . . . . 21 |- CC e. _V
49		elmapg 7490	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 ) )
50	48, 13, 49	sylancr 670	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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 ) )
51	47, 50	mpbird 236	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. Z ) -> ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) e. ( CC ^m S ) )
52	34, 51	eqeltrd 2531	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. Z ) -> ( seq N ( oF + , F ) ` i ) e. ( CC ^m S ) )
53	52	ralrimiva 2804	. . . . . . . . . . . . . . . . 17 |- ( ph -> A. i e. Z ( seq N ( oF + , F ) ` i ) e. ( CC ^m S ) )
54		ffnfv 6054	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) )
55	9, 53, 54	sylanbrc 671	. . . . . . . . . . . . . . . 16 |- ( ph -> seq N ( oF + , F ) : Z --> ( CC ^m S ) )
56	55	ad2antrr 733	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> seq N ( oF + , F ) : Z --> ( CC ^m S ) )
57	3	uztrn2 11183	. . . . . . . . . . . . . . . 16 |- ( ( j e. Z /\ i e. ( ZZ>= ` j ) ) -> i e. Z )
58	57	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> i e. Z )
59	56, 58	ffvelrnd 6028	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( oF + , F ) ` i ) e. ( CC ^m S ) )
60		elmapi 7498	. . . . . . . . . . . . . 14 |- ( ( seq N ( oF + , F ) ` i ) e. ( CC ^m S ) -> ( seq N ( oF + , F ) ` i ) : S --> CC )
61	59, 60	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( oF + , F ) ` i ) : S --> CC )
62	61	ffvelrnda 6027	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( seq N ( oF + , F ) ` i ) ` z ) e. CC )
63		simprl 765	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> j e. Z )
64	56, 63	ffvelrnd 6028	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( oF + , F ) ` j ) e. ( CC ^m S ) )
65		elmapi 7498	. . . . . . . . . . . . . 14 |- ( ( seq N ( oF + , F ) ` j ) e. ( CC ^m S ) -> ( seq N ( oF + , F ) ` j ) : S --> CC )
66	64, 65	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( oF + , F ) ` j ) : S --> CC )
67	66	ffvelrnda 6027	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( seq N ( oF + , F ) ` j ) ` z ) e. CC )
68	62, 67	subcld 9991	. . . . . . . . . . 11 |- ( ( ( ( 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 )
69	68	abscld 13510	. . . . . . . . . 10 |- ( ( ( ( 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 )
70		fzfid 12193	. . . . . . . . . . 11 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( j + 1 ) ... i ) e. Fin )
71		ssun2 3600	. . . . . . . . . . . . . . . 16 |- ( ( j + 1 ) ... i ) C_ ( ( N ... j ) u. ( ( j + 1 ) ... i ) )
72	63, 3	syl6eleq 2541	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> j e. ( ZZ>= ` N ) )
73		simprr 767	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> i e. ( ZZ>= ` j ) )
74		elfzuzb 11801	. . . . . . . . . . . . . . . . . 18 |- ( j e. ( N ... i ) <-> ( j e. ( ZZ>= ` N ) /\ i e. ( ZZ>= ` j ) ) )
75	72, 73, 74	sylanbrc 671	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> j e. ( N ... i ) )
76		fzsplit 11832	. . . . . . . . . . . . . . . . 17 |- ( j e. ( N ... i ) -> ( N ... i ) = ( ( N ... j ) u. ( ( j + 1 ) ... i ) ) )
77	75, 76	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( N ... i ) = ( ( N ... j ) u. ( ( j + 1 ) ... i ) ) )
78	71, 77	syl5sseqr 3483	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( j + 1 ) ... i ) C_ ( N ... i ) )
79	78	sselda 3434	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( ( j + 1 ) ... i ) ) -> k e. ( N ... i ) )
80	79	adantlr 722	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> k e. ( N ... i ) )
81	16	ad2antrr 733	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> F : Z --> ( CC ^m S ) )
82	81, 19, 20	syl2an 480	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... i ) ) -> ( F ` k ) e. ( CC ^m S ) )
83	82, 22	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... i ) ) -> ( F ` k ) : S --> CC )
84	83	ffvelrnda 6027	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... i ) ) /\ z e. S ) -> ( ( F ` k ) ` z ) e. CC )
85	84	an32s 814	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( N ... i ) ) -> ( ( F ` k ) ` z ) e. CC )
86	80, 85	syldan 473	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> ( ( F ` k ) ` z ) e. CC )
87	86	abscld 13510	. . . . . . . . . . 11 |- ( ( ( ( ( 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 )
88	70, 87	fsumrecl 13812	. . . . . . . . . 10 |- ( ( ( ( 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 )
89		mtest.c	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. Z ) -> ( M ` k ) e. RR )
90	3, 1, 89	serfre 12249	. . . . . . . . . . . . . . . 16 |- ( ph -> seq N ( + , M ) : Z --> RR )
91	90	ad2antrr 733	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> seq N ( + , M ) : Z --> RR )
92	91, 58	ffvelrnd 6028	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( + , M ) ` i ) e. RR )
93	91, 63	ffvelrnd 6028	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( + , M ) ` j ) e. RR )
94	92, 93	resubcld 10054	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) e. RR )
95	94	recnd 9674	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) e. CC )
96	95	abscld 13510	. . . . . . . . . . 11 |- ( ( ( 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 467	. . . . . . . . . 10 |- ( ( ( ( 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	57, 34	sylan2 477	. . . . . . . . . . . . . . . . 17 |- ( ( 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 722	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 5872	. . . . . . . . . . . . . . 15 |- ( ( ( 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 5880	. . . . . . . . . . . . . . . 16 |- ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) e. _V
102	46	fvmpt2 5962	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) )
103	101, 102	mpan2 678	. . . . . . . . . . . . . . 15 |- ( 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 ) )
104	100, 103	sylan9eq 2507	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
105	34	ralrimiva 2804	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A. i e. Z ( seq N ( oF + , F ) ` i ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) )
106	105	ad2antrr 733	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) )
107		fveq2 5870	. . . . . . . . . . . . . . . . . . 19 |- ( i = j -> ( seq N ( oF + , F ) ` i ) = ( seq N ( oF + , F ) ` j ) )
108		fveq2 5870	. . . . . . . . . . . . . . . . . . . 20 |- ( i = j -> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) = ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) )
109	108	mpteq2dv 4493	. . . . . . . . . . . . . . . . . . 19 |- ( 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 ) ) )
110	107, 109	eqeq12d 2468	. . . . . . . . . . . . . . . . . 18 |- ( 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 ) ) ) )
111	110	rspccv 3149	. . . . . . . . . . . . . . . . 17 |- ( A. i e. Z ( seq N ( oF + , F ) ` i ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) -> ( j e. Z -> ( seq N ( oF + , F ) ` j ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) ) ) )
112	106, 63, 111	sylc 62	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 5872	. . . . . . . . . . . . . . 15 |- ( ( ( 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 5880	. . . . . . . . . . . . . . . 16 |- ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) e. _V
115		eqid 2453	. . . . . . . . . . . . . . . . 17 |- ( 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 5962	. . . . . . . . . . . . . . . 16 |- ( ( 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 678	. . . . . . . . . . . . . . 15 |- ( 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 2507	. . . . . . . . . . . . . 14 |- ( ( ( ( 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	104, 118	oveq12d 6313	. . . . . . . . . . . . 13 |- ( ( ( ( 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	19	adantl 468	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( N ... i ) ) -> k e. Z )
121	120, 30	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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	58	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> i e. Z )
123	122, 3	syl6eleq 2541	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> i e. ( ZZ>= ` N ) )
124	121, 123, 85	fsumser 13808	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 11803	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( N ... j ) -> k e. ( ZZ>= ` N ) )
126	125, 3	syl6eleqr 2542	. . . . . . . . . . . . . . . . 17 |- ( k e. ( N ... j ) -> k e. Z )
127	126	adantl 468	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( N ... j ) ) -> k e. Z )
128	127, 30	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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	63	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> j e. Z )
130	129, 3	syl6eleq 2541	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> j e. ( ZZ>= ` N ) )
131	81, 126, 20	syl2an 480	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... j ) ) -> ( F ` k ) e. ( CC ^m S ) )
132	131, 22	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... j ) ) -> ( F ` k ) : S --> CC )
133	132	ffvelrnda 6027	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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 814	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 13808	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 6313	. . . . . . . . . . . . 13 |- ( ( ( ( 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		eluzelre 11176	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. ( ZZ>= ` N ) -> j e. RR )
138	72, 137	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> j e. RR )
139	138	ltp1d 10544	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> j < ( j + 1 ) )
140		fzdisj 11833	. . . . . . . . . . . . . . . . . 18 |- ( j < ( j + 1 ) -> ( ( N ... j ) i^i ( ( j + 1 ) ... i ) ) = (/) )
141	139, 140	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( N ... j ) i^i ( ( j + 1 ) ... i ) ) = (/) )
142	141	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( N ... j ) i^i ( ( j + 1 ) ... i ) ) = (/) )
143	77	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( N ... i ) = ( ( N ... j ) u. ( ( j + 1 ) ... i ) ) )
144		fzfid 12193	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( N ... i ) e. Fin )
145	142, 143, 144, 85	fsumsplit 13818	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) )
146	145	eqcomd 2459	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( sum_ k e. ( N ... j ) ( ( F ` k ) ` z ) + sum_ k e. ( ( j + 1 ) ... i ) ( ( F ` k ) ` z ) ) = sum_ k e. ( N ... i ) ( ( F ` k ) ` z ) )
147	144, 85	fsumcl 13811	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> sum_ k e. ( N ... i ) ( ( F ` k ) ` z ) e. CC )
148		fzfid 12193	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( N ... j ) e. Fin )
149	148, 134	fsumcl 13811	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> sum_ k e. ( N ... j ) ( ( F ` k ) ` z ) e. CC )
150	70, 86	fsumcl 13811	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 )
151	147, 149, 150	subaddd 10009	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) <-> ( sum_ k e. ( N ... j ) ( ( F ` k ) ` z ) + sum_ k e. ( ( j + 1 ) ... i ) ( ( F ` k ) ` z ) ) = sum_ k e. ( N ... i ) ( ( F ` k ) ` z ) ) )
152	146, 151	mpbird 236	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) )
153	119, 136, 152	3eqtr2d 2493	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
154	153	fveq2d 5874	. . . . . . . . . . 11 |- ( ( ( ( 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 ) ) )
155	70, 86	fsumabs 13873	. . . . . . . . . . 11 |- ( ( ( ( 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 ) ) )
156	154, 155	eqbrtrd 4426	. . . . . . . . . 10 |- ( ( ( ( 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 ) ) )
157		simpll 761	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ph )
158	157, 19, 89	syl2an 480	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... i ) ) -> ( M ` k ) e. RR )
159	79, 158	syldan 473	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( ( j + 1 ) ... i ) ) -> ( M ` k ) e. RR )
160	159	adantlr 722	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> ( M ` k ) e. RR )
161	80, 19	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> k e. Z )
162		mtest.l	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( k e. Z /\ z e. S ) ) -> ( abs ` ( ( F ` k ) ` z ) ) <_ ( M ` k ) )
163	162	adantlr 722	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ z e. S ) ) -> ( abs ` ( ( F ` k ) ` z ) ) <_ ( M ` k ) )
164	163	adantlr 722	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ ( k e. Z /\ z e. S ) ) -> ( abs ` ( ( F ` k ) ` z ) ) <_ ( M ` k ) )
165	164	anass1rs 817	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. Z ) -> ( abs ` ( ( F ` k ) ` z ) ) <_ ( M ` k ) )
166	161, 165	syldan 473	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) )
167	70, 87, 160, 166	fsumle 13871	. . . . . . . . . . 11 |- ( ( ( ( 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 ) )
168		eqidd 2454	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... i ) ) -> ( M ` k ) = ( M ` k ) )
169	58, 3	syl6eleq 2541	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> i e. ( ZZ>= ` N ) )
170	158	recnd 9674	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... i ) ) -> ( M ` k ) e. CC )
171	168, 169, 170	fsumser 13808	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( N ... i ) ( M ` k ) = ( seq N ( + , M ) ` i ) )
172		eqidd 2454	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... j ) ) -> ( M ` k ) = ( M ` k ) )
173	157, 126, 89	syl2an 480	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... j ) ) -> ( M ` k ) e. RR )
174	173	recnd 9674	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... j ) ) -> ( M ` k ) e. CC )
175	172, 72, 174	fsumser 13808	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( N ... j ) ( M ` k ) = ( seq N ( + , M ) ` j ) )
176	171, 175	oveq12d 6313	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) )
177		fzfid 12193	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( N ... i ) e. Fin )
178	141, 77, 177, 170	fsumsplit 13818	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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	178	eqcomd 2459	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( sum_ k e. ( N ... j ) ( M ` k ) + sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) ) = sum_ k e. ( N ... i ) ( M ` k ) )
180	177, 170	fsumcl 13811	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( N ... i ) ( M ` k ) e. CC )
181		fzfid 12193	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( N ... j ) e. Fin )
182	181, 174	fsumcl 13811	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( N ... j ) ( M ` k ) e. CC )
183		fzfid 12193	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( j + 1 ) ... i ) e. Fin )
184	79, 170	syldan 473	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( ( j + 1 ) ... i ) ) -> ( M ` k ) e. CC )
185	183, 184	fsumcl 13811	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) e. CC )
186	180, 182, 185	subaddd 10009	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) <-> ( sum_ k e. ( N ... j ) ( M ` k ) + sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) ) = sum_ k e. ( N ... i ) ( M ` k ) ) )
187	179, 186	mpbird 236	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) )
188	176, 187	eqtr3d 2489	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
189	188	fveq2d 5874	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
190	189	adantr 467	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) )
191	188, 94	eqeltrrd 2532	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) e. RR )
192	191	adantr 467	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) e. RR )
193		0red 9649	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> 0 e. RR )
194	86	absge0d 13518	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> 0 <_ ( abs ` ( ( F ` k ) ` z ) ) )
195	193, 87, 160, 194, 166	letrd 9797	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> 0 <_ ( M ` k ) )
196	70, 160, 195	fsumge0 13867	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> 0 <_ sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) )
197	192, 196	absidd 13496	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
198	190, 197	eqtrd 2487	. . . . . . . . . . 11 |- ( ( ( ( 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 ) )
199	167, 198	breqtrrd 4432	. . . . . . . . . 10 |- ( ( ( ( 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 ) ) ) )
200	69, 88, 97, 156, 199	letrd 9797	. . . . . . . . 9 |- ( ( ( ( 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 ) ) ) )
201		simpllr 770	. . . . . . . . . . 11 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> r e. RR+ )
202	201	rpred 11348	. . . . . . . . . 10 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> r e. RR )
203		lelttr 9729	. . . . . . . . . 10 |- ( ( ( 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 ) )
204	69, 97, 202, 203	syl3anc 1269	. . . . . . . . 9 |- ( ( ( ( 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 ) )
205	200, 204	mpand 682	. . . . . . . 8 |- ( ( ( ( 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 ) )
206	205	ralrimdva 2808	. . . . . . 7 |- ( ( ( 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 ) )
207	206	anassrs 654	. . . . . 6 |- ( ( ( ( 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 ) )
208	207	ralimdva 2798	. . . . 5 |- ( ( ( 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 ) )
209	208	reximdva 2864	. . . 4 |- ( ( 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 ) )
210	209	ralimdva 2798	. . 3 |- ( 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 ) )
211	5, 210	mpd 15	. 2 |- ( 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 )
212	3, 1, 10, 55	ulmcau 23362	. 2 |- ( 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 ) )
213	211, 212	mpbird 236	1 |- ( ph -> seq N ( oF + , F ) e. dom ( ~~> u ` S ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1446   e. wcel 1889   A.wral 2739   E.wrex 2740   _Vcvv 3047   u. cun 3404   i^i cin 3405   (/)c0 3733   class class class wbr 4405   |-> cmpt 4464   dom cdm 4837   Fn wfn 5580   -->wf 5581   ` cfv 5585  (class class class)co 6295   oFcof 6534   ^m cmap 7477   CCcc 9542   RRcr 9543   0cc0 9544   1c1 9545   + caddc 9547   < clt 9680   <_ cle 9681   - cmin 9865   ZZcz 10944   ZZ>=cuz 11166   RR+crp 11309   ...cfz 11791   seqcseq 12220   abscabs 13309   ~~> cli 13560   sum_csu 13764   ~~> uculm 23343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588  ax-inf2 8151  ax-cnex 9600  ax-resscn 9601  ax-1cn 9602  ax-icn 9603  ax-addcl 9604  ax-addrcl 9605  ax-mulcl 9606  ax-mulrcl 9607  ax-mulcom 9608  ax-addass 9609  ax-mulass 9610  ax-distr 9611  ax-i2m1 9612  ax-1ne0 9613  ax-1rid 9614  ax-rnegex 9615  ax-rrecex 9616  ax-cnre 9617  ax-pre-lttri 9618  ax-pre-lttrn 9619  ax-pre-ltadd 9620  ax-pre-mulgt0 9621  ax-pre-sup 9622  ax-addf 9623  ax-mulf 9624

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-fal 1452  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-nel 2627  df-ral 2744  df-rex 2745  df-reu 2746  df-rmo 2747  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-int 4238  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-se 4797  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-isom 5594  df-riota 6257  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-of 6536  df-om 6698  df-1st 6798  df-2nd 6799  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-oadd 7191  df-er 7368  df-map 7479  df-pm 7480  df-en 7575  df-dom 7576  df-sdom 7577  df-fin 7578  df-sup 7961  df-inf 7962  df-oi 8030  df-card 8378  df-pnf 9682  df-mnf 9683  df-xr 9684  df-ltxr 9685  df-le 9686  df-sub 9867  df-neg 9868  df-div 10277  df-nn 10617  df-2 10675  df-3 10676  df-n0 10877  df-z 10945  df-uz 11167  df-rp 11310  df-ico 11648  df-fz 11792  df-fzo 11923  df-fl 12035  df-seq 12221  df-exp 12280  df-hash 12523  df-cj 13174  df-re 13175  df-im 13176  df-sqrt 13310  df-abs 13311  df-limsup 13538  df-clim 13564  df-rlim 13565  df-sum 13765  df-ulm 23344

This theorem is referenced by:  pserulm  23389  lgamgulmlem6  23971