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 (\frac{π}{4}) = 1$

Step	Hyp	Ref	Expression
1		picn	$⊢ π \in ℂ$
2		4cn	$⊢ 4 \in ℂ$
3		4ne0	$⊢ 4 \neq 0$
4	1 2 3	divcli	$⊢ \frac{π}{4} \in ℂ$
5		sincos4thpi	$⊢ (\sin (\frac{π}{4}) = \frac{1}{\sqrt{2}} \land \cos (\frac{π}{4}) = \frac{1}{\sqrt{2}})$
6	5	simpri	$⊢ \cos (\frac{π}{4}) = \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} \neq 0$
13		recne0	$⊢ (\sqrt{2} \in ℂ \land \sqrt{2} \neq 0) \to \frac{1}{\sqrt{2}} \neq 0$
14	8 12 13	mp2an	$⊢ \frac{1}{\sqrt{2}} \neq 0$
15	6 14	eqnetri	$⊢ \cos (\frac{π}{4}) \neq 0$
16		tanval	$⊢ (\frac{π}{4} \in ℂ \land \cos (\frac{π}{4}) \neq 0) \to \tan (\frac{π}{4}) = \frac{\sin (\frac{π}{4})}{\cos (\frac{π}{4})}$
17	4 15 16	mp2an	$⊢ \tan (\frac{π}{4}) = \frac{\sin (\frac{π}{4})}{\cos (\frac{π}{4})}$
18	5	simpli	$⊢ \sin (\frac{π}{4}) = \frac{1}{\sqrt{2}}$
19	18 6	oveq12i	$⊢ \frac{\sin (\frac{π}{4})}{\cos (\frac{π}{4})} = \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 (\frac{π}{4}) = 1$

Metamath Proof Explorer