HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem fnsmnt 7161
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
StepHypRef Expression
1 fnsmnt.1 . . . . . . . . . . 11 |- N e. NN
21nnnn0 6054 . . . . . . . . . 10 |- N e. NN0
3 elnn0uz 6373 . . . . . . . . . 10 |- (N e. NN0 <-> N e. (ZZ>` 0))
42, 3mpbi 189 . . . . . . . . 9 |- N e. (ZZ>` 0)
5 ax1cn 5241 . . . . . . . . 9 |- 1 e. CC
6 fsumconst 6976 . . . . . . . . 9 |- ((N e. (ZZ>` 0) /\ 1 e. CC) -> sum_k e. (0...N)1 = (((N - 0) + 1) x. 1))
74, 5, 6mp2an 695 . . . . . . . 8 |- sum_k e. (0...N)1 = (((N - 0) + 1) x. 1)
81nncn 5880 . . . . . . . . . . 11 |- N e. CC
9 0cn 5300 . . . . . . . . . . 11 |- 0 e. CC
108, 9subcl 5338 . . . . . . . . . 10 |- (N - 0) e. CC
1110, 5addcl 5292 . . . . . . . . 9 |- ((N - 0) + 1) e. CC
1211mulid1 5304 . . . . . . . 8 |- (((N - 0) + 1) x. 1) = ((N - 0) + 1)
138subid1 5364 . . . . . . . . 9 |- (N - 0) = N
1413opreq1i 3956 . . . . . . . 8 |- ((N - 0) + 1) = (N + 1)
157, 12, 143eqtrr 1492 . . . . . . 7 |- (N + 1) = sum_k e. (0...N)1
1615opreq2i 3957 . . . . . 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 5927 . . . . . . . 8 |- 2 e. CC
18 elfzelz 6414 . . . . . . . . . 10 |- (k e. (0...N) -> k e. ZZ)
19 zcnt 6087 . . . . . . . . . 10 |- (k e. ZZ -> k e. CC)
2018, 19syl 10 . . . . . . . . 9 |- (k e. (0...N) -> k e. CC)
2120rgen 1690 . . . . . . . 8 |- A.k e. (0...N)k e. CC
22 fsummulc1 6971 . . . . . . . 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))
234, 17, 21, 22mp3an 913 . . . . . . 7 |- (2 x. sum_k e. (0...N)k) = sum_k e. (0...N)(2 x. k)
2423opreq1i 3956 . . . . . 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 5883 . . . . . . . . . . 11 |- (N e. NN -> (N + 1) e. NN)
261, 25ax-mp 7 . . . . . . . . . 10 |- (N + 1) e. NN
2726nnnn0 6054 . . . . . . . . 9 |- (N + 1) e. NN0
28 elfznn0t 6428 . . . . . . . . . . 11 |- (k e. (0...(N + 1)) -> k e. NN0)
29 nn0cnt 6056 . . . . . . . . . . 11 |- (k e. NN0 -> k e. CC)
30 sqclt 6542 . . . . . . . . . . 11 |- (k e. CC -> (k^2) e. CC)
3128, 29, 303syl 20 . . . . . . . . . 10 |- (k e. (0...(N + 1)) -> (k^2) e. CC)
3231rgen 1690 . . . . . . . . 9 |- A.k e. (0...(N + 1))(k^2) e. CC
33 fsum0clt 6954 . . . . . . . . 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)
3427, 32, 33mp2an 695 . . . . . . . 8 |- sum_k e. (0...(N + 1))(k^2) e. CC
35 elfznn0t 6428 . . . . . . . . . . 11 |- (k e. (0...N) -> k e. NN0)
3635, 29, 303syl 20 . . . . . . . . . 10 |- (k e. (0...N) -> (k^2) e. CC)
3736rgen 1690 . . . . . . . . 9 |- A.k e. (0...N)(k^2) e. CC
38 fsum0clt 6954 . . . . . . . . 9 |- ((N e. NN0 /\ A.k e. (0...N)(k^2) e. CC) -> sum_k e. (0...N)(k^2) e. CC)
392, 37, 38mp2an 695 . . . . . . . 8 |- sum_k e. (0...N)(k^2) e. CC
4035, 29syl 10 . . . . . . . . . . . . 13 |- (k e. (0...N) -> k e. CC)
4140, 17jctil 292 . . . . . . . . . . . 12 |- (k e. (0...N) -> (2 e. CC /\ k e. CC))
42 axmulcl 5245 . . . . . . . . . . . 12 |- ((2 e. CC /\ k e. CC) -> (2 x. k) e. CC)
4341, 42syl 10 . . . . . . . . . . 11 |- (k e. (0...N) -> (2 x. k) e. CC)
4443rgen 1690 . . . . . . . . . 10 |- A.k e. (0...N)(2 x. k) e. CC
45 fsum0clt 6954 . . . . . . . . . 10 |- ((N e. NN0 /\ A.k e. (0...N)(2 x. k) e. CC) -> sum_k e. (0...N)(2 x. k) e. CC)
462, 44, 45mp2an 695 . . . . . . . . 9 |- sum_k e. (0...N)(2 x. k) e. CC
475a1i 8 . . . . . . . . . . 11 |- (k e. (0...N) -> 1 e. CC)
4847rgen 1690 . . . . . . . . . 10 |- A.k e. (0...N)1 e. CC
49 fsum0clt 6954 . . . . . . . . . 10 |- ((N e. NN0 /\ A.k e. (0...N)1 e. CC) -> sum_k e. (0...N)1 e. CC)
502, 48, 49mp2an 695 . . . . . . . . 9 |- sum_k e. (0...N)1 e. CC
5146, 50addcl 5292 . . . . . . . 8 |- (sum_k e. (0...N)(2 x. k) + sum_k e. (0...N)1) e. CC
52 binom2t 6581 . . . . . . . . . . . . . 14 |- ((k e. CC /\ 1 e. CC) -> ((k + 1)^2) = (((k^2) + (2 x. (k x. 1))) + (1^2)))
535, 52mpan2 694 . . . . . . . . . . . . 13 |- (k e. CC -> ((k + 1)^2) = (((k^2) + (2 x. (k x. 1))) + (1^2)))
54 ax1id 5254 . . . . . . . . . . . . . . . 16 |- (k e. CC -> (k x. 1) = k)
5554opreq2d 3961 . . . . . . . . . . . . . . 15 |- (k e. CC -> (2 x. (k x. 1)) = (2 x. k))
5655opreq2d 3961 . . . . . . . . . . . . . 14 |- (k e. CC -> ((k^2) + (2 x. (k x. 1))) = ((k^2) + (2 x. k)))
57 sq1 6568 . . . . . . . . . . . . . . 15 |- (1^2) = 1
5857a1i 8 . . . . . . . . . . . . . 14 |- (k e. CC -> (1^2) = 1)
5956, 58opreq12d 3963 . . . . . . . . . . . . 13 |- (k e. CC -> (((k^2) + (2 x. (k x. 1))) + (1^2)) = (((k^2) + (2 x. k)) + 1))
6053, 59eqtrd 1499 . . . . . . . . . . . 12 |- (k e. CC -> ((k + 1)^2) = (((k^2) + (2 x. k)) + 1))
6135, 29, 603syl 20 . . . . . . . . . . 11 |- (k e. (0...N) -> ((k + 1)^2) = (((k^2) + (2 x. k)) + 1))
6261sumeq2i 6926 . . . . . . . . . 10 |- sum_k e. (0...N)((k + 1)^2) = sum_k e. (0...N)(((k^2) + (2 x. k)) + 1)
63 axaddcl 5243 . . . . . . . . . . . . . 14 |- (((k^2) e. CC /\ (2 x. k) e. CC) -> ((k^2) + (2 x. k)) e. CC)
6463, 36, 43sylanc 471 . . . . . . . . . . . . 13 |- (k e. (0...N) -> ((k^2) + (2 x. k)) e. CC)
6564, 5jctir 293 . . . . . . . . . . . 12 |- (k e. (0...N) -> (((k^2) + (2 x. k)) e. CC /\ 1 e. CC))
6665rgen 1690 . . . . . . . . . . 11 |- A.k e. (0...N)(((k^2) + (2 x. k)) e. CC /\ 1 e. CC)
67 fsumadd 6960 . . . . . . . . . . 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))
684, 66, 67mp2an 695 . . . . . . . . . 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)
6936, 43jca 288 . . . . . . . . . . . 12 |- (k e. (0...N) -> ((k^2) e. CC /\ (2 x. k) e. CC))
7069rgen 1690 . . . . . . . . . . 11 |- A.k e. (0...N)((k^2) e. CC /\ (2 x. k) e. CC)
71 fsumadd 6960 . . . . . . . . . . . 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)))
7271opreq1d 3960 . . . . . . . . . . 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))
734, 70, 72mp2an 695 . . . . . . . . . 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. (