Theorem atandmneg

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

	Ref	Expression
Assertion	atandmneg	|- ( A e. dom arctan -> -u A e. dom arctan )

Proof

Step	Hyp	Ref	Expression
1		atandm3	|- ( A e. dom arctan <-> ( A e. CC /\ ( A ^ 2 ) =/= -u 1 ) )
2	1	simplbi	|- ( A e. dom arctan -> A e. CC )
3	2	negcld	|- ( A e. dom arctan -> -u A e. CC )
4		sqneg	|- ( A e. CC -> ( -u A ^ 2 ) = ( A ^ 2 ) )
5	2 4	syl	|- ( A e. dom arctan -> ( -u A ^ 2 ) = ( A ^ 2 ) )
6	1	simprbi	|- ( A e. dom arctan -> ( A ^ 2 ) =/= -u 1 )
7	5 6	eqnetrd	|- ( A e. dom arctan -> ( -u A ^ 2 ) =/= -u 1 )
8		atandm3	|- ( -u A e. dom arctan <-> ( -u A e. CC /\ ( -u A ^ 2 ) =/= -u 1 ) )
9	3 7 8	sylanbrc	|- ( A e. dom arctan -> -u A e. dom arctan )