Type  Label  Description 
Statement 

Theorem  cncfval 13001* 
The value of the continuous complex function operation is the set of
continuous functions from to .
(Contributed by Paul
Chapman, 11Oct2007.) (Revised by Mario Carneiro, 9Nov2013.)



Theorem  elcncf 13002* 
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 11Oct2007.) (Revised by Mario
Carneiro, 9Nov2013.)



Theorem  elcncf2 13003* 
Version of elcncf 13002 with arguments commuted. (Contributed by
Mario
Carneiro, 28Apr2014.)



Theorem  cncfrss 13004 
Reverse closure of the continuous function predicate. (Contributed by
Mario Carneiro, 25Aug2014.)



Theorem  cncfrss2 13005 
Reverse closure of the continuous function predicate. (Contributed by
Mario Carneiro, 25Aug2014.)



Theorem  cncff 13006 
A continuous complex function's domain and codomain. (Contributed by
Paul Chapman, 17Jan2008.) (Revised by Mario Carneiro,
25Aug2014.)



Theorem  cncfi 13007* 
Defining property of a continuous function. (Contributed by Mario
Carneiro, 30Apr2014.) (Revised by Mario Carneiro, 25Aug2014.)



Theorem  elcncf1di 13008* 
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26Nov2007.)



Theorem  elcncf1ii 13009* 
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26Nov2007.)



Theorem  rescncf 13010 
A continuous complex function restricted to a subset is continuous.
(Contributed by Paul Chapman, 18Oct2007.) (Revised by Mario Carneiro,
25Aug2014.)



Theorem  cncffvrn 13011 
Change the codomain of a continuous complex function. (Contributed by
Paul Chapman, 18Oct2007.) (Revised by Mario Carneiro, 1May2015.)



Theorem  cncfss 13012 
The set of continuous functions is expanded when the range is expanded.
(Contributed by Mario Carneiro, 30Aug2014.)



Theorem  climcncf 13013 
Image of a limit under a continuous map. (Contributed by Mario
Carneiro, 7Apr2015.)



Theorem  abscncf 13014 
Absolute value is continuous. (Contributed by Paul Chapman,
21Oct2007.) (Revised by Mario Carneiro, 28Apr2014.)



Theorem  recncf 13015 
Real part is continuous. (Contributed by Paul Chapman, 21Oct2007.)
(Revised by Mario Carneiro, 28Apr2014.)



Theorem  imcncf 13016 
Imaginary part is continuous. (Contributed by Paul Chapman,
21Oct2007.) (Revised by Mario Carneiro, 28Apr2014.)



Theorem  cjcncf 13017 
Complex conjugate is continuous. (Contributed by Paul Chapman,
21Oct2007.) (Revised by Mario Carneiro, 28Apr2014.)



Theorem  mulc1cncf 13018* 
Multiplication by a constant is continuous. (Contributed by Paul
Chapman, 28Nov2007.) (Revised by Mario Carneiro, 30Apr2014.)



Theorem  divccncfap 13019* 
Division by a constant is continuous. (Contributed by Paul Chapman,
28Nov2007.) (Revised by Jim Kingdon, 9Jan2023.)

# 

Theorem  cncfco 13020 
The composition of two continuous maps on complex numbers is also
continuous. (Contributed by Jeff Madsen, 2Sep2009.) (Revised by
Mario Carneiro, 25Aug2014.)



Theorem  cncfmet 13021 
Relate complex function continuity to metric space continuity.
(Contributed by Paul Chapman, 26Nov2007.) (Revised by Mario Carneiro,
7Sep2015.)



Theorem  cncfcncntop 13022 
Relate complex function continuity to topological continuity.
(Contributed by Mario Carneiro, 17Feb2015.)

↾_{t} ↾_{t}


Theorem  cncfcn1cntop 13023 
Relate complex function continuity to topological continuity.
(Contributed by Paul Chapman, 28Nov2007.) (Revised by Mario Carneiro,
7Sep2015.) (Revised by Jim Kingdon, 16Jun2023.)



Theorem  cncfmptc 13024* 
A constant function is a continuous function on . (Contributed
by Jeff Madsen, 2Sep2009.) (Revised by Mario Carneiro,
7Sep2015.)



Theorem  cncfmptid 13025* 
The identity function is a continuous function on . (Contributed
by Jeff Madsen, 11Jun2010.) (Revised by Mario Carneiro,
17May2016.)



Theorem  cncfmpt1f 13026* 
Composition of continuous functions. analogue of cnmpt11f 12726.
(Contributed by Mario Carneiro, 3Sep2014.)



Theorem  cncfmpt2fcntop 13027* 
Composition of continuous functions. analogue of cnmpt12f 12728.
(Contributed by Mario Carneiro, 3Sep2014.)



Theorem  addccncf 13028* 
Adding a constant is a continuous function. (Contributed by Jeff
Madsen, 2Sep2009.)



Theorem  cdivcncfap 13029* 
Division with a constant numerator is continuous. (Contributed by Mario
Carneiro, 28Dec2016.) (Revised by Jim Kingdon, 26May2023.)

#
#


Theorem  negcncf 13030* 
The negative function is continuous. (Contributed by Mario Carneiro,
30Dec2016.)



Theorem  negfcncf 13031* 
The negative of a continuous complex function is continuous.
(Contributed by Paul Chapman, 21Jan2008.) (Revised by Mario Carneiro,
25Aug2014.)



Theorem  mulcncflem 13032* 
Lemma for mulcncf 13033. (Contributed by Jim Kingdon, 29May2023.)



Theorem  mulcncf 13033* 
The multiplication of two continuous complex functions is continuous.
(Contributed by Glauco Siliprandi, 29Jun2017.)



Theorem  expcncf 13034* 
The power function on complex numbers, for fixed exponent N, is
continuous. (Contributed by Glauco Siliprandi, 29Jun2017.)



Theorem  cnrehmeocntop 13035* 
The canonical bijection from to described in
cnref1o 9560 is in fact a homeomorphism of the usual
topologies on these
sets. (It is also an isometry, if
is metrized with the
l<SUP>2</SUP> norm.) (Contributed by Mario Carneiro,
25Aug2014.)



Theorem  cnopnap 13036* 
The complex numbers apart from a given complex number form an open set.
(Contributed by Jim Kingdon, 14Dec2023.)

#


PART 8 BASIC REAL AND COMPLEX
ANALYSIS


8.0.1 Dedekind cuts


Theorem  dedekindeulemuub 13037* 
Lemma for dedekindeu 13043. Any element of the upper cut is an upper
bound for the lower cut. (Contributed by Jim Kingdon, 2Feb2024.)



Theorem  dedekindeulemub 13038* 
Lemma for dedekindeu 13043. The lower cut has an upper bound.
(Contributed by Jim Kingdon, 31Jan2024.)



Theorem  dedekindeulemloc 13039* 
Lemma for dedekindeu 13043. The set L is located. (Contributed by Jim
Kingdon, 31Jan2024.)



Theorem  dedekindeulemlub 13040* 
Lemma for dedekindeu 13043. The set L has a least upper bound.
(Contributed by Jim Kingdon, 31Jan2024.)



Theorem  dedekindeulemlu 13041* 
Lemma for dedekindeu 13043. There is a number which separates the
lower
and upper cuts. (Contributed by Jim Kingdon, 31Jan2024.)



Theorem  dedekindeulemeu 13042* 
Lemma for dedekindeu 13043. Part of proving uniqueness. (Contributed
by
Jim Kingdon, 31Jan2024.)



Theorem  dedekindeu 13043* 
A Dedekind cut identifies a unique real number. Similar to dfinp 7387
except that the the Dedekind cut is formed by sets of reals (rather than
positive rationals). But in both cases the defining property of a
Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and
located. (Contributed by Jim Kingdon, 5Jan2024.)



Theorem  suplociccreex 13044* 
An inhabited, boundedabove, located set of reals in a closed interval
has a supremum. A similar theorem is axsuploc 7951 but that one is for
the entire real line rather than a closed interval. (Contributed by
Jim Kingdon, 14Feb2024.)



Theorem  suplociccex 13045* 
An inhabited, boundedabove, located set of reals in a closed interval
has a supremum. A similar theorem is axsuploc 7951 but that one is for the
entire real line rather than a closed interval. (Contributed by Jim
Kingdon, 14Feb2024.)



Theorem  dedekindicclemuub 13046* 
Lemma for dedekindicc 13053. Any element of the upper cut is an upper
bound for the lower cut. (Contributed by Jim Kingdon,
15Feb2024.)



Theorem  dedekindicclemub 13047* 
Lemma for dedekindicc 13053. The lower cut has an upper bound.
(Contributed by Jim Kingdon, 15Feb2024.)



Theorem  dedekindicclemloc 13048* 
Lemma for dedekindicc 13053. The set L is located. (Contributed by Jim
Kingdon, 15Feb2024.)



Theorem  dedekindicclemlub 13049* 
Lemma for dedekindicc 13053. The set L has a least upper bound.
(Contributed by Jim Kingdon, 15Feb2024.)



Theorem  dedekindicclemlu 13050* 
Lemma for dedekindicc 13053. There is a number which separates the
lower
and upper cuts. (Contributed by Jim Kingdon, 15Feb2024.)



Theorem  dedekindicclemeu 13051* 
Lemma for dedekindicc 13053. Part of proving uniqueness. (Contributed
by Jim Kingdon, 15Feb2024.)



Theorem  dedekindicclemicc 13052* 
Lemma for dedekindicc 13053. Same as dedekindicc 13053, except that we
merely show
to be an element of .
Later we will
strengthen that to . (Contributed by Jim Kingdon,
5Jan2024.)



Theorem  dedekindicc 13053* 
A Dedekind cut identifies a unique real number. Similar to dfinp 7387
except that the Dedekind cut is formed by sets of reals (rather than
positive rationals). But in both cases the defining property of a
Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and
located. (Contributed by Jim Kingdon, 19Feb2024.)



8.0.2 Intermediate value theorem


Theorem  ivthinclemlm 13054* 
Lemma for ivthinc 13063. The lower cut is bounded. (Contributed by
Jim Kingdon, 18Feb2024.)



Theorem  ivthinclemum 13055* 
Lemma for ivthinc 13063. The upper cut is bounded. (Contributed by
Jim Kingdon, 18Feb2024.)



Theorem  ivthinclemlopn 13056* 
Lemma for ivthinc 13063. The lower cut is open. (Contributed by
Jim
Kingdon, 6Feb2024.)



Theorem  ivthinclemlr 13057* 
Lemma for ivthinc 13063. The lower cut is rounded. (Contributed by
Jim Kingdon, 18Feb2024.)



Theorem  ivthinclemuopn 13058* 
Lemma for ivthinc 13063. The upper cut is open. (Contributed by
Jim
Kingdon, 19Feb2024.)



Theorem  ivthinclemur 13059* 
Lemma for ivthinc 13063. The upper cut is rounded. (Contributed by
Jim Kingdon, 18Feb2024.)



Theorem  ivthinclemdisj 13060* 
Lemma for ivthinc 13063. The lower and upper cuts are disjoint.
(Contributed by Jim Kingdon, 18Feb2024.)



Theorem  ivthinclemloc 13061* 
Lemma for ivthinc 13063. Locatedness. (Contributed by Jim Kingdon,
18Feb2024.)



Theorem  ivthinclemex 13062* 
Lemma for ivthinc 13063. Existence of a number between the lower
cut
and the upper cut. (Contributed by Jim Kingdon, 20Feb2024.)



Theorem  ivthinc 13063* 
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,
5Feb2024.)



Theorem  ivthdec 13064* 
The intermediate value theorem, decreasing case, for a strictly
monotonic function. (Contributed by Jim Kingdon, 20Feb2024.)



8.1 Derivatives


8.1.1 Real and complex
differentiation


8.1.1.1 Derivatives of functions of one complex
or real variable


Syntax  climc 13065 
The limit operator.

lim 

Syntax  cdv 13066 
The derivative operator.



Definition  dflimced 13067* 
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, 24Dec2016.)
(Revised by Jim Kingdon, 3Jun2023.)

lim
# 

Definition  dfdvap 13068* 
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 wellbehaved 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, 7Aug2014.) (Revised by Jim Kingdon,
25Jun2023.)

↾_{t} #
lim 

Theorem  limcrcl 13069 
Reverse closure for the limit operator. (Contributed by Mario Carneiro,
28Dec2016.)

lim


Theorem  limccl 13070 
Closure of the limit operator. (Contributed by Mario Carneiro,
25Dec2016.)

lim 

Theorem  ellimc3apf 13071* 
Write the epsilondelta definition of a limit. (Contributed by Mario
Carneiro, 28Dec2016.) (Revised by Jim Kingdon, 4Nov2023.)

lim # 

Theorem  ellimc3ap 13072* 
Write the epsilondelta definition of a limit. (Contributed by Mario
Carneiro, 28Dec2016.) Use apartness. (Revised by Jim Kingdon,
3Jun2023.)

lim # 

Theorem  limcdifap 13073* 
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, 25Dec2016.) (Revised by Jim Kingdon,
3Jun2023.)

lim #
lim 

Theorem  limcmpted 13074* 
Express the limit operator for a function defined by a mapping, via
epsilondelta. (Contributed by Jim Kingdon, 3Nov2023.)

lim #


Theorem  limcimolemlt 13075* 
Lemma for limcimo 13076. (Contributed by Jim Kingdon, 3Jul2023.)

↾_{t} # lim lim #
#


Theorem  limcimo 13076* 
Conditions which ensure there is at most one limit value of at
.
(Contributed by Mario Carneiro, 25Dec2016.) (Revised by
Jim Kingdon, 8Jul2023.)

↾_{t} # lim 

Theorem  limcresi 13077 
Any limit of is also
a limit of the restriction of .
(Contributed by Mario Carneiro, 28Dec2016.)

lim lim 

Theorem  cnplimcim 13078 
If a function is continuous at , its limit at equals the
value of the function there. (Contributed by Mario Carneiro,
28Dec2016.) (Revised by Jim Kingdon, 14Jun2023.)

↾_{t}
lim 

Theorem  cnplimclemle 13079 
Lemma for cnplimccntop 13081. Satisfying the epsilon condition for
continuity. (Contributed by Mario Carneiro and Jim Kingdon,
17Nov2023.)

↾_{t} lim
#


Theorem  cnplimclemr 13080 
Lemma for cnplimccntop 13081. The reverse direction. (Contributed by
Mario Carneiro and Jim Kingdon, 17Nov2023.)

↾_{t} lim 

Theorem  cnplimccntop 13081 
A function is continuous at iff its limit at equals the
value of the function there. (Contributed by Mario Carneiro,
28Dec2016.)

↾_{t}
lim 

Theorem  cnlimcim 13082* 
If is a continuous
function, the limit of the function at each
point equals the value of the function. (Contributed by Mario Carneiro,
28Dec2016.) (Revised by Jim Kingdon, 16Jun2023.)

lim 

Theorem  cnlimc 13083* 
is a continuous
function iff the limit of the function at each
point equals the value of the function. (Contributed by Mario Carneiro,
28Dec2016.)

lim 

Theorem  cnlimci 13084 
If is a continuous
function, then the limit of the function at any
point equals its value. (Contributed by Mario Carneiro,
28Dec2016.)

lim 

Theorem  cnmptlimc 13085* 
If is a continuous
function, then the limit of the function at any
point equals its value. (Contributed by Mario Carneiro,
28Dec2016.)

lim 

Theorem  limccnpcntop 13086 
If the limit of at
is and is continuous at
, then the
limit of at is .
(Contributed by Mario Carneiro, 28Dec2016.) (Revised by Jim Kingdon,
18Jun2023.)

↾_{t} lim
lim 

Theorem  limccnp2lem 13087* 
Lemma for limccnp2cntop 13088. This is most of the result, expressed in
epsilondelta form, with a large number of hypotheses so that lengthy
expressions do not need to be repeated. (Contributed by Jim Kingdon,
9Nov2023.)

↾_{t}
lim
lim
#
#
# 

Theorem  limccnp2cntop 13088* 
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, 28Dec2016.) (Revised by Jim Kingdon,
14Nov2023.)

↾_{t}
lim
lim lim 

Theorem  limccoap 13089* 
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, 29Dec2016.)
(Revised by Jim Kingdon, 18Dec2023.)

#
#
#
# lim
# lim
#
lim 

Theorem  reldvg 13090 
The derivative function is a relation. (Contributed by Mario Carneiro,
7Aug2014.) (Revised by Jim Kingdon, 25Jun2023.)



Theorem  dvlemap 13091* 
Closure for a difference quotient. (Contributed by Mario Carneiro,
1Sep2014.) (Revised by Jim Kingdon, 27Jun2023.)

#


Theorem  dvfvalap 13092* 
Value and set bounds on the derivative operator. (Contributed by Mario
Carneiro, 7Aug2014.) (Revised by Jim Kingdon, 27Jun2023.)

↾_{t}
# lim


Theorem  eldvap 13093* 
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, 7Aug2014.) (Revised by Jim Kingdon,
27Jun2023.)

↾_{t} #
lim 

Theorem  dvcl 13094 
The derivative function takes values in the complex numbers.
(Contributed by Mario Carneiro, 7Aug2014.) (Revised by Mario
Carneiro, 9Feb2015.)



Theorem  dvbssntrcntop 13095 
The set of differentiable points is a subset of the interior of the
domain of the function. (Contributed by Mario Carneiro, 7Aug2014.)
(Revised by Jim Kingdon, 27Jun2023.)

↾_{t} 

Theorem  dvbss 13096 
The set of differentiable points is a subset of the domain of the
function. (Contributed by Mario Carneiro, 6Aug2014.) (Revised by
Mario Carneiro, 9Feb2015.)



Theorem  dvbsssg 13097 
The set of differentiable points is a subset of the ambient topology.
(Contributed by Mario Carneiro, 18Mar2015.) (Revised by Jim Kingdon,
28Jun2023.)



Theorem  recnprss 13098 
Both and are subsets of . (Contributed by Mario
Carneiro, 10Feb2015.)



Theorem  dvfgg 13099 
Explicitly write out the functionality condition on derivative for
and . (Contributed by Mario Carneiro, 9Feb2015.)
(Revised by Jim Kingdon, 28Jun2023.)



Theorem  dvfpm 13100 
The derivative is a function. (Contributed by Mario Carneiro,
8Aug2014.) (Revised by Jim Kingdon, 28Jul2023.)

