Metamath Proof Explorer

Theorem atanneg

Description: The arctangent function is odd. (Contributed by Mario Carneiro, 3-Apr-2015)

Ref Expression
Assertion atanneg 
|- ( A e. dom arctan -> ( arctan ` -u A ) = -u ( arctan ` A ) )

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 atandm2 
 |-  ( A e. dom arctan <-> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) )
3 2 simp1bi 
 |-  ( A e. dom arctan -> A e. CC )
4 mulneg2 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. -u A ) = -u ( _i x. A ) )
5 1 3 4 sylancr 
 |-  ( A e. dom arctan -> ( _i x. -u A ) = -u ( _i x. A ) )
6 5 oveq2d 
 |-  ( A e. dom arctan -> ( 1 - ( _i x. -u A ) ) = ( 1 - -u ( _i x. A ) ) )
7 ax-1cn 
 |-  1 e. CC
8 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
9 1 3 8 sylancr 
 |-  ( A e. dom arctan -> ( _i x. A ) e. CC )
10 subneg 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - -u ( _i x. A ) ) = ( 1 + ( _i x. A ) ) )
11 7 9 10 sylancr 
 |-  ( A e. dom arctan -> ( 1 - -u ( _i x. A ) ) = ( 1 + ( _i x. A ) ) )
12 6 11 eqtrd 
 |-  ( A e. dom arctan -> ( 1 - ( _i x. -u A ) ) = ( 1 + ( _i x. A ) ) )
13 12 fveq2d 
 |-  ( A e. dom arctan -> ( log ` ( 1 - ( _i x. -u A ) ) ) = ( log ` ( 1 + ( _i x. A ) ) ) )
14 5 oveq2d 
 |-  ( A e. dom arctan -> ( 1 + ( _i x. -u A ) ) = ( 1 + -u ( _i x. A ) ) )
15 negsub 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + -u ( _i x. A ) ) = ( 1 - ( _i x. A ) ) )
16 7 9 15 sylancr 
 |-  ( A e. dom arctan -> ( 1 + -u ( _i x. A ) ) = ( 1 - ( _i x. A ) ) )
17 14 16 eqtrd 
 |-  ( A e. dom arctan -> ( 1 + ( _i x. -u A ) ) = ( 1 - ( _i x. A ) ) )
18 17 fveq2d 
 |-  ( A e. dom arctan -> ( log ` ( 1 + ( _i x. -u A ) ) ) = ( log ` ( 1 - ( _i x. A ) ) ) )
19 13 18 oveq12d 
 |-  ( A e. dom arctan -> ( ( log ` ( 1 - ( _i x. -u A ) ) ) - ( log ` ( 1 + ( _i x. -u A ) ) ) ) = ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) )
20 subcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - ( _i x. A ) ) e. CC )
21 7 9 20 sylancr 
 |-  ( A e. dom arctan -> ( 1 - ( _i x. A ) ) e. CC )
22 2 simp2bi 
 |-  ( A e. dom arctan -> ( 1 - ( _i x. A ) ) =/= 0 )
23 21 22 logcld 
 |-  ( A e. dom arctan -> ( log ` ( 1 - ( _i x. A ) ) ) e. CC )
24 addcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + ( _i x. A ) ) e. CC )
25 7 9 24 sylancr 
 |-  ( A e. dom arctan -> ( 1 + ( _i x. A ) ) e. CC )
26 2 simp3bi 
 |-  ( A e. dom arctan -> ( 1 + ( _i x. A ) ) =/= 0 )
27 25 26 logcld 
 |-  ( A e. dom arctan -> ( log ` ( 1 + ( _i x. A ) ) ) e. CC )
28 23 27 negsubdi2d 
 |-  ( A e. dom arctan -> -u ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) = ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) )
29 19 28 eqtr4d 
 |-  ( A e. dom arctan -> ( ( log ` ( 1 - ( _i x. -u A ) ) ) - ( log ` ( 1 + ( _i x. -u A ) ) ) ) = -u ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) )
30 29 oveq2d 
 |-  ( A e. dom arctan -> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. -u A ) ) ) - ( log ` ( 1 + ( _i x. -u A ) ) ) ) ) = ( ( _i / 2 ) x. -u ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
31 halfcl 
 |-  ( _i e. CC -> ( _i / 2 ) e. CC )
32 1 31 ax-mp 
 |-  ( _i / 2 ) e. CC
33 23 27 subcld 
 |-  ( A e. dom arctan -> ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) e. CC )
34 mulneg2 
 |-  ( ( ( _i / 2 ) e. CC /\ ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) e. CC ) -> ( ( _i / 2 ) x. -u ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = -u ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
35 32 33 34 sylancr 
 |-  ( A e. dom arctan -> ( ( _i / 2 ) x. -u ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = -u ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
36 30 35 eqtrd 
 |-  ( A e. dom arctan -> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. -u A ) ) ) - ( log ` ( 1 + ( _i x. -u A ) ) ) ) ) = -u ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
37 atandmneg 
 |-  ( A e. dom arctan -> -u A e. dom arctan )
38 atanval 
 |-  ( -u A e. dom arctan -> ( arctan ` -u A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. -u A ) ) ) - ( log ` ( 1 + ( _i x. -u A ) ) ) ) ) )
39 37 38 syl 
 |-  ( A e. dom arctan -> ( arctan ` -u A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. -u A ) ) ) - ( log ` ( 1 + ( _i x. -u A ) ) ) ) ) )
40 atanval 
 |-  ( A e. dom arctan -> ( arctan ` A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
41 40 negeqd 
 |-  ( A e. dom arctan -> -u ( arctan ` A ) = -u ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
42 36 39 41 3eqtr4d 
 |-  ( A e. dom arctan -> ( arctan ` -u A ) = -u ( arctan ` A ) )