Theorem List for Intuitionistic Logic Explorer - 13301-13400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | bl2ioo 13301 |
A ball in terms of an open interval of reals. (Contributed by NM,
18-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
|
|
Theorem | ioo2bl 13302 |
An open interval of reals in terms of a ball. (Contributed by NM,
18-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|
|
|
Theorem | ioo2blex 13303 |
An open interval of reals in terms of a ball. (Contributed by Mario
Carneiro, 14-Nov-2013.)
|
|
|
Theorem | blssioo 13304 |
The balls of the standard real metric space are included in the open
real intervals. (Contributed by NM, 8-May-2007.) (Revised by Mario
Carneiro, 13-Nov-2013.)
|
|
|
Theorem | tgioo 13305 |
The topology generated by open intervals of reals is the same as the
open sets of the standard metric space on the reals. (Contributed by
NM, 7-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
|
|
Theorem | tgqioo 13306 |
The topology generated by open intervals of reals with rational
endpoints is the same as the open sets of the standard metric space on
the reals. In particular, this proves that the standard topology on the
reals is second-countable. (Contributed by Mario Carneiro,
17-Jun-2014.)
|
|
|
Theorem | resubmet 13307 |
The subspace topology induced by a subset of the reals. (Contributed by
Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Aug-2014.)
|
↾t |
|
Theorem | tgioo2cntop 13308 |
The standard topology on the reals is a subspace of the complex metric
topology. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by
Jim Kingdon, 6-Aug-2023.)
|
↾t |
|
Theorem | rerestcntop 13309 |
The subspace topology induced by a subset of the reals. (Contributed by
Mario Carneiro, 13-Aug-2014.) (Revised by Jim Kingdon, 6-Aug-2023.)
|
↾t ↾t |
|
Theorem | addcncntoplem 13310* |
Lemma for addcncntop 13311, subcncntop 13312, and mulcncntop 13313.
(Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon,
22-Oct-2023.)
|
|
|
Theorem | addcncntop 13311 |
Complex number addition is a continuous function. Part of Proposition
14-4.16 of [Gleason] p. 243.
(Contributed by NM, 30-Jul-2007.) (Proof
shortened by Mario Carneiro, 5-May-2014.)
|
|
|
Theorem | subcncntop 13312 |
Complex number subtraction is a continuous function. Part of
Proposition 14-4.16 of [Gleason] p. 243.
(Contributed by NM,
4-Aug-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
|
|
|
Theorem | mulcncntop 13313 |
Complex number multiplication is a continuous function. Part of
Proposition 14-4.16 of [Gleason] p. 243.
(Contributed by NM,
30-Jul-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
|
|
|
Theorem | divcnap 13314* |
Complex number division is a continuous function, when the second
argument is apart from zero. (Contributed by Mario Carneiro,
12-Aug-2014.) (Revised by Jim Kingdon, 25-Oct-2023.)
|
↾t
#
#
|
|
Theorem | fsumcncntop 13315* |
A finite sum of functions to complex numbers from a common topological
space is continuous. The class expression for normally contains
free variables
and to index it.
(Contributed by NM,
8-Aug-2007.) (Revised by Mario Carneiro, 23-Aug-2014.)
|
TopOn
|
|
8.2.7 Topological definitions using the
reals
|
|
Syntax | ccncf 13316 |
Extend class notation to include the operation which returns a class of
continuous complex functions.
|
|
|
Definition | df-cncf 13317* |
Define the operation whose value is a class of continuous complex
functions. (Contributed by Paul Chapman, 11-Oct-2007.)
|
|
|
Theorem | cncfval 13318* |
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 13319* |
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 13320* |
Version of elcncf 13319 with arguments commuted. (Contributed by
Mario
Carneiro, 28-Apr-2014.)
|
|
|
Theorem | cncfrss 13321 |
Reverse closure of the continuous function predicate. (Contributed by
Mario Carneiro, 25-Aug-2014.)
|
|
|
Theorem | cncfrss2 13322 |
Reverse closure of the continuous function predicate. (Contributed by
Mario Carneiro, 25-Aug-2014.)
|
|
|
Theorem | cncff 13323 |
A continuous complex function's domain and codomain. (Contributed by
Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro,
25-Aug-2014.)
|
|
|
Theorem | cncfi 13324* |
Defining property of a continuous function. (Contributed by Mario
Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.)
|
|
|
Theorem | elcncf1di 13325* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
|
|
Theorem | elcncf1ii 13326* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
|
|
Theorem | rescncf 13327 |
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 13328 |
Change the codomain of a continuous complex function. (Contributed by
Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 1-May-2015.)
|
|
|
Theorem | cncfss 13329 |
The set of continuous functions is expanded when the range is expanded.
(Contributed by Mario Carneiro, 30-Aug-2014.)
|
|
|
Theorem | climcncf 13330 |
Image of a limit under a continuous map. (Contributed by Mario
Carneiro, 7-Apr-2015.)
|
|
|
Theorem | abscncf 13331 |
Absolute value is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
|
|
Theorem | recncf 13332 |
Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.)
(Revised by Mario Carneiro, 28-Apr-2014.)
|
|
|
Theorem | imcncf 13333 |
Imaginary part is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
|
|
Theorem | cjcncf 13334 |
Complex conjugate is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
|
|
Theorem | mulc1cncf 13335* |
Multiplication by a constant is continuous. (Contributed by Paul
Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
|
|
Theorem | divccncfap 13336* |
Division by a constant is continuous. (Contributed by Paul Chapman,
28-Nov-2007.) (Revised by Jim Kingdon, 9-Jan-2023.)
|
# |
|
Theorem | cncfco 13337 |
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 13338 |
Relate complex function continuity to metric space continuity.
(Contributed by Paul Chapman, 26-Nov-2007.) (Revised by Mario Carneiro,
7-Sep-2015.)
|
|
|
Theorem | cncfcncntop 13339 |
Relate complex function continuity to topological continuity.
(Contributed by Mario Carneiro, 17-Feb-2015.)
|
↾t ↾t
|
|
Theorem | cncfcn1cntop 13340 |
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 13341* |
A constant function is a continuous function on . (Contributed
by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro,
7-Sep-2015.)
|
|
|
Theorem | cncfmptid 13342* |
The identity function is a continuous function on . (Contributed
by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro,
17-May-2016.)
|
|
|
Theorem | cncfmpt1f 13343* |
Composition of continuous functions. analogue of cnmpt11f 13043.
(Contributed by Mario Carneiro, 3-Sep-2014.)
|
|
|
Theorem | cncfmpt2fcntop 13344* |
Composition of continuous functions. analogue of cnmpt12f 13045.
(Contributed by Mario Carneiro, 3-Sep-2014.)
|
|
|
Theorem | addccncf 13345* |
Adding a constant is a continuous function. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
|
|
Theorem | cdivcncfap 13346* |
Division with a constant numerator is continuous. (Contributed by Mario
Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 26-May-2023.)
|
#
#
|
|
Theorem | negcncf 13347* |
The negative function is continuous. (Contributed by Mario Carneiro,
30-Dec-2016.)
|
|
|
Theorem | negfcncf 13348* |
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 13349* |
Lemma for mulcncf 13350. (Contributed by Jim Kingdon, 29-May-2023.)
|
|
|
Theorem | mulcncf 13350* |
The multiplication of two continuous complex functions is continuous.
(Contributed by Glauco Siliprandi, 29-Jun-2017.)
|
|
|
Theorem | expcncf 13351* |
The power function on complex numbers, for fixed exponent N, is
continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|
|
|
Theorem | cnrehmeocntop 13352* |
The canonical bijection from to described in
cnref1o 9602 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 13353* |
The complex numbers apart from a given complex number form an open set.
(Contributed by Jim Kingdon, 14-Dec-2023.)
|
#
|
|
PART 9 BASIC REAL AND COMPLEX
ANALYSIS
|
|
9.0.1 Dedekind cuts
|
|
Theorem | dedekindeulemuub 13354* |
Lemma for dedekindeu 13360. Any element of the upper cut is an upper
bound for the lower cut. (Contributed by Jim Kingdon, 2-Feb-2024.)
|
|
|
Theorem | dedekindeulemub 13355* |
Lemma for dedekindeu 13360. The lower cut has an upper bound.
(Contributed by Jim Kingdon, 31-Jan-2024.)
|
|
|
Theorem | dedekindeulemloc 13356* |
Lemma for dedekindeu 13360. The set L is located. (Contributed by Jim
Kingdon, 31-Jan-2024.)
|
|
|
Theorem | dedekindeulemlub 13357* |
Lemma for dedekindeu 13360. The set L has a least upper bound.
(Contributed by Jim Kingdon, 31-Jan-2024.)
|
|
|
Theorem | dedekindeulemlu 13358* |
Lemma for dedekindeu 13360. There is a number which separates the
lower
and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.)
|
|
|
Theorem | dedekindeulemeu 13359* |
Lemma for dedekindeu 13360. Part of proving uniqueness. (Contributed
by
Jim Kingdon, 31-Jan-2024.)
|
|
|
Theorem | dedekindeu 13360* |
A Dedekind cut identifies a unique real number. Similar to df-inp 7421
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 13361* |
An inhabited, bounded-above, located set of reals in a closed interval
has a supremum. A similar theorem is axsuploc 7985 but that one is for
the entire real line rather than a closed interval. (Contributed by
Jim Kingdon, 14-Feb-2024.)
|
|
|
Theorem | suplociccex 13362* |
An inhabited, bounded-above, located set of reals in a closed interval
has a supremum. A similar theorem is axsuploc 7985 but that one is for the
entire real line rather than a closed interval. (Contributed by Jim
Kingdon, 14-Feb-2024.)
|
|
|
Theorem | dedekindicclemuub 13363* |
Lemma for dedekindicc 13370. Any element of the upper cut is an upper
bound for the lower cut. (Contributed by Jim Kingdon,
15-Feb-2024.)
|
|
|
Theorem | dedekindicclemub 13364* |
Lemma for dedekindicc 13370. The lower cut has an upper bound.
(Contributed by Jim Kingdon, 15-Feb-2024.)
|
|
|
Theorem | dedekindicclemloc 13365* |
Lemma for dedekindicc 13370. The set L is located. (Contributed by Jim
Kingdon, 15-Feb-2024.)
|
|
|
Theorem | dedekindicclemlub 13366* |
Lemma for dedekindicc 13370. The set L has a least upper bound.
(Contributed by Jim Kingdon, 15-Feb-2024.)
|
|
|
Theorem | dedekindicclemlu 13367* |
Lemma for dedekindicc 13370. There is a number which separates the
lower
and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.)
|
|
|
Theorem | dedekindicclemeu 13368* |
Lemma for dedekindicc 13370. Part of proving uniqueness. (Contributed
by Jim Kingdon, 15-Feb-2024.)
|
|
|
Theorem | dedekindicclemicc 13369* |
Lemma for dedekindicc 13370. Same as dedekindicc 13370, 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 13370* |
A Dedekind cut identifies a unique real number. Similar to df-inp 7421
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.)
|
|
|
9.0.2 Intermediate value theorem
|
|
Theorem | ivthinclemlm 13371* |
Lemma for ivthinc 13380. The lower cut is bounded. (Contributed by
Jim Kingdon, 18-Feb-2024.)
|
|
|
Theorem | ivthinclemum 13372* |
Lemma for ivthinc 13380. The upper cut is bounded. (Contributed by
Jim Kingdon, 18-Feb-2024.)
|
|
|
Theorem | ivthinclemlopn 13373* |
Lemma for ivthinc 13380. The lower cut is open. (Contributed by
Jim
Kingdon, 6-Feb-2024.)
|
|
|
Theorem | ivthinclemlr 13374* |
Lemma for ivthinc 13380. The lower cut is rounded. (Contributed by
Jim Kingdon, 18-Feb-2024.)
|
|
|
Theorem | ivthinclemuopn 13375* |
Lemma for ivthinc 13380. The upper cut is open. (Contributed by
Jim
Kingdon, 19-Feb-2024.)
|
|
|
Theorem | ivthinclemur 13376* |
Lemma for ivthinc 13380. The upper cut is rounded. (Contributed by
Jim Kingdon, 18-Feb-2024.)
|
|
|
Theorem | ivthinclemdisj 13377* |
Lemma for ivthinc 13380. The lower and upper cuts are disjoint.
(Contributed by Jim Kingdon, 18-Feb-2024.)
|
|
|
Theorem | ivthinclemloc 13378* |
Lemma for ivthinc 13380. Locatedness. (Contributed by Jim Kingdon,
18-Feb-2024.)
|
|
|
Theorem | ivthinclemex 13379* |
Lemma for ivthinc 13380. Existence of a number between the lower
cut
and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.)
|
|
|
Theorem | ivthinc 13380* |
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 13381* |
The intermediate value theorem, decreasing case, for a strictly
monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.)
|
|
|
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 13382 |
The limit operator.
|
lim |
|
Syntax | cdv 13383 |
The derivative operator.
|
|
|
Definition | df-limced 13384* |
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 13385* |
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 13386 |
Reverse closure for the limit operator. (Contributed by Mario Carneiro,
28-Dec-2016.)
|
lim
|
|
Theorem | limccl 13387 |
Closure of the limit operator. (Contributed by Mario Carneiro,
25-Dec-2016.)
|
lim |
|
Theorem | ellimc3apf 13388* |
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 13389* |
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 13390* |
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 13391* |
Express the limit operator for a function defined by a mapping, via
epsilon-delta. (Contributed by Jim Kingdon, 3-Nov-2023.)
|
lim #
|
|
Theorem | limcimolemlt 13392* |
Lemma for limcimo 13393. (Contributed by Jim Kingdon, 3-Jul-2023.)
|
↾t # lim lim #
#
|
|
Theorem | limcimo 13393* |
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 13394 |
Any limit of is also
a limit of the restriction of .
(Contributed by Mario Carneiro, 28-Dec-2016.)
|
lim lim |
|
Theorem | cnplimcim 13395 |
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 13396 |
Lemma for cnplimccntop 13398. Satisfying the epsilon condition for
continuity. (Contributed by Mario Carneiro and Jim Kingdon,
17-Nov-2023.)
|
↾t lim
#
|
|
Theorem | cnplimclemr 13397 |
Lemma for cnplimccntop 13398. The reverse direction. (Contributed by
Mario Carneiro and Jim Kingdon, 17-Nov-2023.)
|
↾t lim |
|
Theorem | cnplimccntop 13398 |
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 13399* |
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 13400* |
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 |