mmtheorems73 - Metamath Proof Explorer

Home	Metamath Proof Explorer	< Previous Next >
		Browser slow? Try the Unicode version.

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-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Color key:

Metamath Proof Explorer
(1-9062)

Hilbert Space Explorer
(9063-10650)

Users' Mathboxes
(10651-12229)

**Statement List for Metamath Proof Explorer -** 7201-7300 - Page 73 of 123
Type	Label	Description
Statement

Finite sums (cont.)

Theorem	dffsum 7201	Special case of series sum over a finite index set.


Theorem	fsumserz 7202	A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition of follows as fsum1i 7208 and fsump1i 7209, which should make our notation clear and from which, along with closure fsumcl 7218, we will derive the basic properties of finite sums.


Theorem	fsumserzfi 7203	Version of fsumserz 7202 with a bound-variable hypothesis instead of a distinct variable condition.


Theorem	fsumser0fi 7204	A finite sum expressed in terms of a partial sum of an infinite 0-based series.


Theorem	fsumser1fi 7205	A finite sum expressed in terms of a partial sum of an infinite 1-based series.


Theorem	fsumserz2 7206	A finite sum expressed in terms of a partial sum of an infinite series.
$/\$

Theorem	serzfsum 7207	An infinite series in terms of finite partial sums of .
$/\$ $/\$

Theorem	fsum1i 7208	The finite sum of from to (i.e. a sum with only one term) is i.e. .
$/\$

Theorem	fsump1i 7209	The addition of the next term in a finite sum of is the current term plus i.e. .


Theorem	fsum1fi 7210	The finite sum of a term from to (i.e. a sum with only one term) is , where is effectively not free in .
$/\$

Theorem	fsum1slem 7211	Lemma for fsum1s 7212.

Theorem	fsum1s 7212	The finite sum of a sequence from to (i.e. a sum with only one term) is .
$/\$

Theorem	fsum1s2 7213	The finite sum of a sequence from to (i.e. a sum with only one term) is .
$/\$

Theorem	fsump1fi 7214	The addition of the next term in a finite sum of is the previous term plus .


Theorem	fsump1slem 7215	Lemma for fsump1s 7216.

Theorem	fsump1s 7216	The addition of the next term in a finite sum of is the previous term plus .
$/\$

Theorem	fsumcllem 7217	- Lemma for finite sum closures. (The "-" before "Lemma" forces the math content to be displayed in the Statement List - NM 11-Feb-2008.)
$/\$ $/\$

Theorem	fsumcl 7218	Closure of a finite sum of complex numbers .
$/\$

Theorem	fsum0cl 7219	Closure of a finite sum of complex numbers , starting at index zero.
$/\$

Theorem	fsumrecl 7220	Closure of a finite sum of reals.
$/\$

Theorem	fsum1ps 7221	Separate out the first term in a finite sum.
$/\$ $/\$

Theorem	fsum1p 7222	Separate out the first term in a finite sum.
$/\$ $/\$

Theorem	fsumsplit 7223	Split a finite sum into two parts. Warning: The HTML proof page is 0.6 megabyte in size.
$/\$ $/\$

Theorem	fsum0split 7224	Split a finite sum into two parts.
$/\$ $/\$

Theorem	fsumadd 7225	The sum of two finite sums.
$/\$ $/\$

Theorem	fsum2 7226	The sum of two terms.


Theorem	fsum3 7227	The sum of three terms.


Theorem	fsum4 7228	The sum of four terms.


Theorem	csbfsumlem 7229	Lemma for csbfsum 7230.

Theorem	csbfsum 7230	Distribute substitution for classes over a finite sum.
$/\$ $/\$

Theorem	fsumcom 7231	Interchange order of summation. Warning: The HTML proof page is 0.6MB in size.
$/\$ $/\$

Theorem	fsumrev 7232	Reversal of a finite sum. Warning: The HTML proof page is 0.6 MB in size.
$/\$ $/\$

Theorem	fsumrev2 7233	Reversal of a finite sum.
$/\$

Theorem	fsumshft 7234	Index shift of a finite sum.
$/\$ $/\$

Theorem	fsumshftm 7235	Negative index shift of a finite sum.
$/\$ $/\$

Theorem	fsummulc1 7236	A finite sum multiplied by a constant.
$/\$ $/\$

Theorem	fsummulc2 7237	A finite sum multiplied by a constant.
$/\$ $/\$

Theorem	fsumdivc 7238	A finite sum divided by a constant.
$/\$ $/\$ $/\$

Theorem	fsumdivcALT 7239	A finite sum divided by a constant. (An experiment: this version of fsumdivc 7238 adds 5 bytes and 233 bytes to the compressed and uncompressed proofs, but saves 540 bytes on the HTML page.)
$/\$ $/\$ $/\$

Theorem	fsum2mul 7240	Separate the nested sum of the product .
$/\$ $/\$ $/\$

Theorem	fsumconst 7241	The sum of constant terms ( is not free in ).
$/\$

Theorem	fsum0 7242	If all of the terms of a finite sum are zero, so is the sum.


Theorem	fsumcmp 7243	If all of the terms of finite sums compare, so do the sums.
$/\$ $/\$ $/\$

Theorem	fsumcmp0 7244	If all of the terms of a finite sum are nonnegative, so is the sum.
$/\$ $/\$

Theorem	fsumcmpndx2 7245	A shorter sum of nonnegative terms is smaller than a longer one.
$/\$ $/\$ $/\$ $/\$

Theorem	fsumabs 7246	Generalized triangle inequality: the absolute value of a finite sum is less than or equal to the sum of absolute values.
$/\$

Theorem	fsumabs2mul 7247	The sum of absolute values of the product is less than or equal to the product of the two sums of absolute values.
$/\$ $/\$ $/\$

Theorem	serzcl 7248	Closure of partial sums of an infinite series.
$/\$

Theorem	ser0cl 7249	Closure of partial sums of a 0-based infinite series.
$/\$

Theorem	ser1cl 7250	Closure of partial sums of a 1-based infinite series.
$/\$

Theorem	ser1ser0i 7251	A 1-based infinite series in terms of a 0-based infinite series.


Theorem	serzcl2 7252	Closure of partial sums of an infinite series.
$/\$

Theorem	serzrecl 7253	The partial sums in an infinite series of real terms are real.
$/\$

Theorem	serzrefi 7254	An infinite series of reals is an infinite real sequence.


Theorem	serz1p 7255	Separate out the first term in an infinite series.
$/\$ $/\$

Theorem	serz0 7256	The value of the partial sums in a zero-valued infinite series.


Theorem	serzcmp 7257	Comparison of partial sums of two infinite series of reals.
$/\$ $/\$ $/\$

Theorem	serzcmp0 7258	A partial sum of an infinite series is nonnegative if each term is nonnegative.
$/\$ $/\$

Theorem	serzsplit 7259	Split off an initial piece of the partial sum of an infinite series.
$/\$ $/\$

Theorem	serzmulc1 7260	A constant times a series.
$/\$ $/\$ $/\$

Theorem	serzmulci 7261	A constant times a series.


Theorem	ser0mulci 7262	A constant times a 0-based series.


Theorem	ser1mulci 7263	A constant times a 1-based series.


Theorem	serzrelem 7264	Lemma for serzrei 7265, serzimi 7266 and serzcji 7267.

Theorem	serzrei 7265	The real part of a series. (Contributed by Paul Chapman, 9-Nov-2007.)
$/\$

Theorem	serzimi 7266	The imaginary part of a series. (Contributed by Paul Chapman, 9-Nov-2007.)
$/\$

Theorem	serzcji 7267	The complex conjugate of a series. (Contributed by Paul Chapman, 9-Nov-2007.)
$/\$

Theorem	ser0cji 7268	The complex conjugate of a 0-based series.
$/\$

The binomial theorem

Theorem	binomlem1 7269	Lemma for binomi 7275 (binomial theorem). Break out and simplify the first term of the summation.

Theorem	binomlem2 7270	Lemma for binomi 7275 (binomial theorem). Shift up the summation index with fsumshft 7234, then break out and simplify the last term of the summation.

Theorem	binomlem3 7271	Lemma for binomi 7275 (binomial theorem). Break out the last term of the summation used by the induction hypothesis.

Theorem	binomlem4 7272	Lemma for binomi 7275 (binomial theorem). Break out the first term of the summation used by the induction hypothesis.

Theorem	binomlem5 7273	Lemma for binomi 7275 (binomial theorem). We use Pascal's rule bcpasc 7173 to combine the sum of the summations in binomlem1 7269 and binomlem2 7270 into a single summation.

Theorem	binomlem6 7274	Lemma for binomi 7275 (binomial theorem). Do the final induction.

Theorem	binomi 7275	The binomial theorem: is the sum from to of . Theorem 15-2.8 of [Gleason] p. 296. This final piece of the proof combines the case of binomlem6 7274 with the case.


Theorem	binom1pi 7276	Special case of the binomial theorem for . (Contributed by Paul Chapman, 10-May-2007.)


Theorem	bcxmaslem1 7277	Lemma for bcxmas 7279.

Theorem	bcxmaslem2 7278	Lemma for bcxmas 7279.

Theorem	bcxmas 7279	Parallel summation (Christmas Stocking) theorem for Pascal's Triangle. (Contributed by Paul Chapman, 18-May-2007.)
$/\$

Limits (cont.)

Theorem	clm1i 7280	Express the predicate: The limit of complex number sequence is , or converges to , with more general quantifier restrictions than clim 7180.
$/\$ $/\$ $/\$

Theorem	clm2i 7281	Express the predicate: The limit of complex number sequence is , or converges to .
$/\$

Theorem	clm3i 7282	A sufficient existence condition for convergence of a complex number sequence .
$/\$

Theorem	clm4i 7283	Express the predicate converges to .
$/\$

Theorem	clm4lei 7284	Express the predicate converges to , with a non-strict ordering requirement.
$/\$

Theorem	clm4fi 7285	Express the predicate converges to .
$/\$

Theorem	clm0i 7286	Express the predicate converges to 0.


Theorem	clmnnsi 7287	Express the predicate " converges to ," using implicit substitution.
$/\$

Theorem	clm0nnsi 7288	Express the predicate " converges to 0."


Theorem	clmi1i 7289	Convergence of a sequence of complex numbers.
$/\$ $/\$ $/\$ $/\$

Theorem	clmi2i 7290	Convergence of a sequence of complex numbers.
$/\$ $/\$ $/\$

Theorem	clmi2rpi 7291	Convergence of a sequence of complex numbers, using positive reals.
$/\$ $/\$

Theorem	clm0ii 7292	Convergence of a sequence of complex numbers to zero.
$/\$ $/\$

Theorem	clm4a 7293	Express the predicate converges to , requiring convergence in the upper integers starting at .
$/\$ $/\$

Theorem	clmi2a 7294	Convergence of a sequence of complex numbers in the upper integers starting at .
$/\$ $/\$ $/\$ $/\$

Theorem	climfnn 7295	Express the predicate converges to for an explicit function, using natural numbers.
$/\$

Theorem	clmfnn 7296	Express the predicate converges to for an explicit function, using natural numbers.
$/\$

Theorem	climconsti 7297	An (eventually) constant sequence converges to its value.
$/\$

Theorem	climconst2 7298	A constant sequence on the integers converges to its value.


Theorem	climconst3 7299	A constant sequence converges to its value.
$/\$

Theorem	clim0 7300	The zero sequence converges to zero.

MPE Home Contents

< Previous Next >