Theorem fourierdlem83

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

	Ref	Expression
Hypotheses	fourierdlem83.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
	fourierdlem83.c	⊢ 𝐶 = ( - π (,) π )
	fourierdlem83.fl1	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) ∈ 𝐿1 )
	fourierdlem83.a	⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( 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	fourierdlem83	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑁 ) = ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑥 − 𝑋 ) ) ) d 𝑥 )

Proof

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