Theorem acosval

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

	Ref	Expression
Assertion	acosval	|- ( A e. CC -> ( arccos ` A ) = ( ( _pi / 2 ) - ( arcsin ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	|- ( x = A -> ( arcsin ` x ) = ( arcsin ` A ) )
2	1	oveq2d	|- ( x = A -> ( ( _pi / 2 ) - ( arcsin ` x ) ) = ( ( _pi / 2 ) - ( arcsin ` A ) ) )
3		df-acos	|- arccos = ( x e. CC |-> ( ( _pi / 2 ) - ( arcsin ` x ) ) )
4		ovex	|- ( ( _pi / 2 ) - ( arcsin ` A ) ) e. _V
5	2 3 4	fvmpt	|- ( A e. CC -> ( arccos ` A ) = ( ( _pi / 2 ) - ( arcsin ` A ) ) )