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

Metamath Proof Explorer

Theorem resincl

Description: The sine of a real number is real. (Contributed by NM, 30-Apr-2005)

		Ref	Expression
	Assertion	resincl	$⊢ A \in ℝ \to \sin A \in ℝ$

Step	Hyp	Ref	Expression
1		resinval	$⊢ A \in ℝ \to \sin A = ℑ (e^{i A})$
2		ax-icn	$⊢ i \in ℂ$
3		recn	$⊢ A \in ℝ \to A \in ℂ$
4		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
5	2 3 4	sylancr	$⊢ A \in ℝ \to i A \in ℂ$
6		efcl	$⊢ i A \in ℂ \to e^{i A} \in ℂ$
7	5 6	syl	$⊢ A \in ℝ \to e^{i A} \in ℂ$
8	7	imcld	$⊢ A \in ℝ \to ℑ (e^{i A}) \in ℝ$
9	1 8	eqeltrd	$⊢ A \in ℝ \to \sin A \in ℝ$