Metamath Proof Explorer

Theorem fourierdlem113

Description: Fourier series convergence for periodic, piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem113.f 
|- ( ph -> F : RR --> RR )
fourierdlem113.t 
|- T = ( 2 x. _pi )
fourierdlem113.per 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem113.x 
|- ( ph -> X e. RR )
fourierdlem113.l 
|- ( ph -> L e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
fourierdlem113.r 
|- ( ph -> R e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
fourierdlem113.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 ) ) ) } )
fourierdlem113.m 
|- ( ph -> M e. NN )
fourierdlem113.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem113.dvcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem113.dvlb 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) =/= (/) )
fourierdlem113.dvub 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) =/= (/) )
fourierdlem113.a 
|- A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
fourierdlem113.b 
|- B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
fourierdlem113.15 
|- S = ( n e. NN |-> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
fourierdlem113.e 
|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) ) )
fourierdlem113.exq 
|- ( ph -> ( E ` X ) e. ran Q )
Assertion fourierdlem113 
|- ( 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 ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem113.f 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem113.t 
 |-  T = ( 2 x. _pi )
3 fourierdlem113.per 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
4 fourierdlem113.x 
 |-  ( ph -> X e. RR )
5 fourierdlem113.l 
 |-  ( ph -> L e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
6 fourierdlem113.r 
 |-  ( ph -> R e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
7 fourierdlem113.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 ) ) ) } )
8 fourierdlem113.m 
 |-  ( ph -> M e. NN )
9 fourierdlem113.q 
 |-  ( ph -> Q e. ( P ` M ) )
10 fourierdlem113.dvcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
11 fourierdlem113.dvlb 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) =/= (/) )
12 fourierdlem113.dvub 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) =/= (/) )
13 fourierdlem113.a 
 |-  A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
14 fourierdlem113.b 
 |-  B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
15 fourierdlem113.15 
 |-  S = ( n e. NN |-> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
16 fourierdlem113.e 
 |-  E = ( x e. RR |-> ( x + ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) ) )
17 fourierdlem113.exq 
 |-  ( ph -> ( E ` X ) e. ran Q )
18 oveq1 
 |-  ( w = y -> ( w mod ( 2 x. _pi ) ) = ( y mod ( 2 x. _pi ) ) )
19 18 eqeq1d 
 |-  ( w = y -> ( ( w mod ( 2 x. _pi ) ) = 0 <-> ( y mod ( 2 x. _pi ) ) = 0 ) )
20 oveq2 
 |-  ( w = y -> ( ( k + ( 1 / 2 ) ) x. w ) = ( ( k + ( 1 / 2 ) ) x. y ) )
21 20 fveq2d 
 |-  ( w = y -> ( sin ` ( ( k + ( 1 / 2 ) ) x. w ) ) = ( sin ` ( ( k + ( 1 / 2 ) ) x. y ) ) )
22 fvoveq1 
 |-  ( w = y -> ( sin ` ( w / 2 ) ) = ( sin ` ( y / 2 ) ) )
23 22 oveq2d 
 |-  ( w = y -> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) )
24 21 23 oveq12d 
 |-  ( w = y -> ( ( sin ` ( ( k + ( 1 / 2 ) ) x. w ) ) / ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) = ( ( sin ` ( ( k + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) )
25 19 24 ifbieq2d 
 |-  ( w = y -> if ( ( w mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. w ) ) / ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) ) = if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) )
26 25 cbvmptv 
 |-  ( w e. RR |-> if ( ( w mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. w ) ) / ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) ) ) = ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) )
27 oveq2 
 |-  ( k = m -> ( 2 x. k ) = ( 2 x. m ) )
28 27 oveq1d 
 |-  ( k = m -> ( ( 2 x. k ) + 1 ) = ( ( 2 x. m ) + 1 ) )
29 28 oveq1d 
 |-  ( k = m -> ( ( ( 2 x. k ) + 1 ) / ( 2 x. _pi ) ) = ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) )
30 oveq1 
 |-  ( k = m -> ( k + ( 1 / 2 ) ) = ( m + ( 1 / 2 ) ) )
31 30 fvoveq1d 
 |-  ( k = m -> ( sin ` ( ( k + ( 1 / 2 ) ) x. y ) ) = ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) )
32 31 oveq1d 
 |-  ( k = m -> ( ( sin ` ( ( k + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) = ( ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) )
33 29 32 ifeq12d 
 |-  ( k = m -> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = 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 ) ) ) ) ) )
34 33 mpteq2dv 
 |-  ( k = m -> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) = ( 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 ) ) ) ) ) ) )
35 26 34 eqtrid 
 |-  ( k = m -> ( w e. RR |-> if ( ( w mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. w ) ) / ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) ) ) = ( 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 ) ) ) ) ) ) )
36 35 cbvmptv 
 |-  ( k e. NN |-> ( w e. RR |-> if ( ( w mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. w ) ) / ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) ) ) ) = ( 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 ) ) ) ) ) ) )
37 oveq1 
 |-  ( w = y -> ( w + ( j x. T ) ) = ( y + ( j x. T ) ) )
38 37 eleq1d 
 |-  ( w = y -> ( ( w + ( j x. T ) ) e. ran Q <-> ( y + ( j x. T ) ) e. ran Q ) )
39 38 rexbidv 
 |-  ( w = y -> ( E. j e. ZZ ( w + ( j x. T ) ) e. ran Q <-> E. j e. ZZ ( y + ( j x. T ) ) e. ran Q ) )
40 39 cbvrabv 
 |-  { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } = { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q }
41 40 uneq2i 
 |-  ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) = ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } )
42 41 fveq2i 
 |-  ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) = ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) )
43 42 oveq1i 
 |-  ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) = ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) - 1 )
44 oveq1 
 |-  ( k = j -> ( k x. T ) = ( j x. T ) )
45 44 oveq2d 
 |-  ( k = j -> ( y + ( k x. T ) ) = ( y + ( j x. T ) ) )
46 45 eleq1d 
 |-  ( k = j -> ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( j x. T ) ) e. ran Q ) )
47 46 cbvrexvw 
 |-  ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. j e. ZZ ( y + ( j x. T ) ) e. ran Q )
48 47 rabbii 
 |-  { 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. j e. ZZ ( y + ( j x. T ) ) e. ran Q }
49 48 uneq2i 
 |-  ( { ( -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. j e. ZZ ( y + ( j x. T ) ) e. ran Q } )
50 isoeq5 
 |-  ( ( { ( -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. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( 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 } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) ) )
51 49 50 ax-mp 
 |-  ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( 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 } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) )
52 51 a1i 
 |-  ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( 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 } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) ) )
53 44 oveq2d 
 |-  ( k = j -> ( w + ( k x. T ) ) = ( w + ( j x. T ) ) )
54 53 eleq1d 
 |-  ( k = j -> ( ( w + ( k x. T ) ) e. ran Q <-> ( w + ( j x. T ) ) e. ran Q ) )
55 54 cbvrexvw 
 |-  ( E. k e. ZZ ( w + ( k x. T ) ) e. ran Q <-> E. j e. ZZ ( w + ( j x. T ) ) e. ran Q )
56 55 rabbii 
 |-  { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } = { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q }
57 56 uneq2i 
 |-  ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) = ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } )
58 57 fveq2i 
 |-  ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) = ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) )
59 58 oveq1i 
 |-  ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) = ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 )
60 59 oveq2i 
 |-  ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) = ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) )
61 isoeq4 
 |-  ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) = ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) ) -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) ) )
62 60 61 ax-mp 
 |-  ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) )
63 62 a1i 
 |-  ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) ) )
64 isoeq1 
 |-  ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) ) )
65 52 63 64 3bitrd 
 |-  ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( 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. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) ) )
66 65 cbviotavw 
 |-  ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( 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. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( w + ( j x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. j e. ZZ ( y + ( j x. T ) ) e. ran Q } ) ) )
67 pire 
 |-  _pi e. RR
68 67 renegcli 
 |-  -u _pi e. RR
69 68 a1i 
 |-  ( ph -> -u _pi e. RR )
70 67 a1i 
 |-  ( ph -> _pi e. RR )
71 negpilt0 
 |-  -u _pi < 0
72 71 a1i 
 |-  ( ph -> -u _pi < 0 )
73 pipos 
 |-  0 < _pi
74 73 a1i 
 |-  ( ph -> 0 < _pi )
75 picn 
 |-  _pi e. CC
76 75 2timesi 
 |-  ( 2 x. _pi ) = ( _pi + _pi )
77 75 75 subnegi 
 |-  ( _pi - -u _pi ) = ( _pi + _pi )
78 76 2 77 3eqtr4i 
 |-  T = ( _pi - -u _pi )
79 7 fourierdlem2 
 |-  ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
80 8 79 syl 
 |-  ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
81 9 80 mpbid 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
82 81 simpld 
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
83 elmapi 
 |-  ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
84 82 83 syl 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
85 fzfid 
 |-  ( ph -> ( 0 ... M ) e. Fin )
86 rnffi 
 |-  ( ( Q : ( 0 ... M ) --> RR /\ ( 0 ... M ) e. Fin ) -> ran Q e. Fin )
87 84 85 86 syl2anc 
 |-  ( ph -> ran Q e. Fin )
88 7 8 9 fourierdlem15 
 |-  ( ph -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
89 88 frnd 
 |-  ( ph -> ran Q C_ ( -u _pi [,] _pi ) )
90 81 simprd 
 |-  ( ph -> ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
91 90 simplrd 
 |-  ( ph -> ( Q ` M ) = _pi )
92 88 ffund 
 |-  ( ph -> Fun Q )
93 8 nnnn0d 
 |-  ( ph -> M e. NN0 )
94 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
95 93 94 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
96 eluzfz2 
 |-  ( M e. ( ZZ>= ` 0 ) -> M e. ( 0 ... M ) )
97 95 96 syl 
 |-  ( ph -> M e. ( 0 ... M ) )
98 88 fdmd 
 |-  ( ph -> dom Q = ( 0 ... M ) )
99 98 eqcomd 
 |-  ( ph -> ( 0 ... M ) = dom Q )
100 97 99 eleqtrd 
 |-  ( ph -> M e. dom Q )
101 fvelrn 
 |-  ( ( Fun Q /\ M e. dom Q ) -> ( Q ` M ) e. ran Q )
102 92 100 101 syl2anc 
 |-  ( ph -> ( Q ` M ) e. ran Q )
103 91 102 eqeltrrd 
 |-  ( ph -> _pi e. ran Q )
104 eqid 
 |-  ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) = ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } )
105 isoeq1 
 |-  ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( 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. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( 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 } ) ) ) )
106 41 57 49 3eqtr4ri 
 |-  ( { ( -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. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } )
107 isoeq5 
 |-  ( ( { ( -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. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) -> ( f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( 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. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) ) )
108 106 107 ax-mp 
 |-  ( f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( 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. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) )
109 105 108 bitrdi 
 |-  ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( 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. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) ) )
110 109 cbviotavw 
 |-  ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( 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. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) )
111 eqid 
 |-  { w e. ( ( -u _pi + X ) (,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } = { w e. ( ( -u _pi + X ) (,] ( _pi + X ) ) | E. k e. ZZ ( w + ( k x. T ) ) e. ran Q }
112 69 70 72 74 78 87 89 103 16 4 17 104 110 111 fourierdlem51 
 |-  ( ph -> X e. ran ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { w e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( w + ( 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 } ) ) ) )
113 ax-resscn 
 |-  RR C_ CC
114 113 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> RR C_ CC )
115 ioossre 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
116 115 a1i 
 |-  ( ph -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
117 1 116 fssresd 
 |-  ( ph -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> RR )
118 113 a1i 
 |-  ( ph -> RR C_ CC )
119 117 118 fssd 
 |-  ( ph -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
120 119 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
121 115 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
122 1 118 fssd 
 |-  ( ph -> F : RR --> CC )
123 122 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> F : RR --> CC )
124 ssidd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> RR C_ RR )
125 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
126 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
127 125 126 dvres 
 |-  ( ( ( RR C_ CC /\ F : RR --> CC ) /\ ( RR C_ RR /\ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR ) ) -> ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) )
128 114 123 124 121 127 syl22anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) )
129 128 dmeqd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = dom ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) )
130 ioontr 
 |-  ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) )
131 130 reseq2i 
 |-  ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
132 131 dmeqi 
 |-  dom ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = dom ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
133 132 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = dom ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
134 cncff 
 |-  ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
135 fdm 
 |-  ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC -> dom ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
136 10 134 135 3syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
137 129 133 136 3eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> dom ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
138 dvcn 
 |-  ( ( ( RR C_ CC /\ ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC /\ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR ) /\ dom ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
139 114 120 121 137 138 syl31anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
140 121 114 sstrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
141 84 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
142 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
143 142 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
144 141 143 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
145 144 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
146 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
147 146 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
148 141 147 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
149 81 simprrd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) )
150 149 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
151 125 145 148 150 lptioo1cn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
152 117 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> RR )
153 ssidd 
 |-  ( ph -> RR C_ RR )
154 118 122 153 dvbss 
 |-  ( ph -> dom ( RR _D F ) C_ RR )
155 dvfre 
 |-  ( ( F : RR --> RR /\ RR C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
156 1 153 155 syl2anc 
 |-  ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
157 0re 
 |-  0 e. RR
158 68 157 67 lttri 
 |-  ( ( -u _pi < 0 /\ 0 < _pi ) -> -u _pi < _pi )
159 71 73 158 mp2an 
 |-  -u _pi < _pi
160 159 a1i 
 |-  ( ph -> -u _pi < _pi )
161 90 simplld 
 |-  ( ph -> ( Q ` 0 ) = -u _pi )
162 10 134 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
163 162 140 151 11 125 ellimciota 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( iota x x e. ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) ) e. ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
164 148 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR* )
165 125 164 144 150 lptioo2cn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
166 162 140 165 12 125 ellimciota 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( iota x x e. ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) ) e. ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
167 122 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> F : RR --> CC )
168 zre 
 |-  ( k e. ZZ -> k e. RR )
169 168 adantl 
 |-  ( ( ph /\ k e. ZZ ) -> k e. RR )
170 2pire 
 |-  ( 2 x. _pi ) e. RR
171 170 a1i 
 |-  ( ph -> ( 2 x. _pi ) e. RR )
172 2 171 eqeltrid 
 |-  ( ph -> T e. RR )
173 172 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> T e. RR )
174 169 173 remulcld 
 |-  ( ( ph /\ k e. ZZ ) -> ( k x. T ) e. RR )
175 167 adantr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) -> F : RR --> CC )
176 173 adantr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) -> T e. RR )
177 simplr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) -> k e. ZZ )
178 simpr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) -> t e. RR )
179 3 ad4ant14 
 |-  ( ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
180 175 176 177 178 179 fperiodmul 
 |-  ( ( ( ph /\ k e. ZZ ) /\ t e. RR ) -> ( F ` ( t + ( k x. T ) ) ) = ( F ` t ) )
181 eqid 
 |-  ( RR _D F ) = ( RR _D F )
182 167 174 180 181 fperdvper 
 |-  ( ( ( ph /\ k e. ZZ ) /\ t e. dom ( RR _D F ) ) -> ( ( t + ( k x. T ) ) e. dom ( RR _D F ) /\ ( ( RR _D F ) ` ( t + ( k x. T ) ) ) = ( ( RR _D F ) ` t ) ) )
183 182 an32s 
 |-  ( ( ( ph /\ t e. dom ( RR _D F ) ) /\ k e. ZZ ) -> ( ( t + ( k x. T ) ) e. dom ( RR _D F ) /\ ( ( RR _D F ) ` ( t + ( k x. T ) ) ) = ( ( RR _D F ) ` t ) ) )
184 183 simpld 
 |-  ( ( ( ph /\ t e. dom ( RR _D F ) ) /\ k e. ZZ ) -> ( t + ( k x. T ) ) e. dom ( RR _D F ) )
185 183 simprd 
 |-  ( ( ( ph /\ t e. dom ( RR _D F ) ) /\ k e. ZZ ) -> ( ( RR _D F ) ` ( t + ( k x. T ) ) ) = ( ( RR _D F ) ` t ) )
186 fveq2 
 |-  ( j = i -> ( Q ` j ) = ( Q ` i ) )
187 fvoveq1 
 |-  ( j = i -> ( Q ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) )
188 186 187 oveq12d 
 |-  ( j = i -> ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
189 188 cbvmptv 
 |-  ( j e. ( 0 ..^ M ) |-> ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) = ( i e. ( 0 ..^ M ) |-> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
190 eqid 
 |-  ( t e. RR |-> ( t + ( ( |_ ` ( ( _pi - t ) / T ) ) x. T ) ) ) = ( t e. RR |-> ( t + ( ( |_ ` ( ( _pi - t ) / T ) ) x. T ) ) )
191 154 156 69 70 160 78 8 84 161 91 10 163 166 184 185 189 190 fourierdlem71 
 |-  ( ph -> E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
192 191 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
193 nfv 
 |-  F/ t ( ph /\ i e. ( 0 ..^ M ) )
194 nfra1 
 |-  F/ t A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z
195 193 194 nfan 
 |-  F/ t ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
196 128 131 eqtrdi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) = ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
197 196 fveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) = ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) )
198 fvres 
 |-  ( t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ` t ) = ( ( RR _D F ) ` t ) )
199 197 198 sylan9eq 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) = ( ( RR _D F ) ` t ) )
200 199 fveq2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) = ( abs ` ( ( RR _D F ) ` t ) ) )
201 200 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) = ( abs ` ( ( RR _D F ) ` t ) ) )
202 simplr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
203 ssdmres 
 |-  ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom ( RR _D F ) <-> dom ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
204 136 203 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom ( RR _D F ) )
205 204 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom ( RR _D F ) )
206 simpr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
207 205 206 sseldd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> t e. dom ( RR _D F ) )
208 rspa 
 |-  ( ( 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 )
209 202 207 208 syl2anc 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
210 201 209 eqbrtrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) <_ z )
211 195 210 ralrimia 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) -> A. t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) <_ z )
212 211 ex 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z -> A. t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) <_ z ) )
213 212 reximdv 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z -> E. z e. RR A. t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) <_ z ) )
214 192 213 mpd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> E. z e. RR A. t e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( abs ` ( ( RR _D ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) ` t ) ) <_ z )
215 148 144 152 137 214 ioodvbdlimc1 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) =/= (/) )
216 120 140 151 215 125 ellimciota 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( iota y y e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) ) e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
217 148 144 152 137 214 ioodvbdlimc2 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) =/= (/) )
218 120 140 165 217 125 ellimciota 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( iota y y e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) ) e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
219 resindm 
 |-  ( ( RR _D F ) |` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) = ( ( RR _D F ) |` ( -oo (,) X ) )
220 219 a1i 
 |-  ( ph -> ( ( RR _D F ) |` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) = ( ( RR _D F ) |` ( -oo (,) X ) ) )
221 inss2 
 |-  ( ( -oo (,) X ) i^i dom ( RR _D F ) ) C_ dom ( RR _D F )
222 221 a1i 
 |-  ( ph -> ( ( -oo (,) X ) i^i dom ( RR _D F ) ) C_ dom ( RR _D F ) )
223 156 222 fssresd 
 |-  ( ph -> ( ( RR _D F ) |` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) : ( ( -oo (,) X ) i^i dom ( RR _D F ) ) --> RR )
224 220 223 feq1dd 
 |-  ( ph -> ( ( RR _D F ) |` ( -oo (,) X ) ) : ( ( -oo (,) X ) i^i dom ( RR _D F ) ) --> RR )
225 224 118 fssd 
 |-  ( ph -> ( ( RR _D F ) |` ( -oo (,) X ) ) : ( ( -oo (,) X ) i^i dom ( RR _D F ) ) --> CC )
226 ioosscn 
 |-  ( -oo (,) X ) C_ CC
227 ssinss1 
 |-  ( ( -oo (,) X ) C_ CC -> ( ( -oo (,) X ) i^i dom ( RR _D F ) ) C_ CC )
228 226 227 ax-mp 
 |-  ( ( -oo (,) X ) i^i dom ( RR _D F ) ) C_ CC
229 228 a1i 
 |-  ( ph -> ( ( -oo (,) X ) i^i dom ( RR _D F ) ) C_ CC )
230 3simpb 
 |-  ( ( ph /\ x e. dom ( RR _D F ) /\ k e. ZZ ) -> ( ph /\ k e. ZZ ) )
231 simp2 
 |-  ( ( ph /\ x e. dom ( RR _D F ) /\ k e. ZZ ) -> x e. dom ( RR _D F ) )
232 167 adantr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) -> F : RR --> CC )
233 173 adantr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) -> T e. RR )
234 simplr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) -> k e. ZZ )
235 simpr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) -> x e. RR )
236 eleq1w 
 |-  ( x = y -> ( x e. RR <-> y e. RR ) )
237 236 anbi2d 
 |-  ( x = y -> ( ( ph /\ x e. RR ) <-> ( ph /\ y e. RR ) ) )
238 fvoveq1 
 |-  ( x = y -> ( F ` ( x + T ) ) = ( F ` ( y + T ) ) )
239 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
240 238 239 eqeq12d 
 |-  ( x = y -> ( ( F ` ( x + T ) ) = ( F ` x ) <-> ( F ` ( y + T ) ) = ( F ` y ) ) )
241 237 240 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) ) <-> ( ( ph /\ y e. RR ) -> ( F ` ( y + T ) ) = ( F ` y ) ) ) )
242 241 3 chvarvv 
 |-  ( ( ph /\ y e. RR ) -> ( F ` ( y + T ) ) = ( F ` y ) )
243 242 ad4ant14 
 |-  ( ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) /\ y e. RR ) -> ( F ` ( y + T ) ) = ( F ` y ) )
244 232 233 234 235 243 fperiodmul 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. RR ) -> ( F ` ( x + ( k x. T ) ) ) = ( F ` x ) )
245 167 174 244 181 fperdvper 
 |-  ( ( ( ph /\ k e. ZZ ) /\ x e. dom ( RR _D F ) ) -> ( ( x + ( k x. T ) ) e. dom ( RR _D F ) /\ ( ( RR _D F ) ` ( x + ( k x. T ) ) ) = ( ( RR _D F ) ` x ) ) )
246 230 231 245 syl2anc 
 |-  ( ( ph /\ x e. dom ( RR _D F ) /\ k e. ZZ ) -> ( ( x + ( k x. T ) ) e. dom ( RR _D F ) /\ ( ( RR _D F ) ` ( x + ( k x. T ) ) ) = ( ( RR _D F ) ` x ) ) )
247 246 simpld 
 |-  ( ( ph /\ x e. dom ( RR _D F ) /\ k e. ZZ ) -> ( x + ( k x. T ) ) e. dom ( RR _D F ) )
248 oveq2 
 |-  ( w = x -> ( _pi - w ) = ( _pi - x ) )
249 248 fvoveq1d 
 |-  ( w = x -> ( |_ ` ( ( _pi - w ) / T ) ) = ( |_ ` ( ( _pi - x ) / T ) ) )
250 249 oveq1d 
 |-  ( w = x -> ( ( |_ ` ( ( _pi - w ) / T ) ) x. T ) = ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) )
251 250 cbvmptv 
 |-  ( w e. RR |-> ( ( |_ ` ( ( _pi - w ) / T ) ) x. T ) ) = ( x e. RR |-> ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) )
252 eqid 
 |-  ( x e. RR |-> ( x + ( ( w e. RR |-> ( ( |_ ` ( ( _pi - w ) / T ) ) x. T ) ) ` x ) ) ) = ( x e. RR |-> ( x + ( ( w e. RR |-> ( ( |_ ` ( ( _pi - w ) / T ) ) x. T ) ) ` x ) ) )
253 69 70 160 78 247 4 251 252 7 8 9 204 fourierdlem41 
 |-  ( ph -> ( E. y e. RR ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) /\ E. y e. RR ( X < y /\ ( X (,) y ) C_ dom ( RR _D F ) ) ) )
254 253 simpld 
 |-  ( ph -> E. y e. RR ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) )
255 125 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
256 mnfxr 
 |-  -oo e. RR*
257 rexr 
 |-  ( y e. RR -> y e. RR* )
258 257 mnfled 
 |-  ( y e. RR -> -oo <_ y )
259 iooss1 
 |-  ( ( -oo e. RR* /\ -oo <_ y ) -> ( y (,) X ) C_ ( -oo (,) X ) )
260 256 258 259 sylancr 
 |-  ( y e. RR -> ( y (,) X ) C_ ( -oo (,) X ) )
261 260 3ad2ant2 
 |-  ( ( ph /\ y e. RR /\ ( y (,) X ) C_ dom ( RR _D F ) ) -> ( y (,) X ) C_ ( -oo (,) X ) )
262 simp3 
 |-  ( ( ph /\ y e. RR /\ ( y (,) X ) C_ dom ( RR _D F ) ) -> ( y (,) X ) C_ dom ( RR _D F ) )
263 261 262 ssind 
 |-  ( ( ph /\ y e. RR /\ ( y (,) X ) C_ dom ( RR _D F ) ) -> ( y (,) X ) C_ ( ( -oo (,) X ) i^i dom ( RR _D F ) ) )
264 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
265 264 lpss3 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( ( -oo (,) X ) i^i dom ( RR _D F ) ) C_ CC /\ ( y (,) X ) C_ ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) -> ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( y (,) X ) ) C_ ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) )
266 255 228 263 265 mp3an12i 
 |-  ( ( ph /\ y e. RR /\ ( y (,) X ) C_ dom ( RR _D F ) ) -> ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( y (,) X ) ) C_ ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) )
267 266 3adant3l 
 |-  ( ( ph /\ y e. RR /\ ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) ) -> ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( y (,) X ) ) C_ ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) )
268 257 3ad2ant2 
 |-  ( ( ph /\ y e. RR /\ ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) ) -> y e. RR* )
269 4 3ad2ant1 
 |-  ( ( ph /\ y e. RR /\ ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) ) -> X e. RR )
270 simp3l 
 |-  ( ( ph /\ y e. RR /\ ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) ) -> y < X )
271 125 268 269 270 lptioo2cn 
 |-  ( ( ph /\ y e. RR /\ ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) ) -> X e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( y (,) X ) ) )
272 267 271 sseldd 
 |-  ( ( ph /\ y e. RR /\ ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) ) -> X e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) )
273 272 rexlimdv3a 
 |-  ( ph -> ( E. y e. RR ( y < X /\ ( y (,) X ) C_ dom ( RR _D F ) ) -> X e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) ) )
274 254 273 mpd 
 |-  ( ph -> X e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( ( -oo (,) X ) i^i dom ( RR _D F ) ) ) )
275 246 simprd 
 |-  ( ( ph /\ x e. dom ( RR _D F ) /\ k e. ZZ ) -> ( ( RR _D F ) ` ( x + ( k x. T ) ) ) = ( ( RR _D F ) ` x ) )
276 oveq2 
 |-  ( y = x -> ( _pi - y ) = ( _pi - x ) )
277 276 fvoveq1d 
 |-  ( y = x -> ( |_ ` ( ( _pi - y ) / T ) ) = ( |_ ` ( ( _pi - x ) / T ) ) )
278 277 oveq1d 
 |-  ( y = x -> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) = ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) )
279 278 cbvmptv 
 |-  ( y e. RR |-> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) = ( x e. RR |-> ( ( |_ ` ( ( _pi - x ) / T ) ) x. T ) )
280 id 
 |-  ( z = x -> z = x )
281 fveq2 
 |-  ( z = x -> ( ( y e. RR |-> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ` z ) = ( ( y e. RR |-> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ` x ) )
282 280 281 oveq12d 
 |-  ( z = x -> ( z + ( ( y e. RR |-> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ` z ) ) = ( x + ( ( y e. RR |-> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ` x ) ) )
283 282 cbvmptv 
 |-  ( z e. RR |-> ( z + ( ( y e. RR |-> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ` z ) ) ) = ( x e. RR |-> ( x + ( ( y e. RR |-> ( ( |_ ` ( ( _pi - y ) / T ) ) x. T ) ) ` x ) ) )
284 69 70 160 7 78 8 9 154 156 247 275 10 166 4 279 283 fourierdlem49 
 |-  ( ph -> ( ( ( RR _D F ) |` ( -oo (,) X ) ) limCC X ) =/= (/) )
285 225 229 274 284 125 ellimciota 
 |-  ( ph -> ( iota x x e. ( ( ( RR _D F ) |` ( -oo (,) X ) ) limCC X ) ) e. ( ( ( RR _D F ) |` ( -oo (,) X ) ) limCC X ) )
286 resindm 
 |-  ( ( RR _D F ) |` ( ( X (,) +oo ) i^i dom ( RR _D F ) ) ) = ( ( RR _D F ) |` ( X (,) +oo ) )
287 286 a1i 
 |-  ( ph -> ( ( RR _D F ) |` ( ( X (,) +oo ) i^i dom ( RR _D F ) ) ) = ( ( RR _D F ) |` ( X (,) +oo ) ) )
288 inss2 
 |-  ( ( X (,) +oo ) i^i dom ( RR _D F ) ) C_ dom ( RR _D F )
289 288 a1i 
 |-  ( ph -> ( ( X (,) +oo ) i^i dom ( RR _D F ) ) C_ dom ( RR _D F ) )
290 156 289 fssresd 
 |-  ( ph -> ( ( RR _D F ) |` ( ( X (,) +oo ) i^i dom ( RR _D F ) ) ) : ( ( X (,) +oo ) i^i dom ( RR _D F ) ) --> RR )
291 287 290 feq1dd 
 |-  ( ph -> ( ( RR _D F ) |` ( X (,) +oo ) ) : ( ( X (,) +oo ) i^i dom ( RR _D F ) ) --> RR )
292 291 118 fssd 
 |-  ( ph -> ( ( RR _D F ) |` ( X (,) +oo ) ) : ( ( X (,) +oo ) i^i dom ( RR _D F ) ) --> CC )
293 ioosscn 
 |-  ( X (,) +oo ) C_ CC
294 ssinss1 
 |-  ( ( X (,) +oo ) C_ CC -> ( ( X (,) +oo ) i^i dom ( RR _D F ) ) C_ CC )
295 293 294 ax-mp 
 |-  ( ( X (,) +oo ) i^i dom ( RR _D F ) ) C_ CC
296 295 a1i 
 |-  ( ph -> ( ( X (,) +oo ) i^i dom ( RR _D F ) ) C_ CC )
297 253 simprd 
 |-  ( ph -> E. y e. RR ( X < y /\ ( X (,) y ) C_ dom ( RR _D F ) ) )
298 pnfxr 
 |-  +oo e. RR*
299 257 pnfged 
 |-  ( y e. RR -> y <_ +oo )
300 iooss2 
 |-  ( ( +oo e. RR* /\ y <_ +oo ) -> ( X (,) y ) C_ ( X (,) +oo ) )
301 298 299 300 sylancr 
 |-  ( y e. RR -> ( X (,) y ) C_ ( X (,) +oo ) )
302 301 3ad2ant2 
 |-  ( ( ph /\ y e. RR /\ ( X (,) y ) C_ dom ( RR _D F ) ) -> ( X (,) y ) C_ ( X (,) +oo ) )
303 simp3 
 |-  ( ( ph /\ y e. RR /\ ( X (,) y ) C_ dom ( RR _D F ) ) -> ( X (,) y ) C_ dom ( RR _D F ) )
304 302 303 ssind 
 |-  ( ( ph /\ y e. RR /\ ( X (,) y ) C_ dom ( RR _D F ) ) -> ( X (,) y ) C_ ( ( X (,) +oo ) i^i dom ( RR _D F ) ) )
305 264 lpss3 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( ( X (,) +oo ) i^i dom ( RR _D F ) ) C_ CC /\ ( X (,) y ) C_ ( ( X (,) +oo ) i^i dom ( RR _D F ) ) ) -> ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( X (,) y ) ) C_ ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( ( X (,) +oo ) i^i dom ( RR _D F ) ) ) )
306 255 295 304 305 mp3an12i 
 |-  ( ( ph /\ y e. RR /\ ( X (,) y ) C_ dom ( RR _D F ) ) -> ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( X (,) y ) ) C_ ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( ( X (,) +oo ) i^i dom ( RR _D F ) ) ) )
307 306 3adant3l 
 |-  ( ( ph /\ y e. RR /\ ( X < y /\ ( X (,) y ) C_ dom ( RR _D F ) ) ) -> ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( X (,) y ) ) C_ ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( ( X (,) +oo ) i^i dom ( RR _D F ) ) ) )
308 257 3ad2ant2 
 |-  ( ( ph /\ y e. RR /\ ( X < y /\ ( X (,) y ) C_ dom ( RR _D F ) ) ) -> y e. RR* )
309 4 3ad2ant1 
 |-  ( ( ph /\ y e. RR /\ ( X < y /\ ( X (,) y ) C_ dom ( RR _D F ) ) ) -> X e. RR )
310 simp3l 
 |-  ( ( ph /\ y e. RR /\ ( X < y /\ ( X (,) y ) C_ dom ( RR _D F ) ) ) -> X < y )
311 125 308 309 310 lptioo1cn 
 |-  ( ( ph /\ y e. RR /\ ( X < y /\ ( X (,) y ) C_ dom ( RR _D F ) ) ) -> X e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( X (,) y ) ) )
312 307 311 sseldd 
 |-  ( ( ph /\ y e. RR /\ ( X < y /\ ( X (,) y ) C_ dom ( RR _D F ) ) ) -> X e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( ( X (,) +oo ) i^i dom ( RR _D F ) ) ) )
313 312 rexlimdv3a 
 |-  ( ph -> ( E. y e. RR ( X < y /\ ( X (,) y ) C_ dom ( RR _D F ) ) -> X e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( ( X (,) +oo ) i^i dom ( RR _D F ) ) ) ) )
314 297 313 mpd 
 |-  ( ph -> X e. ( ( limPt ` ( TopOpen ` CCfld ) ) ` ( ( X (,) +oo ) i^i dom ( RR _D F ) ) ) )
315 biid 
 |-  ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ w e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ZZ ) /\ w = ( X + ( k x. T ) ) ) <-> ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ w e. ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) /\ k e. ZZ ) /\ w = ( X + ( k x. T ) ) ) )
316 69 70 160 7 78 8 9 156 247 275 10 163 4 279 283 315 fourierdlem48 
 |-  ( ph -> ( ( ( RR _D F ) |` ( X (,) +oo ) ) limCC X ) =/= (/) )
317 292 296 314 316 125 ellimciota 
 |-  ( ph -> ( iota x x e. ( ( ( RR _D F ) |` ( X (,) +oo ) ) limCC X ) ) e. ( ( ( RR _D F ) |` ( X (,) +oo ) ) limCC X ) )
318 fveq2 
 |-  ( n = k -> ( A ` n ) = ( A ` k ) )
319 fvoveq1 
 |-  ( n = k -> ( cos ` ( n x. X ) ) = ( cos ` ( k x. X ) ) )
320 318 319 oveq12d 
 |-  ( n = k -> ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) = ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) )
321 fveq2 
 |-  ( n = k -> ( B ` n ) = ( B ` k ) )
322 fvoveq1 
 |-  ( n = k -> ( sin ` ( n x. X ) ) = ( sin ` ( k x. X ) ) )
323 321 322 oveq12d 
 |-  ( n = k -> ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) = ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) )
324 320 323 oveq12d 
 |-  ( n = k -> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) = ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
325 324 cbvsumv 
 |-  sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) = sum_ k e. ( 1 ... m ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) )
326 oveq2 
 |-  ( j = m -> ( 1 ... j ) = ( 1 ... m ) )
327 326 eqcomd 
 |-  ( j = m -> ( 1 ... m ) = ( 1 ... j ) )
328 327 sumeq1d 
 |-  ( j = m -> sum_ k e. ( 1 ... m ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) = sum_ k e. ( 1 ... j ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
329 325 328 eqtr2id 
 |-  ( j = m -> sum_ k e. ( 1 ... j ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) = sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
330 329 oveq2d 
 |-  ( j = m -> ( ( ( A ` 0 ) / 2 ) + sum_ k e. ( 1 ... j ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) = ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) )
331 330 cbvmptv 
 |-  ( j e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ k e. ( 1 ... j ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) ) = ( 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 ) ) ) ) ) )
332 1 fdmd 
 |-  ( ph -> dom F = RR )
333 332 eqimssd 
 |-  ( ph -> dom F C_ RR )
334 1 ffdmd 
 |-  ( ph -> F : dom F --> RR )
335 333 sselda 
 |-  ( ( ph /\ t e. dom F ) -> t e. RR )
336 335 adantr 
 |-  ( ( ( ph /\ t e. dom F ) /\ k e. ZZ ) -> t e. RR )
337 168 adantl 
 |-  ( ( ( ph /\ t e. dom F ) /\ k e. ZZ ) -> k e. RR )
338 173 adantlr 
 |-  ( ( ( ph /\ t e. dom F ) /\ k e. ZZ ) -> T e. RR )
339 337 338 remulcld 
 |-  ( ( ( ph /\ t e. dom F ) /\ k e. ZZ ) -> ( k x. T ) e. RR )
340 336 339 readdcld 
 |-  ( ( ( ph /\ t e. dom F ) /\ k e. ZZ ) -> ( t + ( k x. T ) ) e. RR )
341 332 eqcomd 
 |-  ( ph -> RR = dom F )
342 341 ad2antrr 
 |-  ( ( ( ph /\ t e. dom F ) /\ k e. ZZ ) -> RR = dom F )
343 340 342 eleqtrd 
 |-  ( ( ( ph /\ t e. dom F ) /\ k e. ZZ ) -> ( t + ( k x. T ) ) e. dom F )
344 id 
 |-  ( ( ph /\ k e. ZZ ) -> ( ph /\ k e. ZZ ) )
345 344 adantlr 
 |-  ( ( ( ph /\ t e. dom F ) /\ k e. ZZ ) -> ( ph /\ k e. ZZ ) )
346 345 336 180 syl2anc 
 |-  ( ( ( ph /\ t e. dom F ) /\ k e. ZZ ) -> ( F ` ( t + ( k x. T ) ) ) = ( F ` t ) )
347 333 334 69 70 160 78 8 84 161 91 139 216 218 343 346 189 190 fourierdlem71 
 |-  ( ph -> E. u e. RR A. t e. dom F ( abs ` ( F ` t ) ) <_ u )
348 332 raleqdv 
 |-  ( ph -> ( A. t e. dom F ( abs ` ( F ` t ) ) <_ u <-> A. t e. RR ( abs ` ( F ` t ) ) <_ u ) )
349 348 rexbidv 
 |-  ( ph -> ( E. u e. RR A. t e. dom F ( abs ` ( F ` t ) ) <_ u <-> E. u e. RR A. t e. RR ( abs ` ( F ` t ) ) <_ u ) )
350 347 349 mpbid 
 |-  ( ph -> E. u e. RR A. t e. RR ( abs ` ( F ` t ) ) <_ u )
351 1 36 7 8 9 43 66 4 112 2 3 139 216 218 10 285 317 5 6 13 14 331 15 350 191 4 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 ) ) )