Theorem acosval

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

	Ref	Expression
Assertion	acosval	⊢ ( 𝐴 ∈ ℂ → ( arccos ‘ 𝐴 ) = ( ( π / 2 ) − ( arcsin ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑥 = 𝐴 → ( arcsin ‘ 𝑥 ) = ( arcsin ‘ 𝐴 ) )
2	1	oveq2d	⊢ ( 𝑥 = 𝐴 → ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) = ( ( π / 2 ) − ( arcsin ‘ 𝐴 ) ) )
3		df-acos	⊢ arccos = ( 𝑥 ∈ ℂ ↦ ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) )
4		ovex	⊢ ( ( π / 2 ) − ( arcsin ‘ 𝐴 ) ) ∈ V
5	2 3 4	fvmpt	⊢ ( 𝐴 ∈ ℂ → ( arccos ‘ 𝐴 ) = ( ( π / 2 ) − ( arcsin ‘ 𝐴 ) ) )