Metamath Proof Explorer

Theorem atandm4

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

Ref Expression
Assertion atandm4 ⊢ A ∈ dom ⁡ arctan ↔ A ∈ ℂ ∧ 1 + A 2 ≠ 0

Proof

Step Hyp Ref Expression
1 atandm3 ⊢ A ∈ dom ⁡ arctan ↔ A ∈ ℂ ∧ A 2 ≠ − 1
2 sqcl ⊢ A ∈ ℂ → A 2 ∈ ℂ
3 neg1cn ⊢ − 1 ∈ ℂ
4 subeq0 ⊢ A 2 ∈ ℂ ∧ − 1 ∈ ℂ → A 2 − -1 = 0 ↔ A 2 = − 1
5 2 3 4 sylancl ⊢ A ∈ ℂ → A 2 − -1 = 0 ↔ A 2 = − 1
6 ax-1cn ⊢ 1 ∈ ℂ
7 subneg ⊢ A 2 ∈ ℂ ∧ 1 ∈ ℂ → A 2 − -1 = A 2 + 1
8 2 6 7 sylancl ⊢ A ∈ ℂ → A 2 − -1 = A 2 + 1
9 addcom ⊢ A 2 ∈ ℂ ∧ 1 ∈ ℂ → A 2 + 1 = 1 + A 2
10 2 6 9 sylancl ⊢ A ∈ ℂ → A 2 + 1 = 1 + A 2
11 8 10 eqtrd ⊢ A ∈ ℂ → A 2 − -1 = 1 + A 2
12 11 eqeq1d ⊢ A ∈ ℂ → A 2 − -1 = 0 ↔ 1 + A 2 = 0
13 5 12 bitr3d ⊢ A ∈ ℂ → A 2 = − 1 ↔ 1 + A 2 = 0
14 13 necon3bid ⊢ A ∈ ℂ → A 2 ≠ − 1 ↔ 1 + A 2 ≠ 0
15 14 pm5.32i ⊢ A ∈ ℂ ∧ A 2 ≠ − 1 ↔ A ∈ ℂ ∧ 1 + A 2 ≠ 0
16 1 15 bitri ⊢ A ∈ dom ⁡ arctan ↔ A ∈ ℂ ∧ 1 + A 2 ≠ 0