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	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 𝐴 ∈ dom arctan )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 𝐴 ∈ ℂ )
2		sqcl	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )
3	2	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
4	3	abscld	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ ( 𝐴 ↑ 2 ) ) ∈ ℝ )
5		2nn0	⊢ 2 ∈ ℕ0
6		absexp	⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( abs ‘ ( 𝐴 ↑ 2 ) ) = ( ( abs ‘ 𝐴 ) ↑ 2 ) )
7	1 5 6	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ ( 𝐴 ↑ 2 ) ) = ( ( abs ‘ 𝐴 ) ↑ 2 ) )
8		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ 𝐴 ) < 1 )
9		abscl	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
10	9	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
11		1red	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 1 ∈ ℝ )
12		absge0	⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( abs ‘ 𝐴 ) )
13	12	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 0 ≤ ( abs ‘ 𝐴 ) )
14		0le1	⊢ 0 ≤ 1
15	14	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 0 ≤ 1 )
16	10 11 13 15	lt2sqd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( ( abs ‘ 𝐴 ) < 1 ↔ ( ( abs ‘ 𝐴 ) ↑ 2 ) < ( 1 ↑ 2 ) ) )
17	8 16	mpbid	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) < ( 1 ↑ 2 ) )
18		sq1	⊢ ( 1 ↑ 2 ) = 1
19	17 18	breqtrdi	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) < 1 )
20	7 19	eqbrtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ ( 𝐴 ↑ 2 ) ) < 1 )
21	4 20	ltned	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( abs ‘ ( 𝐴 ↑ 2 ) ) ≠ 1 )
22		fveq2	⊢ ( ( 𝐴 ↑ 2 ) = - 1 → ( abs ‘ ( 𝐴 ↑ 2 ) ) = ( abs ‘ - 1 ) )
23		ax-1cn	⊢ 1 ∈ ℂ
24	23	absnegi	⊢ ( abs ‘ - 1 ) = ( abs ‘ 1 )
25		abs1	⊢ ( abs ‘ 1 ) = 1
26	24 25	eqtri	⊢ ( abs ‘ - 1 ) = 1
27	22 26	eqtrdi	⊢ ( ( 𝐴 ↑ 2 ) = - 1 → ( abs ‘ ( 𝐴 ↑ 2 ) ) = 1 )
28	27	necon3i	⊢ ( ( abs ‘ ( 𝐴 ↑ 2 ) ) ≠ 1 → ( 𝐴 ↑ 2 ) ≠ - 1 )
29	21 28	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 𝐴 ↑ 2 ) ≠ - 1 )
30		atandm3	⊢ ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ≠ - 1 ) )
31	1 29 30	sylanbrc	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 𝐴 ∈ dom arctan )