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

Metamath Proof Explorer

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