mmtheorems72 - 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-10682

Color key:

Metamath Proof Explorer (1-8757)

Hilbert Space Explorer (8758-10682)

**Statement List for Metamath Proof Explorer -** 7101-7200 - Page 72 of 107
Type	Label	Description
Statement

Theorem	climserzle 7101	The partial sums of a converging infinite series with nonnegative terms are bounded by its limit.
$/\$

Theorem	climabslem 7102	Lemma for climabs 7103, climcj 7104, climre 7105, and climim 7106.

Theorem	climabs 7103	Limit of the absolute value of a sequence. (Contributed by Paul Chapman, 7-Sep-2007.)
$/\$

Theorem	climcj 7104	Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172.
$/\$

Theorem	climre 7105	Limit of the real part of a sequence. (Contributed by Paul Chapman, 24-Sep-2007.)
$/\$

Theorem	climim 7106	Limit of the imaginary part of a sequence. (Contributed by Paul Chapman, 7-Sep-2007.)
$/\$

Theorem	climubi 7107	The limit of a monotonic sequence is an upper bound.


Theorem	climub 7108	The limit of a monotonic sequence is an upper bound.


Theorem	climsup 7109	A bounded monotonic sequence converges to the supremum of its range. Theorem 12-5.1 of [Gleason] p. 180.


Theorem	climcau 7110	A converging sequence of complex numbers is a Cauchy sequence. Theorem 12-5.3 of [Gleason] p. 180 (necessity part).


Theorem	caucvglem1 7111	Lemma for caucvg 7117. This lemma shows the membership relation for .

Theorem	caucvglem2 7112	Lemma for caucvg 7117. is a nonempty bounded subset of .

Theorem	caucvglem3 7113	Lemma for caucvg 7117. The supremum of is a real number.

Theorem	caucvglem4 7114	Lemma for caucvg 7117. Anything less that the supremum of belongs to .

Theorem	caucvglem5 7115	Lemma for caucvg 7117.

Theorem	caucvglem6 7116	Lemma for caucvg 7117.

Theorem	caucvg 7117	A Cauchy sequence of real numbers converges. The second hypothesis specifies that is a Cauchy sequence. is the set of numbers less than all values of except for finitely many. Reference: Bert G. Wachsmuth, http://www.shu.edu/projects/reals/numseq/proofs/cauconv.html. Request: Please contact Norm Megill if you know of a textbook reference for the version of the proof in the link above. Warning: The HTML proof page is 1/2 megabyte in size.


Theorem	caucvg3a 7118	A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). This version shows the explicit value of the limit (which is why we need all the hypotheses) rather than just its existence.


Theorem	caucvg2 7119	A Cauchy sequence of real numbers converges to a real number.


Theorem	caucvg3lem 7120	Lemma for caucvg3 7121.

Theorem	caucvg3 7121	A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part).


Theorem	caucvg3t 7122	A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). Warning: The HTML proof page is 0.6 megabyte in size.
$/\$

Theorem	serzf0 7123	If an infinite series converges, its underlying sequence converges to zero. Warning: The HTML proof page is 0.6 megabyte in size.


Theorem	ser1f0 7124	If an infinite series converges, its underlying sequence converges to zero. Warning: The HTML proof page is 1/2 megabyte in size.


Theorem	ser1const 7125	Value of the partial series sum of a constant function.


Theorem	ser10 7126	The value of the zero series.


Theorem	ser1clim0 7127	The zero series converges to zero.


Theorem	ser1cmp 7128	Comparison of partial sums of two infinite series of reals.


Theorem	ser1cmp0 7129	A partial sum of an infinite series of nonnegative reals is nonnegative.


Theorem	ser1cmp2lem 7130	Lemma for ser1cmp2 7131.

Theorem	ser1cmp2 7131	Comparison of partial sums of two infinite series of reals that excludes an initial segment.
$/\$ $/\$

Theorem	iserzabslem 7132	Lemma for iserzabs 7133.

Theorem	iserzabs 7133	Generalized triangle inequality: the absolute value of an infinite sum is less than or equal to the sum of absolute values. (Contributed by Paul Chapman, 10-Sep-2007.)
$/\$

Theorem	cvgcmp2lem 7134	Lemma for cvgcmp2 7135.

Theorem	cvgcmp2 7135	A comparison test for convergence of a real infinite series. This version allows us to ignore the initial segment before the -th term.
$/\$