Theorem acos1half

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

	Ref	Expression
Assertion	acos1half	⊢ ( arccos ‘ ( 1 / 2 ) ) = ( π / 3 )

Proof

Step	Hyp	Ref	Expression
1		sincos3rdpi	⊢ ( ( sin ‘ ( π / 3 ) ) = ( ( √ ‘ 3 ) / 2 ) ∧ ( cos ‘ ( π / 3 ) ) = ( 1 / 2 ) )
2	1	simpri	⊢ ( cos ‘ ( π / 3 ) ) = ( 1 / 2 )
3	2	fveq2i	⊢ ( arccos ‘ ( cos ‘ ( π / 3 ) ) ) = ( arccos ‘ ( 1 / 2 ) )
4		pire	⊢ π ∈ ℝ
5		3re	⊢ 3 ∈ ℝ
6		3ne0	⊢ 3 ≠ 0
7	4 5 6	redivcli	⊢ ( π / 3 ) ∈ ℝ
8	7	recni	⊢ ( π / 3 ) ∈ ℂ
9		rere	⊢ ( ( π / 3 ) ∈ ℝ → ( ℜ ‘ ( π / 3 ) ) = ( π / 3 ) )
10	7 9	ax-mp	⊢ ( ℜ ‘ ( π / 3 ) ) = ( π / 3 )
11	7	rexri	⊢ ( π / 3 ) ∈ ℝ*
12		pipos	⊢ 0 < π
13		3pos	⊢ 0 < 3
14	4 5 12 13	divgt0ii	⊢ 0 < ( π / 3 )
15		picn	⊢ π ∈ ℂ
16	4 12	gt0ne0ii	⊢ π ≠ 0
17	15 16	dividi	⊢ ( π / π ) = 1
18		1lt3	⊢ 1 < 3
19	17 18	eqbrtri	⊢ ( π / π ) < 3
20	4 5 4 13 12	ltdiv23ii	⊢ ( ( π / 3 ) < π ↔ ( π / π ) < 3 )
21	19 20	mpbir	⊢ ( π / 3 ) < π
22		0xr	⊢ 0 ∈ ℝ*
23	4	rexri	⊢ π ∈ ℝ*
24		elioo1	⊢ ( ( 0 ∈ ℝ* ∧ π ∈ ℝ* ) → ( ( π / 3 ) ∈ ( 0 (,) π ) ↔ ( ( π / 3 ) ∈ ℝ* ∧ 0 < ( π / 3 ) ∧ ( π / 3 ) < π ) ) )
25	22 23 24	mp2an	⊢ ( ( π / 3 ) ∈ ( 0 (,) π ) ↔ ( ( π / 3 ) ∈ ℝ* ∧ 0 < ( π / 3 ) ∧ ( π / 3 ) < π ) )
26	11 14 21 25	mpbir3an	⊢ ( π / 3 ) ∈ ( 0 (,) π )
27	10 26	eqeltri	⊢ ( ℜ ‘ ( π / 3 ) ) ∈ ( 0 (,) π )
28		acoscos	⊢ ( ( ( π / 3 ) ∈ ℂ ∧ ( ℜ ‘ ( π / 3 ) ) ∈ ( 0 (,) π ) ) → ( arccos ‘ ( cos ‘ ( π / 3 ) ) ) = ( π / 3 ) )
29	8 27 28	mp2an	⊢ ( arccos ‘ ( cos ‘ ( π / 3 ) ) ) = ( π / 3 )
30	3 29	eqtr3i	⊢ ( arccos ‘ ( 1 / 2 ) ) = ( π / 3 )