Theorem acos1half

Description: The arccosine of 1 / 2 is _pi / 3 . (Contributed by SN, 31-Aug-2024)

	Ref	Expression
Assertion	acos1half	$$⊢arccos\left(\frac{1}{2}\right)=\frac{\mathrm{\pi }}{3}$$

Proof

Step	Hyp	Ref	Expression
1		sincos3rdpi	$$⊢\left(\sin \left(\frac{\mathrm{\pi }}{3}\right)=\frac{\sqrt{3}}{2}\wedge \cos \left(\frac{\mathrm{\pi }}{3}\right)=\frac{1}{2}\right)$$
2	1	simpri	$$⊢\cos \left(\frac{\mathrm{\pi }}{3}\right)=\frac{1}{2}$$
3	2	fveq2i	$$⊢arccos\left(\cos \left(\frac{\mathrm{\pi }}{3}\right)\right)=arccos\left(\frac{1}{2}\right)$$
4		pire	$$⊢\mathrm{\pi }\in ℝ$$
5		3re	$$⊢3\in ℝ$$
6		3ne0	$$⊢3\ne 0$$
7	4 5 6	redivcli	$$⊢\frac{\mathrm{\pi }}{3}\in ℝ$$
8	7	recni	$$⊢\frac{\mathrm{\pi }}{3}\in ℂ$$
9		rere	$$⊢\frac{\mathrm{\pi }}{3}\in ℝ\to \Re \left(\frac{\mathrm{\pi }}{3}\right)=\frac{\mathrm{\pi }}{3}$$
10	7 9	ax-mp	$$⊢\Re \left(\frac{\mathrm{\pi }}{3}\right)=\frac{\mathrm{\pi }}{3}$$
11	7	rexri	$$⊢\frac{\mathrm{\pi }}{3}\in {ℝ}^{*}$$
12		pipos	$$⊢0<\mathrm{\pi }$$
13		3pos	$$⊢0<3$$
14	4 5 12 13	divgt0ii	$$⊢0<\frac{\mathrm{\pi }}{3}$$
15		picn	$$⊢\mathrm{\pi }\in ℂ$$
16	4 12	gt0ne0ii	$$⊢\mathrm{\pi }\ne 0$$
17	15 16	dividi	$$⊢\frac{\mathrm{\pi }}{\mathrm{\pi }}=1$$
18		1lt3	$$⊢1<3$$
19	17 18	eqbrtri	$$⊢\frac{\mathrm{\pi }}{\mathrm{\pi }}<3$$
20	4 5 4 13 12	ltdiv23ii	$$⊢\frac{\mathrm{\pi }}{3}<\mathrm{\pi }\leftrightarrow \frac{\mathrm{\pi }}{\mathrm{\pi }}<3$$
21	19 20	mpbir	$$⊢\frac{\mathrm{\pi }}{3}<\mathrm{\pi }$$
22		0xr	$$⊢0\in {ℝ}^{*}$$
23	4	rexri	$$⊢\mathrm{\pi }\in {ℝ}^{*}$$
24		elioo1	$$⊢\left(0\in {ℝ}^{*}\wedge \mathrm{\pi }\in {ℝ}^{*}\right)\to \left(\frac{\mathrm{\pi }}{3}\in \left(0,\mathrm{\pi }\right)\leftrightarrow \left(\frac{\mathrm{\pi }}{3}\in {ℝ}^{*}\wedge 0<\frac{\mathrm{\pi }}{3}\wedge \frac{\mathrm{\pi }}{3}<\mathrm{\pi }\right)\right)$$
25	22 23 24	mp2an	$$⊢\frac{\mathrm{\pi }}{3}\in \left(0,\mathrm{\pi }\right)\leftrightarrow \left(\frac{\mathrm{\pi }}{3}\in {ℝ}^{*}\wedge 0<\frac{\mathrm{\pi }}{3}\wedge \frac{\mathrm{\pi }}{3}<\mathrm{\pi }\right)$$
26	11 14 21 25	mpbir3an	$$⊢\frac{\mathrm{\pi }}{3}\in \left(0,\mathrm{\pi }\right)$$
27	10 26	eqeltri	$$⊢\Re \left(\frac{\mathrm{\pi }}{3}\right)\in \left(0,\mathrm{\pi }\right)$$
28		acoscos	$$⊢\left(\frac{\mathrm{\pi }}{3}\in ℂ\wedge \Re \left(\frac{\mathrm{\pi }}{3}\right)\in \left(0,\mathrm{\pi }\right)\right)\to arccos\left(\cos \left(\frac{\mathrm{\pi }}{3}\right)\right)=\frac{\mathrm{\pi }}{3}$$
29	8 27 28	mp2an	$$⊢arccos\left(\cos \left(\frac{\mathrm{\pi }}{3}\right)\right)=\frac{\mathrm{\pi }}{3}$$
30	3 29	eqtr3i	$$⊢arccos\left(\frac{1}{2}\right)=\frac{\mathrm{\pi }}{3}$$