Theorem clim2serzt 7070

Description: The limit of an infinite series with an initial segment removed. (Contributed by Paul Chapman, 9-Feb-2007.)

Hypotheses

Ref	Expression
clim2serzt.1	|- A e. V
clim2serzt.2	|- F e. V

Assertion

Ref	Expression
clim2serzt	|- (((<.M, + >. seq F) ~~> A /\ N e. (ZZ>` M) /\ A.k e. (ZZ>` M)(F` k) e. CC) -> (<.(N + 1), + >. seq F) ~~> (A - ((<.M, + >. seq F)` N)))

Distinct variable groups:   k,F   k,M   k,N

Proof of Theorem clim2serzt

Step	Hyp	Ref	Expression
1		oprex 3968	. . . . . 6 |- (<.M, + >. seq F) e. V
2		oprex 3968	. . . . . 6 |- (<.(N + 1), + >. seq F) e. V
3		clim2serzt.1	. . . . . 6 |- A e. V
4		negex 5337	. . . . . 6 |- -u((<.M, + >. seq F)` N) e. V
5	1, 2, 3, 4	climaddc1 7054	. . . . 5 |- ((((<.M, + >. seq F) ~~> A /\ -u((<.M, + >. seq F)` N) e. CC) /\ ((N + 1) e. ZZ /\ A.n e. (ZZ>` (N + 1))(((<.M, + >. seq F)` n) e. CC /\ ((<.(N + 1), + >. seq F)` n) = (((<.M, + >. seq F)` n) + -u((<.M, + >. seq F)` N))))) -> (<.(N + 1), + >. seq F) ~~> (A + -u((<.M, + >. seq F)` N)))
6	5	anasss 440	. . . 4 |- (((<.M, + >. seq F) ~~> A /\ (-u((<.M, + >. seq F)` N) e. CC /\ ((N + 1) e. ZZ /\ A.n e. (ZZ>` (N + 1))(((<.M, + >. seq F)` n) e. CC /\ ((<.(N + 1), + >. seq F)` n) = (((<.M, + >. seq F)` n) + -u((<.M, + >. seq F)` N)))))) -> (<.(N + 1), + >. seq F) ~~> (A + -u((<.M, + >. seq F)` N)))
7		clim2serzt.2	. . . . . . . 8 |- F e. V
8	7	serzclt 6983	. . . . . . 7 |- ((N e. (ZZ>` M) /\ A.k e. (M...N)(F` k) e. CC) -> ((<.M, + >. seq F)` N) e. CC)
9		negclt 5340	. . . . . . 7 |- (((<.M, + >. seq F)` N) e. CC -> -u((<.M, + >. seq F)` N) e. CC)
10	8, 9	syl 10	. . . . . 6 |- ((N e. (ZZ>` M) /\ A.k e. (M...N)(F` k) e. CC) -> -u((<.M, + >. seq F)` N) e. CC)
11		elfzuzt 6420	. . . . . . . 8 |- (k e. (M...N) -> k e. (ZZ>` M))
12	11	imim1i 16	. . . . . . 7 |- ((k e. (ZZ>` M) -> (F` k) e. CC) -> (k e. (M...N) -> (F` k) e. CC))
13	12	r19.20i2 1695	. . . . . 6 |- (A.k e. (ZZ>` M)(F` k) e. CC -> A.k e. (M...N)(F` k) e. CC)
14	10, 13	sylan2 451	. . . . 5 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)(F` k) e. CC) -> -u((<.M, + >. seq F)` N) e. CC)
15		eluzelz 6355	. . . . . . . 8 |- (N e. (ZZ>` M) -> N e. ZZ)
16	15	peano2zd 6114	. . . . . . 7 |- (N e. (ZZ>` M) -> (N + 1) e. ZZ)
17	16	adantr 389	. . . . . 6 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)(F` k) e. CC) -> (N + 1) e. ZZ)
18		peano2uz 6379	. . . . . . . . . 10 |- (N e. (ZZ>` M) -> (N + 1) e. (ZZ>` M))
19		uztrn 6360	. . . . . . . . . . 11 |- ((n e. (ZZ>` (N + 1)) /\ (N + 1) e. (ZZ>` M)) -> n e. (ZZ>` M))
20	19	expcom 374	. . . . . . . . . 10 |- ((N + 1) e. (ZZ>` M) -> (n e. (ZZ>` (N + 1)) -> n e. (ZZ>` M)))
21	18, 20	syl 10	. . . . . . . . 9 |- (N e. (ZZ>` M) -> (n e. (ZZ>` (N + 1)) -> n e. (ZZ>` M)))
22	7	serzcl2t 6987	. . . . . . . . . 10 |- ((n e. (ZZ>` M) /\ A.k e. (ZZ>` M)(F` k) e. CC) -> ((<.M, + >. seq F)` n) e. CC)
23	22	expcom 374	. . . . . . . . 9 |- (A.k e. (ZZ>` M)(F` k) e. CC -> (n e. (ZZ>` M) -> ((<.M, + >. seq F)` n) e. CC))
24	21, 23	sylan9 468	. . . . . . . 8 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)(F` k) e. CC) -> (n e. (ZZ>` (N + 1)) -> ((<.M, + >. seq F)` n) e. CC))
25	7	serzcl2t 6987	. . . . . . . . . . . . 13 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)(F` k) e. CC) -> ((<.M, + >. seq F)` N) e. CC)
26	24, 25	jctird 600	. . . . . . . . . . . 12 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)(F` k) e. CC) -> (n e. (ZZ>` (N + 1)) -> (((<.M, + >. seq F)` n) e. CC /\ ((<.M, + >. seq F)` N) e. CC)))
27		negsubt 5354	. . . . . . . . . . . 12 |- ((((<.M, + >. seq F)` n) e. CC /\ ((<.M, + >. seq F)` N) e. CC) -> (((<.M, + >. seq F)` n) + -u((<.M, + >. seq F)` N)) = (((<.M, + >. seq F)` n) - ((<.M, + >. seq F)` N)))
28	26, 27	syl6 22	. . . . . . . . . . 11 |- ((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)(F` k) e. CC) -> (n e. (ZZ>` (N + 1)) -> (((<.M, + >. seq F)` n) + -u((<.M, + >. seq F)` N)) = (((<.M, + >. seq F)` n) - ((<.M, + >. seq F)` N))))
29	28	imp 350	. . . . . . . . . 10 |- (((N e. (ZZ>` M) /\ A.k e. (ZZ>` M)(F` k) e. CC) /\ n e. (ZZ>` (N + 1))) -> (((<.M, + >. seq F)` n) + -u((<.M, + >. seq F)` N)) = (((<.M, + >. seq F)` n) - ((<.M, + >. seq F)` N)))
30		eluzp1m1t 6365	. . . . . . . . . . . . . . . . . . 19 |- ((N e. ZZ /\ n e. (ZZ>` (N + 1))) -> (n - 1) e. (ZZ>` N))
31	30, 15	sylan 448	. . . . . . . . . . . . . . . . . 18 |- ((N e. (ZZ>` M) /\ n e. (ZZ>` (N + 1))) -> (n - 1) e. (ZZ>` N))
32		eluzfzt 6409	. . . . . . . . . . . . . . . . . 18 |- ((N e. (ZZ>` M) /\ (n - 1) e. (ZZ>` N)) -> N e. (M...(n - 1)))
33	31, 32	syldan 467	. . . . . . . . . . . . . . . . 17 |- ((N e. (ZZ>` M) /\ n e. (ZZ>` (N + 1))) -> N e. (M...(n - 1)))
34	33	ancoms 436	. . . . . . . . . . . . . . . 16 |- ((n e. (ZZ>` (N + 1)) /\ N e. (ZZ>` M)) -> N e. (M...(n - 1)))
35	7	serzsplit 6994	. . . . . . . . . . . . . . . . . . 19 |- ((n e. ZZ /\ N e. (M...(n - 1)) /\ A.k e. (M...n)(F` k) e. CC) -> ((<.M, + >. seq F)` n) = (((<.M, + >. seq F)` N) + ((<.(N + 1), + >. seq F)` n)))
36		eluzelz 6355	. . . . . . . . . . . . . . . . . . 19 |- (n e. (ZZ>` (N + 1)) -> n e. ZZ)
37	35, 36	syl3an1 857	. . . . . . . . . . . . . . . . . 18 |- ((n e. (ZZ>` (N + 1)) /\ N e. (M...(n - 1)) /\ A.k e. (M...n)(F` k) e. CC) -> ((<.M, + >. seq F)` n) = (((<.M, + >. seq F)` N) + ((<.(N + 1), + >. seq F)` n)))
38	37	eqcomd 1472	. . . . . . . . . . . . . . . . 17 |- ((n e. (ZZ>` (N + 1)) /\ N e. (M...(n - 1)) /\ A.k e. (M...n)(F` k) e. CC) -> (((<.M, + >. seq F)` N) + ((<.(N + 1), + >. seq F)` n)) = ((<.M, + >. seq F)` n))
39	38	3expia 833	. . . . . . . . . . . . . . . 16 |- ((n e. (ZZ>` (N + 1)) /\ N e. (M...(n - 1))) -> (A.k e. (M...n)(F` k) e. CC -> (((<.M, + >. seq F)` N) + ((<.(N + 1), + >. seq F)` n)) = ((<.M, + >. seq F)` n)))
40	34, 39	syldan 467	. . . . . . . . . . . . . . 15 |- ((n e. (ZZ>` (N + 1)) /\ N e. (ZZ>` M)) -> (A.k e. (M...n)(F` k) e. CC -> (((<.M