P. 377 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37601-37700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	limcresioolb 37601	The right limit doesn't change if the function is restricted to a smaller open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> B < C )   &    |- ( ph -> ( B (,) C ) C_ A )   &    |- ( ph -> D e. RR* )   &    |- ( ph -> C <_ D )   =>    |- ( ph -> ( ( F |` ( B (,) C ) ) lim CC B ) = ( ( F |` ( B (,) D ) ) lim CC B ) )
Theorem	limcleqr 37602	If the left and the right limits are equal, the limit of the function exits and 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. RR )   &    |- ( ph -> L e. ( ( F |` ( -oo (,) B ) ) lim CC B ) )   &    |- ( ph -> R e. ( ( F |` ( B (,) +oo ) ) lim CC B ) )   &    |- ( ph -> L = R )   =>    |- ( ph -> L e. ( F lim CC B ) )
Theorem	lptioo2cn 37603	The upper bound of an open interval is a limit point of the interval, wirth respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- J = ( TopOpen ` ℂfld )   &    |- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> B e. ( ( limPt ` J ) ` ( A (,) B ) ) )
Theorem	lptioo1cn 37604	The lower bound of an open interval is a limit point of the interval, wirth respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- J = ( TopOpen ` ℂfld )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> A e. ( ( limPt ` J ) ` ( A (,) B ) ) )
Theorem	neglimc 37605*	Limit of the negative function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- F = ( x e. A |-> B )   &    |- G = ( x e. A |-> -u B )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ph -> C e. ( F lim CC D ) )   =>    |- ( ph -> -u C e. ( G lim CC D ) )
Theorem	addlimc 37606*	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 37607*	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 37608*	Express the predicate F converges to A. Similar to clim2 13504, 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 37609	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 37610*	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 37611*	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 37612*	Express the predicate F converges to 0. Similar to clim 13494, 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 37613	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 37614*	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 37615*	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 37616	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 37617	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 37618	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 37619	The cosine of negative pi is negative 1. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( cos ` -u pi ) = -u 1
Theorem	sinaover2ne0 37620	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 37621	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 37622	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 37623*	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 37624*	A continuous complex function restricted to a subset is continuous, using "map to" notation. This theorem generalizes cncfmptss 37542 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 37625*	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 37626*	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 37627*	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 37628*	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 37629	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 37630*	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 37631	The empty set is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- (/) e. ( { (/) } Cn { (/) } )
Theorem	fsumcncf 37632*	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 37633*	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 37634	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 37635*	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 37636*	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 37637*	Composition of continuous functions. A generalization of cncfmpt1f 21880 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 37638*	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 37639	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 37640	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 37641*	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 37642*	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 37643*	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 37644	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 37645*	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 37646	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 37647*	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 37648*	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 37649*	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 37650*	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 37651*	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 37652*	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 37653	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 37654*	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 37655*	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 37656*	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 37657*	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 37658	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 37659*	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 37660*	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 37661	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 37662*	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 37663	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 37664*	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 37665	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 37666*	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 37667*	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 37668*	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 37669*	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 37670	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 37671	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 37672*	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 37673	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 37674	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 37675*	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 37676	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 37677*	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 37678*	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 37679*	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 37680*	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 37681*	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	ioodvbdlimc1lem1OLD 37682*	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.) Obsolete version of ioodvbdlimc1lem1 37680 as of 3-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( 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	ioodvbdlimc1lem2OLD 37683*	Limit at the lower bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) Obsolete version of ioodvbdlimc1lem2 37681 as of 3-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( 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 37684*	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 37685*	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	ioodvbdlimc2lemOLD 37686*	Limit at the upper bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) Obsolete version of ioodvbdlimc2lem 37685 as of 3-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( 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 37687*	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 37688	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 37689*	Function-builder for derivative, product rule. A version of dvmptmul 22850 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 37690*	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 37691	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 37692*	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 37693*	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 37694*	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 37695*	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 37696*	Induction step for dvmptfprod 37697. (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 37697*	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 37698*	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 37699*	Induction step for dvnprodlem2 37699. (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 37700*	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 ) ) ) )