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	⊢ ( 𝑋 ∈ ℝ → 𝑆 : ( - π [,] π ) ⟶ ℝ )