![]() |
Metamath
Proof Explorer Theorem List (p. 255 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | limcmpt2 25401* | Express the limit operator for a function defined by a mapping. (Contributed by Mario Carneiro, 25-Dec-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β π΄) & β’ ((π β§ (π§ β π΄ β§ π§ β π΅)) β π· β β) & β’ π½ = (πΎ βΎt π΄) & β’ πΎ = (TopOpenββfld) β β’ (π β (πΆ β ((π§ β (π΄ β {π΅}) β¦ π·) limβ π΅) β (π§ β π΄ β¦ if(π§ = π΅, πΆ, π·)) β ((π½ CnP πΎ)βπ΅))) | ||
Theorem | limcresi 25402 | Any limit of πΉ is also a limit of the restriction of πΉ. (Contributed by Mario Carneiro, 28-Dec-2016.) |
β’ (πΉ limβ π΅) β ((πΉ βΎ πΆ) limβ π΅) | ||
Theorem | limcres 25403 | If π΅ is an interior point of πΆ βͺ {π΅} relative to the domain π΄, then a limit point of πΉ βΎ πΆ extends to a limit of πΉ. (Contributed by Mario Carneiro, 27-Dec-2016.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β πΆ β π΄) & β’ (π β π΄ β β) & β’ πΎ = (TopOpenββfld) & β’ π½ = (πΎ βΎt (π΄ βͺ {π΅})) & β’ (π β π΅ β ((intβπ½)β(πΆ βͺ {π΅}))) β β’ (π β ((πΉ βΎ πΆ) limβ π΅) = (πΉ limβ π΅)) | ||
Theorem | cnplimc 25404 | A function is continuous at π΅ iff its limit at π΅ equals the value of the function there. (Contributed by Mario Carneiro, 28-Dec-2016.) |
β’ πΎ = (TopOpenββfld) & β’ π½ = (πΎ βΎt π΄) β β’ ((π΄ β β β§ π΅ β π΄) β (πΉ β ((π½ CnP πΎ)βπ΅) β (πΉ:π΄βΆβ β§ (πΉβπ΅) β (πΉ limβ π΅)))) | ||
Theorem | cnlimc 25405* | πΉ 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 25406 | 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 25407* | 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 | limccnp 25408 | If the limit of πΉ at π΅ is πΆ and πΊ is continuous at πΆ, then the limit of πΊ β πΉ at π΅ is πΊ(πΆ). (Contributed by Mario Carneiro, 28-Dec-2016.) |
β’ (π β πΉ:π΄βΆπ·) & β’ (π β π· β β) & β’ πΎ = (TopOpenββfld) & β’ π½ = (πΎ βΎt π·) & β’ (π β πΆ β (πΉ limβ π΅)) & β’ (π β πΊ β ((π½ CnP πΎ)βπΆ)) β β’ (π β (πΊβπΆ) β ((πΊ β πΉ) limβ π΅)) | ||
Theorem | limccnp2 25409* | 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.) |
β’ ((π β§ π₯ β π΄) β π β π) & β’ ((π β§ π₯ β π΄) β π β π) & β’ (π β π β β) & β’ (π β π β β) & β’ πΎ = (TopOpenββfld) & β’ π½ = ((πΎ Γt πΎ) βΎt (π Γ π)) & β’ (π β πΆ β ((π₯ β π΄ β¦ π ) limβ π΅)) & β’ (π β π· β ((π₯ β π΄ β¦ π) limβ π΅)) & β’ (π β π» β ((π½ CnP πΎ)ββ¨πΆ, π·β©)) β β’ (π β (πΆπ»π·) β ((π₯ β π΄ β¦ (π π»π)) limβ π΅)) | ||
Theorem | limcco 25410* | Composition of two limits. (Contributed by Mario Carneiro, 29-Dec-2016.) |
β’ ((π β§ (π₯ β π΄ β§ π β πΆ)) β π β π΅) & β’ ((π β§ π¦ β π΅) β π β β) & β’ (π β πΆ β ((π₯ β π΄ β¦ π ) limβ π)) & β’ (π β π· β ((π¦ β π΅ β¦ π) limβ πΆ)) & β’ (π¦ = π β π = π) & β’ ((π β§ (π₯ β π΄ β§ π = πΆ)) β π = π·) β β’ (π β π· β ((π₯ β π΄ β¦ π) limβ π)) | ||
Theorem | limciun 25411* | A point is a limit of πΉ on the finite union βͺ π₯ β π΄π΅(π₯) iff it is the limit of the restriction of πΉ to each π΅(π₯). (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ (π β π΄ β Fin) & β’ (π β βπ₯ β π΄ π΅ β β) & β’ (π β πΉ:βͺ π₯ β π΄ π΅βΆβ) & β’ (π β πΆ β β) β β’ (π β (πΉ limβ πΆ) = (β β© β© π₯ β π΄ ((πΉ βΎ π΅) limβ πΆ))) | ||
Theorem | limcun 25412 | A point is a limit of πΉ on π΄ βͺ π΅ iff it is the limit of the restriction of πΉ to π΄ and to π΅. (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ:(π΄ βͺ π΅)βΆβ) β β’ (π β (πΉ limβ πΆ) = (((πΉ βΎ π΄) limβ πΆ) β© ((πΉ βΎ π΅) limβ πΆ))) | ||
Theorem | dvlem 25413 | Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
β’ (π β πΉ:π·βΆβ) & β’ (π β π· β β) & β’ (π β π΅ β π·) β β’ ((π β§ π΄ β (π· β {π΅})) β (((πΉβπ΄) β (πΉβπ΅)) / (π΄ β π΅)) β β) | ||
Theorem | dvfval 25414* | Value and set bounds on the derivative operator. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 25-Dec-2016.) |
β’ π = (πΎ βΎt π) & β’ πΎ = (TopOpenββfld) β β’ ((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β ((π D πΉ) = βͺ π₯ β ((intβπ)βπ΄)({π₯} Γ ((π§ β (π΄ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β§ (π D πΉ) β (((intβπ)βπ΄) Γ β))) | ||
Theorem | eldv 25415* | 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 Mario Carneiro, 25-Dec-2016.) |
β’ π = (πΎ βΎt π) & β’ πΎ = (TopOpenββfld) & β’ πΊ = (π§ β (π΄ β {π΅}) β¦ (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅))) & β’ (π β π β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) β β’ (π β (π΅(π D πΉ)πΆ β (π΅ β ((intβπ)βπ΄) β§ πΆ β (πΊ limβ π΅)))) | ||
Theorem | dvcl 25416 | 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 | dvbssntr 25417 | 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 Mario Carneiro, 9-Feb-2015.) |
β’ (π β π β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ π½ = (πΎ βΎt π) & β’ πΎ = (TopOpenββfld) β β’ (π β dom (π D πΉ) β ((intβπ½)βπ΄)) | ||
Theorem | dvbss 25418 | 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 | dvbsss 25419 | The set of differentiable points is a subset of the ambient topology. (Contributed by Mario Carneiro, 18-Mar-2015.) |
β’ dom (π D πΉ) β π | ||
Theorem | perfdvf 25420 | The derivative is a function, whenever it is defined relative to a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 25-Dec-2016.) |
β’ πΎ = (TopOpenββfld) β β’ ((πΎ βΎt π) β Perf β (π D πΉ):dom (π D πΉ)βΆβ) | ||
Theorem | recnprss 25421 | Both β and β are subsets of β. (Contributed by Mario Carneiro, 10-Feb-2015.) |
β’ (π β {β, β} β π β β) | ||
Theorem | recnperf 25422 | Both β and β are perfect subsets of β. (Contributed by Mario Carneiro, 28-Dec-2016.) |
β’ πΎ = (TopOpenββfld) β β’ (π β {β, β} β (πΎ βΎt π) β Perf) | ||
Theorem | dvfg 25423 | Explicitly write out the functionality condition on derivative for π = β and β. (Contributed by Mario Carneiro, 9-Feb-2015.) |
β’ (π β {β, β} β (π D πΉ):dom (π D πΉ)βΆβ) | ||
Theorem | dvf 25424 | The derivative is a function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
β’ (β D πΉ):dom (β D πΉ)βΆβ | ||
Theorem | dvfcn 25425 | The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015.) |
β’ (β D πΉ):dom (β D πΉ)βΆβ | ||
Theorem | dvreslem 25426* | Lemma for dvres 25428. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) Commute the consequent and shorten proof. (Revised by Peter Mazsa, 2-Oct-2022.) |
β’ πΎ = (TopOpenββfld) & β’ π = (πΎ βΎt π) & β’ πΊ = (π§ β (π΄ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) & β’ (π β π β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π¦ β β) β β’ (π β (π₯(π D (πΉ βΎ π΅))π¦ β (π₯ β ((intβπ)βπ΅) β§ π₯(π D πΉ)π¦))) | ||
Theorem | dvres2lem 25427* | Lemma for dvres2 25429. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.) |
β’ πΎ = (TopOpenββfld) & β’ π = (πΎ βΎt π) & β’ πΊ = (π§ β (π΄ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) & β’ (π β π β β) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π¦ β β) & β’ (π β π₯(π D πΉ)π¦) & β’ (π β π₯ β π΅) β β’ (π β π₯(π΅ D (πΉ βΎ π΅))π¦) | ||
Theorem | dvres 25428 | Restriction of a derivative. Note that our definition of derivative df-dv 25384 would still make sense if we demanded that π₯ be an element of the domain instead of an interior point of the domain, but then it is possible for a non-differentiable function to have two different derivatives at a single point π₯ when restricted to different subsets containing π₯; a classic example is the absolute value function restricted to [0, +β) and (-β, 0]. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
β’ πΎ = (TopOpenββfld) & β’ π = (πΎ βΎt π) β β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β (π D (πΉ βΎ π΅)) = ((π D πΉ) βΎ ((intβπ)βπ΅))) | ||
Theorem | dvres2 25429 | Restriction of the base set of a derivative. The primary application of this theorem says that if a function is complex-differentiable then it is also real-differentiable. Unlike dvres 25428, there is no simple reverse relation relating real-differentiable functions to complex differentiability, and indeed there are functions like β(π₯) which are everywhere real-differentiable but nowhere complex-differentiable.) (Contributed by Mario Carneiro, 9-Feb-2015.) |
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β ((π D πΉ) βΎ π΅) β (π΅ D (πΉ βΎ π΅))) | ||
Theorem | dvres3 25430 | Restriction of a complex differentiable function to the reals. (Contributed by Mario Carneiro, 10-Feb-2015.) |
β’ (((π β {β, β} β§ πΉ:π΄βΆβ) β§ (π΄ β β β§ π β dom (β D πΉ))) β (π D (πΉ βΎ π)) = ((β D πΉ) βΎ π)) | ||
Theorem | dvres3a 25431 | Restriction of a complex differentiable function to the reals. This version of dvres3 25430 assumes that πΉ is differentiable on its domain, but does not require πΉ to be differentiable on the whole real line. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π½ = (TopOpenββfld) β β’ (((π β {β, β} β§ πΉ:π΄βΆβ) β§ (π΄ β π½ β§ dom (β D πΉ) = π΄)) β (π D (πΉ βΎ π)) = ((β D πΉ) βΎ π)) | ||
Theorem | dvidlem 25432* | Lemma for dvid 25435 and dvconst 25434. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
β’ (π β πΉ:ββΆβ) & β’ ((π β§ (π₯ β β β§ π§ β β β§ π§ β π₯)) β (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯)) = π΅) & β’ π΅ β β β β’ (π β (β D πΉ) = (β Γ {π΅})) | ||
Theorem | dvmptresicc 25433* | Derivative of a function restricted to a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β β β¦ π΄) & β’ ((π β§ π₯ β β) β π΄ β β) & β’ (π β (β D πΉ) = (π₯ β β β¦ π΅)) & β’ ((π β§ π₯ β β) β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) β β’ (π β (β D (π₯ β (πΆ[,]π·) β¦ π΄)) = (π₯ β (πΆ(,)π·) β¦ π΅)) | ||
Theorem | dvconst 25434 | Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
β’ (π΄ β β β (β D (β Γ {π΄})) = (β Γ {0})) | ||
Theorem | dvid 25435 | Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.) |
β’ (β D ( I βΎ β)) = (β Γ {1}) | ||
Theorem | dvcnp 25436* | The difference quotient is continuous at π΅ when the original function is differentiable at π΅. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) |
β’ π½ = (πΎ βΎt π΄) & β’ πΎ = (TopOpenββfld) & β’ πΊ = (π§ β π΄ β¦ if(π§ = π΅, ((π D πΉ)βπ΅), (((πΉβπ§) β (πΉβπ΅)) / (π§ β π΅)))) β β’ (((π β {β, β} β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅ β dom (π D πΉ)) β πΊ β ((π½ CnP πΎ)βπ΅)) | ||
Theorem | dvcnp2 25437 | 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 π΄) & β’ πΎ = (TopOpenββfld) β β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ π΅ β dom (π D πΉ)) β πΉ β ((π½ CnP πΎ)βπ΅)) | ||
Theorem | dvcn 25438 | A differentiable function is continuous. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-Sep-2015.) |
β’ (((π β β β§ πΉ:π΄βΆβ β§ π΄ β π) β§ dom (π D πΉ) = π΄) β πΉ β (π΄βcnββ)) | ||
Theorem | dvnfval 25439* | Value of the iterated derivative. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ πΊ = (π₯ β V β¦ (π D π₯)) β β’ ((π β β β§ πΉ β (β βpm π)) β (π Dπ πΉ) = seq0((πΊ β 1st ), (β0 Γ {πΉ}))) | ||
Theorem | dvnff 25440 | The iterated derivative is a function. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ ((π β {β, β} β§ πΉ β (β βpm π)) β (π Dπ πΉ):β0βΆ(β βpm dom πΉ)) | ||
Theorem | dvn0 25441 | Zero times iterated derivative. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ ((π β β β§ πΉ β (β βpm π)) β ((π Dπ πΉ)β0) = πΉ) | ||
Theorem | dvnp1 25442 | Successor iterated derivative. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ ((π β β β§ πΉ β (β βpm π) β§ π β β0) β ((π Dπ πΉ)β(π + 1)) = (π D ((π Dπ πΉ)βπ))) | ||
Theorem | dvn1 25443 | One times iterated derivative. (Contributed by Mario Carneiro, 1-Jan-2017.) |
β’ ((π β β β§ πΉ β (β βpm π)) β ((π Dπ πΉ)β1) = (π D πΉ)) | ||
Theorem | dvnf 25444 | The N-times derivative is a function. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ ((π β {β, β} β§ πΉ β (β βpm π) β§ π β β0) β ((π Dπ πΉ)βπ):dom ((π Dπ πΉ)βπ)βΆβ) | ||
Theorem | dvnbss 25445 | The set of N-times differentiable points is a subset of the domain of the function. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ ((π β {β, β} β§ πΉ β (β βpm π) β§ π β β0) β dom ((π Dπ πΉ)βπ) β dom πΉ) | ||
Theorem | dvnadd 25446 | The π-th derivative of the π-th derivative of πΉ is the same as the π + π-th derivative of πΉ. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ (((π β {β, β} β§ πΉ β (β βpm π)) β§ (π β β0 β§ π β β0)) β ((π Dπ ((π Dπ πΉ)βπ))βπ) = ((π Dπ πΉ)β(π + π))) | ||
Theorem | dvn2bss 25447 | An N-times differentiable point is an M-times differentiable point, if π β€ π. (Contributed by Mario Carneiro, 30-Dec-2016.) |
β’ ((π β {β, β} β§ πΉ β (β βpm π) β§ π β (0...π)) β dom ((π Dπ πΉ)βπ) β dom ((π Dπ πΉ)βπ)) | ||
Theorem | dvnres 25448 | Multiple derivative version of dvres3a 25431. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ (((π β {β, β} β§ πΉ β (β βpm β) β§ π β β0) β§ dom ((β Dπ πΉ)βπ) = dom πΉ) β ((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π)) | ||
Theorem | cpnfval 25449* | Condition for n-times continuous differentiability. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ (π β β β (πCπβπ) = (π β β0 β¦ {π β (β βpm π) β£ ((π Dπ π)βπ) β (dom πβcnββ)})) | ||
Theorem | fncpn 25450 | The πCπ object is a function. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ (π β β β (πCπβπ) Fn β0) | ||
Theorem | elcpn 25451 | Condition for n-times continuous differentiability. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ ((π β β β§ π β β0) β (πΉ β ((πCπβπ)βπ) β (πΉ β (β βpm π) β§ ((π Dπ πΉ)βπ) β (dom πΉβcnββ)))) | ||
Theorem | cpnord 25452 | πCπ conditions are ordered by strength. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ ((π β {β, β} β§ π β β0 β§ π β (β€β₯βπ)) β ((πCπβπ)βπ) β ((πCπβπ)βπ)) | ||
Theorem | cpncn 25453 | A πCπ function is continuous. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ ((π β {β, β} β§ πΉ β ((πCπβπ)βπ)) β πΉ β (dom πΉβcnββ)) | ||
Theorem | cpnres 25454 | The restriction of a πCπ function is πCπ. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ ((π β {β, β} β§ πΉ β ((πCπββ)βπ)) β (πΉ βΎ π) β ((πCπβπ)βπ)) | ||
Theorem | dvaddbr 25455 | The sum rule for derivatives at a point. For the (simpler but more limited) function version, see dvadd 25457. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) |
β’ (π β πΉ:πβΆβ) & β’ (π β π β π) & β’ (π β πΊ:πβΆβ) & β’ (π β π β π) & β’ (π β π β β) & β’ (π β πΎ β π) & β’ (π β πΏ β π) & β’ (π β πΆ(π D πΉ)πΎ) & β’ (π β πΆ(π D πΊ)πΏ) & β’ π½ = (TopOpenββfld) β β’ (π β πΆ(π D (πΉ βf + πΊ))(πΎ + πΏ)) | ||
Theorem | dvmulbr 25456 | The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmul 25458. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) |
β’ (π β πΉ:πβΆβ) & β’ (π β π β π) & β’ (π β πΊ:πβΆβ) & β’ (π β π β π) & β’ (π β π β β) & β’ (π β πΎ β π) & β’ (π β πΏ β π) & β’ (π β πΆ(π D πΉ)πΎ) & β’ (π β πΆ(π D πΊ)πΏ) & β’ π½ = (TopOpenββfld) β β’ (π β πΆ(π D (πΉ βf Β· πΊ))((πΎ Β· (πΊβπΆ)) + (πΏ Β· (πΉβπΆ)))) | ||
Theorem | dvadd 25457 | The sum rule for derivatives at a point. For the (more general) relation version, see dvaddbr 25455. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
β’ (π β πΉ:πβΆβ) & β’ (π β π β π) & β’ (π β πΊ:πβΆβ) & β’ (π β π β π) & β’ (π β π β {β, β}) & β’ (π β πΆ β dom (π D πΉ)) & β’ (π β πΆ β dom (π D πΊ)) β β’ (π β ((π D (πΉ βf + πΊ))βπΆ) = (((π D πΉ)βπΆ) + ((π D πΊ)βπΆ))) | ||
Theorem | dvmul 25458 | The product rule for derivatives at a point. For the (more general) relation version, see dvmulbr 25456. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
β’ (π β πΉ:πβΆβ) & β’ (π β π β π) & β’ (π β πΊ:πβΆβ) & β’ (π β π β π) & β’ (π β π β {β, β}) & β’ (π β πΆ β dom (π D πΉ)) & β’ (π β πΆ β dom (π D πΊ)) β β’ (π β ((π D (πΉ βf Β· πΊ))βπΆ) = ((((π D πΉ)βπΆ) Β· (πΊβπΆ)) + (((π D πΊ)βπΆ) Β· (πΉβπΆ)))) | ||
Theorem | dvaddf 25459 | 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 (πΉ βf + πΊ)) = ((π D πΉ) βf + (π D πΊ))) | ||
Theorem | dvmulf 25460 | 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 (πΉ βf Β· πΊ)) = (((π D πΉ) βf Β· πΊ) βf + ((π D πΊ) βf Β· πΉ))) | ||
Theorem | dvcmul 25461 | The product rule when one argument is a constant. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:πβΆβ) & β’ (π β π΄ β β) & β’ (π β π β π) & β’ (π β πΆ β dom (π D πΉ)) β β’ (π β ((π D ((π Γ {π΄}) βf Β· πΉ))βπΆ) = (π΄ Β· ((π D πΉ)βπΆ))) | ||
Theorem | dvcmulf 25462 | The product rule when one argument is a constant. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
β’ (π β π β {β, β}) & β’ (π β πΉ:πβΆβ) & β’ (π β π΄ β β) & β’ (π β dom (π D πΉ) = π) β β’ (π β (π D ((π Γ {π΄}) βf Β· πΉ)) = ((π Γ {π΄}) βf Β· (π D πΉ))) | ||
Theorem | dvcobr 25463 | The chain rule for derivatives at a point. For the (simpler but more limited) function version, see dvco 25464. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.) |
β’ (π β πΉ:πβΆβ) & β’ (π β π β π) & β’ (π β πΊ:πβΆπ) & β’ (π β π β π) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΎ β π) & β’ (π β πΏ β π) & β’ (π β (πΊβπΆ)(π D πΉ)πΎ) & β’ (π β πΆ(π D πΊ)πΏ) & β’ π½ = (TopOpenββfld) β β’ (π β πΆ(π D (πΉ β πΊ))(πΎ Β· πΏ)) | ||
Theorem | dvco 25464 | The chain rule for derivatives at a point. For the (more general) relation version, see dvcobr 25463. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
β’ (π β πΉ:πβΆβ) & β’ (π β π β π) & β’ (π β πΊ:πβΆπ) & β’ (π β π β π) & β’ (π β π β {β, β}) & β’ (π β π β {β, β}) & β’ (π β (πΊβπΆ) β dom (π D πΉ)) & β’ (π β πΆ β dom (π D πΊ)) β β’ (π β ((π D (πΉ β πΊ))βπΆ) = (((π D πΉ)β(πΊβπΆ)) Β· ((π D πΊ)βπΆ))) | ||
Theorem | dvcof 25465 | The chain rule for everywhere-differentiable functions. (Contributed by Mario Carneiro, 10-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
β’ (π β π β {β, β}) & β’ (π β π β {β, β}) & β’ (π β πΉ:πβΆβ) & β’ (π β πΊ:πβΆπ) & β’ (π β dom (π D πΉ) = π) & β’ (π β dom (π D πΊ) = π) β β’ (π β (π D (πΉ β πΊ)) = (((π D πΉ) β πΊ) βf Β· (π D πΊ))) | ||
Theorem | dvcjbr 25466 | The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj 25467. (This doesn't follow from dvcobr 25463 because β is not a function on the reals, and even if we used complex derivatives, β is not complex-differentiable.) (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
β’ (π β πΉ:πβΆβ) & β’ (π β π β β) & β’ (π β πΆ β dom (β D πΉ)) β β’ (π β πΆ(β D (β β πΉ))(ββ((β D πΉ)βπΆ))) | ||
Theorem | dvcj 25467 | The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr 25466. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
β’ ((πΉ:πβΆβ β§ π β β) β (β D (β β πΉ)) = (β β (β D πΉ))) | ||
Theorem | dvfre 25468 | The derivative of a real function is real. (Contributed by Mario Carneiro, 1-Sep-2014.) |
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (β D πΉ):dom (β D πΉ)βΆβ) | ||
Theorem | dvnfre 25469 | The π-th derivative of a real function is real. (Contributed by Mario Carneiro, 1-Jan-2017.) |
β’ ((πΉ:π΄βΆβ β§ π΄ β β β§ π β β0) β ((β Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ) | ||
Theorem | dvexp 25470* | Derivative of a power function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 10-Feb-2015.) |
β’ (π β β β (β D (π₯ β β β¦ (π₯βπ))) = (π₯ β β β¦ (π Β· (π₯β(π β 1))))) | ||
Theorem | dvexp2 25471* | 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 | dvrec 25472* | Derivative of the reciprocal function. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.) |
β’ (π΄ β β β (β D (π₯ β (β β {0}) β¦ (π΄ / π₯))) = (π₯ β (β β {0}) β¦ -(π΄ / (π₯β2)))) | ||
Theorem | dvmptres3 25473* | Function-builder for derivative: restrict a derivative to a subset. (Contributed by Mario Carneiro, 11-Feb-2015.) |
β’ π½ = (TopOpenββfld) & β’ (π β π β {β, β}) & β’ (π β π β π½) & β’ (π β (π β© π) = π) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) β β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) | ||
Theorem | dvmptid 25474* | Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ (π β π β {β, β}) β β’ (π β (π D (π₯ β π β¦ π₯)) = (π₯ β π β¦ 1)) | ||
Theorem | dvmptc 25475* | Function-builder for derivative: derivative of a constant. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ (π β π β {β, β}) & β’ (π β π΄ β β) β β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ 0)) | ||
Theorem | dvmptcl 25476* | Closure lemma for dvmptcmul 25481 and other related theorems. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) β β’ ((π β§ π₯ β π) β π΅ β β) | ||
Theorem | dvmptadd 25477* | Function-builder for derivative, addition rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ ((π β§ π₯ β π) β π· β π) & β’ (π β (π D (π₯ β π β¦ πΆ)) = (π₯ β π β¦ π·)) β β’ (π β (π D (π₯ β π β¦ (π΄ + πΆ))) = (π₯ β π β¦ (π΅ + π·))) | ||
Theorem | dvmptmul 25478* | Function-builder for derivative, product rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ ((π β§ π₯ β π) β π· β π) & β’ (π β (π D (π₯ β π β¦ πΆ)) = (π₯ β π β¦ π·)) β β’ (π β (π D (π₯ β π β¦ (π΄ Β· πΆ))) = (π₯ β π β¦ ((π΅ Β· πΆ) + (π· Β· π΄)))) | ||
Theorem | dvmptres2 25479* | Function-builder for derivative: restrict a derivative to a subset. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π β π β π) & β’ π½ = (πΎ βΎt π) & β’ πΎ = (TopOpenββfld) & β’ (π β ((intβπ½)βπ) = π) β β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) | ||
Theorem | dvmptres 25480* | Function-builder for derivative: restrict a derivative to an open subset. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π β π β π) & β’ π½ = (πΎ βΎt π) & β’ πΎ = (TopOpenββfld) & β’ (π β π β π½) β β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) | ||
Theorem | dvmptcmul 25481* | Function-builder for derivative, product rule for constant multiplier. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π β πΆ β β) β β’ (π β (π D (π₯ β π β¦ (πΆ Β· π΄))) = (π₯ β π β¦ (πΆ Β· π΅))) | ||
Theorem | dvmptdivc 25482* | Function-builder for derivative, division rule for constant divisor. (Contributed by Mario Carneiro, 18-May-2016.) |
β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π β πΆ β β) & β’ (π β πΆ β 0) β β’ (π β (π D (π₯ β π β¦ (π΄ / πΆ))) = (π₯ β π β¦ (π΅ / πΆ))) | ||
Theorem | dvmptneg 25483* | Function-builder for derivative, product rule for negatives. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) β β’ (π β (π D (π₯ β π β¦ -π΄)) = (π₯ β π β¦ -π΅)) | ||
Theorem | dvmptsub 25484* | Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ ((π β§ π₯ β π) β πΆ β β) & β’ ((π β§ π₯ β π) β π· β π) & β’ (π β (π D (π₯ β π β¦ πΆ)) = (π₯ β π β¦ π·)) β β’ (π β (π D (π₯ β π β¦ (π΄ β πΆ))) = (π₯ β π β¦ (π΅ β π·))) | ||
Theorem | dvmptcj 25485* | Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) β β’ (π β (β D (π₯ β π β¦ (ββπ΄))) = (π₯ β π β¦ (ββπ΅))) | ||
Theorem | dvmptre 25486* | Function-builder for derivative, real part. (Contributed by Mario Carneiro, 1-Sep-2014.) |
β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) β β’ (π β (β D (π₯ β π β¦ (ββπ΄))) = (π₯ β π β¦ (ββπ΅))) | ||
Theorem | dvmptim 25487* | Function-builder for derivative, imaginary part. (Contributed by Mario Carneiro, 1-Sep-2014.) |
β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) β β’ (π β (β D (π₯ β π β¦ (ββπ΄))) = (π₯ β π β¦ (ββπ΅))) | ||
Theorem | dvmptntr 25488* | Function-builder for derivative: expand the function from an open set to its closure. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 11-Feb-2015.) |
β’ (π β π β β) & β’ (π β π β π) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ π½ = (πΎ βΎt π) & β’ πΎ = (TopOpenββfld) & β’ (π β ((intβπ½)βπ) = π) β β’ (π β (π D (π₯ β π β¦ π΄)) = (π D (π₯ β π β¦ π΄))) | ||
Theorem | dvmptco 25489* | Function-builder for derivative, chain rule. (Contributed by Mario Carneiro, 1-Sep-2014.) |
β’ (π β π β {β, β}) & β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β π) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ ((π β§ π¦ β π) β πΆ β β) & β’ ((π β§ π¦ β π) β π· β π) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ (π β (π D (π¦ β π β¦ πΆ)) = (π¦ β π β¦ π·)) & β’ (π¦ = π΄ β πΆ = πΈ) & β’ (π¦ = π΄ β π· = πΉ) β β’ (π β (π D (π₯ β π β¦ πΈ)) = (π₯ β π β¦ (πΉ Β· π΅))) | ||
Theorem | dvrecg 25490* | Derivative of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ (π β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β (β β {0})) & β’ ((π β§ π₯ β π) β πΆ β π) & β’ (π β (π D (π₯ β π β¦ π΅)) = (π₯ β π β¦ πΆ)) β β’ (π β (π D (π₯ β π β¦ (π΄ / π΅))) = (π₯ β π β¦ -((π΄ Β· πΆ) / (π΅β2)))) | ||
Theorem | dvmptdiv 25491* | Function-builder for derivative, quotient rule. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β {β, β}) & β’ ((π β§ π₯ β π) β π΄ β β) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) & β’ ((π β§ π₯ β π) β πΆ β (β β {0})) & β’ ((π β§ π₯ β π) β π· β β) & β’ (π β (π D (π₯ β π β¦ πΆ)) = (π₯ β π β¦ π·)) β β’ (π β (π D (π₯ β π β¦ (π΄ / πΆ))) = (π₯ β π β¦ (((π΅ Β· πΆ) β (π· Β· π΄)) / (πΆβ2)))) | ||
Theorem | dvmptfsum 25492* | Function-builder for derivative, finite sums rule. (Contributed by Stefan O'Rear, 12-Nov-2014.) |
β’ π½ = (πΎ βΎt π) & β’ πΎ = (TopOpenββfld) & β’ (π β π β {β, β}) & β’ (π β π β π½) & β’ (π β πΌ β Fin) & β’ ((π β§ π β πΌ β§ π₯ β π) β π΄ β β) & β’ ((π β§ π β πΌ β§ π₯ β π) β π΅ β β) & β’ ((π β§ π β πΌ) β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) β β’ (π β (π D (π₯ β π β¦ Ξ£π β πΌ π΄)) = (π₯ β π β¦ Ξ£π β πΌ π΅)) | ||
Theorem | dvcnvlem 25493 | Lemma for dvcnvre 25536. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.) |
β’ π½ = (TopOpenββfld) & β’ πΎ = (π½ βΎt π) & β’ (π β π β {β, β}) & β’ (π β π β πΎ) & β’ (π β πΉ:πβ1-1-ontoβπ) & β’ (π β β‘πΉ β (πβcnβπ)) & β’ (π β dom (π D πΉ) = π) & β’ (π β Β¬ 0 β ran (π D πΉ)) & β’ (π β πΆ β π) β β’ (π β (πΉβπΆ)(π D β‘πΉ)(1 / ((π D πΉ)βπΆ))) | ||
Theorem | dvcnv 25494* | A weak version of dvcnvre 25536, valid for both real and complex domains but under the hypothesis that the inverse function is already known to be continuous, and the image set is known to be open. A more advanced proof can show that these conditions are unnecessary. (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.) |
β’ π½ = (TopOpenββfld) & β’ πΎ = (π½ βΎt π) & β’ (π β π β {β, β}) & β’ (π β π β πΎ) & β’ (π β πΉ:πβ1-1-ontoβπ) & β’ (π β β‘πΉ β (πβcnβπ)) & β’ (π β dom (π D πΉ) = π) & β’ (π β Β¬ 0 β ran (π D πΉ)) β β’ (π β (π D β‘πΉ) = (π₯ β π β¦ (1 / ((π D πΉ)β(β‘πΉβπ₯))))) | ||
Theorem | dvexp3 25495* | Derivative of an exponential of integer exponent. (Contributed by Mario Carneiro, 26-Feb-2015.) |
β’ (π β β€ β (β D (π₯ β (β β {0}) β¦ (π₯βπ))) = (π₯ β (β β {0}) β¦ (π Β· (π₯β(π β 1))))) | ||
Theorem | dveflem 25496 | Derivative of the exponential function at 0. The key step in the proof is eftlub 16052, 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 25497 | Derivative of the exponential function. (Contributed by Mario Carneiro, 9-Aug-2014.) (Proof shortened by Mario Carneiro, 10-Feb-2015.) |
β’ (β D exp) = exp | ||
Theorem | dvsincos 25498 | Derivative of the sine and cosine functions. (Contributed by Mario Carneiro, 21-May-2016.) |
β’ ((β D sin) = cos β§ (β D cos) = (π₯ β β β¦ -(sinβπ₯))) | ||
Theorem | dvsin 25499 | Derivative of the sine function. (Contributed by Mario Carneiro, 21-May-2016.) |
β’ (β D sin) = cos | ||
Theorem | dvcos 25500 | Derivative of the cosine function. (Contributed by Mario Carneiro, 21-May-2016.) |
β’ (β D cos) = (π₯ β β β¦ -(sinβπ₯)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |