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

Metamath Proof Explorer

Theorem atandm3

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

Ref Expression
Assertion atandm3 ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ≠ - 1 ) )

Proof

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