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