Metamath Proof Explorer Home Metamath Proof Explorer
Most Recent Proofs
 
Mirrors  >  Home  >  MPE Home  >  Th. List  >  Recent Other  >  MM 100

Most recent proofs    These are the 10 (GIF, Unicode) or 1000 (GIF, Unicode) most recent proofs in the set.mm database for the Metamath Proof Explorer (and the Hilbert Space Explorer). The set.mm database is maintained on Github with master (stable) and develop (development) versions. This page was created from develop commit 71e7fcc, also available here: set.mm (30MB) or set.mm.bz2 (compressed, 8MB).

Other links    Email: Norm Megill.    Mailing list: Metamath Google Group Updated 28-Apr-2017 .    Syndication: RSS feed (courtesy of Dan Getz).    Related wikis: Wikiproofs (JHilbert) (Recent Changes); Ghilbert site; Ghilbert Google Group.

Recent news items    (20-Apr-2017) Glauco Siliprandi added a new proof in the supplementary list on the 100 theorem list, Stone-Weierstrass Theorem stowei.

(13-Apr-2017) See equidK for a discussion of the recent theorems in my mathbox. -NM

(24-Mar-2017) Alan Sare updated his completeusersproof program.

(28-Feb-2017) David Moews added a new proof to the 100 theorem list, Product of Segments of Chords chordthm, bringing the Metamath total to 62.

(18-Feb-2017) Filip Cernatescu announced Milpgame 0.1 (MILP: Math is like a puzzle!).

(1-Jan-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Isosceles triangle theorem isosctr, bringing the Metamath total to 61.

(1-Jan-2017) Mario Carneiro added 2 new proofs to the 100 theorem list, L'Hôpital's Rule lhop and Taylor's Theorem taylth, bringing the Metamath total to 60.

(28-Dec-2016) David A. Wheeler is putting together a page on Metamath (specifically set.mm) conventions. Comments are welcome on the Google Group thread.

(24-Dec-2016) Mario Carneiro introduced the abbreviation "F/ x ph" (symbols: turned F, x, phi) in df-nf to represent the "effectively not free" idiom "A. x ( ph -> A. x ph )". Theorem nf2 shows a version without nested quantifiers.

(22-Dec-2016) Naip Moro has developed a Metamath database for G. Spencer-Brown's Laws of Form. You can follow the Google Group discussion here.

(20-Dec-2016) In metamath program version 0.137, 'verify markup *' now checks that ax-XXX $a matches axXXX $p when the latter exists, per the discussion at https://groups.google.com/d/msg/metamath/Vtz3CKGmXnI/Fxq3j1I_EQAJ.

(24-Nov-2016) Mingl Yuan has kindly provided a mirror site in Beijing, China. He has also provided an rsync server; type "rsync cn.metamath.org::" in a bash shell to check its status (it should return "metamath metamath").

(14-Aug-2016) All HTML pages on this site should now be mobile-friendly and pass the Mobile-Friendly Test. If you find one that does not, let me know.

(14-Aug-2016) Daniel Whalen wrote a paper describing the use of using deep learning to prove 14% of test theorems taken from set.mm: Holophrasm: a neural Automated Theorem Prover for higher-order logic. The associated program is called Holophrasm.

(14-Aug-2016) David A. Wheeler created a video called Metamath Proof Explorer: A Modern Principia Mathematica

(12-Aug-2016) A Gitter chat room has been created for Metamath.

(9-Aug-2016) Mario Carneiro wrote a Metamath proof verifier in the Scala language as part of the ongoing Metamath -> MMT import project

(9-Aug-2016) David A. Wheeler created a GitHub project called metamath-test (last execution run) to check that different verifiers both pass good databases and detect errors in defective ones.

(4-Aug-2016) Mario gave two presentations at CICM 2016.

(17-Jul-2016) Thierry Arnoux has written EMetamath, a Metamath plugin for the Eclipse IDE.

(16-Jul-2016) Mario recovered Chris Capel's collapsible proof demo.

(13-Jul-2016) FL sent me an updated version of PDF (LaTeX source) developed with Lamport's pf2 package. See the 23-Apr-2012 entry below.

(12-Jul-2016) David A. Wheeler produced a new video for mmj2 called "Creating functions in Metamath". It shows a more efficient approach than his previous recent video "Creating functions in Metamath" (old) but it can be of interest to see both approaches.

(10-Jul-2016) Metamath program version 0.132 changes the command 'show restricted' to 'show discouraged' and adds a new command, 'set discouragement'. See the mmnotes.txt entry of 11-May-2016 (updated 10-Jul-2016).

(12-Jun-2016) Dan Getz has written Metamath.jl, a Metamath proof verifier written in the Julia language.    Older news...

Color key:   Metamath Proof Explorer  Metamath Proof Explorer   Hilbert Space Explorer  Hilbert Space Explorer   User Mathboxes  User Mathboxes  

Last updated on 29-Apr-2017 at 8:38 PM ET.
Recent Additions to the Metamath Proof Explorer   Notes (last updated 10-Jul-16 )
DateLabelDescription
Theorem
 
23-Apr-2017ax9dgenK 27911 Degenerate case of ax-9 1684. Uses only Tarski's FOL axiom schemes (see description for equidK 27889). (Contributed by NM, 23-Apr-2017.)
 |-  -.  A. x  -.  x  =  x
 
20-Apr-2017stowei 26947 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 26946: often times it will be better to use stoweid 26946 in other proofs (but this version is probably easier to be read and understood). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  K  =  ( topGen `  ran  (,) )   &    |-  J  e.  Comp   &    |-  T  =  U. J   &    |-  C  =  ( J  Cn  K )   &    |-  A  C_  C   &    |-  ( ( f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  +  ( g `
  t ) ) )  e.  A )   &    |-  ( ( f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  A )   &    |-  ( x  e.  RR  ->  ( t  e.  T  |->  x )  e.  A )   &    |-  ( ( r  e.  T  /\  t  e.  T  /\  r  =/=  t )  ->  E. h  e.  A  ( h `  r )  =/=  ( h `  t ) )   &    |-  F  e.  C   &    |-  E  e.  RR+   =>    |-  E. f  e.  A  A. t  e.  T  ( abs `  (
 ( f `  t
 )  -  ( F `
  t ) ) )  <  E
 
20-Apr-2017stoweid 26946 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 )
 
20-Apr-2017stoweidlem62 26945 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.)
 |-  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 )
 
20-Apr-2017stoweidlem61 26944 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 ) )
 
20-Apr-2017stoweidlem60 26943 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 ) ) ) )
 
20-Apr-2017stoweidlem59 26942 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 ) ) ) )
 
20-Apr-2017stoweidlem58 26941 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 ) ) )
 
20-Apr-2017stoweidlem57 26940 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 ) ) )
 
20-Apr-2017stoweidlem56 26939 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
 ) ) ) )
 
20-Apr-2017stoweidlem55 26938 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 ) ) )
 
20-Apr-2017stoweidlem54 26937 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 ) ) )
 
20-Apr-2017stoweidlem53 26936 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 ) ) )
 
20-Apr-2017stoweidlem52 26935 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
 ) ) ) )
 
20-Apr-2017stoweidlem51 26934 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 ) ) ) )
 
20-Apr-2017stoweidlem50 26933 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 ) )
 
20-Apr-2017stoweidlem49 26932 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 ) )
 
20-Apr-2017stoweidlem48 26931 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 )
 
20-Apr-2017stoweidlem47 26930 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 )
 
20-Apr-2017stoweidlem46 26929 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 )
 
20-Apr-2017stoweidlem45 26928 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 ) )
 
20-Apr-2017stoweidlem44 26927 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 ) ) )
 
20-Apr-2017stoweidlem43 26926 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 ) ) )
 
20-Apr-2017stoweidlem42 26925 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 ) )
 
20-Apr-2017stoweidlem41 26924 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 ) ) )
 
20-Apr-2017stoweidlem40 26923 This lemma proves that qn is in the subalgebra, as in the prove 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 )
 
20-Apr-2017stoweidlem39 26922 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 ) ) ) ) )
 
20-Apr-2017stoweidlem38 26921 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 GlaucoSiliprandi, 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 ) )
 
20-Apr-2017stoweidlem37 26920 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 )
 
20-Apr-2017stoweidlem36 26919 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 it's 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 ) ) )
 
20-Apr-2017stoweidlem35 26918 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
 ) ) ) )
 
20-Apr-2017stoweidlem34 26917 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 ) ) ) )
 
20-Apr-2017stoweidlem33 26916 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 )
 
20-Apr-2017stoweidlem32 26915 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 )
 
20-Apr-2017stoweidlem31 26914 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 ) ) ) )
 
20-Apr-2017stoweidlem30 26913 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 )
 ) )
 
20-Apr-2017stoweidlem29 26912 When the hypothesis for the extreme value theorem hold, then the inf of the range of the function belongs to the range, it is real and it a lower bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ t F   &    |- 
 F/ t ph   &    |-  T  =  U. J   &    |-  K  =  ( topGen `  ran  (,) )   &    |-  ( ph  ->  J  e.  Comp )   &    |-  ( ph  ->  F  e.  ( J  Cn  K ) )   &    |-  ( ph  ->  T  =/=  (/) )   =>    |-  ( ph  ->  ( sup ( ran  F ,  RR ,  `'  <  )  e.  ran  F  /\  sup ( ran  F ,  RR ,  `'  <  )  e.  RR  /\  A. t  e.  T  sup ( ran 
 F ,  RR ,  `'  <  )  <_  ( F `  t ) ) )
 
20-Apr-2017stoweidlem28 26911 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
 ) ) )
 
20-Apr-2017stoweidlem27 26910 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 ) ) ) )
 
20-Apr-2017stoweidlem26 26909 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 ) )
 
20-Apr-2017stoweidlem25 26908 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 )
 
20-Apr-2017stoweidlem24 26907 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 ) )
 
20-Apr-2017stoweidlem23 26906 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 ) )
 
20-Apr-2017stoweidlem22 26905 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 )
 
20-Apr-2017stoweidlem21 26904 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 )
 
20-Apr-2017stoweidlem20 26903 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 )
 
20-Apr-2017stoweidlem19 26902 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 )
 
20-Apr-2017stoweidlem18 26901 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 ) ) )
 
20-Apr-2017stoweidlem17 26900 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 )
 
20-Apr-2017stoweidlem16 26899 Lemma for stoweid 26946. 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 )
 
20-Apr-2017stoweidlem15 26898 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 ) )
 
20-Apr-2017stoweidlem14 26897 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
 ) )
 
20-Apr-2017stoweidlem13 26896 Lemma for stoweid 26946. This lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon , in [BrosowskiDeutsh] p. 92, the last step of the proof. (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 ) )
 
20-Apr-2017stoweidlem12 26895 Lemma for stoweid 26946. 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 ) ) )
 
20-Apr-2017stoweidlem11 26894 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 ) )
 
20-Apr-2017stoweidlem10 26893 Lemma for stoweid 26946. 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 ) )
 
20-Apr-2017stoweidlem9 26892 Lemma for stoweid 26946: 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 )
 
20-Apr-2017stoweidlem8 26891 Lemma for stoweid 26946: two class variables replace two set 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 )
 
20-Apr-2017stoweidlem7 26890 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 ) )
 
20-Apr-2017stoweidlem6 26889 Lemma for stoweid 26946: two class variables replace two set 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 )
 
20-Apr-2017stoweidlem5 26888 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
 ) ) )
 
20-Apr-2017stoweidlem4 26887 Lemma for stoweid 26946: a class variable replaces a set 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 )
 
20-Apr-2017stoweidlem3 26886 Lemma for stoweid 26946: 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 ) )
 
20-Apr-2017stoweidlem2 26885 lemma for stoweid 26946: 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 )
 
20-Apr-2017stoweidlem1 26884 Lemma for stoweid 26946. This lemma is used by Lemma 1 in [BrosowskiDeutsh] p. 90; the key step uses Bernoulli's inequality bernneq 11105. (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 ) ) )
 
20-Apr-2017fmul01lt1 26883 Given a finite multiplication of values betweeen 0 and 1, a value E larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ i B   &    |- 
 F/ i ph   &    |-  F/_ j A   &    |-  A  =  seq  1 (  x. 
 ,  B )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  B : ( 1 ...
 M ) --> RR )   &    |-  (
 ( ph  /\  i  e.  ( 1 ... M ) )  ->  0  <_  ( B `  i ) )   &    |-  ( ( ph  /\  i  e.  ( 1
 ... M ) ) 
 ->  ( B `  i
 )  <_  1 )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ph  ->  E. j  e.  ( 1 ... M ) ( B `  j )  <  E )   =>    |-  ( ph  ->  ( A `  M )  <  E )
 
20-Apr-2017fmul01lt1lem2 26882 Given a finite multiplication of values betweeen 0 and 1, a value  E larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ i B   &    |- 
 F/ i ph   &    |-  A  =  seq  L (  x.  ,  B )   &    |-  ( ph  ->  L  e.  ZZ )   &    |-  ( ph  ->  M  e.  ( ZZ>= `  L ) )   &    |-  ( ( ph  /\  i  e.  ( L
 ... M ) ) 
 ->  ( B `  i
 )  e.  RR )   &    |-  (
 ( ph  /\  i  e.  ( L ... M ) )  ->  0  <_  ( B `  i ) )   &    |-  ( ( ph  /\  i  e.  ( L
 ... M ) ) 
 ->  ( B `  i
 )  <_  1 )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ph  ->  J  e.  ( L ... M ) )   &    |-  ( ph  ->  ( B `  J )  <  E )   =>    |-  ( ph  ->  ( A `  M )  <  E )
 
20-Apr-2017fmul01lt1lem1 26881 Given a finite multiplication of values betweeen 0 and 1, a value larger than its frist element is larger the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ i B   &    |- 
 F/ i ph   &    |-  A  =  seq  L (  x.  ,  B )   &    |-  ( ph  ->  L  e.  ZZ )   &    |-  ( ph  ->  M  e.  ( ZZ>= `  L ) )   &    |-  ( ( ph  /\  i  e.  ( L
 ... M ) ) 
 ->  ( B `  i
 )  e.  RR )   &    |-  (
 ( ph  /\  i  e.  ( L ... M ) )  ->  0  <_  ( B `  i ) )   &    |-  ( ( ph  /\  i  e.  ( L
 ... M ) ) 
 ->  ( B `  i
 )  <_  1 )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ph  ->  ( B `  L )  <  E )   =>    |-  ( ph  ->  ( A `  M )  <  E )
 
20-Apr-2017fmuldfeq 26880 X and Z are two equivalent definitions of the finite product of real functions. Y is a set of real functions from a common domain T, Y is closed under function multiplication and U is a finite sequence of functions in Y. M is the number of functions multiplied together. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/ i 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  ->  T  e.  _V )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  U : ( 1 ...
 M ) --> Y )   &    |-  ( ( 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.  T )  ->  ( X `  t )  =  ( Z `  t
 ) )
 
20-Apr-2017fmuldfeqlem1 26879 induction step for the proof of fmuldfeq 26880. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/ f ph   &    |-  F/ g ph   &    |-  F/_ t Y   &    |-  P  =  ( f  e.  Y ,  g  e.  Y  |->  ( t  e.  T  |->  ( ( f `
  t )  x.  ( g `  t
 ) ) ) )   &    |-  F  =  ( t  e.  T  |->  ( i  e.  ( 1 ... M )  |->  ( ( U `
  i ) `  t ) ) )   &    |-  ( ph  ->  T  e.  _V )   &    |-  ( ph  ->  U : ( 1 ...
 M ) --> Y )   &    |-  ( ( ph  /\  f  e.  Y  /\  g  e.  Y )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  Y )   &    |-  ( ph  ->  N  e.  ( 1 ... M ) )   &    |-  ( ph  ->  ( N  +  1 )  e.  ( 1 ...
 M ) )   &    |-  ( ph  ->  ( (  seq  1 ( P ,  U ) `  N ) `  t )  =  (  seq  1 (  x.  ,  ( F `
  t ) ) `
  N ) )   &    |-  ( ( ph  /\  f  e.  Y )  ->  f : T --> RR )   =>    |-  ( ( ph  /\  t  e.  T ) 
 ->  ( (  seq  1
 ( P ,  U ) `  ( N  +  1 ) ) `  t )  =  (  seq  1 (  x.  ,  ( F `  t ) ) `  ( N  +  1 ) ) )
 
20-Apr-2017fmulcl 26878 If ' Y ' is closed under the multiplication of two functions, then Y is closed under the multiplication ( ' X ' ) of a finite number of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  P  =  ( f  e.  Y ,  g  e.  Y  |->  ( t  e.  T  |->  ( ( f `  t )  x.  (
 g `  t )
 ) ) )   &    |-  X  =  (  seq  1 ( P ,  U ) `
  N )   &    |-  ( ph  ->  N  e.  (
 1 ... M ) )   &    |-  ( ph  ->  U :
 ( 1 ... M )
 --> Y )   &    |-  ( ( ph  /\  f  e.  Y  /\  g  e.  Y )  ->  ( t  e.  T  |->  ( ( f `  t )  x.  (
 g `  t )
 ) )  e.  Y )   &    |-  ( ph  ->  T  e.  _V