Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic trigonometry
Inverse trigonometric functions
atan0
Next ⟩
atandmcj
Metamath Proof Explorer
Ascii
Unicode
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