H: (sqrt 3) / 2 <> 0 by SQUARE_1:24;
I: zeta |^ 2 = zeta * zeta by lemI;
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) ;
hence zeta |^ 2 <> 1 by I, H; :: thesis: ( zeta |^ 3 = 1 & zeta |^ 2 = (- zeta) - 1 )
J: (sqrt 3) ^2 = 3 by SQUARE_1:def 2;
D: zeta |^ (2 + 1) = (zeta |^ 2) * (zeta |^ 1) by BINOM:10
.= (zeta * zeta) * zeta by I, BINOM:8 ;
then E: Re (zeta |^ 3) = ((- (1 / 2)) * (- (1 / 2))) - (((sqrt 3) / 2) * (- ((sqrt 3) / 2))) by C, B, A, COMPLEX1:9
.= ((- (1 / 2)) * (- (1 / 2))) - ((- ((sqrt 3) * (sqrt 3))) / (2 * 2))
.= ((- (1 / 2)) * (- (1 / 2))) - ((- ((sqrt 3) ^2)) / (2 * 2)) by SQUARE_1:def 1
.= 1 by J ;
Im (zeta |^ 3) = ((- (1 / 2)) * ((sqrt 3) / 2)) + ((- (1 / 2)) * (- ((sqrt 3) / 2))) by D, C, B, A, COMPLEX1:9
.= 0 ;
hence zeta |^ 3 = 1 by E, COMPLEX1:6, COMPLEX1:3, COMPLEX1:def 4; :: thesis: zeta |^ 2 = (- zeta) - 1
reconsider z = zeta as Complex ;
K: ( - z = - zeta & 1r = 1. F_Complex ) by COMPLFLD:def 1, COMPLFLD:2;
( Re (- z) = - (- (1 / 2)) & Im (- z) = - ((sqrt 3) / 2) ) by A, COMPLEX1:17;
then H: Re ((- z) - 1r) = (- (- (1 / 2))) - 1 by COMPLEX1:6, COMPLEX1:19
.= - (1 / 2) ;
Im ((- z) - 1r) = (Im (- z)) - 0 by COMPLEX1:6, COMPLEX1:19;
hence zeta |^ 2 = (- zeta) - 1 by I, K, H, A, COMPLEX1:17, B, C, COMPLEX1:3, COMPLEX1:def 4; :: thesis: verum