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