Theorem atan0

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

	Ref	Expression
Assertion	atan0	⊢ ( arctan ‘ 0 ) = 0

Proof

Step	Hyp	Ref	Expression
1		neg0	⊢ - 0 = 0
2	1	fveq2i	⊢ ( arctan ‘ - 0 ) = ( arctan ‘ 0 )
3		0re	⊢ 0 ∈ ℝ
4		atanre	⊢ ( 0 ∈ ℝ → 0 ∈ dom arctan )
5		atanneg	⊢ ( 0 ∈ dom arctan → ( arctan ‘ - 0 ) = - ( arctan ‘ 0 ) )
6	3 4 5	mp2b	⊢ ( arctan ‘ - 0 ) = - ( arctan ‘ 0 )
7	2 6	eqtr3i	⊢ ( arctan ‘ 0 ) = - ( arctan ‘ 0 )
8		atancl	⊢ ( 0 ∈ dom arctan → ( arctan ‘ 0 ) ∈ ℂ )
9	3 4 8	mp2b	⊢ ( arctan ‘ 0 ) ∈ ℂ
10	9	eqnegi	⊢ ( ( arctan ‘ 0 ) = - ( arctan ‘ 0 ) ↔ ( arctan ‘ 0 ) = 0 )
11	7 10	mpbi	⊢ ( arctan ‘ 0 ) = 0