Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem112 Structured version   Unicode version
Theorem fourierdlem112 37369
Description: Here abbreviations (local definitions) are introduced to prove the fourier 37376 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 5849 . . . . . . . 8 |- ( n = j -> ( A ` n ) = ( A ` j ) )
3 oveq1 6285 . . . . . . . . 9 |- ( n = j -> ( n x. X ) = ( j x. X ) )
43fveq2d 5853 . . . . . . . 8 |- ( n = j -> ( cos ` ( n x. X ) ) = ( cos ` ( j x. X ) ) )
52, 4oveq12d 6296 . . . . . . 7 |- ( n = j -> ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) = ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) )
6 fveq2 5849 . . . . . . . 8 |- ( n = j -> ( B ` n ) = ( B ` j ) )
73fveq2d 5853 . . . . . . . 8 |- ( n = j -> ( sin ` ( n x. X ) ) = ( sin ` ( j x. X ) ) )
86, 7oveq12d 6296 . . . . . . 7 |- ( n = j -> ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) = ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) )
95, 8oveq12d 6296 . . . . . 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 4487 . . . . 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 2431 . . . 4 |- S = ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) )
12 seqeq3 12156 . . . 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 11162 . . . . 5 |- NN = ( ZZ>= ` 1 )
15 1zzd 10936 . . . . 5 |- ( ph -> 1 e. ZZ )
16 nfv 1728 . . . . . . 7 |- F/ n ph
17 nfcv 2564 . . . . . . . 8 |- F/_ n NN
18 nfcv 2564 . . . . . . . . 9 |- F/_ n ( -u pi (,) 0 )
19 nfcv 2564 . . . . . . . . . 10 |- F/_ n ( F ` ( X + s ) )
20 nfcv 2564 . . . . . . . . . 10 |- F/_ n x.
21 nfcv 2564 . . . . . . . . . 10 |- F/_ n ( ( D ` m ) ` s )
2219, 20, 21nfov 6304 . . . . . . . . 9 |- F/_ n ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) )
2318, 22nfitg 22473 . . . . . . . 8 |- F/_ n S. ( -u pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s
2417, 23nfmpt 4483 . . . . . . 7 |- F/_ n ( m e. NN |-> S. ( -u pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s )
25 nfcv 2564 . . . . . . . . 9 |- F/_ n ( 0 (,) pi )
2625, 22nfitg 22473 . . . . . . . 8 |- F/_ n S. ( 0 (,) pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s
2717, 26nfmpt 4483 . . . . . . 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 4484 . . . . . . . . . . . . 13 |- F/_ n ( n e. NN0 |-> ( S. ( -u pi (,) pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / pi ) )
3129, 30nfcxfr 2562 . . . . . . . . . . . 12 |- F/_ n A
32 nfcv 2564 . . . . . . . . . . . 12 |- F/_ n 0
3331, 32nffv 5856 . . . . . . . . . . 11 |- F/_ n ( A ` 0 )
34 nfcv 2564 . . . . . . . . . . 11 |- F/_ n /
35 nfcv 2564 . . . . . . . . . . 11 |- F/_ n 2
3633, 34, 35nfov 6304 . . . . . . . . . 10 |- F/_ n ( ( A ` 0 ) / 2 )
37 nfcv 2564 . . . . . . . . . 10 |- F/_ n +
38 nfcv 2564 . . . . . . . . . . 11 |- F/_ n ( 1 ... m )
3938nfsum1 13661 . . . . . . . . . 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 6304 . . . . . . . . 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 4483 . . . . . . . 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 2562 . . . . . . 7 |- F/_ n Z
43 fourierdlem112.f . . . . . . . 8 |- ( ph -> F : RR --> RR )
44 fourierdlem112.25 . . . . . . . 8 |- ( ph -> X e. RR )
45 eqid 2402 . . . . . . . 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 23144 . . . . . . . . . . . . 13 |- pi e. CC
47462timesi 10697 . . . . . . . . . . . 12 |- ( 2 x. pi ) = ( pi + pi )
48 fourierdlem112.t . . . . . . . . . . . 12 |- T = ( 2 x. pi )
4946, 46subnegi 9934 . . . . . . . . . . . 12 |- ( pi - -u pi ) = ( pi + pi )
5047, 48, 493eqtr4i 2441 . . . . . . . . . . 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 23143 . . . . . . . . . . . . . 14 |- pi e. RR
5554a1i 11 . . . . . . . . . . . . 13 |- ( ph -> pi e. RR )
5655renegcld 10027 . . . . . . . . . . . 12 |- ( ph -> -u pi e. RR )
5756, 44readdcld 9653 . . . . . . . . . . 11 |- ( ph -> ( -u pi + X ) e. RR )
5855, 44readdcld 9653 . . . . . . . . . . 11 |- ( ph -> ( pi + X ) e. RR )
59 negpilt0 36836 . . . . . . . . . . . . . 14 |- -u pi < 0
60 pipos 23145 . . . . . . . . . . . . . 14 |- 0 < pi
6154renegcli 9916 . . . . . . . . . . . . . . 15 |- -u pi e. RR
62 0re 9626 . . . . . . . . . . . . . . 15 |- 0 e. RR
6361, 62, 54lttri 9742 . . . . . . . . . . . . . 14 |- ( ( -u pi < 0 /\ 0 < pi ) -> -u pi < pi )
6459, 60, 63mp2an 670 . . . . . . . . . . . . 13 |- -u pi < pi
6564a1i 11 . . . . . . . . . . . 12 |- ( ph -> -u pi < pi )
6656, 55, 44, 65ltadd1dd 10203 . . . . . . . . . . 11 |- ( ph -> ( -u pi + X ) < ( pi + X ) )
67 oveq1 6285 . . . . . . . . . . . . . . 15 |- ( y = x -> ( y + ( k x. T ) ) = ( x + ( k x. T ) ) )
6867eleq1d 2471 . . . . . . . . . . . . . 14 |- ( y = x -> ( ( y + ( k x. T ) ) e. ran Q <-> ( x + ( k x. T ) ) e. ran Q ) )
6968rexbidv 2918 . . . . . . . . . . . . 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 3058 . . . . . . . . . . . 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 3594 . . . . . . . . . . 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 37311 . . . . . . . . . 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 457 . . . . . . . . 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 457 . . . . . . . 8 |- ( ph -> N e. NN )
7775simprd 461 . . . . . . . 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 463 . . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> F : RR --> RR )
80 fveq2 5849 . . . . . . . . . . . . . . . 16 |- ( i = j -> ( p ` i ) = ( p ` j ) )
81 oveq1 6285 . . . . . . . . . . . . . . . . 17 |- ( i = j -> ( i + 1 ) = ( j + 1 ) )
8281fveq2d 5853 . . . . . . . . . . . . . . . 16 |- ( i = j -> ( p ` ( i + 1 ) ) = ( p ` ( j + 1 ) ) )
8380, 82breq12d 4408 . . . . . . . . . . . . . . 15 |- ( i = j -> ( ( p ` i ) < ( p ` ( i + 1 ) ) <-> ( p ` j ) < ( p ` ( j + 1 ) ) ) )
8483cbvralv 3034 . . . . . . . . . . . . . 14 |- ( A. i e. ( 0..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) <-> A. j e. ( 0..^ n ) ( p ` j ) < ( p ` ( j + 1 ) ) )
8584anbi2i 692 . . . . . . . . . . . . 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 3048 . . . . . . . . . . 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 4478 . . . . . . . . . 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 2431 . . . . . . . . 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 463 . . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> M e. NN )
9153adantr 463 . . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> Q e. ( P ` M ) )
92 fourierdlem112.fper . . . . . . . . . 10 |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
9392adantlr 713 . . . . . . . . 9 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
94 eleq1 2474 . . . . . . . . . . . . 13 |- ( i = j -> ( i e. ( 0..^ M ) <-> j e. ( 0..^ M ) ) )
9594anbi2d 702 . . . . . . . . . . . 12 |- ( i = j -> ( ( ph /\ i e. ( 0..^ M ) ) <-> ( ph /\ j e. ( 0..^ M ) ) ) )
96 fveq2 5849 . . . . . . . . . . . . . . 15 |- ( i = j -> ( Q ` i ) = ( Q ` j ) )
9781fveq2d 5853 . . . . . . . . . . . . . . 15 |- ( i = j -> ( Q ` ( i + 1 ) ) = ( Q ` ( j + 1 ) ) )
9896, 97oveq12d 6296 . . . . . . . . . . . . . 14 |- ( i = j -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) )
9998reseq2d 5094 . . . . . . . . . . . . 13 |- ( i = j -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) )
10098oveq1d 6293 . . . . . . . . . . . . 13 |- ( i = j -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) )
10199, 100eleq12d 2484 . . . . . . . . . . . 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 318 . . . . . . . . . . 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 2041 . . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) )
105104adantlr 713 . . . . . . . . 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 463 . . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( -u pi + X ) e. RR )
10757rexrd 9673 . . . . . . . . . . 11 |- ( ph -> ( -u pi + X ) e. RR* )
108 pnfxr 11374 . . . . . . . . . . . 12 |- +oo e. RR*
109108a1i 11 . . . . . . . . . . 11 |- ( ph -> +oo e. RR* )
11058ltpnfd 36852 . . . . . . . . . . 11 |- ( ph -> ( pi + X ) < +oo )
111107, 109, 58, 66, 110eliood 36900 . . . . . . . . . 10 |- ( ph -> ( pi + X ) e. ( ( -u pi + X ) (,) +oo ) )
112111adantr 463 . . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( pi + X ) e. ( ( -u pi + X ) (,) +oo ) )
113 id 22 . . . . . . . . . . 11 |- ( i e. ( 0..^ N ) -> i e. ( 0..^ N ) )
11472oveq2i 6289 . . . . . . . . . . 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 2500 . . . . . . . . . 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 464 . . . . . . . . 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 6289 . . . . . . . . . . . 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 6201 . . . . . . . . . . . 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 5555 . . . . . . . . . 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 2431 . . . . . . . . 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 37355 . . . . . . . 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 463 . . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> E. w e. RR A. t e. RR ( abs ` ( F ` t ) ) <_ w )
125 nfra1 2785 . . . . . . . . . . 11 |- F/ t A. t e. RR ( abs ` ( F ` t ) ) <_ w
126 elioore 11612 . . . . . . . . . . . . 13 |- ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> t e. RR )
127 rspa 2771 . . . . . . . . . . . . 13 |- ( ( A. t e. RR ( abs ` ( F ` t ) ) <_ w /\ t e. RR ) -> ( abs ` ( F ` t ) ) <_ w )
128126, 127sylan2 472 . . . . . . . . . . . 12 |- ( ( A. t e. RR ( abs ` ( F ` t ) ) <_ w /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( F ` t ) ) <_ w )
129128ex 432 . . . . . . . . . . 11 |- ( A. t e. RR ( abs ` ( F ` t ) ) <_ w -> ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( abs ` ( F ` t ) ) <_ w ) )
130125, 129ralrimi 2804 . . . . . . . . . 10 |- ( A. t e. RR ( abs ` ( F ` t ) ) <_ w -> A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( F ` t ) ) <_ w )
131130reximi 2872 . . . . . . . . 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 3461 . . . . . . . . . . . 12 |- RR C_ RR
134 dvfre 22646 . . . . . . . . . . . 12 |- ( ( F : RR --> RR /\ RR C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
13543, 133, 134sylancl 660 . . . . . . . . . . 11 |- ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
136135adantr 463 . . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
137 eqid 2402 . . . . . . . . . . . . 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 5094 . . . . . . . . . . . . . . . . 17 |- ( i = j -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( RR _D F ) |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) )
141140, 100eleq12d 2484 . . . . . . . . . . . . . . . 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 318 . . . . . . . . . . . . . . 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 2041 . . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 0..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) )
145144adantlr 713 . . . . . . . . . . . . 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 9653 . . . . . . . . . . . . . 14 |- ( ph -> ( -u pi + X ) e. RR )
148147adantr 463 . . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( -u pi + X ) e. RR )
149147rexrd 9673 . . . . . . . . . . . . . . 15 |- ( ph -> ( -u pi + X ) e. RR* )
15055, 146readdcld 9653 . . . . . . . . . . . . . . 15 |- ( ph -> ( pi + X ) e. RR )
15156, 55, 146, 65ltadd1dd 10203 . . . . . . . . . . . . . . 15 |- ( ph -> ( -u pi + X ) < ( pi + X ) )
152150ltpnfd 36852 . . . . . . . . . . . . . . 15 |- ( ph -> ( pi + X ) < +oo )
153149, 109, 150, 151, 152eliood 36900 . . . . . . . . . . . . . 14 |- ( ph -> ( pi + X ) e. ( ( -u pi + X ) (,) +oo ) )
154153adantr 463 . . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( pi + X ) e. ( ( -u pi + X ) (,) +oo ) )
155 oveq1 6285 . . . . . . . . . . . . . . . . . . . . . 22 |- ( k = h -> ( k x. T ) = ( h x. T ) )
156155oveq2d 6294 . . . . . . . . . . . . . . . . . . . . 21 |- ( k = h -> ( y + ( k x. T ) ) = ( y + ( h x. T ) ) )
157156eleq1d 2471 . . . . . . . . . . . . . . . . . . . 20 |- ( k = h -> ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( h x. T ) ) e. ran Q ) )
158157cbvrexv 3035 . . . . . . . . . . . . . . . . . . 19 |- ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. h e. ZZ ( y + ( h x. T ) ) e. ran Q )
159158rgenw 2765 . . . . . . . . . . . . . . . . . 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 2986 . . . . . . . . . . . . . . . . . 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 208 . . . . . . . . . . . . . . . . 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 3594 . . . . . . . . . . . . . . . 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 6202 . . . . . . . . . . . . . . . 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 5555 . . . . . . . . . . . . . 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 2431 . . . . . . . . . . . . 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 2474 . . . . . . . . . . . . . . 15 |- ( v = u -> ( v e. dom ( RR _D F ) <-> u e. dom ( RR _D F ) ) )
168 fveq2 5849 . . . . . . . . . . . . . . 15 |- ( v = u -> ( ( RR _D F ) ` v ) = ( ( RR _D F ) ` u ) )
169167, 168ifbieq1d 3908 . . . . . . . . . . . . . 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 4487 . . . . . . . . . . . . 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 37354 . . . . . . . . . . . 12 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
172 cncff 21689 . . . . . . . . . . . 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 5718 . . . . . . . . . . . 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 5115 . . . . . . . . . . 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 212 . . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ dom ( RR _D F ) )
177136, 176fssresd 5735 . . . . . . . . 9 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
178 ax-resscn 9579 . . . . . . . . . . 11 |- RR C_ CC
179178a1i 11 . . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ N ) ) -> RR C_ CC )
180 cncffvrn 21694 . . . . . . . . . 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 659 . . . . . . . . 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 232 . . . . . . . 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 463 . . . . . . . . . 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 1728 . . . . . . . . . . . . . 14 |- F/ t ( ph /\ i e. ( 0..^ N ) )
186 nfra1 2785 . . . . . . . . . . . . . 14 |- F/ t A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z
187185, 186nfan 1956 . . . . . . . . . . . . 13 |- F/ t ( ( ph /\ i e. ( 0..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
188 fvres 5863 . . . . . . . . . . . . . . . . . 18 |- ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) = ( ( RR _D F ) ` t ) )
189188adantl 464 . . . . . . . . . . . . . . . . 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 5853 . . . . . . . . . . . . . . . 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 713 . . . . . . . . . . . . . . 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 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 )
193176sselda 3442 . . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> t e. dom ( RR _D F ) )
194193adantlr 713 . . . . . . . . . . . . . . . 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 2771 . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . 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 4415 . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . 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 2804 . . . . . . . . . . . 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 432 . . . . . . . . . . 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 2878 . . . . . . . . . 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 2785 . . . . . . . . . . . 12 |- F/ t A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z
204188eqcomd 2410 . . . . . . . . . . . . . . . 16 |- ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( ( RR _D F ) ` t ) = ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) )
205204fveq2d 5853 . . . . . . . . . . . . . . 15 |- ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) = ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) )
206205adantl 464 . . . . . . . . . . . . . 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 2771 . . . . . . . . . . . . . 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 4415 . . . . . . . . . . . . 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 432 . . . . . . . . . . . 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 2804 . . . . . . . . . . 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 2878 . . . . . . . . 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 1728 . . . . . . . . . . . 12 |- F/ i ( ph /\ j e. ( 0..^ M ) )
215 nfcsb1v 3389 . . . . . . . . . . . . 13 |- F/_ i [_ j / i ]_ C
216215nfel1 2580 . . . . . . . . . . . 12 |- F/ i [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` j ) )
217214, 216nfim 1948 . . . . . . . . . . 11 |- F/ i ( ( ph /\ j e. ( 0..^ M ) ) -> [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` j ) ) )
218 csbeq1a 3382 . . . . . . . . . . . . 13 |- ( i = j -> C = [_ j / i ]_ C )
21999, 96oveq12d 6296 . . . . . . . . . . . . 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 2484 . . . . . . . . . . . 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 318 . . . . . . . . . . 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 2040 . . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ M ) ) -> [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` j ) ) )
224223adantlr 713 . . . . . . . . 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 37353 . . . . . . . 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 3389 . . . . . . . . . . . . 13 |- F/_ i [_ j / i ]_ U
227226nfel1 2580 . . . . . . . . . . . 12 |- F/ i [_ j / i ]_ U e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` ( j + 1 ) ) )
228214, 227nfim 1948 . . . . . . . . . . 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 3382 . . . . . . . . . . . . 13 |- ( i = j -> U = [_ j / i ]_ U )
23099, 97oveq12d 6296 . . . . . . . . . . . . 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 2484 . . . . . . . . . . . 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 318 . . . . . . . . . . 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 2040 . . . . . . . . . 10 |- ( ( ph /\ j e. ( 0..^ M ) ) -> [_ j / i ]_ U e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) lim CC ( Q ` ( j + 1 ) ) ) )
235234adantlr 713 . . . . . . . . 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 37356 . . . . . . . 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 2406 . . . . . . . . . 10 |- ( g = s -> ( g = 0 <-> s = 0 ) )
238 oveq2 6286 . . . . . . . . . . . . 13 |- ( g = s -> ( X + g ) = ( X + s ) )
239238fveq2d 5853 . . . . . . . . . . . 12 |- ( g = s -> ( F ` ( X + g ) ) = ( F ` ( X + s ) ) )
240 breq2 4399 . . . . . . . . . . . . 13 |- ( g = s -> ( 0 < g <-> 0 < s ) )
241240ifbid 3907 . . . . . . . . . . . 12 |- ( g = s -> if ( 0 < g , R , L ) = if ( 0 < s , R , L ) )
242239, 241oveq12d 6296 . . . . . . . . . . 11 |- ( g = s -> ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) = ( ( F ` ( X + s ) ) - if ( 0 < s , R , L ) ) )
243 id 22 . . . . . . . . . . 11 |- ( g = s -> g = s )
244242, 243oveq12d 6296 . . . . . . . . . 10 |- ( g = s -> ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , R , L ) ) / s ) )
245237, 244ifbieq2d 3910 . . . . . . . . 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 4487 . . . . . . . 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 2406 . . . . . . . . . 10 |- ( o = s -> ( o = 0 <-> s = 0 ) )
248 id 22 . . . . . . . . . . 11 |- ( o = s -> o = s )
249 oveq1 6285 . . . . . . . . . . . . 13 |- ( o = s -> ( o / 2 ) = ( s / 2 ) )
250249fveq2d 5853 . . . . . . . . . . . 12 |- ( o = s -> ( sin ` ( o / 2 ) ) = ( sin ` ( s / 2 ) ) )
251250oveq2d 6294 . . . . . . . . . . 11 |- ( o = s -> ( 2 x. ( sin ` ( o / 2 ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
252248, 251oveq12d 6296 . . . . . . . . . 10 |- ( o = s -> ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
253247, 252ifbieq2d 3910 . . . . . . . . 9 |- ( o = s -> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) = if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
254253cbvmptv 4487 . . . . . . . 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 5849 . . . . . . . . . 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 5849 . . . . . . . . . 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 6296 . . . . . . . . 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 4487 . . . . . . . 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 6286 . . . . . . . . . 10 |- ( d = s -> ( ( k + ( 1 / 2 ) ) x. d ) = ( ( k + ( 1 / 2 ) ) x. s ) )
260259fveq2d 5853 . . . . . . . . 9 |- ( d = s -> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) = ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) )
261260cbvmptv 4487 . . . . . . . 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 5849 . . . . . . . . . 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 5849 . . . . . . . . . 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 6296 . . . . . . . . 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 4487 . . . . . . . 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 5849 . . . . . . . . . . . . 13 |- ( m = n -> ( D ` m ) = ( D ` n ) )
267266fveq1d 5851 . . . . . . . . . . . 12 |- ( m = n -> ( ( D ` m ) ` s ) = ( ( D ` n ) ` s ) )
268267