Theorem acosf

Description: Domain and range of the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015)

	Ref	Expression
Assertion	acosf	|- arccos : CC --> CC

Proof

Step	Hyp	Ref	Expression
1		df-acos	|- arccos = ( x e. CC |-> ( ( _pi / 2 ) - ( arcsin ` x ) ) )
2		picn	|- _pi e. CC
3		halfcl	|- ( _pi e. CC -> ( _pi / 2 ) e. CC )
4	2 3	ax-mp	|- ( _pi / 2 ) e. CC
5		asincl	|- ( x e. CC -> ( arcsin ` x ) e. CC )
6		subcl	|- ( ( ( _pi / 2 ) e. CC /\ ( arcsin ` x ) e. CC ) -> ( ( _pi / 2 ) - ( arcsin ` x ) ) e. CC )
7	4 5 6	sylancr	|- ( x e. CC -> ( ( _pi / 2 ) - ( arcsin ` x ) ) e. CC )
8	1 7	fmpti	|- arccos : CC --> CC