Description: The arctangent of zero is zero. (Contributed by Mario Carneiro, 31-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | atan0 | ⊢ ( arctan ‘ 0 ) = 0 |
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 |