P. 372 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37101-37200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvdivbd 37101*	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 37102	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 37103	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 37104*	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 37105	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 37106*	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 37107*	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 37108*	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 37109*	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 37110*	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 37111*	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 37112*	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 37113*	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 37114	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 37115*	Function-builder for derivative, product rule. A version of dvmptmul 22658 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 37116*	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 37117	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 37118*	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 37119*	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 37120*	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 37121*	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 37122*	Induction step for dvmptfprod 37123. (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 37123*	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 37124*	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 37125*	Induction step for dvnprodlem2 37125. (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 37126*	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 37127*	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 37128	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 37129*	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 37130*	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 37131	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 37132*	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 37133*	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 37134*	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 37135*	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 37136*	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 37137	The empty set is a measurable function (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- (/) e. MblFn
Theorem	mbfres2cn 37138	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 22346 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 37139	The measure of the empty set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( vol ` (/) ) = 0
Theorem	ditgeqiooicc 37140*	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 37141	The volume of a set is always nonnegative. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. dom vol -> 0 <_ ( vol ` A ) )
Theorem	cnbdibl 37142*	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 37143	A singleton is measurable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. RR -> { A } e. dom vol )
Theorem	ditgeq3d 37144*	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 37145	The empty function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- (/) e. L^1
Theorem	iblsplit 37146*	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 37147	A singleton has 0 Lebesgue measure. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. RR -> ( vol ` { A } ) = 0 )
Theorem	itgvol0 37148*	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 37149*	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 37150*	A version of iblsplit 37146 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 37151*	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 37152	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 37153*	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 37154*	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 37155*	lemma for itgsubsticc 37156 (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 37156*	Integration by u-substitution. The main difference with respect to itgsubst 22744 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 37157*	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 37158	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 37159*	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 37160*	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 37161*	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 37162*	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 37163*	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 )
21.30.12  Stone Weierstrass theorem - real version
Theorem	stoweidlem1 37164	Lemma for stoweid 37226. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90; the key step uses Bernoulli's inequality bernneq 12338. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- ( ph -> N e. NN )   &    |- ( ph -> K e. NN )   &    |- ( ph -> D e. RR+ )   &    |- ( ph -> A e. RR+ )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> A <_ 1 )   &    |- ( ph -> D <_ A )   =>    |- ( ph -> ( ( 1 - ( A ^ N ) ) ^ ( K ^ N ) ) <_ ( 1 / ( ( K x. D ) ^ N ) ) )
Theorem	stoweidlem2 37165*	lemma for stoweid 37226: here we prove that the subalgebra of continuous functions, which contains constant functions, is closed under scaling. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ t ph   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )   &    |- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )   &    |- ( ( ph /\ f e. A ) -> f : T --> RR )   &    |- ( ph -> E e. RR )   &    |- ( ph -> F e. A )   =>    |- ( ph -> ( t e. T |-> ( E x. ( F ` t ) ) ) e. A )
Theorem	stoweidlem3 37166*	Lemma for stoweid 37226: if A is positive and all M terms of a finite product are larger than A, then the finite product is larger than A^M. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ i F   &    |- F/ i ph   &    |- X = seq 1 ( x. , F )   &    |- ( ph -> M e. NN )   &    |- ( ph -> F : ( 1 ... M ) --> RR )   &    |- ( ( ph /\ i e. ( 1 ... M ) ) -> A < ( F ` i ) )   &    |- ( ph -> A e. RR+ )   =>    |- ( ph -> ( A ^ M ) < ( X ` M ) )
Theorem	stoweidlem4 37167*	Lemma for stoweid 37226: a class variable replaces a setvar variable, for constant functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )   =>    |- ( ( ph /\ B e. RR ) -> ( t e. T |-> B ) e. A )
Theorem	stoweidlem5 37168*	There exists a δ as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: 0 < δ < 1 , p >= δ on T \ U. Here D is used to represent δ in the paper and Q to represent T \ U in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ t ph   &    |- D = if ( C <_ ( 1 / 2 ) , C , ( 1 / 2 ) )   &    |- ( ph -> P : T --> RR )   &    |- ( ph -> Q C_ T )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> A. t e. Q C <_ ( P ` t ) )   =>    |- ( ph -> E. d ( d e. RR+ /\ d < 1 /\ A. t e. Q d <_ ( P ` t ) ) )
Theorem	stoweidlem6 37169*	Lemma for stoweid 37226: two class variables replace two setvar variables, for multiplication of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ t f = F   &    |- F/ t g = G   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )   =>    |- ( ( ph /\ F e. A /\ G e. A ) -> ( t e. T |-> ( ( F ` t ) x. ( G ` t ) ) ) e. A )
Theorem	stoweidlem7 37170*	This lemma is used to prove that qn as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91, (at the top of page 91), is such that qn < ε on T \ U, and qn > 1 - ε on V. Here it is proven that, for n large enough, 1-(k*δ/2)^n > 1 - ε , and 1/(k*δ)^n < ε. The variable A is used to represent (k*δ) in the paper, and B is used to represent (k*δ/2). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F = ( i e. NN0 |-> ( ( 1 / A ) ^ i ) )   &    |- G = ( i e. NN0 |-> ( B ^ i ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> 1 < A )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> B < 1 )   &    |- ( ph -> E e. RR+ )   =>    |- ( ph -> E. n e. NN ( ( 1 - E ) < ( 1 - ( B ^ n ) ) /\ ( 1 / ( A ^ n ) ) < E ) )
Theorem	stoweidlem8 37171*	Lemma for stoweid 37226: two class variables replace two setvar variables, for the sum of two functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )   &    |- F/_ t F   &    |- F/_ t G   =>    |- ( ( ph /\ F e. A /\ G e. A ) -> ( t e. T |-> ( ( F ` t ) + ( G ` t ) ) ) e. A )
Theorem	stoweidlem9 37172*	Lemma for stoweid 37226: here the Stone Weierstrass theorem is proven for the trivial case, T is the empty set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- ( ph -> T = (/) )   &    |- ( ph -> ( t e. T |-> 1 ) e. A )   =>    |- ( ph -> E. g e. A A. t e. T ( abs ` ( ( g ` t ) - ( F ` t ) ) ) < E )
Theorem	stoweidlem10 37173	Lemma for stoweid 37226. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90, this lemma is an application of Bernoulli's inequality. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- ( ( A e. RR /\ N e. NN0 /\ A <_ 1 ) -> ( 1 - ( N x. A ) ) <_ ( ( 1 - A ) ^ N ) )
Theorem	stoweidlem11 37174*	This lemma is used to prove that there is a function g as in the proof of [BrosowskiDeutsh] p. 92 (at the top of page 92): this lemma proves that g(t) < ( j + 1 / 3 ) * ε. Here E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- ( ph -> N e. NN )   &    |- ( ph -> t e. T )   &    |- ( ph -> j e. ( 1 ... N ) )   &    |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR )   &    |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( ( X ` i ) ` t ) <_ 1 )   &    |- ( ( ph /\ i e. ( j ... N ) ) -> ( ( X ` i ) ` t ) < ( E / N ) )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> E < ( 1 / 3 ) )   =>    |- ( ph -> ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) )
Theorem	stoweidlem12 37175*	Lemma for stoweid 37226. This Lemma is used by other three Lemmas. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- Q = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )   &    |- ( ph -> P : T --> RR )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> K e. NN0 )   =>    |- ( ( ph /\ t e. T ) -> ( Q ` t ) = ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
Theorem	stoweidlem13 37176	Lemma for stoweid 37226. This lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon, in the last step of the proof in [BrosowskiDeutsh] p. 92. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- ( ph -> E e. RR+ )   &    |- ( ph -> X e. RR )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> j e. RR )   &    |- ( ph -> ( ( j - ( 4 / 3 ) ) x. E ) < X )   &    |- ( ph -> X <_ ( ( j - ( 1 / 3 ) ) x. E ) )   &    |- ( ph -> ( ( j - ( 4 / 3 ) ) x. E ) < Y )   &    |- ( ph -> Y < ( ( j + ( 1 / 3 ) ) x. E ) )   =>    |- ( ph -> ( abs ` ( Y - X ) ) < ( 2 x. E ) )
Theorem	stoweidlem14 37177*	There exists a k as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: k is an integer and 1 < k * δ < 2. D is used to represent δ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- A = { j e. NN | ( 1 / D ) < j }   &    |- ( ph -> D e. RR+ )   &    |- ( ph -> D < 1 )   =>    |- ( ph -> E. k e. NN ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) )
Theorem	stoweidlem15 37178*	This lemma is used to prove the existence of a function p as in Lemma 1 from [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 ≤ p ≤ 1, p(t_0) = 0, and p > 0 on T - U. Here ( G ` I ) is used to represent p(t_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }   &    |- ( ph -> G : ( 1 ... M ) --> Q )   &    |- ( ( ph /\ f e. A ) -> f : T --> RR )   =>    |- ( ( ( ph /\ I e. ( 1 ... M ) ) /\ S e. T ) -> ( ( ( G ` I ) ` S ) e. RR /\ 0 <_ ( ( G ` I ) ` S ) /\ ( ( G ` I ) ` S ) <_ 1 ) )
Theorem	stoweidlem16 37179*	Lemma for stoweid 37226. The subset Y of functions in the algebra A, with values in [ 0 , 1 ], is closed under multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ t ph   &    |- Y = { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }   &    |- H = ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) )   &    |- ( ( ph /\ f e. A ) -> f : T --> RR )   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )   =>    |- ( ( ph /\ f e. Y /\ g e. Y ) -> H e. Y )
Theorem	stoweidlem17 37180*	This lemma proves that the function g (as defined in [BrosowskiDeutsh] p. 91, at the end of page 91) belongs to the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ t ph   &    |- ( ph -> N e. NN )   &    |- ( ph -> X : ( 0 ... N ) --> A )   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )   &    |- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )   &    |- ( ph -> E e. RR )   &    |- ( ( ph /\ f e. A ) -> f : T --> RR )   =>    |- ( ph -> ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) e. A )
Theorem	stoweidlem18 37181*	This theorem proves Lemma 2 in [BrosowskiDeutsh] p. 92 when A is empty, the trivial case. Here D is used to denote the set A of Lemma 2, because the variable A is used for the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t D   &    |- F/ t ph   &    |- F = ( t e. T |-> 1 )   &    |- T = U. J   &    |- ( ( ph /\ a e. RR ) -> ( t e. T |-> a ) e. A )   &    |- ( ph -> B e. ( Clsd ` J ) )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> D = (/) )   =>    |- ( ph -> E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. D ( x ` t ) < E /\ A. t e. B ( 1 - E ) < ( x ` t ) ) )
Theorem	stoweidlem19 37182*	If a set of real functions is closed under multiplication and it contains constants, then it is closed under finite exponentiation. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t F   &    |- F/ t ph   &    |- ( ( ph /\ f e. A ) -> f : T --> RR )   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )   &    |- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )   &    |- ( ph -> F e. A )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( t e. T |-> ( ( F ` t ) ^ N ) ) e. A )
Theorem	stoweidlem20 37183*	If a set A of real functions from a common domain T is closed under the sum of two functions, then it is closed under the sum of a finite number of functions, indexed by G. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ t ph   &    |- F = ( t e. T |-> sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> G : ( 1 ... M ) --> A )   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )   &    |- ( ( ph /\ f e. A ) -> f : T --> RR )   =>    |- ( ph -> F e. A )
Theorem	stoweidlem21 37184*	Once the Stone Weierstrass theorem has been proven for approximating nonnegative functions, then this lemma is used to extend the result to functions with (possibly) negative values. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t G   &    |- F/_ t H   &    |- F/_ t S   &    |- F/ t ph   &    |- G = ( t e. T |-> ( ( H ` t ) + S ) )   &    |- ( ph -> F : T --> RR )   &    |- ( ph -> S e. RR )   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )   &    |- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )   &    |- ( ph -> A. f e. A f : T --> RR )   &    |- ( ph -> H e. A )   &    |- ( ph -> A. t e. T ( abs ` ( ( H ` t ) - ( ( F ` t ) - S ) ) ) < E )   =>    |- ( ph -> E. f e. A A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < E )
Theorem	stoweidlem22 37185*	If a set of real functions from a common domain is closed under addition, multiplication and it contains constants, then it is closed under subtraction. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ t ph   &    |- F/_ t F   &    |- F/_ t G   &    |- H = ( t e. T |-> ( ( F ` t ) - ( G ` t ) ) )   &    |- I = ( t e. T |-> -u 1 )   &    |- L = ( t e. T |-> ( ( I ` t ) x. ( G ` t ) ) )   &    |- ( ( ph /\ f e. A ) -> f : T --> RR )   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )   &    |- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )   =>    |- ( ( ph /\ F e. A /\ G e. A ) -> ( t e. T |-> ( ( F ` t ) - ( G ` t ) ) ) e. A )
Theorem	stoweidlem23 37186*	This lemma is used to prove the existence of a function pt as in the beginning of Lemma 1 [BrosowskiDeutsh] p. 90: for all t in T - U, there exists a function p in the subalgebra, such that pt ( t0 ) = 0 , pt ( t ) > 0, and 0 <= pt <= 1. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ t ph   &    |- F/_ t G   &    |- H = ( t e. T |-> ( ( G ` t ) - ( G ` Z ) ) )   &    |- ( ( ph /\ f e. A ) -> f : T --> RR )   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )   &    |- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )   &    |- ( ph -> S e. T )   &    |- ( ph -> Z e. T )   &    |- ( ph -> G e. A )   &    |- ( ph -> ( G ` S ) =/= ( G ` Z ) )   =>    |- ( ph -> ( H e. A /\ ( H ` S ) =/= ( H ` Z ) /\ ( H ` Z ) = 0 ) )
Theorem	stoweidlem24 37187*	This lemma proves that for n sufficiently large, qn( t ) > ( 1 - epsilon ), for all t in V: see Lemma 1 [BrosowskiDeutsh] p. 90, (at the bottom of page 90). Q is used to represent qn in the paper, N to represent n in the paper, K to represent k, D to represent δ, and E to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- V = { t e. T | ( P ` t ) < ( D / 2 ) }   &    |- Q = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )   &    |- ( ph -> P : T --> RR )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> K e. NN0 )   &    |- ( ph -> D e. RR+ )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> ( 1 - E ) < ( 1 - ( ( ( K x. D ) / 2 ) ^ N ) ) )   &    |- ( ph -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )   =>    |- ( ( ph /\ t e. V ) -> ( 1 - E ) < ( Q ` t ) )
Theorem	stoweidlem25 37188*	This lemma proves that for n sufficiently large, qn( t ) < ε, for all t in T \ U: see Lemma 1 [BrosowskiDeutsh] p. 91 (at the top of page 91). Q is used to represent qn in the paper, N to represent n in the paper, K to represent k, D to represent δ, P to represent p, and E to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- Q = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> K e. NN )   &    |- ( ph -> D e. RR+ )   &    |- ( ph -> P : T --> RR )   &    |- ( ph -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )   &    |- ( ph -> A. t e. ( T \ U ) D <_ ( P ` t ) )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> ( 1 / ( ( K x. D ) ^ N ) ) < E )   =>    |- ( ( ph /\ t e. ( T \ U ) ) -> ( Q ` t ) < E )
Theorem	stoweidlem26 37189*	This lemma is used to prove that there is a function g as in the proof of [BrosowskiDeutsh] p. 92: this lemma proves that g(t) > ( j - 4 / 3 ) * ε. Here L is used to represnt j in the paper, D is used to represent A in the paper, S is used to represent t, and E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t F   &    |- F/ j ph   &    |- F/ t ph   &    |- D = ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )   &    |- B = ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )   &    |- ( ph -> N e. NN )   &    |- ( ph -> T e. _V )   &    |- ( ph -> L e. ( 1 ... N ) )   &    |- ( ph -> S e. ( ( D ` L ) \ ( D ` ( L - 1 ) ) ) )   &    |- ( ph -> F : T --> RR )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> E < ( 1 / 3 ) )   &    |- ( ( ph /\ i e. ( 0 ... N ) ) -> ( X ` i ) : T --> RR )   &    |- ( ( ph /\ i e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` i ) ` t ) )   &    |- ( ( ph /\ i e. ( 0 ... N ) /\ t e. ( B ` i ) ) -> ( 1 - ( E / N ) ) < ( ( X ` i ) ` t ) )   =>    |- ( ph -> ( ( L - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` S ) )
Theorem	stoweidlem27 37190*	This lemma is used to prove the existence of a function p as in Lemma 1 [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p(t_0) = 0, and p > 0 on T - U. Here ( q ` i ) is used to represent p(t_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- G = ( w e. X |-> { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )   &    |- ( ph -> Q e. _V )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Y Fn ran G )   &    |- ( ph -> ran G e. _V )   &    |- ( ( ph /\ l e. ran G ) -> ( Y ` l ) e. l )   &    |- ( ph -> F : ( 1 ... M ) -1-1-onto-> ran G )   &    |- ( ph -> ( T \ U ) C_ U. X )   &    |- F/ t ph   &    |- F/ w ph   &    |- F/_ h Q   =>    |- ( ph -> E. q ( M e. NN /\ ( q : ( 1 ... M ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... M ) 0 < ( ( q ` i ) ` t ) ) ) )
Theorem	stoweidlem28 37191*	There exists a δ as in Lemma 1 [BrosowskiDeutsh] p. 90: 0 < delta < 1 and p >= delta on T \ U. Here d is used to represent δ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t U   &    |- F/ t ph   &    |- K = ( topGen ` ran (,) )   &    |- T = U. J   &    |- ( ph -> J e. Comp )   &    |- ( ph -> P e. ( J Cn K ) )   &    |- ( ph -> A. t e. ( T \ U ) 0 < ( P ` t ) )   &    |- ( ph -> U e. J )   =>    |- ( ph -> E. d ( d e. RR+ /\ d < 1 /\ A. t e. ( T \ U ) d <_ ( P ` t ) ) )
Theorem	stoweidlem29 37192*	When the hypothesis for the extreme value theorem hold, then the inf of the range of the function belongs to the range, it is real and it a lower bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t F   &    |- F/ t ph   &    |- T = U. J   &    |- K = ( topGen ` ran (,) )   &    |- ( ph -> J e. Comp )   &    |- ( ph -> F e. ( J Cn K ) )   &    |- ( ph -> T =/= (/) )   =>    |- ( ph -> ( sup ( ran F , RR , `' < ) e. ran F /\ sup ( ran F , RR , `' < ) e. RR /\ A. t e. T sup ( ran F , RR , `' < ) <_ ( F ` t ) ) )
Theorem	stoweidlem30 37193*	This lemma is used to prove the existence of a function p as in Lemma 1 [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p(t_0) = 0, and p > 0 on T - U. Z is used for t0, P is used for p, ( G ` i ) is used for p(t_i). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }   &    |- P = ( t e. T |-> ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> G : ( 1 ... M ) --> Q )   &    |- ( ( ph /\ f e. A ) -> f : T --> RR )   =>    |- ( ( ph /\ S e. T ) -> ( P ` S ) = ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` S ) ) )
Theorem	stoweidlem31 37194*	This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91: assuming that R is a finite subset of V, x indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all i ranging in the finite indexing set, 0 ≤ xi ≤ 1, xi < ε / m on V(ti), and xi > 1 - ε / m on B. Here M is used to represent m in the paper, E is used to represent ε in the paper, vi is used to represent V(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ h ph   &    |- F/ t ph   &    |- F/ w ph   &    |- Y = { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }   &    |- V = { w e. J | A. e e. RR+ E. h e. A ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( h ` t ) ) }   &    |- G = ( w e. R |-> { h e. A | ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) /\ A. t e. w ( h ` t ) < ( E / M ) /\ A. t e. ( T \ U ) ( 1 - ( E / M ) ) < ( h ` t ) ) } )   &    |- ( ph -> R C_ V )   &    |- ( ph -> M e. NN )   &    |- ( ph -> v : ( 1 ... M ) -1-1-onto-> R )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> B C_ ( T \ U ) )   &    |- ( ph -> V e. _V )   &    |- ( ph -> A e. _V )   &    |- ( ph -> ran G e. Fin )   =>    |- ( ph -> E. x ( x : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( v ` i ) ( ( x ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( x ` i ) ` t ) ) ) )
Theorem	stoweidlem32 37195*	If a set A of real functions from a common domain T is a subalgebra and it contains constants, then it is closed under the sum of a finite number of functions, indexed by G and finally scaled by a real Y. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ t ph   &    |- P = ( t e. T |-> ( Y x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) ) )   &    |- F = ( t e. T |-> sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) )   &    |- H = ( t e. T |-> Y )   &    |- ( ph -> M e. NN )   &    |- ( ph -> Y e. RR )   &    |- ( ph -> G : ( 1 ... M ) --> A )   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )   &    |- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )   &    |- ( ( ph /\ f e. A ) -> f : T --> RR )   =>    |- ( ph -> P e. A )
Theorem	stoweidlem33 37196*	If a set of real functions from a common domain is closed under addition, multiplication and it contains constants, then it is closed under subtraction. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t F   &    |- F/_ t G   &    |- F/ t ph   &    |- ( ( ph /\ f e. A ) -> f : T --> RR )   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )   &    |- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )   =>    |- ( ( ph /\ F e. A /\ G e. A ) -> ( t e. T |-> ( ( F ` t ) - ( G ` t ) ) ) e. A )
Theorem	stoweidlem34 37197*	This lemma proves that for all t in T there is a j as in the proof of [BrosowskiDeutsh] p. 91 (at the bottom of page 91 and at the top of page 92): (j-4/3) * ε < f(t) <= (j-1/3) * ε , g(t) < (j+1/3) * ε, and g(t) > (j-4/3) * ε. Here E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t F   &    |- F/ j ph   &    |- F/ t ph   &    |- D = ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )   &    |- B = ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )   &    |- J = ( t e. T |-> { j e. ( 1 ... N ) | t e. ( D ` j ) } )   &    |- ( ph -> N e. NN )   &    |- ( ph -> T e. _V )   &    |- ( ph -> F : T --> RR )   &    |- ( ( ph /\ t e. T ) -> 0 <_ ( F ` t ) )   &    |- ( ( ph /\ t e. T ) -> ( F ` t ) < ( ( N - 1 ) x. E ) )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> E < ( 1 / 3 ) )   &    |- ( ( ph /\ j e. ( 0 ... N ) ) -> ( X ` j ) : T --> RR )   &    |- ( ( ph /\ j e. ( 0 ... N ) /\ t e. T ) -> 0 <_ ( ( X ` j ) ` t ) )   &    |- ( ( ph /\ j e. ( 0 ... N ) /\ t e. T ) -> ( ( X ` j ) ` t ) <_ 1 )   &    |- ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( D ` j ) ) -> ( ( X ` j ) ` t ) < ( E / N ) )   &    |- ( ( ph /\ j e. ( 0 ... N ) /\ t e. ( B ` j ) ) -> ( 1 - ( E / N ) ) < ( ( X ` j ) ` t ) )   =>    |- ( ph -> A. t e. T E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( ( t e. T |-> sum_ i e. ( 0 ... N ) ( E x. ( ( X ` i ) ` t ) ) ) ` t ) ) ) )
Theorem	stoweidlem35 37198*	This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p(t_0) = 0, and p > 0 on T - U. Here ( q ` i ) is used to represent p(t_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ t ph   &    |- F/ w ph   &    |- F/ h ph   &    |- Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }   &    |- W = { w e. J | E. h e. Q w = { t e. T | 0 < ( h ` t ) } }   &    |- G = ( w e. X |-> { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )   &    |- ( ph -> A e. _V )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> X C_ W )   &    |- ( ph -> ( T \ U ) C_ U. X )   &    |- ( ph -> ( T \ U ) =/= (/) )   =>    |- ( ph -> E. m E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) )
Theorem	stoweidlem36 37199*	This lemma is used to prove the existence of a function pt as in Lemma 1 of [BrosowskiDeutsh] p. 90 (at the beginning of Lemma 1): for all t in T - U, there exists a function p in the subalgebra, such that pt ( t0 ) = 0 , pt ( t ) > 0, and 0 <= pt <= 1. Z is used for t0 , S is used for t e. T - U , h is used for pt . G is used for (ht)^2 and the final h is a normalized version of G ( divided by its norm, see the variable N ). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ h Q   &    |- F/_ t H   &    |- F/_ t F   &    |- F/_ t G   &    |- F/ t ph   &    |- K = ( topGen ` ran (,) )   &    |- Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }   &    |- T = U. J   &    |- G = ( t e. T |-> ( ( F ` t ) x. ( F ` t ) ) )   &    |- N = sup ( ran G , RR , < )   &    |- H = ( t e. T |-> ( ( G ` t ) / N ) )   &    |- ( ph -> J e. Comp )   &    |- ( ph -> A C_ ( J Cn K ) )   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )   &    |- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )   &    |- ( ph -> S e. T )   &    |- ( ph -> Z e. T )   &    |- ( ph -> F e. A )   &    |- ( ph -> ( F ` S ) =/= ( F ` Z ) )   &    |- ( ph -> ( F ` Z ) = 0 )   =>    |- ( ph -> E. h ( h e. Q /\ 0 < ( h ` S ) ) )
Theorem	stoweidlem37 37200*	This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p(t_0) = 0, and p > 0 on T - U. Z is used for t0, P is used for p, ( G ` i ) is used for p(t_i). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }   &    |- P = ( t e. T |-> ( ( 1 / M ) x. sum_ i e. ( 1 ... M ) ( ( G ` i ) ` t ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> G : ( 1 ... M ) --> Q )   &    |- ( ( ph /\ f e. A ) -> f : T --> RR )   &    |- ( ph -> Z e. T )   =>    |- ( ph -> ( P ` Z ) = 0 )