Theorem asin1half

Description: The arcsine of 1 / 2 is _pi / 6 . (Contributed by SN, 31-Aug-2025)

	Ref	Expression
Assertion	asin1half	$$⊢arcsin\left(\frac{1}{2}\right)=\frac{\mathrm{\pi }}{6}$$

Proof

Step	Hyp	Ref	Expression
1		sincos6thpi	$$⊢\left(\sin \left(\frac{\mathrm{\pi }}{6}\right)=\frac{1}{2}\wedge \cos \left(\frac{\mathrm{\pi }}{6}\right)=\frac{\sqrt{3}}{2}\right)$$
2	1	simpli	$$⊢\sin \left(\frac{\mathrm{\pi }}{6}\right)=\frac{1}{2}$$
3	2	fveq2i	$$⊢arcsin\left(\sin \left(\frac{\mathrm{\pi }}{6}\right)\right)=arcsin\left(\frac{1}{2}\right)$$
4		pire	$$⊢\mathrm{\pi }\in ℝ$$
5		6re	$$⊢6\in ℝ$$
6		0re	$$⊢0\in ℝ$$
7		6pos	$$⊢0<6$$
8	6 7	gtneii	$$⊢6\ne 0$$
9	4 5 8	redivcli	$$⊢\frac{\mathrm{\pi }}{6}\in ℝ$$
10		neghalfpire	$$⊢-\frac{\mathrm{\pi }}{2}\in ℝ$$
11		halfpire	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ$$
12		2re	$$⊢2\in ℝ$$
13		pipos	$$⊢0<\mathrm{\pi }$$
14		2pos	$$⊢0<2$$
15	4 12 13 14	divgt0ii	$$⊢0<\frac{\mathrm{\pi }}{2}$$
16		lt0neg2	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ\to \left(0<\frac{\mathrm{\pi }}{2}\leftrightarrow -\frac{\mathrm{\pi }}{2}<0\right)$$
17	15 16	mpbii	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ\to -\frac{\mathrm{\pi }}{2}<0$$
18	11 17	ax-mp	$$⊢-\frac{\mathrm{\pi }}{2}<0$$
19	4 5 13 7	divgt0ii	$$⊢0<\frac{\mathrm{\pi }}{6}$$
20	10 6 9 18 19	lttrii	$$⊢-\frac{\mathrm{\pi }}{2}<\frac{\mathrm{\pi }}{6}$$
21	10 9 20	ltleii	$$⊢-\frac{\mathrm{\pi }}{2}\le \frac{\mathrm{\pi }}{6}$$
22		2lt6	$$⊢2<6$$
23		2rp	$$⊢2\in {ℝ}^{+}$$
24	23	a1i	$$⊢\top \to 2\in {ℝ}^{+}$$
25		6rp	$$⊢6\in {ℝ}^{+}$$
26	25	a1i	$$⊢\top \to 6\in {ℝ}^{+}$$
27		pirp	$$⊢\mathrm{\pi }\in {ℝ}^{+}$$
28	27	a1i	$$⊢\top \to \mathrm{\pi }\in {ℝ}^{+}$$
29	24 26 28	ltdiv2d	$$⊢\top \to \left(2<6\leftrightarrow \frac{\mathrm{\pi }}{6}<\frac{\mathrm{\pi }}{2}\right)$$
30	22 29	mpbii	$$⊢\top \to \frac{\mathrm{\pi }}{6}<\frac{\mathrm{\pi }}{2}$$
31	30	mptru	$$⊢\frac{\mathrm{\pi }}{6}<\frac{\mathrm{\pi }}{2}$$
32	9 11 31	ltleii	$$⊢\frac{\mathrm{\pi }}{6}\le \frac{\mathrm{\pi }}{2}$$
33	10 11	elicc2i	$$⊢\frac{\mathrm{\pi }}{6}\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]\leftrightarrow \left(\frac{\mathrm{\pi }}{6}\in ℝ\wedge -\frac{\mathrm{\pi }}{2}\le \frac{\mathrm{\pi }}{6}\wedge \frac{\mathrm{\pi }}{6}\le \frac{\mathrm{\pi }}{2}\right)$$
34	9 21 32 33	mpbir3an	$$⊢\frac{\mathrm{\pi }}{6}\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]$$
35		reasinsin	$$⊢\frac{\mathrm{\pi }}{6}\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]\to arcsin\left(\sin \left(\frac{\mathrm{\pi }}{6}\right)\right)=\frac{\mathrm{\pi }}{6}$$
36	34 35	ax-mp	$$⊢arcsin\left(\sin \left(\frac{\mathrm{\pi }}{6}\right)\right)=\frac{\mathrm{\pi }}{6}$$
37	3 36	eqtr3i	$$⊢arcsin\left(\frac{1}{2}\right)=\frac{\mathrm{\pi }}{6}$$