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 46170

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 7357	. . . . . 6 ⊢ (𝑚 = 𝑁 → (1...𝑚) = (1...𝑁))
4	3	sumeq1d 15607	. . . . 5 ⊢ (𝑚 = 𝑁 → Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
5	4	oveq2d 7365	. . . 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 12399	. . . . . . 7 ⊢ 0 ∈ ℕ₀
10	9	a1i 11	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℕ₀)
11	9	elexi 3459	. . . . . . 7 ⊢ 0 ∈ V
12		eleq1 2816	. . . . . . . . 9 ⊢ (𝑛 = 0 → (𝑛 ∈ ℕ₀ ↔ 0 ∈ ℕ₀))
13	12	anbi2d 630	. . . . . . . 8 ⊢ (𝑛 = 0 → ((𝜑 ∧ 𝑛 ∈ ℕ₀) ↔ (𝜑 ∧ 0 ∈ ℕ₀)))
14		fveq2 6822	. . . . . . . . 9 ⊢ (𝑛 = 0 → (𝐴‘𝑛) = (𝐴‘0))
15	14	eleq1d 2813	. . . . . . . 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 46110	. . . . . . . . 9 ⊢ (𝜑 → ((𝑛 ∈ ℕ₀ → (𝐴‘𝑛) ∈ ℝ) ∧ (𝑛 ∈ ℕ → (𝐵‘𝑛) ∈ ℝ)))
23	22	simpld 494	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ ℕ₀ → (𝐴‘𝑛) ∈ ℝ))
24	23	imp 406	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝐴‘𝑛) ∈ ℝ)
25	11, 16, 24	vtocl 3513	. . . . . 6 ⊢ ((𝜑 ∧ 0 ∈ ℕ₀) → (𝐴‘0) ∈ ℝ)
26	8, 10, 25	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝐴‘0) ∈ ℝ)
27	26	rehalfcld 12371	. . . 4 ⊢ (𝜑 → ((𝐴‘0) / 2) ∈ ℝ)
28		fzfid 13880	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
29		eleq1 2816	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ ℕ₀ ↔ 𝑛 ∈ ℕ₀))
30	29	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → ((𝜑 ∧ 𝑘 ∈ ℕ₀) ↔ (𝜑 ∧ 𝑛 ∈ ℕ₀)))
31		simpl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → 𝑘 = 𝑛)
32	31	oveq1d 7364	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → (𝑘 · 𝑥) = (𝑛 · 𝑥))
33	32	fveq2d 6826	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑘 · 𝑥)) = (cos‘(𝑛 · 𝑥)))
34	33	oveq2d 7365	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))
35	34	itgeq2dv 25681	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥)
36	35	eleq1d 2813	. . . . . . . . . . . . 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 46104	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝐴‘𝑘) ∈ ℝ ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹) ∧ ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ))
42	41	simprd 495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ)
43	37, 42	chvarvv 1989	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
44		pire 26364	. . . . . . . . . . . 12 ⊢ π ∈ ℝ
45	44	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → π ∈ ℝ)
46		0re 11117	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
47		pipos 26366	. . . . . . . . . . . . 13 ⊢ 0 < π
48	46, 47	gtneii 11228	. . . . . . . . . . . 12 ⊢ π ≠ 0
49	48	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → π ≠ 0)
50	43, 45, 49	redivcld 11952	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
51	50, 20	fmptd 7048	. . . . . . . . 9 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℝ)
52	51	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐴:ℕ₀⟶ℝ)
53		elfznn 13456	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
54	53	nnnn0d 12445	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ₀)
55	54	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ₀)
56	52, 55	ffvelcdmd 7019	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐴‘𝑛) ∈ ℝ)
57	55	nn0red 12446	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℝ)
58		fourierdlem83.x	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℝ)
59	58	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℝ)
60	57, 59	remulcld 11145	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 · 𝑋) ∈ ℝ)
61	60	recoscld 16053	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℝ)
62	56, 61	remulcld 11145	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
63		eleq1 2816	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ ℕ ↔ 𝑛 ∈ ℕ))
64	63	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → ((𝜑 ∧ 𝑘 ∈ ℕ) ↔ (𝜑 ∧ 𝑛 ∈ ℕ)))
65		oveq1 7356	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → (𝑘 · 𝑥) = (𝑛 · 𝑥))
66	65	fveq2d 6826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → (sin‘(𝑘 · 𝑥)) = (sin‘(𝑛 · 𝑥)))
67	66	oveq2d 7365	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑛 → ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
68	67	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
69	68	itgeq2dv 25681	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥)
70	69	eleq1d 2813	. . . . . . . . . . . . 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 46109	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐵‘𝑘) ∈ ℝ ∧ (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥)))) ∈ 𝐿¹) ∧ ∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ))
76	75	simprd 495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ)
77	71, 76	chvarvv 1989	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
78	44	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → π ∈ ℝ)
79	48	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → π ≠ 0)
80	77, 78, 79	redivcld 11952	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
81	80, 21	fmptd 7048	. . . . . . . . 9 ⊢ (𝜑 → 𝐵:ℕ⟶ℝ)
82	81	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐵:ℕ⟶ℝ)
83	53	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ)
84	82, 83	ffvelcdmd 7019	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐵‘𝑛) ∈ ℝ)
85	60	resincld 16052	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
86	84, 85	remulcld 11145	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
87	62, 86	readdcld 11144	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
88	28, 87	fsumrecl 15641	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
89	27, 88	readdcld 11144	. . 3 ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) ∈ ℝ)
90	2, 6, 7, 89	fvmptd 6937	. 2 ⊢ (𝜑 → (𝑆‘𝑁) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
91	20	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐴 = (𝑛 ∈ ℕ₀ ↦ (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
92		oveq1 7356	. . . . . . . . . . . . 13 ⊢ (𝑛 = 0 → (𝑛 · 𝑥) = (0 · 𝑥))
93	92	fveq2d 6826	. . . . . . . . . . . 12 ⊢ (𝑛 = 0 → (cos‘(𝑛 · 𝑥)) = (cos‘(0 · 𝑥)))
94	93	oveq2d 7365	. . . . . . . . . . 11 ⊢ (𝑛 = 0 → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(0 · 𝑥))))
95	94	adantr 480	. . . . . . . . . 10 ⊢ ((𝑛 = 0 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(0 · 𝑥))))
96	95	itgeq2dv 25681	. . . . . . . . 9 ⊢ (𝑛 = 0 → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥)
97	96	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 0) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥)
98	97	oveq1d 7364	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 = 0) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) = (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
99	17, 18, 19, 20, 10	fourierdlem16 46104	. . . . . . . . 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 11952	. . . . . . 7 ⊢ (𝜑 → (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) ∈ ℝ)
104	91, 98, 10, 103	fvmptd 6937	. . . . . 6 ⊢ (𝜑 → (𝐴‘0) = (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
105		ioosscn 13311	. . . . . . . . . . . . . . 15 ⊢ (-π(,)π) ⊆ ℂ
106		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐶)
107	106, 18	eleqtrdi 2838	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ (-π(,)π))
108	105, 107	sselid 3933	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ℂ)
109	108	mul02d 11314	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐶 → (0 · 𝑥) = 0)
110	109	fveq2d 6826	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐶 → (cos‘(0 · 𝑥)) = (cos‘0))
111		cos0 16059	. . . . . . . . . . . 12 ⊢ (cos‘0) = 1
112	110, 111	eqtrdi 2780	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐶 → (cos‘(0 · 𝑥)) = 1)
113	112	oveq2d 7365	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐶 → ((𝐹‘𝑥) · (cos‘(0 · 𝑥))) = ((𝐹‘𝑥) · 1))
114	113	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(0 · 𝑥))) = ((𝐹‘𝑥) · 1))
115	17	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐹:ℝ⟶ℝ)
116		ioossre 13310	. . . . . . . . . . . . . 14 ⊢ (-π(,)π) ⊆ ℝ
117	116, 107	sselid 3933	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ℝ)
118	117	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
119	115, 118	ffvelcdmd 7019	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
120	119	recnd 11143	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
121	120	mulridd 11132	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · 1) = (𝐹‘𝑥))
122	114, 121	eqtrd 2764	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(0 · 𝑥))) = (𝐹‘𝑥))
123	122	itgeq2dv 25681	. . . . . . 7 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 = ∫𝐶(𝐹‘𝑥) d𝑥)
124	123	oveq1d 7364	. . . . . 6 ⊢ (𝜑 → (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) = (∫𝐶(𝐹‘𝑥) d𝑥 / π))
125	104, 124	eqtrd 2764	. . . . 5 ⊢ (𝜑 → (𝐴‘0) = (∫𝐶(𝐹‘𝑥) d𝑥 / π))
126	125	oveq1d 7364	. . . 4 ⊢ (𝜑 → ((𝐴‘0) / 2) = ((∫𝐶(𝐹‘𝑥) d𝑥 / π) / 2))
127	17	feqmptd 6891	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)))
128	127	reseq1d 5929	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ 𝐶))
129	44	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐶 → π ∈ ℝ)
130	129	renegcld 11547	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐶 → -π ∈ ℝ)
131		ioossicc 13336	. . . . . . . . . . . . 13 ⊢ (-π(,)π) ⊆ (-π[,]π)
132	18, 131	eqsstri 3982	. . . . . . . . . . . 12 ⊢ 𝐶 ⊆ (-π[,]π)
133	132	sseli 3931	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ (-π[,]π))
134		eliccre 45486	. . . . . . . . . . 11 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ ∧ 𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
135	130, 129, 133, 134	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ℝ)
136	135	ssriv 3939	. . . . . . . . 9 ⊢ 𝐶 ⊆ ℝ
137		resmpt 5988	. . . . . . . . 9 ⊢ (𝐶 ⊆ ℝ → ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
138	136, 137	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
139	128, 138	eqtr2d 2765	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝐹 ↾ 𝐶))
140	139, 19	eqeltrd 2828	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
141	119, 140	itgcl 25683	. . . . 5 ⊢ (𝜑 → ∫𝐶(𝐹‘𝑥) d𝑥 ∈ ℂ)
142	101	recnd 11143	. . . . 5 ⊢ (𝜑 → π ∈ ℂ)
143		2cnd 12206	. . . . 5 ⊢ (𝜑 → 2 ∈ ℂ)
144		2ne0 12232	. . . . . 6 ⊢ 2 ≠ 0
145	144	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ≠ 0)
146	141, 142, 143, 102, 145	divdiv32d 11925	. . . 4 ⊢ (𝜑 → ((∫𝐶(𝐹‘𝑥) d𝑥 / π) / 2) = ((∫𝐶(𝐹‘𝑥) d𝑥 / 2) / π))
147	141, 143, 145	divrecd 11903	. . . . . 6 ⊢ (𝜑 → (∫𝐶(𝐹‘𝑥) d𝑥 / 2) = (∫𝐶(𝐹‘𝑥) d𝑥 · (1 / 2)))
148	143, 145	reccld 11893	. . . . . . 7 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
149	141, 148	mulcomd 11136	. . . . . 6 ⊢ (𝜑 → (∫𝐶(𝐹‘𝑥) d𝑥 · (1 / 2)) = ((1 / 2) · ∫𝐶(𝐹‘𝑥) d𝑥))
150	148, 119, 140	itgmulc2 25733	. . . . . 6 ⊢ (𝜑 → ((1 / 2) · ∫𝐶(𝐹‘𝑥) d𝑥) = ∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥)
151	147, 149, 150	3eqtrd 2768	. . . . 5 ⊢ (𝜑 → (∫𝐶(𝐹‘𝑥) d𝑥 / 2) = ∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥)
152	151	oveq1d 7364	. . . 4 ⊢ (𝜑 → ((∫𝐶(𝐹‘𝑥) d𝑥 / 2) / π) = (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π))
153	126, 146, 152	3eqtrd 2768	. . 3 ⊢ (𝜑 → ((𝐴‘0) / 2) = (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π))
154	55, 50	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
155	20	fvmpt2 6941	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ₀ ∧ (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐴‘𝑛) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
156	55, 154, 155	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐴‘𝑛) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
157	156	oveq1d 7364	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))))
158	154	recnd 11143	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
159	61	recnd 11143	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℂ)
160	158, 159	mulcomd 11136	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
161	55, 43	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
162	161	recnd 11143	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
163	142	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → π ∈ ℂ)
164	48	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → π ≠ 0)
165	159, 162, 163, 164	divassd 11935	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
166	17	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → 𝐹:ℝ⟶ℝ)
167	117	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
168	166, 167	ffvelcdmd 7019	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
169		nn0re 12393	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℝ)
170	169	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
171	170, 167	remulcld 11145	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℝ)
172	171	recoscld 16053	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
173	168, 172	remulcld 11145	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
174	54, 173	sylanl2 681	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
175		ioombl 25464	. . . . . . . . . . . . . . . . . . 19 ⊢ (-π(,)π) ∈ dom vol
176	18, 175	eqeltri 2824	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐶 ∈ dom vol
177	176	elexi 3459	. . . . . . . . . . . . . . . . 17 ⊢ 𝐶 ∈ V
178	177	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝐶 ∈ V)
179		eqidd 2730	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))))
180		eqidd 2730	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
181	178, 172, 168, 179, 180	offval2 7633	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
182	172	recnd 11143	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℂ)
183	120	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
184	182, 183	mulcomd 11136	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))
185	184	mpteq2dva 5185	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))))
186	181, 185	eqtr2d 2765	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
187		coscn 26353	. . . . . . . . . . . . . . . . . 18 ⊢ cos ∈ (ℂ–cn→ℂ)
188	187	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → cos ∈ (ℂ–cn→ℂ))
189		ax-resscn 11066	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℝ ⊆ ℂ
190	136, 189	sstri 3945	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐶 ⊆ ℂ
191	190	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝐶 ⊆ ℂ)
192	169	recnd 11143	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℂ)
193	192	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝑛 ∈ ℂ)
194		ssid 3958	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℂ ⊆ ℂ
195	194	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ℂ ⊆ ℂ)
196	191, 193, 195	constcncfg 45853	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ 𝑛) ∈ (𝐶–cn→ℂ))
197	191, 195	idcncfg 45854	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ 𝑥) ∈ (𝐶–cn→ℂ))
198	196, 197	mulcncf 25344	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶–cn→ℂ))
199	188, 198	cncfmpt1f 24805	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ))
200		cnmbf 25558	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ dom vol ∧ (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
201	176, 199, 200	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
202	140	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
203		1re 11115	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
204		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))))
205	169	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
206	117	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
207	205, 206	remulcld 11145	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℝ)
208	207	recoscld 16053	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
209	208	ralrimiva 3121	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ₀ → ∀𝑥 ∈ 𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
210	209	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → ∀𝑥 ∈ 𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
211		dmmptg 6191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 ∈ 𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ → dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
212	210, 211	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
213	204, 212	eleqtrd 2830	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦 ∈ 𝐶)
214		eqidd 2730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))))
215		oveq2 7357	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑛 · 𝑥) = (𝑛 · 𝑦))
216	215	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
217	216	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
218		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
219	169	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → 𝑛 ∈ ℝ)
220	136, 218	sselid 3933	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
221	219, 220	remulcld 11145	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (𝑛 · 𝑦) ∈ ℝ)
222	221	recoscld 16053	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (cos‘(𝑛 · 𝑦)) ∈ ℝ)
223	214, 217, 218, 222	fvmptd 6937	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦) = (cos‘(𝑛 · 𝑦)))
224	223	fveq2d 6826	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(cos‘(𝑛 · 𝑦))))
225		abscosbd 45261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 · 𝑦) ∈ ℝ → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
226	221, 225	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
227	224, 226	eqbrtrd 5114	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
228	213, 227	syldan 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
229	228	ralrimiva 3121	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
230		breq2 5096	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 1 → ((abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
231	230	ralbidv 3152	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
232	231	rspcev 3577	. . . . . . . . . . . . . . . . 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 25738	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
236	201, 202, 234, 235	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
237	186, 236	eqeltrd 2828	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
238	55, 237	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
239	159, 174, 238	itgmulc2 25733	. . . . . . . . . . 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 11325	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))))
244	240, 242	mulcomd 11136	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥))) = ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))
245	244	oveq2d 7365	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
246	243, 245	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
247	246	itgeq2dv 25681	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
248	239, 247	eqtrd 2764	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
249	248	oveq1d 7364	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
250	165, 249	eqtr3d 2766	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
251	157, 160, 250	3eqtrd 2768	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
252	83, 80	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
253	21	fvmpt2 6941	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐵‘𝑛) = (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
254	83, 252, 253	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐵‘𝑛) = (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
255	254	oveq1d 7364	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))))
256	252	recnd 11143	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
257	85	recnd 11143	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℂ)
258	256, 257	mulcomd 11136	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
259	83, 77	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
260	259	recnd 11143	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
261	257, 260, 163, 164	divassd 11935	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
262	119	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
263		nnre 12135	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
264	263	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
265	117	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
266	264, 265	remulcld 11145	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℝ)
267	266	resincld 16052	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
268	267	adantll 714	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
269	262, 268	remulcld 11145	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
270	53, 269	sylanl2 681	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
271	177	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 ∈ V)
272		eqidd 2730	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))))
273		eqidd 2730	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
274	271, 268, 262, 272, 273	offval2 7633	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
275	268	recnd 11143	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℂ)
276	120	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
277	275, 276	mulcomd 11136	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
278	277	mpteq2dva 5185	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))))
279	274, 278	eqtr2d 2765	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
280		sincn 26352	. . . . . . . . . . . . . . . . . 18 ⊢ sin ∈ (ℂ–cn→ℂ)
281	280	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sin ∈ (ℂ–cn→ℂ))
282	190	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → 𝐶 ⊆ ℂ)
283	263	recnd 11143	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
284	194	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → ℂ ⊆ ℂ)
285	282, 283, 284	constcncfg 45853	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (𝑥 ∈ 𝐶 ↦ 𝑛) ∈ (𝐶–cn→ℂ))
286	282, 284	idcncfg 45854	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (𝑥 ∈ 𝐶 ↦ 𝑥) ∈ (𝐶–cn→ℂ))
287	285, 286	mulcncf 25344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → (𝑥 ∈ 𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶–cn→ℂ))
288	287	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶–cn→ℂ))
289	281, 288	cncfmpt1f 24805	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ))
290		cnmbf 25558	. . . . . . . . . . . . . . . 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 3121	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → ∀𝑥 ∈ 𝐶 (sin‘(𝑛 · 𝑥)) ∈ ℝ)
295		dmmptg 6191	. . . . . . . . . . . . . . . . . . . . . 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 2830	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦 ∈ 𝐶)
299		eqidd 2730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))))
300	215	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
301	300	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
302		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
303	263	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → 𝑛 ∈ ℝ)
304	136, 302	sselid 3933	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
305	303, 304	remulcld 11145	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (𝑛 · 𝑦) ∈ ℝ)
306	305	resincld 16052	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (sin‘(𝑛 · 𝑦)) ∈ ℝ)
307	299, 301, 302, 306	fvmptd 6937	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦) = (sin‘(𝑛 · 𝑦)))
308	307	fveq2d 6826	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(sin‘(𝑛 · 𝑦))))
309		abssinbd 45277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 · 𝑦) ∈ ℝ → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
310	305, 309	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
311	308, 310	eqbrtrd 5114	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
312	298, 311	syldan 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
313	312	ralrimiva 3121	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
314		breq2 5096	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 1 → ((abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
315	314	ralbidv 3152	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
316	315	rspcev 3577	. . . . . . . . . . . . . . . . 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 25738	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
320	291, 292, 318, 319	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
321	279, 320	eqeltrd 2828	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
322	83, 321	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
323	257, 270, 322	itgmulc2 25733	. . . . . . . . . . 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 11325	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))))
327	324, 325	mulcomd 11136	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥))) = ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))
328	327	oveq2d 7365	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
329	326, 328	eqtrd 2764	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
330	329	itgeq2dv 25681	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
331	323, 330	eqtrd 2764	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
332	331	oveq1d 7364	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
333	261, 332	eqtr3d 2766	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
334	255, 258, 333	3eqtrd 2768	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
335	251, 334	oveq12d 7367	. . . . . 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 11145	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
340	336, 339	remulcld 11145	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) ∈ ℝ)
341	241, 242, 240	mul13d 45262	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
342	242, 241	mulcomd 11136	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))
343	342	oveq2d 7365	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))))
344	341, 343	eqtrd 2764	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))))
345	344	mpteq2dva 5185	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) = (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))))
346	159, 174, 238	iblmulc2 25730	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))) ∈ 𝐿¹)
347	345, 346	eqeltrd 2828	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) ∈ 𝐿¹)
348	340, 347	itgcl 25683	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
349	83, 267	sylan 580	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
350	85	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
351	349, 350	remulcld 11145	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
352	336, 351	remulcld 11145	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
353	241, 325, 324	mul13d 45262	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
354	325, 241	mulcomd 11136	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
355	354	oveq2d 7365	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))))
356	353, 355	eqtrd 2764	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))))
357	356	mpteq2dva 5185	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))))
358	257, 270, 322	iblmulc2 25730	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))) ∈ 𝐿¹)
359	357, 358	eqeltrd 2828	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) ∈ 𝐿¹)
360	352, 359	itgcl 25683	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
361	348, 360, 163, 164	divdird 11938	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π) + (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π)))
362	53	nncnd 12144	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
363	362	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℂ)
364	108	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℂ)
365	58	recnd 11143	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ ℂ)
366	365	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑋 ∈ ℂ)
367	363, 364, 366	subdid 11576	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · (𝑥 − 𝑋)) = ((𝑛 · 𝑥) − (𝑛 · 𝑋)))
368	367	fveq2d 6826	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) = (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))))
369	363, 364	mulcld 11135	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℂ)
370	363, 366	mulcld 11135	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑋) ∈ ℂ)
371		cossub 16078	. . . . . . . . . . . . 13 ⊢ (((𝑛 · 𝑥) ∈ ℂ ∧ (𝑛 · 𝑋) ∈ ℂ) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
372	369, 370, 371	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
373	368, 372	eqtrd 2764	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
374	373	oveq2d 7365	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) = ((𝐹‘𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
375	339	recnd 11143	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℂ)
376	351	recnd 11143	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℂ)
377	241, 375, 376	adddid 11139	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
378	374, 377	eqtrd 2764	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) = (((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
379	378	itgeq2dv 25681	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = ∫𝐶(((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥)
380	340, 347, 352, 359	itgadd 25724	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶(((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥 = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥))
381	379, 380	eqtr2d 2765	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) = ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥)
382	381	oveq1d 7364	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
383	335, 361, 382	3eqtr2d 2770	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
384	383	sumeq2dv 15609	. . . 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 11548	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑥 − 𝑋) ∈ ℝ)
389	385, 388	remulcld 11145	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · (𝑥 − 𝑋)) ∈ ℝ)
390	389	recoscld 16053	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
391	336, 390	remulcld 11145	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
392	177	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ V)
393		eqidd 2730	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))))
394		eqidd 2730	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
395	392, 390, 336, 393, 394	offval2 7633	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · (𝑥 − 𝑋))) · (𝐹‘𝑥))))
396	390	recnd 11143	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℂ)
397	396, 241	mulcomd 11136	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · (𝑥 − 𝑋))) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))))
398	397	mpteq2dva 5185	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · (𝑥 − 𝑋))) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))))
399	395, 398	eqtr2d 2765	. . . . . . 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 45853	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ 𝑋) ∈ (𝐶–cn→ℂ))
407	402, 406	subcncf 25343	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝑥 − 𝑋)) ∈ (𝐶–cn→ℂ))
408	401, 407	mulcncf 25344	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝑛 · (𝑥 − 𝑋))) ∈ (𝐶–cn→ℂ))
409	400, 408	cncfmpt1f 24805	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ (𝐶–cn→ℂ))
410		cnmbf 25558	. . . . . . . . 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 3121	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∀𝑥 ∈ 𝐶 (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
415		dmmptg 6191	. . . . . . . . . . . . . 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 2830	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))) → 𝑦 ∈ 𝐶)
419		eqidd 2730	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))))
420		oveq1 7356	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝑥 − 𝑋) = (𝑦 − 𝑋))
421	420	oveq2d 7365	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑛 · (𝑥 − 𝑋)) = (𝑛 · (𝑦 − 𝑋)))
422	421	fveq2d 6826	. . . . . . . . . . . . . . 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 11548	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (𝑦 − 𝑋) ∈ ℝ)
429	425, 428	remulcld 11145	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (𝑛 · (𝑦 − 𝑋)) ∈ ℝ)
430	429	recoscld 16053	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (cos‘(𝑛 · (𝑦 − 𝑋))) ∈ ℝ)
431	419, 423, 424, 430	fvmptd 6937	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦) = (cos‘(𝑛 · (𝑦 − 𝑋))))
432	431	fveq2d 6826	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) = (abs‘(cos‘(𝑛 · (𝑦 − 𝑋)))))
433		abscosbd 45261	. . . . . . . . . . . . 13 ⊢ ((𝑛 · (𝑦 − 𝑋)) ∈ ℝ → (abs‘(cos‘(𝑛 · (𝑦 − 𝑋)))) ≤ 1)
434	429, 433	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (abs‘(cos‘(𝑛 · (𝑦 − 𝑋)))) ≤ 1)
435	432, 434	eqbrtrd 5114	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1)
436	418, 435	syldan 591	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1)
437	436	ralrimiva 3121	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1)
438		breq2 5096	. . . . . . . . . . 11 ⊢ (𝑏 = 1 → ((abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1))
439	438	ralbidv 3152	. . . . . . . . . 10 ⊢ (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1))
440	439	rspcev 3577	. . . . . . . . 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 25738	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
443	411, 412, 441, 442	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
444	399, 443	eqeltrd 2828	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) ∈ 𝐿¹)
445	391, 444	itgcl 25683	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 ∈ ℂ)
446	28, 142, 445, 102	fsumdivc 15693	. . . 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 25726	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) ∈ 𝐿¹ ∧ ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥))
454	453	simprd 495	. . . . . 6 ⊢ (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥)
455	454	eqcomd 2735	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥)
456	455	oveq1d 7364	. . . 4 ⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
457	384, 446, 456	3eqtr2d 2770	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
458	153, 457	oveq12d 7367	. 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 2729	. . . . . . . . . . 11 ⊢ (𝐷‘𝑁) = (𝐷‘𝑁)
462		eqid 2729	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π))
463	459, 460, 461, 462	dirkertrigeq 46082	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐷‘𝑁) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)))
464		oveq2 7357	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (𝑥 − 𝑋) → (𝑛 · 𝑠) = (𝑛 · (𝑥 − 𝑋)))
465	464	fveq2d 6826	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑥 − 𝑋) → (cos‘(𝑛 · 𝑠)) = (cos‘(𝑛 · (𝑥 − 𝑋))))
466	465	sumeq2sdv 15610	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑥 − 𝑋) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠)) = Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))
467	466	oveq2d 7365	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑥 − 𝑋) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))))
468	467	oveq1d 7364	. . . . . . . . . . 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 11548	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥 − 𝑋) ∈ ℝ)
472		halfre 12337	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ ℝ
473	472	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (1 / 2) ∈ ℝ)
474		fzfid 13880	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (1...𝑁) ∈ Fin)
475	390	an32s 652	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
476	474, 475	fsumrecl 15641	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
477	473, 476	readdcld 11144	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
478	44	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → π ∈ ℝ)
479	48	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → π ≠ 0)
480	477, 478, 479	redivcld 11952	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π) ∈ ℝ)
481	463, 469, 471, 480	fvmptd 6937	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π))
482	481, 480	eqeltrd 2828	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ)
483	119, 482	remulcld 11145	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ ℝ)
484	177	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ V)
485		eqidd 2730	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
486		eqidd 2730	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
487	484, 482, 119, 485, 486	offval2 7633	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))))
488	482	recnd 11143	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℂ)
489	488, 120	mulcomd 11136	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
490	489	mpteq2dva 5185	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))))
491	487, 490	eqtr2d 2765	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) = ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
492		eqid 2729	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))
493		eqid 2729	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))
494	194	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ℂ ⊆ ℂ)
495		cncfss 24790	. . . . . . . . . . . . . 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 11548	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 − 𝑋) ∈ ℝ)
500		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) = (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋))
501	499, 500	fmptd 7048	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)):ℝ⟶ℝ)
502	189	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ℝ ⊆ ℂ)
503	502, 494	idcncfg 45854	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝑥) ∈ (ℝ–cn→ℂ))
504	502, 365, 494	constcncfg 45853	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝑋) ∈ (ℝ–cn→ℂ))
505	503, 504	subcncf 25343	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℂ))
506		cncfcdm 24789	. . . . . . . . . . . . . . . 16 ⊢ ((ℝ ⊆ ℂ ∧ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℂ)) → ((𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)):ℝ⟶ℝ))
507	189, 505, 506	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)):ℝ⟶ℝ))
508	501, 507	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℝ))
509	459	dirkercncf 46088	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁) ∈ (ℝ–cn→ℝ))
510	7, 509	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷‘𝑁) ∈ (ℝ–cn→ℝ))
511	508, 510	cncfcompt 45864	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (ℝ–cn→ℝ))
512	496, 511	sseldd 3936	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (ℝ–cn→ℂ))
513	44	renegcli 11425	. . . . . . . . . . . . . 14 ⊢ -π ∈ ℝ
514		iccssre 13332	. . . . . . . . . . . . . 14 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
515	513, 44, 514	mp2an 692	. . . . . . . . . . . . 13 ⊢ (-π[,]π) ⊆ ℝ
516	515	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (-π[,]π) ⊆ ℝ)
517	459	dirkerf 46078	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁):ℝ⟶ℝ)
518	7, 517	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷‘𝑁):ℝ⟶ℝ)
519	518	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → (𝐷‘𝑁):ℝ⟶ℝ)
520	516	sselda 3935	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
521	58	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
522	520, 521	resubcld 11548	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → (𝑥 − 𝑋) ∈ ℝ)
523	519, 522	ffvelcdmd 7019	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ)
524	523	recnd 11143	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℂ)
525	493, 512, 516, 494, 524	cncfmptssg 45852	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ ((-π[,]π)–cn→ℂ))
526	132	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ⊆ (-π[,]π))
527	492, 525, 526, 494, 488	cncfmptssg 45852	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (𝐶–cn→ℂ))
528		cnmbf 25558	. . . . . . . . . 10 ⊢ ((𝐶 ∈ dom vol ∧ (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (𝐶–cn→ℂ)) → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ MblFn)
529	176, 527, 528	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ MblFn)
530	513	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → -π ∈ ℝ)
531		0red 11118	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ℝ)
532		negpilt0 45263	. . . . . . . . . . . . . . . 16 ⊢ -π < 0
533	532	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -π < 0)
534	47	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 < π)
535	530, 531, 101, 533, 534	lttrd 11277	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -π < π)
536	530, 101, 535	ltled 11264	. . . . . . . . . . . . 13 ⊢ (𝜑 → -π ≤ π)
537	493, 512, 516, 502, 523	cncfmptssg 45852	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ ((-π[,]π)–cn→ℝ))
538	530, 101, 536, 537	evthiccabs 45477	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ∧ ∃𝑧 ∈ (-π[,]π)∀𝑤 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑧)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑤))))
539	538	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)))
540		eqidd 2730	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
541	420	fveq2d 6826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
542	541	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (-π[,]π)) ∧ 𝑥 = 𝑦) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
543		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → 𝑦 ∈ (-π[,]π))
544	518	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (𝐷‘𝑁):ℝ⟶ℝ)
545	515, 543	sselid 3933	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → 𝑦 ∈ ℝ)
546	58	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
547	545, 546	resubcld 11548	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (𝑦 − 𝑋) ∈ ℝ)
548	544, 547	ffvelcdmd 7019	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑦 − 𝑋)) ∈ ℝ)
549	540, 542, 543, 548	fvmptd 6937	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
550	549	fveq2d 6826	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
551	550	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
552		eqidd 2730	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
553		oveq1 7356	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑐 → (𝑥 − 𝑋) = (𝑐 − 𝑋))
554	553	fveq2d 6826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑐 → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑐 − 𝑋)))
555	554	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑥 = 𝑐) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑐 − 𝑋)))
556		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → 𝑐 ∈ (-π[,]π))
557	518	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (𝐷‘𝑁):ℝ⟶ℝ)
558	515, 556	sselid 3933	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → 𝑐 ∈ ℝ)
559	58	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
560	558, 559	resubcld 11548	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (𝑐 − 𝑋) ∈ ℝ)
561	557, 560	ffvelcdmd 7019	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑐 − 𝑋)) ∈ ℝ)
562	552, 555, 556, 561	fvmptd 6937	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐) = ((𝐷‘𝑁)‘(𝑐 − 𝑋)))
563	562	fveq2d 6826	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
564	563	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
565	551, 564	breq12d 5105	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → ((abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ↔ (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
566	565	ralbidva 3150	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ↔ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
567	566	rexbidva 3151	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ↔ ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
568	539, 567	mpbid 232	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
569	561	recnd 11143	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑐 − 𝑋)) ∈ ℂ)
570	569	abscld 15346	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∈ ℝ)
571	570	3adant3 1132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∈ ℝ)
572		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝜑
573		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 𝑐 ∈ (-π[,]π)
574		nfra1 3253	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))
575	572, 573, 574	nf3an 1901	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
576		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
577	482	ralrimiva 3121	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ)
578		dmmptg 6191	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ 𝐶 ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ → dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = 𝐶)
579	577, 578	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = 𝐶)
580	579	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = 𝐶)
581	576, 580	eleqtrd 2830	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → 𝑦 ∈ 𝐶)
582	581	3ad2antl1 1186	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → 𝑦 ∈ 𝐶)
583		eqidd 2730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
584	541	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
585		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
586	518	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝐷‘𝑁):ℝ⟶ℝ)
587	136, 585	sselid 3933	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
588	58	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑋 ∈ ℝ)
589	587, 588	resubcld 11548	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝑦 − 𝑋) ∈ ℝ)
590	586, 589	ffvelcdmd 7019	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑦 − 𝑋)) ∈ ℝ)
591	583, 584, 585, 590	fvmptd 6937	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
592	591	fveq2d 6826	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
593	592	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
594		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
595	132	sseli 3931	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝐶 → 𝑦 ∈ (-π[,]π))
596	595	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ (-π[,]π))
597		rspa 3218	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
598	594, 596, 597	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
599	593, 598	eqbrtrd 5114	. . . . . . . . . . . . . . . 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 3227	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
604		breq2 5096	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) → ((abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
605	604	ralbidv 3152	. . . . . . . . . . . . 13 ⊢ (𝑏 = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
606	605	rspcev 3577	. . . . . . . . . . . 12 ⊢ (((abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏)
607	571, 603, 606	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏)
608	607	rexlimdv3a 3134	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏))
609	568, 608	mpd 15	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏)
610		bddmulibl 25738	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
611	529, 140, 609, 610	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
612	491, 611	eqeltrd 2828	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) ∈ 𝐿¹)
613	142, 483, 612	itgmulc2 25733	. . . . . 6 ⊢ (𝜑 → (π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) = ∫𝐶(π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) d𝑥)
614	142	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → π ∈ ℂ)
615	120, 488, 614	mul13d 45262	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) = (π · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))))
616	489	oveq2d 7365	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (π · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))) = (π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))))
617	615, 616	eqtrd 2764	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) = (π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))))
618	617	itgeq2dv 25681	. . . . . 6 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) d𝑥 = ∫𝐶(π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) d𝑥)
619	613, 618	eqtr4d 2767	. . . . 5 ⊢ (𝜑 → (π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) = ∫𝐶((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) d𝑥)
620	148	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (1 / 2) ∈ ℂ)
621	620, 120	mulcomd 11136	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (1 / 2)))
622	396	an32s 652	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℂ)
623	474, 120, 622	fsummulc2 15691	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) = Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))))
624	623	eqcomd 2735	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) = ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))))
625	621, 624	oveq12d 7367	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) = (((𝐹‘𝑥) · (1 / 2)) + ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))))
626	474, 622	fsumcl 15640	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℂ)
627	120, 620, 626	adddid 11139	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))) = (((𝐹‘𝑥) · (1 / 2)) + ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))))
628	481	oveq1d 7364	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π) = ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π) · π))
629	620, 626	addcld 11134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℂ)
630	629, 614, 479	divcan1d 11901	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π) · π) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))))
631	628, 630	eqtr2d 2765	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) = (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π))
632	631	oveq2d 7365	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))) = ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)))
633	625, 627, 632	3eqtr2rd 2771	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) = (((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))))
634	633	itgeq2dv 25681	. . . . 5 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) d𝑥 = ∫𝐶(((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) d𝑥)
635		remulcl 11094	. . . . . . 7 ⊢ (((1 / 2) ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ) → ((1 / 2) · (𝐹‘𝑥)) ∈ ℝ)
636	472, 119, 635	sylancr 587	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) · (𝐹‘𝑥)) ∈ ℝ)
637	148, 119, 140	iblmulc2 25730	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((1 / 2) · (𝐹‘𝑥))) ∈ 𝐿¹)
638	391	an32s 652	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
639	474, 638	fsumrecl 15641	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
640	453	simpld 494	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) ∈ 𝐿¹)
641	636, 637, 639, 640	itgadd 25724	. . . . 5 ⊢ (𝜑 → ∫𝐶(((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) d𝑥 = (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥))
642	619, 634, 641	3eqtrrd 2769	. . . 4 ⊢ (𝜑 → (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥) = (π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥))
643	642	oveq1d 7364	. . 3 ⊢ (𝜑 → ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥) / π) = ((π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) / π))
644	636, 637	itgcl 25683	. . . 4 ⊢ (𝜑 → ∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 ∈ ℂ)
645	639, 640	itgcl 25683	. . . 4 ⊢ (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 ∈ ℂ)
646	644, 645, 142, 102	divdird 11938	. . 3 ⊢ (𝜑 → ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥) / π) = ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π)))
647	483, 612	itgcl 25683	. . . 4 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥 ∈ ℂ)
648	647, 142, 102	divcan3d 11905	. . 3 ⊢ (𝜑 → ((π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) / π) = ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥)
649	643, 646, 648	3eqtr3d 2772	. 2 ⊢ (𝜑 → ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π)) = ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥)
650	90, 458, 649	3eqtrd 2768	1 ⊢ (𝜑 → (𝑆‘𝑁) = ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 Vcvv 3436 ⊆ wss 3903 ifcif 4476 class class class wbr 5092 ↦ cmpt 5173 dom cdm 5619 ↾ cres 5621 ⟶wf 6478 ‘cfv 6482 (class class class)co 7349 ∘_f cof 7611 ℂcc 11007 ℝcr 11008 0cc0 11009 1c1 11010 + caddc 11012 · cmul 11014 < clt 11149 ≤ cle 11150 − cmin 11347 -cneg 11348 / cdiv 11777 ℕcn 12128 2c2 12183 ℕ₀cn0 12384 (,)cioo 13248 [,]cicc 13251 ...cfz 13410 mod cmo 13773 abscabs 15141 Σcsu 15593 sincsin 15970 cosccos 15971 πcpi 15973 –cn→ccncf 24767 volcvol 25362 MblFncmbf 25513 𝐿¹cibl 25516 ∫citg 25517

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-inf2 9537 ax-cc 10329 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087 ax-addf 11088

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 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-iin 4944 df-disj 5060 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-isom 6491 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-of 7613 df-ofr 7614 df-om 7800 df-1st 7924 df-2nd 7925 df-supp 8094 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-oadd 8392 df-omul 8393 df-er 8625 df-map 8755 df-pm 8756 df-ixp 8825 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-fsupp 9252 df-fi 9301 df-sup 9332 df-inf 9333 df-oi 9402 df-dju 9797 df-card 9835 df-acn 9838 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-5 12194 df-6 12195 df-7 12196 df-8 12197 df-9 12198 df-n0 12385 df-z 12472 df-dec 12592 df-uz 12736 df-q 12850 df-rp 12894 df-xneg 13014 df-xadd 13015 df-xmul 13016 df-ioo 13252 df-ioc 13253 df-ico 13254 df-icc 13255 df-fz 13411 df-fzo 13558 df-fl 13696 df-mod 13774 df-seq 13909 df-exp 13969 df-fac 14181 df-bc 14210 df-hash 14238 df-shft 14974 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-limsup 15378 df-clim 15395 df-rlim 15396 df-sum 15594 df-ef 15974 df-sin 15976 df-cos 15977 df-pi 15979 df-struct 17058 df-sets 17075 df-slot 17093 df-ndx 17105 df-base 17121 df-ress 17142 df-plusg 17174 df-mulr 17175 df-starv 17176 df-sca 17177 df-vsca 17178 df-ip 17179 df-tset 17180 df-ple 17181 df-ds 17183 df-unif 17184 df-hom 17185 df-cco 17186 df-rest 17326 df-topn 17327 df-0g 17345 df-gsum 17346 df-topgen 17347 df-pt 17348 df-prds 17351 df-xrs 17406 df-qtop 17411 df-imas 17412 df-xps 17414 df-mre 17488 df-mrc 17489 df-acs 17491 df-mgm 18514 df-sgrp 18593 df-mnd 18609 df-submnd 18658 df-mulg 18947 df-cntz 19196 df-cmn 19661 df-psmet 21253 df-xmet 21254 df-met 21255 df-bl 21256 df-mopn 21257 df-fbas 21258 df-fg 21259 df-cnfld 21262 df-top 22779 df-topon 22796 df-topsp 22818 df-bases 22831 df-cld 22904 df-ntr 22905 df-cls 22906 df-nei 22983 df-lp 23021 df-perf 23022 df-cn 23112 df-cnp 23113 df-t1 23199 df-haus 23200 df-cmp 23272 df-tx 23447 df-hmeo 23640 df-fil 23731 df-fm 23823 df-flim 23824 df-flf 23825 df-xms 24206 df-ms 24207 df-tms 24208 df-cncf 24769 df-ovol 25363 df-vol 25364 df-mbf 25518 df-itg1 25519 df-itg2 25520 df-ibl 25521 df-itg 25522 df-0p 25569 df-limc 25765 df-dv 25766

This theorem is referenced by: fourierdlem111 46198

W3C validator