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 \in ℝ ⟼ if (x \mod T < π, 1, - 1))$
	sqwvfourb.n	$⊢ φ \to N \in ℕ$
Assertion	sqwvfourb	$⊢ φ \to \frac{\int_{(- π, π)} F (x) \sin N x d x}{π} = if (2 ∥ N, 0, \frac{4}{N π})$

Proof

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

Metamath Proof Explorer

Theorem sqwvfourb

Proof