Theorem atan0

Description: The arctangent of zero is zero. (Contributed by Mario Carneiro, 31-Mar-2015)

	Ref	Expression
Assertion	atan0	$$⊢arctan\left(0\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		neg0	$$⊢-0=0$$
2	1	fveq2i	$$⊢arctan\left(-0\right)=arctan\left(0\right)$$
3		0re	$$⊢0\in ℝ$$
4		atanre	$$⊢0\in ℝ\to 0\in \mathrm{dom}arctan$$
5		atanneg	$$⊢0\in \mathrm{dom}arctan\to arctan\left(-0\right)=-arctan\left(0\right)$$
6	3 4 5	mp2b	$$⊢arctan\left(-0\right)=-arctan\left(0\right)$$
7	2 6	eqtr3i	$$⊢arctan\left(0\right)=-arctan\left(0\right)$$
8		atancl	$$⊢0\in \mathrm{dom}arctan\to arctan\left(0\right)\in ℂ$$
9	3 4 8	mp2b	$$⊢arctan\left(0\right)\in ℂ$$
10	9	eqnegi	$$⊢arctan\left(0\right)=-arctan\left(0\right)\leftrightarrow arctan\left(0\right)=0$$
11	7 10	mpbi	$$⊢arctan\left(0\right)=0$$