Theorem tan4thpi

Description: The tangent of _pi / 4 . (Contributed by Mario Carneiro, 5-Apr-2015) (Proof shortened by SN, 2-Sep-2025)

	Ref	Expression
Assertion	tan4thpi	$$⊢\tan \left(\frac{\mathrm{\pi }}{4}\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		picn	$$⊢\mathrm{\pi }\in ℂ$$
2		4cn	$$⊢4\in ℂ$$
3		4ne0	$$⊢4\ne 0$$
4	1 2 3	divcli	$$⊢\frac{\mathrm{\pi }}{4}\in ℂ$$
5		sincos4thpi	$$⊢\left(\sin \left(\frac{\mathrm{\pi }}{4}\right)=\frac{1}{\sqrt{2}}\wedge \cos \left(\frac{\mathrm{\pi }}{4}\right)=\frac{1}{\sqrt{2}}\right)$$
6	5	simpri	$$⊢\cos \left(\frac{\mathrm{\pi }}{4}\right)=\frac{1}{\sqrt{2}}$$
7		sqrt2re	$$⊢\sqrt{2}\in ℝ$$
8	7	recni	$$⊢\sqrt{2}\in ℂ$$
9		2re	$$⊢2\in ℝ$$
10		2pos	$$⊢0<2$$
11	9 10	sqrtgt0ii	$$⊢0<\sqrt{2}$$
12	7 11	gt0ne0ii	$$⊢\sqrt{2}\ne 0$$
13		recne0	$$⊢\left(\sqrt{2}\in ℂ\wedge \sqrt{2}\ne 0\right)\to \frac{1}{\sqrt{2}}\ne 0$$
14	8 12 13	mp2an	$$⊢\frac{1}{\sqrt{2}}\ne 0$$
15	6 14	eqnetri	$$⊢\cos \left(\frac{\mathrm{\pi }}{4}\right)\ne 0$$
16		tanval	$$⊢\left(\frac{\mathrm{\pi }}{4}\in ℂ\wedge \cos \left(\frac{\mathrm{\pi }}{4}\right)\ne 0\right)\to \tan \left(\frac{\mathrm{\pi }}{4}\right)=\frac{\sin \left(\frac{\mathrm{\pi }}{4}\right)}{\cos \left(\frac{\mathrm{\pi }}{4}\right)}$$
17	4 15 16	mp2an	$$⊢\tan \left(\frac{\mathrm{\pi }}{4}\right)=\frac{\sin \left(\frac{\mathrm{\pi }}{4}\right)}{\cos \left(\frac{\mathrm{\pi }}{4}\right)}$$
18	5	simpli	$$⊢\sin \left(\frac{\mathrm{\pi }}{4}\right)=\frac{1}{\sqrt{2}}$$
19	18 6	oveq12i	$$⊢\frac{\sin \left(\frac{\mathrm{\pi }}{4}\right)}{\cos \left(\frac{\mathrm{\pi }}{4}\right)}=\frac{\frac{1}{\sqrt{2}}}{\frac{1}{\sqrt{2}}}$$
20	8 12	reccli	$$⊢\frac{1}{\sqrt{2}}\in ℂ$$
21	20 14	dividi	$$⊢\frac{\frac{1}{\sqrt{2}}}{\frac{1}{\sqrt{2}}}=1$$
22	17 19 21	3eqtri	$$⊢\tan \left(\frac{\mathrm{\pi }}{4}\right)=1$$