Metamath Proof Explorer

Theorem atandm3

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

Ref Expression
Assertion atandm3 ⊢ A ∈ dom ⁡ arctan ↔ A ∈ ℂ ∧ A 2 ≠ − 1

Proof

Step Hyp Ref Expression
1 3anass ⊢ A ∈ ℂ ∧ A ≠ − i ∧ A ≠ i ↔ A ∈ ℂ ∧ A ≠ − i ∧ A ≠ i
2 atandm ⊢ A ∈ dom ⁡ arctan ↔ A ∈ ℂ ∧ A ≠ − i ∧ A ≠ i
3 ax-icn ⊢ i ∈ ℂ
4 sqeqor ⊢ A ∈ ℂ ∧ i ∈ ℂ → A 2 = i 2 ↔ A = i ∨ A = − i
5 3 4 mpan2 ⊢ A ∈ ℂ → A 2 = i 2 ↔ A = i ∨ A = − i
6 i2 ⊢ i 2 = − 1
7 6 eqeq2i ⊢ A 2 = i 2 ↔ A 2 = − 1
8 orcom ⊢ A = i ∨ A = − i ↔ A = − i ∨ A = i
9 5 7 8 3bitr3g ⊢ A ∈ ℂ → A 2 = − 1 ↔ A = − i ∨ A = i
10 9 necon3abid ⊢ A ∈ ℂ → A 2 ≠ − 1 ↔ ¬ A = − i ∨ A = i
11 neanior ⊢ A ≠ − i ∧ A ≠ i ↔ ¬ A = − i ∨ A = i
12 10 11 bitr4di ⊢ A ∈ ℂ → A 2 ≠ − 1 ↔ A ≠ − i ∧ A ≠ i
13 12 pm5.32i ⊢ A ∈ ℂ ∧ A 2 ≠ − 1 ↔ A ∈ ℂ ∧ A ≠ − i ∧ A ≠ i
14 1 2 13 3bitr4i ⊢ A ∈ dom ⁡ arctan ↔ A ∈ ℂ ∧ A 2 ≠ − 1