Theorem atanval

Description: Value of the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015)

	Ref	Expression
Assertion	atanval	⊢ ( 𝐴 ∈ dom arctan → ( arctan ‘ 𝐴 ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑥 = 𝐴 → ( i · 𝑥 ) = ( i · 𝐴 ) )
2	1	oveq2d	⊢ ( 𝑥 = 𝐴 → ( 1 − ( i · 𝑥 ) ) = ( 1 − ( i · 𝐴 ) ) )
3	2	fveq2d	⊢ ( 𝑥 = 𝐴 → ( log ‘ ( 1 − ( i · 𝑥 ) ) ) = ( log ‘ ( 1 − ( i · 𝐴 ) ) ) )
4	1	oveq2d	⊢ ( 𝑥 = 𝐴 → ( 1 + ( i · 𝑥 ) ) = ( 1 + ( i · 𝐴 ) ) )
5	4	fveq2d	⊢ ( 𝑥 = 𝐴 → ( log ‘ ( 1 + ( i · 𝑥 ) ) ) = ( log ‘ ( 1 + ( i · 𝐴 ) ) ) )
6	3 5	oveq12d	⊢ ( 𝑥 = 𝐴 → ( ( log ‘ ( 1 − ( i · 𝑥 ) ) ) − ( log ‘ ( 1 + ( i · 𝑥 ) ) ) ) = ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
7	6	oveq2d	⊢ ( 𝑥 = 𝐴 → ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝑥 ) ) ) − ( log ‘ ( 1 + ( i · 𝑥 ) ) ) ) ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
8		df-atan	⊢ arctan = ( 𝑥 ∈ ( ℂ ∖ { - i , i } ) ↦ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝑥 ) ) ) − ( log ‘ ( 1 + ( i · 𝑥 ) ) ) ) ) )
9		ovex	⊢ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ∈ V
10	7 8 9	fvmpt	⊢ ( 𝐴 ∈ ( ℂ ∖ { - i , i } ) → ( arctan ‘ 𝐴 ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
11		atanf	⊢ arctan : ( ℂ ∖ { - i , i } ) ⟶ ℂ
12	11	fdmi	⊢ dom arctan = ( ℂ ∖ { - i , i } )
13	10 12	eleq2s	⊢ ( 𝐴 ∈ dom arctan → ( arctan ‘ 𝐴 ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )