Theorem acosval

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

	Ref	Expression
Assertion	acosval	$$⊢A\in ℂ\to arccos\left(A\right)=\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢x=A\to arcsin\left(x\right)=arcsin\left(A\right)$$
2	1	oveq2d	$$⊢x=A\to \left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(x\right)=\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(A\right)$$
3		df-acos	$$⊢arccos=\left(x\in ℂ⟼\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(x\right)\right)$$
4		ovex	$$⊢\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(A\right)\in \mathrm{V}$$
5	2 3 4	fvmpt	$$⊢A\in ℂ\to arccos\left(A\right)=\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(A\right)$$