Metamath Proof Explorer

Theorem acoscl

Description: Closure for the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion acoscl 
|- ( A e. CC -> ( arccos ` A ) e. CC )

Proof

Step Hyp Ref Expression
1 acosf 
 |-  arccos : CC --> CC
2 1 ffvelrni 
 |-  ( A e. CC -> ( arccos ` A ) e. CC )