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

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

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-26619)
  Hilbert Space Explorer  Hilbert Space Explorer
(26620-28142)
  Users' Mathboxes  Users' Mathboxes
(28143-40812)
 

Theorem List for Metamath Proof Explorer - 38101-38200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremfourierdlem94 38101* For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  T  =  ( 2  x.  pi )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  P  =  ( n  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... n ) )  |  ( ( ( p `
  0 )  =  -u pi  /\  ( p `
  n )  =  pi )  /\  A. i  e.  ( 0..^ n ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR  _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( RR 
 _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `
  i ) )  =/=  (/) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( RR 
 _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `
  ( i  +  1 ) ) )  =/=  (/) )   =>    |-  ( ph  ->  (
 ( ( F  |`  ( -oo (,)
 X ) ) lim CC  X )  =/=  (/)  /\  (
 ( F  |`  ( X (,) +oo ) ) lim CC  X )  =/=  (/) ) )
 
Theoremfourierdlem95 38102* Algebraic manipulation of integrals, used by other lemmas. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  ( -u pi  +  X )  /\  ( p `  m )  =  ( pi  +  X ) ) 
 /\  A. i  e.  (
 0..^ m ) ( p `  i )  <  ( p `  ( i  +  1
 ) ) ) }
 )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  V  e.  ( P `  M ) )   &    |-  ( ph  ->  X  e.  ran  V )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( V `
  i ) (,) ( V `  (
 i  +  1 ) ) ) ) lim CC  ( V `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( V `
  i ) (,) ( V `  (
 i  +  1 ) ) ) ) lim CC  ( V `  ( i  +  1 ) ) ) )   &    |-  H  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  (
 ( ( F `  ( X  +  s
 ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )   &    |-  K  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  (
 s  /  ( 2  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) )   &    |-  U  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( H `  s
 )  x.  ( K `
  s ) ) )   &    |-  S  =  ( s  e.  ( -u pi [,] pi )  |->  ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  s ) ) )   &    |-  G  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( U `  s
 )  x.  ( S `
  s ) ) )   &    |-  I  =  ( RR  _D  F )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( I  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) --> RR )   &    |-  ( ph  ->  B  e.  (
 ( I  |`  ( -oo (,)
 X ) ) lim CC  X ) )   &    |-  ( ph  ->  C  e.  (
 ( I  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  ( ph  ->  Y  e.  (
 ( F  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  ( ph  ->  W  e.  (
 ( F  |`  ( -oo (,)
 X ) ) lim CC  X ) )   &    |-  ( ph  ->  A  e.  dom  vol )   &    |-  ( ph  ->  A 
 C_  ( ( -u pi [,] pi )  \  { 0 } )
 )   &    |-  E  =  ( n  e.  NN  |->  ( S. A ( G `  s )  _d s  /  pi ) )   &    |-  D  =  ( n  e.  NN  |->  ( s  e.  RR  |->  if ( ( s  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  /  (
 2  x.  pi ) ) ,  ( ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  s ) ) 
 /  ( ( 2  x.  pi )  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) ) )   &    |-  ( ph  ->  O  e.  RR )   &    |-  (
 ( ph  /\  s  e.  A )  ->  if ( 0  <  s ,  Y ,  W )  =  O )   &    |-  (
 ( ph  /\  n  e. 
 NN )  ->  S. A ( ( D `
  n ) `  s )  _d s  =  ( 1  /  2
 ) )   =>    |-  ( ( ph  /\  n  e.  NN )  ->  (
 ( E `  n )  +  ( O  /  2 ) )  =  S. A ( ( F `  ( X  +  s ) )  x.  ( ( D `
  n ) `  s ) )  _d s )
 
Theoremfourierdlem96 38103* limit for  F at the lower bound of an interval for the moved partition  V. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  (
 ( ph  /\  x  e. 
 RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  ( C (,) +oo ) )   &    |-  ( ph  ->  J  e.  (
 0..^ ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q } ) )  -  1 ) ) )   &    |-  V  =  ( iota g g  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  | 
 E. k  e.  ZZ  ( y  +  (
 k  x.  T ) )  e.  ran  Q } ) )  -  1 ) ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. h  e.  ZZ  ( y  +  ( h  x.  T ) )  e.  ran  Q } ) ) )   =>    |-  ( ph  ->  if (
 ( ( u  e.  ( A (,] B )  |->  if ( u  =  B ,  A ,  u ) ) `  ( ( v  e. 
 RR  |->  ( v  +  ( ( |_ `  (
 ( B  -  v
 )  /  T )
 )  x.  T ) ) ) `  ( V `  J ) ) )  =  ( Q `
  ( ( y  e.  RR  |->  sup ( { j  e.  (
 0..^ M )  |  ( Q `  j
 )  <_  ( ( u  e.  ( A (,] B )  |->  if ( u  =  B ,  A ,  u )
 ) `  ( (
 v  e.  RR  |->  ( v  +  ( ( |_ `  ( ( B  -  v ) 
 /  T ) )  x.  T ) ) ) `  y ) ) } ,  RR ,  <  ) ) `  ( V `  J ) ) ) ,  (
 ( i  e.  (
 0..^ M )  |->  R ) `  ( ( y  e.  RR  |->  sup ( { j  e.  ( 0..^ M )  |  ( Q `  j )  <_  ( ( u  e.  ( A (,] B )  |->  if ( u  =  B ,  A ,  u ) ) `  ( ( v  e.  RR  |->  ( v  +  ( ( |_ `  ( ( B  -  v ) 
 /  T ) )  x.  T ) ) ) `  y ) ) } ,  RR ,  <  ) ) `  ( V `  J ) ) ) ,  ( F `  ( ( u  e.  ( A (,] B )  |->  if ( u  =  B ,  A ,  u ) ) `  ( ( v  e. 
 RR  |->  ( v  +  ( ( |_ `  (
 ( B  -  v
 )  /  T )
 )  x.  T ) ) ) `  ( V `  J ) ) ) ) )  e.  ( ( F  |`  ( ( V `  J ) (,) ( V `  ( J  +  1
 ) ) ) ) lim
 CC  ( V `  J ) ) )
 
Theoremfourierdlem97 38104*  F is continuous on the intervals induced by the moved partition  V. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  G  =  ( RR  _D  F )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  e.  RR )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  (
 ( ph  /\  x  e. 
 RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  ( C (,) +oo ) )   &    |-  ( ph  ->  J  e.  (
 0..^ ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q } ) )  -  1 ) ) )   &    |-  V  =  ( iota g g  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  | 
 E. k  e.  ZZ  ( y  +  (
 k  x.  T ) )  e.  ran  Q } ) )  -  1 ) ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. h  e.  ZZ  ( y  +  ( h  x.  T ) )  e.  ran  Q } ) ) )   &    |-  H  =  ( s  e.  RR  |->  if ( s  e. 
 dom  G ,  ( G `
  s ) ,  0 ) )   =>    |-  ( ph  ->  ( G  |`  ( ( V `  J ) (,) ( V `  ( J  +  1 )
 ) ) )  e.  ( ( ( V `
  J ) (,) ( V `  ( J  +  1 )
 ) ) -cn-> CC )
 )
 
Theoremfourierdlem98 38105*  F is continuous on the intervals induced by the moved partition  V. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  (
 ( ph  /\  x  e. 
 RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  ( C (,) +oo ) )   &    |-  ( ph  ->  J  e.  (
 0..^ ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q } ) )  -  1 ) ) )   &    |-  V  =  ( iota g g  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  | 
 E. k  e.  ZZ  ( y  +  (
 k  x.  T ) )  e.  ran  Q } ) )  -  1 ) ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. h  e.  ZZ  ( y  +  ( h  x.  T ) )  e.  ran  Q } ) ) )   =>    |-  ( ph  ->  ( F  |`  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  e.  ( ( ( V `  J ) (,) ( V `  ( J  +  1
 ) ) ) -cn-> CC ) )
 
Theoremfourierdlem99 38106* limit for  F at the upper bound of an interval for the moved partition  V. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  (
 ( ph  /\  x  e. 
 RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  ( C (,) +oo ) )   &    |-  ( ph  ->  J  e.  (
 0..^ ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q } ) )  -  1 ) ) )   &    |-  V  =  ( iota g g  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  | 
 E. k  e.  ZZ  ( y  +  (
 k  x.  T ) )  e.  ran  Q } ) )  -  1 ) ) ,  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. h  e.  ZZ  ( y  +  ( h  x.  T ) )  e.  ran  Q } ) ) )   =>    |-  ( ph  ->  if (
 ( ( v  e. 
 RR  |->  ( v  +  ( ( |_ `  (
 ( B  -  v
 )  /  T )
 )  x.  T ) ) ) `  ( V `  ( J  +  1 ) ) )  =  ( Q `  ( ( ( y  e.  RR  |->  sup ( { j  e.  (
 0..^ M )  |  ( Q `  j
 )  <_  ( ( u  e.  ( A (,] B )  |->  if ( u  =  B ,  A ,  u )
 ) `  ( (
 v  e.  RR  |->  ( v  +  ( ( |_ `  ( ( B  -  v ) 
 /  T ) )  x.  T ) ) ) `  y ) ) } ,  RR ,  <  ) ) `  ( V `  J ) )  +  1 ) ) ,  ( ( i  e.  ( 0..^ M )  |->  L ) `
  ( ( y  e.  RR  |->  sup ( { j  e.  (
 0..^ M )  |  ( Q `  j
 )  <_  ( ( u  e.  ( A (,] B )  |->  if ( u  =  B ,  A ,  u )
 ) `  ( (
 v  e.  RR  |->  ( v  +  ( ( |_ `  ( ( B  -  v ) 
 /  T ) )  x.  T ) ) ) `  y ) ) } ,  RR ,  <  ) ) `  ( V `  J ) ) ) ,  ( F `  ( ( v  e.  RR  |->  ( v  +  ( ( |_ `  ( ( B  -  v )  /  T ) )  x.  T ) ) ) `  ( V `  ( J  +  1 ) ) ) ) )  e.  (
 ( F  |`  ( ( V `  J ) (,) ( V `  ( J  +  1
 ) ) ) ) lim
 CC  ( V `  ( J  +  1
 ) ) ) )
 
Theoremfourierdlem100 38107* A piecewise continuous function is integrable on any closed interval. This lemma uses local definitions, so that the proof is more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  F : RR --> CC )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T )
 )  =  ( F `
  x ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
 ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  ( C (,) +oo ) )   &    |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  C  /\  ( p `
  m )  =  D )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  N  =  ( ( # `  H )  -  1 )   &    |-  H  =  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q } )   &    |-  S  =  (
 iota f f  Isom  <  ,  <  ( ( 0
 ... N ) ,  H ) )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  (
 ( |_ `  (
 ( B  -  x )  /  T ) )  x.  T ) ) )   &    |-  J  =  ( y  e.  ( A (,] B )  |->  if ( y  =  B ,  A ,  y ) )   &    |-  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( J `
  ( E `  x ) ) } ,  RR ,  <  )
 )   =>    |-  ( ph  ->  ( x  e.  ( C [,] D )  |->  ( F `
  x ) )  e.  L^1 )
 
Theoremfourierdlem101 38108* Integral by substitution for a piecewise continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  D  =  ( n  e.  NN  |->  ( s  e.  RR  |->  if ( ( s  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  /  (
 2  x.  pi ) ) ,  ( ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  s ) ) 
 /  ( ( 2  x.  pi )  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) ) )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  -u pi  /\  ( p `
  m )  =  pi )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  G  =  ( t  e.  ( -u pi [,] pi ) 
 |->  ( ( F `  t )  x.  (
 ( D `  N ) `  ( t  -  X ) ) ) )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  F : (
 -u pi [,] pi )
 --> CC )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   =>    |-  ( ph  ->  S. ( -u pi [,] pi ) ( ( F `
  t )  x.  ( ( D `  N ) `  (
 t  -  X ) ) )  _d t  =  S. ( (
 -u pi  -  X ) [,] ( pi  -  X ) ) ( ( F `  ( X  +  s )
 )  x.  ( ( D `  N ) `
  s ) )  _d s )
 
Theoremfourierdlem102 38109* For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  T  =  ( 2  x.  pi )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  G  =  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )   &    |-  ( ph  ->  ( ( -u pi (,) pi )  \  dom  G )  e.  Fin )   &    |-  ( ph  ->  G  e.  ( dom  G -cn-> CC ) )   &    |-  ( ( ph  /\  x  e.  ( (
 -u pi [,) pi )  \  dom  G ) )  ->  ( ( G  |`  ( x (,) +oo ) ) lim CC  x )  =/=  (/) )   &    |-  ( ( ph  /\  x  e.  ( (
 -u pi (,] pi )  \  dom  G ) )  ->  ( ( G  |`  ( -oo (,) x ) ) lim CC  x )  =/=  (/) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  P  =  ( n  e.  NN  |->  { p  e.  ( RR  ^m  (
 0 ... n ) )  |  ( ( ( p `  0 )  =  -u pi  /\  ( p `  n )  =  pi )  /\  A. i  e.  ( 0..^ n ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  (
 ( |_ `  (
 ( pi  -  x )  /  T ) )  x.  T ) ) )   &    |-  H  =  ( { -u pi ,  pi ,  ( E `  X ) }  u.  (
 ( -u pi [,] pi )  \  dom  G ) )   &    |-  M  =  ( ( # `  H )  -  1 )   &    |-  Q  =  ( iota g g 
 Isom  <  ,  <  (
 ( 0 ... M ) ,  H )
 )   =>    |-  ( ph  ->  (
 ( ( F  |`  ( -oo (,)
 X ) ) lim CC  X )  =/=  (/)  /\  (
 ( F  |`  ( X (,) +oo ) ) lim CC  X )  =/=  (/) ) )
 
Theoremfourierdlem103 38110* The half lower part of the integral equal to the fourier partial sum, converges to half the left limit of the original function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  ( -u pi  +  X )  /\  ( p `  m )  =  ( pi  +  X ) ) 
 /\  A. i  e.  (
 0..^ m ) ( p `  i )  <  ( p `  ( i  +  1
 ) ) ) }
 )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  V  e.  ( P `  M ) )   &    |-  ( ph  ->  X  e.  ran  V )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  E. w  e.  RR  A. t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) ( abs `  ( F `  t ) )  <_  w )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR  _D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) -cn-> RR ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  E. z  e.  RR  A. t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) ( abs `  ( ( RR  _D  F ) `  t ) )  <_  z )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( V `
  i ) (,) ( V `  (
 i  +  1 ) ) ) ) lim CC  ( V `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( V `
  i ) (,) ( V `  (
 i  +  1 ) ) ) ) lim CC  ( V `  ( i  +  1 ) ) ) )   &    |-  H  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  (
 ( ( F `  ( X  +  s
 ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )   &    |-  K  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  (
 s  /  ( 2  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) )   &    |-  U  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( H `  s
 )  x.  ( K `
  s ) ) )   &    |-  S  =  ( s  e.  ( -u pi [,] pi )  |->  ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  s ) ) )   &    |-  G  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( U `  s
 )  x.  ( S `
  s ) ) )   &    |-  Z  =  ( m  e.  NN  |->  S. ( -u pi (,) 0
 ) ( ( F `
  ( X  +  s ) )  x.  ( ( D `  m ) `  s
 ) )  _d s )   &    |-  E  =  ( n  e.  NN  |->  ( S. ( -u pi (,) 0 ) ( G `
  s )  _d s  /  pi ) )   &    |-  ( ph  ->  Y  e.  ( ( F  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  ( ph  ->  W  e.  ( ( F  |`  ( -oo (,) X ) ) lim CC  X ) )   &    |-  ( ph  ->  A  e.  ( ( ( RR  _D  F )  |`  ( -oo (,) X ) ) lim CC  X ) )   &    |-  ( ph  ->  B  e.  ( ( ( RR  _D  F )  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  D  =  ( n  e.  NN  |->  ( s  e.  RR  |->  if ( ( s  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  /  (
 2  x.  pi ) ) ,  ( ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  s ) ) 
 /  ( ( 2  x.  pi )  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) ) )   &    |-  O  =  ( U  |`  ( -u pi [,] d ) )   &    |-  T  =  ( { -u pi ,  d }  u.  ( ran  Q  i^i  ( -u pi (,) d ) ) )   &    |-  N  =  ( ( # `  T )  -  1 )   &    |-  J  =  ( iota f f 
 Isom  <  ,  <  (
 ( 0 ... N ) ,  T )
 )   &    |-  Q  =  ( i  e.  ( 0 ...
 M )  |->  ( ( V `  i )  -  X ) )   &    |-  C  =  ( iota_ l  e.  ( 0..^ M ) ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) 
 C_  ( ( Q `
  l ) (,) ( Q `  (
 l  +  1 ) ) ) )   &    |-  ( ch 
 <->  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  d  e.  ( -u pi (,) 0
 ) )  /\  k  e.  NN )  /\  ( abs `  S. ( d (,) 0 ) ( ( U `  s
 )  x.  ( sin `  ( ( k  +  ( 1  /  2
 ) )  x.  s
 ) ) )  _d s )  <  (
 e  /  2 )
 )  /\  ( abs `  S. ( -u pi (,) d ) ( ( U `  s )  x.  ( sin `  (
 ( k  +  (
 1  /  2 )
 )  x.  s ) ) )  _d s )  <  ( e 
 /  2 ) ) )   =>    |-  ( ph  ->  Z  ~~>  ( W  /  2
 ) )
 
Theoremfourierdlem104 38111* The half upper part of the integral equal to the fourier partial sum, converges to half the right limit of the original function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  ( ph  ->  X  e.  RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  ( -u pi  +  X )  /\  ( p `  m )  =  ( pi  +  X ) ) 
 /\  A. i  e.  (
 0..^ m ) ( p `  i )  <  ( p `  ( i  +  1
 ) ) ) }
 )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  V  e.  ( P `  M ) )   &    |-  ( ph  ->  X  e.  ran  V )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  E. w  e.  RR  A. t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) ( abs `  ( F `  t ) )  <_  w )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR  _D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) -cn-> RR ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  E. z  e.  RR  A. t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1
 ) ) ) ( abs `  ( ( RR  _D  F ) `  t ) )  <_  z )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( V `
  i ) (,) ( V `  (
 i  +  1 ) ) ) ) lim CC  ( V `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( V `
  i ) (,) ( V `  (
 i  +  1 ) ) ) ) lim CC  ( V `  ( i  +  1 ) ) ) )   &    |-  H  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  (
 ( ( F `  ( X  +  s
 ) )  -  if ( 0  <  s ,  Y ,  W ) )  /  s ) ) )   &    |-  K  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  (
 s  /  ( 2  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) )   &    |-  U  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( H `  s
 )  x.  ( K `
  s ) ) )   &    |-  S  =  ( s  e.  ( -u pi [,] pi )  |->  ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  s ) ) )   &    |-  G  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( U `  s
 )  x.  ( S `
  s ) ) )   &    |-  Z  =  ( m  e.  NN  |->  S. ( 0 (,) pi ) ( ( F `
  ( X  +  s ) )  x.  ( ( D `  m ) `  s
 ) )  _d s )   &    |-  E  =  ( n  e.  NN  |->  ( S. ( 0 (,)
 pi ) ( G `
  s )  _d s  /  pi ) )   &    |-  ( ph  ->  Y  e.  ( ( F  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  ( ph  ->  W  e.  ( ( F  |`  ( -oo (,) X ) ) lim CC  X ) )   &    |-  ( ph  ->  A  e.  ( ( ( RR  _D  F )  |`  ( -oo (,) X ) ) lim CC  X ) )   &    |-  ( ph  ->  B  e.  ( ( ( RR  _D  F )  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  D  =  ( n  e.  NN  |->  ( s  e.  RR  |->  if ( ( s  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  /  (
 2  x.  pi ) ) ,  ( ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  s ) ) 
 /  ( ( 2  x.  pi )  x.  ( sin `  (
 s  /  2 )
 ) ) ) ) ) )   &    |-  O  =  ( U  |`  ( d [,] pi ) )   &    |-  T  =  ( { d ,  pi }  u.  ( ran  Q  i^i  ( d (,) pi ) ) )   &    |-  N  =  ( ( # `  T )  -  1 )   &    |-  J  =  ( iota f f 
 Isom  <  ,  <  (
 ( 0 ... N ) ,  T )
 )   &    |-  Q  =  ( i  e.  ( 0 ...
 M )  |->  ( ( V `  i )  -  X ) )   &    |-  C  =  ( iota_ l  e.  ( 0..^ M ) ( ( J `  k ) (,) ( J `  ( k  +  1 ) ) ) 
 C_  ( ( Q `
  l ) (,) ( Q `  (
 l  +  1 ) ) ) )   &    |-  ( ch 
 <->  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  d  e.  ( 0 (,) pi ) )  /\  k  e. 
 NN )  /\  ( abs `  S. ( 0 (,) d ) ( ( U `  s
 )  x.  ( sin `  ( ( k  +  ( 1  /  2
 ) )  x.  s
 ) ) )  _d s )  <  (
 e  /  2 )
 )  /\  ( abs `  S. ( d (,)
 pi ) ( ( U `  s )  x.  ( sin `  (
 ( k  +  (
 1  /  2 )
 )  x.  s ) ) )  _d s )  <  ( e 
 /  2 ) ) )   =>    |-  ( ph  ->  Z  ~~>  ( Y  /  2
 ) )
 
Theoremfourierdlem105 38112* A piecewise continuous function is integrable on any closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  F : RR --> CC )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T )
 )  =  ( F `
  x ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
 ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  D  e.  ( C (,) +oo ) )   =>    |-  ( ph  ->  ( x  e.  ( C [,] D )  |->  ( F `  x ) )  e.  L^1 )
 
Theoremfourierdlem106 38113* For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  T  =  ( 2  x.  pi )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  G  =  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )   &    |-  ( ph  ->  ( ( -u pi (,) pi )  \  dom  G )  e.  Fin )   &    |-  ( ph  ->  G  e.  ( dom  G -cn-> CC ) )   &    |-  ( ( ph  /\  x  e.  ( (
 -u pi [,) pi )  \  dom  G ) )  ->  ( ( G  |`  ( x (,) +oo ) ) lim CC  x )  =/=  (/) )   &    |-  ( ( ph  /\  x  e.  ( (
 -u pi (,] pi )  \  dom  G ) )  ->  ( ( G  |`  ( -oo (,) x ) ) lim CC  x )  =/=  (/) )   &    |-  ( ph  ->  X  e.  RR )   =>    |-  ( ph  ->  (
 ( ( F  |`  ( -oo (,)
 X ) ) lim CC  X )  =/=  (/)  /\  (
 ( F  |`  ( X (,) +oo ) ) lim CC  X )  =/=  (/) ) )
 
Theoremfourierdlem107 38114* The integral of a piecewise continuous periodic function  F is unchanged if the domain is shifted by any positive value  X. This lemma generalizes fourierdlem92 38099 where the integral was shifted by the exact period. This lemma uses local definitions, so that the proof is more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  X  e.  RR+ )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  F : RR --> CC )   &    |-  (
 ( ph  /\  x  e. 
 RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   &    |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  ( A  -  X )  /\  ( p `  m )  =  A )  /\  A. i  e.  ( 0..^ m ) ( p `  i
 )  <  ( p `  ( i  +  1 ) ) ) }
 )   &    |-  H  =  ( {
 ( A  -  X ) ,  A }  u.  { y  e.  (
 ( A  -  X ) [,] A )  | 
 E. k  e.  ZZ  ( y  +  (
 k  x.  T ) )  e.  ran  Q } )   &    |-  N  =  ( ( # `  H )  -  1 )   &    |-  S  =  ( iota f f 
 Isom  <  ,  <  (
 ( 0 ... N ) ,  H )
 )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )   &    |-  Z  =  ( y  e.  ( A (,] B )  |->  if ( y  =  B ,  A ,  y ) )   &    |-  I  =  ( x  e.  RR  |->  sup ( { i  e.  ( 0..^ M )  |  ( Q `  i )  <_  ( Z `
  ( E `  x ) ) } ,  RR ,  <  )
 )   =>    |-  ( ph  ->  S. ( ( A  -  X ) [,] ( B  -  X ) ) ( F `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x )
 
Theoremfourierdlem108 38115* The integral of a piecewise continuous periodic function  F is unchanged if the domain is shifted by any positive value  X. This lemma generalizes fourierdlem92 38099 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  X  e.  RR+ )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  F : RR --> CC )   &    |-  (
 ( ph  /\  x  e. 
 RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   =>    |-  ( ph  ->  S. ( ( A  -  X ) [,] ( B  -  X ) ) ( F `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x )
 
Theoremfourierdlem109 38116* The integral of a piecewise continuous periodic function  F is unchanged if the domain is shifted by any value  X. This lemma generalizes fourierdlem92 38099 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  X  e.  RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  F : RR --> CC )   &    |-  (
 ( ph  /\  x  e. 
 RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   &    |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  ( A  -  X )  /\  ( p `  m )  =  ( B  -  X ) ) 
 /\  A. i  e.  (
 0..^ m ) ( p `  i )  <  ( p `  ( i  +  1
 ) ) ) }
 )   &    |-  H  =  ( {
 ( A  -  X ) ,  ( B  -  X ) }  u.  { x  e.  ( ( A  -  X ) [,] ( B  -  X ) )  | 
 E. k  e.  ZZ  ( x  +  (
 k  x.  T ) )  e.  ran  Q } )   &    |-  N  =  ( ( # `  H )  -  1 )   &    |-  S  =  ( iota f f 
 Isom  <  ,  <  (
 ( 0 ... N ) ,  H )
 )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  ( ( |_ `  ( ( B  -  x )  /  T ) )  x.  T ) ) )   &    |-  J  =  ( y  e.  ( A (,] B )  |->  if ( y  =  B ,  A ,  y ) )   &    |-  I  =  ( x  e.  RR  |->  sup ( { j  e.  ( 0..^ M )  |  ( Q `  j )  <_  ( J `
  ( E `  x ) ) } ,  RR ,  <  )
 )   =>    |-  ( ph  ->  S. ( ( A  -  X ) [,] ( B  -  X ) ) ( F `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x )
 
Theoremfourierdlem110 38117* The integral of a piecewise continuous periodic function  F is unchanged if the domain is shifted by any value  X. This lemma generalizes fourierdlem92 38099 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  T  =  ( B  -  A )   &    |-  ( ph  ->  X  e.  RR )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  A  /\  ( p `
  m )  =  B )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  F : RR --> CC )   &    |-  (
 ( ph  /\  x  e. 
 RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   =>    |-  ( ph  ->  S. ( ( A  -  X ) [,] ( B  -  X ) ) ( F `  x )  _d x  =  S. ( A [,] B ) ( F `  x )  _d x )
 
Theoremfourierdlem111 38118* The fourier partial sum for  F is the sum of two integrals, with the same integrand involving  F and the Dirichlet Kernel 
D, but on two opposite intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `  t )  x.  ( cos `  ( n  x.  t ) ) )  _d t  /  pi ) )   &    |-  B  =  ( n  e.  NN  |->  ( S. ( -u pi (,) pi ) ( ( F `  t )  x.  ( sin `  ( n  x.  t ) ) )  _d t  /  pi ) )   &    |-  S  =  ( m  e.  NN  |->  ( ( ( A `  0 )  /  2
 )  +  sum_ n  e.  ( 1 ... m ) ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) ) )   &    |-  D  =  ( n  e.  NN  |->  ( y  e. 
 RR  |->  if ( ( y 
 mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  n )  +  1 )  /  ( 2  x.  pi ) ) ,  (
 ( sin `  ( ( n  +  ( 1  /  2 ) )  x.  y ) ) 
 /  ( ( 2  x.  pi )  x.  ( sin `  (
 y  /  2 )
 ) ) ) ) ) )   &    |-  P  =  ( m  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  -u pi  /\  ( p `
  m )  =  pi )  /\  A. i  e.  ( 0..^ m ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  F : RR --> RR )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T )
 )  =  ( F `
  x ) )   &    |-  G  =  ( x  e.  RR  |->  ( ( F `
  ( X  +  x ) )  x.  ( ( D `  n ) `  x ) ) )   &    |-  (
 ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
 ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  R  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  L  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   &    |-  T  =  ( 2  x.  pi )   &    |-  O  =  ( m  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... m ) )  |  ( ( ( p `
  0 )  =  ( -u pi  -  X )  /\  ( p `  m )  =  ( pi  -  X ) ) 
 /\  A. i  e.  (
 0..^ m ) ( p `  i )  <  ( p `  ( i  +  1
 ) ) ) }
 )   &    |-  W  =  ( i  e.  ( 0 ...
 M )  |->  ( ( Q `  i )  -  X ) )   =>    |-  ( ( ph  /\  n  e.  NN )  ->  ( S `  n )  =  ( S. ( -u pi (,) 0 ) ( ( F `  ( X  +  s )
 )  x.  ( ( D `  n ) `
  s ) )  _d s  +  S. ( 0 (,) pi ) ( ( F `
  ( X  +  s ) )  x.  ( ( D `  n ) `  s
 ) )  _d s ) )
 
Theoremfourierdlem112 38119* Here abbreviations (local definitions) are introduced to prove the fourier 38126 theorem.  ( Z `  m ) is the mth partial sum of the fourier series. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  D  =  ( m  e.  NN  |->  ( y  e.  RR  |->  if ( ( y  mod  ( 2  x.  pi ) )  =  0 ,  ( ( ( 2  x.  m )  +  1 )  /  (
 2  x.  pi ) ) ,  ( ( sin `  ( ( m  +  ( 1  /  2 ) )  x.  y ) ) 
 /  ( ( 2  x.  pi )  x.  ( sin `  (
 y  /  2 )
 ) ) ) ) ) )   &    |-  P  =  ( n  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... n ) )  |  ( ( ( p `
  0 )  =  -u pi  /\  ( p `
  n )  =  pi )  /\  A. i  e.  ( 0..^ n ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  N  =  ( ( # `  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  (
 ( -u pi  +  X ) [,] ( pi  +  X ) )  | 
 E. k  e.  ZZ  ( y  +  (
 k  x.  T ) )  e.  ran  Q } ) )  -  1 )   &    |-  V  =  (
 iota f f  Isom  <  ,  <  ( ( 0
 ... N ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X ) )  |  E. k  e. 
 ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q } ) ) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  X  e.  ran  V )   &    |-  T  =  ( 2  x.  pi )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  C  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  U  e.  ( ( F  |`  ( ( Q `
  i ) (,) ( Q `  (
 i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR  _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ph  ->  E  e.  ( ( ( RR  _D  F )  |`  ( -oo (,) X ) ) lim CC  X ) )   &    |-  ( ph  ->  I  e.  ( ( ( RR  _D  F )  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  ( ph  ->  L  e.  ( ( F  |`  ( -oo (,) X ) ) lim CC  X ) )   &    |-  ( ph  ->  R  e.  ( ( F  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `
  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  B  =  ( n  e.  NN  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  Z  =  ( m  e.  NN  |->  ( ( ( A `  0 )  /  2
 )  +  sum_ n  e.  ( 1 ... m ) ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) ) )   &    |-  S  =  ( n  e.  NN  |->  ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) )   &    |-  ( ph  ->  E. w  e.  RR  A. t  e.  RR  ( abs `  ( F `  t ) )  <_  w )   &    |-  ( ph  ->  E. z  e.  RR  A. t  e.  dom  ( RR 
 _D  F ) ( abs `  ( ( RR  _D  F ) `  t ) )  <_  z )   &    |-  ( ph  ->  X  e.  RR )   =>    |-  ( ph  ->  ( 
 seq 1 (  +  ,  S )  ~~>  ( (
 ( L  +  R )  /  2 )  -  ( ( A `  0 )  /  2
 ) )  /\  (
 ( ( A `  0 )  /  2
 )  +  sum_ n  e.  NN  ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) )  =  ( ( L  +  R )  /  2
 ) ) )
 
Theoremfourierdlem113 38120* Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  T  =  ( 2  x.  pi )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  L  e.  (
 ( F  |`  ( -oo (,)
 X ) ) lim CC  X ) )   &    |-  ( ph  ->  R  e.  (
 ( F  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  P  =  ( n  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... n ) )  |  ( ( ( p `
  0 )  =  -u pi  /\  ( p `
  n )  =  pi )  /\  A. i  e.  ( 0..^ n ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  Q  e.  ( P `  M ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR  _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1
 ) ) ) -cn-> CC ) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( RR 
 _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `
  i ) )  =/=  (/) )   &    |-  ( ( ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( ( RR 
 _D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) lim CC  ( Q `
  ( i  +  1 ) ) )  =/=  (/) )   &    |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `
  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  B  =  ( n  e.  NN  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  S  =  ( n  e.  NN  |->  ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `
  n )  x.  ( sin `  ( n  x.  X ) ) ) ) )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  (
 ( |_ `  (
 ( pi  -  x )  /  T ) )  x.  T ) ) )   &    |-  ( ph  ->  ( E `  X )  e.  ran  Q )   =>    |-  ( ph  ->  (  seq 1
 (  +  ,  S ) 
 ~~>  ( ( ( L  +  R )  / 
 2 )  -  (
 ( A `  0
 )  /  2 )
 )  /\  ( (
 ( A `  0
 )  /  2 )  +  sum_ n  e.  NN  ( ( ( A `
  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) )  =  ( ( L  +  R )  /  2
 ) ) )
 
Theoremfourierdlem114 38121* Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  T  =  ( 2  x.  pi )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  G  =  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )   &    |-  ( ph  ->  ( ( -u pi (,) pi )  \  dom  G )  e.  Fin )   &    |-  ( ph  ->  G  e.  ( dom  G -cn-> CC ) )   &    |-  ( ( ph  /\  x  e.  ( (
 -u pi [,) pi )  \  dom  G ) )  ->  ( ( G  |`  ( x (,) +oo ) ) lim CC  x )  =/=  (/) )   &    |-  ( ( ph  /\  x  e.  ( (
 -u pi (,] pi )  \  dom  G ) )  ->  ( ( G  |`  ( -oo (,) x ) ) lim CC  x )  =/=  (/) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  L  e.  ( ( F  |`  ( -oo (,)
 X ) ) lim CC  X ) )   &    |-  ( ph  ->  R  e.  (
 ( F  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  B  =  ( n  e.  NN  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  S  =  ( n  e.  NN  |->  ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `
  n )  x.  ( sin `  ( n  x.  X ) ) ) ) )   &    |-  P  =  ( n  e.  NN  |->  { p  e.  ( RR 
 ^m  ( 0 ... n ) )  |  ( ( ( p `
  0 )  =  -u pi  /\  ( p `
  n )  =  pi )  /\  A. i  e.  ( 0..^ n ) ( p `
  i )  < 
 ( p `  (
 i  +  1 ) ) ) } )   &    |-  E  =  ( x  e.  RR  |->  ( x  +  (
 ( |_ `  (
 ( pi  -  x )  /  T ) )  x.  T ) ) )   &    |-  H  =  ( { -u pi ,  pi ,  ( E `  X ) }  u.  (
 ( -u pi [,] pi )  \  dom  G ) )   &    |-  M  =  ( ( # `  H )  -  1 )   &    |-  Q  =  ( iota g g 
 Isom  <  ,  <  (
 ( 0 ... M ) ,  H )
 )   =>    |-  ( ph  ->  (  seq 1 (  +  ,  S )  ~~>  ( ( ( L  +  R ) 
 /  2 )  -  ( ( A `  0 )  /  2
 ) )  /\  (
 ( ( A `  0 )  /  2
 )  +  sum_ n  e.  NN  ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) )  =  ( ( L  +  R )  /  2
 ) ) )
 
Theoremfourierdlem115 38122* Fourier serier convergence, for piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  T  =  ( 2  x.  pi )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  G  =  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )   &    |-  ( ph  ->  ( ( -u pi (,) pi )  \  dom  G )  e.  Fin )   &    |-  ( ph  ->  G  e.  ( dom  G -cn-> CC ) )   &    |-  ( ( ph  /\  x  e.  ( (
 -u pi [,) pi )  \  dom  G ) )  ->  ( ( G  |`  ( x (,) +oo ) ) lim CC  x )  =/=  (/) )   &    |-  ( ( ph  /\  x  e.  ( (
 -u pi (,] pi )  \  dom  G ) )  ->  ( ( G  |`  ( -oo (,) x ) ) lim CC  x )  =/=  (/) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  L  e.  ( ( F  |`  ( -oo (,)
 X ) ) lim CC  X ) )   &    |-  ( ph  ->  R  e.  (
 ( F  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  B  =  ( n  e.  NN  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  S  =  ( k  e.  NN  |->  ( ( ( A `  k )  x.  ( cos `  ( k  x.  X ) ) )  +  ( ( B `
  k )  x.  ( sin `  (
 k  x.  X ) ) ) ) )   =>    |-  ( ph  ->  (  seq 1 (  +  ,  S ) 
 ~~>  ( ( ( L  +  R )  / 
 2 )  -  (
 ( A `  0
 )  /  2 )
 )  /\  ( (
 ( A `  0
 )  /  2 )  +  sum_ n  e.  NN  ( ( ( A `
  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) )  =  ( ( L  +  R )  /  2
 ) ) )
 
Theoremfourierd 38123* Fourier series convergence for periodic, piecewise smooth functions. The series converges to the average value of the left and the right limit of the function. Thus, if the function is continuous at a given point, the series converges exactly to the function value, see fouriercnp 38127. Notice that for a piecewise smooth function, the left and right limits always exist, see fourier2 38128 for an alternative form of the theorem that makes this fact explicit. When the first derivative is continuous, a simpler version of the theorem can be stated, see fouriercn 38133. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  T  =  ( 2  x.  pi )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  G  =  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )   &    |-  ( ph  ->  ( ( -u pi (,) pi )  \  dom  G )  e.  Fin )   &    |-  ( ph  ->  G  e.  ( dom  G -cn-> CC ) )   &    |-  ( ( ph  /\  x  e.  ( (
 -u pi [,) pi )  \  dom  G ) )  ->  ( ( G  |`  ( x (,) +oo ) ) lim CC  x )  =/=  (/) )   &    |-  ( ( ph  /\  x  e.  ( (
 -u pi (,] pi )  \  dom  G ) )  ->  ( ( G  |`  ( -oo (,) x ) ) lim CC  x )  =/=  (/) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  L  e.  ( ( F  |`  ( -oo (,)
 X ) ) lim CC  X ) )   &    |-  ( ph  ->  R  e.  (
 ( F  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  B  =  ( n  e.  NN  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  /  pi ) )   =>    |-  ( ph  ->  (
 ( ( A `  0 )  /  2
 )  +  sum_ n  e.  NN  ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) )  =  ( ( L  +  R )  /  2
 ) )
 
Theoremfourierclimd 38124* Fourier series convergence, for piecewise smooth functions. See fourierd 38123 for the analogous  sum_ equation. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  T  =  ( 2  x.  pi )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  G  =  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )   &    |-  ( ph  ->  ( ( -u pi (,) pi )  \  dom  G )  e.  Fin )   &    |-  ( ph  ->  G  e.  ( dom  G -cn-> CC ) )   &    |-  ( ( ph  /\  x  e.  ( (
 -u pi [,) pi )  \  dom  G ) )  ->  ( ( G  |`  ( x (,) +oo ) ) lim CC  x )  =/=  (/) )   &    |-  ( ( ph  /\  x  e.  ( (
 -u pi (,] pi )  \  dom  G ) )  ->  ( ( G  |`  ( -oo (,) x ) ) lim CC  x )  =/=  (/) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  ( ph  ->  L  e.  ( ( F  |`  ( -oo (,)
 X ) ) lim CC  X ) )   &    |-  ( ph  ->  R  e.  (
 ( F  |`  ( X (,) +oo ) ) lim CC  X ) )   &    |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  B  =  ( n  e.  NN  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  S  =  ( n  e.  NN  |->  ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `
  n )  x.  ( sin `  ( n  x.  X ) ) ) ) )   =>    |-  ( ph  ->  seq 1 (  +  ,  S )  ~~>  ( ( ( L  +  R ) 
 /  2 )  -  ( ( A `  0 )  /  2
 ) ) )
 
Theoremfourierclim 38125* Fourier series convergence, for piecewise smooth functions. See fourier 38126 for the analogous  sum_ equation. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  F : RR --> RR   &    |-  T  =  ( 2  x.  pi )   &    |-  ( x  e.  RR  ->  ( F `  ( x  +  T )
 )  =  ( F `
  x ) )   &    |-  G  =  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )   &    |-  ( ( -u pi (,) pi )  \  dom  G )  e.  Fin   &    |-  G  e.  ( dom  G -cn-> CC )   &    |-  ( x  e.  (
 ( -u pi [,) pi )  \  dom  G ) 
 ->  ( ( G  |`  ( x (,) +oo ) ) lim CC  x )  =/=  (/) )   &    |-  ( x  e.  ( ( -u pi (,] pi ) 
 \  dom  G )  ->  ( ( G  |`  ( -oo (,) x ) ) lim CC  x )  =/=  (/) )   &    |-  X  e.  RR   &    |-  L  e.  (
 ( F  |`  ( -oo (,)
 X ) ) lim CC  X )   &    |-  R  e.  (
 ( F  |`  ( X (,) +oo ) ) lim CC  X )   &    |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `
  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  B  =  ( n  e.  NN  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  S  =  ( n  e.  NN  |->  ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `
  n )  x.  ( sin `  ( n  x.  X ) ) ) ) )   =>    |-  seq 1 (  +  ,  S )  ~~>  ( ( ( L  +  R )  / 
 2 )  -  (
 ( A `  0
 )  /  2 )
 )
 
Theoremfourier 38126* Fourier series convergence for periodic, piecewise smooth functions. The series converges to the average value of the left and the right limit of the function. Thus, if the function is continuous at a given point, the series converges exactly to the function value, see fouriercnp 38127. Notice that for a piecewise smooth function, the left and right limits always exist, see fourier2 38128 for an alternative form of the theorem that makes this fact explicit. When the first derivative is continuous, a simpler version of the theorem can be stated, see fouriercn 38133. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  F : RR --> RR   &    |-  T  =  ( 2  x.  pi )   &    |-  ( x  e.  RR  ->  ( F `  ( x  +  T )
 )  =  ( F `
  x ) )   &    |-  G  =  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )   &    |-  ( ( -u pi (,) pi )  \  dom  G )  e.  Fin   &    |-  G  e.  ( dom  G -cn-> CC )   &    |-  ( x  e.  (
 ( -u pi [,) pi )  \  dom  G ) 
 ->  ( ( G  |`  ( x (,) +oo ) ) lim CC  x )  =/=  (/) )   &    |-  ( x  e.  ( ( -u pi (,] pi ) 
 \  dom  G )  ->  ( ( G  |`  ( -oo (,) x ) ) lim CC  x )  =/=  (/) )   &    |-  X  e.  RR   &    |-  L  e.  (
 ( F  |`  ( -oo (,)
 X ) ) lim CC  X )   &    |-  R  e.  (
 ( F  |`  ( X (,) +oo ) ) lim CC  X )   &    |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `
  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  B  =  ( n  e.  NN  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  /  pi ) )   =>    |-  ( ( ( A `
  0 )  / 
 2 )  +  sum_ n  e.  NN  ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) )  =  ( ( L  +  R )  /  2
 )
 
Theoremfouriercnp 38127* If  F is continuous at the point  X, then its Fourier series at  X, converges to  ( F `  X ). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  T  =  ( 2  x.  pi )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  G  =  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )   &    |-  ( ph  ->  ( ( -u pi (,) pi )  \  dom  G )  e.  Fin )   &    |-  ( ph  ->  G  e.  ( dom  G -cn-> CC ) )   &    |-  ( ( ph  /\  x  e.  ( (
 -u pi [,) pi )  \  dom  G ) )  ->  ( ( G  |`  ( x (,) +oo ) ) lim CC  x )  =/=  (/) )   &    |-  ( ( ph  /\  x  e.  ( (
 -u pi (,] pi )  \  dom  G ) )  ->  ( ( G  |`  ( -oo (,) x ) ) lim CC  x )  =/=  (/) )   &    |-  J  =  ( topGen `  ran  (,) )   &    |-  ( ph  ->  F  e.  (
 ( J  CnP  J ) `  X ) )   &    |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  B  =  ( n  e.  NN  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  /  pi ) )   =>    |-  ( ph  ->  (
 ( ( A `  0 )  /  2
 )  +  sum_ n  e.  NN  ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) )  =  ( F `  X ) )
 
Theoremfourier2 38128* Fourier series convergence, for a piecewise smooth function. Here it is also proven the existence of the left and right limits of  F at any given point  X. See fourierd 38123 for a comparison. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  T  =  ( 2  x.  pi )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  G  =  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )   &    |-  ( ph  ->  ( ( -u pi (,) pi )  \  dom  G )  e.  Fin )   &    |-  ( ph  ->  G  e.  ( dom  G -cn-> CC ) )   &    |-  ( ( ph  /\  x  e.  ( (
 -u pi [,) pi )  \  dom  G ) )  ->  ( ( G  |`  ( x (,) +oo ) ) lim CC  x )  =/=  (/) )   &    |-  ( ( ph  /\  x  e.  ( (
 -u pi (,] pi )  \  dom  G ) )  ->  ( ( G  |`  ( -oo (,) x ) ) lim CC  x )  =/=  (/) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `
  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  B  =  ( n  e.  NN  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  /  pi ) )   =>    |-  ( ph  ->  E. l  e.  ( ( F  |`  ( -oo (,)
 X ) ) lim CC  X ) E. r  e.  ( ( F  |`  ( X (,) +oo ) ) lim CC  X ) ( ( ( A `  0
 )  /  2 )  +  sum_ n  e.  NN  ( ( ( A `
  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) )  =  ( ( l  +  r )  /  2
 ) )
 
Theoremsqwvfoura 38129* Fourier coefficients for the square wave function. Since the square function is an odd function, there is no contribution from the  A coefficients. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  T  =  ( 2  x.  pi )   &    |-  F  =  ( x  e.  RR  |->  if (
 ( x  mod  T )  <  pi ,  1 ,  -u 1 ) )   &    |-  ( ph  ->  N  e.  NN0 )   =>    |-  ( ph  ->  ( S. ( -u pi (,) pi ) ( ( F `
  x )  x.  ( cos `  ( N  x.  x ) ) )  _d x  /  pi )  =  0
 )
 
Theoremsqwvfourb 38130* Fourier series  B coefficients for the square wave function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  T  =  ( 2  x.  pi )   &    |-  F  =  ( x  e.  RR  |->  if (
 ( x  mod  T )  <  pi ,  1 ,  -u 1 ) )   &    |-  ( ph  ->  N  e.  NN )   =>    |-  ( ph  ->  ( S. ( -u pi (,) pi ) ( ( F `
  x )  x.  ( sin `  ( N  x.  x ) ) )  _d x  /  pi )  =  if ( 2  ||  N ,  0 ,  (
 4  /  ( N  x.  pi ) ) ) )
 
Theoremfourierswlem 38131* The Fourier series for the square wave  F converges to  Y, a simpler expression for this special case. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  T  =  ( 2  x.  pi )   &    |-  F  =  ( x  e.  RR  |->  if (
 ( x  mod  T )  <  pi ,  1 ,  -u 1 ) )   &    |-  X  e.  RR   &    |-  Y  =  if ( ( X  mod  pi )  =  0 ,  0 ,  ( F `
  X ) )   =>    |-  Y  =  ( ( if ( ( X  mod  T )  e.  ( 0 (,] pi ) ,  1 ,  -u 1
 )  +  ( F `
  X ) ) 
 /  2 )
 
Theoremfouriersw 38132* Fourier series convergence, for the square wave function. Where  F is discontinuous, the series converges to  0, the average value of the left and the right limits. Notice that  F is an odd function and its Fourier expansion has only sine terms (coefficients for cosine terms are zero). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  T  =  ( 2  x.  pi )   &    |-  F  =  ( x  e.  RR  |->  if (
 ( x  mod  T )  <  pi ,  1 ,  -u 1 ) )   &    |-  X  e.  RR   &    |-  S  =  ( n  e.  NN  |->  ( ( sin `  (
 ( ( 2  x.  n )  -  1
 )  x.  X ) )  /  ( ( 2  x.  n )  -  1 ) ) )   &    |-  Y  =  if ( ( X  mod  pi )  =  0 ,  0 ,  ( F `
  X ) )   =>    |-  ( ( ( 4 
 /  pi )  x. 
 sum_ k  e.  NN  ( ( sin `  (
 ( ( 2  x.  k )  -  1
 )  x.  X ) )  /  ( ( 2  x.  k )  -  1 ) ) )  =  Y  /\  seq 1 (  +  ,  S )  ~~>  ( ( pi 
 /  4 )  x.  Y ) )
 
Theoremfouriercn 38133* If the derivative of  F is continuous, then the Fourier series for  F converges to  F everywhere and the hypothesis are simpler than those for the more general case of a piecewise smooth function ( see fourierd 38123 for a comparison). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
 |-  ( ph  ->  F : RR --> RR )   &    |-  T  =  ( 2  x.  pi )   &    |-  ( ( ph  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x ) )   &    |-  ( ph  ->  ( RR  _D  F )  e.  ( RR -cn-> CC ) )   &    |-  G  =  ( ( RR  _D  F )  |`  ( -u pi (,) pi ) )   &    |-  ( ph  ->  X  e.  RR )   &    |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `
  x )  x.  ( cos `  ( n  x.  x ) ) )  _d x  /  pi ) )   &    |-  B  =  ( n  e.  NN  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( sin `  ( n  x.  x ) ) )  _d x  /  pi ) )   =>    |-  ( ph  ->  (
 ( ( A `  0 )  /  2
 )  +  sum_ n  e.  NN  ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) )  =  ( F `  X ) )
 
21.30.17  e is transcendental
 
Theoremelaa2lem 38134* Elementhood in the set of nonzero algebraic numbers. ' Only if ' part of elaa2 38136. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by AV, 1-Oct-2020.)
 |-  ( ph  ->  A  e.  AA )   &    |-  ( ph  ->  A  =/=  0 )   &    |-  ( ph  ->  G  e.  (Poly `  ZZ ) )   &    |-  ( ph  ->  G  =/=  0p )   &    |-  ( ph  ->  ( G `  A )  =  0 )   &    |-  M  = inf ( { n  e.  NN0  |  ( (coeff `  G ) `  n )  =/=  0 } ,  RR ,  <  )   &    |-  I  =  ( k  e.  NN0  |->  ( (coeff `  G ) `  (
 k  +  M ) ) )   &    |-  F  =  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... ( (deg `  G )  -  M ) ) ( ( I `  k )  x.  (
 z ^ k ) ) )   =>    |-  ( ph  ->  E. f  e.  (Poly `  ZZ )
 ( ( (coeff `  f ) `  0
 )  =/=  0  /\  ( f `  A )  =  0 )
 )
 
Theoremelaa2lemOLD 38135* Elementhood in the set of nonzero algebraic numbers. ' Only if ' part of elaa2 38136. (Contributed by Glauco Siliprandi, 5-Apr-2020.) Obsolete version of elaa2lem 38134 as of 1-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
 |-  ( ph  ->  A  e.  AA )   &    |-  ( ph  ->  A  =/=  0 )   &    |-  ( ph  ->  G  e.  (Poly `  ZZ ) )   &    |-  ( ph  ->  G  =/=  0p )   &    |-  ( ph  ->  ( G `  A )  =  0 )   &    |-  M  =  sup ( { n  e.  NN0  |  ( (coeff `  G ) `  n )  =/=  0 } ,  RR ,  `'  <  )   &    |-  I  =  ( k  e.  NN0  |->  ( (coeff `  G ) `  (
 k  +  M ) ) )   &    |-  F  =  ( z  e.  CC  |->  sum_ k  e.  ( 0 ... ( (deg `  G )  -  M ) ) ( ( I `  k )  x.  (
 z ^ k ) ) )   =>    |-  ( ph  ->  E. f  e.  (Poly `  ZZ )
 ( ( (coeff `  f ) `  0
 )  =/=  0  /\  ( f `  A )  =  0 )
 )
 
Theoremelaa2 38136* Elementhood in the set of nonzero algebraic numbers: when  A is nonzero, the polynomial  f can be chosen with a nonzero constant term. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Proof shortened by AV, 1-Oct-2020.)
 |-  ( A  e.  ( AA  \  { 0 } )  <->  ( A  e.  CC  /\  E. f  e.  (Poly `  ZZ ) ( ( (coeff `  f ) `  0
 )  =/=  0  /\  ( f `  A )  =  0 )
 ) )
 
Theoremetransclem1 38137*  H is a function. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
 |-  ( ph  ->  X  C_  CC )   &    |-  ( ph  ->  P  e.  NN )   &    |-  H  =  ( j  e.  ( 0
 ... M )  |->  ( x  e.  X  |->  ( ( x  -  j
 ) ^ if (
 j  =  0 ,  ( P  -  1
 ) ,  P ) ) ) )   &    |-  ( ph  ->  J  e.  (
 0 ... M ) )   =>    |-  ( ph  ->  ( H `  J ) : X --> CC )
 
Theoremetransclem2 38138* Derivative of  G. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
 |-  F/_ x F   &    |-  ( ph  ->  F : RR --> CC )   &    |-  (
 ( ph  /\  i  e.  ( 0 ... ( R  +  1 )
 ) )  ->  (
 ( RR  Dn F ) `  i
 ) : RR --> CC )   &    |-  G  =  ( x  e.  RR  |->  sum_
 i  e.  ( 0
 ... R ) ( ( ( RR  Dn F ) `  i
 ) `  x )
 )   =>    |-  ( ph  ->  ( RR  _D  G )  =  ( x  e.  RR  |->  sum_
 i  e.  ( 0
 ... R ) ( ( ( RR  Dn F ) `  (
 i  +  1 ) ) `  x ) ) )
 
Theoremetransclem3 38139 The given  if term is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
 |-  ( ph  ->  P  e.  NN )   &    |-  ( ph  ->  C : ( 0 ...
 M ) --> ( 0
 ... N ) )   &    |-  ( ph  ->  J  e.  ( 0 ... M ) )   &    |-  ( ph  ->  K  e.  ZZ )   =>    |-  ( ph  ->  if ( P  <  ( C `  J ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( C `  J ) ) ) )  x.  (
 ( K  -  J ) ^ ( P  -  ( C `  J ) ) ) ) )  e.  ZZ )
 
Theoremetransclem4 38140*  F expressed as a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
 |-  ( ph  ->  A  C_  CC )   &    |-  ( ph  ->  P  e.  NN )   &    |-  ( ph  ->  M  e.  NN0 )   &    |-  F  =  ( x  e.  A  |->  ( ( x ^ ( P  -  1 ) )  x.  prod_ j  e.  (
 1 ... M ) ( ( x  -  j
 ) ^ P ) ) )   &    |-  H  =  ( j  e.  ( 0
 ... M )  |->  ( x  e.  A  |->  ( ( x  -  j
 ) ^ if (
 j  =  0 ,  ( P  -  1
 ) ,  P ) ) ) )   &    |-  E  =  ( x  e.  A  |->  prod_ j  e.  ( 0
 ... M ) ( ( H `  j
 ) `  x )
 )   =>    |-  ( ph  ->  F  =  E )
 
Theoremetransclem5 38141* A change of bound variable, often used in proofs for etransc 38186. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
 |-  (
 j  e.  ( 0
 ... M )  |->  ( x  e.