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 ℝ$$

Proof

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