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