Metamath Proof Explorer


Theorem atanneg

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

Ref Expression
Assertion atanneg ( 𝐴 ∈ dom arctan → ( arctan ‘ - 𝐴 ) = - ( arctan ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ax-icn i ∈ ℂ
2 atandm2 ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ≠ 0 ∧ ( 1 + ( i · 𝐴 ) ) ≠ 0 ) )
3 2 simp1bi ( 𝐴 ∈ dom arctan → 𝐴 ∈ ℂ )
4 mulneg2 ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
5 1 3 4 sylancr ( 𝐴 ∈ dom arctan → ( i · - 𝐴 ) = - ( i · 𝐴 ) )
6 5 oveq2d ( 𝐴 ∈ dom arctan → ( 1 − ( i · - 𝐴 ) ) = ( 1 − - ( i · 𝐴 ) ) )
7 ax-1cn 1 ∈ ℂ
8 mulcl ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
9 1 3 8 sylancr ( 𝐴 ∈ dom arctan → ( i · 𝐴 ) ∈ ℂ )
10 subneg ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − - ( i · 𝐴 ) ) = ( 1 + ( i · 𝐴 ) ) )
11 7 9 10 sylancr ( 𝐴 ∈ dom arctan → ( 1 − - ( i · 𝐴 ) ) = ( 1 + ( i · 𝐴 ) ) )
12 6 11 eqtrd ( 𝐴 ∈ dom arctan → ( 1 − ( i · - 𝐴 ) ) = ( 1 + ( i · 𝐴 ) ) )
13 12 fveq2d ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) = ( log ‘ ( 1 + ( i · 𝐴 ) ) ) )
14 5 oveq2d ( 𝐴 ∈ dom arctan → ( 1 + ( i · - 𝐴 ) ) = ( 1 + - ( i · 𝐴 ) ) )
15 negsub ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + - ( i · 𝐴 ) ) = ( 1 − ( i · 𝐴 ) ) )
16 7 9 15 sylancr ( 𝐴 ∈ dom arctan → ( 1 + - ( i · 𝐴 ) ) = ( 1 − ( i · 𝐴 ) ) )
17 14 16 eqtrd ( 𝐴 ∈ dom arctan → ( 1 + ( i · - 𝐴 ) ) = ( 1 − ( i · 𝐴 ) ) )
18 17 fveq2d ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) = ( log ‘ ( 1 − ( i · 𝐴 ) ) ) )
19 13 18 oveq12d ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) ) = ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) )
20 subcl ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
21 7 9 20 sylancr ( 𝐴 ∈ dom arctan → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
22 2 simp2bi ( 𝐴 ∈ dom arctan → ( 1 − ( i · 𝐴 ) ) ≠ 0 )
23 21 22 logcld ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ∈ ℂ )
24 addcl ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
25 7 9 24 sylancr ( 𝐴 ∈ dom arctan → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
26 2 simp3bi ( 𝐴 ∈ dom arctan → ( 1 + ( i · 𝐴 ) ) ≠ 0 )
27 25 26 logcld ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ∈ ℂ )
28 23 27 negsubdi2d ( 𝐴 ∈ dom arctan → - ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) = ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) )
29 19 28 eqtr4d ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) ) = - ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
30 29 oveq2d ( 𝐴 ∈ dom arctan → ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) ) ) = ( ( i / 2 ) · - ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
31 halfcl ( i ∈ ℂ → ( i / 2 ) ∈ ℂ )
32 1 31 ax-mp ( i / 2 ) ∈ ℂ
33 23 27 subcld ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ∈ ℂ )
34 mulneg2 ( ( ( i / 2 ) ∈ ℂ ∧ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ∈ ℂ ) → ( ( i / 2 ) · - ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = - ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
35 32 33 34 sylancr ( 𝐴 ∈ dom arctan → ( ( i / 2 ) · - ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = - ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
36 30 35 eqtrd ( 𝐴 ∈ dom arctan → ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) ) ) = - ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
37 atandmneg ( 𝐴 ∈ dom arctan → - 𝐴 ∈ dom arctan )
38 atanval ( - 𝐴 ∈ dom arctan → ( arctan ‘ - 𝐴 ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) ) ) )
39 37 38 syl ( 𝐴 ∈ dom arctan → ( arctan ‘ - 𝐴 ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) ) ) )
40 atanval ( 𝐴 ∈ dom arctan → ( arctan ‘ 𝐴 ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
41 40 negeqd ( 𝐴 ∈ dom arctan → - ( arctan ‘ 𝐴 ) = - ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
42 36 39 41 3eqtr4d ( 𝐴 ∈ dom arctan → ( arctan ‘ - 𝐴 ) = - ( arctan ‘ 𝐴 ) )