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

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