Theorem coscn

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

	Ref	Expression
Assertion	coscn	⊢ cos ∈ ( ℂ –cn→ ℂ )

Proof

Step	Hyp	Ref	Expression
1		df-cos	⊢ cos = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) / 2 ) )
2		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
3	2	addcn	⊢ + ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
4	3	a1i	⊢ ( ⊤ → + ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
5		efcn	⊢ exp ∈ ( ℂ –cn→ ℂ )
6	5	a1i	⊢ ( ⊤ → exp ∈ ( ℂ –cn→ ℂ ) )
7		ax-icn	⊢ i ∈ ℂ
8		eqid	⊢ ( 𝑥 ∈ ℂ ↦ ( i · 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ( i · 𝑥 ) )
9	8	mulc1cncf	⊢ ( i ∈ ℂ → ( 𝑥 ∈ ℂ ↦ ( i · 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )
10	7 9	mp1i	⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( i · 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )
11	6 10	cncfmpt1f	⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( exp ‘ ( i · 𝑥 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
12		negicn	⊢ - i ∈ ℂ
13		eqid	⊢ ( 𝑥 ∈ ℂ ↦ ( - i · 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ( - i · 𝑥 ) )
14	13	mulc1cncf	⊢ ( - i ∈ ℂ → ( 𝑥 ∈ ℂ ↦ ( - i · 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )
15	12 14	mp1i	⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( - i · 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )
16	6 15	cncfmpt1f	⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( exp ‘ ( - i · 𝑥 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
17	2 4 11 16	cncfmpt2f	⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) ) ∈ ( ℂ –cn→ ℂ ) )
18		cncff	⊢ ( ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) ) ∈ ( ℂ –cn→ ℂ ) → ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) ) : ℂ ⟶ ℂ )
19	17 18	syl	⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) ) : ℂ ⟶ ℂ )
20		eqid	⊢ ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) )
21	20	fmpt	⊢ ( ∀ 𝑥 ∈ ℂ ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) ∈ ℂ ↔ ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) ) : ℂ ⟶ ℂ )
22	19 21	sylibr	⊢ ( ⊤ → ∀ 𝑥 ∈ ℂ ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) ∈ ℂ )
23		eqidd	⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) ) )
24		eqidd	⊢ ( ⊤ → ( 𝑦 ∈ ℂ ↦ ( 𝑦 / 2 ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑦 / 2 ) ) )
25		oveq1	⊢ ( 𝑦 = ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) → ( 𝑦 / 2 ) = ( ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) / 2 ) )
26	22 23 24 25	fmptcof	⊢ ( ⊤ → ( ( 𝑦 ∈ ℂ ↦ ( 𝑦 / 2 ) ) ∘ ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) / 2 ) ) )
27		2cn	⊢ 2 ∈ ℂ
28		2ne0	⊢ 2 ≠ 0
29		eqid	⊢ ( 𝑦 ∈ ℂ ↦ ( 𝑦 / 2 ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑦 / 2 ) )
30	29	divccncf	⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 𝑦 ∈ ℂ ↦ ( 𝑦 / 2 ) ) ∈ ( ℂ –cn→ ℂ ) )
31	27 28 30	mp2an	⊢ ( 𝑦 ∈ ℂ ↦ ( 𝑦 / 2 ) ) ∈ ( ℂ –cn→ ℂ )
32	31	a1i	⊢ ( ⊤ → ( 𝑦 ∈ ℂ ↦ ( 𝑦 / 2 ) ) ∈ ( ℂ –cn→ ℂ ) )
33	17 32	cncfco	⊢ ( ⊤ → ( ( 𝑦 ∈ ℂ ↦ ( 𝑦 / 2 ) ) ∘ ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) ) ) ∈ ( ℂ –cn→ ℂ ) )
34	26 33	eqeltrrd	⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) / 2 ) ) ∈ ( ℂ –cn→ ℂ ) )
35	34	mptru	⊢ ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) / 2 ) ) ∈ ( ℂ –cn→ ℂ )
36	1 35	eqeltri	⊢ cos ∈ ( ℂ –cn→ ℂ )