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 syl5eq
 |-  ( 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 133 tgioo2
 |-  ( 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 ffvelrnd
 |-  ( ( 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 ffvelrnd
 |-  ( ( 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 ) ) )