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