let x, y, z be complex number ; :: thesis: ( z = x * y implies Im z = ((Re x) * (Im y)) + ((Im x) * (Re y)) )
assume A1: z = x * y ; :: thesis: Im z = ((Re x) * (Im y)) + ((Im x) * (Re y))
consider x1, x2, y1, y2 being Element of REAL such that
A2: x = [*x1,x2*] and
A3: y = [*y1,y2*] and
A4: x * y = [*(+ (* x1,y1),(opp (* x2,y2))),(+ (* x1,y2),(* x2,y1))*] by XCMPLX_0:def 5;
A5: ( Im x = x2 & Im y = y2 ) by A2, A3, Lm3;
A6: ( Re x = x1 & Re y = y1 ) by A2, A3, Lm3;
thus Im z = + (* x1,y2),(* x2,y1) by A1, A4, Lm3
.= (* x1,y2) + (* x2,y1) by Lm8
.= (x1 * y2) + (* x2,y1) by Lm10
.= ((Re x) * (Im y)) + ((Im x) * (Re y)) by A5, A6, Lm10 ; :: thesis: verum