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 ) )