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 ) )