Theorem fnsmnt 7169

Description: Arithmetic series sum of the first (N + 1) non-negative integers. (Contributed by FL, 10-Dec-2006.)

Hypothesis

Ref	Expression
fnsmnt.1	|- N e. NN

Assertion

Ref	Expression
fnsmnt	|- sum_k e. (0...N)k = ((((N + 1)^2) - (N + 1)) / 2)

Distinct variable group:   k,N

Proof of Theorem fnsmnt

Step	Hyp	Ref	Expression
1		fnsmnt.1	. . . . . . . . . . 11 |- N e. NN
2	1	nnnn0 6062	. . . . . . . . . 10 |- N e. NN0
3		elnn0uz 6381	. . . . . . . . . 10 |- (N e. NN0 <-> N e. (ZZ>` 0))
4	2, 3	mpbi 189	. . . . . . . . 9 |- N e. (ZZ>` 0)
5		ax1cn 5249	. . . . . . . . 9 |- 1 e. CC
6		fsumconst 6984	. . . . . . . . 9 |- ((N e. (ZZ>` 0) /\ 1 e. CC) -> sum_k e. (0...N)1 = (((N - 0) + 1) x. 1))
7	4, 5, 6	mp2an 696	. . . . . . . 8 |- sum_k e. (0...N)1 = (((N - 0) + 1) x. 1)
8	1	nncn 5888	. . . . . . . . . . 11 |- N e. CC
9		0cn 5308	. . . . . . . . . . 11 |- 0 e. CC
10	8, 9	subcl 5346	. . . . . . . . . 10 |- (N - 0) e. CC
11	10, 5	addcl 5300	. . . . . . . . 9 |- ((N - 0) + 1) e. CC
12	11	mulid1 5312	. . . . . . . 8 |- (((N - 0) + 1) x. 1) = ((N - 0) + 1)
13	8	subid1 5372	. . . . . . . . 9 |- (N - 0) = N
14	13	opreq1i 3962	. . . . . . . 8 |- ((N - 0) + 1) = (N + 1)
15	7, 12, 14	3eqtrr 1497	. . . . . . 7 |- (N + 1) = sum_k e. (0...N)1
16	15	opreq2i 3963	. . . . . 6 |- ((2 x. sum_k e. (0...N)k) + (N + 1)) = ((2 x. sum_k e. (0...N)k) + sum_k e. (0...N)1)
17		2cn 5935	. . . . . . . 8 |- 2 e. CC
18		elfzelz 6422	. . . . . . . . . 10 |- (k e. (0...N) -> k e. ZZ)
19		zcnt 6095	. . . . . . . . . 10 |- (k e. ZZ -> k e. CC)
20	18, 19	syl 10	. . . . . . . . 9 |- (k e. (0...N) -> k e. CC)
21	20	rgen 1695	. . . . . . . 8 |- A.k e. (0...N)k e. CC
22		fsummulc1 6979	. . . . . . . 8 |- ((N e. (ZZ>` 0) /\ 2 e. CC /\ A.k e. (0...N)k e. CC) -> (2 x. sum_k e. (0...N)k) = sum_k e. (0...N)(2 x. k))
23	4, 17, 21, 22	mp3an 914	. . . . . . 7 |- (2 x. sum_k e. (0...N)k) = sum_k e. (0...N)(2 x. k)
24	23	opreq1i 3962	. . . . . 6 |- ((2 x. sum_k e. (0...N)k) + sum_k e. (0...N)1) = (sum_k e. (0...N)(2 x. k) + sum_k e. (0...N)1)
25		peano2nn 5891	. . . . . . . . . . 11 |- (N e. NN -> (N + 1) e. NN)
26	1, 25	ax-mp 7	. . . . . . . . . 10 |- (N + 1) e. NN
27	26	nnnn0 6062	. . . . . . . . 9 |- (N + 1) e. NN0
28		elfznn0t 6436	. . . . . . . . . . 11 |- (k e. (0...(N + 1)) -> k e. NN0)
29		nn0cnt 6064	. . . . . . . . . . 11 |- (k e. NN0 -> k e. CC)
30		sqclt 6550	. . . . . . . . . . 11 |- (k e. CC -> (k^2) e. CC)
31	28, 29, 30	3syl 20	. . . . . . . . . 10 |- (k e. (0...(N + 1)) -> (k^2) e. CC)
32	31	rgen 1695	. . . . . . . . 9 |- A.k e. (0...(N + 1))(k^2) e. CC
33		fsum0clt 6962	. . . . . . . . 9 |- (((N + 1) e. NN0 /\ A.k e. (0...(N + 1))(k^2) e. CC) -> sum_k e. (0...(N + 1))(k^2) e. CC)
34	27, 32, 33	mp2an 696	. . . . . . . 8 |- sum_k e. (0...(N + 1))(k^2) e. CC
35		elfznn0t 6436	. . . . . . . . . . 11 |- (k e. (0...N) -> k e. NN0)
36	35, 29, 30	3syl 20	. . . . . . . . . 10 |- (k e. (0...N) -> (k^2) e. CC)
37	36	rgen 1695	. . . . . . . . 9 |- A.k e. (0...N)(k^2) e. CC
38		fsum0clt 6962	. . . . . . . . 9 |- ((N e. NN0 /\ A.k e. (0...N)(k^2) e. CC) -> sum_k e. (0...N)(k^2) e. CC)
39	2, 37, 38	mp2an 696	. . . . . . . 8 |- sum_k e. (0...N)(k^2) e. CC
40	35, 29	syl 10	. . . . . . . . . . . . 13 |- (k e. (0...N) -> k e. CC)
41	40, 17	jctil 292	. . . . . . . . . . . 12 |- (k e. (0...N) -> (2 e. CC /\ k e. CC))
42		axmulcl 5253	. . . . . . . . . . . 12 |- ((2 e. CC /\ k e. CC) -> (2 x. k) e. CC)
43	41, 42	syl 10	. . . . . . . . . . 11 |- (k e. (0...N) -> (2 x. k) e. CC)
44	43	rgen 1695	. . . . . . . . . 10 |- A.k e. (0...N)(2 x. k) e. CC
45		fsum0clt 6962	. . . . . . . . . 10 |- ((N e. NN0 /\ A.k e. (0...N)(2 x. k) e. CC) -> sum_k e. (0...N)(2 x. k) e. CC)
46	2, 44, 45	mp2an 696	. . . . . . . . 9 |- sum_k e. (0...N)(2 x. k) e. CC
47	5	a1i 8	. . . . . . . . . . 11 |- (k e. (0...N) -> 1 e. CC)
48	47	rgen 1695	. . . . . . . . . 10 |- A.k e. (0...N)1 e. CC
49		fsum0clt 6962	. . . . . . . . . 10 |- ((N e. NN0 /\ A.k e. (0...N)1 e. CC) -> sum_k e. (0...N)1 e. CC)
50	2, 48, 49	mp2an 696	. . . . . . . . 9 |- sum_k e. (0...N)1 e. CC
51	46, 50	addcl 5300	. . . . . . . 8 |- (sum_k e. (0...N)(2 x. k) + sum_k e. (0...N)1) e. CC
52		binom2t 6589	. . . . . . . . . . . . . 14 |- ((k e. CC /\ 1 e. CC) -> ((k + 1)^2) = (((k^2) + (2 x. (k x. 1))) + (1^2)))
53	5, 52	mpan2 695	. . . . . . . . . . . . 13 |- (k e. CC -> ((k + 1)^2) = (((k^2) + (2 x. (k x. 1))) + (1^2)))
54		ax1id 5262	. . . . . . . . . . . . . . . 16 |- (k e. CC -> (k x. 1) = k)
55	54	opreq2d 3967	. . . . . . . . . . . . . . 15 |- (k e. CC -> (2 x. (k x. 1)) = (2 x. k))
56	55	opreq2d 3967	. . . . . . . . . . . . . 14 |- (k e. CC -> ((k^2) + (2 x. (k x. 1))) = ((k^2) + (2 x. k)))
57		sq1 6576	. . . . . . . . . . . . . . 15 |- (1^2) = 1
58	57	a1i 8	. . . . . . . . . . . . . 14 |- (k e. CC -> (1^2) = 1)
59	56, 58	opreq12d 3969	. . . . . . . . . . . . 13 |- (k e. CC -> (((k^2) + (2 x. (k x. 1))) + (1^2)) = (((k^2) + (2 x. k)) + 1))
60	53, 59	eqtrd 1504	. . . . . . . . . . . 12 |- (k e. CC -> ((k + 1)^2) = (((k^2) + (2 x. k)) + 1))
61	35, 29, 60	3syl 20	. . . . . . . . . . 11 |- (k e. (0...N) -> ((k + 1)^2) = (((k^2) + (2 x. k)) + 1))
62	61	sumeq2i 6934	. . . . . . . . . 10 |- sum_k e. (0...N)((k + 1)^2) = sum_k e. (0...N)(((k^2) + (2 x. k)) + 1)
63		axaddcl 5251	. . . . . . . . . . . . . 14 |- (((k^2) e. CC /\ (2 x. k) e. CC) -> ((k^2) + (2 x. k)) e. CC)
64	63, 36, 43	sylanc 471	. . . . . . . . . . . . 13 |- (k e. (0...N) -> ((k^2) + (2 x. k)) e. CC)
65	64, 5	jctir 293	. . . . . . . . . . . 12 |- (k e. (0...N) -> (((k^2) + (2 x. k)) e. CC /\ 1 e. CC))
66	65	rgen 1695	. . . . . . . . . . 11 |- A.k e. (0...N)(((k^2) + (2 x. k)) e. CC /\ 1 e. CC)
67		fsumadd 6968	. . . . . . . . . . 11 |- ((N e. (ZZ>` 0) /\ A.k e. (0...N)(((k^2) + (2 x. k)) e. CC /\ 1 e. CC)) -> sum_k e. (0...N)(((k^2) + (2 x. k)) + 1) = (sum_k e. (0...N)((k^2) + (2 x. k)) + sum_k e. (0...N)1))
68	4, 66, 67	mp2an 696	. . . . . . . . . 10 |- sum_k e. (0...N)(((k^2) + (2 x. k)) + 1) = (sum_k e. (0...N)((k^2) + (2 x. k)) + sum_k e. (0...N)1)
69	36, 43	jca 288	. . . . . . . . . . . 12 |- (k e. (0...N) -> ((k^2) e. CC /\ (2 x. k) e. CC))
70	69	rgen 1695	. . . . . . . . . . 11 |- A.k e. (0...N)((k^2) e. CC /\ (2 x. k) e. CC)
71		fsumadd 6968	. . . . . . . . . . . 12 |- ((N e. (ZZ>` 0) /\ A.k e. (0...N)((k^2) e. CC /\ (2 x. k) e. CC)) -> sum_k e. (0...N)((k^2) + (2 x. k)) = (sum_k e. (0...N)(k^2) + sum_k e. (0...N)(2 x. k)))
72	71	opreq1d 3966	. . . . . . . . . . 11 |- ((N e. (ZZ>` 0) /\ A.k e. (0...N)((k^2) e. CC /\ (2 x. k) e. CC)) -> (sum_k e. (0...N)((k^2) + (2 x. k)) + sum_k e. (0...N)1) = ((sum_k e. (0...N)(k^2) + sum_k e. (0...N)(2 x. k)) + sum_k e. (0...N)1))
73	4, 70, 72	mp2an 696	. . . . . . . . . 10 |- (sum_k e. (0...N)((k^2) + (2 x. k)) + sum_k e. (0...N)1) = ((sum_k e. (0...N)(k^2) + sum_k e. (0...N)(2 x. k)) + sum_k e. (