Theorem imval2

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

	Ref	Expression
Assertion	imval2	|- ( A e. CC -> ( Im ` A ) = ( ( A - ( * ` A ) ) / ( 2 x. _i ) ) )

Proof

Step	Hyp	Ref	Expression
1		imcl	|- ( A e. CC -> ( Im ` A ) e. RR )
2	1	recnd	|- ( A e. CC -> ( Im ` A ) e. CC )
3		2mulicn	|- ( 2 x. _i ) e. CC
4		2muline0	|- ( 2 x. _i ) =/= 0
5		divcan4	|- ( ( ( Im ` A ) e. CC /\ ( 2 x. _i ) e. CC /\ ( 2 x. _i ) =/= 0 ) -> ( ( ( Im ` A ) x. ( 2 x. _i ) ) / ( 2 x. _i ) ) = ( Im ` A ) )
6	3 4 5	mp3an23	|- ( ( Im ` A ) e. CC -> ( ( ( Im ` A ) x. ( 2 x. _i ) ) / ( 2 x. _i ) ) = ( Im ` A ) )
7	2 6	syl	|- ( A e. CC -> ( ( ( Im ` A ) x. ( 2 x. _i ) ) / ( 2 x. _i ) ) = ( Im ` A ) )
8		recl	|- ( A e. CC -> ( Re ` A ) e. RR )
9	8	recnd	|- ( A e. CC -> ( Re ` A ) e. CC )
10		ax-icn	|- _i e. CC
11		mulcl	|- ( ( _i e. CC /\ ( Im ` A ) e. CC ) -> ( _i x. ( Im ` A ) ) e. CC )
12	10 2 11	sylancr	|- ( A e. CC -> ( _i x. ( Im ` A ) ) e. CC )
13	9 12	addcld	|- ( A e. CC -> ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) e. CC )
14	13 9 12	subsubd	|- ( A e. CC -> ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) - ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) = ( ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) - ( Re ` A ) ) + ( _i x. ( Im ` A ) ) ) )
15		replim	|- ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
16		remim	|- ( A e. CC -> ( * ` A ) = ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) )
17	15 16	oveq12d	|- ( A e. CC -> ( A - ( * ` A ) ) = ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) - ( ( Re ` A ) - ( _i x. ( Im ` A ) ) ) ) )
18	12	2timesd	|- ( A e. CC -> ( 2 x. ( _i x. ( Im ` A ) ) ) = ( ( _i x. ( Im ` A ) ) + ( _i x. ( Im ` A ) ) ) )
19		mulcom	|- ( ( ( Im ` A ) e. CC /\ ( 2 x. _i ) e. CC ) -> ( ( Im ` A ) x. ( 2 x. _i ) ) = ( ( 2 x. _i ) x. ( Im ` A ) ) )
20	3 19	mpan2	|- ( ( Im ` A ) e. CC -> ( ( Im ` A ) x. ( 2 x. _i ) ) = ( ( 2 x. _i ) x. ( Im ` A ) ) )
21		2cn	|- 2 e. CC
22		mulass	|- ( ( 2 e. CC /\ _i e. CC /\ ( Im ` A ) e. CC ) -> ( ( 2 x. _i ) x. ( Im ` A ) ) = ( 2 x. ( _i x. ( Im ` A ) ) ) )
23	21 10 22	mp3an12	|- ( ( Im ` A ) e. CC -> ( ( 2 x. _i ) x. ( Im ` A ) ) = ( 2 x. ( _i x. ( Im ` A ) ) ) )
24	20 23	eqtrd	|- ( ( Im ` A ) e. CC -> ( ( Im ` A ) x. ( 2 x. _i ) ) = ( 2 x. ( _i x. ( Im ` A ) ) ) )
25	2 24	syl	|- ( A e. CC -> ( ( Im ` A ) x. ( 2 x. _i ) ) = ( 2 x. ( _i x. ( Im ` A ) ) ) )
26	9 12	pncan2d	|- ( A e. CC -> ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) - ( Re ` A ) ) = ( _i x. ( Im ` A ) ) )
27	26	oveq1d	|- ( A e. CC -> ( ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) - ( Re ` A ) ) + ( _i x. ( Im ` A ) ) ) = ( ( _i x. ( Im ` A ) ) + ( _i x. ( Im ` A ) ) ) )
28	18 25 27	3eqtr4d	|- ( A e. CC -> ( ( Im ` A ) x. ( 2 x. _i ) ) = ( ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) - ( Re ` A ) ) + ( _i x. ( Im ` A ) ) ) )
29	14 17 28	3eqtr4rd	|- ( A e. CC -> ( ( Im ` A ) x. ( 2 x. _i ) ) = ( A - ( * ` A ) ) )
30	29	oveq1d	|- ( A e. CC -> ( ( ( Im ` A ) x. ( 2 x. _i ) ) / ( 2 x. _i ) ) = ( ( A - ( * ` A ) ) / ( 2 x. _i ) ) )
31	7 30	eqtr3d	|- ( A e. CC -> ( Im ` A ) = ( ( A - ( * ` A ) ) / ( 2 x. _i ) ) )