P. 375 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37401-37500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	itgeq1d 37401*	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 37402	The empty set is a measurable function (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- (/) e. MblFn
Theorem	mbfres2cn 37403	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 22478 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 37404	The measure of the empty set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( vol ` (/) ) = 0
Theorem	ditgeqiooicc 37405*	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 37406	The volume of a set is always nonnegative. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. dom vol -> 0 <_ ( vol ` A ) )
Theorem	cnbdibl 37407*	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 37408	A singleton is measurable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. RR -> { A } e. dom vol )
Theorem	ditgeq3d 37409*	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 37410	The empty function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- (/) e. L^1
Theorem	iblsplit 37411*	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 37412	A singleton has 0 Lebesgue measure. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. RR -> ( vol ` { A } ) = 0 )
Theorem	itgvol0 37413*	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 37414*	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 37415*	A version of iblsplit 37411 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 37416*	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 37417	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 37418*	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 37419*	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 37420*	lemma for itgsubsticc 37421 (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 37421*	Integration by u-substitution. The main difference with respect to itgsubst 22878 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 37422*	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 37423	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 37424*	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 37425*	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 37426*	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 37427*	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 37428*	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 37429	Lemma for stoweid 37493. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90; the key step uses Bernoulli's inequality bernneq 12395. (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 37430*	lemma for stoweid 37493: 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 37431*	Lemma for stoweid 37493: 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 37432*	Lemma for stoweid 37493: 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 37433*	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 37434*	Lemma for stoweid 37493: 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 37435*	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 37436*	Lemma for stoweid 37493: 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 37437*	Lemma for stoweid 37493: 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 37438	Lemma for stoweid 37493. 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 37439*	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 37440*	Lemma for stoweid 37493. 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 37441	Lemma for stoweid 37493. 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 37442*	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 37443*	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 37444*	Lemma for stoweid 37493. 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 37445*	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 37446*	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 37447*	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 37448*	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 37449*	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 37450*	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 37451*	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 37452*	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 37453*	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 37454*	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 37455*	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 37456*	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 37457*	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.) (Revised by AV, 13-Sep-2020.)
|- 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 -> (inf ( ran F , RR , < ) e. ran F /\ inf ( ran F , RR , < ) e. RR /\ A. t e. T inf ( ran F , RR , < ) <_ ( F ` t ) ) )
Theorem	stoweidlem29OLD 37458*	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.) Obsolete version of stoweidlem29 37457 as of 13-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- 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 37459*	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 37460*	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 37461*	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 37462*	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 37463*	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 37464*	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 37465*	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 37466*	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 )
Theorem	stoweidlem38 37467*	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 /\ S e. T ) -> ( 0 <_ ( P ` S ) /\ ( P ` S ) <_ 1 ) )
Theorem	stoweidlem39 37468*	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 W, 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 D is used to represent A in the paper's Lemma 2 (because A is used for the subalgebra), M is used to represent m in the paper, E is used to represent ε, and vi is used to represent V(ti). W is just a local definition, used to shorten statements. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ h ph   &    |- F/ t ph   &    |- F/ w ph   &    |- U = ( T \ B )   &    |- Y = { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }   &    |- W = { 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 ) ) }   &    |- ( ph -> r e. ( ~P W i^i Fin ) )   &    |- ( ph -> D C_ U. r )   &    |- ( ph -> D =/= (/) )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> B C_ T )   &    |- ( ph -> W e. _V )   &    |- ( ph -> A e. _V )   =>    |- ( ph -> E. m e. NN E. v ( v : ( 1 ... m ) --> W /\ D C_ U. ran v /\ 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	stoweidlem40 37469*	This lemma proves that qn is in the subalgebra, as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90. Q is used to represent qn in the paper, N is used to represent n in the paper, and M is used to represent k^n in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t P   &    |- F/ t ph   &    |- Q = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ M ) )   &    |- F = ( t e. T |-> ( 1 - ( ( P ` t ) ^ N ) ) )   &    |- G = ( t e. T |-> 1 )   &    |- H = ( t e. T |-> ( ( P ` t ) ^ N ) )   &    |- ( ph -> P e. A )   &    |- ( ph -> P : T --> RR )   &    |- ( ( 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 -> N e. NN )   &    |- ( ph -> M e. NN )   =>    |- ( ph -> Q e. A )
Theorem	stoweidlem41 37470*	This lemma is used to prove that there exists x as in Lemma 1 of [BrosowskiDeutsh] p. 90: 0 <= x(t) <= 1 for all t in T, x(t) < epsilon for all t in V, x(t) > 1 - epsilon for all t in T \ U. Here we prove the very last step of the proof of Lemma 1: "The result follows from taking x = 1 - qn";. Here E is used to represent ε in the paper, and y to represent qn in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ t ph   &    |- X = ( t e. T |-> ( 1 - ( y ` t ) ) )   &    |- F = ( t e. T |-> 1 )   &    |- V C_ T   &    |- ( ph -> y e. A )   &    |- ( ph -> y : T --> RR )   &    |- ( ( 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 /\ w e. RR ) -> ( t e. T |-> w ) e. A )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) )   &    |- ( ph -> A. t e. V ( 1 - E ) < ( y ` t ) )   &    |- ( ph -> A. t e. ( T \ U ) ( y ` t ) < E )   =>    |- ( ph -> E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. V ( x ` t ) < E /\ A. t e. ( T \ U ) ( 1 - E ) < ( x ` t ) ) )
Theorem	stoweidlem42 37471*	This lemma is used to prove that x built as in Lemma 2 of [BrosowskiDeutsh] p. 91, is such that x > 1 - ε on B. Here X is used to represent x in the paper, and E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ i ph   &    |- F/ t ph   &    |- F/_ t Y   &    |- P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )   &    |- X = ( seq 1 ( P , U ) ` M )   &    |- F = ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )   &    |- Z = ( t e. T |-> ( seq 1 ( x. , ( F ` t ) ) ` M ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> U : ( 1 ... M ) --> Y )   &    |- ( ( ph /\ i e. ( 1 ... M ) ) -> A. t e. B ( 1 - ( E / M ) ) < ( ( U ` i ) ` t ) )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> E < ( 1 / 3 ) )   &    |- ( ( ph /\ f e. Y ) -> f : T --> RR )   &    |- ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y )   &    |- ( ph -> T e. _V )   &    |- ( ph -> B C_ T )   =>    |- ( ph -> A. t e. B ( 1 - E ) < ( X ` t ) )
Theorem	stoweidlem43 37472*	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 pt in the subalgebra, such that pt( t0 ) = 0 , pt ( t ) > 0, and 0 <= pt <= 1. Hera Z is used for t0 , S is used for t e. T - U , h is used for pt. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ g ph   &    |- F/ t ph   &    |- F/_ h Q   &    |- K = ( topGen ` ran (,) )   &    |- Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }   &    |- T = U. J   &    |- ( ph -> J e. Comp )   &    |- ( ph -> A C_ ( J Cn K ) )   &    |- ( ( ph /\ f e. A /\ l e. A ) -> ( t e. T |-> ( ( f ` t ) + ( l ` t ) ) ) e. A )   &    |- ( ( ph /\ f e. A /\ l e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( l ` t ) ) ) e. A )   &    |- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )   &    |- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. g e. A ( g ` r ) =/= ( g ` t ) )   &    |- ( ph -> U e. J )   &    |- ( ph -> Z e. U )   &    |- ( ph -> S e. ( T \ U ) )   =>    |- ( ph -> E. h ( h e. Q /\ 0 < ( h ` S ) ) )
Theorem	stoweidlem44 37473*	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 to represent t0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ j ph   &    |- F/ t ph   &    |- K = ( topGen ` ran (,) )   &    |- 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 -> A. t e. ( T \ U ) E. j e. ( 1 ... M ) 0 < ( ( G ` j ) ` t ) )   &    |- T = U. J   &    |- ( ph -> A C_ ( J Cn K ) )   &    |- ( ( 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 -> Z e. T )   =>    |- ( ph -> E. p e. A ( A. t e. T ( 0 <_ ( p ` t ) /\ ( p ` t ) <_ 1 ) /\ ( p ` Z ) = 0 /\ A. t e. ( T \ U ) 0 < ( p ` t ) ) )
Theorem	stoweidlem45 37474*	This lemma proves that, given an appropriate K (in another theorem we prove such a K exists), there exists a function qn as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91 ( at the top of page 91): 0 <= qn <= 1 , qn < ε on T \ U, and qn > 1 - ε on V. We use y to represent the final qn in the paper (the one with n large enough), N to represent n in the paper, K to represent k, D to represent δ, E to represent ε, and P to represent p. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t P   &    |- F/ t ph   &    |- V = { t e. T | ( P ` t ) < ( D / 2 ) }   &    |- Q = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> K e. NN )   &    |- ( ph -> D e. RR+ )   &    |- ( ph -> D < 1 )   &    |- ( ph -> P e. A )   &    |- ( 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 /\ 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 -> E e. RR+ )   &    |- ( ph -> ( 1 - E ) < ( 1 - ( ( ( K x. D ) / 2 ) ^ N ) ) )   &    |- ( ph -> ( 1 / ( ( K x. D ) ^ N ) ) < E )   =>    |- ( ph -> E. y e. A ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - E ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < E ) )
Theorem	stoweidlem46 37475*	This lemma proves that sets U(t) as defined in Lemma 1 of [BrosowskiDeutsh] p. 90, are a cover of T \ U. Using this lemma, in a later theorem we will prove that a finite subcover exists. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t U   &    |- F/_ h Q   &    |- F/ q ph   &    |- F/ t ph   &    |- K = ( topGen ` ran (,) )   &    |- 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 ) } }   &    |- T = U. J   &    |- ( ph -> J e. Comp )   &    |- ( ph -> A C_ ( J Cn K ) )   &    |- ( ( 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 /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )   &    |- ( ph -> U e. J )   &    |- ( ph -> Z e. U )   &    |- ( ph -> T e. _V )   =>    |- ( ph -> ( T \ U ) C_ U. W )
Theorem	stoweidlem47 37476*	Subtracting a constant from a real continuous function gives another continuous function. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t F   &    |- F/_ t S   &    |- F/ t ph   &    |- T = U. J   &    |- G = ( T X. { -u S } )   &    |- K = ( topGen ` ran (,) )   &    |- ( ph -> J e. Top )   &    |- C = ( J Cn K )   &    |- ( ph -> F e. C )   &    |- ( ph -> S e. RR )   =>    |- ( ph -> ( t e. T |-> ( ( F ` t ) - S ) ) e. C )
Theorem	stoweidlem48 37477*	This lemma is used to prove that x built as in Lemma 2 of [BrosowskiDeutsh] p. 91, is such that x < ε on A. Here X is used to represent x in the paper, E is used to represent ε in the paper, and D is used to represent A in the paper (because A is always used to represent the subalgebra). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ i ph   &    |- F/ t ph   &    |- Y = { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }   &    |- P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )   &    |- X = ( seq 1 ( P , U ) ` M )   &    |- F = ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )   &    |- Z = ( t e. T |-> ( seq 1 ( x. , ( F ` t ) ) ` M ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> W : ( 1 ... M ) --> V )   &    |- ( ph -> U : ( 1 ... M ) --> Y )   &    |- ( ph -> D C_ U. ran W )   &    |- ( ph -> D C_ T )   &    |- ( ( ph /\ i e. ( 1 ... M ) ) -> A. t e. ( W ` i ) ( ( U ` i ) ` t ) < E )   &    |- ( ph -> T e. _V )   &    |- ( ( 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 -> E e. RR+ )   =>    |- ( ph -> A. t e. D ( X ` t ) < E )
Theorem	stoweidlem49 37478*	There exists a function qn as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91 (at the top of page 91): 0 <= qn <= 1 , qn < ε on T \ U, and qn > 1 - ε on V. Here y is used to represent the final qn in the paper (the one with n large enough), N represents n in the paper, K represents k, D represents δ, E represents ε, and P represents p. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t P   &    |- F/ t ph   &    |- V = { t e. T | ( P ` t ) < ( D / 2 ) }   &    |- ( ph -> D e. RR+ )   &    |- ( ph -> D < 1 )   &    |- ( ph -> P e. A )   &    |- ( 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 /\ 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 -> E e. RR+ )   =>    |- ( ph -> E. y e. A ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - E ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < E ) )
Theorem	stoweidlem50 37479*	This lemma proves that sets U(t) as defined in Lemma 1 of [BrosowskiDeutsh] p. 90, contain a finite subcover of T \ U. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t U   &    |- F/ t ph   &    |- K = ( topGen ` ran (,) )   &    |- 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 ) } }   &    |- T = U. J   &    |- C = ( J Cn K )   &    |- ( ph -> J e. Comp )   &    |- ( ph -> A C_ C )   &    |- ( ( 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 /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )   &    |- ( ph -> U e. J )   &    |- ( ph -> Z e. U )   =>    |- ( ph -> E. u ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u ) )
Theorem	stoweidlem51 37480*	There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. Here D is used to represent A in the paper, because here A is used for the subalgebra of functions. E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ i ph   &    |- F/ t ph   &    |- F/ w ph   &    |- F/_ w V   &    |- Y = { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }   &    |- P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )   &    |- X = ( seq 1 ( P , U ) ` M )   &    |- F = ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )   &    |- Z = ( t e. T |-> ( seq 1 ( x. , ( F ` t ) ) ` M ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> W : ( 1 ... M ) --> V )   &    |- ( ph -> U : ( 1 ... M ) --> Y )   &    |- ( ( ph /\ w e. V ) -> w C_ T )   &    |- ( ph -> D C_ U. ran W )   &    |- ( ph -> D C_ T )   &    |- ( ph -> B C_ T )   &    |- ( ( ph /\ i e. ( 1 ... M ) ) -> A. t e. ( W ` i ) ( ( U ` i ) ` t ) < ( E / M ) )   &    |- ( ( ph /\ i e. ( 1 ... M ) ) -> A. t e. B ( 1 - ( E / M ) ) < ( ( U ` i ) ` t ) )   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )   &    |- ( ( ph /\ f e. A ) -> f : T --> RR )   &    |- ( ph -> T e. _V )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> E < ( 1 / 3 ) )   =>    |- ( ph -> E. x ( 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	stoweidlem52 37481*	There exists a neighborood V as in Lemma 1 of [BrosowskiDeutsh] p. 90. Here Z is used to represent t0 in the paper, and v is used to represent V in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t U   &    |- F/ t ph   &    |- F/_ t P   &    |- K = ( topGen ` ran (,) )   &    |- V = { t e. T | ( P ` t ) < ( D / 2 ) }   &    |- T = U. J   &    |- C = ( J Cn K )   &    |- ( ph -> A C_ C )   &    |- ( ( 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 /\ a e. RR ) -> ( t e. T |-> a ) e. A )   &    |- ( ph -> D e. RR+ )   &    |- ( ph -> D < 1 )   &    |- ( ph -> U e. J )   &    |- ( ph -> Z e. U )   &    |- ( ph -> P e. A )   &    |- ( ph -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )   &    |- ( ph -> ( P ` Z ) = 0 )   &    |- ( ph -> A. t e. ( T \ U ) D <_ ( P ` t ) )   =>    |- ( ph -> E. v e. J ( ( Z e. v /\ v C_ U ) /\ A. e e. RR+ E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. v ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) ) )
Theorem	stoweidlem53 37482*	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. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t U   &    |- F/ t ph   &    |- K = ( topGen ` ran (,) )   &    |- 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 ) } }   &    |- T = U. J   &    |- C = ( J Cn K )   &    |- ( ph -> J e. Comp )   &    |- ( ph -> A C_ C )   &    |- ( ( 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 /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )   &    |- ( ph -> U e. J )   &    |- ( ph -> ( T \ U ) =/= (/) )   &    |- ( ph -> Z e. U )   =>    |- ( ph -> E. p e. A ( A. t e. T ( 0 <_ ( p ` t ) /\ ( p ` t ) <_ 1 ) /\ ( p ` Z ) = 0 /\ A. t e. ( T \ U ) 0 < ( p ` t ) ) )
Theorem	stoweidlem54 37483*	There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. Here D is used to represent A in the paper, because here A is used for the subalgebra of functions. E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/ i ph   &    |- F/ t ph   &    |- F/ y ph   &    |- F/ w ph   &    |- T = U. J   &    |- Y = { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }   &    |- P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )   &    |- F = ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( y ` i ) ` t ) ) )   &    |- Z = ( t e. T |-> ( seq 1 ( x. , ( F ` t ) ) ` M ) )   &    |- 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 ) ) }   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )   &    |- ( ( ph /\ f e. A ) -> f : T --> RR )   &    |- ( ph -> M e. NN )   &    |- ( ph -> W : ( 1 ... M ) --> V )   &    |- ( ph -> B C_ T )   &    |- ( ph -> D C_ U. ran W )   &    |- ( ph -> D C_ T )   &    |- ( ph -> E. y ( y : ( 1 ... M ) --> Y /\ A. i e. ( 1 ... M ) ( A. t e. ( W ` i ) ( ( y ` i ) ` t ) < ( E / M ) /\ A. t e. B ( 1 - ( E / M ) ) < ( ( y ` i ) ` t ) ) ) )   &    |- ( ph -> T e. _V )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> E < ( 1 / 3 ) )   =>    |- ( 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	stoweidlem55 37484*	This lemma proves the existence of a function p as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p(t_0) = 0, and p > 0 on T - U. Here Z is used to represent t0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t U   &    |- F/ t ph   &    |- K = ( topGen ` ran (,) )   &    |- ( ph -> J e. Comp )   &    |- T = U. J   &    |- C = ( J Cn K )   &    |- ( ph -> A C_ C )   &    |- ( ( 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 /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )   &    |- ( ph -> U e. J )   &    |- ( ph -> Z e. U )   &    |- 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 ) } }   =>    |- ( ph -> E. p e. A ( A. t e. T ( 0 <_ ( p ` t ) /\ ( p ` t ) <_ 1 ) /\ ( p ` Z ) = 0 /\ A. t e. ( T \ U ) 0 < ( p ` t ) ) )
Theorem	stoweidlem56 37485*	This theorem proves Lemma 1 in [BrosowskiDeutsh] p. 90. Here Z is used to represent t0 in the paper, v is used to represent V in the paper, and e is used to represent ε (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t U   &    |- F/ t ph   &    |- K = ( topGen ` ran (,) )   &    |- ( ph -> J e. Comp )   &    |- T = U. J   &    |- C = ( J Cn K )   &    |- ( ph -> A C_ C )   &    |- ( ( 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 /\ y e. RR ) -> ( t e. T |-> y ) e. A )   &    |- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )   &    |- ( ph -> U e. J )   &    |- ( ph -> Z e. U )   =>    |- ( ph -> E. v e. J ( ( Z e. v /\ v C_ U ) /\ A. e e. RR+ E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. v ( x ` t ) < e /\ A. t e. ( T \ U ) ( 1 - e ) < ( x ` t ) ) ) )
Theorem	stoweidlem57 37486*	There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. In this theorem, it is proven the non-trivial case (the closed set D is nonempty). Here D is used to represent A in the paper, because the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t D   &    |- F/_ t U   &    |- F/ t 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 ) ) }   &    |- K = ( topGen ` ran (,) )   &    |- T = U. J   &    |- C = ( J Cn K )   &    |- U = ( T \ B )   &    |- ( ph -> J e. Comp )   &    |- ( ph -> A C_ C )   &    |- ( ( 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 /\ a e. RR ) -> ( t e. T |-> a ) e. A )   &    |- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )   &    |- ( ph -> B e. ( Clsd ` J ) )   &    |- ( ph -> D e. ( Clsd ` J ) )   &    |- ( ph -> ( B i^i D ) = (/) )   &    |- ( ph -> D =/= (/) )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> E < ( 1 / 3 ) )   =>    |- ( 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	stoweidlem58 37487*	This theorem proves Lemma 2 in [BrosowskiDeutsh] p. 91. Here D is used to represent the set A of Lemma 2, because here the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t D   &    |- F/_ t U   &    |- F/ t ph   &    |- K = ( topGen ` ran (,) )   &    |- T = U. J   &    |- C = ( J Cn K )   &    |- ( ph -> J e. Comp )   &    |- ( ph -> A C_ C )   &    |- ( ( 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 /\ a e. RR ) -> ( t e. T |-> a ) e. A )   &    |- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )   &    |- ( ph -> B e. ( Clsd ` J ) )   &    |- ( ph -> D e. ( Clsd ` J ) )   &    |- ( ph -> ( B i^i D ) = (/) )   &    |- U = ( T \ B )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> E < ( 1 / 3 ) )   =>    |- ( 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	stoweidlem59 37488*	This lemma proves that there exists a function x as in the proof in [BrosowskiDeutsh] p. 91, after Lemma 2: xj is in the subalgebra, 0 <= xj <= 1, xj < ε / n on Aj (meaning A in the paper), xj > 1 - \epslon / n on Bj. Here D is used to represent A in the paper (because A is used for the subalgebra of functions), E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t F   &    |- F/ t ph   &    |- K = ( topGen ` ran (,) )   &    |- T = U. J   &    |- C = ( J Cn K )   &    |- 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 ) } )   &    |- Y = { y e. A | A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) }   &    |- H = ( j e. ( 0 ... N ) |-> { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } )   &    |- ( ph -> J e. Comp )   &    |- ( ph -> A C_ C )   &    |- ( ( 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 /\ y e. RR ) -> ( t e. T |-> y ) e. A )   &    |- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )   &    |- ( ph -> F e. C )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> E < ( 1 / 3 ) )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> E. x ( x : ( 0 ... N ) --> A /\ A. j e. ( 0 ... N ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( x ` j ) ` t ) ) ) )
Theorem	stoweidlem60 37489*	This lemma proves that there exists a function g as in the proof in [BrosowskiDeutsh] p. 91 (this parte of the proof actually spans through pages 91-92): g is in the subalgebra, and for all t in T, there is a j such that (j-4/3)*ε < f(t) <= (j-1/3)*ε and (j-4/3)*ε < g(t) < (j+1/3)*ε. Here F is used to represent f in the paper, and E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t F   &    |- F/ t ph   &    |- K = ( topGen ` ran (,) )   &    |- T = U. J   &    |- C = ( J Cn K )   &    |- 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 -> J e. Comp )   &    |- ( ph -> T =/= (/) )   &    |- ( ph -> A C_ C )   &    |- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t