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