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 46961

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 7427	. . . . . 6 ⊢ (𝑚 = 𝑁 → (1...𝑚) = (1...𝑁))
4	3	sumeq1d 15775	. . . . 5 ⊢ (𝑚 = 𝑁 → Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
5	4	oveq2d 7435	. . . 4 ⊢ (𝑚 = 𝑁 → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
6	5	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝑚 = 𝑁) → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑚)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
7		fourierdlem83.n	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ)
8		id 23	. . . . . 6 ⊢ (𝜑 → 𝜑)
9		0nn0 12534	. . . . . . 7 ⊢ 0 ∈ ℕ₀
10	9	a1i 11	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℕ₀)
11	9	elexi 3479	. . . . . . 7 ⊢ 0 ∈ V
12		eleq1 2853	. . . . . . . . 9 ⊢ (𝑛 = 0 → (𝑛 ∈ ℕ₀ ↔ 0 ∈ ℕ₀))
13	12	anbi2d 642	. . . . . . . 8 ⊢ (𝑛 = 0 → ((𝜑 ∧ 𝑛 ∈ ℕ₀) ↔ (𝜑 ∧ 0 ∈ ℕ₀)))
14		fveq2 6885	. . . . . . . . 9 ⊢ (𝑛 = 0 → (𝐴‘𝑛) = (𝐴‘0))
15	14	eleq1d 2850	. . . . . . . 8 ⊢ (𝑛 = 0 → ((𝐴‘𝑛) ∈ ℝ ↔ (𝐴‘0) ∈ ℝ))
16	13, 15	imbi12d 347	. . . . . . 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 46901	. . . . . . . . 9 ⊢ (𝜑 → ((𝑛 ∈ ℕ₀ → (𝐴‘𝑛) ∈ ℝ) ∧ (𝑛 ∈ ℕ → (𝐵‘𝑛) ∈ ℝ)))
23	22	simpld 500	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ ℕ₀ → (𝐴‘𝑛) ∈ ℝ))
24	23	imp 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝐴‘𝑛) ∈ ℝ)
25	11, 16, 24	vtocl 3527	. . . . . 6 ⊢ ((𝜑 ∧ 0 ∈ ℕ₀) → (𝐴‘0) ∈ ℝ)
26	8, 10, 25	syl2anc 596	. . . . 5 ⊢ (𝜑 → (𝐴‘0) ∈ ℝ)
27	26	rehalfcld 12506	. . . 4 ⊢ (𝜑 → ((𝐴‘0) / 2) ∈ ℝ)
28		fzfid 14027	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
29		eleq1 2853	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ ℕ₀ ↔ 𝑛 ∈ ℕ₀))
30	29	anbi2d 642	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → ((𝜑 ∧ 𝑘 ∈ ℕ₀) ↔ (𝜑 ∧ 𝑛 ∈ ℕ₀)))
31		simpl 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → 𝑘 = 𝑛)
32	31	oveq1d 7434	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → (𝑘 · 𝑥) = (𝑛 · 𝑥))
33	32	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑘 · 𝑥)) = (cos‘(𝑛 · 𝑥)))
34	33	oveq2d 7435	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))
35	34	itgeq2dv 25992	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥)
36	35	eleq1d 2850	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ ↔ ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ))
37	30, 36	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → (((𝜑 ∧ 𝑘 ∈ ℕ₀) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ) ↔ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)))
38	17	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝐹:ℝ⟶ℝ)
39	19	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (𝐹 ↾ 𝐶) ∈ 𝐿¹)
40		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
41	38, 18, 39, 20, 40	fourierdlem16 46895	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → (((𝐴‘𝑘) ∈ ℝ ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹) ∧ ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ))
42	41	simprd 501	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ)
43	37, 42	chvarvv 2022	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
44		pire 26670	. . . . . . . . . . . 12 ⊢ π ∈ ℝ
45	44	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → π ∈ ℝ)
46		0re 11225	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
47		pipos 26674	. . . . . . . . . . . . 13 ⊢ 0 < π
48	46, 47	gtneii 11337	. . . . . . . . . . . 12 ⊢ π ≠ 0
49	48	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → π ≠ 0)
50	43, 45, 49	redivcld 12058	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
51	50, 20	fmptd 7113	. . . . . . . . 9 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℝ)
52	51	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐴:ℕ₀⟶ℝ)
53		elfznn 13598	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
54	53	nnnn0d 12580	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ₀)
55	54	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ₀)
56	52, 55	ffvelcdmd 7084	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐴‘𝑛) ∈ ℝ)
57	55	nn0red 12581	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℝ)
58		fourierdlem83.x	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ℝ)
59	58	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℝ)
60	57, 59	remulcld 11254	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑛 · 𝑋) ∈ ℝ)
61	60	recoscld 16222	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℝ)
62	56, 61	remulcld 11254	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
63		eleq1 2853	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → (𝑘 ∈ ℕ ↔ 𝑛 ∈ ℕ))
64	63	anbi2d 642	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → ((𝜑 ∧ 𝑘 ∈ ℕ) ↔ (𝜑 ∧ 𝑛 ∈ ℕ)))
65		oveq1 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑛 → (𝑘 · 𝑥) = (𝑛 · 𝑥))
66	65	fveq2d 6889	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑛 → (sin‘(𝑘 · 𝑥)) = (sin‘(𝑛 · 𝑥)))
67	66	oveq2d 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑛 → ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
68	67	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
69	68	itgeq2dv 25992	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑛 → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥)
70	69	eleq1d 2850	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑛 → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ ↔ ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ))
71	64, 70	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑛 → (((𝜑 ∧ 𝑘 ∈ ℕ) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ) ↔ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)))
72	17	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:ℝ⟶ℝ)
73	19	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹 ↾ 𝐶) ∈ 𝐿¹)
74		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
75	72, 18, 73, 21, 74	fourierdlem21 46900	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (((𝐵‘𝑘) ∈ ℝ ∧ (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥)))) ∈ 𝐿¹) ∧ ∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ))
76	75	simprd 501	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 ∈ ℝ)
77	71, 76	chvarvv 2022	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
78	44	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → π ∈ ℝ)
79	48	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → π ≠ 0)
80	77, 78, 79	redivcld 12058	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
81	80, 21	fmptd 7113	. . . . . . . . 9 ⊢ (𝜑 → 𝐵:ℕ⟶ℝ)
82	81	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐵:ℕ⟶ℝ)
83	53	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ℕ)
84	82, 83	ffvelcdmd 7084	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐵‘𝑛) ∈ ℝ)
85	60	resincld 16221	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
86	84, 85	remulcld 11254	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
87	62, 86	readdcld 11253	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
88	28, 87	fsumrecl 15808	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
89	27, 88	readdcld 11253	. . 3 ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) ∈ ℝ)
90	2, 6, 7, 89	fvmptd 7001	. 2 ⊢ (𝜑 → (𝑆‘𝑁) = (((𝐴‘0) / 2) + Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))))
91	20	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐴 = (𝑛 ∈ ℕ₀ ↦ (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
92		oveq1 7426	. . . . . . . . . . . . 13 ⊢ (𝑛 = 0 → (𝑛 · 𝑥) = (0 · 𝑥))
93	92	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝑛 = 0 → (cos‘(𝑛 · 𝑥)) = (cos‘(0 · 𝑥)))
94	93	oveq2d 7435	. . . . . . . . . . 11 ⊢ (𝑛 = 0 → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(0 · 𝑥))))
95	94	adantr 486	. . . . . . . . . 10 ⊢ ((𝑛 = 0 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(0 · 𝑥))))
96	95	itgeq2dv 25992	. . . . . . . . 9 ⊢ (𝑛 = 0 → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥)
97	96	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 0) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥)
98	97	oveq1d 7434	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 = 0) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) = (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
99	17, 18, 19, 20, 10	fourierdlem16 46895	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴‘0) ∈ ℝ ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹) ∧ ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 ∈ ℝ))
100	99	simprd 501	. . . . . . . 8 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 ∈ ℝ)
101	44	a1i 11	. . . . . . . 8 ⊢ (𝜑 → π ∈ ℝ)
102	48	a1i 11	. . . . . . . 8 ⊢ (𝜑 → π ≠ 0)
103	100, 101, 102	redivcld 12058	. . . . . . 7 ⊢ (𝜑 → (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) ∈ ℝ)
104	91, 98, 10, 103	fvmptd 7001	. . . . . 6 ⊢ (𝜑 → (𝐴‘0) = (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π))
105		ioosscn 13451	. . . . . . . . . . . . . . 15 ⊢ (-π(,)π) ⊆ ℂ
106		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐶)
107	106, 18	eleqtrdi 2875	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ (-π(,)π))
108	105, 107	sselid 3936	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ℂ)
109	108	mul02d 11423	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐶 → (0 · 𝑥) = 0)
110	109	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐶 → (cos‘(0 · 𝑥)) = (cos‘0))
111		cos0 16228	. . . . . . . . . . . 12 ⊢ (cos‘0) = 1
112	110, 111	eqtrdi 2816	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐶 → (cos‘(0 · 𝑥)) = 1)
113	112	oveq2d 7435	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐶 → ((𝐹‘𝑥) · (cos‘(0 · 𝑥))) = ((𝐹‘𝑥) · 1))
114	113	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(0 · 𝑥))) = ((𝐹‘𝑥) · 1))
115	17	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐹:ℝ⟶ℝ)
116		ioossre 13450	. . . . . . . . . . . . . 14 ⊢ (-π(,)π) ⊆ ℝ
117	116, 107	sselid 3936	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ℝ)
118	117	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
119	115, 118	ffvelcdmd 7084	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
120	119	recnd 11252	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
121	120	mulridd 11241	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · 1) = (𝐹‘𝑥))
122	114, 121	eqtrd 2800	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(0 · 𝑥))) = (𝐹‘𝑥))
123	122	itgeq2dv 25992	. . . . . . 7 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 = ∫𝐶(𝐹‘𝑥) d𝑥)
124	123	oveq1d 7434	. . . . . 6 ⊢ (𝜑 → (∫𝐶((𝐹‘𝑥) · (cos‘(0 · 𝑥))) d𝑥 / π) = (∫𝐶(𝐹‘𝑥) d𝑥 / π))
125	104, 124	eqtrd 2800	. . . . 5 ⊢ (𝜑 → (𝐴‘0) = (∫𝐶(𝐹‘𝑥) d𝑥 / π))
126	125	oveq1d 7434	. . . 4 ⊢ (𝜑 → ((𝐴‘0) / 2) = ((∫𝐶(𝐹‘𝑥) d𝑥 / π) / 2))
127	17	feqmptd 6953	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)))
128	127	reseq1d 5979	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ 𝐶))
129	44	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐶 → π ∈ ℝ)
130	129	renegcld 11656	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐶 → -π ∈ ℝ)
131		ioossicc 13476	. . . . . . . . . . . . 13 ⊢ (-π(,)π) ⊆ (-π[,]π)
132	18, 131	eqsstri 3984	. . . . . . . . . . . 12 ⊢ 𝐶 ⊆ (-π[,]π)
133	132	sseli 3934	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ (-π[,]π))
134		eliccre 46279	. . . . . . . . . . 11 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ ∧ 𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
135	130, 129, 133, 134	syl3anc 1398	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ℝ)
136	135	ssriv 3942	. . . . . . . . 9 ⊢ 𝐶 ⊆ ℝ
137		resmpt 6041	. . . . . . . . 9 ⊢ (𝐶 ⊆ ℝ → ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
138	136, 137	mp1i 14	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
139	128, 138	eqtr2d 2801	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝐹 ↾ 𝐶))
140	139, 19	eqeltrd 2865	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
141	119, 140	itgcl 25994	. . . . 5 ⊢ (𝜑 → ∫𝐶(𝐹‘𝑥) d𝑥 ∈ ℂ)
142	101	recnd 11252	. . . . 5 ⊢ (𝜑 → π ∈ ℂ)
143		2cnd 12334	. . . . 5 ⊢ (𝜑 → 2 ∈ ℂ)
144		2ne0 12362	. . . . . 6 ⊢ 2 ≠ 0
145	144	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ≠ 0)
146	141, 142, 143, 102, 145	divdiv32d 12031	. . . 4 ⊢ (𝜑 → ((∫𝐶(𝐹‘𝑥) d𝑥 / π) / 2) = ((∫𝐶(𝐹‘𝑥) d𝑥 / 2) / π))
147	141, 143, 145	divrecd 12009	. . . . . 6 ⊢ (𝜑 → (∫𝐶(𝐹‘𝑥) d𝑥 / 2) = (∫𝐶(𝐹‘𝑥) d𝑥 · (1 / 2)))
148	143, 145	reccld 11999	. . . . . . 7 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
149	141, 148	mulcomd 11245	. . . . . 6 ⊢ (𝜑 → (∫𝐶(𝐹‘𝑥) d𝑥 · (1 / 2)) = ((1 / 2) · ∫𝐶(𝐹‘𝑥) d𝑥))
150	148, 119, 140	itgmulc2 26044	. . . . . 6 ⊢ (𝜑 → ((1 / 2) · ∫𝐶(𝐹‘𝑥) d𝑥) = ∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥)
151	147, 149, 150	3eqtrd 2804	. . . . 5 ⊢ (𝜑 → (∫𝐶(𝐹‘𝑥) d𝑥 / 2) = ∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥)
152	151	oveq1d 7434	. . . 4 ⊢ (𝜑 → ((∫𝐶(𝐹‘𝑥) d𝑥 / 2) / π) = (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π))
153	126, 146, 152	3eqtrd 2804	. . 3 ⊢ (𝜑 → ((𝐴‘0) / 2) = (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π))
154	55, 50	syldan 603	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
155	20	fvmpt2 7005	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ₀ ∧ (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐴‘𝑛) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
156	55, 154, 155	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐴‘𝑛) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
157	156	oveq1d 7434	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))))
158	154	recnd 11252	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
159	61	recnd 11252	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · 𝑋)) ∈ ℂ)
160	158, 159	mulcomd 11245	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) · (cos‘(𝑛 · 𝑋))) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
161	55, 43	syldan 603	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
162	161	recnd 11252	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
163	142	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → π ∈ ℂ)
164	48	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → π ≠ 0)
165	159, 162, 163, 164	divassd 12041	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)))
166	17	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → 𝐹:ℝ⟶ℝ)
167	117	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
168	166, 167	ffvelcdmd 7084	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
169		nn0re 12528	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℝ)
170	169	ad2antlr 740	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
171	170, 167	remulcld 11254	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℝ)
172	171	recoscld 16222	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
173	168, 172	remulcld 11254	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
174	54, 173	sylanl2 694	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) ∈ ℝ)
175		ioombl 25775	. . . . . . . . . . . . . . . . . . 19 ⊢ (-π(,)π) ∈ dom vol
176	18, 175	eqeltri 2861	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐶 ∈ dom vol
177	176	elexi 3479	. . . . . . . . . . . . . . . . 17 ⊢ 𝐶 ∈ V
178	177	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝐶 ∈ V)
179		eqidd 2766	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))))
180		eqidd 2766	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
181	178, 172, 168, 179, 180	offval2 7704	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
182	172	recnd 11252	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℂ)
183	120	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
184	182, 183	mulcomd 11245	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ₀) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))
185	184	mpteq2dva 5206	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))))
186	181, 185	eqtr2d 2801	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
187		coscn 26659	. . . . . . . . . . . . . . . . . 18 ⊢ cos ∈ (ℂ–cn→ℂ)
188	187	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → cos ∈ (ℂ–cn→ℂ))
189		ax-resscn 11172	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℝ ⊆ ℂ
190	136, 189	sstri 3947	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐶 ⊆ ℂ
191	190	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝐶 ⊆ ℂ)
192	169	recnd 11252	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ₀ → 𝑛 ∈ ℂ)
193	192	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → 𝑛 ∈ ℂ)
194		ssid 3960	. . . . . . . . . . . . . . . . . . . 20 ⊢ ℂ ⊆ ℂ
195	194	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ℂ ⊆ ℂ)
196	191, 193, 195	constcncfg 46644	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ 𝑛) ∈ (𝐶–cn→ℂ))
197	191, 195	idcncfg 46645	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ 𝑥) ∈ (𝐶–cn→ℂ))
198	196, 197	mulcncf 25656	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶–cn→ℂ))
199	188, 198	cncfmpt1f 25124	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ))
200		cnmbf 25869	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ dom vol ∧ (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
201	176, 199, 200	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn)
202	140	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
203		1re 11223	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ
204		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))))
205	169	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
206	117	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
207	205, 206	remulcld 11254	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℝ)
208	207	recoscld 16222	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
209	208	ralrimiva 3159	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ₀ → ∀𝑥 ∈ 𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
210	209	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → ∀𝑥 ∈ 𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ)
211		dmmptg 6245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 ∈ 𝐶 (cos‘(𝑛 · 𝑥)) ∈ ℝ → dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
212	210, 211	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = 𝐶)
213	204, 212	eleqtrd 2867	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → 𝑦 ∈ 𝐶)
214		eqidd 2766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))))
215		oveq2 7427	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑛 · 𝑥) = (𝑛 · 𝑦))
216	215	fveq2d 6889	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
217	216	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑛 · 𝑦)))
218		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
219	169	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → 𝑛 ∈ ℝ)
220	136, 218	sselid 3936	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
221	219, 220	remulcld 11254	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (𝑛 · 𝑦) ∈ ℝ)
222	221	recoscld 16222	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (cos‘(𝑛 · 𝑦)) ∈ ℝ)
223	214, 217, 218, 222	fvmptd 7001	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦) = (cos‘(𝑛 · 𝑦)))
224	223	fveq2d 6889	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(cos‘(𝑛 · 𝑦))))
225		abscosbd 46056	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 · 𝑦) ∈ ℝ → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
226	221, 225	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (abs‘(cos‘(𝑛 · 𝑦))) ≤ 1)
227	224, 226	eqbrtrd 5135	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
228	213, 227	syldan 603	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
229	228	ralrimiva 3159	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ₀ → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
230		breq2 5115	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 1 → ((abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
231	230	ralbidv 3190	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
232	231	rspcev 3583	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
233	203, 229, 232	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ₀ → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
234	233	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
235		bddmulibl 26049	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
236	201, 202, 234, 235	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
237	186, 236	eqeltrd 2865	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ₀) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
238	55, 237	syldan 603	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
239	159, 174, 238	itgmulc2 26044	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) d𝑥)
240	159	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑋)) ∈ ℂ)
241	120	adantlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
242	54, 182	sylanl2 694	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℂ)
243	240, 241, 242	mul12d 11434	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))))
244	240, 242	mulcomd 11245	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥))) = ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))
245	244	oveq2d 7435	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑋)) · (cos‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
246	243, 245	eqtrd 2800	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))))
247	246	itgeq2dv 25992	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
248	239, 247	eqtrd 2800	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥)
249	248	oveq1d 7434	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((cos‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
250	165, 249	eqtr3d 2802	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((cos‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
251	157, 160, 250	3eqtrd 2804	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π))
252	83, 80	syldan 603	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
253	21	fvmpt2 7005	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℕ ∧ (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ) → (𝐵‘𝑛) = (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
254	83, 252, 253	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝐵‘𝑛) = (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
255	254	oveq1d 7434	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = ((∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))))
256	252	recnd 11252	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℂ)
257	85	recnd 11252	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (sin‘(𝑛 · 𝑋)) ∈ ℂ)
258	256, 257	mulcomd 11245	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) · (sin‘(𝑛 · 𝑋))) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
259	83, 77	syldan 603	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
260	259	recnd 11252	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℂ)
261	257, 260, 163, 164	divassd 12041	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)))
262	119	adantlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
263		nnre 12255	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
264	263	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
265	117	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
266	264, 265	remulcld 11254	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℝ)
267	266	resincld 16221	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℕ ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
268	267	adantll 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
269	262, 268	remulcld 11254	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
270	53, 269	sylanl2 694	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
271	177	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 ∈ V)
272		eqidd 2766	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))))
273		eqidd 2766	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
274	271, 268, 262, 272, 273	offval2 7704	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
275	268	recnd 11252	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℂ)
276	120	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℂ)
277	275, 276	mulcomd 11245	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
278	277	mpteq2dva 5206	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))))
279	274, 278	eqtr2d 2801	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
280		sincn 26658	. . . . . . . . . . . . . . . . . 18 ⊢ sin ∈ (ℂ–cn→ℂ)
281	280	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sin ∈ (ℂ–cn→ℂ))
282	190	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → 𝐶 ⊆ ℂ)
283	263	recnd 11252	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
284	194	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → ℂ ⊆ ℂ)
285	282, 283, 284	constcncfg 46644	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (𝑥 ∈ 𝐶 ↦ 𝑛) ∈ (𝐶–cn→ℂ))
286	282, 284	idcncfg 46645	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (𝑥 ∈ 𝐶 ↦ 𝑥) ∈ (𝐶–cn→ℂ))
287	285, 286	mulcncf 25656	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → (𝑥 ∈ 𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶–cn→ℂ))
288	287	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶–cn→ℂ))
289	281, 288	cncfmpt1f 25124	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ))
290		cnmbf 25869	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ dom vol ∧ (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶–cn→ℂ)) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn)
291	176, 289, 290	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn)
292	140	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
293		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))))
294	267	ralrimiva 3159	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → ∀𝑥 ∈ 𝐶 (sin‘(𝑛 · 𝑥)) ∈ ℝ)
295		dmmptg 6245	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑥 ∈ 𝐶 (sin‘(𝑛 · 𝑥)) ∈ ℝ → dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
296	294, 295	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ℕ → dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
297	296	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
298	293, 297	eleqtrd 2867	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦 ∈ 𝐶)
299		eqidd 2766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))))
300	215	fveq2d 6889	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
301	300	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
302		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
303	263	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → 𝑛 ∈ ℝ)
304	136, 302	sselid 3936	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
305	303, 304	remulcld 11254	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (𝑛 · 𝑦) ∈ ℝ)
306	305	resincld 16221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (sin‘(𝑛 · 𝑦)) ∈ ℝ)
307	299, 301, 302, 306	fvmptd 7001	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦) = (sin‘(𝑛 · 𝑦)))
308	307	fveq2d 6889	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(sin‘(𝑛 · 𝑦))))
309		abssinbd 46072	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 · 𝑦) ∈ ℝ → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
310	305, 309	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
311	308, 310	eqbrtrd 5135	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
312	298, 311	syldan 603	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℕ ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
313	312	ralrimiva 3159	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
314		breq2 5115	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = 1 → ((abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
315	314	ralbidv 3190	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
316	315	rspcev 3583	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
317	203, 313, 316	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
318	317	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
319		bddmulibl 26049	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
320	291, 292, 318, 319	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑥 ∈ 𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
321	279, 320	eqeltrd 2865	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
322	83, 321	syldan 603	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿¹)
323	257, 270, 322	itgmulc2 26044	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) d𝑥)
324	257	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑋)) ∈ ℂ)
325	53, 275	sylanl2 694	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℂ)
326	324, 241, 325	mul12d 11434	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))))
327	324, 325	mulcomd 11245	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥))) = ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))
328	327	oveq2d 7435	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑋)) · (sin‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
329	326, 328	eqtrd 2800	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
330	329	itgeq2dv 25992	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))) d𝑥 = ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
331	323, 330	eqtrd 2800	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) = ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥)
332	331	oveq1d 7434	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((sin‘(𝑛 · 𝑋)) · ∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥) / π) = (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
333	261, 332	eqtr3d 2802	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((sin‘(𝑛 · 𝑋)) · (∫𝐶((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) = (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
334	255, 258, 333	3eqtrd 2804	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π))
335	251, 334	oveq12d 7437	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π) + (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π)))
336	54, 168	sylanl2 694	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝐹‘𝑥) ∈ ℝ)
337	55, 208	sylan 592	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑥)) ∈ ℝ)
338	61	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · 𝑋)) ∈ ℝ)
339	337, 338	remulcld 11254	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℝ)
340	336, 339	remulcld 11254	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) ∈ ℝ)
341	241, 242, 240	mul13d 46057	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
342	242, 241	mulcomd 11245	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))
343	342	oveq2d 7435	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑋)) · ((cos‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))))
344	341, 343	eqtrd 2800	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) = ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥)))))
345	344	mpteq2dva 5206	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) = (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))))
346	159, 174, 238	iblmulc2 26041	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))))) ∈ 𝐿¹)
347	345, 346	eqeltrd 2865	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))))) ∈ 𝐿¹)
348	340, 347	itgcl 25994	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
349	83, 267	sylan 592	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
350	85	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (sin‘(𝑛 · 𝑋)) ∈ ℝ)
351	349, 350	remulcld 11254	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℝ)
352	336, 351	remulcld 11254	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) ∈ ℝ)
353	241, 325, 324	mul13d 46057	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))))
354	325, 241	mulcomd 11245	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))
355	354	oveq2d 7435	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑋)) · ((sin‘(𝑛 · 𝑥)) · (𝐹‘𝑥))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))))
356	353, 355	eqtrd 2800	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) = ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥)))))
357	356	mpteq2dva 5206	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))))
358	257, 270, 322	iblmulc2 26041	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((sin‘(𝑛 · 𝑋)) · ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))))) ∈ 𝐿¹)
359	357, 358	eqeltrd 2865	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) ∈ 𝐿¹)
360	352, 359	itgcl 25994	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 ∈ ℂ)
361	348, 360, 163, 164	divdird 12044	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 / π) + (∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥 / π)))
362	53	nncnd 12264	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
363	362	ad2antlr 740	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℂ)
364	108	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℂ)
365	58	recnd 11252	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ ℂ)
366	365	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑋 ∈ ℂ)
367	363, 364, 366	subdid 11685	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · (𝑥 − 𝑋)) = ((𝑛 · 𝑥) − (𝑛 · 𝑋)))
368	367	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) = (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))))
369	363, 364	mulcld 11244	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑥) ∈ ℂ)
370	363, 366	mulcld 11244	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · 𝑋) ∈ ℂ)
371		cossub 16247	. . . . . . . . . . . . 13 ⊢ (((𝑛 · 𝑥) ∈ ℂ ∧ (𝑛 · 𝑋) ∈ ℂ) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
372	369, 370, 371	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘((𝑛 · 𝑥) − (𝑛 · 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
373	368, 372	eqtrd 2800	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) = (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))))
374	373	oveq2d 7435	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) = ((𝐹‘𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
375	339	recnd 11252	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) ∈ ℂ)
376	351	recnd 11252	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))) ∈ ℂ)
377	241, 375, 376	adddid 11248	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋))) + ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) = (((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
378	374, 377	eqtrd 2800	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) = (((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))))
379	378	itgeq2dv 25992	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = ∫𝐶(((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥)
380	340, 347, 352, 359	itgadd 26035	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶(((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) + ((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋))))) d𝑥 = (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥))
381	379, 380	eqtr2d 2801	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) = ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥)
382	381	oveq1d 7434	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((∫𝐶((𝐹‘𝑥) · ((cos‘(𝑛 · 𝑥)) · (cos‘(𝑛 · 𝑋)))) d𝑥 + ∫𝐶((𝐹‘𝑥) · ((sin‘(𝑛 · 𝑥)) · (sin‘(𝑛 · 𝑋)))) d𝑥) / π) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
383	335, 361, 382	3eqtr2d 2806	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
384	383	sumeq2dv 15777	. . . 4 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑛 ∈ (1...𝑁)(∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
385	57	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑛 ∈ ℝ)
386	117	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ ℝ)
387	58	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → 𝑋 ∈ ℝ)
388	386, 387	resubcld 11657	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑥 − 𝑋) ∈ ℝ)
389	385, 388	remulcld 11254	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (𝑛 · (𝑥 − 𝑋)) ∈ ℝ)
390	389	recoscld 16222	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
391	336, 390	remulcld 11254	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
392	177	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ∈ V)
393		eqidd 2766	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))))
394		eqidd 2766	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
395	392, 390, 336, 393, 394	offval2 7704	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · (𝑥 − 𝑋))) · (𝐹‘𝑥))))
396	390	recnd 11252	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℂ)
397	396, 241	mulcomd 11245	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) → ((cos‘(𝑛 · (𝑥 − 𝑋))) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))))
398	397	mpteq2dva 5206	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((cos‘(𝑛 · (𝑥 − 𝑋))) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))))
399	395, 398	eqtr2d 2801	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) = ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
400	187	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → cos ∈ (ℂ–cn→ℂ))
401	83, 285	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ 𝑛) ∈ (𝐶–cn→ℂ))
402	83, 286	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ 𝑥) ∈ (𝐶–cn→ℂ))
403	190	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝐶 ⊆ ℂ)
404	365	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑋 ∈ ℂ)
405	194	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ℂ ⊆ ℂ)
406	403, 404, 405	constcncfg 46644	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ 𝑋) ∈ (𝐶–cn→ℂ))
407	402, 406	subcncf 25655	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝑥 − 𝑋)) ∈ (𝐶–cn→ℂ))
408	401, 407	mulcncf 25656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝑛 · (𝑥 − 𝑋))) ∈ (𝐶–cn→ℂ))
409	400, 408	cncfmpt1f 25124	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ (𝐶–cn→ℂ))
410		cnmbf 25869	. . . . . . . . 9 ⊢ ((𝐶 ∈ dom vol ∧ (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ (𝐶–cn→ℂ)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ MblFn)
411	176, 409, 410	sylancr 599	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ MblFn)
412	140	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹)
413		simpr 490	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))) → 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))))
414	390	ralrimiva 3159	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∀𝑥 ∈ 𝐶 (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
415		dmmptg 6245	. . . . . . . . . . . . . 14 ⊢ (∀𝑥 ∈ 𝐶 (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ → dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) = 𝐶)
416	414, 415	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) = 𝐶)
417	416	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))) → dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) = 𝐶)
418	413, 417	eleqtrd 2867	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))) → 𝑦 ∈ 𝐶)
419		eqidd 2766	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) = (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))))
420		oveq1 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝑥 − 𝑋) = (𝑦 − 𝑋))
421	420	oveq2d 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → (𝑛 · (𝑥 − 𝑋)) = (𝑛 · (𝑦 − 𝑋)))
422	421	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (cos‘(𝑛 · (𝑥 − 𝑋))) = (cos‘(𝑛 · (𝑦 − 𝑋))))
423	422	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → (cos‘(𝑛 · (𝑥 − 𝑋))) = (cos‘(𝑛 · (𝑦 − 𝑋))))
424		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
425	57	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → 𝑛 ∈ ℝ)
426	55, 220	sylan 592	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
427	58	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → 𝑋 ∈ ℝ)
428	426, 427	resubcld 11657	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (𝑦 − 𝑋) ∈ ℝ)
429	425, 428	remulcld 11254	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (𝑛 · (𝑦 − 𝑋)) ∈ ℝ)
430	429	recoscld 16222	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (cos‘(𝑛 · (𝑦 − 𝑋))) ∈ ℝ)
431	419, 423, 424, 430	fvmptd 7001	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦) = (cos‘(𝑛 · (𝑦 − 𝑋))))
432	431	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) = (abs‘(cos‘(𝑛 · (𝑦 − 𝑋)))))
433		abscosbd 46056	. . . . . . . . . . . . 13 ⊢ ((𝑛 · (𝑦 − 𝑋)) ∈ ℝ → (abs‘(cos‘(𝑛 · (𝑦 − 𝑋)))) ≤ 1)
434	429, 433	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (abs‘(cos‘(𝑛 · (𝑦 − 𝑋)))) ≤ 1)
435	432, 434	eqbrtrd 5135	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1)
436	418, 435	syldan 603	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))) → (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1)
437	436	ralrimiva 3159	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1)
438		breq2 5115	. . . . . . . . . . 11 ⊢ (𝑏 = 1 → ((abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1))
439	438	ralbidv 3190	. . . . . . . . . 10 ⊢ (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1))
440	439	rspcev 3583	. . . . . . . . 9 ⊢ ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏)
441	203, 437, 440	sylancr 599	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏)
442		bddmulibl 26049	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))(abs‘((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋))))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
443	411, 412, 441, 442	syl3anc 1398	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑥 ∈ 𝐶 ↦ (cos‘(𝑛 · (𝑥 − 𝑋)))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
444	399, 443	eqeltrd 2865	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) ∈ 𝐿¹)
445	391, 444	itgcl 25994	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 ∈ ℂ)
446	28, 142, 445, 102	fsumdivc 15860	. . . 4 ⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π) = Σ𝑛 ∈ (1...𝑁)(∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
447	176	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ dom vol)
448		anass 474	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑥 ∈ 𝐶)))
449		ancom 466	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ (1...𝑁) ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐶 ∧ 𝑛 ∈ (1...𝑁)))
450	449	anbi2i 635	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑥 ∈ 𝐶)) ↔ (𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑛 ∈ (1...𝑁))))
451	448, 450	bitri 278	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝑁)) ∧ 𝑥 ∈ 𝐶) ↔ (𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑛 ∈ (1...𝑁))))
452	451, 391	sylbir 238	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑛 ∈ (1...𝑁))) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
453	447, 28, 452, 444	itgfsum 26037	. . . . . . 7 ⊢ (𝜑 → ((𝑥 ∈ 𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) ∈ 𝐿¹ ∧ ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥))
454	453	simprd 501	. . . . . 6 ⊢ (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥)
455	454	eqcomd 2771	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 = ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥)
456	455	oveq1d 7434	. . . 4 ⊢ (𝜑 → (Σ𝑛 ∈ (1...𝑁)∫𝐶((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
457	384, 446, 456	3eqtr2d 2806	. . 3 ⊢ (𝜑 → Σ𝑛 ∈ (1...𝑁)(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π))
458	153, 457	oveq12d 7437	. 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 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑁 ∈ ℕ)
461		eqid 2765	. . . . . . . . . . 11 ⊢ (𝐷‘𝑁) = (𝐷‘𝑁)
462		eqid 2765	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π))
463	459, 460, 461, 462	dirkertrigeq 46873	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝐷‘𝑁) = (𝑠 ∈ ℝ ↦ (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π)))
464		oveq2 7427	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = (𝑥 − 𝑋) → (𝑛 · 𝑠) = (𝑛 · (𝑥 − 𝑋)))
465	464	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑥 − 𝑋) → (cos‘(𝑛 · 𝑠)) = (cos‘(𝑛 · (𝑥 − 𝑋))))
466	465	sumeq2sdv 15778	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑥 − 𝑋) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠)) = Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))
467	466	oveq2d 7435	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑥 − 𝑋) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))))
468	467	oveq1d 7434	. . . . . . . . . . 11 ⊢ (𝑠 = (𝑥 − 𝑋) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π))
469	468	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑠 = (𝑥 − 𝑋)) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · 𝑠))) / π) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π))
470	58	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝑋 ∈ ℝ)
471	118, 470	resubcld 11657	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (𝑥 − 𝑋) ∈ ℝ)
472		halfre 12472	. . . . . . . . . . . . 13 ⊢ (1 / 2) ∈ ℝ
473	472	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (1 / 2) ∈ ℝ)
474		fzfid 14027	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (1...𝑁) ∈ Fin)
475	390	an32s 665	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
476	474, 475	fsumrecl 15808	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℝ)
477	473, 476	readdcld 11253	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
478	44	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → π ∈ ℝ)
479	48	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → π ≠ 0)
480	477, 478, 479	redivcld 12058	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π) ∈ ℝ)
481	463, 469, 471, 480	fvmptd 7001	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = (((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π))
482	481, 480	eqeltrd 2865	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ)
483	119, 482	remulcld 11254	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ ℝ)
484	177	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ V)
485		eqidd 2766	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
486		eqidd 2766	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))
487	484, 482, 119, 485, 486	offval2 7704	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))))
488	482	recnd 11252	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℂ)
489	488, 120	mulcomd 11245	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
490	489	mpteq2dva 5206	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))) = (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))))
491	487, 490	eqtr2d 2801	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) = ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))))
492		eqid 2765	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))
493		eqid 2765	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))
494	194	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ℂ ⊆ ℂ)
495		cncfss 25109	. . . . . . . . . . . . . 14 ⊢ ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ))
496	189, 494, 495	sylancr 599	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ))
497		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
498	58	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑋 ∈ ℝ)
499	497, 498	resubcld 11657	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 − 𝑋) ∈ ℝ)
500		eqid 2765	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) = (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋))
501	499, 500	fmptd 7113	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)):ℝ⟶ℝ)
502	189	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ℝ ⊆ ℂ)
503	502, 494	idcncfg 46645	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝑥) ∈ (ℝ–cn→ℂ))
504	502, 365, 494	constcncfg 46644	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝑋) ∈ (ℝ–cn→ℂ))
505	503, 504	subcncf 25655	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℂ))
506		cncfcdm 25108	. . . . . . . . . . . . . . . 16 ⊢ ((ℝ ⊆ ℂ ∧ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℂ)) → ((𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)):ℝ⟶ℝ))
507	189, 505, 506	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℝ) ↔ (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)):ℝ⟶ℝ))
508	501, 507	mpbird 260	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 − 𝑋)) ∈ (ℝ–cn→ℝ))
509	459	dirkercncf 46879	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁) ∈ (ℝ–cn→ℝ))
510	7, 509	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷‘𝑁) ∈ (ℝ–cn→ℝ))
511	508, 510	cncfcompt 46655	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (ℝ–cn→ℝ))
512	496, 511	sseldd 3939	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (ℝ–cn→ℂ))
513	44	renegcli 11534	. . . . . . . . . . . . . 14 ⊢ -π ∈ ℝ
514		iccssre 13472	. . . . . . . . . . . . . 14 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
515	513, 44, 514	mp2an 705	. . . . . . . . . . . . 13 ⊢ (-π[,]π) ⊆ ℝ
516	515	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (-π[,]π) ⊆ ℝ)
517	459	dirkerf 46869	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (𝐷‘𝑁):ℝ⟶ℝ)
518	7, 517	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷‘𝑁):ℝ⟶ℝ)
519	518	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → (𝐷‘𝑁):ℝ⟶ℝ)
520	516	sselda 3938	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → 𝑥 ∈ ℝ)
521	58	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
522	520, 521	resubcld 11657	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → (𝑥 − 𝑋) ∈ ℝ)
523	519, 522	ffvelcdmd 7084	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ)
524	523	recnd 11252	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℂ)
525	493, 512, 516, 494, 524	cncfmptssg 46643	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ ((-π[,]π)–cn→ℂ))
526	132	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ⊆ (-π[,]π))
527	492, 525, 526, 494, 488	cncfmptssg 46643	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (𝐶–cn→ℂ))
528		cnmbf 25869	. . . . . . . . . 10 ⊢ ((𝐶 ∈ dom vol ∧ (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ (𝐶–cn→ℂ)) → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ MblFn)
529	176, 527, 528	sylancr 599	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ MblFn)
530	513	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → -π ∈ ℝ)
531		0red 11226	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ℝ)
532		negpilt0 46058	. . . . . . . . . . . . . . . 16 ⊢ -π < 0
533	532	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -π < 0)
534	47	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 < π)
535	530, 531, 101, 533, 534	lttrd 11386	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -π < π)
536	530, 101, 535	ltled 11373	. . . . . . . . . . . . 13 ⊢ (𝜑 → -π ≤ π)
537	493, 512, 516, 502, 523	cncfmptssg 46643	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ ((-π[,]π)–cn→ℝ))
538	530, 101, 536, 537	evthiccabs 46270	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ∧ ∃𝑧 ∈ (-π[,]π)∀𝑤 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑧)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑤))))
539	538	simpld 500	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)))
540		eqidd 2766	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
541	420	fveq2d 6889	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
542	541	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ (-π[,]π)) ∧ 𝑥 = 𝑦) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
543		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → 𝑦 ∈ (-π[,]π))
544	518	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (𝐷‘𝑁):ℝ⟶ℝ)
545	515, 543	sselid 3936	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → 𝑦 ∈ ℝ)
546	58	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
547	545, 546	resubcld 11657	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (𝑦 − 𝑋) ∈ ℝ)
548	544, 547	ffvelcdmd 7084	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑦 − 𝑋)) ∈ ℝ)
549	540, 542, 543, 548	fvmptd 7001	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
550	549	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
551	550	adantlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
552		eqidd 2766	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
553		oveq1 7426	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑐 → (𝑥 − 𝑋) = (𝑐 − 𝑋))
554	553	fveq2d 6889	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑐 → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑐 − 𝑋)))
555	554	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑥 = 𝑐) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑐 − 𝑋)))
556		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → 𝑐 ∈ (-π[,]π))
557	518	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (𝐷‘𝑁):ℝ⟶ℝ)
558	515, 556	sselid 3936	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → 𝑐 ∈ ℝ)
559	58	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → 𝑋 ∈ ℝ)
560	558, 559	resubcld 11657	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (𝑐 − 𝑋) ∈ ℝ)
561	557, 560	ffvelcdmd 7084	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑐 − 𝑋)) ∈ ℝ)
562	552, 555, 556, 561	fvmptd 7001	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → ((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐) = ((𝐷‘𝑁)‘(𝑐 − 𝑋)))
563	562	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
564	563	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
565	551, 564	breq12d 5124	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π)) ∧ 𝑦 ∈ (-π[,]π)) → ((abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ↔ (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
566	565	ralbidva 3188	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ↔ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
567	566	rexbidva 3189	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝑥 ∈ (-π[,]π) ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑐)) ↔ ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
568	539, 567	mpbid 235	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
569	561	recnd 11252	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → ((𝐷‘𝑁)‘(𝑐 − 𝑋)) ∈ ℂ)
570	569	abscld 15514	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π)) → (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∈ ℝ)
571	570	3adant3 1150	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∈ ℝ)
572		nfv 1947	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝜑
573		nfv 1947	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 𝑐 ∈ (-π[,]π)
574		nfra1 3291	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))
575	572, 573, 574	nf3an 1934	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
576		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
577	482	ralrimiva 3159	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ)
578		dmmptg 6245	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ 𝐶 ((𝐷‘𝑁)‘(𝑥 − 𝑋)) ∈ ℝ → dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = 𝐶)
579	577, 578	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = 𝐶)
580	579	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = 𝐶)
581	576, 580	eleqtrd 2867	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → 𝑦 ∈ 𝐶)
582	581	3ad2antl1 1204	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → 𝑦 ∈ 𝐶)
583		eqidd 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) = (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))))
584	541	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ 𝑥 = 𝑦) → ((𝐷‘𝑁)‘(𝑥 − 𝑋)) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
585		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ 𝐶)
586	518	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝐷‘𝑁):ℝ⟶ℝ)
587	136, 585	sselid 3936	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ ℝ)
588	58	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑋 ∈ ℝ)
589	587, 588	resubcld 11657	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝑦 − 𝑋) ∈ ℝ)
590	586, 589	ffvelcdmd 7084	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝐷‘𝑁)‘(𝑦 − 𝑋)) ∈ ℝ)
591	583, 584, 585, 590	fvmptd 7001	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦) = ((𝐷‘𝑁)‘(𝑦 − 𝑋)))
592	591	fveq2d 6889	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
593	592	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) = (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))))
594		simplr 781	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
595	132	sseli 3934	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ 𝐶 → 𝑦 ∈ (-π[,]π))
596	595	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → 𝑦 ∈ (-π[,]π))
597		rspa 3256	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∧ 𝑦 ∈ (-π[,]π)) → (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
598	594, 596, 597	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
599	593, 598	eqbrtrd 5135	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
600	599	3adantl2 1186	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ 𝐶) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
601	582, 600	syldan 603	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) ∧ 𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
602	601	ex 418	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → (𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) → (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
603	575, 602	ralrimi 3265	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))))
604		breq2 5115	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) → ((abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
605	604	ralbidv 3190	. . . . . . . . . . . . 13 ⊢ (𝑏 = (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) → (∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))))
606	605	rspcev 3583	. . . . . . . . . . . 12 ⊢ (((abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏)
607	571, 603, 606	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (-π[,]π) ∧ ∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋)))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏)
608	607	rexlimdv3a 3172	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑐 ∈ (-π[,]π)∀𝑦 ∈ (-π[,]π)(abs‘((𝐷‘𝑁)‘(𝑦 − 𝑋))) ≤ (abs‘((𝐷‘𝑁)‘(𝑐 − 𝑋))) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏))
609	568, 608	mpd 16	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏)
610		bddmulibl 26049	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∈ MblFn ∧ (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) ∈ 𝐿¹ ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))(abs‘((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋)))‘𝑦)) ≤ 𝑏) → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
611	529, 140, 609, 610	syl3anc 1398	. . . . . . . 8 ⊢ (𝜑 → ((𝑥 ∈ 𝐶 ↦ ((𝐷‘𝑁)‘(𝑥 − 𝑋))) ∘_f · (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) ∈ 𝐿¹)
612	491, 611	eqeltrd 2865	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) ∈ 𝐿¹)
613	142, 483, 612	itgmulc2 26044	. . . . . 6 ⊢ (𝜑 → (π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) = ∫𝐶(π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) d𝑥)
614	142	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → π ∈ ℂ)
615	120, 488, 614	mul13d 46057	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) = (π · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))))
616	489	oveq2d 7435	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (π · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · (𝐹‘𝑥))) = (π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))))
617	615, 616	eqtrd 2800	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) = (π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))))
618	617	itgeq2dv 25992	. . . . . 6 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) d𝑥 = ∫𝐶(π · ((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋)))) d𝑥)
619	613, 618	eqtr4d 2803	. . . . 5 ⊢ (𝜑 → (π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) = ∫𝐶((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) d𝑥)
620	148	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (1 / 2) ∈ ℂ)
621	620, 120	mulcomd 11245	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) · (𝐹‘𝑥)) = ((𝐹‘𝑥) · (1 / 2)))
622	396	an32s 665	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑛 ∈ (1...𝑁)) → (cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℂ)
623	474, 120, 622	fsummulc2 15858	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) = Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))))
624	623	eqcomd 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) = ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))))
625	621, 624	oveq12d 7437	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) = (((𝐹‘𝑥) · (1 / 2)) + ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))))
626	474, 622	fsumcl 15807	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))) ∈ ℂ)
627	120, 620, 626	adddid 11248	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))) = (((𝐹‘𝑥) · (1 / 2)) + ((𝐹‘𝑥) · Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))))
628	481	oveq1d 7434	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π) = ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π) · π))
629	620, 626	addcld 11243	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℂ)
630	629, 614, 479	divcan1d 12007	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) / π) · π) = ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))))
631	628, 630	eqtr2d 2801	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋)))) = (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π))
632	631	oveq2d 7435	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · ((1 / 2) + Σ𝑛 ∈ (1...𝑁)(cos‘(𝑛 · (𝑥 − 𝑋))))) = ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)))
633	625, 627, 632	3eqtr2rd 2807	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) = (((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))))
634	633	itgeq2dv 25992	. . . . 5 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · (((𝐷‘𝑁)‘(𝑥 − 𝑋)) · π)) d𝑥 = ∫𝐶(((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) d𝑥)
635		remulcl 11200	. . . . . . 7 ⊢ (((1 / 2) ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ) → ((1 / 2) · (𝐹‘𝑥)) ∈ ℝ)
636	472, 119, 635	sylancr 599	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((1 / 2) · (𝐹‘𝑥)) ∈ ℝ)
637	148, 119, 140	iblmulc2 26041	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ ((1 / 2) · (𝐹‘𝑥))) ∈ 𝐿¹)
638	391	an32s 665	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑛 ∈ (1...𝑁)) → ((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
639	474, 638	fsumrecl 15808	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) ∈ ℝ)
640	453	simpld 500	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐶 ↦ Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) ∈ 𝐿¹)
641	636, 637, 639, 640	itgadd 26035	. . . . 5 ⊢ (𝜑 → ∫𝐶(((1 / 2) · (𝐹‘𝑥)) + Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋))))) d𝑥 = (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥))
642	619, 634, 641	3eqtrrd 2805	. . . 4 ⊢ (𝜑 → (∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥) = (π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥))
643	642	oveq1d 7434	. . 3 ⊢ (𝜑 → ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥) / π) = ((π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) / π))
644	636, 637	itgcl 25994	. . . 4 ⊢ (𝜑 → ∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 ∈ ℂ)
645	639, 640	itgcl 25994	. . . 4 ⊢ (𝜑 → ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 ∈ ℂ)
646	644, 645, 142, 102	divdird 12044	. . 3 ⊢ (𝜑 → ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 + ∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥) / π) = ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π)))
647	483, 612	itgcl 25994	. . . 4 ⊢ (𝜑 → ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥 ∈ ℂ)
648	647, 142, 102	divcan3d 12011	. . 3 ⊢ (𝜑 → ((π · ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥) / π) = ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥)
649	643, 646, 648	3eqtr3d 2808	. 2 ⊢ (𝜑 → ((∫𝐶((1 / 2) · (𝐹‘𝑥)) d𝑥 / π) + (∫𝐶Σ𝑛 ∈ (1...𝑁)((𝐹‘𝑥) · (cos‘(𝑛 · (𝑥 − 𝑋)))) d𝑥 / π)) = ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥)
650	90, 458, 649	3eqtrd 2804	1 ⊢ (𝜑 → (𝑆‘𝑁) = ∫𝐶((𝐹‘𝑥) · ((𝐷‘𝑁)‘(𝑥 − 𝑋))) d𝑥)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 ∀wral 3081 ∃wrex 3091 Vcvv 3457 ⊆ wss 3906 ifcif 4489 class class class wbr 5111 ↦ cmpt 5194 dom cdm 5663 ↾ cres 5665 ⟶wf 6536 ‘cfv 6540 (class class class)co 7419 ∘_f cof 7682 ℂcc 11113 ℝcr 11114 0cc0 11115 1c1 11116 + caddc 11118 · cmul 11120 < clt 11258 ≤ cle 11259 − cmin 11456 -cneg 11457 / cdiv 11886 ℕcn 12248 2c2 12310 ℕ₀cn0 12519 (,)cioo 13388 [,]cicc 13391 ...cfz 13551 mod cmo 13920 abscabs 15309 Σcsu 15761 sincsin 16139 cosccos 16140 πcpi 16142 –cn→ccncf 25086 volcvol 25673 MblFncmbf 25824 𝐿¹cibl 25827 ∫citg 25828

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-inf2 9617 ax-cc 10434 ax-cnex 11171 ax-resscn 11172 ax-1cn 11173 ax-icn 11174 ax-addcl 11175 ax-addrcl 11176 ax-mulcl 11177 ax-mulrcl 11178 ax-mulcom 11179 ax-addass 11180 ax-mulass 11181 ax-distr 11182 ax-i2m1 11183 ax-1ne0 11184 ax-1rid 11185 ax-rnegex 11186 ax-rrecex 11187 ax-cnre 11188 ax-pre-lttri 11189 ax-pre-lttrn 11190 ax-pre-ltadd 11191 ax-pre-mulgt0 11192 ax-pre-sup 11193 ax-addf 11194

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-disj 5079 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-of 7684 df-ofr 7685 df-om 7869 df-1st 7992 df-2nd 7993 df-supp 8163 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-oadd 8463 df-omul 8464 df-er 8700 df-map 8832 df-pm 8833 df-ixp 8902 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-fsupp 9329 df-fi 9378 df-sup 9409 df-inf 9410 df-oi 9479 df-dju 9903 df-card 9941 df-acn 9944 df-pnf 11260 df-mnf 11261 df-xr 11262 df-ltxr 11263 df-le 11264 df-sub 11458 df-neg 11459 df-div 11887 df-nn 12249 df-2 12318 df-3 12319 df-4 12320 df-5 12321 df-6 12322 df-7 12323 df-8 12324 df-9 12325 df-n0 12520 df-z 12607 df-dec 12728 df-uz 12879 df-q 12989 df-rp 13033 df-xneg 13153 df-xadd 13154 df-xmul 13155 df-ioo 13392 df-ioc 13393 df-ico 13394 df-icc 13395 df-fz 13552 df-fzo 13700 df-fl 13843 df-mod 13921 df-seq 14056 df-exp 14116 df-fac 14328 df-bc 14357 df-hash 14385 df-shft 15128 df-cj 15174 df-re 15175 df-im 15176 df-sqrt 15310 df-abs 15311 df-limsup 15546 df-clim 15563 df-rlim 15564 df-sum 15762 df-ef 16143 df-sin 16145 df-cos 16146 df-pi 16148 df-struct 17229 df-sets 17246 df-slot 17264 df-ndx 17276 df-base 17292 df-ress 17313 df-plusg 17345 df-mulr 17346 df-starv 17347 df-sca 17348 df-vsca 17349 df-ip 17350 df-tset 17351 df-ple 17352 df-ds 17354 df-unif 17355 df-hom 17356 df-cco 17357 df-rest 17497 df-topn 17498 df-0g 17516 df-gsum 17517 df-topgen 17518 df-pt 17519 df-prds 17522 df-xrs 17578 df-qtop 17583 df-imas 17584 df-xps 17586 df-mre 17660 df-mrc 17661 df-acs 17663 df-mgm 18720 df-sgrp 18809 df-mnd 18825 df-submnd 18879 df-mulg 19178 df-cntz 19431 df-cmn 19896 df-psmet 21564 df-xmet 21565 df-met 21566 df-bl 21567 df-mopn 21568 df-fbas 21569 df-fg 21570 df-cnfld 21573 df-top 23101 df-topon 23118 df-topsp 23140 df-bases 23153 df-cld 23226 df-ntr 23227 df-cls 23228 df-nei 23305 df-lp 23343 df-perf 23344 df-cn 23434 df-cnp 23435 df-t1 23521 df-haus 23522 df-cmp 23594 df-tx 23770 df-hmeo 23963 df-fil 24054 df-fm 24146 df-flim 24147 df-flf 24148 df-xms 24528 df-ms 24529 df-tms 24530 df-cncf 25088 df-ovol 25674 df-vol 25675 df-mbf 25829 df-itg1 25830 df-itg2 25831 df-ibl 25832 df-itg 25833 df-0p 25880 df-limc 26076 df-dv 26077

This theorem is used by: fourierdlem111 46989

W3C validator