Type | Label | Description |
Statement |
|
Theorem | ivthinclemuopn 14201* |
Lemma for ivthinc 14206. The upper cut is open. (Contributed by
Jim
Kingdon, 19-Feb-2024.)
|
           ![[,] [,]](_icc.gif)          
  ![[,] [,]](_icc.gif)  
                      ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)             |
|
Theorem | ivthinclemur 14202* |
Lemma for ivthinc 14206. The upper cut is rounded. (Contributed by
Jim Kingdon, 18-Feb-2024.)
|
           ![[,] [,]](_icc.gif)          
  ![[,] [,]](_icc.gif)  
                      ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)        |
|
Theorem | ivthinclemdisj 14203* |
Lemma for ivthinc 14206. The lower and upper cuts are disjoint.
(Contributed by Jim Kingdon, 18-Feb-2024.)
|
           ![[,] [,]](_icc.gif)          
  ![[,] [,]](_icc.gif)  
                      ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)            |
|
Theorem | ivthinclemloc 14204* |
Lemma for ivthinc 14206. Locatedness. (Contributed by Jim Kingdon,
18-Feb-2024.)
|
           ![[,] [,]](_icc.gif)          
  ![[,] [,]](_icc.gif)  
                      ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)    
    |
|
Theorem | ivthinclemex 14205* |
Lemma for ivthinc 14206. Existence of a number between the lower
cut
and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.)
|
           ![[,] [,]](_icc.gif)          
  ![[,] [,]](_icc.gif)  
                      ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)                    |
|
Theorem | ivthinc 14206* |
The intermediate value theorem, increasing case, for a strictly
monotonic function. Theorem 5.5 of [Bauer], p. 494. This is
Metamath 100 proof #79. (Contributed by Jim Kingdon,
5-Feb-2024.)
|
           ![[,] [,]](_icc.gif)          
  ![[,] [,]](_icc.gif)  
                      ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)                          |
|
Theorem | ivthdec 14207* |
The intermediate value theorem, decreasing case, for a strictly
monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.)
|
           ![[,] [,]](_icc.gif)          
  ![[,] [,]](_icc.gif)  
                      ![[,] [,]](_icc.gif)  
   ![[,] [,]](_icc.gif)                          |
|
9.1 Derivatives
|
|
9.1.1 Real and complex
differentiation
|
|
9.1.1.1 Derivatives of functions of one complex
or real variable
|
|
Syntax | climc 14208 |
The limit operator.
|
lim |
|
Syntax | cdv 14209 |
The derivative operator.
|
 |
|
Definition | df-limced 14210* |
Define the set of limits of a complex function at a point. Under normal
circumstances, this will be a singleton or empty, depending on whether
the limit exists. (Contributed by Mario Carneiro, 24-Dec-2016.)
(Revised by Jim Kingdon, 3-Jun-2023.)
|
lim           
        #                        |
|
Definition | df-dvap 14211* |
Define the derivative operator. This acts on functions to produce a
function that is defined where the original function is differentiable,
with value the derivative of the function at these points. The set
here is the
ambient topological space under which we are
evaluating the continuity of the difference quotient. Although the
definition is valid for any subset of and is well-behaved when
contains no
isolated points, we will restrict our attention to the
cases or for the majority of the
development,
these corresponding respectively to real and complex differentiation.
(Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon,
25-Jun-2023.)
|
  
             ↾t             # 
               lim     |
|
Theorem | limcrcl 14212 |
Reverse closure for the limit operator. (Contributed by Mario Carneiro,
28-Dec-2016.)
|
  lim      
   |
|
Theorem | limccl 14213 |
Closure of the limit operator. (Contributed by Mario Carneiro,
25-Dec-2016.)
|
 lim   |
|
Theorem | ellimc3apf 14214* |
Write the epsilon-delta definition of a limit. (Contributed by Mario
Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 4-Nov-2023.)
|
               lim        #                       |
|
Theorem | ellimc3ap 14215* |
Write the epsilon-delta definition of a limit. (Contributed by Mario
Carneiro, 28-Dec-2016.) Use apartness. (Revised by Jim Kingdon,
3-Jun-2023.)
|
           
 lim        #                       |
|
Theorem | limcdifap 14216* |
It suffices to consider functions which are not defined at to
define the limit of a function. In particular, the value of the
original function at does
not affect the limit of .
(Contributed by Mario Carneiro, 25-Dec-2016.) (Revised by Jim Kingdon,
3-Jun-2023.)
|
          lim     #  
lim    |
|
Theorem | limcmpted 14217* |
Express the limit operator for a function defined by a mapping, via
epsilon-delta. (Contributed by Jim Kingdon, 3-Nov-2023.)
|
     
   
   lim        #      
            |
|
Theorem | limcimolemlt 14218* |
Lemma for limcimo 14219. (Contributed by Jim Kingdon, 3-Jul-2023.)
|
               
↾t          #            lim     lim       #                            
     #       
       
 
          
     
        |
|
Theorem | limcimo 14219* |
Conditions which ensure there is at most one limit value of at
.
(Contributed by Mario Carneiro, 25-Dec-2016.) (Revised by
Jim Kingdon, 8-Jul-2023.)
|
               
↾t          #           lim    |
|
Theorem | limcresi 14220 |
Any limit of is also
a limit of the restriction of .
(Contributed by Mario Carneiro, 28-Dec-2016.)
|
 lim     lim   |
|
Theorem | cnplimcim 14221 |
If a function is continuous at , its limit at equals the
value of the function there. (Contributed by Mario Carneiro,
28-Dec-2016.) (Revised by Jim Kingdon, 14-Jun-2023.)
|
      ↾t                    
 lim      |
|
Theorem | cnplimclemle 14222 |
Lemma for cnplimccntop 14224. Satisfying the epsilon condition for
continuity. (Contributed by Mario Carneiro and Jim Kingdon,
17-Nov-2023.)
|
      ↾t                  lim          
#                         
     
 
       
        |
|
Theorem | cnplimclemr 14223 |
Lemma for cnplimccntop 14224. The reverse direction. (Contributed by
Mario Carneiro and Jim Kingdon, 17-Nov-2023.)
|
      ↾t                  lim            |
|
Theorem | cnplimccntop 14224 |
A function is continuous at iff its limit at equals the
value of the function there. (Contributed by Mario Carneiro,
28-Dec-2016.)
|
      ↾t                    
 lim      |
|
Theorem | cnlimcim 14225* |
If is a continuous
function, the limit of the function at each
point equals the value of the function. (Contributed by Mario Carneiro,
28-Dec-2016.) (Revised by Jim Kingdon, 16-Jun-2023.)
|
                 lim      |
|
Theorem | cnlimc 14226* |
is a continuous
function iff the limit of the function at each
point equals the value of the function. (Contributed by Mario Carneiro,
28-Dec-2016.)
|
               
 lim      |
|
Theorem | cnlimci 14227 |
If is a continuous
function, then the limit of the function at any
point equals its value. (Contributed by Mario Carneiro,
28-Dec-2016.)
|
              lim    |
|
Theorem | cnmptlimc 14228* |
If is a continuous
function, then the limit of the function at any
point equals its value. (Contributed by Mario Carneiro,
28-Dec-2016.)
|
 
        
     lim    |
|
Theorem | limccnpcntop 14229 |
If the limit of at
is and is continuous at
, then the
limit of at is    .
(Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon,
18-Jun-2023.)
|
              ↾t    lim           
       lim    |
|
Theorem | limccnp2lem 14230* |
Lemma for limccnp2cntop 14231. This is most of the result, expressed in
epsilon-delta form, with a large number of hypotheses so that lengthy
expressions do not need to be repeated. (Contributed by Jim Kingdon,
9-Nov-2023.)
|
        
           ↾t 
      lim   
   lim                      
              
                           #       
     
        #       
     
       #                         |
|
Theorem | limccnp2cntop 14231* |
The image of a convergent sequence under a continuous map is convergent
to the image of the original point. Binary operation version.
(Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon,
14-Nov-2023.)
|
        
           ↾t 
      lim   
   lim                          lim    |
|
Theorem | limccoap 14232* |
Composition of two limits. This theorem is only usable in the case
where # implies R(x) # so it is less general than
might appear at first. (Contributed by Mario Carneiro, 29-Dec-2016.)
(Revised by Jim Kingdon, 18-Dec-2023.)
|
   #
 
 #    
 #
 
     #   lim      
#   lim   
 
   #
  lim    |
|
Theorem | reldvg 14233 |
The derivative function is a relation. (Contributed by Mario Carneiro,
7-Aug-2014.) (Revised by Jim Kingdon, 25-Jun-2023.)
|
         |
|
Theorem | dvlemap 14234* |
Closure for a difference quotient. (Contributed by Mario Carneiro,
1-Sep-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
|
             #
 
           
 
  |
|
Theorem | dvfvalap 14235* |
Value and set bounds on the derivative operator. (Contributed by Mario
Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
|
 ↾t                             
  
#                 lim    
             |
|
Theorem | eldvap 14236* |
The differentiable predicate. A function is differentiable at
with
derivative iff is defined in a
neighborhood of
and the
difference quotient has limit at .
(Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon,
27-Jun-2023.)
|
 ↾t         #             
                           
 lim      |
|
Theorem | dvcl 14237 |
The derivative function takes values in the complex numbers.
(Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario
Carneiro, 9-Feb-2015.)
|
             
     |
|
Theorem | dvbssntrcntop 14238 |
The set of differentiable points is a subset of the interior of the
domain of the function. (Contributed by Mario Carneiro, 7-Aug-2014.)
(Revised by Jim Kingdon, 27-Jun-2023.)
|
           ↾t                    |
|
Theorem | dvbss 14239 |
The set of differentiable points is a subset of the domain of the
function. (Contributed by Mario Carneiro, 6-Aug-2014.) (Revised by
Mario Carneiro, 9-Feb-2015.)
|
               |
|
Theorem | dvbsssg 14240 |
The set of differentiable points is a subset of the ambient topology.
(Contributed by Mario Carneiro, 18-Mar-2015.) (Revised by Jim Kingdon,
28-Jun-2023.)
|
      
  |
|
Theorem | recnprss 14241 |
Both and are subsets of . (Contributed by Mario
Carneiro, 10-Feb-2015.)
|
      |
|
Theorem | dvfgg 14242 |
Explicitly write out the functionality condition on derivative for
and . (Contributed by Mario Carneiro, 9-Feb-2015.)
(Revised by Jim Kingdon, 28-Jun-2023.)
|
        
         |
|
Theorem | dvfpm 14243 |
The derivative is a function. (Contributed by Mario Carneiro,
8-Aug-2014.) (Revised by Jim Kingdon, 28-Jul-2023.)
|
   
         |
|
Theorem | dvfcnpm 14244 |
The derivative is a function. (Contributed by Mario Carneiro,
9-Feb-2015.) (Revised by Jim Kingdon, 28-Jul-2023.)
|
   
         |
|
Theorem | dvidlemap 14245* |
Lemma for dvid 14247 and dvconst 14246. (Contributed by Mario Carneiro,
8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|
       
 #  
                 
      |
|
Theorem | dvconst 14246 |
Derivative of a constant function. (Contributed by Mario Carneiro,
8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|
             |
|
Theorem | dvid 14247 |
Derivative of the identity function. (Contributed by Mario Carneiro,
8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|
        |
|
Theorem | dvcnp2cntop 14248 |
A function is continuous at each point for which it is differentiable.
(Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario
Carneiro, 28-Dec-2016.)
|
 ↾t         
    
  
        |
|
Theorem | dvcn 14249 |
A differentiable function is continuous. (Contributed by Mario
Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-Sep-2015.)
|
  
    
         |
|
Theorem | dvaddxxbr 14250 |
The sum rule for derivatives at a point. That is, if the derivative
of at is and the derivative of at is
, then the
derivative of the pointwise sum of those two
functions at
is . (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.)
|
                  
                
         |
|
Theorem | dvmulxxbr 14251 |
The product rule for derivatives at a point. For the (simpler but
more limited) function version, see dvmulxx 14253. (Contributed by Mario
Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.)
|
                  
                
                     |
|
Theorem | dvaddxx 14252 |
The sum rule for derivatives at a point. For the (more general)
relation version, see dvaddxxbr 14250. (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.)
|
                    
  
            
                |
|
Theorem | dvmulxx 14253 |
The product rule for derivatives at a point. For the (more general)
relation version, see dvmulxxbr 14251. (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Jim Kingdon, 2-Dec-2023.)
|
                    
  
            
                   
        |
|
Theorem | dviaddf 14254 |
The sum rule for everywhere-differentiable functions. (Contributed by
Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro,
10-Feb-2015.)
|
                   
          
           |
|
Theorem | dvimulf 14255 |
The product rule for everywhere-differentiable functions. (Contributed
by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro,
10-Feb-2015.)
|
                   
          
                 |
|
Theorem | dvcoapbr 14256* |
The chain rule for derivatives at a point. The
#     #    
hypothesis constrains what
functions work for . (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Jim Kingdon, 21-Dec-2023.)
|
                   #     #                                  
        |
|
Theorem | dvcjbr 14257 |
The derivative of the conjugate of a function. For the (simpler but
more limited) function version, see dvcj 14258. (Contributed by Mario
Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|
                               |
|
Theorem | dvcj 14258 |
The derivative of the conjugate of a function. For the (more general)
relation version, see dvcjbr 14257. (Contributed by Mario Carneiro,
1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|
      
          |
|
Theorem | dvfre 14259 |
The derivative of a real function is real. (Contributed by Mario
Carneiro, 1-Sep-2014.)
|
      
          |
|
Theorem | dvexp 14260* |
Derivative of a power function. (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|
  
                  |
|
Theorem | dvexp2 14261* |
Derivative of an exponential, possibly zero power. (Contributed by
Stefan O'Rear, 13-Nov-2014.) (Revised by Mario Carneiro,
10-Feb-2015.)
|
 

        
              |
|
Theorem | dvrecap 14262* |
Derivative of the reciprocal function. (Contributed by Mario Carneiro,
25-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.)
|
  
 #        #
           |
|
Theorem | dvmptidcn 14263 |
Function-builder for derivative: derivative of the identity.
(Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
30-Dec-2023.)
|
 
     |
|
Theorem | dvmptccn 14264* |
Function-builder for derivative: derivative of a constant. (Contributed
by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
30-Dec-2023.)
|
           |
|
Theorem | dvmptclx 14265* |
Closure lemma for dvmptmulx 14267 and other related theorems. (Contributed
by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro,
11-Feb-2015.)
|
          
                 |
|
Theorem | dvmptaddx 14266* |
Function-builder for derivative, addition rule. (Contributed by Mario
Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|
          
             
      
                    |
|
Theorem | dvmptmulx 14267* |
Function-builder for derivative, product rule. (Contributed by Mario
Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|
          
             
      
                        |
|
Theorem | dvmptcmulcn 14268* |
Function-builder for derivative, product rule for constant multiplier.
(Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
31-Dec-2023.)
|
        
                      |
|
Theorem | dvmptnegcn 14269* |
Function-builder for derivative, product rule for negatives.
(Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
31-Dec-2023.)
|
        
            

    |
|
Theorem | dvmptsubcn 14270* |
Function-builder for derivative, subtraction rule. (Contributed by
Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
31-Dec-2023.)
|
        
        
      
                    |
|
Theorem | dvmptcjx 14271* |
Function-builder for derivative, conjugate rule. (Contributed by Mario
Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 24-May-2024.)
|
        
                          |
|
Theorem | dveflem 14272 |
Derivative of the exponential function at 0. The key step in the proof
is eftlub 11700, to show that
             .
(Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario
Carneiro, 28-Dec-2016.)
|
     |
|
Theorem | dvef 14273 |
Derivative of the exponential function. (Contributed by Mario Carneiro,
9-Aug-2014.) (Proof shortened by Mario Carneiro, 10-Feb-2015.)
|
 
 |
|
PART 10 BASIC REAL AND COMPLEX
FUNCTIONS
|
|
10.1 Basic trigonometry
|
|
10.1.1 The exponential, sine, and cosine
functions (cont.)
|
|
Theorem | efcn 14274 |
The exponential function is continuous. (Contributed by Paul Chapman,
15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.)
|
     |
|
Theorem | sincn 14275 |
Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.)
(Revised by Mario Carneiro, 3-Sep-2014.)
|
     |
|
Theorem | coscn 14276 |
Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.)
(Revised by Mario Carneiro, 3-Sep-2014.)
|
     |
|
Theorem | reeff1olem 14277* |
Lemma for reeff1o 14279. (Contributed by Paul Chapman,
18-Oct-2007.)
(Revised by Mario Carneiro, 30-Apr-2014.)
|
          |
|
Theorem | reeff1oleme 14278* |
Lemma for reeff1o 14279. (Contributed by Jim Kingdon, 15-May-2024.)
|
     
      |
|
Theorem | reeff1o 14279 |
The real exponential function is one-to-one onto. (Contributed by Paul
Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 10-Nov-2013.)
|
       |
|
Theorem | efltlemlt 14280 |
Lemma for eflt 14281. The converse of efltim 11708 plus the epsilon-delta
setup. (Contributed by Jim Kingdon, 22-May-2024.)
|
                                                  
  |
|
Theorem | eflt 14281 |
The exponential function on the reals is strictly increasing.
(Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon,
21-May-2024.)
|
               |
|
Theorem | efle 14282 |
The exponential function on the reals is nondecreasing. (Contributed by
Mario Carneiro, 11-Mar-2014.)
|
               |
|
Theorem | reefiso 14283 |
The exponential function on the reals determines an isomorphism from
reals onto positive reals. (Contributed by Steve Rodriguez,
25-Nov-2007.) (Revised by Mario Carneiro, 11-Mar-2014.)
|
      |
|
Theorem | reapef 14284 |
Apartness and the exponential function for reals. (Contributed by Jim
Kingdon, 11-Jul-2024.)
|
    #     #        |
|
10.1.2 Properties of pi =
3.14159...
|
|
Theorem | pilem1 14285 |
Lemma for pire , pigt2lt4 and sinpi . (Contributed by Mario Carneiro,
9-May-2014.)
|
              
   |
|
Theorem | cosz12 14286 |
Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and
Jim Kingdon, 7-Mar-2024.)
|
           |
|
Theorem | sin0pilem1 14287* |
Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim
Kingdon, 8-Mar-2024.)
|
          
              |
|
Theorem | sin0pilem2 14288* |
Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim
Kingdon, 8-Mar-2024.)
|
                       |
|
Theorem | pilem3 14289 |
Lemma for pi related theorems. (Contributed by Jim Kingdon,
9-Mar-2024.)
|
           |
|
Theorem | pigt2lt4 14290 |
is between 2 and 4.
(Contributed by Paul Chapman, 23-Jan-2008.)
(Revised by Mario Carneiro, 9-May-2014.)
|

  |
|
Theorem | sinpi 14291 |
The sine of is 0.
(Contributed by Paul Chapman, 23-Jan-2008.)
|
   
 |
|
Theorem | pire 14292 |
is a real number.
(Contributed by Paul Chapman, 23-Jan-2008.)
|
 |
|
Theorem | picn 14293 |
is a complex number.
(Contributed by David A. Wheeler,
6-Dec-2018.)
|
 |
|
Theorem | pipos 14294 |
is positive.
(Contributed by Paul Chapman, 23-Jan-2008.)
(Revised by Mario Carneiro, 9-May-2014.)
|
 |
|
Theorem | pirp 14295 |
is a positive real.
(Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
 |
|
Theorem | negpicn 14296 |
 is a real number.
(Contributed by David A. Wheeler,
8-Dec-2018.)
|
  |
|
Theorem | sinhalfpilem 14297 |
Lemma for sinhalfpi 14302 and coshalfpi 14303. (Contributed by Paul Chapman,
23-Jan-2008.)
|
               |
|
Theorem | halfpire 14298 |
is real. (Contributed by David Moews,
28-Feb-2017.)
|
   |
|
Theorem | neghalfpire 14299 |
 is real. (Contributed by David A. Wheeler, 8-Dec-2018.)
|
    |
|
Theorem | neghalfpirx 14300 |
 is an extended real. (Contributed by David A. Wheeler,
8-Dec-2018.)
|
    |