Theorem asin1half

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

	Ref	Expression
Assertion	asin1half	|- ( arcsin ` ( 1 / 2 ) ) = ( _pi / 6 )

Proof

Step	Hyp	Ref	Expression
1		sincos6thpi	|- ( ( sin ` ( _pi / 6 ) ) = ( 1 / 2 ) /\ ( cos ` ( _pi / 6 ) ) = ( ( sqrt ` 3 ) / 2 ) )
2	1	simpli	|- ( sin ` ( _pi / 6 ) ) = ( 1 / 2 )
3	2	fveq2i	|- ( arcsin ` ( sin ` ( _pi / 6 ) ) ) = ( arcsin ` ( 1 / 2 ) )
4		pire	|- _pi e. RR
5		6re	|- 6 e. RR
6		0re	|- 0 e. RR
7		6pos	|- 0 < 6
8	6 7	gtneii	|- 6 =/= 0
9	4 5 8	redivcli	|- ( _pi / 6 ) e. RR
10		neghalfpire	|- -u ( _pi / 2 ) e. RR
11		halfpire	|- ( _pi / 2 ) e. RR
12		2re	|- 2 e. RR
13		pipos	|- 0 < _pi
14		2pos	|- 0 < 2
15	4 12 13 14	divgt0ii	|- 0 < ( _pi / 2 )
16		lt0neg2	|- ( ( _pi / 2 ) e. RR -> ( 0 < ( _pi / 2 ) <-> -u ( _pi / 2 ) < 0 ) )
17	15 16	mpbii	|- ( ( _pi / 2 ) e. RR -> -u ( _pi / 2 ) < 0 )
18	11 17	ax-mp	|- -u ( _pi / 2 ) < 0
19	4 5 13 7	divgt0ii	|- 0 < ( _pi / 6 )
20	10 6 9 18 19	lttrii	|- -u ( _pi / 2 ) < ( _pi / 6 )
21	10 9 20	ltleii	|- -u ( _pi / 2 ) <_ ( _pi / 6 )
22		2lt6	|- 2 < 6
23		2rp	|- 2 e. RR+
24	23	a1i	|- ( T. -> 2 e. RR+ )
25		6rp	|- 6 e. RR+
26	25	a1i	|- ( T. -> 6 e. RR+ )
27		pirp	|- _pi e. RR+
28	27	a1i	|- ( T. -> _pi e. RR+ )
29	24 26 28	ltdiv2d	|- ( T. -> ( 2 < 6 <-> ( _pi / 6 ) < ( _pi / 2 ) ) )
30	22 29	mpbii	|- ( T. -> ( _pi / 6 ) < ( _pi / 2 ) )
31	30	mptru	|- ( _pi / 6 ) < ( _pi / 2 )
32	9 11 31	ltleii	|- ( _pi / 6 ) <_ ( _pi / 2 )
33	10 11	elicc2i	|- ( ( _pi / 6 ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) <-> ( ( _pi / 6 ) e. RR /\ -u ( _pi / 2 ) <_ ( _pi / 6 ) /\ ( _pi / 6 ) <_ ( _pi / 2 ) ) )
34	9 21 32 33	mpbir3an	|- ( _pi / 6 ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) )
35		reasinsin	|- ( ( _pi / 6 ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( arcsin ` ( sin ` ( _pi / 6 ) ) ) = ( _pi / 6 ) )
36	34 35	ax-mp	|- ( arcsin ` ( sin ` ( _pi / 6 ) ) ) = ( _pi / 6 )
37	3 36	eqtr3i	|- ( arcsin ` ( 1 / 2 ) ) = ( _pi / 6 )