Theorem bndatandm

Description: A point in the open unit disk is in the domain of the arctangent. (Contributed by Mario Carneiro, 5-Apr-2015)

	Ref	Expression
Assertion	bndatandm	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to A\in \mathrm{dom}arctan$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to A\in ℂ$$
2		sqcl	$$⊢A\in ℂ\to A^2\in ℂ$$
3	2	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to A^2\in ℂ$$
4	3	abscld	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to \left|A^2\right|\in ℝ$$
5		2nn0	$$⊢2\in {\mathbb{N}}_0$$
6		absexp	$$⊢\left(A\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to \left|A^2\right|={\left|A\right|}^2$$
7	1 5 6	sylancl	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to \left|A^2\right|={\left|A\right|}^2$$
8		simpr	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to \left|A\right|<1$$
9		abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$
10	9	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to \left|A\right|\in ℝ$$
11		1red	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to 1\in ℝ$$
12		absge0	$$⊢A\in ℂ\to 0\le \left|A\right|$$
13	12	adantr	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to 0\le \left|A\right|$$
14		0le1	$$⊢0\le 1$$
15	14	a1i	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to 0\le 1$$
16	10 11 13 15	lt2sqd	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to \left(\left|A\right|<1\leftrightarrow {\left|A\right|}^2<1^2\right)$$
17	8 16	mpbid	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to {\left|A\right|}^2<1^2$$
18		sq1	$$⊢1^2=1$$
19	17 18	breqtrdi	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to {\left|A\right|}^2<1$$
20	7 19	eqbrtrd	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to \left|A^2\right|<1$$
21	4 20	ltned	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to \left|A^2\right|\ne 1$$
22		fveq2	$$⊢A^2=-1\to \left|A^2\right|=\left|-1\right|$$
23		ax-1cn	$$⊢1\in ℂ$$
24	23	absnegi	$$⊢\left|-1\right|=\left|1\right|$$
25		abs1	$$⊢\left|1\right|=1$$
26	24 25	eqtri	$$⊢\left|-1\right|=1$$
27	22 26	eqtrdi	$$⊢A^2=-1\to \left|A^2\right|=1$$
28	27	necon3i	$$⊢\left|A^2\right|\ne 1\to A^2\ne -1$$
29	21 28	syl	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to A^2\ne -1$$
30		atandm3	$$⊢A\in \mathrm{dom}arctan\leftrightarrow \left(A\in ℂ\wedge A^2\ne -1\right)$$
31	1 29 30	sylanbrc	$$⊢\left(A\in ℂ\wedge \left|A\right|<1\right)\to A\in \mathrm{dom}arctan$$