tan4thpi

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

		Ref	Expression
	Assertion	tan4thpi	$⊢ \tan (\frac{π}{4}) = 1$

Proof

Step	Hyp	Ref	Expression
1		pire	$⊢ π \in ℝ$
2		4nn	$⊢ 4 \in ℕ$
3		nndivre	$⊢ (π \in ℝ \land 4 \in ℕ) \to \frac{π}{4} \in ℝ$
4	1 2 3	mp2an	$⊢ \frac{π}{4} \in ℝ$
5	4	recni	$⊢ \frac{π}{4} \in ℂ$
6		sincos4thpi	$⊢ (\sin (\frac{π}{4}) = \frac{1}{\sqrt{2}} \land \cos (\frac{π}{4}) = \frac{1}{\sqrt{2}})$
7	6	simpri	$⊢ \cos (\frac{π}{4}) = \frac{1}{\sqrt{2}}$
8		sqrt2re	$⊢ \sqrt{2} \in ℝ$
9	8	recni	$⊢ \sqrt{2} \in ℂ$
10		2re	$⊢ 2 \in ℝ$
11		0le2	$⊢ 0 \leq 2$
12		resqrtth	$⊢ (2 \in ℝ \land 0 \leq 2) \to {\sqrt{2}}^{2} = 2$
13	10 11 12	mp2an	$⊢ {\sqrt{2}}^{2} = 2$
14		2ne0	$⊢ 2 \neq 0$
15	13 14	eqnetri	$⊢ {\sqrt{2}}^{2} \neq 0$
16		sqne0	$⊢ \sqrt{2} \in ℂ \to ({\sqrt{2}}^{2} \neq 0 \leftrightarrow \sqrt{2} \neq 0)$
17	9 16	ax-mp	$⊢ {\sqrt{2}}^{2} \neq 0 \leftrightarrow \sqrt{2} \neq 0$
18	15 17	mpbi	$⊢ \sqrt{2} \neq 0$
19		recne0	$⊢ (\sqrt{2} \in ℂ \land \sqrt{2} \neq 0) \to \frac{1}{\sqrt{2}} \neq 0$
20	9 18 19	mp2an	$⊢ \frac{1}{\sqrt{2}} \neq 0$
21	7 20	eqnetri	$⊢ \cos (\frac{π}{4}) \neq 0$
22		tanval	$⊢ (\frac{π}{4} \in ℂ \land \cos (\frac{π}{4}) \neq 0) \to \tan (\frac{π}{4}) = \frac{\sin (\frac{π}{4})}{\cos (\frac{π}{4})}$
23	5 21 22	mp2an	$⊢ \tan (\frac{π}{4}) = \frac{\sin (\frac{π}{4})}{\cos (\frac{π}{4})}$
24	6	simpli	$⊢ \sin (\frac{π}{4}) = \frac{1}{\sqrt{2}}$
25	24 7	oveq12i	$⊢ \frac{\sin (\frac{π}{4})}{\cos (\frac{π}{4})} = \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 (\frac{π}{4}) = 1$

Metamath Proof Explorer

Theorem tan4thpi

Proof