Theorem tan3rdpi

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

	Ref	Expression
Assertion	tan3rdpi	⊢ ( tan ‘ ( π / 3 ) ) = ( √ ‘ 3 )

Proof

Step	Hyp	Ref	Expression
1		picn	⊢ π ∈ ℂ
2		3cn	⊢ 3 ∈ ℂ
3		3ne0	⊢ 3 ≠ 0
4	1 2 3	divcli	⊢ ( π / 3 ) ∈ ℂ
5		sincos3rdpi	⊢ ( ( sin ‘ ( π / 3 ) ) = ( ( √ ‘ 3 ) / 2 ) ∧ ( cos ‘ ( π / 3 ) ) = ( 1 / 2 ) )
6	5	simpri	⊢ ( cos ‘ ( π / 3 ) ) = ( 1 / 2 )
7		0re	⊢ 0 ∈ ℝ
8		halfgt0	⊢ 0 < ( 1 / 2 )
9	7 8	gtneii	⊢ ( 1 / 2 ) ≠ 0
10	6 9	eqnetri	⊢ ( cos ‘ ( π / 3 ) ) ≠ 0
11		tanval	⊢ ( ( ( π / 3 ) ∈ ℂ ∧ ( cos ‘ ( π / 3 ) ) ≠ 0 ) → ( tan ‘ ( π / 3 ) ) = ( ( sin ‘ ( π / 3 ) ) / ( cos ‘ ( π / 3 ) ) ) )
12	4 10 11	mp2an	⊢ ( tan ‘ ( π / 3 ) ) = ( ( sin ‘ ( π / 3 ) ) / ( cos ‘ ( π / 3 ) ) )
13	5	simpli	⊢ ( sin ‘ ( π / 3 ) ) = ( ( √ ‘ 3 ) / 2 )
14	13 6	oveq12i	⊢ ( ( sin ‘ ( π / 3 ) ) / ( cos ‘ ( π / 3 ) ) ) = ( ( ( √ ‘ 3 ) / 2 ) / ( 1 / 2 ) )
15	2	a1i	⊢ ( ⊤ → 3 ∈ ℂ )
16	15	sqrtcld	⊢ ( ⊤ → ( √ ‘ 3 ) ∈ ℂ )
17		1cnd	⊢ ( ⊤ → 1 ∈ ℂ )
18		2cnd	⊢ ( ⊤ → 2 ∈ ℂ )
19		ax-1ne0	⊢ 1 ≠ 0
20	19	a1i	⊢ ( ⊤ → 1 ≠ 0 )
21		2ne0	⊢ 2 ≠ 0
22	21	a1i	⊢ ( ⊤ → 2 ≠ 0 )
23	16 17 18 20 22	divcan7d	⊢ ( ⊤ → ( ( ( √ ‘ 3 ) / 2 ) / ( 1 / 2 ) ) = ( ( √ ‘ 3 ) / 1 ) )
24	16	div1d	⊢ ( ⊤ → ( ( √ ‘ 3 ) / 1 ) = ( √ ‘ 3 ) )
25	23 24	eqtrd	⊢ ( ⊤ → ( ( ( √ ‘ 3 ) / 2 ) / ( 1 / 2 ) ) = ( √ ‘ 3 ) )
26	25	mptru	⊢ ( ( ( √ ‘ 3 ) / 2 ) / ( 1 / 2 ) ) = ( √ ‘ 3 )
27	12 14 26	3eqtri	⊢ ( tan ‘ ( π / 3 ) ) = ( √ ‘ 3 )