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