Theorem cosf

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

	Ref	Expression
Assertion	cosf	$$⊢\cos :ℂ⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		df-cos	$$⊢\cos =\left(x\in ℂ⟼\frac{{\mathrm{e}}^{\mathrm{i}x}+{\mathrm{e}}^{\left(-\mathrm{i}\right)x}}{2}\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	addcld	$$⊢x\in ℂ\to {\mathrm{e}}^{\mathrm{i}x}+{\mathrm{e}}^{\left(-\mathrm{i}\right)x}\in ℂ$$
13	12	halfcld	$$⊢x\in ℂ\to \frac{{\mathrm{e}}^{\mathrm{i}x}+{\mathrm{e}}^{\left(-\mathrm{i}\right)x}}{2}\in ℂ$$
14	1 13	fmpti	$$⊢\cos :ℂ⟶ℂ$$