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