Theorem isum1p 7149

Description: The infinite sum of a converging infinite series equals the first term plus the infinite sum of the rest of it.

Hypothesis

Ref	Expression
isum1p.1	|- F e. V

Assertion

Ref	Expression
isum1p	|- ((M e. ZZ /\ A.k e. (ZZ>` M)(F` k) e. CC /\ E.x(<.(M + 1), + >. seq F) ~~> x) -> sum_k e. (ZZ>` M)(F` k) = ((F` M) + sum_k e. (ZZ>` (M + 1))(F` k)))

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

Proof of Theorem isum1p

Step	Hyp	Ref	Expression
1		isum1p.1	. . . . . . 7 |- F e. V
2	1	isumclim2t 7142	. . . . . 6 |- (((M + 1) e. ZZ /\ E.x(<.(M + 1), + >. seq F) ~~> x) -> (<.(M + 1), + >. seq F) ~~> sum_k e. (ZZ>` (M + 1))(F` k))
3		peano2z 6121	. . . . . 6 |- (M e. ZZ -> (M + 1) e. ZZ)
4	2, 3	sylan 448	. . . . 5 |- ((M e. ZZ /\ E.x(<.(M + 1), + >. seq F) ~~> x) -> (<.(M + 1), + >. seq F) ~~> sum_k e. (ZZ>` (M + 1))(F` k))
5	4	adantlr 393	. . . 4 |- (((M e. ZZ /\ A.j e. (ZZ>` M)(F` j) e. CC) /\ E.x(<.(M + 1), + >. seq F) ~~> x) -> (<.(M + 1), + >. seq F) ~~> sum_k e. (ZZ>` (M + 1))(F` k))
6		oprex 3974	. . . . . 6 |- ((F` M) + sum_k e. (ZZ>` (M + 1))(F` k)) e. V
7	1, 6	isumclimt 7140	. . . . 5 |- ((M e. ZZ /\ (<.M, + >. seq F) ~~> ((F` M) + sum_k e. (ZZ>` (M + 1))(F` k))) -> sum_k e. (ZZ>` M)(F` k) = ((F` M) + sum_k e. (ZZ>` (M + 1))(F` k)))
8		simpll 412	. . . . 5 |- (((M e. ZZ /\ A.j e. (ZZ>` M)(F` j) e. CC) /\ (<.(M + 1), + >. seq F) ~~> sum_k e. (ZZ>` (M + 1))(F` k)) -> M e. ZZ)
9		oprex 3974	. . . . . . 7 |- (<.(M + 1), + >. seq F) e. V
10		oprex 3974	. . . . . . 7 |- (<.M, + >. seq F) e. V
11		sumex 6927	. . . . . . 7 |- sum_k e. (ZZ>` (M + 1))(F` k) e. V
12		fvex 3723	. . . . . . 7 |- (F` M) e. V
13	9, 10, 11, 12	climaddc2 7063	. . . . . 6 |- ((((<.(M + 1), + >. seq F) ~~> sum_k e. (ZZ>` (M + 1))(F` k) /\ (F` M) e. CC) /\ ((M + 1) e. ZZ /\ A.n e. (ZZ>` (M + 1))(((<.(M + 1), + >. seq F)` n) e. CC /\ ((<.M, + >. seq F)` n) = ((F` M) + ((<.(M + 1), + >. seq F)` n))))) -> (<.M, + >. seq F) ~~> ((F` M) + sum_k e. (ZZ>` (M + 1))(F` k)))
14		pm3.27 323	. . . . . 6 |- (((M e. ZZ /\ A.j e. (ZZ>` M)(F` j) e. CC) /\ (<.(M + 1), + >. seq F) ~~> sum_k e. (ZZ>` (M + 1))(F` k)) -> (<.(M + 1), + >. seq F) ~~> sum_k e. (ZZ>` (M + 1))(F` k))
15		fveq2 3715	. . . . . . . . . 10 |- (j = M -> (F` j) = (F` M))
16	15	eleq1d 1537	. . . . . . . . 9 |- (j = M -> ((F` j) e. CC <-> (F` M) e. CC))
17	16	rcla4va 1871	. . . . . . . 8 |- ((M e. (ZZ>` M) /\ A.j e. (ZZ>` M)(F` j) e. CC) -> (F` M) e. CC)
18		uzidt 6367	. . . . . . . 8 |- (M e. ZZ -> M e. (ZZ>` M))
19	17, 18	sylan 448	. . . . . . 7 |- ((M e. ZZ /\ A.j e. (ZZ>` M)(F` j) e. CC) -> (F` M) e. CC)
20	19	adantr 389	. . . . . 6 |- (((M e. ZZ /\ A.j e. (ZZ>` M)(F` j) e. CC) /\ (<.(M + 1), + >. seq F) ~~> sum_k e. (ZZ>` (M + 1))(F` k)) -> (F` M) e. CC)
21	3	ad2antrr 404	. . . . . 6 |- (((M e. ZZ /\ A.j e. (ZZ>` M)(F` j) e. CC) /\ (<.(M + 1), + >. seq F) ~~> sum_k e. (ZZ>` (M + 1))(F` k)) -> (M + 1) e. ZZ)
22	1	serzclt 6991	. . . . . . . . . 10 |- ((n e. (ZZ>` (M + 1)) /\ A.j e. ((M + 1)...n)(F` j) e. CC) -> ((<.(M + 1), + >. seq F)` n) e. CC)
23		pm3.27 323	. . . . . . . . . 10 |- (((M e. ZZ /\ A.j e. (ZZ>` M)(F` j) e. CC) /\ n e. (ZZ>` (M + 1))) -> n e. (ZZ>` (M + 1)))
24		peano2uzr 6388	. . . . . . . . . . . . . . . 16 |- ((M e. ZZ /\ j e. (ZZ>` (M + 1))) -> j e. (ZZ>` M))
25	24	ex 373	. . . . . . . . . . . . . . 15 |- (M e. ZZ -> (j e. (ZZ>` (M + 1)) -> j e. (ZZ>` M)))
26		elfzuzt 6428	. . . . . . . . . . . . . . 15 |- (j e. ((M + 1)...n) -> j e. (ZZ>` (M + 1)))
27	25, 26	syl5 21	. . . . . . . . . . . . . 14 |- (M e. ZZ -> (j e. ((M + 1)...n) -> j e. (ZZ>` M)))
28	27	imim1d 28	. . . . . . . . . . . . 13 |- (M e. ZZ -> ((j e. (ZZ>` M) -> (F` j) e. CC) -> (j e. ((M + 1)...n) -> (F` j) e. CC)))
29	28	r19.20dv2 1708	. . . . . . . . . . . 12 |- (M e. ZZ -> (A.j e. (ZZ>` M)(F` j) e. CC -> A.j e. ((M + 1)...n)(F` j) e. CC))
30	29	a1dd 42	. . . . . . . . . . 11 |- (M e. ZZ -> (A.j e. (ZZ>` M)(F` j) e. CC -> (n e. (ZZ>` (M + 1)) -> A.j e. ((M + 1)...n)(F` j) e. CC)))
31	30	imp31 362	. . . . . . . . . 10 |- (((M e. ZZ /\ A.j e. (ZZ>` M)(F` j) e. CC) /\ n e. (ZZ>` (M + 1))) -> A.j e. ((M + 1)...n)(F` j) e. CC)
32	22, 23, 31	sylanc 471	. . . . . . . . 9 |- (((M e. ZZ /\ A.j e. (ZZ>` M)(F` j) e. CC) /\ n e. (ZZ>` (M + 1))) -> ((<.(M + 1), + >. seq F)` n) e. CC)
33	1	serz1p 6998	. . . . . . . . . . . . 13 |- ((n e. (ZZ>` M) /\ M < n /\ A.j e. (M...n)(F` j) e. CC) -> ((<.M, + >. seq F)` n) = ((F` M) + ((<.(M + 1), + >. seq F)` n)))
34	33	3expa 832	. . . . . . . . . . . 12 |- (((n e. (ZZ>` M) /\ M < n) /\ A.j e. (M...n)(F` j) e. CC) -> ((<.M, + >. seq F)` n) = ((F` M) + ((<.(M + 1), + >. seq F)` n)))
35		peano2uzr 6388	. . . . . . . . . . . . 13 |- ((M e. ZZ /\ n e. (ZZ>` (M + 1))) -> n e. (ZZ>` M))
36		eluzp1lt 6374	. . . . . . . . . . . . 13 |- ((M e. ZZ /\ n e. (ZZ>` (M + 1))) -> M < n)
37	35, 36	jca 288	. . . . . . . . . . . 12 |- ((M e. ZZ /\ n e. (ZZ>` (M + 1))) -> (n e. (ZZ>` M) /\ M < n))
38	34, 37	sylan 448	. . . . . . . . . . 11 |- (((M e. ZZ /\ n e. (ZZ>` (M + 1))) /\ A.j e. (M...n)(F` j) e. CC) -> ((<.M, + >. seq F)` n) = ((F` M) + ((<.(M + 1), + >. seq F)` n)))
39	38	an1rs 489	. . . . . . . . . 10 |- (((M e. ZZ /\ A.j e. (M...n)(F` j) e. CC) /\ n e. (ZZ>` (M + 1))) -> ((<.M, + >. seq F)` n) = ((F` M) + ((<.(M + 1), + >. seq F)` n)))
40		elfzuzt 6428	. . . . . . . . . . . 12 |- (j e. (M...n) -> j e. (ZZ>` M))
41	40	imim1i 16	. . . . . . . . . . 11 |- ((j e. (ZZ>` M) -> (F` j) e. CC) -> (j e. (M...n) -> (F` j) e. CC))
42	41	r19.20i2 1700	. . . . . . . . . 10 |- (A.j e. (ZZ>` M)(F` j) e. CC -> A.j e. (M...n)(F` j) e. CC)
43	39, 42	sylanl2 461	. . . . . . . . 9 |- (((M e. ZZ /\ A.j e. (ZZ>` M)(F` j) e. CC) /\ n e. (ZZ>` (M + 1))) -> ((<.M, + >. seq F)` n) = ((F` M) + ((<.(M +