P. 374 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37301-37400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	addlimc 37301*	Sum of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. A |-> B )   &    |- G = ( x e. A |-> C )   &    |- H = ( x e. A |-> ( B + C ) )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ( ph /\ x e. A ) -> C e. CC )   &    |- ( ph -> E e. ( F lim CC D ) )   &    |- ( ph -> I e. ( G lim CC D ) )   =>    |- ( ph -> ( E + I ) e. ( H lim CC D ) )
Theorem	0ellimcdiv 37302*	If the numerator converges to 0 and the denominator converges to non zero then the fraction converges to 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. A |-> B )   &    |- G = ( x e. A |-> C )   &    |- H = ( x e. A |-> ( B / C ) )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ( ph /\ x e. A ) -> C e. ( CC \ { 0 } ) )   &    |- ( ph -> 0 e. ( F lim CC E ) )   &    |- ( ph -> D e. ( G lim CC E ) )   &    |- ( ph -> D =/= 0 )   =>    |- ( ph -> 0 e. ( H lim CC E ) )
Theorem	clim2cf 37303*	Express the predicate F converges to A. Similar to clim2 13546, but without the disjoint var constraint F k. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F/_ k F   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ph -> A e. CC )   &    |- ( ( ph /\ k e. Z ) -> B e. CC )   =>    |- ( ph -> ( F ~~> A <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( B - A ) ) < x ) )
Theorem	limclner 37304	For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- K = ( TopOpen ` ℂfld )   &    |- ( ph -> A C_ RR )   &    |- J = ( topGen ` ran (,) )   &    |- ( ph -> F : A --> CC )   &    |- ( 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 lim CC B ) = (/) )
Theorem	sublimc 37305*	Subtraction of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. A |-> B )   &    |- G = ( x e. A |-> C )   &    |- H = ( x e. A |-> ( B - C ) )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ( ph /\ x e. A ) -> C e. CC )   &    |- ( ph -> E e. ( F lim CC D ) )   &    |- ( ph -> I e. ( G lim CC D ) )   =>    |- ( ph -> ( E - I ) e. ( H lim CC D ) )
Theorem	reclimc 37306*	Limit of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. A |-> B )   &    |- G = ( x e. A |-> ( 1 / B ) )   &    |- ( ( ph /\ x e. A ) -> B e. ( CC \ { 0 } ) )   &    |- ( ph -> C e. ( F lim CC D ) )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( 1 / C ) e. ( G lim CC D ) )
Theorem	clim0cf 37307*	Express the predicate F converges to 0. Similar to clim 13536, but without the disjoint var constraint F k. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F/_ k F   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ( ph /\ k e. Z ) -> B e. CC )   =>    |- ( ph -> ( F ~~> 0 <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` B ) < x ) )
Theorem	limclr 37308	For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. In this case, the three limits coincide. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- K = ( TopOpen ` ℂfld )   &    |- ( ph -> A C_ RR )   &    |- J = ( topGen ` ran (,) )   &    |- ( ph -> F : A --> CC )   &    |- ( 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 -> ( ( ( F lim CC B ) =/= (/) <-> L = R ) /\ ( L = R -> L e. ( F lim CC B ) ) ) )
Theorem	divlimc 37309*	Limit of the quotient of two funcions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. A |-> B )   &    |- G = ( x e. A |-> C )   &    |- H = ( x e. A |-> ( B / C ) )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ( ph /\ x e. A ) -> C e. ( CC \ { 0 } ) )   &    |- ( ph -> X e. ( F lim CC D ) )   &    |- ( ph -> Y e. ( G lim CC D ) )   &    |- ( ph -> Y =/= 0 )   &    |- ( ( ph /\ x e. A ) -> C =/= 0 )   =>    |- ( ph -> ( X / Y ) e. ( H lim CC D ) )
Theorem	expfac 37310*	Factorial grows faster than exponential. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )   =>    |- ( A e. CC -> F ~~> 0 )
21.30.8  Trigonometry
Theorem	coseq0 37311	A complex number whose cosine is zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. CC -> ( ( cos ` A ) = 0 <-> ( ( A / pi ) + ( 1 / 2 ) ) e. ZZ ) )
Theorem	sinmulcos 37312	Multiplication formula for sine and cosine. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) x. ( cos ` B ) ) = ( ( ( sin ` ( A + B ) ) + ( sin ` ( A - B ) ) ) / 2 ) )
Theorem	coskpi2 37313	The cosine of an integer multiple of negative pi is either 1 or negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( K e. ZZ -> ( cos ` ( K x. pi ) ) = if ( 2 || K , 1 , -u 1 ) )
Theorem	cosnegpi 37314	The cosine of negative pi is negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( cos ` -u pi ) = -u 1
Theorem	sinaover2ne0 37315	If A in ( 0 , 2 pi ) then sin ( A / 2 ) is not 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. ( 0 (,) ( 2 x. pi ) ) -> ( sin ` ( A / 2 ) ) =/= 0 )
Theorem	cosknegpi 37316	The cosine of an integer multiple of negative pi is either 1 ore negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( K e. ZZ -> ( cos ` ( K x. -u pi ) ) = if ( 2 || K , 1 , -u 1 ) )
21.30.9  Continuous Functions
Theorem	mulcncff 37317	The multiplication 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 ) )   =>    |- ( ph -> ( F oF x. G ) e. ( X -cn-> CC ) )
Theorem	subcncf 37318*	The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) )   =>    |- ( ph -> ( x e. X |-> ( A - B ) ) e. ( X -cn-> CC ) )
Theorem	cncfmptssg 37319*	A continuous complex function restricted to a subset is continuous, using "map to" notation. This theorem generalizes cncfmptss 37237 because it allows to establish a subset for the codomain also. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. A |-> E )   &    |- ( ph -> F e. ( A -cn-> B ) )   &    |- ( ph -> C C_ A )   &    |- ( ph -> D C_ B )   &    |- ( ( ph /\ x e. C ) -> E e. D )   =>    |- ( ph -> ( x e. C |-> E ) e. ( C -cn-> D ) )
Theorem	constcncfg 37320*	A constant function is a continuous function on CC. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A C_ CC )   &    |- ( ph -> B e. C )   &    |- ( ph -> C C_ CC )   =>    |- ( ph -> ( x e. A |-> B ) e. ( A -cn-> C ) )
Theorem	idcncfg 37321*	The identity function is a continuous function on CC. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A C_ B )   &    |- ( ph -> B C_ CC )   =>    |- ( ph -> ( x e. A |-> x ) e. ( A -cn-> B ) )
Theorem	addcncf 37322*	The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) )   =>    |- ( ph -> ( x e. X |-> ( A + B ) ) e. ( X -cn-> CC ) )
Theorem	cncfshift 37323*	A periodic continuous function stays continuous if the domain is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A C_ CC )   &    |- ( ph -> T e. CC )   &    |- B = { x e. CC | E. y e. A x = ( y + T ) }   &    |- ( ph -> F e. ( A -cn-> CC ) )   &    |- G = ( x e. B |-> ( F ` ( x - T ) ) )   =>    |- ( ph -> G e. ( B -cn-> CC ) )
Theorem	resincncf 37324	sin restricted to reals is continuous from reals to reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( sin |` RR ) e. ( RR -cn-> RR )
Theorem	addccncf2 37325*	Adding a constant is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. A |-> ( B + x ) )   =>    |- ( ( A C_ CC /\ B e. CC ) -> F e. ( A -cn-> CC ) )
Theorem	0cnf 37326	The empty set is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- (/) e. ( { (/) } Cn { (/) } )
Theorem	fsumcncf 37327*	The finite sum of continuous complex function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> X C_ CC )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> ( x e. X |-> B ) e. ( X -cn-> CC ) )   =>    |- ( ph -> ( x e. X |-> sum_ k e. A B ) e. ( X -cn-> CC ) )
Theorem	cncfperiod 37328*	A periodic continuous function stays continuous if the domain is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A C_ CC )   &    |- ( ph -> T e. RR )   &    |- B = { x e. CC | E. y e. A x = ( y + T ) }   &    |- ( ph -> F : dom F --> CC )   &    |- ( ph -> B C_ dom F )   &    |- ( ( ph /\ x e. A ) -> ( F ` ( x + T ) ) = ( F ` x ) )   &    |- ( ph -> ( F |` A ) e. ( A -cn-> CC ) )   =>    |- ( ph -> ( F |` B ) e. ( B -cn-> CC ) )
Theorem	subcncff 37329	The subtraction 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 ) )   =>    |- ( ph -> ( F oF - G ) e. ( X -cn-> CC ) )
Theorem	negcncfg 37330*	The opposite of a continuous function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ( x e. A |-> B ) e. ( A -cn-> CC ) )   =>    |- ( ph -> ( x e. A |-> -u B ) e. ( A -cn-> CC ) )
Theorem	cnfdmsn 37331*	A function with a singleton domain is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. V /\ B e. W ) -> ( x e. { A } |-> B ) e. ( ~P { A } Cn ~P { B } ) )
Theorem	cncfcompt 37332*	Composition of continuous functions. A generalization of cncfmpt1f 21841 to arbitrary domains. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ( x e. A |-> B ) e. ( A -cn-> C ) )   &    |- ( ph -> F e. ( C -cn-> D ) )   =>    |- ( ph -> ( x e. A |-> ( F ` B ) ) e. ( A -cn-> D ) )
Theorem	divcncf 37333*	The quotient of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> ( CC \ { 0 } ) ) )   =>    |- ( ph -> ( x e. X |-> ( A / B ) ) e. ( X -cn-> CC ) )
Theorem	addcncff 37334	The addition 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 ) )   =>    |- ( ph -> ( F oF + G ) e. ( X -cn-> CC ) )
Theorem	ioccncflimc 37335	Limit at the upper bound, of a continuous function defined on a left open right closed 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 ` B ) e. ( ( F |` ( A (,) B ) ) lim CC B ) )
Theorem	cncfuni 37336*	A function is continuous if it's domain is the union of sets over which the function is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A C_ CC )   &    |- ( ph -> F : A --> CC )   &    |- ( ph -> A C_ U. B )   &    |- ( ( ph /\ b e. B ) -> ( A i^i b ) e. ( ( TopOpen ` ℂfld ) ↾t A ) )   &    |- ( ( ph /\ b e. B ) -> ( F |` b ) e. ( ( A i^i b ) -cn-> CC ) )   =>    |- ( ph -> F e. ( A -cn-> CC ) )
Theorem	icccncfext 37337*	A continuous function on a closed interval can be extended to a continuous function on the whole real line. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F/_ x F   &    |- J = ( topGen ` ran (,) )   &    |- Y = U. K   &    |- G = ( x e. RR |-> if ( x e. ( A [,] B ) , ( F ` x ) , if ( x < A , ( F ` A ) , ( F ` B ) ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> K e. Top )   &    |- ( ph -> F e. ( ( J ↾t ( A [,] B ) ) Cn K ) )   =>    |- ( ph -> ( G e. ( J Cn ( K ↾t ran F ) ) /\ ( G |` ( A [,] B ) ) = F ) )
Theorem	cncficcgt0 37338*	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 37339	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 37340*	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 37341	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 37342*	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 37343*	A continuous function F on an open interval ( A (,) B ) can be extended to a continuous function G on the corresponding close 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 37344*	A continuous function F on an open interval ( A (,) B ) can be extended to a continuous function G on the corresponding close 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 37345*	A continuous function F on an open interval ( A (,) B ) can be extended to a continuous function G on the corresponding close 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 37346*	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 37347*	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 37348	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 37349*	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 37350*	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 37351*	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 ) )
21.30.10  Derivatives
Theorem	dvsinexp 37352*	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 37353	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	dvrecg 37354*	Derivative of the reciprocal of a function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> S e. { RR , CC } )   &    |- ( ph -> A e. CC )   &    |- ( ( ph /\ x e. X ) -> B e. ( CC \ { 0 } ) )   &    |- ( ( ph /\ x e. X ) -> C e. V )   &    |- ( ph -> ( S _D ( x e. X |-> B ) ) = ( x e. X |-> C ) )   =>    |- ( ph -> ( S _D ( x e. X |-> ( A / B ) ) ) = ( x e. X |-> -u ( ( A x. C ) / ( B ^ 2 ) ) ) )
Theorem	dvsinax 37355*	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 37356	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 37357*	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 37358	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 37359*	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 37360	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	dvmptdiv 37361*	Function-builder for derivative, quotient rule. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( 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 \ { 0 } ) )   &    |- ( ( ph /\ x e. X ) -> D e. CC )   &    |- ( ph -> ( S _D ( x e. X |-> C ) ) = ( x e. X |-> D ) )   =>    |- ( ph -> ( S _D ( x e. X |-> ( A / C ) ) ) = ( x e. X |-> ( ( ( B x. C ) - ( D x. A ) ) / ( C ^ 2 ) ) ) )
Theorem	fperdvper 37362*	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 37363*	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 37364*	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 37365	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 37366	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 37367*	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 37368	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 37369	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 37370*	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 37371	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 37372*	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 37373*	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 37374*	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 37375*	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.)
|- ( 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 = sup ( { 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 37376*	Limit at the lower bound of an open interval, for a function with bounded derivative. (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. 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 37377*	A real function with bounded derivative, has a limit at the upper bound of an open 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 -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )   =>    |- ( ph -> ( F lim CC A ) =/= (/) )
Theorem	ioodvbdlimc2lem 37378*	Limit at the upper bound of an open interval, for a function with bounded derivative. (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. 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 37379*	A real function with bounded derivative, has a limit at the upper bound of an open 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 -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )   =>    |- ( ph -> ( F lim CC B ) =/= (/) )
Theorem	dvdmsscn 37380	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 37381*	Function-builder for derivative, product rule. A version of dvmptmul 22792 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 37382*	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 37383	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 37384*	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 37385*	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 37386*	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 37387*	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 37388*	Induction step for dvmptfprod 37389. (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 37389*	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 37390*	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 37391*	Induction step for dvnprodlem2 37391. (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 37392*	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 37393*	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 ) ) ) )
21.30.11  Integrals
Theorem	volioo 37394	The measure of an open interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol ` ( A (,) B ) ) = ( B - A ) )
Theorem	itgsin0pilem1 37395*	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 37396*	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 37397	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 37398*	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 37399*	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 37400*	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 ) ) ) )