Metamath Proof Explorer

Theorem atandm3

Description: A compact form of atandm . (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion atandm3 
|- ( A e. dom arctan <-> ( A e. CC /\ ( A ^ 2 ) =/= -u 1 ) )

Proof

Step Hyp Ref Expression
1 3anass 
 |-  ( ( A e. CC /\ A =/= -u _i /\ A =/= _i ) <-> ( A e. CC /\ ( A =/= -u _i /\ A =/= _i ) ) )
2 atandm 
 |-  ( A e. dom arctan <-> ( A e. CC /\ A =/= -u _i /\ A =/= _i ) )
3 ax-icn 
 |-  _i e. CC
4 sqeqor 
 |-  ( ( A e. CC /\ _i e. CC ) -> ( ( A ^ 2 ) = ( _i ^ 2 ) <-> ( A = _i \/ A = -u _i ) ) )
5 3 4 mpan2 
 |-  ( A e. CC -> ( ( A ^ 2 ) = ( _i ^ 2 ) <-> ( A = _i \/ A = -u _i ) ) )
6 i2 
 |-  ( _i ^ 2 ) = -u 1
7 6 eqeq2i 
 |-  ( ( A ^ 2 ) = ( _i ^ 2 ) <-> ( A ^ 2 ) = -u 1 )
8 orcom 
 |-  ( ( A = _i \/ A = -u _i ) <-> ( A = -u _i \/ A = _i ) )
9 5 7 8 3bitr3g 
 |-  ( A e. CC -> ( ( A ^ 2 ) = -u 1 <-> ( A = -u _i \/ A = _i ) ) )
10 9 necon3abid 
 |-  ( A e. CC -> ( ( A ^ 2 ) =/= -u 1 <-> -. ( A = -u _i \/ A = _i ) ) )
11 neanior 
 |-  ( ( A =/= -u _i /\ A =/= _i ) <-> -. ( A = -u _i \/ A = _i ) )
12 10 11 bitr4di 
 |-  ( A e. CC -> ( ( A ^ 2 ) =/= -u 1 <-> ( A =/= -u _i /\ A =/= _i ) ) )
13 12 pm5.32i 
 |-  ( ( A e. CC /\ ( A ^ 2 ) =/= -u 1 ) <-> ( A e. CC /\ ( A =/= -u _i /\ A =/= _i ) ) )
14 1 2 13 3bitr4i 
 |-  ( A e. dom arctan <-> ( A e. CC /\ ( A ^ 2 ) =/= -u 1 ) )