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 46166

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 7411	. . . . . 6 ⊢ (𝑚 = 𝑁 → (1...𝑚) = (1...𝑁))
4	3	sumeq1d 15714	. . . . 5 ⊢ (𝑚 = 𝑁 → Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
5	4	oveq2d 7419	. . . 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 12514	. . . . . . 7 ⊢ 0 ∈ ℕ₀
10	9	a1i 11	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℕ₀)
11	9	elexi 3482	. . . . . . 7 ⊢ 0 ∈ V
12		eleq1 2822	. . . . . . . . 9 ⊢ (𝑛 = 0 → (𝑛 ∈ ℕ₀ ↔ 0 ∈ ℕ₀))
13	12	anbi2d 630	. . . . . . . 8 ⊢ (𝑛 = 0 → ((𝜑 ∧ 𝑛 ∈ ℕ₀) ↔ (𝜑 ∧ 0 ∈ ℕ₀)))
14		fveq2 6875	. . . . . . . . 9 ⊢ (𝑛 = 0 → (𝐴‘𝑛) = (𝐴‘0))
15	14	eleq1d 2819	. . . . . . . 8 ⊢ (𝑛 = 0 → ((𝐴‘𝑛) ∈ ℝ ↔ (𝐴‘0) ∈ ℝ))
16	13, 15	imbi12d 344	. . . . . . 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 46106	. . . . . . . . 9 ⊢ (𝜑 → ((𝑛 ∈ ℕ₀ → (𝐴‘𝑛) ∈ ℝ) ∧ (𝑛 ∈ ℕ → (𝐵‘𝑛) ∈ ℝ)))
23	22	simpld 494	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ ℕ₀ → (𝐴‘𝑛) ∈ ℝ))
24	23	imp 406	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝐴‘𝑛) ∈ ℝ)
25	11, 16, 24	vtocl 3537	. . . . . 6 ⊢ ((𝜑 ∧ 0 ∈ ℕ₀) → (𝐴‘0) ∈ ℝ)
26	8, 10, 25	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝐴‘0) ∈ ℝ)
27	26	rehalfcld 12486	. . . 4 ⊢ (𝜑 → ((𝐴‘0) / 2) ∈ ℝ)
28		fzfid 13989	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
29		eleq1 2822	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ ℕ₀ ↔ 𝑛 ∈ ℕ₀))
30	29	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → ((𝜑 ∧ 𝑘 ∈ ℕ₀) ↔ (𝜑 ∧ 𝑛 ∈ ℕ₀)))
31		simpl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → 𝑘 = 𝑛)
32	31	oveq1d 7418	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → (𝑘 · 𝑥) = (𝑛 · 𝑥))
33	32	fveq2d 6879	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑘 · 𝑥)) = (cos‘(𝑛 · 𝑥)))
34	33	oveq2d 7419	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))
35	34	itgeq2dv 25733	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥)
36	35	eleq1d 2819	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ ↔ ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ))
37	30, 36	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → (((𝜑 ∧ 𝑘 ∈ ℕ₀) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ) ↔ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)))
38	17	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝐹:ℝ⟶ℝ)
39	19	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐹 ↾ 𝐶) ∈ 𝐿¹)
40		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
41	38, 18, 39, 20, 40	fourierdlem16 46100	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝐴‘𝑘) ∈ ℝ ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹) ∧ ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ))
42	41	simprd 495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ)
43	37, 42	chvarvv 1998	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
44		pire 26416	. . . . . . . . . . . 12 ⊢ π ∈ ℝ
45	44	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → π ∈ ℝ)
46		0re 11235	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
47		pipos 26418	. . . . . . . . . . . . 13 ⊢ 0 < π
48	46, 47	gtneii 11345	. . . . . . . . . . . 12 ⊢ π ≠ 0
49	48	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → π ≠ 0)
50	43, 45, 49	redivcld 12067	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
51	50, 20	fmptd 7103	. . . . . . . . 9 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℝ)
52	51	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐴:ℕ₀⟶ℝ)
53		elfznn 13568	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
54	53	nnnn0d 12560	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ₀)
55	54	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ₀)
56	52, 55	ffvelcdmd 7074	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐴‘𝑛) ∈ ℝ)
57	55	nn0red 12561	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℝ)
58		fourierdlem83.x	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℝ)
59	58	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℝ)
60	57, 59	remulcld 11263	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 · 𝑋) ∈ ℝ)
61	60	recoscld 16160	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℝ)
62	56, 61	remulcld 11263	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
63		eleq1 2822	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ ℕ ↔ 𝑛 ∈ ℕ))
64	63	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → ((𝜑 ∧ 𝑘 ∈ ℕ) ↔ (𝜑 ∧ 𝑛 ∈ ℕ)))
65		oveq1 7410	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → (𝑘 · 𝑥) = (𝑛 · 𝑥))
66	65	fveq2d 6879	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → (sin‘(𝑘 · 𝑥)) = (sin‘(𝑛 · 𝑥)))
67	66	oveq2d 7419	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑛 → ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
68	67	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
69	68	itgeq2dv 25733	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥)
70	69	eleq1d 2819	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ ↔ ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ))
71	64, 70	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → (((𝜑 ∧ 𝑘 ∈ ℕ) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ) ↔ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)))
72	17	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:ℝ⟶ℝ)
73	19	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹 ↾ 𝐶) ∈ 𝐿¹)
74		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
75	72, 18, 73, 21, 74	fourierdlem21 46105	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐵‘𝑘) ∈ ℝ ∧ (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥)))) ∈ 𝐿¹) ∧ ∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ))
76	75	simprd 495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ)
77	71, 76	chvarvv 1998	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
78	44	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → π ∈ ℝ)
79	48	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → π ≠ 0)
80	77, 78, 79	redivcld 12067	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
81	80, 21	fmptd 7103	. . . . . . . . 9 ⊢ (𝜑 → 𝐵:ℕ⟶ℝ)
82	81	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐵:ℕ⟶ℝ)
83	53	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ)
84	82, 83	ffvelcdmd 7074	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐵‘𝑛) ∈ ℝ)
85	60	resincld 16159	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
86	84, 85	remulcld 11263	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
87	62, 86	readdcld 11262	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
88	28, 87	fsumrecl 15748	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
89	27, 88	readdcld 11262	. . 3 ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) ∈ ℝ)
90	2, 6, 7, 89	fvmptd 6992	. 2 ⊢ (𝜑 → (𝑆‘𝑁) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
91	20	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐴 = (𝑛 ∈ ℕ₀ ↦ (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
92		oveq1 7410	. . . . . . . . . . . . 13 ⊢ (𝑛 = 0 → (𝑛 · 𝑥) = (0 · 𝑥))
93	92	fveq2d 6879	. . . . . . . . . . . 12 ⊢ (𝑛 = 0 → (cos‘(𝑛 · 𝑥)) = (cos‘(0 · 𝑥)))
94	93	oveq2d 7419	. . . . . . . . . . 11 ⊢ (𝑛 = 0 → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(0 · 𝑥))))
95	94	adantr 480	. . . . . . . . . 10 ⊢ ((𝑛 = 0 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(0 · 𝑥))))
96	95	itgeq2dv 25733	. . . . . . . . 9 ⊢ (𝑛 = 0 → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥)
97	96	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 0) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥)
98	97	oveq1d 7418	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 = 0) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) = (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
99	17, 18, 19, 20, 10	fourierdlem16 46100	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴‘0) ∈ ℝ ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹) ∧ ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 ∈ ℝ))
100	99	simprd 495	. . . . . . . 8 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 ∈ ℝ)
101	44	a1i 11	. . . . . . . 8 ⊢ (𝜑 → π ∈ ℝ)
102	48	a1i 11	. . . . . . . 8 ⊢ (𝜑 → π ≠ 0)
103	100, 101, 102	redivcld 12067	. . . . . . 7 ⊢ (𝜑 → (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) ∈ ℝ)
104	91, 98, 10, 103	fvmptd 6992	. . . . . 6 ⊢ (𝜑 → (𝐴‘0) = (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
105		ioosscn 13423	. . . . . . . . . . . . . . 15 ⊢ (-π(,)π) ⊆ ℂ
106		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐶)
107	106, 18	eleqtrdi 2844	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ (-π(,)π))
108	105, 107	sselid 3956	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ℂ)
109	108	mul02d 11431	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐶 → (0 · 𝑥) = 0)
110	109	fveq2d 6879	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐶 → (cos‘(0 · 𝑥)) = (cos‘0))
111		cos0 16166	. . . . . . . . . . . 12 ⊢ (cos‘0) = 1
112	110, 111	eqtrdi 2786	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐶 → (cos‘(0 · 𝑥)) = 1)
113	112	oveq2d 7419	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐶 → ((𝐹‘𝑥) · (cos‘(0 · 𝑥))) = ((𝐹‘𝑥) · 1))
114	113	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(0 · 𝑥))) = ((𝐹‘𝑥) · 1))
115	17	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐹:ℝ⟶ℝ)
116		ioossre 13422	. . . . . . . . . . . . . 14 ⊢ (-π(,)π) ⊆ ℝ
117	116, 107	sselid 3956	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ℝ)
118	117	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
119	115, 118	ffvelcdmd 7074	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
120	119	recnd 11261	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
121	120	mulridd 11250	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · 1) = (𝐹‘𝑥))
122	114, 121	eqtrd 2770	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(0 · 𝑥))) = (𝐹‘𝑥))
123	122	itgeq2dv 25733	. . . . . . 7 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 = ∫𝐶(𝐹‘𝑥) d𝑥)
124	123	oveq1d 7418	. . . . . 6 ⊢ (𝜑 → (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) = (∫𝐶(𝐹‘𝑥) d𝑥 / π))
125	104, 124	eqtrd 2770	. . . . 5 ⊢ (𝜑 → (𝐴‘0) = (∫𝐶(𝐹‘𝑥) d𝑥 / π))
126	125	oveq1d 7418	. . . 4 ⊢ (𝜑 → ((𝐴‘0) / 2) = ((∫𝐶(𝐹‘𝑥) d𝑥 / π) / 2))
127	17	feqmptd 6946	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)))
128	127	reseq1d 5965	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ 𝐶))
129	44	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐶 → π ∈ ℝ)
130	129	renegcld 11662	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐶 → -π ∈ ℝ)
131		ioossicc 13448	. . . . . . . . . . . . 13 ⊢ (-π(,)π) ⊆ (-π[,]π)
132	18, 131	eqsstri 4005	. . . . . . . . . . . 12 ⊢ 𝐶 ⊆ (-π[,]π)
133	132	sseli 3954	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ (-π[,]π))
134		eliccre 45482	. . . . . . . . . . 11 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ ∧ 𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
135	130, 129, 133, 134	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ℝ)
136	135	ssriv 3962	. . . . . . . . 9 ⊢ 𝐶 ⊆ ℝ
137		resmpt 6024	. . . . . . . . 9 ⊢ (𝐶 ⊆ ℝ → ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
138	136, 137	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
139	128, 138	eqtr2d 2771	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝐹 ↾ 𝐶))
140	139, 19	eqeltrd 2834	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
141	119, 140	itgcl 25735	. . . . 5 ⊢ (𝜑 → ∫𝐶(𝐹‘𝑥) d𝑥 ∈ ℂ)
142	101	recnd 11261	. . . . 5 ⊢ (𝜑 → π ∈ ℂ)
143		2cnd 12316	. . . . 5 ⊢ (𝜑 → 2 ∈ ℂ)
144		2ne0 12342	. . . . . 6 ⊢ 2 ≠ 0
145	144	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ≠ 0)
146	141, 142, 143, 102, 145	divdiv32d 12040	. . . 4 ⊢ (𝜑 → ((∫𝐶(𝐹‘𝑥) d𝑥 / π) / 2) = ((∫𝐶(𝐹‘𝑥) d𝑥 / 2) / π))
147	141, 143, 145	divrecd 12018	. . . . . 6 ⊢ (𝜑 → (∫𝐶(𝐹‘𝑥) d𝑥 / 2) = (∫𝐶(𝐹‘𝑥) d𝑥 · (1 / 2)))
148	143, 145	reccld 12008	. . . . . . 7 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
149	141, 148	mulcomd 11254	. . . . . 6 ⊢ (𝜑 → (∫𝐶(𝐹‘𝑥) d𝑥 · (1 / 2)) = ((1 / 2) · ∫𝐶(𝐹‘𝑥) d𝑥))
150	148, 119, 140	itgmulc2 25785	. . . . . 6 ⊢ (𝜑 → ((1 / 2) · ∫𝐶(𝐹‘𝑥) d𝑥) = ∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥)
151	147, 149, 150	3eqtrd 2774	. . . . 5 ⊢ (𝜑 → (∫𝐶(𝐹‘𝑥) d𝑥 / 2) = ∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥)
152	151	oveq1d 7418	. . . 4 ⊢ (𝜑 → ((∫𝐶(𝐹‘𝑥) d𝑥 / 2) / π) = (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π))
153	126, 146, 152	3eqtrd 2774	. . 3 ⊢ (𝜑 → ((𝐴‘0) / 2) = (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π))
154	55, 50	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
155	20	fvmpt2 6996	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ₀ ∧ (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐴‘𝑛) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
156	55, 154, 155	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐴‘𝑛) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
157	156	oveq1d 7418	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))))
158	154	recnd 11261	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
159	61	recnd 11261	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℂ)
160	158, 159	mulcomd 11254	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
161	55, 43	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
162	161	recnd 11261	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
163	142	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → π ∈ ℂ)
164	48	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → π ≠ 0)
165	159, 162, 163, 164	divassd 12050	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
166	17	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → 𝐹:ℝ⟶ℝ)
167	117	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
168	166, 167	ffvelcdmd 7074	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
169		nn0re 12508	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℝ)
170	169	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
171	170, 167	remulcld 11263	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℝ)
172	171	recoscld 16160	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
173	168, 172	remulcld 11263	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
174	54, 173	sylanl2 681	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
175		ioombl 25516	. . . . . . . . . . . . . . . . . . 19 ⊢ (-π(,)π) ∈ dom vol
176	18, 175	eqeltri 2830	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐶 ∈ dom vol
177	176	elexi 3482	. . . . . . . . . . . . . . . . 17 ⊢ 𝐶 ∈ V
178	177	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝐶 ∈ V)
179		eqidd 2736	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))))
180		eqidd 2736	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
181	178, 172, 168, 179, 180	offval2 7689	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
182	172	recnd 11261	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℂ)
183	120	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
184	182, 183	mulcomd 11254	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))
185	184	mpteq2dva 5214	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))))
186	181, 185	eqtr2d 2771	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
187		coscn 26405	. . . . . . . . . . . . . . . . . 18 ⊢ cos ∈ (ℂ–cn→ℂ)
188	187	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → cos ∈ (ℂ–cn→ℂ))
189		ax-resscn 11184	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℝ ⊆ ℂ
190	136, 189	sstri 3968	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐶 ⊆ ℂ
191	190	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝐶 ⊆ ℂ)
192	169	recnd 11261	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℂ)
193	192	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝑛 ∈ ℂ)
194		ssid 3981	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℂ ⊆ ℂ
195	194	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ℂ ⊆ ℂ)
196	191, 193, 195	constcncfg 45849	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ 𝑛) ∈ (𝐶–cn→ℂ))
197	191, 195	idcncfg 45850	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ 𝑥) ∈ (𝐶–cn→ℂ))
198	196, 197	mulcncf 25396	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶–cn→ℂ))
199	188, 198	cncfmpt1f 24856	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ))
200		cnmbf 25610	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ dom vol ∧ (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
201	176, 199, 200	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
202	140	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
203		1re 11233	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
204		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))))
205	169	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
206	117	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
207	205, 206	remulcld 11263	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℝ)
208	207	recoscld 16160	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
209	208	ralrimiva 3132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ₀ → ∀𝑥 ∈ 𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
210	209	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → ∀𝑥 ∈ 𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
211		dmmptg 6231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 ∈ 𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ → dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
212	210, 211	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
213	204, 212	eleqtrd 2836	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦 ∈ 𝐶)
214		eqidd 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))))
215		oveq2 7411	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑛 · 𝑥) = (𝑛 · 𝑦))
216	215	fveq2d 6879	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
217	216	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
218		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
219	169	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → 𝑛 ∈ ℝ)
220	136, 218	sselid 3956	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
221	219, 220	remulcld 11263	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (𝑛 · 𝑦) ∈ ℝ)
222	221	recoscld 16160	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (cos‘(𝑛 · 𝑦)) ∈ ℝ)
223	214, 217, 218, 222	fvmptd 6992	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦) = (cos‘(𝑛 · 𝑦)))
224	223	fveq2d 6879	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(cos‘(𝑛 · 𝑦))))
225		abscosbd 45255	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 · 𝑦) ∈ ℝ → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
226	221, 225	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
227	224, 226	eqbrtrd 5141	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
228	213, 227	syldan 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
229	228	ralrimiva 3132	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
230		breq2 5123	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 1 → ((abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
231	230	ralbidv 3163	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
232	231	rspcev 3601	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
233	203, 229, 232	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ₀ → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
234	233	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
235		bddmulibl 25790	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
236	201, 202, 234, 235	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
237	186, 236	eqeltrd 2834	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
238	55, 237	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
239	159, 174, 238	itgmulc2 25785	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) d𝑥)
240	159	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑋)) ∈ ℂ)
241	120	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
242	54, 182	sylanl2 681	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℂ)
243	240, 241, 242	mul12d 11442	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))))
244	240, 242	mulcomd 11254	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥))) = ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))
245	244	oveq2d 7419	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
246	243, 245	eqtrd 2770	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
247	246	itgeq2dv 25733	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
248	239, 247	eqtrd 2770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
249	248	oveq1d 7418	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
250	165, 249	eqtr3d 2772	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
251	157, 160, 250	3eqtrd 2774	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
252	83, 80	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
253	21	fvmpt2 6996	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐵‘𝑛) = (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
254	83, 252, 253	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐵‘𝑛) = (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
255	254	oveq1d 7418	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))))
256	252	recnd 11261	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
257	85	recnd 11261	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℂ)
258	256, 257	mulcomd 11254	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
259	83, 77	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
260	259	recnd 11261	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
261	257, 260, 163, 164	divassd 12050	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
262	119	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
263		nnre 12245	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
264	263	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
265	117	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
266	264, 265	remulcld 11263	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℝ)
267	266	resincld 16159	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
268	267	adantll 714	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
269	262, 268	remulcld 11263	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
270	53, 269	sylanl2 681	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
271	177	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 ∈ V)
272		eqidd 2736	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))))
273		eqidd 2736	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
274	271, 268, 262, 272, 273	offval2 7689	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
275	268	recnd 11261	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℂ)
276	120	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
277	275, 276	mulcomd 11254	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
278	277	mpteq2dva 5214	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))))
279	274, 278	eqtr2d 2771	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
280		sincn 26404	. . . . . . . . . . . . . . . . . 18 ⊢ sin ∈ (ℂ–cn→ℂ)
281	280	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sin ∈ (ℂ–cn→ℂ))
282	190	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → 𝐶 ⊆ ℂ)
283	263	recnd 11261	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
284	194	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → ℂ ⊆ ℂ)
285	282, 283, 284	constcncfg 45849	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (𝑥 ∈ 𝐶 ↦ 𝑛) ∈ (𝐶–cn→ℂ))
286	282, 284	idcncfg 45850	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (𝑥 ∈ 𝐶 ↦ 𝑥) ∈ (𝐶–cn→ℂ))
287	285, 286	mulcncf 25396	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → (𝑥 ∈ 𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶–cn→ℂ))
288	287	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶–cn→ℂ))
289	281, 288	cncfmpt1f 24856	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ))
290		cnmbf 25610	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ dom vol ∧ (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ)) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn)
291	176, 289, 290	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn)
292	140	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
293		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))))
294	267	ralrimiva 3132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → ∀𝑥 ∈ 𝐶 (sin‘(𝑛 · 𝑥)) ∈ ℝ)
295		dmmptg 6231	. . . . . . . . . . . . . . . . . . . . . 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 2836	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦 ∈ 𝐶)
299		eqidd 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))))
300	215	fveq2d 6879	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
301	300	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
302		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
303	263	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → 𝑛 ∈ ℝ)
304	136, 302	sselid 3956	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
305	303, 304	remulcld 11263	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (𝑛 · 𝑦) ∈ ℝ)
306	305	resincld 16159	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (sin‘(𝑛 · 𝑦)) ∈ ℝ)
307	299, 301, 302, 306	fvmptd 6992	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦) = (sin‘(𝑛 · 𝑦)))
308	307	fveq2d 6879	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(sin‘(𝑛 · 𝑦))))
309		abssinbd 45272	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 · 𝑦) ∈ ℝ → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
310	305, 309	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
311	308, 310	eqbrtrd 5141	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
312	298, 311	syldan 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
313	312	ralrimiva 3132	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
314		breq2 5123	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 1 → ((abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
315	314	ralbidv 3163	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
316	315	rspcev 3601	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
317	203, 313, 316	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
318	317	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
319		bddmulibl 25790	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
320	291, 292, 318, 319	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
321	279, 320	eqeltrd 2834	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
322	83, 321	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
323	257, 270, 322	itgmulc2 25785	. . . . . . . . . . 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 11442	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))))
327	324, 325	mulcomd 11254	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥))) = ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))
328	327	oveq2d 7419	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
329	326, 328	eqtrd 2770	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
330	329	itgeq2dv 25733	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
331	323, 330	eqtrd 2770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
332	331	oveq1d 7418	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
333	261, 332	eqtr3d 2772	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
334	255, 258, 333	3eqtrd 2774	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
335	251, 334	oveq12d 7421	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π) + (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π)))
336	54, 168	sylanl2 681	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
337	55, 208	sylan 580	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
338	61	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑋)) ∈ ℝ)
339	337, 338	remulcld 11263	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
340	336, 339	remulcld 11263	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) ∈ ℝ)
341	241, 242, 240	mul13d 45256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
342	242, 241	mulcomd 11254	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))
343	342	oveq2d 7419	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))))
344	341, 343	eqtrd 2770	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))))
345	344	mpteq2dva 5214	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) = (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))))
346	159, 174, 238	iblmulc2 25782	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))) ∈ 𝐿¹)
347	345, 346	eqeltrd 2834	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) ∈ 𝐿¹)
348	340, 347	itgcl 25735	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
349	83, 267	sylan 580	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
350	85	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
351	349, 350	remulcld 11263	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
352	336, 351	remulcld 11263	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
353	241, 325, 324	mul13d 45256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
354	325, 241	mulcomd 11254	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
355	354	oveq2d 7419	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))))
356	353, 355	eqtrd 2770	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))))
357	356	mpteq2dva 5214	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))))
358	257, 270, 322	iblmulc2 25782	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))) ∈ 𝐿¹)
359	357, 358	eqeltrd 2834	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) ∈ 𝐿¹)
360	352, 359	itgcl 25735	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
361	348, 360, 163, 164	divdird 12053	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π) + (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π)))
362	53	nncnd 12254	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
363	362	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℂ)
364	108	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℂ)
365	58	recnd 11261	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ ℂ)
366	365	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑋 ∈ ℂ)
367	363, 364, 366	subdid 11691	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · (𝑥 − 𝑋)) = ((𝑛 · 𝑥) − (𝑛 · 𝑋)))
368	367	fveq2d 6879	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) = (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))))
369	363, 364	mulcld 11253	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℂ)
370	363, 366	mulcld 11253	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑋) ∈ ℂ)
371		cossub 16185	. . . . . . . . . . . . 13 ⊢ (((𝑛 · 𝑥) ∈ ℂ ∧ (𝑛 · 𝑋) ∈ ℂ) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
372	369, 370, 371	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
373	368, 372	eqtrd 2770	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
374	373	oveq2d 7419	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) = ((𝐹‘𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
375	339	recnd 11261	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℂ)
376	351	recnd 11261	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℂ)
377	241, 375, 376	adddid 11257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
378	374, 377	eqtrd 2770	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) = (((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
379	378	itgeq2dv 25733	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = ∫𝐶(((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥)
380	340, 347, 352, 359	itgadd 25776	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶(((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥 = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥))
381	379, 380	eqtr2d 2771	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) = ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥)
382	381	oveq1d 7418	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
383	335, 361, 382	3eqtr2d 2776	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
384	383	sumeq2dv 15716	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
385	57	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
386	117	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
387	58	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑋 ∈ ℝ)
388	386, 387	resubcld 11663	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑥 − 𝑋) ∈ ℝ)
389	385, 388	remulcld 11263	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · (𝑥 − 𝑋)) ∈ ℝ)
390	389	recoscld 16160	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
391	336, 390	remulcld 11263	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
392	177	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ V)
393		eqidd 2736	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))))
394		eqidd 2736	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
395	392, 390, 336, 393, 394	offval2 7689	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · (𝑥 − 𝑋))) · (𝐹‘𝑥))))
396	390	recnd 11261	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℂ)
397	396, 241	mulcomd 11254	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · (𝑥 − 𝑋))) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))))
398	397	mpteq2dva 5214	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · (𝑥 − 𝑋))) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))))
399	395, 398	eqtr2d 2771	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) = ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
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 45849	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ 𝑋) ∈ (𝐶–cn→ℂ))
407	402, 406	subcncf 25395	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝑥 − 𝑋)) ∈ (𝐶–cn→ℂ))
408	401, 407	mulcncf 25396	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝑛 · (𝑥 − 𝑋))) ∈ (𝐶–cn→ℂ))
409	400, 408	cncfmpt1f 24856	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ (𝐶–cn→ℂ))
410		cnmbf 25610	. . . . . . . . 9 ⊢ ((𝐶 ∈ dom vol ∧ (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ (𝐶–cn→ℂ)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ MblFn)
411	176, 409, 410	sylancr 587	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ MblFn)
412	140	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
413		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))) → 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))))
414	390	ralrimiva 3132	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∀𝑥 ∈ 𝐶 (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
415		dmmptg 6231	. . . . . . . . . . . . . 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 2836	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))) → 𝑦 ∈ 𝐶)
419		eqidd 2736	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))))
420		oveq1 7410	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝑥 − 𝑋) = (𝑦 − 𝑋))
421	420	oveq2d 7419	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑛 · (𝑥 − 𝑋)) = (𝑛 · (𝑦 − 𝑋)))
422	421	fveq2d 6879	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (cos‘(𝑛 · (𝑥 − 𝑋))) = (cos‘(𝑛 · (𝑦 − 𝑋))))
423	422	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → (cos‘(𝑛 · (𝑥 − 𝑋))) = (cos‘(𝑛 · (𝑦 − 𝑋))))
424		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
425	57	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → 𝑛 ∈ ℝ)
426	55, 220	sylan 580	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
427	58	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → 𝑋 ∈ ℝ)
428	426, 427	resubcld 11663	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (𝑦 − 𝑋) ∈ ℝ)
429	425, 428	remulcld 11263	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (𝑛 · (𝑦 − 𝑋)) ∈ ℝ)
430	429	recoscld 16160	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (cos‘(𝑛 · (𝑦 − 𝑋))) ∈ ℝ)
431	419, 423, 424, 430	fvmptd 6992	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦) = (cos‘(𝑛 · (𝑦 − 𝑋))))
432	431	fveq2d 6879	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) = (abs‘(cos‘(𝑛 · (𝑦 − 𝑋)))))
433		abscosbd 45255	. . . . . . . . . . . . 13 ⊢ ((𝑛 · (𝑦 − 𝑋)) ∈ ℝ → (abs‘(cos‘(𝑛 · (𝑦 − 𝑋)))) ≤ 1)
434	429, 433	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (abs‘(cos‘(𝑛 · (𝑦 − 𝑋)))) ≤ 1)
435	432, 434	eqbrtrd 5141	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1)
436	418, 435	syldan 591	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1)
437	436	ralrimiva 3132	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1)
438		breq2 5123	. . . . . . . . . . 11 ⊢ (𝑏 = 1 → ((abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1))
439	438	ralbidv 3163	. . . . . . . . . 10 ⊢ (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1))
440	439	rspcev 3601	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏)
441	203, 437, 440	sylancr 587	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏)
442		bddmulibl 25790	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
443	411, 412, 441, 442	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
444	399, 443	eqeltrd 2834	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) ∈ 𝐿¹)
445	391, 444	itgcl 25735	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 ∈ ℂ)
446	28, 142, 445, 102	fsumdivc 15800	. . . 4 ⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π) = Σ𝑛 ∈ (1...𝑁)(∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
447	176	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ dom vol)
448		anass 468	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑥 ∈ 𝐶)))
449		ancom 460	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (1...𝑁) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐶 ∧ 𝑛 ∈ (1...𝑁)))
450	449	anbi2i 623	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑥 ∈ 𝐶)) ↔ (𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑛 ∈ (1...𝑁))))
451	448, 450	bitri 275	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑛 ∈ (1...𝑁))))
452	451, 391	sylbir 235	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑛 ∈ (1...𝑁))) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
453	447, 28, 452, 444	itgfsum 25778	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) ∈ 𝐿¹ ∧ ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥))
454	453	simprd 495	. . . . . 6 ⊢ (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥)
455	454	eqcomd 2741	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥)
456	455	oveq1d 7418	. . . 4 ⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
457	384, 446, 456	3eqtr2d 2776	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
458	153, 457	oveq12d 7421	. 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 2735	. . . . . . . . . . 11 ⊢ (𝐷‘𝑁) = (𝐷‘𝑁)
462		eqid 2735	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π))
463	459, 460, 461, 462	dirkertrigeq 46078	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐷‘𝑁) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)))
464		oveq2 7411	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (𝑥 − 𝑋) → (𝑛 · 𝑠) = (𝑛 · (𝑥 − 𝑋)))
465	464	fveq2d 6879	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑥 − 𝑋) → (cos‘(𝑛 · 𝑠)) = (cos‘(𝑛 · (𝑥 − 𝑋))))
466	465	sumeq2sdv 15717	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑥 − 𝑋) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠)) = Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))
467	466	oveq2d 7419	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑥 − 𝑋) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))))
468	467	oveq1d 7418	. . . . . . . . . . 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 11663	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥 − 𝑋) ∈ ℝ)
472		halfre 12452	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ ℝ
473	472	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (1 / 2) ∈ ℝ)
474		fzfid 13989	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (1...𝑁) ∈ Fin)
475	390	an32s 652	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
476	474, 475	fsumrecl 15748	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
477	473, 476	readdcld 11262	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
478	44	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → π ∈ ℝ)
479	48	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → π ≠ 0)
480	477, 478, 479	redivcld 12067	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π) ∈ ℝ)
481	463, 469, 471, 480	fvmptd 6992	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π))
482	481, 480	eqeltrd 2834	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ)
483	119, 482	remulcld 11263	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ ℝ)
484	177	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ V)
485		eqidd 2736	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
486		eqidd 2736	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
487	484, 482, 119, 485, 486	offval2 7689	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))))
488	482	recnd 11261	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℂ)
489	488, 120	mulcomd 11254	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
490	489	mpteq2dva 5214	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))))
491	487, 490	eqtr2d 2771	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) = ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
492		eqid 2735	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))
493		eqid 2735	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))
494	194	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ℂ ⊆ ℂ)
495		cncfss 24841	. . . . . . . . . . . . . 14 ⊢ ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ))
496	189, 494, 495	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ))
497		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
498	58	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑋 ∈ ℝ)
499	497, 498	resubcld 11663	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 − 𝑋) ∈ ℝ)
500		eqid 2735	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) = (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋))
501	499, 500	fmptd 7103	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)):ℝ⟶ℝ)
502	189	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ℝ ⊆ ℂ)
503	502, 494	idcncfg 45850	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝑥) ∈ (ℝ–cn→ℂ))
504	502, 365, 494	constcncfg 45849	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝑋) ∈ (ℝ–cn→ℂ))
505	503, 504	subcncf 25395	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℂ))
506		cncfcdm 24840	. . . . . . . . . . . . . . . 16 ⊢ ((ℝ ⊆ ℂ ∧ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℂ)) → ((𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)):ℝ⟶ℝ))
507	189, 505, 506	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)):ℝ⟶ℝ))
508	501, 507	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℝ))
509	459	dirkercncf 46084	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁) ∈ (ℝ–cn→ℝ))
510	7, 509	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷‘𝑁) ∈ (ℝ–cn→ℝ))
511	508, 510	cncfcompt 45860	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (ℝ–cn→ℝ))
512	496, 511	sseldd 3959	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (ℝ–cn→ℂ))
513	44	renegcli 11542	. . . . . . . . . . . . . 14 ⊢ -π ∈ ℝ
514		iccssre 13444	. . . . . . . . . . . . . 14 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
515	513, 44, 514	mp2an 692	. . . . . . . . . . . . 13 ⊢ (-π[,]π) ⊆ ℝ
516	515	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (-π[,]π) ⊆ ℝ)
517	459	dirkerf 46074	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁):ℝ⟶ℝ)
518	7, 517	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷‘𝑁):ℝ⟶ℝ)
519	518	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → (𝐷‘𝑁):ℝ⟶ℝ)
520	516	sselda 3958	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
521	58	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
522	520, 521	resubcld 11663	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → (𝑥 − 𝑋) ∈ ℝ)
523	519, 522	ffvelcdmd 7074	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ)
524	523	recnd 11261	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℂ)
525	493, 512, 516, 494, 524	cncfmptssg 45848	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ ((-π[,]π)–cn→ℂ))
526	132	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ⊆ (-π[,]π))
527	492, 525, 526, 494, 488	cncfmptssg 45848	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (𝐶–cn→ℂ))
528		cnmbf 25610	. . . . . . . . . 10 ⊢ ((𝐶 ∈ dom vol ∧ (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (𝐶–cn→ℂ)) → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ MblFn)
529	176, 527, 528	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ MblFn)
530	513	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → -π ∈ ℝ)
531		0red 11236	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ℝ)
532		negpilt0 45257	. . . . . . . . . . . . . . . 16 ⊢ -π < 0
533	532	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -π < 0)
534	47	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 < π)
535	530, 531, 101, 533, 534	lttrd 11394	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -π < π)
536	530, 101, 535	ltled 11381	. . . . . . . . . . . . 13 ⊢ (𝜑 → -π ≤ π)
537	493, 512, 516, 502, 523	cncfmptssg 45848	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ ((-π[,]π)–cn→ℝ))
538	530, 101, 536, 537	evthiccabs 45473	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ∧ ∃𝑧 ∈ (-π[,]π)∀𝑤 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑧)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑤))))
539	538	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)))
540		eqidd 2736	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
541	420	fveq2d 6879	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
542	541	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (-π[,]π)) ∧ 𝑥 = 𝑦) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
543		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → 𝑦 ∈ (-π[,]π))
544	518	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (𝐷‘𝑁):ℝ⟶ℝ)
545	515, 543	sselid 3956	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → 𝑦 ∈ ℝ)
546	58	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
547	545, 546	resubcld 11663	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (𝑦 − 𝑋) ∈ ℝ)
548	544, 547	ffvelcdmd 7074	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑦 − 𝑋)) ∈ ℝ)
549	540, 542, 543, 548	fvmptd 6992	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
550	549	fveq2d 6879	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
551	550	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
552		eqidd 2736	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
553		oveq1 7410	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑐 → (𝑥 − 𝑋) = (𝑐 − 𝑋))
554	553	fveq2d 6879	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑐 → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑐 − 𝑋)))
555	554	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑥 = 𝑐) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑐 − 𝑋)))
556		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → 𝑐 ∈ (-π[,]π))
557	518	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (𝐷‘𝑁):ℝ⟶ℝ)
558	515, 556	sselid 3956	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → 𝑐 ∈ ℝ)
559	58	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
560	558, 559	resubcld 11663	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (𝑐 − 𝑋) ∈ ℝ)
561	557, 560	ffvelcdmd 7074	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑐 − 𝑋)) ∈ ℝ)
562	552, 555, 556, 561	fvmptd 6992	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐) = ((𝐷‘𝑁)‘(𝑐 − 𝑋)))
563	562	fveq2d 6879	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
564	563	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
565	551, 564	breq12d 5132	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → ((abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ↔ (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
566	565	ralbidva 3161	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ↔ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
567	566	rexbidva 3162	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ↔ ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
568	539, 567	mpbid 232	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
569	561	recnd 11261	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑐 − 𝑋)) ∈ ℂ)
570	569	abscld 15453	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∈ ℝ)
571	570	3adant3 1132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∈ ℝ)
572		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝜑
573		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 𝑐 ∈ (-π[,]π)
574		nfra1 3266	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))
575	572, 573, 574	nf3an 1901	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
576		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
577	482	ralrimiva 3132	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ)
578		dmmptg 6231	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ 𝐶 ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ → dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = 𝐶)
579	577, 578	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = 𝐶)
580	579	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = 𝐶)
581	576, 580	eleqtrd 2836	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → 𝑦 ∈ 𝐶)
582	581	3ad2antl1 1186	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → 𝑦 ∈ 𝐶)
583		eqidd 2736	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
584	541	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
585		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
586	518	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝐷‘𝑁):ℝ⟶ℝ)
587	136, 585	sselid 3956	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
588	58	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑋 ∈ ℝ)
589	587, 588	resubcld 11663	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝑦 − 𝑋) ∈ ℝ)
590	586, 589	ffvelcdmd 7074	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑦 − 𝑋)) ∈ ℝ)
591	583, 584, 585, 590	fvmptd 6992	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
592	591	fveq2d 6879	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
593	592	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
594		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
595	132	sseli 3954	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝐶 → 𝑦 ∈ (-π[,]π))
596	595	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ (-π[,]π))
597		rspa 3231	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
598	594, 596, 597	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
599	593, 598	eqbrtrd 5141	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
600	599	3adantl2 1168	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
601	582, 600	syldan 591	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
602	601	ex 412	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → (𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
603	575, 602	ralrimi 3240	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
604		breq2 5123	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) → ((abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
605	604	ralbidv 3163	. . . . . . . . . . . . 13 ⊢ (𝑏 = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
606	605	rspcev 3601	. . . . . . . . . . . 12 ⊢ (((abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏)
607	571, 603, 606	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏)
608	607	rexlimdv3a 3145	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏))
609	568, 608	mpd 15	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏)
610		bddmulibl 25790	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
611	529, 140, 609, 610	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
612	491, 611	eqeltrd 2834	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) ∈ 𝐿¹)
613	142, 483, 612	itgmulc2 25785	. . . . . 6 ⊢ (𝜑 → (π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) = ∫𝐶(π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) d𝑥)
614	142	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → π ∈ ℂ)
615	120, 488, 614	mul13d 45256	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) = (π · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))))
616	489	oveq2d 7419	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (π · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))) = (π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))))
617	615, 616	eqtrd 2770	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) = (π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))))
618	617	itgeq2dv 25733	. . . . . 6 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) d𝑥 = ∫𝐶(π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) d𝑥)
619	613, 618	eqtr4d 2773	. . . . 5 ⊢ (𝜑 → (π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) = ∫𝐶((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) d𝑥)
620	148	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (1 / 2) ∈ ℂ)
621	620, 120	mulcomd 11254	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (1 / 2)))
622	396	an32s 652	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℂ)
623	474, 120, 622	fsummulc2 15798	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) = Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))))
624	623	eqcomd 2741	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) = ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))))
625	621, 624	oveq12d 7421	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) = (((𝐹‘𝑥) · (1 / 2)) + ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))))
626	474, 622	fsumcl 15747	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℂ)
627	120, 620, 626	adddid 11257	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))) = (((𝐹‘𝑥) · (1 / 2)) + ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))))
628	481	oveq1d 7418	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π) = ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π) · π))
629	620, 626	addcld 11252	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℂ)
630	629, 614, 479	divcan1d 12016	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π) · π) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))))
631	628, 630	eqtr2d 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) = (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π))
632	631	oveq2d 7419	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))) = ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)))
633	625, 627, 632	3eqtr2rd 2777	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) = (((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))))
634	633	itgeq2dv 25733	. . . . 5 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) d𝑥 = ∫𝐶(((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) d𝑥)
635		remulcl 11212	. . . . . . 7 ⊢ (((1 / 2) ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ) → ((1 / 2) · (𝐹‘𝑥)) ∈ ℝ)
636	472, 119, 635	sylancr 587	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) · (𝐹‘𝑥)) ∈ ℝ)
637	148, 119, 140	iblmulc2 25782	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((1 / 2) · (𝐹‘𝑥))) ∈ 𝐿¹)
638	391	an32s 652	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
639	474, 638	fsumrecl 15748	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
640	453	simpld 494	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) ∈ 𝐿¹)
641	636, 637, 639, 640	itgadd 25776	. . . . 5 ⊢ (𝜑 → ∫𝐶(((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) d𝑥 = (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥))
642	619, 634, 641	3eqtrrd 2775	. . . 4 ⊢ (𝜑 → (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥) = (π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥))
643	642	oveq1d 7418	. . 3 ⊢ (𝜑 → ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥) / π) = ((π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) / π))
644	636, 637	itgcl 25735	. . . 4 ⊢ (𝜑 → ∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 ∈ ℂ)
645	639, 640	itgcl 25735	. . . 4 ⊢ (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 ∈ ℂ)
646	644, 645, 142, 102	divdird 12053	. . 3 ⊢ (𝜑 → ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥) / π) = ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π)))
647	483, 612	itgcl 25735	. . . 4 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥 ∈ ℂ)
648	647, 142, 102	divcan3d 12020	. . 3 ⊢ (𝜑 → ((π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) / π) = ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥)
649	643, 646, 648	3eqtr3d 2778	. 2 ⊢ (𝜑 → ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π)) = ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥)
650	90, 458, 649	3eqtrd 2774	1 ⊢ (𝜑 → (𝑆‘𝑁) = ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2108 ≠ wne 2932 ∀wral 3051 ∃wrex 3060 Vcvv 3459 ⊆ wss 3926 ifcif 4500 class class class wbr 5119 ↦ cmpt 5201 dom cdm 5654 ↾ cres 5656 ⟶wf 6526 ‘cfv 6530 (class class class)co 7403 ∘_f cof 7667 ℂcc 11125 ℝcr 11126 0cc0 11127 1c1 11128 + caddc 11130 · cmul 11132 < clt 11267 ≤ cle 11268 − cmin 11464 -cneg 11465 / cdiv 11892 ℕcn 12238 2c2 12293 ℕ₀cn0 12499 (,)cioo 13360 [,]cicc 13363 ...cfz 13522 mod cmo 13884 abscabs 15251 Σcsu 15700 sincsin 16077 cosccos 16078 πcpi 16080 –cn→ccncf 24818 volcvol 25414 MblFncmbf 25565 𝐿¹cibl 25568 ∫citg 25569

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7727 ax-inf2 9653 ax-cc 10447 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205 ax-addf 11206

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-tp 4606 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-iin 4970 df-disj 5087 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-se 5607 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6483 df-fun 6532 df-fn 6533 df-f 6534 df-f1 6535 df-fo 6536 df-f1o 6537 df-fv 6538 df-isom 6539 df-riota 7360 df-ov 7406 df-oprab 7407 df-mpo 7408 df-of 7669 df-ofr 7670 df-om 7860 df-1st 7986 df-2nd 7987 df-supp 8158 df-frecs 8278 df-wrecs 8309 df-recs 8383 df-rdg 8422 df-1o 8478 df-2o 8479 df-oadd 8482 df-omul 8483 df-er 8717 df-map 8840 df-pm 8841 df-ixp 8910 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-fsupp 9372 df-fi 9421 df-sup 9452 df-inf 9453 df-oi 9522 df-dju 9913 df-card 9951 df-acn 9954 df-pnf 11269 df-mnf 11270 df-xr 11271 df-ltxr 11272 df-le 11273 df-sub 11466 df-neg 11467 df-div 11893 df-nn 12239 df-2 12301 df-3 12302 df-4 12303 df-5 12304 df-6 12305 df-7 12306 df-8 12307 df-9 12308 df-n0 12500 df-z 12587 df-dec 12707 df-uz 12851 df-q 12963 df-rp 13007 df-xneg 13126 df-xadd 13127 df-xmul 13128 df-ioo 13364 df-ioc 13365 df-ico 13366 df-icc 13367 df-fz 13523 df-fzo 13670 df-fl 13807 df-mod 13885 df-seq 14018 df-exp 14078 df-fac 14290 df-bc 14319 df-hash 14347 df-shft 15084 df-cj 15116 df-re 15117 df-im 15118 df-sqrt 15252 df-abs 15253 df-limsup 15485 df-clim 15502 df-rlim 15503 df-sum 15701 df-ef 16081 df-sin 16083 df-cos 16084 df-pi 16086 df-struct 17164 df-sets 17181 df-slot 17199 df-ndx 17211 df-base 17227 df-ress 17250 df-plusg 17282 df-mulr 17283 df-starv 17284 df-sca 17285 df-vsca 17286 df-ip 17287 df-tset 17288 df-ple 17289 df-ds 17291 df-unif 17292 df-hom 17293 df-cco 17294 df-rest 17434 df-topn 17435 df-0g 17453 df-gsum 17454 df-topgen 17455 df-pt 17456 df-prds 17459 df-xrs 17514 df-qtop 17519 df-imas 17520 df-xps 17522 df-mre 17596 df-mrc 17597 df-acs 17599 df-mgm 18616 df-sgrp 18695 df-mnd 18711 df-submnd 18760 df-mulg 19049 df-cntz 19298 df-cmn 19761 df-psmet 21305 df-xmet 21306 df-met 21307 df-bl 21308 df-mopn 21309 df-fbas 21310 df-fg 21311 df-cnfld 21314 df-top 22830 df-topon 22847 df-topsp 22869 df-bases 22882 df-cld 22955 df-ntr 22956 df-cls 22957 df-nei 23034 df-lp 23072 df-perf 23073 df-cn 23163 df-cnp 23164 df-t1 23250 df-haus 23251 df-cmp 23323 df-tx 23498 df-hmeo 23691 df-fil 23782 df-fm 23874 df-flim 23875 df-flf 23876 df-xms 24257 df-ms 24258 df-tms 24259 df-cncf 24820 df-ovol 25415 df-vol 25416 df-mbf 25570 df-itg1 25571 df-itg2 25572 df-ibl 25573 df-itg 25574 df-0p 25621 df-limc 25817 df-dv 25818

This theorem is referenced by: fourierdlem111 46194

W3C validator