Metamath Proof Explorer
Description: Closure of the cosine function with a complex argument. (Contributed by NM, 28Apr2005) (Revised by Mario Carneiro, 30Apr2014)


Ref 
Expression 

Assertion 
coscl 
$${\u22a2}{A}\in \u2102\to \mathrm{cos}{A}\in \u2102$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

cosf 
$${\u22a2}\mathrm{cos}:\u2102\u27f6\u2102$$ 
2 
1

ffvelrni 
$${\u22a2}{A}\in \u2102\to \mathrm{cos}{A}\in \u2102$$ 