set F = F_Complex ;
set p = X^3-2 ;
set M = {3-Root(2),(3-Root(2) * zeta),(3-Root(2) * (zeta ^2))};
I: F_Real is Subfield of F_Complex by FIELD_4:7;
reconsider r = 3-Root(2) as Element of F_Complex ;
reconsider z = zeta as Complex ;
H: Roots (F_Complex,X^3-2) = { a where a is Element of F_Complex : a is_a_root_of X^3-2 , F_Complex } by FIELD_4:def 4;
K: zeta ^2 = zeta * zeta by O_RING_1:def 1
.= z ^2 by SQUARE_1:def 1 ;
L: (z ^2) |^ 3 = (z * z) |^ 3 by SQUARE_1:def 1
.= (z |^ 3) * (z |^ 3) by NEWTON:7
.= (z |^ 3) ^2 by SQUARE_1:def 1
.= 1 ^2 by LZ23, lem3c
.= 1 * 1 by SQUARE_1:def 1 ;
now :: thesis: for o being object st o in {r,(r * zeta),(r * (zeta ^2))} holds
o in Roots (F_Complex,X^3-2)
let o be object ; :: thesis: ( o in {r,(r * zeta),(r * (zeta ^2))} implies b1 in Roots (F_Complex,X^3-2) )
assume B: o in {r,(r * zeta),(r * (zeta ^2))} ; :: thesis: b1 in Roots (F_Complex,X^3-2)
then reconsider c = o as Element of F_Complex ;
per cases ( o = r or o = r * zeta or o = r * (zeta ^2) ) by B, ENUMSET1:def 1;
suppose o = r * zeta ; :: thesis: b1 in Roots (F_Complex,X^3-2)
then Ext_eval (X^3-2,c) = ((r * zeta) |^ 3) - 2 by evalext2
.= (((3 -Root 2) * z) |^ 3) - 2 by lem3c
.= (((3 -Root 2) |^ 3) * (z |^ 3)) - 2 by lemcontr2
.= (2 * (z |^ 3)) - 2 by PREPOWER:def 2
.= (2 * 1) - 2 by LZ23, lem3c
.= 0. F_Real
.= 0. F_Complex by I, EC_PF_1:def 1 ;
then c is_a_root_of X^3-2 , F_Complex by FIELD_4:def 2;
hence o in Roots (F_Complex,X^3-2) by H; :: thesis: verum
end;
suppose o = r * (zeta ^2) ; :: thesis: b1 in Roots (F_Complex,X^3-2)
then Ext_eval (X^3-2,c) = ((r * (zeta ^2)) |^ 3) - 2 by evalext2
.= (((3 -Root 2) * (z ^2)) |^ 3) - 2 by K, lem3c
.= (((3 -Root 2) |^ 3) * ((z ^2) |^ 3)) - 2 by lemcontr2
.= (2 * 1) - 2 by L, PREPOWER:def 2
.= 0. F_Real
.= 0. F_Complex by I, EC_PF_1:def 1 ;
then c is_a_root_of X^3-2 , F_Complex by FIELD_4:def 2;
hence o in Roots (F_Complex,X^3-2) by H; :: thesis: verum
end;
end;
end;
then B: {3-Root(2),(3-Root(2) * zeta),(3-Root(2) * (zeta ^2))} c= Roots (F_Complex,X^3-2) ;
the carrier of (Polynom-Ring F_Rat) c= the carrier of (Polynom-Ring F_Complex) by FIELD_4:10;
then reconsider q = X^3-2 as Element of the carrier of (Polynom-Ring F_Complex) ;
H: deg q = 3 by LL, FIELD_4:20;
then reconsider q = q as non constant Element of the carrier of (Polynom-Ring F_Complex) by RING_4:def 4;
C: card {3-Root(2),(3-Root(2) * zeta),(3-Root(2) * (zeta ^2))} = 3
proof
zeta = (- (1 / 2)) + (<i> * ((sqrt 3) / 2)) ;
then ( 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: ( r <> 0. F_Complex & zeta <> 0. F_Complex ) ;
C1: now :: thesis: not r = r * zeta
assume r = r * zeta ; :: thesis: contradiction
then r * (1. F_Complex) = r * zeta ;
hence contradiction by D4, VECTSP_2:8; :: thesis: verum
end;
C2: now :: thesis: not r = r * (zeta ^2)
assume r = r * (zeta ^2) ; :: thesis: contradiction
then r * (1. F_Complex) = r * (zeta * zeta) by O_RING_1:def 1;
then zeta * zeta = 1. F_Complex by D4, VECTSP_2:8
.= 1r by COMPLFLD:def 1 ;
hence contradiction by D2, D3, COMPLEX1:6; :: thesis: verum
end;
C3: now :: thesis: not r * zeta = r * (zeta ^2)
assume r * zeta = r * (zeta ^2) ; :: thesis: contradiction
then zeta = zeta ^2 by D4, VECTSP_2:8
.= zeta * zeta by O_RING_1:def 1 ;
then zeta * (1. F_Complex) = zeta * zeta ;
hence contradiction by D4, VECTSP_2:8; :: thesis: verum
end;
thus card {3-Root(2),(3-Root(2) * zeta),(3-Root(2) * (zeta ^2))} = 3 by C1, C2, C3, CARD_2:58; :: thesis: verum
end;
D: card (Roots (F_Complex,X^3-2)) = 3
proof
F: card (Roots q) <= 3 by H, RING_5:22;
G: 3 <= card (Roots (F_Complex,X^3-2)) by C, B, NAT_1:43;
Roots (F_Complex,X^3-2) = Roots q by FIELD_7:13;
hence card (Roots (F_Complex,X^3-2)) = 3 by F, G, XXREAL_0:1; :: thesis: verum
end;
thus Roots (F_Complex,X^3-2) = {3-Root(2),(3-Root(2) * zeta),(3-Root(2) * (zeta ^2))} by B, C, D, lemfinset; :: thesis: verum