Theorem atandm3

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

	Ref	Expression
Assertion	atandm3	$$⊢A\in \mathrm{dom}arctan\leftrightarrow \left(A\in ℂ\wedge A^2\ne -1\right)$$

Proof

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