atandmneg

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

		Ref	Expression
	Assertion	atandmneg	$⊢ A \in dom arctan \to - A \in dom arctan$

Step	Hyp	Ref	Expression
1		atandm3	$⊢ A \in dom arctan \leftrightarrow (A \in ℂ \land A^{2} \neq - 1)$
2	1	simplbi	$⊢ A \in dom arctan \to A \in ℂ$
3	2	negcld	$⊢ A \in dom arctan \to - A \in ℂ$
4		sqneg	$⊢ A \in ℂ \to {(- A)}^{2} = A^{2}$
5	2 4	syl	$⊢ A \in dom arctan \to {(- A)}^{2} = A^{2}$
6	1	simprbi	$⊢ A \in dom arctan \to A^{2} \neq - 1$
7	5 6	eqnetrd	$⊢ A \in dom arctan \to {(- A)}^{2} \neq - 1$
8		atandm3	$⊢ - A \in dom arctan \leftrightarrow (- A \in ℂ \land {(- A)}^{2} \neq - 1)$
9	3 7 8	sylanbrc	$⊢ A \in dom arctan \to - A \in dom arctan$

Metamath Proof Explorer