atandm3

Description: A compact form of atandm . (Contributed by Mario Carneiro, 31-Mar-2015)

		Ref	Expression
	Assertion	atandm3	$⊢ A \in dom arctan \leftrightarrow (A \in ℂ \land A^{2} \neq - 1)$

Step	Hyp	Ref	Expression
1		3anass	$⊢ (A \in ℂ \land A \neq - i \land A \neq i) \leftrightarrow (A \in ℂ \land (A \neq - i \land A \neq i))$
2		atandm	$⊢ A \in dom arctan \leftrightarrow (A \in ℂ \land A \neq - i \land A \neq i)$
3		ax-icn	$⊢ i \in ℂ$
4		sqeqor	$⊢ (A \in ℂ \land i \in ℂ) \to (A^{2} = i^{2} \leftrightarrow (A = i \lor A = - i))$
5	3 4	mpan2	$⊢ A \in ℂ \to (A^{2} = i^{2} \leftrightarrow (A = i \lor A = - i))$
6		i2	$⊢ i^{2} = - 1$
7	6	eqeq2i	$⊢ A^{2} = i^{2} \leftrightarrow A^{2} = - 1$
8		orcom	$⊢ (A = i \lor A = - i) \leftrightarrow (A = - i \lor A = i)$
9	5 7 8	3bitr3g	$⊢ A \in ℂ \to (A^{2} = - 1 \leftrightarrow (A = - i \lor A = i))$
10	9	necon3abid	$⊢ A \in ℂ \to (A^{2} \neq - 1 \leftrightarrow \neg (A = - i \lor A = i))$
11		neanior	$⊢ (A \neq - i \land A \neq i) \leftrightarrow \neg (A = - i \lor A = i)$
12	10 11	bitr4di	$⊢ A \in ℂ \to (A^{2} \neq - 1 \leftrightarrow (A \neq - i \land A \neq i))$
13	12	pm5.32i	$⊢ (A \in ℂ \land A^{2} \neq - 1) \leftrightarrow (A \in ℂ \land (A \neq - i \land A \neq i))$
14	1 2 13	3bitr4i	$⊢ A \in dom arctan \leftrightarrow (A \in ℂ \land A^{2} \neq - 1)$

Metamath Proof Explorer