This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sincn

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

Ref Expression
Assertion sincn sin ∈ ( ℂ –cn→ ℂ )

Proof

Step Hyp Ref Expression
1 df-sin ⊢ sin = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) )
2 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
3 2 subcn ⊢ − ∈ ( ( ( 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 · i ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑦 / ( 2 · i ) ) ) )
25 oveq1 ⊢ ( 𝑦 = ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) → ( 𝑦 / ( 2 · i ) ) = ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) )
26 22 23 24 25 fmptcof ⊢ ( ⊤ → ( ( 𝑦 ∈ ℂ ↦ ( 𝑦 / ( 2 · i ) ) ) ∘ ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) ) )
27 2mulicn ⊢ ( 2 · i ) ∈ ℂ
28 2muline0 ⊢ ( 2 · i ) ≠ 0
29 eqid ⊢ ( 𝑦 ∈ ℂ ↦ ( 𝑦 / ( 2 · i ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑦 / ( 2 · i ) ) )
30 29 divccncf ⊢ ( ( ( 2 · i ) ∈ ℂ ∧ ( 2 · i ) ≠ 0 ) → ( 𝑦 ∈ ℂ ↦ ( 𝑦 / ( 2 · i ) ) ) ∈ ( ℂ –cn→ ℂ ) )
31 27 28 30 mp2an ⊢ ( 𝑦 ∈ ℂ ↦ ( 𝑦 / ( 2 · i ) ) ) ∈ ( ℂ –cn→ ℂ )
32 31 a1i ⊢ ( ⊤ → ( 𝑦 ∈ ℂ ↦ ( 𝑦 / ( 2 · i ) ) ) ∈ ( ℂ –cn→ ℂ ) )
33 17 32 cncfco ⊢ ( ⊤ → ( ( 𝑦 ∈ ℂ ↦ ( 𝑦 / ( 2 · i ) ) ) ∘ ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ) ) ∈ ( ℂ –cn→ ℂ ) )
34 26 33 eqeltrrd ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) ) ∈ ( ℂ –cn→ ℂ ) )
35 34 mptru ⊢ ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) ) ∈ ( ℂ –cn→ ℂ )
36 1 35 eqeltri ⊢ sin ∈ ( ℂ –cn→ ℂ )