Theorem atandmneg

Description: The domain of the arctangent function is closed under negatives. (Contributed by Mario Carneiro, 3-Apr-2015)

	Ref	Expression
Assertion	atandmneg	⊢ ( 𝐴 ∈ dom arctan → - 𝐴 ∈ dom arctan )

Proof

Step	Hyp	Ref	Expression
1		atandm3	⊢ ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ≠ - 1 ) )
2	1	simplbi	⊢ ( 𝐴 ∈ dom arctan → 𝐴 ∈ ℂ )
3	2	negcld	⊢ ( 𝐴 ∈ dom arctan → - 𝐴 ∈ ℂ )
4		sqneg	⊢ ( 𝐴 ∈ ℂ → ( - 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
5	2 4	syl	⊢ ( 𝐴 ∈ dom arctan → ( - 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
6	1	simprbi	⊢ ( 𝐴 ∈ dom arctan → ( 𝐴 ↑ 2 ) ≠ - 1 )
7	5 6	eqnetrd	⊢ ( 𝐴 ∈ dom arctan → ( - 𝐴 ↑ 2 ) ≠ - 1 )
8		atandm3	⊢ ( - 𝐴 ∈ dom arctan ↔ ( - 𝐴 ∈ ℂ ∧ ( - 𝐴 ↑ 2 ) ≠ - 1 ) )
9	3 7 8	sylanbrc	⊢ ( 𝐴 ∈ dom arctan → - 𝐴 ∈ dom arctan )