sincn

Description: Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007) (Revised by Mario Carneiro, 3-Sep-2014)

		Ref	Expression
	Assertion	sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		df-sin	$⊢ \sin = (x \in ℂ ⟼ \frac{e^{i x} - e^{(- i) x}}{2 i})$
2		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
3	2	subcn	$⊢ - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
4	3	a1i	$⊢ ⊤ \to - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
5		efcn	$⊢ \exp : ℂ \underset{cn}{⟶} ℂ$
6	5	a1i	$⊢ ⊤ \to \exp : ℂ \underset{cn}{⟶} ℂ$
7		ax-icn	$⊢ i \in ℂ$
8		eqid	$⊢ (x \in ℂ ⟼ i x) = (x \in ℂ ⟼ i x)$
9	8	mulc1cncf	$⊢ i \in ℂ \to (x \in ℂ ⟼ i x) : ℂ \underset{cn}{⟶} ℂ$
10	7 9	mp1i	$⊢ ⊤ \to (x \in ℂ ⟼ i x) : ℂ \underset{cn}{⟶} ℂ$
11	6 10	cncfmpt1f	$⊢ ⊤ \to (x \in ℂ ⟼ e^{i x}) : ℂ \underset{cn}{⟶} ℂ$
12		negicn	$⊢ - i \in ℂ$
13		eqid	$⊢ (x \in ℂ ⟼ (- i) x) = (x \in ℂ ⟼ (- i) x)$
14	13	mulc1cncf	$⊢ - i \in ℂ \to (x \in ℂ ⟼ (- i) x) : ℂ \underset{cn}{⟶} ℂ$
15	12 14	mp1i	$⊢ ⊤ \to (x \in ℂ ⟼ (- i) x) : ℂ \underset{cn}{⟶} ℂ$
16	6 15	cncfmpt1f	$⊢ ⊤ \to (x \in ℂ ⟼ e^{(- i) x}) : ℂ \underset{cn}{⟶} ℂ$
17	2 4 11 16	cncfmpt2f	$⊢ ⊤ \to (x \in ℂ ⟼ e^{i x} - e^{(- i) x}) : ℂ \underset{cn}{⟶} ℂ$
18		cncff	$⊢ (x \in ℂ ⟼ e^{i x} - e^{(- i) x}) : ℂ \underset{cn}{⟶} ℂ \to (x \in ℂ ⟼ e^{i x} - e^{(- i) x}) : ℂ ⟶ ℂ$
19	17 18	syl	$⊢ ⊤ \to (x \in ℂ ⟼ e^{i x} - e^{(- i) x}) : ℂ ⟶ ℂ$
20		eqid	$⊢ (x \in ℂ ⟼ e^{i x} - e^{(- i) x}) = (x \in ℂ ⟼ e^{i x} - e^{(- i) x})$
21	20	fmpt	$⊢ \forall x \in ℂ e^{i x} - e^{(- i) x} \in ℂ \leftrightarrow (x \in ℂ ⟼ e^{i x} - e^{(- i) x}) : ℂ ⟶ ℂ$
22	19 21	sylibr	$⊢ ⊤ \to \forall x \in ℂ e^{i x} - e^{(- i) x} \in ℂ$
23		eqidd	$⊢ ⊤ \to (x \in ℂ ⟼ e^{i x} - e^{(- i) x}) = (x \in ℂ ⟼ e^{i x} - e^{(- i) x})$
24		eqidd	$⊢ ⊤ \to (y \in ℂ ⟼ \frac{y}{2 i}) = (y \in ℂ ⟼ \frac{y}{2 i})$
25		oveq1	$⊢ y = e^{i x} - e^{(- i) x} \to \frac{y}{2 i} = \frac{e^{i x} - e^{(- i) x}}{2 i}$
26	22 23 24 25	fmptcof	$⊢ ⊤ \to (y \in ℂ ⟼ \frac{y}{2 i}) \circ (x \in ℂ ⟼ e^{i x} - e^{(- i) x}) = (x \in ℂ ⟼ \frac{e^{i x} - e^{(- i) x}}{2 i})$
27		2mulicn	$⊢ 2 i \in ℂ$
28		2muline0	$⊢ 2 i \neq 0$
29		eqid	$⊢ (y \in ℂ ⟼ \frac{y}{2 i}) = (y \in ℂ ⟼ \frac{y}{2 i})$
30	29	divccncf	$⊢ (2 i \in ℂ \land 2 i \neq 0) \to (y \in ℂ ⟼ \frac{y}{2 i}) : ℂ \underset{cn}{⟶} ℂ$
31	27 28 30	mp2an	$⊢ (y \in ℂ ⟼ \frac{y}{2 i}) : ℂ \underset{cn}{⟶} ℂ$
32	31	a1i	$⊢ ⊤ \to (y \in ℂ ⟼ \frac{y}{2 i}) : ℂ \underset{cn}{⟶} ℂ$
33	17 32	cncfco	$⊢ ⊤ \to ((y \in ℂ ⟼ \frac{y}{2 i}) \circ (x \in ℂ ⟼ e^{i x} - e^{(- i) x})) : ℂ \underset{cn}{⟶} ℂ$
34	26 33	eqeltrrd	$⊢ ⊤ \to (x \in ℂ ⟼ \frac{e^{i x} - e^{(- i) x}}{2 i}) : ℂ \underset{cn}{⟶} ℂ$
35	34	mptru	$⊢ (x \in ℂ ⟼ \frac{e^{i x} - e^{(- i) x}}{2 i}) : ℂ \underset{cn}{⟶} ℂ$
36	1 35	eqeltri	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem sincn

Proof