Metamath Proof Explorer

Theorem acos1half

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

Ref Expression
Assertion acos1half 
|- ( arccos ` ( 1 / 2 ) ) = ( _pi / 3 )

Proof

Step Hyp Ref Expression
1 sincos3rdpi 
 |-  ( ( sin ` ( _pi / 3 ) ) = ( ( sqrt ` 3 ) / 2 ) /\ ( cos ` ( _pi / 3 ) ) = ( 1 / 2 ) )
2 1 simpri 
 |-  ( cos ` ( _pi / 3 ) ) = ( 1 / 2 )
3 2 fveq2i 
 |-  ( arccos ` ( cos ` ( _pi / 3 ) ) ) = ( arccos ` ( 1 / 2 ) )
4 pire 
 |-  _pi e. RR
5 3re 
 |-  3 e. RR
6 3ne0 
 |-  3 =/= 0
7 4 5 6 redivcli 
 |-  ( _pi / 3 ) e. RR
8 7 recni 
 |-  ( _pi / 3 ) e. CC
9 rere 
 |-  ( ( _pi / 3 ) e. RR -> ( Re ` ( _pi / 3 ) ) = ( _pi / 3 ) )
10 7 9 ax-mp 
 |-  ( Re ` ( _pi / 3 ) ) = ( _pi / 3 )
11 7 rexri 
 |-  ( _pi / 3 ) e. RR*
12 pipos 
 |-  0 < _pi
13 3pos 
 |-  0 < 3
14 4 5 12 13 divgt0ii 
 |-  0 < ( _pi / 3 )
15 picn 
 |-  _pi e. CC
16 4 12 gt0ne0ii 
 |-  _pi =/= 0
17 15 16 dividi 
 |-  ( _pi / _pi ) = 1
18 1lt3 
 |-  1 < 3
19 17 18 eqbrtri 
 |-  ( _pi / _pi ) < 3
20 4 5 4 13 12 ltdiv23ii 
 |-  ( ( _pi / 3 ) < _pi <-> ( _pi / _pi ) < 3 )
21 19 20 mpbir 
 |-  ( _pi / 3 ) < _pi
22 0xr 
 |-  0 e. RR*
23 4 rexri 
 |-  _pi e. RR*
24 elioo1 
 |-  ( ( 0 e. RR* /\ _pi e. RR* ) -> ( ( _pi / 3 ) e. ( 0 (,) _pi ) <-> ( ( _pi / 3 ) e. RR* /\ 0 < ( _pi / 3 ) /\ ( _pi / 3 ) < _pi ) ) )
25 22 23 24 mp2an 
 |-  ( ( _pi / 3 ) e. ( 0 (,) _pi ) <-> ( ( _pi / 3 ) e. RR* /\ 0 < ( _pi / 3 ) /\ ( _pi / 3 ) < _pi ) )
26 11 14 21 25 mpbir3an 
 |-  ( _pi / 3 ) e. ( 0 (,) _pi )
27 10 26 eqeltri 
 |-  ( Re ` ( _pi / 3 ) ) e. ( 0 (,) _pi )
28 acoscos 
 |-  ( ( ( _pi / 3 ) e. CC /\ ( Re ` ( _pi / 3 ) ) e. ( 0 (,) _pi ) ) -> ( arccos ` ( cos ` ( _pi / 3 ) ) ) = ( _pi / 3 ) )
29 8 27 28 mp2an 
 |-  ( arccos ` ( cos ` ( _pi / 3 ) ) ) = ( _pi / 3 )
30 3 29 eqtr3i 
 |-  ( arccos ` ( 1 / 2 ) ) = ( _pi / 3 )