Statement List for Metamath Proof Explorer - 7201-7300 - Page 73 of 107
| 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)    |
| |
| Theorem | fsum0diag2 7213 |
Two ways to express "the sum of       where
."
|
       
                      
                 ![]_](_urbrack.gif)    |
| |
| 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 |