Metamath Proof Explorer

Theorem fourierdlem21

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

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

Proof

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