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