Metamath Proof Explorer

Theorem asincl

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

Ref Expression
Assertion asincl 
|- ( A e. CC -> ( arcsin ` A ) e. CC )

Proof

Step Hyp Ref Expression
1 asinf 
 |-  arcsin : CC --> CC
2 1 ffvelcdmi 
 |-  ( A e. CC -> ( arcsin ` A ) e. CC )