Theorem acos1

Description: The arcsine of 1 is _pi / 2 . (Contributed by Mario Carneiro, 2-Apr-2015)

	Ref	Expression
Assertion	acos1	$$⊢arccos\left(1\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$$⊢1\in ℂ$$
2		acosval	$$⊢1\in ℂ\to arccos\left(1\right)=\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(1\right)$$
3	1 2	ax-mp	$$⊢arccos\left(1\right)=\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(1\right)$$
4		asin1	$$⊢arcsin\left(1\right)=\frac{\mathrm{\pi }}{2}$$
5	4	oveq2i	$$⊢\left(\frac{\mathrm{\pi }}{2}\right)-arcsin\left(1\right)=\left(\frac{\mathrm{\pi }}{2}\right)-\left(\frac{\mathrm{\pi }}{2}\right)$$
6		picn	$$⊢\mathrm{\pi }\in ℂ$$
7		halfcl	$$⊢\mathrm{\pi }\in ℂ\to \frac{\mathrm{\pi }}{2}\in ℂ$$
8	6 7	ax-mp	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ$$
9	8	subidi	$$⊢\left(\frac{\mathrm{\pi }}{2}\right)-\left(\frac{\mathrm{\pi }}{2}\right)=0$$
10	3 5 9	3eqtri	$$⊢arccos\left(1\right)=0$$