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

Theorem fourierdlem112 31842
Description: Here abbreviations (local definitions) are introduced to prove the fourier 31849 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 . . . . . 6  |-  S  =  ( n  e.  NN  |->  ( ( ( A `
 n )  x.  ( cos `  (
n  x.  X ) ) )  +  ( ( B `  n
)  x.  ( sin `  ( n  x.  X
) ) ) ) )
2 fveq2 5872 . . . . . . . . 9  |-  ( n  =  j  ->  ( A `  n )  =  ( A `  j ) )
3 oveq1 6302 . . . . . . . . . 10  |-  ( n  =  j  ->  (
n  x.  X )  =  ( j  x.  X ) )
43fveq2d 5876 . . . . . . . . 9  |-  ( n  =  j  ->  ( cos `  ( n  x.  X ) )  =  ( cos `  (
j  x.  X ) ) )
52, 4oveq12d 6313 . . . . . . . 8  |-  ( n  =  j  ->  (
( A `  n
)  x.  ( cos `  ( n  x.  X
) ) )  =  ( ( A `  j )  x.  ( cos `  ( j  x.  X ) ) ) )
6 fveq2 5872 . . . . . . . . 9  |-  ( n  =  j  ->  ( B `  n )  =  ( B `  j ) )
73fveq2d 5876 . . . . . . . . 9  |-  ( n  =  j  ->  ( sin `  ( n  x.  X ) )  =  ( sin `  (
j  x.  X ) ) )
86, 7oveq12d 6313 . . . . . . . 8  |-  ( n  =  j  ->  (
( B `  n
)  x.  ( sin `  ( n  x.  X
) ) )  =  ( ( B `  j )  x.  ( sin `  ( j  x.  X ) ) ) )
95, 8oveq12d 6313 . . . . . . 7  |-  ( 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 4544 . . . . . 6  |-  ( 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 2496 . . . . 5  |-  S  =  ( j  e.  NN  |->  ( ( ( A `
 j )  x.  ( cos `  (
j  x.  X ) ) )  +  ( ( B `  j
)  x.  ( sin `  ( j  x.  X
) ) ) ) )
12 seqeq3 12092 . . . . 5  |-  ( 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, 12ax-mp 5 . . . 4  |-  seq 1
(  +  ,  S
)  =  seq 1
(  +  ,  ( j  e.  NN  |->  ( ( ( A `  j )  x.  ( cos `  ( j  x.  X ) ) )  +  ( ( B `
 j )  x.  ( sin `  (
j  x.  X ) ) ) ) ) )
1413a1i 11 . . 3  |-  ( ph  ->  seq 1 (  +  ,  S )  =  seq 1 (  +  ,  ( j  e.  NN  |->  ( ( ( A `  j )  x.  ( cos `  (
j  x.  X ) ) )  +  ( ( B `  j
)  x.  ( sin `  ( j  x.  X
) ) ) ) ) ) )
15 nnuz 11129 . . . . 5  |-  NN  =  ( ZZ>= `  1 )
16 1z 10906 . . . . . 6  |-  1  e.  ZZ
1716a1i 11 . . . . 5  |-  ( ph  ->  1  e.  ZZ )
18 nfv 1683 . . . . . . 7  |-  F/ n ph
19 nfcv 2629 . . . . . . . 8  |-  F/_ n NN
20 nfcv 2629 . . . . . . . . 9  |-  F/_ n
( -u pi (,) 0
)
21 nfcv 2629 . . . . . . . . . 10  |-  F/_ n
( F `  ( X  +  s )
)
22 nfcv 2629 . . . . . . . . . 10  |-  F/_ n  x.
23 nfcv 2629 . . . . . . . . . 10  |-  F/_ n
( ( D `  m ) `  s
)
2421, 22, 23nfov 6318 . . . . . . . . 9  |-  F/_ n
( ( F `  ( X  +  s
) )  x.  (
( D `  m
) `  s )
)
2520, 24nfitg 22049 . . . . . . . 8  |-  F/_ n S. ( -u pi (,) 0 ) ( ( F `  ( X  +  s ) )  x.  ( ( D `
 m ) `  s ) )  _d s
2619, 25nfmpt 4541 . . . . . . 7  |-  F/_ n
( m  e.  NN  |->  S. ( -u pi (,) 0 ) ( ( F `  ( X  +  s ) )  x.  ( ( D `
 m ) `  s ) )  _d s )
27 nfcv 2629 . . . . . . . . 9  |-  F/_ n
( 0 (,) pi )
2827, 24nfitg 22049 . . . . . . . 8  |-  F/_ n S. ( 0 (,) pi ) ( ( F `
 ( X  +  s ) )  x.  ( ( D `  m ) `  s
) )  _d s
2919, 28nfmpt 4541 . . . . . . 7  |-  F/_ n
( m  e.  NN  |->  S. ( 0 (,) pi ) ( ( F `
 ( X  +  s ) )  x.  ( ( D `  m ) `  s
) )  _d s )
30 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 ) ) ) ) ) )
31 fourierdlem112.a . . . . . . . . . . . . 13  |-  A  =  ( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi ) )
32 nfmpt1 4542 . . . . . . . . . . . . 13  |-  F/_ n
( n  e.  NN0  |->  ( S. ( -u pi (,) pi ) ( ( F `  x )  x.  ( cos `  (
n  x.  x ) ) )  _d x  /  pi ) )
3331, 32nfcxfr 2627 . . . . . . . . . . . 12  |-  F/_ n A
34 nfcv 2629 . . . . . . . . . . . 12  |-  F/_ n
0
3533, 34nffv 5879 . . . . . . . . . . 11  |-  F/_ n
( A `  0
)
36 nfcv 2629 . . . . . . . . . . 11  |-  F/_ n  /
37 nfcv 2629 . . . . . . . . . . 11  |-  F/_ n
2
3835, 36, 37nfov 6318 . . . . . . . . . 10  |-  F/_ n
( ( A ` 
0 )  /  2
)
39 nfcv 2629 . . . . . . . . . 10  |-  F/_ n  +
40 nfcv 2629 . . . . . . . . . . 11  |-  F/_ n
( 1 ... m
)
4140nfsum1 13492 . . . . . . . . . 10  |-  F/_ n sum_ n  e.  ( 1 ... m ) ( ( ( A `  n )  x.  ( cos `  ( n  x.  X ) ) )  +  ( ( B `
 n )  x.  ( sin `  (
n  x.  X ) ) ) )
4238, 39, 41nfov 6318 . . . . . . . . 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 ) ) ) ) )
4319, 42nfmpt 4541 . . . . . . . 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 ) ) ) ) ) )
4430, 43nfcxfr 2627 . . . . . . 7  |-  F/_ n Z
45 fourierdlem112.f . . . . . . . 8  |-  ( ph  ->  F : RR --> RR )
46 fourierdlem112.25 . . . . . . . 8  |-  ( ph  ->  X  e.  RR )
47 eqid 2467 . . . . . . . 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 ) ) ) } )
48 ax-resscn 9561 . . . . . . . . . . . . . 14  |-  RR  C_  CC
49 pire 22718 . . . . . . . . . . . . . 14  |-  pi  e.  RR
5048, 49sselii 3506 . . . . . . . . . . . . 13  |-  pi  e.  CC
51 subneg 9880 . . . . . . . . . . . . 13  |-  ( ( pi  e.  CC  /\  pi  e.  CC )  -> 
( pi  -  -u pi )  =  ( pi  +  pi ) )
5250, 50, 51mp2an 672 . . . . . . . . . . . 12  |-  ( pi 
-  -u pi )  =  ( pi  +  pi )
53502timesi 10668 . . . . . . . . . . . . 13  |-  ( 2  x.  pi )  =  ( pi  +  pi )
5453eqcomi 2480 . . . . . . . . . . . 12  |-  ( pi  +  pi )  =  ( 2  x.  pi )
55 fourierdlem112.t . . . . . . . . . . . . 13  |-  T  =  ( 2  x.  pi )
5655eqcomi 2480 . . . . . . . . . . . 12  |-  ( 2  x.  pi )  =  T
5752, 54, 563eqtrri 2501 . . . . . . . . . . 11  |-  T  =  ( pi  -  -u pi )
58 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 ) ) ) } )
59 fourierdlem112.m . . . . . . . . . . 11  |-  ( ph  ->  M  e.  NN )
60 fourierdlem112.q . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  ( P `
 M ) )
6149a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  pi  e.  RR )
6261renegcld 9998 . . . . . . . . . . . 12  |-  ( ph  -> 
-u pi  e.  RR )
6362, 46readdcld 9635 . . . . . . . . . . 11  |-  ( ph  ->  ( -u pi  +  X )  e.  RR )
6461, 46readdcld 9635 . . . . . . . . . . 11  |-  ( ph  ->  ( pi  +  X
)  e.  RR )
65 negpilt0 31362 . . . . . . . . . . . . . 14  |-  -u pi  <  0
66 pipos 22720 . . . . . . . . . . . . . 14  |-  0  <  pi
6749renegcli 9892 . . . . . . . . . . . . . . 15  |-  -u pi  e.  RR
68 0re 9608 . . . . . . . . . . . . . . 15  |-  0  e.  RR
6967, 68, 49lttri 9722 . . . . . . . . . . . . . 14  |-  ( (
-u pi  <  0  /\  0  <  pi )  ->  -u pi  <  pi )
7065, 66, 69mp2an 672 . . . . . . . . . . . . 13  |-  -u pi  <  pi
7170a1i 11 . . . . . . . . . . . 12  |-  ( ph  -> 
-u pi  <  pi )
7262, 61, 46, 71ltadd1dd 10175 . . . . . . . . . . 11  |-  ( ph  ->  ( -u pi  +  X )  <  (
pi  +  X ) )
73 oveq1 6302 . . . . . . . . . . . . . . 15  |-  ( y  =  x  ->  (
y  +  ( k  x.  T ) )  =  ( x  +  ( k  x.  T
) ) )
7473eleq1d 2536 . . . . . . . . . . . . . 14  |-  ( y  =  x  ->  (
( y  +  ( k  x.  T ) )  e.  ran  Q  <->  ( x  +  ( k  x.  T ) )  e.  ran  Q ) )
7574rexbidv 2978 . . . . . . . . . . . . 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 ) )
7675cbvrabv 3117 . . . . . . . . . . . 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 }
7776uneq2i 3660 . . . . . . . . . . 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 } )
78 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 )
79 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 }
) ) )
8057, 58, 59, 60, 63, 64, 72, 47, 77, 78, 79fourierdlem54 31784 . . . . . . . . . 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 } ) ) ) )
8180simpld 459 . . . . . . . . 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 ) ) )
8281simpld 459 . . . . . . . 8  |-  ( ph  ->  N  e.  NN )
8381simprd 463 . . . . . . . 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 ) )
84 fourierdlem112.xran . . . . . . . 8  |-  ( ph  ->  X  e.  ran  V
)
8545adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  F : RR --> RR )
86 fveq2 5872 . . . . . . . . . . . . . . . 16  |-  ( i  =  j  ->  (
p `  i )  =  ( p `  j ) )
87 oveq1 6302 . . . . . . . . . . . . . . . . 17  |-  ( i  =  j  ->  (
i  +  1 )  =  ( j  +  1 ) )
8887fveq2d 5876 . . . . . . . . . . . . . . . 16  |-  ( i  =  j  ->  (
p `  ( i  +  1 ) )  =  ( p `  ( j  +  1 ) ) )
8986, 88breq12d 4466 . . . . . . . . . . . . . . 15  |-  ( i  =  j  ->  (
( p `  i
)  <  ( p `  ( i  +  1 ) )  <->  ( p `  j )  <  (
p `  ( j  +  1 ) ) ) )
9089cbvralv 3093 . . . . . . . . . . . . . 14  |-  ( A. i  e.  ( 0..^ n ) ( p `
 i )  < 
( p `  (
i  +  1 ) )  <->  A. j  e.  ( 0..^ n ) ( p `  j )  <  ( p `  ( j  +  1 ) ) )
9190anbi2i 694 . . . . . . . . . . . . 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 ) ) ) )
9291a1i 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 ) ) ) ) )
9392rabbiia 3107 . . . . . . . . . . 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 ) ) ) }
9493mpteq2i 4536 . . . . . . . . . 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 ) ) ) } )
9558, 94eqtri 2496 . . . . . . . . 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 ) ) ) } )
9659adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  M  e.  NN )
9760adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  Q  e.  ( P `  M ) )
98 fourierdlem112.fper . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
9998adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) )
100 eleq1 2539 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  (
i  e.  ( 0..^ M )  <->  j  e.  ( 0..^ M ) ) )
101100anbi2d 703 . . . . . . . . . . . 12  |-  ( i  =  j  ->  (
( ph  /\  i  e.  ( 0..^ M ) )  <->  ( ph  /\  j  e.  ( 0..^ M ) ) ) )
102 fveq2 5872 . . . . . . . . . . . . . . 15  |-  ( i  =  j  ->  ( Q `  i )  =  ( Q `  j ) )
10387fveq2d 5876 . . . . . . . . . . . . . . 15  |-  ( i  =  j  ->  ( Q `  ( i  +  1 ) )  =  ( Q `  ( j  +  1 ) ) )
104102, 103oveq12d 6313 . . . . . . . . . . . . . 14  |-  ( i  =  j  ->  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) )  =  ( ( Q `
 j ) (,) ( Q `  (
j  +  1 ) ) ) )
105104reseq2d 5279 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  ( F  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) )
106104oveq1d 6310 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  (
( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC )  =  ( ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) -cn-> CC ) )
107105, 106eleq12d 2549 . . . . . . . . . . . 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 ) ) )
108101, 107imbi12d 320 . . . . . . . . . . 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 ) ) ) )
109 fourierdlem112.fcn . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
110108, 109chvarv 1983 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) )  e.  ( ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) -cn-> CC ) )
111110adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  j  e.  ( 0..^ M ) )  ->  ( F  |`  ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) )  e.  ( ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) -cn-> CC ) )
11263adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( -u pi  +  X )  e.  RR )
11363rexrd 9655 . . . . . . . . . . 11  |-  ( ph  ->  ( -u pi  +  X )  e.  RR* )
114 pnfxr 11333 . . . . . . . . . . . 12  |- +oo  e.  RR*
115114a1i 11 . . . . . . . . . . 11  |-  ( ph  -> +oo  e.  RR* )
11664ltpnfd 31380 . . . . . . . . . . 11  |-  ( ph  ->  ( pi  +  X
)  < +oo )
117113, 115, 64, 72, 116eliood 31418 . . . . . . . . . 10  |-  ( ph  ->  ( pi  +  X
)  e.  ( (
-u pi  +  X
) (,) +oo )
)
118117adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( pi  +  X )  e.  ( ( -u pi  +  X ) (,) +oo ) )
119 id 22 . . . . . . . . . . 11  |-  ( i  e.  ( 0..^ N )  ->  i  e.  ( 0..^ N ) )
12078oveq2i 6306 . . . . . . . . . . 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 ) )
121119, 120syl6eleq 2565 . . . . . . . . . 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 ) ) )
122121adantl 466 . . . . . . . . 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 ) ) )
12378oveq2i 6306 . . . . . . . . . . . 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 ) )
124 isoeq4 6217 . . . . . . . . . . . 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 } ) ) ) )
125123, 124ax-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 } ) ) )
126125iotabii 5579 . . . . . . . . . 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 }
) ) )
12779, 126eqtri 2496 . . . . . . . . 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 }
) ) )
12885, 95, 57, 96, 97, 99, 111, 112, 118, 122, 127fourierdlem98 31828 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( F  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> CC ) )
129 fourierdlem112.fbd . . . . . . . . . 10  |-  ( ph  ->  E. w  e.  RR  A. t  e.  RR  ( abs `  ( F `  t ) )  <_  w )
130129adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  E. w  e.  RR  A. t  e.  RR  ( abs `  ( F `  t ) )  <_  w )
131 nfra1 2848 . . . . . . . . . . . 12  |-  F/ t A. t  e.  RR  ( abs `  ( F `
 t ) )  <_  w
132 simpl 457 . . . . . . . . . . . . . 14  |-  ( ( A. t  e.  RR  ( abs `  ( F `
 t ) )  <_  w  /\  t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  ->  A. t  e.  RR  ( abs `  ( F `  t )
)  <_  w )
133 elioore 11571 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  ->  t  e.  RR )
134133adantl 466 . . . . . . . . . . . . . 14  |-  ( ( A. t  e.  RR  ( abs `  ( F `
 t ) )  <_  w  /\  t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  ->  t  e.  RR )
135 rspa 2834 . . . . . . . . . . . . . 14  |-  ( ( A. t  e.  RR  ( abs `  ( F `
 t ) )  <_  w  /\  t  e.  RR )  ->  ( abs `  ( F `  t ) )  <_  w )
136132, 134, 135syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( A. t  e.  RR  ( abs `  ( F `
 t ) )  <_  w  /\  t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  ->  ( abs `  ( F `  t ) )  <_  w )
137136ex 434 . . . . . . . . . . . 12  |-  ( A. t  e.  RR  ( abs `  ( F `  t ) )  <_  w  ->  ( t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) )  ->  ( abs `  ( F `  t
) )  <_  w
) )
138131, 137ralrimi 2867 . . . . . . . . . . 11  |-  ( A. t  e.  RR  ( abs `  ( F `  t ) )  <_  w  ->  A. t  e.  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ( abs `  ( F `  t )
)  <_  w )
139138reximi 2935 . . . . . . . . . 10  |-  ( 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 )
140139a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( 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
) )
141130, 140mpd 15 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  E. w  e.  RR  A. t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ( abs `  ( F `
 t ) )  <_  w )
142 ssid 3528 . . . . . . . . . . . . 13  |-  RR  C_  RR
143142a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  RR  C_  RR )
144 dvfre 22222 . . . . . . . . . . . 12  |-  ( ( F : RR --> RR  /\  RR  C_  RR )  -> 
( RR  _D  F
) : dom  ( RR  _D  F ) --> RR )
14545, 143, 144syl2anc 661 . . . . . . . . . . 11  |-  ( ph  ->  ( RR  _D  F
) : dom  ( RR  _D  F ) --> RR )
146145adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( RR  _D  F ) : dom  ( RR  _D  F
) --> RR )
147 eqid 2467 . . . . . . . . . . . . . 14  |-  ( RR 
_D  F )  =  ( RR  _D  F
)
14849a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  pi  e.  RR )
14967a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  -u pi  e.  RR )
150104reseq2d 5279 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  j  ->  (
( RR  _D  F
)  |`  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) ) )  =  ( ( RR  _D  F )  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) )
151150, 106eleq12d 2549 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) )
152101, 151imbi12d 320 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) ) )
153 fourierdlem112.fdvcn . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  F )  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
154152, 153chvarv 1983 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0..^ M ) )  ->  ( ( RR 
_D  F )  |`  ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) )  e.  ( ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) -cn-> CC ) )
155154adantlr 714 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) )
156 fourierdlem112.x . . . . . . . . . . . . . . . 16  |-  ( ph  ->  X  e.  RR )
15762, 156readdcld 9635 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( -u pi  +  X )  e.  RR )
158157adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( -u pi  +  X )  e.  RR )
159157rexrd 9655 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( -u pi  +  X )  e.  RR* )
16061, 156readdcld 9635 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( pi  +  X
)  e.  RR )
16162, 61, 156, 71ltadd1dd 10175 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( -u pi  +  X )  <  (
pi  +  X ) )
162160ltpnfd 31380 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( pi  +  X
)  < +oo )
163159, 115, 160, 161, 162eliood 31418 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( pi  +  X
)  e.  ( (
-u pi  +  X
) (,) +oo )
)
164163adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( pi  +  X )  e.  ( ( -u pi  +  X ) (,) +oo ) )
165 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  h  ->  (
k  x.  T )  =  ( h  x.  T ) )
166165oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  h  ->  (
y  +  ( k  x.  T ) )  =  ( y  +  ( h  x.  T
) ) )
167166eleq1d 2536 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  h  ->  (
( y  +  ( k  x.  T ) )  e.  ran  Q  <->  ( y  +  ( h  x.  T ) )  e.  ran  Q ) )
168167cbvrexv 3094 . . . . . . . . . . . . . . . . . . . . 21  |-  ( E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q  <->  E. h  e.  ZZ  ( y  +  ( h  x.  T
) )  e.  ran  Q )
169168rgenw 2828 . . . . . . . . . . . . . . . . . . . 20  |-  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
)
170 rabbi 3045 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 }
)
171169, 170mpbi 208 . . . . . . . . . . . . . . . . . . 19  |-  { 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 }
172171uneq2i 3660 . . . . . . . . . . . . . . . . . 18  |-  ( { ( -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 }
)
173 isoeq5 6218 . . . . . . . . . . . . . . . . . 18  |-  ( ( { ( -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 } ) ) ) )
174172, 173ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( 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 } ) ) )
175174ax-gen 1601 . . . . . . . . . . . . . . . 16  |-  A. 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 } ) )  <->  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 } ) ) )
176 iotabi 5566 . . . . . . . . . . . . . . . 16  |-  ( A. 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 } ) )  <->  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 } ) ) )  ->  ( 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 }
) ) ) )
177175, 176ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( 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 }
) ) )
178127, 177eqtri 2496 . . . . . . . . . . . . . 14  |-  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 }
) ) )
179 eleq1 2539 . . . . . . . . . . . . . . . 16  |-  ( v  =  u  ->  (
v  e.  dom  ( RR  _D  F )  <->  u  e.  dom  ( RR  _D  F
) ) )
180 fveq2 5872 . . . . . . . . . . . . . . . 16  |-  ( v  =  u  ->  (
( RR  _D  F
) `  v )  =  ( ( RR 
_D  F ) `  u ) )
181 eqidd 2468 . . . . . . . . . . . . . . . 16  |-  ( v  =  u  ->  0  =  0 )
182179, 180, 181ifeq123d 31337 . . . . . . . . . . . . . . 15  |-  ( 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 ) )
183182cbvmptv 4544 . . . . . . . . . . . . . 14  |-  ( 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 ) )
18485, 147, 95, 148, 149, 57, 96, 97, 99, 155, 158, 164, 122, 178, 183fourierdlem97 31827 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> CC ) )
185 cncff 21265 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
186184, 185syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> CC )
187 fdm 5741 . . . . . . . . . . . 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 ) ) ) )
188186, 187syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  dom  ( ( RR  _D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  =  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) )
189 ssdmres 5301 . . . . . . . . . . 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 ) ) ) )
190188, 189sylibr 212 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  C_  dom  ( RR  _D  F
) )
191 fssres 5757 . . . . . . . . . 10  |-  ( ( ( RR  _D  F
) : dom  ( RR  _D  F ) --> RR 
/\  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  C_  dom  ( RR  _D  F
) )  ->  (
( RR  _D  F
)  |`  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) ) ) : ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) --> RR )
192146, 190, 191syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) : ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) --> RR )
19348a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  RR  C_  CC )
194 cncffvrn 21270 . . . . . . . . . 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 ) )
195193, 184, 194syl2anc 661 . . . . . . . . 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 ) )
196192, 195mpbird 232 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( ( RR 
_D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  e.  ( ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) -cn-> RR ) )
197 fourierdlem112.fdvbd . . . . . . . . . . 11  |-  ( ph  ->  E. z  e.  RR  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )
198197adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  E. z  e.  RR  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )
199 nfv 1683 . . . . . . . . . . . . . 14  |-  F/ t ( ph  /\  i  e.  ( 0..^ N ) )
200 nfra1 2848 . . . . . . . . . . . . . 14  |-  F/ t A. t  e.  dom  ( RR  _D  F
) ( abs `  (
( RR  _D  F
) `  t )
)  <_  z
201199, 200nfan 1875 . . . . . . . . . . . . 13  |-  F/ t ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  A. t  e.  dom  ( RR  _D  F ) ( abs `  ( ( RR  _D  F ) `
 t ) )  <_  z )
202 simpr 461 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  ->  t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )
203 fvres 5886 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  ->  (
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  t )  =  ( ( RR 
_D  F ) `  t ) )
204202, 203syl 16 . . . . . . . . . . . . . . . . 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 ) )
205204fveq2d 5876 . . . . . . . . . . . . . . . 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 ) ) )
206205adantlr 714 . . . . . . . . . . . . . . 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
) ) )
207 simplr 754 . . . . . . . . . . . . . . . 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 )
208190sselda 3509 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  t  e.  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) )  ->  t  e.  dom  ( RR  _D  F ) )
209208adantlr 714 . . . . . . . . . . . . . . . 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 ) )
210 rspa 2834 . . . . . . . . . . . . . . . 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 )
211207, 209, 210syl2anc 661 . . . . . . . . . . . . . . 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 )
212206, 211eqbrtrd 4473 . . . . . . . . . . . . . 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 )
213212ex 434 . . . . . . . . . . . . 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
) )
214201, 213ralrimi 2867 . . . . . . . . . . . 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 )
215214ex 434 . . . . . . . . . . 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 )
)
216215reximdv 2941 . . . . . . . . . 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 ) )
217198, 216mpd 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 )
218 nfra1 2848 . . . . . . . . . . . 12  |-  F/ t A. t  e.  ( ( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ( abs `  (
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  t ) )  <_  z
219203eqcomd 2475 . . . . . . . . . . . . . . . 16  |-  ( t  e.  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  ->  (
( RR  _D  F
) `  t )  =  ( ( ( RR  _D  F )  |`  ( ( V `  i ) (,) ( V `  ( i  +  1 ) ) ) ) `  t
) )
220219fveq2d 5876 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( ( V `
 i ) (,) ( V `  (
i  +  1 ) ) )  ->  ( abs `  ( ( RR 
_D  F ) `  t ) )  =  ( abs `  (
( ( RR  _D  F )  |`  (
( V `  i
) (,) ( V `
 ( i  +  1 ) ) ) ) `  t ) ) )
221220adantl 466 . . . . . . . . . . . . . 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
) ) )
222 rspa 2834 . . . . . . . . . . . . . 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 )
223221, 222eqbrtrd 4473 . . . . . . . . . . . . 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 )
224223ex 434 . . . . . . . . . . . 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 )
)
225218, 224ralrimi 2867 . . . . . . . . . . 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 )
226225a1i 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 ) )
227226reximdv 2941 . . . . . . . . 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
) )
228217, 227mpd 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 )
229 nfv 1683 . . . . . . . . . . . 12  |-  F/ i ( ph  /\  j  e.  ( 0..^ M ) )
230 nfcv 2629 . . . . . . . . . . . . . 14  |-  F/_ i
j
231230nfcsb1 3455 . . . . . . . . . . . . 13  |-  F/_ i [_ j  /  i ]_ C
232 nfcv 2629 . . . . . . . . . . . . 13  |-  F/_ i
( ( F  |`  ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) ) lim CC  ( Q `  j )
)
233231, 232nfel 2642 . . . . . . . . . . . 12  |-  F/ i
[_ j  /  i ]_ C  e.  (
( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 j ) )
234229, 233nfim 1867 . . . . . . . . . . 11  |-  F/ i ( ( ph  /\  j  e.  ( 0..^ M ) )  ->  [_ j  /  i ]_ C  e.  (
( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 j ) ) )
235 csbeq1a 3449 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  C  =  [_ j  /  i ]_ C )
236105, 102oveq12d 6313 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  (
( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) )  =  ( ( F  |`  ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) ) lim CC  ( Q `  j )
) )
237235, 236eleq12d 2549 . . . . . . . . . . . 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 ) ) ) )
238101, 237imbi12d 320 . . . . . . . . . . 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 ) ) ) ) )
239 fourierdlem112.c . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  C  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 i ) ) )
240234, 238, 239chvar 1982 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ M ) )  ->  [_ j  /  i ]_ C  e.  (
( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 j ) ) )
241240adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  j  e.  ( 0..^ M ) )  ->  [_ j  / 
i ]_ C  e.  ( ( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 j ) ) )
24285, 95, 57, 96, 97, 99, 111, 241, 112, 118, 122, 127fourierdlem96 31826 . . . . . . . 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 )
) )
243230nfcsb1 3455 . . . . . . . . . . . . 13  |-  F/_ i [_ j  /  i ]_ U
244 nfcv 2629 . . . . . . . . . . . . 13  |-  F/_ i
( ( F  |`  ( ( Q `  j ) (,) ( Q `  ( j  +  1 ) ) ) ) lim CC  ( Q `  ( j  +  1 ) ) )
245243, 244nfel 2642 . . . . . . . . . . . 12  |-  F/ i
[_ j  /  i ]_ U  e.  (
( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 ( j  +  1 ) ) )
246229, 245nfim 1867 . . . . . . . . . . 11  |-  F/ i ( ( ph  /\  j  e.  ( 0..^ M ) )  ->  [_ j  /  i ]_ U  e.  (
( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 ( j  +  1 ) ) ) )
247 csbeq1a 3449 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  U  =  [_ j  /  i ]_ U )
248105, 103oveq12d 6313 . . . . . . . . . . . . 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 ) ) ) )
249247, 248eleq12d 2549 . . . . . . . . . . . 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 ) ) ) ) )
250101, 249imbi12d 320 . . . . . . . . . . 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 ) ) ) ) ) )
251 fourierdlem112.u . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  U  e.  ( ( F  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) lim CC  ( Q `
 ( i  +  1 ) ) ) )
252246, 250, 251chvar 1982 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0..^ M ) )  ->  [_ j  /  i ]_ U  e.  (
( F  |`  (
( Q `  j
) (,) ( Q `
 ( j  +  1 ) ) ) ) lim CC  ( Q `
 ( j  +  1 ) ) ) )
253252adantlr 714 . . . . . . . . 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 ) ) ) )
25485, 95, 57, 96, 97, 99, 111, 253, 158, 164, 122, 127fourierdlem99 31829 . . . . . . . 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 ) ) ) )
255 eqeq1 2471 . . . . . . . . . 10  |-  ( g  =  s  ->  (
g  =  0  <->  s  =  0 ) )
256 eqidd 2468 . . . . . . . . . 10  |-  ( g  =  s  ->  0  =  0 )
257 oveq2 6303 . . . . . . . . . . . . 13  |-  ( g  =  s  ->  ( X  +  g )  =  ( X  +  s ) )
258257fveq2d 5876 . . . . . . . . . . . 12  |-  ( g  =  s  ->  ( F `  ( X  +  g ) )  =  ( F `  ( X  +  s
) ) )
259 breq2 4457 . . . . . . . . . . . . 13  |-  ( g  =  s  ->  (
0  <  g  <->  0  <  s ) )
260 eqidd 2468 . . . . . . . . . . . . 13  |-  ( g  =  s  ->  R  =  R )
261 eqidd 2468 . . . . . . . . . . . . 13  |-  ( g  =  s  ->  L  =  L )
262259, 260, 261ifeq123d 31337 . . . . . . . . . . . 12  |-  ( g  =  s  ->  if ( 0  <  g ,  R ,  L )  =  if ( 0  <  s ,  R ,  L ) )
263258, 262oveq12d 6313 . . . . . . . . . . 11  |-  ( g  =  s  ->  (
( F `  ( X  +  g )
)  -  if ( 0  <  g ,  R ,  L ) )  =  ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  R ,  L ) ) )
264 id 22 . . . . . . . . . . 11  |-  ( g  =  s  ->  g  =  s )
265263, 264oveq12d 6313 . . . . . . . . . 10  |-  ( g  =  s  ->  (
( ( F `  ( X  +  g
) )  -  if ( 0  <  g ,  R ,  L ) )  /  g )  =  ( ( ( F `  ( X  +  s ) )  -  if ( 0  <  s ,  R ,  L ) )  / 
s ) )
266255, 256, 265ifeq123d 31337 . . . . . . . . 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 ) ) )
267266cbvmptv 4544 . . . . . . . 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 ) ) )
268 eqeq1 2471 . . . . . . . . . 10  |-  ( o  =  s  ->  (
o  =  0  <->  s  =  0 ) )
269 eqidd 2468 . . . . . . . . . 10  |-  ( o  =  s  ->  1  =  1 )
270 id 22 . . . . . . . . . . 11  |-  ( o  =  s  ->  o  =  s )
271 oveq1 6302 . . . . . . . . . . . . 13  |-  ( o  =  s  ->  (
o  /  2 )  =  ( s  / 
2 ) )
272271fveq2d 5876 . . . . . . . . . . . 12  |-  ( o  =  s  ->  ( sin `  ( o  / 
2 ) )  =  ( sin `  (
s  /  2 ) ) )
273272oveq2d 6311 . . . . . . . . . . 11  |-  ( o  =  s  ->  (
2  x.  ( sin `  ( o  /  2
) ) )  =  ( 2  x.  ( sin `  ( s  / 
2 ) ) ) )
274270, 273oveq12d 6313 . . . . . . . . . 10  |-  ( o  =  s  ->  (
o  /  ( 2  x.  ( sin `  (
o  /  2 ) ) ) )  =  ( s  /  (
2  x.  ( sin `  ( s  /  2
) ) ) ) )
275268, 269, 274ifeq123d 31337 . . . . . . . . 9  |-  ( o  =  s  ->  if ( o  =  0 ,  1 ,  ( o  /  ( 2  x.  ( sin `  (
o  /  2 ) ) ) ) )  =  if ( s  =  0 ,  1 ,  ( s  / 
( 2  x.  ( sin `  ( s  / 
2 ) ) ) ) ) )
276275cbvmptv 4544 . . . . . . . 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 ) ) ) ) ) )
277 fveq2 5872 . . . . . . . . . 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
) )
278 fveq2 5872 . . . . . . . . . 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 ) )
279277, 278oveq12d 6313 . . . . . . . . 9  |-  ( r  =  s  ->  (
( ( g  e.  ( -u pi [,] pi )  |->  if ( g  =  0 ,  0 ,  ( ( ( F `  ( X