Step |
Hyp |
Ref |
Expression |
1 |
|
ax-icn |
⊢ i ∈ ℂ |
2 |
|
mulcl |
⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ ) |
3 |
1 2
|
mpan |
⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ ) |
4 |
|
imval |
⊢ ( ( i · 𝐴 ) ∈ ℂ → ( ℑ ‘ ( i · 𝐴 ) ) = ( ℜ ‘ ( ( i · 𝐴 ) / i ) ) ) |
5 |
3 4
|
syl |
⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ ( i · 𝐴 ) ) = ( ℜ ‘ ( ( i · 𝐴 ) / i ) ) ) |
6 |
|
ine0 |
⊢ i ≠ 0 |
7 |
|
divcan3 |
⊢ ( ( 𝐴 ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 ) → ( ( i · 𝐴 ) / i ) = 𝐴 ) |
8 |
1 6 7
|
mp3an23 |
⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) / i ) = 𝐴 ) |
9 |
8
|
fveq2d |
⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ ( ( i · 𝐴 ) / i ) ) = ( ℜ ‘ 𝐴 ) ) |
10 |
5 9
|
eqtr2d |
⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) = ( ℑ ‘ ( i · 𝐴 ) ) ) |