Metamath Proof Explorer


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