Theorem List for Intuitionistic Logic Explorer - 13001-13100 *Has distinct variable
group(s)
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, 11-Oct-2007.) (Revised by Mario Carneiro, 9-Nov-2013.)
|
|
|
Theorem | elcncf 13002* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 11-Oct-2007.) (Revised by Mario
Carneiro, 9-Nov-2013.)
|
|
|
Theorem | elcncf2 13003* |
Version of elcncf 13002 with arguments commuted. (Contributed by
Mario
Carneiro, 28-Apr-2014.)
|
|
|
Theorem | cncfrss 13004 |
Reverse closure of the continuous function predicate. (Contributed by
Mario Carneiro, 25-Aug-2014.)
|
|
|
Theorem | cncfrss2 13005 |
Reverse closure of the continuous function predicate. (Contributed by
Mario Carneiro, 25-Aug-2014.)
|
|
|
Theorem | cncff 13006 |
A continuous complex function's domain and codomain. (Contributed by
Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro,
25-Aug-2014.)
|
|
|
Theorem | cncfi 13007* |
Defining property of a continuous function. (Contributed by Mario
Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.)
|
|
|
Theorem | elcncf1di 13008* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
|
|
Theorem | elcncf1ii 13009* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
|
|
Theorem | rescncf 13010 |
A continuous complex function restricted to a subset is continuous.
(Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro,
25-Aug-2014.)
|
|
|
Theorem | cncffvrn 13011 |
Change the codomain of a continuous complex function. (Contributed by
Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 1-May-2015.)
|
|
|
Theorem | cncfss 13012 |
The set of continuous functions is expanded when the range is expanded.
(Contributed by Mario Carneiro, 30-Aug-2014.)
|
|
|
Theorem | climcncf 13013 |
Image of a limit under a continuous map. (Contributed by Mario
Carneiro, 7-Apr-2015.)
|
|
|
Theorem | abscncf 13014 |
Absolute value is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
|
|
Theorem | recncf 13015 |
Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.)
(Revised by Mario Carneiro, 28-Apr-2014.)
|
|
|
Theorem | imcncf 13016 |
Imaginary part is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
|
|
Theorem | cjcncf 13017 |
Complex conjugate is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
|
|
Theorem | mulc1cncf 13018* |
Multiplication by a constant is continuous. (Contributed by Paul
Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
|
|
Theorem | divccncfap 13019* |
Division by a constant is continuous. (Contributed by Paul Chapman,
28-Nov-2007.) (Revised by Jim Kingdon, 9-Jan-2023.)
|
# |
|
Theorem | cncfco 13020 |
The composition of two continuous maps on complex numbers is also
continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by
Mario Carneiro, 25-Aug-2014.)
|
|
|
Theorem | cncfmet 13021 |
Relate complex function continuity to metric space continuity.
(Contributed by Paul Chapman, 26-Nov-2007.) (Revised by Mario Carneiro,
7-Sep-2015.)
|
|
|
Theorem | cncfcncntop 13022 |
Relate complex function continuity to topological continuity.
(Contributed by Mario Carneiro, 17-Feb-2015.)
|
↾t ↾t
|
|
Theorem | cncfcn1cntop 13023 |
Relate complex function continuity to topological continuity.
(Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro,
7-Sep-2015.) (Revised by Jim Kingdon, 16-Jun-2023.)
|
|
|
Theorem | cncfmptc 13024* |
A constant function is a continuous function on . (Contributed
by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro,
7-Sep-2015.)
|
|
|
Theorem | cncfmptid 13025* |
The identity function is a continuous function on . (Contributed
by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro,
17-May-2016.)
|
|
|
Theorem | cncfmpt1f 13026* |
Composition of continuous functions. analogue of cnmpt11f 12726.
(Contributed by Mario Carneiro, 3-Sep-2014.)
|
|
|
Theorem | cncfmpt2fcntop 13027* |
Composition of continuous functions. analogue of cnmpt12f 12728.
(Contributed by Mario Carneiro, 3-Sep-2014.)
|
|
|
Theorem | addccncf 13028* |
Adding a constant is a continuous function. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
|
|
Theorem | cdivcncfap 13029* |
Division with a constant numerator is continuous. (Contributed by Mario
Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 26-May-2023.)
|
#
#
|
|
Theorem | negcncf 13030* |
The negative function is continuous. (Contributed by Mario Carneiro,
30-Dec-2016.)
|
|
|
Theorem | negfcncf 13031* |
The negative of a continuous complex function is continuous.
(Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro,
25-Aug-2014.)
|
|
|
Theorem | mulcncflem 13032* |
Lemma for mulcncf 13033. (Contributed by Jim Kingdon, 29-May-2023.)
|
|
|
Theorem | mulcncf 13033* |
The multiplication of two continuous complex functions is continuous.
(Contributed by Glauco Siliprandi, 29-Jun-2017.)
|
|
|
Theorem | expcncf 13034* |
The power function on complex numbers, for fixed exponent N, is
continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|
|
|
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,
25-Aug-2014.)
|
|
|
Theorem | cnopnap 13036* |
The complex numbers apart from a given complex number form an open set.
(Contributed by Jim Kingdon, 14-Dec-2023.)
|
#
|
|
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, 2-Feb-2024.)
|
|
|
Theorem | dedekindeulemub 13038* |
Lemma for dedekindeu 13043. The lower cut has an upper bound.
(Contributed by Jim Kingdon, 31-Jan-2024.)
|
|
|
Theorem | dedekindeulemloc 13039* |
Lemma for dedekindeu 13043. The set L is located. (Contributed by Jim
Kingdon, 31-Jan-2024.)
|
|
|
Theorem | dedekindeulemlub 13040* |
Lemma for dedekindeu 13043. The set L has a least upper bound.
(Contributed by Jim Kingdon, 31-Jan-2024.)
|
|
|
Theorem | dedekindeulemlu 13041* |
Lemma for dedekindeu 13043. There is a number which separates the
lower
and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.)
|
|
|
Theorem | dedekindeulemeu 13042* |
Lemma for dedekindeu 13043. Part of proving uniqueness. (Contributed
by
Jim Kingdon, 31-Jan-2024.)
|
|
|
Theorem | dedekindeu 13043* |
A Dedekind cut identifies a unique real number. Similar to df-inp 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, 5-Jan-2024.)
|
|
|
Theorem | suplociccreex 13044* |
An inhabited, bounded-above, 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, 14-Feb-2024.)
|
|
|
Theorem | suplociccex 13045* |
An inhabited, bounded-above, 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, 14-Feb-2024.)
|
|
|
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,
15-Feb-2024.)
|
|
|
Theorem | dedekindicclemub 13047* |
Lemma for dedekindicc 13053. The lower cut has an upper bound.
(Contributed by Jim Kingdon, 15-Feb-2024.)
|
|
|
Theorem | dedekindicclemloc 13048* |
Lemma for dedekindicc 13053. The set L is located. (Contributed by Jim
Kingdon, 15-Feb-2024.)
|
|
|
Theorem | dedekindicclemlub 13049* |
Lemma for dedekindicc 13053. The set L has a least upper bound.
(Contributed by Jim Kingdon, 15-Feb-2024.)
|
|
|
Theorem | dedekindicclemlu 13050* |
Lemma for dedekindicc 13053. There is a number which separates the
lower
and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.)
|
|
|
Theorem | dedekindicclemeu 13051* |
Lemma for dedekindicc 13053. Part of proving uniqueness. (Contributed
by Jim Kingdon, 15-Feb-2024.)
|
|
|
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,
5-Jan-2024.)
|
|
|
Theorem | dedekindicc 13053* |
A Dedekind cut identifies a unique real number. Similar to df-inp 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, 19-Feb-2024.)
|
|
|
8.0.2 Intermediate value theorem
|
|
Theorem | ivthinclemlm 13054* |
Lemma for ivthinc 13063. The lower cut is bounded. (Contributed by
Jim Kingdon, 18-Feb-2024.)
|
|
|
Theorem | ivthinclemum 13055* |
Lemma for ivthinc 13063. The upper cut is bounded. (Contributed by
Jim Kingdon, 18-Feb-2024.)
|
|
|
Theorem | ivthinclemlopn 13056* |
Lemma for ivthinc 13063. The lower cut is open. (Contributed by
Jim
Kingdon, 6-Feb-2024.)
|
|
|
Theorem | ivthinclemlr 13057* |
Lemma for ivthinc 13063. The lower cut is rounded. (Contributed by
Jim Kingdon, 18-Feb-2024.)
|
|
|
Theorem | ivthinclemuopn 13058* |
Lemma for ivthinc 13063. The upper cut is open. (Contributed by
Jim
Kingdon, 19-Feb-2024.)
|
|
|
Theorem | ivthinclemur 13059* |
Lemma for ivthinc 13063. The upper cut is rounded. (Contributed by
Jim Kingdon, 18-Feb-2024.)
|
|
|
Theorem | ivthinclemdisj 13060* |
Lemma for ivthinc 13063. The lower and upper cuts are disjoint.
(Contributed by Jim Kingdon, 18-Feb-2024.)
|
|
|
Theorem | ivthinclemloc 13061* |
Lemma for ivthinc 13063. Locatedness. (Contributed by Jim Kingdon,
18-Feb-2024.)
|
|
|
Theorem | ivthinclemex 13062* |
Lemma for ivthinc 13063. Existence of a number between the lower
cut
and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.)
|
|
|
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,
5-Feb-2024.)
|
|
|
Theorem | ivthdec 13064* |
The intermediate value theorem, decreasing case, for a strictly
monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.)
|
|
|
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 | df-limced 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, 24-Dec-2016.)
(Revised by Jim Kingdon, 3-Jun-2023.)
|
lim
# |
|
Definition | df-dvap 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 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 13069 |
Reverse closure for the limit operator. (Contributed by Mario Carneiro,
28-Dec-2016.)
|
lim
|
|
Theorem | limccl 13070 |
Closure of the limit operator. (Contributed by Mario Carneiro,
25-Dec-2016.)
|
lim |
|
Theorem | ellimc3apf 13071* |
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 13072* |
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 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, 25-Dec-2016.) (Revised by Jim Kingdon,
3-Jun-2023.)
|
lim #
lim |
|
Theorem | limcmpted 13074* |
Express the limit operator for a function defined by a mapping, via
epsilon-delta. (Contributed by Jim Kingdon, 3-Nov-2023.)
|
lim #
|
|
Theorem | limcimolemlt 13075* |
Lemma for limcimo 13076. (Contributed by Jim Kingdon, 3-Jul-2023.)
|
↾t # lim lim #
#
|
|
Theorem | limcimo 13076* |
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 13077 |
Any limit of is also
a limit of the restriction of .
(Contributed by Mario Carneiro, 28-Dec-2016.)
|
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,
28-Dec-2016.) (Revised by Jim Kingdon, 14-Jun-2023.)
|
↾t
lim |
|
Theorem | cnplimclemle 13079 |
Lemma for cnplimccntop 13081. Satisfying the epsilon condition for
continuity. (Contributed by Mario Carneiro and Jim Kingdon,
17-Nov-2023.)
|
↾t lim
#
|
|
Theorem | cnplimclemr 13080 |
Lemma for cnplimccntop 13081. The reverse direction. (Contributed by
Mario Carneiro and Jim Kingdon, 17-Nov-2023.)
|
↾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,
28-Dec-2016.)
|
↾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,
28-Dec-2016.) (Revised by Jim Kingdon, 16-Jun-2023.)
|
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,
28-Dec-2016.)
|
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,
28-Dec-2016.)
|
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,
28-Dec-2016.)
|
lim |
|
Theorem | limccnpcntop 13086 |
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 13087* |
Lemma for limccnp2cntop 13088. 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 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, 28-Dec-2016.) (Revised by Jim Kingdon,
14-Nov-2023.)
|
↾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, 29-Dec-2016.)
(Revised by Jim Kingdon, 18-Dec-2023.)
|
#
#
#
# lim
# lim
#
lim |
|
Theorem | reldvg 13090 |
The derivative function is a relation. (Contributed by Mario Carneiro,
7-Aug-2014.) (Revised by Jim Kingdon, 25-Jun-2023.)
|
|
|
Theorem | dvlemap 13091* |
Closure for a difference quotient. (Contributed by Mario Carneiro,
1-Sep-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
|
#
|
|
Theorem | dvfvalap 13092* |
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 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, 7-Aug-2014.) (Revised by Jim Kingdon,
27-Jun-2023.)
|
↾t #
lim |
|
Theorem | dvcl 13094 |
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 13095 |
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 13096 |
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 13097 |
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 13098 |
Both and are subsets of . (Contributed by Mario
Carneiro, 10-Feb-2015.)
|
|
|
Theorem | dvfgg 13099 |
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 13100 |
The derivative is a function. (Contributed by Mario Carneiro,
8-Aug-2014.) (Revised by Jim Kingdon, 28-Jul-2023.)
|
|