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 : ℂ ⟶ ℂ$

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

Metamath Proof Explorer