Theorem mtest 20273

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 ( o F + , 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 12419	. . . 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 643	. . 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 11290	. . . . . . . . . . . . . . . . . . 19 |- ( N e. ZZ -> seq N ( o F + , F ) Fn ( ZZ>= ` N ) )
7	1, 6	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> seq N ( o F + , F ) Fn ( ZZ>= ` N ) )
8	3	fneq2i 5499	. . . . . . . . . . . . . . . . . 18 |- ( seq N ( o F + , F ) Fn Z <-> seq N ( o F + , F ) Fn ( ZZ>= ` N ) )
9	7, 8	sylibr 204	. . . . . . . . . . . . . . . . 17 |- ( ph -> seq N ( o F + , F ) Fn Z )
10		mtest.s	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> S e. V )
11		elex 2924	. . . . . . . . . . . . . . . . . . . . . 22 |- ( S e. V -> S e. _V )
12	10, 11	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> S e. _V )
13	12	adantr 452	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. Z ) -> S e. _V )
14		simpr 448	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. Z ) -> i e. Z )
15	14, 3	syl6eleq 2494	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. Z ) -> i e. ( ZZ>= ` N ) )
16		mtest.f	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> F : Z --> ( CC ^m S ) )
17	16	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ i e. Z ) -> F : Z --> ( CC ^m S ) )
18		elfzuz 11011	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k e. ( N ... i ) -> k e. ( ZZ>= ` N ) )
19	18, 3	syl6eleqr 2495	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k e. ( N ... i ) -> k e. Z )
20		ffvelrn 5827	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( F : Z --> ( CC ^m S ) /\ k e. Z ) -> ( F ` k ) e. ( CC ^m S ) )
21	17, 19, 20	syl2an 464	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> ( F ` k ) e. ( CC ^m S ) )
22		elmapi 6997	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( F ` k ) e. ( CC ^m S ) -> ( F ` k ) : S --> CC )
23	21, 22	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> ( F ` k ) : S --> CC )
24	23	feqmptd 5738	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> ( F ` k ) = ( z e. S |-> ( ( F ` k ) ` z ) ) )
25	19	adantl 453	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> k e. Z )
26		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( n = k -> ( F ` n ) = ( F ` k ) )
27	26	fveq1d 5689	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = k -> ( ( F ` n ) ` z ) = ( ( F ` k ) ` z ) )
28		eqid 2404	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. Z |-> ( ( F ` n ) ` z ) ) = ( n e. Z |-> ( ( F ` n ) ` z ) )
29		fvex 5701	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( F ` k ) ` z ) e. _V
30	27, 28, 29	fvmpt 5765	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. Z -> ( ( n e. Z |-> ( ( F ` n ) ` z ) ) ` k ) = ( ( F ` k ) ` z ) )
31	25, 30	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ i e. Z ) /\ k e. ( N ... i ) ) -> ( ( n e. Z |-> ( ( F ` n ) ` z ) ) ` k ) = ( ( F ` k ) ` z ) )
32	31	mpteq2dv 4256	. . . . . . . . . . . . . . . . . . . . 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 2439	. . . . . . . . . . . . . . . . . . . 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 11335	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. Z ) -> ( seq N ( o F + , F ) ` i ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) )
35	1	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ z e. S ) -> N e. ZZ )
36	16	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ n e. Z ) -> ( F ` n ) e. ( CC ^m S ) )
37		elmapi 6997	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( F ` n ) e. ( CC ^m S ) -> ( F ` n ) : S --> CC )
38	36, 37	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ n e. Z ) -> ( F ` n ) : S --> CC )
39	38	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ n e. Z ) /\ z e. S ) -> ( ( F ` n ) ` z ) e. CC )
40	39	an32s 780	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ z e. S ) /\ n e. Z ) -> ( ( F ` n ) ` z ) e. CC )
41	40, 28	fmptd 5852	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ z e. S ) -> ( n e. Z |-> ( ( F ` n ) ` z ) ) : Z --> CC )
42	41	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ z e. S ) /\ i e. Z ) -> ( ( n e. Z |-> ( ( F ` n ) ` z ) ) ` i ) e. CC )
43	3, 35, 42	serf 11306	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ z e. S ) -> seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) : Z --> CC )
44	43	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ z e. S ) /\ i e. Z ) -> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) e. CC )
45	44	an32s 780	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ i e. Z ) /\ z e. S ) -> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) e. CC )
46		eqid 2404	. . . . . . . . . . . . . . . . . . . . 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 5852	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. Z ) -> ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) : S --> CC )
48		cnex 9027	. . . . . . . . . . . . . . . . . . . . 21 |- CC e. _V
49		elmapg 6990	. . . . . . . . . . . . . . . . . . . . 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 645	. . . . . . . . . . . . . . . . . . . 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 224	. . . . . . . . . . . . . . . . . . 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 2478	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. Z ) -> ( seq N ( o F + , F ) ` i ) e. ( CC ^m S ) )
53	52	ralrimiva 2749	. . . . . . . . . . . . . . . . 17 |- ( ph -> A. i e. Z ( seq N ( o F + , F ) ` i ) e. ( CC ^m S ) )
54		ffnfv 5853	. . . . . . . . . . . . . . . . 17 |- ( seq N ( o F + , F ) : Z --> ( CC ^m S ) <-> ( seq N ( o F + , F ) Fn Z /\ A. i e. Z ( seq N ( o F + , F ) ` i ) e. ( CC ^m S ) ) )
55	9, 53, 54	sylanbrc 646	. . . . . . . . . . . . . . . 16 |- ( ph -> seq N ( o F + , F ) : Z --> ( CC ^m S ) )
56	55	ad2antrr 707	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> seq N ( o F + , F ) : Z --> ( CC ^m S ) )
57	3	uztrn2 10459	. . . . . . . . . . . . . . . 16 |- ( ( j e. Z /\ i e. ( ZZ>= ` j ) ) -> i e. Z )
58	57	adantl 453	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> i e. Z )
59	56, 58	ffvelrnd 5830	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( o F + , F ) ` i ) e. ( CC ^m S ) )
60		elmapi 6997	. . . . . . . . . . . . . 14 |- ( ( seq N ( o F + , F ) ` i ) e. ( CC ^m S ) -> ( seq N ( o F + , F ) ` i ) : S --> CC )
61	59, 60	syl 16	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( o F + , F ) ` i ) : S --> CC )
62	61	ffvelrnda 5829	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( seq N ( o F + , F ) ` i ) ` z ) e. CC )
63		simprl 733	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> j e. Z )
64	56, 63	ffvelrnd 5830	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( o F + , F ) ` j ) e. ( CC ^m S ) )
65		elmapi 6997	. . . . . . . . . . . . . 14 |- ( ( seq N ( o F + , F ) ` j ) e. ( CC ^m S ) -> ( seq N ( o F + , F ) ` j ) : S --> CC )
66	64, 65	syl 16	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( o F + , F ) ` j ) : S --> CC )
67	66	ffvelrnda 5829	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( seq N ( o F + , F ) ` j ) ` z ) e. CC )
68	62, 67	subcld 9367	. . . . . . . . . . 11 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( ( seq N ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) e. CC )
69	68	abscld 12193	. . . . . . . . . 10 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( abs ` ( ( ( seq N ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) ) e. RR )
70		fzfid 11267	. . . . . . . . . . 11 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( j + 1 ) ... i ) e. Fin )
71		ssun2 3471	. . . . . . . . . . . . . . . 16 |- ( ( j + 1 ) ... i ) C_ ( ( N ... j ) u. ( ( j + 1 ) ... i ) )
72	63, 3	syl6eleq 2494	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> j e. ( ZZ>= ` N ) )
73		simprr 734	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> i e. ( ZZ>= ` j ) )
74		elfzuzb 11009	. . . . . . . . . . . . . . . . . 18 |- ( j e. ( N ... i ) <-> ( j e. ( ZZ>= ` N ) /\ i e. ( ZZ>= ` j ) ) )
75	72, 73, 74	sylanbrc 646	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> j e. ( N ... i ) )
76		fzsplit 11033	. . . . . . . . . . . . . . . . 17 |- ( j e. ( N ... i ) -> ( N ... i ) = ( ( N ... j ) u. ( ( j + 1 ) ... i ) ) )
77	75, 76	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( N ... i ) = ( ( N ... j ) u. ( ( j + 1 ) ... i ) ) )
78	71, 77	syl5sseqr 3357	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( j + 1 ) ... i ) C_ ( N ... i ) )
79	78	sselda 3308	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( ( j + 1 ) ... i ) ) -> k e. ( N ... i ) )
80	79	adantlr 696	. . . . . . . . . . . . 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 707	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> F : Z --> ( CC ^m S ) )
82	81, 19, 20	syl2an 464	. . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... i ) ) -> ( F ` k ) : S --> CC )
84	83	ffvelrnda 5829	. . . . . . . . . . . . . 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 780	. . . . . . . . . . . . 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 457	. . . . . . . . . . . 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 12193	. . . . . . . . . . 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 12483	. . . . . . . . . 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 11307	. . . . . . . . . . . . . . . 16 |- ( ph -> seq N ( + , M ) : Z --> RR )
91	90	ad2antrr 707	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> seq N ( + , M ) : Z --> RR )
92	91, 58	ffvelrnd 5830	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( + , M ) ` i ) e. RR )
93	91, 63	ffvelrnd 5830	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( + , M ) ` j ) e. RR )
94	92, 93	resubcld 9421	. . . . . . . . . . . . 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 9070	. . . . . . . . . . . 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 12193	. . . . . . . . . . 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 452	. . . . . . . . . 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 461	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( o F + , F ) ` i ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) )
99	98	adantlr 696	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( o F + , F ) ` i ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) )
100	99	fveq1d 5689	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( seq N ( o F + , F ) ` i ) ` z ) = ( ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) ` z ) )
101		fvex 5701	. . . . . . . . . . . . . . . 16 |- ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) e. _V
102	46	fvmpt2 5771	. . . . . . . . . . . . . . . 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 653	. . . . . . . . . . . . . . 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 2456	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( seq N ( o F + , F ) ` i ) ` z ) = ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) )
105	34	ralrimiva 2749	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A. i e. Z ( seq N ( o F + , F ) ` i ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) )
106	105	ad2antrr 707	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> A. i e. Z ( seq N ( o F + , F ) ` i ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) )
107		fveq2 5687	. . . . . . . . . . . . . . . . . . 19 |- ( i = j -> ( seq N ( o F + , F ) ` i ) = ( seq N ( o F + , F ) ` j ) )
108		fveq2 5687	. . . . . . . . . . . . . . . . . . . 20 |- ( i = j -> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) = ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) )
109	108	mpteq2dv 4256	. . . . . . . . . . . . . . . . . . 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 2418	. . . . . . . . . . . . . . . . . 18 |- ( i = j -> ( ( seq N ( o F + , F ) ` i ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) <-> ( seq N ( o F + , F ) ` j ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) ) ) )
111	110	rspccv 3009	. . . . . . . . . . . . . . . . 17 |- ( A. i e. Z ( seq N ( o F + , F ) ` i ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) ) -> ( j e. Z -> ( seq N ( o F + , F ) ` j ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) ) ) )
112	106, 63, 111	sylc 58	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( seq N ( o F + , F ) ` j ) = ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) ) )
113	112	fveq1d 5689	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( seq N ( o F + , F ) ` j ) ` z ) = ( ( z e. S |-> ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) ) ` z ) )
114		fvex 5701	. . . . . . . . . . . . . . . 16 |- ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) e. _V
115		eqid 2404	. . . . . . . . . . . . . . . . 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 5771	. . . . . . . . . . . . . . . 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 653	. . . . . . . . . . . . . . 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 2456	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( seq N ( o F + , F ) ` j ) ` z ) = ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) )
119	104, 118	oveq12d 6058	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( ( seq N ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) = ( ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` i ) - ( seq N ( + , ( n e. Z |-> ( ( F ` n ) ` z ) ) ) ` j ) ) )
120	19	adantl 453	. . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . 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 452	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> i e. Z )
123	122, 3	syl6eleq 2494	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> i e. ( ZZ>= ` N ) )
124	121, 123, 85	fsumser 12479	. . . . . . . . . . . . . 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 11011	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( N ... j ) -> k e. ( ZZ>= ` N ) )
126	125, 3	syl6eleqr 2495	. . . . . . . . . . . . . . . . 17 |- ( k e. ( N ... j ) -> k e. Z )
127	126	adantl 453	. . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . 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 452	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> j e. Z )
130	129, 3	syl6eleq 2494	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> j e. ( ZZ>= ` N ) )
131	81, 126, 20	syl2an 464	. . . . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... j ) ) -> ( F ` k ) : S --> CC )
133	132	ffvelrnda 5829	. . . . . . . . . . . . . . . 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 780	. . . . . . . . . . . . . . 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 12479	. . . . . . . . . . . . . 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 6058	. . . . . . . . . . . . 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 10453	. . . . . . . . . . . . . . . . . . . 20 |- ( j e. ( ZZ>= ` N ) -> j e. RR )
138	72, 137	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> j e. RR )
139	138	ltp1d 9897	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> j < ( j + 1 ) )
140		fzdisj 11034	. . . . . . . . . . . . . . . . . 18 |- ( j < ( j + 1 ) -> ( ( N ... j ) i^i ( ( j + 1 ) ... i ) ) = (/) )
141	139, 140	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( N ... j ) i^i ( ( j + 1 ) ... i ) ) = (/) )
142	141	adantr 452	. . . . . . . . . . . . . . . 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 452	. . . . . . . . . . . . . . . 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 11267	. . . . . . . . . . . . . . . 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 12488	. . . . . . . . . . . . . . 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 2409	. . . . . . . . . . . . . 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 12482	. . . . . . . . . . . . . . 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 11267	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( N ... j ) e. Fin )
149	148, 134	fsumcl 12482	. . . . . . . . . . . . . . 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 12482	. . . . . . . . . . . . . . 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 9385	. . . . . . . . . . . . . 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 224	. . . . . . . . . . . . 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 2442	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( ( seq N ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) = sum_ k e. ( ( j + 1 ) ... i ) ( ( F ` k ) ` z ) )
154	153	fveq2d 5691	. . . . . . . . . . 11 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( abs ` ( ( ( seq N ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) ) = ( abs ` sum_ k e. ( ( j + 1 ) ... i ) ( ( F ` k ) ` z ) ) )
155	70, 86	fsumabs 12535	. . . . . . . . . . 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 4192	. . . . . . . . . 10 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( abs ` ( ( ( seq N ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) ) <_ sum_ k e. ( ( j + 1 ) ... i ) ( abs ` ( ( F ` k ) ` z ) ) )
157		simpll 731	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ph )
158	157, 19, 89	syl2an 464	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... i ) ) -> ( M ` k ) e. RR )
159	79, 158	syldan 457	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( ( j + 1 ) ... i ) ) -> ( M ` k ) e. RR )
160	159	adantlr 696	. . . . . . . . . . . 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 16	. . . . . . . . . . . . 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 696	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ r e. RR+ ) /\ ( k e. Z /\ z e. S ) ) -> ( abs ` ( ( F ` k ) ` z ) ) <_ ( M ` k ) )
164	163	adantlr 696	. . . . . . . . . . . . . 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 783	. . . . . . . . . . . . 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 457	. . . . . . . . . . . 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 12533	. . . . . . . . . . 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 2405	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... i ) ) -> ( M ` k ) = ( M ` k ) )
169	58, 3	syl6eleq 2494	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> i e. ( ZZ>= ` N ) )
170	158	recnd 9070	. . . . . . . . . . . . . . . . 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 12479	. . . . . . . . . . . . . . . 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 2405	. . . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ k e. ( N ... j ) ) -> ( M ` k ) e. RR )
174	173	recnd 9070	. . . . . . . . . . . . . . . . 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 12479	. . . . . . . . . . . . . . . 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 6058	. . . . . . . . . . . . . . 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 11267	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( N ... i ) e. Fin )
178	141, 77, 177, 170	fsumsplit 12488	. . . . . . . . . . . . . . . . 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 2409	. . . . . . . . . . . . . . . 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 12482	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( N ... i ) ( M ` k ) e. CC )
181		fzfid 11267	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( N ... j ) e. Fin )
182	181, 174	fsumcl 12482	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> sum_ k e. ( N ... j ) ( M ` k ) e. CC )
183		fzfid 11267	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) -> ( ( j + 1 ) ... i ) e. Fin )
184	79, 170	syldan 457	. . . . . . . . . . . . . . . . . 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 12482	. . . . . . . . . . . . . . . . 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 9385	. . . . . . . . . . . . . . . 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 224	. . . . . . . . . . . . . . 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 2438	. . . . . . . . . . . . . 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 5691	. . . . . . . . . . . . 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 452	. . . . . . . . . . . 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 2479	. . . . . . . . . . . . . 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 452	. . . . . . . . . . . . 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		0re 9047	. . . . . . . . . . . . . . . 16 |- 0 e. RR
194	193	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> 0 e. RR )
195	86	absge0d 12201	. . . . . . . . . . . . . . 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 ) ) )
196	194, 87, 160, 195, 166	letrd 9183	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) /\ k e. ( ( j + 1 ) ... i ) ) -> 0 <_ ( M ` k ) )
197	70, 160, 196	fsumge0 12529	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> 0 <_ sum_ k e. ( ( j + 1 ) ... i ) ( M ` k ) )
198	192, 197	absidd 12180	. . . . . . . . . . . 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 ) )
199	190, 198	eqtrd 2436	. . . . . . . . . . 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 ) )
200	167, 199	breqtrrd 4198	. . . . . . . . . 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 ) ) ) )
201	69, 88, 97, 156, 200	letrd 9183	. . . . . . . . 9 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( abs ` ( ( ( seq N ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) ) <_ ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) )
202		simpllr 736	. . . . . . . . . . 11 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> r e. RR+ )
203	202	rpred 10604	. . . . . . . . . 10 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> r e. RR )
204		lelttr 9121	. . . . . . . . . 10 |- ( ( ( abs ` ( ( ( seq N ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) ) e. RR /\ ( abs ` ( ( seq N ( + , M ) ` i ) - ( seq N ( + , M ) ` j ) ) ) e. RR /\ r e. RR ) -> ( ( ( abs ` ( ( ( seq N ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , 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 ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) ) < r ) )
205	69, 97, 203, 204	syl3anc 1184	. . . . . . . . 9 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( j e. Z /\ i e. ( ZZ>= ` j ) ) ) /\ z e. S ) -> ( ( ( abs ` ( ( ( seq N ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , 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 ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) ) < r ) )
206	201, 205	mpand 657	. . . . . . . 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 ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) ) < r ) )
207	206	ralrimdva 2756	. . . . . . 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 ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) ) < r ) )
208	207	anassrs 630	. . . . . 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 ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) ) < r ) )
209	208	ralimdva 2744	. . . . 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 ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) ) < r ) )
210	209	reximdva 2778	. . . 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 ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) ) < r ) )
211	210	ralimdva 2744	. . 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 ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) ) < r ) )
212	5, 211	mpd 15	. 2 |- ( ph -> A. r e. RR+ E. j e. Z A. i e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( seq N ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) ) < r )
213	3, 1, 10, 55	ulmcau 20264	. 2 |- ( ph -> ( seq N ( o F + , 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 ( o F + , F ) ` i ) ` z ) - ( ( seq N ( o F + , F ) ` j ) ` z ) ) ) < r ) )
214	212, 213	mpbird 224	1 |- ( ph -> seq N ( o F + , F ) e. dom ( ~~> u ` S ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721   A.wral 2666   E.wrex 2667   _Vcvv 2916   u. cun 3278   i^i cin 3279   (/)c0 3588   class class class wbr 4172   e. cmpt 4226   dom cdm 4837   Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6040   o Fcof 6262   ^m cmap 6977   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   + caddc 8949   < clt 9076   <_ cle 9077   - cmin 9247   ZZcz 10238   ZZ>=cuz 10444   RR+crp 10568   ...cfz 10999   seq cseq 11278   abscabs 11994   ~~> cli 12233   sum_csu 12434   ~~> uculm 20245

This theorem is referenced by:  pserulm  20291  lgamgulmlem6  24771

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025  ax-mulf 9026

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  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-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-oi 7435  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-rp 10569  df-ico 10878  df-fz 11000  df-fzo 11091  df-fl 11157  df-seq 11279  df-exp 11338  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-limsup 12220  df-clim 12237  df-rlim 12238  df-sum 12435  df-ulm 20246