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

Metamath Proof Explorer

Theorem atandm

Description: Since the property is a little lengthy, we abbreviate A e. CC /\ A =/= -ui /\ A =/= i as A e. dom arctan . This is the necessary precondition for the definition of arctan to make sense. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion atandm ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ - i ∧ 𝐴 ≠ i ) )

Proof

Step Hyp Ref Expression
1 eldif ⊢ ( 𝐴 ∈ ( ℂ ∖ { - i , i } ) ↔ ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ { - i , i } ) )
2 elprg ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ { - i , i } ↔ ( 𝐴 = - i ∨ 𝐴 = i ) ) )
3 2 notbid ⊢ ( 𝐴 ∈ ℂ → ( ¬ 𝐴 ∈ { - i , i } ↔ ¬ ( 𝐴 = - i ∨ 𝐴 = i ) ) )
4 neanior ⊢ ( ( 𝐴 ≠ - i ∧ 𝐴 ≠ i ) ↔ ¬ ( 𝐴 = - i ∨ 𝐴 = i ) )
5 3 4 bitr4di ⊢ ( 𝐴 ∈ ℂ → ( ¬ 𝐴 ∈ { - i , i } ↔ ( 𝐴 ≠ - i ∧ 𝐴 ≠ i ) ) )
6 5 pm5.32i ⊢ ( ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ { - i , i } ) ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐴 ≠ - i ∧ 𝐴 ≠ i ) ) )
7 1 6 bitri ⊢ ( 𝐴 ∈ ( ℂ ∖ { - i , i } ) ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐴 ≠ - i ∧ 𝐴 ≠ i ) ) )
8 ovex ⊢ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝑥 ) ) ) − ( log ‘ ( 1 + ( i · 𝑥 ) ) ) ) ) ∈ V
9 df-atan ⊢ arctan = ( 𝑥 ∈ ( ℂ ∖ { - i , i } ) ↦ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝑥 ) ) ) − ( log ‘ ( 1 + ( i · 𝑥 ) ) ) ) ) )
10 8 9 dmmpti ⊢ dom arctan = ( ℂ ∖ { - i , i } )
11 10 eleq2i ⊢ ( 𝐴 ∈ dom arctan ↔ 𝐴 ∈ ( ℂ ∖ { - i , i } ) )
12 3anass ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ - i ∧ 𝐴 ≠ i ) ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐴 ≠ - i ∧ 𝐴 ≠ i ) ) )
13 7 11 12 3bitr4i ⊢ ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ - i ∧ 𝐴 ≠ i ) )