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