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

Metamath Proof Explorer

Theorem sinf

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

Ref Expression
Assertion sinf sin : ℂ ⟶ ℂ

Proof

Step Hyp Ref Expression
1 df-sin ⊢ sin = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) )
2 ax-icn ⊢ i ∈ ℂ
3 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( i · 𝑥 ) ∈ ℂ )
4 2 3 mpan ⊢ ( 𝑥 ∈ ℂ → ( i · 𝑥 ) ∈ ℂ )
5 efcl ⊢ ( ( i · 𝑥 ) ∈ ℂ → ( exp ‘ ( i · 𝑥 ) ) ∈ ℂ )
6 4 5 syl ⊢ ( 𝑥 ∈ ℂ → ( exp ‘ ( i · 𝑥 ) ) ∈ ℂ )
7 negicn ⊢ - i ∈ ℂ
8 mulcl ⊢ ( ( - i ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( - i · 𝑥 ) ∈ ℂ )
9 7 8 mpan ⊢ ( 𝑥 ∈ ℂ → ( - i · 𝑥 ) ∈ ℂ )
10 efcl ⊢ ( ( - i · 𝑥 ) ∈ ℂ → ( exp ‘ ( - i · 𝑥 ) ) ∈ ℂ )
11 9 10 syl ⊢ ( 𝑥 ∈ ℂ → ( exp ‘ ( - i · 𝑥 ) ) ∈ ℂ )
12 6 11 subcld ⊢ ( 𝑥 ∈ ℂ → ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ∈ ℂ )
13 2mulicn ⊢ ( 2 · i ) ∈ ℂ
14 2muline0 ⊢ ( 2 · i ) ≠ 0
15 divcl ⊢ ( ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ∈ ℂ ∧ ( 2 · i ) ∈ ℂ ∧ ( 2 · i ) ≠ 0 ) → ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) ∈ ℂ )
16 13 14 15 mp3an23 ⊢ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ∈ ℂ → ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) ∈ ℂ )
17 12 16 syl ⊢ ( 𝑥 ∈ ℂ → ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) ∈ ℂ )
18 1 17 fmpti ⊢ sin : ℂ ⟶ ℂ