Theorem List for Intuitionistic Logic Explorer - 13201-13300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | suplociccex 13201* |
An inhabited, bounded-above, located set of reals in a closed interval
has a supremum. A similar theorem is axsuploc 7965 but that one is for the
entire real line rather than a closed interval. (Contributed by Jim
Kingdon, 14-Feb-2024.)
|
|
|
Theorem | dedekindicclemuub 13202* |
Lemma for dedekindicc 13209. Any element of the upper cut is an upper
bound for the lower cut. (Contributed by Jim Kingdon,
15-Feb-2024.)
|
|
|
Theorem | dedekindicclemub 13203* |
Lemma for dedekindicc 13209. The lower cut has an upper bound.
(Contributed by Jim Kingdon, 15-Feb-2024.)
|
|
|
Theorem | dedekindicclemloc 13204* |
Lemma for dedekindicc 13209. The set L is located. (Contributed by Jim
Kingdon, 15-Feb-2024.)
|
|
|
Theorem | dedekindicclemlub 13205* |
Lemma for dedekindicc 13209. The set L has a least upper bound.
(Contributed by Jim Kingdon, 15-Feb-2024.)
|
|
|
Theorem | dedekindicclemlu 13206* |
Lemma for dedekindicc 13209. There is a number which separates the
lower
and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.)
|
|
|
Theorem | dedekindicclemeu 13207* |
Lemma for dedekindicc 13209. Part of proving uniqueness. (Contributed
by Jim Kingdon, 15-Feb-2024.)
|
|
|
Theorem | dedekindicclemicc 13208* |
Lemma for dedekindicc 13209. Same as dedekindicc 13209, 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 13209* |
A Dedekind cut identifies a unique real number. Similar to df-inp 7401
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 13210* |
Lemma for ivthinc 13219. The lower cut is bounded. (Contributed by
Jim Kingdon, 18-Feb-2024.)
|
|
|
Theorem | ivthinclemum 13211* |
Lemma for ivthinc 13219. The upper cut is bounded. (Contributed by
Jim Kingdon, 18-Feb-2024.)
|
|
|
Theorem | ivthinclemlopn 13212* |
Lemma for ivthinc 13219. The lower cut is open. (Contributed by
Jim
Kingdon, 6-Feb-2024.)
|
|
|
Theorem | ivthinclemlr 13213* |
Lemma for ivthinc 13219. The lower cut is rounded. (Contributed by
Jim Kingdon, 18-Feb-2024.)
|
|
|
Theorem | ivthinclemuopn 13214* |
Lemma for ivthinc 13219. The upper cut is open. (Contributed by
Jim
Kingdon, 19-Feb-2024.)
|
|
|
Theorem | ivthinclemur 13215* |
Lemma for ivthinc 13219. The upper cut is rounded. (Contributed by
Jim Kingdon, 18-Feb-2024.)
|
|
|
Theorem | ivthinclemdisj 13216* |
Lemma for ivthinc 13219. The lower and upper cuts are disjoint.
(Contributed by Jim Kingdon, 18-Feb-2024.)
|
|
|
Theorem | ivthinclemloc 13217* |
Lemma for ivthinc 13219. Locatedness. (Contributed by Jim Kingdon,
18-Feb-2024.)
|
|
|
Theorem | ivthinclemex 13218* |
Lemma for ivthinc 13219. Existence of a number between the lower
cut
and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.)
|
|
|
Theorem | ivthinc 13219* |
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 13220* |
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 13221 |
The limit operator.
|
lim |
|
Syntax | cdv 13222 |
The derivative operator.
|
|
|
Definition | df-limced 13223* |
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 13224* |
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 13225 |
Reverse closure for the limit operator. (Contributed by Mario Carneiro,
28-Dec-2016.)
|
lim
|
|
Theorem | limccl 13226 |
Closure of the limit operator. (Contributed by Mario Carneiro,
25-Dec-2016.)
|
lim |
|
Theorem | ellimc3apf 13227* |
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 13228* |
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 13229* |
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 13230* |
Express the limit operator for a function defined by a mapping, via
epsilon-delta. (Contributed by Jim Kingdon, 3-Nov-2023.)
|
lim #
|
|
Theorem | limcimolemlt 13231* |
Lemma for limcimo 13232. (Contributed by Jim Kingdon, 3-Jul-2023.)
|
↾t # lim lim #
#
|
|
Theorem | limcimo 13232* |
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 13233 |
Any limit of is also
a limit of the restriction of .
(Contributed by Mario Carneiro, 28-Dec-2016.)
|
lim lim |
|
Theorem | cnplimcim 13234 |
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 13235 |
Lemma for cnplimccntop 13237. Satisfying the epsilon condition for
continuity. (Contributed by Mario Carneiro and Jim Kingdon,
17-Nov-2023.)
|
↾t lim
#
|
|
Theorem | cnplimclemr 13236 |
Lemma for cnplimccntop 13237. The reverse direction. (Contributed by
Mario Carneiro and Jim Kingdon, 17-Nov-2023.)
|
↾t lim |
|
Theorem | cnplimccntop 13237 |
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 13238* |
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 13239* |
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 13240 |
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 13241* |
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 13242 |
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 13243* |
Lemma for limccnp2cntop 13244. 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 13244* |
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 13245* |
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 13246 |
The derivative function is a relation. (Contributed by Mario Carneiro,
7-Aug-2014.) (Revised by Jim Kingdon, 25-Jun-2023.)
|
|
|
Theorem | dvlemap 13247* |
Closure for a difference quotient. (Contributed by Mario Carneiro,
1-Sep-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
|
#
|
|
Theorem | dvfvalap 13248* |
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 13249* |
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 13250 |
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 13251 |
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 13252 |
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 13253 |
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 13254 |
Both and are subsets of . (Contributed by Mario
Carneiro, 10-Feb-2015.)
|
|
|
Theorem | dvfgg 13255 |
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 13256 |
The derivative is a function. (Contributed by Mario Carneiro,
8-Aug-2014.) (Revised by Jim Kingdon, 28-Jul-2023.)
|
|
|
Theorem | dvfcnpm 13257 |
The derivative is a function. (Contributed by Mario Carneiro,
9-Feb-2015.) (Revised by Jim Kingdon, 28-Jul-2023.)
|
|
|
Theorem | dvidlemap 13258* |
Lemma for dvid 13260 and dvconst 13259. (Contributed by Mario Carneiro,
8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|
#
|
|
Theorem | dvconst 13259 |
Derivative of a constant function. (Contributed by Mario Carneiro,
8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|
|
|
Theorem | dvid 13260 |
Derivative of the identity function. (Contributed by Mario Carneiro,
8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|
|
|
Theorem | dvcnp2cntop 13261 |
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 13262 |
A differentiable function is continuous. (Contributed by Mario
Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-Sep-2015.)
|
|
|
Theorem | dvaddxxbr 13263 |
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 13264 |
The product rule for derivatives at a point. For the (simpler but
more limited) function version, see dvmulxx 13266. (Contributed by Mario
Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.)
|
|
|
Theorem | dvaddxx 13265 |
The sum rule for derivatives at a point. For the (more general)
relation version, see dvaddxxbr 13263. (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.)
|
|
|
Theorem | dvmulxx 13266 |
The product rule for derivatives at a point. For the (more general)
relation version, see dvmulxxbr 13264. (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Jim Kingdon, 2-Dec-2023.)
|
|
|
Theorem | dviaddf 13267 |
The sum rule for everywhere-differentiable functions. (Contributed by
Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro,
10-Feb-2015.)
|
|
|
Theorem | dvimulf 13268 |
The product rule for everywhere-differentiable functions. (Contributed
by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro,
10-Feb-2015.)
|
|
|
Theorem | dvcoapbr 13269* |
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 13270 |
The derivative of the conjugate of a function. For the (simpler but
more limited) function version, see dvcj 13271. (Contributed by Mario
Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|
|
|
Theorem | dvcj 13271 |
The derivative of the conjugate of a function. For the (more general)
relation version, see dvcjbr 13270. (Contributed by Mario Carneiro,
1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|
|
|
Theorem | dvfre 13272 |
The derivative of a real function is real. (Contributed by Mario
Carneiro, 1-Sep-2014.)
|
|
|
Theorem | dvexp 13273* |
Derivative of a power function. (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|
|
|
Theorem | dvexp2 13274* |
Derivative of an exponential, possibly zero power. (Contributed by
Stefan O'Rear, 13-Nov-2014.) (Revised by Mario Carneiro,
10-Feb-2015.)
|
|
|
Theorem | dvrecap 13275* |
Derivative of the reciprocal function. (Contributed by Mario Carneiro,
25-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.)
|
# #
|
|
Theorem | dvmptidcn 13276 |
Function-builder for derivative: derivative of the identity.
(Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
30-Dec-2023.)
|
|
|
Theorem | dvmptccn 13277* |
Function-builder for derivative: derivative of a constant. (Contributed
by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
30-Dec-2023.)
|
|
|
Theorem | dvmptclx 13278* |
Closure lemma for dvmptmulx 13280 and other related theorems. (Contributed
by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro,
11-Feb-2015.)
|
|
|
Theorem | dvmptaddx 13279* |
Function-builder for derivative, addition rule. (Contributed by Mario
Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|
|
|
Theorem | dvmptmulx 13280* |
Function-builder for derivative, product rule. (Contributed by Mario
Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|
|
|
Theorem | dvmptcmulcn 13281* |
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 13282* |
Function-builder for derivative, product rule for negatives.
(Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
31-Dec-2023.)
|
|
|
Theorem | dvmptsubcn 13283* |
Function-builder for derivative, subtraction rule. (Contributed by
Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
31-Dec-2023.)
|
|
|
Theorem | dvmptcjx 13284* |
Function-builder for derivative, conjugate rule. (Contributed by Mario
Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 24-May-2024.)
|
|
|
Theorem | dveflem 13285 |
Derivative of the exponential function at 0. The key step in the proof
is eftlub 11625, to show that
.
(Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario
Carneiro, 28-Dec-2016.)
|
|
|
Theorem | dvef 13286 |
Derivative of the exponential function. (Contributed by Mario Carneiro,
9-Aug-2014.) (Proof shortened by Mario Carneiro, 10-Feb-2015.)
|
|
|
PART 9 BASIC REAL AND COMPLEX
FUNCTIONS
|
|
9.1 Basic trigonometry
|
|
9.1.1 The exponential, sine, and cosine
functions (cont.)
|
|
Theorem | efcn 13287 |
The exponential function is continuous. (Contributed by Paul Chapman,
15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.)
|
|
|
Theorem | sincn 13288 |
Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.)
(Revised by Mario Carneiro, 3-Sep-2014.)
|
|
|
Theorem | coscn 13289 |
Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.)
(Revised by Mario Carneiro, 3-Sep-2014.)
|
|
|
Theorem | reeff1olem 13290* |
Lemma for reeff1o 13292. (Contributed by Paul Chapman,
18-Oct-2007.)
(Revised by Mario Carneiro, 30-Apr-2014.)
|
|
|
Theorem | reeff1oleme 13291* |
Lemma for reeff1o 13292. (Contributed by Jim Kingdon, 15-May-2024.)
|
|
|
Theorem | reeff1o 13292 |
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 13293 |
Lemma for eflt 13294. The converse of efltim 11633 plus the epsilon-delta
setup. (Contributed by Jim Kingdon, 22-May-2024.)
|
|
|
Theorem | eflt 13294 |
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 13295 |
The exponential function on the reals is nondecreasing. (Contributed by
Mario Carneiro, 11-Mar-2014.)
|
|
|
Theorem | reefiso 13296 |
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 13297 |
Apartness and the exponential function for reals. (Contributed by Jim
Kingdon, 11-Jul-2024.)
|
# # |
|
9.1.2 Properties of pi =
3.14159...
|
|
Theorem | pilem1 13298 |
Lemma for pire , pigt2lt4 and sinpi . (Contributed by Mario Carneiro,
9-May-2014.)
|
|
|
Theorem | cosz12 13299 |
Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and
Jim Kingdon, 7-Mar-2024.)
|
|
|
Theorem | sin0pilem1 13300* |
Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim
Kingdon, 8-Mar-2024.)
|
|