Theorem tan3rdpi

Description: The tangent of _pi / 3 is sqrt 3 . (Contributed by SN, 2-Sep-2025)

	Ref	Expression
Assertion	tan3rdpi	|- ( tan ` ( _pi / 3 ) ) = ( sqrt ` 3 )

Proof

Step	Hyp	Ref	Expression
1		picn	|- _pi e. CC
2		3cn	|- 3 e. CC
3		3ne0	|- 3 =/= 0
4	1 2 3	divcli	|- ( _pi / 3 ) e. CC
5		sincos3rdpi	|- ( ( sin ` ( _pi / 3 ) ) = ( ( sqrt ` 3 ) / 2 ) /\ ( cos ` ( _pi / 3 ) ) = ( 1 / 2 ) )
6	5	simpri	|- ( cos ` ( _pi / 3 ) ) = ( 1 / 2 )
7		0re	|- 0 e. RR
8		halfgt0	|- 0 < ( 1 / 2 )
9	7 8	gtneii	|- ( 1 / 2 ) =/= 0
10	6 9	eqnetri	|- ( cos ` ( _pi / 3 ) ) =/= 0
11		tanval	|- ( ( ( _pi / 3 ) e. CC /\ ( cos ` ( _pi / 3 ) ) =/= 0 ) -> ( tan ` ( _pi / 3 ) ) = ( ( sin ` ( _pi / 3 ) ) / ( cos ` ( _pi / 3 ) ) ) )
12	4 10 11	mp2an	|- ( tan ` ( _pi / 3 ) ) = ( ( sin ` ( _pi / 3 ) ) / ( cos ` ( _pi / 3 ) ) )
13	5	simpli	|- ( sin ` ( _pi / 3 ) ) = ( ( sqrt ` 3 ) / 2 )
14	13 6	oveq12i	|- ( ( sin ` ( _pi / 3 ) ) / ( cos ` ( _pi / 3 ) ) ) = ( ( ( sqrt ` 3 ) / 2 ) / ( 1 / 2 ) )
15	2	a1i	|- ( T. -> 3 e. CC )
16	15	sqrtcld	|- ( T. -> ( sqrt ` 3 ) e. CC )
17		1cnd	|- ( T. -> 1 e. CC )
18		2cnd	|- ( T. -> 2 e. CC )
19		ax-1ne0	|- 1 =/= 0
20	19	a1i	|- ( T. -> 1 =/= 0 )
21		2ne0	|- 2 =/= 0
22	21	a1i	|- ( T. -> 2 =/= 0 )
23	16 17 18 20 22	divcan7d	|- ( T. -> ( ( ( sqrt ` 3 ) / 2 ) / ( 1 / 2 ) ) = ( ( sqrt ` 3 ) / 1 ) )
24	16	div1d	|- ( T. -> ( ( sqrt ` 3 ) / 1 ) = ( sqrt ` 3 ) )
25	23 24	eqtrd	|- ( T. -> ( ( ( sqrt ` 3 ) / 2 ) / ( 1 / 2 ) ) = ( sqrt ` 3 ) )
26	25	mptru	|- ( ( ( sqrt ` 3 ) / 2 ) / ( 1 / 2 ) ) = ( sqrt ` 3 )
27	12 14 26	3eqtri	|- ( tan ` ( _pi / 3 ) ) = ( sqrt ` 3 )