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	⊢ 𝑇 = ( 2 · π )
	sqwvfoura.f	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) )
	sqwvfoura.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	sqwvfoura	⊢ ( 𝜑 → ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 / π ) = 0 )

Proof

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