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 ⁢ π
sqwvfourb.f ⊢ F = x ∈ ℝ ⟼ if x mod T < π 1 − 1
sqwvfourb.n ⊢ φ → N ∈ ℕ
Assertion sqwvfourb ⊢ φ → ∫ − π π F ⁡ x ⁢ sin ⁡ N ⁢ x dx π = if 2 ∥ N 0 4 N ⁢ π

Proof

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