Metamath Proof Explorer

Theorem fourierdlem18

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

Ref Expression
Hypotheses fourierdlem18.n ⊢ φ → N ∈ ℝ
fourierdlem18.s ⊢ S = s ∈ − π π ⟼ sin ⁡ N + 1 2 ⁢ s
Assertion fourierdlem18 ⊢ φ → S : − π π ⟶cn ℝ

Proof

Step Hyp Ref Expression
1 fourierdlem18.n ⊢ φ → N ∈ ℝ
2 fourierdlem18.s ⊢ S = s ∈ − π π ⟼ sin ⁡ N + 1 2 ⁢ s
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 ⊢ φ → N + 1 2 ∈ ℝ
9 8 adantr ⊢ φ ∧ s ∈ − π π → N + 1 2 ∈ ℝ
10 pire ⊢ π ∈ ℝ
11 10 renegcli ⊢ − π ∈ ℝ
12 iccssre ⊢ − π ∈ ℝ ∧ π ∈ ℝ → − π π ⊆ ℝ
13 11 10 12 mp2an ⊢ − π π ⊆ ℝ
14 13 sseli ⊢ s ∈ − π π → s ∈ ℝ
15 14 adantl ⊢ φ ∧ s ∈ − π π → s ∈ ℝ
16 9 15 remulcld ⊢ φ ∧ s ∈ − π π → N + 1 2 ⁢ s ∈ ℝ
17 eqid ⊢ s ∈ − π π ⟼ N + 1 2 ⁢ s = s ∈ − π π ⟼ N + 1 2 ⁢ s
18 16 17 fmptd ⊢ φ → s ∈ − π π ⟼ N + 1 2 ⁢ s : − π π ⟶ ℝ
19 fcompt ⊢ sin ↾ ℝ : ℝ ⟶ ℝ ∧ s ∈ − π π ⟼ N + 1 2 ⁢ s : − π π ⟶ ℝ → sin ↾ ℝ ∘ s ∈ − π π ⟼ N + 1 2 ⁢ s = x ∈ − π π ⟼ sin ↾ ℝ ⁡ s ∈ − π π ⟼ N + 1 2 ⁢ s ⁡ x
20 5 18 19 sylancr ⊢ φ → sin ↾ ℝ ∘ s ∈ − π π ⟼ N + 1 2 ⁢ s = x ∈ − π π ⟼ sin ↾ ℝ ⁡ s ∈ − π π ⟼ N + 1 2 ⁢ s ⁡ x
21 eqidd ⊢ φ ∧ x ∈ − π π → s ∈ − π π ⟼ N + 1 2 ⁢ s = s ∈ − π π ⟼ N + 1 2 ⁢ s
22 oveq2 ⊢ s = x → N + 1 2 ⁢ s = N + 1 2 ⁢ x
23 22 adantl ⊢ φ ∧ x ∈ − π π ∧ s = x → N + 1 2 ⁢ s = N + 1 2 ⁢ x
24 simpr ⊢ φ ∧ x ∈ − π π → x ∈ − π π
25 8 adantr ⊢ φ ∧ x ∈ − π π → N + 1 2 ∈ ℝ
26 13 24 sseldi ⊢ φ ∧ x ∈ − π π → x ∈ ℝ
27 25 26 remulcld ⊢ φ ∧ x ∈ − π π → N + 1 2 ⁢ x ∈ ℝ
28 21 23 24 27 fvmptd ⊢ φ ∧ x ∈ − π π → s ∈ − π π ⟼ N + 1 2 ⁢ s ⁡ x = N + 1 2 ⁢ x
29 28 fveq2d ⊢ φ ∧ x ∈ − π π → sin ↾ ℝ ⁡ s ∈ − π π ⟼ N + 1 2 ⁢ s ⁡ x = sin ↾ ℝ ⁡ N + 1 2 ⁢ x
30 29 mpteq2dva ⊢ φ → x ∈ − π π ⟼ sin ↾ ℝ ⁡ s ∈ − π π ⟼ N + 1 2 ⁢ s ⁡ x = x ∈ − π π ⟼ sin ↾ ℝ ⁡ N + 1 2 ⁢ x
31 fvres ⊢ N + 1 2 ⁢ x ∈ ℝ → sin ↾ ℝ ⁡ N + 1 2 ⁢ x = sin ⁡ N + 1 2 ⁢ x
32 27 31 syl ⊢ φ ∧ x ∈ − π π → sin ↾ ℝ ⁡ N + 1 2 ⁢ x = sin ⁡ N + 1 2 ⁢ x
33 32 mpteq2dva ⊢ φ → x ∈ − π π ⟼ sin ↾ ℝ ⁡ N + 1 2 ⁢ x = x ∈ − π π ⟼ sin ⁡ N + 1 2 ⁢ x
34 oveq2 ⊢ x = s → N + 1 2 ⁢ x = N + 1 2 ⁢ s
35 34 fveq2d ⊢ x = s → sin ⁡ N + 1 2 ⁢ x = sin ⁡ N + 1 2 ⁢ s
36 35 cbvmptv ⊢ x ∈ − π π ⟼ sin ⁡ N + 1 2 ⁢ x = s ∈ − π π ⟼ sin ⁡ N + 1 2 ⁢ s
37 36 a1i ⊢ φ → x ∈ − π π ⟼ sin ⁡ N + 1 2 ⁢ x = s ∈ − π π ⟼ sin ⁡ N + 1 2 ⁢ s
38 30 33 37 3eqtrd ⊢ φ → x ∈ − π π ⟼ sin ↾ ℝ ⁡ s ∈ − π π ⟼ N + 1 2 ⁢ s ⁡ x = s ∈ − π π ⟼ sin ⁡ N + 1 2 ⁢ s
39 2 eqcomi ⊢ s ∈ − π π ⟼ sin ⁡ N + 1 2 ⁢ s = S
40 39 a1i ⊢ φ → s ∈ − π π ⟼ sin ⁡ N + 1 2 ⁢ s = S
41 20 38 40 3eqtrrd ⊢ φ → S = sin ↾ ℝ ∘ s ∈ − π π ⟼ N + 1 2 ⁢ s
42 ax-resscn ⊢ ℝ ⊆ ℂ
43 13 42 sstri ⊢ − π π ⊆ ℂ
44 43 a1i ⊢ φ → − π π ⊆ ℂ
45 1 recnd ⊢ φ → N ∈ ℂ
46 halfcn ⊢ 1 2 ∈ ℂ
47 46 a1i ⊢ φ → 1 2 ∈ ℂ
48 45 47 addcld ⊢ φ → N + 1 2 ∈ ℂ
49 ssid ⊢ ℂ ⊆ ℂ
50 49 a1i ⊢ φ → ℂ ⊆ ℂ
51 44 48 50 constcncfg ⊢ φ → s ∈ − π π ⟼ N + 1 2 : − π π ⟶cn ℂ
52 44 50 idcncfg ⊢ φ → s ∈ − π π ⟼ s : − π π ⟶cn ℂ
53 51 52 mulcncf ⊢ φ → s ∈ − π π ⟼ N + 1 2 ⁢ s : − π π ⟶cn ℂ
54 ssid ⊢ − π π ⊆ − π π
55 54 a1i ⊢ φ → − π π ⊆ − π π
56 42 a1i ⊢ φ → ℝ ⊆ ℂ
57 17 53 55 56 16 cncfmptssg ⊢ φ → s ∈ − π π ⟼ N + 1 2 ⁢ s : − π π ⟶cn ℝ
58 3 a1i ⊢ φ → sin ↾ ℝ : ℝ ⟶cn ℝ
59 57 58 cncfco ⊢ φ → sin ↾ ℝ ∘ s ∈ − π π ⟼ N + 1 2 ⁢ s : − π π ⟶cn ℝ
60 41 59 eqeltrd ⊢ φ → S : − π π ⟶cn ℝ