Theorem tan4thpi

Description: The tangent of _pi / 4 . (Contributed by Mario Carneiro, 5-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		pire	$$⊢\mathrm{\pi }\in ℝ$$
2		4nn	$$⊢4\in \mathbb{N}$$
3		nndivre	$$⊢\left(\mathrm{\pi }\in ℝ\wedge 4\in \mathbb{N}\right)\to \frac{\mathrm{\pi }}{4}\in ℝ$$
4	1 2 3	mp2an	$$⊢\frac{\mathrm{\pi }}{4}\in ℝ$$
5	4	recni	$$⊢\frac{\mathrm{\pi }}{4}\in ℂ$$
6		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)$$
7	6	simpri	$$⊢\cos \left(\frac{\mathrm{\pi }}{4}\right)=\frac{1}{\sqrt{2}}$$
8		sqrt2re	$$⊢\sqrt{2}\in ℝ$$
9	8	recni	$$⊢\sqrt{2}\in ℂ$$
10		2re	$$⊢2\in ℝ$$
11		0le2	$$⊢0\le 2$$
12		resqrtth	$$⊢\left(2\in ℝ\wedge 0\le 2\right)\to {\sqrt{2}}^2=2$$
13	10 11 12	mp2an	$$⊢{\sqrt{2}}^2=2$$
14		2ne0	$$⊢2\ne 0$$
15	13 14	eqnetri	$$⊢{\sqrt{2}}^2\ne 0$$
16		sqne0	$$⊢\sqrt{2}\in ℂ\to \left({\sqrt{2}}^2\ne 0\leftrightarrow \sqrt{2}\ne 0\right)$$
17	9 16	ax-mp	$$⊢{\sqrt{2}}^2\ne 0\leftrightarrow \sqrt{2}\ne 0$$
18	15 17	mpbi	$$⊢\sqrt{2}\ne 0$$
19		recne0	$$⊢\left(\sqrt{2}\in ℂ\wedge \sqrt{2}\ne 0\right)\to \frac{1}{\sqrt{2}}\ne 0$$
20	9 18 19	mp2an	$$⊢\frac{1}{\sqrt{2}}\ne 0$$
21	7 20	eqnetri	$$⊢\cos \left(\frac{\mathrm{\pi }}{4}\right)\ne 0$$
22		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)}$$
23	5 21 22	mp2an	$$⊢\tan \left(\frac{\mathrm{\pi }}{4}\right)=\frac{\sin \left(\frac{\mathrm{\pi }}{4}\right)}{\cos \left(\frac{\mathrm{\pi }}{4}\right)}$$
24	6	simpli	$$⊢\sin \left(\frac{\mathrm{\pi }}{4}\right)=\frac{1}{\sqrt{2}}$$
25	24 7	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}}}$$
26	9 18	reccli	$$⊢\frac{1}{\sqrt{2}}\in ℂ$$
27	26 20	dividi	$$⊢\frac{\frac{1}{\sqrt{2}}}{\frac{1}{\sqrt{2}}}=1$$
28	23 25 27	3eqtri	$$⊢\tan \left(\frac{\mathrm{\pi }}{4}\right)=1$$