Type | Label | Description |
Statement |
|
Theorem | ellimc3ap 14401* |
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β π΅) β (πΆ β β β§ βπ₯ β β+
βπ¦ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ((πΉβπ§) β πΆ)) < π₯)))) |
|
Theorem | limcdifap 14402* |
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 14403* |
Express the limit operator for a function defined by a mapping, via
epsilon-delta. (Contributed by Jim Kingdon, 3-Nov-2023.)
|
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ ((π β§ π§ β π΄) β π· β β)
β β’ (π β (πΆ β ((π§ β π΄ β¦ π·) limβ π΅) β (πΆ β β β§ βπ₯ β β+
βπ¦ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ(π· β πΆ)) < π₯)))) |
|
Theorem | limcimolemlt 14404* |
Lemma for limcimo 14405. (Contributed by Jim Kingdon, 3-Jul-2023.)
|
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΅ β πΆ)
& β’ (π β π΅ β π)
& β’ (π β πΆ β (πΎ βΎt π)) & β’ (π β π β {β, β}) & β’ (π β {π β πΆ β£ π # π΅} β π΄)
& β’ πΎ = (MetOpenβ(abs β β
))
& β’ (π β π· β β+) & β’ (π β π β (πΉ limβ π΅)) & β’ (π β π β (πΉ limβ π΅)) & β’ (π β βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π·) β (absβ((πΉβπ§) β π)) < ((absβ(π β π)) / 2))) & β’ (π β πΊ β β+) & β’ (π β βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < πΊ) β (absβ((πΉβπ€) β π)) < ((absβ(π β π)) / 2))) β β’ (π β (absβ(π β π)) < (absβ(π β π))) |
|
Theorem | limcimo 14405* |
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 π)) & β’ (π β π β {β, β}) & β’ (π β {π β πΆ β£ π # π΅} β π΄)
& β’ πΎ = (MetOpenβ(abs β β
)) β β’ (π β β*π₯ π₯ β (πΉ limβ π΅)) |
|
Theorem | limcresi 14406 |
Any limit of πΉ is also a limit of the restriction
of πΉ.
(Contributed by Mario Carneiro, 28-Dec-2016.)
|
β’ (πΉ limβ π΅) β ((πΉ βΎ πΆ) limβ π΅) |
|
Theorem | cnplimcim 14407 |
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.)
|
β’ πΎ = (MetOpenβ(abs β β
))
& β’ π½ = (πΎ βΎt π΄) β β’ ((π΄ β β β§ π΅ β π΄) β (πΉ β ((π½ CnP πΎ)βπ΅) β (πΉ:π΄βΆβ β§ (πΉβπ΅) β (πΉ limβ π΅)))) |
|
Theorem | cnplimclemle 14408 |
Lemma for cnplimccntop 14410. Satisfying the epsilon condition for
continuity. (Contributed by Mario Carneiro and Jim Kingdon,
17-Nov-2023.)
|
β’ πΎ = (MetOpenβ(abs β β
))
& β’ π½ = (πΎ βΎt π΄)
& β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΅ β π΄)
& β’ (π β (πΉβπ΅) β (πΉ limβ π΅)) & β’ (π β πΈ β β+) & β’ (π β π· β β+) & β’ (π β π β π΄)
& β’ ((π β§ π # π΅ β§ (absβ(π β π΅)) < π·) β (absβ((πΉβπ) β (πΉβπ΅))) < (πΈ / 2)) & β’ (π β (absβ(π β π΅)) < π·) β β’ (π β (absβ((πΉβπ) β (πΉβπ΅))) < πΈ) |
|
Theorem | cnplimclemr 14409 |
Lemma for cnplimccntop 14410. The reverse direction. (Contributed by
Mario Carneiro and Jim Kingdon, 17-Nov-2023.)
|
β’ πΎ = (MetOpenβ(abs β β
))
& β’ π½ = (πΎ βΎt π΄)
& β’ (π β π΄ β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΅ β π΄)
& β’ (π β (πΉβπ΅) β (πΉ limβ π΅)) β β’ (π β πΉ β ((π½ CnP πΎ)βπ΅)) |
|
Theorem | cnplimccntop 14410 |
A function is continuous at π΅ iff its limit at π΅ equals
the
value of the function there. (Contributed by Mario Carneiro,
28-Dec-2016.)
|
β’ πΎ = (MetOpenβ(abs β β
))
& β’ π½ = (πΎ βΎt π΄) β β’ ((π΄ β β β§ π΅ β π΄) β (πΉ β ((π½ CnP πΎ)βπ΅) β (πΉ:π΄βΆβ β§ (πΉβπ΅) β (πΉ limβ π΅)))) |
|
Theorem | cnlimcim 14411* |
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.)
|
β’ (π΄ β β β (πΉ β (π΄βcnββ) β (πΉ:π΄βΆβ β§ βπ₯ β π΄ (πΉβπ₯) β (πΉ limβ π₯)))) |
|
Theorem | cnlimc 14412* |
πΉ
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.)
|
β’ (π΄ β β β (πΉ β (π΄βcnββ) β (πΉ:π΄βΆβ β§ βπ₯ β π΄ (πΉβπ₯) β (πΉ limβ π₯)))) |
|
Theorem | cnlimci 14413 |
If πΉ is a continuous function, then the
limit of the function at any
point equals its value. (Contributed by Mario Carneiro,
28-Dec-2016.)
|
β’ (π β πΉ β (π΄βcnβπ·)) & β’ (π β π΅ β π΄) β β’ (π β (πΉβπ΅) β (πΉ limβ π΅)) |
|
Theorem | cnmptlimc 14414* |
If πΉ is a continuous function, then the
limit of the function at any
point equals its value. (Contributed by Mario Carneiro,
28-Dec-2016.)
|
β’ (π β (π₯ β π΄ β¦ π) β (π΄βcnβπ·)) & β’ (π β π΅ β π΄)
& β’ (π₯ = π΅ β π = π) β β’ (π β π β ((π₯ β π΄ β¦ π) limβ π΅)) |
|
Theorem | limccnpcntop 14415 |
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.)
|
β’ (π β πΉ:π΄βΆπ·)
& β’ (π β π· β β) & β’ πΎ = (MetOpenβ(abs β
β ))
& β’ π½ = (πΎ βΎt π·)
& β’ (π β πΆ β (πΉ limβ π΅)) & β’ (π β πΊ β ((π½ CnP πΎ)βπΆ)) β β’ (π β (πΊβπΆ) β ((πΊ β πΉ) limβ π΅)) |
|
Theorem | limccnp2lem 14416* |
Lemma for limccnp2cntop 14417. 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.)
|
β’ ((π β§ π₯ β π΄) β π
β π)
& β’ ((π β§ π₯ β π΄) β π β π)
& β’ (π β π β β) & β’ (π β π β β) & β’ πΎ = (MetOpenβ(abs β
β ))
& β’ π½ = ((πΎ Γt πΎ) βΎt (π Γ π)) & β’ (π β πΆ β ((π₯ β π΄ β¦ π
) limβ π΅)) & β’ (π β π· β ((π₯ β π΄ β¦ π) limβ π΅)) & β’ (π β π» β ((π½ CnP πΎ)ββ¨πΆ, π·β©)) & β’ β²π₯π
& β’ (π β πΈ β β+) & β’ (π β πΏ β β+) & β’ (π β βπ β π βπ β π (((πΆ((abs β β ) βΎ (π Γ π))π) < πΏ β§ (π·((abs β β ) βΎ (π Γ π))π ) < πΏ) β ((πΆπ»π·)(abs β β )(ππ»π )) < πΈ)) & β’ (π β πΉ β β+) & β’ (π β βπ₯ β π΄ ((π₯ # π΅ β§ (absβ(π₯ β π΅)) < πΉ) β (absβ(π
β πΆ)) < πΏ)) & β’ (π β πΊ β β+) & β’ (π β βπ₯ β π΄ ((π₯ # π΅ β§ (absβ(π₯ β π΅)) < πΊ) β (absβ(π β π·)) < πΏ)) β β’ (π β βπ β β+ βπ₯ β π΄ ((π₯ # π΅ β§ (absβ(π₯ β π΅)) < π) β (absβ((π
π»π) β (πΆπ»π·))) < πΈ)) |
|
Theorem | limccnp2cntop 14417* |
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.)
|
β’ ((π β§ π₯ β π΄) β π
β π)
& β’ ((π β§ π₯ β π΄) β π β π)
& β’ (π β π β β) & β’ (π β π β β) & β’ πΎ = (MetOpenβ(abs β
β ))
& β’ π½ = ((πΎ Γt πΎ) βΎt (π Γ π)) & β’ (π β πΆ β ((π₯ β π΄ β¦ π
) limβ π΅)) & β’ (π β π· β ((π₯ β π΄ β¦ π) limβ π΅)) & β’ (π β π» β ((π½ CnP πΎ)ββ¨πΆ, π·β©)) β β’ (π β (πΆπ»π·) β ((π₯ β π΄ β¦ (π
π»π)) limβ π΅)) |
|
Theorem | limccoap 14418* |
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 14419 |
The derivative function is a relation. (Contributed by Mario Carneiro,
7-Aug-2014.) (Revised by Jim Kingdon, 25-Jun-2023.)
|
β’ ((π β β β§ πΉ β (β βpm
π)) β Rel (π D πΉ)) |
|
Theorem | dvlemap 14420* |
Closure for a difference quotient. (Contributed by Mario Carneiro,
1-Sep-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
|
β’ (π β πΉ:π·βΆβ) & β’ (π β π· β β) & β’ (π β π΅ β π·) β β’ ((π β§ π΄ β {π€ β π· β£ π€ # π΅}) β (((πΉβπ΄) β (πΉβπ΅)) / (π΄ β π΅)) β β) |
|
Theorem | dvfvalap 14421* |
Value and set bounds on the derivative operator. (Contributed by Mario
Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 27-Jun-2023.)
|
β’ π = (πΎ βΎt π)
& β’ πΎ = (MetOpenβ(abs β β
)) β β’ ((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β ((π D πΉ) = βͺ
π₯ β ((intβπ)βπ΄)({π₯} Γ ((π§ β {π€ β π΄ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β§ (π D πΉ) β (((intβπ)βπ΄) Γ β))) |
|
Theorem | eldvap 14422* |
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 π)
& β’ πΎ = (MetOpenβ(abs β β
))
& β’ πΊ = (π§ β {π€ β π΄ β£ π€ # π΅} β¦ (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅))) & β’ (π β π β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) β β’ (π β (π΅(π D πΉ)πΆ β (π΅ β ((intβπ)βπ΄) β§ πΆ β (πΊ limβ π΅)))) |
|
Theorem | dvcl 14423 |
The derivative function takes values in the complex numbers.
(Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario
Carneiro, 9-Feb-2015.)
|
β’ (π β π β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) β β’ ((π β§ π΅(π D πΉ)πΆ) β πΆ β β) |
|
Theorem | dvbssntrcntop 14424 |
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 π)
& β’ πΎ = (MetOpenβ(abs β β
)) β β’ (π β dom (π D πΉ) β ((intβπ½)βπ΄)) |
|
Theorem | dvbss 14425 |
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.)
|
β’ (π β π β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) β β’ (π β dom (π D πΉ) β π΄) |
|
Theorem | dvbsssg 14426 |
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.)
|
β’ ((π β β β§ πΉ β (β βpm
π)) β dom (π D πΉ) β π) |
|
Theorem | recnprss 14427 |
Both β and β are
subsets of β. (Contributed by Mario
Carneiro, 10-Feb-2015.)
|
β’ (π β {β, β} β π β
β) |
|
Theorem | dvfgg 14428 |
Explicitly write out the functionality condition on derivative for
π =
β and β. (Contributed by Mario
Carneiro, 9-Feb-2015.)
(Revised by Jim Kingdon, 28-Jun-2023.)
|
β’ ((π β {β, β} β§ πΉ β (β
βpm π)) β (π D πΉ):dom (π D πΉ)βΆβ) |
|
Theorem | dvfpm 14429 |
The derivative is a function. (Contributed by Mario Carneiro,
8-Aug-2014.) (Revised by Jim Kingdon, 28-Jul-2023.)
|
β’ (πΉ β (β βpm
β) β (β D πΉ):dom (β D πΉ)βΆβ) |
|
Theorem | dvfcnpm 14430 |
The derivative is a function. (Contributed by Mario Carneiro,
9-Feb-2015.) (Revised by Jim Kingdon, 28-Jul-2023.)
|
β’ (πΉ β (β βpm
β) β (β D πΉ):dom (β D πΉ)βΆβ) |
|
Theorem | dvidlemap 14431* |
Lemma for dvid 14433 and dvconst 14432. (Contributed by Mario Carneiro,
8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|
β’ (π β πΉ:ββΆβ) & β’ ((π β§ (π₯ β β β§ π§ β β β§ π§ # π₯)) β (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯)) = π΅)
& β’ π΅ β β
β β’ (π β (β D πΉ) = (β Γ {π΅})) |
|
Theorem | dvconst 14432 |
Derivative of a constant function. (Contributed by Mario Carneiro,
8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|
β’ (π΄ β β β (β D (β
Γ {π΄})) = (β
Γ {0})) |
|
Theorem | dvid 14433 |
Derivative of the identity function. (Contributed by Mario Carneiro,
8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.)
|
β’ (β D ( I βΎ β)) = (β
Γ {1}) |
|
Theorem | dvcnp2cntop 14434 |
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 π΄)
& β’ πΎ = (MetOpenβ(abs β β
)) β β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅ β dom (π D πΉ)) β πΉ β ((π½ CnP πΎ)βπ΅)) |
|
Theorem | dvcn 14435 |
A differentiable function is continuous. (Contributed by Mario
Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-Sep-2015.)
|
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ dom (π D πΉ) = π΄) β πΉ β (π΄βcnββ)) |
|
Theorem | dvaddxxbr 14436 |
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.)
|
β’ (π β πΉ:πβΆβ) & β’ (π β π β π)
& β’ (π β πΊ:πβΆβ) & β’ (π β π β β) & β’ (π β πΆ(π D πΉ)πΎ)
& β’ (π β πΆ(π D πΊ)πΏ)
& β’ π½ = (MetOpenβ(abs β β
)) β β’ (π β πΆ(π D (πΉ βπ + πΊ))(πΎ + πΏ)) |
|
Theorem | dvmulxxbr 14437 |
The product rule for derivatives at a point. For the (simpler but
more limited) function version, see dvmulxx 14439. (Contributed by Mario
Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.)
|
β’ (π β πΉ:πβΆβ) & β’ (π β π β π)
& β’ (π β πΊ:πβΆβ) & β’ (π β π β β) & β’ (π β πΆ(π D πΉ)πΎ)
& β’ (π β πΆ(π D πΊ)πΏ)
& β’ π½ = (MetOpenβ(abs β β
)) β β’ (π β πΆ(π D (πΉ βπ Β· πΊ))((πΎ Β· (πΊβπΆ)) + (πΏ Β· (πΉβπΆ)))) |
|
Theorem | dvaddxx 14438 |
The sum rule for derivatives at a point. For the (more general)
relation version, see dvaddxxbr 14436. (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.)
|
β’ (π β πΉ:πβΆβ) & β’ (π β π β π)
& β’ (π β πΊ:πβΆβ) & β’ (π β π β {β, β}) & β’ (π β πΆ β dom (π D πΉ)) & β’ (π β πΆ β dom (π D πΊ)) β β’ (π β ((π D (πΉ βπ + πΊ))βπΆ) = (((π D πΉ)βπΆ) + ((π D πΊ)βπΆ))) |
|
Theorem | dvmulxx 14439 |
The product rule for derivatives at a point. For the (more general)
relation version, see dvmulxxbr 14437. (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Jim Kingdon, 2-Dec-2023.)
|
β’ (π β πΉ:πβΆβ) & β’ (π β π β π)
& β’ (π β πΊ:πβΆβ) & β’ (π β π β {β, β}) & β’ (π β πΆ β dom (π D πΉ)) & β’ (π β πΆ β dom (π D πΊ)) β β’ (π β ((π D (πΉ βπ Β· πΊ))βπΆ) = ((((π D πΉ)βπΆ) Β· (πΊβπΆ)) + (((π D πΊ)βπΆ) Β· (πΉβπΆ)))) |
|
Theorem | dviaddf 14440 |
The sum rule for everywhere-differentiable functions. (Contributed by
Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro,
10-Feb-2015.)
|
β’ (π β π β {β, β}) & β’ (π β π β π)
& β’ (π β πΉ:πβΆβ) & β’ (π β πΊ:πβΆβ) & β’ (π β dom (π D πΉ) = π)
& β’ (π β dom (π D πΊ) = π) β β’ (π β (π D (πΉ βπ + πΊ)) = ((π D πΉ) βπ + (π D πΊ))) |
|
Theorem | dvimulf 14441 |
The product rule for everywhere-differentiable functions. (Contributed
by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro,
10-Feb-2015.)
|
β’ (π β π β {β, β}) & β’ (π β π β π)
& β’ (π β πΉ:πβΆβ) & β’ (π β πΊ:πβΆβ) & β’ (π β dom (π D πΉ) = π)
& β’ (π β dom (π D πΊ) = π) β β’ (π β (π D (πΉ βπ Β· πΊ)) = (((π D πΉ) βπ Β·
πΊ)
βπ + ((π D πΊ) βπ Β·
πΉ))) |
|
Theorem | dvcoapbr 14442* |
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.)
|
β’ (π β πΉ:πβΆβ) & β’ (π β π β π)
& β’ (π β πΊ:πβΆπ)
& β’ (π β π β π)
& β’ (π β βπ’ β π (π’ # πΆ β (πΊβπ’) # (πΊβπΆ))) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β (πΊβπΆ)(π D πΉ)πΎ)
& β’ (π β πΆ(π D πΊ)πΏ)
& β’ π½ = (MetOpenβ(abs β β
)) β β’ (π β πΆ(π D (πΉ β πΊ))(πΎ Β· πΏ)) |
|
Theorem | dvcjbr 14443 |
The derivative of the conjugate of a function. For the (simpler but
more limited) function version, see dvcj 14444. (Contributed by Mario
Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|
β’ (π β πΉ:πβΆβ) & β’ (π β π β β) & β’ (π β πΆ β dom (β D πΉ)) β β’ (π β πΆ(β D (β β πΉ))(ββ((β D
πΉ)βπΆ))) |
|
Theorem | dvcj 14444 |
The derivative of the conjugate of a function. For the (more general)
relation version, see dvcjbr 14443. (Contributed by Mario Carneiro,
1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|
β’ ((πΉ:πβΆβ β§ π β β) β (β D
(β β πΉ)) =
(β β (β D πΉ))) |
|
Theorem | dvfre 14445 |
The derivative of a real function is real. (Contributed by Mario
Carneiro, 1-Sep-2014.)
|
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (β D πΉ):dom (β D πΉ)βΆβ) |
|
Theorem | dvexp 14446* |
Derivative of a power function. (Contributed by Mario Carneiro,
9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)
|
β’ (π β β β (β D (π₯ β β β¦ (π₯βπ))) = (π₯ β β β¦ (π Β· (π₯β(π β 1))))) |
|
Theorem | dvexp2 14447* |
Derivative of an exponential, possibly zero power. (Contributed by
Stefan O'Rear, 13-Nov-2014.) (Revised by Mario Carneiro,
10-Feb-2015.)
|
β’ (π β β0 β (β
D (π₯ β β
β¦ (π₯βπ))) = (π₯ β β β¦ if(π = 0, 0, (π Β· (π₯β(π β 1)))))) |
|
Theorem | dvrecap 14448* |
Derivative of the reciprocal function. (Contributed by Mario Carneiro,
25-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.)
|
β’ (π΄ β β β (β D (π₯ β {π€ β β β£ π€ # 0} β¦ (π΄ / π₯))) = (π₯ β {π€ β β β£ π€ # 0} β¦ -(π΄ / (π₯β2)))) |
|
Theorem | dvmptidcn 14449 |
Function-builder for derivative: derivative of the identity.
(Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
30-Dec-2023.)
|
β’ (β D (π₯ β β β¦ π₯)) = (π₯ β β β¦ 1) |
|
Theorem | dvmptccn 14450* |
Function-builder for derivative: derivative of a constant. (Contributed
by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
30-Dec-2023.)
|
β’ (π β π΄ β β)
β β’ (π β (β D (π₯ β β β¦ π΄)) = (π₯ β β β¦ 0)) |
|
Theorem | dvmptclx 14451* |
Closure lemma for dvmptmulx 14453 and other related theorems. (Contributed
by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro,
11-Feb-2015.)
|
β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π)
& β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π β π β π) β β’ ((π β§ π₯ β π) β π΅ β β) |
|
Theorem | dvmptaddx 14452* |
Function-builder for derivative, addition rule. (Contributed by Mario
Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|
β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π)
& β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π β π β π)
& β’ ((π β§ π₯ β π) β πΆ β β) & β’ ((π β§ π₯ β π) β π· β π)
& β’ (π β (π D (π₯ β π β¦ πΆ)) = (π₯ β π β¦ π·)) β β’ (π β (π D (π₯ β π β¦ (π΄ + πΆ))) = (π₯ β π β¦ (π΅ + π·))) |
|
Theorem | dvmptmulx 14453* |
Function-builder for derivative, product rule. (Contributed by Mario
Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|
β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π)
& β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π β π β π)
& β’ ((π β§ π₯ β π) β πΆ β β) & β’ ((π β§ π₯ β π) β π· β π)
& β’ (π β (π D (π₯ β π β¦ πΆ)) = (π₯ β π β¦ π·)) β β’ (π β (π D (π₯ β π β¦ (π΄ Β· πΆ))) = (π₯ β π β¦ ((π΅ Β· πΆ) + (π· Β· π΄)))) |
|
Theorem | dvmptcmulcn 14454* |
Function-builder for derivative, product rule for constant multiplier.
(Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
31-Dec-2023.)
|
β’ ((π β§ π₯ β β) β π΄ β β) & β’ ((π β§ π₯ β β) β π΅ β π)
& β’ (π β (β D (π₯ β β β¦ π΄)) = (π₯ β β β¦ π΅)) & β’ (π β πΆ β β)
β β’ (π β (β D (π₯ β β β¦ (πΆ Β· π΄))) = (π₯ β β β¦ (πΆ Β· π΅))) |
|
Theorem | dvmptnegcn 14455* |
Function-builder for derivative, product rule for negatives.
(Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
31-Dec-2023.)
|
β’ ((π β§ π₯ β β) β π΄ β β) & β’ ((π β§ π₯ β β) β π΅ β π)
& β’ (π β (β D (π₯ β β β¦ π΄)) = (π₯ β β β¦ π΅)) β β’ (π β (β D (π₯ β β β¦ -π΄)) = (π₯ β β β¦ -π΅)) |
|
Theorem | dvmptsubcn 14456* |
Function-builder for derivative, subtraction rule. (Contributed by
Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon,
31-Dec-2023.)
|
β’ ((π β§ π₯ β β) β π΄ β β) & β’ ((π β§ π₯ β β) β π΅ β π)
& β’ (π β (β D (π₯ β β β¦ π΄)) = (π₯ β β β¦ π΅)) & β’ ((π β§ π₯ β β) β πΆ β β) & β’ ((π β§ π₯ β β) β π· β π)
& β’ (π β (β D (π₯ β β β¦ πΆ)) = (π₯ β β β¦ π·)) β β’ (π β (β D (π₯ β β β¦ (π΄ β πΆ))) = (π₯ β β β¦ (π΅ β π·))) |
|
Theorem | dvmptcjx 14457* |
Function-builder for derivative, conjugate rule. (Contributed by Mario
Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 24-May-2024.)
|
β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π)
& β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π β π β β)
β β’ (π β (β D (π₯ β π β¦ (ββπ΄))) = (π₯ β π β¦ (ββπ΅))) |
|
Theorem | dveflem 14458 |
Derivative of the exponential function at 0. The key step in the proof
is eftlub 11711, to show that
abs(exp(π₯) β 1 β π₯) β€ abs(π₯)β2 Β· (3 / 4).
(Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario
Carneiro, 28-Dec-2016.)
|
β’ 0(β D exp)1 |
|
Theorem | dvef 14459 |
Derivative of the exponential function. (Contributed by Mario Carneiro,
9-Aug-2014.) (Proof shortened by Mario Carneiro, 10-Feb-2015.)
|
β’ (β D exp) = exp |
|
PART 10 BASIC REAL AND COMPLEX
FUNCTIONS
|
|
10.1 Basic trigonometry
|
|
10.1.1 The exponential, sine, and cosine
functions (cont.)
|
|
Theorem | efcn 14460 |
The exponential function is continuous. (Contributed by Paul Chapman,
15-Sep-2007.) (Revised by Mario Carneiro, 20-Jun-2015.)
|
β’ exp β (ββcnββ) |
|
Theorem | sincn 14461 |
Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.)
(Revised by Mario Carneiro, 3-Sep-2014.)
|
β’ sin β (ββcnββ) |
|
Theorem | coscn 14462 |
Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.)
(Revised by Mario Carneiro, 3-Sep-2014.)
|
β’ cos β (ββcnββ) |
|
Theorem | reeff1olem 14463* |
Lemma for reeff1o 14465. (Contributed by Paul Chapman,
18-Oct-2007.)
(Revised by Mario Carneiro, 30-Apr-2014.)
|
β’ ((π β β β§ 1 < π) β βπ₯ β β
(expβπ₯) = π) |
|
Theorem | reeff1oleme 14464* |
Lemma for reeff1o 14465. (Contributed by Jim Kingdon, 15-May-2024.)
|
β’ (π β (0(,)e) β βπ₯ β β
(expβπ₯) = π) |
|
Theorem | reeff1o 14465 |
The real exponential function is one-to-one onto. (Contributed by Paul
Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 10-Nov-2013.)
|
β’ (exp βΎ β):ββ1-1-ontoββ+ |
|
Theorem | efltlemlt 14466 |
Lemma for eflt 14467. The converse of efltim 11719 plus the epsilon-delta
setup. (Contributed by Jim Kingdon, 22-May-2024.)
|
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (expβπ΄) < (expβπ΅)) & β’ (π β π· β β+) & β’ (π β ((absβ(π΄ β π΅)) < π· β (absβ((expβπ΄) β (expβπ΅))) < ((expβπ΅) β (expβπ΄))))
β β’ (π β π΄ < π΅) |
|
Theorem | eflt 14467 |
The exponential function on the reals is strictly increasing.
(Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon,
21-May-2024.)
|
β’ ((π΄ β β β§ π΅ β β) β (π΄ < π΅ β (expβπ΄) < (expβπ΅))) |
|
Theorem | efle 14468 |
The exponential function on the reals is nondecreasing. (Contributed by
Mario Carneiro, 11-Mar-2014.)
|
β’ ((π΄ β β β§ π΅ β β) β (π΄ β€ π΅ β (expβπ΄) β€ (expβπ΅))) |
|
Theorem | reefiso 14469 |
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.)
|
β’ (exp βΎ β) Isom < , <
(β, β+) |
|
Theorem | reapef 14470 |
Apartness and the exponential function for reals. (Contributed by Jim
Kingdon, 11-Jul-2024.)
|
β’ ((π΄ β β β§ π΅ β β) β (π΄ # π΅ β (expβπ΄) # (expβπ΅))) |
|
10.1.2 Properties of pi =
3.14159...
|
|
Theorem | pilem1 14471 |
Lemma for pire , pigt2lt4 and sinpi . (Contributed by Mario Carneiro,
9-May-2014.)
|
β’ (π΄ β (β+ β© (β‘sin β {0})) β (π΄ β β+ β§
(sinβπ΄) =
0)) |
|
Theorem | cosz12 14472 |
Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and
Jim Kingdon, 7-Mar-2024.)
|
β’ βπ β (1(,)2)(cosβπ) = 0 |
|
Theorem | sin0pilem1 14473* |
Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim
Kingdon, 8-Mar-2024.)
|
β’ βπ β (1(,)2)((cosβπ) = 0 β§ βπ₯ β (π(,)(2 Β· π))0 < (sinβπ₯)) |
|
Theorem | sin0pilem2 14474* |
Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim
Kingdon, 8-Mar-2024.)
|
β’ βπ β (2(,)4)((sinβπ) = 0 β§ βπ₯ β (0(,)π)0 < (sinβπ₯)) |
|
Theorem | pilem3 14475 |
Lemma for pi related theorems. (Contributed by Jim Kingdon,
9-Mar-2024.)
|
β’ (Ο β (2(,)4) β§ (sinβΟ)
= 0) |
|
Theorem | pigt2lt4 14476 |
Ο is between 2 and 4. (Contributed by Paul Chapman,
23-Jan-2008.)
(Revised by Mario Carneiro, 9-May-2014.)
|
β’ (2 < Ο β§ Ο <
4) |
|
Theorem | sinpi 14477 |
The sine of Ο is 0. (Contributed by Paul Chapman,
23-Jan-2008.)
|
β’ (sinβΟ) = 0 |
|
Theorem | pire 14478 |
Ο is a real number. (Contributed by Paul Chapman,
23-Jan-2008.)
|
β’ Ο β β |
|
Theorem | picn 14479 |
Ο is a complex number. (Contributed by David A.
Wheeler,
6-Dec-2018.)
|
β’ Ο β β |
|
Theorem | pipos 14480 |
Ο is positive. (Contributed by Paul Chapman,
23-Jan-2008.)
(Revised by Mario Carneiro, 9-May-2014.)
|
β’ 0 < Ο |
|
Theorem | pirp 14481 |
Ο is a positive real. (Contributed by Glauco
Siliprandi,
11-Dec-2019.)
|
β’ Ο β
β+ |
|
Theorem | negpicn 14482 |
-Ο is a real number. (Contributed by David A.
Wheeler,
8-Dec-2018.)
|
β’ -Ο β β |
|
Theorem | sinhalfpilem 14483 |
Lemma for sinhalfpi 14488 and coshalfpi 14489. (Contributed by Paul Chapman,
23-Jan-2008.)
|
β’ ((sinβ(Ο / 2)) = 1 β§
(cosβ(Ο / 2)) = 0) |
|
Theorem | halfpire 14484 |
Ο / 2 is real. (Contributed by David Moews,
28-Feb-2017.)
|
β’ (Ο / 2) β β |
|
Theorem | neghalfpire 14485 |
-Ο / 2 is real. (Contributed by David A. Wheeler,
8-Dec-2018.)
|
β’ -(Ο / 2) β β |
|
Theorem | neghalfpirx 14486 |
-Ο / 2 is an extended real. (Contributed by David
A. Wheeler,
8-Dec-2018.)
|
β’ -(Ο / 2) β
β* |
|
Theorem | pidiv2halves 14487 |
Adding Ο / 2 to itself gives Ο. See 2halves 9161.
(Contributed by David A. Wheeler, 8-Dec-2018.)
|
β’ ((Ο / 2) + (Ο / 2)) =
Ο |
|
Theorem | sinhalfpi 14488 |
The sine of Ο / 2 is 1. (Contributed by Paul
Chapman,
23-Jan-2008.)
|
β’ (sinβ(Ο / 2)) = 1 |
|
Theorem | coshalfpi 14489 |
The cosine of Ο / 2 is 0. (Contributed by Paul
Chapman,
23-Jan-2008.)
|
β’ (cosβ(Ο / 2)) = 0 |
|
Theorem | cosneghalfpi 14490 |
The cosine of -Ο / 2 is zero. (Contributed by David
Moews,
28-Feb-2017.)
|
β’ (cosβ-(Ο / 2)) = 0 |
|
Theorem | efhalfpi 14491 |
The exponential of iΟ / 2 is i. (Contributed by Mario
Carneiro, 9-May-2014.)
|
β’ (expβ(i Β· (Ο / 2))) =
i |
|
Theorem | cospi 14492 |
The cosine of Ο is -1.
(Contributed by Paul Chapman,
23-Jan-2008.)
|
β’ (cosβΟ) = -1 |
|
Theorem | efipi 14493 |
The exponential of i Β· Ο is -1. (Contributed by Paul
Chapman, 23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
β’ (expβ(i Β· Ο)) =
-1 |
|
Theorem | eulerid 14494 |
Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised
by Mario Carneiro, 9-May-2014.)
|
β’ ((expβ(i Β· Ο)) + 1) =
0 |
|
Theorem | sin2pi 14495 |
The sine of 2Ο is 0. (Contributed by Paul Chapman,
23-Jan-2008.)
|
β’ (sinβ(2 Β· Ο)) =
0 |
|
Theorem | cos2pi 14496 |
The cosine of 2Ο is 1. (Contributed by Paul
Chapman,
23-Jan-2008.)
|
β’ (cosβ(2 Β· Ο)) =
1 |
|
Theorem | ef2pi 14497 |
The exponential of 2Οi is 1.
(Contributed by Mario
Carneiro, 9-May-2014.)
|
β’ (expβ(i Β· (2 Β· Ο))) =
1 |
|
Theorem | ef2kpi 14498 |
If πΎ is an integer, then the exponential
of 2πΎΟi is 1.
(Contributed by Mario Carneiro, 9-May-2014.)
|
β’ (πΎ β β€ β (expβ((i
Β· (2 Β· Ο)) Β· πΎ)) = 1) |
|
Theorem | efper 14499 |
The exponential function is periodic. (Contributed by Paul Chapman,
21-Apr-2008.) (Proof shortened by Mario Carneiro, 10-May-2014.)
|
β’ ((π΄ β β β§ πΎ β β€) β (expβ(π΄ + ((i Β· (2 Β·
Ο)) Β· πΎ))) =
(expβπ΄)) |
|
Theorem | sinperlem 14500 |
Lemma for sinper 14501 and cosper 14502. (Contributed by Paul Chapman,
23-Jan-2008.) (Revised by Mario Carneiro, 10-May-2014.)
|
β’ (π΄ β β β (πΉβπ΄) = (((expβ(i Β· π΄))π(expβ(-i Β· π΄))) / π·)) & β’ ((π΄ + (πΎ Β· (2 Β· Ο))) β
β β (πΉβ(π΄ + (πΎ Β· (2 Β· Ο)))) =
(((expβ(i Β· (π΄ + (πΎ Β· (2 Β· Ο)))))π(expβ(-i Β· (π΄ + (πΎ Β· (2 Β· Ο)))))) / π·))
β β’ ((π΄ β β β§ πΎ β β€) β (πΉβ(π΄ + (πΎ Β· (2 Β· Ο)))) = (πΉβπ΄)) |