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