P. 403 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40201-40300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sublevolico 40201	The Lebesgue measure of a left-closed, right-open interval is greater or equal to the difference of the two bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( B - A ) <_ ( vol ` ( A [,) B ) ) )
Theorem	dmvolss 40202	Lebesgue measurable sets are subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- dom vol C_ ~P RR
Theorem	ismbl3 40203*	The predicate " A is Lebesgue-measurable". Similar to ismbl2 23295, but here +e is used, and the precondition ( vol* ` x ) e. RR can be dropped. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( A e. dom vol <-> ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) )
Theorem	volioof 40204	The function that assigns the Lebesgue measure to open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( vol o. (,) ) : ( RR* X. RR* ) --> ( 0 [,] +oo )
Theorem	ovolsplit 40205	The Lebesgue outer measure function is finitely sub-additive: application to a set split in two parts, using addition for extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A C_ RR )   =>    |- ( ph -> ( vol* ` A ) <_ ( ( vol* ` ( A i^i B ) ) +e ( vol* ` ( A \ B ) ) ) )
Theorem	fvvolioof 40206	The function value of the Lebesgue measure of an open interval composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> F : A --> ( RR* X. RR* ) )   &    |- ( ph -> X e. A )   =>    |- ( ph -> ( ( ( vol o. (,) ) o. F ) ` X ) = ( vol ` ( ( 1st ` ( F ` X ) ) (,) ( 2nd ` ( F ` X ) ) ) ) )
Theorem	volioore 40207	The measure of an open interval. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A (,) B ) ) = if ( A <_ B , ( B - A ) , 0 ) )
Theorem	fvvolicof 40208	The function value of the Lebesgue measure of a left-closed right-open interval composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> F : A --> ( RR* X. RR* ) )   &    |- ( ph -> X e. A )   =>    |- ( ph -> ( ( ( vol o. [,) ) o. F ) ` X ) = ( vol ` ( ( 1st ` ( F ` X ) ) [,) ( 2nd ` ( F ` X ) ) ) ) )
Theorem	voliooico 40209	An open interval and a left-closed, right-open interval with the same real bounds, have the same Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( vol ` ( A (,) B ) ) = ( vol ` ( A [,) B ) ) )
Theorem	ismbl4 40210*	The predicate " A is Lebesgue-measurable". Similar to ismbl 23294, but here +e is used, and the precondition ( vol* ` x ) e. RR can be dropped. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( A e. dom vol <-> ( A C_ RR /\ A. x e. ~P RR ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) ) )
Theorem	volioofmpt 40211*	( ( vol o. (,) ) o. F ) expressed in map-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- F/_ x F   &    |- ( ph -> F : A --> ( RR* X. RR* ) )   =>    |- ( ph -> ( ( vol o. (,) ) o. F ) = ( x e. A |-> ( vol ` ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) ) ) )
Theorem	volicoff 40212	( ( vol o. [,) ) o. F ) expressed in map-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> F : A --> ( RR X. RR* ) )   =>    |- ( ph -> ( ( vol o. [,) ) o. F ) : A --> ( 0 [,] +oo ) )
Theorem	voliooicof 40213	The Lebesgue measure of open intervals is the same as the Lebesgue measure of left-closed right open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> F : A --> ( RR X. RR ) )   =>    |- ( ph -> ( ( vol o. (,) ) o. F ) = ( ( vol o. [,) ) o. F ) )
Theorem	volicofmpt 40214*	( ( vol o. [,) ) o. F ) expressed in map-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- F/_ x F   &    |- ( ph -> F : A --> ( RR X. RR* ) )   =>    |- ( ph -> ( ( vol o. [,) ) o. F ) = ( x e. A |-> ( vol ` ( ( 1st ` ( F ` x ) ) [,) ( 2nd ` ( F ` x ) ) ) ) ) )
Theorem	volicc 40215	The Lebesgue measure of a closed interval. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol ` ( A [,] B ) ) = ( B - A ) )
Theorem	voliccico 40216	A closed interval and a left-closed, right-open interval with the same real bounds, have the same Lebesgue measure. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( vol ` ( A [,] B ) ) = ( vol ` ( A [,) B ) ) )
Theorem	mbfdmssre 40217	The domain of a measurable function is a subset of the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( F e. MblFn -> dom F C_ RR )
20.32.12  Stone Weierstrass theorem - real version
Theorem	stoweidlem1 40218	Lemma for stoweid 40280. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90; the key step uses Bernoulli's inequality bernneq 12990. (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 40219*	lemma for stoweid 40280: 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 40220*	Lemma for stoweid 40280: 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 40221*	Lemma for stoweid 40280: 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 40222*	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 40223*	Lemma for stoweid 40280: 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 40224*	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 40225*	Lemma for stoweid 40280: 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 40226*	Lemma for stoweid 40280: 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 40227	Lemma for stoweid 40280. 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 40228*	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 40229*	Lemma for stoweid 40280. 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 40230	Lemma for stoweid 40280. 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 40231*	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 40232*	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 40233*	Lemma for stoweid 40280. 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 40234*	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 40235*	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 40236*	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 40237*	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 40238*	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 40239*	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 40240*	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 40241*	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 40242*	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 40243*	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 40244*	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 40245*	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 40246*	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	stoweidlem30 40247*	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 40248*	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 40249*	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 40250*	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 40251*	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 40252*	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 40253*	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 40254*	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 40255*	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 40256*	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 40257*	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 40258*	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 40259*	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 40260*	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 40261*	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 40262*	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 40263*	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 40264*	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 40265*	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 40266*	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 40267*	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 40268*	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 40269*	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 40270*	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 40271*	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 40272*	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 40273*	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 40274*	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 40275*	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 40276*	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 40277*	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 ) + ( 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 -> A. t e. T 0 <_ ( F ` t ) )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> E < ( 1 / 3 ) )   =>    |- ( ph -> E. g e. A A. t e. T E. j e. RR ( ( ( ( j - ( 4 / 3 ) ) x. E ) < ( F ` t ) /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) /\ ( ( g ` t ) < ( ( j + ( 1 / 3 ) ) x. E ) /\ ( ( j - ( 4 / 3 ) ) x. E ) < ( g ` t ) ) ) )
Theorem	stoweidlem61 40278*	This lemma proves that there exists a function g as in the proof in [BrosowskiDeutsh] p. 92: g is in the subalgebra, and for all t in T, abs( f(t) - g(t) ) < 2*ε. Here F is used to represent f in the paper, and E is used to represent ε. For this lemma there's the further assumption that the function F to be approximated is nonnegative (this assumption is removed in a later theorem). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t F   &    |- F/ t ph   &    |- K = ( topGen ` ran (,) )   &    |- ( ph -> J e. Comp )   &    |- T = U. J   &    |- ( ph -> T =/= (/) )   &    |- 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 -> F e. C )   &    |- ( ph -> A. t e. T 0 <_ ( F ` t ) )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> E < ( 1 / 3 ) )   =>    |- ( ph -> E. g e. A A. t e. T ( abs ` ( ( g ` t ) - ( F ` t ) ) ) < ( 2 x. E ) )
Theorem	stoweidlem62 40279*	This theorem proves the Stone Weierstrass theorem for the non-trivial case in which T is nonempty. The proof follows [BrosowskiDeutsh] p. 89 (through page 92). (Contributed by Glauco Siliprandi, 20-Apr-2017.) (Revised by AV, 13-Sep-2020.)
|- F/_ t F   &    |- F/ f ph   &    |- F/ t ph   &    |- H = ( t e. T |-> ( ( F ` t ) - inf ( ran F , RR , < ) ) )   &    |- K = ( topGen ` ran (,) )   &    |- T = U. J   &    |- ( ph -> J e. Comp )   &    |- 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 -> F e. C )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> T =/= (/) )   &    |- ( ph -> E < ( 1 / 3 ) )   =>    |- ( ph -> E. f e. A A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < E )
Theorem	stoweid 40280*	This theorem proves the Stone-Weierstrass theorem for real-valued functions: let J be a compact topology on T, and C be the set of real continuous functions on T. Assume that A is a subalgebra of C (closed under addition and multiplication of functions) containing constant functions and discriminating points (if r and t are distinct points in T, then there exists a function h in A such that h(r) is distinct from h(t) ). Then, for any continuous function F and for any positive real E, there exists a function f in the subalgebra A, such that f approximates F up to E ( E represents the usual ε value). As a classical example, given any a, b reals, the closed interval T = [ a , b ] could be taken, along with the subalgebra A of real polynomials on T, and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on [ a , b ]. The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- F/_ t F   &    |- 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. h e. A ( h ` r ) =/= ( h ` t ) )   &    |- ( ph -> F e. C )   &    |- ( ph -> E e. RR+ )   =>    |- ( ph -> E. f e. A A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < E )
Theorem	stowei 40281*	This theorem proves the Stone-Weierstrass theorem for real-valued functions: let J be a compact topology on T, and C be the set of real continuous functions on T. Assume that A is a subalgebra of C (closed under addition and multiplication of functions) containing constant functions and discriminating points (if r and t are distinct points in T, then there exists a function h in A such that h(r) is distinct from h(t) ). Then, for any continuous function F and for any positive real E, there exists a function f in the subalgebra A, such that f approximates F up to E ( E represents the usual ε value). As a classical example, given any a, b reals, the closed interval T = [ a , b ] could be taken, along with the subalgebra A of real polynomials on T, and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on [ a , b ]. The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. The deduction version of this theorem is stoweid 40280: often times it will be better to use stoweid 40280 in other proofs (but this version is probably easier to be read and understood). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
|- K = ( topGen ` ran (,) )   &    |- J e. Comp   &    |- T = U. J   &    |- C = ( J Cn K )   &    |- A C_ C   &    |- ( ( f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )   &    |- ( ( f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )   &    |- ( x e. RR -> ( t e. T |-> x ) e. A )   &    |- ( ( r e. T /\ t e. T /\ r =/= t ) -> E. h e. A ( h ` r ) =/= ( h ` t ) )   &    |- F e. C   &    |- E e. RR+   =>    |- E. f e. A A. t e. T ( abs ` ( ( f ` t ) - ( F ` t ) ) ) < E
20.32.13  Wallis' product for π
Theorem	wallispilem1 40282*	I is monotone: increasing the exponent, the integral decreases. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- I = ( n e. NN0 |-> S. ( 0 (,) pi ) ( ( sin ` x ) ^ n ) _d x )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( I ` ( N + 1 ) ) <_ ( I ` N ) )
Theorem	wallispilem2 40283*	A first set of properties for the sequence I that will be used in the proof of the Wallis product formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- I = ( n e. NN0 |-> S. ( 0 (,) pi ) ( ( sin ` x ) ^ n ) _d x )   =>    |- ( ( I ` 0 ) = pi /\ ( I ` 1 ) = 2 /\ ( N e. ( ZZ>= ` 2 ) -> ( I ` N ) = ( ( ( N - 1 ) / N ) x. ( I ` ( N - 2 ) ) ) ) )
Theorem	wallispilem3 40284*	I maps to real values. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- I = ( n e. NN0 |-> S. ( 0 (,) pi ) ( ( sin ` x ) ^ n ) _d x )   =>    |- ( N e. NN0 -> ( I ` N ) e. RR+ )
Theorem	wallispilem4 40285*	F maps to explicit expression for the ratio of two consecutive values of I. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
|- F = ( k e. NN |-> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) )   &    |- I = ( n e. NN0 |-> S. ( 0 (,) pi ) ( ( sin ` z ) ^ n ) _d z )   &    |- G = ( n e. NN |-> ( ( I ` ( 2 x. n ) ) / ( I ` ( ( 2 x. n ) + 1 ) ) ) )   &    |- H = ( n e. NN |-> ( ( pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) )   =>    |- G = H
Theorem	wallispilem5 40286*	The sequence H converges to 1. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
|- F = ( k e. NN |-> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) )   &    |- I = ( n e. NN0 |-> S. ( 0 (,) pi ) ( ( sin ` x ) ^ n ) _d x )   &    |- G = ( n e. NN |-> ( ( I ` ( 2 x. n ) ) / ( I ` ( ( 2 x. n ) + 1 ) ) ) )   &    |- H = ( n e. NN |-> ( ( pi / 2 ) x. ( 1 / ( seq 1 ( x. , F ) ` n ) ) ) )   &    |- L = ( n e. NN |-> ( ( ( 2 x. n ) + 1 ) / ( 2 x. n ) ) )   =>    |- H ~~> 1
Theorem	wallispi 40287*	Wallis' formula for π : Wallis' product converges to π / 2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- F = ( k e. NN |-> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) )   &    |- W = ( n e. NN |-> ( seq 1 ( x. , F ) ` n ) )   =>    |- W ~~> ( pi / 2 )
Theorem	wallispi2lem1 40288	An intermediate step between the first version of the Wallis' formula for π and the second version of Wallis' formula. This second version will then be used to prove Stirling's approximation formula for the factorial. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
|- ( N e. NN -> ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) / ( ( 2 x. k ) - 1 ) ) x. ( ( 2 x. k ) / ( ( 2 x. k ) + 1 ) ) ) ) ) ` N ) = ( ( 1 / ( ( 2 x. N ) + 1 ) ) x. ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` N ) ) )
Theorem	wallispi2lem2 40289	Two expressions are proven to be equal, and this is used to complete the proof of the second version of Wallis' formula for π . (Contributed by Glauco Siliprandi, 30-Jun-2017.)
|- ( N e. NN -> ( seq 1 ( x. , ( k e. NN |-> ( ( ( 2 x. k ) ^ 4 ) / ( ( ( 2 x. k ) x. ( ( 2 x. k ) - 1 ) ) ^ 2 ) ) ) ) ` N ) = ( ( ( 2 ^ ( 4 x. N ) ) x. ( ( ! ` N ) ^ 4 ) ) / ( ( ! ` ( 2 x. N ) ) ^ 2 ) ) )
Theorem	wallispi2 40290	An alternative version of Wallis' formula for π ; this second formula uses factorials and it is later used to prove Stirling's approximation formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- V = ( n e. NN |-> ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) )   =>    |- V ~~> ( pi / 2 )
20.32.14  Stirling's approximation formula for ` n ` factorial
Theorem	stirlinglem1 40291	A simple limit of fractions is computed. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
|- H = ( n e. NN |-> ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) )   &    |- F = ( n e. NN |-> ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) )   &    |- G = ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) )   &    |- L = ( n e. NN |-> ( 1 / n ) )   =>    |- H ~~> ( 1 / 2 )
Theorem	stirlinglem2 40292	A maps to positive reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )   =>    |- ( N e. NN -> ( A ` N ) e. RR+ )
Theorem	stirlinglem3 40293	Long but simple algebraic transformations are applied to show that V, the Wallis formula for π , can be expressed in terms of A, the Stirling's approximation formula for the factorial, up to a constant factor. This will allow (in a later theorem) to determine the right constant factor to be put into the A, in order to get the exact Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )   &    |- D = ( n e. NN |-> ( A ` ( 2 x. n ) ) )   &    |- E = ( n e. NN |-> ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) )   &    |- V = ( n e. NN |-> ( ( ( ( 2 ^ ( 4 x. n ) ) x. ( ( ! ` n ) ^ 4 ) ) / ( ( ! ` ( 2 x. n ) ) ^ 2 ) ) / ( ( 2 x. n ) + 1 ) ) )   =>    |- V = ( n e. NN |-> ( ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) x. ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) )
Theorem	stirlinglem4 40294*	Algebraic manipulation of ( ( B n ) - ( B ( n + 1 ) ) ). It will be used in other theorems to show that B is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )   &    |- B = ( n e. NN |-> ( log ` ( A ` n ) ) )   &    |- J = ( n e. NN |-> ( ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) - 1 ) )   =>    |- ( N e. NN -> ( ( B ` N ) - ( B ` ( N + 1 ) ) ) = ( J ` N ) )
Theorem	stirlinglem5 40295*	If T is between 0 and 1, then a series (without alternating negative and positive terms) is given that converges to log (1+T)/(1-T) . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- D = ( j e. NN |-> ( ( -u 1 ^ ( j - 1 ) ) x. ( ( T ^ j ) / j ) ) )   &    |- E = ( j e. NN |-> ( ( T ^ j ) / j ) )   &    |- F = ( j e. NN |-> ( ( ( -u 1 ^ ( j - 1 ) ) x. ( ( T ^ j ) / j ) ) + ( ( T ^ j ) / j ) ) )   &    |- H = ( j e. NN0 |-> ( 2 x. ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( T ^ ( ( 2 x. j ) + 1 ) ) ) ) )   &    |- G = ( j e. NN0 |-> ( ( 2 x. j ) + 1 ) )   &    |- ( ph -> T e. RR+ )   &    |- ( ph -> ( abs ` T ) < 1 )   =>    |- ( ph -> seq 0 ( + , H ) ~~> ( log ` ( ( 1 + T ) / ( 1 - T ) ) ) )
Theorem	stirlinglem6 40296*	A series that converges to log (N+1)/N. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- H = ( j e. NN0 |-> ( 2 x. ( ( 1 / ( ( 2 x. j ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. j ) + 1 ) ) ) ) )   =>    |- ( N e. NN -> seq 0 ( + , H ) ~~> ( log ` ( ( N + 1 ) / N ) ) )
Theorem	stirlinglem7 40297*	Algebraic manipulation of the formula for J(n). (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- J = ( n e. NN |-> ( ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) - 1 ) )   &    |- K = ( k e. NN |-> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) )   &    |- H = ( k e. NN0 |-> ( 2 x. ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( ( 2 x. k ) + 1 ) ) ) ) )   =>    |- ( N e. NN -> seq 1 ( + , K ) ~~> ( J ` N ) )
Theorem	stirlinglem8 40298	If A converges to C, then F converges to C^2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- F/ n ph   &    |- F/_ n A   &    |- F/_ n D   &    |- D = ( n e. NN |-> ( A ` ( 2 x. n ) ) )   &    |- ( ph -> A : NN --> RR+ )   &    |- F = ( n e. NN |-> ( ( ( A ` n ) ^ 4 ) / ( ( D ` n ) ^ 2 ) ) )   &    |- L = ( n e. NN |-> ( ( A ` n ) ^ 4 ) )   &    |- M = ( n e. NN |-> ( ( D ` n ) ^ 2 ) )   &    |- ( ( ph /\ n e. NN ) -> ( D ` n ) e. RR+ )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> A ~~> C )   =>    |- ( ph -> F ~~> ( C ^ 2 ) )
Theorem	stirlinglem9 40299*	( ( B ` N ) - ( B ` ( N + 1 ) ) ) is expressed as a limit of a series. This result will be used both to prove that B is decreasing and to prove that B is bounded (below). It will follow that B converges in the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )   &    |- B = ( n e. NN |-> ( log ` ( A ` n ) ) )   &    |- J = ( n e. NN |-> ( ( ( ( 1 + ( 2 x. n ) ) / 2 ) x. ( log ` ( ( n + 1 ) / n ) ) ) - 1 ) )   &    |- K = ( k e. NN |-> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) )   =>    |- ( N e. NN -> seq 1 ( + , K ) ~~> ( ( B ` N ) - ( B ` ( N + 1 ) ) ) )
Theorem	stirlinglem10 40300*	A bound for any B(N)-B(N + 1) that will allow to find a lower bound for the whole B sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|- A = ( n e. NN |-> ( ( ! ` n ) / ( ( sqr ` ( 2 x. n ) ) x. ( ( n / _e ) ^ n ) ) ) )   &    |- B = ( n e. NN |-> ( log ` ( A ` n ) ) )   &    |- K = ( k e. NN |-> ( ( 1 / ( ( 2 x. k ) + 1 ) ) x. ( ( 1 / ( ( 2 x. N ) + 1 ) ) ^ ( 2 x. k ) ) ) )   &    |- L = ( k e. NN |-> ( ( 1 / ( ( ( 2 x. N ) + 1 ) ^ 2 ) ) ^ k ) )   =>    |- ( N e. NN -> ( ( B ` N ) - ( B ` ( N + 1 ) ) ) <_ ( ( 1 / 4 ) x. ( 1 / ( N x. ( N + 1 ) ) ) ) )