Metamath Proof Explorer

Theorem fourierdlem18

Description: The function S is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem18.n ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
fourierdlem18.s ⊢ 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
Assertion fourierdlem18 ( 𝜑 → 𝑆 ∈ ( ( - π [,] π ) –cn→ ℝ ) )

Proof

Step Hyp Ref Expression
1 fourierdlem18.n ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
2 fourierdlem18.s ⊢ 𝑆 = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
3 resincncf ⊢ ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℝ )
4 cncff ⊢ ( ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℝ ) → ( sin ↾ ℝ ) : ℝ ⟶ ℝ )
5 3 4 ax-mp ⊢ ( sin ↾ ℝ ) : ℝ ⟶ ℝ
6 halfre ⊢ ( 1 / 2 ) ∈ ℝ
7 6 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
8 1 7 readdcld ⊢ ( 𝜑 → ( 𝑁 + ( 1 / 2 ) ) ∈ ℝ )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( 𝑁 + ( 1 / 2 ) ) ∈ ℝ )
10 pire ⊢ π ∈ ℝ
11 10 renegcli ⊢ - π ∈ ℝ
12 iccssre ⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ) → ( - π [,] π ) ⊆ ℝ )
13 11 10 12 mp2an ⊢ ( - π [,] π ) ⊆ ℝ
14 13 sseli ⊢ ( 𝑠 ∈ ( - π [,] π ) → 𝑠 ∈ ℝ )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → 𝑠 ∈ ℝ )
16 9 15 remulcld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( - π [,] π ) ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ∈ ℝ )
17 eqid ⊢ ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) )
18 16 17 fmptd ⊢ ( 𝜑 → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) : ( - π [,] π ) ⟶ ℝ )
19 fcompt ⊢ ( ( ( sin ↾ ℝ ) : ℝ ⟶ ℝ ∧ ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) : ( - π [,] π ) ⟶ ℝ ) → ( ( sin ↾ ℝ ) ∘ ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ) = ( 𝑥 ∈ ( - π [,] π ) ↦ ( ( sin ↾ ℝ ) ‘ ( ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ‘ 𝑥 ) ) ) )
20 5 18 19 sylancr ⊢ ( 𝜑 → ( ( sin ↾ ℝ ) ∘ ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ) = ( 𝑥 ∈ ( - π [,] π ) ↦ ( ( sin ↾ ℝ ) ‘ ( ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ‘ 𝑥 ) ) ) )
21 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) = ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
22 oveq2 ⊢ ( 𝑠 = 𝑥 → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) ∧ 𝑠 = 𝑥 ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) → 𝑥 ∈ ( - π [,] π ) )
25 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) → ( 𝑁 + ( 1 / 2 ) ) ∈ ℝ )
26 13 24 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) → 𝑥 ∈ ℝ )
27 25 26 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ∈ ℝ )
28 21 23 24 27 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) → ( ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ‘ 𝑥 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) )
29 28 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) → ( ( sin ↾ ℝ ) ‘ ( ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ‘ 𝑥 ) ) = ( ( sin ↾ ℝ ) ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) )
30 29 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] π ) ↦ ( ( sin ↾ ℝ ) ‘ ( ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( - π [,] π ) ↦ ( ( sin ↾ ℝ ) ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) ) )
31 fvres ⊢ ( ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ∈ ℝ → ( ( sin ↾ ℝ ) ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) )
32 27 31 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ) → ( ( sin ↾ ℝ ) ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) )
33 32 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] π ) ↦ ( ( sin ↾ ℝ ) ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) ) = ( 𝑥 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) ) )
34 oveq2 ⊢ ( 𝑥 = 𝑠 → ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) = ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) )
35 34 fveq2d ⊢ ( 𝑥 = 𝑠 → ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) = ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
36 35 cbvmptv ⊢ ( 𝑥 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) ) = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) )
37 36 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑥 ) ) ) = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ) )
38 30 33 37 3eqtrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] π ) ↦ ( ( sin ↾ ℝ ) ‘ ( ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ‘ 𝑥 ) ) ) = ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ) )
39 2 eqcomi ⊢ ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ) = 𝑆
40 39 a1i ⊢ ( 𝜑 → ( 𝑠 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ) = 𝑆 )
41 20 38 40 3eqtrrd ⊢ ( 𝜑 → 𝑆 = ( ( sin ↾ ℝ ) ∘ ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ) )
42 ax-resscn ⊢ ℝ ⊆ ℂ
43 13 42 sstri ⊢ ( - π [,] π ) ⊆ ℂ
44 43 a1i ⊢ ( 𝜑 → ( - π [,] π ) ⊆ ℂ )
45 1 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
46 halfcn ⊢ ( 1 / 2 ) ∈ ℂ
47 46 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
48 45 47 addcld ⊢ ( 𝜑 → ( 𝑁 + ( 1 / 2 ) ) ∈ ℂ )
49 ssid ⊢ ℂ ⊆ ℂ
50 49 a1i ⊢ ( 𝜑 → ℂ ⊆ ℂ )
51 44 48 50 constcncfg ⊢ ( 𝜑 → ( 𝑠 ∈ ( - π [,] π ) ↦ ( 𝑁 + ( 1 / 2 ) ) ) ∈ ( ( - π [,] π ) –cn→ ℂ ) )
52 44 50 idcncfg ⊢ ( 𝜑 → ( 𝑠 ∈ ( - π [,] π ) ↦ 𝑠 ) ∈ ( ( - π [,] π ) –cn→ ℂ ) )
53 51 52 mulcncf ⊢ ( 𝜑 → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ∈ ( ( - π [,] π ) –cn→ ℂ ) )
54 ssid ⊢ ( - π [,] π ) ⊆ ( - π [,] π )
55 54 a1i ⊢ ( 𝜑 → ( - π [,] π ) ⊆ ( - π [,] π ) )
56 42 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
57 17 53 55 56 16 cncfmptssg ⊢ ( 𝜑 → ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ∈ ( ( - π [,] π ) –cn→ ℝ ) )
58 3 a1i ⊢ ( 𝜑 → ( sin ↾ ℝ ) ∈ ( ℝ –cn→ ℝ ) )
59 57 58 cncfco ⊢ ( 𝜑 → ( ( sin ↾ ℝ ) ∘ ( 𝑠 ∈ ( - π [,] π ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑠 ) ) ) ∈ ( ( - π [,] π ) –cn→ ℝ ) )
60 41 59 eqeltrd ⊢ ( 𝜑 → 𝑆 ∈ ( ( - π [,] π ) –cn→ ℝ ) )