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→ ℂ )