Theorem sinacos

Description: The sine of the arccosine of A is sqrt ( 1 - A ^ 2 ) . (Contributed by Mario Carneiro, 2-Apr-2015)

	Ref	Expression
Assertion	sinacos	$$⊢A\in ℂ\to \sin arccos\left(A\right)=\sqrt{1-A^2}$$

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	oveq2d	$$⊢A\in ℂ\to \left(\frac{\mathrm{\pi }}{2}\right)-arccos\left(A\right)=\left(\frac{\mathrm{\pi }}{2}\right)-\left(\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(A\right)\right)$$
3		picn	$$⊢\mathrm{\pi }\in ℂ$$
4		halfcl	$$⊢\mathrm{\pi }\in ℂ\to \frac{\mathrm{\pi }}{2}\in ℂ$$
5	3 4	ax-mp	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ$$
6		asincl	$$⊢A\in ℂ\to arcsin\left(A\right)\in ℂ$$
7		nncan	$$⊢\left(\frac{\mathrm{\pi }}{2}\in ℂ\wedge arcsin\left(A\right)\in ℂ\right)\to \left(\frac{\mathrm{\pi }}{2}\right)-\left(\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(A\right)\right)=arcsin\left(A\right)$$
8	5 6 7	sylancr	$$⊢A\in ℂ\to \left(\frac{\mathrm{\pi }}{2}\right)-\left(\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(A\right)\right)=arcsin\left(A\right)$$
9	2 8	eqtrd	$$⊢A\in ℂ\to \left(\frac{\mathrm{\pi }}{2}\right)-arccos\left(A\right)=arcsin\left(A\right)$$
10	9	fveq2d	$$⊢A\in ℂ\to \cos \left(\left(\frac{\mathrm{\pi }}{2}\right)-arccos\left(A\right)\right)=\cos arcsin\left(A\right)$$
11		acoscl	$$⊢A\in ℂ\to arccos\left(A\right)\in ℂ$$
12		coshalfpim	$$⊢arccos\left(A\right)\in ℂ\to \cos \left(\left(\frac{\mathrm{\pi }}{2}\right)-arccos\left(A\right)\right)=\sin arccos\left(A\right)$$
13	11 12	syl	$$⊢A\in ℂ\to \cos \left(\left(\frac{\mathrm{\pi }}{2}\right)-arccos\left(A\right)\right)=\sin arccos\left(A\right)$$
14		cosasin	$$⊢A\in ℂ\to \cos arcsin\left(A\right)=\sqrt{1-A^2}$$
15	10 13 14	3eqtr3d	$$⊢A\in ℂ\to \sin arccos\left(A\right)=\sqrt{1-A^2}$$