atandm4

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

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

Step	Hyp	Ref	Expression
1		atandm3	$⊢ A \in dom arctan \leftrightarrow (A \in ℂ \land A^{2} \neq - 1)$
2		sqcl	$⊢ A \in ℂ \to A^{2} \in ℂ$
3		neg1cn	$⊢ - 1 \in ℂ$
4		subeq0	$⊢ (A^{2} \in ℂ \land - 1 \in ℂ) \to (A^{2} - -1 = 0 \leftrightarrow A^{2} = - 1)$
5	2 3 4	sylancl	$⊢ A \in ℂ \to (A^{2} - -1 = 0 \leftrightarrow A^{2} = - 1)$
6		ax-1cn	$⊢ 1 \in ℂ$
7		subneg	$⊢ (A^{2} \in ℂ \land 1 \in ℂ) \to A^{2} - -1 = A^{2} + 1$
8	2 6 7	sylancl	$⊢ A \in ℂ \to A^{2} - -1 = A^{2} + 1$
9		addcom	$⊢ (A^{2} \in ℂ \land 1 \in ℂ) \to A^{2} + 1 = 1 + A^{2}$
10	2 6 9	sylancl	$⊢ A \in ℂ \to A^{2} + 1 = 1 + A^{2}$
11	8 10	eqtrd	$⊢ A \in ℂ \to A^{2} - -1 = 1 + A^{2}$
12	11	eqeq1d	$⊢ A \in ℂ \to (A^{2} - -1 = 0 \leftrightarrow 1 + A^{2} = 0)$
13	5 12	bitr3d	$⊢ A \in ℂ \to (A^{2} = - 1 \leftrightarrow 1 + A^{2} = 0)$
14	13	necon3bid	$⊢ A \in ℂ \to (A^{2} \neq - 1 \leftrightarrow 1 + A^{2} \neq 0)$
15	14	pm5.32i	$⊢ (A \in ℂ \land A^{2} \neq - 1) \leftrightarrow (A \in ℂ \land 1 + A^{2} \neq 0)$
16	1 15	bitri	$⊢ A \in dom arctan \leftrightarrow (A \in ℂ \land 1 + A^{2} \neq 0)$

Metamath Proof Explorer