HomeUnicode version.
| Home |
Metamath Proof Explorer | < Previous Next > |
| Browser slow? Try the
Unicode version. |
| Color key: | Metamath Proof Explorer
(1-9062) |
Hilbert Space Explorer
(9063-10650) |
Users' Mathboxes
(10651-12229) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | climunii 7301 | An infinite sequence of complex numbers converges to at most one limit. |
             | ||
| Theorem | climuni 7302 | An infinite sequence of complex numbers converges to at most one limit. |
 | ||
| Theorem | climeu 7303 | An infinite sequence of complex numbers converges to at most one limit. |
 
| ||
| Theorem | climreu 7304 | An infinite sequence of complex numbers converges to at most one limit. |
 | ||
| Theorem | 2climnn 7305 | If two sequences converge to each other, they converge to the same limit. |
    
       
| ||
| Theorem | 2climnn0 7306 | If two sequences converge to each other, they converge to the same limit. |
| ||
| Theorem | climshfti 7307 | A shifted function converges iff the original function converges. |
    | ||
| Theorem | climresi 7308 | A function restricted to upper integers converges iff the original function converges. |
  | ||
| Theorem | climshft2i 7309 | A shifted function converges iff the original function converges. (Contributed by Paul Chapman, 19-Nov-2007.) |
  | ||
| Theorem | iserzshft2i 7310 | Index shift of an infinite series. (Contributed by Paul Chapman, 19-Nov-2007.) |
 
 
| ||
| Theorem | climuz0i 7311 | A zero sequence converges to zero. |
   | ||
| Theorem | serzclim0 7312 | The zero series converges to zero. (Contributed by Paul Chapman, 9-Feb-2007.) |
| | ||
| Theorem | climrecl 7313 | The limit of a convergent real sequence is real. Corollary 12-2.5 of [Gleason] p. 172. |
|
| ||
| Theorem | climfnrcli 7314 | The limit of a convergent real sequence on natural numbers is real. Corollary 12-2.5 of [Gleason] p. 172. |
  | ||
| Theorem | climge0 7315 | A nonnegative sequence converges to a nonnegative number. |
|
| ||
| Theorem | climabs0i 7316 | Convergence to zero of the absolute value is equivalent to convergence to zero. |
| | ||
| Theorem | climaddlem1 7317 | Lemma for climadd 7320. |
| Theorem | climaddlem2 7318 | Lemma for climadd 7320. |
| Theorem | climaddlem3 7319 | Lemma for climadd 7320. Warning: The HTML proof page is 3/4 megabyte in size. |
| Theorem | climadd 7320 | Limit of the sum of two converging sequences. Proposition 12-2.1(a) of [Gleason] p. 168. |
| ||
| Theorem | climaddc1 7321 |
Limit of a constant 
added to each term of a sequence.
|
|
| ||
| Theorem | climaddc2 7322 |
Limit of a constant
added to each term of a sequence.
|
|
| ||
| Theorem | climmullem1 7323 | Lemma for climmul 7331. |
| Theorem | climmullem2 7324 | Lemma for climmul 7331. |
| Theorem | climmullem3 7325 | Lemma for climmul 7331. |
| Theorem | climmullem4 7326 | Lemma for climmul 7331. |
| Theorem | climmullem5 7327 | Lemma for climmul 7331. Instead of the infimum that Gleason uses (bottom of p. 170), we use recreclt 6047 to give us a number smaller than both a given number and 1. Warning: The HTML proof page is 1/2 megabyte in size. |
| Theorem | climmullem6 7328 | Lemma for climmul 7331. |
| Theorem | climmullem7 7329 | Lemma for climmul 7331. |
| Theorem | climmullem8 7330 | Lemma for climmul 7331. Warning: The HTML proof page is 3/4 megabyte in size. |
| Theorem | climmul 7331 | Limit of the product of two converging sequences. Proposition 12-2.1(c) of [Gleason] p. 168. |
 | ||
| Theorem | climmulc2 7332 |
Limit of a sequence multiplied by a constant . Corollary 12-2.2
of [Gleason] p. 171.
|
|
| ||
| Theorem | climsub 7333 | Limit of the difference of two converging sequences. Proposition 12-2.1(b) of [Gleason] p. 168. |
|
| ||
| Theorem | climsubc2 7334 |
Limit of a constant
minus each term of a sequence.
|
|
| ||
| Theorem | climaddci 7335 |
Limit of a constant
added to a sequence.
|
 | ||
| Theorem | climmulci 7336 |
Limit of a sequence multiplied by a constant . Corollary 12-2.2
of [Gleason] p. 171.
|
| | ||
| Theorem | clim2serz 7337 | The limit of an infinite series with an initial segment removed. (Contributed by Paul Chapman, 9-Feb-2007.) |
 | ||
| Theorem | iserzex 7338 | If an infinite series converges, so does the series with initial terms removed. (Contributed by Paul Chapman, 9-Feb-2007.) |
|
| ||
| Theorem | iserzmulc1 7339 | Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) |
|
| ||
| Theorem | climcmplem 7340 | Lemma for climcmp 7341. |
| Theorem | climcmp 7341 | Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) |
|
| ||
| Theorem | climcmpc1 7342 | Comparison of a constant to the limit of a sequence. |
|
| ||
| Theorem | climsqueeze 7343 | Convergence of a sequence sandwiched between another converging sequence and its limit. |
|
| ||
| Theorem | climsqueeze2 7344 | Convergence of a sequence sandwiched between another converging sequence and its limit. |
|
| ||
| Theorem | iserzcmp 7345 | Comparison of the limits of two infinite series. (Contributed by Paul Chapman, 12-Nov-2007.) |
|
| ||
| Theorem | iserzcmp0 7346 | The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Paul Chapman, 9-Feb-2007.) |
| | ||
| Theorem | iserzshfti 7347 | Index shift of an infinite series. (Contributed by Paul Chapman, 31-Oct-2007.) |
|
| ||
| Theorem | clim2serzi 7348 | Limit of an infinite series with an initial segment removed. |
|
| ||
| Theorem | iserzexi 7349 | If an infinite series converges, so does the series with initial terms removed. (Contributed by Paul Chapman, 23-Nov-2007.) |
|
| ||
| Theorem | climserzlei 7350 | The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. |
|
| ||
| Theorem | climabslem 7351 | Lemma for climabsi 7352, climcji 7353, climrei 7354, and climimi 7355. |
| Theorem | climabsi 7352 | Limit of the absolute value of a sequence. (Contributed by Paul Chapman, 7-Sep-2007.) |
| | ||
| Theorem | climcji 7353 | Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. |
 | ||
| Theorem | climrei 7354 | Limit of the real part of a sequence. (Contributed by Paul Chapman, 24-Sep-2007.) |
 | ||
| Theorem | climimi 7355 | Limit of the imaginary part of a sequence. (Contributed by Paul Chapman, 7-Sep-2007.) |
 | ||
| Theorem | climubii 7356 | The limit of a monotonic sequence is an upper bound. |
|
| ||
| Theorem | climubi 7357 | The limit of a monotonic sequence is an upper bound. |
|
| ||
| Theorem | climsupi 7358 | A bounded monotonic sequence converges to the supremum of its range. Theorem 12-5.1 of [Gleason] p. 180. |
  | ||
| Theorem | climcaui 7359 | A converging sequence of complex numbers is a Cauchy sequence. Theorem 12-5.3 of [Gleason] p. 180 (necessity part). |
| ||
| Theorem | caucvglem1 7360 |
Lemma for caucvgi 7366. This lemma shows the membership relation
for
 .
|
| Theorem | caucvglem2 7361 |
Lemma for caucvgi 7366. is a nonempty bounded subset of
.
|
| Theorem | caucvglem3 7362 |
Lemma for caucvgi 7366. The supremum of is a real number.
|
| Theorem | caucvglem4 7363 |
Lemma for caucvgi 7366. Anything less that the supremum of
belongs to .
|
| Theorem | caucvglem5 7364 | Lemma for caucvgi 7366. |
| Theorem | caucvglem6 7365 | Lemma for caucvgi 7366. |
| Theorem | caucvgi 7366 |
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 | caucvg3ai 7367 | 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 | caucvg2i 7368 | A Cauchy sequence of real numbers converges to a real number. |
|
| ||
| Theorem | caucvg3lem 7369 | Lemma for caucvg3i 7370. |
| Theorem | caucvg3i 7370 | A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of [Gleason] p. 180 (sufficiency part). |
|
| ||
| Theorem | caucvg3 7371 | 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 | serzf0i 7372 | If an infinite series converges, its underlying sequence converges to zero. Warning: The HTML proof page is 0.6 megabyte in size. |
|
| ||
| Theorem | ser1f0i 7373 | If an infinite series converges, its underlying sequence converges to zero. (Proof shortened by Eric Schmidt, 31-Oct-2009.) |
 | ||
| Theorem | ser1consti 7374 | Value of the partial series sum of a constant function. |
|
| ||
| Theorem | ser10 7375 | The value of the zero series. |
|
| ||
| Theorem | ser1clim0 7376 | The zero series converges to zero. |
|
| ||
| Theorem | ser1cmpi 7377 | Comparison of partial sums of two infinite series of reals. |
|
| ||
| Theorem | ser1cmp0i 7378 | A partial sum of an infinite series of nonnegative reals is nonnegative. |
|
| ||
| Theorem | ser1cmp2lem 7379 | Lemma for ser1cmp2i 7380. |
| Theorem | ser1cmp2i 7380 | Comparison of partial sums of two infinite series of reals that excludes an initial segment. |
|
| ||
| Theorem | iserzabslem 7381 | Lemma for iserzabsi 7382. |
| Theorem | iserzabsi 7382 | 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 7383 | Lemma for cvgcmp2i 7384. |
| Theorem | cvgcmp2i 7384 |
A comparison test for convergence of a real infinite series. This
version allows us to ignore the initial segment before the -th
term.
|
|
| ||
| Theorem | cvgcmp2clem 7385 | Lemma for cvgcmp2ci 7387. |
| Theorem | cvgcmp2clemOLD 7386 | Lemma for cvgcmp2ci 7387. |
| Theorem | cvgcmp2ci 7387 |
A comparison test for convergence of a real infinite series. This
version of cvgcmp2i 7384 allows the reference sequence (whose
infinite series converges) to be multiplied by a nonnegative constant
before the
comparison.
|
|
| ||
| Theorem | cvgcmpi 7388 | A comparison test for convergence of a real infinite series. Similar to Exercise 3 of [Gleason] p. 182, except that we show the explicit limit rather than just its existence. |
|
| ||
| Theorem | cvgcmpubi 7389 | An upper bound for the limit of a real infinite series. This theorem can also be used to compare two infinite series. |
|
| ||
| Theorem | cvgcmp3ci 7390 | A comparison test for convergence of a complex infinite series, where the reference sequence is multiplied by a constant. This version of cvgcmp3cei 7391 shows the explicit value of the limit (which is why we need all the hypotheses). |
| ||
| Theorem | cvgcmp3cei 7391 |
A comparison test for convergence of a complex infinite series.
If, beyond a certain index , the absolute value of sequence
is smaller
than a constant times
a convergent reference
sequence ,
then converges to a
complex number. This
version of cvgcmp3ci 7390 shows just the existence of the limit rather
than its explicit value.
|
|
| ||
| Theorem | cvgcmp3cetlem1 7392 | Lemma for cvgcmp3ce 7394. |
| Theorem | cvgcmp3cetlem2 7393 | Lemma for cvgcmp3ce 7394. |
| Theorem | cvgcmp3ce 7394 | A comparison test for convergence of a complex infinite series. Closed theorem form of cvgcmp3cei 7391. |
|
| ||
| Infinite sums (cont.) | ||
| Theorem | dfisum 7395 | Series sum with an infinite index set (i.e. an infinite series). |
 
| ||
| Theorem | isumval 7396 |
The value of the sum of a series from to
infinity is the
unique (by climuni 7302) value it converges to (if it converges).
The sum
evaluates to the empty set when it doesn't converge, but this shouldn't
be depended on to indicate non-convergence (because it would presuppose a
construction-dependent property of complex numbers, i.e. that no complex
number equals the empty set, which, although by 0ncn 5405
is true for our
specific construction, is not specified by their axioms and may fail for
some other construction). Instead, use
to indicate
non-convergence.
|
| | ||
| Theorem | isumvaltfi 7397 | Version of isumval 7396 with a bound-variable hypothesis instead of a distinct variable condition. |
|
| ||
| Theorem | isumval2 7398 |
Sum of from to
infinity.
|
|
| ||
| Theorem | isumclimtfi 7399 | Version of isumclim 7400 with a bound-variable hypothesis instead of a distinct variable condition. |
|
| ||
| Theorem | isumclim 7400 | An infinite sum equals the value its series converges to. |
| | ||
| MPE Home Contents | Copyright terms: Public domain | < Previous Next > |