Theorem isum1p 7296

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	isumclim2 7289	. . . . . 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 6248	. . . . . 6 |- (M e. ZZ -> (M + 1) e. ZZ)
4	2, 3	sylan 459	. . . . 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 402	. . . 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 4041	. . . . . 6 |- ((F` M) + sum_k e. (ZZ>` (M + 1))(F` k)) e. V
7	1, 6	isumclim 7286	. . . . 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 421	. . . . 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 4041	. . . . . . 7 |- (<.(M + 1), + >. seq F) e. V
10		oprex 4041	. . . . . . 7 |- (<.M, + >. seq F) e. V
11		sumex 7071	. . . . . . 7 |- sum_k e. (ZZ>` (M + 1))(F` k) e. V
12		fvex 3789	. . . . . . 7 |- (F` M) e. V
13	9, 10, 11, 12	climaddc2 7209	. . . . . 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 330	. . . . . 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 3781	. . . . . . . . . 10 |- (j = M -> (F` j) = (F` M))
16	15	eleq1d 1587	. . . . . . . . 9 |- (j = M -> ((F` j) e. CC <-> (F` M) e. CC))
17	16	rcla4va 1922	. . . . . . . 8 |- ((M e. (ZZ>` M) /\ A.j e. (ZZ>` M)(F` j) e. CC) -> (F` M) e. CC)
18		uzid 6453	. . . . . . . 8 |- (M e. ZZ -> M e. (ZZ>` M))
19	17, 18	sylan 459	. . . . . . 7 |- ((M e. ZZ /\ A.j e. (ZZ>` M)(F` j) e. CC) -> (F` M) e. CC)
20	19	adantr 398	. . . . . 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 413	. . . . . 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	serzcl 7135	. . . . . . . . . 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 330	. . . . . . . . . 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 6474	. . . . . . . . . . . . . . . 16 |- ((M e. ZZ /\ j e. (ZZ>` (M + 1))) -> j e. (ZZ>` M))
25	24	ex 380	. . . . . . . . . . . . . . 15 |- (M e. ZZ -> (j e. (ZZ>` (M + 1)) -> j e. (ZZ>` M)))
26		elfzuz 6514	. . . . . . . . . . . . . . 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 1758	. . . . . . . . . . . 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 369	. . . . . . . . . 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 482	. . . . . . . . 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 7142	. . . . . . . . . . . . 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 845	. . . . . . . . . . . 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 6474	. . . . . . . . . . . . 13 |- ((M e. ZZ /\ n e. (ZZ>` (M + 1))) -> n e. (ZZ>` M))
36		eluzp1l 6460	. . . . . . . . . . . . 13 |- ((M e. ZZ /\ n e. (ZZ>` (M + 1))) -> M < n)
37	35, 36	jca 295	. . . . . . . . . . . 12 |- ((M e. ZZ /\ n e. (ZZ>` (M + 1))) -> (n e. (ZZ>` M) /\ M < n))
38	34, 37	sylan 459	. . . . . . . . . . 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 500	. . . . . . . . . 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		elfzuz 6514	. . . . . . . . . . . 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 1750	. . . . . . . . . 10 |- (A.j e. (ZZ>` M)(F` j) e. CC -> A.j e. (M...n)(F` j) e. CC)
43	39, 42	sylanl2 472	. . . . . . . . 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 + 1