Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem112 Structured version   Unicode version

Theorem fourierdlem112 37946
Description: Here abbreviations (local definitions) are introduced to prove the fourier 37953 theorem.  ( Z `  m ) is the mth partial sum of the fourier series. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem112.f  |-  ( ph  ->  F : RR --> RR )
fourierdlem112.d  |-  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 ) ) ) ) ) ) )
fourierdlem112.p  |-  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 ) ) ) } )
fourierdlem112.m  |-  ( ph  ->  M  e.  NN )
fourierdlem112.q  |-  ( ph  ->  Q  e.  ( P `
 M ) )
fourierdlem112.n  |-  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 )
fourierdlem112.v  |-  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 }
) ) )
fourierdlem112.x  |-  ( ph  ->  X  e.  RR )
fourierdlem112.xran  |-  ( ph  ->  X  e.  ran  V
)
fourierdlem112.t  |-  T  =  ( 2  x.  pi )
fourierdlem112.fper  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
fourierdlem112.fcn  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
fourierdlem112.c  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  C  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
fourierdlem112.u  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  U  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
fourierdlem112.fdvcn  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
fourierdlem112.e  |-  ( ph  ->  E  e.  ( ( ( RR  _D  F
)  |`  ( -oo (,) X ) ) lim CC  X ) )
fourierdlem112.i  |-  ( ph  ->  I  e.  ( ( ( RR  _D  F
)  |`  ( X (,) +oo ) ) lim CC  X
) )
fourierdlem112.l  |-  ( ph  ->  L  e.  ( ( F  |`  ( -oo (,) X ) ) lim CC  X ) )
fourierdlem112.r  |-  ( ph  ->  R  e.  ( ( F  |`  ( X (,) +oo ) ) lim CC  X ) )
fourierdlem112.a  |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi ) )
fourierdlem112.b  |-  B  =  ( n  e.  NN  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( sin `  (
n  x.  x ) ) )  _d x  /  pi ) )
fourierdlem112.z  |-  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 ) ) ) ) ) )
fourierdlem112.23  |-  S  =  ( n  e.  NN  |->  ( ( ( A `
 n )  x.  ( cos `  (
n  x.  X ) ) )  +  ( ( B `  n
)  x.  ( sin `  ( n  x.  X
) ) ) ) )
fourierdlem112.fbd  |-  ( ph  ->  E. w  e.  RR  A. t  e.  RR  ( abs `  ( F `  t ) )  <_  w )
fourierdlem112.fdvbd  |-  ( ph  ->  E. z  e.  RR  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )
fourierdlem112.25  |-  ( ph  ->  X  e.  RR )
Assertion
Ref Expression
fourierdlem112  |-  ( 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 ) ) )
Distinct variable groups:    A, k, m, n    B, k, m, n    t, C, m   
x, C, m    D, i, k, m, n, x, y    i, F, t, z    y, F, t, k, m    z, k, m    n, F    w, F, i, t, z    x, F    i, L, t, z, k, m    n, L   
w, L    f, M, i, t, y, m    n, M, x    M, p, i, n, y    i, N, t, w, z    f, N, y, m    n, N, p    x, N, f    Q, f, i, t, y, k, m    Q, n, x    Q, p, k    R, i, t, z, k, m    R, n    w, R    T, f, t, y, i, k, m    T, n, x    T, p    t, U, m    x, U    i, V, t, w, z    f, V, k, m    n, V, p   
x, V    i, X, t, z    f, X, y, k, m    n, X, p    w, X    x, X    m, Z    ph, i, t, w, z    ph, f,
k, m, y    ph, n    w, m    ph, x
Allowed substitution hints:    ph( p)    A( x, y, z, w, t, f, i, p)    B( x, y, z, w, t, f, i, p)    C( y, z, w, f, i, k, n, p)    D( z, w, t, f, p)    P( x, y, z, w, t, f, i, k, m, n, p)    Q( z, w)    R( x, y, f, p)    S( x, y, z, w, t, f, i, k, m, n, p)    T( z, w)    U( y, z, w, f, i, k, n, p)    E( x, y, z, w, t, f, i, k, m, n, p)    F( f, p)    I( x, y, z, w, t, f, i, k, m, n, p)    L( x, y, f, p)    M( z, w, k)    N( k)    V( y)    Z( x, y, z, w, t, f, i, k, n, p)

Proof of Theorem fourierdlem112
Dummy variables  j 
l  a  s  b  e  g  c  u  q  r  v  h  d  o are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem112.23 . . . . 5  |-  S  =  ( n  e.  NN  |->  ( ( ( A `
 n )  x.  ( cos `  (
n  x.  X ) ) )  +  ( ( B `  n
)  x.  ( sin `  ( n  x.  X
) ) ) ) )
2 fveq2 5879 . . . . . . . 8  |-  ( n  =  j  ->  ( A `  n )  =  ( A `  j ) )
3 oveq1 6310 . . . . . . . . 9  |-  ( n  =  j  ->  (
n  x.  X )  =  ( j  x.  X ) )
43fveq2d 5883 . . . . . . . 8  |-  ( n  =  j  ->  ( cos `  ( n  x.  X ) )  =  ( cos `  (
j  x.  X ) ) )
52, 4oveq12d 6321 . . . . . . 7  |-  ( n  =  j  ->  (
( A `  n
)  x.  ( cos `  ( n  x.  X
) ) )  =  ( ( A `  j )  x.  ( cos `  ( j  x.  X ) ) ) )
6 fveq2 5879 . . . . . . . 8  |-  ( n  =  j  ->  ( B `  n )  =  ( B `  j ) )
73fveq2d 5883 . . . . . . . 8  |-  ( n  =  j  ->  ( sin `  ( n  x.  X ) )  =  ( sin `  (
j  x.  X ) ) )
86, 7oveq12d 6321 . . . . . . 7  |-  ( n  =  j  ->  (
( B `  n
)  x.  ( sin `  ( n  x.  X
) ) )  =  ( ( B `  j )  x.  ( sin `  ( j  x.  X ) ) ) )
95, 8oveq12d 6321 . . . . . 6  |-  ( n  =  j  ->  (
( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `
 n )  x.  ( sin `  (
n  x.  X ) ) ) )  =  ( ( ( A `
 j )  x.  ( cos `  (
j  x.  X ) ) )  +  ( ( B `  j
)  x.  ( sin `  ( j  x.  X
) ) ) ) )
109cbvmptv 4514 . . . . 5  |-  ( n  e.  NN  |->  ( ( ( A `  n
)  x.  ( cos `  ( n  x.  X
) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) )  =  ( j  e.  NN  |->  ( ( ( A `  j )  x.  ( cos `  ( j  x.  X ) ) )  +  ( ( B `
 j )  x.  ( sin `  (
j  x.  X ) ) ) ) )
111, 10eqtri 2452 . . . 4  |-  S  =  ( j  e.  NN  |->  ( ( ( A `
 j )  x.  ( cos `  (
j  x.  X ) ) )  +  ( ( B `  j
)  x.  ( sin `  ( j  x.  X
) ) ) ) )
12 seqeq3 12219 . . . 4  |-  ( S  =  ( j  e.  NN  |->  ( ( ( A `  j )  x.  ( cos `  (
j  x.  X ) ) )  +  ( ( B `  j
)  x.  ( sin `  ( j  x.  X
) ) ) ) )  ->  seq 1
(  +  ,  S
)  =  seq 1
(  +  ,  ( j  e.  NN  |->  ( ( ( A `  j )  x.  ( cos `  ( j  x.  X ) ) )  +  ( ( B `
 j )  x.  ( sin `  (
j  x.  X ) ) ) ) ) ) )
1311, 12mp1i 13 . . 3  |-  ( ph  ->  seq 1 (  +  ,  S )  =  seq 1 (  +  ,  ( j  e.  NN  |->  ( ( ( A `  j )  x.  ( cos `  (
j  x.  X ) ) )  +  ( ( B `  j
)  x.  ( sin `  ( j  x.  X
) ) ) ) ) ) )
14 nnuz 11196 . . . . 5  |-  NN  =  ( ZZ>= `  1 )
15 1zzd 10970 . . . . 5  |-  ( ph  ->  1  e.  ZZ )
16 nfv 1752 . . . . . . 7  |-  F/ n ph
17 nfcv 2585 . . . . . . . 8  |-  F/_ n NN
18 nfcv 2585 . . . . . . . . 9  |-  F/_ n
( -u pi (,) 0
)
19 nfcv 2585 . . . . . . . . . 10  |-  F/_ n
( F `  ( X  +  s )
)
20 nfcv 2585 . . . . . . . . . 10  |-  F/_ n  x.
21 nfcv 2585 . . . . . . . . . 10  |-  F/_ n
( ( D `  m ) `  s
)
2219, 20, 21nfov 6329 . . . . . . . . 9  |-  F/_ n
( ( F `  ( X  +  s
) )  x.  (
( D `  m
) `  s )
)
2318, 22nfitg 22724 . . . . . . . 8  |-  F/_ n S. ( -u pi (,) 0 ) ( ( F `  ( X  +  s ) )  x.  ( ( D `
 m ) `  s ) )  _d s
2417, 23nfmpt 4510 . . . . . . 7  |-  F/_ n
( m  e.  NN  |->  S. ( -u pi (,) 0 ) ( ( F `  ( X  +  s ) )  x.  ( ( D `
 m ) `  s ) )  _d s )
25 nfcv 2585 . . . . . . . . 9  |-  F/_ n
( 0 (,) pi )
2625, 22nfitg 22724 . . . . . . . 8  |-  F/_ n S. ( 0 (,) pi ) ( ( F `
 ( X  +  s ) )  x.  ( ( D `  m ) `  s
) )  _d s
2717, 26nfmpt 4510 . . . . . . 7  |-  F/_ n
( m  e.  NN  |->  S. ( 0 (,) pi ) ( ( F `
 ( X  +  s ) )  x.  ( ( D `  m ) `  s
) )  _d s )
28 fourierdlem112.z . . . . . . . 8  |-  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 ) ) ) ) ) )
29 fourierdlem112.a . . . . . . . . . . . . 13  |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi ) )
30 nfmpt1 4511 . . . . . . . . . . . . 13  |-  F/_ n
( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi ) )
3129, 30nfcxfr 2583 . . . . . . . . . . . 12  |-  F/_ n A
32 nfcv 2585 . . . . . . . . . . . 12  |-  F/_ n
0
3331, 32nffv 5886 . . . . . . . . . . 11  |-  F/_ n
( A `  0
)
34 nfcv 2585 . . . . . . . . . . 11  |-  F/_ n  /
35 nfcv 2585 . . . . . . . . . . 11  |-  F/_ n
2
3633, 34, 35nfov 6329 . . . . . . . . . 10  |-  F/_ n
( ( A ` 
0 )  /  2
)
37 nfcv 2585 . . . . . . . . . 10  |-  F/_ n  +
38 nfcv 2585 . . . . . . . . . . 11  |-  F/_ n
( 1 ... m
)
3938nfsum1 13749 . . . . . . . . . 10  |-  F/_ n sum_ n  e.  ( 1 ... m ) ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `
 n )  x.  ( sin `  (
n  x.  X ) ) ) )
4036, 37, 39nfov 6329 . . . . . . . . 9  |-  F/_ n
( ( ( A `
 0 )  / 
2 )  +  sum_ n  e.  ( 1 ... m ) ( ( ( A `  n
)  x.  ( cos `  ( n  x.  X
) ) )  +  ( ( B `  n )  x.  ( sin `  ( n  x.  X ) ) ) ) )
4117, 40nfmpt 4510 . . . . . . . 8  |-  F/_ n
( 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 ) ) ) ) ) )
4228, 41nfcxfr 2583 . . . . . . 7  |-  F/_ n Z
43 fourierdlem112.f . . . . . . . 8  |-  ( ph  ->  F : RR --> RR )
44 fourierdlem112.25 . . . . . . . 8  |-  ( ph  ->  X  e.  RR )
45 eqid 2423 . . . . . . . 8  |-  ( n  e.  NN  |->  { p  e.  ( RR  ^m  (
0 ... n ) )  |  ( ( ( p `  0 )  =  ( -u pi  +  X )  /\  (
p `  n )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ n ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )  =  ( n  e.  NN  |->  { p  e.  ( RR  ^m  (
0 ... n ) )  |  ( ( ( p `  0 )  =  ( -u pi  +  X )  /\  (
p `  n )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ n ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } )
46 picn 23406 . . . . . . . . . . . . 13  |-  pi  e.  CC
47462timesi 10732 . . . . . . . . . . . 12  |-  ( 2  x.  pi )  =  ( pi  +  pi )
48 fourierdlem112.t . . . . . . . . . . . 12  |-  T  =  ( 2  x.  pi )
4946, 46subnegi 9955 . . . . . . . . . . . 12  |-  ( pi 
-  -u pi )  =  ( pi  +  pi )
5047, 48, 493eqtr4i 2462 . . . . . . . . . . 11  |-  T  =  ( pi  -  -u pi )
51 fourierdlem112.p . . . . . . . . . . 11  |-  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 ) ) ) } )
52 fourierdlem112.m . . . . . . . . . . 11  |-  ( ph  ->  M  e.  NN )
53 fourierdlem112.q . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  ( P `
 M ) )
54 pire 23405 . . . . . . . . . . . . . 14  |-  pi  e.  RR
5554a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  pi  e.  RR )
5655renegcld 10048 . . . . . . . . . . . 12  |-  ( ph  -> 
-u pi  e.  RR )
5756, 44readdcld 9672 . . . . . . . . . . 11  |-  ( ph  ->  ( -u pi  +  X )  e.  RR )
5855, 44readdcld 9672 . . . . . . . . . . 11  |-  ( ph  ->  ( pi  +  X
)  e.  RR )
59 negpilt0 37376 . . . . . . . . . . . . . 14  |-  -u pi  <  0
60 pipos 23407 . . . . . . . . . . . . . 14  |-  0  <  pi
6154renegcli 9937 . . . . . . . . . . . . . . 15  |-  -u pi  e.  RR
62 0re 9645 . . . . . . . . . . . . . . 15  |-  0  e.  RR
6361, 62, 54lttri 9762 . . . . . . . . . . . . . 14  |-  ( (
-u pi  <  0  /\  0  <  pi )  ->  -u pi  <  pi )
6459, 60, 63mp2an 677 . . . . . . . . . . . . 13  |-  -u pi  <  pi
6564a1i 11 . . . . . . . . . . . 12  |-  ( ph  -> 
-u pi  <  pi )
6656, 55, 44, 65ltadd1dd 10226 . . . . . . . . . . 11  |-  ( ph  ->  ( -u pi  +  X )  <  (
pi  +  X ) )
67 oveq1 6310 . . . . . . . . . . . . . . 15  |-  ( y  =  x  ->  (
y  +  ( k  x.  T ) )  =  ( x  +  ( k  x.  T
) ) )
6867eleq1d 2492 . . . . . . . . . . . . . 14  |-  ( y  =  x  ->  (
( y  +  ( k  x.  T ) )  e.  ran  Q  <->  ( x  +  ( k  x.  T ) )  e.  ran  Q ) )
6968rexbidv 2940 . . . . . . . . . . . . 13  |-  ( y  =  x  ->  ( E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q  <->  E. k  e.  ZZ  (
x  +  ( k  x.  T ) )  e.  ran  Q ) )
7069cbvrabv 3081 . . . . . . . . . . . 12  |-  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }  =  { x  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q }
7170uneq2i 3618 . . . . . . . . . . 11  |-  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)  =  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { x  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( x  +  ( k  x.  T
) )  e.  ran  Q } )
72 fourierdlem112.n . . . . . . . . . . 11  |-  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 )
73 fourierdlem112.v . . . . . . . . . . 11  |-  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 }
) ) )
7450, 51, 52, 53, 57, 58, 66, 45, 71, 72, 73fourierdlem54 37888 . . . . . . . . . 10  |-  ( ph  ->  ( ( N  e.  NN  /\  V  e.  ( ( n  e.  NN  |->  { p  e.  ( RR  ^m  (
0 ... n ) )  |  ( ( ( p `  0 )  =  ( -u pi  +  X )  /\  (
p `  n )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ n ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } ) `
 N ) )  /\  V  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 } ) ) ) )
7574simpld 461 . . . . . . . . 9  |-  ( ph  ->  ( N  e.  NN  /\  V  e.  ( ( n  e.  NN  |->  { p  e.  ( RR 
^m  ( 0 ... n ) )  |  ( ( ( p `
 0 )  =  ( -u pi  +  X )  /\  (
p `  n )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ n ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } ) `
 N ) ) )
7675simpld 461 . . . . . . . 8  |-  ( ph  ->  N  e.  NN )
7775simprd 465 . . . . . . . 8  |-  ( ph  ->  V  e.  ( ( n  e.  NN  |->  { p  e.  ( RR 
^m  ( 0 ... n ) )  |  ( ( ( p `
 0 )  =  ( -u pi  +  X )  /\  (
p `  n )  =  ( pi  +  X ) )  /\  A. i  e.  ( 0..^ n ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) } ) `
 N ) )
78 fourierdlem112.xran . . . . . . . 8  |-  ( ph  ->  X  e.  ran  V
)
7943adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  F : RR --> RR )
80 fveq2 5879 . . . . . . . . . . . . . . . 16  |-  ( i  =  j  ->  (
p `  i )  =  ( p `  j ) )
81 oveq1 6310 . . . . . . . . . . . . . . . . 17  |-  ( i  =  j  ->  (
i  +  1 )  =  ( j  +  1 ) )
8281fveq2d 5883 . . . . . . . . . . . . . . . 16  |-  ( i  =  j  ->  (
p `  ( i  +  1 ) )  =  ( p `  ( j  +  1 ) ) )
8380, 82breq12d 4434 . . . . . . . . . . . . . . 15  |-  ( i  =  j  ->  (
( p `  i
)  <  ( p `  ( i  +  1 ) )  <->  ( p `  j )  <  (
p `  ( j  +  1 ) ) ) )
8483cbvralv 3056 . . . . . . . . . . . . . 14  |-  ( A. i  e.  ( 0..^ n ) ( p `
 i )  < 
( p `  (
i  +  1 ) )  <->  A. j  e.  ( 0..^ n ) ( p `  j )  <  ( p `  ( j  +  1 ) ) )
8584anbi2i 699 . . . . . . . . . . . . 13  |-  ( ( ( ( p ` 
0 )  =  -u pi  /\  ( p `  n )  =  pi )  /\  A. i  e.  ( 0..^ n ) ( p `  i
)  <  ( p `  ( i  +  1 ) ) )  <->  ( (
( p `  0
)  =  -u pi  /\  ( p `  n
)  =  pi )  /\  A. j  e.  ( 0..^ n ) ( p `  j
)  <  ( p `  ( j  +  1 ) ) ) )
8685a1i 11 . . . . . . . . . . . 12  |-  ( p  e.  ( RR  ^m  ( 0 ... n
) )  ->  (
( ( ( p `
 0 )  = 
-u pi  /\  (
p `  n )  =  pi )  /\  A. i  e.  ( 0..^ n ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) )  <->  ( (
( p `  0
)  =  -u pi  /\  ( p `  n
)  =  pi )  /\  A. j  e.  ( 0..^ n ) ( p `  j
)  <  ( p `  ( j  +  1 ) ) ) ) )
8786rabbiia 3070 . . . . . . . . . . 11  |-  { p  e.  ( RR  ^m  (
0 ... n ) )  |  ( ( ( p `  0 )  =  -u pi  /\  (
p `  n )  =  pi )  /\  A. i  e.  ( 0..^ n ) ( p `
 i )  < 
( p `  (
i  +  1 ) ) ) }  =  { p  e.  ( RR  ^m  ( 0 ... n ) )  |  ( ( ( p `
 0 )  = 
-u pi  /\  (
p `  n )  =  pi )  /\  A. j  e.  ( 0..^ n ) ( p `
 j )  < 
( p `  (
j  +  1 ) ) ) }
8887mpteq2i 4505 . . . . . . . . . 10  |-  ( 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 ) ) ) } )  =  ( n  e.  NN  |->  { p  e.  ( RR  ^m  (
0 ... n ) )  |  ( ( ( p `  0 )  =  -u pi  /\  (
p `  n )  =  pi )  /\  A. j  e.  ( 0..^ n ) ( p `
 j )  < 
( p `  (
j  +  1 ) ) ) } )
8951, 88eqtri 2452 . . . . . . . . 9  |-  P  =  ( n  e.  NN  |->  { p  e.  ( RR  ^m  ( 0 ... n ) )  |  ( ( ( p `
 0 )  = 
-u pi  /\  (
p `  n )  =  pi )  /\  A. j  e.  ( 0..^ n ) ( p `
 j )  < 
( p `  (
j  +  1 ) ) ) } )
9052adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  M  e.  NN )
9153adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  Q  e.  ( P `  M ) )
92 fourierdlem112.fper . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
9392adantlr 720 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) )
94 eleq1 2495 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  (
i  e.  ( 0..^ M )  <->  j  e.  ( 0..^ M ) ) )
9594anbi2d 709 . . . . . . . . . . . 12  |-  ( i  =  j  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  <->  ( ph  /\  j  e.  ( 0..^ M ) ) ) )
96 fveq2 5879 . . . . . . . . . . . . . . 15  |-  ( i  =  j  ->  ( Q `  i )  =  ( Q `  j ) )
9781fveq2d 5883 . . . . . . . . . . . . . . 15  |-  ( i  =  j  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( j  +  1 ) ) )
9896, 97oveq12d 6321 . . . . . . . . . . . . . 14  |-  ( i  =  j  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  =  ( ( Q `
 j ) (,) ( Q `  (
j  +  1 ) ) ) )
9998reseq2d 5122 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) )
10098oveq1d 6318 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  (
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC )  =  ( ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) -cn-> CC ) )
10199, 100eleq12d 2505 . . . . . . . . . . . 12  |-  ( i  =  j  ->  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC )  <->  ( F  |`  ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) )  e.  ( ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) -cn-> CC ) ) )
10295, 101imbi12d 322 . . . . . . . . . . 11  |-  ( i  =  j  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  -> 
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC ) )  <->  ( ( ph  /\  j  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) )  e.  ( ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) -cn-> CC ) ) ) )
103 fourierdlem112.fcn . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
104102, 103chvarv 2069 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) )  e.  ( ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) -cn-> CC ) )
105104adantlr 720 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  j  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) )  e.  ( ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) -cn-> CC ) )
10657adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( -u pi  +  X )  e.  RR )
10757rexrd 9692 . . . . . . . . . . 11  |-  ( ph  ->  ( -u pi  +  X )  e.  RR* )
108 pnfxr 11414 . . . . . . . . . . . 12  |- +oo  e.  RR*
109108a1i 11 . . . . . . . . . . 11  |-  ( ph  -> +oo  e.  RR* )
11058ltpnfd 11425 . . . . . . . . . . 11  |-  ( ph  ->  ( pi  +  X
)  < +oo )
111107, 109, 58, 66, 110eliood 37470 . . . . . . . . . 10  |-  ( ph  ->  ( pi  +  X
)  e.  ( (
-u pi  +  X
) (,) +oo )
)
112111adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( pi  +  X )  e.  ( ( -u pi  +  X ) (,) +oo ) )
113 id 23 . . . . . . . . . . 11  |-  ( i  e.  ( 0..^ N )  ->  i  e.  ( 0..^ N ) )
11472oveq2i 6314 . . . . . . . . . . 11  |-  ( 0..^ N )  =  ( 0..^ ( ( # `  ( { ( -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 ) )
115113, 114syl6eleq 2521 . . . . . . . . . 10  |-  ( i  e.  ( 0..^ N )  ->  i  e.  ( 0..^ ( ( # `  ( { ( -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 ) ) )
116115adantl 468 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  i  e.  ( 0..^ ( ( # `  ( { ( -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 ) ) )
11772oveq2i 6314 . . . . . . . . . . . 12  |-  ( 0 ... N )  =  ( 0 ... (
( # `  ( { ( -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 ) )
118 isoeq4 6226 . . . . . . . . . . . 12  |-  ( ( 0 ... N )  =  ( 0 ... ( ( # `  ( { ( -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 ) )  ->  (
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 }
) )  <->  f  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -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 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) ) ) )
119117, 118ax-mp 5 . . . . . . . . . . 11  |-  ( 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 }
) )  <->  f  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -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 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) ) )
120119iotabii 5585 . . . . . . . . . 10  |-  ( 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 } ) ) )  =  ( iota f
f  Isom  <  ,  <  ( ( 0 ... (
( # `  ( { ( -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 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
) ) )
12173, 120eqtri 2452 . . . . . . . . 9  |-  V  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... (
( # `  ( { ( -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 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
) ) )
12279, 89, 50, 90, 91, 93, 105, 106, 112, 116, 121fourierdlem98 37932 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> CC ) )
123 fourierdlem112.fbd . . . . . . . . . 10  |-  ( ph  ->  E. w  e.  RR  A. t  e.  RR  ( abs `  ( F `  t ) )  <_  w )
124123adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  E. w  e.  RR  A. t  e.  RR  ( abs `  ( F `  t ) )  <_  w )
125 nfra1 2807 . . . . . . . . . . 11  |-  F/ t A. t  e.  RR  ( abs `  ( F `
 t ) )  <_  w
126 elioore 11668 . . . . . . . . . . . . 13  |-  ( t  e.  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  ->  t  e.  RR )
127 rspa 2793 . . . . . . . . . . . . 13  |-  ( ( A. t  e.  RR  ( abs `  ( F `
 t ) )  <_  w  /\  t  e.  RR )  ->  ( abs `  ( F `  t ) )  <_  w )
128126, 127sylan2 477 . . . . . . . . . . . 12  |-  ( ( A. t  e.  RR  ( abs `  ( F `
 t ) )  <_  w  /\  t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  ->  ( abs `  ( F `  t ) )  <_  w )
129128ex 436 . . . . . . . . . . 11  |-  ( A. t  e.  RR  ( abs `  ( F `  t ) )  <_  w  ->  ( t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) )  ->  ( abs `  ( F `  t
) )  <_  w
) )
130125, 129ralrimi 2826 . . . . . . . . . 10  |-  ( A. t  e.  RR  ( abs `  ( F `  t ) )  <_  w  ->  A. t  e.  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ( abs `  ( F `  t )
)  <_  w )
131130reximi 2894 . . . . . . . . 9  |-  ( E. w  e.  RR  A. t  e.  RR  ( abs `  ( F `  t ) )  <_  w  ->  E. w  e.  RR  A. t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ( abs `  ( F `
 t ) )  <_  w )
132124, 131syl 17 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  E. w  e.  RR  A. t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ( abs `  ( F `
 t ) )  <_  w )
133 ssid 3484 . . . . . . . . . . . 12  |-  RR  C_  RR
134 dvfre 22897 . . . . . . . . . . . 12  |-  ( ( F : RR --> RR  /\  RR  C_  RR )  -> 
( RR  _D  F
) : dom  ( RR  _D  F ) --> RR )
13543, 133, 134sylancl 667 . . . . . . . . . . 11  |-  ( ph  ->  ( RR  _D  F
) : dom  ( RR  _D  F ) --> RR )
136135adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( RR  _D  F ) : dom  ( RR  _D  F
) --> RR )
137 eqid 2423 . . . . . . . . . . . . 13  |-  ( RR 
_D  F )  =  ( RR  _D  F
)
13854a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  pi  e.  RR )
13961a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  -u pi  e.  RR )
14098reseq2d 5122 . . . . . . . . . . . . . . . . 17  |-  ( i  =  j  ->  (
( RR  _D  F
)  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( ( RR  _D  F )  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) )
141140, 100eleq12d 2505 . . . . . . . . . . . . . . . 16  |-  ( i  =  j  ->  (
( ( RR  _D  F )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC )  <->  ( ( RR  _D  F )  |`  ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) )  e.  ( ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) -cn-> CC ) ) )
14295, 141imbi12d 322 . . . . . . . . . . . . . . 15  |-  ( i  =  j  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  -> 
( ( RR  _D  F )  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )
-cn-> CC ) )  <->  ( ( ph  /\  j  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  F )  |`  ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) )  e.  ( ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) -cn-> CC ) ) ) )
143 fourierdlem112.fdvcn . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
144142, 143chvarv 2069 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  F )  |`  ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) )  e.  ( ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) -cn-> CC ) )
145144adantlr 720 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  j  e.  ( 0..^ M ) )  ->  ( ( RR  _D  F )  |`  ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) )  e.  ( ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) -cn-> CC ) )
146 fourierdlem112.x . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  e.  RR )
14756, 146readdcld 9672 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( -u pi  +  X )  e.  RR )
148147adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( -u pi  +  X )  e.  RR )
149147rexrd 9692 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( -u pi  +  X )  e.  RR* )
15055, 146readdcld 9672 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( pi  +  X
)  e.  RR )
15156, 55, 146, 65ltadd1dd 10226 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( -u pi  +  X )  <  (
pi  +  X ) )
152150ltpnfd 11425 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( pi  +  X
)  < +oo )
153149, 109, 150, 151, 152eliood 37470 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( pi  +  X
)  e.  ( (
-u pi  +  X
) (,) +oo )
)
154153adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( pi  +  X )  e.  ( ( -u pi  +  X ) (,) +oo ) )
155 oveq1 6310 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  h  ->  (
k  x.  T )  =  ( h  x.  T ) )
156155oveq2d 6319 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  h  ->  (
y  +  ( k  x.  T ) )  =  ( y  +  ( h  x.  T
) ) )
157156eleq1d 2492 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  h  ->  (
( y  +  ( k  x.  T ) )  e.  ran  Q  <->  ( y  +  ( h  x.  T ) )  e.  ran  Q ) )
158157cbvrexv 3057 . . . . . . . . . . . . . . . . . . 19  |-  ( E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q  <->  E. h  e.  ZZ  ( y  +  ( h  x.  T
) )  e.  ran  Q )
159158rgenw 2787 . . . . . . . . . . . . . . . . . 18  |-  A. y  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) ) ( E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q  <->  E. h  e.  ZZ  ( y  +  ( h  x.  T ) )  e.  ran  Q
)
160 rabbi 3008 . . . . . . . . . . . . . . . . . 18  |-  ( A. y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X ) ) ( E. k  e.  ZZ  ( y  +  ( k  x.  T ) )  e.  ran  Q  <->  E. h  e.  ZZ  (
y  +  ( h  x.  T ) )  e.  ran  Q )  <->  { y  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q }  =  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. h  e.  ZZ  (
y  +  ( h  x.  T ) )  e.  ran  Q }
)
161159, 160mpbi 212 . . . . . . . . . . . . . . . . 17  |-  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }  =  { y  e.  ( ( -u pi  +  X ) [,] (
pi  +  X ) )  |  E. h  e.  ZZ  ( y  +  ( h  x.  T
) )  e.  ran  Q }
162161uneq2i 3618 . . . . . . . . . . . . . . . 16  |-  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)  =  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. h  e.  ZZ  (
y  +  ( h  x.  T ) )  e.  ran  Q }
)
163 isoeq5 6227 . . . . . . . . . . . . . . . 16  |-  ( ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
)  =  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. h  e.  ZZ  (
y  +  ( h  x.  T ) )  e.  ran  Q }
)  ->  ( f  Isom  <  ,  <  (
( 0 ... (
( # `  ( { ( -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 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
) )  <->  f  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -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 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. h  e.  ZZ  ( y  +  ( h  x.  T
) )  e.  ran  Q } ) ) ) )
164162, 163ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( f 
Isom  <  ,  <  (
( 0 ... (
( # `  ( { ( -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 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q }
) )  <->  f  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -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 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. h  e.  ZZ  ( y  +  ( h  x.  T
) )  e.  ran  Q } ) ) )
165164iotabii 5585 . . . . . . . . . . . . . 14  |-  ( iota f f  Isom  <  ,  <  ( ( 0 ... ( ( # `  ( { ( -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 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X
) }  u.  {
y  e.  ( (
-u pi  +  X
) [,] ( pi  +  X ) )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) ) )  =  ( iota f
f  Isom  <  ,  <  ( ( 0 ... (
( # `  ( { ( -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 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. h  e.  ZZ  (
y  +  ( h  x.  T ) )  e.  ran  Q }
) ) )
166121, 165eqtri 2452 . . . . . . . . . . . . 13  |-  V  =  ( iota f f 
Isom  <  ,  <  (
( 0 ... (
( # `  ( { ( -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 ) ) ,  ( { ( -u pi  +  X ) ,  ( pi  +  X ) }  u.  { y  e.  ( ( -u pi  +  X ) [,] ( pi  +  X
) )  |  E. h  e.  ZZ  (
y  +  ( h  x.  T ) )  e.  ran  Q }
) ) )
167 eleq1 2495 . . . . . . . . . . . . . . 15  |-  ( v  =  u  ->  (
v  e.  dom  ( RR  _D  F )  <->  u  e.  dom  ( RR  _D  F
) ) )
168 fveq2 5879 . . . . . . . . . . . . . . 15  |-  ( v  =  u  ->  (
( RR  _D  F
) `  v )  =  ( ( RR 
_D  F ) `  u ) )
169167, 168ifbieq1d 3933 . . . . . . . . . . . . . 14  |-  ( v  =  u  ->  if ( v  e.  dom  ( RR  _D  F
) ,  ( ( RR  _D  F ) `
 v ) ,  0 )  =  if ( u  e.  dom  ( RR  _D  F
) ,  ( ( RR  _D  F ) `
 u ) ,  0 ) )
170169cbvmptv 4514 . . . . . . . . . . . . 13  |-  ( v  e.  RR  |->  if ( v  e.  dom  ( RR  _D  F ) ,  ( ( RR  _D  F ) `  v
) ,  0 ) )  =  ( u  e.  RR  |->  if ( u  e.  dom  ( RR  _D  F ) ,  ( ( RR  _D  F ) `  u
) ,  0 ) )
17179, 137, 89, 138, 139, 50, 90, 91, 93, 145, 148, 154, 116, 166, 170fourierdlem97 37931 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> CC ) )
172 cncff 21917 . . . . . . . . . . . 12  |-  ( ( ( RR  _D  F
)  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) )  e.  ( ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) -cn-> CC )  ->  ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> CC )
173 fdm 5748 . . . . . . . . . . . 12  |-  ( ( ( RR  _D  F
)  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> CC  ->  dom  ( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) )  =  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
174171, 172, 1733syl 18 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  dom  ( ( RR  _D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  =  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) )
175 ssdmres 5143 . . . . . . . . . . 11  |-  ( ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) 
C_  dom  ( RR  _D  F )  <->  dom  ( ( RR  _D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  =  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) )
176174, 175sylibr 216 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  C_  dom  ( RR  _D  F
) )
177136, 176fssresd 5765 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> RR )
178 ax-resscn 9598 . . . . . . . . . . 11  |-  RR  C_  CC
179178a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  RR  C_  CC )
180 cncffvrn 21922 . . . . . . . . . 10  |-  ( ( RR  C_  CC  /\  (
( RR  _D  F
)  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) )  e.  ( ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) -cn-> CC ) )  ->  ( (
( RR  _D  F
)  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) )  e.  ( ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) -cn-> RR )  <-> 
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> RR ) )
181179, 171, 180syl2anc 666 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( ( ( RR  _D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> RR )  <->  ( ( RR  _D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> RR ) )
182177, 181mpbird 236 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> RR ) )
183 fourierdlem112.fdvbd . . . . . . . . . . 11  |-  ( ph  ->  E. z  e.  RR  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )
184183adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  E. z  e.  RR  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )
185 nfv 1752 . . . . . . . . . . . . . 14  |-  F/ t ( ph  /\  i  e.  ( 0..^ N ) )
186 nfra1 2807 . . . . . . . . . . . . . 14  |-  F/ t A. t  e.  dom  ( RR  _D  F
) ( abs `  (
( RR  _D  F
) `  t )
)  <_  z
187185, 186nfan 1985 . . . . . . . . . . . . 13  |-  F/ t ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )
188 fvres 5893 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  ->  (
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  t )  =  ( ( RR 
_D  F ) `  t ) )
189188adantl 468 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  ->  (
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  t )  =  ( ( RR 
_D  F ) `  t ) )
190189fveq2d 5883 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  ->  ( abs `  ( ( ( RR  _D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) `  t
) )  =  ( abs `  ( ( RR  _D  F ) `
 t ) ) )
191190adantlr 720 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )  /\  t  e.  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) )  -> 
( abs `  (
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  t ) )  =  ( abs `  ( ( RR  _D  F ) `  t
) ) )
192 simplr 761 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )  /\  t  e.  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) )  ->  A. t  e.  dom  ( RR  _D  F
) ( abs `  (
( RR  _D  F
) `  t )
)  <_  z )
193176sselda 3465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  ->  t  e.  dom  ( RR  _D  F ) )
194193adantlr 720 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )  /\  t  e.  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) )  -> 
t  e.  dom  ( RR  _D  F ) )
195 rspa 2793 . . . . . . . . . . . . . . . 16  |-  ( ( A. t  e.  dom  ( RR  _D  F
) ( abs `  (
( RR  _D  F
) `  t )
)  <_  z  /\  t  e.  dom  ( RR 
_D  F ) )  ->  ( abs `  (
( RR  _D  F
) `  t )
)  <_  z )
196192, 194, 195syl2anc 666 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )  /\  t  e.  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) )  -> 
( abs `  (
( RR  _D  F
) `  t )
)  <_  z )
197191, 196eqbrtrd 4442 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )  /\  t  e.  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) )  -> 
( abs `  (
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  t ) )  <_  z )
198197ex 436 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `  t
) )  <_  z
)  ->  ( t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) )  ->  ( abs `  ( ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) `  t
) )  <_  z
) )
199187, 198ralrimi 2826 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `  t
) )  <_  z
)  ->  A. t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ( abs `  (
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  t ) )  <_  z )
200199ex 436 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `  t
) )  <_  z  ->  A. t  e.  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ( abs `  (
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  t ) )  <_  z )
)
201200reximdv 2900 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( E. z  e.  RR  A. t  e. 
dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `  t
) )  <_  z  ->  E. z  e.  RR  A. t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ( abs `  ( ( ( RR  _D  F
)  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) ) `  t ) )  <_ 
z ) )
202184, 201mpd 15 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  E. z  e.  RR  A. t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ( abs `  ( ( ( RR  _D  F
)  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) ) `  t ) )  <_ 
z )
203 nfra1 2807 . . . . . . . . . . . 12  |-  F/ t A. t  e.  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ( abs `  (
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  t ) )  <_  z
204188eqcomd 2431 . . . . . . . . . . . . . . . 16  |-  ( t  e.  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  ->  (
( RR  _D  F
) `  t )  =  ( ( ( RR  _D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) `  t
) )
205204fveq2d 5883 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  ->  ( abs `  ( ( RR 
_D  F ) `  t ) )  =  ( abs `  (
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  t ) ) )
206205adantl 468 . . . . . . . . . . . . . 14  |-  ( ( A. t  e.  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ( abs `  (
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  t ) )  <_  z  /\  t  e.  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) )  -> 
( abs `  (
( RR  _D  F
) `  t )
)  =  ( abs `  ( ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) `  t
) ) )
207 rspa 2793 . . . . . . . . . . . . . 14  |-  ( ( A. t  e.  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ( abs `  (
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  t ) )  <_  z  /\  t  e.  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) )  -> 
( abs `  (
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  t ) )  <_  z )
208206, 207eqbrtrd 4442 . . . . . . . . . . . . 13  |-  ( ( A. t  e.  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ( abs `  (
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  t ) )  <_  z  /\  t  e.  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) )  -> 
( abs `  (
( RR  _D  F
) `  t )
)  <_  z )
209208ex 436 . . . . . . . . . . . 12  |-  ( A. t  e.  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) ( abs `  ( ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) `  t
) )  <_  z  ->  ( t  e.  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) )  ->  ( abs `  (
( RR  _D  F
) `  t )
)  <_  z )
)
210203, 209ralrimi 2826 . . . . . . . . . . 11  |-  ( A. t  e.  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) ( abs `  ( ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) `  t
) )  <_  z  ->  A. t  e.  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ( abs `  (
( RR  _D  F
) `  t )
)  <_  z )
211210a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( A. t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ( abs `  (
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  t ) )  <_  z  ->  A. t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z ) )
212211reximdv 2900 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( E. z  e.  RR  A. t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ( abs `  (
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  t ) )  <_  z  ->  E. z  e.  RR  A. t  e.  ( ( V `  i ) (,) ( V `  (
i  +  1 ) ) ) ( abs `  ( ( RR  _D  F ) `  t
) )  <_  z
) )
213202, 212mpd 15 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  E. z  e.  RR  A. t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )
214 nfv 1752 . . . . . . . . . . . 12  |-  F/ i ( ph  /\  j  e.  ( 0..^ M ) )
215 nfcsb1v 3412 . . . . . . . . . . . . 13  |-  F/_ i [_ j  /  i ]_ C
216215nfel1 2601 . . . . . . . . . . . 12  |-  F/ i
[_ j  /  i ]_ C  e.  (
( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 j ) )
217214, 216nfim 1977 . . . . . . . . . . 11  |-  F/ i ( ( ph  /\  j  e.  ( 0..^ M ) )  ->  [_ j  /  i ]_ C  e.  (
( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 j ) ) )
218 csbeq1a 3405 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  C  =  [_ j  /  i ]_ C )
21999, 96oveq12d 6321 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) )  =  ( ( F  |`  ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) ) lim CC  ( Q `  j )
) )
220218, 219eleq12d 2505 . . . . . . . . . . . 12  |-  ( i  =  j  ->  ( C  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) )  <->  [_ j  /  i ]_ C  e.  (
( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 j ) ) ) )
22195, 220imbi12d 322 . . . . . . . . . . 11  |-  ( i  =  j  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  ->  C  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  i ) ) )  <->  ( ( ph  /\  j  e.  ( 0..^ M ) )  ->  [_ j  /  i ]_ C  e.  (
( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 j ) ) ) ) )
222 fourierdlem112.c . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  C  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
223217, 221, 222chvar 2068 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ M ) )  ->  [_ j  /  i ]_ C  e.  (
( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 j ) ) )
224223adantlr 720 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  j  e.  ( 0..^ M ) )  ->  [_ j  / 
i ]_ C  e.  ( ( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 j ) ) )
22579, 89, 50, 90, 91, 93, 105, 224, 106, 112, 116, 121fourierdlem96 37930 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  if ( ( ( d  e.  (
-u pi (,] pi )  |->  if ( d  =  pi ,  -u pi ,  d )
) `  ( (
c  e.  RR  |->  ( c  +  ( ( |_ `  ( ( pi  -  c )  /  T ) )  x.  T ) ) ) `  ( V `
 i ) ) )  =  ( Q `
 ( ( y  e.  RR  |->  sup ( { f  e.  ( 0..^ M )  |  ( Q `  f
)  <_  ( (
d  e.  ( -u pi (,] pi )  |->  if ( d  =  pi ,  -u pi ,  d ) ) `  (
( c  e.  RR  |->  ( c  +  ( ( |_ `  (
( pi  -  c
)  /  T ) )  x.  T ) ) ) `  y
) ) } ,  RR ,  <  ) ) `
 ( V `  i ) ) ) ,  ( ( j  e.  ( 0..^ M )  |->  [_ j  /  i ]_ C ) `  (
( y  e.  RR  |->  sup ( { f  e.  ( 0..^ M )  |  ( Q `  f )  <_  (
( d  e.  (
-u pi (,] pi )  |->  if ( d  =  pi ,  -u pi ,  d )
) `  ( (
c  e.  RR  |->  ( c  +  ( ( |_ `  ( ( pi  -  c )  /  T ) )  x.  T ) ) ) `  y ) ) } ,  RR ,  <  ) ) `  ( V `  i ) ) ) ,  ( F `  ( ( d  e.  ( -u pi (,] pi )  |->  if ( d  =  pi ,  -u pi ,  d ) ) `  (
( c  e.  RR  |->  ( c  +  ( ( |_ `  (
( pi  -  c
)  /  T ) )  x.  T ) ) ) `  ( V `  i )
) ) ) )  e.  ( ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) lim CC  ( V `  i )
) )
226 nfcsb1v 3412 . . . . . . . . . . . . 13  |-  F/_ i [_ j  /  i ]_ U
227226nfel1 2601 . . . . . . . . . . . 12  |-  F/ i
[_ j  /  i ]_ U  e.  (
( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 ( j  +  1 ) ) )
228214, 227nfim 1977 . . . . . . . . . . 11  |-  F/ i ( ( ph  /\  j  e.  ( 0..^ M ) )  ->  [_ j  /  i ]_ U  e.  (
( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 ( j  +  1 ) ) ) )
229 csbeq1a 3405 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  U  =  [_ j  /  i ]_ U )
23099, 97oveq12d 6321 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) )  =  ( ( F  |`  ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) ) lim CC  ( Q `  ( j  +  1 ) ) ) )
231229, 230eleq12d 2505 . . . . . . . . . . . 12  |-  ( i  =  j  ->  ( U  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) )  <->  [_ j  /  i ]_ U  e.  (
( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 ( j  +  1 ) ) ) ) )
23295, 231imbi12d 322 . . . . . . . . . . 11  |-  ( i  =  j  ->  (
( ( ph  /\  i  e.  ( 0..^ M ) )  ->  U  e.  ( ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) ) lim CC  ( Q `  ( i  +  1 ) ) ) )  <->  ( ( ph  /\  j  e.  ( 0..^ M ) )  ->  [_ j  /  i ]_ U  e.  (
( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 ( j  +  1 ) ) ) ) ) )
233 fourierdlem112.u . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  U  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
234228, 232, 233chvar 2068 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ M ) )  ->  [_ j  /  i ]_ U  e.  (
( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 ( j  +  1 ) ) ) )
235234adantlr 720 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  j  e.  ( 0..^ M ) )  ->  [_ j  / 
i ]_ U  e.  ( ( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 ( j  +  1 ) ) ) )
23679, 89, 50, 90, 91, 93, 105, 235, 148, 154, 116, 121fourierdlem99 37933 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  if ( ( ( e  e.  RR  |->  ( e  +  ( ( |_ `  (
( pi  -  e
)  /  T ) )  x.  T ) ) ) `  ( V `  ( i  +  1 ) ) )  =  ( Q `
 ( ( ( y  e.  RR  |->  sup ( { h  e.  ( 0..^ M )  |  ( Q `  h )  <_  (
( g  e.  (
-u pi (,] pi )  |->  if ( g  =  pi ,  -u pi ,  g )
) `  ( (
e  e.  RR  |->  ( e  +  ( ( |_ `  ( ( pi  -  e )  /  T ) )  x.  T ) ) ) `  y ) ) } ,  RR ,  <  ) ) `  ( V `  i ) )  +  1 ) ) ,  ( ( j  e.  ( 0..^ M )  |->  [_ j  /  i ]_ U
) `  ( (
y  e.  RR  |->  sup ( { h  e.  ( 0..^ M )  |  ( Q `  h )  <_  (
( g  e.  (
-u pi (,] pi )  |->  if ( g  =  pi ,  -u pi ,  g )
) `  ( (
e  e.  RR  |->  ( e  +  ( ( |_ `  ( ( pi  -  e )  /  T ) )  x.  T ) ) ) `  y ) ) } ,  RR ,  <  ) ) `  ( V `  i ) ) ) ,  ( F `  ( ( e  e.  RR  |->  ( e  +  ( ( |_ `  ( ( pi  -  e )  /  T ) )  x.  T ) ) ) `  ( V `
 ( i  +  1 ) ) ) ) )  e.  ( ( F  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) lim CC  ( V `
 ( i  +  1 ) ) ) )
237 eqeq1 2427 . . . . . . . . . 10  |-  ( g  =  s  ->  (
g  =  0  <->  s  =  0 ) )
238 oveq2 6311 . . . . . . . . . . . . 13  |-  ( g  =  s  ->  ( X  +  g )  =  ( X  +  s ) )
239238fveq2d 5883 . . . . . . . . . . . 12  |-  ( g  =  s  ->  ( F `  ( X  +  g ) )  =  ( F `  ( X  +  s
) ) )
240 breq2 4425 . . . . . . . . . . . . 13  |-  ( g  =  s  ->  (
0  <  g  <->  0  <  s ) )
241240ifbid 3932 . . . . . . . . . . . 12  |-  ( g  =  s  ->  if ( 0  <  g ,  R ,  L )  =  if ( 0  <  s ,  R ,  L ) )
242239, 241oveq12d 6321 . . . . . . . . . . 11  |-  ( g  =  s  ->  (
( F `  ( X  +  g )
)  -  if ( 0  <  g ,  R ,  L ) )  =  ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  R ,  L ) ) )
243 id 23 . . . . . . . . . . 11  |-  ( g  =  s  ->  g  =  s )
244242, 243oveq12d 6321 . . . . . . . . . 10  |-  ( g  =  s  ->  (
( ( F `  ( X  +  g
) )  -  if ( 0  <  g ,  R ,  L ) )  /  g )  =  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  R ,  L ) )  / 
s ) )
245237, 244ifbieq2d 3935 . . . . . . . . 9  |-  ( g  =  s  ->  if ( g  =  0 ,  0 ,  ( ( ( F `  ( X  +  g
) )  -  if ( 0  <  g ,  R ,  L ) )  /  g ) )  =  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s )
)  -  if ( 0  <  s ,  R ,  L ) )  /  s ) ) )
246245cbvmptv 4514 . . . . . . . 8  |-  ( g  e.  ( -u pi [,] pi )  |->  if ( g  =  0 ,  0 ,  ( ( ( F `  ( X  +  g )
)  -  if ( 0  <  g ,  R ,  L ) )  /  g ) ) )  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  0 ,  ( ( ( F `  ( X  +  s
) )  -  if ( 0  <  s ,  R ,  L ) )  /  s ) ) )
247 eqeq1 2427 . . . . . . . . . 10  |-  ( o  =  s  ->  (
o  =  0  <->  s  =  0 ) )
248 id 23 . . . . . . . . . . 11  |-  ( o  =  s  ->  o  =  s )
249 oveq1 6310 . . . . . . . . . . . . 13  |-  ( o  =  s  ->  (
o  /  2 )  =  ( s  / 
2 ) )
250249fveq2d 5883 . . . . . . . . . . . 12  |-  ( o  =  s  ->  ( sin `  ( o  / 
2 ) )  =  ( sin `  (
s  /  2 ) ) )
251250oveq2d 6319 . . . . . . . . . . 11  |-  ( o  =  s  ->  (
2  x.  ( sin `  ( o  /  2
) ) )  =  ( 2  x.  ( sin `  ( s  / 
2 ) ) ) )
252248, 251oveq12d 6321 . . . . . . . . . 10  |-  ( o  =  s  ->  (
o  /  ( 2  x.  ( sin `  (
o  /  2 ) ) ) )  =  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )
253247, 252ifbieq2d 3935 . . . . . . . . 9  |-  ( o  =  s  ->  if ( o  =  0 ,  1 ,  ( o  /  ( 2  x.  ( sin `  (
o  /  2 ) ) ) ) )  =  if ( s  =  0 ,  1 ,  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )
254253cbvmptv 4514 . . . . . . . 8  |-  ( o  e.  ( -u pi [,] pi )  |->  if ( o  =  0 ,  1 ,  ( o  /  ( 2  x.  ( sin `  (
o  /  2 ) ) ) ) ) )  =  ( s  e.  ( -u pi [,] pi )  |->  if ( s  =  0 ,  1 ,  ( s  /  ( 2  x.  ( sin `  (
s  /  2 ) ) ) ) ) )
255 fveq2 5879 . . . . . . . . . 10  |-  ( r  =  s  ->  (
( g  e.  (
-u pi [,] pi )  |->  if ( g  =  0 ,  0 ,  ( ( ( F `  ( X  +  g ) )  -  if ( 0  <  g ,  R ,  L ) )  / 
g ) ) ) `
 r )  =  ( ( g  e.  ( -u pi [,] pi )  |->  if ( g  =  0 ,  0 ,  ( ( ( F `  ( X  +  g )
)  -  if ( 0  <  g ,  R ,  L ) )  /  g ) ) ) `  s
) )
256 fveq2 5879 . . . . . . . . . 10  |-  ( r  =  s  ->  (
( o  e.  (
-u pi [,] pi )  |->  if ( o  =  0 ,  1 ,  ( o  / 
( 2  x.  ( sin `  ( o  / 
2 ) ) ) ) ) ) `  r )  =  ( ( o  e.  (
-u pi [,] pi )  |->  if ( o  =  0 ,  1 ,  ( o  / 
( 2  x.  ( sin `  ( o  / 
2 ) ) ) ) ) ) `  s ) )
257255, 256oveq12d 6321 . . . . . . . . 9  |-  ( r  =  s  ->  (
( ( g  e.  ( -u pi [,] pi )  |->  if ( g  =  0 ,  0 ,  ( ( ( F `  ( X  +  g )
)  -  if ( 0  <  g ,  R ,  L ) )  /  g ) ) ) `  r
)  x.  ( ( o  e.  ( -u pi [,] pi )  |->  if ( o  =  0 ,  1 ,  ( o  /  ( 2  x.  ( sin `  (
o  /  2 ) ) ) ) ) ) `  r ) )  =  ( ( ( g  e.  (
-u pi [,] pi )  |->  if ( g  =  0 ,  0 ,  ( ( ( F `  ( X  +  g ) )  -  if ( 0  <  g ,  R ,  L ) )  / 
g ) ) ) `
 s )  x.  ( ( o  e.  ( -u pi [,] pi )  |->  if ( o  =  0 ,  1 ,  ( o  /  ( 2  x.  ( sin `  (
o  /  2 ) ) ) ) ) ) `  s ) ) )
258257cbvmptv 4514 . . . . . . . 8  |-  ( r  e.  ( -u pi [,] pi )  |->  ( ( ( g  e.  (
-u pi [,] pi )  |->  if ( g  =  0 ,  0 ,  ( ( ( F `  ( X  +  g ) )  -  if ( 0  <  g ,  R ,  L ) )  / 
g ) ) ) `
 r )  x.  ( ( o  e.  ( -u pi [,] pi )  |->  if ( o  =  0 ,  1 ,  ( o  /  ( 2  x.  ( sin `  (
o  /  2 ) ) ) ) ) ) `  r ) ) )  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( ( g  e.  ( -u pi [,] pi )  |->  if ( g  =  0 ,  0 ,  ( ( ( F `  ( X  +  g )
)  -  if ( 0  <  g ,  R ,  L ) )  /  g ) ) ) `  s
)  x.  ( ( o  e.  ( -u pi [,] pi )  |->  if ( o  =  0 ,  1 ,  ( o  /  ( 2  x.  ( sin `  (
o  /  2 ) ) ) ) ) ) `  s ) ) )
259 oveq2 6311 . . . . . . . . . 10  |-  ( d  =  s  ->  (
( k  +  ( 1  /  2 ) )  x.  d )  =  ( ( k  +  ( 1  / 
2 ) )  x.  s ) )
260259fveq2d 5883 . . . . . . . . 9  |-  ( d  =  s  ->  ( sin `  ( ( k  +  ( 1  / 
2 ) )  x.  d ) )  =  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )
261260cbvmptv 4514 . . . . . . . 8  |-  ( d  e.  ( -u pi [,] pi )  |->  ( sin `  ( ( k  +  ( 1  /  2
) )  x.  d
) ) )  =  ( s  e.  (
-u pi [,] pi )  |->  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  s ) ) )
262 fveq2 5879 . . . . . . . . . 10  |-  ( z  =  s  ->  (
( r  e.  (
-u pi [,] pi )  |->  ( ( ( g  e.  ( -u pi [,] pi )  |->  if ( g  =  0 ,  0 ,  ( ( ( F `  ( X  +  g
) )  -  if ( 0  <  g ,  R ,  L ) )  /  g ) ) ) `  r
)  x.  ( ( o  e.  ( -u pi [,] pi )  |->  if ( o  =  0 ,  1 ,  ( o  /  ( 2  x.  ( sin `  (
o  /  2 ) ) ) ) ) ) `  r ) ) ) `  z
)  =  ( ( r  e.  ( -u pi [,] pi )  |->  ( ( ( g  e.  ( -u pi [,] pi )  |->  if ( g  =  0 ,  0 ,  ( ( ( F `  ( X  +  g )
)  -  if ( 0  <  g ,  R ,  L ) )  /  g ) ) ) `  r
)  x.  ( ( o  e.  ( -u pi [,] pi )  |->  if ( o  =  0 ,  1 ,  ( o  /  ( 2  x.  ( sin `  (
o  /  2 ) ) ) ) ) ) `  r ) ) ) `  s
) )
263 fveq2 5879 . . . . . . . . . 10  |-  ( z  =  s  ->  (
( d  e.  (
-u pi [,] pi )  |->  ( sin `  (
( k  +  ( 1  /  2 ) )  x.  d ) ) ) `  z
)  =  ( ( d  e.  ( -u pi [,] pi )  |->  ( sin `  ( ( k  +  ( 1  /  2 ) )  x.  d ) ) ) `  s ) )
264262, 263oveq12d 6321 . . . . . . . . 9  |-  ( z  =  s  ->  (
( ( r  e.  ( -u pi [,] pi )  |->  ( ( ( g  e.  (
-u pi [,] pi )  |->  if ( g  =  0 ,  0 ,  ( ( ( F `  ( X  +  g ) )  -  if ( 0  <  g ,  R ,  L ) )  / 
g ) ) ) `
 r )  x.  ( ( o  e.  ( -u pi [,] pi )  |->  if ( o  =  0 ,  1 ,  ( o  /  ( 2  x.  ( sin `  (
o  /  2 ) ) ) ) ) ) `  r ) ) ) `  z
)  x.  ( ( d  e.  ( -u pi [,] pi )  |->  ( sin `  ( ( k  +  ( 1  /  2 ) )  x.  d ) ) ) `  z ) )  =  ( ( ( r  e.  (
-u pi [,] pi )  |->  ( ( ( g  e.  ( -u pi [,] pi )  |->  if ( g  =  0 ,  0 ,  ( ( ( F `  ( X  +  g
) )  -  if ( 0  <  g ,  R ,  L ) )  /  g ) ) ) `  r
)  x.  ( ( o  e.  ( -u pi [,] pi )  |->  if ( o  =  0 ,  1 ,  ( o  /  ( 2  x.  ( sin `  (
o  /  2 ) ) ) ) ) ) `  r ) ) ) `  s
)  x.  ( ( d  e.  ( -u pi [,] pi )  |->  ( sin `  ( ( k  +  ( 1  /  2 ) )  x.  d ) ) ) `  s ) ) )
265264cbvmptv 4514 . . . . . . . 8  |-  ( z  e.  ( -u pi [,] pi )  |->  ( ( ( r  e.  (
-u pi [,] pi )  |->  ( ( ( g  e.  ( -u pi [,] pi )  |->  if ( g  =  0 ,  0 ,  ( ( ( F `  ( X  +  g
) )  -  if ( 0  <  g ,  R ,  L ) )  /  g ) ) ) `  r
)  x.  ( ( o  e.  ( -u pi [,] pi )  |->  if ( o  =  0 ,  1 ,  ( o  /  ( 2  x.  ( sin `  (
o  /  2 ) ) ) ) ) ) `  r ) ) ) `  z
)  x.  ( ( d  e.  ( -u pi [,] pi )  |->  ( sin `  ( ( k  +  ( 1  /  2 ) )  x.  d ) ) ) `  z ) ) )  =  ( s  e.  ( -u pi [,] pi )  |->  ( ( ( r  e.  ( -u pi [,] pi )  |->  ( ( ( g  e.  (
-u pi [,] pi )  |->  if ( g  =  0 ,  0 ,  ( ( ( F `  ( X  +  g ) )  -  if ( 0  <  g ,  R ,  L ) )  / 
g ) ) ) `
 r )  x.  ( ( o  e.  ( -u pi [,] pi )  |->  if ( o  =  0 ,  1 ,  ( o  /  ( 2  x.  ( sin `  (
o  /  2 ) ) ) ) ) ) `  r ) ) ) `  s
)  x.  ( ( d  e.  ( -u pi [,] pi )  |->  ( sin `  ( ( k  +  ( 1  /  2 ) )  x.  d ) ) ) `  s ) ) )
266 fveq2 5879 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  ( D `  m )  =  ( D `  n ) )
267266fveq1d 5881 . . . . . . . . . . . 12  |-  ( m  =  n  ->  (
( D `  m
) `  s )  =  ( ( D `
 n ) `  s ) )
268267oveq2d