Theorem sqwvfoura 39121

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

Hypotheses

Ref	Expression
sqwvfoura.t	⊢ 𝑇 = (2 · π)
sqwvfoura.f	⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1))
sqwvfoura.n	⊢ (𝜑 → 𝑁 ∈ ℕ0)

Assertion

Ref	Expression
sqwvfoura	⊢ (𝜑 → (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 / π) = 0)

Distinct variable groups:   𝑥,𝑁   𝜑,𝑥

Allowed substitution hints:   𝑇(𝑥)   𝐹(𝑥)

Proof of Theorem sqwvfoura

Step	Hyp	Ref	Expression
1		pire 24014	. . . . . 6 ⊢ π ∈ ℝ
2	1	renegcli 10221	. . . . 5 ⊢ -π ∈ ℝ
3	2	a1i 11	. . . 4 ⊢ (𝜑 → -π ∈ ℝ)
4	1	a1i 11	. . . 4 ⊢ (𝜑 → π ∈ ℝ)
5		0re 9919	. . . . . 6 ⊢ 0 ∈ ℝ
6		negpilt0 38433	. . . . . . 7 ⊢ -π < 0
7	2, 5, 6	ltleii 10039	. . . . . 6 ⊢ -π ≤ 0
8		pipos 24016	. . . . . . 7 ⊢ 0 < π
9	5, 1, 8	ltleii 10039	. . . . . 6 ⊢ 0 ≤ π
10	2, 1	elicc2i 12110	. . . . . 6 ⊢ (0 ∈ (-π[,]π) ↔ (0 ∈ ℝ ∧ -π ≤ 0 ∧ 0 ≤ π))
11	5, 7, 9, 10	mpbir3an 1237	. . . . 5 ⊢ 0 ∈ (-π[,]π)
12	11	a1i 11	. . . 4 ⊢ (𝜑 → 0 ∈ (-π[,]π))
13		1red 9934	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → 1 ∈ ℝ)
14	13	renegcld 10336	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → -1 ∈ ℝ)
15	13, 14	ifcld 4081	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ)
16	15	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ)
17		sqwvfoura.f	. . . . . . . . 9 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1))
18	16, 17	fmptd 6292	. . . . . . . 8 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
19	18	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π(,)π)) → 𝐹:ℝ⟶ℝ)
20		elioore 12076	. . . . . . . 8 ⊢ (𝑥 ∈ (-π(,)π) → 𝑥 ∈ ℝ)
21	20	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π(,)π)) → 𝑥 ∈ ℝ)
22	19, 21	ffvelrnd 6268	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π(,)π)) → (𝐹‘𝑥) ∈ ℝ)
23		sqwvfoura.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
24	23	nn0red 11229	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℝ)
25	24	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π(,)π)) → 𝑁 ∈ ℝ)
26	25, 21	remulcld 9949	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π(,)π)) → (𝑁 · 𝑥) ∈ ℝ)
27	26	recoscld 14713	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π(,)π)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
28	22, 27	remulcld 9949	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π(,)π)) → ((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) ∈ ℝ)
29	28	recnd 9947	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π(,)π)) → ((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) ∈ ℂ)
30		elioore 12076	. . . . . . . . . 10 ⊢ (𝑥 ∈ (-π(,)0) → 𝑥 ∈ ℝ)
31	30, 15	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ (-π(,)0) → if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ)
32	17	fvmpt2 6200	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ ∧ if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ) → (𝐹‘𝑥) = if((𝑥 mod 𝑇) < π, 1, -1))
33	30, 31, 32	syl2anc 691	. . . . . . . . 9 ⊢ (𝑥 ∈ (-π(,)0) → (𝐹‘𝑥) = if((𝑥 mod 𝑇) < π, 1, -1))
34	1	a1i 11	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-π(,)0) → π ∈ ℝ)
35		sqwvfoura.t	. . . . . . . . . . . . . 14 ⊢ 𝑇 = (2 · π)
36		2rp 11713	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ+
37		pirp 24017	. . . . . . . . . . . . . . 15 ⊢ π ∈ ℝ+
38		rpmulcl 11731	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℝ+ ∧ π ∈ ℝ+) → (2 · π) ∈ ℝ+)
39	36, 37, 38	mp2an 704	. . . . . . . . . . . . . 14 ⊢ (2 · π) ∈ ℝ+
40	35, 39	eqeltri 2684	. . . . . . . . . . . . 13 ⊢ 𝑇 ∈ ℝ+
41	40	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (-π(,)0) → 𝑇 ∈ ℝ+)
42	30, 41	modcld 12536	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-π(,)0) → (𝑥 mod 𝑇) ∈ ℝ)
43		picn 24015	. . . . . . . . . . . . . . . . 17 ⊢ π ∈ ℂ
44	43	2timesi 11024	. . . . . . . . . . . . . . . 16 ⊢ (2 · π) = (π + π)
45	35, 44	eqtri 2632	. . . . . . . . . . . . . . 15 ⊢ 𝑇 = (π + π)
46	45	oveq2i 6560	. . . . . . . . . . . . . 14 ⊢ (-π + 𝑇) = (-π + (π + π))
47	2	recni 9931	. . . . . . . . . . . . . . 15 ⊢ -π ∈ ℂ
48	47, 43, 43	addassi 9927	. . . . . . . . . . . . . 14 ⊢ ((-π + π) + π) = (-π + (π + π))
49	43	negidi 10229	. . . . . . . . . . . . . . . . 17 ⊢ (π + -π) = 0
50	43, 47, 49	addcomli 10107	. . . . . . . . . . . . . . . 16 ⊢ (-π + π) = 0
51	50	oveq1i 6559	. . . . . . . . . . . . . . 15 ⊢ ((-π + π) + π) = (0 + π)
52	43	addid2i 10103	. . . . . . . . . . . . . . 15 ⊢ (0 + π) = π
53	51, 52	eqtri 2632	. . . . . . . . . . . . . 14 ⊢ ((-π + π) + π) = π
54	46, 48, 53	3eqtr2ri 2639	. . . . . . . . . . . . 13 ⊢ π = (-π + 𝑇)
55	2	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (-π(,)0) → -π ∈ ℝ)
56		2re 10967	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ
57	56, 1	remulcli 9933	. . . . . . . . . . . . . . . 16 ⊢ (2 · π) ∈ ℝ
58	35, 57	eqeltri 2684	. . . . . . . . . . . . . . 15 ⊢ 𝑇 ∈ ℝ
59	58	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (-π(,)0) → 𝑇 ∈ ℝ)
60	2	rexri 9976	. . . . . . . . . . . . . . . 16 ⊢ -π ∈ ℝ*
61	60	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (-π(,)0) → -π ∈ ℝ*)
62		0red 9920	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (-π(,)0) → 0 ∈ ℝ)
63	62	rexrd 9968	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (-π(,)0) → 0 ∈ ℝ*)
64		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (-π(,)0) → 𝑥 ∈ (-π(,)0))
65		ioogtlb 38564	. . . . . . . . . . . . . . 15 ⊢ ((-π ∈ ℝ* ∧ 0 ∈ ℝ* ∧ 𝑥 ∈ (-π(,)0)) → -π < 𝑥)
66	61, 63, 64, 65	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (-π(,)0) → -π < 𝑥)
67	55, 30, 59, 66	ltadd1dd 10517	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (-π(,)0) → (-π + 𝑇) < (𝑥 + 𝑇))
68	54, 67	syl5eqbr 4618	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (-π(,)0) → π < (𝑥 + 𝑇))
69	58	recni 9931	. . . . . . . . . . . . . . . . 17 ⊢ 𝑇 ∈ ℂ
70	69	mulid2i 9922	. . . . . . . . . . . . . . . 16 ⊢ (1 · 𝑇) = 𝑇
71	70	eqcomi 2619	. . . . . . . . . . . . . . 15 ⊢ 𝑇 = (1 · 𝑇)
72	71	oveq2i 6560	. . . . . . . . . . . . . 14 ⊢ (𝑥 + 𝑇) = (𝑥 + (1 · 𝑇))
73	72	oveq1i 6559	. . . . . . . . . . . . 13 ⊢ ((𝑥 + 𝑇) mod 𝑇) = ((𝑥 + (1 · 𝑇)) mod 𝑇)
74	30, 59	readdcld 9948	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) ∈ ℝ)
75	8	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (-π(,)0) → 0 < π)
76	62, 34, 74, 75, 68	lttrd 10077	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (-π(,)0) → 0 < (𝑥 + 𝑇))
77	62, 74, 76	ltled 10064	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (-π(,)0) → 0 ≤ (𝑥 + 𝑇))
78		iooltub 38582	. . . . . . . . . . . . . . . . 17 ⊢ ((-π ∈ ℝ* ∧ 0 ∈ ℝ* ∧ 𝑥 ∈ (-π(,)0)) → 𝑥 < 0)
79	61, 63, 64, 78	syl3anc 1318	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (-π(,)0) → 𝑥 < 0)
80	30, 62, 59, 79	ltadd1dd 10517	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) < (0 + 𝑇))
81	69	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (-π(,)0) → 𝑇 ∈ ℂ)
82	81	addid2d 10116	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (-π(,)0) → (0 + 𝑇) = 𝑇)
83	80, 82	breqtrd 4609	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) < 𝑇)
84		modid 12557	. . . . . . . . . . . . . 14 ⊢ ((((𝑥 + 𝑇) ∈ ℝ ∧ 𝑇 ∈ ℝ+) ∧ (0 ≤ (𝑥 + 𝑇) ∧ (𝑥 + 𝑇) < 𝑇)) → ((𝑥 + 𝑇) mod 𝑇) = (𝑥 + 𝑇))
85	74, 41, 77, 83, 84	syl22anc 1319	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (-π(,)0) → ((𝑥 + 𝑇) mod 𝑇) = (𝑥 + 𝑇))
86		1zzd 11285	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (-π(,)0) → 1 ∈ ℤ)
87		modcyc 12567	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ 𝑇 ∈ ℝ+ ∧ 1 ∈ ℤ) → ((𝑥 + (1 · 𝑇)) mod 𝑇) = (𝑥 mod 𝑇))
88	30, 41, 86, 87	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (-π(,)0) → ((𝑥 + (1 · 𝑇)) mod 𝑇) = (𝑥 mod 𝑇))
89	73, 85, 88	3eqtr3a 2668	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) = (𝑥 mod 𝑇))
90	68, 89	breqtrd 4609	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-π(,)0) → π < (𝑥 mod 𝑇))
91	34, 42, 90	ltnsymd 10065	. . . . . . . . . 10 ⊢ (𝑥 ∈ (-π(,)0) → ¬ (𝑥 mod 𝑇) < π)
92	91	iffalsed 4047	. . . . . . . . 9 ⊢ (𝑥 ∈ (-π(,)0) → if((𝑥 mod 𝑇) < π, 1, -1) = -1)
93	33, 92	eqtrd 2644	. . . . . . . 8 ⊢ (𝑥 ∈ (-π(,)0) → (𝐹‘𝑥) = -1)
94	93	oveq1d 6564	. . . . . . 7 ⊢ (𝑥 ∈ (-π(,)0) → ((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) = (-1 · (cos‘(𝑁 · 𝑥))))
95	94	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π(,)0)) → ((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) = (-1 · (cos‘(𝑁 · 𝑥))))
96	95	mpteq2dva 4672	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (-π(,)0) ↦ ((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥)))) = (𝑥 ∈ (-π(,)0) ↦ (-1 · (cos‘(𝑁 · 𝑥)))))
97		1cnd 9935	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℂ)
98	97	negcld 10258	. . . . . 6 ⊢ (𝜑 → -1 ∈ ℂ)
99	24	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π(,)0)) → 𝑁 ∈ ℝ)
100	30	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π(,)0)) → 𝑥 ∈ ℝ)
101	99, 100	remulcld 9949	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π(,)0)) → (𝑁 · 𝑥) ∈ ℝ)
102	101	recoscld 14713	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π(,)0)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
103		ioossicc 12130	. . . . . . . 8 ⊢ (-π(,)0) ⊆ (-π[,]0)
104	103	a1i 11	. . . . . . 7 ⊢ (𝜑 → (-π(,)0) ⊆ (-π[,]0))
105		ioombl 23140	. . . . . . . 8 ⊢ (-π(,)0) ∈ dom vol
106	105	a1i 11	. . . . . . 7 ⊢ (𝜑 → (-π(,)0) ∈ dom vol)
107	24	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]0)) → 𝑁 ∈ ℝ)
108		iccssre 12126	. . . . . . . . . . . 12 ⊢ ((-π ∈ ℝ ∧ 0 ∈ ℝ) → (-π[,]0) ⊆ ℝ)
109	2, 5, 108	mp2an 704	. . . . . . . . . . 11 ⊢ (-π[,]0) ⊆ ℝ
110	109	sseli 3564	. . . . . . . . . 10 ⊢ (𝑥 ∈ (-π[,]0) → 𝑥 ∈ ℝ)
111	110	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]0)) → 𝑥 ∈ ℝ)
112	107, 111	remulcld 9949	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]0)) → (𝑁 · 𝑥) ∈ ℝ)
113	112	recoscld 14713	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]0)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
114		0red 9920	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℝ)
115		coscn 24003	. . . . . . . . . 10 ⊢ cos ∈ (ℂ–cn→ℂ)
116	115	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → cos ∈ (ℂ–cn→ℂ))
117		ax-resscn 9872	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
118	109, 117	sstri 3577	. . . . . . . . . . . 12 ⊢ (-π[,]0) ⊆ ℂ
119	118	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (-π[,]0) ⊆ ℂ)
120	24	recnd 9947	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℂ)
121		ssid 3587	. . . . . . . . . . . 12 ⊢ ℂ ⊆ ℂ
122	121	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℂ ⊆ ℂ)
123	119, 120, 122	constcncfg 38756	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (-π[,]0) ↦ 𝑁) ∈ ((-π[,]0)–cn→ℂ))
124	119, 122	idcncfg 38757	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (-π[,]0) ↦ 𝑥) ∈ ((-π[,]0)–cn→ℂ))
125	123, 124	mulcncf 23023	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (-π[,]0) ↦ (𝑁 · 𝑥)) ∈ ((-π[,]0)–cn→ℂ))
126	116, 125	cncfmpt1f 22524	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (-π[,]0) ↦ (cos‘(𝑁 · 𝑥))) ∈ ((-π[,]0)–cn→ℂ))
127		cniccibl 23413	. . . . . . . 8 ⊢ ((-π ∈ ℝ ∧ 0 ∈ ℝ ∧ (𝑥 ∈ (-π[,]0) ↦ (cos‘(𝑁 · 𝑥))) ∈ ((-π[,]0)–cn→ℂ)) → (𝑥 ∈ (-π[,]0) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
128	3, 114, 126, 127	syl3anc 1318	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (-π[,]0) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
129	104, 106, 113, 128	iblss 23377	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (-π(,)0) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
130	98, 102, 129	iblmulc2 23403	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (-π(,)0) ↦ (-1 · (cos‘(𝑁 · 𝑥)))) ∈ 𝐿1)
131	96, 130	eqeltrd 2688	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (-π(,)0) ↦ ((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥)))) ∈ 𝐿1)
132		elioore 12076	. . . . . . . . . 10 ⊢ (𝑥 ∈ (0(,)π) → 𝑥 ∈ ℝ)
133	132, 15	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ (0(,)π) → if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ)
134	132, 133, 32	syl2anc 691	. . . . . . . . 9 ⊢ (𝑥 ∈ (0(,)π) → (𝐹‘𝑥) = if((𝑥 mod 𝑇) < π, 1, -1))
135	40	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0(,)π) → 𝑇 ∈ ℝ+)
136		0red 9920	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (0(,)π) → 0 ∈ ℝ)
137	136	rexrd 9968	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (0(,)π) → 0 ∈ ℝ*)
138	1	rexri 9976	. . . . . . . . . . . . . . 15 ⊢ π ∈ ℝ*
139	138	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (0(,)π) → π ∈ ℝ*)
140		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (0(,)π) → 𝑥 ∈ (0(,)π))
141		ioogtlb 38564	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑥 ∈ (0(,)π)) → 0 < 𝑥)
142	137, 139, 140, 141	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (0(,)π) → 0 < 𝑥)
143	136, 132, 142	ltled 10064	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0(,)π) → 0 ≤ 𝑥)
144	1	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (0(,)π) → π ∈ ℝ)
145	58	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (0(,)π) → 𝑇 ∈ ℝ)
146		iooltub 38582	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑥 ∈ (0(,)π)) → 𝑥 < π)
147	137, 139, 140, 146	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (0(,)π) → 𝑥 < π)
148		2timesgt 38441	. . . . . . . . . . . . . . . 16 ⊢ (π ∈ ℝ+ → π < (2 · π))
149	37, 148	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ π < (2 · π)
150	149, 35	breqtrri 4610	. . . . . . . . . . . . . 14 ⊢ π < 𝑇
151	150	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (0(,)π) → π < 𝑇)
152	132, 144, 145, 147, 151	lttrd 10077	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0(,)π) → 𝑥 < 𝑇)
153		modid 12557	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ ∧ 𝑇 ∈ ℝ+) ∧ (0 ≤ 𝑥 ∧ 𝑥 < 𝑇)) → (𝑥 mod 𝑇) = 𝑥)
154	132, 135, 143, 152, 153	syl22anc 1319	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0(,)π) → (𝑥 mod 𝑇) = 𝑥)
155	154, 147	eqbrtrd 4605	. . . . . . . . . 10 ⊢ (𝑥 ∈ (0(,)π) → (𝑥 mod 𝑇) < π)
156	155	iftrued 4044	. . . . . . . . 9 ⊢ (𝑥 ∈ (0(,)π) → if((𝑥 mod 𝑇) < π, 1, -1) = 1)
157	134, 156	eqtrd 2644	. . . . . . . 8 ⊢ (𝑥 ∈ (0(,)π) → (𝐹‘𝑥) = 1)
158	157	oveq1d 6564	. . . . . . 7 ⊢ (𝑥 ∈ (0(,)π) → ((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) = (1 · (cos‘(𝑁 · 𝑥))))
159	158	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → ((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) = (1 · (cos‘(𝑁 · 𝑥))))
160	159	mpteq2dva 4672	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥)))) = (𝑥 ∈ (0(,)π) ↦ (1 · (cos‘(𝑁 · 𝑥)))))
161	24	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → 𝑁 ∈ ℝ)
162	132	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → 𝑥 ∈ ℝ)
163	161, 162	remulcld 9949	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 · 𝑥) ∈ ℝ)
164	163	recoscld 14713	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)π)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
165		ioossicc 12130	. . . . . . . 8 ⊢ (0(,)π) ⊆ (0[,]π)
166	165	a1i 11	. . . . . . 7 ⊢ (𝜑 → (0(,)π) ⊆ (0[,]π))
167		ioombl 23140	. . . . . . . 8 ⊢ (0(,)π) ∈ dom vol
168	167	a1i 11	. . . . . . 7 ⊢ (𝜑 → (0(,)π) ∈ dom vol)
169	24	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → 𝑁 ∈ ℝ)
170		iccssre 12126	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ π ∈ ℝ) → (0[,]π) ⊆ ℝ)
171	5, 1, 170	mp2an 704	. . . . . . . . . . 11 ⊢ (0[,]π) ⊆ ℝ
172	171	sseli 3564	. . . . . . . . . 10 ⊢ (𝑥 ∈ (0[,]π) → 𝑥 ∈ ℝ)
173	172	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → 𝑥 ∈ ℝ)
174	169, 173	remulcld 9949	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (𝑁 · 𝑥) ∈ ℝ)
175	174	recoscld 14713	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]π)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
176	171, 117	sstri 3577	. . . . . . . . . . . 12 ⊢ (0[,]π) ⊆ ℂ
177	176	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (0[,]π) ⊆ ℂ)
178	177, 120, 122	constcncfg 38756	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ 𝑁) ∈ ((0[,]π)–cn→ℂ))
179	177, 122	idcncfg 38757	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ 𝑥) ∈ ((0[,]π)–cn→ℂ))
180	178, 179	mulcncf 23023	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (𝑁 · 𝑥)) ∈ ((0[,]π)–cn→ℂ))
181	116, 180	cncfmpt1f 22524	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (cos‘(𝑁 · 𝑥))) ∈ ((0[,]π)–cn→ℂ))
182		cniccibl 23413	. . . . . . . 8 ⊢ ((0 ∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ (cos‘(𝑁 · 𝑥))) ∈ ((0[,]π)–cn→ℂ)) → (𝑥 ∈ (0[,]π) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
183	114, 4, 181, 182	syl3anc 1318	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (0[,]π) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
184	166, 168, 175, 183	iblss 23377	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
185	97, 164, 184	iblmulc2 23403	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ (1 · (cos‘(𝑁 · 𝑥)))) ∈ 𝐿1)
186	160, 185	eqeltrd 2688	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥)))) ∈ 𝐿1)
187	3, 4, 12, 29, 131, 186	itgsplitioo 23410	. . 3 ⊢ (𝜑 → ∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = (∫(-π(,)0)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥))
188	187	oveq1d 6564	. 2 ⊢ (𝜑 → (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 / π) = ((∫(-π(,)0)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥) / π))
189	95	itgeq2dv 23354	. . . . 5 ⊢ (𝜑 → ∫(-π(,)0)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = ∫(-π(,)0)(-1 · (cos‘(𝑁 · 𝑥))) d𝑥)
190	98, 102, 129	itgmulc2 23406	. . . . 5 ⊢ (𝜑 → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = ∫(-π(,)0)(-1 · (cos‘(𝑁 · 𝑥))) d𝑥)
191		oveq1 6556	. . . . . . . . . . . . . 14 ⊢ (𝑁 = 0 → (𝑁 · 𝑥) = (0 · 𝑥))
192		ioosscn 38563	. . . . . . . . . . . . . . . 16 ⊢ (-π(,)0) ⊆ ℂ
193	192	sseli 3564	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (-π(,)0) → 𝑥 ∈ ℂ)
194	193	mul02d 10113	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (-π(,)0) → (0 · 𝑥) = 0)
195	191, 194	sylan9eq 2664	. . . . . . . . . . . . 13 ⊢ ((𝑁 = 0 ∧ 𝑥 ∈ (-π(,)0)) → (𝑁 · 𝑥) = 0)
196	195	fveq2d 6107	. . . . . . . . . . . 12 ⊢ ((𝑁 = 0 ∧ 𝑥 ∈ (-π(,)0)) → (cos‘(𝑁 · 𝑥)) = (cos‘0))
197		cos0 14719	. . . . . . . . . . . 12 ⊢ (cos‘0) = 1
198	196, 197	syl6eq 2660	. . . . . . . . . . 11 ⊢ ((𝑁 = 0 ∧ 𝑥 ∈ (-π(,)0)) → (cos‘(𝑁 · 𝑥)) = 1)
199	198	adantll 746	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 = 0) ∧ 𝑥 ∈ (-π(,)0)) → (cos‘(𝑁 · 𝑥)) = 1)
200	199	itgeq2dv 23354	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑁 = 0) → ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥 = ∫(-π(,)0)1 d𝑥)
201		ioovolcl 23144	. . . . . . . . . . . . 13 ⊢ ((-π ∈ ℝ ∧ 0 ∈ ℝ) → (vol‘(-π(,)0)) ∈ ℝ)
202	2, 5, 201	mp2an 704	. . . . . . . . . . . 12 ⊢ (vol‘(-π(,)0)) ∈ ℝ
203	202	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (vol‘(-π(,)0)) ∈ ℝ)
204		itgconst 23391	. . . . . . . . . . 11 ⊢ (((-π(,)0) ∈ dom vol ∧ (vol‘(-π(,)0)) ∈ ℝ ∧ 1 ∈ ℂ) → ∫(-π(,)0)1 d𝑥 = (1 · (vol‘(-π(,)0))))
205	106, 203, 97, 204	syl3anc 1318	. . . . . . . . . 10 ⊢ (𝜑 → ∫(-π(,)0)1 d𝑥 = (1 · (vol‘(-π(,)0))))
206	205	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑁 = 0) → ∫(-π(,)0)1 d𝑥 = (1 · (vol‘(-π(,)0))))
207		volioo 38840	. . . . . . . . . . . . . . 15 ⊢ ((-π ∈ ℝ ∧ 0 ∈ ℝ ∧ -π ≤ 0) → (vol‘(-π(,)0)) = (0 − -π))
208	2, 5, 7, 207	mp3an 1416	. . . . . . . . . . . . . 14 ⊢ (vol‘(-π(,)0)) = (0 − -π)
209		0cn 9911	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℂ
210	209, 43	subnegi 10239	. . . . . . . . . . . . . 14 ⊢ (0 − -π) = (0 + π)
211	208, 210, 52	3eqtri 2636	. . . . . . . . . . . . 13 ⊢ (vol‘(-π(,)0)) = π
212	211	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (vol‘(-π(,)0)) = π)
213	212	oveq2d 6565	. . . . . . . . . . 11 ⊢ (𝜑 → (1 · (vol‘(-π(,)0))) = (1 · π))
214	43	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → π ∈ ℂ)
215	214	mulid2d 9937	. . . . . . . . . . 11 ⊢ (𝜑 → (1 · π) = π)
216	213, 215	eqtrd 2644	. . . . . . . . . 10 ⊢ (𝜑 → (1 · (vol‘(-π(,)0))) = π)
217	216	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑁 = 0) → (1 · (vol‘(-π(,)0))) = π)
218	200, 206, 217	3eqtrd 2648	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑁 = 0) → ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥 = π)
219	218	oveq2d 6565	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 = 0) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = (-1 · π))
220	43	mulm1i 10354	. . . . . . . 8 ⊢ (-1 · π) = -π
221	220	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 = 0) → (-1 · π) = -π)
222		iftrue 4042	. . . . . . . . 9 ⊢ (𝑁 = 0 → if(𝑁 = 0, -π, 0) = -π)
223	222	eqcomd 2616	. . . . . . . 8 ⊢ (𝑁 = 0 → -π = if(𝑁 = 0, -π, 0))
224	223	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 = 0) → -π = if(𝑁 = 0, -π, 0))
225	219, 221, 224	3eqtrd 2648	. . . . . 6 ⊢ ((𝜑 ∧ 𝑁 = 0) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, -π, 0))
226	24	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑁 = 0) → 𝑁 ∈ ℝ)
227	23	nn0ge0d 11231	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝑁)
228	227	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑁 = 0) → 0 ≤ 𝑁)
229		neqne 2790	. . . . . . . . 9 ⊢ (¬ 𝑁 = 0 → 𝑁 ≠ 0)
230	229	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑁 = 0) → 𝑁 ≠ 0)
231	226, 228, 230	ne0gt0d 10053	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝑁 = 0) → 0 < 𝑁)
232		1cnd 9935	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 0 < 𝑁) → 1 ∈ ℂ)
233	232	negcld 10258	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 < 𝑁) → -1 ∈ ℂ)
234	233	mul01d 10114	. . . . . . . 8 ⊢ ((𝜑 ∧ 0 < 𝑁) → (-1 · 0) = 0)
235	120	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 0 < 𝑁) → 𝑁 ∈ ℂ)
236	2	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 0 < 𝑁) → -π ∈ ℝ)
237		0red 9920	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 0 < 𝑁) → 0 ∈ ℝ)
238	7	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 0 < 𝑁) → -π ≤ 0)
239		simpr 476	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 0 < 𝑁) → 0 < 𝑁)
240	239	gt0ne0d 10471	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 0 < 𝑁) → 𝑁 ≠ 0)
241	235, 236, 237, 238, 240	itgcoscmulx 38861	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 0 < 𝑁) → ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥 = (((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) / 𝑁))
242	120	mul01d 10114	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 · 0) = 0)
243	242	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (sin‘(𝑁 · 0)) = (sin‘0))
244		sin0 14718	. . . . . . . . . . . . . . 15 ⊢ (sin‘0) = 0
245	243, 244	syl6eq 2660	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (sin‘(𝑁 · 0)) = 0)
246	120, 214	mulneg2d 10363	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 · -π) = -(𝑁 · π))
247	246	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (sin‘(𝑁 · -π)) = (sin‘-(𝑁 · π)))
248	120, 214	mulcld 9939	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 · π) ∈ ℂ)
249		sinneg 14715	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 · π) ∈ ℂ → (sin‘-(𝑁 · π)) = -(sin‘(𝑁 · π)))
250	248, 249	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (sin‘-(𝑁 · π)) = -(sin‘(𝑁 · π)))
251	247, 250	eqtrd 2644	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (sin‘(𝑁 · -π)) = -(sin‘(𝑁 · π)))
252	245, 251	oveq12d 6567	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) = (0 − -(sin‘(𝑁 · π))))
253		0cnd 9912	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ ℂ)
254	248	sincld 14699	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (sin‘(𝑁 · π)) ∈ ℂ)
255	253, 254	subnegd 10278	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0 − -(sin‘(𝑁 · π))) = (0 + (sin‘(𝑁 · π))))
256	254	addid2d 10116	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0 + (sin‘(𝑁 · π))) = (sin‘(𝑁 · π)))
257	252, 255, 256	3eqtrd 2648	. . . . . . . . . . . 12 ⊢ (𝜑 → ((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) = (sin‘(𝑁 · π)))
258	257	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 0 < 𝑁) → ((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) = (sin‘(𝑁 · π)))
259	258	oveq1d 6564	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 0 < 𝑁) → (((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) / 𝑁) = ((sin‘(𝑁 · π)) / 𝑁))
260	23	nn0zd 11356	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℤ)
261		sinkpi 24075	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℤ → (sin‘(𝑁 · π)) = 0)
262	260, 261	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (sin‘(𝑁 · π)) = 0)
263	262	oveq1d 6564	. . . . . . . . . . . 12 ⊢ (𝜑 → ((sin‘(𝑁 · π)) / 𝑁) = (0 / 𝑁))
264	263	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 0 < 𝑁) → ((sin‘(𝑁 · π)) / 𝑁) = (0 / 𝑁))
265	235, 240	div0d 10679	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 0 < 𝑁) → (0 / 𝑁) = 0)
266	264, 265	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 0 < 𝑁) → ((sin‘(𝑁 · π)) / 𝑁) = 0)
267	241, 259, 266	3eqtrd 2648	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 < 𝑁) → ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥 = 0)
268	267	oveq2d 6565	. . . . . . . 8 ⊢ ((𝜑 ∧ 0 < 𝑁) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = (-1 · 0))
269	240	neneqd 2787	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 < 𝑁) → ¬ 𝑁 = 0)
270	269	iffalsed 4047	. . . . . . . 8 ⊢ ((𝜑 ∧ 0 < 𝑁) → if(𝑁 = 0, -π, 0) = 0)
271	234, 268, 270	3eqtr4d 2654	. . . . . . 7 ⊢ ((𝜑 ∧ 0 < 𝑁) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, -π, 0))
272	231, 271	syldan 486	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝑁 = 0) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, -π, 0))
273	225, 272	pm2.61dan 828	. . . . 5 ⊢ (𝜑 → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, -π, 0))
274	189, 190, 273	3eqtr2d 2650	. . . 4 ⊢ (𝜑 → ∫(-π(,)0)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = if(𝑁 = 0, -π, 0))
275	159	itgeq2dv 23354	. . . . 5 ⊢ (𝜑 → ∫(0(,)π)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = ∫(0(,)π)(1 · (cos‘(𝑁 · 𝑥))) d𝑥)
276	97, 164, 184	itgmulc2 23406	. . . . 5 ⊢ (𝜑 → (1 · ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥) = ∫(0(,)π)(1 · (cos‘(𝑁 · 𝑥))) d𝑥)
277	164, 184	itgcl 23356	. . . . . . 7 ⊢ (𝜑 → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 ∈ ℂ)
278	277	mulid2d 9937	. . . . . 6 ⊢ (𝜑 → (1 · ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥) = ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥)
279		simpl 472	. . . . . . . . . . . . . 14 ⊢ ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → 𝑁 = 0)
280	279	oveq1d 6564	. . . . . . . . . . . . 13 ⊢ ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 · 𝑥) = (0 · 𝑥))
281	132	recnd 9947	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0(,)π) → 𝑥 ∈ ℂ)
282	281	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → 𝑥 ∈ ℂ)
283	282	mul02d 10113	. . . . . . . . . . . . 13 ⊢ ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (0 · 𝑥) = 0)
284	280, 283	eqtrd 2644	. . . . . . . . . . . 12 ⊢ ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 · 𝑥) = 0)
285	284	fveq2d 6107	. . . . . . . . . . 11 ⊢ ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (cos‘(𝑁 · 𝑥)) = (cos‘0))
286	285, 197	syl6eq 2660	. . . . . . . . . 10 ⊢ ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (cos‘(𝑁 · 𝑥)) = 1)
287	286	adantll 746	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 = 0) ∧ 𝑥 ∈ (0(,)π)) → (cos‘(𝑁 · 𝑥)) = 1)
288	287	itgeq2dv 23354	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑁 = 0) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = ∫(0(,)π)1 d𝑥)
289		ioovolcl 23144	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ π ∈ ℝ) → (vol‘(0(,)π)) ∈ ℝ)
290	5, 1, 289	mp2an 704	. . . . . . . . . 10 ⊢ (vol‘(0(,)π)) ∈ ℝ
291		ax-1cn 9873	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
292		itgconst 23391	. . . . . . . . . 10 ⊢ (((0(,)π) ∈ dom vol ∧ (vol‘(0(,)π)) ∈ ℝ ∧ 1 ∈ ℂ) → ∫(0(,)π)1 d𝑥 = (1 · (vol‘(0(,)π))))
293	167, 290, 291, 292	mp3an 1416	. . . . . . . . 9 ⊢ ∫(0(,)π)1 d𝑥 = (1 · (vol‘(0(,)π)))
294	293	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑁 = 0) → ∫(0(,)π)1 d𝑥 = (1 · (vol‘(0(,)π))))
295	43	mulid2i 9922	. . . . . . . . . 10 ⊢ (1 · π) = π
296		volioo 38840	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ π ∈ ℝ ∧ 0 ≤ π) → (vol‘(0(,)π)) = (π − 0))
297	5, 1, 9, 296	mp3an 1416	. . . . . . . . . . . . 13 ⊢ (vol‘(0(,)π)) = (π − 0)
298	43	subid1i 10232	. . . . . . . . . . . . 13 ⊢ (π − 0) = π
299	297, 298	eqtri 2632	. . . . . . . . . . . 12 ⊢ (vol‘(0(,)π)) = π
300	299	oveq2i 6560	. . . . . . . . . . 11 ⊢ (1 · (vol‘(0(,)π))) = (1 · π)
301	300	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 = 0 → (1 · (vol‘(0(,)π))) = (1 · π))
302		iftrue 4042	. . . . . . . . . 10 ⊢ (𝑁 = 0 → if(𝑁 = 0, π, 0) = π)
303	295, 301, 302	3eqtr4a 2670	. . . . . . . . 9 ⊢ (𝑁 = 0 → (1 · (vol‘(0(,)π))) = if(𝑁 = 0, π, 0))
304	303	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑁 = 0) → (1 · (vol‘(0(,)π))) = if(𝑁 = 0, π, 0))
305	288, 294, 304	3eqtrd 2648	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 = 0) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = if(𝑁 = 0, π, 0))
306	262, 245	oveq12d 6567	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) = (0 − 0))
307	253	subidd 10259	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0 − 0) = 0)
308	306, 307	eqtrd 2644	. . . . . . . . . . . 12 ⊢ (𝜑 → ((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) = 0)
309	308	oveq1d 6564	. . . . . . . . . . 11 ⊢ (𝜑 → (((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) / 𝑁) = (0 / 𝑁))
310	309	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 0 < 𝑁) → (((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) / 𝑁) = (0 / 𝑁))
311	310, 265	eqtrd 2644	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 < 𝑁) → (((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) / 𝑁) = 0)
312	1	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 0 < 𝑁) → π ∈ ℝ)
313	9	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 0 < 𝑁) → 0 ≤ π)
314	235, 237, 312, 313, 240	itgcoscmulx 38861	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 < 𝑁) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = (((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) / 𝑁))
315	269	iffalsed 4047	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 < 𝑁) → if(𝑁 = 0, π, 0) = 0)
316	311, 314, 315	3eqtr4d 2654	. . . . . . . 8 ⊢ ((𝜑 ∧ 0 < 𝑁) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = if(𝑁 = 0, π, 0))
317	231, 316	syldan 486	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝑁 = 0) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = if(𝑁 = 0, π, 0))
318	305, 317	pm2.61dan 828	. . . . . 6 ⊢ (𝜑 → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = if(𝑁 = 0, π, 0))
319	278, 318	eqtrd 2644	. . . . 5 ⊢ (𝜑 → (1 · ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, π, 0))
320	275, 276, 319	3eqtr2d 2650	. . . 4 ⊢ (𝜑 → ∫(0(,)π)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = if(𝑁 = 0, π, 0))
321	274, 320	oveq12d 6567	. . 3 ⊢ (𝜑 → (∫(-π(,)0)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥) = (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)))
322	321	oveq1d 6564	. 2 ⊢ (𝜑 → ((∫(-π(,)0)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥) / π) = ((if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) / π))
323	222, 302	oveq12d 6567	. . . . . . 7 ⊢ (𝑁 = 0 → (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = (-π + π))
324	323, 50	syl6eq 2660	. . . . . 6 ⊢ (𝑁 = 0 → (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = 0)
325		iffalse 4045	. . . . . . . 8 ⊢ (¬ 𝑁 = 0 → if(𝑁 = 0, -π, 0) = 0)
326		iffalse 4045	. . . . . . . 8 ⊢ (¬ 𝑁 = 0 → if(𝑁 = 0, π, 0) = 0)
327	325, 326	oveq12d 6567	. . . . . . 7 ⊢ (¬ 𝑁 = 0 → (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = (0 + 0))
328		00id 10090	. . . . . . 7 ⊢ (0 + 0) = 0
329	327, 328	syl6eq 2660	. . . . . 6 ⊢ (¬ 𝑁 = 0 → (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = 0)
330	324, 329	pm2.61i 175	. . . . 5 ⊢ (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = 0
331	330	oveq1i 6559	. . . 4 ⊢ ((if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) / π) = (0 / π)
332	5, 8	gtneii 10028	. . . . 5 ⊢ π ≠ 0
333	43, 332	div0i 10638	. . . 4 ⊢ (0 / π) = 0
334	331, 333	eqtri 2632	. . 3 ⊢ ((if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) / π) = 0
335	334	a1i 11	. 2 ⊢ (𝜑 → ((if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) / π) = 0)
336	188, 322, 335	3eqtrd 2648	1 ⊢ (𝜑 → (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 / π) = 0)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780   ⊆ wss 3540  ifcif 4036   class class class wbr 4583   ↦ cmpt 4643  dom cdm 5038  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  ℝ^*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145  -cneg 10146   / cdiv 10563  2c2 10947  ℕ₀cn0 11169  ℤcz 11254  ℝ⁺crp 11708  (,)cioo 12046  [,]cicc 12049   mod cmo 12530  sincsin 14633  cosccos 14634  πcpi 14636  –cn→ccncf 22487  volcvol 23039  𝐿¹cibl 23192  ∫citg 23193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cc 9140  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-disj 4554  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-ofr 6796  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-omul 7452  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-acn 8651  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ioc 12051  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-fac 12923  df-bc 12952  df-hash 12980  df-shft 13655  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-limsup 14050  df-clim 14067  df-rlim 14068  df-sum 14265  df-ef 14637  df-sin 14639  df-cos 14640  df-pi 14642  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-hom 15793  df-cco 15794  df-rest 15906  df-topn 15907  df-0g 15925  df-gsum 15926  df-topgen 15927  df-pt 15928  df-prds 15931  df-xrs 15985  df-qtop 15990  df-imas 15991  df-xps 15993  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-mulg 17364  df-cntz 17573  df-cmn 18018  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-fbas 19564  df-fg 19565  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cld 20633  df-ntr 20634  df-cls 20635  df-nei 20712  df-lp 20750  df-perf 20751  df-cn 20841  df-cnp 20842  df-haus 20929  df-cmp 21000  df-tx 21175  df-hmeo 21368  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-xms 21935  df-ms 21936  df-tms 21937  df-cncf 22489  df-ovol 23040  df-vol 23041  df-mbf 23194  df-itg1 23195  df-itg2 23196  df-ibl 23197  df-itg 23198  df-0p 23243  df-limc 23436  df-dv 23437

This theorem is referenced by:  fouriersw  39124