atanneg

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

		Ref	Expression
	Assertion	atanneg	$⊢ A \in dom arctan \to arctan (- A) = - arctan (A)$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$⊢ i \in ℂ$
2		atandm2	$⊢ A \in dom arctan \leftrightarrow (A \in ℂ \land 1 - i A \neq 0 \land 1 + i A \neq 0)$
3	2	simp1bi	$⊢ A \in dom arctan \to A \in ℂ$
4		mulneg2	$⊢ (i \in ℂ \land A \in ℂ) \to i (- A) = - i A$
5	1 3 4	sylancr	$⊢ A \in dom arctan \to i (- A) = - i A$
6	5	oveq2d	$⊢ A \in dom arctan \to 1 - i (- A) = 1 - (- i A)$
7		ax-1cn	$⊢ 1 \in ℂ$
8		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
9	1 3 8	sylancr	$⊢ A \in dom arctan \to i A \in ℂ$
10		subneg	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 - (- i A) = 1 + i A$
11	7 9 10	sylancr	$⊢ A \in dom arctan \to 1 - (- i A) = 1 + i A$
12	6 11	eqtrd	$⊢ A \in dom arctan \to 1 - i (- A) = 1 + i A$
13	12	fveq2d	$⊢ A \in dom arctan \to \log (1 - i (- A)) = \log (1 + i A)$
14	5	oveq2d	$⊢ A \in dom arctan \to 1 + i (- A) = 1 + (- i A)$
15		negsub	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 + (- i A) = 1 - i A$
16	7 9 15	sylancr	$⊢ A \in dom arctan \to 1 + (- i A) = 1 - i A$
17	14 16	eqtrd	$⊢ A \in dom arctan \to 1 + i (- A) = 1 - i A$
18	17	fveq2d	$⊢ A \in dom arctan \to \log (1 + i (- A)) = \log (1 - i A)$
19	13 18	oveq12d	$⊢ A \in dom arctan \to \log (1 - i (- A)) - \log (1 + i (- A)) = \log (1 + i A) - \log (1 - i A)$
20		subcl	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 - i A \in ℂ$
21	7 9 20	sylancr	$⊢ A \in dom arctan \to 1 - i A \in ℂ$
22	2	simp2bi	$⊢ A \in dom arctan \to 1 - i A \neq 0$
23	21 22	logcld	$⊢ A \in dom arctan \to \log (1 - i A) \in ℂ$
24		addcl	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 + i A \in ℂ$
25	7 9 24	sylancr	$⊢ A \in dom arctan \to 1 + i A \in ℂ$
26	2	simp3bi	$⊢ A \in dom arctan \to 1 + i A \neq 0$
27	25 26	logcld	$⊢ A \in dom arctan \to \log (1 + i A) \in ℂ$
28	23 27	negsubdi2d	$⊢ A \in dom arctan \to - (\log (1 - i A) - \log (1 + i A)) = \log (1 + i A) - \log (1 - i A)$
29	19 28	eqtr4d	$⊢ A \in dom arctan \to \log (1 - i (- A)) - \log (1 + i (- A)) = - (\log (1 - i A) - \log (1 + i A))$
30	29	oveq2d	$⊢ A \in dom arctan \to (\frac{i}{2}) (\log (1 - i (- A)) - \log (1 + i (- A))) = (\frac{i}{2}) (- (\log (1 - i A) - \log (1 + i A)))$
31		halfcl	$⊢ i \in ℂ \to \frac{i}{2} \in ℂ$
32	1 31	ax-mp	$⊢ \frac{i}{2} \in ℂ$
33	23 27	subcld	$⊢ A \in dom arctan \to \log (1 - i A) - \log (1 + i A) \in ℂ$
34		mulneg2	$⊢ (\frac{i}{2} \in ℂ \land \log (1 - i A) - \log (1 + i A) \in ℂ) \to (\frac{i}{2}) (- (\log (1 - i A) - \log (1 + i A))) = - (\frac{i}{2}) (\log (1 - i A) - \log (1 + i A))$
35	32 33 34	sylancr	$⊢ A \in dom arctan \to (\frac{i}{2}) (- (\log (1 - i A) - \log (1 + i A))) = - (\frac{i}{2}) (\log (1 - i A) - \log (1 + i A))$
36	30 35	eqtrd	$⊢ A \in dom arctan \to (\frac{i}{2}) (\log (1 - i (- A)) - \log (1 + i (- A))) = - (\frac{i}{2}) (\log (1 - i A) - \log (1 + i A))$
37		atandmneg	$⊢ A \in dom arctan \to - A \in dom arctan$
38		atanval	$⊢ - A \in dom arctan \to arctan (- A) = (\frac{i}{2}) (\log (1 - i (- A)) - \log (1 + i (- A)))$
39	37 38	syl	$⊢ A \in dom arctan \to arctan (- A) = (\frac{i}{2}) (\log (1 - i (- A)) - \log (1 + i (- A)))$
40		atanval	$⊢ A \in dom arctan \to arctan (A) = (\frac{i}{2}) (\log (1 - i A) - \log (1 + i A))$
41	40	negeqd	$⊢ A \in dom arctan \to - arctan (A) = - (\frac{i}{2}) (\log (1 - i A) - \log (1 + i A))$
42	36 39 41	3eqtr4d	$⊢ A \in dom arctan \to arctan (- A) = - arctan (A)$

Metamath Proof Explorer

Theorem atanneg

Proof