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 ⊢ A ∈ ℂ → sin ⁡ A ∈ ℂ

Proof

Step Hyp Ref Expression
1 sinf ⊢ sin : ℂ ⟶ ℂ
2 1 ffvelcdmi ⊢ A ∈ ℂ → sin ⁡ A ∈ ℂ