HomeUnicode version.
| Home |
Metamath Proof Explorer | < Previous Next > |
| Browser slow? Try the
Unicode version. |
| Color key: | Metamath Proof Explorer
(1-8743)
|
Hilbert Space Explorer
(8744-10676)
|
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cvgratlem2ALT 7201 |
Lemma for cvgrat 7208. Using expsubt 6544, restate cvgratlem1ALT 7200 with an
absolute index 
instead of just an offset from the starting index
 .
|
| Theorem | cvgratlem3ALT 7202 |
Lemma for cvgrat 7208. Restate cvgratlem2ALT 7201 (which was for a real
function) in terms of the absolute values of the terms of a complex
function  , with
the help of an auxiliary function  .
|
| Theorem | cvgratlem1 7203 |
Lemma for cvgrat 7208. Establish, by induction, an exponential
upper
bound for the terms of a real series, given that the ratio of successive
terms is less than some positive constant  beyond a starting index
.
|
| Theorem | cvgratlem2 7204 |
Lemma for cvgrat 7208. Using expsubt 6544, restate cvgratlem1 7203
with an
absolute index
instead of just an offset from the starting index
.
|
| Theorem | cvgratlem3 7205 |
Lemma for cvgrat 7208. Restate cvgratlem2 7204 (which was for a real
function) in terms of the absolute values of the terms of a complex
function , with
the help of an auxiliary function .
|
| Theorem | cvgratlem4 7206 | Lemma for cvgrat 7208. The ratio of successive terms meeting the ratio test criterion is positive. |
| Theorem | cvgratlem5 7207 |
Lemma for cvgrat 7208. A complex infinite series meeting the
ratio test criterion converges. We show that the partial sums of
are smaller
than the partial sums of a geometric series (which
converges by geolimi 7189), so by the comparison test
cvgcmp3cet 7144, also converges.
|
| Theorem | cvgrat 7208 |
Ratio test for convergence of a complex infinite series. If the ratio
of the absolute
values of of successive terms in an infinite
sequence is
less than 1 for all terms beyond some index ,
then the infinite sum of the terms of converges to a complex
number. Equivalent to first part of Exercise 4 of [Gleason] p. 182.
|
          
   
         | ||
| The product of two finite sums | ||
| Theorem | fsum0diaglem1 7209 | Lemma for fsum0diag 7211. |
| Theorem | fsum0diaglem2 7210 | Lemma for fsum0diag 7211 that provides its induction hypothesis. Warning: The HTML proof page is 0.8 megabyte in size. |
| Theorem | fsum0diag 7211 |
Two ways to express "the sum of   where
 ."
|
  
  
 
![]_](_urbrack.gif){kind=small} | ||
| Theorem | fsum0diag2 7212 |
Two ways to express "the sum of where
."
|
|
| ||
| Theorem | fsum0diag3 7213 |
Two ways to express "the sum of where
."
|
|
| ||
| Theorem | fsum0diag4 7214 |
Two ways to express "the sum of where
."
|
|
| ||
| Continuous complex functions | ||
| Syntax | ccncf 7215 | Extend class notation to include the operation which returns a class of continuous complex functions. |
  | ||
| Definition | df-cncf 7216 | Define the operation whose value is a class of continuous complex functions. |
   
    
  
 | ||
| Theorem | cncfval 7217 |
The value of the continuous complex function operation is the set of
continuous functions from to .
(Contributed by Paul
Chapman, 11-Oct-2007.)
|
|
| ||
| Theorem | elcncf 7218 |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 11-Oct-2007.)
|
| ||
| Theorem | cncff 7219 | A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008.) |
 
| ||
| Theorem | cncffvelrnOLD 7220 | A continuous complex function's value belongs to its codomain. (Contributed by Paul Chapman, 21-Jan-2008.) |
|
| ||
| Theorem | cncffvelrn 7221 | A continuous complex function's value belongs to its codomain. (Contributed by Paul Chapman, 21-Jan-2008.) |
|
| ||
| Theorem | negfcncf 7222 | The negative of a continuous complex function is continuous. (Contributed by Paul Chapman, 21-Jan-2008.) |
 
| ||
| Theorem | elcncf1d 7223 |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
 | ||
| Theorem | elcncf1i 7224 |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
|
| ||
| Theorem | rescncf 7225 | A continuous complex function restricted to a subset is continuous. (Contributed by Paul Chapman, 18-Oct-2007.) |
 | ||
| Theorem | cncffvrn 7226 | Change the codomain of a continuous complex function. (Contributed by Paul Chapman, 18-Oct-2007.) |
|
| ||
| Theorem | abscncflem 7227 | Lemma for abscncf 7228, recncf 7229, imcncf 7230, and cjcncf 7231. |
| Theorem | abscncf 7228 | Absolute value is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) |
| | ||
| Theorem | recncf 7229 | Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) |
 | ||
| Theorem | imcncf 7230 | Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) |
 | ||
| Theorem | cjcncf 7231 | Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) |
 | ||
| Theorem | mulc1cncf 7232 | Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) |
|
| ||
| Theorem | divccncf 7233 | Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) |
 | ||
| Intermediate value theorem | ||
| Theorem | ivthlem1 7234 | Lemma for isupivth 7243. |
| Theorem | ivthlem2 7235 | Lemma for isupivth 7243. |
| Theorem | ivthlem3 7236 | Lemma for isupivth 7243. |
| Theorem | ivthlem4 7237 | Lemma for isupivth 7243. |
| Theorem | ivthlem5 7238 | Lemma for isupivth 7243. |
| Theorem | ivthlem6 7239 | Lemma for isupivth 7243: modus tollens case 1. |
| Theorem | ivthlem7 7240 | Lemma for isupivth 7243: modus tollens case 2. |
| Theorem | ivthlem8 7241 | Lemma for isupivth 7243. |
| Theorem | ivthlem9 7242 | Lemma for isupivth 7243. |
| Theorem | isupivth 7243 | The intermediate value theorem, increasing case with supremum solution. (Contributed by Paul Chapman, 22-Jan-2008.) |
 [,]  [,]  [,]
(,) | ||
| Theorem | dsupivthlem 7244 | Lemma for dsupivth 7245. |
| Theorem | dsupivth 7245 | The intermediate value theorem, decreasing case with supremum solution. (Contributed by Paul Chapman, 22-Jan-2008.) |
| [,] [,] [,]
(,) | ||
| Theorem | ivthlem4OLD 7246 | Lemma for ivthOLD 7251. |
| Theorem | ivthlem5OLD 7247 | Lemma for ivthOLD 7251. |
| Theorem | ivthlem6OLD 7248 | Lemma for ivthOLD 7251: modus tollens case 1. |
| Theorem | ivthlem7OLD 7249 | Lemma for ivthOLD 7251: modus tollens case 2. |
| Theorem | ivthlem8OLD 7250 | |