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

Metamath Proof Explorer

Theorem fourierdlem5

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

Ref Expression
Hypothesis fourierdlem5.1 ⊢ 𝑆 = ( 𝑥 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑋 + ( 1 / 2 ) ) · 𝑥 ) ) )
Assertion fourierdlem5 ( 𝑋 ∈ ℝ → 𝑆 : ( - π [,] π ) ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 fourierdlem5.1 ⊢ 𝑆 = ( 𝑥 ∈ ( - π [,] π ) ↦ ( sin ‘ ( ( 𝑋 + ( 1 / 2 ) ) · 𝑥 ) ) )
2 simpl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑥 ∈ ( - π [,] π ) ) → 𝑋 ∈ ℝ )
3 1red ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑥 ∈ ( - π [,] π ) ) → 1 ∈ ℝ )
4 3 rehalfcld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑥 ∈ ( - π [,] π ) ) → ( 1 / 2 ) ∈ ℝ )
5 2 4 readdcld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑥 ∈ ( - π [,] π ) ) → ( 𝑋 + ( 1 / 2 ) ) ∈ ℝ )
6 pire ⊢ π ∈ ℝ
7 6 renegcli ⊢ - π ∈ ℝ
8 iccssre ⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ) → ( - π [,] π ) ⊆ ℝ )
9 7 6 8 mp2an ⊢ ( - π [,] π ) ⊆ ℝ
10 9 sseli ⊢ ( 𝑥 ∈ ( - π [,] π ) → 𝑥 ∈ ℝ )
11 10 adantl ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑥 ∈ ( - π [,] π ) ) → 𝑥 ∈ ℝ )
12 5 11 remulcld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑥 ∈ ( - π [,] π ) ) → ( ( 𝑋 + ( 1 / 2 ) ) · 𝑥 ) ∈ ℝ )
13 12 resincld ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑥 ∈ ( - π [,] π ) ) → ( sin ‘ ( ( 𝑋 + ( 1 / 2 ) ) · 𝑥 ) ) ∈ ℝ )
14 13 1 fmptd ⊢ ( 𝑋 ∈ ℝ → 𝑆 : ( - π [,] π ) ⟶ ℝ )