This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem76

Description: Continuity of O and its limits with respect to the S partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem76.f 
|- ( ph -> F : RR --> RR )
fourierdlem76.xre 
|- ( ph -> X e. RR )
fourierdlem76.p 
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` m ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
fourierdlem76.m 
|- ( ph -> M e. NN )
fourierdlem76.v 
|- ( ph -> V e. ( P ` M ) )
fourierdlem76.fcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem76.r 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` i ) ) )
fourierdlem76.l 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` ( i + 1 ) ) ) )
fourierdlem76.a 
|- ( ph -> A e. RR )
fourierdlem76.b 
|- ( ph -> B e. RR )
fourierdlem76.altb 
|- ( ph -> A < B )
fourierdlem76.ab 
|- ( ph -> ( A [,] B ) C_ ( -u _pi [,] _pi ) )
fourierdlem76.n0 
|- ( ph -> -. 0 e. ( A [,] B ) )
fourierdlem76.c 
|- ( ph -> C e. RR )
fourierdlem76.o 
|- O = ( s e. ( A [,] B ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
fourierdlem76.q 
|- Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
fourierdlem76.t 
|- T = ( { A , B } u. ( ran Q i^i ( A (,) B ) ) )
fourierdlem76.n 
|- N = ( ( # ` T ) - 1 )
fourierdlem76.s 
|- S = ( iota f f Isom < , < ( ( 0 ... N ) , T ) )
fourierdlem76.d 
|- D = ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) )
fourierdlem76.e 
|- E = ( ( ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) )
fourierdlem76.ch 
|- ( ch <-> ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
Assertion fourierdlem76 
|- ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D e. ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) /\ E e. ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) ) /\ ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem76.f 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem76.xre 
 |-  ( ph -> X e. RR )
3 fourierdlem76.p 
 |-  P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = ( -u _pi + X ) /\ ( p ` m ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
4 fourierdlem76.m 
 |-  ( ph -> M e. NN )
5 fourierdlem76.v 
 |-  ( ph -> V e. ( P ` M ) )
6 fourierdlem76.fcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
7 fourierdlem76.r 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` i ) ) )
8 fourierdlem76.l 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` ( i + 1 ) ) ) )
9 fourierdlem76.a 
 |-  ( ph -> A e. RR )
10 fourierdlem76.b 
 |-  ( ph -> B e. RR )
11 fourierdlem76.altb 
 |-  ( ph -> A < B )
12 fourierdlem76.ab 
 |-  ( ph -> ( A [,] B ) C_ ( -u _pi [,] _pi ) )
13 fourierdlem76.n0 
 |-  ( ph -> -. 0 e. ( A [,] B ) )
14 fourierdlem76.c 
 |-  ( ph -> C e. RR )
15 fourierdlem76.o 
 |-  O = ( s e. ( A [,] B ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
16 fourierdlem76.q 
 |-  Q = ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) )
17 fourierdlem76.t 
 |-  T = ( { A , B } u. ( ran Q i^i ( A (,) B ) ) )
18 fourierdlem76.n 
 |-  N = ( ( # ` T ) - 1 )
19 fourierdlem76.s 
 |-  S = ( iota f f Isom < , < ( ( 0 ... N ) , T ) )
20 fourierdlem76.d 
 |-  D = ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) )
21 fourierdlem76.e 
 |-  E = ( ( ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) )
22 fourierdlem76.ch 
 |-  ( ch <-> ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
23 eqid 
 |-  ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / s ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / s ) )
24 eqid 
 |-  ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
25 eqid 
 |-  ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
26 simplll 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ph )
27 22 26 sylbi 
 |-  ( ch -> ph )
28 27 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ph )
29 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
30 9 rexrd 
 |-  ( ph -> A e. RR* )
31 27 30 syl 
 |-  ( ch -> A e. RR* )
32 31 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> A e. RR* )
33 10 rexrd 
 |-  ( ph -> B e. RR* )
34 27 33 syl 
 |-  ( ch -> B e. RR* )
35 34 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> B e. RR* )
36 elioore 
 |-  ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> s e. RR )
37 36 adantl 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. RR )
38 27 9 syl 
 |-  ( ch -> A e. RR )
39 38 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> A e. RR )
40 prfi 
 |-  { A , B } e. Fin
41 40 a1i 
 |-  ( ph -> { A , B } e. Fin )
42 fzfid 
 |-  ( ph -> ( 0 ... M ) e. Fin )
43 16 rnmptfi 
 |-  ( ( 0 ... M ) e. Fin -> ran Q e. Fin )
44 infi 
 |-  ( ran Q e. Fin -> ( ran Q i^i ( A (,) B ) ) e. Fin )
45 42 43 44 3syl 
 |-  ( ph -> ( ran Q i^i ( A (,) B ) ) e. Fin )
46 unfi 
 |-  ( ( { A , B } e. Fin /\ ( ran Q i^i ( A (,) B ) ) e. Fin ) -> ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) e. Fin )
47 41 45 46 syl2anc 
 |-  ( ph -> ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) e. Fin )
48 17 47 eqeltrid 
 |-  ( ph -> T e. Fin )
49 prssg 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A e. RR /\ B e. RR ) <-> { A , B } C_ RR ) )
50 9 10 49 syl2anc 
 |-  ( ph -> ( ( A e. RR /\ B e. RR ) <-> { A , B } C_ RR ) )
51 9 10 50 mpbi2and 
 |-  ( ph -> { A , B } C_ RR )
52 inss2 
 |-  ( ran Q i^i ( A (,) B ) ) C_ ( A (,) B )
53 ioossre 
 |-  ( A (,) B ) C_ RR
54 52 53 sstri 
 |-  ( ran Q i^i ( A (,) B ) ) C_ RR
55 54 a1i 
 |-  ( ph -> ( ran Q i^i ( A (,) B ) ) C_ RR )
56 51 55 unssd 
 |-  ( ph -> ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) C_ RR )
57 17 56 eqsstrid 
 |-  ( ph -> T C_ RR )
58 48 57 19 18 fourierdlem36 
 |-  ( ph -> S Isom < , < ( ( 0 ... N ) , T ) )
59 27 58 syl 
 |-  ( ch -> S Isom < , < ( ( 0 ... N ) , T ) )
60 isof1o 
 |-  ( S Isom < , < ( ( 0 ... N ) , T ) -> S : ( 0 ... N ) -1-1-onto-> T )
61 f1of 
 |-  ( S : ( 0 ... N ) -1-1-onto-> T -> S : ( 0 ... N ) --> T )
62 59 60 61 3syl 
 |-  ( ch -> S : ( 0 ... N ) --> T )
63 27 57 syl 
 |-  ( ch -> T C_ RR )
64 62 63 fssd 
 |-  ( ch -> S : ( 0 ... N ) --> RR )
65 64 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> S : ( 0 ... N ) --> RR )
66 simpllr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> j e. ( 0 ..^ N ) )
67 22 66 sylbi 
 |-  ( ch -> j e. ( 0 ..^ N ) )
68 elfzofz 
 |-  ( j e. ( 0 ..^ N ) -> j e. ( 0 ... N ) )
69 67 68 syl 
 |-  ( ch -> j e. ( 0 ... N ) )
70 69 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> j e. ( 0 ... N ) )
71 65 70 ffvelcdmd 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( S ` j ) e. RR )
72 58 60 61 3syl 
 |-  ( ph -> S : ( 0 ... N ) --> T )
73 frn 
 |-  ( S : ( 0 ... N ) --> T -> ran S C_ T )
74 72 73 syl 
 |-  ( ph -> ran S C_ T )
75 9 leidd 
 |-  ( ph -> A <_ A )
76 9 10 11 ltled 
 |-  ( ph -> A <_ B )
77 9 10 9 75 76 eliccd 
 |-  ( ph -> A e. ( A [,] B ) )
78 10 leidd 
 |-  ( ph -> B <_ B )
79 9 10 10 76 78 eliccd 
 |-  ( ph -> B e. ( A [,] B ) )
80 prssg 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A e. ( A [,] B ) /\ B e. ( A [,] B ) ) <-> { A , B } C_ ( A [,] B ) ) )
81 9 10 80 syl2anc 
 |-  ( ph -> ( ( A e. ( A [,] B ) /\ B e. ( A [,] B ) ) <-> { A , B } C_ ( A [,] B ) ) )
82 77 79 81 mpbi2and 
 |-  ( ph -> { A , B } C_ ( A [,] B ) )
83 52 29 sstri 
 |-  ( ran Q i^i ( A (,) B ) ) C_ ( A [,] B )
84 83 a1i 
 |-  ( ph -> ( ran Q i^i ( A (,) B ) ) C_ ( A [,] B ) )
85 82 84 unssd 
 |-  ( ph -> ( { A , B } u. ( ran Q i^i ( A (,) B ) ) ) C_ ( A [,] B ) )
86 17 85 eqsstrid 
 |-  ( ph -> T C_ ( A [,] B ) )
87 74 86 sstrd 
 |-  ( ph -> ran S C_ ( A [,] B ) )
88 27 87 syl 
 |-  ( ch -> ran S C_ ( A [,] B ) )
89 ffun 
 |-  ( S : ( 0 ... N ) --> RR -> Fun S )
90 64 89 syl 
 |-  ( ch -> Fun S )
91 fdm 
 |-  ( S : ( 0 ... N ) --> RR -> dom S = ( 0 ... N ) )
92 64 91 syl 
 |-  ( ch -> dom S = ( 0 ... N ) )
93 92 eqcomd 
 |-  ( ch -> ( 0 ... N ) = dom S )
94 69 93 eleqtrd 
 |-  ( ch -> j e. dom S )
95 fvelrn 
 |-  ( ( Fun S /\ j e. dom S ) -> ( S ` j ) e. ran S )
96 90 94 95 syl2anc 
 |-  ( ch -> ( S ` j ) e. ran S )
97 88 96 sseldd 
 |-  ( ch -> ( S ` j ) e. ( A [,] B ) )
98 iccgelb 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( S ` j ) e. ( A [,] B ) ) -> A <_ ( S ` j ) )
99 31 34 97 98 syl3anc 
 |-  ( ch -> A <_ ( S ` j ) )
100 99 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> A <_ ( S ` j ) )
101 71 rexrd 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( S ` j ) e. RR* )
102 fzofzp1 
 |-  ( j e. ( 0 ..^ N ) -> ( j + 1 ) e. ( 0 ... N ) )
103 67 102 syl 
 |-  ( ch -> ( j + 1 ) e. ( 0 ... N ) )
104 64 103 ffvelcdmd 
 |-  ( ch -> ( S ` ( j + 1 ) ) e. RR )
105 104 rexrd 
 |-  ( ch -> ( S ` ( j + 1 ) ) e. RR* )
106 105 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( S ` ( j + 1 ) ) e. RR* )
107 simpr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
108 ioogtlb 
 |-  ( ( ( S ` j ) e. RR* /\ ( S ` ( j + 1 ) ) e. RR* /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( S ` j ) < s )
109 101 106 107 108 syl3anc 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( S ` j ) < s )
110 39 71 37 100 109 lelttrd 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> A < s )
111 104 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( S ` ( j + 1 ) ) e. RR )
112 27 10 syl 
 |-  ( ch -> B e. RR )
113 112 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> B e. RR )
114 iooltub 
 |-  ( ( ( S ` j ) e. RR* /\ ( S ` ( j + 1 ) ) e. RR* /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s < ( S ` ( j + 1 ) ) )
115 101 106 107 114 syl3anc 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s < ( S ` ( j + 1 ) ) )
116 103 93 eleqtrd 
 |-  ( ch -> ( j + 1 ) e. dom S )
117 fvelrn 
 |-  ( ( Fun S /\ ( j + 1 ) e. dom S ) -> ( S ` ( j + 1 ) ) e. ran S )
118 90 116 117 syl2anc 
 |-  ( ch -> ( S ` ( j + 1 ) ) e. ran S )
119 88 118 sseldd 
 |-  ( ch -> ( S ` ( j + 1 ) ) e. ( A [,] B ) )
120 iccleub 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( S ` ( j + 1 ) ) e. ( A [,] B ) ) -> ( S ` ( j + 1 ) ) <_ B )
121 31 34 119 120 syl3anc 
 |-  ( ch -> ( S ` ( j + 1 ) ) <_ B )
122 121 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( S ` ( j + 1 ) ) <_ B )
123 37 111 113 115 122 ltletrd 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s < B )
124 32 35 37 110 123 eliood 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. ( A (,) B ) )
125 29 124 sselid 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. ( A [,] B ) )
126 1 adantr 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> F : RR --> RR )
127 2 adantr 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> X e. RR )
128 9 10 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
129 128 sselda 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> s e. RR )
130 127 129 readdcld 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> ( X + s ) e. RR )
131 126 130 ffvelcdmd 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> ( F ` ( X + s ) ) e. RR )
132 28 125 131 syl2anc 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( F ` ( X + s ) ) e. RR )
133 132 recnd 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( F ` ( X + s ) ) e. CC )
134 14 recnd 
 |-  ( ph -> C e. CC )
135 27 134 syl 
 |-  ( ch -> C e. CC )
136 135 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> C e. CC )
137 133 136 subcld 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( F ` ( X + s ) ) - C ) e. CC )
138 ioossre 
 |-  ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ RR
139 138 a1i 
 |-  ( ch -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ RR )
140 139 sselda 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. RR )
141 140 recnd 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. CC )
142 nne 
 |-  ( -. s =/= 0 <-> s = 0 )
143 142 biimpi 
 |-  ( -. s =/= 0 -> s = 0 )
144 143 eqcomd 
 |-  ( -. s =/= 0 -> 0 = s )
145 144 adantl 
 |-  ( ( ( ph /\ s e. ( A [,] B ) ) /\ -. s =/= 0 ) -> 0 = s )
146 simpr 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> s e. ( A [,] B ) )
147 146 adantr 
 |-  ( ( ( ph /\ s e. ( A [,] B ) ) /\ -. s =/= 0 ) -> s e. ( A [,] B ) )
148 145 147 eqeltrd 
 |-  ( ( ( ph /\ s e. ( A [,] B ) ) /\ -. s =/= 0 ) -> 0 e. ( A [,] B ) )
149 13 ad2antrr 
 |-  ( ( ( ph /\ s e. ( A [,] B ) ) /\ -. s =/= 0 ) -> -. 0 e. ( A [,] B ) )
150 148 149 condan 
 |-  ( ( ph /\ s e. ( A [,] B ) ) -> s =/= 0 )
151 28 125 150 syl2anc 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s =/= 0 )
152 137 141 151 divcld 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( ( F ` ( X + s ) ) - C ) / s ) e. CC )
153 2cnd 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> 2 e. CC )
154 141 halfcld 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( s / 2 ) e. CC )
155 154 sincld 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( sin ` ( s / 2 ) ) e. CC )
156 153 155 mulcld 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
157 36 recnd 
 |-  ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> s e. CC )
158 157 adantl 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. CC )
159 158 halfcld 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( s / 2 ) e. CC )
160 159 sincld 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( sin ` ( s / 2 ) ) e. CC )
161 2ne0 
 |-  2 =/= 0
162 161 a1i 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> 2 =/= 0 )
163 27 12 syl 
 |-  ( ch -> ( A [,] B ) C_ ( -u _pi [,] _pi ) )
164 163 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( A [,] B ) C_ ( -u _pi [,] _pi ) )
165 164 125 sseldd 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. ( -u _pi [,] _pi ) )
166 fourierdlem44 
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ s =/= 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 )
167 165 151 166 syl2anc 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( sin ` ( s / 2 ) ) =/= 0 )
168 153 160 162 167 mulne0d 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 )
169 141 156 168 divcld 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. CC )
170 eqid 
 |-  ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - C ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - C ) )
171 eqid 
 |-  ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> s ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> s )
172 151 neneqd 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> -. s = 0 )
173 velsn 
 |-  ( s e. { 0 } <-> s = 0 )
174 172 173 sylnibr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> -. s e. { 0 } )
175 141 174 eldifd 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. ( CC \ { 0 } ) )
176 eqid 
 |-  ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( F ` ( X + s ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( F ` ( X + s ) ) )
177 eqid 
 |-  ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> C ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> C )
178 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
179 178 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
180 pire 
 |-  _pi e. RR
181 180 renegcli 
 |-  -u _pi e. RR
182 181 a1i 
 |-  ( ph -> -u _pi e. RR )
183 182 2 readdcld 
 |-  ( ph -> ( -u _pi + X ) e. RR )
184 180 a1i 
 |-  ( ph -> _pi e. RR )
185 184 2 readdcld 
 |-  ( ph -> ( _pi + X ) e. RR )
186 183 185 iccssred 
 |-  ( ph -> ( ( -u _pi + X ) [,] ( _pi + X ) ) C_ RR )
187 186 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( -u _pi + X ) [,] ( _pi + X ) ) C_ RR )
188 3 4 5 fourierdlem15 
 |-  ( ph -> V : ( 0 ... M ) --> ( ( -u _pi + X ) [,] ( _pi + X ) ) )
189 188 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> V : ( 0 ... M ) --> ( ( -u _pi + X ) [,] ( _pi + X ) ) )
190 189 179 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) e. ( ( -u _pi + X ) [,] ( _pi + X ) ) )
191 187 190 sseldd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) e. RR )
192 2 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> X e. RR )
193 191 192 resubcld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` i ) - X ) e. RR )
194 16 fvmpt2 
 |-  ( ( i e. ( 0 ... M ) /\ ( ( V ` i ) - X ) e. RR ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
195 179 193 194 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) = ( ( V ` i ) - X ) )
196 195 193 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
197 196 adantlr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
198 197 adantr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
199 22 198 sylbi 
 |-  ( ch -> ( Q ` i ) e. RR )
200 fveq2 
 |-  ( i = j -> ( V ` i ) = ( V ` j ) )
201 200 oveq1d 
 |-  ( i = j -> ( ( V ` i ) - X ) = ( ( V ` j ) - X ) )
202 201 cbvmptv 
 |-  ( i e. ( 0 ... M ) |-> ( ( V ` i ) - X ) ) = ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) )
203 16 202 eqtri 
 |-  Q = ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) )
204 203 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q = ( j e. ( 0 ... M ) |-> ( ( V ` j ) - X ) ) )
205 fveq2 
 |-  ( j = ( i + 1 ) -> ( V ` j ) = ( V ` ( i + 1 ) ) )
206 205 oveq1d 
 |-  ( j = ( i + 1 ) -> ( ( V ` j ) - X ) = ( ( V ` ( i + 1 ) ) - X ) )
207 206 adantl 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j = ( i + 1 ) ) -> ( ( V ` j ) - X ) = ( ( V ` ( i + 1 ) ) - X ) )
208 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
209 208 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
210 189 209 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` ( i + 1 ) ) e. ( ( -u _pi + X ) [,] ( _pi + X ) ) )
211 187 210 sseldd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` ( i + 1 ) ) e. RR )
212 211 192 resubcld 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` ( i + 1 ) ) - X ) e. RR )
213 204 207 209 212 fvmptd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) )
214 213 212 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
215 214 adantlr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
216 215 adantr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
217 22 216 sylbi 
 |-  ( ch -> ( Q ` ( i + 1 ) ) e. RR )
218 3 fourierdlem2 
 |-  ( M e. NN -> ( V e. ( P ` M ) <-> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u _pi + X ) /\ ( V ` M ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) ) )
219 4 218 syl 
 |-  ( ph -> ( V e. ( P ` M ) <-> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u _pi + X ) /\ ( V ` M ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) ) )
220 5 219 mpbid 
 |-  ( ph -> ( V e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( V ` 0 ) = ( -u _pi + X ) /\ ( V ` M ) = ( _pi + X ) ) /\ A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) ) ) )
221 220 simprrd 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( V ` i ) < ( V ` ( i + 1 ) ) )
222 221 r19.21bi 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( V ` i ) < ( V ` ( i + 1 ) ) )
223 191 211 192 222 ltsub1dd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( V ` i ) - X ) < ( ( V ` ( i + 1 ) ) - X ) )
224 223 195 213 3brtr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
225 224 adantlr 
 |-  ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
226 225 adantr 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
227 22 226 sylbi 
 |-  ( ch -> ( Q ` i ) < ( Q ` ( i + 1 ) ) )
228 22 biimpi 
 |-  ( ch -> ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
229 228 simplrd 
 |-  ( ch -> i e. ( 0 ..^ M ) )
230 27 229 191 syl2anc 
 |-  ( ch -> ( V ` i ) e. RR )
231 230 rexrd 
 |-  ( ch -> ( V ` i ) e. RR* )
232 231 adantr 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` i ) e. RR* )
233 27 229 211 syl2anc 
 |-  ( ch -> ( V ` ( i + 1 ) ) e. RR )
234 233 rexrd 
 |-  ( ch -> ( V ` ( i + 1 ) ) e. RR* )
235 234 adantr 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` ( i + 1 ) ) e. RR* )
236 27 2 syl 
 |-  ( ch -> X e. RR )
237 236 adantr 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> X e. RR )
238 elioore 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s e. RR )
239 238 adantl 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
240 237 239 readdcld 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) e. RR )
241 27 229 195 syl2anc 
 |-  ( ch -> ( Q ` i ) = ( ( V ` i ) - X ) )
242 241 oveq2d 
 |-  ( ch -> ( X + ( Q ` i ) ) = ( X + ( ( V ` i ) - X ) ) )
243 236 recnd 
 |-  ( ch -> X e. CC )
244 230 recnd 
 |-  ( ch -> ( V ` i ) e. CC )
245 243 244 pncan3d 
 |-  ( ch -> ( X + ( ( V ` i ) - X ) ) = ( V ` i ) )
246 242 245 eqtr2d 
 |-  ( ch -> ( V ` i ) = ( X + ( Q ` i ) ) )
247 246 adantr 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` i ) = ( X + ( Q ` i ) ) )
248 199 adantr 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR )
249 199 rexrd 
 |-  ( ch -> ( Q ` i ) e. RR* )
250 249 adantr 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
251 217 rexrd 
 |-  ( ch -> ( Q ` ( i + 1 ) ) e. RR* )
252 251 adantr 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
253 simpr 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
254 ioogtlb 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < s )
255 250 252 253 254 syl3anc 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` i ) < s )
256 248 239 237 255 ltadd2dd 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + ( Q ` i ) ) < ( X + s ) )
257 247 256 eqbrtrd 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( V ` i ) < ( X + s ) )
258 217 adantr 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
259 iooltub 
 |-  ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s < ( Q ` ( i + 1 ) ) )
260 250 252 253 259 syl3anc 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s < ( Q ` ( i + 1 ) ) )
261 239 258 237 260 ltadd2dd 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) < ( X + ( Q ` ( i + 1 ) ) ) )
262 27 229 213 syl2anc 
 |-  ( ch -> ( Q ` ( i + 1 ) ) = ( ( V ` ( i + 1 ) ) - X ) )
263 262 oveq2d 
 |-  ( ch -> ( X + ( Q ` ( i + 1 ) ) ) = ( X + ( ( V ` ( i + 1 ) ) - X ) ) )
264 233 recnd 
 |-  ( ch -> ( V ` ( i + 1 ) ) e. CC )
265 243 264 pncan3d 
 |-  ( ch -> ( X + ( ( V ` ( i + 1 ) ) - X ) ) = ( V ` ( i + 1 ) ) )
266 263 265 eqtrd 
 |-  ( ch -> ( X + ( Q ` ( i + 1 ) ) ) = ( V ` ( i + 1 ) ) )
267 266 adantr 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + ( Q ` ( i + 1 ) ) ) = ( V ` ( i + 1 ) ) )
268 261 267 breqtrd 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) < ( V ` ( i + 1 ) ) )
269 232 235 240 257 268 eliood 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( X + s ) e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
270 fvres 
 |-  ( ( X + s ) e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -> ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` ( X + s ) ) = ( F ` ( X + s ) ) )
271 269 270 syl 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` ( X + s ) ) = ( F ` ( X + s ) ) )
272 271 eqcomd 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( F ` ( X + s ) ) = ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` ( X + s ) ) )
273 272 mpteq2dva 
 |-  ( ch -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` ( X + s ) ) ) )
274 ioosscn 
 |-  ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ CC
275 274 a1i 
 |-  ( ch -> ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ CC )
276 27 229 6 syl2anc 
 |-  ( ch -> ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) e. ( ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) -cn-> CC ) )
277 ioosscn 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC
278 277 a1i 
 |-  ( ch -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ CC )
279 275 276 278 243 269 fourierdlem23 
 |-  ( ch -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` ( X + s ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
280 273 279 eqeltrd 
 |-  ( ch -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
281 27 1 syl 
 |-  ( ch -> F : RR --> RR )
282 ioossre 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
283 282 a1i 
 |-  ( ch -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
284 eqid 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) )
285 ioossre 
 |-  ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ RR
286 285 a1i 
 |-  ( ch -> ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) C_ RR )
287 239 260 ltned 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s =/= ( Q ` ( i + 1 ) ) )
288 27 229 8 syl2anc 
 |-  ( ch -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` ( i + 1 ) ) ) )
289 266 eqcomd 
 |-  ( ch -> ( V ` ( i + 1 ) ) = ( X + ( Q ` ( i + 1 ) ) ) )
290 289 oveq2d 
 |-  ( ch -> ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` ( i + 1 ) ) ) = ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( X + ( Q ` ( i + 1 ) ) ) ) )
291 288 290 eleqtrd 
 |-  ( ch -> L e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( X + ( Q ` ( i + 1 ) ) ) ) )
292 217 recnd 
 |-  ( ch -> ( Q ` ( i + 1 ) ) e. CC )
293 281 236 283 284 269 286 287 291 292 fourierdlem53 
 |-  ( ch -> L e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
294 64 69 ffvelcdmd 
 |-  ( ch -> ( S ` j ) e. RR )
295 elfzoelz 
 |-  ( j e. ( 0 ..^ N ) -> j e. ZZ )
296 zre 
 |-  ( j e. ZZ -> j e. RR )
297 67 295 296 3syl 
 |-  ( ch -> j e. RR )
298 297 ltp1d 
 |-  ( ch -> j < ( j + 1 ) )
299 isorel 
 |-  ( ( S Isom < , < ( ( 0 ... N ) , T ) /\ ( j e. ( 0 ... N ) /\ ( j + 1 ) e. ( 0 ... N ) ) ) -> ( j < ( j + 1 ) <-> ( S ` j ) < ( S ` ( j + 1 ) ) ) )
300 59 69 103 299 syl12anc 
 |-  ( ch -> ( j < ( j + 1 ) <-> ( S ` j ) < ( S ` ( j + 1 ) ) ) )
301 298 300 mpbid 
 |-  ( ch -> ( S ` j ) < ( S ` ( j + 1 ) ) )
302 22 simprbi 
 |-  ( ch -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
303 eqid 
 |-  if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` ( j + 1 ) ) ) ) = if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` ( j + 1 ) ) ) )
304 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) u. { ( Q ` ( i + 1 ) ) } ) )
305 199 217 227 280 293 294 104 301 302 303 304 fourierdlem33 
 |-  ( ch -> if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` ( j + 1 ) ) ) ) e. ( ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) )
306 eqidd 
 |-  ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) )
307 simpr 
 |-  ( ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) /\ s = ( S ` ( j + 1 ) ) ) -> s = ( S ` ( j + 1 ) ) )
308 307 oveq2d 
 |-  ( ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) /\ s = ( S ` ( j + 1 ) ) ) -> ( X + s ) = ( X + ( S ` ( j + 1 ) ) ) )
309 308 fveq2d 
 |-  ( ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) /\ s = ( S ` ( j + 1 ) ) ) -> ( F ` ( X + s ) ) = ( F ` ( X + ( S ` ( j + 1 ) ) ) ) )
310 249 adantr 
 |-  ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) e. RR* )
311 251 adantr 
 |-  ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
312 104 adantr 
 |-  ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( S ` ( j + 1 ) ) e. RR )
313 199 217 294 104 301 302 fourierdlem10 
 |-  ( ch -> ( ( Q ` i ) <_ ( S ` j ) /\ ( S ` ( j + 1 ) ) <_ ( Q ` ( i + 1 ) ) ) )
314 313 simpld 
 |-  ( ch -> ( Q ` i ) <_ ( S ` j ) )
315 199 294 104 314 301 lelttrd 
 |-  ( ch -> ( Q ` i ) < ( S ` ( j + 1 ) ) )
316 315 adantr 
 |-  ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( Q ` i ) < ( S ` ( j + 1 ) ) )
317 217 adantr 
 |-  ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
318 313 simprd 
 |-  ( ch -> ( S ` ( j + 1 ) ) <_ ( Q ` ( i + 1 ) ) )
319 318 adantr 
 |-  ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( S ` ( j + 1 ) ) <_ ( Q ` ( i + 1 ) ) )
320 neqne 
 |-  ( -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) -> ( S ` ( j + 1 ) ) =/= ( Q ` ( i + 1 ) ) )
321 320 necomd 
 |-  ( -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) -> ( Q ` ( i + 1 ) ) =/= ( S ` ( j + 1 ) ) )
322 321 adantl 
 |-  ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( Q ` ( i + 1 ) ) =/= ( S ` ( j + 1 ) ) )
323 312 317 319 322 leneltd 
 |-  ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( S ` ( j + 1 ) ) < ( Q ` ( i + 1 ) ) )
324 310 311 312 316 323 eliood 
 |-  ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( S ` ( j + 1 ) ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
325 236 104 readdcld 
 |-  ( ch -> ( X + ( S ` ( j + 1 ) ) ) e. RR )
326 281 325 ffvelcdmd 
 |-  ( ch -> ( F ` ( X + ( S ` ( j + 1 ) ) ) ) e. RR )
327 326 adantr 
 |-  ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( F ` ( X + ( S ` ( j + 1 ) ) ) ) e. RR )
328 306 309 324 327 fvmptd 
 |-  ( ( ch /\ -. ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` ( j + 1 ) ) ) = ( F ` ( X + ( S ` ( j + 1 ) ) ) ) )
329 328 ifeq2da 
 |-  ( ch -> if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` ( j + 1 ) ) ) ) = if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) )
330 302 resmptd 
 |-  ( ch -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( F ` ( X + s ) ) ) )
331 330 oveq1d 
 |-  ( ch -> ( ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) = ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( F ` ( X + s ) ) ) limCC ( S ` ( j + 1 ) ) ) )
332 305 329 331 3eltr3d 
 |-  ( ch -> if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( F ` ( X + s ) ) ) limCC ( S ` ( j + 1 ) ) ) )
333 ax-resscn 
 |-  RR C_ CC
334 139 333 sstrdi 
 |-  ( ch -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ CC )
335 104 recnd 
 |-  ( ch -> ( S ` ( j + 1 ) ) e. CC )
336 177 334 135 335 constlimc 
 |-  ( ch -> C e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> C ) limCC ( S ` ( j + 1 ) ) ) )
337 176 177 170 133 136 332 336 sublimc 
 |-  ( ch -> ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - C ) ) limCC ( S ` ( j + 1 ) ) ) )
338 334 171 335 idlimc 
 |-  ( ch -> ( S ` ( j + 1 ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> s ) limCC ( S ` ( j + 1 ) ) ) )
339 27 119 jca 
 |-  ( ch -> ( ph /\ ( S ` ( j + 1 ) ) e. ( A [,] B ) ) )
340 eleq1 
 |-  ( s = ( S ` ( j + 1 ) ) -> ( s e. ( A [,] B ) <-> ( S ` ( j + 1 ) ) e. ( A [,] B ) ) )
341 340 anbi2d 
 |-  ( s = ( S ` ( j + 1 ) ) -> ( ( ph /\ s e. ( A [,] B ) ) <-> ( ph /\ ( S ` ( j + 1 ) ) e. ( A [,] B ) ) ) )
342 neeq1 
 |-  ( s = ( S ` ( j + 1 ) ) -> ( s =/= 0 <-> ( S ` ( j + 1 ) ) =/= 0 ) )
343 341 342 imbi12d 
 |-  ( s = ( S ` ( j + 1 ) ) -> ( ( ( ph /\ s e. ( A [,] B ) ) -> s =/= 0 ) <-> ( ( ph /\ ( S ` ( j + 1 ) ) e. ( A [,] B ) ) -> ( S ` ( j + 1 ) ) =/= 0 ) ) )
344 343 150 vtoclg 
 |-  ( ( S ` ( j + 1 ) ) e. RR -> ( ( ph /\ ( S ` ( j + 1 ) ) e. ( A [,] B ) ) -> ( S ` ( j + 1 ) ) =/= 0 ) )
345 104 339 344 sylc 
 |-  ( ch -> ( S ` ( j + 1 ) ) =/= 0 )
346 170 171 23 137 175 337 338 345 151 divlimc 
 |-  ( ch -> ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / s ) ) limCC ( S ` ( j + 1 ) ) ) )
347 eqid 
 |-  ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) )
348 153 160 mulcld 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
349 168 neneqd 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> -. ( 2 x. ( sin ` ( s / 2 ) ) ) = 0 )
350 2re 
 |-  2 e. RR
351 350 a1i 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> 2 e. RR )
352 36 rehalfcld 
 |-  ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> ( s / 2 ) e. RR )
353 352 resincld 
 |-  ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -> ( sin ` ( s / 2 ) ) e. RR )
354 353 adantl 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( sin ` ( s / 2 ) ) e. RR )
355 351 354 remulcld 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. RR )
356 elsng 
 |-  ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. RR -> ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. { 0 } <-> ( 2 x. ( sin ` ( s / 2 ) ) ) = 0 ) )
357 355 356 syl 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. { 0 } <-> ( 2 x. ( sin ` ( s / 2 ) ) ) = 0 ) )
358 349 357 mtbird 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> -. ( 2 x. ( sin ` ( s / 2 ) ) ) e. { 0 } )
359 348 358 eldifd 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. ( CC \ { 0 } ) )
360 eqid 
 |-  ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> 2 ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> 2 )
361 eqid 
 |-  ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( sin ` ( s / 2 ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( sin ` ( s / 2 ) ) )
362 2cnd 
 |-  ( ch -> 2 e. CC )
363 360 334 362 335 constlimc 
 |-  ( ch -> 2 e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> 2 ) limCC ( S ` ( j + 1 ) ) ) )
364 352 ad2antrl 
 |-  ( ( ch /\ ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) /\ ( s / 2 ) =/= ( ( S ` ( j + 1 ) ) / 2 ) ) ) -> ( s / 2 ) e. RR )
365 recn 
 |-  ( x e. RR -> x e. CC )
366 365 sincld 
 |-  ( x e. RR -> ( sin ` x ) e. CC )
367 366 adantl 
 |-  ( ( ch /\ x e. RR ) -> ( sin ` x ) e. CC )
368 eqid 
 |-  ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( s / 2 ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( s / 2 ) )
369 2cn 
 |-  2 e. CC
370 eldifsn 
 |-  ( 2 e. ( CC \ { 0 } ) <-> ( 2 e. CC /\ 2 =/= 0 ) )
371 369 161 370 mpbir2an 
 |-  2 e. ( CC \ { 0 } )
372 371 a1i 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> 2 e. ( CC \ { 0 } ) )
373 161 a1i 
 |-  ( ch -> 2 =/= 0 )
374 171 360 368 158 372 338 363 373 162 divlimc 
 |-  ( ch -> ( ( S ` ( j + 1 ) ) / 2 ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( s / 2 ) ) limCC ( S ` ( j + 1 ) ) ) )
375 sinf 
 |-  sin : CC --> CC
376 375 a1i 
 |-  ( T. -> sin : CC --> CC )
377 333 a1i 
 |-  ( T. -> RR C_ CC )
378 376 377 feqresmpt 
 |-  ( T. -> ( sin |` RR ) = ( x e. RR |-> ( sin ` x ) ) )
379 378 mptru 
 |-  ( sin |` RR ) = ( x e. RR |-> ( sin ` x ) )
380 resincncf 
 |-  ( sin |` RR ) e. ( RR -cn-> RR )
381 379 380 eqeltrri 
 |-  ( x e. RR |-> ( sin ` x ) ) e. ( RR -cn-> RR )
382 381 a1i 
 |-  ( ch -> ( x e. RR |-> ( sin ` x ) ) e. ( RR -cn-> RR ) )
383 104 rehalfcld 
 |-  ( ch -> ( ( S ` ( j + 1 ) ) / 2 ) e. RR )
384 fveq2 
 |-  ( x = ( ( S ` ( j + 1 ) ) / 2 ) -> ( sin ` x ) = ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) )
385 382 383 384 cnmptlimc 
 |-  ( ch -> ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) e. ( ( x e. RR |-> ( sin ` x ) ) limCC ( ( S ` ( j + 1 ) ) / 2 ) ) )
386 fveq2 
 |-  ( x = ( s / 2 ) -> ( sin ` x ) = ( sin ` ( s / 2 ) ) )
387 fveq2 
 |-  ( ( s / 2 ) = ( ( S ` ( j + 1 ) ) / 2 ) -> ( sin ` ( s / 2 ) ) = ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) )
388 387 ad2antll 
 |-  ( ( ch /\ ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) /\ ( s / 2 ) = ( ( S ` ( j + 1 ) ) / 2 ) ) ) -> ( sin ` ( s / 2 ) ) = ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) )
389 364 367 374 385 386 388 limcco 
 |-  ( ch -> ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( sin ` ( s / 2 ) ) ) limCC ( S ` ( j + 1 ) ) ) )
390 360 361 347 153 160 363 389 mullimc 
 |-  ( ch -> ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) )
391 335 halfcld 
 |-  ( ch -> ( ( S ` ( j + 1 ) ) / 2 ) e. CC )
392 391 sincld 
 |-  ( ch -> ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) e. CC )
393 163 119 sseldd 
 |-  ( ch -> ( S ` ( j + 1 ) ) e. ( -u _pi [,] _pi ) )
394 fourierdlem44 
 |-  ( ( ( S ` ( j + 1 ) ) e. ( -u _pi [,] _pi ) /\ ( S ` ( j + 1 ) ) =/= 0 ) -> ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) =/= 0 )
395 393 345 394 syl2anc 
 |-  ( ch -> ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) =/= 0 )
396 362 392 373 395 mulne0d 
 |-  ( ch -> ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) =/= 0 )
397 171 347 24 158 359 338 390 396 168 divlimc 
 |-  ( ch -> ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) limCC ( S ` ( j + 1 ) ) ) )
398 23 24 25 152 169 346 397 mullimc 
 |-  ( ch -> ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC ( S ` ( j + 1 ) ) ) )
399 20 a1i 
 |-  ( ch -> D = ( ( ( if ( ( S ` ( j + 1 ) ) = ( Q ` ( i + 1 ) ) , L , ( F ` ( X + ( S ` ( j + 1 ) ) ) ) ) - C ) / ( S ` ( j + 1 ) ) ) x. ( ( S ` ( j + 1 ) ) / ( 2 x. ( sin ` ( ( S ` ( j + 1 ) ) / 2 ) ) ) ) ) )
400 15 reseq1i 
 |-  ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( ( s e. ( A [,] B ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) )
401 ioossicc 
 |-  ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( S ` j ) [,] ( S ` ( j + 1 ) ) )
402 iccss 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( A <_ ( S ` j ) /\ ( S ` ( j + 1 ) ) <_ B ) ) -> ( ( S ` j ) [,] ( S ` ( j + 1 ) ) ) C_ ( A [,] B ) )
403 38 112 99 121 402 syl22anc 
 |-  ( ch -> ( ( S ` j ) [,] ( S ` ( j + 1 ) ) ) C_ ( A [,] B ) )
404 401 403 sstrid 
 |-  ( ch -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( A [,] B ) )
405 404 resmptd 
 |-  ( ch -> ( ( s e. ( A [,] B ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
406 400 405 eqtrid 
 |-  ( ch -> ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
407 406 oveq1d 
 |-  ( ch -> ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) = ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC ( S ` ( j + 1 ) ) ) )
408 398 399 407 3eltr4d 
 |-  ( ch -> D e. ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) )
409 22 408 sylbir 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> D e. ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) )
410 248 255 gtned 
 |-  ( ( ch /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s =/= ( Q ` i ) )
411 27 229 7 syl2anc 
 |-  ( ch -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` i ) ) )
412 246 oveq2d 
 |-  ( ch -> ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( V ` i ) ) = ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( X + ( Q ` i ) ) ) )
413 411 412 eleqtrd 
 |-  ( ch -> R e. ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) limCC ( X + ( Q ` i ) ) ) )
414 199 recnd 
 |-  ( ch -> ( Q ` i ) e. CC )
415 281 236 283 284 269 286 410 413 414 fourierdlem53 
 |-  ( ch -> R e. ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) limCC ( Q ` i ) ) )
416 eqid 
 |-  if ( ( S ` j ) = ( Q ` i ) , R , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` j ) ) ) = if ( ( S ` j ) = ( Q ` i ) , R , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` j ) ) )
417 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) ) = ( ( TopOpen ` CCfld ) |`t ( ( Q ` i ) [,) ( Q ` ( i + 1 ) ) ) )
418 199 217 227 280 415 294 104 301 302 416 417 fourierdlem32 
 |-  ( ch -> if ( ( S ` j ) = ( Q ` i ) , R , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` j ) ) ) e. ( ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) )
419 eqidd 
 |-  ( ( ch /\ -. ( S ` j ) = ( Q ` i ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) )
420 oveq2 
 |-  ( s = ( S ` j ) -> ( X + s ) = ( X + ( S ` j ) ) )
421 420 fveq2d 
 |-  ( s = ( S ` j ) -> ( F ` ( X + s ) ) = ( F ` ( X + ( S ` j ) ) ) )
422 421 adantl 
 |-  ( ( ( ch /\ -. ( S ` j ) = ( Q ` i ) ) /\ s = ( S ` j ) ) -> ( F ` ( X + s ) ) = ( F ` ( X + ( S ` j ) ) ) )
423 249 adantr 
 |-  ( ( ch /\ -. ( S ` j ) = ( Q ` i ) ) -> ( Q ` i ) e. RR* )
424 251 adantr 
 |-  ( ( ch /\ -. ( S ` j ) = ( Q ` i ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
425 294 adantr 
 |-  ( ( ch /\ -. ( S ` j ) = ( Q ` i ) ) -> ( S ` j ) e. RR )
426 199 adantr 
 |-  ( ( ch /\ -. ( S ` j ) = ( Q ` i ) ) -> ( Q ` i ) e. RR )
427 314 adantr 
 |-  ( ( ch /\ -. ( S ` j ) = ( Q ` i ) ) -> ( Q ` i ) <_ ( S ` j ) )
428 neqne 
 |-  ( -. ( S ` j ) = ( Q ` i ) -> ( S ` j ) =/= ( Q ` i ) )
429 428 adantl 
 |-  ( ( ch /\ -. ( S ` j ) = ( Q ` i ) ) -> ( S ` j ) =/= ( Q ` i ) )
430 426 425 427 429 leneltd 
 |-  ( ( ch /\ -. ( S ` j ) = ( Q ` i ) ) -> ( Q ` i ) < ( S ` j ) )
431 104 adantr 
 |-  ( ( ch /\ -. ( S ` j ) = ( Q ` i ) ) -> ( S ` ( j + 1 ) ) e. RR )
432 217 adantr 
 |-  ( ( ch /\ -. ( S ` j ) = ( Q ` i ) ) -> ( Q ` ( i + 1 ) ) e. RR )
433 301 adantr 
 |-  ( ( ch /\ -. ( S ` j ) = ( Q ` i ) ) -> ( S ` j ) < ( S ` ( j + 1 ) ) )
434 318 adantr 
 |-  ( ( ch /\ -. ( S ` j ) = ( Q ` i ) ) -> ( S ` ( j + 1 ) ) <_ ( Q ` ( i + 1 ) ) )
435 425 431 432 433 434 ltletrd 
 |-  ( ( ch /\ -. ( S ` j ) = ( Q ` i ) ) -> ( S ` j ) < ( Q ` ( i + 1 ) ) )
436 423 424 425 430 435 eliood 
 |-  ( ( ch /\ -. ( S ` j ) = ( Q ` i ) ) -> ( S ` j ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
437 236 294 readdcld 
 |-  ( ch -> ( X + ( S ` j ) ) e. RR )
438 281 437 ffvelcdmd 
 |-  ( ch -> ( F ` ( X + ( S ` j ) ) ) e. RR )
439 438 adantr 
 |-  ( ( ch /\ -. ( S ` j ) = ( Q ` i ) ) -> ( F ` ( X + ( S ` j ) ) ) e. RR )
440 419 422 436 439 fvmptd 
 |-  ( ( ch /\ -. ( S ` j ) = ( Q ` i ) ) -> ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` j ) ) = ( F ` ( X + ( S ` j ) ) ) )
441 440 ifeq2da 
 |-  ( ch -> if ( ( S ` j ) = ( Q ` i ) , R , ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) ` ( S ` j ) ) ) = if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) )
442 330 oveq1d 
 |-  ( ch -> ( ( ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( F ` ( X + s ) ) ) |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) = ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( F ` ( X + s ) ) ) limCC ( S ` j ) ) )
443 418 441 442 3eltr3d 
 |-  ( ch -> if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( F ` ( X + s ) ) ) limCC ( S ` j ) ) )
444 294 recnd 
 |-  ( ch -> ( S ` j ) e. CC )
445 177 334 135 444 constlimc 
 |-  ( ch -> C e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> C ) limCC ( S ` j ) ) )
446 176 177 170 133 136 443 445 sublimc 
 |-  ( ch -> ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - C ) ) limCC ( S ` j ) ) )
447 334 171 444 idlimc 
 |-  ( ch -> ( S ` j ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> s ) limCC ( S ` j ) ) )
448 27 97 jca 
 |-  ( ch -> ( ph /\ ( S ` j ) e. ( A [,] B ) ) )
449 eleq1 
 |-  ( s = ( S ` j ) -> ( s e. ( A [,] B ) <-> ( S ` j ) e. ( A [,] B ) ) )
450 449 anbi2d 
 |-  ( s = ( S ` j ) -> ( ( ph /\ s e. ( A [,] B ) ) <-> ( ph /\ ( S ` j ) e. ( A [,] B ) ) ) )
451 neeq1 
 |-  ( s = ( S ` j ) -> ( s =/= 0 <-> ( S ` j ) =/= 0 ) )
452 450 451 imbi12d 
 |-  ( s = ( S ` j ) -> ( ( ( ph /\ s e. ( A [,] B ) ) -> s =/= 0 ) <-> ( ( ph /\ ( S ` j ) e. ( A [,] B ) ) -> ( S ` j ) =/= 0 ) ) )
453 452 150 vtoclg 
 |-  ( ( S ` j ) e. ( A [,] B ) -> ( ( ph /\ ( S ` j ) e. ( A [,] B ) ) -> ( S ` j ) =/= 0 ) )
454 97 448 453 sylc 
 |-  ( ch -> ( S ` j ) =/= 0 )
455 170 171 23 137 175 446 447 454 151 divlimc 
 |-  ( ch -> ( ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / s ) ) limCC ( S ` j ) ) )
456 360 334 362 444 constlimc 
 |-  ( ch -> 2 e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> 2 ) limCC ( S ` j ) ) )
457 352 ad2antrl 
 |-  ( ( ch /\ ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) /\ ( s / 2 ) =/= ( ( S ` j ) / 2 ) ) ) -> ( s / 2 ) e. RR )
458 171 360 368 158 372 447 456 373 162 divlimc 
 |-  ( ch -> ( ( S ` j ) / 2 ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( s / 2 ) ) limCC ( S ` j ) ) )
459 294 rehalfcld 
 |-  ( ch -> ( ( S ` j ) / 2 ) e. RR )
460 fveq2 
 |-  ( x = ( ( S ` j ) / 2 ) -> ( sin ` x ) = ( sin ` ( ( S ` j ) / 2 ) ) )
461 382 459 460 cnmptlimc 
 |-  ( ch -> ( sin ` ( ( S ` j ) / 2 ) ) e. ( ( x e. RR |-> ( sin ` x ) ) limCC ( ( S ` j ) / 2 ) ) )
462 fveq2 
 |-  ( ( s / 2 ) = ( ( S ` j ) / 2 ) -> ( sin ` ( s / 2 ) ) = ( sin ` ( ( S ` j ) / 2 ) ) )
463 462 ad2antll 
 |-  ( ( ch /\ ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) /\ ( s / 2 ) = ( ( S ` j ) / 2 ) ) ) -> ( sin ` ( s / 2 ) ) = ( sin ` ( ( S ` j ) / 2 ) ) )
464 457 367 458 461 386 463 limcco 
 |-  ( ch -> ( sin ` ( ( S ` j ) / 2 ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( sin ` ( s / 2 ) ) ) limCC ( S ` j ) ) )
465 360 361 347 153 160 456 464 mullimc 
 |-  ( ch -> ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) limCC ( S ` j ) ) )
466 444 halfcld 
 |-  ( ch -> ( ( S ` j ) / 2 ) e. CC )
467 466 sincld 
 |-  ( ch -> ( sin ` ( ( S ` j ) / 2 ) ) e. CC )
468 163 97 sseldd 
 |-  ( ch -> ( S ` j ) e. ( -u _pi [,] _pi ) )
469 fourierdlem44 
 |-  ( ( ( S ` j ) e. ( -u _pi [,] _pi ) /\ ( S ` j ) =/= 0 ) -> ( sin ` ( ( S ` j ) / 2 ) ) =/= 0 )
470 468 454 469 syl2anc 
 |-  ( ch -> ( sin ` ( ( S ` j ) / 2 ) ) =/= 0 )
471 362 467 373 470 mulne0d 
 |-  ( ch -> ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) =/= 0 )
472 171 347 24 158 359 447 465 471 168 divlimc 
 |-  ( ch -> ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) limCC ( S ` j ) ) )
473 23 24 25 152 169 455 472 mullimc 
 |-  ( ch -> ( ( ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) e. ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC ( S ` j ) ) )
474 21 a1i 
 |-  ( ch -> E = ( ( ( if ( ( S ` j ) = ( Q ` i ) , R , ( F ` ( X + ( S ` j ) ) ) ) - C ) / ( S ` j ) ) x. ( ( S ` j ) / ( 2 x. ( sin ` ( ( S ` j ) / 2 ) ) ) ) ) )
475 406 oveq1d 
 |-  ( ch -> ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) = ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC ( S ` j ) ) )
476 473 474 475 3eltr4d 
 |-  ( ch -> E e. ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) )
477 22 476 sylbir 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> E e. ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) )
478 302 sselda 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
479 478 272 syldan 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( F ` ( X + s ) ) = ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` ( X + s ) ) )
480 479 mpteq2dva 
 |-  ( ch -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( F ` ( X + s ) ) ) = ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` ( X + s ) ) ) )
481 231 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( V ` i ) e. RR* )
482 234 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( V ` ( i + 1 ) ) e. RR* )
483 236 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> X e. RR )
484 483 140 readdcld 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( X + s ) e. RR )
485 246 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( V ` i ) = ( X + ( Q ` i ) ) )
486 199 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( Q ` i ) e. RR )
487 249 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( Q ` i ) e. RR* )
488 251 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
489 487 488 478 254 syl3anc 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( Q ` i ) < s )
490 486 37 483 489 ltadd2dd 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( X + ( Q ` i ) ) < ( X + s ) )
491 485 490 eqbrtrd 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( V ` i ) < ( X + s ) )
492 217 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
493 487 488 478 259 syl3anc 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> s < ( Q ` ( i + 1 ) ) )
494 37 492 483 493 ltadd2dd 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( X + s ) < ( X + ( Q ` ( i + 1 ) ) ) )
495 266 adantr 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( X + ( Q ` ( i + 1 ) ) ) = ( V ` ( i + 1 ) ) )
496 494 495 breqtrd 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( X + s ) < ( V ` ( i + 1 ) ) )
497 481 482 484 491 496 eliood 
 |-  ( ( ch /\ s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) -> ( X + s ) e. ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) )
498 275 276 334 243 497 fourierdlem23 
 |-  ( ch -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( F |` ( ( V ` i ) (,) ( V ` ( i + 1 ) ) ) ) ` ( X + s ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
499 480 498 eqeltrd 
 |-  ( ch -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( F ` ( X + s ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
500 ssid 
 |-  CC C_ CC
501 500 a1i 
 |-  ( ch -> CC C_ CC )
502 334 135 501 constcncfg 
 |-  ( ch -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> C ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
503 499 502 subcncf 
 |-  ( ch -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( F ` ( X + s ) ) - C ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
504 175 ralrimiva 
 |-  ( ch -> A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) s e. ( CC \ { 0 } ) )
505 dfss3 
 |-  ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( CC \ { 0 } ) <-> A. s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) s e. ( CC \ { 0 } ) )
506 504 505 sylibr 
 |-  ( ch -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( CC \ { 0 } ) )
507 difssd 
 |-  ( ch -> ( CC \ { 0 } ) C_ CC )
508 506 507 idcncfg 
 |-  ( ch -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> s ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> ( CC \ { 0 } ) ) )
509 503 508 divcncf 
 |-  ( ch -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( F ` ( X + s ) ) - C ) / s ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
510 334 501 idcncfg 
 |-  ( ch -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> s ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
511 359 347 fmptd 
 |-  ( ch -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) --> ( CC \ { 0 } ) )
512 334 362 501 constcncfg 
 |-  ( ch -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> 2 ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
513 sincn 
 |-  sin e. ( CC -cn-> CC )
514 513 a1i 
 |-  ( ch -> sin e. ( CC -cn-> CC ) )
515 371 a1i 
 |-  ( ch -> 2 e. ( CC \ { 0 } ) )
516 334 515 507 constcncfg 
 |-  ( ch -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> 2 ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> ( CC \ { 0 } ) ) )
517 510 516 divcncf 
 |-  ( ch -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( s / 2 ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
518 514 517 cncfmpt1f 
 |-  ( ch -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( sin ` ( s / 2 ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
519 512 518 mulcncf 
 |-  ( ch -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
520 cncfcdm 
 |-  ( ( ( CC \ { 0 } ) C_ CC /\ ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) ) -> ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> ( CC \ { 0 } ) ) <-> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) --> ( CC \ { 0 } ) ) )
521 507 519 520 syl2anc 
 |-  ( ch -> ( ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> ( CC \ { 0 } ) ) <-> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) --> ( CC \ { 0 } ) ) )
522 511 521 mpbird 
 |-  ( ch -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> ( CC \ { 0 } ) ) )
523 510 522 divcncf 
 |-  ( ch -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
524 509 523 mulcncf 
 |-  ( ch -> ( s e. ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) |-> ( ( ( ( F ` ( X + s ) ) - C ) / s ) x. ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
525 406 524 eqeltrd 
 |-  ( ch -> ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
526 22 525 sylbir 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
527 409 477 526 jca31 
 |-  ( ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) /\ ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( ( D e. ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) /\ E e. ( ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) ) /\ ( O |` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) ) )