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

Metamath Proof Explorer

Theorem atanf

Description: Domain and codoamin of the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion atanf 
|- arctan : ( CC \ { -u _i , _i } ) --> CC

Proof

Step Hyp Ref Expression
1 df-atan 
 |-  arctan = ( x e. ( CC \ { -u _i , _i } ) |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) )
2 ovex 
 |-  ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) e. _V
3 2 1 dmmpti 
 |-  dom arctan = ( CC \ { -u _i , _i } )
4 3 eleq2i 
 |-  ( x e. dom arctan <-> x e. ( CC \ { -u _i , _i } ) )
5 ax-icn 
 |-  _i e. CC
6 halfcl 
 |-  ( _i e. CC -> ( _i / 2 ) e. CC )
7 5 6 ax-mp 
 |-  ( _i / 2 ) e. CC
8 ax-1cn 
 |-  1 e. CC
9 atandm2 
 |-  ( x e. dom arctan <-> ( x e. CC /\ ( 1 - ( _i x. x ) ) =/= 0 /\ ( 1 + ( _i x. x ) ) =/= 0 ) )
10 9 simp1bi 
 |-  ( x e. dom arctan -> x e. CC )
11 mulcl 
 |-  ( ( _i e. CC /\ x e. CC ) -> ( _i x. x ) e. CC )
12 5 10 11 sylancr 
 |-  ( x e. dom arctan -> ( _i x. x ) e. CC )
13 subcl 
 |-  ( ( 1 e. CC /\ ( _i x. x ) e. CC ) -> ( 1 - ( _i x. x ) ) e. CC )
14 8 12 13 sylancr 
 |-  ( x e. dom arctan -> ( 1 - ( _i x. x ) ) e. CC )
15 9 simp2bi 
 |-  ( x e. dom arctan -> ( 1 - ( _i x. x ) ) =/= 0 )
16 14 15 logcld 
 |-  ( x e. dom arctan -> ( log ` ( 1 - ( _i x. x ) ) ) e. CC )
17 addcl 
 |-  ( ( 1 e. CC /\ ( _i x. x ) e. CC ) -> ( 1 + ( _i x. x ) ) e. CC )
18 8 12 17 sylancr 
 |-  ( x e. dom arctan -> ( 1 + ( _i x. x ) ) e. CC )
19 9 simp3bi 
 |-  ( x e. dom arctan -> ( 1 + ( _i x. x ) ) =/= 0 )
20 18 19 logcld 
 |-  ( x e. dom arctan -> ( log ` ( 1 + ( _i x. x ) ) ) e. CC )
21 16 20 subcld 
 |-  ( x e. dom arctan -> ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) e. CC )
22 mulcl 
 |-  ( ( ( _i / 2 ) e. CC /\ ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) e. CC ) -> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) e. CC )
23 7 21 22 sylancr 
 |-  ( x e. dom arctan -> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) e. CC )
24 4 23 sylbir 
 |-  ( x e. ( CC \ { -u _i , _i } ) -> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) e. CC )
25 1 24 fmpti 
 |-  arctan : ( CC \ { -u _i , _i } ) --> CC