Metamath Proof Explorer

Theorem sqwvfourb

Description: Fourier series B coefficients for the square wave function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses sqwvfourb.t 
|- T = ( 2 x. _pi )
sqwvfourb.f 
|- F = ( x e. RR |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) )
sqwvfourb.n 
|- ( ph -> N e. NN )
Assertion sqwvfourb 
|- ( ph -> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x / _pi ) = if ( 2 || N , 0 , ( 4 / ( N x. _pi ) ) ) )

Proof

Step Hyp Ref Expression
1 sqwvfourb.t 
 |-  T = ( 2 x. _pi )
2 sqwvfourb.f 
 |-  F = ( x e. RR |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) )
3 sqwvfourb.n 
 |-  ( ph -> N e. NN )
4 pire 
 |-  _pi e. RR
5 4 renegcli 
 |-  -u _pi e. RR
6 5 a1i 
 |-  ( ph -> -u _pi e. RR )
7 4 a1i 
 |-  ( ph -> _pi e. RR )
8 0re 
 |-  0 e. RR
9 negpilt0 
 |-  -u _pi < 0
10 5 8 9 ltleii 
 |-  -u _pi <_ 0
11 pipos 
 |-  0 < _pi
12 8 4 11 ltleii 
 |-  0 <_ _pi
13 5 4 elicc2i 
 |-  ( 0 e. ( -u _pi [,] _pi ) <-> ( 0 e. RR /\ -u _pi <_ 0 /\ 0 <_ _pi ) )
14 8 10 12 13 mpbir3an 
 |-  0 e. ( -u _pi [,] _pi )
15 14 a1i 
 |-  ( ph -> 0 e. ( -u _pi [,] _pi ) )
16 elioore 
 |-  ( x e. ( -u _pi (,) _pi ) -> x e. RR )
17 16 adantl 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> x e. RR )
18 1re 
 |-  1 e. RR
19 18 renegcli 
 |-  -u 1 e. RR
20 18 19 ifcli 
 |-  if ( ( x mod T ) < _pi , 1 , -u 1 ) e. RR
21 2 fvmpt2 
 |-  ( ( x e. RR /\ if ( ( x mod T ) < _pi , 1 , -u 1 ) e. RR ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
22 17 20 21 sylancl 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
23 20 a1i 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> if ( ( x mod T ) < _pi , 1 , -u 1 ) e. RR )
24 23 recnd 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> if ( ( x mod T ) < _pi , 1 , -u 1 ) e. CC )
25 22 24 eqeltrd 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> ( F ` x ) e. CC )
26 3 nncnd 
 |-  ( ph -> N e. CC )
27 26 adantr 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> N e. CC )
28 17 recnd 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> x e. CC )
29 27 28 mulcld 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> ( N x. x ) e. CC )
30 29 sincld 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> ( sin ` ( N x. x ) ) e. CC )
31 25 30 mulcld 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) e. CC )
32 elioore 
 |-  ( x e. ( -u _pi (,) 0 ) -> x e. RR )
33 32 20 21 sylancl 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
34 4 a1i 
 |-  ( x e. ( -u _pi (,) 0 ) -> _pi e. RR )
35 2rp 
 |-  2 e. RR+
36 pirp 
 |-  _pi e. RR+
37 rpmulcl 
 |-  ( ( 2 e. RR+ /\ _pi e. RR+ ) -> ( 2 x. _pi ) e. RR+ )
38 35 36 37 mp2an 
 |-  ( 2 x. _pi ) e. RR+
39 1 38 eqeltri 
 |-  T e. RR+
40 39 a1i 
 |-  ( x e. ( -u _pi (,) 0 ) -> T e. RR+ )
41 32 40 modcld 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( x mod T ) e. RR )
42 picn 
 |-  _pi e. CC
43 42 2timesi 
 |-  ( 2 x. _pi ) = ( _pi + _pi )
44 1 43 eqtri 
 |-  T = ( _pi + _pi )
45 44 oveq2i 
 |-  ( -u _pi + T ) = ( -u _pi + ( _pi + _pi ) )
46 5 recni 
 |-  -u _pi e. CC
47 46 42 42 addassi 
 |-  ( ( -u _pi + _pi ) + _pi ) = ( -u _pi + ( _pi + _pi ) )
48 42 negidi 
 |-  ( _pi + -u _pi ) = 0
49 42 46 48 addcomli 
 |-  ( -u _pi + _pi ) = 0
50 49 oveq1i 
 |-  ( ( -u _pi + _pi ) + _pi ) = ( 0 + _pi )
51 42 addid2i 
 |-  ( 0 + _pi ) = _pi
52 50 51 eqtri 
 |-  ( ( -u _pi + _pi ) + _pi ) = _pi
53 45 47 52 3eqtr2ri 
 |-  _pi = ( -u _pi + T )
54 53 a1i 
 |-  ( x e. ( -u _pi (,) 0 ) -> _pi = ( -u _pi + T ) )
55 5 a1i 
 |-  ( x e. ( -u _pi (,) 0 ) -> -u _pi e. RR )
56 2re 
 |-  2 e. RR
57 56 4 remulcli 
 |-  ( 2 x. _pi ) e. RR
58 1 57 eqeltri 
 |-  T e. RR
59 58 a1i 
 |-  ( x e. ( -u _pi (,) 0 ) -> T e. RR )
60 5 rexri 
 |-  -u _pi e. RR*
61 0xr 
 |-  0 e. RR*
62 ioogtlb 
 |-  ( ( -u _pi e. RR* /\ 0 e. RR* /\ x e. ( -u _pi (,) 0 ) ) -> -u _pi < x )
63 60 61 62 mp3an12 
 |-  ( x e. ( -u _pi (,) 0 ) -> -u _pi < x )
64 55 32 59 63 ltadd1dd 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( -u _pi + T ) < ( x + T ) )
65 54 64 eqbrtrd 
 |-  ( x e. ( -u _pi (,) 0 ) -> _pi < ( x + T ) )
66 58 recni 
 |-  T e. CC
67 66 mulid2i 
 |-  ( 1 x. T ) = T
68 67 eqcomi 
 |-  T = ( 1 x. T )
69 68 oveq2i 
 |-  ( x + T ) = ( x + ( 1 x. T ) )
70 69 oveq1i 
 |-  ( ( x + T ) mod T ) = ( ( x + ( 1 x. T ) ) mod T )
71 32 59 readdcld 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( x + T ) e. RR )
72 0red 
 |-  ( x e. ( -u _pi (,) 0 ) -> 0 e. RR )
73 11 a1i 
 |-  ( x e. ( -u _pi (,) 0 ) -> 0 < _pi )
74 72 34 71 73 65 lttrd 
 |-  ( x e. ( -u _pi (,) 0 ) -> 0 < ( x + T ) )
75 72 71 74 ltled 
 |-  ( x e. ( -u _pi (,) 0 ) -> 0 <_ ( x + T ) )
76 iooltub 
 |-  ( ( -u _pi e. RR* /\ 0 e. RR* /\ x e. ( -u _pi (,) 0 ) ) -> x < 0 )
77 60 61 76 mp3an12 
 |-  ( x e. ( -u _pi (,) 0 ) -> x < 0 )
78 32 72 59 77 ltadd1dd 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( x + T ) < ( 0 + T ) )
79 59 recnd 
 |-  ( x e. ( -u _pi (,) 0 ) -> T e. CC )
80 79 addid2d 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( 0 + T ) = T )
81 78 80 breqtrd 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( x + T ) < T )
82 modid 
 |-  ( ( ( ( x + T ) e. RR /\ T e. RR+ ) /\ ( 0 <_ ( x + T ) /\ ( x + T ) < T ) ) -> ( ( x + T ) mod T ) = ( x + T ) )
83 71 40 75 81 82 syl22anc 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( ( x + T ) mod T ) = ( x + T ) )
84 1zzd 
 |-  ( x e. ( -u _pi (,) 0 ) -> 1 e. ZZ )
85 modcyc 
 |-  ( ( x e. RR /\ T e. RR+ /\ 1 e. ZZ ) -> ( ( x + ( 1 x. T ) ) mod T ) = ( x mod T ) )
86 32 40 84 85 syl3anc 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( ( x + ( 1 x. T ) ) mod T ) = ( x mod T ) )
87 70 83 86 3eqtr3a 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( x + T ) = ( x mod T ) )
88 65 87 breqtrd 
 |-  ( x e. ( -u _pi (,) 0 ) -> _pi < ( x mod T ) )
89 34 41 88 ltnsymd 
 |-  ( x e. ( -u _pi (,) 0 ) -> -. ( x mod T ) < _pi )
90 89 iffalsed 
 |-  ( x e. ( -u _pi (,) 0 ) -> if ( ( x mod T ) < _pi , 1 , -u 1 ) = -u 1 )
91 33 90 eqtrd 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( F ` x ) = -u 1 )
92 91 adantl 
 |-  ( ( ph /\ x e. ( -u _pi (,) 0 ) ) -> ( F ` x ) = -u 1 )
93 92 oveq1d 
 |-  ( ( ph /\ x e. ( -u _pi (,) 0 ) ) -> ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) = ( -u 1 x. ( sin ` ( N x. x ) ) ) )
94 93 mpteq2dva 
 |-  ( ph -> ( x e. ( -u _pi (,) 0 ) |-> ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) ) = ( x e. ( -u _pi (,) 0 ) |-> ( -u 1 x. ( sin ` ( N x. x ) ) ) ) )
95 neg1cn 
 |-  -u 1 e. CC
96 95 a1i 
 |-  ( ph -> -u 1 e. CC )
97 3 nnred 
 |-  ( ph -> N e. RR )
98 97 adantr 
 |-  ( ( ph /\ x e. ( -u _pi (,) 0 ) ) -> N e. RR )
99 32 adantl 
 |-  ( ( ph /\ x e. ( -u _pi (,) 0 ) ) -> x e. RR )
100 98 99 remulcld 
 |-  ( ( ph /\ x e. ( -u _pi (,) 0 ) ) -> ( N x. x ) e. RR )
101 100 resincld 
 |-  ( ( ph /\ x e. ( -u _pi (,) 0 ) ) -> ( sin ` ( N x. x ) ) e. RR )
102 ioossicc 
 |-  ( -u _pi (,) 0 ) C_ ( -u _pi [,] 0 )
103 102 a1i 
 |-  ( ph -> ( -u _pi (,) 0 ) C_ ( -u _pi [,] 0 ) )
104 ioombl 
 |-  ( -u _pi (,) 0 ) e. dom vol
105 104 a1i 
 |-  ( ph -> ( -u _pi (,) 0 ) e. dom vol )
106 97 adantr 
 |-  ( ( ph /\ x e. ( -u _pi [,] 0 ) ) -> N e. RR )
107 iccssre 
 |-  ( ( -u _pi e. RR /\ 0 e. RR ) -> ( -u _pi [,] 0 ) C_ RR )
108 5 8 107 mp2an 
 |-  ( -u _pi [,] 0 ) C_ RR
109 108 sseli 
 |-  ( x e. ( -u _pi [,] 0 ) -> x e. RR )
110 109 adantl 
 |-  ( ( ph /\ x e. ( -u _pi [,] 0 ) ) -> x e. RR )
111 106 110 remulcld 
 |-  ( ( ph /\ x e. ( -u _pi [,] 0 ) ) -> ( N x. x ) e. RR )
112 111 resincld 
 |-  ( ( ph /\ x e. ( -u _pi [,] 0 ) ) -> ( sin ` ( N x. x ) ) e. RR )
113 0red 
 |-  ( ph -> 0 e. RR )
114 sincn 
 |-  sin e. ( CC -cn-> CC )
115 114 a1i 
 |-  ( ph -> sin e. ( CC -cn-> CC ) )
116 ax-resscn 
 |-  RR C_ CC
117 108 116 sstri 
 |-  ( -u _pi [,] 0 ) C_ CC
118 117 a1i 
 |-  ( ph -> ( -u _pi [,] 0 ) C_ CC )
119 ssid 
 |-  CC C_ CC
120 119 a1i 
 |-  ( ph -> CC C_ CC )
121 118 26 120 constcncfg 
 |-  ( ph -> ( x e. ( -u _pi [,] 0 ) |-> N ) e. ( ( -u _pi [,] 0 ) -cn-> CC ) )
122 118 120 idcncfg 
 |-  ( ph -> ( x e. ( -u _pi [,] 0 ) |-> x ) e. ( ( -u _pi [,] 0 ) -cn-> CC ) )
123 121 122 mulcncf 
 |-  ( ph -> ( x e. ( -u _pi [,] 0 ) |-> ( N x. x ) ) e. ( ( -u _pi [,] 0 ) -cn-> CC ) )
124 115 123 cncfmpt1f 
 |-  ( ph -> ( x e. ( -u _pi [,] 0 ) |-> ( sin ` ( N x. x ) ) ) e. ( ( -u _pi [,] 0 ) -cn-> CC ) )
125 cniccibl 
 |-  ( ( -u _pi e. RR /\ 0 e. RR /\ ( x e. ( -u _pi [,] 0 ) |-> ( sin ` ( N x. x ) ) ) e. ( ( -u _pi [,] 0 ) -cn-> CC ) ) -> ( x e. ( -u _pi [,] 0 ) |-> ( sin ` ( N x. x ) ) ) e. L^1 )
126 6 113 124 125 syl3anc 
 |-  ( ph -> ( x e. ( -u _pi [,] 0 ) |-> ( sin ` ( N x. x ) ) ) e. L^1 )
127 103 105 112 126 iblss 
 |-  ( ph -> ( x e. ( -u _pi (,) 0 ) |-> ( sin ` ( N x. x ) ) ) e. L^1 )
128 96 101 127 iblmulc2 
 |-  ( ph -> ( x e. ( -u _pi (,) 0 ) |-> ( -u 1 x. ( sin ` ( N x. x ) ) ) ) e. L^1 )
129 94 128 eqeltrd 
 |-  ( ph -> ( x e. ( -u _pi (,) 0 ) |-> ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) ) e. L^1 )
130 60 a1i 
 |-  ( x e. ( 0 (,) _pi ) -> -u _pi e. RR* )
131 4 rexri 
 |-  _pi e. RR*
132 131 a1i 
 |-  ( x e. ( 0 (,) _pi ) -> _pi e. RR* )
133 elioore 
 |-  ( x e. ( 0 (,) _pi ) -> x e. RR )
134 5 a1i 
 |-  ( x e. ( 0 (,) _pi ) -> -u _pi e. RR )
135 0red 
 |-  ( x e. ( 0 (,) _pi ) -> 0 e. RR )
136 9 a1i 
 |-  ( x e. ( 0 (,) _pi ) -> -u _pi < 0 )
137 ioogtlb 
 |-  ( ( 0 e. RR* /\ _pi e. RR* /\ x e. ( 0 (,) _pi ) ) -> 0 < x )
138 61 131 137 mp3an12 
 |-  ( x e. ( 0 (,) _pi ) -> 0 < x )
139 134 135 133 136 138 lttrd 
 |-  ( x e. ( 0 (,) _pi ) -> -u _pi < x )
140 iooltub 
 |-  ( ( 0 e. RR* /\ _pi e. RR* /\ x e. ( 0 (,) _pi ) ) -> x < _pi )
141 61 131 140 mp3an12 
 |-  ( x e. ( 0 (,) _pi ) -> x < _pi )
142 130 132 133 139 141 eliood 
 |-  ( x e. ( 0 (,) _pi ) -> x e. ( -u _pi (,) _pi ) )
143 142 22 sylan2 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
144 39 a1i 
 |-  ( x e. ( 0 (,) _pi ) -> T e. RR+ )
145 135 133 138 ltled 
 |-  ( x e. ( 0 (,) _pi ) -> 0 <_ x )
146 4 a1i 
 |-  ( x e. ( 0 (,) _pi ) -> _pi e. RR )
147 58 a1i 
 |-  ( x e. ( 0 (,) _pi ) -> T e. RR )
148 2timesgt 
 |-  ( _pi e. RR+ -> _pi < ( 2 x. _pi ) )
149 36 148 ax-mp 
 |-  _pi < ( 2 x. _pi )
150 149 1 breqtrri 
 |-  _pi < T
151 150 a1i 
 |-  ( x e. ( 0 (,) _pi ) -> _pi < T )
152 133 146 147 141 151 lttrd 
 |-  ( x e. ( 0 (,) _pi ) -> x < T )
153 modid 
 |-  ( ( ( x e. RR /\ T e. RR+ ) /\ ( 0 <_ x /\ x < T ) ) -> ( x mod T ) = x )
154 133 144 145 152 153 syl22anc 
 |-  ( x e. ( 0 (,) _pi ) -> ( x mod T ) = x )
155 154 141 eqbrtrd 
 |-  ( x e. ( 0 (,) _pi ) -> ( x mod T ) < _pi )
156 155 iftrued 
 |-  ( x e. ( 0 (,) _pi ) -> if ( ( x mod T ) < _pi , 1 , -u 1 ) = 1 )
157 156 adantl 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> if ( ( x mod T ) < _pi , 1 , -u 1 ) = 1 )
158 143 157 eqtrd 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( F ` x ) = 1 )
159 158 oveq1d 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) = ( 1 x. ( sin ` ( N x. x ) ) ) )
160 142 30 sylan2 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( sin ` ( N x. x ) ) e. CC )
161 160 mulid2d 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( 1 x. ( sin ` ( N x. x ) ) ) = ( sin ` ( N x. x ) ) )
162 159 161 eqtrd 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) = ( sin ` ( N x. x ) ) )
163 162 mpteq2dva 
 |-  ( ph -> ( x e. ( 0 (,) _pi ) |-> ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) ) = ( x e. ( 0 (,) _pi ) |-> ( sin ` ( N x. x ) ) ) )
164 ioossicc 
 |-  ( 0 (,) _pi ) C_ ( 0 [,] _pi )
165 164 a1i 
 |-  ( ph -> ( 0 (,) _pi ) C_ ( 0 [,] _pi ) )
166 ioombl 
 |-  ( 0 (,) _pi ) e. dom vol
167 166 a1i 
 |-  ( ph -> ( 0 (,) _pi ) e. dom vol )
168 97 adantr 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> N e. RR )
169 iccssre 
 |-  ( ( 0 e. RR /\ _pi e. RR ) -> ( 0 [,] _pi ) C_ RR )
170 8 4 169 mp2an 
 |-  ( 0 [,] _pi ) C_ RR
171 170 sseli 
 |-  ( x e. ( 0 [,] _pi ) -> x e. RR )
172 171 adantl 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> x e. RR )
173 168 172 remulcld 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> ( N x. x ) e. RR )
174 173 resincld 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> ( sin ` ( N x. x ) ) e. RR )
175 170 116 sstri 
 |-  ( 0 [,] _pi ) C_ CC
176 175 a1i 
 |-  ( ph -> ( 0 [,] _pi ) C_ CC )
177 176 26 120 constcncfg 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> N ) e. ( ( 0 [,] _pi ) -cn-> CC ) )
178 176 120 idcncfg 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> x ) e. ( ( 0 [,] _pi ) -cn-> CC ) )
179 177 178 mulcncf 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> ( N x. x ) ) e. ( ( 0 [,] _pi ) -cn-> CC ) )
180 115 179 cncfmpt1f 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> ( sin ` ( N x. x ) ) ) e. ( ( 0 [,] _pi ) -cn-> CC ) )
181 cniccibl 
 |-  ( ( 0 e. RR /\ _pi e. RR /\ ( x e. ( 0 [,] _pi ) |-> ( sin ` ( N x. x ) ) ) e. ( ( 0 [,] _pi ) -cn-> CC ) ) -> ( x e. ( 0 [,] _pi ) |-> ( sin ` ( N x. x ) ) ) e. L^1 )
182 113 7 180 181 syl3anc 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> ( sin ` ( N x. x ) ) ) e. L^1 )
183 165 167 174 182 iblss 
 |-  ( ph -> ( x e. ( 0 (,) _pi ) |-> ( sin ` ( N x. x ) ) ) e. L^1 )
184 163 183 eqeltrd 
 |-  ( ph -> ( x e. ( 0 (,) _pi ) |-> ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) ) e. L^1 )
185 6 7 15 31 129 184 itgsplitioo 
 |-  ( ph -> S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x = ( S. ( -u _pi (,) 0 ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x + S. ( 0 (,) _pi ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x ) )
186 185 oveq1d 
 |-  ( ph -> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x / _pi ) = ( ( S. ( -u _pi (,) 0 ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x + S. ( 0 (,) _pi ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x ) / _pi ) )
187 91 oveq1d 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) = ( -u 1 x. ( sin ` ( N x. x ) ) ) )
188 187 adantl 
 |-  ( ( ph /\ x e. ( -u _pi (,) 0 ) ) -> ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) = ( -u 1 x. ( sin ` ( N x. x ) ) ) )
189 60 a1i 
 |-  ( x e. ( -u _pi (,) 0 ) -> -u _pi e. RR* )
190 131 a1i 
 |-  ( x e. ( -u _pi (,) 0 ) -> _pi e. RR* )
191 32 72 34 77 73 lttrd 
 |-  ( x e. ( -u _pi (,) 0 ) -> x < _pi )
192 189 190 32 63 191 eliood 
 |-  ( x e. ( -u _pi (,) 0 ) -> x e. ( -u _pi (,) _pi ) )
193 192 30 sylan2 
 |-  ( ( ph /\ x e. ( -u _pi (,) 0 ) ) -> ( sin ` ( N x. x ) ) e. CC )
194 193 mulm1d 
 |-  ( ( ph /\ x e. ( -u _pi (,) 0 ) ) -> ( -u 1 x. ( sin ` ( N x. x ) ) ) = -u ( sin ` ( N x. x ) ) )
195 188 194 eqtrd 
 |-  ( ( ph /\ x e. ( -u _pi (,) 0 ) ) -> ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) = -u ( sin ` ( N x. x ) ) )
196 195 itgeq2dv 
 |-  ( ph -> S. ( -u _pi (,) 0 ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x = S. ( -u _pi (,) 0 ) -u ( sin ` ( N x. x ) ) _d x )
197 101 127 itgneg 
 |-  ( ph -> -u S. ( -u _pi (,) 0 ) ( sin ` ( N x. x ) ) _d x = S. ( -u _pi (,) 0 ) -u ( sin ` ( N x. x ) ) _d x )
198 3 nnne0d 
 |-  ( ph -> N =/= 0 )
199 10 a1i 
 |-  ( ph -> -u _pi <_ 0 )
200 26 198 6 113 199 itgsincmulx 
 |-  ( ph -> S. ( -u _pi (,) 0 ) ( sin ` ( N x. x ) ) _d x = ( ( ( cos ` ( N x. -u _pi ) ) - ( cos ` ( N x. 0 ) ) ) / N ) )
201 3 nnzd 
 |-  ( ph -> N e. ZZ )
202 cosknegpi 
 |-  ( N e. ZZ -> ( cos ` ( N x. -u _pi ) ) = if ( 2 || N , 1 , -u 1 ) )
203 201 202 syl 
 |-  ( ph -> ( cos ` ( N x. -u _pi ) ) = if ( 2 || N , 1 , -u 1 ) )
204 26 mul01d 
 |-  ( ph -> ( N x. 0 ) = 0 )
205 204 fveq2d 
 |-  ( ph -> ( cos ` ( N x. 0 ) ) = ( cos ` 0 ) )
206 cos0 
 |-  ( cos ` 0 ) = 1
207 205 206 eqtrdi 
 |-  ( ph -> ( cos ` ( N x. 0 ) ) = 1 )
208 203 207 oveq12d 
 |-  ( ph -> ( ( cos ` ( N x. -u _pi ) ) - ( cos ` ( N x. 0 ) ) ) = ( if ( 2 || N , 1 , -u 1 ) - 1 ) )
209 1m1e0 
 |-  ( 1 - 1 ) = 0
210 iftrue 
 |-  ( 2 || N -> if ( 2 || N , 1 , -u 1 ) = 1 )
211 210 oveq1d 
 |-  ( 2 || N -> ( if ( 2 || N , 1 , -u 1 ) - 1 ) = ( 1 - 1 ) )
212 iftrue 
 |-  ( 2 || N -> if ( 2 || N , 0 , -u 2 ) = 0 )
213 209 211 212 3eqtr4a 
 |-  ( 2 || N -> ( if ( 2 || N , 1 , -u 1 ) - 1 ) = if ( 2 || N , 0 , -u 2 ) )
214 iffalse 
 |-  ( -. 2 || N -> if ( 2 || N , 1 , -u 1 ) = -u 1 )
215 214 oveq1d 
 |-  ( -. 2 || N -> ( if ( 2 || N , 1 , -u 1 ) - 1 ) = ( -u 1 - 1 ) )
216 ax-1cn 
 |-  1 e. CC
217 negdi2 
 |-  ( ( 1 e. CC /\ 1 e. CC ) -> -u ( 1 + 1 ) = ( -u 1 - 1 ) )
218 216 216 217 mp2an 
 |-  -u ( 1 + 1 ) = ( -u 1 - 1 )
219 218 eqcomi 
 |-  ( -u 1 - 1 ) = -u ( 1 + 1 )
220 219 a1i 
 |-  ( -. 2 || N -> ( -u 1 - 1 ) = -u ( 1 + 1 ) )
221 1p1e2 
 |-  ( 1 + 1 ) = 2
222 221 negeqi 
 |-  -u ( 1 + 1 ) = -u 2
223 iffalse 
 |-  ( -. 2 || N -> if ( 2 || N , 0 , -u 2 ) = -u 2 )
224 222 223 eqtr4id 
 |-  ( -. 2 || N -> -u ( 1 + 1 ) = if ( 2 || N , 0 , -u 2 ) )
225 215 220 224 3eqtrd 
 |-  ( -. 2 || N -> ( if ( 2 || N , 1 , -u 1 ) - 1 ) = if ( 2 || N , 0 , -u 2 ) )
226 213 225 pm2.61i 
 |-  ( if ( 2 || N , 1 , -u 1 ) - 1 ) = if ( 2 || N , 0 , -u 2 )
227 208 226 eqtrdi 
 |-  ( ph -> ( ( cos ` ( N x. -u _pi ) ) - ( cos ` ( N x. 0 ) ) ) = if ( 2 || N , 0 , -u 2 ) )
228 227 oveq1d 
 |-  ( ph -> ( ( ( cos ` ( N x. -u _pi ) ) - ( cos ` ( N x. 0 ) ) ) / N ) = ( if ( 2 || N , 0 , -u 2 ) / N ) )
229 200 228 eqtrd 
 |-  ( ph -> S. ( -u _pi (,) 0 ) ( sin ` ( N x. x ) ) _d x = ( if ( 2 || N , 0 , -u 2 ) / N ) )
230 229 negeqd 
 |-  ( ph -> -u S. ( -u _pi (,) 0 ) ( sin ` ( N x. x ) ) _d x = -u ( if ( 2 || N , 0 , -u 2 ) / N ) )
231 0cn 
 |-  0 e. CC
232 2cn 
 |-  2 e. CC
233 232 negcli 
 |-  -u 2 e. CC
234 231 233 ifcli 
 |-  if ( 2 || N , 0 , -u 2 ) e. CC
235 234 a1i 
 |-  ( ph -> if ( 2 || N , 0 , -u 2 ) e. CC )
236 235 26 198 divnegd 
 |-  ( ph -> -u ( if ( 2 || N , 0 , -u 2 ) / N ) = ( -u if ( 2 || N , 0 , -u 2 ) / N ) )
237 neg0 
 |-  -u 0 = 0
238 212 negeqd 
 |-  ( 2 || N -> -u if ( 2 || N , 0 , -u 2 ) = -u 0 )
239 iftrue 
 |-  ( 2 || N -> if ( 2 || N , 0 , 2 ) = 0 )
240 237 238 239 3eqtr4a 
 |-  ( 2 || N -> -u if ( 2 || N , 0 , -u 2 ) = if ( 2 || N , 0 , 2 ) )
241 232 negnegi 
 |-  -u -u 2 = 2
242 223 negeqd 
 |-  ( -. 2 || N -> -u if ( 2 || N , 0 , -u 2 ) = -u -u 2 )
243 iffalse 
 |-  ( -. 2 || N -> if ( 2 || N , 0 , 2 ) = 2 )
244 241 242 243 3eqtr4a 
 |-  ( -. 2 || N -> -u if ( 2 || N , 0 , -u 2 ) = if ( 2 || N , 0 , 2 ) )
245 240 244 pm2.61i 
 |-  -u if ( 2 || N , 0 , -u 2 ) = if ( 2 || N , 0 , 2 )
246 245 oveq1i 
 |-  ( -u if ( 2 || N , 0 , -u 2 ) / N ) = ( if ( 2 || N , 0 , 2 ) / N )
247 246 a1i 
 |-  ( ph -> ( -u if ( 2 || N , 0 , -u 2 ) / N ) = ( if ( 2 || N , 0 , 2 ) / N ) )
248 230 236 247 3eqtrd 
 |-  ( ph -> -u S. ( -u _pi (,) 0 ) ( sin ` ( N x. x ) ) _d x = ( if ( 2 || N , 0 , 2 ) / N ) )
249 196 197 248 3eqtr2d 
 |-  ( ph -> S. ( -u _pi (,) 0 ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x = ( if ( 2 || N , 0 , 2 ) / N ) )
250 133 20 21 sylancl 
 |-  ( x e. ( 0 (,) _pi ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
251 250 156 eqtrd 
 |-  ( x e. ( 0 (,) _pi ) -> ( F ` x ) = 1 )
252 251 oveq1d 
 |-  ( x e. ( 0 (,) _pi ) -> ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) = ( 1 x. ( sin ` ( N x. x ) ) ) )
253 252 adantl 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) = ( 1 x. ( sin ` ( N x. x ) ) ) )
254 253 161 eqtrd 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) = ( sin ` ( N x. x ) ) )
255 254 itgeq2dv 
 |-  ( ph -> S. ( 0 (,) _pi ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x = S. ( 0 (,) _pi ) ( sin ` ( N x. x ) ) _d x )
256 12 a1i 
 |-  ( ph -> 0 <_ _pi )
257 26 198 113 7 256 itgsincmulx 
 |-  ( ph -> S. ( 0 (,) _pi ) ( sin ` ( N x. x ) ) _d x = ( ( ( cos ` ( N x. 0 ) ) - ( cos ` ( N x. _pi ) ) ) / N ) )
258 coskpi2 
 |-  ( N e. ZZ -> ( cos ` ( N x. _pi ) ) = if ( 2 || N , 1 , -u 1 ) )
259 201 258 syl 
 |-  ( ph -> ( cos ` ( N x. _pi ) ) = if ( 2 || N , 1 , -u 1 ) )
260 207 259 oveq12d 
 |-  ( ph -> ( ( cos ` ( N x. 0 ) ) - ( cos ` ( N x. _pi ) ) ) = ( 1 - if ( 2 || N , 1 , -u 1 ) ) )
261 210 oveq2d 
 |-  ( 2 || N -> ( 1 - if ( 2 || N , 1 , -u 1 ) ) = ( 1 - 1 ) )
262 209 261 239 3eqtr4a 
 |-  ( 2 || N -> ( 1 - if ( 2 || N , 1 , -u 1 ) ) = if ( 2 || N , 0 , 2 ) )
263 214 oveq2d 
 |-  ( -. 2 || N -> ( 1 - if ( 2 || N , 1 , -u 1 ) ) = ( 1 - -u 1 ) )
264 216 216 subnegi 
 |-  ( 1 - -u 1 ) = ( 1 + 1 )
265 264 a1i 
 |-  ( -. 2 || N -> ( 1 - -u 1 ) = ( 1 + 1 ) )
266 221 243 eqtr4id 
 |-  ( -. 2 || N -> ( 1 + 1 ) = if ( 2 || N , 0 , 2 ) )
267 263 265 266 3eqtrd 
 |-  ( -. 2 || N -> ( 1 - if ( 2 || N , 1 , -u 1 ) ) = if ( 2 || N , 0 , 2 ) )
268 262 267 pm2.61i 
 |-  ( 1 - if ( 2 || N , 1 , -u 1 ) ) = if ( 2 || N , 0 , 2 )
269 260 268 eqtrdi 
 |-  ( ph -> ( ( cos ` ( N x. 0 ) ) - ( cos ` ( N x. _pi ) ) ) = if ( 2 || N , 0 , 2 ) )
270 269 oveq1d 
 |-  ( ph -> ( ( ( cos ` ( N x. 0 ) ) - ( cos ` ( N x. _pi ) ) ) / N ) = ( if ( 2 || N , 0 , 2 ) / N ) )
271 255 257 270 3eqtrd 
 |-  ( ph -> S. ( 0 (,) _pi ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x = ( if ( 2 || N , 0 , 2 ) / N ) )
272 249 271 oveq12d 
 |-  ( ph -> ( S. ( -u _pi (,) 0 ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x + S. ( 0 (,) _pi ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x ) = ( ( if ( 2 || N , 0 , 2 ) / N ) + ( if ( 2 || N , 0 , 2 ) / N ) ) )
273 231 232 ifcli 
 |-  if ( 2 || N , 0 , 2 ) e. CC
274 273 a1i 
 |-  ( ph -> if ( 2 || N , 0 , 2 ) e. CC )
275 274 274 26 198 divdird 
 |-  ( ph -> ( ( if ( 2 || N , 0 , 2 ) + if ( 2 || N , 0 , 2 ) ) / N ) = ( ( if ( 2 || N , 0 , 2 ) / N ) + ( if ( 2 || N , 0 , 2 ) / N ) ) )
276 239 239 oveq12d 
 |-  ( 2 || N -> ( if ( 2 || N , 0 , 2 ) + if ( 2 || N , 0 , 2 ) ) = ( 0 + 0 ) )
277 00id 
 |-  ( 0 + 0 ) = 0
278 276 277 eqtrdi 
 |-  ( 2 || N -> ( if ( 2 || N , 0 , 2 ) + if ( 2 || N , 0 , 2 ) ) = 0 )
279 278 oveq1d 
 |-  ( 2 || N -> ( ( if ( 2 || N , 0 , 2 ) + if ( 2 || N , 0 , 2 ) ) / N ) = ( 0 / N ) )
280 279 adantl 
 |-  ( ( ph /\ 2 || N ) -> ( ( if ( 2 || N , 0 , 2 ) + if ( 2 || N , 0 , 2 ) ) / N ) = ( 0 / N ) )
281 26 198 div0d 
 |-  ( ph -> ( 0 / N ) = 0 )
282 281 adantr 
 |-  ( ( ph /\ 2 || N ) -> ( 0 / N ) = 0 )
283 iftrue 
 |-  ( 2 || N -> if ( 2 || N , 0 , ( 4 / N ) ) = 0 )
284 283 eqcomd 
 |-  ( 2 || N -> 0 = if ( 2 || N , 0 , ( 4 / N ) ) )
285 284 adantl 
 |-  ( ( ph /\ 2 || N ) -> 0 = if ( 2 || N , 0 , ( 4 / N ) ) )
286 280 282 285 3eqtrd 
 |-  ( ( ph /\ 2 || N ) -> ( ( if ( 2 || N , 0 , 2 ) + if ( 2 || N , 0 , 2 ) ) / N ) = if ( 2 || N , 0 , ( 4 / N ) ) )
287 243 243 oveq12d 
 |-  ( -. 2 || N -> ( if ( 2 || N , 0 , 2 ) + if ( 2 || N , 0 , 2 ) ) = ( 2 + 2 ) )
288 2p2e4 
 |-  ( 2 + 2 ) = 4
289 287 288 eqtrdi 
 |-  ( -. 2 || N -> ( if ( 2 || N , 0 , 2 ) + if ( 2 || N , 0 , 2 ) ) = 4 )
290 289 oveq1d 
 |-  ( -. 2 || N -> ( ( if ( 2 || N , 0 , 2 ) + if ( 2 || N , 0 , 2 ) ) / N ) = ( 4 / N ) )
291 iffalse 
 |-  ( -. 2 || N -> if ( 2 || N , 0 , ( 4 / N ) ) = ( 4 / N ) )
292 290 291 eqtr4d 
 |-  ( -. 2 || N -> ( ( if ( 2 || N , 0 , 2 ) + if ( 2 || N , 0 , 2 ) ) / N ) = if ( 2 || N , 0 , ( 4 / N ) ) )
293 292 adantl 
 |-  ( ( ph /\ -. 2 || N ) -> ( ( if ( 2 || N , 0 , 2 ) + if ( 2 || N , 0 , 2 ) ) / N ) = if ( 2 || N , 0 , ( 4 / N ) ) )
294 286 293 pm2.61dan 
 |-  ( ph -> ( ( if ( 2 || N , 0 , 2 ) + if ( 2 || N , 0 , 2 ) ) / N ) = if ( 2 || N , 0 , ( 4 / N ) ) )
295 272 275 294 3eqtr2d 
 |-  ( ph -> ( S. ( -u _pi (,) 0 ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x + S. ( 0 (,) _pi ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x ) = if ( 2 || N , 0 , ( 4 / N ) ) )
296 295 oveq1d 
 |-  ( ph -> ( ( S. ( -u _pi (,) 0 ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x + S. ( 0 (,) _pi ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x ) / _pi ) = ( if ( 2 || N , 0 , ( 4 / N ) ) / _pi ) )
297 283 oveq1d 
 |-  ( 2 || N -> ( if ( 2 || N , 0 , ( 4 / N ) ) / _pi ) = ( 0 / _pi ) )
298 297 adantl 
 |-  ( ( ph /\ 2 || N ) -> ( if ( 2 || N , 0 , ( 4 / N ) ) / _pi ) = ( 0 / _pi ) )
299 8 11 gtneii 
 |-  _pi =/= 0
300 42 299 div0i 
 |-  ( 0 / _pi ) = 0
301 300 a1i 
 |-  ( ( ph /\ 2 || N ) -> ( 0 / _pi ) = 0 )
302 iftrue 
 |-  ( 2 || N -> if ( 2 || N , 0 , ( 4 / ( N x. _pi ) ) ) = 0 )
303 302 eqcomd 
 |-  ( 2 || N -> 0 = if ( 2 || N , 0 , ( 4 / ( N x. _pi ) ) ) )
304 303 adantl 
 |-  ( ( ph /\ 2 || N ) -> 0 = if ( 2 || N , 0 , ( 4 / ( N x. _pi ) ) ) )
305 298 301 304 3eqtrd 
 |-  ( ( ph /\ 2 || N ) -> ( if ( 2 || N , 0 , ( 4 / N ) ) / _pi ) = if ( 2 || N , 0 , ( 4 / ( N x. _pi ) ) ) )
306 291 oveq1d 
 |-  ( -. 2 || N -> ( if ( 2 || N , 0 , ( 4 / N ) ) / _pi ) = ( ( 4 / N ) / _pi ) )
307 306 adantl 
 |-  ( ( ph /\ -. 2 || N ) -> ( if ( 2 || N , 0 , ( 4 / N ) ) / _pi ) = ( ( 4 / N ) / _pi ) )
308 4cn 
 |-  4 e. CC
309 308 a1i 
 |-  ( ph -> 4 e. CC )
310 42 a1i 
 |-  ( ph -> _pi e. CC )
311 299 a1i 
 |-  ( ph -> _pi =/= 0 )
312 309 26 310 198 311 divdiv1d 
 |-  ( ph -> ( ( 4 / N ) / _pi ) = ( 4 / ( N x. _pi ) ) )
313 312 adantr 
 |-  ( ( ph /\ -. 2 || N ) -> ( ( 4 / N ) / _pi ) = ( 4 / ( N x. _pi ) ) )
314 iffalse 
 |-  ( -. 2 || N -> if ( 2 || N , 0 , ( 4 / ( N x. _pi ) ) ) = ( 4 / ( N x. _pi ) ) )
315 314 eqcomd 
 |-  ( -. 2 || N -> ( 4 / ( N x. _pi ) ) = if ( 2 || N , 0 , ( 4 / ( N x. _pi ) ) ) )
316 315 adantl 
 |-  ( ( ph /\ -. 2 || N ) -> ( 4 / ( N x. _pi ) ) = if ( 2 || N , 0 , ( 4 / ( N x. _pi ) ) ) )
317 307 313 316 3eqtrd 
 |-  ( ( ph /\ -. 2 || N ) -> ( if ( 2 || N , 0 , ( 4 / N ) ) / _pi ) = if ( 2 || N , 0 , ( 4 / ( N x. _pi ) ) ) )
318 305 317 pm2.61dan 
 |-  ( ph -> ( if ( 2 || N , 0 , ( 4 / N ) ) / _pi ) = if ( 2 || N , 0 , ( 4 / ( N x. _pi ) ) ) )
319 186 296 318 3eqtrd 
 |-  ( ph -> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x / _pi ) = if ( 2 || N , 0 , ( 4 / ( N x. _pi ) ) ) )