This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℂ ∧ ( 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 )