P. 237 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23601-23700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	itgabs 23601*	The triangle inequality for integrals. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   =>    |- ( ph -> ( abs ` S. A B _d x ) <_ S. A ( abs ` B ) _d x )
Theorem	itgsplit 23602*	The S. integral splits under an almost disjoint union. (Contributed by Mario Carneiro, 11-Aug-2014.)
|- ( ph -> ( vol* ` ( A i^i B ) ) = 0 )   &    |- ( ph -> U = ( A u. B ) )   &    |- ( ( ph /\ x e. U ) -> C e. V )   &    |- ( ph -> ( x e. A |-> C ) e. L^1 )   &    |- ( ph -> ( x e. B |-> C ) e. L^1 )   =>    |- ( ph -> S. U C _d x = ( S. A C _d x + S. B C _d x ) )
Theorem	itgspliticc 23603*	The S. integral splits on closed intervals with matching endpoints. (Contributed by Mario Carneiro, 13-Aug-2014.)
|- ( ph -> A e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> B e. ( A [,] C ) )   &    |- ( ( ph /\ x e. ( A [,] C ) ) -> D e. V )   &    |- ( ph -> ( x e. ( A [,] B ) |-> D ) e. L^1 )   &    |- ( ph -> ( x e. ( B [,] C ) |-> D ) e. L^1 )   =>    |- ( ph -> S. ( A [,] C ) D _d x = ( S. ( A [,] B ) D _d x + S. ( B [,] C ) D _d x ) )
Theorem	itgsplitioo 23604*	The S. integral splits on open intervals with matching endpoints. (Contributed by Mario Carneiro, 2-Sep-2014.)
|- ( ph -> A e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> B e. ( A [,] C ) )   &    |- ( ( ph /\ x e. ( A (,) C ) ) -> D e. CC )   &    |- ( ph -> ( x e. ( A (,) B ) |-> D ) e. L^1 )   &    |- ( ph -> ( x e. ( B (,) C ) |-> D ) e. L^1 )   =>    |- ( ph -> S. ( A (,) C ) D _d x = ( S. ( A (,) B ) D _d x + S. ( B (,) C ) D _d x ) )
Theorem	bddmulibl 23605*	A bounded function times an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)
|- ( ( F e. MblFn /\ G e. L^1 /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> ( F oF x. G ) e. L^1 )
Theorem	bddibl 23606*	A bounded function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)
|- ( ( F e. MblFn /\ ( vol ` dom F ) e. RR /\ E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x ) -> F e. L^1 )
Theorem	cniccibl 23607	A continuous function on a closed bounded interval is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)
|- ( ( A e. RR /\ B e. RR /\ F e. ( ( A [,] B ) -cn-> CC ) ) -> F e. L^1 )
Theorem	itggt0 23608*	The integral of a strictly positive function is positive. (Contributed by Mario Carneiro, 30-Aug-2014.)
|- ( ph -> 0 < ( vol ` A ) )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   &    |- ( ( ph /\ x e. A ) -> B e. RR+ )   =>    |- ( ph -> 0 < S. A B _d x )
Theorem	itgcn 23609*	Transfer itg2cn 23530 to the full Lebesgue integral. (Contributed by Mario Carneiro, 1-Sep-2014.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. L^1 )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> E. d e. RR+ A. u e. dom vol ( ( u C_ A /\ ( vol ` u ) < d ) -> S. u ( abs ` B ) _d x < C ) )
13.2.2.2  Lesbesgue directed integral
Syntax	cdit 23610	Extend class notation with the directed integral.
class S__ [ A -> B ] C _d x
Definition	df-ditg 23611	Define the directed integral, which is just a regular integral but with a sign change when the limits are interchanged. The A and B here are the lower and upper limits of the integral, usually written as a subscript and superscript next to the integral sign. We define the region of integration to be an open interval instead of closed so that we can use +oo , -oo for limits and also integrate up to a singularity at an endpoint. (Contributed by Mario Carneiro, 13-Aug-2014.)
|- S__ [ A -> B ] C _d x = if ( A <_ B , S. ( A (,) B ) C _d x , -u S. ( B (,) A ) C _d x )
Theorem	ditgeq1 23612*	Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.)
|- ( A = B -> S__ [ A -> C ] D _d x = S__ [ B -> C ] D _d x )
Theorem	ditgeq2 23613*	Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.)
|- ( A = B -> S__ [ C -> A ] D _d x = S__ [ C -> B ] D _d x )
Theorem	ditgeq3 23614*	Equality theorem for the directed integral. (The domain of the equality here is very rough; for more precise bounds one should decompose it with ditgpos 23620 first and use the equality theorems for df-itg 23392.) (Contributed by Mario Carneiro, 13-Aug-2014.)
|- ( A. x e. RR D = E -> S__ [ A -> B ] D _d x = S__ [ A -> B ] E _d x )
Theorem	ditgeq3dv 23615*	Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.)
|- ( ( ph /\ x e. RR ) -> D = E )   =>    |- ( ph -> S__ [ A -> B ] D _d x = S__ [ A -> B ] E _d x )
Theorem	ditgex 23616	A directed integral is a set. (Contributed by Mario Carneiro, 7-Sep-2014.)
|- S__ [ A -> B ] C _d x e. _V
Theorem	ditg0 23617*	Value of the directed integral from a point to itself. (Contributed by Mario Carneiro, 13-Aug-2014.)
|- S__ [ A -> A ] B _d x = 0
Theorem	cbvditg 23618*	Change bound variable in a directed integral. (Contributed by Mario Carneiro, 7-Sep-2014.)
|- ( x = y -> C = D )   &    |- F/_ y C   &    |- F/_ x D   =>    |- S__ [ A -> B ] C _d x = S__ [ A -> B ] D _d y
Theorem	cbvditgv 23619*	Change bound variable in a directed integral. (Contributed by Mario Carneiro, 7-Sep-2014.)
|- ( x = y -> C = D )   =>    |- S__ [ A -> B ] C _d x = S__ [ A -> B ] D _d y
Theorem	ditgpos 23620*	Value of the directed integral in the forward direction. (Contributed by Mario Carneiro, 13-Aug-2014.)
|- ( ph -> A <_ B )   =>    |- ( ph -> S__ [ A -> B ] C _d x = S. ( A (,) B ) C _d x )
Theorem	ditgneg 23621*	Value of the directed integral in the backward direction. (Contributed by Mario Carneiro, 13-Aug-2014.)
|- ( ph -> A <_ B )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> S__ [ B -> A ] C _d x = -u S. ( A (,) B ) C _d x )
Theorem	ditgcl 23622*	Closure of a directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.)
|- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> A e. ( X [,] Y ) )   &    |- ( ph -> B e. ( X [,] Y ) )   &    |- ( ( ph /\ x e. ( X (,) Y ) ) -> C e. V )   &    |- ( ph -> ( x e. ( X (,) Y ) |-> C ) e. L^1 )   =>    |- ( ph -> S__ [ A -> B ] C _d x e. CC )
Theorem	ditgswap 23623*	Reverse a directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.)
|- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> A e. ( X [,] Y ) )   &    |- ( ph -> B e. ( X [,] Y ) )   &    |- ( ( ph /\ x e. ( X (,) Y ) ) -> C e. V )   &    |- ( ph -> ( x e. ( X (,) Y ) |-> C ) e. L^1 )   =>    |- ( ph -> S__ [ B -> A ] C _d x = -u S__ [ A -> B ] C _d x )
Theorem	ditgsplitlem 23624*	Lemma for ditgsplit 23625. (Contributed by Mario Carneiro, 13-Aug-2014.)
|- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> A e. ( X [,] Y ) )   &    |- ( ph -> B e. ( X [,] Y ) )   &    |- ( ph -> C e. ( X [,] Y ) )   &    |- ( ( ph /\ x e. ( X (,) Y ) ) -> D e. V )   &    |- ( ph -> ( x e. ( X (,) Y ) |-> D ) e. L^1 )   &    |- ( ( ps /\ th ) <-> ( A <_ B /\ B <_ C ) )   =>    |- ( ( ( ph /\ ps ) /\ th ) -> S__ [ A -> C ] D _d x = ( S__ [ A -> B ] D _d x + S__ [ B -> C ] D _d x ) )
Theorem	ditgsplit 23625*	This theorem is the raison d'être for the directed integral, because unlike itgspliticc 23603, there is no constraint on the ordering of the points A , B , C in the domain. (Contributed by Mario Carneiro, 13-Aug-2014.)
|- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> A e. ( X [,] Y ) )   &    |- ( ph -> B e. ( X [,] Y ) )   &    |- ( ph -> C e. ( X [,] Y ) )   &    |- ( ( ph /\ x e. ( X (,) Y ) ) -> D e. V )   &    |- ( ph -> ( x e. ( X (,) Y ) |-> D ) e. L^1 )   =>    |- ( ph -> S__ [ A -> C ] D _d x = ( S__ [ A -> B ] D _d x + S__ [ B -> C ] D _d x ) )
13.3  Derivatives
13.3.1  Real and complex differentiation
13.3.1.1  Derivatives of functions of one complex or real variable
Syntax	climc 23626	The limit operator.
class lim CC
Syntax	cdv 23627	The derivative operator.
class _D
Syntax	cdvn 23628	The n-th derivative operator.
class Dn
Syntax	ccpn 23629	The set of n-times continuously differentiable functions.
class C^n
Definition	df-limc 23630*	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.)
|- lim CC = ( f e. ( CC ^pm CC ) , x e. CC |-> { y | [. ( TopOpen ` ℂfld ) / j ]. ( z e. ( dom f u. { x } ) |-> if ( z = x , y , ( f ` z ) ) ) e. ( ( ( j ↾t ( dom f u. { x } ) ) CnP j ) ` x ) } )
Definition	df-dv 23631*	Define the derivative operator on functions on the reals. 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 s 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 CC and is well-behaved when s contains no isolated points, we will restrict our attention to the cases s = RR or s = CC for the majority of the development, these corresponding respectively to real and complex differentiation. (Contributed by Mario Carneiro, 7-Aug-2014.)
|- _D = ( s e. ~P CC , f e. ( CC ^pm s ) |-> U_ x e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) lim CC x ) ) )
Definition	df-dvn 23632*	Define the n-th derivative operator on functions on the complex numbers. This just iterates the derivative operation according to the last argument. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- Dn = ( s e. ~P CC , f e. ( CC ^pm s ) |-> seq 0 ( ( ( x e. _V |-> ( s _D x ) ) o. 1st ) , ( NN0 X. { f } ) ) )
Definition	df-cpn 23633*	Define the set of n-times continuously differentiable functions. (Contributed by Stefan O'Rear, 15-Nov-2014.)
|- C^n = ( s e. ~P CC |-> ( x e. NN0 |-> { f e. ( CC ^pm s ) | ( ( s Dn f ) ` x ) e. ( dom f -cn-> CC ) } ) )
Theorem	reldv 23634	The derivative function is a relation. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 24-Dec-2016.)
|- Rel ( S _D F )
Theorem	limcvallem 23635*	Lemma for ellimc 23637. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- J = ( K ↾t ( A u. { B } ) )   &    |- K = ( TopOpen ` ℂfld )   &    |- G = ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) )   =>    |- ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) -> ( G e. ( ( J CnP K ) ` B ) -> C e. CC ) )
Theorem	limcfval 23636*	Value and set bounds on the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- J = ( K ↾t ( A u. { B } ) )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ( F : A --> CC /\ A C_ CC /\ B e. CC ) -> ( ( F lim CC B ) = { y | ( z e. ( A u. { B } ) |-> if ( z = B , y , ( F ` z ) ) ) e. ( ( J CnP K ) ` B ) } /\ ( F lim CC B ) C_ CC ) )
Theorem	ellimc 23637*	Value of the limit predicate. C is the limit of the function F at B if the function G, formed by adding B to the domain of F and setting it to C, is continuous at B. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- J = ( K ↾t ( A u. { B } ) )   &    |- K = ( TopOpen ` ℂfld )   &    |- G = ( z e. ( A u. { B } ) |-> if ( z = B , C , ( F ` z ) ) )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( C e. ( F lim CC B ) <-> G e. ( ( J CnP K ) ` B ) ) )
Theorem	limcrcl 23638	Reverse closure for the limit operator. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( C e. ( F lim CC B ) -> ( F : dom F --> CC /\ dom F C_ CC /\ B e. CC ) )
Theorem	limccl 23639	Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( F lim CC B ) C_ CC
Theorem	limcdif 23640	It suffices to consider functions which are not defined at B to define the limit of a function. In particular, the value of the original function F at B does not affect the limit of F. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( ph -> F : A --> CC )   =>    |- ( ph -> ( F lim CC B ) = ( ( F |` ( A \ { B } ) ) lim CC B ) )
Theorem	ellimc2 23641*	Write the definition of a limit directly in terms of open sets of the topology on the complex numbers. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ph -> ( C e. ( F lim CC B ) <-> ( C e. CC /\ A. u e. K ( C e. u -> E. w e. K ( B e. w /\ ( F " ( w i^i ( A \ { B } ) ) ) C_ u ) ) ) ) )
Theorem	limcnlp 23642	If B is not a limit point of the domain of the function F, then every point is a limit of F at B. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   &    |- K = ( TopOpen ` ℂfld )   &    |- ( ph -> -. B e. ( ( limPt ` K ) ` A ) )   =>    |- ( ph -> ( F lim CC B ) = CC )
Theorem	ellimc3 23643*	Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( C e. ( F lim CC B ) <-> ( C e. CC /\ A. x e. RR+ E. y e. RR+ A. z e. A ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) )
Theorem	limcflflem 23644	Lemma for limcflf 23645. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. ( ( limPt ` K ) ` A ) )   &    |- K = ( TopOpen ` ℂfld )   &    |- C = ( A \ { B } )   &    |- L = ( ( ( nei ` K ) ` { B } ) ↾t C )   =>    |- ( ph -> L e. ( Fil ` C ) )
Theorem	limcflf 23645	The limit operator can be expressed as a filter limit, from the filter of neighborhoods of B restricted to A \ { B }, to the topology of the complex numbers. (If B is not a limit point of A, then it is still formally a filter limit, but the neighborhood filter is not a proper filter in this case.) (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. ( ( limPt ` K ) ` A ) )   &    |- K = ( TopOpen ` ℂfld )   &    |- C = ( A \ { B } )   &    |- L = ( ( ( nei ` K ) ` { B } ) ↾t C )   =>    |- ( ph -> ( F lim CC B ) = ( ( K fLimf L ) ` ( F |` C ) ) )
Theorem	limcmo 23646*	If B is a limit point of the domain of the function F, then there is at most one limit value of F at B. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ CC )   &    |- ( ph -> B e. ( ( limPt ` K ) ` A ) )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ph -> E* x x e. ( F lim CC B ) )
Theorem	limcmpt 23647*	Express the limit operator for a function defined by a mapping. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( ph -> A C_ CC )   &    |- ( ph -> B e. CC )   &    |- ( ( ph /\ z e. A ) -> D e. CC )   &    |- J = ( K ↾t ( A u. { B } ) )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ph -> ( C e. ( ( z e. A |-> D ) lim CC B ) <-> ( z e. ( A u. { B } ) |-> if ( z = B , C , D ) ) e. ( ( J CnP K ) ` B ) ) )
Theorem	limcmpt2 23648*	Express the limit operator for a function defined by a mapping. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( ph -> A C_ CC )   &    |- ( ph -> B e. A )   &    |- ( ( ph /\ ( z e. A /\ z =/= B ) ) -> D e. CC )   &    |- J = ( K ↾t A )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ph -> ( C e. ( ( z e. ( A \ { B } ) |-> D ) lim CC B ) <-> ( z e. A |-> if ( z = B , C , D ) ) e. ( ( J CnP K ) ` B ) ) )
Theorem	limcresi 23649	Any limit of F is also a limit of the restriction of F. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( F lim CC B ) C_ ( ( F |` C ) lim CC B )
Theorem	limcres 23650	If B is an interior point of C u. { B } relative to the domain A, then a limit point of F |` C extends to a limit of F. (Contributed by Mario Carneiro, 27-Dec-2016.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> C C_ A )   &    |- ( ph -> A C_ CC )   &    |- K = ( TopOpen ` ℂfld )   &    |- J = ( K ↾t ( A u. { B } ) )   &    |- ( ph -> B e. ( ( int ` J ) ` ( C u. { B } ) ) )   =>    |- ( ph -> ( ( F |` C ) lim CC B ) = ( F lim CC B ) )
Theorem	cnplimc 23651	A function is continuous at B iff its limit at B equals the value of the function there. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- K = ( TopOpen ` ℂfld )   &    |- J = ( K ↾t A )   =>    |- ( ( A C_ CC /\ B e. A ) -> ( F e. ( ( J CnP K ) ` B ) <-> ( F : A --> CC /\ ( F ` B ) e. ( F lim CC B ) ) ) )
Theorem	cnlimc 23652*	F 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.)
|- ( A C_ CC -> ( F e. ( A -cn-> CC ) <-> ( F : A --> CC /\ A. x e. A ( F ` x ) e. ( F lim CC x ) ) ) )
Theorem	cnlimci 23653	If F is a continuous function, then the limit of the function at any point equals its value. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( ph -> F e. ( A -cn-> D ) )   &    |- ( ph -> B e. A )   =>    |- ( ph -> ( F ` B ) e. ( F lim CC B ) )
Theorem	cnmptlimc 23654*	If F is a continuous function, then the limit of the function at any point equals its value. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( ph -> ( x e. A |-> X ) e. ( A -cn-> D ) )   &    |- ( ph -> B e. A )   &    |- ( x = B -> X = Y )   =>    |- ( ph -> Y e. ( ( x e. A |-> X ) lim CC B ) )
Theorem	limccnp 23655	If the limit of F at B is C and G is continuous at C, then the limit of G o. F at B is G ( C ). (Contributed by Mario Carneiro, 28-Dec-2016.)
|- ( ph -> F : A --> D )   &    |- ( ph -> D C_ CC )   &    |- K = ( TopOpen ` ℂfld )   &    |- J = ( K ↾t D )   &    |- ( ph -> C e. ( F lim CC B ) )   &    |- ( ph -> G e. ( ( J CnP K ) ` C ) )   =>    |- ( ph -> ( G ` C ) e. ( ( G o. F ) lim CC B ) )
Theorem	limccnp2 23656*	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.)
|- ( ( ph /\ x e. A ) -> R e. X )   &    |- ( ( ph /\ x e. A ) -> S e. Y )   &    |- ( ph -> X C_ CC )   &    |- ( ph -> Y C_ CC )   &    |- K = ( TopOpen ` ℂfld )   &    |- J = ( ( K tX K ) ↾t ( X X. Y ) )   &    |- ( ph -> C e. ( ( x e. A |-> R ) lim CC B ) )   &    |- ( ph -> D e. ( ( x e. A |-> S ) lim CC B ) )   &    |- ( ph -> H e. ( ( J CnP K ) ` <. C , D >. ) )   =>    |- ( ph -> ( C H D ) e. ( ( x e. A |-> ( R H S ) ) lim CC B ) )
Theorem	limcco 23657*	Composition of two limits. (Contributed by Mario Carneiro, 29-Dec-2016.)
|- ( ( ph /\ ( x e. A /\ R =/= C ) ) -> R e. B )   &    |- ( ( ph /\ y e. B ) -> S e. CC )   &    |- ( ph -> C e. ( ( x e. A |-> R ) lim CC X ) )   &    |- ( ph -> D e. ( ( y e. B |-> S ) lim CC C ) )   &    |- ( y = R -> S = T )   &    |- ( ( ph /\ ( x e. A /\ R = C ) ) -> T = D )   =>    |- ( ph -> D e. ( ( x e. A |-> T ) lim CC X ) )
Theorem	limciun 23658*	A point is a limit of F on the finite union U_ x e. A B ( x ) iff it is the limit of the restriction of F to each B ( x ). (Contributed by Mario Carneiro, 30-Dec-2016.)
|- ( ph -> A e. Fin )   &    |- ( ph -> A. x e. A B C_ CC )   &    |- ( ph -> F : U_ x e. A B --> CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( F lim CC C ) = ( CC i^i |^|_ x e. A ( ( F |` B ) lim CC C ) ) )
Theorem	limcun 23659	A point is a limit of F on A u. B iff it is the limit of the restriction of F to A and to B. (Contributed by Mario Carneiro, 30-Dec-2016.)
|- ( ph -> A C_ CC )   &    |- ( ph -> B C_ CC )   &    |- ( ph -> F : ( A u. B ) --> CC )   =>    |- ( ph -> ( F lim CC C ) = ( ( ( F |` A ) lim CC C ) i^i ( ( F |` B ) lim CC C ) ) )
Theorem	dvlem 23660	Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- ( ph -> F : D --> CC )   &    |- ( ph -> D C_ CC )   &    |- ( ph -> B e. D )   =>    |- ( ( ph /\ A e. ( D \ { B } ) ) -> ( ( ( F ` A ) - ( F ` B ) ) / ( A - B ) ) e. CC )
Theorem	dvfval 23661*	Value and set bounds on the derivative operator. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 25-Dec-2016.)
|- T = ( K ↾t S )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) -> ( ( S _D F ) = U_ x e. ( ( int ` T ) ` A ) ( { x } X. ( ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) ) lim CC x ) ) /\ ( S _D F ) C_ ( ( ( int ` T ) ` A ) X. CC ) ) )
Theorem	eldv 23662*	The differentiable predicate. A function F is differentiable at B with derivative C iff F is defined in a neighborhood of B and the difference quotient has limit C at B. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 25-Dec-2016.)
|- T = ( K ↾t S )   &    |- K = ( TopOpen ` ℂfld )   &    |- G = ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ S )   =>    |- ( ph -> ( B ( S _D F ) C <-> ( B e. ( ( int ` T ) ` A ) /\ C e. ( G lim CC B ) ) ) )
Theorem	dvcl 23663	The derivative function takes values in the complex numbers. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- ( ph -> S C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ S )   =>    |- ( ( ph /\ B ( S _D F ) C ) -> C e. CC )
Theorem	dvbssntr 23664	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.)
|- ( ph -> S C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ S )   &    |- J = ( K ↾t S )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ph -> dom ( S _D F ) C_ ( ( int ` J ) ` A ) )
Theorem	dvbss 23665	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.)
|- ( ph -> S C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ S )   =>    |- ( ph -> dom ( S _D F ) C_ A )
Theorem	dvbsss 23666	The set of differentiable points is a subset of the ambient topology. (Contributed by Mario Carneiro, 18-Mar-2015.)
|- dom ( S _D F ) C_ S
Theorem	perfdvf 23667	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.)
|- K = ( TopOpen ` ℂfld )   =>    |- ( ( K ↾t S ) e. Perf -> ( S _D F ) : dom ( S _D F ) --> CC )
Theorem	recnprss 23668	Both RR and CC are subsets of CC. (Contributed by Mario Carneiro, 10-Feb-2015.)
|- ( S e. { RR , CC } -> S C_ CC )
Theorem	recnperf 23669	Both RR and CC are perfect subsets of CC. (Contributed by Mario Carneiro, 28-Dec-2016.)
|- K = ( TopOpen ` ℂfld )   =>    |- ( S e. { RR , CC } -> ( K ↾t S ) e. Perf )
Theorem	dvfg 23670	Explicitly write out the functionality condition on derivative for S = RR and CC. (Contributed by Mario Carneiro, 9-Feb-2015.)
|- ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )
Theorem	dvf 23671	The derivative is a function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- ( RR _D F ) : dom ( RR _D F ) --> CC
Theorem	dvfcn 23672	The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015.)
|- ( CC _D F ) : dom ( CC _D F ) --> CC
Theorem	dvreslem 23673*	Lemma for dvres 23675. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
|- K = ( TopOpen ` ℂfld )   &    |- T = ( K ↾t S )   &    |- G = ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ S )   &    |- ( ph -> B C_ S )   &    |- ( ph -> y e. CC )   =>    |- ( ph -> ( x ( S _D ( F |` B ) ) y <-> ( x ( S _D F ) y /\ x e. ( ( int ` T ) ` B ) ) ) )
Theorem	dvres2lem 23674*	Lemma for dvres2 23676. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 28-Dec-2016.)
|- K = ( TopOpen ` ℂfld )   &    |- T = ( K ↾t S )   &    |- G = ( z e. ( A \ { x } ) |-> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ S )   &    |- ( ph -> B C_ S )   &    |- ( ph -> y e. CC )   &    |- ( ph -> x ( S _D F ) y )   &    |- ( ph -> x e. B )   =>    |- ( ph -> x ( B _D ( F |` B ) ) y )
Theorem	dvres 23675	Restriction of a derivative. Note that our definition of derivative df-dv 23631 would still make sense if we demanded that x 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 x when restricted to different subsets containing x; a classic example is the absolute value function restricted to [ 0 , +oo ) and ( -oo , 0 ]. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- K = ( TopOpen ` ℂfld )   &    |- T = ( K ↾t S )   =>    |- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( S _D ( F |` B ) ) = ( ( S _D F ) |` ( ( int ` T ) ` B ) ) )
Theorem	dvres2 23676	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 23675, there is no simple reverse relation relating real differentiable functions to complex differentiability, and indeed there are functions like Re ( x ) which are everywhere real-differentiable but nowhere complex-differentiable.) (Contributed by Mario Carneiro, 9-Feb-2015.)
|- ( ( ( S C_ CC /\ F : A --> CC ) /\ ( A C_ S /\ B C_ S ) ) -> ( ( S _D F ) |` B ) C_ ( B _D ( F |` B ) ) )
Theorem	dvres3 23677	Restriction of a complex differentiable function to the reals. (Contributed by Mario Carneiro, 10-Feb-2015.)
|- ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A C_ CC /\ S C_ dom ( CC _D F ) ) ) -> ( S _D ( F |` S ) ) = ( ( CC _D F ) |` S ) )
Theorem	dvres3a 23678	Restriction of a complex differentiable function to the reals. This version of dvres3 23677 assumes that F is differentiable on its domain, but does not require F to be differentiable on the whole real line. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- ( ( ( S e. { RR , CC } /\ F : A --> CC ) /\ ( A e. J /\ dom ( CC _D F ) = A ) ) -> ( S _D ( F |` S ) ) = ( ( CC _D F ) |` S ) )
Theorem	dvidlem 23679*	Lemma for dvid 23681 and dvconst 23680. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- ( ph -> F : CC --> CC )   &    |- ( ( ph /\ ( x e. CC /\ z e. CC /\ z =/= x ) ) -> ( ( ( F ` z ) - ( F ` x ) ) / ( z - x ) ) = B )   &    |- B e. CC   =>    |- ( ph -> ( CC _D F ) = ( CC X. { B } ) )
Theorem	dvconst 23680	Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- ( A e. CC -> ( CC _D ( CC X. { A } ) ) = ( CC X. { 0 } ) )
Theorem	dvid 23681	Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 9-Feb-2015.)
|- ( CC _D ( _I |` CC ) ) = ( CC X. { 1 } )
Theorem	dvcnp 23682*	The difference quotient is continuous at B when the original function is differentiable at B. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Mario Carneiro, 28-Dec-2016.)
|- J = ( K ↾t A )   &    |- K = ( TopOpen ` ℂfld )   &    |- G = ( z e. A |-> if ( z = B , ( ( S _D F ) ` B ) , ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) )   =>    |- ( ( ( S e. { RR , CC } /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> G e. ( ( J CnP K ) ` B ) )
Theorem	dvcnp2 23683	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.)
|- J = ( K ↾t A )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ B e. dom ( S _D F ) ) -> F e. ( ( J CnP K ) ` B ) )
Theorem	dvcn 23684	A differentiable function is continuous. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by Mario Carneiro, 7-Sep-2015.)
|- ( ( ( S C_ CC /\ F : A --> CC /\ A C_ S ) /\ dom ( S _D F ) = A ) -> F e. ( A -cn-> CC ) )
Theorem	dvnfval 23685*	Value of the iterated derivative. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- G = ( x e. _V |-> ( S _D x ) )   =>    |- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( S Dn F ) = seq 0 ( ( G o. 1st ) , ( NN0 X. { F } ) ) )
Theorem	dvnff 23686	The iterated derivative is a function. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> ( S Dn F ) : NN0 --> ( CC ^pm dom F ) )
Theorem	dvn0 23687	Zero times iterated derivative. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )
Theorem	dvnp1 23688	Successor iterated derivative. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( ( S Dn F ) ` ( N + 1 ) ) = ( S _D ( ( S Dn F ) ` N ) ) )
Theorem	dvn1 23689	One times iterated derivative. (Contributed by Mario Carneiro, 1-Jan-2017.)
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 1 ) = ( S _D F ) )
Theorem	dvnf 23690	The N-times derivative is a function. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( ( S Dn F ) ` N ) : dom ( ( S Dn F ) ` N ) --> CC )
Theorem	dvnbss 23691	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.)
|- ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> dom ( ( S Dn F ) ` N ) C_ dom F )
Theorem	dvnadd 23692	The N-th derivative of the M-th derivative of F is the same as the M + N-th derivative of F. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( S Dn ( ( S Dn F ) ` M ) ) ` N ) = ( ( S Dn F ) ` ( M + N ) ) )
Theorem	dvn2bss 23693	An N-times differentiable point is an M-times differentiable point, if M <_ N. (Contributed by Mario Carneiro, 30-Dec-2016.)
|- ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ M e. ( 0 ... N ) ) -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` M ) )
Theorem	dvnres 23694	Multiple derivative version of dvres3a 23678. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm CC ) /\ N e. NN0 ) /\ dom ( ( CC Dn F ) ` N ) = dom F ) -> ( ( S Dn ( F |` S ) ) ` N ) = ( ( ( CC Dn F ) ` N ) |` S ) )
Theorem	cpnfval 23695*	Condition for n-times continuous differentiability. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( S C_ CC -> ( C^n ` S ) = ( n e. NN0 |-> { f e. ( CC ^pm S ) | ( ( S Dn f ) ` n ) e. ( dom f -cn-> CC ) } ) )
Theorem	fncpn 23696	The C^n object is a function. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( S C_ CC -> ( C^n ` S ) Fn NN0 )
Theorem	elcpn 23697	Condition for n-times continuous differentiability. (Contributed by Stefan O'Rear, 15-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ( S C_ CC /\ N e. NN0 ) -> ( F e. ( ( C^n ` S ) ` N ) <-> ( F e. ( CC ^pm S ) /\ ( ( S Dn F ) ` N ) e. ( dom F -cn-> CC ) ) ) )
Theorem	cpnord 23698	C^n conditions are ordered by strength. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
|- ( ( S e. { RR , CC } /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> ( ( C^n ` S ) ` N ) C_ ( ( C^n ` S ) ` M ) )
Theorem	cpncn 23699	A C^n function is continuous. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> F e. ( dom F -cn-> CC ) )
Theorem	cpnres 23700	The restriction of a C^n function is C^n. (Contributed by Mario Carneiro, 11-Feb-2015.)
|- ( ( S e. { RR , CC } /\ F e. ( ( C^n ` CC ) ` N ) ) -> ( F |` S ) e. ( ( C^n ` S ) ` N ) )