fourierdlem5

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

		Ref	Expression
	Hypothesis	fourierdlem5.1	$⊢ S = (x \in [- π, π] ⟼ \sin (X + (\frac{1}{2})) x)$
	Assertion	fourierdlem5	$⊢ X \in ℝ \to S : [- π, π] ⟶ ℝ$

Step	Hyp	Ref	Expression
1		fourierdlem5.1	$⊢ S = (x \in [- π, π] ⟼ \sin (X + (\frac{1}{2})) x)$
2		simpl	$⊢ (X \in ℝ \land x \in [- π, π]) \to X \in ℝ$
3		1red	$⊢ (X \in ℝ \land x \in [- π, π]) \to 1 \in ℝ$
4	3	rehalfcld	$⊢ (X \in ℝ \land x \in [- π, π]) \to \frac{1}{2} \in ℝ$
5	2 4	readdcld	$⊢ (X \in ℝ \land x \in [- π, π]) \to X + (\frac{1}{2}) \in ℝ$
6		pire	$⊢ π \in ℝ$
7	6	renegcli	$⊢ - π \in ℝ$
8		iccssre	$⊢ (- π \in ℝ \land π \in ℝ) \to [- π, π] \subseteq ℝ$
9	7 6 8	mp2an	$⊢ [- π, π] \subseteq ℝ$
10	9	sseli	$⊢ x \in [- π, π] \to x \in ℝ$
11	10	adantl	$⊢ (X \in ℝ \land x \in [- π, π]) \to x \in ℝ$
12	5 11	remulcld	$⊢ (X \in ℝ \land x \in [- π, π]) \to (X + (\frac{1}{2})) x \in ℝ$
13	12	resincld	$⊢ (X \in ℝ \land x \in [- π, π]) \to \sin (X + (\frac{1}{2})) x \in ℝ$
14	13 1	fmptd	$⊢ X \in ℝ \to S : [- π, π] ⟶ ℝ$

Metamath Proof Explorer