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 ) )