zeta = (- (1 / 2)) + (<i> * ((sqrt 3) / 2)) ;
then A: ( Re zeta = - (1 / 2) & Im zeta = (sqrt 3) / 2 ) by COMPLEX1:12;
then B: Re (zeta * zeta) = ((- (1 / 2)) ^2) - (((sqrt 3) / 2) ^2) by COMPLEX1:16
.= ((- (1 / 2)) ^2) - (((sqrt 3) / 2) * ((sqrt 3) / 2)) by SQUARE_1:def 1
.= ((- (1 / 2)) ^2) - (((sqrt 3) * (sqrt 3)) / (2 * 2))
.= ((- (1 / 2)) ^2) - (((sqrt 3) ^2) / (2 * 2)) by SQUARE_1:def 1
.= ((- (1 / 2)) ^2) - (3 / (2 * 2)) by SQUARE_1:def 2
.= ((- (1 / 2)) * (- (1 / 2))) - (3 / (2 * 2)) by SQUARE_1:def 1
.= - (1 / 2) ;
C: Im (zeta * zeta) = 2 * ((- (1 / 2)) * ((sqrt 3) / 2)) by A, COMPLEX1:16
.= - ((sqrt 3) / 2) ;
( Re ((- (1 / 2)) + (<i> * (- ((sqrt 3) / 2)))) = - (1 / 2) & Im ((- (1 / 2)) + (<i> * (- ((sqrt 3) / 2)))) = - ((sqrt 3) / 2) ) by COMPLEX1:12;
then zeta * zeta = (- (1 / 2)) + (<i> * (- ((sqrt 3) / 2))) by B, C, COMPLEX1:3;
hence zeta ^2 = (- (1 / 2)) - ((<i> * (sqrt 3)) / 2) by O_RING_1:def 1; :: thesis: verum