Metamath Proof Explorer

Theorem fourierdlem112

Description: Here abbreviations (local definitions) are introduced to prove the fourier theorem. ( Zm ) is the m_th partial sum of the fourier series. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem112.f 
|- ( ph -> F : RR --> RR )
fourierdlem112.d 
|- D = ( m e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
fourierdlem112.p 
|- P = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` n ) = _pi ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem112.m 
|- ( ph -> M e. NN )
fourierdlem112.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem112.n 
|- N = ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 )
fourierdlem112.v 
|- V = ( iota f f Isom < , < ( ( 0 ... N ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) )
fourierdlem112.x 
|- ( ph -> X e. RR )
fourierdlem112.xran 
|- ( ph -> X e. ran V )
fourierdlem112.t 
|- T = ( 2 x. _pi )
fourierdlem112.fper 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem112.fcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem112.c 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> C e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
fourierdlem112.u 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> U e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
fourierdlem112.fdvcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem112.e 
|- ( ph -> E e. ( ( ( RR _D F ) |` ( -oo (,) X ) ) limCC X ) )
fourierdlem112.i 
|- ( ph -> I e. ( ( ( RR _D F ) |` ( X (,) +oo ) ) limCC X ) )
fourierdlem112.l 
|- ( ph -> L e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
fourierdlem112.r 
|- ( ph -> R e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
fourierdlem112.a 
|- A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
fourierdlem112.b 
|- B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
fourierdlem112.z 
|- Z = ( m e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) )
fourierdlem112.23 
|- S = ( n e. NN |-> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
fourierdlem112.fbd 
|- ( ph -> E. w e. RR A. t e. RR ( abs ` ( F ` t ) ) <_ w )
fourierdlem112.fdvbd 
|- ( ph -> E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
fourierdlem112.25 
|- ( ph -> X e. RR )
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem112.f 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem112.d 
 |-  D = ( m e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
3 fourierdlem112.p 
 |-  P = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` n ) = _pi ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
4 fourierdlem112.m 
 |-  ( ph -> M e. NN )
5 fourierdlem112.q 
 |-  ( ph -> Q e. ( P ` M ) )
6 fourierdlem112.n 
 |-  N = ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 )
7 fourierdlem112.v 
 |-  V = ( iota f f Isom < , < ( ( 0 ... N ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) )
8 fourierdlem112.x 
 |-  ( ph -> X e. RR )
9 fourierdlem112.xran 
 |-  ( ph -> X e. ran V )
10 fourierdlem112.t 
 |-  T = ( 2 x. _pi )
11 fourierdlem112.fper 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
12 fourierdlem112.fcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
13 fourierdlem112.c 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> C e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
14 fourierdlem112.u 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> U e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
15 fourierdlem112.fdvcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
16 fourierdlem112.e 
 |-  ( ph -> E e. ( ( ( RR _D F ) |` ( -oo (,) X ) ) limCC X ) )
17 fourierdlem112.i 
 |-  ( ph -> I e. ( ( ( RR _D F ) |` ( X (,) +oo ) ) limCC X ) )
18 fourierdlem112.l 
 |-  ( ph -> L e. ( ( F |` ( -oo (,) X ) ) limCC X ) )
19 fourierdlem112.r 
 |-  ( ph -> R e. ( ( F |` ( X (,) +oo ) ) limCC X ) )
20 fourierdlem112.a 
 |-  A = ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
21 fourierdlem112.b 
 |-  B = ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) )
22 fourierdlem112.z 
 |-  Z = ( m e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) )
23 fourierdlem112.23 
 |-  S = ( n e. NN |-> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
24 fourierdlem112.fbd 
 |-  ( ph -> E. w e. RR A. t e. RR ( abs ` ( F ` t ) ) <_ w )
25 fourierdlem112.fdvbd 
 |-  ( ph -> E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
26 fourierdlem112.25 
 |-  ( ph -> X e. RR )
27 fveq2 
 |-  ( n = j -> ( A ` n ) = ( A ` j ) )
28 oveq1 
 |-  ( n = j -> ( n x. X ) = ( j x. X ) )
29 28 fveq2d 
 |-  ( n = j -> ( cos ` ( n x. X ) ) = ( cos ` ( j x. X ) ) )
30 27 29 oveq12d 
 |-  ( n = j -> ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) = ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) )
31 fveq2 
 |-  ( n = j -> ( B ` n ) = ( B ` j ) )
32 28 fveq2d 
 |-  ( n = j -> ( sin ` ( n x. X ) ) = ( sin ` ( j x. X ) ) )
33 31 32 oveq12d 
 |-  ( n = j -> ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) = ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) )
34 30 33 oveq12d 
 |-  ( n = j -> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) = ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) )
35 34 cbvmptv 
 |-  ( n e. NN |-> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) )
36 23 35 eqtri 
 |-  S = ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) )
37 seqeq3 
 |-  ( S = ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) -> seq 1 ( + , S ) = seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) )
38 36 37 mp1i 
 |-  ( ph -> seq 1 ( + , S ) = seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) )
39 nnuz 
 |-  NN = ( ZZ>= ` 1 )
40 1zzd 
 |-  ( ph -> 1 e. ZZ )
41 nfv 
 |-  F/ n ph
42 nfcv 
 |-  F/_ n NN
43 nfcv 
 |-  F/_ n ( -u _pi (,) 0 )
44 nfcv 
 |-  F/_ n ( F ` ( X + s ) )
45 nfcv 
 |-  F/_ n x.
46 nfcv 
 |-  F/_ n ( ( D ` m ) ` s )
47 44 45 46 nfov 
 |-  F/_ n ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) )
48 43 47 nfitg 
 |-  F/_ n S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s
49 42 48 nfmpt 
 |-  F/_ n ( m e. NN |-> S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s )
50 nfcv 
 |-  F/_ n ( 0 (,) _pi )
51 50 47 nfitg 
 |-  F/_ n S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s
52 42 51 nfmpt 
 |-  F/_ n ( m e. NN |-> S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s )
53 nfmpt1 
 |-  F/_ n ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) )
54 20 53 nfcxfr 
 |-  F/_ n A
55 nfcv 
 |-  F/_ n 0
56 54 55 nffv 
 |-  F/_ n ( A ` 0 )
57 nfcv 
 |-  F/_ n /
58 nfcv 
 |-  F/_ n 2
59 56 57 58 nfov 
 |-  F/_ n ( ( A ` 0 ) / 2 )
60 nfcv 
 |-  F/_ n +
61 nfcv 
 |-  F/_ n ( 1 ... m )
62 61 nfsum1 
 |-  F/_ n sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) )
63 59 60 62 nfov 
 |-  F/_ n ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
64 42 63 nfmpt 
 |-  F/_ n ( m e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) )
65 22 64 nfcxfr 
 |-  F/_ n Z
66 eqid 
 |-  ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` n ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` n ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
67 picn 
 |-  _pi e. CC
68 67 2timesi 
 |-  ( 2 x. _pi ) = ( _pi + _pi )
69 67 67 subnegi 
 |-  ( _pi - -u _pi ) = ( _pi + _pi )
70 68 10 69 3eqtr4i 
 |-  T = ( _pi - -u _pi )
71 pire 
 |-  _pi e. RR
72 71 a1i 
 |-  ( ph -> _pi e. RR )
73 72 renegcld 
 |-  ( ph -> -u _pi e. RR )
74 73 26 readdcld 
 |-  ( ph -> ( -u _pi + X ) e. RR )
75 72 26 readdcld 
 |-  ( ph -> ( _pi + X ) e. RR )
76 negpilt0 
 |-  -u _pi < 0
77 pipos 
 |-  0 < _pi
78 71 renegcli 
 |-  -u _pi e. RR
79 0re 
 |-  0 e. RR
80 78 79 71 lttri 
 |-  ( ( -u _pi < 0 /\ 0 < _pi ) -> -u _pi < _pi )
81 76 77 80 mp2an 
 |-  -u _pi < _pi
82 81 a1i 
 |-  ( ph -> -u _pi < _pi )
83 73 72 26 82 ltadd1dd 
 |-  ( ph -> ( -u _pi + X ) < ( _pi + X ) )
84 oveq1 
 |-  ( y = x -> ( y + ( k x. T ) ) = ( x + ( k x. T ) ) )
85 84 eleq1d 
 |-  ( y = x -> ( ( y + ( k x. T ) ) e. ran Q <-> ( x + ( k x. T ) ) e. ran Q ) )
86 85 rexbidv 
 |-  ( y = x -> ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( x + ( k x. T ) ) e. ran Q ) )
87 86 cbvrabv 
 |-  { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { x e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q }
88 87 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. { x e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
89 70 3 4 5 74 75 83 66 88 6 7 fourierdlem54 
 |-  ( ph -> ( ( N e. NN /\ V e. ( ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` n ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) ` N ) ) /\ V Isom < , < ( ( 0 ... N ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) )
90 89 simpld 
 |-  ( ph -> ( N e. NN /\ V e. ( ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` n ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) ` N ) ) )
91 90 simpld 
 |-  ( ph -> N e. NN )
92 90 simprd 
 |-  ( ph -> V e. ( ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` n ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) ` N ) )
93 1 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> F : RR --> RR )
94 fveq2 
 |-  ( i = j -> ( p ` i ) = ( p ` j ) )
95 oveq1 
 |-  ( i = j -> ( i + 1 ) = ( j + 1 ) )
96 95 fveq2d 
 |-  ( i = j -> ( p ` ( i + 1 ) ) = ( p ` ( j + 1 ) ) )
97 94 96 breq12d 
 |-  ( i = j -> ( ( p ` i ) < ( p ` ( i + 1 ) ) <-> ( p ` j ) < ( p ` ( j + 1 ) ) ) )
98 97 cbvralvw 
 |-  ( A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) <-> A. j e. ( 0 ..^ n ) ( p ` j ) < ( p ` ( j + 1 ) ) )
99 98 anbi2i 
 |-  ( ( ( ( p ` 0 ) = -u _pi /\ ( p ` n ) = _pi ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) <-> ( ( ( p ` 0 ) = -u _pi /\ ( p ` n ) = _pi ) /\ A. j e. ( 0 ..^ n ) ( p ` j ) < ( p ` ( j + 1 ) ) ) )
100 99 a1i 
 |-  ( p e. ( RR ^m ( 0 ... n ) ) -> ( ( ( ( p ` 0 ) = -u _pi /\ ( p ` n ) = _pi ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) <-> ( ( ( p ` 0 ) = -u _pi /\ ( p ` n ) = _pi ) /\ A. j e. ( 0 ..^ n ) ( p ` j ) < ( p ` ( j + 1 ) ) ) ) )
101 100 rabbiia 
 |-  { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` n ) = _pi ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } = { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` n ) = _pi ) /\ A. j e. ( 0 ..^ n ) ( p ` j ) < ( p ` ( j + 1 ) ) ) }
102 101 mpteq2i 
 |-  ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` n ) = _pi ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` n ) = _pi ) /\ A. j e. ( 0 ..^ n ) ( p ` j ) < ( p ` ( j + 1 ) ) ) } )
103 3 102 eqtri 
 |-  P = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` n ) = _pi ) /\ A. j e. ( 0 ..^ n ) ( p ` j ) < ( p ` ( j + 1 ) ) ) } )
104 4 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> M e. NN )
105 5 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> Q e. ( P ` M ) )
106 11 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
107 eleq1w 
 |-  ( i = j -> ( i e. ( 0 ..^ M ) <-> j e. ( 0 ..^ M ) ) )
108 107 anbi2d 
 |-  ( i = j -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ j e. ( 0 ..^ M ) ) ) )
109 fveq2 
 |-  ( i = j -> ( Q ` i ) = ( Q ` j ) )
110 95 fveq2d 
 |-  ( i = j -> ( Q ` ( i + 1 ) ) = ( Q ` ( j + 1 ) ) )
111 109 110 oveq12d 
 |-  ( i = j -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) = ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) )
112 111 reseq2d 
 |-  ( i = j -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) )
113 111 oveq1d 
 |-  ( i = j -> ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) = ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) )
114 112 113 eleq12d 
 |-  ( i = j -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) <-> ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) ) )
115 108 114 imbi12d 
 |-  ( i = j -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) ) <-> ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) ) ) )
116 115 12 chvarvv 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) )
117 116 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) )
118 74 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( -u _pi + X ) e. RR )
119 74 rexrd 
 |-  ( ph -> ( -u _pi + X ) e. RR* )
120 pnfxr 
 |-  +oo e. RR*
121 120 a1i 
 |-  ( ph -> +oo e. RR* )
122 75 ltpnfd 
 |-  ( ph -> ( _pi + X ) < +oo )
123 119 121 75 83 122 eliood 
 |-  ( ph -> ( _pi + X ) e. ( ( -u _pi + X ) (,) +oo ) )
124 123 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( _pi + X ) e. ( ( -u _pi + X ) (,) +oo ) )
125 id 
 |-  ( i e. ( 0 ..^ N ) -> i e. ( 0 ..^ N ) )
126 6 oveq2i 
 |-  ( 0 ..^ N ) = ( 0 ..^ ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) )
127 125 126 eleqtrdi 
 |-  ( i e. ( 0 ..^ N ) -> i e. ( 0 ..^ ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) )
128 127 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> i e. ( 0 ..^ ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) )
129 6 oveq2i 
 |-  ( 0 ... N ) = ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) )
130 isoeq4 
 |-  ( ( 0 ... N ) = ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) -> ( f Isom < , < ( ( 0 ... N ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) )
131 129 130 ax-mp 
 |-  ( f Isom < , < ( ( 0 ... N ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) )
132 131 iotabii 
 |-  ( iota f f Isom < , < ( ( 0 ... N ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) )
133 7 132 eqtri 
 |-  V = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) )
134 93 103 70 104 105 106 117 118 124 128 133 fourierdlem98 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
135 24 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> E. w e. RR A. t e. RR ( abs ` ( F ` t ) ) <_ w )
136 nfra1 
 |-  F/ t A. t e. RR ( abs ` ( F ` t ) ) <_ w
137 elioore 
 |-  ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> t e. RR )
138 rspa 
 |-  ( ( A. t e. RR ( abs ` ( F ` t ) ) <_ w /\ t e. RR ) -> ( abs ` ( F ` t ) ) <_ w )
139 137 138 sylan2 
 |-  ( ( A. t e. RR ( abs ` ( F ` t ) ) <_ w /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( F ` t ) ) <_ w )
140 139 ex 
 |-  ( A. t e. RR ( abs ` ( F ` t ) ) <_ w -> ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( abs ` ( F ` t ) ) <_ w ) )
141 136 140 ralrimi 
 |-  ( A. t e. RR ( abs ` ( F ` t ) ) <_ w -> A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( F ` t ) ) <_ w )
142 141 reximi 
 |-  ( E. w e. RR A. t e. RR ( abs ` ( F ` t ) ) <_ w -> E. w e. RR A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( F ` t ) ) <_ w )
143 135 142 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> E. w e. RR A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( F ` t ) ) <_ w )
144 ssid 
 |-  RR C_ RR
145 dvfre 
 |-  ( ( F : RR --> RR /\ RR C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
146 1 144 145 sylancl 
 |-  ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
147 146 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
148 eqid 
 |-  ( RR _D F ) = ( RR _D F )
149 71 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> _pi e. RR )
150 78 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> -u _pi e. RR )
151 111 reseq2d 
 |-  ( i = j -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( RR _D F ) |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) )
152 151 113 eleq12d 
 |-  ( i = j -> ( ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) <-> ( ( RR _D F ) |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) ) )
153 108 152 imbi12d 
 |-  ( i = j -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) ) <-> ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) ) ) )
154 153 15 chvarvv 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) )
155 154 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 0 ..^ M ) ) -> ( ( RR _D F ) |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) e. ( ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) -cn-> CC ) )
156 73 8 readdcld 
 |-  ( ph -> ( -u _pi + X ) e. RR )
157 156 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( -u _pi + X ) e. RR )
158 156 rexrd 
 |-  ( ph -> ( -u _pi + X ) e. RR* )
159 72 8 readdcld 
 |-  ( ph -> ( _pi + X ) e. RR )
160 73 72 8 82 ltadd1dd 
 |-  ( ph -> ( -u _pi + X ) < ( _pi + X ) )
161 159 ltpnfd 
 |-  ( ph -> ( _pi + X ) < +oo )
162 158 121 159 160 161 eliood 
 |-  ( ph -> ( _pi + X ) e. ( ( -u _pi + X ) (,) +oo ) )
163 162 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( _pi + X ) e. ( ( -u _pi + X ) (,) +oo ) )
164 oveq1 
 |-  ( k = h -> ( k x. T ) = ( h x. T ) )
165 164 oveq2d 
 |-  ( k = h -> ( y + ( k x. T ) ) = ( y + ( h x. T ) ) )
166 165 eleq1d 
 |-  ( k = h -> ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( h x. T ) ) e. ran Q ) )
167 166 cbvrexvw 
 |-  ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. h e. ZZ ( y + ( h x. T ) ) e. ran Q )
168 167 rgenw 
 |-  A. y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. h e. ZZ ( y + ( h x. T ) ) e. ran Q )
169 rabbi 
 |-  ( A. y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. h e. ZZ ( y + ( h x. T ) ) e. ran Q ) <-> { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } )
170 168 169 mpbi 
 |-  { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q }
171 170 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. h e. ZZ ( y + ( h x. T ) ) e. ran Q } )
172 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. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) -> ( f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) ) )
173 171 172 ax-mp 
 |-  ( f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )
174 173 iotabii 
 |-  ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) ) = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )
175 133 174 eqtri 
 |-  V = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( -u _pi + X ) , ( _pi + X ) } u. { y e. ( ( -u _pi + X ) [,] ( _pi + X ) ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )
176 eleq1w 
 |-  ( v = u -> ( v e. dom ( RR _D F ) <-> u e. dom ( RR _D F ) ) )
177 fveq2 
 |-  ( v = u -> ( ( RR _D F ) ` v ) = ( ( RR _D F ) ` u ) )
178 176 177 ifbieq1d 
 |-  ( v = u -> if ( v e. dom ( RR _D F ) , ( ( RR _D F ) ` v ) , 0 ) = if ( u e. dom ( RR _D F ) , ( ( RR _D F ) ` u ) , 0 ) )
179 178 cbvmptv 
 |-  ( v e. RR |-> if ( v e. dom ( RR _D F ) , ( ( RR _D F ) ` v ) , 0 ) ) = ( u e. RR |-> if ( u e. dom ( RR _D F ) , ( ( RR _D F ) ` u ) , 0 ) )
180 93 148 103 149 150 70 104 105 106 155 157 163 128 175 179 fourierdlem97 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
181 cncff 
 |-  ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> CC )
182 fdm 
 |-  ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> CC -> dom ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) = ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
183 180 181 182 3syl 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> dom ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) = ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
184 ssdmres 
 |-  ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ dom ( RR _D F ) <-> dom ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) = ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
185 183 184 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ dom ( RR _D F ) )
186 147 185 fssresd 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR )
187 ax-resscn 
 |-  RR C_ CC
188 187 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> RR C_ CC )
189 cncffvrn 
 |-  ( ( RR C_ CC /\ ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) ) -> ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> RR ) <-> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR ) )
190 188 180 189 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> RR ) <-> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) : ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) --> RR ) )
191 186 190 mpbird 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> RR ) )
192 25 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
193 nfv 
 |-  F/ t ( ph /\ i e. ( 0 ..^ N ) )
194 nfra1 
 |-  F/ t A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z
195 193 194 nfan 
 |-  F/ t ( ( ph /\ i e. ( 0 ..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
196 fvres 
 |-  ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) = ( ( RR _D F ) ` t ) )
197 196 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) = ( ( RR _D F ) ` t ) )
198 197 fveq2d 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) = ( abs ` ( ( RR _D F ) ` t ) ) )
199 198 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) = ( abs ` ( ( RR _D F ) ` t ) ) )
200 simplr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
201 185 sselda 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> t e. dom ( RR _D F ) )
202 201 adantlr 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> t e. dom ( RR _D F ) )
203 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 )
204 200 202 203 syl2anc 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
205 199 204 eqbrtrd 
 |-  ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z )
206 205 ex 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) -> ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z ) )
207 195 206 ralrimi 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) -> A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z )
208 207 ex 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z -> A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z ) )
209 208 reximdv 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( E. z e. RR A. t e. dom ( RR _D F ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z -> E. z e. RR A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z ) )
210 192 209 mpd 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> E. z e. RR A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z )
211 nfra1 
 |-  F/ t A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z
212 196 eqcomd 
 |-  ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( ( RR _D F ) ` t ) = ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) )
213 212 fveq2d 
 |-  ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) = ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) )
214 213 adantl 
 |-  ( ( A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) = ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) )
215 rspa 
 |-  ( ( A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z )
216 214 215 eqbrtrd 
 |-  ( ( A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z /\ t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
217 216 ex 
 |-  ( A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z -> ( t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) )
218 211 217 ralrimi 
 |-  ( A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z -> A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
219 218 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z -> A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) )
220 219 reximdv 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( E. z e. RR A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( ( RR _D F ) |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` t ) ) <_ z -> E. z e. RR A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z ) )
221 210 220 mpd 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> E. z e. RR A. t e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ( abs ` ( ( RR _D F ) ` t ) ) <_ z )
222 nfv 
 |-  F/ i ( ph /\ j e. ( 0 ..^ M ) )
223 nfcsb1v 
 |-  F/_ i [_ j / i ]_ C
224 223 nfel1 
 |-  F/ i [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) limCC ( Q ` j ) )
225 222 224 nfim 
 |-  F/ i ( ( ph /\ j e. ( 0 ..^ M ) ) -> [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) limCC ( Q ` j ) ) )
226 csbeq1a 
 |-  ( i = j -> C = [_ j / i ]_ C )
227 112 109 oveq12d 
 |-  ( i = j -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) = ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) limCC ( Q ` j ) ) )
228 226 227 eleq12d 
 |-  ( i = j -> ( C e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) <-> [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) limCC ( Q ` j ) ) ) )
229 108 228 imbi12d 
 |-  ( i = j -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> C e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) ) <-> ( ( ph /\ j e. ( 0 ..^ M ) ) -> [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) limCC ( Q ` j ) ) ) ) )
230 225 229 13 chvarfv 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) limCC ( Q ` j ) ) )
231 230 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 0 ..^ M ) ) -> [_ j / i ]_ C e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) limCC ( Q ` j ) ) )
232 93 103 70 104 105 106 117 231 118 124 128 133 fourierdlem96 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> if ( ( ( d e. ( -u _pi (,] _pi ) |-> if ( d = _pi , -u _pi , d ) ) ` ( ( c e. RR |-> ( c + ( ( |_ ` ( ( _pi - c ) / T ) ) x. T ) ) ) ` ( V ` i ) ) ) = ( Q ` ( ( y e. RR |-> sup ( { f e. ( 0 ..^ M ) | ( Q ` f ) <_ ( ( d e. ( -u _pi (,] _pi ) |-> if ( d = _pi , -u _pi , d ) ) ` ( ( c e. RR |-> ( c + ( ( |_ ` ( ( _pi - c ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` i ) ) ) , ( ( j e. ( 0 ..^ M ) |-> [_ j / i ]_ C ) ` ( ( y e. RR |-> sup ( { f e. ( 0 ..^ M ) | ( Q ` f ) <_ ( ( d e. ( -u _pi (,] _pi ) |-> if ( d = _pi , -u _pi , d ) ) ` ( ( c e. RR |-> ( c + ( ( |_ ` ( ( _pi - c ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` i ) ) ) , ( F ` ( ( d e. ( -u _pi (,] _pi ) |-> if ( d = _pi , -u _pi , d ) ) ` ( ( c e. RR |-> ( c + ( ( |_ ` ( ( _pi - c ) / T ) ) x. T ) ) ) ` ( V ` i ) ) ) ) ) e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` i ) ) )
233 nfcsb1v 
 |-  F/_ i [_ j / i ]_ U
234 233 nfel1 
 |-  F/ i [_ j / i ]_ U e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) limCC ( Q ` ( j + 1 ) ) )
235 222 234 nfim 
 |-  F/ i ( ( ph /\ j e. ( 0 ..^ M ) ) -> [_ j / i ]_ U e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) limCC ( Q ` ( j + 1 ) ) ) )
236 csbeq1a 
 |-  ( i = j -> U = [_ j / i ]_ U )
237 112 110 oveq12d 
 |-  ( i = j -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) limCC ( Q ` ( j + 1 ) ) ) )
238 236 237 eleq12d 
 |-  ( i = j -> ( U e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) <-> [_ j / i ]_ U e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) limCC ( Q ` ( j + 1 ) ) ) ) )
239 108 238 imbi12d 
 |-  ( i = j -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> U e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) ) <-> ( ( ph /\ j e. ( 0 ..^ M ) ) -> [_ j / i ]_ U e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) limCC ( Q ` ( j + 1 ) ) ) ) ) )
240 235 239 14 chvarfv 
 |-  ( ( ph /\ j e. ( 0 ..^ M ) ) -> [_ j / i ]_ U e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) limCC ( Q ` ( j + 1 ) ) ) )
241 240 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 0 ..^ M ) ) -> [_ j / i ]_ U e. ( ( F |` ( ( Q ` j ) (,) ( Q ` ( j + 1 ) ) ) ) limCC ( Q ` ( j + 1 ) ) ) )
242 93 103 70 104 105 106 117 241 157 163 128 133 fourierdlem99 
 |-  ( ( ph /\ i e. ( 0 ..^ N ) ) -> if ( ( ( e e. RR |-> ( e + ( ( |_ ` ( ( _pi - e ) / T ) ) x. T ) ) ) ` ( V ` ( i + 1 ) ) ) = ( Q ` ( ( ( y e. RR |-> sup ( { h e. ( 0 ..^ M ) | ( Q ` h ) <_ ( ( g e. ( -u _pi (,] _pi ) |-> if ( g = _pi , -u _pi , g ) ) ` ( ( e e. RR |-> ( e + ( ( |_ ` ( ( _pi - e ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` i ) ) + 1 ) ) , ( ( j e. ( 0 ..^ M ) |-> [_ j / i ]_ U ) ` ( ( y e. RR |-> sup ( { h e. ( 0 ..^ M ) | ( Q ` h ) <_ ( ( g e. ( -u _pi (,] _pi ) |-> if ( g = _pi , -u _pi , g ) ) ` ( ( e e. RR |-> ( e + ( ( |_ ` ( ( _pi - e ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` i ) ) ) , ( F ` ( ( e e. RR |-> ( e + ( ( |_ ` ( ( _pi - e ) / T ) ) x. T ) ) ) ` ( V ` ( i + 1 ) ) ) ) ) e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` ( i + 1 ) ) ) )
243 eqeq1 
 |-  ( g = s -> ( g = 0 <-> s = 0 ) )
244 oveq2 
 |-  ( g = s -> ( X + g ) = ( X + s ) )
245 244 fveq2d 
 |-  ( g = s -> ( F ` ( X + g ) ) = ( F ` ( X + s ) ) )
246 breq2 
 |-  ( g = s -> ( 0 < g <-> 0 < s ) )
247 246 ifbid 
 |-  ( g = s -> if ( 0 < g , R , L ) = if ( 0 < s , R , L ) )
248 245 247 oveq12d 
 |-  ( g = s -> ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) = ( ( F ` ( X + s ) ) - if ( 0 < s , R , L ) ) )
249 id 
 |-  ( g = s -> g = s )
250 248 249 oveq12d 
 |-  ( g = s -> ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) = ( ( ( F ` ( X + s ) ) - if ( 0 < s , R , L ) ) / s ) )
251 243 250 ifbieq2d 
 |-  ( g = s -> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) = if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , R , L ) ) / s ) ) )
252 251 cbvmptv 
 |-  ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 0 , ( ( ( F ` ( X + s ) ) - if ( 0 < s , R , L ) ) / s ) ) )
253 eqeq1 
 |-  ( o = s -> ( o = 0 <-> s = 0 ) )
254 id 
 |-  ( o = s -> o = s )
255 oveq1 
 |-  ( o = s -> ( o / 2 ) = ( s / 2 ) )
256 255 fveq2d 
 |-  ( o = s -> ( sin ` ( o / 2 ) ) = ( sin ` ( s / 2 ) ) )
257 256 oveq2d 
 |-  ( o = s -> ( 2 x. ( sin ` ( o / 2 ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
258 254 257 oveq12d 
 |-  ( o = s -> ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
259 253 258 ifbieq2d 
 |-  ( o = s -> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) = if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
260 259 cbvmptv 
 |-  ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
261 fveq2 
 |-  ( r = s -> ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) = ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` s ) )
262 fveq2 
 |-  ( r = s -> ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) = ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` s ) )
263 261 262 oveq12d 
 |-  ( r = s -> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) = ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` s ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` s ) ) )
264 263 cbvmptv 
 |-  ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) = ( s e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` s ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` s ) ) )
265 oveq2 
 |-  ( d = s -> ( ( k + ( 1 / 2 ) ) x. d ) = ( ( k + ( 1 / 2 ) ) x. s ) )
266 265 fveq2d 
 |-  ( d = s -> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) = ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) )
267 266 cbvmptv 
 |-  ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) = ( s e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) )
268 fveq2 
 |-  ( z = s -> ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) = ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) )
269 fveq2 
 |-  ( z = s -> ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) = ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` s ) )
270 268 269 oveq12d 
 |-  ( z = s -> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) = ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` s ) ) )
271 270 cbvmptv 
 |-  ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) = ( s e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` s ) ) )
272 fveq2 
 |-  ( m = n -> ( D ` m ) = ( D ` n ) )
273 272 fveq1d 
 |-  ( m = n -> ( ( D ` m ) ` s ) = ( ( D ` n ) ` s ) )
274 273 oveq2d 
 |-  ( m = n -> ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
275 274 adantr 
 |-  ( ( m = n /\ s e. ( -u _pi (,) 0 ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
276 275 itgeq2dv 
 |-  ( m = n -> S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s = S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
277 276 cbvmptv 
 |-  ( m e. NN |-> S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) = ( n e. NN |-> S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
278 oveq1 
 |-  ( c = k -> ( c + ( 1 / 2 ) ) = ( k + ( 1 / 2 ) ) )
279 278 oveq1d 
 |-  ( c = k -> ( ( c + ( 1 / 2 ) ) x. d ) = ( ( k + ( 1 / 2 ) ) x. d ) )
280 279 fveq2d 
 |-  ( c = k -> ( sin ` ( ( c + ( 1 / 2 ) ) x. d ) ) = ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) )
281 280 mpteq2dv 
 |-  ( c = k -> ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( c + ( 1 / 2 ) ) x. d ) ) ) = ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) )
282 281 fveq1d 
 |-  ( c = k -> ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( c + ( 1 / 2 ) ) x. d ) ) ) ` z ) = ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) )
283 282 oveq2d 
 |-  ( c = k -> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( c + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) = ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) )
284 283 mpteq2dv 
 |-  ( c = k -> ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( c + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) = ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) )
285 284 fveq1d 
 |-  ( c = k -> ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( c + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) = ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) )
286 285 adantr 
 |-  ( ( c = k /\ s e. ( -u _pi (,) 0 ) ) -> ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( c + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) = ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) )
287 286 itgeq2dv 
 |-  ( c = k -> S. ( -u _pi (,) 0 ) ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( c + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) _d s = S. ( -u _pi (,) 0 ) ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) _d s )
288 287 oveq1d 
 |-  ( c = k -> ( S. ( -u _pi (,) 0 ) ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( c + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) _d s / _pi ) = ( S. ( -u _pi (,) 0 ) ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) _d s / _pi ) )
289 288 cbvmptv 
 |-  ( c e. NN |-> ( S. ( -u _pi (,) 0 ) ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( c + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) _d s / _pi ) ) = ( k e. NN |-> ( S. ( -u _pi (,) 0 ) ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) _d s / _pi ) )
290 oveq1 
 |-  ( y = s -> ( y mod ( 2 x. _pi ) ) = ( s mod ( 2 x. _pi ) ) )
291 290 eqeq1d 
 |-  ( y = s -> ( ( y mod ( 2 x. _pi ) ) = 0 <-> ( s mod ( 2 x. _pi ) ) = 0 ) )
292 oveq2 
 |-  ( y = s -> ( ( m + ( 1 / 2 ) ) x. y ) = ( ( m + ( 1 / 2 ) ) x. s ) )
293 292 fveq2d 
 |-  ( y = s -> ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) = ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) )
294 oveq1 
 |-  ( y = s -> ( y / 2 ) = ( s / 2 ) )
295 294 fveq2d 
 |-  ( y = s -> ( sin ` ( y / 2 ) ) = ( sin ` ( s / 2 ) ) )
296 295 oveq2d 
 |-  ( y = s -> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) )
297 293 296 oveq12d 
 |-  ( y = s -> ( ( sin ` ( ( m + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) = ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) )
298 291 297 ifbieq2d 
 |-  ( y = s -> 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 ) ) ) ) ) = if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) )
299 298 cbvmptv 
 |-  ( 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 ) ) ) ) ) ) = ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) )
300 simpl 
 |-  ( ( m = k /\ s e. RR ) -> m = k )
301 300 oveq2d 
 |-  ( ( m = k /\ s e. RR ) -> ( 2 x. m ) = ( 2 x. k ) )
302 301 oveq1d 
 |-  ( ( m = k /\ s e. RR ) -> ( ( 2 x. m ) + 1 ) = ( ( 2 x. k ) + 1 ) )
303 302 oveq1d 
 |-  ( ( m = k /\ s e. RR ) -> ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) = ( ( ( 2 x. k ) + 1 ) / ( 2 x. _pi ) ) )
304 300 oveq1d 
 |-  ( ( m = k /\ s e. RR ) -> ( m + ( 1 / 2 ) ) = ( k + ( 1 / 2 ) ) )
305 304 oveq1d 
 |-  ( ( m = k /\ s e. RR ) -> ( ( m + ( 1 / 2 ) ) x. s ) = ( ( k + ( 1 / 2 ) ) x. s ) )
306 305 fveq2d 
 |-  ( ( m = k /\ s e. RR ) -> ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) = ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) )
307 306 oveq1d 
 |-  ( ( m = k /\ s e. RR ) -> ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) = ( ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) )
308 303 307 ifeq12d 
 |-  ( ( m = k /\ s e. RR ) -> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) = if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) )
309 308 mpteq2dva 
 |-  ( m = k -> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. m ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( m + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
310 299 309 syl5eq 
 |-  ( m = k -> ( 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 ) ) ) ) ) ) = ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
311 310 cbvmptv 
 |-  ( 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 ) ) ) ) ) ) ) = ( k e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
312 2 311 eqtri 
 |-  D = ( k e. NN |-> ( s e. RR |-> if ( ( s mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. k ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( k + ( 1 / 2 ) ) x. s ) ) / ( ( 2 x. _pi ) x. ( sin ` ( s / 2 ) ) ) ) ) ) )
313 eqid 
 |-  ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) |` ( -u _pi [,] l ) ) = ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) |` ( -u _pi [,] l ) )
314 eqid 
 |-  ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) = ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) )
315 eqid 
 |-  ( ( # ` ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) - 1 ) = ( ( # ` ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) - 1 )
316 isoeq1 
 |-  ( u = w -> ( u Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) - 1 ) ) , ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) <-> w Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) - 1 ) ) , ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) ) )
317 316 cbviotavw 
 |-  ( iota u u Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) - 1 ) ) , ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) ) = ( iota w w Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) - 1 ) ) , ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) )
318 fveq2 
 |-  ( j = i -> ( V ` j ) = ( V ` i ) )
319 318 oveq1d 
 |-  ( j = i -> ( ( V ` j ) - X ) = ( ( V ` i ) - X ) )
320 319 cbvmptv 
 |-  ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) = ( i e. ( 0 ... N ) |-> ( ( V ` i ) - X ) )
321 eqid 
 |-  ( iota_ m e. ( 0 ..^ N ) ( ( ( iota u u Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) - 1 ) ) , ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) ) ` b ) (,) ( ( iota u u Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) - 1 ) ) , ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) ) ` ( b + 1 ) ) ) C_ ( ( ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) ` m ) (,) ( ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) ` ( m + 1 ) ) ) ) = ( iota_ m e. ( 0 ..^ N ) ( ( ( iota u u Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) - 1 ) ) , ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) ) ` b ) (,) ( ( iota u u Isom < , < ( ( 0 ... ( ( # ` ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) - 1 ) ) , ( { -u _pi , l } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( -u _pi (,) l ) ) ) ) ) ` ( b + 1 ) ) ) C_ ( ( ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) ` m ) (,) ( ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) ` ( m + 1 ) ) ) )
322 fveq2 
 |-  ( a = s -> ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) = ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) )
323 oveq2 
 |-  ( a = s -> ( ( b + ( 1 / 2 ) ) x. a ) = ( ( b + ( 1 / 2 ) ) x. s ) )
324 323 fveq2d 
 |-  ( a = s -> ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) = ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) )
325 322 324 oveq12d 
 |-  ( a = s -> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) = ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) )
326 325 cbvitgv 
 |-  S. ( l (,) 0 ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a = S. ( l (,) 0 ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s
327 326 fveq2i 
 |-  ( abs ` S. ( l (,) 0 ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a ) = ( abs ` S. ( l (,) 0 ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s )
328 327 breq1i 
 |-  ( ( abs ` S. ( l (,) 0 ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a ) < ( i / 2 ) <-> ( abs ` S. ( l (,) 0 ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( i / 2 ) )
329 328 anbi2i 
 |-  ( ( ( ( ( ph /\ i e. RR+ ) /\ l e. ( -u _pi (,) 0 ) ) /\ b e. NN ) /\ ( abs ` S. ( l (,) 0 ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a ) < ( i / 2 ) ) <-> ( ( ( ( ph /\ i e. RR+ ) /\ l e. ( -u _pi (,) 0 ) ) /\ b e. NN ) /\ ( abs ` S. ( l (,) 0 ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( i / 2 ) ) )
330 325 cbvitgv 
 |-  S. ( -u _pi (,) l ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a = S. ( -u _pi (,) l ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s
331 330 fveq2i 
 |-  ( abs ` S. ( -u _pi (,) l ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a ) = ( abs ` S. ( -u _pi (,) l ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s )
332 331 breq1i 
 |-  ( ( abs ` S. ( -u _pi (,) l ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a ) < ( i / 2 ) <-> ( abs ` S. ( -u _pi (,) l ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( i / 2 ) )
333 329 332 anbi12i 
 |-  ( ( ( ( ( ( ph /\ i e. RR+ ) /\ l e. ( -u _pi (,) 0 ) ) /\ b e. NN ) /\ ( abs ` S. ( l (,) 0 ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a ) < ( i / 2 ) ) /\ ( abs ` S. ( -u _pi (,) l ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a ) < ( i / 2 ) ) <-> ( ( ( ( ( ph /\ i e. RR+ ) /\ l e. ( -u _pi (,) 0 ) ) /\ b e. NN ) /\ ( abs ` S. ( l (,) 0 ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( i / 2 ) ) /\ ( abs ` S. ( -u _pi (,) l ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( i / 2 ) ) )
334 1 26 66 91 92 9 134 143 191 221 232 242 252 260 264 267 271 277 289 19 18 16 17 312 313 314 315 317 320 321 333 fourierdlem103 
 |-  ( ph -> ( m e. NN |-> S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) ~~> ( L / 2 ) )
335 nnex 
 |-  NN e. _V
336 335 mptex 
 |-  ( 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 ) ) ) ) ) ) e. _V
337 22 336 eqeltri 
 |-  Z e. _V
338 337 a1i 
 |-  ( ph -> Z e. _V )
339 274 adantr 
 |-  ( ( m = n /\ s e. ( 0 (,) _pi ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) = ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
340 339 itgeq2dv 
 |-  ( m = n -> S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s = S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
341 340 cbvmptv 
 |-  ( m e. NN |-> S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) = ( n e. NN |-> S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
342 285 adantr 
 |-  ( ( c = k /\ s e. ( 0 (,) _pi ) ) -> ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( c + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) = ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) )
343 342 itgeq2dv 
 |-  ( c = k -> S. ( 0 (,) _pi ) ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( c + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) _d s = S. ( 0 (,) _pi ) ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) _d s )
344 343 oveq1d 
 |-  ( c = k -> ( S. ( 0 (,) _pi ) ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( c + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) _d s / _pi ) = ( S. ( 0 (,) _pi ) ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) _d s / _pi ) )
345 344 cbvmptv 
 |-  ( c e. NN |-> ( S. ( 0 (,) _pi ) ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( c + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) _d s / _pi ) ) = ( k e. NN |-> ( S. ( 0 (,) _pi ) ( ( z e. ( -u _pi [,] _pi ) |-> ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` z ) x. ( ( d e. ( -u _pi [,] _pi ) |-> ( sin ` ( ( k + ( 1 / 2 ) ) x. d ) ) ) ` z ) ) ) ` s ) _d s / _pi ) )
346 eqid 
 |-  ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) |` ( e [,] _pi ) ) = ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) |` ( e [,] _pi ) )
347 eqid 
 |-  ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) = ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) )
348 eqid 
 |-  ( ( # ` ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) - 1 ) = ( ( # ` ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) - 1 )
349 isoeq1 
 |-  ( u = v -> ( u Isom < , < ( ( 0 ... ( ( # ` ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) - 1 ) ) , ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) <-> v Isom < , < ( ( 0 ... ( ( # ` ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) - 1 ) ) , ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) ) )
350 349 cbviotavw 
 |-  ( iota u u Isom < , < ( ( 0 ... ( ( # ` ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) - 1 ) ) , ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) ) = ( iota v v Isom < , < ( ( 0 ... ( ( # ` ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) - 1 ) ) , ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) )
351 eqid 
 |-  ( iota_ a e. ( 0 ..^ N ) ( ( ( iota u u Isom < , < ( ( 0 ... ( ( # ` ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) - 1 ) ) , ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) ) ` b ) (,) ( ( iota u u Isom < , < ( ( 0 ... ( ( # ` ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) - 1 ) ) , ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) ) ` ( b + 1 ) ) ) C_ ( ( ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) ` a ) (,) ( ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) ` ( a + 1 ) ) ) ) = ( iota_ a e. ( 0 ..^ N ) ( ( ( iota u u Isom < , < ( ( 0 ... ( ( # ` ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) - 1 ) ) , ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) ) ` b ) (,) ( ( iota u u Isom < , < ( ( 0 ... ( ( # ` ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) - 1 ) ) , ( { e , _pi } u. ( ran ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) i^i ( e (,) _pi ) ) ) ) ) ` ( b + 1 ) ) ) C_ ( ( ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) ` a ) (,) ( ( j e. ( 0 ... N ) |-> ( ( V ` j ) - X ) ) ` ( a + 1 ) ) ) )
352 325 cbvitgv 
 |-  S. ( 0 (,) e ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a = S. ( 0 (,) e ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s
353 352 fveq2i 
 |-  ( abs ` S. ( 0 (,) e ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a ) = ( abs ` S. ( 0 (,) e ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s )
354 353 breq1i 
 |-  ( ( abs ` S. ( 0 (,) e ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a ) < ( q / 2 ) <-> ( abs ` S. ( 0 (,) e ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( q / 2 ) )
355 354 anbi2i 
 |-  ( ( ( ( ( ph /\ q e. RR+ ) /\ e e. ( 0 (,) _pi ) ) /\ b e. NN ) /\ ( abs ` S. ( 0 (,) e ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a ) < ( q / 2 ) ) <-> ( ( ( ( ph /\ q e. RR+ ) /\ e e. ( 0 (,) _pi ) ) /\ b e. NN ) /\ ( abs ` S. ( 0 (,) e ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( q / 2 ) ) )
356 325 cbvitgv 
 |-  S. ( e (,) _pi ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a = S. ( e (,) _pi ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s
357 356 fveq2i 
 |-  ( abs ` S. ( e (,) _pi ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a ) = ( abs ` S. ( e (,) _pi ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s )
358 357 breq1i 
 |-  ( ( abs ` S. ( e (,) _pi ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a ) < ( q / 2 ) <-> ( abs ` S. ( e (,) _pi ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( q / 2 ) )
359 355 358 anbi12i 
 |-  ( ( ( ( ( ( ph /\ q e. RR+ ) /\ e e. ( 0 (,) _pi ) ) /\ b e. NN ) /\ ( abs ` S. ( 0 (,) e ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a ) < ( q / 2 ) ) /\ ( abs ` S. ( e (,) _pi ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` a ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. a ) ) ) _d a ) < ( q / 2 ) ) <-> ( ( ( ( ( ph /\ q e. RR+ ) /\ e e. ( 0 (,) _pi ) ) /\ b e. NN ) /\ ( abs ` S. ( 0 (,) e ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( q / 2 ) ) /\ ( abs ` S. ( e (,) _pi ) ( ( ( r e. ( -u _pi [,] _pi ) |-> ( ( ( g e. ( -u _pi [,] _pi ) |-> if ( g = 0 , 0 , ( ( ( F ` ( X + g ) ) - if ( 0 < g , R , L ) ) / g ) ) ) ` r ) x. ( ( o e. ( -u _pi [,] _pi ) |-> if ( o = 0 , 1 , ( o / ( 2 x. ( sin ` ( o / 2 ) ) ) ) ) ) ` r ) ) ) ` s ) x. ( sin ` ( ( b + ( 1 / 2 ) ) x. s ) ) ) _d s ) < ( q / 2 ) ) )
360 1 26 66 91 92 9 134 143 191 221 232 242 252 260 264 267 271 341 345 19 18 16 17 312 346 347 348 350 320 351 359 fourierdlem104 
 |-  ( ph -> ( m e. NN |-> S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) ~~> ( R / 2 ) )
361 eqidd 
 |-  ( ( ph /\ n e. NN ) -> ( m e. NN |-> S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) = ( m e. NN |-> S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) )
362 276 adantl 
 |-  ( ( ( ph /\ n e. NN ) /\ m = n ) -> S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s = S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
363 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
364 elioore 
 |-  ( s e. ( -u _pi (,) 0 ) -> s e. RR )
365 1 adantr 
 |-  ( ( ph /\ s e. RR ) -> F : RR --> RR )
366 26 adantr 
 |-  ( ( ph /\ s e. RR ) -> X e. RR )
367 simpr 
 |-  ( ( ph /\ s e. RR ) -> s e. RR )
368 366 367 readdcld 
 |-  ( ( ph /\ s e. RR ) -> ( X + s ) e. RR )
369 365 368 ffvelrnd 
 |-  ( ( ph /\ s e. RR ) -> ( F ` ( X + s ) ) e. RR )
370 369 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( F ` ( X + s ) ) e. RR )
371 2 dirkerre 
 |-  ( ( n e. NN /\ s e. RR ) -> ( ( D ` n ) ` s ) e. RR )
372 371 adantll 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( ( D ` n ) ` s ) e. RR )
373 370 372 remulcld 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. RR ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) e. RR )
374 364 373 sylan2 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi (,) 0 ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) e. RR )
375 ioossicc 
 |-  ( -u _pi (,) 0 ) C_ ( -u _pi [,] 0 )
376 78 leidi 
 |-  -u _pi <_ -u _pi
377 79 71 77 ltleii 
 |-  0 <_ _pi
378 iccss 
 |-  ( ( ( -u _pi e. RR /\ _pi e. RR ) /\ ( -u _pi <_ -u _pi /\ 0 <_ _pi ) ) -> ( -u _pi [,] 0 ) C_ ( -u _pi [,] _pi ) )
379 78 71 376 377 378 mp4an 
 |-  ( -u _pi [,] 0 ) C_ ( -u _pi [,] _pi )
380 375 379 sstri 
 |-  ( -u _pi (,) 0 ) C_ ( -u _pi [,] _pi )
381 380 a1i 
 |-  ( ( ph /\ n e. NN ) -> ( -u _pi (,) 0 ) C_ ( -u _pi [,] _pi ) )
382 ioombl 
 |-  ( -u _pi (,) 0 ) e. dom vol
383 382 a1i 
 |-  ( ( ph /\ n e. NN ) -> ( -u _pi (,) 0 ) e. dom vol )
384 1 adantr 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> F : RR --> RR )
385 26 adantr 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> X e. RR )
386 73 72 iccssred 
 |-  ( ph -> ( -u _pi [,] _pi ) C_ RR )
387 386 sselda 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> s e. RR )
388 385 387 readdcld 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( X + s ) e. RR )
389 384 388 ffvelrnd 
 |-  ( ( ph /\ s e. ( -u _pi [,] _pi ) ) -> ( F ` ( X + s ) ) e. RR )
390 389 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( F ` ( X + s ) ) e. RR )
391 iccssre 
 |-  ( ( -u _pi e. RR /\ _pi e. RR ) -> ( -u _pi [,] _pi ) C_ RR )
392 78 71 391 mp2an 
 |-  ( -u _pi [,] _pi ) C_ RR
393 392 sseli 
 |-  ( s e. ( -u _pi [,] _pi ) -> s e. RR )
394 393 371 sylan2 
 |-  ( ( n e. NN /\ s e. ( -u _pi [,] _pi ) ) -> ( ( D ` n ) ` s ) e. RR )
395 394 adantll 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( ( D ` n ) ` s ) e. RR )
396 390 395 remulcld 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( -u _pi [,] _pi ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) e. RR )
397 78 a1i 
 |-  ( ( ph /\ n e. NN ) -> -u _pi e. RR )
398 71 a1i 
 |-  ( ( ph /\ n e. NN ) -> _pi e. RR )
399 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> F : RR --> RR )
400 26 adantr 
 |-  ( ( ph /\ n e. NN ) -> X e. RR )
401 91 adantr 
 |-  ( ( ph /\ n e. NN ) -> N e. NN )
402 92 adantr 
 |-  ( ( ph /\ n e. NN ) -> V e. ( ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` n ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) ` N ) )
403 134 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ N ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
404 232 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ N ) ) -> if ( ( ( d e. ( -u _pi (,] _pi ) |-> if ( d = _pi , -u _pi , d ) ) ` ( ( c e. RR |-> ( c + ( ( |_ ` ( ( _pi - c ) / T ) ) x. T ) ) ) ` ( V ` i ) ) ) = ( Q ` ( ( y e. RR |-> sup ( { f e. ( 0 ..^ M ) | ( Q ` f ) <_ ( ( d e. ( -u _pi (,] _pi ) |-> if ( d = _pi , -u _pi , d ) ) ` ( ( c e. RR |-> ( c + ( ( |_ ` ( ( _pi - c ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` i ) ) ) , ( ( j e. ( 0 ..^ M ) |-> [_ j / i ]_ C ) ` ( ( y e. RR |-> sup ( { f e. ( 0 ..^ M ) | ( Q ` f ) <_ ( ( d e. ( -u _pi (,] _pi ) |-> if ( d = _pi , -u _pi , d ) ) ` ( ( c e. RR |-> ( c + ( ( |_ ` ( ( _pi - c ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` i ) ) ) , ( F ` ( ( d e. ( -u _pi (,] _pi ) |-> if ( d = _pi , -u _pi , d ) ) ` ( ( c e. RR |-> ( c + ( ( |_ ` ( ( _pi - c ) / T ) ) x. T ) ) ) ` ( V ` i ) ) ) ) ) e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` i ) ) )
405 242 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ i e. ( 0 ..^ N ) ) -> if ( ( ( e e. RR |-> ( e + ( ( |_ ` ( ( _pi - e ) / T ) ) x. T ) ) ) ` ( V ` ( i + 1 ) ) ) = ( Q ` ( ( ( y e. RR |-> sup ( { h e. ( 0 ..^ M ) | ( Q ` h ) <_ ( ( g e. ( -u _pi (,] _pi ) |-> if ( g = _pi , -u _pi , g ) ) ` ( ( e e. RR |-> ( e + ( ( |_ ` ( ( _pi - e ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` i ) ) + 1 ) ) , ( ( j e. ( 0 ..^ M ) |-> [_ j / i ]_ U ) ` ( ( y e. RR |-> sup ( { h e. ( 0 ..^ M ) | ( Q ` h ) <_ ( ( g e. ( -u _pi (,] _pi ) |-> if ( g = _pi , -u _pi , g ) ) ` ( ( e e. RR |-> ( e + ( ( |_ ` ( ( _pi - e ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` i ) ) ) , ( F ` ( ( e e. RR |-> ( e + ( ( |_ ` ( ( _pi - e ) / T ) ) x. T ) ) ) ` ( V ` ( i + 1 ) ) ) ) ) e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` ( i + 1 ) ) ) )
406 2 dirkercncf 
 |-  ( n e. NN -> ( D ` n ) e. ( RR -cn-> RR ) )
407 406 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( D ` n ) e. ( RR -cn-> RR ) )
408 eqid 
 |-  ( s e. ( -u _pi [,] _pi ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) = ( s e. ( -u _pi [,] _pi ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) )
409 397 398 399 400 66 401 402 403 404 405 320 3 407 408 fourierdlem84 
 |-  ( ( ph /\ n e. NN ) -> ( s e. ( -u _pi [,] _pi ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) e. L^1 )
410 381 383 396 409 iblss 
 |-  ( ( ph /\ n e. NN ) -> ( s e. ( -u _pi (,) 0 ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) e. L^1 )
411 374 410 itgcl 
 |-  ( ( ph /\ n e. NN ) -> S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s e. CC )
412 361 362 363 411 fvmptd 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) ` n ) = S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
413 412 411 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) ` n ) e. CC )
414 eqidd 
 |-  ( ( ph /\ n e. NN ) -> ( m e. NN |-> S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) = ( m e. NN |-> S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) )
415 340 adantl 
 |-  ( ( ( ph /\ n e. NN ) /\ m = n ) -> S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s = S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
416 1 adantr 
 |-  ( ( ph /\ s e. ( 0 (,) _pi ) ) -> F : RR --> RR )
417 26 adantr 
 |-  ( ( ph /\ s e. ( 0 (,) _pi ) ) -> X e. RR )
418 elioore 
 |-  ( s e. ( 0 (,) _pi ) -> s e. RR )
419 418 adantl 
 |-  ( ( ph /\ s e. ( 0 (,) _pi ) ) -> s e. RR )
420 417 419 readdcld 
 |-  ( ( ph /\ s e. ( 0 (,) _pi ) ) -> ( X + s ) e. RR )
421 416 420 ffvelrnd 
 |-  ( ( ph /\ s e. ( 0 (,) _pi ) ) -> ( F ` ( X + s ) ) e. RR )
422 421 adantlr 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( 0 (,) _pi ) ) -> ( F ` ( X + s ) ) e. RR )
423 418 371 sylan2 
 |-  ( ( n e. NN /\ s e. ( 0 (,) _pi ) ) -> ( ( D ` n ) ` s ) e. RR )
424 423 adantll 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( 0 (,) _pi ) ) -> ( ( D ` n ) ` s ) e. RR )
425 422 424 remulcld 
 |-  ( ( ( ph /\ n e. NN ) /\ s e. ( 0 (,) _pi ) ) -> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) e. RR )
426 ioossicc 
 |-  ( 0 (,) _pi ) C_ ( 0 [,] _pi )
427 78 79 76 ltleii 
 |-  -u _pi <_ 0
428 71 leidi 
 |-  _pi <_ _pi
429 iccss 
 |-  ( ( ( -u _pi e. RR /\ _pi e. RR ) /\ ( -u _pi <_ 0 /\ _pi <_ _pi ) ) -> ( 0 [,] _pi ) C_ ( -u _pi [,] _pi ) )
430 78 71 427 428 429 mp4an 
 |-  ( 0 [,] _pi ) C_ ( -u _pi [,] _pi )
431 426 430 sstri 
 |-  ( 0 (,) _pi ) C_ ( -u _pi [,] _pi )
432 431 a1i 
 |-  ( ( ph /\ n e. NN ) -> ( 0 (,) _pi ) C_ ( -u _pi [,] _pi ) )
433 ioombl 
 |-  ( 0 (,) _pi ) e. dom vol
434 433 a1i 
 |-  ( ( ph /\ n e. NN ) -> ( 0 (,) _pi ) e. dom vol )
435 432 434 396 409 iblss 
 |-  ( ( ph /\ n e. NN ) -> ( s e. ( 0 (,) _pi ) |-> ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) ) e. L^1 )
436 425 435 itgcl 
 |-  ( ( ph /\ n e. NN ) -> S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s e. CC )
437 414 415 363 436 fvmptd 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) ` n ) = S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s )
438 437 436 eqeltrd 
 |-  ( ( ph /\ n e. NN ) -> ( ( m e. NN |-> S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) ` n ) e. CC )
439 eleq1w 
 |-  ( m = n -> ( m e. NN <-> n e. NN ) )
440 439 anbi2d 
 |-  ( m = n -> ( ( ph /\ m e. NN ) <-> ( ph /\ n e. NN ) ) )
441 fveq2 
 |-  ( m = n -> ( Z ` m ) = ( Z ` n ) )
442 276 340 oveq12d 
 |-  ( m = n -> ( S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s + S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) = ( S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s + S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s ) )
443 441 442 eqeq12d 
 |-  ( m = n -> ( ( Z ` m ) = ( S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s + S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) <-> ( Z ` n ) = ( S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s + S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s ) ) )
444 440 443 imbi12d 
 |-  ( m = n -> ( ( ( ph /\ m e. NN ) -> ( Z ` m ) = ( S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s + S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) ) <-> ( ( ph /\ n e. NN ) -> ( Z ` n ) = ( S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s + S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s ) ) ) )
445 oveq1 
 |-  ( n = m -> ( n x. x ) = ( m x. x ) )
446 445 fveq2d 
 |-  ( n = m -> ( cos ` ( n x. x ) ) = ( cos ` ( m x. x ) ) )
447 446 oveq2d 
 |-  ( n = m -> ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) = ( ( F ` x ) x. ( cos ` ( m x. x ) ) ) )
448 447 adantr 
 |-  ( ( n = m /\ x e. ( -u _pi (,) _pi ) ) -> ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) = ( ( F ` x ) x. ( cos ` ( m x. x ) ) ) )
449 448 itgeq2dv 
 |-  ( n = m -> S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x = S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( m x. x ) ) ) _d x )
450 449 oveq1d 
 |-  ( n = m -> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) = ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( m x. x ) ) ) _d x / _pi ) )
451 450 cbvmptv 
 |-  ( n e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( n x. x ) ) ) _d x / _pi ) ) = ( m e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( m x. x ) ) ) _d x / _pi ) )
452 20 451 eqtri 
 |-  A = ( m e. NN0 |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( m x. x ) ) ) _d x / _pi ) )
453 445 fveq2d 
 |-  ( n = m -> ( sin ` ( n x. x ) ) = ( sin ` ( m x. x ) ) )
454 453 oveq2d 
 |-  ( n = m -> ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) = ( ( F ` x ) x. ( sin ` ( m x. x ) ) ) )
455 454 adantr 
 |-  ( ( n = m /\ x e. ( -u _pi (,) _pi ) ) -> ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) = ( ( F ` x ) x. ( sin ` ( m x. x ) ) ) )
456 455 itgeq2dv 
 |-  ( n = m -> S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x = S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( m x. x ) ) ) _d x )
457 456 oveq1d 
 |-  ( n = m -> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) = ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( m x. x ) ) ) _d x / _pi ) )
458 457 cbvmptv 
 |-  ( n e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( n x. x ) ) ) _d x / _pi ) ) = ( m e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( m x. x ) ) ) _d x / _pi ) )
459 21 458 eqtri 
 |-  B = ( m e. NN |-> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( m x. x ) ) ) _d x / _pi ) )
460 fveq2 
 |-  ( n = k -> ( A ` n ) = ( A ` k ) )
461 oveq1 
 |-  ( n = k -> ( n x. X ) = ( k x. X ) )
462 461 fveq2d 
 |-  ( n = k -> ( cos ` ( n x. X ) ) = ( cos ` ( k x. X ) ) )
463 460 462 oveq12d 
 |-  ( n = k -> ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) = ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) )
464 fveq2 
 |-  ( n = k -> ( B ` n ) = ( B ` k ) )
465 461 fveq2d 
 |-  ( n = k -> ( sin ` ( n x. X ) ) = ( sin ` ( k x. X ) ) )
466 464 465 oveq12d 
 |-  ( n = k -> ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) = ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) )
467 463 466 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 ) ) ) ) )
468 467 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 ) ) ) )
469 468 oveq2i 
 |-  ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( ( A ` 0 ) / 2 ) + sum_ k e. ( 1 ... m ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
470 469 mpteq2i 
 |-  ( 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 ) ) ) ) ) ) = ( m e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ k e. ( 1 ... m ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) )
471 oveq2 
 |-  ( m = n -> ( 1 ... m ) = ( 1 ... n ) )
472 471 sumeq1d 
 |-  ( m = n -> sum_ k e. ( 1 ... m ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) = sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
473 472 oveq2d 
 |-  ( m = n -> ( ( ( A ` 0 ) / 2 ) + sum_ k e. ( 1 ... m ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) = ( ( ( A ` 0 ) / 2 ) + sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) )
474 473 cbvmptv 
 |-  ( m e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ k e. ( 1 ... m ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) ) = ( n e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) )
475 fveq2 
 |-  ( k = m -> ( A ` k ) = ( A ` m ) )
476 oveq1 
 |-  ( k = m -> ( k x. X ) = ( m x. X ) )
477 476 fveq2d 
 |-  ( k = m -> ( cos ` ( k x. X ) ) = ( cos ` ( m x. X ) ) )
478 475 477 oveq12d 
 |-  ( k = m -> ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) = ( ( A ` m ) x. ( cos ` ( m x. X ) ) ) )
479 fveq2 
 |-  ( k = m -> ( B ` k ) = ( B ` m ) )
480 476 fveq2d 
 |-  ( k = m -> ( sin ` ( k x. X ) ) = ( sin ` ( m x. X ) ) )
481 479 480 oveq12d 
 |-  ( k = m -> ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) = ( ( B ` m ) x. ( sin ` ( m x. X ) ) ) )
482 478 481 oveq12d 
 |-  ( k = m -> ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) = ( ( ( A ` m ) x. ( cos ` ( m x. X ) ) ) + ( ( B ` m ) x. ( sin ` ( m x. X ) ) ) ) )
483 482 cbvsumv 
 |-  sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) = sum_ m e. ( 1 ... n ) ( ( ( A ` m ) x. ( cos ` ( m x. X ) ) ) + ( ( B ` m ) x. ( sin ` ( m x. X ) ) ) )
484 483 oveq2i 
 |-  ( ( ( A ` 0 ) / 2 ) + sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) = ( ( ( A ` 0 ) / 2 ) + sum_ m e. ( 1 ... n ) ( ( ( A ` m ) x. ( cos ` ( m x. X ) ) ) + ( ( B ` m ) x. ( sin ` ( m x. X ) ) ) ) )
485 484 mpteq2i 
 |-  ( n e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) ) = ( n e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ m e. ( 1 ... n ) ( ( ( A ` m ) x. ( cos ` ( m x. X ) ) ) + ( ( B ` m ) x. ( sin ` ( m x. X ) ) ) ) ) )
486 474 485 eqtri 
 |-  ( m e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ k e. ( 1 ... m ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) ) = ( n e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ m e. ( 1 ... n ) ( ( ( A ` m ) x. ( cos ` ( m x. X ) ) ) + ( ( B ` m ) x. ( sin ` ( m x. X ) ) ) ) ) )
487 22 470 486 3eqtri 
 |-  Z = ( n e. NN |-> ( ( ( A ` 0 ) / 2 ) + sum_ m e. ( 1 ... n ) ( ( ( A ` m ) x. ( cos ` ( m x. X ) ) ) + ( ( B ` m ) x. ( sin ` ( m x. X ) ) ) ) ) )
488 oveq2 
 |-  ( y = x -> ( X + y ) = ( X + x ) )
489 488 fveq2d 
 |-  ( y = x -> ( F ` ( X + y ) ) = ( F ` ( X + x ) ) )
490 fveq2 
 |-  ( y = x -> ( ( D ` m ) ` y ) = ( ( D ` m ) ` x ) )
491 489 490 oveq12d 
 |-  ( y = x -> ( ( F ` ( X + y ) ) x. ( ( D ` m ) ` y ) ) = ( ( F ` ( X + x ) ) x. ( ( D ` m ) ` x ) ) )
492 491 cbvmptv 
 |-  ( y e. RR |-> ( ( F ` ( X + y ) ) x. ( ( D ` m ) ` y ) ) ) = ( x e. RR |-> ( ( F ` ( X + x ) ) x. ( ( D ` m ) ` x ) ) )
493 eqid 
 |-  ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = ( -u _pi - X ) /\ ( p ` n ) = ( _pi - X ) ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) = ( n e. NN |-> { p e. ( RR ^m ( 0 ... n ) ) | ( ( ( p ` 0 ) = ( -u _pi - X ) /\ ( p ` n ) = ( _pi - X ) ) /\ A. i e. ( 0 ..^ n ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
494 fveq2 
 |-  ( j = i -> ( Q ` j ) = ( Q ` i ) )
495 494 oveq1d 
 |-  ( j = i -> ( ( Q ` j ) - X ) = ( ( Q ` i ) - X ) )
496 495 cbvmptv 
 |-  ( j e. ( 0 ... M ) |-> ( ( Q ` j ) - X ) ) = ( i e. ( 0 ... M ) |-> ( ( Q ` i ) - X ) )
497 452 459 487 2 3 4 5 8 1 11 492 12 13 14 10 493 496 fourierdlem111 
 |-  ( ( ph /\ m e. NN ) -> ( Z ` m ) = ( S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s + S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) )
498 444 497 chvarvv 
 |-  ( ( ph /\ n e. NN ) -> ( Z ` n ) = ( S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s + S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s ) )
499 412 437 oveq12d 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( m e. NN |-> S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) ` n ) + ( ( m e. NN |-> S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) ` n ) ) = ( S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s + S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` n ) ` s ) ) _d s ) )
500 498 499 eqtr4d 
 |-  ( ( ph /\ n e. NN ) -> ( Z ` n ) = ( ( ( m e. NN |-> S. ( -u _pi (,) 0 ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) ` n ) + ( ( m e. NN |-> S. ( 0 (,) _pi ) ( ( F ` ( X + s ) ) x. ( ( D ` m ) ` s ) ) _d s ) ` n ) ) )
501 41 49 52 65 39 40 334 338 360 413 438 500 climaddf 
 |-  ( ph -> Z ~~> ( ( L / 2 ) + ( R / 2 ) ) )
502 limccl 
 |-  ( ( F |` ( -oo (,) X ) ) limCC X ) C_ CC
503 502 18 sselid 
 |-  ( ph -> L e. CC )
504 limccl 
 |-  ( ( F |` ( X (,) +oo ) ) limCC X ) C_ CC
505 504 19 sselid 
 |-  ( ph -> R e. CC )
506 2cnd 
 |-  ( ph -> 2 e. CC )
507 2pos 
 |-  0 < 2
508 507 a1i 
 |-  ( ph -> 0 < 2 )
509 508 gt0ne0d 
 |-  ( ph -> 2 =/= 0 )
510 503 505 506 509 divdird 
 |-  ( ph -> ( ( L + R ) / 2 ) = ( ( L / 2 ) + ( R / 2 ) ) )
511 501 510 breqtrrd 
 |-  ( ph -> Z ~~> ( ( L + R ) / 2 ) )
512 0nn0 
 |-  0 e. NN0
513 1 adantr 
 |-  ( ( ph /\ 0 e. NN0 ) -> F : RR --> RR )
514 eqid 
 |-  ( -u _pi (,) _pi ) = ( -u _pi (,) _pi )
515 ioossre 
 |-  ( -u _pi (,) _pi ) C_ RR
516 515 a1i 
 |-  ( ph -> ( -u _pi (,) _pi ) C_ RR )
517 1 516 feqresmpt 
 |-  ( ph -> ( F |` ( -u _pi (,) _pi ) ) = ( x e. ( -u _pi (,) _pi ) |-> ( F ` x ) ) )
518 ioossicc 
 |-  ( -u _pi (,) _pi ) C_ ( -u _pi [,] _pi )
519 518 a1i 
 |-  ( ph -> ( -u _pi (,) _pi ) C_ ( -u _pi [,] _pi ) )
520 ioombl 
 |-  ( -u _pi (,) _pi ) e. dom vol
521 520 a1i 
 |-  ( ph -> ( -u _pi (,) _pi ) e. dom vol )
522 1 adantr 
 |-  ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> F : RR --> RR )
523 386 sselda 
 |-  ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> x e. RR )
524 522 523 ffvelrnd 
 |-  ( ( ph /\ x e. ( -u _pi [,] _pi ) ) -> ( F ` x ) e. RR )
525 1 386 feqresmpt 
 |-  ( ph -> ( F |` ( -u _pi [,] _pi ) ) = ( x e. ( -u _pi [,] _pi ) |-> ( F ` x ) ) )
526 187 a1i 
 |-  ( ph -> RR C_ CC )
527 1 526 fssd 
 |-  ( ph -> F : RR --> CC )
528 527 386 fssresd 
 |-  ( ph -> ( F |` ( -u _pi [,] _pi ) ) : ( -u _pi [,] _pi ) --> CC )
529 ioossicc 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) )
530 78 rexri 
 |-  -u _pi e. RR*
531 530 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> -u _pi e. RR* )
532 71 rexri 
 |-  _pi e. RR*
533 532 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> _pi e. RR* )
534 3 4 5 fourierdlem15 
 |-  ( ph -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
535 534 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> ( -u _pi [,] _pi ) )
536 simpr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ..^ M ) )
537 531 533 535 536 fourierdlem8 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) [,] ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
538 529 537 sstrid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ ( -u _pi [,] _pi ) )
539 538 resabs1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( -u _pi [,] _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
540 539 12 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( -u _pi [,] _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
541 539 eqcomd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( ( F |` ( -u _pi [,] _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
542 541 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) = ( ( ( F |` ( -u _pi [,] _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
543 13 542 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> C e. ( ( ( F |` ( -u _pi [,] _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
544 541 oveq1d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) = ( ( ( F |` ( -u _pi [,] _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
545 14 544 eleqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> U e. ( ( ( F |` ( -u _pi [,] _pi ) ) |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
546 3 4 5 528 540 543 545 fourierdlem69 
 |-  ( ph -> ( F |` ( -u _pi [,] _pi ) ) e. L^1 )
547 525 546 eqeltrrd 
 |-  ( ph -> ( x e. ( -u _pi [,] _pi ) |-> ( F ` x ) ) e. L^1 )
548 519 521 524 547 iblss 
 |-  ( ph -> ( x e. ( -u _pi (,) _pi ) |-> ( F ` x ) ) e. L^1 )
549 517 548 eqeltrd 
 |-  ( ph -> ( F |` ( -u _pi (,) _pi ) ) e. L^1 )
550 549 adantr 
 |-  ( ( ph /\ 0 e. NN0 ) -> ( F |` ( -u _pi (,) _pi ) ) e. L^1 )
551 simpr 
 |-  ( ( ph /\ 0 e. NN0 ) -> 0 e. NN0 )
552 513 514 550 20 551 fourierdlem16 
 |-  ( ( ph /\ 0 e. NN0 ) -> ( ( ( A ` 0 ) e. RR /\ ( x e. ( -u _pi (,) _pi ) |-> ( F ` x ) ) e. L^1 ) /\ S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( 0 x. x ) ) ) _d x e. RR ) )
553 552 simplld 
 |-  ( ( ph /\ 0 e. NN0 ) -> ( A ` 0 ) e. RR )
554 512 553 mpan2 
 |-  ( ph -> ( A ` 0 ) e. RR )
555 554 rehalfcld 
 |-  ( ph -> ( ( A ` 0 ) / 2 ) e. RR )
556 555 recnd 
 |-  ( ph -> ( ( A ` 0 ) / 2 ) e. CC )
557 335 mptex 
 |-  ( n e. NN |-> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) e. _V
558 557 a1i 
 |-  ( ph -> ( n e. NN |-> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) e. _V )
559 simpr 
 |-  ( ( ph /\ m e. NN ) -> m e. NN )
560 555 adantr 
 |-  ( ( ph /\ m e. NN ) -> ( ( A ` 0 ) / 2 ) e. RR )
561 fzfid 
 |-  ( ( ph /\ m e. NN ) -> ( 1 ... m ) e. Fin )
562 simpll 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. ( 1 ... m ) ) -> ph )
563 elfznn 
 |-  ( n e. ( 1 ... m ) -> n e. NN )
564 563 adantl 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. ( 1 ... m ) ) -> n e. NN )
565 simpl 
 |-  ( ( ph /\ n e. NN ) -> ph )
566 363 nnnn0d 
 |-  ( ( ph /\ n e. NN ) -> n e. NN0 )
567 eleq1w 
 |-  ( k = n -> ( k e. NN0 <-> n e. NN0 ) )
568 567 anbi2d 
 |-  ( k = n -> ( ( ph /\ k e. NN0 ) <-> ( ph /\ n e. NN0 ) ) )
569 fveq2 
 |-  ( k = n -> ( A ` k ) = ( A ` n ) )
570 569 eleq1d 
 |-  ( k = n -> ( ( A ` k ) e. RR <-> ( A ` n ) e. RR ) )
571 568 570 imbi12d 
 |-  ( k = n -> ( ( ( ph /\ k e. NN0 ) -> ( A ` k ) e. RR ) <-> ( ( ph /\ n e. NN0 ) -> ( A ` n ) e. RR ) ) )
572 1 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> F : RR --> RR )
573 549 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> ( F |` ( -u _pi (,) _pi ) ) e. L^1 )
574 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
575 572 514 573 20 574 fourierdlem16 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( A ` k ) e. RR /\ ( x e. ( -u _pi (,) _pi ) |-> ( F ` x ) ) e. L^1 ) /\ S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( k x. x ) ) ) _d x e. RR ) )
576 575 simplld 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ` k ) e. RR )
577 571 576 chvarvv 
 |-  ( ( ph /\ n e. NN0 ) -> ( A ` n ) e. RR )
578 565 566 577 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( A ` n ) e. RR )
579 363 nnred 
 |-  ( ( ph /\ n e. NN ) -> n e. RR )
580 579 400 remulcld 
 |-  ( ( ph /\ n e. NN ) -> ( n x. X ) e. RR )
581 580 recoscld 
 |-  ( ( ph /\ n e. NN ) -> ( cos ` ( n x. X ) ) e. RR )
582 578 581 remulcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) e. RR )
583 eleq1w 
 |-  ( k = n -> ( k e. NN <-> n e. NN ) )
584 583 anbi2d 
 |-  ( k = n -> ( ( ph /\ k e. NN ) <-> ( ph /\ n e. NN ) ) )
585 fveq2 
 |-  ( k = n -> ( B ` k ) = ( B ` n ) )
586 585 eleq1d 
 |-  ( k = n -> ( ( B ` k ) e. RR <-> ( B ` n ) e. RR ) )
587 584 586 imbi12d 
 |-  ( k = n -> ( ( ( ph /\ k e. NN ) -> ( B ` k ) e. RR ) <-> ( ( ph /\ n e. NN ) -> ( B ` n ) e. RR ) ) )
588 1 adantr 
 |-  ( ( ph /\ k e. NN ) -> F : RR --> RR )
589 549 adantr 
 |-  ( ( ph /\ k e. NN ) -> ( F |` ( -u _pi (,) _pi ) ) e. L^1 )
590 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
591 588 514 589 21 590 fourierdlem21 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( B ` k ) e. RR /\ ( x e. ( -u _pi (,) _pi ) |-> ( ( F ` x ) x. ( sin ` ( k x. x ) ) ) ) e. L^1 ) /\ S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( k x. x ) ) ) _d x e. RR ) )
592 591 simplld 
 |-  ( ( ph /\ k e. NN ) -> ( B ` k ) e. RR )
593 587 592 chvarvv 
 |-  ( ( ph /\ n e. NN ) -> ( B ` n ) e. RR )
594 580 resincld 
 |-  ( ( ph /\ n e. NN ) -> ( sin ` ( n x. X ) ) e. RR )
595 593 594 remulcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) e. RR )
596 582 595 readdcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) e. RR )
597 562 564 596 syl2anc 
 |-  ( ( ( ph /\ m e. NN ) /\ n e. ( 1 ... m ) ) -> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) e. RR )
598 561 597 fsumrecl 
 |-  ( ( ph /\ m e. NN ) -> sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) e. RR )
599 560 598 readdcld 
 |-  ( ( ph /\ 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 ) ) ) ) ) e. RR )
600 22 fvmpt2 
 |-  ( ( 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 ) ) ) ) ) e. RR ) -> ( Z ` m ) = ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) )
601 559 599 600 syl2anc 
 |-  ( ( ph /\ m e. NN ) -> ( Z ` m ) = ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) )
602 601 599 eqeltrd 
 |-  ( ( ph /\ m e. NN ) -> ( Z ` m ) e. RR )
603 602 recnd 
 |-  ( ( ph /\ m e. NN ) -> ( Z ` m ) e. CC )
604 eqidd 
 |-  ( ( ph /\ m e. NN ) -> ( n e. NN |-> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) = ( n e. NN |-> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) )
605 oveq2 
 |-  ( n = m -> ( 1 ... n ) = ( 1 ... m ) )
606 605 sumeq1d 
 |-  ( n = m -> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) = sum_ k e. ( 1 ... m ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
607 606 adantl 
 |-  ( ( ( ph /\ m e. NN ) /\ n = m ) -> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) = sum_ k e. ( 1 ... m ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
608 sumex 
 |-  sum_ k e. ( 1 ... m ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) e. _V
609 608 a1i 
 |-  ( ( ph /\ m e. NN ) -> sum_ k e. ( 1 ... m ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) e. _V )
610 604 607 559 609 fvmptd 
 |-  ( ( ph /\ m e. NN ) -> ( ( n e. NN |-> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) ` m ) = sum_ k e. ( 1 ... m ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
611 560 recnd 
 |-  ( ( ph /\ m e. NN ) -> ( ( A ` 0 ) / 2 ) e. CC )
612 598 recnd 
 |-  ( ( ph /\ m e. NN ) -> sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) e. CC )
613 611 612 pncan2d 
 |-  ( ( ph /\ 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 ) ) ) ) ) - ( ( A ` 0 ) / 2 ) ) = sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
614 613 468 eqtr2di 
 |-  ( ( ph /\ m e. NN ) -> sum_ k e. ( 1 ... m ) ( ( ( 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 ) ) ) ) ) - ( ( A ` 0 ) / 2 ) ) )
615 ovex 
 |-  ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) e. _V
616 22 fvmpt2 
 |-  ( ( 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 ) ) ) ) ) e. _V ) -> ( Z ` m ) = ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) )
617 559 615 616 sylancl 
 |-  ( ( ph /\ m e. NN ) -> ( Z ` m ) = ( ( ( A ` 0 ) / 2 ) + sum_ n e. ( 1 ... m ) ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) )
618 617 eqcomd 
 |-  ( ( ph /\ 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 ) ) ) ) ) = ( Z ` m ) )
619 618 oveq1d 
 |-  ( ( ph /\ 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 ) ) ) ) ) - ( ( A ` 0 ) / 2 ) ) = ( ( Z ` m ) - ( ( A ` 0 ) / 2 ) ) )
620 610 614 619 3eqtrd 
 |-  ( ( ph /\ m e. NN ) -> ( ( n e. NN |-> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) ` m ) = ( ( Z ` m ) - ( ( A ` 0 ) / 2 ) ) )
621 39 40 511 556 558 603 620 climsubc1 
 |-  ( ph -> ( n e. NN |-> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) ~~> ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) )
622 seqex 
 |-  seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) e. _V
623 622 a1i 
 |-  ( ph -> seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) e. _V )
624 eqidd 
 |-  ( ( ph /\ l e. NN ) -> ( n e. NN |-> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) = ( n e. NN |-> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) )
625 oveq2 
 |-  ( n = l -> ( 1 ... n ) = ( 1 ... l ) )
626 625 sumeq1d 
 |-  ( n = l -> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) = sum_ k e. ( 1 ... l ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
627 626 adantl 
 |-  ( ( ( ph /\ l e. NN ) /\ n = l ) -> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) = sum_ k e. ( 1 ... l ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
628 simpr 
 |-  ( ( ph /\ l e. NN ) -> l e. NN )
629 fzfid 
 |-  ( ( ph /\ l e. NN ) -> ( 1 ... l ) e. Fin )
630 elfznn 
 |-  ( k e. ( 1 ... l ) -> k e. NN )
631 630 nnnn0d 
 |-  ( k e. ( 1 ... l ) -> k e. NN0 )
632 631 576 sylan2 
 |-  ( ( ph /\ k e. ( 1 ... l ) ) -> ( A ` k ) e. RR )
633 630 nnred 
 |-  ( k e. ( 1 ... l ) -> k e. RR )
634 633 adantl 
 |-  ( ( ph /\ k e. ( 1 ... l ) ) -> k e. RR )
635 8 adantr 
 |-  ( ( ph /\ k e. ( 1 ... l ) ) -> X e. RR )
636 634 635 remulcld 
 |-  ( ( ph /\ k e. ( 1 ... l ) ) -> ( k x. X ) e. RR )
637 636 recoscld 
 |-  ( ( ph /\ k e. ( 1 ... l ) ) -> ( cos ` ( k x. X ) ) e. RR )
638 632 637 remulcld 
 |-  ( ( ph /\ k e. ( 1 ... l ) ) -> ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) e. RR )
639 630 592 sylan2 
 |-  ( ( ph /\ k e. ( 1 ... l ) ) -> ( B ` k ) e. RR )
640 636 resincld 
 |-  ( ( ph /\ k e. ( 1 ... l ) ) -> ( sin ` ( k x. X ) ) e. RR )
641 639 640 remulcld 
 |-  ( ( ph /\ k e. ( 1 ... l ) ) -> ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) e. RR )
642 638 641 readdcld 
 |-  ( ( ph /\ k e. ( 1 ... l ) ) -> ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) e. RR )
643 642 adantlr 
 |-  ( ( ( ph /\ l e. NN ) /\ k e. ( 1 ... l ) ) -> ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) e. RR )
644 629 643 fsumrecl 
 |-  ( ( ph /\ l e. NN ) -> sum_ k e. ( 1 ... l ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) e. RR )
645 624 627 628 644 fvmptd 
 |-  ( ( ph /\ l e. NN ) -> ( ( n e. NN |-> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) ` l ) = sum_ k e. ( 1 ... l ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
646 eleq1w 
 |-  ( n = l -> ( n e. NN <-> l e. NN ) )
647 646 anbi2d 
 |-  ( n = l -> ( ( ph /\ n e. NN ) <-> ( ph /\ l e. NN ) ) )
648 fveq2 
 |-  ( n = l -> ( seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) ` n ) = ( seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) ` l ) )
649 626 648 eqeq12d 
 |-  ( n = l -> ( sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) = ( seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) ` n ) <-> sum_ k e. ( 1 ... l ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) = ( seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) ` l ) ) )
650 647 649 imbi12d 
 |-  ( n = l -> ( ( ( ph /\ n e. NN ) -> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) = ( seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) ` n ) ) <-> ( ( ph /\ l e. NN ) -> sum_ k e. ( 1 ... l ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) = ( seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) ` l ) ) ) )
651 eqidd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) = ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) )
652 fveq2 
 |-  ( j = k -> ( A ` j ) = ( A ` k ) )
653 oveq1 
 |-  ( j = k -> ( j x. X ) = ( k x. X ) )
654 653 fveq2d 
 |-  ( j = k -> ( cos ` ( j x. X ) ) = ( cos ` ( k x. X ) ) )
655 652 654 oveq12d 
 |-  ( j = k -> ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) = ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) )
656 fveq2 
 |-  ( j = k -> ( B ` j ) = ( B ` k ) )
657 653 fveq2d 
 |-  ( j = k -> ( sin ` ( j x. X ) ) = ( sin ` ( k x. X ) ) )
658 656 657 oveq12d 
 |-  ( j = k -> ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) = ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) )
659 655 658 oveq12d 
 |-  ( j = k -> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) = ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
660 659 adantl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) /\ j = k ) -> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) = ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
661 elfznn 
 |-  ( k e. ( 1 ... n ) -> k e. NN )
662 661 adantl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. NN )
663 simpll 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ph )
664 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
665 nn0re 
 |-  ( k e. NN0 -> k e. RR )
666 665 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> k e. RR )
667 8 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> X e. RR )
668 666 667 remulcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( k x. X ) e. RR )
669 668 recoscld 
 |-  ( ( ph /\ k e. NN0 ) -> ( cos ` ( k x. X ) ) e. RR )
670 576 669 remulcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) e. RR )
671 664 670 sylan2 
 |-  ( ( ph /\ k e. NN ) -> ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) e. RR )
672 664 668 sylan2 
 |-  ( ( ph /\ k e. NN ) -> ( k x. X ) e. RR )
673 672 resincld 
 |-  ( ( ph /\ k e. NN ) -> ( sin ` ( k x. X ) ) e. RR )
674 592 673 remulcld 
 |-  ( ( ph /\ k e. NN ) -> ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) e. RR )
675 671 674 readdcld 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) e. RR )
676 663 662 675 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) e. RR )
677 651 660 662 676 fvmptd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ` k ) = ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) )
678 363 39 eleqtrdi 
 |-  ( ( ph /\ n e. NN ) -> n e. ( ZZ>= ` 1 ) )
679 676 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) e. CC )
680 677 678 679 fsumser 
 |-  ( ( ph /\ n e. NN ) -> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) = ( seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) ` n ) )
681 650 680 chvarvv 
 |-  ( ( ph /\ l e. NN ) -> sum_ k e. ( 1 ... l ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) = ( seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) ` l ) )
682 645 681 eqtrd 
 |-  ( ( ph /\ l e. NN ) -> ( ( n e. NN |-> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) ` l ) = ( seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) ` l ) )
683 39 558 623 40 682 climeq 
 |-  ( ph -> ( ( n e. NN |-> sum_ k e. ( 1 ... n ) ( ( ( A ` k ) x. ( cos ` ( k x. X ) ) ) + ( ( B ` k ) x. ( sin ` ( k x. X ) ) ) ) ) ~~> ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) <-> seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) ~~> ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) ) )
684 621 683 mpbid 
 |-  ( ph -> seq 1 ( + , ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ) ~~> ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) )
685 38 684 eqbrtrd 
 |-  ( ph -> seq 1 ( + , S ) ~~> ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) )
686 eqidd 
 |-  ( ( ph /\ n e. NN ) -> ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) = ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) )
687 fveq2 
 |-  ( j = n -> ( A ` j ) = ( A ` n ) )
688 oveq1 
 |-  ( j = n -> ( j x. X ) = ( n x. X ) )
689 688 fveq2d 
 |-  ( j = n -> ( cos ` ( j x. X ) ) = ( cos ` ( n x. X ) ) )
690 687 689 oveq12d 
 |-  ( j = n -> ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) = ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) )
691 fveq2 
 |-  ( j = n -> ( B ` j ) = ( B ` n ) )
692 688 fveq2d 
 |-  ( j = n -> ( sin ` ( j x. X ) ) = ( sin ` ( n x. X ) ) )
693 691 692 oveq12d 
 |-  ( j = n -> ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) = ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) )
694 690 693 oveq12d 
 |-  ( j = n -> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) = ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
695 694 adantl 
 |-  ( ( ( ph /\ n e. NN ) /\ j = n ) -> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) = ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
696 686 695 363 596 fvmptd 
 |-  ( ( ph /\ n e. NN ) -> ( ( j e. NN |-> ( ( ( A ` j ) x. ( cos ` ( j x. X ) ) ) + ( ( B ` j ) x. ( sin ` ( j x. X ) ) ) ) ) ` n ) = ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) )
697 596 recnd 
 |-  ( ( ph /\ n e. NN ) -> ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) e. CC )
698 39 40 696 697 684 isumclim 
 |-  ( ph -> sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) = ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) )
699 698 oveq2d 
 |-  ( ph -> ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( ( A ` 0 ) / 2 ) + ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) ) )
700 503 505 addcld 
 |-  ( ph -> ( L + R ) e. CC )
701 700 halfcld 
 |-  ( ph -> ( ( L + R ) / 2 ) e. CC )
702 556 701 pncan3d 
 |-  ( ph -> ( ( ( A ` 0 ) / 2 ) + ( ( ( L + R ) / 2 ) - ( ( A ` 0 ) / 2 ) ) ) = ( ( L + R ) / 2 ) )
703 699 702 eqtrd 
 |-  ( ph -> ( ( ( A ` 0 ) / 2 ) + sum_ n e. NN ( ( ( A ` n ) x. ( cos ` ( n x. X ) ) ) + ( ( B ` n ) x. ( sin ` ( n x. X ) ) ) ) ) = ( ( L + R ) / 2 ) )
704 685 703 jca 
 |-  ( 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 ) ) )