Metamath Proof Explorer

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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
121 120 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
122 121 mulid1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝑥 ) · 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 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ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 cncffvrn ⊢ ( ( ℝ ⊆ ℂ ∧ ( 𝑥 ∈ ℝ ↦ ( 𝑥 − 𝑋 ) ) ∈ ( ℝ –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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑥 − 𝑋 ) ) ∈ ℝ )
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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( - π [,] π ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑦 − 𝑋 ) ) ∈ ℝ )
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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( - π [,] π ) ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑐 − 𝑋 ) ) ∈ ℝ )
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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝐷 ‘ 𝑁 ) ‘ ( 𝑦 − 𝑋 ) ) ∈ ℝ )
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 𝑥 )