fourierdlem83 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fourierdlem83		Structured version Visualization version GIF version

Theorem fourierdlem83 39082

Description: The fourier partial sum for 𝐹 rewritten as an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem83.f	⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
fourierdlem83.c	⊢ 𝐶 = (-π(,)π)
fourierdlem83.fl1	⊢ (𝜑 → (𝐹 ↾ 𝐶) ∈ 𝐿¹)
fourierdlem83.a	⊢ 𝐴 = (𝑛 ∈ ℕ₀ ↦ (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
fourierdlem83.b	⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
fourierdlem83.x	⊢ (𝜑 → 𝑋 ∈ ℝ)
fourierdlem83.s	⊢ 𝑆 = (𝑚 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
fourierdlem83.d	⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))))))
fourierdlem83.n	⊢ (𝜑 → 𝑁 ∈ ℕ)

**Assertion**
Ref	Expression
fourierdlem83	⊢ (𝜑 → (𝑆‘𝑁) = ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥)

Distinct variable groups: 𝐴,𝑚,𝑛 𝐵,𝑚 𝑥,𝐶,𝑛,𝑠 𝑥,𝐷,𝑠 𝑛,𝐹,𝑥 𝑥,𝑁 𝑚,𝑁,𝑛 𝑁,𝑠 𝑥,𝑋 𝑚,𝑋,𝑛 𝑋,𝑠 𝜑,𝑥,𝑛 𝜑,𝑚 𝜑,𝑠 Allowed substitution hints: 𝐴(𝑥,𝑠) 𝐵(𝑥,𝑛,𝑠) 𝐶(𝑚) 𝐷(𝑚,𝑛) 𝑆(𝑥,𝑚,𝑛,𝑠) 𝐹(𝑚,𝑠)

Proof of Theorem fourierdlem83 Dummy variables 𝑏 𝑐 𝑦 𝑘 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem83.s	. . . 4 ⊢ 𝑆 = (𝑚 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
2	1	a1i 11	. . 3 ⊢ (𝜑 → 𝑆 = (𝑚 ∈ ℕ ↦ (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))))
3		oveq2 6557	. . . . . 6 ⊢ (𝑚 = 𝑁 → (1...𝑚) = (1...𝑁))
4	3	sumeq1d 14279	. . . . 5 ⊢ (𝑚 = 𝑁 → Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
5	4	oveq2d 6565	. . . 4 ⊢ (𝑚 = 𝑁 → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
6	5	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝑚 = 𝑁) → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
7		fourierdlem83.n	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ)
8		id 22	. . . . . 6 ⊢ (𝜑 → 𝜑)
9		0nn0 11184	. . . . . . 7 ⊢ 0 ∈ ℕ₀
10	9	a1i 11	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℕ₀)
11	9	elexi 3186	. . . . . . 7 ⊢ 0 ∈ V
12		eleq1 2676	. . . . . . . . 9 ⊢ (𝑛 = 0 → (𝑛 ∈ ℕ₀ ↔ 0 ∈ ℕ₀))
13	12	anbi2d 736	. . . . . . . 8 ⊢ (𝑛 = 0 → ((𝜑 ∧ 𝑛 ∈ ℕ₀) ↔ (𝜑 ∧ 0 ∈ ℕ₀)))
14		fveq2 6103	. . . . . . . . 9 ⊢ (𝑛 = 0 → (𝐴‘𝑛) = (𝐴‘0))
15	14	eleq1d 2672	. . . . . . . 8 ⊢ (𝑛 = 0 → ((𝐴‘𝑛) ∈ ℝ ↔ (𝐴‘0) ∈ ℝ))
16	13, 15	imbi12d 333	. . . . . . 7 ⊢ (𝑛 = 0 → (((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝐴‘𝑛) ∈ ℝ) ↔ ((𝜑 ∧ 0 ∈ ℕ₀) → (𝐴‘0) ∈ ℝ)))
17		fourierdlem83.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
18		fourierdlem83.c	. . . . . . . . . 10 ⊢ 𝐶 = (-π(,)π)
19		fourierdlem83.fl1	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 ↾ 𝐶) ∈ 𝐿¹)
20		fourierdlem83.a	. . . . . . . . . 10 ⊢ 𝐴 = (𝑛 ∈ ℕ₀ ↦ (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
21		fourierdlem83.b	. . . . . . . . . 10 ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
22	17, 18, 19, 20, 21	fourierdlem22 39022	. . . . . . . . 9 ⊢ (𝜑 → ((𝑛 ∈ ℕ₀ → (𝐴‘𝑛) ∈ ℝ) ∧ (𝑛 ∈ ℕ → (𝐵‘𝑛) ∈ ℝ)))
23	22	simpld 474	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ ℕ₀ → (𝐴‘𝑛) ∈ ℝ))
24	23	imp 444	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝐴‘𝑛) ∈ ℝ)
25	11, 16, 24	vtocl 3232	. . . . . 6 ⊢ ((𝜑 ∧ 0 ∈ ℕ₀) → (𝐴‘0) ∈ ℝ)
26	8, 10, 25	syl2anc 691	. . . . 5 ⊢ (𝜑 → (𝐴‘0) ∈ ℝ)
27	26	rehalfcld 11156	. . . 4 ⊢ (𝜑 → ((𝐴‘0) / 2) ∈ ℝ)
28		fzfid 12634	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
29		eleq1 2676	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ ℕ₀ ↔ 𝑛 ∈ ℕ₀))
30	29	anbi2d 736	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → ((𝜑 ∧ 𝑘 ∈ ℕ₀) ↔ (𝜑 ∧ 𝑛 ∈ ℕ₀)))
31		simpl 472	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → 𝑘 = 𝑛)
32	31	oveq1d 6564	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → (𝑘 · 𝑥) = (𝑛 · 𝑥))
33	32	fveq2d 6107	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑘 · 𝑥)) = (cos‘(𝑛 · 𝑥)))
34	33	oveq2d 6565	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))
35	34	itgeq2dv 23354	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥)
36	35	eleq1d 2672	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ ↔ ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ))
37	30, 36	imbi12d 333	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → (((𝜑 ∧ 𝑘 ∈ ℕ₀) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ) ↔ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)))
38	17	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝐹:ℝ⟶ℝ)
39	19	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐹 ↾ 𝐶) ∈ 𝐿¹)
40		simpr 476	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
41	38, 18, 39, 20, 40	fourierdlem16 39016	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝐴‘𝑘) ∈ ℝ ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹) ∧ ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ))
42	41	simprd 478	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ)
43	37, 42	chvarv 2251	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
44		pire 24014	. . . . . . . . . . . 12 ⊢ π ∈ ℝ
45	44	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → π ∈ ℝ)
46		0re 9919	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
47		pipos 24016	. . . . . . . . . . . . 13 ⊢ 0 < π
48	46, 47	gtneii 10028	. . . . . . . . . . . 12 ⊢ π ≠ 0
49	48	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → π ≠ 0)
50	43, 45, 49	redivcld 10732	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
51	50, 20	fmptd 6292	. . . . . . . . 9 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℝ)
52	51	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐴:ℕ₀⟶ℝ)
53		elfznn 12241	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
54	53	nnnn0d 11228	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ₀)
55	54	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ₀)
56	52, 55	ffvelrnd 6268	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐴‘𝑛) ∈ ℝ)
57	55	nn0red 11229	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℝ)
58		fourierdlem83.x	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℝ)
59	58	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℝ)
60	57, 59	remulcld 9949	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 · 𝑋) ∈ ℝ)
61	60	recoscld 14713	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℝ)
62	56, 61	remulcld 9949	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
63		eleq1 2676	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ ℕ ↔ 𝑛 ∈ ℕ))
64	63	anbi2d 736	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → ((𝜑 ∧ 𝑘 ∈ ℕ) ↔ (𝜑 ∧ 𝑛 ∈ ℕ)))
65		oveq1 6556	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → (𝑘 · 𝑥) = (𝑛 · 𝑥))
66	65	fveq2d 6107	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → (sin‘(𝑘 · 𝑥)) = (sin‘(𝑛 · 𝑥)))
67	66	oveq2d 6565	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑛 → ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
68	67	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
69	68	itgeq2dv 23354	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥)
70	69	eleq1d 2672	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ ↔ ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ))
71	64, 70	imbi12d 333	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → (((𝜑 ∧ 𝑘 ∈ ℕ) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ) ↔ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)))
72	17	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:ℝ⟶ℝ)
73	19	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹 ↾ 𝐶) ∈ 𝐿¹)
74		simpr 476	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
75	72, 18, 73, 21, 74	fourierdlem21 39021	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐵‘𝑘) ∈ ℝ ∧ (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥)))) ∈ 𝐿¹) ∧ ∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ))
76	75	simprd 478	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ)
77	71, 76	chvarv 2251	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
78	44	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → π ∈ ℝ)
79	48	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → π ≠ 0)
80	77, 78, 79	redivcld 10732	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
81	80, 21	fmptd 6292	. . . . . . . . 9 ⊢ (𝜑 → 𝐵:ℕ⟶ℝ)
82	81	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐵:ℕ⟶ℝ)
83	53	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ)
84	82, 83	ffvelrnd 6268	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐵‘𝑛) ∈ ℝ)
85	60	resincld 14712	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
86	84, 85	remulcld 9949	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
87	62, 86	readdcld 9948	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
88	28, 87	fsumrecl 14312	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
89	27, 88	readdcld 9948	. . 3 ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) ∈ ℝ)
90	2, 6, 7, 89	fvmptd 6197	. 2 ⊢ (𝜑 → (𝑆‘𝑁) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
91	20	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐴 = (𝑛 ∈ ℕ₀ ↦ (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
92		oveq1 6556	. . . . . . . . . . . . 13 ⊢ (𝑛 = 0 → (𝑛 · 𝑥) = (0 · 𝑥))
93	92	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (𝑛 = 0 → (cos‘(𝑛 · 𝑥)) = (cos‘(0 · 𝑥)))
94	93	oveq2d 6565	. . . . . . . . . . 11 ⊢ (𝑛 = 0 → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(0 · 𝑥))))
95	94	adantr 480	. . . . . . . . . 10 ⊢ ((𝑛 = 0 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(0 · 𝑥))))
96	95	itgeq2dv 23354	. . . . . . . . 9 ⊢ (𝑛 = 0 → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥)
97	96	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 0) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥)
98	97	oveq1d 6564	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 = 0) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) = (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
99	17, 18, 19, 20, 10	fourierdlem16 39016	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴‘0) ∈ ℝ ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹) ∧ ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 ∈ ℝ))
100	99	simprd 478	. . . . . . . 8 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 ∈ ℝ)
101	44	a1i 11	. . . . . . . 8 ⊢ (𝜑 → π ∈ ℝ)
102	48	a1i 11	. . . . . . . 8 ⊢ (𝜑 → π ≠ 0)
103	100, 101, 102	redivcld 10732	. . . . . . 7 ⊢ (𝜑 → (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) ∈ ℝ)
104	91, 98, 10, 103	fvmptd 6197	. . . . . 6 ⊢ (𝜑 → (𝐴‘0) = (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
105		ioosscn 38563	. . . . . . . . . . . . . . 15 ⊢ (-π(,)π) ⊆ ℂ
106		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐶)
107	106, 18	syl6eleq 2698	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ (-π(,)π))
108	105, 107	sseldi 3566	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ℂ)
109	108	mul02d 10113	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐶 → (0 · 𝑥) = 0)
110	109	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐶 → (cos‘(0 · 𝑥)) = (cos‘0))
111		cos0 14719	. . . . . . . . . . . 12 ⊢ (cos‘0) = 1
112	110, 111	syl6eq 2660	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐶 → (cos‘(0 · 𝑥)) = 1)
113	112	oveq2d 6565	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐶 → ((𝐹‘𝑥) · (cos‘(0 · 𝑥))) = ((𝐹‘𝑥) · 1))
114	113	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(0 · 𝑥))) = ((𝐹‘𝑥) · 1))
115	17	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐹:ℝ⟶ℝ)
116		ioossre 12106	. . . . . . . . . . . . . 14 ⊢ (-π(,)π) ⊆ ℝ
117	116, 107	sseldi 3566	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ℝ)
118	117	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
119	115, 118	ffvelrnd 6268	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
120	119	recnd 9947	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
121	120	mulid1d 9936	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · 1) = (𝐹‘𝑥))
122	114, 121	eqtrd 2644	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(0 · 𝑥))) = (𝐹‘𝑥))
123	122	itgeq2dv 23354	. . . . . . 7 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 = ∫𝐶(𝐹‘𝑥) d𝑥)
124	123	oveq1d 6564	. . . . . 6 ⊢ (𝜑 → (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) = (∫𝐶(𝐹‘𝑥) d𝑥 / π))
125	104, 124	eqtrd 2644	. . . . 5 ⊢ (𝜑 → (𝐴‘0) = (∫𝐶(𝐹‘𝑥) d𝑥 / π))
126	125	oveq1d 6564	. . . 4 ⊢ (𝜑 → ((𝐴‘0) / 2) = ((∫𝐶(𝐹‘𝑥) d𝑥 / π) / 2))
127	17	feqmptd 6159	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)))
128	127	reseq1d 5316	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ 𝐶))
129	44	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐶 → π ∈ ℝ)
130	129	renegcld 10336	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐶 → -π ∈ ℝ)
131		ioossicc 12130	. . . . . . . . . . . . 13 ⊢ (-π(,)π) ⊆ (-π[,]π)
132	18, 131	eqsstri 3598	. . . . . . . . . . . 12 ⊢ 𝐶 ⊆ (-π[,]π)
133	132	sseli 3564	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ (-π[,]π))
134		eliccre 38575	. . . . . . . . . . 11 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ ∧ 𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
135	130, 129, 133, 134	syl3anc 1318	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ℝ)
136	135	ssriv 3572	. . . . . . . . 9 ⊢ 𝐶 ⊆ ℝ
137		resmpt 5369	. . . . . . . . 9 ⊢ (𝐶 ⊆ ℝ → ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
138	136, 137	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
139	128, 138	eqtr2d 2645	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝐹 ↾ 𝐶))
140	139, 19	eqeltrd 2688	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
141	119, 140	itgcl 23356	. . . . 5 ⊢ (𝜑 → ∫𝐶(𝐹‘𝑥) d𝑥 ∈ ℂ)
142	101	recnd 9947	. . . . 5 ⊢ (𝜑 → π ∈ ℂ)
143		2cnd 10970	. . . . 5 ⊢ (𝜑 → 2 ∈ ℂ)
144		2ne0 10990	. . . . . 6 ⊢ 2 ≠ 0
145	144	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ≠ 0)
146	141, 142, 143, 102, 145	divdiv32d 10705	. . . 4 ⊢ (𝜑 → ((∫𝐶(𝐹‘𝑥) d𝑥 / π) / 2) = ((∫𝐶(𝐹‘𝑥) d𝑥 / 2) / π))
147	141, 143, 145	divrecd 10683	. . . . . 6 ⊢ (𝜑 → (∫𝐶(𝐹‘𝑥) d𝑥 / 2) = (∫𝐶(𝐹‘𝑥) d𝑥 · (1 / 2)))
148	143, 145	reccld 10673	. . . . . . 7 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
149	141, 148	mulcomd 9940	. . . . . 6 ⊢ (𝜑 → (∫𝐶(𝐹‘𝑥) d𝑥 · (1 / 2)) = ((1 / 2) · ∫𝐶(𝐹‘𝑥) d𝑥))
150	148, 119, 140	itgmulc2 23406	. . . . . 6 ⊢ (𝜑 → ((1 / 2) · ∫𝐶(𝐹‘𝑥) d𝑥) = ∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥)
151	147, 149, 150	3eqtrd 2648	. . . . 5 ⊢ (𝜑 → (∫𝐶(𝐹‘𝑥) d𝑥 / 2) = ∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥)
152	151	oveq1d 6564	. . . 4 ⊢ (𝜑 → ((∫𝐶(𝐹‘𝑥) d𝑥 / 2) / π) = (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π))
153	126, 146, 152	3eqtrd 2648	. . 3 ⊢ (𝜑 → ((𝐴‘0) / 2) = (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π))
154	55, 50	syldan 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
155	20	fvmpt2 6200	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ₀ ∧ (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐴‘𝑛) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
156	55, 154, 155	syl2anc 691	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐴‘𝑛) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
157	156	oveq1d 6564	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))))
158	154	recnd 9947	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
159	61	recnd 9947	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℂ)
160	158, 159	mulcomd 9940	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
161	55, 43	syldan 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
162	161	recnd 9947	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
163	142	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → π ∈ ℂ)
164	48	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → π ≠ 0)
165	159, 162, 163, 164	divassd 10715	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
166	17	ad2antrr 758	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → 𝐹:ℝ⟶ℝ)
167	117	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
168	166, 167	ffvelrnd 6268	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
169		nn0re 11178	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℝ)
170	169	ad2antlr 759	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
171	170, 167	remulcld 9949	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℝ)
172	171	recoscld 14713	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
173	168, 172	remulcld 9949	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
174	54, 173	sylanl2 681	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
175		ioombl 23140	. . . . . . . . . . . . . . . . . . 19 ⊢ (-π(,)π) ∈ dom vol
176	18, 175	eqeltri 2684	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐶 ∈ dom vol
177	176	elexi 3186	. . . . . . . . . . . . . . . . 17 ⊢ 𝐶 ∈ V
178	177	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝐶 ∈ V)
179		eqidd 2611	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))))
180		eqidd 2611	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
181	178, 172, 168, 179, 180	offval2 6812	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_𝑓 · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
182	172	recnd 9947	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℂ)
183	120	adantlr 747	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
184	182, 183	mulcomd 9940	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))
185	184	mpteq2dva 4672	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))))
186	181, 185	eqtr2d 2645	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_𝑓 · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
187		coscn 24003	. . . . . . . . . . . . . . . . . 18 ⊢ cos ∈ (ℂ–cn→ℂ)
188	187	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → cos ∈ (ℂ–cn→ℂ))
189		ax-resscn 9872	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℝ ⊆ ℂ
190	136, 189	sstri 3577	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐶 ⊆ ℂ
191	190	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝐶 ⊆ ℂ)
192	169	recnd 9947	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℂ)
193	192	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝑛 ∈ ℂ)
194		ssid 3587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℂ ⊆ ℂ
195	194	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ℂ ⊆ ℂ)
196	191, 193, 195	constcncfg 38756	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ 𝑛) ∈ (𝐶–cn→ℂ))
197	191, 195	idcncfg 38757	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ 𝑥) ∈ (𝐶–cn→ℂ))
198	196, 197	mulcncf 23023	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶–cn→ℂ))
199	188, 198	cncfmpt1f 22524	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ))
200		cnmbf 23232	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ dom vol ∧ (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
201	176, 199, 200	sylancr 694	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
202	140	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
203		1re 9918	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
204		simpr 476	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))))
205	169	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
206	117	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
207	205, 206	remulcld 9949	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℝ)
208	207	recoscld 14713	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
209	208	ralrimiva 2949	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ₀ → ∀𝑥 ∈ 𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
210	209	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → ∀𝑥 ∈ 𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
211		dmmptg 5549	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 ∈ 𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ → dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
212	210, 211	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
213	204, 212	eleqtrd 2690	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦 ∈ 𝐶)
214		eqidd 2611	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))))
215		oveq2 6557	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑛 · 𝑥) = (𝑛 · 𝑦))
216	215	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
217	216	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
218		simpr 476	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
219	169	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → 𝑛 ∈ ℝ)
220	136, 218	sseldi 3566	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
221	219, 220	remulcld 9949	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (𝑛 · 𝑦) ∈ ℝ)
222	221	recoscld 14713	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (cos‘(𝑛 · 𝑦)) ∈ ℝ)
223	214, 217, 218, 222	fvmptd 6197	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦) = (cos‘(𝑛 · 𝑦)))
224	223	fveq2d 6107	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(cos‘(𝑛 · 𝑦))))
225		abscosbd 38431	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 · 𝑦) ∈ ℝ → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
226	221, 225	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
227	224, 226	eqbrtrd 4605	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
228	213, 227	syldan 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
229	228	ralrimiva 2949	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
230		breq2 4587	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 1 → ((abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
231	230	ralbidv 2969	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
232	231	rspcev 3282	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
233	203, 229, 232	sylancr 694	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ₀ → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
234	233	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
235		bddmulibl 23411	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_𝑓 · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
236	201, 202, 234, 235	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_𝑓 · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
237	186, 236	eqeltrd 2688	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
238	55, 237	syldan 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
239	159, 174, 238	itgmulc2 23406	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) d𝑥)
240	159	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑋)) ∈ ℂ)
241	120	adantlr 747	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
242	54, 182	sylanl2 681	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℂ)
243	240, 241, 242	mul12d 10124	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))))
244	240, 242	mulcomd 9940	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥))) = ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))
245	244	oveq2d 6565	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
246	243, 245	eqtrd 2644	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
247	246	itgeq2dv 23354	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
248	239, 247	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
249	248	oveq1d 6564	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
250	165, 249	eqtr3d 2646	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
251	157, 160, 250	3eqtrd 2648	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
252	83, 80	syldan 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
253	21	fvmpt2 6200	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐵‘𝑛) = (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
254	83, 252, 253	syl2anc 691	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐵‘𝑛) = (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
255	254	oveq1d 6564	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))))
256	252	recnd 9947	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
257	85	recnd 9947	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℂ)
258	256, 257	mulcomd 9940	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
259	83, 77	syldan 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
260	259	recnd 9947	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
261	257, 260, 163, 164	divassd 10715	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
262	119	adantlr 747	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
263		nnre 10904	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
264	263	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
265	117	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
266	264, 265	remulcld 9949	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℝ)
267	266	resincld 14712	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
268	267	adantll 746	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
269	262, 268	remulcld 9949	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
270	53, 269	sylanl2 681	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
271	177	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 ∈ V)
272		eqidd 2611	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))))
273		eqidd 2611	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
274	271, 268, 262, 272, 273	offval2 6812	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_𝑓 · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
275	268	recnd 9947	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℂ)
276	120	adantlr 747	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
277	275, 276	mulcomd 9940	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
278	277	mpteq2dva 4672	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))))
279	274, 278	eqtr2d 2645	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_𝑓 · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
280		sincn 24002	. . . . . . . . . . . . . . . . . 18 ⊢ sin ∈ (ℂ–cn→ℂ)
281	280	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sin ∈ (ℂ–cn→ℂ))
282	190	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → 𝐶 ⊆ ℂ)
283	263	recnd 9947	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
284	194	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → ℂ ⊆ ℂ)
285	282, 283, 284	constcncfg 38756	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (𝑥 ∈ 𝐶 ↦ 𝑛) ∈ (𝐶–cn→ℂ))
286	282, 284	idcncfg 38757	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (𝑥 ∈ 𝐶 ↦ 𝑥) ∈ (𝐶–cn→ℂ))
287	285, 286	mulcncf 23023	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → (𝑥 ∈ 𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶–cn→ℂ))
288	287	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶–cn→ℂ))
289	281, 288	cncfmpt1f 22524	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ))
290		cnmbf 23232	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ dom vol ∧ (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ)) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn)
291	176, 289, 290	sylancr 694	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn)
292	140	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
293		simpr 476	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))))
294	267	ralrimiva 2949	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → ∀𝑥 ∈ 𝐶 (sin‘(𝑛 · 𝑥)) ∈ ℝ)
295		dmmptg 5549	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑥 ∈ 𝐶 (sin‘(𝑛 · 𝑥)) ∈ ℝ → dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
296	294, 295	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ℕ → dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
297	296	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
298	293, 297	eleqtrd 2690	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦 ∈ 𝐶)
299		eqidd 2611	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))))
300	215	fveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
301	300	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
302		simpr 476	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
303	263	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → 𝑛 ∈ ℝ)
304	136, 302	sseldi 3566	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
305	303, 304	remulcld 9949	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (𝑛 · 𝑦) ∈ ℝ)
306	305	resincld 14712	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (sin‘(𝑛 · 𝑦)) ∈ ℝ)
307	299, 301, 302, 306	fvmptd 6197	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦) = (sin‘(𝑛 · 𝑦)))
308	307	fveq2d 6107	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(sin‘(𝑛 · 𝑦))))
309		abssinbd 38450	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 · 𝑦) ∈ ℝ → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
310	305, 309	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
311	308, 310	eqbrtrd 4605	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
312	298, 311	syldan 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
313	312	ralrimiva 2949	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
314		breq2 4587	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 1 → ((abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
315	314	ralbidv 2969	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
316	315	rspcev 3282	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
317	203, 313, 316	sylancr 694	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
318	317	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
319		bddmulibl 23411	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_𝑓 · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
320	291, 292, 318, 319	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_𝑓 · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
321	279, 320	eqeltrd 2688	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
322	83, 321	syldan 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
323	257, 270, 322	itgmulc2 23406	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) d𝑥)
324	257	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑋)) ∈ ℂ)
325	53, 275	sylanl2 681	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℂ)
326	324, 241, 325	mul12d 10124	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))))
327	324, 325	mulcomd 9940	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥))) = ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))
328	327	oveq2d 6565	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
329	326, 328	eqtrd 2644	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
330	329	itgeq2dv 23354	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
331	323, 330	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
332	331	oveq1d 6564	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
333	261, 332	eqtr3d 2646	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
334	255, 258, 333	3eqtrd 2648	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
335	251, 334	oveq12d 6567	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π) + (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π)))
336	54, 168	sylanl2 681	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
337	55, 208	sylan 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
338	61	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑋)) ∈ ℝ)
339	337, 338	remulcld 9949	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
340	336, 339	remulcld 9949	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) ∈ ℝ)
341	241, 242, 240	mul13d 38432	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
342	242, 241	mulcomd 9940	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))
343	342	oveq2d 6565	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))))
344	341, 343	eqtrd 2644	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))))
345	344	mpteq2dva 4672	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) = (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))))
346	159, 174, 238	iblmulc2 23403	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))) ∈ 𝐿¹)
347	345, 346	eqeltrd 2688	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) ∈ 𝐿¹)
348	340, 347	itgcl 23356	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
349	83, 267	sylan 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
350	85	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
351	349, 350	remulcld 9949	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
352	336, 351	remulcld 9949	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
353	241, 325, 324	mul13d 38432	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
354	325, 241	mulcomd 9940	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
355	354	oveq2d 6565	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))))
356	353, 355	eqtrd 2644	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))))
357	356	mpteq2dva 4672	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))))
358	257, 270, 322	iblmulc2 23403	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))) ∈ 𝐿¹)
359	357, 358	eqeltrd 2688	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) ∈ 𝐿¹)
360	352, 359	itgcl 23356	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
361	348, 360, 163, 164	divdird 10718	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π) + (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π)))
362	53	nncnd 10913	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
363	362	ad2antlr 759	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℂ)
364	108	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℂ)
365	58	recnd 9947	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ ℂ)
366	365	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑋 ∈ ℂ)
367	363, 364, 366	subdid 10365	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · (𝑥 − 𝑋)) = ((𝑛 · 𝑥) − (𝑛 · 𝑋)))
368	367	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) = (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))))
369	363, 364	mulcld 9939	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℂ)
370	363, 366	mulcld 9939	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑋) ∈ ℂ)
371		cossub 14738	. . . . . . . . . . . . 13 ⊢ (((𝑛 · 𝑥) ∈ ℂ ∧ (𝑛 · 𝑋) ∈ ℂ) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
372	369, 370, 371	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
373	368, 372	eqtrd 2644	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
374	373	oveq2d 6565	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) = ((𝐹‘𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
375	339	recnd 9947	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℂ)
376	351	recnd 9947	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℂ)
377	241, 375, 376	adddid 9943	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
378	374, 377	eqtrd 2644	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) = (((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
379	378	itgeq2dv 23354	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = ∫𝐶(((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥)
380	340, 347, 352, 359	itgadd 23397	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶(((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥 = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥))
381	379, 380	eqtr2d 2645	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) = ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥)
382	381	oveq1d 6564	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
383	335, 361, 382	3eqtr2d 2650	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
384	383	sumeq2dv 14281	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
385	57	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
386	117	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
387	58	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑋 ∈ ℝ)
388	386, 387	resubcld 10337	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑥 − 𝑋) ∈ ℝ)
389	385, 388	remulcld 9949	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · (𝑥 − 𝑋)) ∈ ℝ)
390	389	recoscld 14713	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
391	336, 390	remulcld 9949	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
392	177	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ V)
393		eqidd 2611	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))))
394		eqidd 2611	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
395	392, 390, 336, 393, 394	offval2 6812	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_𝑓 · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · (𝑥 − 𝑋))) · (𝐹‘𝑥))))
396	390	recnd 9947	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℂ)
397	396, 241	mulcomd 9940	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · (𝑥 − 𝑋))) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))))
398	397	mpteq2dva 4672	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · (𝑥 − 𝑋))) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))))
399	395, 398	eqtr2d 2645	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) = ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_𝑓 · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
400	187	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → cos ∈ (ℂ–cn→ℂ))
401	83, 285	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ 𝑛) ∈ (𝐶–cn→ℂ))
402	83, 286	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ 𝑥) ∈ (𝐶–cn→ℂ))
403	190	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ⊆ ℂ)
404	365	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
405	194	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ℂ ⊆ ℂ)
406	403, 404, 405	constcncfg 38756	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ 𝑋) ∈ (𝐶–cn→ℂ))
407	402, 406	subcncf 38754	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝑥 − 𝑋)) ∈ (𝐶–cn→ℂ))
408	401, 407	mulcncf 23023	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝑛 · (𝑥 − 𝑋))) ∈ (𝐶–cn→ℂ))
409	400, 408	cncfmpt1f 22524	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ (𝐶–cn→ℂ))
410		cnmbf 23232	. . . . . . . . 9 ⊢ ((𝐶 ∈ dom vol ∧ (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ (𝐶–cn→ℂ)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ MblFn)
411	176, 409, 410	sylancr 694	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ MblFn)
412	140	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
413		simpr 476	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))) → 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))))
414	390	ralrimiva 2949	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∀𝑥 ∈ 𝐶 (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
415		dmmptg 5549	. . . . . . . . . . . . . 14 ⊢ (∀𝑥 ∈ 𝐶 (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ → dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) = 𝐶)
416	414, 415	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) = 𝐶)
417	416	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))) → dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) = 𝐶)
418	413, 417	eleqtrd 2690	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))) → 𝑦 ∈ 𝐶)
419		eqidd 2611	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))))
420		oveq1 6556	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝑥 − 𝑋) = (𝑦 − 𝑋))
421	420	oveq2d 6565	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑛 · (𝑥 − 𝑋)) = (𝑛 · (𝑦 − 𝑋)))
422	421	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (cos‘(𝑛 · (𝑥 − 𝑋))) = (cos‘(𝑛 · (𝑦 − 𝑋))))
423	422	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → (cos‘(𝑛 · (𝑥 − 𝑋))) = (cos‘(𝑛 · (𝑦 − 𝑋))))
424		simpr 476	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
425	57	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → 𝑛 ∈ ℝ)
426	55, 220	sylan 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
427	58	ad2antrr 758	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → 𝑋 ∈ ℝ)
428	426, 427	resubcld 10337	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (𝑦 − 𝑋) ∈ ℝ)
429	425, 428	remulcld 9949	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (𝑛 · (𝑦 − 𝑋)) ∈ ℝ)
430	429	recoscld 14713	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (cos‘(𝑛 · (𝑦 − 𝑋))) ∈ ℝ)
431	419, 423, 424, 430	fvmptd 6197	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦) = (cos‘(𝑛 · (𝑦 − 𝑋))))
432	431	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) = (abs‘(cos‘(𝑛 · (𝑦 − 𝑋)))))
433		abscosbd 38431	. . . . . . . . . . . . 13 ⊢ ((𝑛 · (𝑦 − 𝑋)) ∈ ℝ → (abs‘(cos‘(𝑛 · (𝑦 − 𝑋)))) ≤ 1)
434	429, 433	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (abs‘(cos‘(𝑛 · (𝑦 − 𝑋)))) ≤ 1)
435	432, 434	eqbrtrd 4605	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1)
436	418, 435	syldan 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1)
437	436	ralrimiva 2949	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1)
438		breq2 4587	. . . . . . . . . . 11 ⊢ (𝑏 = 1 → ((abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1))
439	438	ralbidv 2969	. . . . . . . . . 10 ⊢ (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1))
440	439	rspcev 3282	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏)
441	203, 437, 440	sylancr 694	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏)
442		bddmulibl 23411	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_𝑓 · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
443	411, 412, 441, 442	syl3anc 1318	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_𝑓 · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
444	399, 443	eqeltrd 2688	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) ∈ 𝐿¹)
445	391, 444	itgcl 23356	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 ∈ ℂ)
446	28, 142, 445, 102	fsumdivc 14360	. . . 4 ⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π) = Σ𝑛 ∈ (1...𝑁)(∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
447	176	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ dom vol)
448		anass 679	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑥 ∈ 𝐶)))
449		ancom 465	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (1...𝑁) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐶 ∧ 𝑛 ∈ (1...𝑁)))
450	449	anbi2i 726	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑥 ∈ 𝐶)) ↔ (𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑛 ∈ (1...𝑁))))
451	448, 450	bitri 263	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑛 ∈ (1...𝑁))))
452	451, 391	sylbir 224	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑛 ∈ (1...𝑁))) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
453	447, 28, 452, 444	itgfsum 23399	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) ∈ 𝐿¹ ∧ ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥))
454	453	simprd 478	. . . . . 6 ⊢ (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥)
455	454	eqcomd 2616	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥)
456	455	oveq1d 6564	. . . 4 ⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
457	384, 446, 456	3eqtr2d 2650	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
458	153, 457	oveq12d 6567	. 2 ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π)))
459		fourierdlem83.d	. . . . . . . . . . 11 ⊢ 𝐷 = (𝑛 ∈ ℕ ↦ (𝑠 ∈ ℝ ↦ if((𝑠 mod (2 · π)) = 0, (((2 · 𝑛) + 1) / (2 · π)), ((sin‘((𝑛 + (1 / 2)) · 𝑠)) / ((2 · π) · (sin‘(𝑠 / 2)))))))
460	7	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑁 ∈ ℕ)
461		eqid 2610	. . . . . . . . . . 11 ⊢ (𝐷‘𝑁) = (𝐷‘𝑁)
462		eqid 2610	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π))
463	459, 460, 461, 462	dirkertrigeq 38994	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐷‘𝑁) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)))
464		oveq2 6557	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (𝑥 − 𝑋) → (𝑛 · 𝑠) = (𝑛 · (𝑥 − 𝑋)))
465	464	fveq2d 6107	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑥 − 𝑋) → (cos‘(𝑛 · 𝑠)) = (cos‘(𝑛 · (𝑥 − 𝑋))))
466	465	sumeq2sdv 14282	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑥 − 𝑋) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠)) = Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))
467	466	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑥 − 𝑋) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))))
468	467	oveq1d 6564	. . . . . . . . . . 11 ⊢ (𝑠 = (𝑥 − 𝑋) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π))
469	468	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑠 = (𝑥 − 𝑋)) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π))
470	58	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑋 ∈ ℝ)
471	118, 470	resubcld 10337	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥 − 𝑋) ∈ ℝ)
472		halfre 11123	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ ℝ
473	472	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (1 / 2) ∈ ℝ)
474		fzfid 12634	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (1...𝑁) ∈ Fin)
475	390	an32s 842	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
476	474, 475	fsumrecl 14312	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
477	473, 476	readdcld 9948	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
478	44	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → π ∈ ℝ)
479	48	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → π ≠ 0)
480	477, 478, 479	redivcld 10732	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π) ∈ ℝ)
481	463, 469, 471, 480	fvmptd 6197	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π))
482	481, 480	eqeltrd 2688	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ)
483	119, 482	remulcld 9949	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ ℝ)
484	177	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ V)
485		eqidd 2611	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
486		eqidd 2611	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
487	484, 482, 119, 485, 486	offval2 6812	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_𝑓 · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))))
488	482	recnd 9947	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℂ)
489	488, 120	mulcomd 9940	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
490	489	mpteq2dva 4672	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))))
491	487, 490	eqtr2d 2645	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) = ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_𝑓 · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
492		eqid 2610	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))
493		eqid 2610	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))
494	194	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ℂ ⊆ ℂ)
495		cncfss 22510	. . . . . . . . . . . . . 14 ⊢ ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ))
496	189, 494, 495	sylancr 694	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ))
497		simpr 476	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
498	58	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑋 ∈ ℝ)
499	497, 498	resubcld 10337	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 − 𝑋) ∈ ℝ)
500		eqid 2610	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) = (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋))
501	499, 500	fmptd 6292	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)):ℝ⟶ℝ)
502	189	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ℝ ⊆ ℂ)
503	502, 494	idcncfg 38757	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝑥) ∈ (ℝ–cn→ℂ))
504	502, 365, 494	constcncfg 38756	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝑋) ∈ (ℝ–cn→ℂ))
505	503, 504	subcncf 38754	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℂ))
506		cncffvrn 22509	. . . . . . . . . . . . . . . 16 ⊢ ((ℝ ⊆ ℂ ∧ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℂ)) → ((𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)):ℝ⟶ℝ))
507	189, 505, 506	sylancr 694	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)):ℝ⟶ℝ))
508	501, 507	mpbird 246	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℝ))
509	459	dirkercncf 39000	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁) ∈ (ℝ–cn→ℝ))
510	7, 509	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷‘𝑁) ∈ (ℝ–cn→ℝ))
511	508, 510	cncfcompt 38768	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (ℝ–cn→ℝ))
512	496, 511	sseldd 3569	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (ℝ–cn→ℂ))
513	44	renegcli 10221	. . . . . . . . . . . . . 14 ⊢ -π ∈ ℝ
514		iccssre 12126	. . . . . . . . . . . . . 14 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
515	513, 44, 514	mp2an 704	. . . . . . . . . . . . 13 ⊢ (-π[,]π) ⊆ ℝ
516	515	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (-π[,]π) ⊆ ℝ)
517	459	dirkerf 38990	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁):ℝ⟶ℝ)
518	7, 517	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷‘𝑁):ℝ⟶ℝ)
519	518	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → (𝐷‘𝑁):ℝ⟶ℝ)
520	516	sselda 3568	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
521	58	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
522	520, 521	resubcld 10337	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → (𝑥 − 𝑋) ∈ ℝ)
523	519, 522	ffvelrnd 6268	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ)
524	523	recnd 9947	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℂ)
525	493, 512, 516, 494, 524	cncfmptssg 38755	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ ((-π[,]π)–cn→ℂ))
526	132	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ⊆ (-π[,]π))
527	492, 525, 526, 494, 488	cncfmptssg 38755	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (𝐶–cn→ℂ))
528		cnmbf 23232	. . . . . . . . . 10 ⊢ ((𝐶 ∈ dom vol ∧ (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (𝐶–cn→ℂ)) → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ MblFn)
529	176, 527, 528	sylancr 694	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ MblFn)
530	513	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → -π ∈ ℝ)
531		0red 9920	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ℝ)
532		negpilt0 38433	. . . . . . . . . . . . . . . 16 ⊢ -π < 0
533	532	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -π < 0)
534	47	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 < π)
535	530, 531, 101, 533, 534	lttrd 10077	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -π < π)
536	530, 101, 535	ltled 10064	. . . . . . . . . . . . 13 ⊢ (𝜑 → -π ≤ π)
537	493, 512, 516, 502, 523	cncfmptssg 38755	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ ((-π[,]π)–cn→ℝ))
538	530, 101, 536, 537	evthiccabs 38565	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ∧ ∃𝑧 ∈ (-π[,]π)∀𝑤 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑧)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑤))))
539	538	simpld 474	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)))
540		eqidd 2611	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
541	420	fveq2d 6107	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
542	541	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (-π[,]π)) ∧ 𝑥 = 𝑦) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
543		simpr 476	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → 𝑦 ∈ (-π[,]π))
544	518	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (𝐷‘𝑁):ℝ⟶ℝ)
545	515, 543	sseldi 3566	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → 𝑦 ∈ ℝ)
546	58	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
547	545, 546	resubcld 10337	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (𝑦 − 𝑋) ∈ ℝ)
548	544, 547	ffvelrnd 6268	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑦 − 𝑋)) ∈ ℝ)
549	540, 542, 543, 548	fvmptd 6197	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
550	549	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
551	550	adantlr 747	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
552		eqidd 2611	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
553		oveq1 6556	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑐 → (𝑥 − 𝑋) = (𝑐 − 𝑋))
554	553	fveq2d 6107	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑐 → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑐 − 𝑋)))
555	554	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑥 = 𝑐) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑐 − 𝑋)))
556		simpr 476	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → 𝑐 ∈ (-π[,]π))
557	518	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (𝐷‘𝑁):ℝ⟶ℝ)
558	515, 556	sseldi 3566	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → 𝑐 ∈ ℝ)
559	58	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
560	558, 559	resubcld 10337	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (𝑐 − 𝑋) ∈ ℝ)
561	557, 560	ffvelrnd 6268	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑐 − 𝑋)) ∈ ℝ)
562	552, 555, 556, 561	fvmptd 6197	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐) = ((𝐷‘𝑁)‘(𝑐 − 𝑋)))
563	562	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
564	563	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
565	551, 564	breq12d 4596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → ((abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ↔ (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
566	565	ralbidva 2968	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ↔ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
567	566	rexbidva 3031	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ↔ ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
568	539, 567	mpbid 221	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
569	561	recnd 9947	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑐 − 𝑋)) ∈ ℂ)
570	569	abscld 14023	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∈ ℝ)
571	570	3adant3 1074	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∈ ℝ)
572		nfv 1830	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝜑
573		nfv 1830	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 𝑐 ∈ (-π[,]π)
574		nfra1 2925	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))
575	572, 573, 574	nf3an 1819	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
576		simpr 476	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
577	482	ralrimiva 2949	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ)
578		dmmptg 5549	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ 𝐶 ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ → dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = 𝐶)
579	577, 578	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = 𝐶)
580	579	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = 𝐶)
581	576, 580	eleqtrd 2690	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → 𝑦 ∈ 𝐶)
582	581	3ad2antl1 1216	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → 𝑦 ∈ 𝐶)
583		eqidd 2611	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
584	541	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
585		simpr 476	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
586	518	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝐷‘𝑁):ℝ⟶ℝ)
587	136, 585	sseldi 3566	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
588	58	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑋 ∈ ℝ)
589	587, 588	resubcld 10337	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝑦 − 𝑋) ∈ ℝ)
590	586, 589	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑦 − 𝑋)) ∈ ℝ)
591	583, 584, 585, 590	fvmptd 6197	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
592	591	fveq2d 6107	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
593	592	adantlr 747	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
594		simplr 788	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
595	132	sseli 3564	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝐶 → 𝑦 ∈ (-π[,]π))
596	595	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ (-π[,]π))
597		rspa 2914	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
598	594, 596, 597	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
599	593, 598	eqbrtrd 4605	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
600	599	3adantl2 1211	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
601	582, 600	syldan 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
602	601	ex 449	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → (𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
603	575, 602	ralrimi 2940	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
604		breq2 4587	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) → ((abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
605	604	ralbidv 2969	. . . . . . . . . . . . 13 ⊢ (𝑏 = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
606	605	rspcev 3282	. . . . . . . . . . . 12 ⊢ (((abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏)
607	571, 603, 606	syl2anc 691	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏)
608	607	rexlimdv3a 3015	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏))
609	568, 608	mpd 15	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏)
610		bddmulibl 23411	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_𝑓 · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
611	529, 140, 609, 610	syl3anc 1318	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_𝑓 · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
612	491, 611	eqeltrd 2688	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) ∈ 𝐿¹)
613	142, 483, 612	itgmulc2 23406	. . . . . 6 ⊢ (𝜑 → (π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) = ∫𝐶(π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) d𝑥)
614	142	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → π ∈ ℂ)
615	120, 488, 614	mul13d 38432	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) = (π · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))))
616	489	oveq2d 6565	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (π · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))) = (π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))))
617	615, 616	eqtrd 2644	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) = (π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))))
618	617	itgeq2dv 23354	. . . . . 6 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) d𝑥 = ∫𝐶(π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) d𝑥)
619	613, 618	eqtr4d 2647	. . . . 5 ⊢ (𝜑 → (π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) = ∫𝐶((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) d𝑥)
620	148	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (1 / 2) ∈ ℂ)
621	620, 120	mulcomd 9940	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (1 / 2)))
622	396	an32s 842	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℂ)
623	474, 120, 622	fsummulc2 14358	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) = Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))))
624	623	eqcomd 2616	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) = ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))))
625	621, 624	oveq12d 6567	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) = (((𝐹‘𝑥) · (1 / 2)) + ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))))
626	474, 622	fsumcl 14311	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℂ)
627	120, 620, 626	adddid 9943	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))) = (((𝐹‘𝑥) · (1 / 2)) + ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))))
628	481	oveq1d 6564	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π) = ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π) · π))
629	620, 626	addcld 9938	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℂ)
630	629, 614, 479	divcan1d 10681	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π) · π) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))))
631	628, 630	eqtr2d 2645	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) = (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π))
632	631	oveq2d 6565	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))) = ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)))
633	625, 627, 632	3eqtr2rd 2651	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) = (((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))))
634	633	itgeq2dv 23354	. . . . 5 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) d𝑥 = ∫𝐶(((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) d𝑥)
635		remulcl 9900	. . . . . . 7 ⊢ (((1 / 2) ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ) → ((1 / 2) · (𝐹‘𝑥)) ∈ ℝ)
636	472, 119, 635	sylancr 694	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) · (𝐹‘𝑥)) ∈ ℝ)
637	148, 119, 140	iblmulc2 23403	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((1 / 2) · (𝐹‘𝑥))) ∈ 𝐿¹)
638	391	an32s 842	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
639	474, 638	fsumrecl 14312	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
640	453	simpld 474	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) ∈ 𝐿¹)
641	636, 637, 639, 640	itgadd 23397	. . . . 5 ⊢ (𝜑 → ∫𝐶(((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) d𝑥 = (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥))
642	619, 634, 641	3eqtrrd 2649	. . . 4 ⊢ (𝜑 → (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥) = (π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥))
643	642	oveq1d 6564	. . 3 ⊢ (𝜑 → ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥) / π) = ((π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) / π))
644	636, 637	itgcl 23356	. . . 4 ⊢ (𝜑 → ∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 ∈ ℂ)
645	639, 640	itgcl 23356	. . . 4 ⊢ (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 ∈ ℂ)
646	644, 645, 142, 102	divdird 10718	. . 3 ⊢ (𝜑 → ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥) / π) = ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π)))
647	483, 612	itgcl 23356	. . . 4 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥 ∈ ℂ)
648	647, 142, 102	divcan3d 10685	. . 3 ⊢ (𝜑 → ((π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) / π) = ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥)
649	643, 646, 648	3eqtr3d 2652	. 2 ⊢ (𝜑 → ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π)) = ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥)
650	90, 458, 649	3eqtrd 2648	1 ⊢ (𝜑 → (𝑆‘𝑁) = ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 Vcvv 3173 ⊆ wss 3540 ifcif 4036 class class class wbr 4583 ↦ cmpt 4643 dom cdm 5038 ↾ cres 5040 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ∘_𝑓 cof 6793 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 < clt 9953 ≤ cle 9954 − cmin 10145 -cneg 10146 / cdiv 10563 ℕcn 10897 2c2 10947 ℕ₀cn0 11169 (,)cioo 12046 [,]cicc 12049 ...cfz 12197 mod cmo 12530 abscabs 13822 Σcsu 14264 sincsin 14633 cosccos 14634 πcpi 14636 –cn→ccncf 22487 volcvol 23039 MblFncmbf 23189 𝐿¹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-t1 20928 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: fourierdlem111 39110

W3C validator