Theorem atandm4

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

	Ref	Expression
Assertion	atandm4	⊢ ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ≠ 0 ) )

Proof

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