Metamath Proof Explorer

Theorem atanval

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

Ref Expression
Assertion atanval 
|- ( A e. dom arctan -> ( arctan ` A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = A -> ( _i x. x ) = ( _i x. A ) )
2 1 oveq2d 
 |-  ( x = A -> ( 1 - ( _i x. x ) ) = ( 1 - ( _i x. A ) ) )
3 2 fveq2d 
 |-  ( x = A -> ( log ` ( 1 - ( _i x. x ) ) ) = ( log ` ( 1 - ( _i x. A ) ) ) )
4 1 oveq2d 
 |-  ( x = A -> ( 1 + ( _i x. x ) ) = ( 1 + ( _i x. A ) ) )
5 4 fveq2d 
 |-  ( x = A -> ( log ` ( 1 + ( _i x. x ) ) ) = ( log ` ( 1 + ( _i x. A ) ) ) )
6 3 5 oveq12d 
 |-  ( x = A -> ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) = ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) )
7 6 oveq2d 
 |-  ( x = A -> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
8 df-atan 
 |-  arctan = ( x e. ( CC \ { -u _i , _i } ) |-> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. x ) ) ) - ( log ` ( 1 + ( _i x. x ) ) ) ) ) )
9 ovex 
 |-  ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) e. _V
10 7 8 9 fvmpt 
 |-  ( A e. ( CC \ { -u _i , _i } ) -> ( arctan ` A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
11 atanf 
 |-  arctan : ( CC \ { -u _i , _i } ) --> CC
12 11 fdmi 
 |-  dom arctan = ( CC \ { -u _i , _i } )
13 10 12 eleq2s 
 |-  ( A e. dom arctan -> ( arctan ` A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )