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