This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem16

Description: The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem16.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourierdlem16.c ⊢ 𝐶 = ( - π (,) π )
fourierdlem16.fibl ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) ∈ 𝐿1 )
fourierdlem16.a ⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
fourierdlem16.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion fourierdlem16 ( 𝜑 → ( ( ( 𝐴 ‘ 𝑁 ) ∈ ℝ ∧ ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 ) ∧ ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ∈ ℝ ) )

Proof

Step Hyp Ref Expression
1 fourierdlem16.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fourierdlem16.c ⊢ 𝐶 = ( - π (,) π )
3 fourierdlem16.fibl ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) ∈ 𝐿1 )
4 fourierdlem16.a ⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ ( ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) )
5 fourierdlem16.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐹 : ℝ ⟶ ℝ )
7 ioossre ⊢ ( - π (,) π ) ⊆ ℝ
8 id ⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐶 )
9 8 2 eleqtrdi ⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ ( - π (,) π ) )
10 7 9 sselid ⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ ℝ )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ℝ )
12 6 11 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
13 12 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
14 nn0re ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℝ )
15 14 adantr ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑥 ∈ 𝐶 ) → 𝑛 ∈ ℝ )
16 10 adantl ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ℝ )
17 15 16 remulcld ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑛 · 𝑥 ) ∈ ℝ )
18 17 recoscld ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑥 ∈ 𝐶 ) → ( cos ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ )
19 18 adantll ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( cos ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ )
20 13 19 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∈ ℝ )
21 ioombl ⊢ ( - π (,) π ) ∈ dom vol
22 2 21 eqeltri ⊢ 𝐶 ∈ dom vol
23 22 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝐶 ∈ dom vol )
24 eqidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) = ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) )
25 eqidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) )
26 23 19 13 24 25 offval2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∘f · ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐶 ↦ ( ( cos ‘ ( 𝑛 · 𝑥 ) ) · ( 𝐹 ‘ 𝑥 ) ) ) )
27 19 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( cos ‘ ( 𝑛 · 𝑥 ) ) ∈ ℂ )
28 13 recnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
29 27 28 mulcomd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐶 ) → ( ( cos ‘ ( 𝑛 · 𝑥 ) ) · ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) )
30 29 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( ( cos ‘ ( 𝑛 · 𝑥 ) ) · ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) )
31 26 30 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) = ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∘f · ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
32 coscn ⊢ cos ∈ ( ℂ –cn→ ℂ )
33 32 a1i ⊢ ( 𝑛 ∈ ℕ0 → cos ∈ ( ℂ –cn→ ℂ ) )
34 2 7 eqsstri ⊢ 𝐶 ⊆ ℝ
35 ax-resscn ⊢ ℝ ⊆ ℂ
36 34 35 sstri ⊢ 𝐶 ⊆ ℂ
37 36 a1i ⊢ ( 𝑛 ∈ ℕ0 → 𝐶 ⊆ ℂ )
38 14 recnd ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ )
39 ssid ⊢ ℂ ⊆ ℂ
40 39 a1i ⊢ ( 𝑛 ∈ ℕ0 → ℂ ⊆ ℂ )
41 37 38 40 constcncfg ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑥 ∈ 𝐶 ↦ 𝑛 ) ∈ ( 𝐶 –cn→ ℂ ) )
42 cncfmptid ⊢ ( ( 𝐶 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ 𝐶 ↦ 𝑥 ) ∈ ( 𝐶 –cn→ ℂ ) )
43 36 39 42 mp2an ⊢ ( 𝑥 ∈ 𝐶 ↦ 𝑥 ) ∈ ( 𝐶 –cn→ ℂ )
44 43 a1i ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑥 ∈ 𝐶 ↦ 𝑥 ) ∈ ( 𝐶 –cn→ ℂ ) )
45 41 44 mulcncf ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑥 ∈ 𝐶 ↦ ( 𝑛 · 𝑥 ) ) ∈ ( 𝐶 –cn→ ℂ ) )
46 33 45 cncfmpt1f ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∈ ( 𝐶 –cn→ ℂ ) )
47 cnmbf ⊢ ( ( 𝐶 ∈ dom vol ∧ ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∈ ( 𝐶 –cn→ ℂ ) ) → ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∈ MblFn )
48 22 46 47 sylancr ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∈ MblFn )
49 48 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∈ MblFn )
50 1 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) )
51 50 reseq1d ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) = ( ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ 𝐶 ) )
52 resmpt ⊢ ( 𝐶 ⊆ ℝ → ( ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ 𝐶 ) = ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) )
53 34 52 mp1i ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ 𝐶 ) = ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) )
54 51 53 eqtr2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ↾ 𝐶 ) )
55 54 3 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
56 55 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
57 1re ⊢ 1 ∈ ℝ
58 simpr ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) → 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) )
59 nfv ⊢ Ⅎ 𝑥 𝑛 ∈ ℕ0
60 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) )
61 60 nfdm ⊢ Ⅎ 𝑥 dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) )
62 61 nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) )
63 59 62 nfan ⊢ Ⅎ 𝑥 ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) )
64 18 ex ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑥 ∈ 𝐶 → ( cos ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ ) )
65 64 adantr ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) → ( 𝑥 ∈ 𝐶 → ( cos ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ ) )
66 63 65 ralrimi ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) → ∀ 𝑥 ∈ 𝐶 ( cos ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ )
67 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝐶 ( cos ‘ ( 𝑛 · 𝑥 ) ) ∈ ℝ → dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) = 𝐶 )
68 66 67 syl ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) → dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) = 𝐶 )
69 58 68 eleqtrd ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) → 𝑦 ∈ 𝐶 )
70 eqidd ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) = ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) )
71 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑛 · 𝑥 ) = ( 𝑛 · 𝑦 ) )
72 71 fveq2d ⊢ ( 𝑥 = 𝑦 → ( cos ‘ ( 𝑛 · 𝑥 ) ) = ( cos ‘ ( 𝑛 · 𝑦 ) ) )
73 72 adantl ⊢ ( ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 = 𝑦 ) → ( cos ‘ ( 𝑛 · 𝑥 ) ) = ( cos ‘ ( 𝑛 · 𝑦 ) ) )
74 simpr ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ∈ 𝐶 )
75 14 adantr ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → 𝑛 ∈ ℝ )
76 34 74 sselid ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ∈ ℝ )
77 75 76 remulcld ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑛 · 𝑦 ) ∈ ℝ )
78 77 recoscld ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( cos ‘ ( 𝑛 · 𝑦 ) ) ∈ ℝ )
79 70 73 74 78 fvmptd ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) = ( cos ‘ ( 𝑛 · 𝑦 ) ) )
80 79 fveq2d ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) = ( abs ‘ ( cos ‘ ( 𝑛 · 𝑦 ) ) ) )
81 abscosbd ⊢ ( ( 𝑛 · 𝑦 ) ∈ ℝ → ( abs ‘ ( cos ‘ ( 𝑛 · 𝑦 ) ) ) ≤ 1 )
82 77 81 syl ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( abs ‘ ( cos ‘ ( 𝑛 · 𝑦 ) ) ) ≤ 1 )
83 80 82 eqbrtrd ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ 𝐶 ) → ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 )
84 69 83 syldan ⊢ ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) → ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 )
85 84 ralrimiva ⊢ ( 𝑛 ∈ ℕ0 → ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 )
86 breq2 ⊢ ( 𝑏 = 1 → ( ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 ↔ ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 ) )
87 86 ralbidv ⊢ ( 𝑏 = 1 → ( ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 ↔ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 ) )
88 87 rspcev ⊢ ( ( 1 ∈ ℝ ∧ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 1 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 )
89 57 85 88 sylancr ⊢ ( 𝑛 ∈ ℕ0 → ∃ 𝑏 ∈ ℝ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 )
90 89 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 )
91 bddmulibl ⊢ ( ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 ∧ ∃ 𝑏 ∈ ℝ ∀ 𝑦 ∈ dom ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ( abs ‘ ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ‘ 𝑦 ) ) ≤ 𝑏 ) → ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∘f · ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ) ∈ 𝐿1 )
92 49 56 90 91 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑥 ∈ 𝐶 ↦ ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ∘f · ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ) ∈ 𝐿1 )
93 31 92 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐶 ↦ ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) ) ∈ 𝐿1 )
94 20 93 itgrecl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 ∈ ℝ )
95 pire ⊢ π ∈ ℝ
96 95 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → π ∈ ℝ )
97 0re ⊢ 0 ∈ ℝ
98 pipos ⊢ 0 < π
99 97 98 gtneii ⊢ π ≠ 0
100 99 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → π ≠ 0 )
101 94 96 100 redivcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 / π ) ∈ ℝ )
102 101 4 fmptd ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℝ )
103 102 5 ffvelcdmd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑁 ) ∈ ℝ )
104 5 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) )
105 eleq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 ∈ ℕ0 ↔ 𝑁 ∈ ℕ0 ) )
106 105 anbi2d ⊢ ( 𝑛 = 𝑁 → ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) ↔ ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) ) )
107 simpl ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 ∈ 𝐶 ) → 𝑛 = 𝑁 )
108 107 oveq1d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑛 · 𝑥 ) = ( 𝑁 · 𝑥 ) )
109 108 fveq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 ∈ 𝐶 ) → ( cos ‘ ( 𝑛 · 𝑥 ) ) = ( cos ‘ ( 𝑁 · 𝑥 ) ) )
110 109 oveq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 ∈ 𝐶 ) → ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) )
111 110 itgeq2dv ⊢ ( 𝑛 = 𝑁 → ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 = ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 )
112 111 eleq1d ⊢ ( 𝑛 = 𝑁 → ( ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 ∈ ℝ ↔ ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ∈ ℝ ) )
113 106 112 imbi12d ⊢ ( 𝑛 = 𝑁 → ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑛 · 𝑥 ) ) ) d 𝑥 ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ∈ ℝ ) ) )
114 113 94 vtoclg ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ∈ ℝ ) )
115 5 104 114 sylc ⊢ ( 𝜑 → ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ∈ ℝ )
116 103 55 115 jca31 ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 𝑁 ) ∈ ℝ ∧ ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 ) ∧ ∫ 𝐶 ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ∈ ℝ ) )