Metamath Proof Explorer

Theorem atandm

Description: Since the property is a little lengthy, we abbreviate A e. CC /\ A =/= -ui /\ A =/= i as A e. dom arctan . This is the necessary precondition for the definition of arctan to make sense. (Contributed by Mario Carneiro, 31-Mar-2015)

		Ref	Expression
	Assertion	atandm	$⊢ A \in dom arctan \leftrightarrow (A \in ℂ \land A \neq - i \land A \neq i)$

Proof

Step	Hyp	Ref	Expression
1		eldif	$⊢ A \in (ℂ ∖ \{- i, i\}) \leftrightarrow (A \in ℂ \land \neg A \in \{- i, i\})$
2		elprg	$⊢ A \in ℂ \to (A \in \{- i, i\} \leftrightarrow (A = - i \lor A = i))$
3	2	notbid	$⊢ A \in ℂ \to (\neg A \in \{- i, i\} \leftrightarrow \neg (A = - i \lor A = i))$
4		neanior	$⊢ (A \neq - i \land A \neq i) \leftrightarrow \neg (A = - i \lor A = i)$
5	3 4	bitr4di	$⊢ A \in ℂ \to (\neg A \in \{- i, i\} \leftrightarrow (A \neq - i \land A \neq i))$
6	5	pm5.32i	$⊢ (A \in ℂ \land \neg A \in \{- i, i\}) \leftrightarrow (A \in ℂ \land (A \neq - i \land A \neq i))$
7	1 6	bitri	$⊢ A \in (ℂ ∖ \{- i, i\}) \leftrightarrow (A \in ℂ \land (A \neq - i \land A \neq i))$
8		ovex	$⊢ (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x)) \in V$
9		df-atan	$⊢ arctan = (x \in (ℂ ∖ \{- i, i\}) ⟼ (\frac{i}{2}) (\log (1 - i x) - \log (1 + i x)))$
10	8 9	dmmpti	$⊢ dom arctan = ℂ ∖ \{- i, i\}$
11	10	eleq2i	$⊢ A \in dom arctan \leftrightarrow A \in (ℂ ∖ \{- i, i\})$
12		3anass	$⊢ (A \in ℂ \land A \neq - i \land A \neq i) \leftrightarrow (A \in ℂ \land (A \neq - i \land A \neq i))$
13	7 11 12	3bitr4i	$⊢ A \in dom arctan \leftrightarrow (A \in ℂ \land A \neq - i \land A \neq i)$