mmtheorems71 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10781

Statement List for Metamath Proof Explorer - 7001-7100 - Page 71 of 108

Type	Label	Description
Statement
Theorem	fsumser0f 7001	A finite sum expressed in terms of a partial sum of an infinite 0-based series.
|- F e. V   &   |- (x e. F -> A.k x e. F)   =>   |- (N e. NN0 -> sum_k e. (0...N)(F` k) = (( + seq0 F)` N))
Theorem	fsumser1f 7002	A finite sum expressed in terms of a partial sum of an infinite 1-based series.
|- F e. V   &   |- (x e. F -> A.k x e. F)   =>   |- (N e. NN -> sum_k e. (1...N)(F` k) = (( + seq1 F)` N))
Theorem	fsumserz2 7003	A finite sum expressed in terms of a partial sum of an infinite series.
|- A e. V   &   |- F = {<.k, y>. | (k e. (ZZ>` M) /\ y = A)}   =>   |- (N e. (ZZ>` M) -> sum_k e. (M...N)A = ((<.M, + >. seq F)` N))
Theorem	serzfsum 7004	An infinite series in terms of finite partial sums of A(k).
|- A e. V   &   |- F = {<.k, y>. | (k e. (ZZ>` M) /\ y = A)}   &   |- G = {<.n, z>. | (n e. (ZZ>` M) /\ z = sum_k e. (M...n)A)}   =>   |- (M e. ZZ -> (<.M, + >. seq F) = G)
Theorem	fsum1 7005	The finite sum of A(k) from k = M to M (i.e. a sum with only one term) is B i.e. A(M).
|- (k = M -> A = B)   =>   |- ((B e. C /\ M e. ZZ) -> sum_k e. (M...M)A = B)
Theorem	fsump1 7006	The addition of the next term in a finite sum of A(k) is the current term plus B i.e. A(N + 1).
|- A e. V   &   |- B e. V   &   |- (k = (N + 1) -> A = B)   =>   |- (N e. (ZZ>` M) -> sum_k e. (M...(N + 1))A = (sum_k e. (M...N)A + B))
Theorem	fsum1f 7007	The finite sum of a term A(k) from M to M (i.e. a sum with only one term) is A(M) = B, where k is effectively not free in B.
|- (x e. B -> A.k x e. B)   &   |- (k = M -> A = B)   =>   |- ((B e. C /\ M e. ZZ) -> sum_k e. (M...M)A = B)
Theorem	fsum1slem 7008	Lemma for fsum1s 7009.
Theorem	fsum1s 7009	The finite sum of a sequence A(k) from M to M (i.e. a sum with only one term) is A(M).
|- ((M e. ZZ /\ A.k e. (M...M)A e. B) -> sum_k e. (M...M)A = [_M / k]_A)
Theorem	fsum1s2 7010	The finite sum of a sequence A(k) from M to M (i.e. a sum with only one term) is A(M).
|- ((M e. ZZ /\ [_M / k]_A e. B) -> sum_k e. (M...M)A = [_M / k]_A)
Theorem	fsump1f 7011	The addition of the next term in a finite sum of A(k) is the previous term plus A(N + 1) = B.
|- A e. V   &   |- B e. V   &   |- (x e. B -> A.k x e. B)   &   |- (k = (N + 1) -> A = B)   =>   |- (N e. (ZZ>` M) -> sum_k e. (M...(N + 1))A = (sum_k e. (M...N)A + B))
Theorem	fsump1slem 7012	Lemma for fsump1s 7013.
Theorem	fsump1s 7013	The addition of the next term in a finite sum of A(k) is the previous term plus A(N + 1).
|- ((N e. (ZZ>` M) /\ A.k e. (M...(N + 1))A e. B) -> sum_k e. (M...(N + 1))A = (sum_k e. (M...N)A + [_(N + 1) / k]_A))
Theorem	fsumcllem 7014	- Lemma for finite sum closures. (The "-" before "Lemma" forces the math content to be displayed in the Statement List - NM 11-Feb-2008.)
|- ((x e. C /\ y e. C) -> (x + y) e. C)   =>   |- ((N e. (ZZ>` M) /\ A.k e. (M...N)A e. C) -> sum_k e. (M...N)A e. C)
Theorem	fsumclt 7015	Closure of a finite sum of complex numbers A(k).
|- ((N e. (ZZ>` M) /\ A.k e. (M...N)A e. CC) -> sum_k e. (M...N)A e. CC)
Theorem	fsum0clt 7016	Closure of a finite sum of complex numbers A(k), starting at index zero.
|- ((N e. NN0 /\ A.k e. (0...N)A e. CC) -> sum_k e. (0...N)A e. CC)
Theorem	fsumreclt 7017	Closure of a finite sum of reals.
|- ((N e. (ZZ>` M) /\ A.k e. (M...N)A e. RR) -> sum_k e. (M...N)A e. RR)
Theorem	fsum1ps 7018	Separate out the first term in a finite sum.
|- ((N e. (ZZ>` M) /\ M < N /\ A.k e. (M...N)A e. CC) -> sum_k e. (M...N)A = ([_M / k]_A + sum_k e. ((M + 1)...N)A))
Theorem	fsum1p 7019	Separate out the first term in a finite sum.
|- (k = M -> A = B)   =>   |- ((N e. (ZZ>` M) /\ M < N /\ A.k e. (M...N)A e. CC) -> sum_k e. (M...N)A = (B + sum_k e. ((M + 1)...N)A))
Theorem	fsumsplit 7020	Split a finite sum into two parts. Warning: The HTML proof page is 0.6 megabyte in size.
|- ((N e. ZZ /\ K e. (M...(N - 1)) /\ A.k e. (M...N)A e. CC) -> sum_k e. (M...N)A = (sum_k e. (M...K)A + sum_k e. ((K + 1)...N)A))
Theorem	fsum0split 7021	Split a finite sum into two parts.
|- ((N e. ZZ /\ K e. (1...N) /\ A.k e. (0...N)A e. CC) -> sum_k e. (0...N)A = (sum_k e. (0...(N - K))A + sum_k e. (((N - K) + 1)...N)A))
Theorem	fsumadd 7022	The sum of two finite sums.
|- ((N e. (ZZ>` M) /\ A.k e. (M...N)(A e. CC /\ B e. CC)) -> sum_k e. (M...N)(A + B) = (sum_k e. (M...N)A + sum_k e. (M...N)B))
Theorem	fsum2 7023	The sum of two terms.
|- A e. V   =>   |- (M e. ZZ -> sum_k e. (M...(M + 1))A = ([_M / k]_A + [_(M + 1) / k]_A))
Theorem	fsum3 7024	The sum of three terms.
|- A e. V   =>   |- (M e. ZZ -> sum_k e. (M...(M + 2))A = (([_M / k]_A + [_(M + 1) / k]_A) + [_(M + 2) / k]_A))
Theorem	fsum4 7025	The sum of four terms.
|- A e. V   =>   |- (M e. ZZ -> sum_k e. (M...(M + 3))A = ((([_M / k]_A + [_(M + 1) / k]_A) + [_(M + 2) / k]_A) + [_(M + 3) / k]_A))
Theorem	csbfsumlem 7026	Lemma for csbfsum 7027.
Theorem	csbfsum 7027	Distribute substitution for classes over a finite sum.
|- ((A e. C /\ N e. (ZZ>` M) /\ A.k e. (M...N)[_A / x]_B e. CC) -> [_A / x]_sum_k e. (M...N)B = sum_k e. (M...N)[_A / x]_B)
Theorem	fsumcom 7028	Interchange order of summation. Warning: The HTML proof page is 0.6MB in size.
|- ((K e. (ZZ>` J) /\ N e. (ZZ>` M) /\ A.j e. (J...K)A.m e. (M...N)A e. CC) -> sum_j e. (J...K)sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...K)A)
Theorem	fsumrev 7029	Reversal of a finite sum. Warning: The HTML proof page is 0.6 MB in size.
|- ((N e. (ZZ>` M) /\ K e. ZZ /\ A.j e. (M...N)A e. CC) -> sum_j e. (M...N)A = sum_k e. ((K - N)...(K - M))[_(K - k) / j]_A)
Theorem	fsumrev2 7030	Reversal of a finite sum.
|- ((N e. (ZZ>` M) /\ A.j e. (M...N)A e. CC) -> sum_j e. (M...N)A = sum_k e. (M...N)[_((M + N) - k) / j]_A)
Theorem	fsumshft 7031	Index shift of a finite sum.
|- ((N e. (ZZ>` M) /\ K e. ZZ /\ A.j e. (M...N)A e. CC) -> sum_j e. (M...N)A = sum_k e. ((M + K)...(N + K))[_(k - K) / j]_A)
Theorem	fsumshftm 7032	Negative index shift of a finite sum.
|- ((N e. (ZZ>` M) /\ K e. ZZ /\ A.j e. (M...N)A e. CC) -> sum_j e. (M...N)A = sum_k e. ((M - K)...(N - K))[_(k + K) / j]_A)