Database
REAL AND COMPLEX NUMBERS
Elementary trigonometry
The exponential, sine, and cosine functions
sincld
Next ⟩
coscld
Metamath Proof Explorer
Ascii
Unicode
Theorem
sincld
Description:
Closure of the sine function.
(Contributed by
Mario Carneiro
, 29-May-2016)
Ref
Expression
Hypothesis
sincld.1
⊢
φ
→
A
∈
ℂ
Assertion
sincld
⊢
φ
→
sin
⁡
A
∈
ℂ
Proof
Step
Hyp
Ref
Expression
1
sincld.1
⊢
φ
→
A
∈
ℂ
2
sincl
⊢
A
∈
ℂ
→
sin
⁡
A
∈
ℂ
3
1
2
syl
⊢
φ
→
sin
⁡
A
∈
ℂ