This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ ( π / 3 ) ) = ( ( √ ‘ 3 ) / 2 ) ∧ ( cos ‘ ( π / 3 ) ) = ( 1 / 2 ) )

Proof

Step Hyp Ref Expression
1 picn ⊢ π ∈ ℂ
2 2cn ⊢ 2 ∈ ℂ
3 2ne0 ⊢ 2 ≠ 0
4 2 3 reccli ⊢ ( 1 / 2 ) ∈ ℂ
5 3cn ⊢ 3 ∈ ℂ
6 3ne0 ⊢ 3 ≠ 0
7 5 6 reccli ⊢ ( 1 / 3 ) ∈ ℂ
8 1 4 7 subdii ⊢ ( π · ( ( 1 / 2 ) − ( 1 / 3 ) ) ) = ( ( π · ( 1 / 2 ) ) − ( π · ( 1 / 3 ) ) )
9 halfthird ⊢ ( ( 1 / 2 ) − ( 1 / 3 ) ) = ( 1 / 6 )
10 9 oveq2i ⊢ ( π · ( ( 1 / 2 ) − ( 1 / 3 ) ) ) = ( π · ( 1 / 6 ) )
11 8 10 eqtr3i ⊢ ( ( π · ( 1 / 2 ) ) − ( π · ( 1 / 3 ) ) ) = ( π · ( 1 / 6 ) )
12 1 2 3 divreci ⊢ ( π / 2 ) = ( π · ( 1 / 2 ) )
13 1 5 6 divreci ⊢ ( π / 3 ) = ( π · ( 1 / 3 ) )
14 12 13 oveq12i ⊢ ( ( π / 2 ) − ( π / 3 ) ) = ( ( π · ( 1 / 2 ) ) − ( π · ( 1 / 3 ) ) )
15 6cn ⊢ 6 ∈ ℂ
16 6nn ⊢ 6 ∈ ℕ
17 16 nnne0i ⊢ 6 ≠ 0
18 1 15 17 divreci ⊢ ( π / 6 ) = ( π · ( 1 / 6 ) )
19 11 14 18 3eqtr4i ⊢ ( ( π / 2 ) − ( π / 3 ) ) = ( π / 6 )
20 19 fveq2i ⊢ ( cos ‘ ( ( π / 2 ) − ( π / 3 ) ) ) = ( cos ‘ ( π / 6 ) )
21 1 5 6 divcli ⊢ ( π / 3 ) ∈ ℂ
22 coshalfpim ⊢ ( ( π / 3 ) ∈ ℂ → ( cos ‘ ( ( π / 2 ) − ( π / 3 ) ) ) = ( sin ‘ ( π / 3 ) ) )
23 21 22 ax-mp ⊢ ( cos ‘ ( ( π / 2 ) − ( π / 3 ) ) ) = ( sin ‘ ( π / 3 ) )
24 sincos6thpi ⊢ ( ( sin ‘ ( π / 6 ) ) = ( 1 / 2 ) ∧ ( cos ‘ ( π / 6 ) ) = ( ( √ ‘ 3 ) / 2 ) )
25 24 simpri ⊢ ( cos ‘ ( π / 6 ) ) = ( ( √ ‘ 3 ) / 2 )
26 20 23 25 3eqtr3i ⊢ ( sin ‘ ( π / 3 ) ) = ( ( √ ‘ 3 ) / 2 )
27 19 fveq2i ⊢ ( sin ‘ ( ( π / 2 ) − ( π / 3 ) ) ) = ( sin ‘ ( π / 6 ) )
28 sinhalfpim ⊢ ( ( π / 3 ) ∈ ℂ → ( sin ‘ ( ( π / 2 ) − ( π / 3 ) ) ) = ( cos ‘ ( π / 3 ) ) )
29 21 28 ax-mp ⊢ ( sin ‘ ( ( π / 2 ) − ( π / 3 ) ) ) = ( cos ‘ ( π / 3 ) )
30 24 simpli ⊢ ( sin ‘ ( π / 6 ) ) = ( 1 / 2 )
31 27 29 30 3eqtr3i ⊢ ( cos ‘ ( π / 3 ) ) = ( 1 / 2 )
32 26 31 pm3.2i ⊢ ( ( sin ‘ ( π / 3 ) ) = ( ( √ ‘ 3 ) / 2 ) ∧ ( cos ‘ ( π / 3 ) ) = ( 1 / 2 ) )