Metamath Proof Explorer

Theorem fourierdlem5

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

Ref Expression
Hypothesis fourierdlem5.1 ⊢ S = x ∈ − π π ⟼ sin ⁡ X + 1 2 ⁢ x
Assertion fourierdlem5 ⊢ X ∈ ℝ → S : − π π ⟶ ℝ

Proof

Step Hyp Ref Expression
1 fourierdlem5.1 ⊢ S = x ∈ − π π ⟼ sin ⁡ X + 1 2 ⁢ x
2 simpl ⊢ X ∈ ℝ ∧ x ∈ − π π → X ∈ ℝ
3 1red ⊢ X ∈ ℝ ∧ x ∈ − π π → 1 ∈ ℝ
4 3 rehalfcld ⊢ X ∈ ℝ ∧ x ∈ − π π → 1 2 ∈ ℝ
5 2 4 readdcld ⊢ X ∈ ℝ ∧ x ∈ − π π → X + 1 2 ∈ ℝ
6 pire ⊢ π ∈ ℝ
7 6 renegcli ⊢ − π ∈ ℝ
8 iccssre ⊢ − π ∈ ℝ ∧ π ∈ ℝ → − π π ⊆ ℝ
9 7 6 8 mp2an ⊢ − π π ⊆ ℝ
10 9 sseli ⊢ x ∈ − π π → x ∈ ℝ
11 10 adantl ⊢ X ∈ ℝ ∧ x ∈ − π π → x ∈ ℝ
12 5 11 remulcld ⊢ X ∈ ℝ ∧ x ∈ − π π → X + 1 2 ⁢ x ∈ ℝ
13 12 resincld ⊢ X ∈ ℝ ∧ x ∈ − π π → sin ⁡ X + 1 2 ⁢ x ∈ ℝ
14 13 1 fmptd ⊢ X ∈ ℝ → S : − π π ⟶ ℝ