Theorem atan1

Description: The arctangent of 1 is _pi / 4 . (Contributed by Mario Carneiro, 2-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		tan4thpi	$$⊢\tan \left(\frac{\mathrm{\pi }}{4}\right)=1$$
2	1	fveq2i	$$⊢arctan\left(\tan \left(\frac{\mathrm{\pi }}{4}\right)\right)=arctan\left(1\right)$$
3		pire	$$⊢\mathrm{\pi }\in ℝ$$
4		4nn	$$⊢4\in \mathbb{N}$$
5		nndivre	$$⊢\left(\mathrm{\pi }\in ℝ\wedge 4\in \mathbb{N}\right)\to \frac{\mathrm{\pi }}{4}\in ℝ$$
6	3 4 5	mp2an	$$⊢\frac{\mathrm{\pi }}{4}\in ℝ$$
7	6	recni	$$⊢\frac{\mathrm{\pi }}{4}\in ℂ$$
8		rere	$$⊢\frac{\mathrm{\pi }}{4}\in ℝ\to \Re \left(\frac{\mathrm{\pi }}{4}\right)=\frac{\mathrm{\pi }}{4}$$
9	6 8	ax-mp	$$⊢\Re \left(\frac{\mathrm{\pi }}{4}\right)=\frac{\mathrm{\pi }}{4}$$
10		pirp	$$⊢\mathrm{\pi }\in {ℝ}^{+}$$
11		rphalfcl	$$⊢\mathrm{\pi }\in {ℝ}^{+}\to \frac{\mathrm{\pi }}{2}\in {ℝ}^{+}$$
12	10 11	ax-mp	$$⊢\frac{\mathrm{\pi }}{2}\in {ℝ}^{+}$$
13		rpgt0	$$⊢\frac{\mathrm{\pi }}{2}\in {ℝ}^{+}\to 0<\frac{\mathrm{\pi }}{2}$$
14	12 13	ax-mp	$$⊢0<\frac{\mathrm{\pi }}{2}$$
15		halfpire	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ$$
16		lt0neg2	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ\to \left(0<\frac{\mathrm{\pi }}{2}\leftrightarrow -\frac{\mathrm{\pi }}{2}<0\right)$$
17	15 16	ax-mp	$$⊢0<\frac{\mathrm{\pi }}{2}\leftrightarrow -\frac{\mathrm{\pi }}{2}<0$$
18	14 17	mpbi	$$⊢-\frac{\mathrm{\pi }}{2}<0$$
19		nnrp	$$⊢4\in \mathbb{N}\to 4\in {ℝ}^{+}$$
20	4 19	ax-mp	$$⊢4\in {ℝ}^{+}$$
21		rpdivcl	$$⊢\left(\mathrm{\pi }\in {ℝ}^{+}\wedge 4\in {ℝ}^{+}\right)\to \frac{\mathrm{\pi }}{4}\in {ℝ}^{+}$$
22	10 20 21	mp2an	$$⊢\frac{\mathrm{\pi }}{4}\in {ℝ}^{+}$$
23		rpgt0	$$⊢\frac{\mathrm{\pi }}{4}\in {ℝ}^{+}\to 0<\frac{\mathrm{\pi }}{4}$$
24	22 23	ax-mp	$$⊢0<\frac{\mathrm{\pi }}{4}$$
25		neghalfpire	$$⊢-\frac{\mathrm{\pi }}{2}\in ℝ$$
26		0re	$$⊢0\in ℝ$$
27	25 26 6	lttri	$$⊢\left(-\frac{\mathrm{\pi }}{2}<0\wedge 0<\frac{\mathrm{\pi }}{4}\right)\to -\frac{\mathrm{\pi }}{2}<\frac{\mathrm{\pi }}{4}$$
28	18 24 27	mp2an	$$⊢-\frac{\mathrm{\pi }}{2}<\frac{\mathrm{\pi }}{4}$$
29	3	recni	$$⊢\mathrm{\pi }\in ℂ$$
30		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
31		divdiv1	$$⊢\left(\mathrm{\pi }\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{\frac{\mathrm{\pi }}{2}}{2}=\frac{\mathrm{\pi }}{2\cdot 2}$$
32	29 30 30 31	mp3an	$$⊢\frac{\frac{\mathrm{\pi }}{2}}{2}=\frac{\mathrm{\pi }}{2\cdot 2}$$
33		2t2e4	$$⊢2\cdot 2=4$$
34	33	oveq2i	$$⊢\frac{\mathrm{\pi }}{2\cdot 2}=\frac{\mathrm{\pi }}{4}$$
35	32 34	eqtri	$$⊢\frac{\frac{\mathrm{\pi }}{2}}{2}=\frac{\mathrm{\pi }}{4}$$
36		rphalflt	$$⊢\frac{\mathrm{\pi }}{2}\in {ℝ}^{+}\to \frac{\frac{\mathrm{\pi }}{2}}{2}<\frac{\mathrm{\pi }}{2}$$
37	12 36	ax-mp	$$⊢\frac{\frac{\mathrm{\pi }}{2}}{2}<\frac{\mathrm{\pi }}{2}$$
38	35 37	eqbrtrri	$$⊢\frac{\mathrm{\pi }}{4}<\frac{\mathrm{\pi }}{2}$$
39	25	rexri	$$⊢-\frac{\mathrm{\pi }}{2}\in {ℝ}^{*}$$
40	15	rexri	$$⊢\frac{\mathrm{\pi }}{2}\in {ℝ}^{*}$$
41		elioo2	$$⊢\left(-\frac{\mathrm{\pi }}{2}\in {ℝ}^{*}\wedge \frac{\mathrm{\pi }}{2}\in {ℝ}^{*}\right)\to \left(\frac{\mathrm{\pi }}{4}\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\leftrightarrow \left(\frac{\mathrm{\pi }}{4}\in ℝ\wedge -\frac{\mathrm{\pi }}{2}<\frac{\mathrm{\pi }}{4}\wedge \frac{\mathrm{\pi }}{4}<\frac{\mathrm{\pi }}{2}\right)\right)$$
42	39 40 41	mp2an	$$⊢\frac{\mathrm{\pi }}{4}\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\leftrightarrow \left(\frac{\mathrm{\pi }}{4}\in ℝ\wedge -\frac{\mathrm{\pi }}{2}<\frac{\mathrm{\pi }}{4}\wedge \frac{\mathrm{\pi }}{4}<\frac{\mathrm{\pi }}{2}\right)$$
43	6 28 38 42	mpbir3an	$$⊢\frac{\mathrm{\pi }}{4}\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)$$
44	9 43	eqeltri	$$⊢\Re \left(\frac{\mathrm{\pi }}{4}\right)\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)$$
45		atantan	$$⊢\left(\frac{\mathrm{\pi }}{4}\in ℂ\wedge \Re \left(\frac{\mathrm{\pi }}{4}\right)\in \left(-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right)\right)\to arctan\left(\tan \left(\frac{\mathrm{\pi }}{4}\right)\right)=\frac{\mathrm{\pi }}{4}$$
46	7 44 45	mp2an	$$⊢arctan\left(\tan \left(\frac{\mathrm{\pi }}{4}\right)\right)=\frac{\mathrm{\pi }}{4}$$
47	2 46	eqtr3i	$$⊢arctan\left(1\right)=\frac{\mathrm{\pi }}{4}$$