HomeHome Metamath Proof Explorer
Theorem List (p. 378 of 402)
< 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-26506)
  Hilbert Space Explorer  Hilbert Space Explorer
(26507-28029)
  Users' Mathboxes  Users' Mathboxes
(28030-40127)
 

Theorem List for Metamath Proof Explorer - 37701-37800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremdvnprod 37701* The multinomial formula for the  N-th derivative of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
 |-  ( ph  ->  S  e.  { RR ,  CC } )   &    |-  ( ph  ->  X  e.  (
 ( TopOpen ` fld )t  S ) )   &    |-  ( ph  ->  T  e.  Fin )   &    |-  ( ( ph  /\  t  e.  T )  ->  ( H `  t ) : X --> CC )   &    |-  ( ph  ->  N  e.  NN0 )   &    |-  ( ( ph  /\  t  e.  T  /\  k  e.  ( 0 ... N ) )  ->  ( ( S  Dn ( H `  t ) ) `  k ) : X --> CC )   &    |-  F  =  ( x  e.  X  |->  prod_ t  e.  T  ( ( H `  t
 ) `  x )
 )   &    |-  C  =  ( n  e.  NN0  |->  { c  e.  ( ( 0 ... n )  ^m  T )  |  sum_ t  e.  T  ( c `  t )  =  n } )   =>    |-  ( ph  ->  (
 ( S  Dn F ) `  N )  =  ( x  e.  X  |->  sum_ c  e.  ( C `  N ) ( ( ( ! `  N )  /  prod_ t  e.  T  ( ! `  ( c `  t
 ) ) )  x. 
 prod_ t  e.  T  ( ( ( S  Dn ( H `
  t ) ) `
  ( c `  t ) ) `  x ) ) ) )
 
21.30.11  Integrals
 
Theoremvolioo 37702 The measure of an open interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR  /\  A  <_  B )  ->  ( vol `  ( A (,) B ) )  =  ( B  -  A ) )
 
Theoremitgsin0pilem1 37703* Calculation of the integral for sine on the (0,π) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  C  =  ( t  e.  (
 0 [,] pi )  |->  -u ( cos `  t )
 )   =>    |- 
 S. ( 0 (,)
 pi ) ( sin `  x )  _d x  =  2
 
Theoremibliccsinexp 37704* sin^n on a closed interval is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR  /\  N  e.  NN0 )  ->  ( x  e.  ( A [,] B )  |->  ( ( sin `  x ) ^ N ) )  e.  L^1 )
 
Theoremitgsin0pi 37705 Calculation of the integral for sine on the (0,π) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  S. ( 0 (,) pi ) ( sin `  x )  _d x  =  2
 
Theoremiblioosinexp 37706* sin^n on an open integral is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR  /\  N  e.  NN0 )  ->  ( x  e.  ( A (,) B )  |->  ( ( sin `  x ) ^ N ) )  e.  L^1 )
 
Theoremitgsinexplem1 37707* Integration by parts is applied to integrate sin^(N+1). (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F  =  ( x  e.  CC  |->  ( ( sin `  x ) ^ N ) )   &    |-  G  =  ( x  e.  CC  |->  -u ( cos `  x ) )   &    |-  H  =  ( x  e.  CC  |->  ( ( N  x.  (
 ( sin `  x ) ^ ( N  -  1 ) ) )  x.  ( cos `  x ) ) )   &    |-  I  =  ( x  e.  CC  |->  ( ( ( sin `  x ) ^ N )  x.  ( sin `  x ) ) )   &    |-  L  =  ( x  e.  CC  |->  ( ( ( N  x.  ( ( sin `  x ) ^ ( N  -  1 ) ) )  x.  ( cos `  x ) )  x.  -u ( cos `  x ) ) )   &    |-  M  =  ( x  e.  CC  |->  ( ( ( cos `  x ) ^ 2
 )  x.  ( ( sin `  x ) ^ ( N  -  1 ) ) ) )   &    |-  ( ph  ->  N  e.  NN )   =>    |-  ( ph  ->  S. ( 0 (,) pi ) ( ( ( sin `  x ) ^ N )  x.  ( sin `  x ) )  _d x  =  ( N  x.  S. (
 0 (,) pi ) ( ( ( cos `  x ) ^ 2 )  x.  ( ( sin `  x ) ^ ( N  -  1 ) ) )  _d x ) )
 
Theoremitgsinexp 37708* A recursive formula for the integral of sin^N on the interval (0,π) . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  I  =  ( n  e.  NN0  |->  S. ( 0 (,) pi ) ( ( sin `  x ) ^ n )  _d x )   &    |-  ( ph  ->  N  e.  ( ZZ>=
 `  2 ) )   =>    |-  ( ph  ->  ( I `  N )  =  ( ( ( N  -  1 )  /  N )  x.  ( I `  ( N  -  2
 ) ) ) )
 
Theoremiblconstmpt 37709* A constant function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  (
 ( A  e.  dom  vol  /\  ( vol `  A )  e.  RR  /\  B  e.  CC )  ->  ( x  e.  A  |->  B )  e.  L^1 )
 
Theoremitgeq1d 37710* Equality theorem for an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  S. A C  _d x  =  S. B C  _d x )
 
Theoremmbf0 37711 The empty set is a measurable function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  (/)  e. MblFn
 
Theoremmbfres2cn 37712 Measurability of a piecewise function: if  F is measurable on subsets  B and  C of its domain, and these pieces make up all of  A, then  F is measurable on the whole domain. Similar to mbfres2 22536 but here the theorem is extended to complex valued functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : A --> CC )   &    |-  ( ph  ->  ( F  |`  B )  e. MblFn )   &    |-  ( ph  ->  ( F  |`  C )  e. MblFn )   &    |-  ( ph  ->  ( B  u.  C )  =  A )   =>    |-  ( ph  ->  F  e. MblFn )
 
Theoremvol0 37713 The measure of the empty set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( vol `  (/) )  =  0
 
Theoremditgeqiooicc 37714* A function  F on an open interval, has the same directed integral as its extension  G on the closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  G  =  ( x  e.  ( A [,] B )  |->  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `  x ) ) ) )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <_  B )   &    |-  ( ph  ->  F : ( A (,) B ) --> RR )   =>    |-  ( ph  ->  S__
 [ A  ->  B ] ( F `  x )  _d x  =  S__ [ A  ->  B ] ( G `  x )  _d x )
 
Theoremvolge0 37715 The volume of a set is always nonnegative. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( A  e.  dom  vol  ->  0 
 <_  ( vol `  A ) )
 
Theoremcnbdibl 37716* A continuous bounded function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  dom  vol )   &    |-  ( ph  ->  ( vol `  A )  e.  RR )   &    |-  ( ph  ->  F  e.  ( A -cn-> CC ) )   &    |-  ( ph  ->  E. x  e.  RR  A. y  e.  dom  F ( abs `  ( F `  y ) )  <_  x )   =>    |-  ( ph  ->  F  e.  L^1 )
 
Theoremsnmbl 37717 A singleton is measurable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( A  e.  RR  ->  { A }  e.  dom  vol )
 
Theoremditgeq3d 37718* Equality theorem for the directed integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  <_  B )   &    |-  ( ( ph  /\  x  e.  ( A (,) B ) )  ->  D  =  E )   =>    |-  ( ph  ->  S__ [ A  ->  B ] D  _d x  =  S__ [ A  ->  B ] E  _d x )
 
Theoremiblempty 37719 The empty function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  (/)  e.  L^1
 
Theoremiblsplit 37720* The union of two integrable functions is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  ( vol* `  ( A  i^i  B ) )  =  0
 )   &    |-  ( ph  ->  U  =  ( A  u.  B ) )   &    |-  ( ( ph  /\  x  e.  U ) 
 ->  C  e.  CC )   &    |-  ( ph  ->  ( x  e.  A  |->  C )  e.  L^1 )   &    |-  ( ph  ->  ( x  e.  B  |->  C )  e.  L^1 )   =>    |-  ( ph  ->  ( x  e.  U  |->  C )  e.  L^1 )
 
Theoremvolsn 37721 A singleton has 0 Lebesgue measure. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( A  e.  RR  ->  ( vol `  { A }
 )  =  0 )
 
Theoremitgvol0 37722* If the domani is negligible, the function is integrable and the integral is 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  C_  RR )   &    |-  ( ph  ->  ( vol* `  A )  =  0 )   &    |-  (
 ( ph  /\  x  e.  A )  ->  B  e.  CC )   =>    |-  ( ph  ->  (
 ( x  e.  A  |->  B )  e.  L^1  /\  S. A B  _d x  =  0
 ) )
 
Theoremitgcoscmulx 37723* Exercise: the integral of  x  |->  cos a x on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  B  <_  C )   &    |-  ( ph  ->  A  =/=  0 )   =>    |-  ( ph  ->  S. ( B (,) C ) ( cos `  ( A  x.  x ) )  _d x  =  ( ( ( sin `  ( A  x.  C ) )  -  ( sin `  ( A  x.  B ) ) )  /  A ) )
 
Theoremiblsplitf 37724* A version of iblsplit 37720 using bound-variable hypotheses instead of distinct variable conditions" (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  F/ x ph   &    |-  ( ph  ->  ( vol* `  ( A  i^i  B ) )  =  0 )   &    |-  ( ph  ->  U  =  ( A  u.  B ) )   &    |-  ( ( ph  /\  x  e.  U ) 
 ->  C  e.  CC )   &    |-  ( ph  ->  ( x  e.  A  |->  C )  e.  L^1 )   &    |-  ( ph  ->  ( x  e.  B  |->  C )  e.  L^1 )   =>    |-  ( ph  ->  ( x  e.  U  |->  C )  e.  L^1 )
 
Theoremibliooicc 37725* If a function is integrable on an open interval, it is integrable on the corresponding closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  ( x  e.  ( A (,) B )  |->  C )  e.  L^1 )   &    |-  ( ( ph  /\  x  e.  ( A [,] B ) ) 
 ->  C  e.  CC )   =>    |-  ( ph  ->  ( x  e.  ( A [,] B )  |->  C )  e.  L^1 )
 
Theoremvolioc 37726 The measure of left open, right closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR  /\  A  <_  B )  ->  ( vol `  ( A (,] B ) )  =  ( B  -  A ) )
 
Theoremiblspltprt 37727* If a function is integrable on any interval of a partition, then it is integrable on the whole interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  F/ t ph   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  N  e.  ( ZZ>=
 `  ( M  +  1 ) ) )   &    |-  ( ( ph  /\  i  e.  ( M ... N ) )  ->  ( P `
  i )  e. 
 RR )   &    |-  ( ( ph  /\  i  e.  ( M..^ N ) )  ->  ( P `  i )  <  ( P `  ( i  +  1
 ) ) )   &    |-  (
 ( ph  /\  t  e.  ( ( P `  M ) [,] ( P `  N ) ) )  ->  A  e.  CC )   &    |-  ( ( ph  /\  i  e.  ( M..^ N ) )  ->  ( t  e.  (
 ( P `  i
 ) [,] ( P `  ( i  +  1
 ) ) )  |->  A )  e.  L^1 )   =>    |-  ( ph  ->  (
 t  e.  ( ( P `  M ) [,] ( P `  N ) )  |->  A )  e.  L^1 )
 
Theoremitgsincmulx 37728* Exercise: the integral of  x  |->  sin a x on an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  A  =/=  0 )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  B  <_  C )   =>    |-  ( ph  ->  S. ( B (,) C ) ( sin `  ( A  x.  x ) )  _d x  =  ( ( ( cos `  ( A  x.  B ) )  -  ( cos `  ( A  x.  C ) ) )  /  A ) )
 
Theoremitgsubsticclem 37729* lemma for itgsubsticc 37730. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  F  =  ( u  e.  ( K [,] L )  |->  C )   &    |-  G  =  ( u  e.  RR  |->  if ( u  e.  ( K [,] L ) ,  ( F `  u ) ,  if ( u  <  K ,  ( F `  K ) ,  ( F `  L ) ) ) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  Y  e.  RR )   &    |-  ( ph  ->  X  <_  Y )   &    |-  ( ph  ->  ( x  e.  ( X [,] Y )  |->  A )  e.  ( ( X [,] Y ) -cn-> ( K [,] L ) ) )   &    |-  ( ph  ->  ( x  e.  ( X (,) Y )  |->  B )  e.  ( ( ( X (,) Y ) -cn-> CC )  i^i  L^1 ) )   &    |-  ( ph  ->  F  e.  ( ( K [,] L ) -cn-> CC ) )   &    |-  ( ph  ->  K  e.  RR )   &    |-  ( ph  ->  L  e.  RR )   &    |-  ( ph  ->  K  <_  L )   &    |-  ( ph  ->  ( RR  _D  ( x  e.  ( X [,] Y )  |->  A ) )  =  ( x  e.  ( X (,) Y )  |->  B ) )   &    |-  ( u  =  A  ->  C  =  E )   &    |-  ( x  =  X  ->  A  =  K )   &    |-  ( x  =  Y  ->  A  =  L )   =>    |-  ( ph  ->  S__ [ K  ->  L ] C  _d u  =  S__ [ X  ->  Y ] ( E  x.  B )  _d x )
 
Theoremitgsubsticc 37730* Integration by u-substitution. The main difference with respect to itgsubst 22936 is that here we consider the range of  A ( x ) to be in the closed interval  ( K [,] L
). If  A ( x ) is a continuous, differentiable function from  [ X ,  Y ] to  ( Z ,  W ), whose derivative is continuous and integrable, and  C ( u ) is a continuous function on  ( Z ,  W ), then the integral of  C ( u ) from  K  =  A ( X ) to  L  =  A ( Y ) is equal to the integral of  C ( A ( x ) )  _D  A ( x ) from  X to  Y. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  Y  e.  RR )   &    |-  ( ph  ->  X 
 <_  Y )   &    |-  ( ph  ->  ( x  e.  ( X [,] Y )  |->  A )  e.  ( ( X [,] Y )
 -cn-> ( K [,] L ) ) )   &    |-  ( ph  ->  ( u  e.  ( K [,] L )  |->  C )  e.  ( ( K [,] L ) -cn-> CC ) )   &    |-  ( ph  ->  ( x  e.  ( X (,) Y )  |->  B )  e.  ( ( ( X (,) Y ) -cn-> CC )  i^i  L^1 ) )   &    |-  ( ph  ->  ( RR  _D  ( x  e.  ( X [,] Y )  |->  A ) )  =  ( x  e.  ( X (,) Y )  |->  B ) )   &    |-  ( u  =  A  ->  C  =  E )   &    |-  ( x  =  X  ->  A  =  K )   &    |-  ( x  =  Y  ->  A  =  L )   &    |-  ( ph  ->  K  e.  RR )   &    |-  ( ph  ->  L  e.  RR )   =>    |-  ( ph  ->  S__
 [ K  ->  L ] C  _d u  =  S__ [ X  ->  Y ] ( E  x.  B )  _d x )
 
Theoremitgioocnicc 37731* The integral of a piecewise continuous function  F on an open interval is equal to the integral of the continuous function  G, in the corresponding closed interval.  G is equal to  F on the open interval, but it is continuous at the two boundaries, also. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  F : dom  F --> CC )   &    |-  ( ph  ->  ( F  |`  ( A (,) B ) )  e.  ( ( A (,) B ) -cn-> CC ) )   &    |-  ( ph  ->  ( A [,] B ) 
 C_  dom  F )   &    |-  ( ph  ->  R  e.  (
 ( F  |`  ( A (,) B ) ) lim
 CC  A ) )   &    |-  ( ph  ->  L  e.  ( ( F  |`  ( A (,) B ) ) lim
 CC  B ) )   &    |-  G  =  ( x  e.  ( A [,] B )  |->  if ( x  =  A ,  R ,  if ( x  =  B ,  L ,  ( F `
  x ) ) ) )   =>    |-  ( ph  ->  ( G  e.  L^1  /\  S. ( A [,] B ) ( G `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x ) )
 
Theoremiblcncfioo 37732 A continuous function  F on an open interval  ( A (,) B ) with a finite right limit  R in  A and a finite left limit  L in  B is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  F  e.  ( ( A (,) B ) -cn-> CC ) )   &    |-  ( ph  ->  L  e.  ( F lim CC  B ) )   &    |-  ( ph  ->  R  e.  ( F lim CC  A ) )   =>    |-  ( ph  ->  F  e.  L^1 )
 
Theoremitgspltprt 37733* The  S. integral splits on a given partition  P. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  ( M  +  1 ) ) )   &    |-  ( ph  ->  P : ( M ... N ) --> RR )   &    |-  (
 ( ph  /\  i  e.  ( M..^ N ) )  ->  ( P `  i )  <  ( P `  ( i  +  1 ) ) )   &    |-  ( ( ph  /\  t  e.  ( ( P `  M ) [,] ( P `  N ) ) )  ->  A  e.  CC )   &    |-  ( ( ph  /\  i  e.  ( M..^ N ) )  ->  ( t  e.  (
 ( P `  i
 ) [,] ( P `  ( i  +  1
 ) ) )  |->  A )  e.  L^1 )   =>    |-  ( ph  ->  S. ( ( P `  M ) [,] ( P `  N ) ) A  _d t  = 
 sum_ i  e.  ( M..^ N ) S. (
 ( P `  i
 ) [,] ( P `  ( i  +  1
 ) ) ) A  _d t )
 
Theoremitgiccshift 37734* The integral of a function,  F stays the same if its closed interval domain is shifted by  T. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A 
 <_  B )   &    |-  ( ph  ->  F  e.  ( ( A [,] B ) -cn-> CC ) )   &    |-  ( ph  ->  T  e.  RR+ )   &    |-  G  =  ( x  e.  ( ( A  +  T ) [,] ( B  +  T ) )  |->  ( F `  ( x  -  T ) ) )   =>    |-  ( ph  ->  S. ( ( A  +  T ) [,] ( B  +  T )
 ) ( G `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x )
 
Theoremitgperiod 37735* The integral of a periodic function, with period  T stays the same if the domain of integration is shifted. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A 
 <_  B )   &    |-  ( ph  ->  T  e.  RR+ )   &    |-  ( ph  ->  F : RR --> CC )   &    |-  (
 ( ph  /\  x  e.  ( A [,] B ) )  ->  ( F `
  ( x  +  T ) )  =  ( F `  x ) )   &    |-  ( ph  ->  ( F  |`  ( A [,] B ) )  e.  ( ( A [,] B ) -cn-> CC ) )   =>    |-  ( ph  ->  S. ( ( A  +  T ) [,] ( B  +  T )
 ) ( F `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x )
 
Theoremitgsbtaddcnst 37736* Integral substitution, adding a constant to the function's argument. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A 
 <_  B )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  F  e.  (
 ( A [,] B ) -cn-> CC ) )   =>    |-  ( ph  ->  S__
 [ ( A  -  X )  ->  ( B  -  X ) ]
 ( F `  ( X  +  s )
 )  _d s  =  S__ [ A  ->  B ] ( F `  t )  _d t
 )
 
Theoremitgeq2d 37737* Equality theorem for an integral. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
 |-  (
 ( ph  /\  x  e.  A )  ->  B  =  C )   =>    |-  ( ph  ->  S. A B  _d x  =  S. A C  _d x )
 
21.30.12  Stone Weierstrass theorem - real version
 
Theoremstoweidlem1 37738 Lemma for stoweid 37802. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90; the key step uses Bernoulli's inequality bernneq 12341. (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 ) ) )
 
Theoremstoweidlem2 37739* lemma for stoweid 37802: 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 )
 
Theoremstoweidlem3 37740* Lemma for stoweid 37802: 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 37741* Lemma for stoweid 37802: 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 37742* 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 37743* Lemma for stoweid 37802: 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 37744* 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 37745* Lemma for stoweid 37802: 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 37746* Lemma for stoweid 37802: 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 37747 Lemma for stoweid 37802. 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 37748* 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 37749* Lemma for stoweid 37802. 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 37750 Lemma for stoweid 37802. 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 37751* 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 37752* 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 37753* Lemma for stoweid 37802. 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 37754* 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 37755* 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 37756* 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 37757* 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 37758* 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 37759* 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 37760* 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 37761* 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 37762* 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 37763* 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 37764* 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 37765* 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 37766* 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 37767* 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 37766 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 37768* 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 37769* 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 37770* 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 37771* 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 37772* 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 37773* 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 37774* 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 37775* 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 37776* 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 37777* 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 37778* 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 37779* 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 37780* 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 37781* 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 37782* 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 37783* 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 37784* 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 37785* 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 37786* 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 37787* 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 37788* 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 37789* 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 37790* 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 37791* 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 37792* 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 37793* 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 37794* 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 37795* 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 37796* 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  ->