atanf

Description: Domain and codoamin of the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015)

		Ref	Expression
	Assertion	atanf	$⊢ arctan : ℂ ∖ \{- i, i\} ⟶ ℂ$

Proof

Step	Hyp	Ref	Expression
1		df-atan	$⊢ arctan = (x \in (ℂ ∖ \{- i, i\}) ⟼ (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x)))$
2		ovex	$⊢ (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x)) \in V$
3	2 1	dmmpti	$⊢ dom arctan = ℂ ∖ \{- i, i\}$
4	3	eleq2i	$⊢ x \in dom arctan \leftrightarrow x \in (ℂ ∖ \{- i, i\})$
5		ax-icn	$⊢ i \in ℂ$
6		halfcl	$⊢ i \in ℂ \to \frac{i}{2} \in ℂ$
7	5 6	ax-mp	$⊢ \frac{i}{2} \in ℂ$
8		ax-1cn	$⊢ 1 \in ℂ$
9		atandm2	$⊢ x \in dom arctan \leftrightarrow (x \in ℂ \land 1 - i x \neq 0 \land 1 + i x \neq 0)$
10	9	simp1bi	$⊢ x \in dom arctan \to x \in ℂ$
11		mulcl	$⊢ (i \in ℂ \land x \in ℂ) \to i x \in ℂ$
12	5 10 11	sylancr	$⊢ x \in dom arctan \to i x \in ℂ$
13		subcl	$⊢ (1 \in ℂ \land i x \in ℂ) \to 1 - i x \in ℂ$
14	8 12 13	sylancr	$⊢ x \in dom arctan \to 1 - i x \in ℂ$
15	9	simp2bi	$⊢ x \in dom arctan \to 1 - i x \neq 0$
16	14 15	logcld	$⊢ x \in dom arctan \to \log (1 - i x) \in ℂ$
17		addcl	$⊢ (1 \in ℂ \land i x \in ℂ) \to 1 + i x \in ℂ$
18	8 12 17	sylancr	$⊢ x \in dom arctan \to 1 + i x \in ℂ$
19	9	simp3bi	$⊢ x \in dom arctan \to 1 + i x \neq 0$
20	18 19	logcld	$⊢ x \in dom arctan \to \log (1 + i x) \in ℂ$
21	16 20	subcld	$⊢ x \in dom arctan \to \log (1 - i x) - \log (1 + i x) \in ℂ$
22		mulcl	$⊢ (\frac{i}{2} \in ℂ \land \log (1 - i x) - \log (1 + i x) \in ℂ) \to (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x)) \in ℂ$
23	7 21 22	sylancr	$⊢ x \in dom arctan \to (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x)) \in ℂ$
24	4 23	sylbir	$⊢ x \in (ℂ ∖ \{- i, i\}) \to (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x)) \in ℂ$
25	1 24	fmpti	$⊢ arctan : ℂ ∖ \{- i, i\} ⟶ ℂ$

Metamath Proof Explorer

Theorem atanf

Proof