Theorem tan3rdpi

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

	Ref	Expression
Assertion	tan3rdpi	$$⊢\tan \left(\frac{\mathrm{\pi }}{3}\right)=\sqrt{3}$$

Proof

Step	Hyp	Ref	Expression
1		picn	$$⊢\mathrm{\pi }\in ℂ$$
2		3cn	$$⊢3\in ℂ$$
3		3ne0	$$⊢3\ne 0$$
4	1 2 3	divcli	$$⊢\frac{\mathrm{\pi }}{3}\in ℂ$$
5		sincos3rdpi	$$⊢\left(\sin \left(\frac{\mathrm{\pi }}{3}\right)=\frac{\sqrt{3}}{2}\wedge \cos \left(\frac{\mathrm{\pi }}{3}\right)=\frac{1}{2}\right)$$
6	5	simpri	$$⊢\cos \left(\frac{\mathrm{\pi }}{3}\right)=\frac{1}{2}$$
7		0re	$$⊢0\in ℝ$$
8		halfgt0	$$⊢0<\frac{1}{2}$$
9	7 8	gtneii	$$⊢\frac{1}{2}\ne 0$$
10	6 9	eqnetri	$$⊢\cos \left(\frac{\mathrm{\pi }}{3}\right)\ne 0$$
11		tanval	$$⊢\left(\frac{\mathrm{\pi }}{3}\in ℂ\wedge \cos \left(\frac{\mathrm{\pi }}{3}\right)\ne 0\right)\to \tan \left(\frac{\mathrm{\pi }}{3}\right)=\frac{\sin \left(\frac{\mathrm{\pi }}{3}\right)}{\cos \left(\frac{\mathrm{\pi }}{3}\right)}$$
12	4 10 11	mp2an	$$⊢\tan \left(\frac{\mathrm{\pi }}{3}\right)=\frac{\sin \left(\frac{\mathrm{\pi }}{3}\right)}{\cos \left(\frac{\mathrm{\pi }}{3}\right)}$$
13	5	simpli	$$⊢\sin \left(\frac{\mathrm{\pi }}{3}\right)=\frac{\sqrt{3}}{2}$$
14	13 6	oveq12i	$$⊢\frac{\sin \left(\frac{\mathrm{\pi }}{3}\right)}{\cos \left(\frac{\mathrm{\pi }}{3}\right)}=\frac{\frac{\sqrt{3}}{2}}{\frac{1}{2}}$$
15	2	a1i	$$⊢\top \to 3\in ℂ$$
16	15	sqrtcld	$$⊢\top \to \sqrt{3}\in ℂ$$
17		1cnd	$$⊢\top \to 1\in ℂ$$
18		2cnd	$$⊢\top \to 2\in ℂ$$
19		ax-1ne0	$$⊢1\ne 0$$
20	19	a1i	$$⊢\top \to 1\ne 0$$
21		2ne0	$$⊢2\ne 0$$
22	21	a1i	$$⊢\top \to 2\ne 0$$
23	16 17 18 20 22	divcan7d	$$⊢\top \to \frac{\frac{\sqrt{3}}{2}}{\frac{1}{2}}=\frac{\sqrt{3}}{1}$$
24	16	div1d	$$⊢\top \to \frac{\sqrt{3}}{1}=\sqrt{3}$$
25	23 24	eqtrd	$$⊢\top \to \frac{\frac{\sqrt{3}}{2}}{\frac{1}{2}}=\sqrt{3}$$
26	25	mptru	$$⊢\frac{\frac{\sqrt{3}}{2}}{\frac{1}{2}}=\sqrt{3}$$
27	12 14 26	3eqtri	$$⊢\tan \left(\frac{\mathrm{\pi }}{3}\right)=\sqrt{3}$$