set F = F_Complex ;
set a = 3-CRoot(2) * zeta;
set b = 3-CRoot(2) * (zeta ^2);
set c = 3-CRoot(2) ;
A: X- (3-CRoot(2) * zeta) =
rpoly (1,(3-CRoot(2) * zeta))
by FIELD_9:def 2
.=
<%(- (3-CRoot(2) * zeta)),(1. F_Complex)%>
by RING_5:10
;
B: X- (3-CRoot(2) * (zeta ^2)) =
rpoly (1,(3-CRoot(2) * (zeta ^2)))
by FIELD_9:def 2
.=
<%(- (3-CRoot(2) * (zeta ^2))),(1. F_Complex)%>
by RING_5:10
;
C: X- 3-CRoot(2) =
rpoly (1,3-CRoot(2))
by FIELD_9:def 2
.=
<%(- 3-CRoot(2)),(1. F_Complex)%>
by RING_5:10
;
D: (X- (3-CRoot(2) * zeta)) * (X- (3-CRoot(2) * (zeta ^2))) =
<%(- (3-CRoot(2) * zeta)),(1. F_Complex)%> *' <%(- (3-CRoot(2) * (zeta ^2))),(1. F_Complex)%>
by A, B, POLYNOM3:def 10
.=
<%((- (3-CRoot(2) * zeta)) * (- (3-CRoot(2) * (zeta ^2)))),(((1. F_Complex) * (- (3-CRoot(2) * (zeta ^2)))) + ((1. F_Complex) * (- (3-CRoot(2) * zeta)))),((1. F_Complex) * (1. F_Complex))%>
by FIELD_9:24
.=
<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>
by VECTSP_1:10
;
F_Real is Subfield of F_Complex
by FIELD_4:7;
then H0:
F_Real is Subring of F_Complex
by FIELD_5:12;
H1: (3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2)) =
(3-CRoot(2) * 3-CRoot(2)) * (zeta * (zeta ^2))
.=
(3-CRoot(2) * 3-CRoot(2)) * (zeta |^ 3)
by lemI
.=
(3-Root(2) |^ 1) * 3-Root(2)
by LZ23, BINOM:8
.=
(3-Root(2) |^ 1) * (3-Root(2) |^ 1)
by BINOM:8
.=
3-Root(2) |^ (1 + 1)
by BINOM:10
;
H3:
- 3-CRoot(2) = - 3-Root(2)
by H0, FIELD_6:17;
H4:
1 = 1. F_Complex
by COMPLFLD:def 1, COMPLEX1:def 4;
then H5:
- 2 = - ((1. F_Complex) + (1. F_Complex))
by COMPLFLD:2;
1 = 1. F_Complex
by COMPLEX1:def 4, COMPLFLD:def 1;
then H6:
- 1 = - (1. F_Complex)
by COMPLFLD:2;
(zeta ^2) + zeta = (zeta |^ (1 + 1)) + zeta
by lemI;
then (3-CRoot(2) * (zeta ^2)) + (3-CRoot(2) * zeta) =
3-CRoot(2) * ((- (1. F_Complex)) + ((- zeta) + zeta))
by H6, LZ23
.=
3-CRoot(2) * ((- (1. F_Complex)) + (0. F_Complex))
by RLVECT_1:5
.=
- (3-CRoot(2) * (1. F_Complex))
by VECTSP_1:8
.=
- 3-Root(2)
by H0, FIELD_6:17
;
then H6: - (- 3-Root(2)) =
- ((3-CRoot(2) * (zeta ^2)) + (3-CRoot(2) * zeta))
by COMPLFLD:2
.=
(- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))
by RLVECT_1:31
;
reconsider p1 = X- 3-CRoot(2) as Polynomial of F_Complex ;
p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> = X^3-2
proof
J:
5
-' 1
= 5
- 1
by XREAL_0:def 2;
L:
4
-' 1
= 4
- 1
by XREAL_0:def 2;
then K:
( 2
-' 1
= 2
- 1 & 3
-' 1
= 3
- 1 & 3
-' 2
= 3
- 2 & 4
-' 1
= 3 & 4
-' 2
= 4
- 2 )
by XREAL_0:def 2;
the
carrier of
(Polynom-Ring F_Rat) c= the
carrier of
(Polynom-Ring F_Complex)
by FIELD_4:10;
then
X^3-2 is
Element of the
carrier of
(Polynom-Ring F_Complex)
;
then reconsider q =
X^3-2 as
Polynomial of
F_Complex ;
set p2 =
<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>;
A:
dom (p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>) =
NAT
by FUNCT_2:def 1
.=
dom q
by FUNCT_2:def 1
;
now for o being object st o in dom q holds
(p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>) . o = q . olet o be
object ;
( o in dom q implies (p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>) . b1 = q . b1 )assume
o in dom q
;
(p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>) . b1 = q . b1then reconsider i =
o as
Element of
NAT ;
consider r being
FinSequence of the
carrier of
F_Complex such that B1:
(
len r = i + 1 &
(p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>) . i = Sum r & ( for
k being
Element of
NAT st
k in dom r holds
r . k = (p1 . (k -' 1)) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . ((i + 1) -' k)) ) )
by POLYNOM3:def 9;
(
i <= 3 implies not not
i = 0 & ... & not
i = 3 )
;
per cases then
( i = 0 or i = 1 or i = 2 or i = 3 or i > 3 )
;
suppose C1:
i = 0
;
(p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>) . b1 = q . b1then B2:
r = <*(r . 1)*>
by B1, FINSEQ_1:40;
then
dom r = {1}
by FINSEQ_1:2, FINSEQ_1:38;
then
1
in dom r
by TARSKI:def 1;
then r . 1 =
(p1 . (1 -' 1)) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . ((0 + 1) -' 1))
by C1, B1
.=
(p1 . (1 -' 1)) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . 0)
by NAT_2:8
.=
(p1 . 0) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . 0)
by NAT_2:8
.=
(p1 . 0) * ((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2)))
by FIELD_9:16
.=
(- 3-CRoot(2)) * ((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2)))
by C, POLYNOM5:38
.=
- (3-Root(2) * (3-Root(2) |^ 2))
by H1, H3
.=
- ((3-Root(2) |^ 2) * (3-Root(2) |^ 1))
by BINOM:8
.=
- (3-Root(2) |^ (2 + 1))
by BINOM:10
.=
- ((1. F_Complex) + (1. F_Complex))
by H4, COMPLFLD:2, R32
;
hence
(p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>) . o = q . o
by H5, C1, LL0, B1, B2, RLVECT_1:44;
verum end; suppose C1:
i = 1
;
(p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>) . b1 = q . b1then B3:
r = <*(r . 1),(r . 2)*>
by B1, FINSEQ_1:44;
B4:
dom r = {1,2}
by B1, C1, FINSEQ_1:def 3, FINSEQ_1:2;
then
1
in dom r
by TARSKI:def 2;
then B5:
r . 1 =
(p1 . (1 -' 1)) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . ((1 + 1) -' 1))
by C1, B1
.=
(p1 . 0) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . 1)
by K, NAT_2:8
.=
(- 3-CRoot(2)) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . 1)
by C, POLYNOM5:38
.=
(- 3-CRoot(2)) * ((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta)))
by FIELD_9:16
;
2
in dom r
by B4, TARSKI:def 2;
then r . 2 =
(p1 . (2 -' 1)) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . ((1 + 1) -' 2))
by C1, B1
.=
(p1 . 1) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . 0)
by K, NAT_2:8
.=
(1. F_Complex) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . 0)
by C, POLYNOM5:38
.=
(1. F_Complex) * ((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2)))
by FIELD_9:16
;
then Sum r =
((- 3-CRoot(2)) * ((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta)))) + ((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2)))
by B3, B5, RLVECT_1:45
.=
(- (3-Root(2) * 3-Root(2))) + (3-Root(2) |^ 2)
by H3, H6, H1
.=
(- ((3-Root(2) |^ 1) * 3-Root(2))) + (3-Root(2) |^ 2)
by BINOM:8
.=
(- ((3-Root(2) |^ 1) * (3-Root(2) |^ 1))) + (3-Root(2) |^ 2)
by BINOM:8
.=
(- (3-Root(2) |^ (1 + 1))) + (3-Root(2) |^ 2)
by BINOM:10
.=
0
;
hence
(p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>) . o = q . o
by B1, C1, LL0;
verum end; suppose C1:
i = 2
;
(p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>) . b1 = q . b1then B3:
r = <*(r . 1),(r . 2),(r . 3)*>
by B1, FINSEQ_1:45;
B4:
dom r =
Seg 3
by B1, C1, FINSEQ_1:def 3
.=
(Seg 2) \/ {(2 + 1)}
by FINSEQ_1:9
.=
{1,2,3}
by FINSEQ_1:2, ENUMSET1:3
;
then
1
in dom r
by ENUMSET1:def 1;
then B5:
r . 1 =
(p1 . (1 -' 1)) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . ((2 + 1) -' 1))
by C1, B1
.=
(p1 . 0) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . 2)
by K, NAT_2:8
.=
(p1 . 0) * (1. F_Complex)
by FIELD_9:16
.=
- 3-CRoot(2)
by C, POLYNOM5:38
;
2
in dom r
by B4, ENUMSET1:def 1;
then B6:
r . 2 =
(p1 . 1) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . 1)
by K, C1, B1
.=
(1. F_Complex) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . 1)
by C, POLYNOM5:38
.=
(- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))
by FIELD_9:16
;
3
in dom r
by B4, ENUMSET1:def 1;
then r . 3 =
(p1 . 2) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . ((2 + 1) -' 3))
by K, C1, B1
.=
(0. F_Complex) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . ((2 + 1) -' 3))
by C, POLYNOM5:38
;
then Sum r =
((- 3-CRoot(2)) + ((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta)))) + (0. F_Complex)
by B3, B5, B6, RLVECT_1:46
.=
0
by H3, H6
;
hence
(p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>) . o = q . o
by B1, C1, LL0;
verum end; suppose C1:
i = 3
;
(p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>) . b1 = q . b1then B3:
r = <*(r . 1),(r . 2),(r . 3),(r . 4)*>
by B1, FINSEQ_4:76;
B4:
dom r =
Seg 4
by B1, C1, FINSEQ_1:def 3
.=
(Seg 3) \/ {(3 + 1)}
by FINSEQ_1:9
.=
((Seg 2) \/ {(2 + 1)}) \/ {4}
by FINSEQ_1:9
.=
{1,2,3} \/ {4}
by FINSEQ_1:2, ENUMSET1:3
.=
{1,2,3,4}
by ENUMSET1:6
;
then
1
in dom r
by ENUMSET1:def 2;
then B5:
r . 1 =
(p1 . (1 -' 1)) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . ((3 + 1) -' 1))
by C1, B1
.=
(p1 . 0) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . 3)
by L, NAT_2:8
.=
(p1 . 0) * (0. F_Complex)
by FIELD_9:16
;
2
in dom r
by B4, ENUMSET1:def 2;
then B6:
r . 2 =
(p1 . 1) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . 2)
by K, C1, B1
.=
(p1 . 1) * (1. F_Complex)
by FIELD_9:16
.=
1. F_Complex
by C, POLYNOM5:38
;
3
in dom r
by B4, ENUMSET1:def 2;
then B7:
r . 3 =
(p1 . 2) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . ((3 + 1) -' 3))
by K, C1, B1
.=
(0. F_Complex) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . ((3 + 1) -' 3))
by C, POLYNOM5:38
;
4
in dom r
by B4, ENUMSET1:def 2;
then r . 4 =
(p1 . 3) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . ((3 + 1) -' 4))
by L, C1, B1
.=
(0. F_Complex) * (<%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> . ((3 + 1) -' 4))
by C, POLYNOM5:38
;
then
r = <*(0. F_Complex),(1. F_Complex),(0. F_Complex)*> ^ <*(0. F_Complex)*>
by B3, B5, B6, B7, FINSEQ_4:74;
then Sum r =
(Sum <*(0. F_Complex),(1. F_Complex),(0. F_Complex)*>) + (Sum <*(0. F_Complex)*>)
by RLVECT_1:41
.=
(Sum <*(0. F_Complex),(1. F_Complex),(0. F_Complex)*>) + (0. F_Complex)
by RLVECT_1:44
.=
((0. F_Complex) + (1. F_Complex)) + (0. F_Complex)
by RLVECT_1:46
.=
1
by COMPLFLD:def 1, COMPLEX1:def 4
;
hence
(p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>) . o = q . o
by B1, C1, LL0;
verum end; suppose C11:
i > 3
;
(p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>) . b1 = q . b1reconsider q1 =
q as
Element of the
carrier of
(Polynom-Ring F_Complex) by POLYNOM3:def 10;
CC:
deg q1 = 3
by LL, FIELD_4:20;
C0:
deg q = (len q) - 1
by HURWITZ:def 2;
C1:
i >= 3
+ 1
by C11, NAT_1:13;
then E:
q . i = 0. F_Complex
by CC, C0, ALGSEQ_1:8;
1. F_Complex <> 0. F_Complex
;
then C2:
(
len p1 = 2 &
deg <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> = 2 )
by C, POLYNOM5:40, FIELD_9:18;
C3:
deg <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> = (len <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>) - 1
by HURWITZ:def 2;
len (p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>) <= ((len p1) + (len <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>)) -' 1
by leng;
hence
(p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%>) . o = q . o
by J, E, C1, C3, C2, XXREAL_0:2, ALGSEQ_1:8;
verum end; end;
hence
p1 *' <%((3-CRoot(2) * zeta) * (3-CRoot(2) * (zeta ^2))),((- (3-CRoot(2) * (zeta ^2))) + (- (3-CRoot(2) * zeta))),(1. F_Complex)%> = X^3-2
by A;
verum
end;
then
(X- 3-CRoot(2)) * ((X- (3-CRoot(2) * zeta)) * (X- (3-CRoot(2) * (zeta ^2)))) = X^3-2
by D, POLYNOM3:def 10;
hence
X^3-2 = ((X- 3-CRoot(2)) * (X- (3-CRoot(2) * zeta))) * (X- (3-CRoot(2) * (zeta ^2)))
by GROUP_1:def 3; verum