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

Metamath Proof Explorer

Theorem atandm

Description: Since the property is a little lengthy, we abbreviate A e. CC /\ A =/= -ui /\ A =/= i as A e. dom arctan . This is the necessary precondition for the definition of arctan to make sense. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion atandm 
|- ( A e. dom arctan <-> ( A e. CC /\ A =/= -u _i /\ A =/= _i ) )

Proof

Step Hyp Ref Expression
1 eldif 
 |-  ( A e. ( CC \ { -u _i , _i } ) <-> ( A e. CC /\ -. A e. { -u _i , _i } ) )
2 elprg 
 |-  ( A e. CC -> ( A e. { -u _i , _i } <-> ( A = -u _i \/ A = _i ) ) )
3 2 notbid 
 |-  ( A e. CC -> ( -. A e. { -u _i , _i } <-> -. ( A = -u _i \/ A = _i ) ) )
4 neanior 
 |-  ( ( A =/= -u _i /\ A =/= _i ) <-> -. ( A = -u _i \/ A = _i ) )
5 3 4 bitr4di 
 |-  ( A e. CC -> ( -. A e. { -u _i , _i } <-> ( A =/= -u _i /\ A =/= _i ) ) )
6 5 pm5.32i 
 |-  ( ( A e. CC /\ -. A e. { -u _i , _i } ) <-> ( A e. CC /\ ( A =/= -u _i /\ A =/= _i ) ) )
7 1 6 bitri 
 |-  ( A e. ( CC \ { -u _i , _i } ) <-> ( A e. CC /\ ( A =/= -u _i /\ A =/= _i ) ) )
8 ovex 
 |-  ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) e. _V
9 df-atan 
 |-  arctan = ( x e. ( CC \ { -u _i , _i } ) |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) )
10 8 9 dmmpti 
 |-  dom arctan = ( CC \ { -u _i , _i } )
11 10 eleq2i 
 |-  ( A e. dom arctan <-> A e. ( CC \ { -u _i , _i } ) )
12 3anass 
 |-  ( ( A e. CC /\ A =/= -u _i /\ A =/= _i ) <-> ( A e. CC /\ ( A =/= -u _i /\ A =/= _i ) ) )
13 7 11 12 3bitr4i 
 |-  ( A e. dom arctan <-> ( A e. CC /\ A =/= -u _i /\ A =/= _i ) )