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

Metamath Proof Explorer

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