Metamath Proof Explorer

Theorem sqwvfoura

Description: Fourier coefficients for the square wave function. Since the square function is an odd function, there is no contribution from the A coefficients. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 sqwvfoura.t 
 |-  T = ( 2 x. _pi )
2 sqwvfoura.f 
 |-  F = ( x e. RR |-> if ( ( x mod T ) < _pi , 1 , -u 1 ) )
3 sqwvfoura.n 
 |-  ( ph -> N e. NN0 )
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 1red 
 |-  ( x e. RR -> 1 e. RR )
17 16 renegcld 
 |-  ( x e. RR -> -u 1 e. RR )
18 16 17 ifcld 
 |-  ( x e. RR -> if ( ( x mod T ) < _pi , 1 , -u 1 ) e. RR )
19 18 adantl 
 |-  ( ( ph /\ x e. RR ) -> if ( ( x mod T ) < _pi , 1 , -u 1 ) e. RR )
20 19 2 fmptd 
 |-  ( ph -> F : RR --> RR )
21 20 adantr 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> F : RR --> RR )
22 elioore 
 |-  ( x e. ( -u _pi (,) _pi ) -> x e. RR )
23 22 adantl 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> x e. RR )
24 21 23 ffvelrnd 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> ( F ` x ) e. RR )
25 3 nn0red 
 |-  ( ph -> N e. RR )
26 25 adantr 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> N e. RR )
27 26 23 remulcld 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> ( N x. x ) e. RR )
28 27 recoscld 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> ( cos ` ( N x. x ) ) e. RR )
29 24 28 remulcld 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) e. RR )
30 29 recnd 
 |-  ( ( ph /\ x e. ( -u _pi (,) _pi ) ) -> ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) e. CC )
31 elioore 
 |-  ( x e. ( -u _pi (,) 0 ) -> x e. RR )
32 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 ) )
33 31 18 32 syl2anc2 
 |-  ( 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 31 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 5 a1i 
 |-  ( x e. ( -u _pi (,) 0 ) -> -u _pi e. RR )
55 2re 
 |-  2 e. RR
56 55 4 remulcli 
 |-  ( 2 x. _pi ) e. RR
57 1 56 eqeltri 
 |-  T e. RR
58 57 a1i 
 |-  ( x e. ( -u _pi (,) 0 ) -> T e. RR )
59 5 rexri 
 |-  -u _pi e. RR*
60 59 a1i 
 |-  ( x e. ( -u _pi (,) 0 ) -> -u _pi e. RR* )
61 0red 
 |-  ( x e. ( -u _pi (,) 0 ) -> 0 e. RR )
62 61 rexrd 
 |-  ( x e. ( -u _pi (,) 0 ) -> 0 e. RR* )
63 id 
 |-  ( x e. ( -u _pi (,) 0 ) -> x e. ( -u _pi (,) 0 ) )
64 ioogtlb 
 |-  ( ( -u _pi e. RR* /\ 0 e. RR* /\ x e. ( -u _pi (,) 0 ) ) -> -u _pi < x )
65 60 62 63 64 syl3anc 
 |-  ( x e. ( -u _pi (,) 0 ) -> -u _pi < x )
66 54 31 58 65 ltadd1dd 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( -u _pi + T ) < ( x + T ) )
67 53 66 eqbrtrid 
 |-  ( x e. ( -u _pi (,) 0 ) -> _pi < ( x + T ) )
68 57 recni 
 |-  T e. CC
69 68 mulid2i 
 |-  ( 1 x. T ) = T
70 69 eqcomi 
 |-  T = ( 1 x. T )
71 70 oveq2i 
 |-  ( x + T ) = ( x + ( 1 x. T ) )
72 71 oveq1i 
 |-  ( ( x + T ) mod T ) = ( ( x + ( 1 x. T ) ) mod T )
73 31 58 readdcld 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( x + T ) e. RR )
74 11 a1i 
 |-  ( x e. ( -u _pi (,) 0 ) -> 0 < _pi )
75 61 34 73 74 67 lttrd 
 |-  ( x e. ( -u _pi (,) 0 ) -> 0 < ( x + T ) )
76 61 73 75 ltled 
 |-  ( x e. ( -u _pi (,) 0 ) -> 0 <_ ( x + T ) )
77 iooltub 
 |-  ( ( -u _pi e. RR* /\ 0 e. RR* /\ x e. ( -u _pi (,) 0 ) ) -> x < 0 )
78 60 62 63 77 syl3anc 
 |-  ( x e. ( -u _pi (,) 0 ) -> x < 0 )
79 31 61 58 78 ltadd1dd 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( x + T ) < ( 0 + T ) )
80 68 a1i 
 |-  ( x e. ( -u _pi (,) 0 ) -> T e. CC )
81 80 addid2d 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( 0 + T ) = T )
82 79 81 breqtrd 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( x + T ) < T )
83 modid 
 |-  ( ( ( ( x + T ) e. RR /\ T e. RR+ ) /\ ( 0 <_ ( x + T ) /\ ( x + T ) < T ) ) -> ( ( x + T ) mod T ) = ( x + T ) )
84 73 40 76 82 83 syl22anc 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( ( x + T ) mod T ) = ( x + T ) )
85 1zzd 
 |-  ( x e. ( -u _pi (,) 0 ) -> 1 e. ZZ )
86 modcyc 
 |-  ( ( x e. RR /\ T e. RR+ /\ 1 e. ZZ ) -> ( ( x + ( 1 x. T ) ) mod T ) = ( x mod T ) )
87 31 40 85 86 syl3anc 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( ( x + ( 1 x. T ) ) mod T ) = ( x mod T ) )
88 72 84 87 3eqtr3a 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( x + T ) = ( x mod T ) )
89 67 88 breqtrd 
 |-  ( x e. ( -u _pi (,) 0 ) -> _pi < ( x mod T ) )
90 34 41 89 ltnsymd 
 |-  ( x e. ( -u _pi (,) 0 ) -> -. ( x mod T ) < _pi )
91 90 iffalsed 
 |-  ( x e. ( -u _pi (,) 0 ) -> if ( ( x mod T ) < _pi , 1 , -u 1 ) = -u 1 )
92 33 91 eqtrd 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( F ` x ) = -u 1 )
93 92 oveq1d 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) = ( -u 1 x. ( cos ` ( N x. x ) ) ) )
94 93 adantl 
 |-  ( ( ph /\ x e. ( -u _pi (,) 0 ) ) -> ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) = ( -u 1 x. ( cos ` ( N x. x ) ) ) )
95 94 mpteq2dva 
 |-  ( ph -> ( x e. ( -u _pi (,) 0 ) |-> ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) ) = ( x e. ( -u _pi (,) 0 ) |-> ( -u 1 x. ( cos ` ( N x. x ) ) ) ) )
96 1cnd 
 |-  ( ph -> 1 e. CC )
97 96 negcld 
 |-  ( ph -> -u 1 e. CC )
98 25 adantr 
 |-  ( ( ph /\ x e. ( -u _pi (,) 0 ) ) -> N e. RR )
99 31 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 recoscld 
 |-  ( ( ph /\ x e. ( -u _pi (,) 0 ) ) -> ( cos ` ( 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 25 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 recoscld 
 |-  ( ( ph /\ x e. ( -u _pi [,] 0 ) ) -> ( cos ` ( N x. x ) ) e. RR )
113 0red 
 |-  ( ph -> 0 e. RR )
114 coscn 
 |-  cos e. ( CC -cn-> CC )
115 114 a1i 
 |-  ( ph -> cos 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 25 recnd 
 |-  ( ph -> N e. CC )
120 ssid 
 |-  CC C_ CC
121 120 a1i 
 |-  ( ph -> CC C_ CC )
122 118 119 121 constcncfg 
 |-  ( ph -> ( x e. ( -u _pi [,] 0 ) |-> N ) e. ( ( -u _pi [,] 0 ) -cn-> CC ) )
123 118 121 idcncfg 
 |-  ( ph -> ( x e. ( -u _pi [,] 0 ) |-> x ) e. ( ( -u _pi [,] 0 ) -cn-> CC ) )
124 122 123 mulcncf 
 |-  ( ph -> ( x e. ( -u _pi [,] 0 ) |-> ( N x. x ) ) e. ( ( -u _pi [,] 0 ) -cn-> CC ) )
125 115 124 cncfmpt1f 
 |-  ( ph -> ( x e. ( -u _pi [,] 0 ) |-> ( cos ` ( N x. x ) ) ) e. ( ( -u _pi [,] 0 ) -cn-> CC ) )
126 cniccibl 
 |-  ( ( -u _pi e. RR /\ 0 e. RR /\ ( x e. ( -u _pi [,] 0 ) |-> ( cos ` ( N x. x ) ) ) e. ( ( -u _pi [,] 0 ) -cn-> CC ) ) -> ( x e. ( -u _pi [,] 0 ) |-> ( cos ` ( N x. x ) ) ) e. L^1 )
127 6 113 125 126 syl3anc 
 |-  ( ph -> ( x e. ( -u _pi [,] 0 ) |-> ( cos ` ( N x. x ) ) ) e. L^1 )
128 103 105 112 127 iblss 
 |-  ( ph -> ( x e. ( -u _pi (,) 0 ) |-> ( cos ` ( N x. x ) ) ) e. L^1 )
129 97 101 128 iblmulc2 
 |-  ( ph -> ( x e. ( -u _pi (,) 0 ) |-> ( -u 1 x. ( cos ` ( N x. x ) ) ) ) e. L^1 )
130 95 129 eqeltrd 
 |-  ( ph -> ( x e. ( -u _pi (,) 0 ) |-> ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) ) e. L^1 )
131 elioore 
 |-  ( x e. ( 0 (,) _pi ) -> x e. RR )
132 131 18 32 syl2anc2 
 |-  ( x e. ( 0 (,) _pi ) -> ( F ` x ) = if ( ( x mod T ) < _pi , 1 , -u 1 ) )
133 39 a1i 
 |-  ( x e. ( 0 (,) _pi ) -> T e. RR+ )
134 0red 
 |-  ( x e. ( 0 (,) _pi ) -> 0 e. RR )
135 134 rexrd 
 |-  ( x e. ( 0 (,) _pi ) -> 0 e. RR* )
136 4 rexri 
 |-  _pi e. RR*
137 136 a1i 
 |-  ( x e. ( 0 (,) _pi ) -> _pi e. RR* )
138 id 
 |-  ( x e. ( 0 (,) _pi ) -> x e. ( 0 (,) _pi ) )
139 ioogtlb 
 |-  ( ( 0 e. RR* /\ _pi e. RR* /\ x e. ( 0 (,) _pi ) ) -> 0 < x )
140 135 137 138 139 syl3anc 
 |-  ( x e. ( 0 (,) _pi ) -> 0 < x )
141 134 131 140 ltled 
 |-  ( x e. ( 0 (,) _pi ) -> 0 <_ x )
142 4 a1i 
 |-  ( x e. ( 0 (,) _pi ) -> _pi e. RR )
143 57 a1i 
 |-  ( x e. ( 0 (,) _pi ) -> T e. RR )
144 iooltub 
 |-  ( ( 0 e. RR* /\ _pi e. RR* /\ x e. ( 0 (,) _pi ) ) -> x < _pi )
145 135 137 138 144 syl3anc 
 |-  ( x e. ( 0 (,) _pi ) -> x < _pi )
146 2timesgt 
 |-  ( _pi e. RR+ -> _pi < ( 2 x. _pi ) )
147 36 146 ax-mp 
 |-  _pi < ( 2 x. _pi )
148 147 1 breqtrri 
 |-  _pi < T
149 148 a1i 
 |-  ( x e. ( 0 (,) _pi ) -> _pi < T )
150 131 142 143 145 149 lttrd 
 |-  ( x e. ( 0 (,) _pi ) -> x < T )
151 modid 
 |-  ( ( ( x e. RR /\ T e. RR+ ) /\ ( 0 <_ x /\ x < T ) ) -> ( x mod T ) = x )
152 131 133 141 150 151 syl22anc 
 |-  ( x e. ( 0 (,) _pi ) -> ( x mod T ) = x )
153 152 145 eqbrtrd 
 |-  ( x e. ( 0 (,) _pi ) -> ( x mod T ) < _pi )
154 153 iftrued 
 |-  ( x e. ( 0 (,) _pi ) -> if ( ( x mod T ) < _pi , 1 , -u 1 ) = 1 )
155 132 154 eqtrd 
 |-  ( x e. ( 0 (,) _pi ) -> ( F ` x ) = 1 )
156 155 oveq1d 
 |-  ( x e. ( 0 (,) _pi ) -> ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) = ( 1 x. ( cos ` ( N x. x ) ) ) )
157 156 adantl 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) = ( 1 x. ( cos ` ( N x. x ) ) ) )
158 157 mpteq2dva 
 |-  ( ph -> ( x e. ( 0 (,) _pi ) |-> ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) ) = ( x e. ( 0 (,) _pi ) |-> ( 1 x. ( cos ` ( N x. x ) ) ) ) )
159 25 adantr 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> N e. RR )
160 131 adantl 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> x e. RR )
161 159 160 remulcld 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( N x. x ) e. RR )
162 161 recoscld 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( cos ` ( N x. x ) ) e. RR )
163 ioossicc 
 |-  ( 0 (,) _pi ) C_ ( 0 [,] _pi )
164 163 a1i 
 |-  ( ph -> ( 0 (,) _pi ) C_ ( 0 [,] _pi ) )
165 ioombl 
 |-  ( 0 (,) _pi ) e. dom vol
166 165 a1i 
 |-  ( ph -> ( 0 (,) _pi ) e. dom vol )
167 25 adantr 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> N e. RR )
168 iccssre 
 |-  ( ( 0 e. RR /\ _pi e. RR ) -> ( 0 [,] _pi ) C_ RR )
169 8 4 168 mp2an 
 |-  ( 0 [,] _pi ) C_ RR
170 169 sseli 
 |-  ( x e. ( 0 [,] _pi ) -> x e. RR )
171 170 adantl 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> x e. RR )
172 167 171 remulcld 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> ( N x. x ) e. RR )
173 172 recoscld 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> ( cos ` ( N x. x ) ) e. RR )
174 169 116 sstri 
 |-  ( 0 [,] _pi ) C_ CC
175 174 a1i 
 |-  ( ph -> ( 0 [,] _pi ) C_ CC )
176 175 119 121 constcncfg 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> N ) e. ( ( 0 [,] _pi ) -cn-> CC ) )
177 175 121 idcncfg 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> x ) e. ( ( 0 [,] _pi ) -cn-> CC ) )
178 176 177 mulcncf 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> ( N x. x ) ) e. ( ( 0 [,] _pi ) -cn-> CC ) )
179 115 178 cncfmpt1f 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> ( cos ` ( N x. x ) ) ) e. ( ( 0 [,] _pi ) -cn-> CC ) )
180 cniccibl 
 |-  ( ( 0 e. RR /\ _pi e. RR /\ ( x e. ( 0 [,] _pi ) |-> ( cos ` ( N x. x ) ) ) e. ( ( 0 [,] _pi ) -cn-> CC ) ) -> ( x e. ( 0 [,] _pi ) |-> ( cos ` ( N x. x ) ) ) e. L^1 )
181 113 7 179 180 syl3anc 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> ( cos ` ( N x. x ) ) ) e. L^1 )
182 164 166 173 181 iblss 
 |-  ( ph -> ( x e. ( 0 (,) _pi ) |-> ( cos ` ( N x. x ) ) ) e. L^1 )
183 96 162 182 iblmulc2 
 |-  ( ph -> ( x e. ( 0 (,) _pi ) |-> ( 1 x. ( cos ` ( N x. x ) ) ) ) e. L^1 )
184 158 183 eqeltrd 
 |-  ( ph -> ( x e. ( 0 (,) _pi ) |-> ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) ) e. L^1 )
185 6 7 15 30 130 184 itgsplitioo 
 |-  ( ph -> S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x = ( S. ( -u _pi (,) 0 ) ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x + S. ( 0 (,) _pi ) ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x ) )
186 185 oveq1d 
 |-  ( ph -> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x / _pi ) = ( ( S. ( -u _pi (,) 0 ) ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x + S. ( 0 (,) _pi ) ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x ) / _pi ) )
187 94 itgeq2dv 
 |-  ( ph -> S. ( -u _pi (,) 0 ) ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x = S. ( -u _pi (,) 0 ) ( -u 1 x. ( cos ` ( N x. x ) ) ) _d x )
188 97 101 128 itgmulc2 
 |-  ( ph -> ( -u 1 x. S. ( -u _pi (,) 0 ) ( cos ` ( N x. x ) ) _d x ) = S. ( -u _pi (,) 0 ) ( -u 1 x. ( cos ` ( N x. x ) ) ) _d x )
189 oveq1 
 |-  ( N = 0 -> ( N x. x ) = ( 0 x. x ) )
190 ioosscn 
 |-  ( -u _pi (,) 0 ) C_ CC
191 190 sseli 
 |-  ( x e. ( -u _pi (,) 0 ) -> x e. CC )
192 191 mul02d 
 |-  ( x e. ( -u _pi (,) 0 ) -> ( 0 x. x ) = 0 )
193 189 192 sylan9eq 
 |-  ( ( N = 0 /\ x e. ( -u _pi (,) 0 ) ) -> ( N x. x ) = 0 )
194 193 fveq2d 
 |-  ( ( N = 0 /\ x e. ( -u _pi (,) 0 ) ) -> ( cos ` ( N x. x ) ) = ( cos ` 0 ) )
195 cos0 
 |-  ( cos ` 0 ) = 1
196 194 195 eqtrdi 
 |-  ( ( N = 0 /\ x e. ( -u _pi (,) 0 ) ) -> ( cos ` ( N x. x ) ) = 1 )
197 196 adantll 
 |-  ( ( ( ph /\ N = 0 ) /\ x e. ( -u _pi (,) 0 ) ) -> ( cos ` ( N x. x ) ) = 1 )
198 197 itgeq2dv 
 |-  ( ( ph /\ N = 0 ) -> S. ( -u _pi (,) 0 ) ( cos ` ( N x. x ) ) _d x = S. ( -u _pi (,) 0 ) 1 _d x )
199 ioovolcl 
 |-  ( ( -u _pi e. RR /\ 0 e. RR ) -> ( vol ` ( -u _pi (,) 0 ) ) e. RR )
200 5 8 199 mp2an 
 |-  ( vol ` ( -u _pi (,) 0 ) ) e. RR
201 200 a1i 
 |-  ( ph -> ( vol ` ( -u _pi (,) 0 ) ) e. RR )
202 itgconst 
 |-  ( ( ( -u _pi (,) 0 ) e. dom vol /\ ( vol ` ( -u _pi (,) 0 ) ) e. RR /\ 1 e. CC ) -> S. ( -u _pi (,) 0 ) 1 _d x = ( 1 x. ( vol ` ( -u _pi (,) 0 ) ) ) )
203 105 201 96 202 syl3anc 
 |-  ( ph -> S. ( -u _pi (,) 0 ) 1 _d x = ( 1 x. ( vol ` ( -u _pi (,) 0 ) ) ) )
204 203 adantr 
 |-  ( ( ph /\ N = 0 ) -> S. ( -u _pi (,) 0 ) 1 _d x = ( 1 x. ( vol ` ( -u _pi (,) 0 ) ) ) )
205 volioo 
 |-  ( ( -u _pi e. RR /\ 0 e. RR /\ -u _pi <_ 0 ) -> ( vol ` ( -u _pi (,) 0 ) ) = ( 0 - -u _pi ) )
206 5 8 10 205 mp3an 
 |-  ( vol ` ( -u _pi (,) 0 ) ) = ( 0 - -u _pi )
207 0cn 
 |-  0 e. CC
208 207 42 subnegi 
 |-  ( 0 - -u _pi ) = ( 0 + _pi )
209 206 208 51 3eqtri 
 |-  ( vol ` ( -u _pi (,) 0 ) ) = _pi
210 209 a1i 
 |-  ( ph -> ( vol ` ( -u _pi (,) 0 ) ) = _pi )
211 210 oveq2d 
 |-  ( ph -> ( 1 x. ( vol ` ( -u _pi (,) 0 ) ) ) = ( 1 x. _pi ) )
212 42 a1i 
 |-  ( ph -> _pi e. CC )
213 212 mulid2d 
 |-  ( ph -> ( 1 x. _pi ) = _pi )
214 211 213 eqtrd 
 |-  ( ph -> ( 1 x. ( vol ` ( -u _pi (,) 0 ) ) ) = _pi )
215 214 adantr 
 |-  ( ( ph /\ N = 0 ) -> ( 1 x. ( vol ` ( -u _pi (,) 0 ) ) ) = _pi )
216 198 204 215 3eqtrd 
 |-  ( ( ph /\ N = 0 ) -> S. ( -u _pi (,) 0 ) ( cos ` ( N x. x ) ) _d x = _pi )
217 216 oveq2d 
 |-  ( ( ph /\ N = 0 ) -> ( -u 1 x. S. ( -u _pi (,) 0 ) ( cos ` ( N x. x ) ) _d x ) = ( -u 1 x. _pi ) )
218 42 mulm1i 
 |-  ( -u 1 x. _pi ) = -u _pi
219 218 a1i 
 |-  ( ( ph /\ N = 0 ) -> ( -u 1 x. _pi ) = -u _pi )
220 iftrue 
 |-  ( N = 0 -> if ( N = 0 , -u _pi , 0 ) = -u _pi )
221 220 eqcomd 
 |-  ( N = 0 -> -u _pi = if ( N = 0 , -u _pi , 0 ) )
222 221 adantl 
 |-  ( ( ph /\ N = 0 ) -> -u _pi = if ( N = 0 , -u _pi , 0 ) )
223 217 219 222 3eqtrd 
 |-  ( ( ph /\ N = 0 ) -> ( -u 1 x. S. ( -u _pi (,) 0 ) ( cos ` ( N x. x ) ) _d x ) = if ( N = 0 , -u _pi , 0 ) )
224 25 adantr 
 |-  ( ( ph /\ -. N = 0 ) -> N e. RR )
225 3 nn0ge0d 
 |-  ( ph -> 0 <_ N )
226 225 adantr 
 |-  ( ( ph /\ -. N = 0 ) -> 0 <_ N )
227 neqne 
 |-  ( -. N = 0 -> N =/= 0 )
228 227 adantl 
 |-  ( ( ph /\ -. N = 0 ) -> N =/= 0 )
229 224 226 228 ne0gt0d 
 |-  ( ( ph /\ -. N = 0 ) -> 0 < N )
230 1cnd 
 |-  ( ( ph /\ 0 < N ) -> 1 e. CC )
231 230 negcld 
 |-  ( ( ph /\ 0 < N ) -> -u 1 e. CC )
232 231 mul01d 
 |-  ( ( ph /\ 0 < N ) -> ( -u 1 x. 0 ) = 0 )
233 119 adantr 
 |-  ( ( ph /\ 0 < N ) -> N e. CC )
234 5 a1i 
 |-  ( ( ph /\ 0 < N ) -> -u _pi e. RR )
235 0red 
 |-  ( ( ph /\ 0 < N ) -> 0 e. RR )
236 10 a1i 
 |-  ( ( ph /\ 0 < N ) -> -u _pi <_ 0 )
237 simpr 
 |-  ( ( ph /\ 0 < N ) -> 0 < N )
238 237 gt0ne0d 
 |-  ( ( ph /\ 0 < N ) -> N =/= 0 )
239 233 234 235 236 238 itgcoscmulx 
 |-  ( ( ph /\ 0 < N ) -> S. ( -u _pi (,) 0 ) ( cos ` ( N x. x ) ) _d x = ( ( ( sin ` ( N x. 0 ) ) - ( sin ` ( N x. -u _pi ) ) ) / N ) )
240 119 mul01d 
 |-  ( ph -> ( N x. 0 ) = 0 )
241 240 fveq2d 
 |-  ( ph -> ( sin ` ( N x. 0 ) ) = ( sin ` 0 ) )
242 sin0 
 |-  ( sin ` 0 ) = 0
243 241 242 eqtrdi 
 |-  ( ph -> ( sin ` ( N x. 0 ) ) = 0 )
244 119 212 mulneg2d 
 |-  ( ph -> ( N x. -u _pi ) = -u ( N x. _pi ) )
245 244 fveq2d 
 |-  ( ph -> ( sin ` ( N x. -u _pi ) ) = ( sin ` -u ( N x. _pi ) ) )
246 119 212 mulcld 
 |-  ( ph -> ( N x. _pi ) e. CC )
247 sinneg 
 |-  ( ( N x. _pi ) e. CC -> ( sin ` -u ( N x. _pi ) ) = -u ( sin ` ( N x. _pi ) ) )
248 246 247 syl 
 |-  ( ph -> ( sin ` -u ( N x. _pi ) ) = -u ( sin ` ( N x. _pi ) ) )
249 245 248 eqtrd 
 |-  ( ph -> ( sin ` ( N x. -u _pi ) ) = -u ( sin ` ( N x. _pi ) ) )
250 243 249 oveq12d 
 |-  ( ph -> ( ( sin ` ( N x. 0 ) ) - ( sin ` ( N x. -u _pi ) ) ) = ( 0 - -u ( sin ` ( N x. _pi ) ) ) )
251 0cnd 
 |-  ( ph -> 0 e. CC )
252 246 sincld 
 |-  ( ph -> ( sin ` ( N x. _pi ) ) e. CC )
253 251 252 subnegd 
 |-  ( ph -> ( 0 - -u ( sin ` ( N x. _pi ) ) ) = ( 0 + ( sin ` ( N x. _pi ) ) ) )
254 252 addid2d 
 |-  ( ph -> ( 0 + ( sin ` ( N x. _pi ) ) ) = ( sin ` ( N x. _pi ) ) )
255 250 253 254 3eqtrd 
 |-  ( ph -> ( ( sin ` ( N x. 0 ) ) - ( sin ` ( N x. -u _pi ) ) ) = ( sin ` ( N x. _pi ) ) )
256 255 adantr 
 |-  ( ( ph /\ 0 < N ) -> ( ( sin ` ( N x. 0 ) ) - ( sin ` ( N x. -u _pi ) ) ) = ( sin ` ( N x. _pi ) ) )
257 256 oveq1d 
 |-  ( ( ph /\ 0 < N ) -> ( ( ( sin ` ( N x. 0 ) ) - ( sin ` ( N x. -u _pi ) ) ) / N ) = ( ( sin ` ( N x. _pi ) ) / N ) )
258 3 nn0zd 
 |-  ( ph -> N e. ZZ )
259 sinkpi 
 |-  ( N e. ZZ -> ( sin ` ( N x. _pi ) ) = 0 )
260 258 259 syl 
 |-  ( ph -> ( sin ` ( N x. _pi ) ) = 0 )
261 260 oveq1d 
 |-  ( ph -> ( ( sin ` ( N x. _pi ) ) / N ) = ( 0 / N ) )
262 261 adantr 
 |-  ( ( ph /\ 0 < N ) -> ( ( sin ` ( N x. _pi ) ) / N ) = ( 0 / N ) )
263 233 238 div0d 
 |-  ( ( ph /\ 0 < N ) -> ( 0 / N ) = 0 )
264 262 263 eqtrd 
 |-  ( ( ph /\ 0 < N ) -> ( ( sin ` ( N x. _pi ) ) / N ) = 0 )
265 239 257 264 3eqtrd 
 |-  ( ( ph /\ 0 < N ) -> S. ( -u _pi (,) 0 ) ( cos ` ( N x. x ) ) _d x = 0 )
266 265 oveq2d 
 |-  ( ( ph /\ 0 < N ) -> ( -u 1 x. S. ( -u _pi (,) 0 ) ( cos ` ( N x. x ) ) _d x ) = ( -u 1 x. 0 ) )
267 238 neneqd 
 |-  ( ( ph /\ 0 < N ) -> -. N = 0 )
268 267 iffalsed 
 |-  ( ( ph /\ 0 < N ) -> if ( N = 0 , -u _pi , 0 ) = 0 )
269 232 266 268 3eqtr4d 
 |-  ( ( ph /\ 0 < N ) -> ( -u 1 x. S. ( -u _pi (,) 0 ) ( cos ` ( N x. x ) ) _d x ) = if ( N = 0 , -u _pi , 0 ) )
270 229 269 syldan 
 |-  ( ( ph /\ -. N = 0 ) -> ( -u 1 x. S. ( -u _pi (,) 0 ) ( cos ` ( N x. x ) ) _d x ) = if ( N = 0 , -u _pi , 0 ) )
271 223 270 pm2.61dan 
 |-  ( ph -> ( -u 1 x. S. ( -u _pi (,) 0 ) ( cos ` ( N x. x ) ) _d x ) = if ( N = 0 , -u _pi , 0 ) )
272 187 188 271 3eqtr2d 
 |-  ( ph -> S. ( -u _pi (,) 0 ) ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x = if ( N = 0 , -u _pi , 0 ) )
273 157 itgeq2dv 
 |-  ( ph -> S. ( 0 (,) _pi ) ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x = S. ( 0 (,) _pi ) ( 1 x. ( cos ` ( N x. x ) ) ) _d x )
274 96 162 182 itgmulc2 
 |-  ( ph -> ( 1 x. S. ( 0 (,) _pi ) ( cos ` ( N x. x ) ) _d x ) = S. ( 0 (,) _pi ) ( 1 x. ( cos ` ( N x. x ) ) ) _d x )
275 162 182 itgcl 
 |-  ( ph -> S. ( 0 (,) _pi ) ( cos ` ( N x. x ) ) _d x e. CC )
276 275 mulid2d 
 |-  ( ph -> ( 1 x. S. ( 0 (,) _pi ) ( cos ` ( N x. x ) ) _d x ) = S. ( 0 (,) _pi ) ( cos ` ( N x. x ) ) _d x )
277 simpl 
 |-  ( ( N = 0 /\ x e. ( 0 (,) _pi ) ) -> N = 0 )
278 277 oveq1d 
 |-  ( ( N = 0 /\ x e. ( 0 (,) _pi ) ) -> ( N x. x ) = ( 0 x. x ) )
279 131 recnd 
 |-  ( x e. ( 0 (,) _pi ) -> x e. CC )
280 279 adantl 
 |-  ( ( N = 0 /\ x e. ( 0 (,) _pi ) ) -> x e. CC )
281 280 mul02d 
 |-  ( ( N = 0 /\ x e. ( 0 (,) _pi ) ) -> ( 0 x. x ) = 0 )
282 278 281 eqtrd 
 |-  ( ( N = 0 /\ x e. ( 0 (,) _pi ) ) -> ( N x. x ) = 0 )
283 282 fveq2d 
 |-  ( ( N = 0 /\ x e. ( 0 (,) _pi ) ) -> ( cos ` ( N x. x ) ) = ( cos ` 0 ) )
284 283 195 eqtrdi 
 |-  ( ( N = 0 /\ x e. ( 0 (,) _pi ) ) -> ( cos ` ( N x. x ) ) = 1 )
285 284 adantll 
 |-  ( ( ( ph /\ N = 0 ) /\ x e. ( 0 (,) _pi ) ) -> ( cos ` ( N x. x ) ) = 1 )
286 285 itgeq2dv 
 |-  ( ( ph /\ N = 0 ) -> S. ( 0 (,) _pi ) ( cos ` ( N x. x ) ) _d x = S. ( 0 (,) _pi ) 1 _d x )
287 ioovolcl 
 |-  ( ( 0 e. RR /\ _pi e. RR ) -> ( vol ` ( 0 (,) _pi ) ) e. RR )
288 8 4 287 mp2an 
 |-  ( vol ` ( 0 (,) _pi ) ) e. RR
289 ax-1cn 
 |-  1 e. CC
290 itgconst 
 |-  ( ( ( 0 (,) _pi ) e. dom vol /\ ( vol ` ( 0 (,) _pi ) ) e. RR /\ 1 e. CC ) -> S. ( 0 (,) _pi ) 1 _d x = ( 1 x. ( vol ` ( 0 (,) _pi ) ) ) )
291 165 288 289 290 mp3an 
 |-  S. ( 0 (,) _pi ) 1 _d x = ( 1 x. ( vol ` ( 0 (,) _pi ) ) )
292 291 a1i 
 |-  ( ( ph /\ N = 0 ) -> S. ( 0 (,) _pi ) 1 _d x = ( 1 x. ( vol ` ( 0 (,) _pi ) ) ) )
293 42 mulid2i 
 |-  ( 1 x. _pi ) = _pi
294 volioo 
 |-  ( ( 0 e. RR /\ _pi e. RR /\ 0 <_ _pi ) -> ( vol ` ( 0 (,) _pi ) ) = ( _pi - 0 ) )
295 8 4 12 294 mp3an 
 |-  ( vol ` ( 0 (,) _pi ) ) = ( _pi - 0 )
296 42 subid1i 
 |-  ( _pi - 0 ) = _pi
297 295 296 eqtri 
 |-  ( vol ` ( 0 (,) _pi ) ) = _pi
298 297 oveq2i 
 |-  ( 1 x. ( vol ` ( 0 (,) _pi ) ) ) = ( 1 x. _pi )
299 298 a1i 
 |-  ( N = 0 -> ( 1 x. ( vol ` ( 0 (,) _pi ) ) ) = ( 1 x. _pi ) )
300 iftrue 
 |-  ( N = 0 -> if ( N = 0 , _pi , 0 ) = _pi )
301 293 299 300 3eqtr4a 
 |-  ( N = 0 -> ( 1 x. ( vol ` ( 0 (,) _pi ) ) ) = if ( N = 0 , _pi , 0 ) )
302 301 adantl 
 |-  ( ( ph /\ N = 0 ) -> ( 1 x. ( vol ` ( 0 (,) _pi ) ) ) = if ( N = 0 , _pi , 0 ) )
303 286 292 302 3eqtrd 
 |-  ( ( ph /\ N = 0 ) -> S. ( 0 (,) _pi ) ( cos ` ( N x. x ) ) _d x = if ( N = 0 , _pi , 0 ) )
304 260 243 oveq12d 
 |-  ( ph -> ( ( sin ` ( N x. _pi ) ) - ( sin ` ( N x. 0 ) ) ) = ( 0 - 0 ) )
305 251 subidd 
 |-  ( ph -> ( 0 - 0 ) = 0 )
306 304 305 eqtrd 
 |-  ( ph -> ( ( sin ` ( N x. _pi ) ) - ( sin ` ( N x. 0 ) ) ) = 0 )
307 306 oveq1d 
 |-  ( ph -> ( ( ( sin ` ( N x. _pi ) ) - ( sin ` ( N x. 0 ) ) ) / N ) = ( 0 / N ) )
308 307 adantr 
 |-  ( ( ph /\ 0 < N ) -> ( ( ( sin ` ( N x. _pi ) ) - ( sin ` ( N x. 0 ) ) ) / N ) = ( 0 / N ) )
309 308 263 eqtrd 
 |-  ( ( ph /\ 0 < N ) -> ( ( ( sin ` ( N x. _pi ) ) - ( sin ` ( N x. 0 ) ) ) / N ) = 0 )
310 4 a1i 
 |-  ( ( ph /\ 0 < N ) -> _pi e. RR )
311 12 a1i 
 |-  ( ( ph /\ 0 < N ) -> 0 <_ _pi )
312 233 235 310 311 238 itgcoscmulx 
 |-  ( ( ph /\ 0 < N ) -> S. ( 0 (,) _pi ) ( cos ` ( N x. x ) ) _d x = ( ( ( sin ` ( N x. _pi ) ) - ( sin ` ( N x. 0 ) ) ) / N ) )
313 267 iffalsed 
 |-  ( ( ph /\ 0 < N ) -> if ( N = 0 , _pi , 0 ) = 0 )
314 309 312 313 3eqtr4d 
 |-  ( ( ph /\ 0 < N ) -> S. ( 0 (,) _pi ) ( cos ` ( N x. x ) ) _d x = if ( N = 0 , _pi , 0 ) )
315 229 314 syldan 
 |-  ( ( ph /\ -. N = 0 ) -> S. ( 0 (,) _pi ) ( cos ` ( N x. x ) ) _d x = if ( N = 0 , _pi , 0 ) )
316 303 315 pm2.61dan 
 |-  ( ph -> S. ( 0 (,) _pi ) ( cos ` ( N x. x ) ) _d x = if ( N = 0 , _pi , 0 ) )
317 276 316 eqtrd 
 |-  ( ph -> ( 1 x. S. ( 0 (,) _pi ) ( cos ` ( N x. x ) ) _d x ) = if ( N = 0 , _pi , 0 ) )
318 273 274 317 3eqtr2d 
 |-  ( ph -> S. ( 0 (,) _pi ) ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x = if ( N = 0 , _pi , 0 ) )
319 272 318 oveq12d 
 |-  ( ph -> ( S. ( -u _pi (,) 0 ) ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x + S. ( 0 (,) _pi ) ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x ) = ( if ( N = 0 , -u _pi , 0 ) + if ( N = 0 , _pi , 0 ) ) )
320 319 oveq1d 
 |-  ( ph -> ( ( S. ( -u _pi (,) 0 ) ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x + S. ( 0 (,) _pi ) ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x ) / _pi ) = ( ( if ( N = 0 , -u _pi , 0 ) + if ( N = 0 , _pi , 0 ) ) / _pi ) )
321 220 300 oveq12d 
 |-  ( N = 0 -> ( if ( N = 0 , -u _pi , 0 ) + if ( N = 0 , _pi , 0 ) ) = ( -u _pi + _pi ) )
322 321 49 eqtrdi 
 |-  ( N = 0 -> ( if ( N = 0 , -u _pi , 0 ) + if ( N = 0 , _pi , 0 ) ) = 0 )
323 iffalse 
 |-  ( -. N = 0 -> if ( N = 0 , -u _pi , 0 ) = 0 )
324 iffalse 
 |-  ( -. N = 0 -> if ( N = 0 , _pi , 0 ) = 0 )
325 323 324 oveq12d 
 |-  ( -. N = 0 -> ( if ( N = 0 , -u _pi , 0 ) + if ( N = 0 , _pi , 0 ) ) = ( 0 + 0 ) )
326 00id 
 |-  ( 0 + 0 ) = 0
327 325 326 eqtrdi 
 |-  ( -. N = 0 -> ( if ( N = 0 , -u _pi , 0 ) + if ( N = 0 , _pi , 0 ) ) = 0 )
328 322 327 pm2.61i 
 |-  ( if ( N = 0 , -u _pi , 0 ) + if ( N = 0 , _pi , 0 ) ) = 0
329 328 oveq1i 
 |-  ( ( if ( N = 0 , -u _pi , 0 ) + if ( N = 0 , _pi , 0 ) ) / _pi ) = ( 0 / _pi )
330 8 11 gtneii 
 |-  _pi =/= 0
331 42 330 div0i 
 |-  ( 0 / _pi ) = 0
332 329 331 eqtri 
 |-  ( ( if ( N = 0 , -u _pi , 0 ) + if ( N = 0 , _pi , 0 ) ) / _pi ) = 0
333 332 a1i 
 |-  ( ph -> ( ( if ( N = 0 , -u _pi , 0 ) + if ( N = 0 , _pi , 0 ) ) / _pi ) = 0 )
334 186 320 333 3eqtrd 
 |-  ( ph -> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( cos ` ( N x. x ) ) ) _d x / _pi ) = 0 )