P. 402 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40101-40200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cncficcgt0 40101*	A the absolute value of a continuous function on a closed interval, that is never 0, has a strictly positive lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. ( A [,] B ) |-> C )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> ( RR \ { 0 } ) ) )   =>    |- ( ph -> E. y e. RR+ A. x e. ( A [,] B ) y <_ ( abs ` C ) )
Theorem	icocncflimc 40102	Limit at the lower bound, of a continuous function defined on a left closed right open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A < B )   &    |- ( ph -> F e. ( ( A [,) B ) -cn-> CC ) )   =>    |- ( ph -> ( F ` A ) e. ( ( F |` ( A (,) B ) ) lim CC A ) )
Theorem	cncfdmsn 40103*	A complex function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. CC /\ B e. CC ) -> ( x e. { A } |-> B ) e. ( { A } -cn-> { B } ) )
Theorem	divcncff 40104	The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F e. ( X -cn-> CC ) )   &    |- ( ph -> G e. ( X -cn-> ( CC \ { 0 } ) ) )   =>    |- ( ph -> ( F oF / G ) e. ( X -cn-> CC ) )
Theorem	cncfshiftioo 40105*	A periodic continuous function stays continuous if the domain is an open interval that is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- C = ( A (,) B )   &    |- ( ph -> T e. RR )   &    |- D = ( ( A + T ) (,) ( B + T ) )   &    |- ( ph -> F e. ( C -cn-> CC ) )   &    |- G = ( x e. D |-> ( F ` ( x - T ) ) )   =>    |- ( ph -> G e. ( D -cn-> CC ) )
Theorem	cncfiooicclem1 40106*	A continuous function F on an open interval ( A (,) B ) can be extended to a continuous function G on the corresponding closed interval, if it has a finite right limit R in A and a finite left limit L in B. F can be complex valued. This lemma assumes A < B, the invoking theorem drops this assumption. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F/ x ph   &    |- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )   &    |- ( ph -> L e. ( F lim CC B ) )   &    |- ( ph -> R e. ( F lim CC A ) )   =>    |- ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )
Theorem	cncfiooicc 40107*	A continuous function F on an open interval ( A (,) B ) can be extended to a continuous function G on the corresponding closed interval, if it has a finite right limit R in A and a finite left limit L in B. F can be complex valued. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F/ x ph   &    |- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )   &    |- ( ph -> L e. ( F lim CC B ) )   &    |- ( ph -> R e. ( F lim CC A ) )   =>    |- ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )
Theorem	cncfiooiccre 40108*	A continuous function F on an open interval ( A (,) B ) can be extended to a continuous function G on the corresponding closed interval, if it has a finite right limit R in A and a finite left limit L in B. F is assumed to be real-valued. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F/ x ph   &    |- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F e. ( ( A (,) B ) -cn-> RR ) )   &    |- ( ph -> L e. ( F lim CC B ) )   &    |- ( ph -> R e. ( F lim CC A ) )   =>    |- ( ph -> G e. ( ( A [,] B ) -cn-> RR ) )
Theorem	cncfioobdlem 40109*	G actually extends F. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F : ( A (,) B ) --> V )   &    |- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )   &    |- ( ph -> C e. ( A (,) B ) )   =>    |- ( ph -> ( G ` C ) = ( F ` C ) )
Theorem	cncfioobd 40110*	A continuous function F on an open interval ( A (,) B ) with a finite right limit R in A and a finite left limit L in B is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )   &    |- ( ph -> L e. ( F lim CC B ) )   &    |- ( ph -> R e. ( F lim CC A ) )   =>    |- ( ph -> E. x e. RR A. y e. ( A (,) B ) ( abs ` ( F ` y ) ) <_ x )
Theorem	jumpncnp 40111	Jump discontinuity or discontinuity of the first kind: if the left and the right limit don't match, the function is discontinuous at the point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- K = ( TopOpen ` ℂfld )   &    |- ( ph -> A C_ RR )   &    |- J = ( topGen ` ran (,) )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> B e. RR )   &    |- ( ph -> B e. ( ( limPt ` J ) ` ( A i^i ( -oo (,) B ) ) ) )   &    |- ( ph -> B e. ( ( limPt ` J ) ` ( A i^i ( B (,) +oo ) ) ) )   &    |- ( ph -> L e. ( ( F |` ( -oo (,) B ) ) lim CC B ) )   &    |- ( ph -> R e. ( ( F |` ( B (,) +oo ) ) lim CC B ) )   &    |- ( ph -> L =/= R )   =>    |- ( ph -> -. F e. ( ( J CnP ( TopOpen ` ℂfld ) ) ` B ) )
Theorem	cncfcompt2 40112*	Composition of continuous functions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ x ph   &    |- ( ph -> ( x e. A |-> R ) e. ( A -cn-> B ) )   &    |- ( ph -> ( y e. C |-> S ) e. ( C -cn-> E ) )   &    |- ( ph -> B C_ C )   &    |- ( y = R -> S = T )   =>    |- ( ph -> ( x e. A |-> T ) e. ( A -cn-> E ) )
Theorem	cxpcncf2 40113*	The complex power function is continuous with respect to its second argument. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( A e. ( CC \ ( -oo (,] 0 ) ) -> ( x e. CC |-> ( A ^c x ) ) e. ( CC -cn-> CC ) )
Theorem	fprodcncf 40114*	The finite product of continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> A C_ CC )   &    |- ( ph -> B e. Fin )   &    |- ( ( ph /\ x e. A /\ k e. B ) -> C e. CC )   &    |- ( ( ph /\ k e. B ) -> ( x e. A |-> C ) e. ( A -cn-> CC ) )   =>    |- ( ph -> ( x e. A |-> prod_ k e. B C ) e. ( A -cn-> CC ) )
Theorem	add1cncf 40115*	Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> A e. CC )   &    |- F = ( x e. CC |-> ( x + A ) )   =>    |- ( ph -> F e. ( CC -cn-> CC ) )
Theorem	add2cncf 40116*	Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> A e. CC )   &    |- F = ( x e. CC |-> ( A + x ) )   =>    |- ( ph -> F e. ( CC -cn-> CC ) )
Theorem	sub1cncfd 40117*	Subtracting a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> A e. CC )   &    |- F = ( x e. CC |-> ( x - A ) )   =>    |- ( ph -> F e. ( CC -cn-> CC ) )
Theorem	sub2cncfd 40118*	Subtraction from a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> A e. CC )   &    |- F = ( x e. CC |-> ( A - x ) )   =>    |- ( ph -> F e. ( CC -cn-> CC ) )
Theorem	fprodsub2cncf 40119*	F is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- F = ( x e. CC |-> prod_ k e. A ( B - x ) )   =>    |- ( ph -> F e. ( CC -cn-> CC ) )
Theorem	fprodadd2cncf 40120*	F is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- F = ( x e. CC |-> prod_ k e. A ( B + x ) )   =>    |- ( ph -> F e. ( CC -cn-> CC ) )
Theorem	fprodsubrecnncnvlem 40121*	The sequence S of finite products, where every factor is subtracted an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- S = ( n e. NN |-> prod_ k e. A ( B - ( 1 / n ) ) )   &    |- F = ( x e. CC |-> prod_ k e. A ( B - x ) )   &    |- G = ( n e. NN |-> ( 1 / n ) )   =>    |- ( ph -> S ~~> prod_ k e. A B )
Theorem	fprodsubrecnncnv 40122*	The sequence S of finite products, where every factor is subtracted an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- F/ k ph   &    |- ( ph -> X e. Fin )   &    |- ( ( ph /\ k e. X ) -> A e. CC )   &    |- S = ( n e. NN |-> prod_ k e. X ( A - ( 1 / n ) ) )   =>    |- ( ph -> S ~~> prod_ k e. X A )
Theorem	fprodaddrecnncnvlem 40123*	The sequence S of finite products, where every factor is added an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- S = ( n e. NN |-> prod_ k e. A ( B + ( 1 / n ) ) )   &    |- F = ( x e. CC |-> prod_ k e. A ( B + x ) )   &    |- G = ( n e. NN |-> ( 1 / n ) )   =>    |- ( ph -> S ~~> prod_ k e. A B )
Theorem	fprodaddrecnncnv 40124*	The sequence S of finite products, where every factor is added an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- F/ k ph   &    |- ( ph -> X e. Fin )   &    |- ( ( ph /\ k e. X ) -> A e. CC )   &    |- S = ( n e. NN |-> prod_ k e. X ( A + ( 1 / n ) ) )   =>    |- ( ph -> S ~~> prod_ k e. X A )
20.32.10  Derivatives
Theorem	dvsinexp 40125*	The derivative of sin^N . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- ( ph -> N e. NN )   =>    |- ( ph -> ( CC _D ( x e. CC |-> ( ( sin ` x ) ^ N ) ) ) = ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) )
Theorem	dvcosre 40126	The real derivative of the cosine. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- ( RR _D ( x e. RR |-> ( cos ` x ) ) ) = ( x e. RR |-> -u ( sin ` x ) )
Theorem	dvsinax 40127*	Derivative exercise: the derivative with respect to y of sin(Ay), given a constant A. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. CC -> ( CC _D ( y e. CC |-> ( sin ` ( A x. y ) ) ) ) = ( y e. CC |-> ( A x. ( cos ` ( A x. y ) ) ) ) )
Theorem	dvsubf 40128	The subtraction rule for everywhere-differentiable functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> G : X --> CC )   &    |- ( ph -> dom ( S _D F ) = X )   &    |- ( ph -> dom ( S _D G ) = X )   =>    |- ( ph -> ( S _D ( F oF - G ) ) = ( ( S _D F ) oF - ( S _D G ) ) )
Theorem	dvmptconst 40129*	Function-builder for derivative: derivative of a constant. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> A e. ( ( TopOpen ` ℂfld ) ↾t S ) )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( S _D ( x e. A |-> B ) ) = ( x e. A |-> 0 ) )
Theorem	dvcnre 40130	From compex differentiation to real differentiation. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( F : CC --> CC /\ RR C_ dom ( CC _D F ) ) -> ( RR _D ( F |` RR ) ) = ( ( CC _D F ) |` RR ) )
Theorem	dvmptidg 40131*	Function-builder for derivative: derivative of the identity. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> A e. ( ( TopOpen ` ℂfld ) ↾t S ) )   =>    |- ( ph -> ( S _D ( x e. A |-> x ) ) = ( x e. A |-> 1 ) )
Theorem	dvresntr 40132	Function-builder for derivative: expand the function from an open set to its closure. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> S C_ CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> F : X --> CC )   &    |- J = ( K ↾t S )   &    |- K = ( TopOpen ` ℂfld )   &    |- ( ph -> ( ( int ` J ) ` X ) = Y )   =>    |- ( ph -> ( S _D F ) = ( S _D ( F |` Y ) ) )
Theorem	fperdvper 40133*	The derivative of a periodic function is periodic. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> CC )   &    |- ( ph -> T e. RR )   &    |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )   &    |- G = ( RR _D F )   =>    |- ( ( ph /\ x e. dom G ) -> ( ( x + T ) e. dom G /\ ( G ` ( x + T ) ) = ( G ` x ) ) )
Theorem	dvmptresicc 40134*	Derivative of a function restricted to a closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. CC |-> A )   &    |- ( ( ph /\ x e. CC ) -> A e. CC )   &    |- ( ph -> ( CC _D F ) = ( x e. CC |-> B ) )   &    |- ( ( ph /\ x e. CC ) -> B e. CC )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   =>    |- ( ph -> ( RR _D ( x e. ( C [,] D ) |-> A ) ) = ( x e. ( C (,) D ) |-> B ) )
Theorem	dvasinbx 40135*	Derivative exercise: the derivative with respect to y of A x sin(By), given two constants A and B. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. CC /\ B e. CC ) -> ( CC _D ( y e. CC |-> ( A x. ( sin ` ( B x. y ) ) ) ) ) = ( y e. CC |-> ( ( A x. B ) x. ( cos ` ( B x. y ) ) ) ) )
Theorem	dvresioo 40136	Restriction of a derivative to an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A C_ RR /\ F : A --> CC ) -> ( RR _D ( F |` ( B (,) C ) ) ) = ( ( RR _D F ) |` ( B (,) C ) ) )
Theorem	dvdivf 40137	The quotient rule for everywhere-differentiable functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> G : X --> ( CC \ { 0 } ) )   &    |- ( ph -> dom ( S _D F ) = X )   &    |- ( ph -> dom ( S _D G ) = X )   =>    |- ( ph -> ( S _D ( F oF / G ) ) = ( ( ( ( S _D F ) oF x. G ) oF - ( ( S _D G ) oF x. F ) ) oF / ( G oF x. G ) ) )
Theorem	dvdivbd 40138*	A sufficient condition for the derivative to be bounded, for the quotient of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ( ph /\ x e. X ) -> A e. CC )   &    |- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> C ) )   &    |- ( ( ph /\ x e. X ) -> C e. CC )   &    |- ( ( ph /\ x e. X ) -> B e. CC )   &    |- ( ph -> U e. RR )   &    |- ( ph -> R e. RR )   &    |- ( ph -> T e. RR )   &    |- ( ph -> Q e. RR )   &    |- ( ( ph /\ x e. X ) -> ( abs ` C ) <_ U )   &    |- ( ( ph /\ x e. X ) -> ( abs ` B ) <_ R )   &    |- ( ( ph /\ x e. X ) -> ( abs ` D ) <_ T )   &    |- ( ( ph /\ x e. X ) -> ( abs ` A ) <_ Q )   &    |- ( ph -> ( S _D ( x e. X |-> B ) ) = ( x e. X |-> D ) )   &    |- ( ( ph /\ x e. X ) -> D e. CC )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> A. x e. X E <_ ( abs ` B ) )   &    |- F = ( S _D ( x e. X |-> ( A / B ) ) )   =>    |- ( ph -> E. b e. RR A. x e. X ( abs ` ( F ` x ) ) <_ b )
Theorem	dvsubcncf 40139	A sufficient condition for the derivative of a product to be continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> G : X --> CC )   &    |- ( ph -> ( S _D F ) e. ( X -cn-> CC ) )   &    |- ( ph -> ( S _D G ) e. ( X -cn-> CC ) )   =>    |- ( ph -> ( S _D ( F oF - G ) ) e. ( X -cn-> CC ) )
Theorem	dvmulcncf 40140	A sufficient condition for the derivative of a product to be continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> G : X --> CC )   &    |- ( ph -> ( S _D F ) e. ( X -cn-> CC ) )   &    |- ( ph -> ( S _D G ) e. ( X -cn-> CC ) )   =>    |- ( ph -> ( S _D ( F oF x. G ) ) e. ( X -cn-> CC ) )
Theorem	dvcosax 40141*	Derivative exercise: the derivative with respect to x of cos(Ax), given a constant A. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. CC -> ( CC _D ( x e. CC |-> ( cos ` ( A x. x ) ) ) ) = ( x e. CC |-> ( A x. -u ( sin ` ( A x. x ) ) ) ) )
Theorem	dvdivcncf 40142	A sufficient condition for the derivative of a quotient to be continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> G : X --> ( CC \ { 0 } ) )   &    |- ( ph -> ( S _D F ) e. ( X -cn-> CC ) )   &    |- ( ph -> ( S _D G ) e. ( X -cn-> CC ) )   =>    |- ( ph -> ( S _D ( F oF / G ) ) e. ( X -cn-> CC ) )
Theorem	dvbdfbdioolem1 40143*	Given a function with bounded derivative, on an open interval, here is an absolute bound to the difference of the image of two points in the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F : ( A (,) B ) --> RR )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> K e. RR )   &    |- ( ph -> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ K )   &    |- ( ph -> C e. ( A (,) B ) )   &    |- ( ph -> D e. ( C (,) B ) )   =>    |- ( ph -> ( ( abs ` ( ( F ` D ) - ( F ` C ) ) ) <_ ( K x. ( D - C ) ) /\ ( abs ` ( ( F ` D ) - ( F ` C ) ) ) <_ ( K x. ( B - A ) ) ) )
Theorem	dvbdfbdioolem2 40144*	A function on an open interval, with bounded derivative, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F : ( A (,) B ) --> RR )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> K e. RR )   &    |- ( ph -> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ K )   &    |- M = ( ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) + ( K x. ( B - A ) ) )   =>    |- ( ph -> A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ M )
Theorem	dvbdfbdioo 40145*	A function on an open interval, with bounded derivative, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F : ( A (,) B ) --> RR )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> E. a e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ a )   =>    |- ( ph -> E. b e. RR A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b )
Theorem	ioodvbdlimc1lem1 40146*	If F has bounded derivative on ( A (,) B ) then a sequence of points in its image converges to its limsup. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 3-Oct-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F e. ( ( A (,) B ) -cn-> RR ) )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> R : ( ZZ>= ` M ) --> ( A (,) B ) )   &    |- S = ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) )   &    |- ( ph -> R e. dom ~~> )   &    |- K = inf ( { k e. ( ZZ>= ` M ) | A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } , RR , < )   =>    |- ( ph -> S ~~> ( limsup ` S ) )
Theorem	ioodvbdlimc1lem2 40147*	Limit at the lower bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 3-Oct-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F : ( A (,) B ) --> RR )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )   &    |- Y = sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < )   &    |- M = ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 )   &    |- S = ( j e. ( ZZ>= ` M ) |-> ( F ` ( A + ( 1 / j ) ) ) )   &    |- R = ( j e. ( ZZ>= ` M ) |-> ( A + ( 1 / j ) ) )   &    |- N = if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M )   &    |- ( ch <-> ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) )   =>    |- ( ph -> ( limsup ` S ) e. ( F lim CC A ) )
Theorem	ioodvbdlimc1 40148*	A real function with bounded derivative, has a limit at the upper bound of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by AV, 3-Oct-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F : ( A (,) B ) --> RR )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )   =>    |- ( ph -> ( F lim CC A ) =/= (/) )
Theorem	ioodvbdlimc2lem 40149*	Limit at the upper bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 3-Oct-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> F : ( A (,) B ) --> RR )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )   &    |- Y = sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < )   &    |- M = ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 )   &    |- S = ( j e. ( ZZ>= ` M ) |-> ( F ` ( B - ( 1 / j ) ) ) )   &    |- R = ( j e. ( ZZ>= ` M ) |-> ( B - ( 1 / j ) ) )   &    |- N = if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M )   &    |- ( ch <-> ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - B ) ) < ( 1 / j ) ) )   =>    |- ( ph -> ( limsup ` S ) e. ( F lim CC B ) )
Theorem	ioodvbdlimc2 40150*	A real function with bounded derivative, has a limit at the upper bound of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by AV, 3-Oct-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F : ( A (,) B ) --> RR )   &    |- ( ph -> dom ( RR _D F ) = ( A (,) B ) )   &    |- ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )   =>    |- ( ph -> ( F lim CC B ) =/= (/) )
Theorem	dvdmsscn 40151	X is a subset of CC. This statement is very often used when computing derivatives. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )   =>    |- ( ph -> X C_ CC )
Theorem	dvmptmulf 40152*	Function-builder for derivative, product rule. A version of dvmptmul 23724 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ x ph   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ( ph /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ x e. X ) -> B e. V )   &    |- ( ph -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )   &    |- ( ( ph /\ x e. X ) -> C e. CC )   &    |- ( ( ph /\ x e. X ) -> D e. W )   &    |- ( ph -> ( S _D ( x e. X |-> C ) ) = ( x e. X |-> D ) )   =>    |- ( ph -> ( S _D ( x e. X |-> ( A x. C ) ) ) = ( x e. X |-> ( ( B x. C ) + ( D x. A ) ) ) )
Theorem	dvnmptdivc 40153*	Function-builder for iterated derivative, division rule for constant divisor. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> X C_ S )   &    |- ( ( ph /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ x e. X /\ n e. ( 0 ... M ) ) -> B e. CC )   &    |- ( ( ph /\ n e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> A ) ) ` n ) = ( x e. X |-> B ) )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C =/= 0 )   &    |- ( ph -> M e. NN0 )   =>    |- ( ( ph /\ n e. ( 0 ... M ) ) -> ( ( S Dn ( x e. X |-> ( A / C ) ) ) ` n ) = ( x e. X |-> ( B / C ) ) )
Theorem	dvdsn1add 40154	If K divides N but K does not divide M, then K does not divide ( M + N ). (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( -. K || M /\ K || N ) -> -. K || ( M + N ) ) )
Theorem	dvxpaek 40155*	Derivative of the polynomial ( x + A ) ^ K. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )   &    |- ( ph -> A e. CC )   &    |- ( ph -> K e. NN )   =>    |- ( ph -> ( S _D ( x e. X |-> ( ( x + A ) ^ K ) ) ) = ( x e. X |-> ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) ) )
Theorem	dvnmptconst 40156*	The N-th derivative of a constant function. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )   &    |- ( ph -> A e. CC )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> ( ( S Dn ( x e. X |-> A ) ) ` N ) = ( x e. X |-> 0 ) )
Theorem	dvnxpaek 40157*	The n-th derivative of the polynomial (x+A)^K. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )   &    |- ( ph -> A e. CC )   &    |- ( ph -> K e. NN0 )   &    |- F = ( x e. X |-> ( ( x + A ) ^ K ) )   =>    |- ( ( ph /\ N e. NN0 ) -> ( ( S Dn F ) ` N ) = ( x e. X |-> if ( K < N , 0 , ( ( ( ! ` K ) / ( ! ` ( K - N ) ) ) x. ( ( x + A ) ^ ( K - N ) ) ) ) ) )
Theorem	dvnmul 40158*	Function-builder for the N-th derivative, product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )   &    |- ( ( ph /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ x e. X ) -> B e. CC )   &    |- ( ph -> N e. NN0 )   &    |- F = ( x e. X |-> A )   &    |- G = ( x e. X |-> B )   &    |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn F ) ` k ) : X --> CC )   &    |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn G ) ` k ) : X --> CC )   &    |- C = ( k e. ( 0 ... N ) |-> ( ( S Dn F ) ` k ) )   &    |- D = ( k e. ( 0 ... N ) |-> ( ( S Dn G ) ` k ) )   =>    |- ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) = ( x e. X |-> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) ) )
Theorem	dvmptfprodlem 40159*	Induction step for dvmptfprod 40160. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ x ph   &    |- F/ i ph   &    |- F/ j ph   &    |- F/_ i F   &    |- F/_ j G   &    |- ( ( ph /\ i e. I /\ x e. X ) -> A e. CC )   &    |- ( ph -> D e. Fin )   &    |- ( ph -> E e. _V )   &    |- ( ph -> -. E e. D )   &    |- ( ph -> ( D u. { E } ) C_ I )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ( ( ph /\ x e. X ) /\ j e. D ) -> C e. CC )   &    |- ( ph -> ( S _D ( x e. X |-> prod_ i e. D A ) ) = ( x e. X |-> sum_ j e. D ( C x. prod_ i e. ( D \ { j } ) A ) ) )   &    |- ( ( ph /\ x e. X ) -> G e. CC )   &    |- ( ph -> ( S _D ( x e. X |-> F ) ) = ( x e. X |-> G ) )   &    |- ( i = E -> A = F )   &    |- ( j = E -> C = G )   =>    |- ( ph -> ( S _D ( x e. X |-> prod_ i e. ( D u. { E } ) A ) ) = ( x e. X |-> sum_ j e. ( D u. { E } ) ( C x. prod_ i e. ( ( D u. { E } ) \ { j } ) A ) ) )
Theorem	dvmptfprod 40160*	Function-builder for derivative, finite product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F/ i ph   &    |- F/ j ph   &    |- J = ( K ↾t S )   &    |- K = ( TopOpen ` ℂfld )   &    |- ( ph -> S e. { RR , CC } )   &    |- ( ph -> X e. J )   &    |- ( ph -> I e. Fin )   &    |- ( ( ph /\ i e. I /\ x e. X ) -> A e. CC )   &    |- ( ( ph /\ i e. I /\ x e. X ) -> B e. CC )   &    |- ( ( ph /\ i e. I ) -> ( S _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )   &    |- ( i = j -> B = C )   =>    |- ( ph -> ( S _D ( x e. X |-> prod_ i e. I A ) ) = ( x e. X |-> sum_ j e. I ( C x. prod_ i e. ( I \ { j } ) A ) ) )
Theorem	dvnprodlem1 40161*	D is bijective. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- C = ( s e. ~P T |-> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) )   &    |- ( ph -> J e. NN0 )   &    |- D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. )   &    |- ( ph -> T e. Fin )   &    |- ( ph -> Z e. T )   &    |- ( ph -> -. Z e. R )   &    |- ( ph -> ( R u. { Z } ) C_ T )   =>    |- ( ph -> D : ( ( C ` ( R u. { Z } ) ) ` J ) -1-1-onto-> U_ k e. ( 0 ... J ) ( { k } X. ( ( C ` R ) ` k ) ) )
Theorem	dvnprodlem2 40162*	Induction step for dvnprodlem2 40162. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )   &    |- ( ph -> T e. Fin )   &    |- ( ( ph /\ t e. T ) -> ( H ` t ) : X --> CC )   &    |- ( ph -> N e. NN0 )   &    |- ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` j ) : X --> CC )   &    |- C = ( s e. ~P T |-> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) )   &    |- ( ph -> R C_ T )   &    |- ( ph -> Z e. ( T \ R ) )   &    |- ( ph -> A. k e. ( 0 ... N ) ( ( S Dn ( x e. X |-> prod_ t e. R ( ( H ` t ) ` x ) ) ) ` k ) = ( x e. X |-> sum_ c e. ( ( C ` R ) ` k ) ( ( ( ! ` k ) / prod_ t e. R ( ! ` ( c ` t ) ) ) x. prod_ t e. R ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )   &    |- ( ph -> J e. ( 0 ... N ) )   &    |- D = ( c e. ( ( C ` ( R u. { Z } ) ) ` J ) |-> <. ( J - ( c ` Z ) ) , ( c |` R ) >. )   =>    |- ( ph -> ( ( S Dn ( x e. X |-> prod_ t e. ( R u. { Z } ) ( ( H ` t ) ` x ) ) ) ` J ) = ( x e. X |-> sum_ c e. ( ( C ` ( R u. { Z } ) ) ` J ) ( ( ( ! ` J ) / prod_ t e. ( R u. { Z } ) ( ! ` ( c ` t ) ) ) x. prod_ t e. ( R u. { Z } ) ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
Theorem	dvnprodlem3 40163*	The multinomial formula for the k-th derivative of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )   &    |- ( ph -> T e. Fin )   &    |- ( ( ph /\ t e. T ) -> ( H ` t ) : X --> CC )   &    |- ( ph -> N e. NN0 )   &    |- ( ( ph /\ t e. T /\ j e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` j ) : X --> CC )   &    |- F = ( x e. X |-> prod_ t e. T ( ( H ` t ) ` x ) )   &    |- D = ( s e. ~P T |-> ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m s ) | sum_ t e. s ( c ` t ) = n } ) )   &    |- C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m T ) | sum_ t e. T ( c ` t ) = n } )   =>    |- ( ph -> ( ( S Dn F ) ` N ) = ( x e. X |-> sum_ c e. ( C ` N ) ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( c ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
Theorem	dvnprod 40164*	The multinomial formula for the N-th derivative of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )   &    |- ( ph -> T e. Fin )   &    |- ( ( ph /\ t e. T ) -> ( H ` t ) : X --> CC )   &    |- ( ph -> N e. NN0 )   &    |- ( ( ph /\ t e. T /\ k e. ( 0 ... N ) ) -> ( ( S Dn ( H ` t ) ) ` k ) : X --> CC )   &    |- F = ( x e. X |-> prod_ t e. T ( ( H ` t ) ` x ) )   &    |- C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m T ) | sum_ t e. T ( c ` t ) = n } )   =>    |- ( ph -> ( ( S Dn F ) ` N ) = ( x e. X |-> sum_ c e. ( C ` N ) ( ( ( ! ` N ) / prod_ t e. T ( ! ` ( c ` t ) ) ) x. prod_ t e. T ( ( ( S Dn ( H ` t ) ) ` ( c ` t ) ) ` x ) ) ) )
20.32.11  Integrals
Theorem	itgsin0pilem1 40165*	Calculation of the integral for sine on the (0,π) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- C = ( t e. ( 0 [,] pi ) |-> -u ( cos ` t ) )   =>    |- S. ( 0 (,) pi ) ( sin ` x ) _d x = 2
Theorem	ibliccsinexp 40166*	sin^n on a closed interval is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- ( ( A e. RR /\ B e. RR /\ N e. NN0 ) -> ( x e. ( A [,] B ) |-> ( ( sin ` x ) ^ N ) ) e. L^1 )
Theorem	itgsin0pi 40167	Calculation of the integral for sine on the (0,π) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- S. ( 0 (,) pi ) ( sin ` x ) _d x = 2
Theorem	iblioosinexp 40168*	sin^n on an open integral is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- ( ( A e. RR /\ B e. RR /\ N e. NN0 ) -> ( x e. ( A (,) B ) |-> ( ( sin ` x ) ^ N ) ) e. L^1 )
Theorem	itgsinexplem1 40169*	Integration by parts is applied to integrate sin^(N+1). (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- F = ( x e. CC |-> ( ( sin ` x ) ^ N ) )   &    |- G = ( x e. CC |-> -u ( cos ` x ) )   &    |- H = ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) )   &    |- I = ( x e. CC |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) )   &    |- L = ( x e. CC |-> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) )   &    |- M = ( x e. CC |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> S. ( 0 (,) pi ) ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) _d x = ( N x. S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x ) )
Theorem	itgsinexp 40170*	A recursive formula for the integral of sin^N on the interval (0,π) . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- I = ( n e. NN0 |-> S. ( 0 (,) pi ) ( ( sin ` x ) ^ n ) _d x )   &    |- ( ph -> N e. ( ZZ>= ` 2 ) )   =>    |- ( ph -> ( I ` N ) = ( ( ( N - 1 ) / N ) x. ( I ` ( N - 2 ) ) ) )
Theorem	iblconstmpt 40171*	A constant function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( x e. A |-> B ) e. L^1 )
Theorem	itgeq1d 40172*	Equality theorem for an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A = B )   =>    |- ( ph -> S. A C _d x = S. B C _d x )
Theorem	mbf0 40173	The empty set is a measurable function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- (/) e. MblFn
Theorem	mbfres2cn 40174	Measurability of a piecewise function: if F is measurable on subsets B and C of its domain, and these pieces make up all of A, then F is measurable on the whole domain. Similar to mbfres2 23412 but here the theorem is extended to complex valued functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> ( F |` B ) e. MblFn )   &    |- ( ph -> ( F |` C ) e. MblFn )   &    |- ( ph -> ( B u. C ) = A )   =>    |- ( ph -> F e. MblFn )
Theorem	vol0 40175	The measure of the empty set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( vol ` (/) ) = 0
Theorem	ditgeqiooicc 40176*	A function F on an open interval, has the same directed integral as its extension G on the closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> F : ( A (,) B ) --> RR )   =>    |- ( ph -> S__ [ A -> B ] ( F ` x ) _d x = S__ [ A -> B ] ( G ` x ) _d x )
Theorem	volge0 40177	The volume of a set is always nonnegative. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. dom vol -> 0 <_ ( vol ` A ) )
Theorem	cnbdibl 40178*	A continuous bounded function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. dom vol )   &    |- ( ph -> ( vol ` A ) e. RR )   &    |- ( ph -> F e. ( A -cn-> CC ) )   &    |- ( ph -> E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x )   =>    |- ( ph -> F e. L^1 )
Theorem	snmbl 40179	A singleton is measurable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. RR -> { A } e. dom vol )
Theorem	ditgeq3d 40180*	Equality theorem for the directed integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A <_ B )   &    |- ( ( ph /\ x e. ( A (,) B ) ) -> D = E )   =>    |- ( ph -> S__ [ A -> B ] D _d x = S__ [ A -> B ] E _d x )
Theorem	iblempty 40181	The empty function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- (/) e. L^1
Theorem	iblsplit 40182*	The union of two integrable functions is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ( vol* ` ( A i^i B ) ) = 0 )   &    |- ( ph -> U = ( A u. B ) )   &    |- ( ( ph /\ x e. U ) -> C e. CC )   &    |- ( ph -> ( x e. A |-> C ) e. L^1 )   &    |- ( ph -> ( x e. B |-> C ) e. L^1 )   =>    |- ( ph -> ( x e. U |-> C ) e. L^1 )
Theorem	volsn 40183	A singleton has 0 Lebesgue measure. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. RR -> ( vol ` { A } ) = 0 )
Theorem	itgvol0 40184*	If the domani is negligible, the function is integrable and the integral is 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A C_ RR )   &    |- ( ph -> ( vol* ` A ) = 0 )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   =>    |- ( ph -> ( ( x e. A |-> B ) e. L^1 /\ S. A B _d x = 0 ) )
Theorem	itgcoscmulx 40185*	Exercise: the integral of x |-> cos a x on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> B <_ C )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> S. ( B (,) C ) ( cos ` ( A x. x ) ) _d x = ( ( ( sin ` ( A x. C ) ) - ( sin ` ( A x. B ) ) ) / A ) )
Theorem	iblsplitf 40186*	A version of iblsplit 40182 using bound-variable hypotheses instead of distinct variable conditions" (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F/ x ph   &    |- ( ph -> ( vol* ` ( A i^i B ) ) = 0 )   &    |- ( ph -> U = ( A u. B ) )   &    |- ( ( ph /\ x e. U ) -> C e. CC )   &    |- ( ph -> ( x e. A |-> C ) e. L^1 )   &    |- ( ph -> ( x e. B |-> C ) e. L^1 )   =>    |- ( ph -> ( x e. U |-> C ) e. L^1 )
Theorem	ibliooicc 40187*	If a function is integrable on an open interval, it is integrable on the corresponding closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( x e. ( A (,) B ) |-> C ) e. L^1 )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> C e. CC )   =>    |- ( ph -> ( x e. ( A [,] B ) |-> C ) e. L^1 )
Theorem	volioc 40188	The measure of left open, right closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol ` ( A (,] B ) ) = ( B - A ) )
Theorem	iblspltprt 40189*	If a function is integrable on any interval of a partition, then it is integrable on the whole interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F/ t ph   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )   &    |- ( ( ph /\ i e. ( M ... N ) ) -> ( P ` i ) e. RR )   &    |- ( ( ph /\ i e. ( M..^ N ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) )   &    |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` N ) ) ) -> A e. CC )   &    |- ( ( ph /\ i e. ( M..^ N ) ) -> ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) |-> A ) e. L^1 )   =>    |- ( ph -> ( t e. ( ( P ` M ) [,] ( P ` N ) ) |-> A ) e. L^1 )
Theorem	itgsincmulx 40190*	Exercise: the integral of x |-> sin a x on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> B <_ C )   =>    |- ( ph -> S. ( B (,) C ) ( sin ` ( A x. x ) ) _d x = ( ( ( cos ` ( A x. B ) ) - ( cos ` ( A x. C ) ) ) / A ) )
Theorem	itgsubsticclem 40191*	lemma for itgsubsticc 40192. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( u e. ( K [,] L ) |-> C )   &    |- G = ( u e. RR |-> if ( u e. ( K [,] L ) , ( F ` u ) , if ( u < K , ( F ` K ) , ( F ` L ) ) ) )   &    |- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> X <_ Y )   &    |- ( ph -> ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> ( K [,] L ) ) )   &    |- ( ph -> ( x e. ( X (,) Y ) |-> B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) )   &    |- ( ph -> F e. ( ( K [,] L ) -cn-> CC ) )   &    |- ( ph -> K e. RR )   &    |- ( ph -> L e. RR )   &    |- ( ph -> K <_ L )   &    |- ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> A ) ) = ( x e. ( X (,) Y ) |-> B ) )   &    |- ( u = A -> C = E )   &    |- ( x = X -> A = K )   &    |- ( x = Y -> A = L )   =>    |- ( ph -> S__ [ K -> L ] C _d u = S__ [ X -> Y ] ( E x. B ) _d x )
Theorem	itgsubsticc 40192*	Integration by u-substitution. The main difference with respect to itgsubst 23812 is that here we consider the range of A ( x ) to be in the closed interval ( K [,] L ). If A ( x ) is a continuous, differentiable function from [ X , Y ] to ( Z , W ), whose derivative is continuous and integrable, and C ( u ) is a continuous function on ( Z , W ), then the integral of C ( u ) from K = A ( X ) to L = A ( Y ) is equal to the integral of C ( A ( x ) ) _D A ( x ) from X to Y. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> X <_ Y )   &    |- ( ph -> ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> ( K [,] L ) ) )   &    |- ( ph -> ( u e. ( K [,] L ) |-> C ) e. ( ( K [,] L ) -cn-> CC ) )   &    |- ( ph -> ( x e. ( X (,) Y ) |-> B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) )   &    |- ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> A ) ) = ( x e. ( X (,) Y ) |-> B ) )   &    |- ( u = A -> C = E )   &    |- ( x = X -> A = K )   &    |- ( x = Y -> A = L )   &    |- ( ph -> K e. RR )   &    |- ( ph -> L e. RR )   =>    |- ( ph -> S__ [ K -> L ] C _d u = S__ [ X -> Y ] ( E x. B ) _d x )
Theorem	itgioocnicc 40193*	The integral of a piecewise continuous function F on an open interval is equal to the integral of the continuous function G, in the corresponding closed interval. G is equal to F on the open interval, but it is continuous at the two boundaries, also. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F : dom F --> CC )   &    |- ( ph -> ( F |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )   &    |- ( ph -> ( A [,] B ) C_ dom F )   &    |- ( ph -> R e. ( ( F |` ( A (,) B ) ) lim CC A ) )   &    |- ( ph -> L e. ( ( F |` ( A (,) B ) ) lim CC B ) )   &    |- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )   =>    |- ( ph -> ( G e. L^1 /\ S. ( A [,] B ) ( G ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x ) )
Theorem	iblcncfioo 40194	A continuous function F on an open interval ( A (,) B ) with a finite right limit R in A and a finite left limit L in B is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )   &    |- ( ph -> L e. ( F lim CC B ) )   &    |- ( ph -> R e. ( F lim CC A ) )   =>    |- ( ph -> F e. L^1 )
Theorem	itgspltprt 40195*	The S. integral splits on a given partition P. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )   &    |- ( ph -> P : ( M ... N ) --> RR )   &    |- ( ( ph /\ i e. ( M..^ N ) ) -> ( P ` i ) < ( P ` ( i + 1 ) ) )   &    |- ( ( ph /\ t e. ( ( P ` M ) [,] ( P ` N ) ) ) -> A e. CC )   &    |- ( ( ph /\ i e. ( M..^ N ) ) -> ( t e. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) |-> A ) e. L^1 )   =>    |- ( ph -> S. ( ( P ` M ) [,] ( P ` N ) ) A _d t = sum_ i e. ( M..^ N ) S. ( ( P ` i ) [,] ( P ` ( i + 1 ) ) ) A _d t )
Theorem	itgiccshift 40196*	The integral of a function, F stays the same if its closed interval domain is shifted by T. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )   &    |- ( ph -> T e. RR+ )   &    |- G = ( x e. ( ( A + T ) [,] ( B + T ) ) |-> ( F ` ( x - T ) ) )   =>    |- ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( G ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
Theorem	itgperiod 40197*	The integral of a periodic function, with period T stays the same if the domain of integration is shifted. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> T e. RR+ )   &    |- ( ph -> F : RR --> CC )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )   &    |- ( ph -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )   =>    |- ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
Theorem	itgsbtaddcnst 40198*	Integral substitution, adding a constant to the function's argument. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> X e. RR )   &    |- ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )   =>    |- ( ph -> S__ [ ( A - X ) -> ( B - X ) ] ( F ` ( X + s ) ) _d s = S__ [ A -> B ] ( F ` t ) _d t )
Theorem	itgeq2d 40199*	Equality theorem for an integral. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> S. A B _d x = S. A C _d x )
Theorem	volico 40200	The measure of left closed, right open interval. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) = if ( A < B , ( B - A ) , 0 ) )