Metamath Proof Explorer

Theorem sincos3rdpi

Description: The sine and cosine of _pi / 3 . (Contributed by Mario Carneiro, 21-May-2016)

Ref Expression
Assertion sincos3rdpi 
|- ( ( sin ` ( _pi / 3 ) ) = ( ( sqrt ` 3 ) / 2 ) /\ ( cos ` ( _pi / 3 ) ) = ( 1 / 2 ) )

Proof

Step Hyp Ref Expression
1 picn 
 |-  _pi e. CC
2 2cn 
 |-  2 e. CC
3 2ne0 
 |-  2 =/= 0
4 2 3 reccli 
 |-  ( 1 / 2 ) e. CC
5 3cn 
 |-  3 e. CC
6 3ne0 
 |-  3 =/= 0
7 5 6 reccli 
 |-  ( 1 / 3 ) e. CC
8 1 4 7 subdii 
 |-  ( _pi x. ( ( 1 / 2 ) - ( 1 / 3 ) ) ) = ( ( _pi x. ( 1 / 2 ) ) - ( _pi x. ( 1 / 3 ) ) )
9 halfthird 
 |-  ( ( 1 / 2 ) - ( 1 / 3 ) ) = ( 1 / 6 )
10 9 oveq2i 
 |-  ( _pi x. ( ( 1 / 2 ) - ( 1 / 3 ) ) ) = ( _pi x. ( 1 / 6 ) )
11 8 10 eqtr3i 
 |-  ( ( _pi x. ( 1 / 2 ) ) - ( _pi x. ( 1 / 3 ) ) ) = ( _pi x. ( 1 / 6 ) )
12 1 2 3 divreci 
 |-  ( _pi / 2 ) = ( _pi x. ( 1 / 2 ) )
13 1 5 6 divreci 
 |-  ( _pi / 3 ) = ( _pi x. ( 1 / 3 ) )
14 12 13 oveq12i 
 |-  ( ( _pi / 2 ) - ( _pi / 3 ) ) = ( ( _pi x. ( 1 / 2 ) ) - ( _pi x. ( 1 / 3 ) ) )
15 6cn 
 |-  6 e. CC
16 6nn 
 |-  6 e. NN
17 16 nnne0i 
 |-  6 =/= 0
18 1 15 17 divreci 
 |-  ( _pi / 6 ) = ( _pi x. ( 1 / 6 ) )
19 11 14 18 3eqtr4i 
 |-  ( ( _pi / 2 ) - ( _pi / 3 ) ) = ( _pi / 6 )
20 19 fveq2i 
 |-  ( cos ` ( ( _pi / 2 ) - ( _pi / 3 ) ) ) = ( cos ` ( _pi / 6 ) )
21 1 5 6 divcli 
 |-  ( _pi / 3 ) e. CC
22 coshalfpim 
 |-  ( ( _pi / 3 ) e. CC -> ( cos ` ( ( _pi / 2 ) - ( _pi / 3 ) ) ) = ( sin ` ( _pi / 3 ) ) )
23 21 22 ax-mp 
 |-  ( cos ` ( ( _pi / 2 ) - ( _pi / 3 ) ) ) = ( sin ` ( _pi / 3 ) )
24 sincos6thpi 
 |-  ( ( sin ` ( _pi / 6 ) ) = ( 1 / 2 ) /\ ( cos ` ( _pi / 6 ) ) = ( ( sqrt ` 3 ) / 2 ) )
25 24 simpri 
 |-  ( cos ` ( _pi / 6 ) ) = ( ( sqrt ` 3 ) / 2 )
26 20 23 25 3eqtr3i 
 |-  ( sin ` ( _pi / 3 ) ) = ( ( sqrt ` 3 ) / 2 )
27 19 fveq2i 
 |-  ( sin ` ( ( _pi / 2 ) - ( _pi / 3 ) ) ) = ( sin ` ( _pi / 6 ) )
28 sinhalfpim 
 |-  ( ( _pi / 3 ) e. CC -> ( sin ` ( ( _pi / 2 ) - ( _pi / 3 ) ) ) = ( cos ` ( _pi / 3 ) ) )
29 21 28 ax-mp 
 |-  ( sin ` ( ( _pi / 2 ) - ( _pi / 3 ) ) ) = ( cos ` ( _pi / 3 ) )
30 24 simpli 
 |-  ( sin ` ( _pi / 6 ) ) = ( 1 / 2 )
31 27 29 30 3eqtr3i 
 |-  ( cos ` ( _pi / 3 ) ) = ( 1 / 2 )
32 26 31 pm3.2i 
 |-  ( ( sin ` ( _pi / 3 ) ) = ( ( sqrt ` 3 ) / 2 ) /\ ( cos ` ( _pi / 3 ) ) = ( 1 / 2 ) )