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

Proof

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

Metamath Proof Explorer

Theorem sqwvfoura

Proof