HomeHome Metamath Proof Explorer
Theorem List (p. 273 of 315)
< 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-21490)
  Hilbert Space Explorer  Hilbert Space Explorer
(21491-23013)
  Users' Mathboxes  Users' Mathboxes
(23014-31421)
 

Theorem List for Metamath Proof Explorer - 27201-27300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremstoweidlem53 27201* 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 27202* 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 27203* 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 27204* 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 27205* 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 27206* This theorem proves Lemma 2 in [BrosowskiDeutsh] p. 91. Here D is used to represent the set A of Lemma 2, because here the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ t D   &    |-  F/_ t U   &    |-  F/ t ph   &    |-  K  =  ( topGen `  ran  (,) )   &    |-  T  =  U. J   &    |-  C  =  ( J  Cn  K )   &    |-  ( ph  ->  J  e.  Comp
 )   &    |-  ( ph  ->  A  C_  C )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  ( t  e.  T  |->  ( ( f `  t )  +  (
 g `  t )
 ) )  e.  A )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  a  e.  RR )  ->  (
 t  e.  T  |->  a )  e.  A )   &    |-  ( ( ph  /\  (
 r  e.  T  /\  t  e.  T  /\  r  =/=  t ) ) 
 ->  E. q  e.  A  ( q `  r
 )  =/=  ( q `  t ) )   &    |-  ( ph  ->  B  e.  ( Clsd `  J ) )   &    |-  ( ph  ->  D  e.  ( Clsd `  J )
 )   &    |-  ( ph  ->  ( B  i^i  D )  =  (/) )   &    |-  U  =  ( T  \  B )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ph  ->  E  <  ( 1  / 
 3 ) )   =>    |-  ( ph  ->  E. x  e.  A  (
 A. t  e.  T  ( 0  <_  ( x `  t )  /\  ( x `  t ) 
 <_  1 )  /\  A. t  e.  D  ( x `  t )  <  E  /\  A. t  e.  B  ( 1  -  E )  <  ( x `
  t ) ) )
 
Theoremstoweidlem59 27207* This lemma proves that there exists a function  x as in the proof in [BrosowskiDeutsh] p. 91, after Lemma 2: xj is in the subalgebra, 0 <= xj <= 1, xj < ε / n on Aj (meaning A in the paper), xj > 1 - \epslon / n on Bj. Here  D is used to represent A in the paper (because A is used for the subalgebra of functions),  E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ t F   &    |- 
 F/ t ph   &    |-  K  =  (
 topGen `  ran  (,) )   &    |-  T  =  U. J   &    |-  C  =  ( J  Cn  K )   &    |-  D  =  ( j  e.  ( 0 ... N )  |->  { t  e.  T  |  ( F `  t
 )  <_  ( (
 j  -  ( 1 
 /  3 ) )  x.  E ) }
 )   &    |-  B  =  ( j  e.  ( 0 ...
 N )  |->  { t  e.  T  |  ( ( j  +  ( 1 
 /  3 ) )  x.  E )  <_  ( F `  t ) } )   &    |-  Y  =  {
 y  e.  A  |  A. t  e.  T  ( 0  <_  (
 y `  t )  /\  ( y `  t
 )  <_  1 ) }   &    |-  H  =  ( j  e.  ( 0 ...
 N )  |->  { y  e.  Y  |  ( A. t  e.  ( D `  j ) ( y `
  t )  < 
 ( E  /  N )  /\  A. t  e.  ( B `  j
 ) ( 1  -  ( E  /  N ) )  <  ( y `
  t ) ) } )   &    |-  ( ph  ->  J  e.  Comp )   &    |-  ( ph  ->  A 
 C_  C )   &    |-  (
 ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  +  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  y  e.  RR )  ->  (
 t  e.  T  |->  y )  e.  A )   &    |-  ( ( ph  /\  (
 r  e.  T  /\  t  e.  T  /\  r  =/=  t ) ) 
 ->  E. q  e.  A  ( q `  r
 )  =/=  ( q `  t ) )   &    |-  ( ph  ->  F  e.  C )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ph  ->  E  <  ( 1  / 
 3 ) )   &    |-  ( ph  ->  N  e.  NN )   =>    |-  ( ph  ->  E. x ( x : ( 0
 ... N ) --> A  /\  A. j  e.  ( 0
 ... N ) (
 A. t  e.  T  ( 0  <_  (
 ( x `  j
 ) `  t )  /\  ( ( x `  j ) `  t
 )  <_  1 )  /\  A. t  e.  ( D `  j ) ( ( x `  j
 ) `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `  j
 ) ( 1  -  ( E  /  N ) )  <  ( ( x `  j ) `
  t ) ) ) )
 
Theoremstoweidlem60 27208* This lemma proves that there exists a function g as in the proof in [BrosowskiDeutsh] p. 91 (this parte of the proof actually spans through pages 91-92): g is in the subalgebra, and for all  t in  T, there is a  j such that (j-4/3)*ε < f(t) <= (j-1/3)*ε and (j-4/3)*ε < g(t) < (j+1/3)*ε. Here  F is used to represent f in the paper, and  E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ t F   &    |- 
 F/ t ph   &    |-  K  =  (
 topGen `  ran  (,) )   &    |-  T  =  U. J   &    |-  C  =  ( J  Cn  K )   &    |-  D  =  ( j  e.  ( 0 ... n )  |->  { t  e.  T  |  ( F `  t
 )  <_  ( (
 j  -  ( 1 
 /  3 ) )  x.  E ) }
 )   &    |-  B  =  ( j  e.  ( 0 ... n )  |->  { t  e.  T  |  ( ( j  +  ( 1 
 /  3 ) )  x.  E )  <_  ( F `  t ) } )   &    |-  ( ph  ->  J  e.  Comp )   &    |-  ( ph  ->  T  =/=  (/) )   &    |-  ( ph  ->  A 
 C_  C )   &    |-  (
 ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  +  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  y  e.  RR )  ->  (
 t  e.  T  |->  y )  e.  A )   &    |-  ( ( ph  /\  (
 r  e.  T  /\  t  e.  T  /\  r  =/=  t ) ) 
 ->  E. q  e.  A  ( q `  r
 )  =/=  ( q `  t ) )   &    |-  ( ph  ->  F  e.  C )   &    |-  ( ph  ->  A. t  e.  T  0  <_  ( F `  t ) )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ph  ->  E  <  ( 1  / 
 3 ) )   =>    |-  ( ph  ->  E. g  e.  A  A. t  e.  T  E. j  e.  RR  ( ( ( ( j  -  (
 4  /  3 )
 )  x.  E )  <  ( F `  t )  /\  ( F `
  t )  <_  ( ( j  -  ( 1  /  3
 ) )  x.  E ) )  /\  ( ( g `  t )  <  ( ( j  +  ( 1  / 
 3 ) )  x.  E )  /\  (
 ( j  -  (
 4  /  3 )
 )  x.  E )  <  ( g `  t ) ) ) )
 
Theoremstoweidlem61 27209* This lemma proves that there exists a function  g as in the proof in [BrosowskiDeutsh] p. 92:  g is in the subalgebra, and for all  t in  T, abs( f(t) - g(t) ) < 2*ε. Here  F is used to represent f in the paper, and  E is used to represent ε. For this lemma there's the further assumption that the function  F to be approximated is nonnegative (this assumption is removed in a later theorem). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ t F   &    |- 
 F/ t ph   &    |-  K  =  (
 topGen `  ran  (,) )   &    |-  ( ph  ->  J  e.  Comp )   &    |-  T  =  U. J   &    |-  ( ph  ->  T  =/=  (/) )   &    |-  C  =  ( J  Cn  K )   &    |-  ( ph  ->  A  C_  C )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  ( t  e.  T  |->  ( ( f `  t )  +  (
 g `  t )
 ) )  e.  A )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  x  e.  RR )  ->  (
 t  e.  T  |->  x )  e.  A )   &    |-  ( ( ph  /\  (
 r  e.  T  /\  t  e.  T  /\  r  =/=  t ) ) 
 ->  E. q  e.  A  ( q `  r
 )  =/=  ( q `  t ) )   &    |-  ( ph  ->  F  e.  C )   &    |-  ( ph  ->  A. t  e.  T  0  <_  ( F `  t ) )   &    |-  ( ph  ->  E  e.  RR+ )   &    |-  ( ph  ->  E  <  ( 1  / 
 3 ) )   =>    |-  ( ph  ->  E. g  e.  A  A. t  e.  T  ( abs `  ( ( g `
  t )  -  ( F `  t ) ) )  <  (
 2  x.  E ) )
 
Theoremstoweidlem62 27210* 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 )
 
Theoremstoweid 27211* This theorem proves the Stone-Weierstrass theorem for real valued functions: let  J be a compact topology on  T, and  C be the set of real continuous functions on  T. Assume that  A is a subalgebra of  C (closed under addition and multiplication of functions) containing constant functions and discriminating points (if  r and  t are distinct points in  T, then there exists a function  h in  A such that h(r) is distinct from h(t) ). Then, for any continuous function 
F and for any positive real  E, there exists a function  f in the subalgebra  A, such that  f approximates  F up to  E ( E represents the usual ε value). As a classical example, given any a,b reals, the closed interval  T  =  [
a ,  b ] could be taken, along with the subalgebra  A of real polynomials on  T, and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on  [ a ,  b ]. The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
 |-  F/_ t F   &    |- 
 F/ t ph   &    |-  K  =  (
 topGen `  ran  (,) )   &    |-  ( ph  ->  J  e.  Comp )   &    |-  T  =  U. J   &    |-  C  =  ( J  Cn  K )   &    |-  ( ph  ->  A  C_  C )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  ( t  e.  T  |->  ( ( f `  t )  +  (
 g `  t )
 ) )  e.  A )   &    |-  ( ( ph  /\  f  e.  A  /\  g  e.  A )  ->  (
 t  e.  T  |->  ( ( f `  t
 )  x.  ( g `
  t ) ) )  e.  A )   &    |-  ( ( ph  /\  x  e.  RR )  ->  (
 t  e.  T  |->  x )  e.  A )   &    |-  ( ( ph  /\  (
 r  e.  T  /\  t  e.  T  /\  r  =/=  t ) ) 
 ->  E. h  e.  A  ( h `  r )  =/=  ( h `  t ) )   &    |-  ( ph  ->  F  e.  C )   &    |-  ( ph  ->  E  e.  RR+ )   =>    |-  ( ph  ->  E. f  e.  A  A. t  e.  T  ( abs `  (
 ( f `  t
 )  -  ( F `
  t ) ) )  <  E )
 
Theoremstowei 27212* 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 27211: often times it will be better to use stoweid 27211 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
 
18.19.7  Wallis' product for π
 
Theoremwallispilem1 27213*  I is monotone: increasing the exponent, the integral decreases. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  I  =  ( n  e.  NN0  |->  S. ( 0 (,) pi ) ( ( sin `  x ) ^ n )  _d x )   &    |-  ( ph  ->  N  e.  NN0 )   =>    |-  ( ph  ->  ( I `  ( N  +  1 ) )  <_  ( I `  N ) )
 
Theoremwallispilem2 27214* A first set of properties for the sequence  I that will be used in the proof of the Wallis product formula (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  I  =  ( n  e.  NN0  |->  S. ( 0 (,) pi ) ( ( sin `  x ) ^ n )  _d x )   =>    |-  ( ( I `
  0 )  =  pi  /\  ( I `
  1 )  =  2  /\  ( N  e.  ( ZZ>= `  2
 )  ->  ( I `  N )  =  ( ( ( N  -  1 )  /  N )  x.  ( I `  ( N  -  2
 ) ) ) ) )
 
Theoremwallispilem3 27215* I maps to real values (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  I  =  ( n  e.  NN0  |->  S. ( 0 (,) pi ) ( ( sin `  x ) ^ n )  _d x )   =>    |-  ( N  e.  NN0 
 ->  ( I `  N )  e.  RR+ )
 
Theoremwallispilem4 27216*  F maps to explicit expression for the ratio of two consecutive values of  I (Contributed by Glauco Siliprandi, 30-Jun-2017.)
 |-  F  =  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  -  1
 ) )  x.  (
 ( 2  x.  k
 )  /  ( (
 2  x.  k )  +  1 ) ) ) )   &    |-  I  =  ( n  e.  NN0  |->  S. (
 0 (,) pi ) ( ( sin `  z
 ) ^ n )  _d z )   &    |-  G  =  ( n  e.  NN  |->  ( ( I `  ( 2  x.  n ) )  /  ( I `  ( ( 2  x.  n )  +  1 ) ) ) )   &    |-  H  =  ( n  e.  NN  |->  ( ( pi  /  2
 )  x.  ( 1 
 /  (  seq  1
 (  x.  ,  F ) `  n ) ) ) )   =>    |-  G  =  H
 
Theoremwallispilem5 27217* The sequence  H converges to 1. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
 |-  F  =  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  -  1
 ) )  x.  (
 ( 2  x.  k
 )  /  ( (
 2  x.  k )  +  1 ) ) ) )   &    |-  I  =  ( n  e.  NN0  |->  S. (
 0 (,) pi ) ( ( sin `  x ) ^ n )  _d x )   &    |-  G  =  ( n  e.  NN  |->  ( ( I `  (
 2  x.  n ) )  /  ( I `
  ( ( 2  x.  n )  +  1 ) ) ) )   &    |-  H  =  ( n  e.  NN  |->  ( ( pi  /  2
 )  x.  ( 1 
 /  (  seq  1
 (  x.  ,  F ) `  n ) ) ) )   &    |-  L  =  ( n  e.  NN  |->  ( ( ( 2  x.  n )  +  1 )  /  ( 2  x.  n ) ) )   =>    |-  H  ~~>  1
 
Theoremwallispi 27218* Wallis' formula for π : Wallis' product converges to π / 2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F  =  ( k  e.  NN  |->  ( ( ( 2  x.  k )  /  ( ( 2  x.  k )  -  1
 ) )  x.  (
 ( 2  x.  k
 )  /  ( (
 2  x.  k )  +  1 ) ) ) )   &    |-  W  =  ( n  e.  NN  |->  ( 
 seq  1 (  x. 
 ,  F ) `  n ) )   =>    |-  W  ~~>  ( pi  /  2 )
 
Theoremwallispi2lem1 27219 An intermediate step between the first version of the Wallis' formula for π and the second version of Wallis' formula. This second version will then be used to prove Stirling's approximation formula for the factorial. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
 |-  ( N  e.  NN  ->  ( 
 seq  1 (  x. 
 ,  ( k  e. 
 NN  |->  ( ( ( 2  x.  k ) 
 /  ( ( 2  x.  k )  -  1 ) )  x.  ( ( 2  x.  k )  /  (
 ( 2  x.  k
 )  +  1 ) ) ) ) ) `
  N )  =  ( ( 1  /  ( ( 2  x.  N )  +  1 ) )  x.  (  seq  1 (  x.  ,  ( k  e.  NN  |->  ( ( ( 2  x.  k ) ^
 4 )  /  (
 ( ( 2  x.  k )  x.  (
 ( 2  x.  k
 )  -  1 ) ) ^ 2 ) ) ) ) `  N ) ) )
 
Theoremwallispi2lem2 27220 Two expressions are proven to be equal, and this is used to complete the proof of the second version of Wallis' formula for π . (Contributed by Glauco Siliprandi, 30-Jun-2017.)
 |-  ( N  e.  NN  ->  ( 
 seq  1 (  x. 
 ,  ( k  e. 
 NN  |->  ( ( ( 2  x.  k ) ^ 4 )  /  ( ( ( 2  x.  k )  x.  ( ( 2  x.  k )  -  1
 ) ) ^ 2
 ) ) ) ) `
  N )  =  ( ( ( 2 ^ ( 4  x.  N ) )  x.  ( ( ! `  N ) ^ 4
 ) )  /  (
 ( ! `  (
 2  x.  N ) ) ^ 2 ) ) )
 
Theoremwallispi2 27221 An alternative version of Wallis' formula for π ; this second formula uses factorials and it is later used to proof Stirling's approximation formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  V  =  ( n  e.  NN  |->  ( ( ( ( 2 ^ ( 4  x.  n ) )  x.  ( ( ! `
  n ) ^
 4 ) )  /  ( ( ! `  ( 2  x.  n ) ) ^ 2
 ) )  /  (
 ( 2  x.  n )  +  1 )
 ) )   =>    |-  V  ~~>  ( pi  / 
 2 )
 
18.19.8  Stirling's approximation formula for ` n ` factorial
 
Theoremstirlinglem1 27222 A simple limit of fractions is computed. (Contributed by Glauco Siliprandi, 30-Jun-2017.)
 |-  H  =  ( n  e.  NN  |->  ( ( n ^
 2 )  /  ( n  x.  ( ( 2  x.  n )  +  1 ) ) ) )   &    |-  F  =  ( n  e.  NN  |->  ( 1  -  ( 1 
 /  ( ( 2  x.  n )  +  1 ) ) ) )   &    |-  G  =  ( n  e.  NN  |->  ( 1  /  ( ( 2  x.  n )  +  1 ) ) )   &    |-  L  =  ( n  e.  NN  |->  ( 1  /  n ) )   =>    |-  H  ~~>  ( 1  / 
 2 )
 
Theoremstirlinglem2 27223  A maps to positive reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   =>    |-  ( N  e.  NN  ->  ( A `  N )  e.  RR+ )
 
Theoremstirlinglem3 27224 Long but simple algebraic transformations are applied to show that  V, the Wallis formula for π , can be expressed in terms of  A, the Stirling's approximation formula for the factorial, up to a constant factor. This will allow (in a later theorem) to determine the right constant factor to be put into the  A, in order to get the exact Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  D  =  ( n  e.  NN  |->  ( A `  ( 2  x.  n ) ) )   &    |-  E  =  ( n  e.  NN  |->  ( ( sqr `  (
 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) )   &    |-  V  =  ( n  e.  NN  |->  ( ( ( ( 2 ^ ( 4  x.  n ) )  x.  ( ( ! `  n ) ^ 4
 ) )  /  (
 ( ! `  (
 2  x.  n ) ) ^ 2 ) )  /  ( ( 2  x.  n )  +  1 ) ) )   =>    |-  V  =  ( n  e.  NN  |->  ( ( ( ( A `  n ) ^ 4
 )  /  ( ( D `  n ) ^
 2 ) )  x.  ( ( n ^
 2 )  /  ( n  x.  ( ( 2  x.  n )  +  1 ) ) ) ) )
 
Theoremstirlinglem4 27225* Algebraic manipulation of  ( ( B n ) - ( B  ( n  +  1 ) ) ). It will be used in other theorems to show that  B is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  B  =  ( n  e.  NN  |->  ( log `  ( A `  n ) ) )   &    |-  J  =  ( n  e.  NN  |->  ( ( ( ( 1  +  (
 2  x.  n ) )  /  2 )  x.  ( log `  (
 ( n  +  1 )  /  n ) ) )  -  1
 ) )   =>    |-  ( N  e.  NN  ->  ( ( B `  N )  -  ( B `  ( N  +  1 ) ) )  =  ( J `  N ) )
 
Theoremstirlinglem5 27226* If  T is between  0 and  1, then a series (without alternating negative and positive terms) is given that converges to log (1+T)/(1-T) . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  D  =  ( j  e.  NN  |->  ( ( -u 1 ^ ( j  -  1 ) )  x.  ( ( T ^
 j )  /  j
 ) ) )   &    |-  E  =  ( j  e.  NN  |->  ( ( T ^
 j )  /  j
 ) )   &    |-  F  =  ( j  e.  NN  |->  ( ( ( -u 1 ^ ( j  -  1 ) )  x.  ( ( T ^
 j )  /  j
 ) )  +  (
 ( T ^ j
 )  /  j )
 ) )   &    |-  H  =  ( j  e.  NN0  |->  ( 2  x.  ( ( 1 
 /  ( ( 2  x.  j )  +  1 ) )  x.  ( T ^ (
 ( 2  x.  j
 )  +  1 ) ) ) ) )   &    |-  G  =  ( j  e.  NN0  |->  ( ( 2  x.  j )  +  1 ) )   &    |-  ( ph  ->  T  e.  RR+ )   &    |-  ( ph  ->  ( abs `  T )  < 
 1 )   =>    |-  ( ph  ->  seq  0
 (  +  ,  H ) 
 ~~>  ( log `  (
 ( 1  +  T )  /  ( 1  -  T ) ) ) )
 
Theoremstirlinglem6 27227* A series that converges to log (N+1)/N (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  H  =  ( j  e.  NN0  |->  ( 2  x.  (
 ( 1  /  (
 ( 2  x.  j
 )  +  1 ) )  x.  ( ( 1  /  ( ( 2  x.  N )  +  1 ) ) ^ ( ( 2  x.  j )  +  1 ) ) ) ) )   =>    |-  ( N  e.  NN  ->  seq  0 (  +  ,  H )  ~~>  ( log `  ( ( N  +  1 )  /  N ) ) )
 
Theoremstirlinglem7 27228* Algebraic manipulation of the formula for J(n) (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  J  =  ( n  e.  NN  |->  ( ( ( ( 1  +  ( 2  x.  n ) ) 
 /  2 )  x.  ( log `  (
 ( n  +  1 )  /  n ) ) )  -  1
 ) )   &    |-  K  =  ( k  e.  NN  |->  ( ( 1  /  (
 ( 2  x.  k
 )  +  1 ) )  x.  ( ( 1  /  ( ( 2  x.  N )  +  1 ) ) ^ ( 2  x.  k ) ) ) )   &    |-  H  =  ( k  e.  NN0  |->  ( 2  x.  ( ( 1 
 /  ( ( 2  x.  k )  +  1 ) )  x.  ( ( 1  /  ( ( 2  x.  N )  +  1 ) ) ^ (
 ( 2  x.  k
 )  +  1 ) ) ) ) )   =>    |-  ( N  e.  NN  ->  seq  1 (  +  ,  K )  ~~>  ( J `  N ) )
 
Theoremstirlinglem8 27229 If  A converges to  C, then  F converges to C^2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F/ n ph   &    |-  F/_ n A   &    |-  F/_ n D   &    |-  D  =  ( n  e.  NN  |->  ( A `
  ( 2  x.  n ) ) )   &    |-  ( ph  ->  A : NN
 --> RR+ )   &    |-  F  =  ( n  e.  NN  |->  ( ( ( A `  n ) ^ 4
 )  /  ( ( D `  n ) ^
 2 ) ) )   &    |-  L  =  ( n  e.  NN  |->  ( ( A `
  n ) ^
 4 ) )   &    |-  M  =  ( n  e.  NN  |->  ( ( D `  n ) ^ 2
 ) )   &    |-  ( ( ph  /\  n  e.  NN )  ->  ( D `  n )  e.  RR+ )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A  ~~>  C )   =>    |-  ( ph  ->  F  ~~>  ( C ^ 2 ) )
 
Theoremstirlinglem9 27230*  ( ( B `  N )  -  ( B `  ( N  +  1
) ) ) is expressed as a limit of a series. This result will be used both to prove that  B is decreasing and to prove that  B is bounded (below). It will follow that  B converges in the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  B  =  ( n  e.  NN  |->  ( log `  ( A `  n ) ) )   &    |-  J  =  ( n  e.  NN  |->  ( ( ( ( 1  +  (
 2  x.  n ) )  /  2 )  x.  ( log `  (
 ( n  +  1 )  /  n ) ) )  -  1
 ) )   &    |-  K  =  ( k  e.  NN  |->  ( ( 1  /  (
 ( 2  x.  k
 )  +  1 ) )  x.  ( ( 1  /  ( ( 2  x.  N )  +  1 ) ) ^ ( 2  x.  k ) ) ) )   =>    |-  ( N  e.  NN  ->  seq  1 (  +  ,  K )  ~~>  ( ( B `  N )  -  ( B `  ( N  +  1 ) ) ) )
 
Theoremstirlinglem10 27231* A bound for any B(N)-B(N + 1) that will allow to find a lower bound for the whole  B sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  B  =  ( n  e.  NN  |->  ( log `  ( A `  n ) ) )   &    |-  K  =  ( k  e.  NN  |->  ( ( 1 
 /  ( ( 2  x.  k )  +  1 ) )  x.  ( ( 1  /  ( ( 2  x.  N )  +  1 ) ) ^ (
 2  x.  k ) ) ) )   &    |-  L  =  ( k  e.  NN  |->  ( ( 1  /  ( ( ( 2  x.  N )  +  1 ) ^ 2
 ) ) ^ k
 ) )   =>    |-  ( N  e.  NN  ->  ( ( B `  N )  -  ( B `  ( N  +  1 ) ) ) 
 <_  ( ( 1  / 
 4 )  x.  (
 1  /  ( N  x.  ( N  +  1 ) ) ) ) )
 
Theoremstirlinglem11 27232*  B is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  B  =  ( n  e.  NN  |->  ( log `  ( A `  n ) ) )   &    |-  K  =  ( k  e.  NN  |->  ( ( 1 
 /  ( ( 2  x.  k )  +  1 ) )  x.  ( ( 1  /  ( ( 2  x.  N )  +  1 ) ) ^ (
 2  x.  k ) ) ) )   =>    |-  ( N  e.  NN  ->  ( B `  ( N  +  1
 ) )  <  ( B `  N ) )
 
Theoremstirlinglem12 27233* The sequence  B is bounded below. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  B  =  ( n  e.  NN  |->  ( log `  ( A `  n ) ) )   &    |-  F  =  ( n  e.  NN  |->  ( 1  /  ( n  x.  ( n  +  1 )
 ) ) )   =>    |-  ( N  e.  NN  ->  ( ( B `
  1 )  -  ( 1  /  4
 ) )  <_  ( B `  N ) )
 
Theoremstirlinglem13 27234*  B is decreasing and has a lower bound, then it converges. Since  B is  log A, in another theorem it is proven that  A converges also. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  B  =  ( n  e.  NN  |->  ( log `  ( A `  n ) ) )   =>    |-  E. d  e.  RR  B  ~~>  d
 
Theoremstirlinglem14 27235* The sequence  A converges to a positive real. This proves that the Stirling's formula converges to the factorial, up to a constant. In another theorem, using Wallis' formula for π& , such constant is exactly determined, thus proving the Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  A  =  ( n  e.  NN  |->  ( ( ! `  n )  /  (
 ( sqr `  ( 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  B  =  ( n  e.  NN  |->  ( log `  ( A `  n ) ) )   =>    |-  E. c  e.  RR+  A  ~~>  c
 
Theoremstirlinglem15 27236* The Stirling's formula is proven using a number of local definitions. The main theorem stirling 27237 will use this final lemma, but it will not expose the local definitions. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  F/ n ph   &    |-  S  =  ( n  e.  NN0  |->  ( ( sqr `  ( (
 2  x.  pi )  x.  n ) )  x.  ( ( n 
 /  _e ) ^ n ) ) )   &    |-  A  =  ( n  e.  NN  |->  ( ( ! `
  n )  /  ( ( sqr `  (
 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) ) )   &    |-  D  =  ( n  e.  NN  |->  ( A `  ( 2  x.  n ) ) )   &    |-  E  =  ( n  e.  NN  |->  ( ( sqr `  (
 2  x.  n ) )  x.  ( ( n  /  _e ) ^ n ) ) )   &    |-  V  =  ( n  e.  NN  |->  ( ( ( ( 2 ^ ( 4  x.  n ) )  x.  ( ( ! `  n ) ^ 4
 ) )  /  (
 ( ! `  (
 2  x.  n ) ) ^ 2 ) )  /  ( ( 2  x.  n )  +  1 ) ) )   &    |-  F  =  ( n  e.  NN  |->  ( ( ( A `  n ) ^ 4
 )  /  ( ( D `  n ) ^
 2 ) ) )   &    |-  H  =  ( n  e.  NN  |->  ( ( n ^ 2 )  /  ( n  x.  (
 ( 2  x.  n )  +  1 )
 ) ) )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A  ~~>  C )   =>    |-  ( ph  ->  ( n  e.  NN  |->  ( ( ! `  n ) 
 /  ( S `  n ) ) )  ~~>  1 )
 
Theoremstirling 27237 Stirling's approximation formula for 
n factorial. The proof follows two major steps: first it is proven that  S and  n factorial are asymptotically equivalent, up to an unknown constant. Then, using Wallis' formula for π it is proven that the unknown constant is the square root of π and then the exact Stirling's formula is established. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  S  =  ( n  e.  NN0  |->  ( ( sqr `  (
 ( 2  x.  pi )  x.  n ) )  x.  ( ( n 
 /  _e ) ^ n ) ) )   =>    |-  ( n  e.  NN  |->  ( ( ! `  n )  /  ( S `  n ) ) )  ~~>  1
 
Theoremstirlingr 27238 Stirling's approximation formula for 
n factorial: here convergence is expressed with respect to the standard topology on the reals. The main theorem stirling 27237 is proven for convergence in the topology of complex numbers. The variable  R is used to denote convergence with respect to the standard topology on the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
 |-  S  =  ( n  e.  NN0  |->  ( ( sqr `  (
 ( 2  x.  pi )  x.  n ) )  x.  ( ( n 
 /  _e ) ^ n ) ) )   &    |-  R  =  ( ~~> t `  ( topGen `  ran  (,) )
 )   =>    |-  ( n  e.  NN  |->  ( ( ! `  n )  /  ( S `  n ) ) ) R 1
 
18.20  Mathbox for Jarvin Udandy
 
TheoremhirstL-ax3 27239 The third axiom of a system called "L" but proven to be a theorem since set.mm uses a different third axiom. This is named hirst after Holly P. Hirst and Jeffry L. Hirst. Axiom A3 of [Mendelson] p. 35. (Contributed by Jarvin Udandy, 7-Feb-2015.) (Proof modification is discouraged.)
 |-  (
 ( -.  ph  ->  -. 
 ps )  ->  (
 ( -.  ph  ->  ps )  ->  ph ) )
 
Theoremax3h 27240 Recovery of ax-3 9 from hirstL-ax3 27239. (Contributed by Jarvin Udandy, 3-Jul-2015.)
 |-  (
 ( -.  ph  ->  -. 
 ps )  ->  ( ps  ->  ph ) )
 
Theoremaibandbiaiffaiffb 27241 A closed form showing (a implies b and b implies a) same-as (a same-as b) (Contributed by Jarvin Udandy, 3-Sep-2016.)
 |-  (
 ( ( ph  ->  ps )  /\  ( ps 
 ->  ph ) )  <->  ( ph  <->  ps ) )
 
Theoremaibandbiaiaiffb 27242 A closed form showing (a implies b and b implies a) implies (a same-as b) (Contributed by Jarvin Udandy, 3-Sep-2016.)
 |-  (
 ( ( ph  ->  ps )  /\  ( ps 
 ->  ph ) )  ->  ( ph  <->  ps ) )
 
Theoremnotatnand 27243 Do not use. Use intnanr instead. Given not a, there exists a proof for not (a and b). (Contributed by Jarvin Udandy, 31-Aug-2016.)
 |-  -.  ph   =>    |-  -.  ( ph  /\  ps )
 
Theoremaistia 27244 Given a is equivalent to T., there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.)
 |-  ( ph 
 <->  T.  )   =>    |-  ph
 
Theoremaisfina 27245 Given a is equivalent to F., there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.)
 |-  ( ph 
 <->  F.  )   =>    |- 
 -.  ph
 
Theorembothtbothsame 27246 Given both a,b are equivalent to T., there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
 |-  ( ph 
 <->  T.  )   &    |-  ( ps  <->  T.  )   =>    |-  ( ph  <->  ps )
 
Theorembothfbothsame 27247 Given both a,b are equivalent to F., there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  F.  )   =>    |-  ( ph  <->  ps )
 
Theoremaiffbbtat 27248 Given a is equivalent to b, b is equivalent to T. there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
 |-  ( ph 
 <->  ps )   &    |-  ( ps  <->  T.  )   =>    |-  ( ph  <->  T.  )
 
Theoremaisbbisfaisf 27249 Given a is equivalent to b, b is equivalent to F. there exists a proof for a is equivalent to F. (Contributed by Jarvin Udandy, 30-Aug-2016.)
 |-  ( ph 
 <->  ps )   &    |-  ( ps  <->  F.  )   =>    |-  ( ph  <->  F.  )
 
Theoremaxorbtnotaiffb 27250 Given a is exclusive to b, there exists a proof for (not (a if-and-only-if b)) df-xor is a closed form of this. (Contributed by Jarvin Udandy, 7-Sep-2016.)
 |-  ( ph \/_ ps )   =>    |-  -.  ( ph  <->  ps )
 
Theoremaiffnbandciffatnotciffb 27251 Given a is equivalent to NOT b, c is equivalent to a. there exists a proof for ( not ( c iff b ) ). (Contributed by Jarvin Udandy, 7-Sep-2016.)
 |-  ( ph 
 <->  -.  ps )   &    |-  ( ch 
 <-> 
 ph )   =>    |- 
 -.  ( ch  <->  ps )
 
Theoremaxorbciffatcxorb 27252 Given a is equivalent to NOT b, c is equivalent to a. there exists a proof for ( c xor b ) . (Contributed by Jarvin Udandy, 7-Sep-2016.)
 |-  ( ph \/_ ps )   &    |-  ( ch 
 <-> 
 ph )   =>    |-  ( ch \/_ ps )
 
Theoremaibnbna 27253 Given a implies b, not b, there exists a proof for not a. (Contributed by Jarvin Udandy, 1-Sep-2016.)
 |-  ( ph  ->  ps )   &    |-  -.  ps   =>    |-  -.  ph
 
Theoremaibnbaif 27254 Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.)
 |-  ( ph  ->  ps )   &    |-  -.  ps   =>    |-  ( ph  <->  F.  )
 
Theoremaiffbtbat 27255 Given a is equivalent to b, T. is equivalent to b. there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
 |-  ( ph 
 <->  ps )   &    |-  (  T.  <->  ps )   =>    |-  ( ph  <->  T.  )
 
Theoremastbstanbst 27256 Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for a and b is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
 |-  ( ph 
 <->  T.  )   &    |-  ( ps  <->  T.  )   =>    |-  ( ( ph  /\ 
 ps )  <->  T.  )
 
Theoremaistbistaandb 27257 Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for (a and b). (Contributed by Jarvin Udandy, 9-Sep-2016.)
 |-  ( ph 
 <->  T.  )   &    |-  ( ps  <->  T.  )   =>    |-  ( ph  /\  ps )
 
Theoremaisbnaxb 27258 Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.)
 |-  ( ph 
 <->  ps )   =>    |- 
 -.  ( ph \/_ ps )
 
Theoremiatbtatnnb 27259 Given a implies b, there exists a proof for a implies not not b. (Contributed by Jarvin Udandy, 2-Sep-2016.)
 |-  ( ph  ->  ps )   =>    |-  ( ph  ->  -.  -.  ps )
 
Theorematbiffatnnb 27260 If a implies b, is is implied a implies not not b (Contributed by Jarvin Udandy, 28-Aug-2016.)
 |-  (
 ( ph  ->  ps )  ->  ( ph  ->  -.  -.  ps ) )
 
Theorembisaiaisb 27261 Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.)
 |-  (
 ( ps  <->  ph )  ->  ( ph 
 <->  ps ) )
 
Theorematbiffatnnbalt 27262 If a implies b, it is implied a implies not not b (Contributed by Jarvin Udandy, 29-Aug-2016.)
 |-  (
 ( ph  ->  ps )  ->  ( ph  ->  -.  -.  ps ) )
 
Theoremabnotbtaxb 27263 Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
 |-  ph   &    |-  -.  ps   =>    |-  ( ph \/_ ps )
 
Theoremabnotataxb 27264 Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
 |-  -.  ph   &    |-  ps   =>    |-  ( ph \/_ ps )
 
Theoremconimpf 27265 Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 28-Aug-2016.)
 |-  ph   &    |-  -.  ps   &    |-  ( ph  ->  ps )   =>    |-  ( ph  <->  F.  )
 
Theoremconimpfalt 27266 Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 29-Aug-2016.)
 |-  ph   &    |-  -.  ps   &    |-  ( ph  ->  ps )   =>    |-  ( ph  <->  F.  )
 
Theoremaistbisfiaxb 27267 Given a is equivalent to T., Given b is equivalent to F. there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
 |-  ( ph 
 <->  T.  )   &    |-  ( ps  <->  F.  )   =>    |-  ( ph \/_ ps )
 
Theoremaisfbistiaxb 27268 Given a is equivalent to F., Given b is equivalent to T., there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  T.  )   =>    |-  ( ph \/_ ps )
 
Theoremabcdta 27269 Given (((a and b) and c) and d), there exists a proof for a (Contributed by Jarvin Udandy, 3-Sep-2016.)
 |-  (
 ( ( ph  /\  ps )  /\  ch )  /\  th )   =>    |-  ph
 
Theoremabcdtb 27270 Given (((a and b) and c) and d), there exists a proof for b (Contributed by Jarvin Udandy, 3-Sep-2016.)
 |-  (
 ( ( ph  /\  ps )  /\  ch )  /\  th )   =>    |- 
 ps
 
Theoremabcdtc 27271 Given (((a and b) and c) and d), there exists a proof for c (Contributed by Jarvin Udandy, 3-Sep-2016.)
 |-  (
 ( ( ph  /\  ps )  /\  ch )  /\  th )   =>    |- 
 ch
 
Theoremabcdtd 27272 Given (((a and b) and c) and d), there exists a proof for d (Contributed by Jarvin Udandy, 3-Sep-2016.)
 |-  (
 ( ( ph  /\  ps )  /\  ch )  /\  th )   =>    |- 
 th
 
Theoremmdandyv0 27273 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  T.  )   &    |-  ( ch 
 <->  F.  )   &    |-  ( th  <->  F.  )   &    |-  ( ta  <->  F.  )   &    |-  ( et  <->  F.  )   =>    |-  ( ( ( ( ch  <->  ph )  /\  ( th 
 <-> 
 ph ) )  /\  ( ta  <->  ph ) )  /\  ( et  <->  ph ) )
 
Theoremmdandyv1 27274 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  T.  )   &    |-  ( ch 
 <->  T.  )   &    |-  ( th  <->  F.  )   &    |-  ( ta  <->  F.  )   &    |-  ( et  <->  F.  )   =>    |-  ( ( ( ( ch  <->  ps )  /\  ( th 
 <-> 
 ph ) )  /\  ( ta  <->  ph ) )  /\  ( et  <->  ph ) )
 
Theoremmdandyv2 27275 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  T.  )   &    |-  ( ch 
 <->  F.  )   &    |-  ( th  <->  T.  )   &    |-  ( ta 
 <->  F.  )   &    |-  ( et  <->  F.  )   =>    |-  ( ( ( ( ch  <->  ph )  /\  ( th 
 <->  ps ) )  /\  ( ta  <->  ph ) )  /\  ( et  <->  ph ) )
 
Theoremmdandyv3 27276 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  T.  )   &    |-  ( ch 
 <->  T.  )   &    |-  ( th  <->  T.  )   &    |-  ( ta 
 <->  F.  )   &    |-  ( et  <->  F.  )   =>    |-  ( ( ( ( ch  <->  ps )  /\  ( th 
 <->  ps ) )  /\  ( ta  <->  ph ) )  /\  ( et  <->  ph ) )
 
Theoremmdandyv4 27277 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  T.  )   &    |-  ( ch 
 <->  F.  )   &    |-  ( th  <->  F.  )   &    |-  ( ta  <->  T.  )   &    |-  ( et 
 <->  F.  )   =>    |-  ( ( ( ( ch  <->  ph )  /\  ( th 
 <-> 
 ph ) )  /\  ( ta  <->  ps ) )  /\  ( et  <->  ph ) )
 
Theoremmdandyv5 27278 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  T.  )   &    |-  ( ch 
 <->  T.  )   &    |-  ( th  <->  F.  )   &    |-  ( ta  <->  T.  )   &    |-  ( et 
 <->  F.  )   =>    |-  ( ( ( ( ch  <->  ps )  /\  ( th 
 <-> 
 ph ) )  /\  ( ta  <->  ps ) )  /\  ( et  <->  ph ) )
 
Theoremmdandyv6 27279 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  T.  )   &    |-  ( ch 
 <->  F.  )   &    |-  ( th  <->  T.  )   &    |-  ( ta 
 <->  T.  )   &    |-  ( et  <->  F.  )   =>    |-  ( ( ( ( ch  <->  ph )  /\  ( th 
 <->  ps ) )  /\  ( ta  <->  ps ) )  /\  ( et  <->  ph ) )
 
Theoremmdandyv7 27280 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  T.  )   &    |-  ( ch 
 <->  T.  )   &    |-  ( th  <->  T.  )   &    |-  ( ta 
 <->  T.  )   &    |-  ( et  <->  F.  )   =>    |-  ( ( ( ( ch  <->  ps )  /\  ( th 
 <->  ps ) )  /\  ( ta  <->  ps ) )  /\  ( et  <->  ph ) )
 
Theoremmdandyv8 27281 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  T.  )   &    |-  ( ch 
 <->  F.  )   &    |-  ( th  <->  F.  )   &    |-  ( ta  <->  F.  )   &    |-  ( et  <->  T.  )   =>    |-  ( ( ( ( ch  <->  ph )  /\  ( th 
 <-> 
 ph ) )  /\  ( ta  <->  ph ) )  /\  ( et  <->  ps ) )
 
Theoremmdandyv9 27282 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  T.  )   &    |-  ( ch 
 <->  T.  )   &    |-  ( th  <->  F.  )   &    |-  ( ta  <->  F.  )   &    |-  ( et  <->  T.  )   =>    |-  ( ( ( ( ch  <->  ps )  /\  ( th 
 <-> 
 ph ) )  /\  ( ta  <->  ph ) )  /\  ( et  <->  ps ) )
 
Theoremmdandyv10 27283 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  T.  )   &    |-  ( ch 
 <->  F.  )   &    |-  ( th  <->  T.  )   &    |-  ( ta 
 <->  F.  )   &    |-  ( et  <->  T.  )   =>    |-  ( ( ( ( ch  <->  ph )  /\  ( th 
 <->  ps ) )  /\  ( ta  <->  ph ) )  /\  ( et  <->  ps ) )
 
Theoremmdandyv11 27284 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  T.  )   &    |-  ( ch 
 <->  T.  )   &    |-  ( th  <->  T.  )   &    |-  ( ta 
 <->  F.  )   &    |-  ( et  <->  T.  )   =>    |-  ( ( ( ( ch  <->  ps )  /\  ( th 
 <->  ps ) )  /\  ( ta  <->  ph ) )  /\  ( et  <->  ps ) )
 
Theoremmdandyv12 27285 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  T.  )   &    |-  ( ch 
 <->  F.  )   &    |-  ( th  <->  F.  )   &    |-  ( ta  <->  T.  )   &    |-  ( et 
 <->  T.  )   =>    |-  ( ( ( ( ch  <->  ph )  /\  ( th 
 <-> 
 ph ) )  /\  ( ta  <->  ps ) )  /\  ( et  <->  ps ) )
 
Theoremmdandyv13 27286 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  T.  )   &    |-  ( ch 
 <->  T.  )   &    |-  ( th  <->  F.  )   &    |-  ( ta  <->  T.  )   &    |-  ( et 
 <->  T.  )   =>    |-  ( ( ( ( ch  <->  ps )  /\  ( th 
 <-> 
 ph ) )  /\  ( ta  <->  ps ) )  /\  ( et  <->  ps ) )
 
Theoremmdandyv14 27287 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  T.  )   &    |-  ( ch 
 <->  F.  )   &    |-  ( th  <->  T.  )   &    |-  ( ta 
 <->  T.  )   &    |-  ( et  <->  T.  )   =>    |-  ( ( ( ( ch  <->  ph )  /\  ( th 
 <->  ps ) )  /\  ( ta  <->  ps ) )  /\  ( et  <->  ps ) )
 
Theoremmdandyv15 27288 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
 |-  ( ph 
 <->  F.  )   &    |-  ( ps  <->  T.  )   &    |-  ( ch 
 <->  T.  )   &    |-  ( th  <->  T.  )   &    |-  ( ta 
 <->  T.  )   &    |-  ( et  <->  T.  )   =>    |-  ( ( ( ( ch  <->  ps )  /\  ( th 
 <->  ps ) )  /\  ( ta  <->  ps ) )  /\  ( et  <->  ps ) )
 
Theoremmdandyvr0 27289 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
 |-  ( ph 
 <->  ze )   &    |-  ( ps  <->  si )   &    |-  ( ch  <->  ph )   &    |-  ( th  <->  ph )   &    |-  ( ta  <->  ph )   &    |-  ( et  <->  ph )   =>    |-  ( ( ( ( ch  <->  ze )  /\  ( th 
 <->  ze ) )  /\  ( ta  <->  ze ) )  /\  ( et  <->  ze ) )
 
Theoremmdandyvr1 27290 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
 |-  ( ph 
 <->  ze )   &    |-  ( ps  <->  si )   &    |-  ( ch  <->  ps )   &    |-  ( th  <->  ph )   &    |-  ( ta  <->  ph )   &    |-  ( et  <->  ph )   =>    |-  ( ( ( ( ch  <->  si )  /\  ( th 
 <->  ze ) )  /\  ( ta  <->  ze ) )  /\  ( et  <->  ze ) )
 
Theoremmdandyvr2 27291 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
 |-  ( ph 
 <->  ze )   &    |-  ( ps  <->  si )   &    |-  ( ch  <->  ph )   &    |-  ( th  <->  ps )   &    |-  ( ta  <->  ph )   &    |-  ( et  <->  ph )   =>    |-  ( ( ( ( ch  <->  ze )  /\  ( th 
 <-> 
 si ) )  /\  ( ta  <->  ze ) )  /\  ( et  <->  ze ) )
 
Theoremmdandyvr3 27292 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
 |-  ( ph 
 <->  ze )   &    |-  ( ps  <->  si )   &    |-  ( ch  <->  ps )   &    |-  ( th  <->  ps )   &    |-  ( ta  <->  ph )   &    |-  ( et  <->  ph )   =>    |-  ( ( ( ( ch  <->  si )  /\  ( th 
 <-> 
 si ) )  /\  ( ta  <->  ze ) )  /\  ( et  <->  ze ) )
 
Theoremmdandyvr4 27293 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
 |-  ( ph 
 <->  ze )   &    |-  ( ps  <->  si )   &    |-  ( ch  <->  ph )   &    |-  ( th  <->  ph )   &    |-  ( ta  <->  ps )   &    |-  ( et  <->  ph )   =>    |-  ( ( ( ( ch  <->  ze )  /\  ( th 
 <->  ze ) )  /\  ( ta  <->  si ) )  /\  ( et  <->  ze ) )
 
Theoremmdandyvr5 27294 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
 |-  ( ph 
 <->  ze )   &    |-  ( ps  <->  si )   &    |-  ( ch  <->  ps )   &    |-  ( th  <->  ph )   &    |-  ( ta  <->  ps )   &    |-  ( et  <->  ph )   =>    |-  ( ( ( ( ch  <->  si )  /\  ( th 
 <->  ze ) )  /\  ( ta  <->  si ) )  /\  ( et  <->  ze ) )
 
Theoremmdandyvr6 27295 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
 |-  ( ph 
 <->  ze )   &    |-  ( ps  <->  si )   &    |-  ( ch  <->  ph )   &    |-  ( th  <->  ps )   &    |-  ( ta  <->  ps )   &    |-  ( et  <->  ph )   =>    |-  ( ( ( ( ch  <->  ze )  /\  ( th 
 <-> 
 si ) )  /\  ( ta  <->  si ) )  /\  ( et  <->  ze ) )
 
Theoremmdandyvr7 27296 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
 |-  ( ph 
 <->  ze )   &    |-  ( ps  <->  si )   &    |-  ( ch  <->  ps )   &    |-  ( th  <->  ps )   &    |-  ( ta  <->  ps )   &    |-  ( et  <->  ph )   =>    |-  ( ( ( ( ch  <->  si )  /\  ( th 
 <-> 
 si ) )  /\  ( ta  <->  si ) )  /\  ( et  <->  ze ) )
 
Theoremmdandyvr8 27297 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
 |-  ( ph 
 <->  ze )   &    |-  ( ps  <->  si )   &    |-  ( ch  <->  ph )   &    |-  ( th  <->  ph )   &    |-  ( ta  <->  ph )   &    |-  ( et  <->  ps )   =>    |-  ( ( ( ( ch  <->  ze )  /\  ( th 
 <->  ze ) )  /\  ( ta  <->  ze ) )  /\  ( et  <->  si ) )
 
Theoremmdandyvr9 27298 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
 |-  ( ph 
 <->  ze )   &    |-  ( ps  <->  si )   &    |-  ( ch  <->  ps )   &    |-  ( th  <->  ph )   &    |-  ( ta  <->  ph )   &    |-  ( et  <->  ps )   =>    |-  ( ( ( ( ch  <->  si )  /\  ( th 
 <->  ze ) )  /\  ( ta  <->  ze ) )  /\  ( et  <->  si ) )
 
Theoremmdandyvr10 27299 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
 |-  ( ph 
 <->  ze )   &    |-  ( ps  <->  si )   &    |-  ( ch  <->  ph )   &    |-  ( th  <->  ps )   &    |-  ( ta  <->  ph )   &    |-  ( et  <->  ps )   =>    |-  ( ( ( ( ch  <->  ze )  /\  ( th 
 <-> 
 si ) )  /\  ( ta  <->  ze ) )  /\  ( et  <->  si ) )
 
Theoremmdandyvr11 27300 Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
 |-  ( ph 
 <->  ze )   &    |-  ( ps  <->  si )   &    |-  ( ch  <->  ps )   &    |-  ( th  <->  ps )   &    |-  ( ta  <->  ph )   &    |-  ( et  <->  ps )   =>    |-  ( ( ( ( ch  <->  si )  /\  ( th 
 <-> 
 si ) )  /\  ( ta  <->  ze ) )  /\  ( et  <->  si ) )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19100 192 19101-19200 193 19201-19300 194 19301-19400 195 19401-19500 196 19501-19600 197 19601-19700 198 19701-19800 199 19801-19900 200 19901-20000 201 20001-20100 202 20101-20200 203 20201-20300 204 20301-20400 205 20401-20500 206 20501-20600 207 20601-20700 208 20701-20800 209 20801-20900 210 20901-21000 211 21001-21100 212 21101-21200 213 21201-21300 214 21301-21400 215 21401-21500 216 21501-21600 217 21601-21700 218 21701-21800 219 21801-21900 220 21901-22000 221 22001-22100 222 22101-22200 223 22201-22300 224 22301-22400 225 22401-22500 226 22501-22600 227 22601-22700 228 22701-22800 229 22801-22900 230 22901-23000 231 23001-23100 232 23101-23200 233 23201-23300 234 23301-23400 235 23401-23500 236 23501-23600 237 23601-23700 238 23701-23800 239 23801-23900 240 23901-24000 241 24001-24100 242 24101-24200 243 24201-24300 244 24301-24400 245 24401-24500 246 24501-24600 247 24601-24700 248 24701-24800 249 24801-24900 250 24901-25000 251 25001-25100 252 25101-25200 253 25201-25300 254 25301-25400 255 25401-25500 256 25501-25600 257 25601-25700 258 25701-25800 259 25801-25900 260 25901-26000 261 26001-26100 262 26101-26200 263 26201-26300 264 26301-26400 265 26401-26500 266 26501-26600 267 26601-26700 268 26701-26800 269 26801-26900 270 26901-27000 271 27001-27100 272 27101-27200 273 27201-27300 274 27301-27400 275 27401-27500 276 27501-27600 277 27601-27700 278 27701-27800 279 27801-27900 280 27901-28000 281 28001-28100 282 28101-28200 283 28201-28300 284 28301-28400 285 28401-28500 286 28501-28600 287 28601-28700 288 28701-28800 289 28801-28900 290 28901-29000 291 29001-29100 292 29101-29200 293 29201-29300 294 29301-29400 295 29401-29500 296 29501-29600 297 29601-29700 298 29701-29800 299 29801-29900 300 29901-30000 301 30001-30100 302 30101-30200 303 30201-30300 304 30301-30400 305 30401-30500 306 30501-30600 307 30601-30700 308 30701-30800 309 30801-30900 310 30901-31000 311 31001-31100 312 31101-31200 313 31201-31300 314 31301-31400 315 31401-31421
  Copyright terms: Public domain < Previous  Next >