Theorem sinf

Description: Domain and codomain of the sine function. (Contributed by Paul Chapman, 22-Oct-2007) (Revised by Mario Carneiro, 30-Apr-2014)

	Ref	Expression
Assertion	sinf	$$⊢\sin :ℂ⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		df-sin	$$⊢\sin =\left(x\in ℂ⟼\frac{{\mathrm{e}}^{\mathrm{i}x}-{\mathrm{e}}^{\left(-\mathrm{i}\right)x}}{2\mathrm{i}}\right)$$
2		ax-icn	$$⊢\mathrm{i}\in ℂ$$
3		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge x\in ℂ\right)\to \mathrm{i}x\in ℂ$$
4	2 3	mpan	$$⊢x\in ℂ\to \mathrm{i}x\in ℂ$$
5		efcl	$$⊢\mathrm{i}x\in ℂ\to {\mathrm{e}}^{\mathrm{i}x}\in ℂ$$
6	4 5	syl	$$⊢x\in ℂ\to {\mathrm{e}}^{\mathrm{i}x}\in ℂ$$
7		negicn	$$⊢-\mathrm{i}\in ℂ$$
8		mulcl	$$⊢\left(-\mathrm{i}\in ℂ\wedge x\in ℂ\right)\to \left(-\mathrm{i}\right)x\in ℂ$$
9	7 8	mpan	$$⊢x\in ℂ\to \left(-\mathrm{i}\right)x\in ℂ$$
10		efcl	$$⊢\left(-\mathrm{i}\right)x\in ℂ\to {\mathrm{e}}^{\left(-\mathrm{i}\right)x}\in ℂ$$
11	9 10	syl	$$⊢x\in ℂ\to {\mathrm{e}}^{\left(-\mathrm{i}\right)x}\in ℂ$$
12	6 11	subcld	$$⊢x\in ℂ\to {\mathrm{e}}^{\mathrm{i}x}-{\mathrm{e}}^{\left(-\mathrm{i}\right)x}\in ℂ$$
13		2mulicn	$$⊢2\mathrm{i}\in ℂ$$
14		2muline0	$$⊢2\mathrm{i}\ne 0$$
15		divcl	$$⊢\left({\mathrm{e}}^{\mathrm{i}x}-{\mathrm{e}}^{\left(-\mathrm{i}\right)x}\in ℂ\wedge 2\mathrm{i}\in ℂ\wedge 2\mathrm{i}\ne 0\right)\to \frac{{\mathrm{e}}^{\mathrm{i}x}-{\mathrm{e}}^{\left(-\mathrm{i}\right)x}}{2\mathrm{i}}\in ℂ$$
16	13 14 15	mp3an23	$$⊢{\mathrm{e}}^{\mathrm{i}x}-{\mathrm{e}}^{\left(-\mathrm{i}\right)x}\in ℂ\to \frac{{\mathrm{e}}^{\mathrm{i}x}-{\mathrm{e}}^{\left(-\mathrm{i}\right)x}}{2\mathrm{i}}\in ℂ$$
17	12 16	syl	$$⊢x\in ℂ\to \frac{{\mathrm{e}}^{\mathrm{i}x}-{\mathrm{e}}^{\left(-\mathrm{i}\right)x}}{2\mathrm{i}}\in ℂ$$
18	1 17	fmpti	$$⊢\sin :ℂ⟶ℂ$$