Theorem asin1half

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

	Ref	Expression
Assertion	asin1half	⊢ ( arcsin ‘ ( 1 / 2 ) ) = ( π / 6 )

Proof

Step	Hyp	Ref	Expression
1		sincos6thpi	⊢ ( ( sin ‘ ( π / 6 ) ) = ( 1 / 2 ) ∧ ( cos ‘ ( π / 6 ) ) = ( ( √ ‘ 3 ) / 2 ) )
2	1	simpli	⊢ ( sin ‘ ( π / 6 ) ) = ( 1 / 2 )
3	2	fveq2i	⊢ ( arcsin ‘ ( sin ‘ ( π / 6 ) ) ) = ( arcsin ‘ ( 1 / 2 ) )
4		pire	⊢ π ∈ ℝ
5		6re	⊢ 6 ∈ ℝ
6		0re	⊢ 0 ∈ ℝ
7		6pos	⊢ 0 < 6
8	6 7	gtneii	⊢ 6 ≠ 0
9	4 5 8	redivcli	⊢ ( π / 6 ) ∈ ℝ
10		neghalfpire	⊢ - ( π / 2 ) ∈ ℝ
11		halfpire	⊢ ( π / 2 ) ∈ ℝ
12		2re	⊢ 2 ∈ ℝ
13		pipos	⊢ 0 < π
14		2pos	⊢ 0 < 2
15	4 12 13 14	divgt0ii	⊢ 0 < ( π / 2 )
16		lt0neg2	⊢ ( ( π / 2 ) ∈ ℝ → ( 0 < ( π / 2 ) ↔ - ( π / 2 ) < 0 ) )
17	15 16	mpbii	⊢ ( ( π / 2 ) ∈ ℝ → - ( π / 2 ) < 0 )
18	11 17	ax-mp	⊢ - ( π / 2 ) < 0
19	4 5 13 7	divgt0ii	⊢ 0 < ( π / 6 )
20	10 6 9 18 19	lttrii	⊢ - ( π / 2 ) < ( π / 6 )
21	10 9 20	ltleii	⊢ - ( π / 2 ) ≤ ( π / 6 )
22		2lt6	⊢ 2 < 6
23		2rp	⊢ 2 ∈ ℝ+
24	23	a1i	⊢ ( ⊤ → 2 ∈ ℝ+ )
25		6rp	⊢ 6 ∈ ℝ+
26	25	a1i	⊢ ( ⊤ → 6 ∈ ℝ+ )
27		pirp	⊢ π ∈ ℝ+
28	27	a1i	⊢ ( ⊤ → π ∈ ℝ+ )
29	24 26 28	ltdiv2d	⊢ ( ⊤ → ( 2 < 6 ↔ ( π / 6 ) < ( π / 2 ) ) )
30	22 29	mpbii	⊢ ( ⊤ → ( π / 6 ) < ( π / 2 ) )
31	30	mptru	⊢ ( π / 6 ) < ( π / 2 )
32	9 11 31	ltleii	⊢ ( π / 6 ) ≤ ( π / 2 )
33	10 11	elicc2i	⊢ ( ( π / 6 ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ↔ ( ( π / 6 ) ∈ ℝ ∧ - ( π / 2 ) ≤ ( π / 6 ) ∧ ( π / 6 ) ≤ ( π / 2 ) ) )
34	9 21 32 33	mpbir3an	⊢ ( π / 6 ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) )
35		reasinsin	⊢ ( ( π / 6 ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( arcsin ‘ ( sin ‘ ( π / 6 ) ) ) = ( π / 6 ) )
36	34 35	ax-mp	⊢ ( arcsin ‘ ( sin ‘ ( π / 6 ) ) ) = ( π / 6 )
37	3 36	eqtr3i	⊢ ( arcsin ‘ ( 1 / 2 ) ) = ( π / 6 )