Theorem cosacos

Description: The arccosine function is an inverse to cos . (Contributed by Mario Carneiro, 1-Apr-2015)

	Ref	Expression
Assertion	cosacos	$$⊢A\in ℂ\to \cos arccos\left(A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		acosval	$$⊢A\in ℂ\to arccos\left(A\right)=\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(A\right)$$
2	1	fveq2d	$$⊢A\in ℂ\to \cos arccos\left(A\right)=\cos \left(\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(A\right)\right)$$
3		asincl	$$⊢A\in ℂ\to arcsin\left(A\right)\in ℂ$$
4		coshalfpim	$$⊢arcsin\left(A\right)\in ℂ\to \cos \left(\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(A\right)\right)=\sin arcsin\left(A\right)$$
5	3 4	syl	$$⊢A\in ℂ\to \cos \left(\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(A\right)\right)=\sin arcsin\left(A\right)$$
6		sinasin	$$⊢A\in ℂ\to \sin arcsin\left(A\right)=A$$
7	2 5 6	3eqtrd	$$⊢A\in ℂ\to \cos arccos\left(A\right)=A$$