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 46204

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 7439	. . . . . 6 ⊢ (𝑚 = 𝑁 → (1...𝑚) = (1...𝑁))
4	3	sumeq1d 15736	. . . . 5 ⊢ (𝑚 = 𝑁 → Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
5	4	oveq2d 7447	. . . 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 12541	. . . . . . 7 ⊢ 0 ∈ ℕ₀
10	9	a1i 11	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℕ₀)
11	9	elexi 3503	. . . . . . 7 ⊢ 0 ∈ V
12		eleq1 2829	. . . . . . . . 9 ⊢ (𝑛 = 0 → (𝑛 ∈ ℕ₀ ↔ 0 ∈ ℕ₀))
13	12	anbi2d 630	. . . . . . . 8 ⊢ (𝑛 = 0 → ((𝜑 ∧ 𝑛 ∈ ℕ₀) ↔ (𝜑 ∧ 0 ∈ ℕ₀)))
14		fveq2 6906	. . . . . . . . 9 ⊢ (𝑛 = 0 → (𝐴‘𝑛) = (𝐴‘0))
15	14	eleq1d 2826	. . . . . . . 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 46144	. . . . . . . . 9 ⊢ (𝜑 → ((𝑛 ∈ ℕ₀ → (𝐴‘𝑛) ∈ ℝ) ∧ (𝑛 ∈ ℕ → (𝐵‘𝑛) ∈ ℝ)))
23	22	simpld 494	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ ℕ₀ → (𝐴‘𝑛) ∈ ℝ))
24	23	imp 406	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝐴‘𝑛) ∈ ℝ)
25	11, 16, 24	vtocl 3558	. . . . . 6 ⊢ ((𝜑 ∧ 0 ∈ ℕ₀) → (𝐴‘0) ∈ ℝ)
26	8, 10, 25	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝐴‘0) ∈ ℝ)
27	26	rehalfcld 12513	. . . 4 ⊢ (𝜑 → ((𝐴‘0) / 2) ∈ ℝ)
28		fzfid 14014	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
29		eleq1 2829	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ ℕ₀ ↔ 𝑛 ∈ ℕ₀))
30	29	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → ((𝜑 ∧ 𝑘 ∈ ℕ₀) ↔ (𝜑 ∧ 𝑛 ∈ ℕ₀)))
31		simpl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → 𝑘 = 𝑛)
32	31	oveq1d 7446	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → (𝑘 · 𝑥) = (𝑛 · 𝑥))
33	32	fveq2d 6910	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑘 · 𝑥)) = (cos‘(𝑛 · 𝑥)))
34	33	oveq2d 7447	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))
35	34	itgeq2dv 25817	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥)
36	35	eleq1d 2826	. . . . . . . . . . . . 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 46138	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝐴‘𝑘) ∈ ℝ ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹) ∧ ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ))
42	41	simprd 495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ)
43	37, 42	chvarvv 1998	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
44		pire 26500	. . . . . . . . . . . 12 ⊢ π ∈ ℝ
45	44	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → π ∈ ℝ)
46		0re 11263	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
47		pipos 26502	. . . . . . . . . . . . 13 ⊢ 0 < π
48	46, 47	gtneii 11373	. . . . . . . . . . . 12 ⊢ π ≠ 0
49	48	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → π ≠ 0)
50	43, 45, 49	redivcld 12095	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
51	50, 20	fmptd 7134	. . . . . . . . 9 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℝ)
52	51	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐴:ℕ₀⟶ℝ)
53		elfznn 13593	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
54	53	nnnn0d 12587	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ₀)
55	54	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ₀)
56	52, 55	ffvelcdmd 7105	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐴‘𝑛) ∈ ℝ)
57	55	nn0red 12588	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℝ)
58		fourierdlem83.x	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℝ)
59	58	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℝ)
60	57, 59	remulcld 11291	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 · 𝑋) ∈ ℝ)
61	60	recoscld 16180	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℝ)
62	56, 61	remulcld 11291	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
63		eleq1 2829	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ ℕ ↔ 𝑛 ∈ ℕ))
64	63	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → ((𝜑 ∧ 𝑘 ∈ ℕ) ↔ (𝜑 ∧ 𝑛 ∈ ℕ)))
65		oveq1 7438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → (𝑘 · 𝑥) = (𝑛 · 𝑥))
66	65	fveq2d 6910	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → (sin‘(𝑘 · 𝑥)) = (sin‘(𝑛 · 𝑥)))
67	66	oveq2d 7447	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑛 → ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
68	67	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
69	68	itgeq2dv 25817	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥)
70	69	eleq1d 2826	. . . . . . . . . . . . 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 46143	. . . . . . . . . . . . 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 12095	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
81	80, 21	fmptd 7134	. . . . . . . . 9 ⊢ (𝜑 → 𝐵:ℕ⟶ℝ)
82	81	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐵:ℕ⟶ℝ)
83	53	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ)
84	82, 83	ffvelcdmd 7105	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐵‘𝑛) ∈ ℝ)
85	60	resincld 16179	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
86	84, 85	remulcld 11291	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
87	62, 86	readdcld 11290	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
88	28, 87	fsumrecl 15770	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
89	27, 88	readdcld 11290	. . 3 ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) ∈ ℝ)
90	2, 6, 7, 89	fvmptd 7023	. 2 ⊢ (𝜑 → (𝑆‘𝑁) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
91	20	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐴 = (𝑛 ∈ ℕ₀ ↦ (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
92		oveq1 7438	. . . . . . . . . . . . 13 ⊢ (𝑛 = 0 → (𝑛 · 𝑥) = (0 · 𝑥))
93	92	fveq2d 6910	. . . . . . . . . . . 12 ⊢ (𝑛 = 0 → (cos‘(𝑛 · 𝑥)) = (cos‘(0 · 𝑥)))
94	93	oveq2d 7447	. . . . . . . . . . 11 ⊢ (𝑛 = 0 → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(0 · 𝑥))))
95	94	adantr 480	. . . . . . . . . 10 ⊢ ((𝑛 = 0 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(0 · 𝑥))))
96	95	itgeq2dv 25817	. . . . . . . . 9 ⊢ (𝑛 = 0 → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥)
97	96	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 0) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥)
98	97	oveq1d 7446	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 = 0) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) = (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
99	17, 18, 19, 20, 10	fourierdlem16 46138	. . . . . . . . 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 12095	. . . . . . 7 ⊢ (𝜑 → (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) ∈ ℝ)
104	91, 98, 10, 103	fvmptd 7023	. . . . . 6 ⊢ (𝜑 → (𝐴‘0) = (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
105		ioosscn 13449	. . . . . . . . . . . . . . 15 ⊢ (-π(,)π) ⊆ ℂ
106		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐶)
107	106, 18	eleqtrdi 2851	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ (-π(,)π))
108	105, 107	sselid 3981	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ℂ)
109	108	mul02d 11459	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐶 → (0 · 𝑥) = 0)
110	109	fveq2d 6910	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐶 → (cos‘(0 · 𝑥)) = (cos‘0))
111		cos0 16186	. . . . . . . . . . . 12 ⊢ (cos‘0) = 1
112	110, 111	eqtrdi 2793	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐶 → (cos‘(0 · 𝑥)) = 1)
113	112	oveq2d 7447	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐶 → ((𝐹‘𝑥) · (cos‘(0 · 𝑥))) = ((𝐹‘𝑥) · 1))
114	113	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(0 · 𝑥))) = ((𝐹‘𝑥) · 1))
115	17	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐹:ℝ⟶ℝ)
116		ioossre 13448	. . . . . . . . . . . . . 14 ⊢ (-π(,)π) ⊆ ℝ
117	116, 107	sselid 3981	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ℝ)
118	117	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
119	115, 118	ffvelcdmd 7105	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
120	119	recnd 11289	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
121	120	mulridd 11278	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · 1) = (𝐹‘𝑥))
122	114, 121	eqtrd 2777	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(0 · 𝑥))) = (𝐹‘𝑥))
123	122	itgeq2dv 25817	. . . . . . 7 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 = ∫𝐶(𝐹‘𝑥) d𝑥)
124	123	oveq1d 7446	. . . . . 6 ⊢ (𝜑 → (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) = (∫𝐶(𝐹‘𝑥) d𝑥 / π))
125	104, 124	eqtrd 2777	. . . . 5 ⊢ (𝜑 → (𝐴‘0) = (∫𝐶(𝐹‘𝑥) d𝑥 / π))
126	125	oveq1d 7446	. . . 4 ⊢ (𝜑 → ((𝐴‘0) / 2) = ((∫𝐶(𝐹‘𝑥) d𝑥 / π) / 2))
127	17	feqmptd 6977	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)))
128	127	reseq1d 5996	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ 𝐶))
129	44	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐶 → π ∈ ℝ)
130	129	renegcld 11690	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐶 → -π ∈ ℝ)
131		ioossicc 13473	. . . . . . . . . . . . 13 ⊢ (-π(,)π) ⊆ (-π[,]π)
132	18, 131	eqsstri 4030	. . . . . . . . . . . 12 ⊢ 𝐶 ⊆ (-π[,]π)
133	132	sseli 3979	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ (-π[,]π))
134		eliccre 45518	. . . . . . . . . . 11 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ ∧ 𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
135	130, 129, 133, 134	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ℝ)
136	135	ssriv 3987	. . . . . . . . 9 ⊢ 𝐶 ⊆ ℝ
137		resmpt 6055	. . . . . . . . 9 ⊢ (𝐶 ⊆ ℝ → ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
138	136, 137	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
139	128, 138	eqtr2d 2778	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝐹 ↾ 𝐶))
140	139, 19	eqeltrd 2841	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
141	119, 140	itgcl 25819	. . . . 5 ⊢ (𝜑 → ∫𝐶(𝐹‘𝑥) d𝑥 ∈ ℂ)
142	101	recnd 11289	. . . . 5 ⊢ (𝜑 → π ∈ ℂ)
143		2cnd 12344	. . . . 5 ⊢ (𝜑 → 2 ∈ ℂ)
144		2ne0 12370	. . . . . 6 ⊢ 2 ≠ 0
145	144	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ≠ 0)
146	141, 142, 143, 102, 145	divdiv32d 12068	. . . 4 ⊢ (𝜑 → ((∫𝐶(𝐹‘𝑥) d𝑥 / π) / 2) = ((∫𝐶(𝐹‘𝑥) d𝑥 / 2) / π))
147	141, 143, 145	divrecd 12046	. . . . . 6 ⊢ (𝜑 → (∫𝐶(𝐹‘𝑥) d𝑥 / 2) = (∫𝐶(𝐹‘𝑥) d𝑥 · (1 / 2)))
148	143, 145	reccld 12036	. . . . . . 7 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
149	141, 148	mulcomd 11282	. . . . . 6 ⊢ (𝜑 → (∫𝐶(𝐹‘𝑥) d𝑥 · (1 / 2)) = ((1 / 2) · ∫𝐶(𝐹‘𝑥) d𝑥))
150	148, 119, 140	itgmulc2 25869	. . . . . 6 ⊢ (𝜑 → ((1 / 2) · ∫𝐶(𝐹‘𝑥) d𝑥) = ∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥)
151	147, 149, 150	3eqtrd 2781	. . . . 5 ⊢ (𝜑 → (∫𝐶(𝐹‘𝑥) d𝑥 / 2) = ∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥)
152	151	oveq1d 7446	. . . 4 ⊢ (𝜑 → ((∫𝐶(𝐹‘𝑥) d𝑥 / 2) / π) = (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π))
153	126, 146, 152	3eqtrd 2781	. . 3 ⊢ (𝜑 → ((𝐴‘0) / 2) = (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π))
154	55, 50	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
155	20	fvmpt2 7027	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ₀ ∧ (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐴‘𝑛) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
156	55, 154, 155	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐴‘𝑛) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
157	156	oveq1d 7446	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))))
158	154	recnd 11289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
159	61	recnd 11289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℂ)
160	158, 159	mulcomd 11282	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
161	55, 43	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
162	161	recnd 11289	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
163	142	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → π ∈ ℂ)
164	48	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → π ≠ 0)
165	159, 162, 163, 164	divassd 12078	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
166	17	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → 𝐹:ℝ⟶ℝ)
167	117	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
168	166, 167	ffvelcdmd 7105	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
169		nn0re 12535	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℝ)
170	169	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
171	170, 167	remulcld 11291	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℝ)
172	171	recoscld 16180	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
173	168, 172	remulcld 11291	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
174	54, 173	sylanl2 681	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
175		ioombl 25600	. . . . . . . . . . . . . . . . . . 19 ⊢ (-π(,)π) ∈ dom vol
176	18, 175	eqeltri 2837	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐶 ∈ dom vol
177	176	elexi 3503	. . . . . . . . . . . . . . . . 17 ⊢ 𝐶 ∈ V
178	177	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝐶 ∈ V)
179		eqidd 2738	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))))
180		eqidd 2738	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
181	178, 172, 168, 179, 180	offval2 7717	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
182	172	recnd 11289	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℂ)
183	120	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
184	182, 183	mulcomd 11282	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))
185	184	mpteq2dva 5242	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))))
186	181, 185	eqtr2d 2778	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
187		coscn 26489	. . . . . . . . . . . . . . . . . 18 ⊢ cos ∈ (ℂ–cn→ℂ)
188	187	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → cos ∈ (ℂ–cn→ℂ))
189		ax-resscn 11212	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℝ ⊆ ℂ
190	136, 189	sstri 3993	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐶 ⊆ ℂ
191	190	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝐶 ⊆ ℂ)
192	169	recnd 11289	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℂ)
193	192	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝑛 ∈ ℂ)
194		ssid 4006	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℂ ⊆ ℂ
195	194	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ℂ ⊆ ℂ)
196	191, 193, 195	constcncfg 45887	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ 𝑛) ∈ (𝐶–cn→ℂ))
197	191, 195	idcncfg 45888	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ 𝑥) ∈ (𝐶–cn→ℂ))
198	196, 197	mulcncf 25480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶–cn→ℂ))
199	188, 198	cncfmpt1f 24940	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ))
200		cnmbf 25694	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ dom vol ∧ (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
201	176, 199, 200	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
202	140	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
203		1re 11261	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
204		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))))
205	169	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
206	117	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
207	205, 206	remulcld 11291	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℝ)
208	207	recoscld 16180	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
209	208	ralrimiva 3146	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ₀ → ∀𝑥 ∈ 𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
210	209	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → ∀𝑥 ∈ 𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
211		dmmptg 6262	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 ∈ 𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ → dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
212	210, 211	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
213	204, 212	eleqtrd 2843	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦 ∈ 𝐶)
214		eqidd 2738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))))
215		oveq2 7439	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑛 · 𝑥) = (𝑛 · 𝑦))
216	215	fveq2d 6910	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
217	216	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
218		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
219	169	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → 𝑛 ∈ ℝ)
220	136, 218	sselid 3981	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
221	219, 220	remulcld 11291	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (𝑛 · 𝑦) ∈ ℝ)
222	221	recoscld 16180	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (cos‘(𝑛 · 𝑦)) ∈ ℝ)
223	214, 217, 218, 222	fvmptd 7023	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦) = (cos‘(𝑛 · 𝑦)))
224	223	fveq2d 6910	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(cos‘(𝑛 · 𝑦))))
225		abscosbd 45290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 · 𝑦) ∈ ℝ → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
226	221, 225	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
227	224, 226	eqbrtrd 5165	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
228	213, 227	syldan 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
229	228	ralrimiva 3146	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
230		breq2 5147	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 1 → ((abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
231	230	ralbidv 3178	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
232	231	rspcev 3622	. . . . . . . . . . . . . . . . 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 25874	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
236	201, 202, 234, 235	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
237	186, 236	eqeltrd 2841	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
238	55, 237	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
239	159, 174, 238	itgmulc2 25869	. . . . . . . . . . 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 11470	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))))
244	240, 242	mulcomd 11282	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥))) = ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))
245	244	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
246	243, 245	eqtrd 2777	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
247	246	itgeq2dv 25817	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
248	239, 247	eqtrd 2777	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
249	248	oveq1d 7446	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
250	165, 249	eqtr3d 2779	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
251	157, 160, 250	3eqtrd 2781	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
252	83, 80	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
253	21	fvmpt2 7027	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐵‘𝑛) = (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
254	83, 252, 253	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐵‘𝑛) = (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
255	254	oveq1d 7446	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))))
256	252	recnd 11289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
257	85	recnd 11289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℂ)
258	256, 257	mulcomd 11282	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
259	83, 77	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
260	259	recnd 11289	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
261	257, 260, 163, 164	divassd 12078	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
262	119	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
263		nnre 12273	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
264	263	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
265	117	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
266	264, 265	remulcld 11291	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℝ)
267	266	resincld 16179	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
268	267	adantll 714	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
269	262, 268	remulcld 11291	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
270	53, 269	sylanl2 681	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
271	177	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 ∈ V)
272		eqidd 2738	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))))
273		eqidd 2738	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
274	271, 268, 262, 272, 273	offval2 7717	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
275	268	recnd 11289	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℂ)
276	120	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
277	275, 276	mulcomd 11282	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
278	277	mpteq2dva 5242	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))))
279	274, 278	eqtr2d 2778	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
280		sincn 26488	. . . . . . . . . . . . . . . . . 18 ⊢ sin ∈ (ℂ–cn→ℂ)
281	280	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sin ∈ (ℂ–cn→ℂ))
282	190	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → 𝐶 ⊆ ℂ)
283	263	recnd 11289	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
284	194	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → ℂ ⊆ ℂ)
285	282, 283, 284	constcncfg 45887	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (𝑥 ∈ 𝐶 ↦ 𝑛) ∈ (𝐶–cn→ℂ))
286	282, 284	idcncfg 45888	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (𝑥 ∈ 𝐶 ↦ 𝑥) ∈ (𝐶–cn→ℂ))
287	285, 286	mulcncf 25480	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → (𝑥 ∈ 𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶–cn→ℂ))
288	287	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶–cn→ℂ))
289	281, 288	cncfmpt1f 24940	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ))
290		cnmbf 25694	. . . . . . . . . . . . . . . 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 3146	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → ∀𝑥 ∈ 𝐶 (sin‘(𝑛 · 𝑥)) ∈ ℝ)
295		dmmptg 6262	. . . . . . . . . . . . . . . . . . . . . 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 2843	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦 ∈ 𝐶)
299		eqidd 2738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))))
300	215	fveq2d 6910	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
301	300	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
302		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
303	263	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → 𝑛 ∈ ℝ)
304	136, 302	sselid 3981	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
305	303, 304	remulcld 11291	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (𝑛 · 𝑦) ∈ ℝ)
306	305	resincld 16179	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (sin‘(𝑛 · 𝑦)) ∈ ℝ)
307	299, 301, 302, 306	fvmptd 7023	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦) = (sin‘(𝑛 · 𝑦)))
308	307	fveq2d 6910	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(sin‘(𝑛 · 𝑦))))
309		abssinbd 45307	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 · 𝑦) ∈ ℝ → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
310	305, 309	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
311	308, 310	eqbrtrd 5165	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
312	298, 311	syldan 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
313	312	ralrimiva 3146	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
314		breq2 5147	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 1 → ((abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
315	314	ralbidv 3178	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
316	315	rspcev 3622	. . . . . . . . . . . . . . . . 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 25874	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
320	291, 292, 318, 319	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
321	279, 320	eqeltrd 2841	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
322	83, 321	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
323	257, 270, 322	itgmulc2 25869	. . . . . . . . . . 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 11470	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))))
327	324, 325	mulcomd 11282	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥))) = ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))
328	327	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
329	326, 328	eqtrd 2777	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
330	329	itgeq2dv 25817	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
331	323, 330	eqtrd 2777	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
332	331	oveq1d 7446	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
333	261, 332	eqtr3d 2779	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
334	255, 258, 333	3eqtrd 2781	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
335	251, 334	oveq12d 7449	. . . . . 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 11291	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
340	336, 339	remulcld 11291	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) ∈ ℝ)
341	241, 242, 240	mul13d 45291	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
342	242, 241	mulcomd 11282	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))
343	342	oveq2d 7447	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))))
344	341, 343	eqtrd 2777	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))))
345	344	mpteq2dva 5242	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) = (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))))
346	159, 174, 238	iblmulc2 25866	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))) ∈ 𝐿¹)
347	345, 346	eqeltrd 2841	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) ∈ 𝐿¹)
348	340, 347	itgcl 25819	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
349	83, 267	sylan 580	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
350	85	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
351	349, 350	remulcld 11291	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
352	336, 351	remulcld 11291	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
353	241, 325, 324	mul13d 45291	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
354	325, 241	mulcomd 11282	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
355	354	oveq2d 7447	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))))
356	353, 355	eqtrd 2777	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))))
357	356	mpteq2dva 5242	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))))
358	257, 270, 322	iblmulc2 25866	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))) ∈ 𝐿¹)
359	357, 358	eqeltrd 2841	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) ∈ 𝐿¹)
360	352, 359	itgcl 25819	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
361	348, 360, 163, 164	divdird 12081	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π) + (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π)))
362	53	nncnd 12282	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
363	362	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℂ)
364	108	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℂ)
365	58	recnd 11289	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ ℂ)
366	365	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑋 ∈ ℂ)
367	363, 364, 366	subdid 11719	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · (𝑥 − 𝑋)) = ((𝑛 · 𝑥) − (𝑛 · 𝑋)))
368	367	fveq2d 6910	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) = (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))))
369	363, 364	mulcld 11281	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℂ)
370	363, 366	mulcld 11281	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑋) ∈ ℂ)
371		cossub 16205	. . . . . . . . . . . . 13 ⊢ (((𝑛 · 𝑥) ∈ ℂ ∧ (𝑛 · 𝑋) ∈ ℂ) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
372	369, 370, 371	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
373	368, 372	eqtrd 2777	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
374	373	oveq2d 7447	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) = ((𝐹‘𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
375	339	recnd 11289	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℂ)
376	351	recnd 11289	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℂ)
377	241, 375, 376	adddid 11285	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
378	374, 377	eqtrd 2777	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) = (((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
379	378	itgeq2dv 25817	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = ∫𝐶(((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥)
380	340, 347, 352, 359	itgadd 25860	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶(((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥 = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥))
381	379, 380	eqtr2d 2778	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) = ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥)
382	381	oveq1d 7446	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
383	335, 361, 382	3eqtr2d 2783	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
384	383	sumeq2dv 15738	. . . 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 11691	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑥 − 𝑋) ∈ ℝ)
389	385, 388	remulcld 11291	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · (𝑥 − 𝑋)) ∈ ℝ)
390	389	recoscld 16180	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
391	336, 390	remulcld 11291	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
392	177	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ V)
393		eqidd 2738	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))))
394		eqidd 2738	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
395	392, 390, 336, 393, 394	offval2 7717	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · (𝑥 − 𝑋))) · (𝐹‘𝑥))))
396	390	recnd 11289	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℂ)
397	396, 241	mulcomd 11282	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · (𝑥 − 𝑋))) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))))
398	397	mpteq2dva 5242	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · (𝑥 − 𝑋))) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))))
399	395, 398	eqtr2d 2778	. . . . . . 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 45887	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ 𝑋) ∈ (𝐶–cn→ℂ))
407	402, 406	subcncf 25479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝑥 − 𝑋)) ∈ (𝐶–cn→ℂ))
408	401, 407	mulcncf 25480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝑛 · (𝑥 − 𝑋))) ∈ (𝐶–cn→ℂ))
409	400, 408	cncfmpt1f 24940	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ (𝐶–cn→ℂ))
410		cnmbf 25694	. . . . . . . . 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 3146	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∀𝑥 ∈ 𝐶 (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
415		dmmptg 6262	. . . . . . . . . . . . . 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 2843	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))) → 𝑦 ∈ 𝐶)
419		eqidd 2738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))))
420		oveq1 7438	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝑥 − 𝑋) = (𝑦 − 𝑋))
421	420	oveq2d 7447	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑛 · (𝑥 − 𝑋)) = (𝑛 · (𝑦 − 𝑋)))
422	421	fveq2d 6910	. . . . . . . . . . . . . . 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 11691	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (𝑦 − 𝑋) ∈ ℝ)
429	425, 428	remulcld 11291	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (𝑛 · (𝑦 − 𝑋)) ∈ ℝ)
430	429	recoscld 16180	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (cos‘(𝑛 · (𝑦 − 𝑋))) ∈ ℝ)
431	419, 423, 424, 430	fvmptd 7023	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦) = (cos‘(𝑛 · (𝑦 − 𝑋))))
432	431	fveq2d 6910	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) = (abs‘(cos‘(𝑛 · (𝑦 − 𝑋)))))
433		abscosbd 45290	. . . . . . . . . . . . 13 ⊢ ((𝑛 · (𝑦 − 𝑋)) ∈ ℝ → (abs‘(cos‘(𝑛 · (𝑦 − 𝑋)))) ≤ 1)
434	429, 433	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (abs‘(cos‘(𝑛 · (𝑦 − 𝑋)))) ≤ 1)
435	432, 434	eqbrtrd 5165	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1)
436	418, 435	syldan 591	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1)
437	436	ralrimiva 3146	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1)
438		breq2 5147	. . . . . . . . . . 11 ⊢ (𝑏 = 1 → ((abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1))
439	438	ralbidv 3178	. . . . . . . . . 10 ⊢ (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1))
440	439	rspcev 3622	. . . . . . . . 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 25874	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
443	411, 412, 441, 442	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
444	399, 443	eqeltrd 2841	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) ∈ 𝐿¹)
445	391, 444	itgcl 25819	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 ∈ ℂ)
446	28, 142, 445, 102	fsumdivc 15822	. . . 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 25862	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) ∈ 𝐿¹ ∧ ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥))
454	453	simprd 495	. . . . . 6 ⊢ (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥)
455	454	eqcomd 2743	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥)
456	455	oveq1d 7446	. . . 4 ⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
457	384, 446, 456	3eqtr2d 2783	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
458	153, 457	oveq12d 7449	. 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 2737	. . . . . . . . . . 11 ⊢ (𝐷‘𝑁) = (𝐷‘𝑁)
462		eqid 2737	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π))
463	459, 460, 461, 462	dirkertrigeq 46116	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐷‘𝑁) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)))
464		oveq2 7439	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (𝑥 − 𝑋) → (𝑛 · 𝑠) = (𝑛 · (𝑥 − 𝑋)))
465	464	fveq2d 6910	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑥 − 𝑋) → (cos‘(𝑛 · 𝑠)) = (cos‘(𝑛 · (𝑥 − 𝑋))))
466	465	sumeq2sdv 15739	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑥 − 𝑋) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠)) = Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))
467	466	oveq2d 7447	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑥 − 𝑋) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))))
468	467	oveq1d 7446	. . . . . . . . . . 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 11691	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥 − 𝑋) ∈ ℝ)
472		halfre 12480	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ ℝ
473	472	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (1 / 2) ∈ ℝ)
474		fzfid 14014	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (1...𝑁) ∈ Fin)
475	390	an32s 652	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
476	474, 475	fsumrecl 15770	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
477	473, 476	readdcld 11290	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
478	44	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → π ∈ ℝ)
479	48	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → π ≠ 0)
480	477, 478, 479	redivcld 12095	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π) ∈ ℝ)
481	463, 469, 471, 480	fvmptd 7023	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π))
482	481, 480	eqeltrd 2841	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ)
483	119, 482	remulcld 11291	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ ℝ)
484	177	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ V)
485		eqidd 2738	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
486		eqidd 2738	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
487	484, 482, 119, 485, 486	offval2 7717	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))))
488	482	recnd 11289	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℂ)
489	488, 120	mulcomd 11282	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
490	489	mpteq2dva 5242	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))))
491	487, 490	eqtr2d 2778	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) = ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
492		eqid 2737	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))
493		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))
494	194	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ℂ ⊆ ℂ)
495		cncfss 24925	. . . . . . . . . . . . . 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 11691	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 − 𝑋) ∈ ℝ)
500		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) = (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋))
501	499, 500	fmptd 7134	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)):ℝ⟶ℝ)
502	189	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ℝ ⊆ ℂ)
503	502, 494	idcncfg 45888	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝑥) ∈ (ℝ–cn→ℂ))
504	502, 365, 494	constcncfg 45887	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝑋) ∈ (ℝ–cn→ℂ))
505	503, 504	subcncf 25479	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℂ))
506		cncfcdm 24924	. . . . . . . . . . . . . . . 16 ⊢ ((ℝ ⊆ ℂ ∧ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℂ)) → ((𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)):ℝ⟶ℝ))
507	189, 505, 506	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)):ℝ⟶ℝ))
508	501, 507	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℝ))
509	459	dirkercncf 46122	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁) ∈ (ℝ–cn→ℝ))
510	7, 509	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷‘𝑁) ∈ (ℝ–cn→ℝ))
511	508, 510	cncfcompt 45898	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (ℝ–cn→ℝ))
512	496, 511	sseldd 3984	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (ℝ–cn→ℂ))
513	44	renegcli 11570	. . . . . . . . . . . . . 14 ⊢ -π ∈ ℝ
514		iccssre 13469	. . . . . . . . . . . . . 14 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
515	513, 44, 514	mp2an 692	. . . . . . . . . . . . 13 ⊢ (-π[,]π) ⊆ ℝ
516	515	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (-π[,]π) ⊆ ℝ)
517	459	dirkerf 46112	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁):ℝ⟶ℝ)
518	7, 517	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷‘𝑁):ℝ⟶ℝ)
519	518	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → (𝐷‘𝑁):ℝ⟶ℝ)
520	516	sselda 3983	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
521	58	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
522	520, 521	resubcld 11691	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → (𝑥 − 𝑋) ∈ ℝ)
523	519, 522	ffvelcdmd 7105	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ)
524	523	recnd 11289	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℂ)
525	493, 512, 516, 494, 524	cncfmptssg 45886	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ ((-π[,]π)–cn→ℂ))
526	132	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ⊆ (-π[,]π))
527	492, 525, 526, 494, 488	cncfmptssg 45886	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (𝐶–cn→ℂ))
528		cnmbf 25694	. . . . . . . . . 10 ⊢ ((𝐶 ∈ dom vol ∧ (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (𝐶–cn→ℂ)) → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ MblFn)
529	176, 527, 528	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ MblFn)
530	513	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → -π ∈ ℝ)
531		0red 11264	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ℝ)
532		negpilt0 45292	. . . . . . . . . . . . . . . 16 ⊢ -π < 0
533	532	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -π < 0)
534	47	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 < π)
535	530, 531, 101, 533, 534	lttrd 11422	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -π < π)
536	530, 101, 535	ltled 11409	. . . . . . . . . . . . 13 ⊢ (𝜑 → -π ≤ π)
537	493, 512, 516, 502, 523	cncfmptssg 45886	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ ((-π[,]π)–cn→ℝ))
538	530, 101, 536, 537	evthiccabs 45509	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ∧ ∃𝑧 ∈ (-π[,]π)∀𝑤 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑧)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑤))))
539	538	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)))
540		eqidd 2738	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
541	420	fveq2d 6910	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
542	541	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (-π[,]π)) ∧ 𝑥 = 𝑦) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
543		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → 𝑦 ∈ (-π[,]π))
544	518	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (𝐷‘𝑁):ℝ⟶ℝ)
545	515, 543	sselid 3981	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → 𝑦 ∈ ℝ)
546	58	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
547	545, 546	resubcld 11691	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (𝑦 − 𝑋) ∈ ℝ)
548	544, 547	ffvelcdmd 7105	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑦 − 𝑋)) ∈ ℝ)
549	540, 542, 543, 548	fvmptd 7023	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
550	549	fveq2d 6910	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
551	550	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
552		eqidd 2738	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
553		oveq1 7438	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑐 → (𝑥 − 𝑋) = (𝑐 − 𝑋))
554	553	fveq2d 6910	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑐 → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑐 − 𝑋)))
555	554	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑥 = 𝑐) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑐 − 𝑋)))
556		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → 𝑐 ∈ (-π[,]π))
557	518	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (𝐷‘𝑁):ℝ⟶ℝ)
558	515, 556	sselid 3981	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → 𝑐 ∈ ℝ)
559	58	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
560	558, 559	resubcld 11691	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (𝑐 − 𝑋) ∈ ℝ)
561	557, 560	ffvelcdmd 7105	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑐 − 𝑋)) ∈ ℝ)
562	552, 555, 556, 561	fvmptd 7023	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐) = ((𝐷‘𝑁)‘(𝑐 − 𝑋)))
563	562	fveq2d 6910	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
564	563	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
565	551, 564	breq12d 5156	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → ((abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ↔ (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
566	565	ralbidva 3176	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ↔ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
567	566	rexbidva 3177	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ↔ ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
568	539, 567	mpbid 232	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
569	561	recnd 11289	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑐 − 𝑋)) ∈ ℂ)
570	569	abscld 15475	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∈ ℝ)
571	570	3adant3 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∈ ℝ)
572		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝜑
573		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 𝑐 ∈ (-π[,]π)
574		nfra1 3284	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))
575	572, 573, 574	nf3an 1901	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
576		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
577	482	ralrimiva 3146	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ)
578		dmmptg 6262	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ 𝐶 ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ → dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = 𝐶)
579	577, 578	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = 𝐶)
580	579	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = 𝐶)
581	576, 580	eleqtrd 2843	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → 𝑦 ∈ 𝐶)
582	581	3ad2antl1 1186	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → 𝑦 ∈ 𝐶)
583		eqidd 2738	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
584	541	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
585		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
586	518	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝐷‘𝑁):ℝ⟶ℝ)
587	136, 585	sselid 3981	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
588	58	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑋 ∈ ℝ)
589	587, 588	resubcld 11691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝑦 − 𝑋) ∈ ℝ)
590	586, 589	ffvelcdmd 7105	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑦 − 𝑋)) ∈ ℝ)
591	583, 584, 585, 590	fvmptd 7023	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
592	591	fveq2d 6910	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
593	592	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
594		simplr 769	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
595	132	sseli 3979	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝐶 → 𝑦 ∈ (-π[,]π))
596	595	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ (-π[,]π))
597		rspa 3248	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
598	594, 596, 597	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
599	593, 598	eqbrtrd 5165	. . . . . . . . . . . . . . . 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 3257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
604		breq2 5147	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) → ((abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
605	604	ralbidv 3178	. . . . . . . . . . . . 13 ⊢ (𝑏 = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
606	605	rspcev 3622	. . . . . . . . . . . 12 ⊢ (((abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏)
607	571, 603, 606	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏)
608	607	rexlimdv3a 3159	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏))
609	568, 608	mpd 15	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏)
610		bddmulibl 25874	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
611	529, 140, 609, 610	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
612	491, 611	eqeltrd 2841	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) ∈ 𝐿¹)
613	142, 483, 612	itgmulc2 25869	. . . . . 6 ⊢ (𝜑 → (π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) = ∫𝐶(π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) d𝑥)
614	142	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → π ∈ ℂ)
615	120, 488, 614	mul13d 45291	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) = (π · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))))
616	489	oveq2d 7447	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (π · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))) = (π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))))
617	615, 616	eqtrd 2777	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) = (π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))))
618	617	itgeq2dv 25817	. . . . . 6 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) d𝑥 = ∫𝐶(π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) d𝑥)
619	613, 618	eqtr4d 2780	. . . . 5 ⊢ (𝜑 → (π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) = ∫𝐶((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) d𝑥)
620	148	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (1 / 2) ∈ ℂ)
621	620, 120	mulcomd 11282	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (1 / 2)))
622	396	an32s 652	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℂ)
623	474, 120, 622	fsummulc2 15820	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) = Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))))
624	623	eqcomd 2743	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) = ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))))
625	621, 624	oveq12d 7449	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) = (((𝐹‘𝑥) · (1 / 2)) + ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))))
626	474, 622	fsumcl 15769	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℂ)
627	120, 620, 626	adddid 11285	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))) = (((𝐹‘𝑥) · (1 / 2)) + ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))))
628	481	oveq1d 7446	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π) = ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π) · π))
629	620, 626	addcld 11280	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℂ)
630	629, 614, 479	divcan1d 12044	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π) · π) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))))
631	628, 630	eqtr2d 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) = (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π))
632	631	oveq2d 7447	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))) = ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)))
633	625, 627, 632	3eqtr2rd 2784	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) = (((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))))
634	633	itgeq2dv 25817	. . . . 5 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) d𝑥 = ∫𝐶(((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) d𝑥)
635		remulcl 11240	. . . . . . 7 ⊢ (((1 / 2) ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ) → ((1 / 2) · (𝐹‘𝑥)) ∈ ℝ)
636	472, 119, 635	sylancr 587	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) · (𝐹‘𝑥)) ∈ ℝ)
637	148, 119, 140	iblmulc2 25866	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((1 / 2) · (𝐹‘𝑥))) ∈ 𝐿¹)
638	391	an32s 652	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
639	474, 638	fsumrecl 15770	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
640	453	simpld 494	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) ∈ 𝐿¹)
641	636, 637, 639, 640	itgadd 25860	. . . . 5 ⊢ (𝜑 → ∫𝐶(((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) d𝑥 = (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥))
642	619, 634, 641	3eqtrrd 2782	. . . 4 ⊢ (𝜑 → (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥) = (π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥))
643	642	oveq1d 7446	. . 3 ⊢ (𝜑 → ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥) / π) = ((π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) / π))
644	636, 637	itgcl 25819	. . . 4 ⊢ (𝜑 → ∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 ∈ ℂ)
645	639, 640	itgcl 25819	. . . 4 ⊢ (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 ∈ ℂ)
646	644, 645, 142, 102	divdird 12081	. . 3 ⊢ (𝜑 → ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥) / π) = ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π)))
647	483, 612	itgcl 25819	. . . 4 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥 ∈ ℂ)
648	647, 142, 102	divcan3d 12048	. . 3 ⊢ (𝜑 → ((π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) / π) = ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥)
649	643, 646, 648	3eqtr3d 2785	. 2 ⊢ (𝜑 → ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π)) = ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥)
650	90, 458, 649	3eqtrd 2781	1 ⊢ (𝜑 → (𝑆‘𝑁) = ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 Vcvv 3480 ⊆ wss 3951 ifcif 4525 class class class wbr 5143 ↦ cmpt 5225 dom cdm 5685 ↾ cres 5687 ⟶wf 6557 ‘cfv 6561 (class class class)co 7431 ∘_f cof 7695 ℂcc 11153 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 · cmul 11160 < clt 11295 ≤ cle 11296 − cmin 11492 -cneg 11493 / cdiv 11920 ℕcn 12266 2c2 12321 ℕ₀cn0 12526 (,)cioo 13387 [,]cicc 13390 ...cfz 13547 mod cmo 13909 abscabs 15273 Σcsu 15722 sincsin 16099 cosccos 16100 πcpi 16102 –cn→ccncf 24902 volcvol 25498 MblFncmbf 25649 𝐿¹cibl 25652 ∫citg 25653

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 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681 ax-cc 10475 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233 ax-addf 11234

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-iin 4994 df-disj 5111 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-ofr 7698 df-om 7888 df-1st 8014 df-2nd 8015 df-supp 8186 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-oadd 8510 df-omul 8511 df-er 8745 df-map 8868 df-pm 8869 df-ixp 8938 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-fsupp 9402 df-fi 9451 df-sup 9482 df-inf 9483 df-oi 9550 df-dju 9941 df-card 9979 df-acn 9982 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-4 12331 df-5 12332 df-6 12333 df-7 12334 df-8 12335 df-9 12336 df-n0 12527 df-z 12614 df-dec 12734 df-uz 12879 df-q 12991 df-rp 13035 df-xneg 13154 df-xadd 13155 df-xmul 13156 df-ioo 13391 df-ioc 13392 df-ico 13393 df-icc 13394 df-fz 13548 df-fzo 13695 df-fl 13832 df-mod 13910 df-seq 14043 df-exp 14103 df-fac 14313 df-bc 14342 df-hash 14370 df-shft 15106 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-limsup 15507 df-clim 15524 df-rlim 15525 df-sum 15723 df-ef 16103 df-sin 16105 df-cos 16106 df-pi 16108 df-struct 17184 df-sets 17201 df-slot 17219 df-ndx 17231 df-base 17248 df-ress 17275 df-plusg 17310 df-mulr 17311 df-starv 17312 df-sca 17313 df-vsca 17314 df-ip 17315 df-tset 17316 df-ple 17317 df-ds 17319 df-unif 17320 df-hom 17321 df-cco 17322 df-rest 17467 df-topn 17468 df-0g 17486 df-gsum 17487 df-topgen 17488 df-pt 17489 df-prds 17492 df-xrs 17547 df-qtop 17552 df-imas 17553 df-xps 17555 df-mre 17629 df-mrc 17630 df-acs 17632 df-mgm 18653 df-sgrp 18732 df-mnd 18748 df-submnd 18797 df-mulg 19086 df-cntz 19335 df-cmn 19800 df-psmet 21356 df-xmet 21357 df-met 21358 df-bl 21359 df-mopn 21360 df-fbas 21361 df-fg 21362 df-cnfld 21365 df-top 22900 df-topon 22917 df-topsp 22939 df-bases 22953 df-cld 23027 df-ntr 23028 df-cls 23029 df-nei 23106 df-lp 23144 df-perf 23145 df-cn 23235 df-cnp 23236 df-t1 23322 df-haus 23323 df-cmp 23395 df-tx 23570 df-hmeo 23763 df-fil 23854 df-fm 23946 df-flim 23947 df-flf 23948 df-xms 24330 df-ms 24331 df-tms 24332 df-cncf 24904 df-ovol 25499 df-vol 25500 df-mbf 25654 df-itg1 25655 df-itg2 25656 df-ibl 25657 df-itg 25658 df-0p 25705 df-limc 25901 df-dv 25902

This theorem is referenced by: fourierdlem111 46232

W3C validator