# Metamath Proof Explorer

## 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 {ℕ}_{0}$
6 absexp ${⊢}\left({A}\in ℂ\wedge 2\in {ℕ}_{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↔{\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 syl6eq ${⊢}{{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↔\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$