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 
 |-  -u 0 = 0
2 1 fveq2i 
 |-  ( arctan ` -u 0 ) = ( arctan ` 0 )
3 0re 
 |-  0 e. RR
4 atanre 
 |-  ( 0 e. RR -> 0 e. dom arctan )
5 atanneg 
 |-  ( 0 e. dom arctan -> ( arctan ` -u 0 ) = -u ( arctan ` 0 ) )
6 3 4 5 mp2b 
 |-  ( arctan ` -u 0 ) = -u ( arctan ` 0 )
7 2 6 eqtr3i 
 |-  ( arctan ` 0 ) = -u ( arctan ` 0 )
8 atancl 
 |-  ( 0 e. dom arctan -> ( arctan ` 0 ) e. CC )
9 3 4 8 mp2b 
 |-  ( arctan ` 0 ) e. CC
10 9 eqnegi 
 |-  ( ( arctan ` 0 ) = -u ( arctan ` 0 ) <-> ( arctan ` 0 ) = 0 )
11 7 10 mpbi 
 |-  ( arctan ` 0 ) = 0