:: POLYEQ_4 semantic presentation

REAL is set
NAT is non zero epsilon-transitive epsilon-connected ordinal Element of K6(REAL)
K6(REAL) is set
COMPLEX is set
NAT is non zero epsilon-transitive epsilon-connected ordinal set
K6(NAT) is set
K6(NAT) is set
K7(NAT,REAL) is set
K6(K7(NAT,REAL)) is set
0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
sqrt 0 is complex real ext-real Element of REAL
4 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() Element of NAT
2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() Element of NAT
3 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() Element of NAT
1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() Element of NAT
8 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() Element of NAT
a is complex real ext-real Element of REAL
- a is complex real ext-real set
b is complex real ext-real Element of REAL
a / b is complex real ext-real set
2 * b is complex real ext-real set
x is complex real ext-real Element of REAL
x / b is complex real ext-real set
delta (b,a,x) is complex real ext-real Element of REAL
sqrt (delta (b,a,x)) is complex real ext-real Element of REAL
(- a) + (sqrt (delta (b,a,x))) is complex real ext-real set
((- a) + (sqrt (delta (b,a,x)))) / (2 * b) is complex real ext-real set
(- a) - (sqrt (delta (b,a,x))) is complex real ext-real set
((- a) - (sqrt (delta (b,a,x)))) / (2 * b) is complex real ext-real set
a ^2 is complex real ext-real Element of REAL
a * a is complex real ext-real set
4 * b is complex real ext-real set
(4 * b) * x is complex real ext-real set
(a ^2) - ((4 * b) * x) is complex real ext-real set
sqrt ((a ^2) - ((4 * b) * x)) is complex real ext-real set
(- a) + (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
0 + 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() set
((- a) + (sqrt ((a ^2) - ((4 * b) * x)))) / (2 * b) is complex real ext-real set
- ((4 * b) * x) is complex real ext-real set
- (- ((4 * b) * x)) is complex real ext-real set
(a ^2) + 0 is complex real ext-real set
(a ^2) + (- ((4 * b) * x)) is complex real ext-real set
sqrt (a ^2) is complex real ext-real Element of REAL
- (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
- (- a) is complex real ext-real set
(- (sqrt ((a ^2) - ((4 * b) * x)))) + (- a) is complex real ext-real set
(- (- a)) + (- a) is complex real ext-real set
(- a) - (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
((- a) - (sqrt ((a ^2) - ((4 * b) * x)))) / (2 * b) is complex real ext-real set
0 * 2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() even set
b * 2 is complex real ext-real set
b * x is complex real ext-real set
4 * (b * x) is complex real ext-real set
- ((4 * b) * x) is complex real ext-real set
- (- ((4 * b) * x)) is complex real ext-real set
(a ^2) + 0 is complex real ext-real set
(a ^2) + (- ((4 * b) * x)) is complex real ext-real set
sqrt (a ^2) is complex real ext-real Element of REAL
sqrt ((a ^2) - ((4 * b) * x)) is complex real ext-real set
0 + a is complex real ext-real set
(0 + a) + (- a) is complex real ext-real set
(- a) + (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
((- a) + (sqrt ((a ^2) - ((4 * b) * x)))) / (2 * b) is complex real ext-real set
- (- a) is complex real ext-real set
0 + (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
(- a) + 0 is complex real ext-real set
(sqrt ((a ^2) - ((4 * b) * x))) + a is complex real ext-real set
- ((sqrt ((a ^2) - ((4 * b) * x))) + a) is complex real ext-real set
- (- ((sqrt ((a ^2) - ((4 * b) * x))) + a)) is complex real ext-real set
(- a) - (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
((- a) - (sqrt ((a ^2) - ((4 * b) * x)))) / (2 * b) is complex real ext-real set
a is complex real ext-real Element of REAL
- a is complex real ext-real set
b is complex real ext-real Element of REAL
a / b is complex real ext-real set
2 * b is complex real ext-real set
x is complex real ext-real Element of REAL
x / b is complex real ext-real set
delta (b,a,x) is complex real ext-real Element of REAL
sqrt (delta (b,a,x)) is complex real ext-real Element of REAL
(- a) + (sqrt (delta (b,a,x))) is complex real ext-real set
((- a) + (sqrt (delta (b,a,x)))) / (2 * b) is complex real ext-real set
(- a) - (sqrt (delta (b,a,x))) is complex real ext-real set
((- a) - (sqrt (delta (b,a,x)))) / (2 * b) is complex real ext-real set
a ^2 is complex real ext-real Element of REAL
a * a is complex real ext-real set
4 * b is complex real ext-real set
(4 * b) * x is complex real ext-real set
(a ^2) - ((4 * b) * x) is complex real ext-real set
- ((4 * b) * x) is complex real ext-real set
- (- ((4 * b) * x)) is complex real ext-real set
(a ^2) + 0 is complex real ext-real set
(a ^2) + (- ((4 * b) * x)) is complex real ext-real set
sqrt (a ^2) is complex real ext-real Element of REAL
sqrt ((a ^2) - ((4 * b) * x)) is complex real ext-real set
a + (- a) is complex real ext-real set
0 + (a + (- a)) is complex real ext-real set
(- a) + (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
((- a) + (sqrt ((a ^2) - ((4 * b) * x)))) / (2 * b) is complex real ext-real set
a + (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
0 + 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() set
- (a + (sqrt ((a ^2) - ((4 * b) * x)))) is complex real ext-real set
- (- (a + (sqrt ((a ^2) - ((4 * b) * x))))) is complex real ext-real set
(- a) - (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
((- a) - (sqrt ((a ^2) - ((4 * b) * x)))) / (2 * b) is complex real ext-real set
sqrt ((a ^2) - ((4 * b) * x)) is complex real ext-real set
0 * 2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() even set
b * 2 is complex real ext-real set
(- a) + (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
0 + 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() set
((- a) + (sqrt ((a ^2) - ((4 * b) * x)))) / (2 * b) is complex real ext-real set
b * x is complex real ext-real set
4 * (b * x) is complex real ext-real set
- ((4 * b) * x) is complex real ext-real set
- (- ((4 * b) * x)) is complex real ext-real set
(a ^2) + 0 is complex real ext-real set
(a ^2) + (- ((4 * b) * x)) is complex real ext-real set
sqrt (a ^2) is complex real ext-real Element of REAL
0 + a is complex real ext-real set
(0 + a) + (- a) is complex real ext-real set
a + (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
- (a + (sqrt ((a ^2) - ((4 * b) * x)))) is complex real ext-real set
(- a) - (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
((- a) - (sqrt ((a ^2) - ((4 * b) * x)))) / (2 * b) is complex real ext-real set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
a / b is complex real ext-real set
2 * b is complex real ext-real set
x is complex real ext-real Element of REAL
- x is complex real ext-real set
delta (b,x,a) is complex real ext-real Element of REAL
sqrt (delta (b,x,a)) is complex real ext-real Element of REAL
(- x) + (sqrt (delta (b,x,a))) is complex real ext-real set
((- x) + (sqrt (delta (b,x,a)))) / (2 * b) is complex real ext-real set
(- x) - (sqrt (delta (b,x,a))) is complex real ext-real set
((- x) - (sqrt (delta (b,x,a)))) / (2 * b) is complex real ext-real set
4 * 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() set
4 * b is complex real ext-real set
0 * a is complex real ext-real set
(4 * b) * a is complex real ext-real set
- ((4 * b) * a) is complex real ext-real set
x ^2 is complex real ext-real Element of REAL
x * x is complex real ext-real set
(x ^2) + (- ((4 * b) * a)) is complex real ext-real set
(x ^2) + 0 is complex real ext-real set
(x ^2) - ((4 * b) * a) is complex real ext-real set
sqrt ((x ^2) - ((4 * b) * a)) is complex real ext-real set
sqrt (x ^2) is complex real ext-real Element of REAL
2 * 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() even set
(- ((4 * b) * a)) + (x ^2) is complex real ext-real set
0 + 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() set
- (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
- (- (sqrt ((x ^2) - ((4 * b) * a)))) is complex real ext-real set
- 0 is complex real ext-real non positive V33() set
(- (sqrt ((x ^2) - ((4 * b) * a)))) + (- x) is complex real ext-real set
(- x) - (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
(- x) + (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
0 + x is complex real ext-real set
(0 + x) + (- x) is complex real ext-real set
((- x) + (sqrt ((x ^2) - ((4 * b) * a)))) / (2 * b) is complex real ext-real set
x + (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
- (x + (sqrt ((x ^2) - ((4 * b) * a)))) is complex real ext-real set
- (- (x + (sqrt ((x ^2) - ((4 * b) * a))))) is complex real ext-real set
(- x) - (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
((- x) - (sqrt ((x ^2) - ((4 * b) * a)))) / (2 * b) is complex real ext-real set
(sqrt ((x ^2) - ((4 * b) * a))) + (- x) is complex real ext-real set
(sqrt (delta (b,x,a))) + (- x) is complex real ext-real set
4 * b is complex real ext-real set
(4 * b) * 0 is complex real ext-real set
(4 * b) * a is complex real ext-real set
- ((4 * b) * a) is complex real ext-real set
x ^2 is complex real ext-real Element of REAL
x * x is complex real ext-real set
(x ^2) + (- ((4 * b) * a)) is complex real ext-real set
(x ^2) + 0 is complex real ext-real set
(x ^2) - ((4 * b) * a) is complex real ext-real set
sqrt ((x ^2) - ((4 * b) * a)) is complex real ext-real set
sqrt (x ^2) is complex real ext-real Element of REAL
(- ((4 * b) * a)) + (x ^2) is complex real ext-real set
0 + 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() set
- (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
- (- (sqrt ((x ^2) - ((4 * b) * a)))) is complex real ext-real set
- 0 is complex real ext-real non positive V33() set
(- (sqrt ((x ^2) - ((4 * b) * a)))) + (- x) is complex real ext-real set
(- x) - (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
(- x) + (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
0 + x is complex real ext-real set
(0 + x) + (- x) is complex real ext-real set
((- x) + (sqrt ((x ^2) - ((4 * b) * a)))) / (2 * b) is complex real ext-real set
x + (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
- (x + (sqrt ((x ^2) - ((4 * b) * a)))) is complex real ext-real set
- (- (x + (sqrt ((x ^2) - ((4 * b) * a))))) is complex real ext-real set
(- x) - (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
((- x) - (sqrt ((x ^2) - ((4 * b) * a)))) / (2 * b) is complex real ext-real set
(sqrt ((x ^2) - ((4 * b) * a))) + (- x) is complex real ext-real set
(sqrt (delta (b,x,a))) + (- x) is complex real ext-real set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
b |^ x is complex real ext-real Element of REAL
x -root a is complex real ext-real Element of REAL
- (x -root a) is complex real ext-real set
- b is complex real ext-real set
(- b) |^ x is complex real ext-real set
x -root ((- b) |^ x) is complex real ext-real set
- 1 is non zero complex real ext-real non positive V33() set
(- 1) * (x -root a) is complex real ext-real set
(- 1) * (- b) is complex real ext-real set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
b / a is complex real ext-real set
- (b / a) is complex real ext-real set
x is complex real ext-real Element of REAL
Polynom (a,b,0,x) is complex real ext-real Element of REAL
x ^2 is complex real ext-real Element of REAL
x * x is complex real ext-real set
a * (x ^2) is complex real ext-real set
b * x is complex real ext-real set
(a * (x ^2)) + (b * x) is complex real ext-real set
((a * (x ^2)) + (b * x)) + 0 is complex real ext-real set
a * x is complex real ext-real set
(a * x) + b is complex real ext-real set
((a * x) + b) + 0 is complex real ext-real set
(((a * x) + b) + 0) * x is complex real ext-real set
- b is complex real ext-real set
((a * x) + b) + (- b) is complex real ext-real set
0 + (- b) is complex real ext-real set
(- b) / a is complex real ext-real set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
Polynom (a,0,0,b) is complex real ext-real Element of REAL
b ^2 is complex real ext-real Element of REAL
b * b is complex real ext-real set
a * (b ^2) is complex real ext-real set
0 * b is complex real ext-real set
(a * (b ^2)) + (0 * b) is complex real ext-real set
((a * (b ^2)) + (0 * b)) + 0 is complex real ext-real set
a is complex real ext-real Element of REAL
2 * a is complex real ext-real set
b is complex real ext-real Element of REAL
- b is complex real ext-real set
x is complex real ext-real Element of REAL
delta (a,b,x) is complex real ext-real Element of REAL
sqrt (delta (a,b,x)) is complex real ext-real Element of REAL
(- b) + (sqrt (delta (a,b,x))) is complex real ext-real set
((- b) + (sqrt (delta (a,b,x)))) / (2 * a) is complex real ext-real set
(- b) - (sqrt (delta (a,b,x))) is complex real ext-real set
((- b) - (sqrt (delta (a,b,x)))) / (2 * a) is complex real ext-real set
y is complex real ext-real Element of REAL
q is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
y |^ q is complex real ext-real Element of REAL
Polynom (a,b,x,(y |^ q)) is complex real ext-real Element of REAL
q -root (((- b) + (sqrt (delta (a,b,x)))) / (2 * a)) is complex real ext-real set
q -root (((- b) - (sqrt (delta (a,b,x)))) / (2 * a)) is complex real ext-real set
a is complex real ext-real Element of REAL
2 * a is complex real ext-real set
b is complex real ext-real Element of REAL
b / a is complex real ext-real set
- b is complex real ext-real set
x is complex real ext-real Element of REAL
x / a is complex real ext-real set
delta (a,b,x) is complex real ext-real Element of REAL
sqrt (delta (a,b,x)) is complex real ext-real Element of REAL
(- b) + (sqrt (delta (a,b,x))) is complex real ext-real set
((- b) + (sqrt (delta (a,b,x)))) / (2 * a) is complex real ext-real set
(- b) - (sqrt (delta (a,b,x))) is complex real ext-real set
((- b) - (sqrt (delta (a,b,x)))) / (2 * a) is complex real ext-real set
y is complex real ext-real Element of REAL
q is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
y |^ q is complex real ext-real Element of REAL
Polynom (a,b,x,(y |^ q)) is complex real ext-real Element of REAL
q -root (((- b) + (sqrt (delta (a,b,x)))) / (2 * a)) is complex real ext-real set
- (q -root (((- b) + (sqrt (delta (a,b,x)))) / (2 * a))) is complex real ext-real set
q -root (((- b) - (sqrt (delta (a,b,x)))) / (2 * a)) is complex real ext-real set
- (q -root (((- b) - (sqrt (delta (a,b,x)))) / (2 * a))) is complex real ext-real set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
b / a is complex real ext-real set
- (b / a) is complex real ext-real set
x is complex real ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
x |^ y is complex real ext-real Element of REAL
Polynom (a,b,0,(x |^ y)) is complex real ext-real Element of REAL
y -root (- (b / a)) is complex real ext-real set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
b / a is complex real ext-real set
- (b / a) is complex real ext-real set
x is complex real ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
x |^ y is complex real ext-real Element of REAL
Polynom (a,b,0,(x |^ y)) is complex real ext-real Element of REAL
y -root (- (b / a)) is complex real ext-real set
- (y -root (- (b / a))) is complex real ext-real set
5 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() Element of NAT
a is complex real ext-real Element of REAL
a |^ 3 is complex real ext-real Element of REAL
a ^2 is complex real ext-real Element of REAL
a * a is complex real ext-real set
a |^ 5 is complex real ext-real Element of REAL
a |^ 4 is complex real ext-real Element of REAL
a |^ 2 is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
b |^ 3 is complex real ext-real Element of REAL
(a |^ 3) + (b |^ 3) is complex real ext-real set
a + b is complex real ext-real set
a * b is complex real ext-real set
(a ^2) - (a * b) is complex real ext-real set
b ^2 is complex real ext-real Element of REAL
b * b is complex real ext-real set
((a ^2) - (a * b)) + (b ^2) is complex real ext-real set
(a + b) * (((a ^2) - (a * b)) + (b ^2)) is complex real ext-real set
b |^ 5 is complex real ext-real Element of REAL
(a |^ 5) + (b |^ 5) is complex real ext-real set
(a |^ 3) * b is complex real ext-real set
(a |^ 4) - ((a |^ 3) * b) is complex real ext-real set
b |^ 2 is complex real ext-real Element of REAL
(a |^ 2) * (b |^ 2) is complex real ext-real set
((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2)) is complex real ext-real set
a * (b |^ 3) is complex real ext-real set
(((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2))) - (a * (b |^ 3)) is complex real ext-real set
b |^ 4 is complex real ext-real Element of REAL
((((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2))) - (a * (b |^ 3))) + (b |^ 4) is complex real ext-real set
(a + b) * (((((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2))) - (a * (b |^ 3))) + (b |^ 4)) is complex real ext-real set
(a |^ 4) * a is complex real ext-real set
b * (a |^ 4) is complex real ext-real set
((a |^ 4) * a) + (b * (a |^ 4)) is complex real ext-real set
0 * (a |^ 4) is complex real ext-real set
(((a |^ 4) * a) + (b * (a |^ 4))) + (0 * (a |^ 4)) is complex real ext-real set
((a |^ 3) * b) * (a + b) is complex real ext-real set
((((a |^ 4) * a) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b)) is complex real ext-real set
((a |^ 2) * (b |^ 2)) * (a + b) is complex real ext-real set
(((((a |^ 4) * a) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b)) is complex real ext-real set
(a * (b |^ 3)) * (a + b) is complex real ext-real set
((((((a |^ 4) * a) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b)) is complex real ext-real set
(b |^ 4) * (a + b) is complex real ext-real set
(((((((a |^ 4) * a) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b))) + ((b |^ 4) * (a + b)) is complex real ext-real set
a |^ 1 is complex real ext-real Element of REAL
(a |^ 4) * (a |^ 1) is complex real ext-real set
((a |^ 4) * (a |^ 1)) + (b * (a |^ 4)) is complex real ext-real set
(((a |^ 4) * (a |^ 1)) + (b * (a |^ 4))) + (0 * (a |^ 4)) is complex real ext-real set
((((a |^ 4) * (a |^ 1)) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b)) is complex real ext-real set
(((((a |^ 4) * (a |^ 1)) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b)) is complex real ext-real set
((((((a |^ 4) * (a |^ 1)) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b)) is complex real ext-real set
(((((((a |^ 4) * (a |^ 1)) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b))) + ((b |^ 4) * (a + b)) is complex real ext-real set
4 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() set
a |^ (4 + 1) is complex real ext-real Element of REAL
(a |^ (4 + 1)) + (b * (a |^ 4)) is complex real ext-real set
(a + b) + 0 is complex real ext-real set
((a |^ 3) * b) * ((a + b) + 0) is complex real ext-real set
((a |^ (4 + 1)) + (b * (a |^ 4))) - (((a |^ 3) * b) * ((a + b) + 0)) is complex real ext-real set
(((a |^ (4 + 1)) + (b * (a |^ 4))) - (((a |^ 3) * b) * ((a + b) + 0))) + (((a |^ 2) * (b |^ 2)) * (a + b)) is complex real ext-real set
((((a |^ (4 + 1)) + (b * (a |^ 4))) - (((a |^ 3) * b) * ((a + b) + 0))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b)) is complex real ext-real set
(((((a |^ (4 + 1)) + (b * (a |^ 4))) - (((a |^ 3) * b) * ((a + b) + 0))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b))) + ((b |^ 4) * (a + b)) is complex real ext-real set
(a |^ 5) + (b * (a |^ 4)) is complex real ext-real set
a * (a |^ 3) is complex real ext-real set
(a * (a |^ 3)) * b is complex real ext-real set
b * ((a |^ 3) * b) is complex real ext-real set
((a * (a |^ 3)) * b) + (b * ((a |^ 3) * b)) is complex real ext-real set
((a |^ 5) + (b * (a |^ 4))) - (((a * (a |^ 3)) * b) + (b * ((a |^ 3) * b))) is complex real ext-real set
a * ((a |^ 2) * (b |^ 2)) is complex real ext-real set
b * ((a |^ 2) * (b |^ 2)) is complex real ext-real set
(a * ((a |^ 2) * (b |^ 2))) + (b * ((a |^ 2) * (b |^ 2))) is complex real ext-real set
(((a |^ 5) + (b * (a |^ 4))) - (((a * (a |^ 3)) * b) + (b * ((a |^ 3) * b)))) + ((a * ((a |^ 2) * (b |^ 2))) + (b * ((a |^ 2) * (b |^ 2)))) is complex real ext-real set
a * (a * (b |^ 3)) is complex real ext-real set
b * (a * (b |^ 3)) is complex real ext-real set
(a * (a * (b |^ 3))) + (b * (a * (b |^ 3))) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a * (a |^ 3)) * b) + (b * ((a |^ 3) * b)))) + ((a * ((a |^ 2) * (b |^ 2))) + (b * ((a |^ 2) * (b |^ 2))))) - ((a * (a * (b |^ 3))) + (b * (a * (b |^ 3)))) is complex real ext-real set
a * (b |^ 4) is complex real ext-real set
b * (b |^ 4) is complex real ext-real set
(a * (b |^ 4)) + (b * (b |^ 4)) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a * (a |^ 3)) * b) + (b * ((a |^ 3) * b)))) + ((a * ((a |^ 2) * (b |^ 2))) + (b * ((a |^ 2) * (b |^ 2))))) - ((a * (a * (b |^ 3))) + (b * (a * (b |^ 3))))) + ((a * (b |^ 4)) + (b * (b |^ 4))) is complex real ext-real set
(a |^ 4) * b is complex real ext-real set
(b * b) * (a |^ 3) is complex real ext-real set
((a |^ 4) * b) + ((b * b) * (a |^ 3)) is complex real ext-real set
((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3))) is complex real ext-real set
(a |^ 2) * a is complex real ext-real set
((a |^ 2) * a) * (b |^ 2) is complex real ext-real set
b * (b |^ 2) is complex real ext-real set
(b * (b |^ 2)) * (a |^ 2) is complex real ext-real set
(((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2)) is complex real ext-real set
(((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + ((((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2))) is complex real ext-real set
(a * a) * (b |^ 3) is complex real ext-real set
b * (b |^ 3) is complex real ext-real set
(b * (b |^ 3)) * a is complex real ext-real set
((a * a) * (b |^ 3)) + ((b * (b |^ 3)) * a) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + ((((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b * (b |^ 3)) * a)) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + ((((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b * (b |^ 3)) * a))) + ((a * (b |^ 4)) + (b * (b |^ 4))) is complex real ext-real set
(b |^ 4) * a is complex real ext-real set
((a * a) * (b |^ 3)) + ((b |^ 4) * a) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + ((((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a)) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + ((((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b * (b |^ 4))) is complex real ext-real set
2 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() set
a |^ (2 + 1) is complex real ext-real Element of REAL
(a |^ (2 + 1)) * (b |^ 2) is complex real ext-real set
(b |^ 2) * b is complex real ext-real set
((b |^ 2) * b) * (a |^ 2) is complex real ext-real set
((a |^ (2 + 1)) * (b |^ 2)) + (((b |^ 2) * b) * (a |^ 2)) is complex real ext-real set
(((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ (2 + 1)) * (b |^ 2)) + (((b |^ 2) * b) * (a |^ 2))) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ (2 + 1)) * (b |^ 2)) + (((b |^ 2) * b) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a)) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ (2 + 1)) * (b |^ 2)) + (((b |^ 2) * b) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b * (b |^ 4))) is complex real ext-real set
(a |^ 3) * (b |^ 2) is complex real ext-real set
b |^ (2 + 1) is complex real ext-real Element of REAL
(b |^ (2 + 1)) * (a |^ 2) is complex real ext-real set
((a |^ 3) * (b |^ 2)) + ((b |^ (2 + 1)) * (a |^ 2)) is complex real ext-real set
(((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ (2 + 1)) * (a |^ 2))) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ (2 + 1)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a)) is complex real ext-real set
(b |^ 4) * b is complex real ext-real set
(a * (b |^ 4)) + ((b |^ 4) * b) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ (2 + 1)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + ((b |^ 4) * b)) is complex real ext-real set
(b |^ 3) * (a |^ 2) is complex real ext-real set
((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)) is complex real ext-real set
(((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2))) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a)) is complex real ext-real set
b |^ (4 + 1) is complex real ext-real Element of REAL
(a * (b |^ 4)) + (b |^ (4 + 1)) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ (4 + 1))) is complex real ext-real set
b |^ 1 is complex real ext-real Element of REAL
(b |^ 1) * b is complex real ext-real set
((b |^ 1) * b) * (a |^ 3) is complex real ext-real set
((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)) is complex real ext-real set
((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3))) is complex real ext-real set
(((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2))) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a)) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ (4 + 1))) is complex real ext-real set
(a |^ 1) * a is complex real ext-real set
((a |^ 1) * a) * (b |^ 3) is complex real ext-real set
(((a |^ 1) * a) * (b |^ 3)) + ((b |^ 4) * a) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - ((((a |^ 1) * a) * (b |^ 3)) + ((b |^ 4) * a)) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - ((((a |^ 1) * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ (4 + 1))) is complex real ext-real set
1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() set
b |^ (1 + 1) is complex real ext-real Element of REAL
(b |^ (1 + 1)) * (a |^ 3) is complex real ext-real set
((a |^ 4) * b) + ((b |^ (1 + 1)) * (a |^ 3)) is complex real ext-real set
((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b |^ (1 + 1)) * (a |^ 3))) is complex real ext-real set
(((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b |^ (1 + 1)) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2))) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b |^ (1 + 1)) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - ((((a |^ 1) * a) * (b |^ 3)) + ((b |^ 4) * a)) is complex real ext-real set
(a * (b |^ 4)) + (b |^ 5) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b |^ (1 + 1)) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - ((((a |^ 1) * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ 5)) is complex real ext-real set
(a |^ 2) * (b |^ 3) is complex real ext-real set
(a |^ 5) + ((a |^ 2) * (b |^ 3)) is complex real ext-real set
((a |^ 2) * (b |^ 3)) + (a * (b |^ 4)) is complex real ext-real set
((a |^ 5) + ((a |^ 2) * (b |^ 3))) - (((a |^ 2) * (b |^ 3)) + (a * (b |^ 4))) is complex real ext-real set
(((a |^ 5) + ((a |^ 2) * (b |^ 3))) - (((a |^ 2) * (b |^ 3)) + (a * (b |^ 4)))) + ((a * (b |^ 4)) + (b |^ 5)) is complex real ext-real set
(((a ^2) - (a * b)) + (b ^2)) * (a + b) is complex real ext-real set
(a ^2) * a is complex real ext-real set
b * (a ^2) is complex real ext-real set
((a ^2) * a) + (b * (a ^2)) is complex real ext-real set
a * (a * b) is complex real ext-real set
b * (a * b) is complex real ext-real set
(a * (a * b)) + (b * (a * b)) is complex real ext-real set
(((a ^2) * a) + (b * (a ^2))) - ((a * (a * b)) + (b * (a * b))) is complex real ext-real set
a * (b ^2) is complex real ext-real set
b * (b ^2) is complex real ext-real set
(a * (b ^2)) + (b * (b ^2)) is complex real ext-real set
0 * (b ^2) is complex real ext-real set
((a * (b ^2)) + (b * (b ^2))) + (0 * (b ^2)) is complex real ext-real set
((((a ^2) * a) + (b * (a ^2))) - ((a * (a * b)) + (b * (a * b)))) + (((a * (b ^2)) + (b * (b ^2))) + (0 * (b ^2))) is complex real ext-real set
(a |^ 3) + (b * (a ^2)) is complex real ext-real set
((a |^ 3) + (b * (a ^2))) - ((a * (a * b)) + (b * (a * b))) is complex real ext-real set
(((a |^ 3) + (b * (a ^2))) - ((a * (a * b)) + (b * (a * b)))) + ((a * (b ^2)) + (b * (b ^2))) is complex real ext-real set
(a ^2) * b is complex real ext-real set
(b * b) * a is complex real ext-real set
((a ^2) * b) + ((b * b) * a) is complex real ext-real set
((a |^ 3) + (b * (a ^2))) - (((a ^2) * b) + ((b * b) * a)) is complex real ext-real set
(a * (b ^2)) + (b |^ 3) is complex real ext-real set
(((a |^ 3) + (b * (a ^2))) - (((a ^2) * b) + ((b * b) * a))) + ((a * (b ^2)) + (b |^ 3)) is complex real ext-real set
- 1 is non zero complex real ext-real non positive V33() set
a is complex real ext-real Element of REAL
2 * a is complex real ext-real set
a ^2 is complex real ext-real Element of REAL
a * a is complex real ext-real set
3 * (a ^2) is complex real ext-real set
b is complex real ext-real Element of REAL
b ^2 is complex real ext-real Element of REAL
b * b is complex real ext-real set
(2 * a) * b is complex real ext-real set
(b ^2) - ((2 * a) * b) is complex real ext-real set
((b ^2) - ((2 * a) * b)) - (3 * (a ^2)) is complex real ext-real set
a - b is complex real ext-real set
sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))) is complex real ext-real set
(a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2)))) is complex real ext-real set
((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) is complex real ext-real set
(a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2)))) is complex real ext-real set
((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) is complex real ext-real set
x is complex real ext-real Element of REAL
Polynom (a,b,b,a,x) is complex real ext-real Element of REAL
x |^ 3 is complex real ext-real Element of REAL
a * (x |^ 3) is complex real ext-real set
x ^2 is complex real ext-real Element of REAL
x * x is complex real ext-real set
b * (x ^2) is complex real ext-real set
(a * (x |^ 3)) + (b * (x ^2)) is complex real ext-real set
b * x is complex real ext-real set
((a * (x |^ 3)) + (b * (x ^2))) + (b * x) is complex real ext-real set
(((a * (x |^ 3)) + (b * (x ^2))) + (b * x)) + a is complex real ext-real set
(x |^ 3) + 1 is complex real ext-real set
((x |^ 3) + 1) * a is complex real ext-real set
(x ^2) + x is complex real ext-real set
((x ^2) + x) + 0 is complex real ext-real set
(((x ^2) + x) + 0) * b is complex real ext-real set
(((x |^ 3) + 1) * a) + ((((x ^2) + x) + 0) * b) is complex real ext-real set
1 to_power 3 is complex real ext-real Element of REAL
1 |^ 3 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() set
(x |^ 3) + (1 to_power 3) is complex real ext-real set
((x |^ 3) + (1 to_power 3)) * a is complex real ext-real set
x + 1 is complex real ext-real set
(x + 1) * x is complex real ext-real set
((x + 1) * x) * b is complex real ext-real set
(((x |^ 3) + (1 to_power 3)) * a) + (((x + 1) * x) * b) is complex real ext-real set
x * 1 is complex real ext-real set
(x ^2) - (x * 1) is complex real ext-real set
1 ^2 is complex real ext-real Element of REAL
1 * 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() set
((x ^2) - (x * 1)) + (1 ^2) is complex real ext-real set
(x + 1) * (((x ^2) - (x * 1)) + (1 ^2)) is complex real ext-real set
((x + 1) * (((x ^2) - (x * 1)) + (1 ^2))) * a is complex real ext-real set
(((x + 1) * (((x ^2) - (x * 1)) + (1 ^2))) * a) + (((x + 1) * x) * b) is complex real ext-real set
(x ^2) * a is complex real ext-real set
x * a is complex real ext-real set
((x ^2) * a) - (x * a) is complex real ext-real set
x * b is complex real ext-real set
(((x ^2) * a) - (x * a)) + (x * b) is complex real ext-real set
((((x ^2) * a) - (x * a)) + (x * b)) + a is complex real ext-real set
(((((x ^2) * a) - (x * a)) + (x * b)) + a) * (x + 1) is complex real ext-real set
a * (x ^2) is complex real ext-real set
(a - b) * x is complex real ext-real set
(a * (x ^2)) - ((a - b) * x) is complex real ext-real set
((a * (x ^2)) - ((a - b) * x)) + a is complex real ext-real set
- a is complex real ext-real set
(- a) + b is complex real ext-real set
delta (a,((- a) + b),a) is complex real ext-real set
((- a) + b) ^2 is complex real ext-real set
((- a) + b) * ((- a) + b) is complex real ext-real set
4 * a is complex real ext-real set
(4 * a) * a is complex real ext-real set
(((- a) + b) ^2) - ((4 * a) * a) is complex real ext-real set
4 - 1 is complex real ext-real V33() set
- (4 - 1) is complex real ext-real V33() set
(- (4 - 1)) * (a ^2) is complex real ext-real set
((b ^2) - ((2 * a) * b)) + ((- (4 - 1)) * (a ^2)) is complex real ext-real set
((- a) + b) * x is complex real ext-real set
(a * (x ^2)) + (((- a) + b) * x) is complex real ext-real set
((a * (x ^2)) + (((- a) + b) * x)) + a is complex real ext-real set
Polynom (a,((- a) + b),a,x) is set
- ((- a) + b) is complex real ext-real set
sqrt (delta (a,((- a) + b),a)) is complex real ext-real set
(- ((- a) + b)) + (sqrt (delta (a,((- a) + b),a))) is complex real ext-real set
((- ((- a) + b)) + (sqrt (delta (a,((- a) + b),a)))) / (2 * a) is complex real ext-real set
(- ((- a) + b)) - (sqrt (delta (a,((- a) + b),a))) is complex real ext-real set
((- ((- a) + b)) - (sqrt (delta (a,((- a) + b),a)))) / (2 * a) is complex real ext-real set
a * (x ^2) is complex real ext-real set
(a - b) * x is complex real ext-real set
(a * (x ^2)) - ((a - b) * x) is complex real ext-real set
((a * (x ^2)) - ((a - b) * x)) + a is complex real ext-real set
a * (x ^2) is complex real ext-real set
(a - b) * x is complex real ext-real set
(a * (x ^2)) - ((a - b) * x) is complex real ext-real set
((a * (x ^2)) - ((a - b) * x)) + a is complex real ext-real set
a is complex set
m is complex set
m |^ 5 is complex set
a * (m |^ 5) is complex set
b is complex set
m |^ 4 is complex set
b * (m |^ 4) is complex set
(a * (m |^ 5)) + (b * (m |^ 4)) is complex set
x is complex set
m |^ 3 is complex set
x * (m |^ 3) is complex set
((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3)) is complex set
y is complex set
m ^2 is complex set
m * m is complex set
y * (m ^2) is complex set
(((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2)) is complex set
q is complex set
q * m is complex set
((((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2))) + (q * m) is complex set
n is complex set
(((((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2))) + (q * m)) + n is complex set
a is complex set
b is complex set
x is complex set
y is complex set
q is complex set
n is complex set
m is complex set
(a,b,x,y,q,n,m) is set
m |^ 5 is complex set
a * (m |^ 5) is complex set
m |^ 4 is complex set
b * (m |^ 4) is complex set
(a * (m |^ 5)) + (b * (m |^ 4)) is complex set
m |^ 3 is complex set
x * (m |^ 3) is complex set
((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3)) is complex set
m ^2 is complex set
m * m is complex set
y * (m ^2) is complex set
(((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2)) is complex set
q * m is complex set
((((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2))) + (q * m) is complex set
(((((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2))) + (q * m)) + n is complex set
a is complex real ext-real set
b is complex real ext-real set
x is complex real ext-real set
y is complex real ext-real set
q is complex real ext-real set
n is complex real ext-real set
m is complex real ext-real set
(a,b,x,y,q,n,m) is complex set
m |^ 5 is complex real ext-real set
a * (m |^ 5) is complex real ext-real set
m |^ 4 is complex real ext-real set
b * (m |^ 4) is complex real ext-real set
(a * (m |^ 5)) + (b * (m |^ 4)) is complex real ext-real set
m |^ 3 is complex real ext-real set
x * (m |^ 3) is complex real ext-real set
((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3)) is complex real ext-real set
m ^2 is complex real ext-real set
m * m is complex real ext-real set
y * (m ^2) is complex real ext-real set
(((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2)) is complex real ext-real set
q * m is complex real ext-real set
((((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2))) + (q * m) is complex real ext-real set
(((((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2))) + (q * m)) + n is complex real ext-real set
a is complex real ext-real Element of REAL
2 * a is complex real ext-real set
a ^2 is complex real ext-real Element of REAL
a * a is complex real ext-real set
5 * (a ^2) is complex real ext-real set
4 * a is complex real ext-real set
b is complex real ext-real Element of REAL
b ^2 is complex real ext-real Element of REAL
b * b is complex real ext-real set
(2 * a) * b is complex real ext-real set
(b ^2) + ((2 * a) * b) is complex real ext-real set
((b ^2) + ((2 * a) * b)) + (5 * (a ^2)) is complex real ext-real set
a - b is complex real ext-real set
x is complex real ext-real Element of REAL
(4 * a) * x is complex real ext-real set
(((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * x) is complex real ext-real set
sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * x)) is complex real ext-real set
(a - b) + (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * x))) is complex real ext-real set
((a - b) + (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * x)))) / (2 * a) is complex real ext-real set
(a - b) - (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * x))) is complex real ext-real set
((a - b) - (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * x)))) / (2 * a) is complex real ext-real set
y is complex real ext-real Element of REAL
(a,b,x,x,b,a,y) is complex real ext-real set
y |^ 5 is complex real ext-real set
a * (y |^ 5) is complex real ext-real set
y |^ 4 is complex real ext-real set
b * (y |^ 4) is complex real ext-real set
(a * (y |^ 5)) + (b * (y |^ 4)) is complex real ext-real set
y |^ 3 is complex real ext-real set
x * (y |^ 3) is complex real ext-real set
((a * (y |^ 5)) + (b * (y |^ 4))) + (x * (y |^ 3)) is complex real ext-real set
y ^2 is complex real ext-real set
y * y is complex real ext-real set
x * (y ^2) is complex real ext-real set
(((a * (y |^ 5)) + (b * (y |^ 4))) + (x * (y |^ 3))) + (x * (y ^2)) is complex real ext-real set
b * y is complex real ext-real set
((((a * (y |^ 5)) + (b * (y |^ 4))) + (x * (y |^ 3))) + (x * (y ^2))) + (b * y) is complex real ext-real set
(((((a * (y |^ 5)) + (b * (y |^ 4))) + (x * (y |^ 3))) + (x * (y ^2))) + (b * y)) + a is complex real ext-real set
q is complex real ext-real Element of REAL
n is complex real ext-real Element of REAL
- q is complex real ext-real set
delta (1,(- q),1) is complex real ext-real set
sqrt (delta (1,(- q),1)) is complex real ext-real set
q + (sqrt (delta (1,(- q),1))) is complex real ext-real set
(q + (sqrt (delta (1,(- q),1)))) / 2 is complex real ext-real set
- n is complex real ext-real set
delta (1,(- n),1) is complex real ext-real set
sqrt (delta (1,(- n),1)) is complex real ext-real set
n + (sqrt (delta (1,(- n),1))) is complex real ext-real set
(n + (sqrt (delta (1,(- n),1)))) / 2 is complex real ext-real set
q - (sqrt (delta (1,(- q),1))) is complex real ext-real set
(q - (sqrt (delta (1,(- q),1)))) / 2 is complex real ext-real set
n - (sqrt (delta (1,(- n),1))) is complex real ext-real set
(n - (sqrt (delta (1,(- n),1)))) / 2 is complex real ext-real set
y |^ 5 is complex real ext-real Element of REAL
(y |^ 5) + 1 is complex real ext-real set
((y |^ 5) + 1) * a is complex real ext-real set
y |^ 4 is complex real ext-real Element of REAL
(y |^ 4) + y is complex real ext-real set
((y |^ 4) + y) + 0 is complex real ext-real set
(((y |^ 4) + y) + 0) * b is complex real ext-real set
(((y |^ 5) + 1) * a) + ((((y |^ 4) + y) + 0) * b) is complex real ext-real set
y |^ 3 is complex real ext-real Element of REAL
x * (y |^ 3) is complex real ext-real set
y ^2 is complex real ext-real Element of REAL
x * (y ^2) is complex real ext-real set
(x * (y |^ 3)) + (x * (y ^2)) is complex real ext-real set
0 * x is complex real ext-real set
((x * (y |^ 3)) + (x * (y ^2))) + (0 * x) is complex real ext-real set
((((y |^ 5) + 1) * a) + ((((y |^ 4) + y) + 0) * b)) + (((x * (y |^ 3)) + (x * (y ^2))) + (0 * x)) is complex real ext-real set
1 |^ 5 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
(y |^ 5) + (1 |^ 5) is complex real ext-real set
((y |^ 5) + (1 |^ 5)) * a is complex real ext-real set
3 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() set
y |^ (3 + 1) is complex real ext-real Element of REAL
(y |^ (3 + 1)) + y is complex real ext-real set
((y |^ (3 + 1)) + y) * b is complex real ext-real set
(((y |^ 5) + (1 |^ 5)) * a) + (((y |^ (3 + 1)) + y) * b) is complex real ext-real set
(y |^ 3) + (y ^2) is complex real ext-real set
((y |^ 3) + (y ^2)) * x is complex real ext-real set
((((y |^ 5) + (1 |^ 5)) * a) + (((y |^ (3 + 1)) + y) * b)) + (((y |^ 3) + (y ^2)) * x) is complex real ext-real set
(y |^ 3) * y is complex real ext-real set
((y |^ 3) * y) + y is complex real ext-real set
(((y |^ 3) * y) + y) * b is complex real ext-real set
(((y |^ 5) + (1 |^ 5)) * a) + ((((y |^ 3) * y) + y) * b) is complex real ext-real set
2 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() set
y |^ (2 + 1) is complex real ext-real Element of REAL
(y |^ (2 + 1)) + (y ^2) is complex real ext-real set
((y |^ (2 + 1)) + (y ^2)) * x is complex real ext-real set
((((y |^ 5) + (1 |^ 5)) * a) + ((((y |^ 3) * y) + y) * b)) + (((y |^ (2 + 1)) + (y ^2)) * x) is complex real ext-real set
(y |^ 3) + 1 is complex real ext-real set
((y |^ 3) + 1) + 0 is complex real ext-real set
(((y |^ 3) + 1) + 0) * y is complex real ext-real set
((((y |^ 3) + 1) + 0) * y) * b is complex real ext-real set
(((y |^ 5) + (1 |^ 5)) * a) + (((((y |^ 3) + 1) + 0) * y) * b) is complex real ext-real set
1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() set
y |^ (1 + 1) is complex real ext-real Element of REAL
y * (y |^ (1 + 1)) is complex real ext-real set
1 * (y ^2) is complex real ext-real set
(y * (y |^ (1 + 1))) + (1 * (y ^2)) is complex real ext-real set
0 * (y ^2) is complex real ext-real set
((y * (y |^ (1 + 1))) + (1 * (y ^2))) + (0 * (y ^2)) is complex real ext-real set
(((y * (y |^ (1 + 1))) + (1 * (y ^2))) + (0 * (y ^2))) * x is complex real ext-real set
((((y |^ 5) + (1 |^ 5)) * a) + (((((y |^ 3) + 1) + 0) * y) * b)) + ((((y * (y |^ (1 + 1))) + (1 * (y ^2))) + (0 * (y ^2))) * x) is complex real ext-real set
y |^ 1 is complex real ext-real Element of REAL
(y |^ 1) * y is complex real ext-real set
y * ((y |^ 1) * y) is complex real ext-real set
(y * ((y |^ 1) * y)) + (1 * (y ^2)) is complex real ext-real set
((y * ((y |^ 1) * y)) + (1 * (y ^2))) + (0 * (y ^2)) is complex real ext-real set
(((y * ((y |^ 1) * y)) + (1 * (y ^2))) + (0 * (y ^2))) * x is complex real ext-real set
((((y |^ 5) + (1 |^ 5)) * a) + (((((y |^ 3) + 1) + 0) * y) * b)) + ((((y * ((y |^ 1) * y)) + (1 * (y ^2))) + (0 * (y ^2))) * x) is complex real ext-real set
y * (y ^2) is complex real ext-real set
(y * (y ^2)) + (1 * (y ^2)) is complex real ext-real set
((y * (y ^2)) + (1 * (y ^2))) + (0 * (y ^2)) is complex real ext-real set
(((y * (y ^2)) + (1 * (y ^2))) + (0 * (y ^2))) * x is complex real ext-real set
((((y |^ 5) + (1 |^ 5)) * a) + (((((y |^ 3) + 1) + 0) * y) * b)) + ((((y * (y ^2)) + (1 * (y ^2))) + (0 * (y ^2))) * x) is complex real ext-real set
y + 1 is complex real ext-real set
(y |^ 3) * 1 is complex real ext-real set
(y |^ 4) - ((y |^ 3) * 1) is complex real ext-real set
y |^ 2 is complex real ext-real Element of REAL
1 |^ 2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
(y |^ 2) * (1 |^ 2) is complex real ext-real set
((y |^ 4) - ((y |^ 3) * 1)) + ((y |^ 2) * (1 |^ 2)) is complex real ext-real set
1 |^ 3 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
y * (1 |^ 3) is complex real ext-real set
(((y |^ 4) - ((y |^ 3) * 1)) + ((y |^ 2) * (1 |^ 2))) - (y * (1 |^ 3)) is complex real ext-real set
1 |^ 4 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
((((y |^ 4) - ((y |^ 3) * 1)) + ((y |^ 2) * (1 |^ 2))) - (y * (1 |^ 3))) + (1 |^ 4) is complex real ext-real set
(y + 1) * (((((y |^ 4) - ((y |^ 3) * 1)) + ((y |^ 2) * (1 |^ 2))) - (y * (1 |^ 3))) + (1 |^ 4)) is complex real ext-real set
((y + 1) * (((((y |^ 4) - ((y |^ 3) * 1)) + ((y |^ 2) * (1 |^ 2))) - (y * (1 |^ 3))) + (1 |^ 4))) * a is complex real ext-real set
((y |^ 3) + 1) * y is complex real ext-real set
(((y |^ 3) + 1) * y) * b is complex real ext-real set
(((y + 1) * (((((y |^ 4) - ((y |^ 3) * 1)) + ((y |^ 2) * (1 |^ 2))) - (y * (1 |^ 3))) + (1 |^ 4))) * a) + ((((y |^ 3) + 1) * y) * b) is complex real ext-real set
(y + 1) + 0 is complex real ext-real set
((y + 1) + 0) * (y ^2) is complex real ext-real set
(((y + 1) + 0) * (y ^2)) * x is complex real ext-real set
((((y + 1) * (((((y |^ 4) - ((y |^ 3) * 1)) + ((y |^ 2) * (1 |^ 2))) - (y * (1 |^ 3))) + (1 |^ 4))) * a) + ((((y |^ 3) + 1) * y) * b)) + ((((y + 1) + 0) * (y ^2)) * x) is complex real ext-real set
(y |^ 4) - (y |^ 3) is complex real ext-real set
(y |^ 2) * 1 is complex real ext-real set
((y |^ 4) - (y |^ 3)) + ((y |^ 2) * 1) is complex real ext-real set
(((y |^ 4) - (y |^ 3)) + ((y |^ 2) * 1)) - (y * (1 |^ 3)) is complex real ext-real set
((((y |^ 4) - (y |^ 3)) + ((y |^ 2) * 1)) - (y * (1 |^ 3))) + (1 |^ 4) is complex real ext-real set
(y + 1) * (((((y |^ 4) - (y |^ 3)) + ((y |^ 2) * 1)) - (y * (1 |^ 3))) + (1 |^ 4)) is complex real ext-real set
((y + 1) * (((((y |^ 4) - (y |^ 3)) + ((y |^ 2) * 1)) - (y * (1 |^ 3))) + (1 |^ 4))) * a is complex real ext-real set
(((y + 1) * (((((y |^ 4) - (y |^ 3)) + ((y |^ 2) * 1)) - (y * (1 |^ 3))) + (1 |^ 4))) * a) + ((((y |^ 3) + 1) * y) * b) is complex real ext-real set
((((y + 1) * (((((y |^ 4) - (y |^ 3)) + ((y |^ 2) * 1)) - (y * (1 |^ 3))) + (1 |^ 4))) * a) + ((((y |^ 3) + 1) * y) * b)) + ((((y + 1) + 0) * (y ^2)) * x) is complex real ext-real set
((y |^ 4) - (y |^ 3)) + (y |^ 2) is complex real ext-real set
y * 1 is complex real ext-real set
(((y |^ 4) - (y |^ 3)) + (y |^ 2)) - (y * 1) is complex real ext-real set
((((y |^ 4) - (y |^ 3)) + (y |^ 2)) - (y * 1)) + (1 |^ 4) is complex real ext-real set
(y + 1) * (((((y |^ 4) - (y |^ 3)) + (y |^ 2)) - (y * 1)) + (1 |^ 4)) is complex real ext-real set
((y + 1) * (((((y |^ 4) - (y |^ 3)) + (y |^ 2)) - (y * 1)) + (1 |^ 4))) * a is complex real ext-real set
(((y + 1) * (((((y |^ 4) - (y |^ 3)) + (y |^ 2)) - (y * 1)) + (1 |^ 4))) * a) + ((((y |^ 3) + 1) * y) * b) is complex real ext-real set
((((y + 1) * (((((y |^ 4) - (y |^ 3)) + (y |^ 2)) - (y * 1)) + (1 |^ 4))) * a) + ((((y |^ 3) + 1) * y) * b)) + ((((y + 1) + 0) * (y ^2)) * x) is complex real ext-real set
(((y |^ 4) - (y |^ 3)) + (y |^ 2)) - y is complex real ext-real set
((((y |^ 4) - (y |^ 3)) + (y |^ 2)) - y) + 1 is complex real ext-real set
(y + 1) * (((((y |^ 4) - (y |^ 3)) + (y |^ 2)) - y) + 1) is complex real ext-real set
((y + 1) * (((((y |^ 4) - (y |^ 3)) + (y |^ 2)) - y) + 1)) * a is complex real ext-real set
(((y + 1) * (((((y |^ 4) - (y |^ 3)) + (y |^ 2)) - y) + 1)) * a) + ((((y |^ 3) + 1) * y) * b) is complex real ext-real set
((((y + 1) * (((((y |^ 4) - (y |^ 3)) + (y |^ 2)) - y) + 1)) * a) + ((((y |^ 3) + 1) * y) * b)) + ((((y + 1) + 0) * (y ^2)) * x) is complex real ext-real set
(y |^ 3) + (1 |^ 3) is complex real ext-real set
((y |^ 3) + (1 |^ 3)) * y is complex real ext-real set
(((y |^ 3) + (1 |^ 3)) * y) * b is complex real ext-real set
(((y + 1) * (((((y |^ 4) - (y |^ 3)) + (y |^ 2)) - y) + 1)) * a) + ((((y |^ 3) + (1 |^ 3)) * y) * b) is complex real ext-real set
(y + 1) * (y ^2) is complex real ext-real set
((y + 1) * (y ^2)) * x is complex real ext-real set
((((y + 1) * (((((y |^ 4) - (y |^ 3)) + (y |^ 2)) - y) + 1)) * a) + ((((y |^ 3) + (1 |^ 3)) * y) * b)) + (((y + 1) * (y ^2)) * x) is complex real ext-real set
(y ^2) - (y * 1) is complex real ext-real set
1 ^2 is complex real ext-real Element of REAL
1 * 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() set
((y ^2) - (y * 1)) + (1 ^2) is complex real ext-real set
(y + 1) * (((y ^2) - (y * 1)) + (1 ^2)) is complex real ext-real set
((y + 1) * (((y ^2) - (y * 1)) + (1 ^2))) * y is complex real ext-real set
(((y + 1) * (((y ^2) - (y * 1)) + (1 ^2))) * y) * b is complex real ext-real set
(((y + 1) * (((((y |^ 4) - (y |^ 3)) + (y |^ 2)) - y) + 1)) * a) + ((((y + 1) * (((y ^2) - (y * 1)) + (1 ^2))) * y) * b) is complex real ext-real set
((((y + 1) * (((((y |^ 4) - (y |^ 3)) + (y |^ 2)) - y) + 1)) * a) + ((((y + 1) * (((y ^2) - (y * 1)) + (1 ^2))) * y) * b)) + (((y + 1) * (y ^2)) * x) is complex real ext-real set
a * (y |^ 4) is complex real ext-real set
a * (y |^ 3) is complex real ext-real set
(a * (y |^ 4)) - (a * (y |^ 3)) is complex real ext-real set
a * (y |^ 2) is complex real ext-real set
((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2)) is complex real ext-real set
a * y is complex real ext-real set
(((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y) is complex real ext-real set
((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a is complex real ext-real set
(y * y) * y is complex real ext-real set
((y * y) * y) * b is complex real ext-real set
(y * y) * b is complex real ext-real set
(((y * y) * y) * b) - ((y * y) * b) is complex real ext-real set
((((y * y) * y) * b) - ((y * y) * b)) + (b * y) is complex real ext-real set
(((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + (((((y * y) * y) * b) - ((y * y) * b)) + (b * y)) is complex real ext-real set
(y * y) * x is complex real ext-real set
((((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + (((((y * y) * y) * b) - ((y * y) * b)) + (b * y))) + ((y * y) * x) is complex real ext-real set
(((((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + (((((y * y) * y) * b) - ((y * y) * b)) + (b * y))) + ((y * y) * x)) * (y + 1) is complex real ext-real set
((y |^ 1) * y) * y is complex real ext-real set
(((y |^ 1) * y) * y) * b is complex real ext-real set
((((y |^ 1) * y) * y) * b) - ((y * y) * b) is complex real ext-real set
(((((y |^ 1) * y) * y) * b) - ((y * y) * b)) + (b * y) is complex real ext-real set
(((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + ((((((y |^ 1) * y) * y) * b) - ((y * y) * b)) + (b * y)) is complex real ext-real set
((((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + ((((((y |^ 1) * y) * y) * b) - ((y * y) * b)) + (b * y))) + ((y * y) * x) is complex real ext-real set
(((((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + ((((((y |^ 1) * y) * y) * b) - ((y * y) * b)) + (b * y))) + ((y * y) * x)) * (y + 1) is complex real ext-real set
((y |^ 1) * y) * x is complex real ext-real set
((((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + ((((((y |^ 1) * y) * y) * b) - ((y * y) * b)) + (b * y))) + (((y |^ 1) * y) * x) is complex real ext-real set
(((((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + ((((((y |^ 1) * y) * y) * b) - ((y * y) * b)) + (b * y))) + (((y |^ 1) * y) * x)) * (y + 1) is complex real ext-real set
(y |^ (1 + 1)) * x is complex real ext-real set
((((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + ((((((y |^ 1) * y) * y) * b) - ((y * y) * b)) + (b * y))) + ((y |^ (1 + 1)) * x) is complex real ext-real set
(((((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + ((((((y |^ 1) * y) * y) * b) - ((y * y) * b)) + (b * y))) + ((y |^ (1 + 1)) * x)) * (y + 1) is complex real ext-real set
(y |^ (1 + 1)) * y is complex real ext-real set
((y |^ (1 + 1)) * y) * b is complex real ext-real set
(((y |^ (1 + 1)) * y) * b) - ((y * y) * b) is complex real ext-real set
((((y |^ (1 + 1)) * y) * b) - ((y * y) * b)) + (b * y) is complex real ext-real set
(((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + (((((y |^ (1 + 1)) * y) * b) - ((y * y) * b)) + (b * y)) is complex real ext-real set
(y |^ 2) * x is complex real ext-real set
((((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + (((((y |^ (1 + 1)) * y) * b) - ((y * y) * b)) + (b * y))) + ((y |^ 2) * x) is complex real ext-real set
(((((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + (((((y |^ (1 + 1)) * y) * b) - ((y * y) * b)) + (b * y))) + ((y |^ 2) * x)) * (y + 1) is complex real ext-real set
(y |^ (2 + 1)) * b is complex real ext-real set
((y |^ (2 + 1)) * b) - ((y * y) * b) is complex real ext-real set
(((y |^ (2 + 1)) * b) - ((y * y) * b)) + (b * y) is complex real ext-real set
(((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + ((((y |^ (2 + 1)) * b) - ((y * y) * b)) + (b * y)) is complex real ext-real set
((((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + ((((y |^ (2 + 1)) * b) - ((y * y) * b)) + (b * y))) + ((y |^ 2) * x) is complex real ext-real set
(((((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + ((((y |^ (2 + 1)) * b) - ((y * y) * b)) + (b * y))) + ((y |^ 2) * x)) * (y + 1) is complex real ext-real set
(y |^ 3) * b is complex real ext-real set
((y |^ 1) * y) * b is complex real ext-real set
((y |^ 3) * b) - (((y |^ 1) * y) * b) is complex real ext-real set
(((y |^ 3) * b) - (((y |^ 1) * y) * b)) + (b * y) is complex real ext-real set
(((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + ((((y |^ 3) * b) - (((y |^ 1) * y) * b)) + (b * y)) is complex real ext-real set
((((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + ((((y |^ 3) * b) - (((y |^ 1) * y) * b)) + (b * y))) + ((y |^ 2) * x) is complex real ext-real set
(((((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + ((((y |^ 3) * b) - (((y |^ 1) * y) * b)) + (b * y))) + ((y |^ 2) * x)) * (y + 1) is complex real ext-real set
(y |^ (1 + 1)) * b is complex real ext-real set
((y |^ 3) * b) - ((y |^ (1 + 1)) * b) is complex real ext-real set
(((y |^ 3) * b) - ((y |^ (1 + 1)) * b)) + (b * y) is complex real ext-real set
(((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + ((((y |^ 3) * b) - ((y |^ (1 + 1)) * b)) + (b * y)) is complex real ext-real set
((((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + ((((y |^ 3) * b) - ((y |^ (1 + 1)) * b)) + (b * y))) + ((y |^ 2) * x) is complex real ext-real set
(((((((a * (y |^ 4)) - (a * (y |^ 3))) + (a * (y |^ 2))) - (a * y)) + a) + ((((y |^ 3) * b) - ((y |^ (1 + 1)) * b)) + (b * y))) + ((y |^ 2) * x)) * (y + 1) is complex real ext-real set
(a - b) * (y |^ 3) is complex real ext-real set
(a * (y |^ 4)) - ((a - b) * (y |^ 3)) is complex real ext-real set
a + x is complex real ext-real set
(a + x) - b is complex real ext-real set
((a + x) - b) * (y |^ 2) is complex real ext-real set
((a * (y |^ 4)) - ((a - b) * (y |^ 3))) + (((a + x) - b) * (y |^ 2)) is complex real ext-real set
(a - b) * y is complex real ext-real set
(((a * (y |^ 4)) - ((a - b) * (y |^ 3))) + (((a + x) - b) * (y |^ 2))) - ((a - b) * y) is complex real ext-real set
((((a * (y |^ 4)) - ((a - b) * (y |^ 3))) + (((a + x) - b) * (y |^ 2))) - ((a - b) * y)) + a is complex real ext-real set
(((((a * (y |^ 4)) - ((a - b) * (y |^ 3))) + (((a + x) - b) * (y |^ 2))) - ((a - b) * y)) + a) * (y + 1) is complex real ext-real set
1 / y is complex real ext-real set
y + (1 / y) is complex real ext-real set
- a is complex real ext-real set
(- a) + b is complex real ext-real set
((- a) + b) * (y |^ 3) is complex real ext-real set
(a * (y |^ 4)) + (((- a) + b) * (y |^ 3)) is complex real ext-real set
((a + x) - b) * (y |^ (1 + 1)) is complex real ext-real set
((a * (y |^ 4)) + (((- a) + b) * (y |^ 3))) + (((a + x) - b) * (y |^ (1 + 1))) is complex real ext-real set
((- a) + b) * y is complex real ext-real set
(((a * (y |^ 4)) + (((- a) + b) * (y |^ 3))) + (((a + x) - b) * (y |^ (1 + 1)))) + (((- a) + b) * y) is complex real ext-real set
((((a * (y |^ 4)) + (((- a) + b) * (y |^ 3))) + (((a + x) - b) * (y |^ (1 + 1)))) + (((- a) + b) * y)) + a is complex real ext-real set
((a + x) - b) * ((y |^ 1) * y) is complex real ext-real set
((a * (y |^ 4)) + (((- a) + b) * (y |^ 3))) + (((a + x) - b) * ((y |^ 1) * y)) is complex real ext-real set
(((a * (y |^ 4)) + (((- a) + b) * (y |^ 3))) + (((a + x) - b) * ((y |^ 1) * y))) + (((- a) + b) * y) is complex real ext-real set
((((a * (y |^ 4)) + (((- a) + b) * (y |^ 3))) + (((a + x) - b) * ((y |^ 1) * y))) + (((- a) + b) * y)) + a is complex real ext-real set
((a + x) - b) * (y ^2) is complex real ext-real set
((a * (y |^ 4)) + (((- a) + b) * (y |^ 3))) + (((a + x) - b) * (y ^2)) is complex real ext-real set
(((a * (y |^ 4)) + (((- a) + b) * (y |^ 3))) + (((a + x) - b) * (y ^2))) + (((- a) + b) * y) is complex real ext-real set
((((a * (y |^ 4)) + (((- a) + b) * (y |^ 3))) + (((a + x) - b) * (y ^2))) + (((- a) + b) * y)) + a is complex real ext-real set
Polynom (a,((- a) + b),((a + x) - b),((- a) + b),a,y) is set
- ((- a) + b) is complex real ext-real set
((- a) + b) ^2 is complex real ext-real set
((- a) + b) * ((- a) + b) is complex real ext-real set
(4 * a) * ((a + x) - b) is complex real ext-real set
(((- a) + b) ^2) - ((4 * a) * ((a + x) - b)) is complex real ext-real set
8 * (a ^2) is complex real ext-real set
((((- a) + b) ^2) - ((4 * a) * ((a + x) - b))) + (8 * (a ^2)) is complex real ext-real set
sqrt (((((- a) + b) ^2) - ((4 * a) * ((a + x) - b))) + (8 * (a ^2))) is complex real ext-real set
(- ((- a) + b)) + (sqrt (((((- a) + b) ^2) - ((4 * a) * ((a + x) - b))) + (8 * (a ^2)))) is complex real ext-real set
((- ((- a) + b)) + (sqrt (((((- a) + b) ^2) - ((4 * a) * ((a + x) - b))) + (8 * (a ^2))))) / (2 * a) is complex real ext-real set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
a + b is complex real ext-real set
a * b is complex real ext-real set
x is complex real ext-real Element of REAL
x ^2 is complex real ext-real Element of REAL
x * x is complex real ext-real set
y is complex real ext-real Element of REAL
4 * y is complex real ext-real set
(x ^2) - (4 * y) is complex real ext-real set
sqrt ((x ^2) - (4 * y)) is complex real ext-real set
x + (sqrt ((x ^2) - (4 * y))) is complex real ext-real set
(x + (sqrt ((x ^2) - (4 * y)))) / 2 is complex real ext-real set
x - (sqrt ((x ^2) - (4 * y))) is complex real ext-real set
(x - (sqrt ((x ^2) - (4 * y)))) / 2 is complex real ext-real set
- x is complex real ext-real set
delta (1,(- x),y) is complex real ext-real set
(- x) ^2 is complex real ext-real set
(- x) * (- x) is complex real ext-real set
4 * 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() set
(4 * 1) * y is complex real ext-real set
((- x) ^2) - ((4 * 1) * y) is complex real ext-real set
b ^2 is complex real ext-real Element of REAL
b * b is complex real ext-real set
1 * (b ^2) is complex real ext-real set
(- x) * b is complex real ext-real set
(1 * (b ^2)) + ((- x) * b) is complex real ext-real set
((1 * (b ^2)) + ((- x) * b)) + y is complex real ext-real set
Polynom (1,(- x),y,b) is set
- (- x) is complex real ext-real set
sqrt (delta (1,(- x),y)) is complex real ext-real set
(- (- x)) + (sqrt (delta (1,(- x),y))) is complex real ext-real set
2 * 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() even set
((- (- x)) + (sqrt (delta (1,(- x),y)))) / (2 * 1) is complex real ext-real set
(- (- x)) - (sqrt (delta (1,(- x),y))) is complex real ext-real set
((- (- x)) - (sqrt (delta (1,(- x),y)))) / (2 * 1) is complex real ext-real set
x + (sqrt (delta (1,(- x),y))) is complex real ext-real set
(x + (sqrt (delta (1,(- x),y)))) / 2 is complex real ext-real set
x * 2 is complex real ext-real set
(x * 2) / 2 is complex real ext-real set
x / 2 is complex real ext-real set
(sqrt (delta (1,(- x),y))) / 2 is complex real ext-real set
(x / 2) + ((sqrt (delta (1,(- x),y))) / 2) is complex real ext-real set
((x * 2) / 2) - ((x / 2) + ((sqrt (delta (1,(- x),y))) / 2)) is complex real ext-real set
(sqrt ((x ^2) - (4 * y))) / 2 is complex real ext-real set
(x / 2) + ((sqrt ((x ^2) - (4 * y))) / 2) is complex real ext-real set
((x * 2) / 2) - ((x / 2) + ((sqrt ((x ^2) - (4 * y))) / 2)) is complex real ext-real set
x - (sqrt (delta (1,(- x),y))) is complex real ext-real set
(x - (sqrt (delta (1,(- x),y)))) / 2 is complex real ext-real set
(x - (sqrt (delta (1,(- x),y)))) + 0 is complex real ext-real set
((x - (sqrt (delta (1,(- x),y)))) + 0) / 2 is complex real ext-real set
x - (((x - (sqrt (delta (1,(- x),y)))) + 0) / 2) is complex real ext-real set
(x - (sqrt ((x ^2) - (4 * y)))) + 0 is complex real ext-real set
((x - (sqrt ((x ^2) - (4 * y)))) + 0) / 2 is complex real ext-real set
x - (((x - (sqrt ((x ^2) - (4 * y)))) + 0) / 2) is complex real ext-real set
x + (sqrt (delta (1,(- x),y))) is complex real ext-real set
(x + (sqrt (delta (1,(- x),y)))) / 2 is complex real ext-real set
x - (sqrt (delta (1,(- x),y))) is complex real ext-real set
(x - (sqrt (delta (1,(- x),y)))) / 2 is complex real ext-real set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
x ^2 is complex real ext-real Element of REAL
x * x is complex real ext-real set
y is complex real ext-real Element of REAL
4 * y is complex real ext-real set
(x ^2) - (4 * y) is complex real ext-real set
sqrt ((x ^2) - (4 * y)) is complex real ext-real set
x + (sqrt ((x ^2) - (4 * y))) is complex real ext-real set
(x + (sqrt ((x ^2) - (4 * y)))) / 2 is complex real ext-real set
x - (sqrt ((x ^2) - (4 * y))) is complex real ext-real set
(x - (sqrt ((x ^2) - (4 * y)))) / 2 is complex real ext-real set
q is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
a |^ q is complex real ext-real Element of REAL
b |^ q is complex real ext-real Element of REAL
(a |^ q) + (b |^ q) is complex real ext-real set
(a |^ q) * (b |^ q) is complex real ext-real set
q -root ((x + (sqrt ((x ^2) - (4 * y)))) / 2) is complex real ext-real set
q -root ((x - (sqrt ((x ^2) - (4 * y)))) / 2) is complex real ext-real set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
x ^2 is complex real ext-real Element of REAL
x * x is complex real ext-real set
y is complex real ext-real Element of REAL
4 * y is complex real ext-real set
(x ^2) - (4 * y) is complex real ext-real set
sqrt ((x ^2) - (4 * y)) is complex real ext-real set
x + (sqrt ((x ^2) - (4 * y))) is complex real ext-real set
(x + (sqrt ((x ^2) - (4 * y)))) / 2 is complex real ext-real set
x - (sqrt ((x ^2) - (4 * y))) is complex real ext-real set
(x - (sqrt ((x ^2) - (4 * y)))) / 2 is complex real ext-real set
q is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
a |^ q is complex real ext-real Element of REAL
b |^ q is complex real ext-real Element of REAL
(a |^ q) + (b |^ q) is complex real ext-real set
(a |^ q) * (b |^ q) is complex real ext-real set
q -root ((x + (sqrt ((x ^2) - (4 * y)))) / 2) is complex real ext-real set
q -root ((x - (sqrt ((x ^2) - (4 * y)))) / 2) is complex real ext-real set
- (q -root ((x + (sqrt ((x ^2) - (4 * y)))) / 2)) is complex real ext-real set
- (q -root ((x - (sqrt ((x ^2) - (4 * y)))) / 2)) is complex real ext-real set
- (4 * y) is complex real ext-real set
- (- (4 * y)) is complex real ext-real set
(x ^2) + 0 is complex real ext-real set
(x ^2) + (- (4 * y)) is complex real ext-real set
sqrt (x ^2) is complex real ext-real Element of REAL
- (sqrt ((x ^2) - (4 * y))) is complex real ext-real set
- x is complex real ext-real set
(- (sqrt ((x ^2) - (4 * y)))) + x is complex real ext-real set
(- x) + 0 is complex real ext-real set
((- x) + 0) + x is complex real ext-real set
0 + x is complex real ext-real set
(0 + x) - (sqrt ((x ^2) - (4 * y))) is complex real ext-real set
((0 + x) - (sqrt ((x ^2) - (4 * y)))) / 2 is complex real ext-real set
delta (1,(- x),y) is complex real ext-real set
(- x) ^2 is complex real ext-real set
(- x) * (- x) is complex real ext-real set
4 * 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() set
(4 * 1) * y is complex real ext-real set
((- x) ^2) - ((4 * 1) * y) is complex real ext-real set
sqrt (delta (1,(- x),y)) is complex real ext-real set
- (- x) is complex real ext-real set
(- (- x)) + (sqrt (delta (1,(- x),y))) is complex real ext-real set
0 + 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() set
(0 + x) + (sqrt ((x ^2) - (4 * y))) is complex real ext-real set
((0 + x) + (sqrt ((x ^2) - (4 * y)))) / 2 is complex real ext-real set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
y is complex real ext-real Element of REAL
x + y is complex real ext-real set
x - y is complex real ext-real set
(x + y) / 2 is complex real ext-real set
(x - y) / 2 is complex real ext-real set
q is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
a |^ q is complex real ext-real Element of REAL
b |^ q is complex real ext-real Element of REAL
(a |^ q) + (b |^ q) is complex real ext-real set
(a |^ q) - (b |^ q) is complex real ext-real set
q -root ((x + y) / 2) is complex real ext-real set
q -root ((x - y) / 2) is complex real ext-real set
- (q -root ((x - y) / 2)) is complex real ext-real set
- (q -root ((x + y) / 2)) is complex real ext-real set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
a * x is complex real ext-real set
y is complex real ext-real Element of REAL
b * y is complex real ext-real set
q is complex real ext-real Element of REAL
q / x is complex real ext-real set
q / a is complex real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
b |^ n is complex real ext-real Element of REAL
a * (b |^ n) is complex real ext-real set
y |^ n is complex real ext-real Element of REAL
x * (y |^ n) is complex real ext-real set
(a * (b |^ n)) + (x * (y |^ n)) is complex real ext-real set
n -root (q / x) is complex real ext-real set
n -root (q / a) is complex real ext-real set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
2 * m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() even set
(2 * m) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() non even set
0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() set
0 to_power n is complex real ext-real set
0 |^ n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() set
a * (0 to_power n) is complex real ext-real set
(a * (0 to_power n)) + (x * (y |^ n)) is complex real ext-real set
a * 0 is complex real ext-real set
(a * 0) + (x * (y |^ n)) is complex real ext-real set
0 to_power n is complex real ext-real set
0 |^ n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() set
x * (0 to_power n) is complex real ext-real set
(a * (b |^ n)) + (x * (0 to_power n)) is complex real ext-real set
x * 0 is complex real ext-real set
(a * (b |^ n)) + (x * 0) is complex real ext-real set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
a * x is complex real ext-real set
y is complex real ext-real Element of REAL
b * y is complex real ext-real set
q is complex real ext-real Element of REAL
q / x is complex real ext-real set
q / a is complex real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
b |^ n is complex real ext-real Element of REAL
a * (b |^ n) is complex real ext-real set
y |^ n is complex real ext-real Element of REAL
x * (y |^ n) is complex real ext-real set
(a * (b |^ n)) + (x * (y |^ n)) is complex real ext-real set
n -root (q / x) is complex real ext-real set
- (n -root (q / x)) is complex real ext-real set
n -root (q / a) is complex real ext-real set
- (n -root (q / a)) is complex real ext-real set
0 to_power n is complex real ext-real set
0 |^ n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() set
a * (0 to_power n) is complex real ext-real set
(a * (0 to_power n)) + (x * (y |^ n)) is complex real ext-real set
a * 0 is complex real ext-real set
(a * 0) + (x * (y |^ n)) is complex real ext-real set
0 to_power n is complex real ext-real set
0 |^ n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() set
x * (0 to_power n) is complex real ext-real set
(a * (b |^ n)) + (x * (0 to_power n)) is complex real ext-real set
x * 0 is complex real ext-real set
(a * (b |^ n)) + (x * 0) is complex real ext-real set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
x * a is complex real ext-real set
x / a is complex real ext-real set
a / x is complex real ext-real set
y is complex real ext-real Element of REAL
b * y is complex real ext-real set
q is complex real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
b |^ n is complex real ext-real Element of REAL
a * (b |^ n) is complex real ext-real set
n -root (x / a) is complex real ext-real set
n -root (a / x) is complex real ext-real set
q * (n -root (a / x)) is complex real ext-real set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
2 * m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() even set
(2 * m) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() non even set
(n -root (x / a)) * (n -root (a / x)) is complex real ext-real set
y * ((n -root (x / a)) * (n -root (a / x))) is complex real ext-real set
(x / a) * (a / x) is complex real ext-real set
n -root ((x / a) * (a / x)) is complex real ext-real set
y * (n -root ((x / a) * (a / x))) is complex real ext-real set
x " is complex real ext-real set
a * (x ") is complex real ext-real set
(x / a) * (a * (x ")) is complex real ext-real set
n -root ((x / a) * (a * (x "))) is complex real ext-real set
y * (n -root ((x / a) * (a * (x ")))) is complex real ext-real set
(x / a) * a is complex real ext-real set
((x / a) * a) * (x ") is complex real ext-real set
n -root (((x / a) * a) * (x ")) is complex real ext-real set
y * (n -root (((x / a) * a) * (x "))) is complex real ext-real set
x * (x ") is complex real ext-real set
n -root (x * (x ")) is complex real ext-real set
y * (n -root (x * (x "))) is complex real ext-real set
x / x is complex real ext-real set
n -root (x / x) is complex real ext-real set
y * (n -root (x / x)) is complex real ext-real set
0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V33() set
n -root 1 is complex real ext-real Element of REAL
y * (n -root 1) is complex real ext-real set
y * 1 is complex real ext-real set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
x / a is complex real ext-real set
a / x is complex real ext-real set
y is complex real ext-real Element of REAL
b * y is complex real ext-real set
q is complex real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V33() Element of NAT
b |^ n is complex real ext-real Element of REAL
a * (b |^ n) is complex real ext-real set
n -root (x / a) is complex real ext-real set
n -root (a / x) is complex real ext-real set
q * (n -root (a / x)) is complex real ext-real set
- (n -root (x / a)) is complex real ext-real set
- (q * (n -root (a / x))) is complex real ext-real set
(x / a) " is complex real ext-real set
1 / (x / a) is complex real ext-real set
1 * a is complex real ext-real set
(1 * a) / x is complex real ext-real set
(n -root (x / a)) * (n -root (a / x)) is complex real ext-real set
y * ((n -root (x / a)) * (n -root (a / x))) is complex real ext-real set
(x / a) * (a / x) is complex real ext-real set
n -root ((x / a) * (a / x)) is complex real ext-real set
y * (n -root ((x / a) * (a / x))) is complex real ext-real set
x " is complex real ext-real set
a * (x ") is complex real ext-real set
(x / a) * (a * (x ")) is complex real ext-real set
n -root ((x / a) * (a * (x "))) is complex real ext-real set
y * (n -root ((x / a) * (a * (x ")))) is complex real ext-real set
(x / a) * a is complex real ext-real set
((x / a) * a) * (x ") is complex real ext-real set
n -root (((x / a) * a) * (x ")) is complex real ext-real set
y * (n -root (((x / a) * a) * (x "))) is complex real ext-real set
x * (x ") is complex real ext-real set
n -root (x * (x ")) is complex real ext-real set
y * (n -root (x * (x "))) is complex real ext-real set
x / x is complex real ext-real set
n -root (x / x) is complex real ext-real set
y * (n -root (x / x)) is complex real ext-real set
n -root 1 is complex real ext-real Element of REAL
y * (n -root 1) is complex real ext-real set
y * 1 is complex real ext-real set
(n -root (x / a)) * (n -root (a / x)) is complex real ext-real set
y * ((n -root (x / a)) * (n -root (a / x))) is complex real ext-real set
(x / a) * (a / x) is complex real ext-real set
n -root ((x / a) * (a / x)) is complex real ext-real set
y * (n -root ((x / a) * (a / x))) is complex real ext-real set
x " is complex real ext-real set
a * (x ") is complex real ext-real set
(x / a) * (a * (x ")) is complex real ext-real set
n -root ((x / a) * (a * (x "))) is complex real ext-real set
y * (n -root ((x / a) * (a * (x ")))) is complex real ext-real set
(x / a) * a is complex real ext-real set
((x / a) * a) * (x ") is complex real ext-real set
n -root (((x / a) * a) * (x ")) is complex real ext-real set
y * (n -root (((x / a) * a) * (x "))) is complex real ext-real set
x * (x ") is complex real ext-real set
n -root (x * (x ")) is complex real ext-real set
y * (n -root (x * (x "))) is complex real ext-real set
x / x is complex real ext-real set
n -root (x / x) is complex real ext-real set
y * (n -root (x / x)) is complex real ext-real set
n -root 1 is complex real ext-real Element of REAL
y * (n -root 1) is complex real ext-real set
y * 1 is complex real ext-real set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
a to_power b is complex real ext-real Element of REAL
log (a,1) is complex real ext-real Element of REAL
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
a to_power b is complex real ext-real Element of REAL
log (a,a) is complex real ext-real Element of REAL
a is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
log (a,x) is complex real ext-real Element of REAL
a to_power 0 is complex real ext-real Element of REAL
a |^ 0 is complex real ext-real set
a is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
log (a,x) is complex real ext-real Element of REAL
a to_power 1 is complex real ext-real Element of REAL
a |^ 1 is complex real ext-real set