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

Metamath Proof Explorer

Theorem imval2

Description: The imaginary part of a number in terms of complex conjugate. (Contributed by NM, 30-Apr-2005)

Ref Expression
Assertion imval2 ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) = ( ( 𝐴 − ( ∗ ‘ 𝐴 ) ) / ( 2 · i ) ) )

Proof

Step Hyp Ref Expression
1 imcl ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
2 1 recnd ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℂ )
3 2mulicn ⊢ ( 2 · i ) ∈ ℂ
4 2muline0 ⊢ ( 2 · i ) ≠ 0
5 divcan4 ⊢ ( ( ( ℑ ‘ 𝐴 ) ∈ ℂ ∧ ( 2 · i ) ∈ ℂ ∧ ( 2 · i ) ≠ 0 ) → ( ( ( ℑ ‘ 𝐴 ) · ( 2 · i ) ) / ( 2 · i ) ) = ( ℑ ‘ 𝐴 ) )
6 3 4 5 mp3an23 ⊢ ( ( ℑ ‘ 𝐴 ) ∈ ℂ → ( ( ( ℑ ‘ 𝐴 ) · ( 2 · i ) ) / ( 2 · i ) ) = ( ℑ ‘ 𝐴 ) )
7 2 6 syl ⊢ ( 𝐴 ∈ ℂ → ( ( ( ℑ ‘ 𝐴 ) · ( 2 · i ) ) / ( 2 · i ) ) = ( ℑ ‘ 𝐴 ) )
8 recl ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
9 8 recnd ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℂ )
10 ax-icn ⊢ i ∈ ℂ
11 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
12 10 2 11 sylancr ⊢ ( 𝐴 ∈ ℂ → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
13 9 12 addcld ⊢ ( 𝐴 ∈ ℂ → ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ∈ ℂ )
14 13 9 12 subsubd ⊢ ( 𝐴 ∈ ℂ → ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) − ( ℜ ‘ 𝐴 ) ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
15 replim ⊢ ( 𝐴 ∈ ℂ → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
16 remim ⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) = ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) )
17 15 16 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − ( ∗ ‘ 𝐴 ) ) = ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) − ( ( ℜ ‘ 𝐴 ) − ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
18 12 2timesd ⊢ ( 𝐴 ∈ ℂ → ( 2 · ( i · ( ℑ ‘ 𝐴 ) ) ) = ( ( i · ( ℑ ‘ 𝐴 ) ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
19 mulcom ⊢ ( ( ( ℑ ‘ 𝐴 ) ∈ ℂ ∧ ( 2 · i ) ∈ ℂ ) → ( ( ℑ ‘ 𝐴 ) · ( 2 · i ) ) = ( ( 2 · i ) · ( ℑ ‘ 𝐴 ) ) )
20 3 19 mpan2 ⊢ ( ( ℑ ‘ 𝐴 ) ∈ ℂ → ( ( ℑ ‘ 𝐴 ) · ( 2 · i ) ) = ( ( 2 · i ) · ( ℑ ‘ 𝐴 ) ) )
21 2cn ⊢ 2 ∈ ℂ
22 mulass ⊢ ( ( 2 ∈ ℂ ∧ i ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( ( 2 · i ) · ( ℑ ‘ 𝐴 ) ) = ( 2 · ( i · ( ℑ ‘ 𝐴 ) ) ) )
23 21 10 22 mp3an12 ⊢ ( ( ℑ ‘ 𝐴 ) ∈ ℂ → ( ( 2 · i ) · ( ℑ ‘ 𝐴 ) ) = ( 2 · ( i · ( ℑ ‘ 𝐴 ) ) ) )
24 20 23 eqtrd ⊢ ( ( ℑ ‘ 𝐴 ) ∈ ℂ → ( ( ℑ ‘ 𝐴 ) · ( 2 · i ) ) = ( 2 · ( i · ( ℑ ‘ 𝐴 ) ) ) )
25 2 24 syl ⊢ ( 𝐴 ∈ ℂ → ( ( ℑ ‘ 𝐴 ) · ( 2 · i ) ) = ( 2 · ( i · ( ℑ ‘ 𝐴 ) ) ) )
26 9 12 pncan2d ⊢ ( 𝐴 ∈ ℂ → ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) − ( ℜ ‘ 𝐴 ) ) = ( i · ( ℑ ‘ 𝐴 ) ) )
27 26 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) − ( ℜ ‘ 𝐴 ) ) + ( i · ( ℑ ‘ 𝐴 ) ) ) = ( ( i · ( ℑ ‘ 𝐴 ) ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
28 18 25 27 3eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( ( ℑ ‘ 𝐴 ) · ( 2 · i ) ) = ( ( ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) − ( ℜ ‘ 𝐴 ) ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
29 14 17 28 3eqtr4rd ⊢ ( 𝐴 ∈ ℂ → ( ( ℑ ‘ 𝐴 ) · ( 2 · i ) ) = ( 𝐴 − ( ∗ ‘ 𝐴 ) ) )
30 29 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( ( ℑ ‘ 𝐴 ) · ( 2 · i ) ) / ( 2 · i ) ) = ( ( 𝐴 − ( ∗ ‘ 𝐴 ) ) / ( 2 · i ) ) )
31 7 30 eqtr3d ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) = ( ( 𝐴 − ( ∗ ‘ 𝐴 ) ) / ( 2 · i ) ) )