:: POLYEQ_1 semantic presentation

REAL is V33() V34() V35() V39() set

NAT is V33() V34() V35() V36() V37() V38() V39() M2(K6(REAL))

K6(REAL) is set

COMPLEX is V33() V39() set

omega is V33() V34() V35() V36() V37() V38() V39() set

K6(omega) is set

K6(NAT) is set

K7(NAT,REAL) is set

K6(K7(NAT,REAL)) is set

0 is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

sqrt 0 is complex real ext-real M2( REAL )

4 is non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

sqrt 4 is complex real ext-real M2( REAL )

2 is non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

1 is non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

- 1 is non zero complex real ext-real M2( REAL )

a is complex set

x is complex set

a * x is complex set

c is complex set

(a * x) + c is complex set

a is complex set

c is complex set

x is complex set

(a,c,x) is set

a * x is complex set

(a * x) + c is complex set

a is complex real ext-real set

c is complex real ext-real set

x is complex real ext-real set

(a,c,x) is complex set

a * x is complex real ext-real set

(a * x) + c is complex real ext-real set

a is complex real ext-real M2( REAL )

c is complex real ext-real M2( REAL )

x is complex real ext-real M2( REAL )

(a,c,x) is complex real ext-real set

a * x is complex real ext-real set

(a * x) + c is complex real ext-real set

a is complex set

c is complex set

x is complex set

(a,c,x) is complex set

a * x is complex set

(a * x) + c is complex set

c / a is complex set

- (c / a) is complex set

a " is complex set

- c is complex set

(a ") * (- c) is complex set

(a ") * (a * x) is complex set

(a ") * a is complex set

((a ") * a) * x is complex set

1 * x is complex set

(a ") * c is complex set

- ((a ") * c) is complex set

a is complex set

(0,0,a) is complex set

0 * a is complex set

(0 * a) + 0 is complex set

a is complex set

c is complex set

(0,a,c) is complex set

0 * c is complex set

(0 * c) + a is complex set

a is complex set

x is complex set

x ^2 is complex set

x * x is complex set

a * (x ^2) is complex set

c is complex set

c * x is complex set

(a * (x ^2)) + (c * x) is complex set

x is complex set

((a * (x ^2)) + (c * x)) + x is complex set

a is complex real ext-real set

c is complex real ext-real set

x is complex real ext-real set

x is complex real ext-real set

(a,c,x,x) is set

x ^2 is complex real ext-real set

x * x is complex real ext-real set

a * (x ^2) is complex real ext-real set

c * x is complex real ext-real set

(a * (x ^2)) + (c * x) is complex real ext-real set

((a * (x ^2)) + (c * x)) + x is complex real ext-real set

a is complex set

c is complex set

x is complex set

x is complex set

(a,c,x,x) is set

x ^2 is complex set

x * x is complex set

a * (x ^2) is complex set

c * x is complex set

(a * (x ^2)) + (c * x) is complex set

((a * (x ^2)) + (c * x)) + x is complex set

a is complex real ext-real M2( REAL )

c is complex real ext-real M2( REAL )

x is complex real ext-real M2( REAL )

x is complex real ext-real M2( REAL )

(a,c,x,x) is complex real ext-real set

x ^2 is complex real ext-real set

x * x is complex real ext-real set

a * (x ^2) is complex real ext-real set

c * x is complex real ext-real set

(a * (x ^2)) + (c * x) is complex real ext-real set

((a * (x ^2)) + (c * x)) + x is complex real ext-real set

a is complex set

c is complex set

x is complex set

x is complex set

d is complex set

x is complex set

(a,c,x,(- 1)) is complex set

(- 1) ^2 is complex real ext-real set

(- 1) * (- 1) is non zero complex real ext-real set

a * ((- 1) ^2) is complex set

c * (- 1) is complex set

(a * ((- 1) ^2)) + (c * (- 1)) is complex set

((a * ((- 1) ^2)) + (c * (- 1))) + x is complex set

(x,d,x,(- 1)) is complex set

x * ((- 1) ^2) is complex set

d * (- 1) is complex set

(x * ((- 1) ^2)) + (d * (- 1)) is complex set

((x * ((- 1) ^2)) + (d * (- 1))) + x is complex set

(a,c,x,0) is complex set

0 ^2 is complex real ext-real set

0 * 0 is complex real ext-real set

a * (0 ^2) is complex set

c * 0 is complex set

(a * (0 ^2)) + (c * 0) is complex set

((a * (0 ^2)) + (c * 0)) + x is complex set

(x,d,x,0) is complex set

x * (0 ^2) is complex set

d * 0 is complex set

(x * (0 ^2)) + (d * 0) is complex set

((x * (0 ^2)) + (d * 0)) + x is complex set

(a,c,x,1) is complex set

1 ^2 is complex real ext-real set

1 * 1 is non zero complex real ext-real set

a * (1 ^2) is complex set

c * 1 is complex set

(a * (1 ^2)) + (c * 1) is complex set

((a * (1 ^2)) + (c * 1)) + x is complex set

(x,d,x,1) is complex set

x * (1 ^2) is complex set

d * 1 is complex set

(x * (1 ^2)) + (d * 1) is complex set

((x * (1 ^2)) + (d * 1)) + x is complex set

a is complex real ext-real set

2 * a is complex real ext-real M2( REAL )

c is complex real ext-real set

- c is complex real ext-real set

x is complex real ext-real set

delta (a,c,x) is complex real ext-real set

sqrt (delta (a,c,x)) is complex real ext-real set

(- c) + (sqrt (delta (a,c,x))) is complex real ext-real set

((- c) + (sqrt (delta (a,c,x)))) / (2 * a) is complex real ext-real M2( REAL )

(- c) - (sqrt (delta (a,c,x))) is complex real ext-real set

((- c) - (sqrt (delta (a,c,x)))) / (2 * a) is complex real ext-real M2( REAL )

a * x is complex real ext-real set

a ^2 is complex real ext-real set

a * a is complex real ext-real set

d is complex real ext-real set

d ^2 is complex real ext-real set

d * d is complex real ext-real set

(a ^2) * (d ^2) is complex real ext-real set

a * c is complex real ext-real set

(a * c) * d is complex real ext-real set

((a ^2) * (d ^2)) + ((a * c) * d) is complex real ext-real set

(a,c,x,d) is complex real ext-real set

a * (d ^2) is complex real ext-real set

c * d is complex real ext-real set

(a * (d ^2)) + (c * d) is complex real ext-real set

((a * (d ^2)) + (c * d)) + x is complex real ext-real set

a * (((a * (d ^2)) + (c * d)) + x) is complex real ext-real set

a * 0 is complex real ext-real M2( REAL )

a * (a * (d ^2)) is complex real ext-real set

a * (c * d) is complex real ext-real set

(a * (a * (d ^2))) + (a * (c * d)) is complex real ext-real set

((a * (a * (d ^2))) + (a * (c * d))) + (a * x) is complex real ext-real set

c ^2 is complex real ext-real set

c * c is complex real ext-real set

(c ^2) / 4 is complex real ext-real M2( REAL )

(((a ^2) * (d ^2)) + ((a * c) * d)) + ((c ^2) / 4) is complex real ext-real M2( REAL )

4 " is non zero complex real ext-real positive M2( REAL )

(c ^2) * (4 ") is complex real ext-real M2( REAL )

((((a ^2) * (d ^2)) + ((a * c) * d)) + ((c ^2) / 4)) - ((c ^2) * (4 ")) is complex real ext-real M2( REAL )

4 * (a * x) is complex real ext-real M2( REAL )

(4 * (a * x)) * (4 ") is complex real ext-real M2( REAL )

- ((4 * (a * x)) * (4 ")) is complex real ext-real M2( REAL )

4 * a is complex real ext-real M2( REAL )

(4 * a) * x is complex real ext-real M2( REAL )

(c ^2) - ((4 * a) * x) is complex real ext-real M2( REAL )

a * d is complex real ext-real set

c / 2 is complex real ext-real M2( REAL )

(a * d) + (c / 2) is complex real ext-real M2( REAL )

(c ^2) - (4 * (a * x)) is complex real ext-real M2( REAL )

((c ^2) - (4 * (a * x))) / 4 is complex real ext-real M2( REAL )

sqrt (((c ^2) - (4 * (a * x))) / 4) is complex real ext-real M2( REAL )

((a * d) + (c / 2)) - (sqrt (((c ^2) - (4 * (a * x))) / 4)) is complex real ext-real M2( REAL )

sqrt ((c ^2) - (4 * (a * x))) is complex real ext-real M2( REAL )

(sqrt ((c ^2) - (4 * (a * x)))) / 2 is complex real ext-real M2( REAL )

2 " is non zero complex real ext-real positive M2( REAL )

c * (2 ") is complex real ext-real M2( REAL )

(sqrt ((c ^2) - (4 * (a * x)))) * (2 ") is complex real ext-real M2( REAL )

(c * (2 ")) - ((sqrt ((c ^2) - (4 * (a * x)))) * (2 ")) is complex real ext-real M2( REAL )

- ((c * (2 ")) - ((sqrt ((c ^2) - (4 * (a * x)))) * (2 "))) is complex real ext-real M2( REAL )

(- c) * (2 ") is complex real ext-real M2( REAL )

(sqrt (delta (a,c,x))) * (2 ") is complex real ext-real M2( REAL )

((- c) * (2 ")) + ((sqrt (delta (a,c,x))) * (2 ")) is complex real ext-real M2( REAL )

(((- c) * (2 ")) + ((sqrt (delta (a,c,x))) * (2 "))) / a is complex real ext-real M2( REAL )

a " is complex real ext-real set

(((- c) * (2 ")) + ((sqrt (delta (a,c,x))) * (2 "))) * (a ") is complex real ext-real M2( REAL )

(2 ") * (a ") is complex real ext-real M2( REAL )

((- c) + (sqrt (delta (a,c,x)))) * ((2 ") * (a ")) is complex real ext-real M2( REAL )

(2 * a) " is complex real ext-real M2( REAL )

((- c) + (sqrt (delta (a,c,x)))) * ((2 * a) ") is complex real ext-real M2( REAL )

((a * d) + (c / 2)) + (sqrt (((c ^2) - (4 * (a * x))) / 4)) is complex real ext-real M2( REAL )

- (sqrt (((c ^2) - (4 * (a * x))) / 4)) is complex real ext-real M2( REAL )

- ((sqrt ((c ^2) - (4 * (a * x)))) / 2) is complex real ext-real M2( REAL )

(c * (2 ")) + ((sqrt ((c ^2) - (4 * (a * x)))) * (2 ")) is complex real ext-real M2( REAL )

- ((c * (2 ")) + ((sqrt ((c ^2) - (4 * (a * x)))) * (2 "))) is complex real ext-real M2( REAL )

((- c) * (2 ")) - ((sqrt (delta (a,c,x))) * (2 ")) is complex real ext-real M2( REAL )

(((- c) * (2 ")) - ((sqrt (delta (a,c,x))) * (2 "))) / a is complex real ext-real M2( REAL )

(((- c) * (2 ")) - ((sqrt (delta (a,c,x))) * (2 "))) * (a ") is complex real ext-real M2( REAL )

((- c) - (sqrt (delta (a,c,x)))) * ((2 ") * (a ")) is complex real ext-real M2( REAL )

((- c) - (sqrt (delta (a,c,x)))) * ((2 * a) ") is complex real ext-real M2( REAL )

0 / 4 is complex real ext-real M2( REAL )

((a * d) + (c / 2)) ^2 is complex real ext-real M2( REAL )

((a * d) + (c / 2)) * ((a * d) + (c / 2)) is complex real ext-real set

(sqrt (((c ^2) - (4 * (a * x))) / 4)) ^2 is complex real ext-real M2( REAL )

(sqrt (((c ^2) - (4 * (a * x))) / 4)) * (sqrt (((c ^2) - (4 * (a * x))) / 4)) is complex real ext-real set

(((a * d) + (c / 2)) - (sqrt (((c ^2) - (4 * (a * x))) / 4))) * (((a * d) + (c / 2)) + (sqrt (((c ^2) - (4 * (a * x))) / 4))) is complex real ext-real M2( REAL )

x is complex real ext-real set

(a,c,x,x) is complex real ext-real set

x ^2 is complex real ext-real set

x * x is complex real ext-real set

a * (x ^2) is complex real ext-real set

c * x is complex real ext-real set

(a * (x ^2)) + (c * x) is complex real ext-real set

((a * (x ^2)) + (c * x)) + x is complex real ext-real set

a is complex set

c is complex set

x is complex set

delta (a,c,x) is complex set

x is complex set

(a,c,x,x) is complex set

x ^2 is complex set

x * x is complex set

a * (x ^2) is complex set

c * x is complex set

(a * (x ^2)) + (c * x) is complex set

((a * (x ^2)) + (c * x)) + x is complex set

2 * a is complex set

c / (2 * a) is complex set

- (c / (2 * a)) is complex set

a ^2 is complex set

a * a is complex set

(a ^2) * (x ^2) is complex set

a * c is complex set

(a * c) * x is complex set

((a ^2) * (x ^2)) + ((a * c) * x) is complex set

c ^2 is complex set

c * c is complex set

4 * a is complex set

(4 * a) * x is complex set

(c ^2) - ((4 * a) * x) is complex set

a * (((a * (x ^2)) + (c * x)) + x) is complex set

a * x is complex set

(((a ^2) * (x ^2)) + ((a * c) * x)) + (a * x) is complex set

a * x is complex set

(a * x) ^2 is complex set

(a * x) * (a * x) is complex set

(a * x) * c is complex set

2 " is non zero complex real ext-real positive M2( REAL )

((a * x) * c) * (2 ") is complex set

2 * (((a * x) * c) * (2 ")) is complex set

((a * x) ^2) + (2 * (((a * x) * c) * (2 "))) is complex set

c / 2 is complex set

(c / 2) ^2 is complex set

(c / 2) * (c / 2) is complex set

(((a * x) ^2) + (2 * (((a * x) * c) * (2 ")))) + ((c / 2) ^2) is complex set

(a * x) + (c / 2) is complex set

((a * x) + (c / 2)) ^2 is complex set

((a * x) + (c / 2)) * ((a * x) + (c / 2)) is complex set

c * (2 ") is complex set

- (c * (2 ")) is complex set

(- (c * (2 "))) / a is complex set

(- 1) * (c * (2 ")) is complex set

a " is complex set

((- 1) * (c * (2 "))) * (a ") is complex set

(2 ") * (a ") is complex set

c * ((2 ") * (a ")) is complex set

(c * ((2 ") * (a "))) * 1 is complex set

- ((c * ((2 ") * (a "))) * 1) is complex set

(2 * a) " is complex set

c * ((2 * a) ") is complex set

- (c * ((2 * a) ")) is complex set

a is complex real ext-real set

c is complex real ext-real set

x is complex real ext-real set

delta (a,c,x) is complex real ext-real set

a * x is complex real ext-real set

c ^2 is complex real ext-real set

c * c is complex real ext-real set

4 * a is complex real ext-real M2( REAL )

(4 * a) * x is complex real ext-real M2( REAL )

(c ^2) - ((4 * a) * x) is complex real ext-real M2( REAL )

4 * (a * x) is complex real ext-real M2( REAL )

(c ^2) - (4 * (a * x)) is complex real ext-real M2( REAL )

4 " is non zero complex real ext-real positive M2( REAL )

((c ^2) - (4 * (a * x))) * (4 ") is complex real ext-real M2( REAL )

d is complex real ext-real set

(a,c,x,d) is complex real ext-real set

d ^2 is complex real ext-real set

d * d is complex real ext-real set

a * (d ^2) is complex real ext-real set

c * d is complex real ext-real set

(a * (d ^2)) + (c * d) is complex real ext-real set

((a * (d ^2)) + (c * d)) + x is complex real ext-real set

a ^2 is complex real ext-real set

a * a is complex real ext-real set

(a ^2) * (d ^2) is complex real ext-real set

a * c is complex real ext-real set

(a * c) * d is complex real ext-real set

((a ^2) * (d ^2)) + ((a * c) * d) is complex real ext-real set

a * (((a * (d ^2)) + (c * d)) + x) is complex real ext-real set

a * 0 is complex real ext-real M2( REAL )

(c ^2) / 4 is complex real ext-real M2( REAL )

(((a ^2) * (d ^2)) + ((a * c) * d)) + ((c ^2) / 4) is complex real ext-real M2( REAL )

(c ^2) * (4 ") is complex real ext-real M2( REAL )

(4 * (a * x)) * (4 ") is complex real ext-real M2( REAL )

((c ^2) * (4 ")) - ((4 * (a * x)) * (4 ")) is complex real ext-real M2( REAL )

((((a ^2) * (d ^2)) + ((a * c) * d)) + ((c ^2) / 4)) - (((c ^2) * (4 ")) - ((4 * (a * x)) * (4 "))) is complex real ext-real M2( REAL )

a * d is complex real ext-real set

c / 2 is complex real ext-real M2( REAL )

(a * d) + (c / 2) is complex real ext-real M2( REAL )

((a * d) + (c / 2)) ^2 is complex real ext-real M2( REAL )

((a * d) + (c / 2)) * ((a * d) + (c / 2)) is complex real ext-real set

a is complex real ext-real set

c is complex set

x is complex set

x / c is complex set

- (x / c) is complex set

(0,c,x,a) is complex set

a ^2 is complex real ext-real set

a * a is complex real ext-real set

0 * (a ^2) is complex real ext-real set

c * a is complex set

(0 * (a ^2)) + (c * a) is complex set

((0 * (a ^2)) + (c * a)) + x is complex set

- x is complex set

(- x) / c is complex set

(- 1) * x is complex set

c " is complex set

((- 1) * x) * (c ") is complex set

x * (c ") is complex set

(- 1) * (x * (c ")) is complex set

(- 1) * (x / c) is complex set

a is complex set

(0,0,0,a) is complex set

a ^2 is complex set

a * a is complex set

0 * (a ^2) is complex set

0 * a is complex set

(0 * (a ^2)) + (0 * a) is complex set

((0 * (a ^2)) + (0 * a)) + 0 is complex set

a is complex set

c is complex set

(0,0,a,c) is complex set

c ^2 is complex set

c * c is complex set

0 * (c ^2) is complex set

0 * c is complex set

(0 * (c ^2)) + (0 * c) is complex set

((0 * (c ^2)) + (0 * c)) + a is complex set

a is complex set

c is complex set

x is complex set

c - x is complex set

x is complex set

c - x is complex set

(c - x) * (c - x) is complex set

a * ((c - x) * (c - x)) is complex set

a is complex real ext-real set

c is complex real ext-real set

x is complex real ext-real set

x is complex real ext-real set

(a,c,x,x) is set

c - x is complex real ext-real set

c - x is complex real ext-real set

(c - x) * (c - x) is complex real ext-real set

a * ((c - x) * (c - x)) is complex real ext-real set

a is complex real ext-real M2( REAL )

c is complex real ext-real M2( REAL )

x is complex real ext-real M2( REAL )

x is complex real ext-real M2( REAL )

(a,c,x,x) is complex real ext-real set

c - x is complex real ext-real set

c - x is complex real ext-real set

(c - x) * (c - x) is complex real ext-real set

a * ((c - x) * (c - x)) is complex real ext-real set

a is complex real ext-real set

c is complex real ext-real set

a + c is complex real ext-real set

- (a + c) is complex real ext-real set

a * c is complex real ext-real set

x is complex set

x is complex set

d is complex set

x / x is complex set

d / x is complex set

x is complex real ext-real set

x - a is complex real ext-real set

x - c is complex real ext-real set

(x - a) * (x - c) is complex real ext-real set

x ^2 is complex real ext-real set

x * x is complex real ext-real set

((x - a) * (x - c)) - (x ^2) is complex real ext-real set

(x,x,d,x) is complex set

x * (x ^2) is complex set

x * x is complex set

(x * (x ^2)) + (x * x) is complex set

((x * (x ^2)) + (x * x)) + d is complex set

(x,x,a,c) is set

x * ((x - a) * (x - c)) is complex set

x * (((x - a) * (x - c)) - (x ^2)) is complex set

(x * x) + d is complex set

((x * x) + d) / x is complex set

x " is complex set

(x ") * ((x * x) + d) is complex set

(x ") * (x * x) is complex set

(x ") * d is complex set

((x ") * (x * x)) + ((x ") * d) is complex set

x * c is complex real ext-real set

(x * x) - (x * c) is complex real ext-real set

a * x is complex real ext-real set

((x * x) - (x * c)) - (a * x) is complex real ext-real set

(((x * x) - (x * c)) - (a * x)) + (a * c) is complex real ext-real set

(x ") * x is complex set

((x ") * x) * x is complex set

(x ^2) + (((x ") * x) * x) is complex set

((x ^2) + (((x ") * x) * x)) + ((x ") * d) is complex set

(a + c) * x is complex real ext-real set

(x ^2) - ((a + c) * x) is complex real ext-real set

((x ^2) - ((a + c) * x)) + (a * c) is complex real ext-real set

(x / x) * x is complex set

(x ^2) + ((x / x) * x) is complex set

((x ^2) + ((x / x) * x)) + ((x ") * d) is complex set

((x ^2) + ((x / x) * x)) + (d / x) is complex set

(1,(- (a + c)),(a * c),x) is complex real ext-real set

1 * (x ^2) is complex real ext-real set

(- (a + c)) * x is complex real ext-real set

(1 * (x ^2)) + ((- (a + c)) * x) is complex real ext-real set

((1 * (x ^2)) + ((- (a + c)) * x)) + (a * c) is complex real ext-real set

(1,(x / x),(d / x),x) is complex set

(1 * (x ^2)) + ((x / x) * x) is complex set

((1 * (x ^2)) + ((x / x) * x)) + (d / x) is complex set

a is complex set

d is complex set

3 is non zero natural complex real ext-real positive V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

d |^ 3 is complex set

a * (d |^ 3) is complex set

c is complex set

d ^2 is complex set

d * d is complex set

c * (d ^2) is complex set

(a * (d |^ 3)) + (c * (d ^2)) is complex set

x is complex set

x * d is complex set

((a * (d |^ 3)) + (c * (d ^2))) + (x * d) is complex set

x is complex set

(((a * (d |^ 3)) + (c * (d ^2))) + (x * d)) + x is complex set

a is complex set

c is complex set

x is complex set

x is complex set

d is complex set

(a,c,x,x,d) is set

d |^ 3 is complex set

a * (d |^ 3) is complex set

d ^2 is complex set

d * d is complex set

c * (d ^2) is complex set

(a * (d |^ 3)) + (c * (d ^2)) is complex set

x * d is complex set

((a * (d |^ 3)) + (c * (d ^2))) + (x * d) is complex set

(((a * (d |^ 3)) + (c * (d ^2))) + (x * d)) + x is complex set

a is complex real ext-real set

c is complex real ext-real set

x is complex real ext-real set

x is complex real ext-real set

d is complex real ext-real set

(a,c,x,x,d) is complex set

d |^ 3 is complex real ext-real set

a * (d |^ 3) is complex real ext-real set

d ^2 is complex real ext-real set

d * d is complex real ext-real set

c * (d ^2) is complex real ext-real set

(a * (d |^ 3)) + (c * (d ^2)) is complex real ext-real set

x * d is complex real ext-real set

((a * (d |^ 3)) + (c * (d ^2))) + (x * d) is complex real ext-real set

(((a * (d |^ 3)) + (c * (d ^2))) + (x * d)) + x is complex real ext-real set

a is complex real ext-real M2( REAL )

c is complex real ext-real M2( REAL )

x is complex real ext-real M2( REAL )

x is complex real ext-real M2( REAL )

d is complex real ext-real M2( REAL )

(a,c,x,x,d) is complex real ext-real set

d |^ 3 is complex real ext-real set

a * (d |^ 3) is complex real ext-real set

d ^2 is complex real ext-real set

d * d is complex real ext-real set

c * (d ^2) is complex real ext-real set

(a * (d |^ 3)) + (c * (d ^2)) is complex real ext-real set

x * d is complex real ext-real set

((a * (d |^ 3)) + (c * (d ^2))) + (x * d) is complex real ext-real set

(((a * (d |^ 3)) + (c * (d ^2))) + (x * d)) + x is complex real ext-real set

2 * 1 is non zero natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

(2 * 1) + 1 is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

a is complex real ext-real set

c is complex real ext-real set

x is complex real ext-real set

x is complex real ext-real set

d is complex real ext-real set

x is complex real ext-real set

u is complex real ext-real set

v is complex real ext-real set

(- 1) |^ 3 is complex real ext-real M2( REAL )

2 + 1 is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

1 |^ (2 + 1) is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

- (1 |^ (2 + 1)) is complex real ext-real M2( REAL )

1 |^ 2 is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

(1 |^ 2) * 1 is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

- ((1 |^ 2) * 1) is complex real ext-real M2( REAL )

0 |^ 3 is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

2 |^ 1 is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

2 to_power 1 is complex real ext-real M2( REAL )

2 |^ 3 is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

2 |^ (2 + 1) is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

1 + 1 is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

2 |^ (1 + 1) is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

(2 |^ (1 + 1)) * 2 is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

(2 |^ 1) * 2 is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

((2 |^ 1) * 2) * 2 is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

2 * 2 is non zero natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

(2 |^ 1) * (2 * 2) is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

(a,c,x,x,2) is complex real ext-real set

2 |^ 3 is natural complex real ext-real set

a * (2 |^ 3) is complex real ext-real set

2 ^2 is complex real ext-real set

2 * 2 is non zero complex real ext-real set

c * (2 ^2) is complex real ext-real set

(a * (2 |^ 3)) + (c * (2 ^2)) is complex real ext-real set

x * 2 is complex real ext-real set

((a * (2 |^ 3)) + (c * (2 ^2))) + (x * 2) is complex real ext-real set

(((a * (2 |^ 3)) + (c * (2 ^2))) + (x * 2)) + x is complex real ext-real set

(d,x,u,v,2) is complex real ext-real set

d * (2 |^ 3) is complex real ext-real set

x * (2 ^2) is complex real ext-real set

(d * (2 |^ 3)) + (x * (2 ^2)) is complex real ext-real set

u * 2 is complex real ext-real set

((d * (2 |^ 3)) + (x * (2 ^2))) + (u * 2) is complex real ext-real set

(((d * (2 |^ 3)) + (x * (2 ^2))) + (u * 2)) + v is complex real ext-real set

(a,c,x,x,1) is complex real ext-real set

1 |^ 3 is natural complex real ext-real set

a * (1 |^ 3) is complex real ext-real set

1 ^2 is complex real ext-real set

1 * 1 is non zero complex real ext-real set

c * (1 ^2) is complex real ext-real set

(a * (1 |^ 3)) + (c * (1 ^2)) is complex real ext-real set

x * 1 is complex real ext-real set

((a * (1 |^ 3)) + (c * (1 ^2))) + (x * 1) is complex real ext-real set

(((a * (1 |^ 3)) + (c * (1 ^2))) + (x * 1)) + x is complex real ext-real set

(d,x,u,v,1) is complex real ext-real set

d * (1 |^ 3) is complex real ext-real set

x * (1 ^2) is complex real ext-real set

(d * (1 |^ 3)) + (x * (1 ^2)) is complex real ext-real set

u * 1 is complex real ext-real set

((d * (1 |^ 3)) + (x * (1 ^2))) + (u * 1) is complex real ext-real set

(((d * (1 |^ 3)) + (x * (1 ^2))) + (u * 1)) + v is complex real ext-real set

a * 1 is complex real ext-real M2( REAL )

c * 1 is complex real ext-real M2( REAL )

(a * 1) + (c * 1) is complex real ext-real M2( REAL )

x * 1 is complex real ext-real M2( REAL )

((a * 1) + (c * 1)) + (x * 1) is complex real ext-real M2( REAL )

(((a * 1) + (c * 1)) + (x * 1)) + x is complex real ext-real M2( REAL )

a + c is complex real ext-real set

(a + c) + x is complex real ext-real set

((a + c) + x) + x is complex real ext-real set

d * 1 is complex real ext-real M2( REAL )

x * 1 is complex real ext-real M2( REAL )

(d * 1) + (x * 1) is complex real ext-real M2( REAL )

u * 1 is complex real ext-real M2( REAL )

((d * 1) + (x * 1)) + (u * 1) is complex real ext-real M2( REAL )

(((d * 1) + (x * 1)) + (u * 1)) + v is complex real ext-real M2( REAL )

d + x is complex real ext-real set

(d + x) + u is complex real ext-real set

((d + x) + u) + v is complex real ext-real set

(a,c,x,x,0) is complex real ext-real set

0 |^ 3 is natural complex real ext-real set

a * (0 |^ 3) is complex real ext-real set

0 ^2 is complex real ext-real set

0 * 0 is complex real ext-real set

c * (0 ^2) is complex real ext-real set

(a * (0 |^ 3)) + (c * (0 ^2)) is complex real ext-real set

x * 0 is complex real ext-real set

((a * (0 |^ 3)) + (c * (0 ^2))) + (x * 0) is complex real ext-real set

(((a * (0 |^ 3)) + (c * (0 ^2))) + (x * 0)) + x is complex real ext-real set

(d,x,u,v,0) is complex real ext-real set

d * (0 |^ 3) is complex real ext-real set

x * (0 ^2) is complex real ext-real set

(d * (0 |^ 3)) + (x * (0 ^2)) is complex real ext-real set

u * 0 is complex real ext-real set

((d * (0 |^ 3)) + (x * (0 ^2))) + (u * 0) is complex real ext-real set

(((d * (0 |^ 3)) + (x * (0 ^2))) + (u * 0)) + v is complex real ext-real set

(a,c,x,x,(- 1)) is complex real ext-real set

(- 1) |^ 3 is complex real ext-real set

a * ((- 1) |^ 3) is complex real ext-real set

(- 1) ^2 is complex real ext-real set

(- 1) * (- 1) is non zero complex real ext-real set

c * ((- 1) ^2) is complex real ext-real set

(a * ((- 1) |^ 3)) + (c * ((- 1) ^2)) is complex real ext-real set

x * (- 1) is complex real ext-real set

((a * ((- 1) |^ 3)) + (c * ((- 1) ^2))) + (x * (- 1)) is complex real ext-real set

(((a * ((- 1) |^ 3)) + (c * ((- 1) ^2))) + (x * (- 1))) + x is complex real ext-real set

(d,x,u,v,(- 1)) is complex real ext-real set

d * ((- 1) |^ 3) is complex real ext-real set

x * ((- 1) ^2) is complex real ext-real set

(d * ((- 1) |^ 3)) + (x * ((- 1) ^2)) is complex real ext-real set

u * (- 1) is complex real ext-real set

((d * ((- 1) |^ 3)) + (x * ((- 1) ^2))) + (u * (- 1)) is complex real ext-real set

(((d * ((- 1) |^ 3)) + (x * ((- 1) ^2))) + (u * (- 1))) + v is complex real ext-real set

a is complex real ext-real set

c is complex real ext-real set

x is complex real ext-real set

c - x is complex real ext-real set

x is complex real ext-real set

c - x is complex real ext-real set

(c - x) * (c - x) is complex real ext-real set

d is complex real ext-real set

c - d is complex real ext-real set

((c - x) * (c - x)) * (c - d) is complex real ext-real set

a * (((c - x) * (c - x)) * (c - d)) is complex real ext-real set

a is complex real ext-real set

c is complex real ext-real set

x is complex real ext-real set

x is complex real ext-real set

d is complex real ext-real set

(a,c,x,x,d) is set

c - x is complex real ext-real set

c - x is complex real ext-real set

(c - x) * (c - x) is complex real ext-real set

c - d is complex real ext-real set

((c - x) * (c - x)) * (c - d) is complex real ext-real set

a * (((c - x) * (c - x)) * (c - d)) is complex real ext-real set

a is complex real ext-real M2( REAL )

c is complex real ext-real M2( REAL )

x is complex real ext-real M2( REAL )

x is complex real ext-real M2( REAL )

d is complex real ext-real M2( REAL )

(a,c,x,x,d) is complex real ext-real set

c - x is complex real ext-real set

c - x is complex real ext-real set

(c - x) * (c - x) is complex real ext-real set

c - d is complex real ext-real set

((c - x) * (c - x)) * (c - d) is complex real ext-real set

a * (((c - x) * (c - x)) * (c - d)) is complex real ext-real set

a is complex real ext-real set

c is complex real ext-real set

c / a is complex real ext-real set

x is complex real ext-real set

x / a is complex real ext-real set

x is complex real ext-real set

x / a is complex real ext-real set

d is complex real ext-real set

x is complex real ext-real set

d + x is complex real ext-real set

d * x is complex real ext-real set

u is complex real ext-real set

(d + x) + u is complex real ext-real set

- ((d + x) + u) is complex real ext-real set

x * u is complex real ext-real set

(d * x) + (x * u) is complex real ext-real set

d * u is complex real ext-real set

((d * x) + (x * u)) + (d * u) is complex real ext-real set

(d * x) * u is complex real ext-real set

- ((d * x) * u) is complex real ext-real set

t is complex real ext-real set

t |^ 3 is complex real ext-real set

a * (t |^ 3) is complex real ext-real set

t ^2 is complex real ext-real set

t * t is complex real ext-real set

c * (t ^2) is complex real ext-real set

(a * (t |^ 3)) + (c * (t ^2)) is complex real ext-real set

x * t is complex real ext-real set

((a * (t |^ 3)) + (c * (t ^2))) + (x * t) is complex real ext-real set

(((a * (t |^ 3)) + (c * (t ^2))) + (x * t)) + x is complex real ext-real set

t - d is complex real ext-real set

t - x is complex real ext-real set

(t - d) * (t - x) is complex real ext-real set

t - u is complex real ext-real set

((t - d) * (t - x)) * (t - u) is complex real ext-real set

t |^ 1 is complex real ext-real set

t to_power 1 is complex real ext-real set

2 + 1 is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

t |^ (2 + 1) is complex real ext-real set

1 + 1 is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

t |^ (1 + 1) is complex real ext-real set

(t |^ (1 + 1)) * t is complex real ext-real set

(t |^ 1) * t is complex real ext-real set

((t |^ 1) * t) * t is complex real ext-real set

(t * t) * t is complex real ext-real set

(a,c,x,x,t) is complex real ext-real set

(a,t,d,x,u) is complex real ext-real set

a * (((t - d) * (t - x)) * (t - u)) is complex real ext-real set

((((a * (t |^ 3)) + (c * (t ^2))) + (x * t)) + x) / a is complex real ext-real set

a " is complex real ext-real set

(a ") * ((((a * (t |^ 3)) + (c * (t ^2))) + (x * t)) + x) is complex real ext-real set

(a ") * a is complex real ext-real set

((a ") * a) * (t |^ 3) is complex real ext-real set

(a ") * c is complex real ext-real set

((a ") * c) * (t ^2) is complex real ext-real set

(((a ") * a) * (t |^ 3)) + (((a ") * c) * (t ^2)) is complex real ext-real set

(x * t) + x is complex real ext-real set

(a ") * ((x * t) + x) is complex real ext-real set

((((a ") * a) * (t |^ 3)) + (((a ") * c) * (t ^2))) + ((a ") * ((x * t) + x)) is complex real ext-real set

1 * (t |^ 3) is complex real ext-real M2( REAL )

(1 * (t |^ 3)) + (((a ") * c) * (t ^2)) is complex real ext-real M2( REAL )

(a ") * x is complex real ext-real set

((a ") * x) * t is complex real ext-real set

(a ") * x is complex real ext-real set

(((a ") * x) * t) + ((a ") * x) is complex real ext-real set

((1 * (t |^ 3)) + (((a ") * c) * (t ^2))) + ((((a ") * x) * t) + ((a ") * x)) is complex real ext-real M2( REAL )

(c / a) * (t ^2) is complex real ext-real set

(1 * (t |^ 3)) + ((c / a) * (t ^2)) is complex real ext-real M2( REAL )

((1 * (t |^ 3)) + ((c / a) * (t ^2))) + ((((a ") * x) * t) + ((a ") * x)) is complex real ext-real M2( REAL )

(x / a) * t is complex real ext-real set

((x / a) * t) + ((a ") * x) is complex real ext-real set

((1 * (t |^ 3)) + ((c / a) * (t ^2))) + (((x / a) * t) + ((a ") * x)) is complex real ext-real M2( REAL )

((x / a) * t) + (x / a) is complex real ext-real set

((1 * (t |^ 3)) + ((c / a) * (t ^2))) + (((x / a) * t) + (x / a)) is complex real ext-real M2( REAL )

(1,(c / a),(x / a),(x / a),t) is complex real ext-real set

1 * (t |^ 3) is complex real ext-real set

(1 * (t |^ 3)) + ((c / a) * (t ^2)) is complex real ext-real set

((1 * (t |^ 3)) + ((c / a) * (t ^2))) + ((x / a) * t) is complex real ext-real set

(((1 * (t |^ 3)) + ((c / a) * (t ^2))) + ((x / a) * t)) + (x / a) is complex real ext-real set

(1,(- ((d + x) + u)),(((d * x) + (x * u)) + (d * u)),(- ((d * x) * u)),t) is complex real ext-real set

(- ((d + x) + u)) * (t ^2) is complex real ext-real set

(1 * (t |^ 3)) + ((- ((d + x) + u)) * (t ^2)) is complex real ext-real set

(((d * x) + (x * u)) + (d * u)) * t is complex real ext-real set

((1 * (t |^ 3)) + ((- ((d + x) + u)) * (t ^2))) + ((((d * x) + (x * u)) + (d * u)) * t) is complex real ext-real set

(((1 * (t |^ 3)) + ((- ((d + x) + u)) * (t ^2))) + ((((d * x) + (x * u)) + (d * u)) * t)) + (- ((d * x) * u)) is complex real ext-real set

a is complex real ext-real set

a |^ 3 is complex real ext-real set

a ^2 is complex real ext-real set

a * a is complex real ext-real set

c is complex real ext-real set

a + c is complex real ext-real set

(a + c) |^ 3 is complex real ext-real set

3 * c is complex real ext-real M2( REAL )

(3 * c) * (a ^2) is complex real ext-real M2( REAL )

c ^2 is complex real ext-real set

c * c is complex real ext-real set

3 * (c ^2) is complex real ext-real M2( REAL )

(3 * (c ^2)) * a is complex real ext-real M2( REAL )

((3 * c) * (a ^2)) + ((3 * (c ^2)) * a) is complex real ext-real M2( REAL )

(a |^ 3) + (((3 * c) * (a ^2)) + ((3 * (c ^2)) * a)) is complex real ext-real M2( REAL )

c |^ 3 is complex real ext-real set

((a |^ 3) + (((3 * c) * (a ^2)) + ((3 * (c ^2)) * a))) + (c |^ 3) is complex real ext-real M2( REAL )

2 + 1 is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

(a + c) |^ (2 + 1) is complex real ext-real set

1 + 1 is natural complex real ext-real V33() V34() V35() V36() V37() V38() V40() V53() M3( REAL , NAT )

(a + c) |^ (1 + 1) is complex real ext-real set

((a + c) |^ (1 + 1)) * (a + c) is complex real ext-real set

(a + c) |^ 1 is complex real ext-real set

((a + c) |^ 1) * (a + c) is complex real ext-real set

(((a + c) |^ 1) * (a + c)) * (a + c) is complex real ext-real set

(a + c) ^2 is complex real ext-real set

(a + c) * (a + c) is complex real ext-real set

((a + c) |^ 1) * ((a + c) ^2) is complex real ext-real set

(a + c) to_power 1 is complex real ext-real set

2 * a is complex real ext-real M2( REAL )

(2 * a) * c is complex real ext-real M2( REAL )

(a ^2) + ((2 * a) * c) is complex real ext-real M2( REAL )

((a ^2) + ((2 * a) * c)) + (c ^2) is complex real ext-real M2( REAL )

((a + c) to_power 1) * (((a ^2) + ((2 * a) * c)) + (c ^2)) is complex real ext-real M2( REAL )

(a + c) * (((a ^2) + ((2 * a) * c)) + (c ^2)) is complex real ext-real M2( REAL )

a * (a ^2) is complex real ext-real set

(2 + 1) * (c ^2) is complex real ext-real M2( REAL )

((2 + 1) * (c ^2)) * a is complex real ext-real M2( REAL )

((3 * c) * (a ^2)) + (((2 + 1) * (c ^2)) * a) is complex real ext-real M2( REAL )

(a * (a ^2)) + (((3 * c) * (a ^2)) + (((2 + 1) * (c ^2)) * a)) is complex real ext-real M2( REAL )

c * (c ^2) is complex real ext-real set

((a * (a ^2)) + (((3 * c) * (a ^2)) + (((2 + 1) * (c ^2)) * a))) + (c * (c ^2)) is complex real ext-real M2( REAL )

a |^ (2 + 1) is complex real ext-real set

a |^ (1 + 1) is complex real ext-real set

(a |^ (1 + 1)) * a is complex real ext-real set

a |^ 1 is complex real ext-real set

(a |^ 1) * a is complex real ext-real set

((a |^ 1) * a) * a is complex real ext-real set

(a |^ 1) * (a ^2) is complex real ext-real set

a to_power 1 is complex real ext-real set

(a to_power 1) * (a ^2) is complex real ext-real set

c |^ (2 + 1) is complex real ext-real set

c |^ (1 + 1) is complex real ext-real set

(c |^ (1 + 1)) * c is complex real ext-real set

c |^ 1 is complex real ext-real set

(c |^ 1) * c is complex real ext-real set

((c |^ 1) * c) * c is complex real ext-real set

(c |^ 1) * (c ^2) is complex real ext-real set

c to_power 1 is complex real ext-real set

(c to_power 1) * (c ^2) is complex real ext-real set

a is complex real ext-real set

3 * a is complex real ext-real M2( REAL )

c is complex real ext-real set

c / (3 * a) is complex real ext-real M2( REAL )

- (c / (3 * a)) is complex real ext-real M2( REAL )

c / a is complex real ext-real set

x is complex real ext-real set

x / a is complex real ext-real set

x is complex real ext-real set

x / a is complex real ext-real set

d is complex real ext-real set

(a,c,x,x,d) is complex real ext-real set

d |^ 3 is complex real ext-real set

a * (d |^ 3) is complex real ext-real set

d ^2 is complex real ext-real set

d * d is complex real ext-real set

c * (d ^2) is complex real ext-real set

(a * (d |^ 3)) + (c * (d ^2)) is complex real ext-real set

x * d is complex real ext-real set

((a * (d |^ 3)) + (c * (d ^2))) + (x * d) is complex real ext-real set

(((a * (d |^ 3)) + (c * (d ^2))) + (x * d)) + x is complex real ext-real set

d + (c / (3 * a)) is complex real ext-real M2( REAL )

x is complex real ext-real set

u is complex real ext-real set

v is complex real ext-real set

z2 is complex real ext-real set

3 * z2 is complex real ext-real M2( REAL )

(3 * z2) + x is complex real ext-real M2( REAL )

z2 ^2 is complex real ext-real set

z2 * z2 is complex real ext-real set

3 * (z2 ^2) is complex real ext-real M2( REAL )

x * z2 is complex real ext-real set

2 * (x * z2) is complex real ext-real M2( REAL )

(3 * (z2 ^2)) + (2 * (x * z2)) is complex real ext-real M2( REAL )

((3 * (z2 ^2)) + (2 * (x * z2))) + u is complex real ext-real M2( REAL )

z2 |^ 3 is complex real ext-real set

x * (z2 ^2) is complex real ext-real set

(z2 |^ 3) + (x * (z2 ^2)) is complex real ext-real set

u * z2 is complex real ext-real set

(u * z2) + v is complex real ext-real set

((z2 |^ 3) + (x * (z2 ^2))) + ((u * z2) + v) is complex real ext-real set

z1 is complex real ext-real set

z1 |^ 3 is complex real ext-real set

z1 ^2 is complex real ext-real set

z1 * z1 is complex real ext-real set

((3 * z2) + x) * (z1 ^2) is complex real ext-real M2( REAL )

(((3 * (z2 ^2)) + (2 * (x * z2))) + u) * z1 is complex real ext-real M2( REAL )

(((3 * z2) + x) * (z1 ^2)) + ((((3 * (z2 ^2)) + (2 * (x * z2))) + u) * z1) is complex real ext-real M2( REAL )

(z1 |^ 3) + ((((3 * z2) + x) * (z1 ^2)) + ((((3 * (z2 ^2)) + (2 * (x * z2))) + u) * z1)) is complex real ext-real M2( REAL )

((z1 |^ 3) + ((((3 * z2) + x) * (z1 ^2)) + ((((3 * (z2 ^2)) + (2 * (x * z2))) + u) * z1))) + (((z2 |^ 3) + (x * (z2 ^2))) + ((u * z2) + v)) is complex real ext-real M2( REAL )

a " is complex real ext-real set

(x * d) + x is complex real ext-real set

((a * (d |^ 3)) + (c * (d ^2))) + ((x * d) + x) is complex real ext-real set

(a ") * (((a * (d |^ 3)) + (c * (d ^2))) + ((x * d) + x)) is complex real ext-real set

(a ") * a is complex real ext-real set

((a ") * a) * (d |^ 3) is complex real ext-real set

(a ") * (c * (d ^2)) is complex real ext-real set

(((a ") * a) * (d |^ 3)) + ((a ") * (c * (d ^2))) is complex real ext-real set

(a ") * ((x * d) + x) is complex real ext-real set

((((a ") * a) * (d |^ 3)) + ((a ") * (c * (d ^2)))) + ((a ") * ((x * d) + x)) is complex real ext-real set

1 * (d |^ 3) is complex real ext-real M2( REAL )

(1 * (d |^ 3)) + ((a ") * (c * (d ^2))) is complex real ext-real M2( REAL )

((1 * (d |^ 3)) + ((a ") * (c * (d ^2)))) + ((a ") * ((x * d) + x)) is complex real ext-real M2( REAL )

(a ") * c is complex real ext-real set

((a ") * c) * (d ^2) is complex real ext-real set

(d |^ 3) + (((a ") * c) * (d ^2)) is complex real ext-real set

(a ") * x is complex real ext-real set

((a ") * x) * d is complex real ext-real set

((d |^ 3) + (((a ") * c) * (d ^2))) + (((a ") * x) * d) is complex real ext-real set

(a ") * x is complex real ext-real set

(((d |^ 3) + (((a ") * c) * (d ^2))) + (((a ") * x) * d)) + ((a ") * x) is complex real ext-real set

(c / a) * (d ^2) is complex real ext-real set

(d |^ 3) + ((c / a) * (d ^2)) is complex real ext-real set

((d |^ 3) + ((c / a) * (d ^2))) + (((a ") * x) * d) is complex real ext-real set

(((d |^ 3) + ((c / a) * (d ^2))) + (((a ") * x) * d)) + ((a ") * x) is complex real ext-real set

(x / a) * d is complex real ext-real set

((d |^ 3) + ((c / a) * (d ^2))) + ((x / a) * d) is complex real ext-real set

(((d |^ 3) + ((c / a) * (d ^2))) + ((x / a) * d)) + ((a ") * x) is complex real ext-real set

x * (d ^2) is complex real ext-real set

(d |^ 3) + (x * (d ^2)) is complex real ext-real set

u * d is complex real ext-real set

((d |^ 3) + (x * (d ^2))) + (u * d) is complex real ext-real set

(((d |^ 3) + (x * (d ^2))) + (u * d)) + v is complex real ext-real set

(3 * z2) * (z1 ^2) is complex real ext-real M2( REAL )

(3 * (z2 ^2)) * z1 is complex real ext-real M2( REAL )

((3 * z2) * (z1 ^2)) + ((3 * (z2 ^2)) * z1) is complex real ext-real M2( REAL )

(z1 |^ 3) + (((3 * z2) * (z1 ^2)) + ((3 * (z2 ^2)) * z1)) is complex real ext-real M2( REAL )

((z1 |^ 3) + (((3 * z2) * (z1 ^2)) + ((3 * (z2 ^2)) * z1))) + (z2 |^ 3) is complex real ext-real M2( REAL )

x * (z1 ^2) is complex real ext-real set

(2 * (x * z2)) * z1 is complex real ext-real M2( REAL )

(x * (z1 ^2)) + ((2 * (x * z2)) * z1) is complex real ext-real M2( REAL )

((x * (z1 ^2)) + ((2 * (x * z2)) * z1)) + (x * (z2 ^2)) is complex real ext-real M2( REAL )

(((z1 |^ 3) + (((3 * z2) * (z1 ^2)) + ((3 * (z2 ^2)) * z1))) + (z2 |^ 3)) + (((x * (z1 ^2)) + ((2 * (x * z2)) * z1)) + (x * (z2 ^2))) is complex real ext-real M2( REAL )

z1 + z2 is complex real ext-real set

u * (z1 + z2) is complex real ext-real set

((((z1 |^ 3) + (((3 * z2) * (z1 ^2)) + ((3 * (z2 ^2)) * z1))) + (z2 |^ 3)) + (((x * (z1 ^2)) + ((2 * (x * z2)) * z1)) + (x * (z2 ^2)))) + (u * (z1 + z2)) is complex real ext-real M2( REAL )

(((((z1 |^ 3) + (((3 * z2) * (z1 ^2)) + ((3 * (z2 ^2)) * z1))) + (z2 |^ 3)) + (((x * (z1 ^2)) + ((2 * (x * z2)) * z1)) + (x * (z2 ^2)))) + (u * (z1 + z2))) + v is complex real ext-real M2( REAL )

((2 * (x * z2)) * z1) + (x * (z1 ^2)) is complex real ext-real M2( REAL )

((z1 |^ 3) + (((3 * z2) * (z1 ^2)) + ((3 * (z2 ^2)) * z1))) + (((2 * (x * z2)) * z1) + (x * (z1 ^2))) is complex real ext-real M2( REAL )

u * z1 is complex real ext-real set

(u * z1) + (((z2 |^ 3) + (x * (z2 ^2))) + ((u * z2) + v)) is complex real ext-real set

(((z1 |^ 3) + (((3 * z2) * (z1 ^2)) + ((3 * (z2 ^2)) * z1))) + (((2 * (x * z2)) * z1) + (x * (z1 ^2)))) + ((u * z1) + (((z2 |^ 3) + (x * (z2 ^2))) + ((u * z2) + v))) is complex real ext-real M2( REAL )

a is complex real ext-real set

3 * a is complex real ext-real M2( REAL )

a ^2 is complex real ext-real set

a * a is complex real ext-real set

3 * (a ^2) is complex real ext-real M2( REAL )

c is complex real ext-real set

c / (3 * a) is complex real ext-real M2( REAL )

- (c / (3 * a)) is complex real ext-real M2( REAL )

c / a is complex real ext-real set

c ^2 is complex real ext-real set

c * c is complex real ext-real set

(c / (3 * a)) |^ 3 is complex real ext-real M2( REAL )

2 * ((c / (3 * a)) |^ 3) is complex real ext-real M2( REAL )

x is complex real ext-real set

x / a is complex real ext-real set

(3 * a) * x is complex real ext-real M2( REAL )

((3 * a) * x) - (c ^2) is complex real ext-real M2( REAL )

(((3 * a) * x) - (c ^2)) / (3 * (a ^2)) is complex real ext-real M2( REAL )

c * x is complex real ext-real set

x is complex real ext-real set

x / a is complex real ext-real set

(3 * a) * x is complex real ext-real M2( REAL )

((3 * a) * x) - (c * x) is complex real ext-real M2( REAL )

(((3 * a) * x) - (c * x)) / (3 * (a ^2)) is complex real ext-real M2( REAL )

(2 * ((c / (3 * a)) |^ 3)) + ((((3 * a) * x) - (c * x)) / (3 * (a ^2))) is complex real ext-real M2( REAL )

d is complex real ext-real set

(a,c,x,x,d) is complex real ext-real set

d |^ 3 is complex real ext-real set

a * (d |^ 3) is complex real ext-real set

d ^2 is complex real ext-real set

d * d is complex real ext-real set

c * (d ^2) is complex real ext-real set

(a * (d |^ 3)) + (c * (d ^2)) is complex real ext-real set

x * d is complex real ext-real set

((a