This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )