HomeHome Metamath Proof Explorer
Theorem List (p. 380 of 409)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-26620)
  Hilbert Space Explorer  Hilbert Space Explorer
(26621-28143)
  Users' Mathboxes  Users' Mathboxes
(28144-40813)
 

Theorem List for Metamath Proof Explorer - 37901-38000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremstoweidlem3 37901* Lemma for stoweid 37963: 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 ) )
 
Theoremstoweidlem4 37902* Lemma for stoweid 37963: 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 )
 
Theoremstoweidlem5 37903* 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
 ) ) )
 
Theoremstoweidlem6 37904* Lemma for stoweid 37963: 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 )
 
Theoremstoweidlem7 37905* 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 ) )
 
Theoremstoweidlem8 37906* Lemma for stoweid 37963: 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 )
 
Theoremstoweidlem9 37907* Lemma for stoweid 37963: 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 )
 
Theoremstoweidlem10 37908 Lemma for stoweid 37963. 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 ) )
 
Theoremstoweidlem11 37909* 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 ) )
 
Theoremstoweidlem12 37910* Lemma for stoweid 37963. 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 ) ) )
 
Theoremstoweidlem13 37911 Lemma for stoweid 37963. 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 ) )
 
Theoremstoweidlem14 37912* 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
 ) )
 
Theoremstoweidlem15 37913* 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 ) )
 
Theoremstoweidlem16 37914* Lemma for stoweid 37963. 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 )
 
Theoremstoweidlem17 37915* 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 )
 
Theoremstoweidlem18 37916* 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 ) ) )
 
Theoremstoweidlem19 37917* 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 )
 
Theoremstoweidlem20 37918* 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 )
 
Theoremstoweidlem21 37919* 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 )
 
Theoremstoweidlem22 37920* 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 )
 
Theoremstoweidlem23 37921* 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 ) )
 
Theoremstoweidlem24 37922* 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 ) )
 
Theoremstoweidlem25 37923* 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 )
 
Theoremstoweidlem26 37924* 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 ) )
 
Theoremstoweidlem27 37925* 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 ) ) ) )
 
Theoremstoweidlem28 37926* 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
 ) ) )
 
Theoremstoweidlem29 37927* 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 ) ) )
 
Theoremstoweidlem29OLD 37928* 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 37927 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 ) ) )
 
Theoremstoweidlem30 37929* 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 )
 ) )
 
Theoremstoweidlem31 37930* 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 ) ) ) )
 
Theoremstoweidlem32 37931* 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 )
 
Theoremstoweidlem33 37932* 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 )
 
Theoremstoweidlem34 37933* 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 ) ) ) )
 
Theoremstoweidlem35 37934* 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
 ) ) ) )
 
Theoremstoweidlem36 37935* 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 ) ) )
 
Theoremstoweidlem37 37936* 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 )
 
Theoremstoweidlem38 37937* 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 ) )
 
Theoremstoweidlem39 37938* 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 ) ) ) ) )
 
Theoremstoweidlem40 37939* 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 )
 
Theoremstoweidlem41 37940* 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 ) ) )
 
Theoremstoweidlem42 37941* 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 ) )
 
Theoremstoweidlem43 37942* 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 ) ) )
 
Theoremstoweidlem44 37943* 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 ) ) )
 
Theoremstoweidlem45 37944* 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 ) )
 
Theoremstoweidlem46 37945* 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 )
 
Theoremstoweidlem47 37946* 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 )
 
Theoremstoweidlem48 37947* 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 )
 
Theoremstoweidlem49 37948* 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 ) )
 
Theoremstoweidlem50 37949* 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 ) )
 
Theoremstoweidlem51 37950* 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 ) ) ) )
 
Theoremstoweidlem52 37951* 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
 ) ) ) )
 
Theoremstoweidlem53 37952* 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 ) ) )
 
Theoremstoweidlem54 37953* 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 ) ) )
 
Theoremstoweidlem55 37954* 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 ) ) )
 
Theoremstoweidlem56 37955* 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
 ) ) ) )
 
Theoremstoweidlem57 37956* 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 ) ) )
 
Theoremstoweidlem58 37957* 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 ) ) )
 
Theoremstoweidlem59 37958* 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 ) ) ) )
 
Theoremstoweidlem60 37959* 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 ) ) ) )
 
Theoremstoweidlem61 37960* 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 ) )
 
Theoremstoweidlem62 37961* 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 )
 
Theoremstoweidlem62OLD 37962* 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.) Obsolete version of stoweidlem62 37961 as of 13-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
 |-  F/_ t F   &    |- 
 F/ f ph   &    |-  F/ t ph   &    |-  H  =  ( t  e.  T  |->  ( ( F `  t )  -  sup ( 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 )
 
Theoremstoweid 37963* 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 )
 
Theoremstowei 37964* 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 37963: often times it will be better to use stoweid 37963 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
 
21.30.13  Wallis' product for π
 
Theoremwallispilem1 37965*  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 ) )
 
Theoremwallispilem2 37966* 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
 ) ) ) ) )
 
Theoremwallispilem3 37967* 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+ )
 
Theoremwallispilem4 37968*  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
 
Theoremwallispilem5 37969* 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
 
Theoremwallispi 37970* 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 )
 
Theoremwallispi2lem1 37971 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 ) ) )
 
Theoremwallispi2lem2 37972 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 ) ) )
 
Theoremwallispi2 37973 An alternative version of Wallis' formula for π ; this second formula uses factorials and it is later used to proof 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 )
 
21.30.14  Stirling's approximation formula for ` n ` factorial
 
Theoremstirlinglem1 37974 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 )
 
Theoremstirlinglem2 37975  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+ )
 
Theoremstirlinglem3 37976 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 ) ) ) ) )
 
Theoremstirlinglem4 37977* 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  |->