Metamath Proof Explorer


Theorem sincl

Description: Closure of the sine function. (Contributed by NM, 28-Apr-2005) (Revised by Mario Carneiro, 30-Apr-2014)

Ref Expression
Assertion sincl ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )

Proof

Step Hyp Ref Expression
1 sinf sin : ℂ ⟶ ℂ
2 1 ffvelrni ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )