H:
zeta * zeta = zeta ^2
by O_RING_1:def 1;
D0:
(sqrt 3) / 2 <> 0
by SQUARE_1:24;
zeta = (- (1 / 2)) + (<i> * ((sqrt 3) / 2))
;
then
( Re zeta = - (1 / 2) & Im zeta = (sqrt 3) / 2 )
by COMPLEX1:12;
then Im (zeta * zeta) =
2 * ((- (1 / 2)) * ((sqrt 3) / 2))
by COMPLEX1:16
.=
- ((sqrt 3) / 2)
;
hence
( not zeta in REAL & not zeta ^2 in REAL )
by H, D0; verum