:: POLYEQ_5 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
K7(NAT,REAL) is set
K6(K7(NAT,REAL)) is set
K7(NAT,COMPLEX) is set
K6(K7(NAT,COMPLEX)) is set
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is set
K7(REAL,REAL) is set
K6(K7(REAL,REAL)) is set
NAT is non zero epsilon-transitive epsilon-connected ordinal set
K6(NAT) is set
K6(NAT) is set
RAT is set
INT is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is set
K7(K7(NAT,NAT),NAT) is set
K6(K7(K7(NAT,NAT),NAT)) is set
0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative Element of NAT
1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
PI is complex real ext-real Element of REAL
K320(2,PI) is complex real ext-real Element of REAL
<i> is complex Element of COMPLEX
cos 0 is complex real ext-real Element of REAL
sin 0 is complex real ext-real Element of REAL
z is complex set
z * z is complex set
z |^ 2 is complex set
z |^ 1 is complex set
(z |^ 1) * z is complex set
1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
z |^ (1 + 1) is complex set
3 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
z is complex set
z * z is complex set
(z * z) * z is complex set
z |^ 3 is complex set
z |^ 2 is complex set
(z |^ 2) * z is complex set
2 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
z |^ (2 + 1) is complex set
4 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
z is complex set
z * z is complex set
(z * z) * z is complex set
((z * z) * z) * z is complex set
z |^ 4 is complex set
z |^ 3 is complex set
(z |^ 3) * z is complex set
3 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
z |^ (3 + 1) is complex set
z is complex set
z |^ 2 is complex set
2 * z is complex set
a2 is complex set
z - a2 is complex set
(z - a2) |^ 2 is complex set
(2 * z) * a2 is complex set
(z |^ 2) - ((2 * z) * a2) is complex set
a2 |^ 2 is complex set
((z |^ 2) - ((2 * z) * a2)) + (a2 |^ 2) is complex set
(z - a2) * (z - a2) is complex set
z ^2 is complex set
z * z is complex set
(z ^2) - ((2 * z) * a2) is complex set
a2 ^2 is complex set
a2 * a2 is complex set
((z ^2) - ((2 * z) * a2)) + (a2 ^2) is complex set
((z |^ 2) - ((2 * z) * a2)) + (a2 * a2) is complex set
z is complex set
z |^ 3 is complex set
z |^ 2 is complex set
3 * (z |^ 2) is complex set
a2 is complex set
z - a2 is complex set
(z - a2) |^ 3 is complex set
(3 * (z |^ 2)) * a2 is complex set
(z |^ 3) - ((3 * (z |^ 2)) * a2) is complex set
a2 |^ 2 is complex set
3 * (a2 |^ 2) is complex set
(3 * (a2 |^ 2)) * z is complex set
((z |^ 3) - ((3 * (z |^ 2)) * a2)) + ((3 * (a2 |^ 2)) * z) is complex set
a2 |^ 3 is complex set
(((z |^ 3) - ((3 * (z |^ 2)) * a2)) + ((3 * (a2 |^ 2)) * z)) - (a2 |^ 3) is complex set
2 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(z - a2) |^ (2 + 1) is complex set
(z - a2) |^ 2 is complex set
((z - a2) |^ 2) * (z - a2) is complex set
2 * z is complex set
(2 * z) * a2 is complex set
(z |^ 2) - ((2 * z) * a2) is complex set
((z |^ 2) - ((2 * z) * a2)) + (a2 |^ 2) is complex set
(((z |^ 2) - ((2 * z) * a2)) + (a2 |^ 2)) * (z - a2) is complex set
(z |^ 2) * z is complex set
(z |^ 2) * a2 is complex set
((z |^ 2) * z) - ((z |^ 2) * a2) is complex set
((2 * z) * a2) * z is complex set
((2 * z) * a2) * a2 is complex set
(((2 * z) * a2) * z) - (((2 * z) * a2) * a2) is complex set
(((z |^ 2) * z) - ((z |^ 2) * a2)) - ((((2 * z) * a2) * z) - (((2 * z) * a2) * a2)) is complex set
(a2 |^ 2) * z is complex set
(a2 |^ 2) * a2 is complex set
((a2 |^ 2) * z) - ((a2 |^ 2) * a2) is complex set
((((z |^ 2) * z) - ((z |^ 2) * a2)) - ((((2 * z) * a2) * z) - (((2 * z) * a2) * a2))) + (((a2 |^ 2) * z) - ((a2 |^ 2) * a2)) is complex set
a2 |^ (2 + 1) is complex set
((a2 |^ 2) * z) - (a2 |^ (2 + 1)) is complex set
((((z |^ 2) * z) - ((z |^ 2) * a2)) - ((((2 * z) * a2) * z) - (((2 * z) * a2) * a2))) + (((a2 |^ 2) * z) - (a2 |^ (2 + 1))) is complex set
(z |^ 3) - ((z |^ 2) * a2) is complex set
z * z is complex set
2 * (z * z) is complex set
(2 * (z * z)) * a2 is complex set
((2 * (z * z)) * a2) - (((2 * z) * a2) * a2) is complex set
((z |^ 3) - ((z |^ 2) * a2)) - (((2 * (z * z)) * a2) - (((2 * z) * a2) * a2)) is complex set
((a2 |^ 2) * z) - (a2 |^ 3) is complex set
(((z |^ 3) - ((z |^ 2) * a2)) - (((2 * (z * z)) * a2) - (((2 * z) * a2) * a2))) + (((a2 |^ 2) * z) - (a2 |^ 3)) is complex set
z |^ 1 is complex set
(z |^ 1) * z is complex set
2 * ((z |^ 1) * z) is complex set
(2 * ((z |^ 1) * z)) * a2 is complex set
((2 * ((z |^ 1) * z)) * a2) - (((2 * z) * a2) * a2) is complex set
((z |^ 3) - ((z |^ 2) * a2)) - (((2 * ((z |^ 1) * z)) * a2) - (((2 * z) * a2) * a2)) is complex set
(((z |^ 3) - ((z |^ 2) * a2)) - (((2 * ((z |^ 1) * z)) * a2) - (((2 * z) * a2) * a2))) + (((a2 |^ 2) * z) - (a2 |^ 3)) is complex set
1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
z |^ (1 + 1) is complex set
2 * (z |^ (1 + 1)) is complex set
(2 * (z |^ (1 + 1))) * a2 is complex set
((2 * (z |^ (1 + 1))) * a2) - (((2 * z) * a2) * a2) is complex set
((z |^ 3) - ((z |^ 2) * a2)) - (((2 * (z |^ (1 + 1))) * a2) - (((2 * z) * a2) * a2)) is complex set
(((z |^ 3) - ((z |^ 2) * a2)) - (((2 * (z |^ (1 + 1))) * a2) - (((2 * z) * a2) * a2))) + (((a2 |^ 2) * z) - (a2 |^ 3)) is complex set
a2 * a2 is complex set
2 * (a2 * a2) is complex set
(2 * (a2 * a2)) * z is complex set
((z |^ 3) - ((3 * (z |^ 2)) * a2)) + ((2 * (a2 * a2)) * z) is complex set
(((z |^ 3) - ((3 * (z |^ 2)) * a2)) + ((2 * (a2 * a2)) * z)) + ((a2 |^ 2) * z) is complex set
((((z |^ 3) - ((3 * (z |^ 2)) * a2)) + ((2 * (a2 * a2)) * z)) + ((a2 |^ 2) * z)) - (a2 |^ 3) is complex set
a2 |^ 1 is complex set
(a2 |^ 1) * a2 is complex set
2 * ((a2 |^ 1) * a2) is complex set
(2 * ((a2 |^ 1) * a2)) * z is complex set
((z |^ 3) - ((3 * (z |^ 2)) * a2)) + ((2 * ((a2 |^ 1) * a2)) * z) is complex set
(((z |^ 3) - ((3 * (z |^ 2)) * a2)) + ((2 * ((a2 |^ 1) * a2)) * z)) + ((a2 |^ 2) * z) is complex set
((((z |^ 3) - ((3 * (z |^ 2)) * a2)) + ((2 * ((a2 |^ 1) * a2)) * z)) + ((a2 |^ 2) * z)) - (a2 |^ 3) is complex set
a2 |^ (1 + 1) is complex set
2 * (a2 |^ (1 + 1)) is complex set
(2 * (a2 |^ (1 + 1))) * z is complex set
((z |^ 3) - ((3 * (z |^ 2)) * a2)) + ((2 * (a2 |^ (1 + 1))) * z) is complex set
(((z |^ 3) - ((3 * (z |^ 2)) * a2)) + ((2 * (a2 |^ (1 + 1))) * z)) + ((a2 |^ 2) * z) is complex set
((((z |^ 3) - ((3 * (z |^ 2)) * a2)) + ((2 * (a2 |^ (1 + 1))) * z)) + ((a2 |^ 2) * z)) - (a2 |^ 3) is complex set
6 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
z is complex set
z |^ 4 is complex set
z |^ 3 is complex set
4 * (z |^ 3) is complex set
z |^ 2 is complex set
6 * (z |^ 2) is complex set
a2 is complex set
z - a2 is complex set
(z - a2) |^ 4 is complex set
(4 * (z |^ 3)) * a2 is complex set
(z |^ 4) - ((4 * (z |^ 3)) * a2) is complex set
a2 |^ 2 is complex set
(6 * (z |^ 2)) * (a2 |^ 2) is complex set
((z |^ 4) - ((4 * (z |^ 3)) * a2)) + ((6 * (z |^ 2)) * (a2 |^ 2)) is complex set
a2 |^ 3 is complex set
4 * (a2 |^ 3) is complex set
(4 * (a2 |^ 3)) * z is complex set
(((z |^ 4) - ((4 * (z |^ 3)) * a2)) + ((6 * (z |^ 2)) * (a2 |^ 2))) - ((4 * (a2 |^ 3)) * z) is complex set
a2 |^ 4 is complex set
((((z |^ 4) - ((4 * (z |^ 3)) * a2)) + ((6 * (z |^ 2)) * (a2 |^ 2))) - ((4 * (a2 |^ 3)) * z)) + (a2 |^ 4) is complex set
3 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(z - a2) |^ (3 + 1) is complex set
(z - a2) |^ 3 is complex set
((z - a2) |^ 3) * (z - a2) is complex set
3 * (z |^ 2) is complex set
(3 * (z |^ 2)) * a2 is complex set
(z |^ 3) - ((3 * (z |^ 2)) * a2) is complex set
3 * (a2 |^ 2) is complex set
(3 * (a2 |^ 2)) * z is complex set
((z |^ 3) - ((3 * (z |^ 2)) * a2)) + ((3 * (a2 |^ 2)) * z) is complex set
(((z |^ 3) - ((3 * (z |^ 2)) * a2)) + ((3 * (a2 |^ 2)) * z)) - (a2 |^ 3) is complex set
((((z |^ 3) - ((3 * (z |^ 2)) * a2)) + ((3 * (a2 |^ 2)) * z)) - (a2 |^ 3)) * (z - a2) is complex set
(z |^ 3) * z is complex set
(z |^ 3) * a2 is complex set
((z |^ 3) * z) - ((z |^ 3) * a2) is complex set
((3 * (z |^ 2)) * a2) * z is complex set
- (((3 * (z |^ 2)) * a2) * z) is complex set
((3 * (z |^ 2)) * a2) * a2 is complex set
(- (((3 * (z |^ 2)) * a2) * z)) + (((3 * (z |^ 2)) * a2) * a2) is complex set
(((z |^ 3) * z) - ((z |^ 3) * a2)) + ((- (((3 * (z |^ 2)) * a2) * z)) + (((3 * (z |^ 2)) * a2) * a2)) is complex set
((3 * (a2 |^ 2)) * z) * z is complex set
((3 * (a2 |^ 2)) * z) * a2 is complex set
(((3 * (a2 |^ 2)) * z) * z) - (((3 * (a2 |^ 2)) * z) * a2) is complex set
((((z |^ 3) * z) - ((z |^ 3) * a2)) + ((- (((3 * (z |^ 2)) * a2) * z)) + (((3 * (z |^ 2)) * a2) * a2))) + ((((3 * (a2 |^ 2)) * z) * z) - (((3 * (a2 |^ 2)) * z) * a2)) is complex set
(a2 |^ 3) * z is complex set
- ((a2 |^ 3) * z) is complex set
(a2 |^ 3) * a2 is complex set
(- ((a2 |^ 3) * z)) + ((a2 |^ 3) * a2) is complex set
(((((z |^ 3) * z) - ((z |^ 3) * a2)) + ((- (((3 * (z |^ 2)) * a2) * z)) + (((3 * (z |^ 2)) * a2) * a2))) + ((((3 * (a2 |^ 2)) * z) * z) - (((3 * (a2 |^ 2)) * z) * a2))) + ((- ((a2 |^ 3) * z)) + ((a2 |^ 3) * a2)) is complex set
a2 |^ (3 + 1) is complex set
(- ((a2 |^ 3) * z)) + (a2 |^ (3 + 1)) is complex set
(((((z |^ 3) * z) - ((z |^ 3) * a2)) + ((- (((3 * (z |^ 2)) * a2) * z)) + (((3 * (z |^ 2)) * a2) * a2))) + ((((3 * (a2 |^ 2)) * z) * z) - (((3 * (a2 |^ 2)) * z) * a2))) + ((- ((a2 |^ 3) * z)) + (a2 |^ (3 + 1))) is complex set
(z |^ 4) - ((z |^ 3) * a2) is complex set
(z |^ 2) * z is complex set
3 * ((z |^ 2) * z) is complex set
(3 * ((z |^ 2) * z)) * a2 is complex set
- ((3 * ((z |^ 2) * z)) * a2) is complex set
(- ((3 * ((z |^ 2) * z)) * a2)) + (((3 * (z |^ 2)) * a2) * a2) is complex set
((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * ((z |^ 2) * z)) * a2)) + (((3 * (z |^ 2)) * a2) * a2)) is complex set
(((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * ((z |^ 2) * z)) * a2)) + (((3 * (z |^ 2)) * a2) * a2))) + ((((3 * (a2 |^ 2)) * z) * z) - (((3 * (a2 |^ 2)) * z) * a2)) is complex set
(- ((a2 |^ 3) * z)) + (a2 |^ 4) is complex set
((((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * ((z |^ 2) * z)) * a2)) + (((3 * (z |^ 2)) * a2) * a2))) + ((((3 * (a2 |^ 2)) * z) * z) - (((3 * (a2 |^ 2)) * z) * a2))) + ((- ((a2 |^ 3) * z)) + (a2 |^ 4)) is complex set
2 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
z |^ (2 + 1) is complex set
3 * (z |^ (2 + 1)) is complex set
(3 * (z |^ (2 + 1))) * a2 is complex set
- ((3 * (z |^ (2 + 1))) * a2) is complex set
(- ((3 * (z |^ (2 + 1))) * a2)) + (((3 * (z |^ 2)) * a2) * a2) is complex set
((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ (2 + 1))) * a2)) + (((3 * (z |^ 2)) * a2) * a2)) is complex set
(((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ (2 + 1))) * a2)) + (((3 * (z |^ 2)) * a2) * a2))) + ((((3 * (a2 |^ 2)) * z) * z) - (((3 * (a2 |^ 2)) * z) * a2)) is complex set
((((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ (2 + 1))) * a2)) + (((3 * (z |^ 2)) * a2) * a2))) + ((((3 * (a2 |^ 2)) * z) * z) - (((3 * (a2 |^ 2)) * z) * a2))) + ((- ((a2 |^ 3) * z)) + (a2 |^ 4)) is complex set
3 * (z |^ 3) is complex set
(3 * (z |^ 3)) * a2 is complex set
- ((3 * (z |^ 3)) * a2) is complex set
a2 * a2 is complex set
(3 * (z |^ 2)) * (a2 * a2) is complex set
(- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 * a2)) is complex set
((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 * a2))) is complex set
(((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 * a2)))) + ((((3 * (a2 |^ 2)) * z) * z) - (((3 * (a2 |^ 2)) * z) * a2)) is complex set
((((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 * a2)))) + ((((3 * (a2 |^ 2)) * z) * z) - (((3 * (a2 |^ 2)) * z) * a2))) + ((- ((a2 |^ 3) * z)) + (a2 |^ 4)) is complex set
a2 |^ 1 is complex set
(a2 |^ 1) * a2 is complex set
(3 * (z |^ 2)) * ((a2 |^ 1) * a2) is complex set
(- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * ((a2 |^ 1) * a2)) is complex set
((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * ((a2 |^ 1) * a2))) is complex set
(((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * ((a2 |^ 1) * a2)))) + ((((3 * (a2 |^ 2)) * z) * z) - (((3 * (a2 |^ 2)) * z) * a2)) is complex set
((((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * ((a2 |^ 1) * a2)))) + ((((3 * (a2 |^ 2)) * z) * z) - (((3 * (a2 |^ 2)) * z) * a2))) + ((- ((a2 |^ 3) * z)) + (a2 |^ 4)) is complex set
1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
a2 |^ (1 + 1) is complex set
(3 * (z |^ 2)) * (a2 |^ (1 + 1)) is complex set
(- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 |^ (1 + 1))) is complex set
((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 |^ (1 + 1)))) is complex set
(((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 |^ (1 + 1))))) + ((((3 * (a2 |^ 2)) * z) * z) - (((3 * (a2 |^ 2)) * z) * a2)) is complex set
((((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 |^ (1 + 1))))) + ((((3 * (a2 |^ 2)) * z) * z) - (((3 * (a2 |^ 2)) * z) * a2))) + ((- ((a2 |^ 3) * z)) + (a2 |^ 4)) is complex set
(3 * (z |^ 2)) * (a2 |^ 2) is complex set
(- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 |^ 2)) is complex set
((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 |^ 2))) is complex set
z * z is complex set
(3 * (a2 |^ 2)) * (z * z) is complex set
((3 * (a2 |^ 2)) * (z * z)) - (((3 * (a2 |^ 2)) * z) * a2) is complex set
(((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 |^ 2)))) + (((3 * (a2 |^ 2)) * (z * z)) - (((3 * (a2 |^ 2)) * z) * a2)) is complex set
((((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 |^ 2)))) + (((3 * (a2 |^ 2)) * (z * z)) - (((3 * (a2 |^ 2)) * z) * a2))) + ((- ((a2 |^ 3) * z)) + (a2 |^ 4)) is complex set
z |^ 1 is complex set
(z |^ 1) * z is complex set
(3 * (a2 |^ 2)) * ((z |^ 1) * z) is complex set
(3 * (a2 |^ 2)) * a2 is complex set
((3 * (a2 |^ 2)) * a2) * z is complex set
((3 * (a2 |^ 2)) * ((z |^ 1) * z)) - (((3 * (a2 |^ 2)) * a2) * z) is complex set
(((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 |^ 2)))) + (((3 * (a2 |^ 2)) * ((z |^ 1) * z)) - (((3 * (a2 |^ 2)) * a2) * z)) is complex set
((((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 |^ 2)))) + (((3 * (a2 |^ 2)) * ((z |^ 1) * z)) - (((3 * (a2 |^ 2)) * a2) * z))) + ((- ((a2 |^ 3) * z)) + (a2 |^ 4)) is complex set
z |^ (1 + 1) is complex set
(3 * (a2 |^ 2)) * (z |^ (1 + 1)) is complex set
(a2 |^ 2) * a2 is complex set
3 * ((a2 |^ 2) * a2) is complex set
(3 * ((a2 |^ 2) * a2)) * z is complex set
((3 * (a2 |^ 2)) * (z |^ (1 + 1))) - ((3 * ((a2 |^ 2) * a2)) * z) is complex set
(((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 |^ 2)))) + (((3 * (a2 |^ 2)) * (z |^ (1 + 1))) - ((3 * ((a2 |^ 2) * a2)) * z)) is complex set
((((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 |^ 2)))) + (((3 * (a2 |^ 2)) * (z |^ (1 + 1))) - ((3 * ((a2 |^ 2) * a2)) * z))) + ((- ((a2 |^ 3) * z)) + (a2 |^ 4)) is complex set
(3 * (a2 |^ 2)) * (z |^ 2) is complex set
a2 |^ (2 + 1) is complex set
3 * (a2 |^ (2 + 1)) is complex set
(3 * (a2 |^ (2 + 1))) * z is complex set
((3 * (a2 |^ 2)) * (z |^ 2)) - ((3 * (a2 |^ (2 + 1))) * z) is complex set
(((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 |^ 2)))) + (((3 * (a2 |^ 2)) * (z |^ 2)) - ((3 * (a2 |^ (2 + 1))) * z)) is complex set
((((z |^ 4) - ((z |^ 3) * a2)) + ((- ((3 * (z |^ 3)) * a2)) + ((3 * (z |^ 2)) * (a2 |^ 2)))) + (((3 * (a2 |^ 2)) * (z |^ 2)) - ((3 * (a2 |^ (2 + 1))) * z))) + ((- ((a2 |^ 3) * z)) + (a2 |^ 4)) is complex set
z is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative set
a2 is complex set
|.a2.| is complex real ext-real Element of REAL
z -root |.a2.| is complex real ext-real set
Arg a2 is complex real ext-real Element of REAL
(Arg a2) / z is complex real ext-real Element of COMPLEX
cos ((Arg a2) / z) is complex real ext-real set
sin ((Arg a2) / z) is complex real ext-real set
(sin ((Arg a2) / z)) * <i> is complex set
(cos ((Arg a2) / z)) + ((sin ((Arg a2) / z)) * <i>) is complex set
(z -root |.a2.|) * ((cos ((Arg a2) / z)) + ((sin ((Arg a2) / z)) * <i>)) is complex set
z is complex set
a2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative set
(a2,z) is complex set
|.z.| is complex real ext-real Element of REAL
a2 -root |.z.| is complex real ext-real set
Arg z is complex real ext-real Element of REAL
(Arg z) / a2 is complex real ext-real Element of COMPLEX
cos ((Arg z) / a2) is complex real ext-real set
sin ((Arg z) / a2) is complex real ext-real set
(sin ((Arg z) / a2)) * <i> is complex set
(cos ((Arg z) / a2)) + ((sin ((Arg z) / a2)) * <i>) is complex set
(a2 -root |.z.|) * ((cos ((Arg z) / a2)) + ((sin ((Arg z) / a2)) * <i>)) is complex set
(a2,z) |^ a2 is complex set
a1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
a1 -root |.z.| is complex real ext-real set
2 * PI is complex real ext-real Element of REAL
(2 * PI) * 0 is complex real ext-real Element of REAL
(Arg z) + ((2 * PI) * 0) is complex real ext-real Element of REAL
((Arg z) + ((2 * PI) * 0)) / a1 is complex real ext-real Element of COMPLEX
cos (((Arg z) + ((2 * PI) * 0)) / a1) is complex real ext-real set
(a1 -root |.z.|) * (cos (((Arg z) + ((2 * PI) * 0)) / a1)) is complex real ext-real set
sin (((Arg z) + ((2 * PI) * 0)) / a1) is complex real ext-real set
(a1 -root |.z.|) * (sin (((Arg z) + ((2 * PI) * 0)) / a1)) is complex real ext-real set
((a1 -root |.z.|) * (sin (((Arg z) + ((2 * PI) * 0)) / a1))) * <i> is complex set
((a1 -root |.z.|) * (cos (((Arg z) + ((2 * PI) * 0)) / a1))) + (((a1 -root |.z.|) * (sin (((Arg z) + ((2 * PI) * 0)) / a1))) * <i>) is complex set
(((a1 -root |.z.|) * (cos (((Arg z) + ((2 * PI) * 0)) / a1))) + (((a1 -root |.z.|) * (sin (((Arg z) + ((2 * PI) * 0)) / a1))) * <i>)) |^ a1 is complex set
z is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative set
a2 is complex real ext-real set
(z,a2) is complex set
|.a2.| is complex real ext-real Element of REAL
z -root |.a2.| is complex real ext-real set
Arg a2 is complex real ext-real Element of REAL
(Arg a2) / z is complex real ext-real Element of COMPLEX
cos ((Arg a2) / z) is complex real ext-real set
sin ((Arg a2) / z) is complex real ext-real set
(sin ((Arg a2) / z)) * <i> is complex set
(cos ((Arg a2) / z)) + ((sin ((Arg a2) / z)) * <i>) is complex set
(z -root |.a2.|) * ((cos ((Arg a2) / z)) + ((sin ((Arg a2) / z)) * <i>)) is complex set
z -root a2 is complex real ext-real set
a1 is complex real ext-real Element of REAL
Arg a1 is complex real ext-real Element of REAL
z is complex set
a2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative set
(a2,z) is complex set
|.z.| is complex real ext-real Element of REAL
a2 -root |.z.| is complex real ext-real set
Arg z is complex real ext-real Element of REAL
(Arg z) / a2 is complex real ext-real Element of COMPLEX
cos ((Arg z) / a2) is complex real ext-real set
sin ((Arg z) / a2) is complex real ext-real set
(sin ((Arg z) / a2)) * <i> is complex set
(cos ((Arg z) / a2)) + ((sin ((Arg z) / a2)) * <i>) is complex set
(a2 -root |.z.|) * ((cos ((Arg z) / a2)) + ((sin ((Arg z) / a2)) * <i>)) is complex set
a1 is complex real ext-real set
z / a1 is complex Element of COMPLEX
(a2,(z / a1)) is complex set
|.(z / a1).| is complex real ext-real Element of REAL
a2 -root |.(z / a1).| is complex real ext-real set
Arg (z / a1) is complex real ext-real Element of REAL
(Arg (z / a1)) / a2 is complex real ext-real Element of COMPLEX
cos ((Arg (z / a1)) / a2) is complex real ext-real set
sin ((Arg (z / a1)) / a2) is complex real ext-real set
(sin ((Arg (z / a1)) / a2)) * <i> is complex set
(cos ((Arg (z / a1)) / a2)) + ((sin ((Arg (z / a1)) / a2)) * <i>) is complex set
(a2 -root |.(z / a1).|) * ((cos ((Arg (z / a1)) / a2)) + ((sin ((Arg (z / a1)) / a2)) * <i>)) is complex set
(a2,a1) is complex set
|.a1.| is complex real ext-real Element of REAL
a2 -root |.a1.| is complex real ext-real set
Arg a1 is complex real ext-real Element of REAL
(Arg a1) / a2 is complex real ext-real Element of COMPLEX
cos ((Arg a1) / a2) is complex real ext-real set
sin ((Arg a1) / a2) is complex real ext-real set
(sin ((Arg a1) / a2)) * <i> is complex set
(cos ((Arg a1) / a2)) + ((sin ((Arg a1) / a2)) * <i>) is complex set
(a2 -root |.a1.|) * ((cos ((Arg a1) / a2)) + ((sin ((Arg a1) / a2)) * <i>)) is complex set
(a2,z) / (a2,a1) is complex Element of COMPLEX
1 / a1 is complex real ext-real Element of COMPLEX
0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
a3 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
z * (1 / a1) is complex set
a0 is complex real ext-real Element of REAL
z * a0 is complex set
Arg (z * a0) is complex real ext-real Element of REAL
|.z.| / |.a1.| is complex real ext-real Element of COMPLEX
a3 -root (|.z.| / |.a1.|) is complex real ext-real set
(Arg z) / a3 is complex real ext-real Element of COMPLEX
cos ((Arg z) / a3) is complex real ext-real set
sin ((Arg z) / a3) is complex real ext-real set
(sin ((Arg z) / a3)) * <i> is complex set
(cos ((Arg z) / a3)) + ((sin ((Arg z) / a3)) * <i>) is complex set
(a3 -root (|.z.| / |.a1.|)) * ((cos ((Arg z) / a3)) + ((sin ((Arg z) / a3)) * <i>)) is complex set
a3 -root |.z.| is complex real ext-real set
a3 -root |.a1.| is complex real ext-real set
(a3 -root |.z.|) / (a3 -root |.a1.|) is complex real ext-real Element of COMPLEX
((a3 -root |.z.|) / (a3 -root |.a1.|)) * ((cos ((Arg z) / a3)) + ((sin ((Arg z) / a3)) * <i>)) is complex set
(a3 -root |.a1.|) / (a3 -root |.z.|) is complex real ext-real Element of COMPLEX
((cos ((Arg z) / a3)) + ((sin ((Arg z) / a3)) * <i>)) / ((a3 -root |.a1.|) / (a3 -root |.z.|)) is complex Element of COMPLEX
(a3 -root |.z.|) * ((cos ((Arg z) / a3)) + ((sin ((Arg z) / a3)) * <i>)) is complex set
((a3 -root |.z.|) * ((cos ((Arg z) / a3)) + ((sin ((Arg z) / a3)) * <i>))) / (a3 -root |.a1.|) is complex Element of COMPLEX
a3 -root a1 is complex real ext-real set
(a2,z) / (a3 -root a1) is complex Element of COMPLEX
z is complex set
(2,z) is complex set
|.z.| is complex real ext-real Element of REAL
2 -root |.z.| is complex real ext-real set
Arg z is complex real ext-real Element of REAL
(Arg z) / 2 is complex real ext-real Element of COMPLEX
cos ((Arg z) / 2) is complex real ext-real set
sin ((Arg z) / 2) is complex real ext-real set
(sin ((Arg z) / 2)) * <i> is complex set
(cos ((Arg z) / 2)) + ((sin ((Arg z) / 2)) * <i>) is complex set
(2 -root |.z.|) * ((cos ((Arg z) / 2)) + ((sin ((Arg z) / 2)) * <i>)) is complex set
- (2,z) is complex set
a2 is complex set
a2 |^ 2 is complex set
(2,z) |^ 2 is complex set
(2,z) * (2,z) is complex set
a2 * a2 is complex set
a2 - (2,z) is complex set
a2 + (2,z) is complex set
(a2 - (2,z)) * (a2 + (2,z)) is complex set
(a2 * a2) - ((2,z) * (2,z)) is complex set
z is complex set
z |^ 2 is complex set
a2 is complex set
a2 * z is complex set
(z |^ 2) + (a2 * z) is complex set
a1 is complex set
a0 is complex set
a1 + a0 is complex set
- (a1 + a0) is complex set
a1 * a0 is complex set
a3 is complex set
((z |^ 2) + (a2 * z)) + a3 is complex set
z - a1 is complex set
z - a0 is complex set
(z - a1) * (z - a0) is complex set
z * z is complex set
(z * z) + (a2 * z) is complex set
((z * z) + (a2 * z)) + a3 is complex set
z is complex set
z |^ 2 is complex set
a2 is complex set
a2 * (z |^ 2) is complex set
2 * a2 is complex set
a1 is complex set
a1 * z is complex set
(a2 * (z |^ 2)) + (a1 * z) is complex set
a1 / (2 * a2) is complex Element of COMPLEX
- (a1 / (2 * a2)) is complex Element of COMPLEX
a0 is complex set
((a2 * (z |^ 2)) + (a1 * z)) + a0 is complex set
delta (a0,a1,a2) is complex set
a1 ^2 is complex set
a1 * a1 is complex set
4 * a0 is complex set
(4 * a0) * a2 is complex set
(a1 ^2) - ((4 * a0) * a2) is complex set
(2,(delta (a0,a1,a2))) is complex set
|.(delta (a0,a1,a2)).| is complex real ext-real Element of REAL
2 -root |.(delta (a0,a1,a2)).| is complex real ext-real set
Arg (delta (a0,a1,a2)) is complex real ext-real Element of REAL
(Arg (delta (a0,a1,a2))) / 2 is complex real ext-real Element of COMPLEX
cos ((Arg (delta (a0,a1,a2))) / 2) is complex real ext-real set
sin ((Arg (delta (a0,a1,a2))) / 2) is complex real ext-real set
(sin ((Arg (delta (a0,a1,a2))) / 2)) * <i> is complex set
(cos ((Arg (delta (a0,a1,a2))) / 2)) + ((sin ((Arg (delta (a0,a1,a2))) / 2)) * <i>) is complex set
(2 -root |.(delta (a0,a1,a2)).|) * ((cos ((Arg (delta (a0,a1,a2))) / 2)) + ((sin ((Arg (delta (a0,a1,a2))) / 2)) * <i>)) is complex set
(2,(delta (a0,a1,a2))) / (2 * a2) is complex Element of COMPLEX
(- (a1 / (2 * a2))) + ((2,(delta (a0,a1,a2))) / (2 * a2)) is complex Element of COMPLEX
(- (a1 / (2 * a2))) - ((2,(delta (a0,a1,a2))) / (2 * a2)) is complex Element of COMPLEX
((- (a1 / (2 * a2))) + ((2,(delta (a0,a1,a2))) / (2 * a2))) + ((- (a1 / (2 * a2))) - ((2,(delta (a0,a1,a2))) / (2 * a2))) is complex Element of COMPLEX
- (((- (a1 / (2 * a2))) + ((2,(delta (a0,a1,a2))) / (2 * a2))) + ((- (a1 / (2 * a2))) - ((2,(delta (a0,a1,a2))) / (2 * a2)))) is complex Element of COMPLEX
(a1 / (2 * a2)) + (a1 / (2 * a2)) is complex Element of COMPLEX
1 / 2 is non zero complex real ext-real positive non negative Element of COMPLEX
a1 / a2 is complex Element of COMPLEX
(1 / 2) * (a1 / a2) is complex Element of COMPLEX
((1 / 2) * (a1 / a2)) + (a1 / (2 * a2)) is complex Element of COMPLEX
((1 / 2) * (a1 / a2)) + ((1 / 2) * (a1 / a2)) is complex Element of COMPLEX
(((a2 * (z |^ 2)) + (a1 * z)) + a0) / a2 is complex Element of COMPLEX
((((a2 * (z |^ 2)) + (a1 * z)) + a0) / a2) * a2 is complex set
(a2 * (z |^ 2)) / a2 is complex Element of COMPLEX
(a1 * z) / a2 is complex Element of COMPLEX
((a2 * (z |^ 2)) / a2) + ((a1 * z) / a2) is complex Element of COMPLEX
a0 / a2 is complex Element of COMPLEX
(((a2 * (z |^ 2)) / a2) + ((a1 * z) / a2)) + (a0 / a2) is complex Element of COMPLEX
((((a2 * (z |^ 2)) / a2) + ((a1 * z) / a2)) + (a0 / a2)) * a2 is complex set
(z |^ 2) + ((a1 * z) / a2) is complex set
((z |^ 2) + ((a1 * z) / a2)) + (a0 / a2) is complex set
(((z |^ 2) + ((a1 * z) / a2)) + (a0 / a2)) * a2 is complex set
z / a2 is complex Element of COMPLEX
a1 * (z / a2) is complex set
(z |^ 2) + (a1 * (z / a2)) is complex set
((z |^ 2) + (a1 * (z / a2))) + (a0 / a2) is complex set
(((z |^ 2) + (a1 * (z / a2))) + (a0 / a2)) * a2 is complex set
a2 / a1 is complex Element of COMPLEX
z / (a2 / a1) is complex Element of COMPLEX
(z |^ 2) + (z / (a2 / a1)) is complex set
((z |^ 2) + (z / (a2 / a1))) + (a0 / a2) is complex set
(((z |^ 2) + (z / (a2 / a1))) + (a0 / a2)) * a2 is complex set
(a1 / a2) * z is complex set
(z |^ 2) + ((a1 / a2) * z) is complex set
((z |^ 2) + ((a1 / a2) * z)) + (a0 / a2) is complex set
(((z |^ 2) + ((a1 / a2) * z)) + (a0 / a2)) * a2 is complex set
((- (a1 / (2 * a2))) + ((2,(delta (a0,a1,a2))) / (2 * a2))) * ((- (a1 / (2 * a2))) - ((2,(delta (a0,a1,a2))) / (2 * a2))) is complex Element of COMPLEX
(a1 / (2 * a2)) * (a1 / (2 * a2)) is complex Element of COMPLEX
((2,(delta (a0,a1,a2))) / (2 * a2)) * ((2,(delta (a0,a1,a2))) / (2 * a2)) is complex Element of COMPLEX
((a1 / (2 * a2)) * (a1 / (2 * a2))) - (((2,(delta (a0,a1,a2))) / (2 * a2)) * ((2,(delta (a0,a1,a2))) / (2 * a2))) is complex Element of COMPLEX
(2 * a2) * (2 * a2) is complex set
(a1 * a1) / ((2 * a2) * (2 * a2)) is complex Element of COMPLEX
((a1 * a1) / ((2 * a2) * (2 * a2))) - (((2,(delta (a0,a1,a2))) / (2 * a2)) * ((2,(delta (a0,a1,a2))) / (2 * a2))) is complex Element of COMPLEX
4 * a2 is complex set
(4 * a2) * a2 is complex set
(a1 * a1) / ((4 * a2) * a2) is complex Element of COMPLEX
(2,(delta (a0,a1,a2))) * (2,(delta (a0,a1,a2))) is complex set
((2,(delta (a0,a1,a2))) * (2,(delta (a0,a1,a2)))) / ((2 * a2) * (2 * a2)) is complex Element of COMPLEX
((a1 * a1) / ((4 * a2) * a2)) - (((2,(delta (a0,a1,a2))) * (2,(delta (a0,a1,a2)))) / ((2 * a2) * (2 * a2))) is complex Element of COMPLEX
(2,(delta (a0,a1,a2))) |^ 2 is complex set
((2,(delta (a0,a1,a2))) |^ 2) / ((2 * a2) * (2 * a2)) is complex Element of COMPLEX
((a1 * a1) / ((4 * a2) * a2)) - (((2,(delta (a0,a1,a2))) |^ 2) / ((2 * a2) * (2 * a2))) is complex Element of COMPLEX
(delta (a0,a1,a2)) / ((2 * a2) * (2 * a2)) is complex Element of COMPLEX
((a1 * a1) / ((4 * a2) * a2)) - ((delta (a0,a1,a2)) / ((2 * a2) * (2 * a2))) is complex Element of COMPLEX
(a1 * a1) - (delta (a0,a1,a2)) is complex set
((a1 * a1) - (delta (a0,a1,a2))) / ((4 * a2) * a2) is complex Element of COMPLEX
a0 * (4 * a2) is complex set
a2 * (4 * a2) is complex set
(a0 * (4 * a2)) / (a2 * (4 * a2)) is complex Element of COMPLEX
(4 * a2) / (4 * a2) is complex Element of COMPLEX
(a0 / a2) * ((4 * a2) / (4 * a2)) is complex Element of COMPLEX
(a0 / a2) * 1 is complex set
9 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
27 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
54 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
z is complex set
z |^ 3 is complex set
z |^ 2 is complex set
a2 is complex set
a2 / 3 is complex Element of COMPLEX
a2 |^ 2 is complex set
9 * a2 is complex set
a2 |^ 3 is complex set
2 * (a2 |^ 3) is complex set
a2 * (z |^ 2) is complex set
(z |^ 3) + (a2 * (z |^ 2)) is complex set
a1 is complex set
3 * a1 is complex set
(3 * a1) - (a2 |^ 2) is complex set
((3 * a1) - (a2 |^ 2)) / 9 is complex Element of COMPLEX
(9 * a2) * a1 is complex set
((9 * a2) * a1) - (2 * (a2 |^ 3)) is complex set
a1 * z is complex set
((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z) is complex set
a0 is complex set
27 * a0 is complex set
(((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0) is complex set
((((9 * a2) * a1) - (2 * (a2 |^ 3))) - (27 * a0)) / 54 is complex Element of COMPLEX
(((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0 is complex set
a3 is complex set
a3 - (a2 / 3) is complex set
a3 |^ 3 is complex set
a4 is complex set
3 * a4 is complex set
(3 * a4) * a3 is complex set
(a3 |^ 3) + ((3 * a4) * a3) is complex set
s4 is complex set
2 * s4 is complex set
((a3 |^ 3) + ((3 * a4) * a3)) - (2 * s4) is complex set
3 * z is complex set
3 * a3 is complex set
(3 * a3) - a2 is complex set
(3 * a3) |^ 2 is complex set
3 |^ 2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
a3 |^ 2 is complex set
(3 |^ 2) * (a3 |^ 2) is complex set
3 * 3 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(3 * 3) * (a3 |^ 2) is complex set
9 * (a3 |^ 2) is complex set
(3 * a3) |^ 3 is complex set
3 |^ 3 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
(3 |^ 3) * (a3 |^ 3) is complex set
(3 * 3) * 3 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
((3 * 3) * 3) * (a3 |^ 3) is complex set
27 * (a3 |^ 3) is complex set
27 * (z |^ 3) is complex set
((3 * 3) * 3) * (z |^ 3) is complex set
(3 |^ 3) * (z |^ 3) is complex set
((3 * a3) - a2) |^ 3 is complex set
3 * (9 * (a3 |^ 2)) is complex set
(3 * (9 * (a3 |^ 2))) * a2 is complex set
(27 * (a3 |^ 3)) - ((3 * (9 * (a3 |^ 2))) * a2) is complex set
3 * (a2 |^ 2) is complex set
(3 * (a2 |^ 2)) * (3 * a3) is complex set
((27 * (a3 |^ 3)) - ((3 * (9 * (a3 |^ 2))) * a2)) + ((3 * (a2 |^ 2)) * (3 * a3)) is complex set
(((27 * (a3 |^ 3)) - ((3 * (9 * (a3 |^ 2))) * a2)) + ((3 * (a2 |^ 2)) * (3 * a3))) - (a2 |^ 3) is complex set
27 * a2 is complex set
(27 * a2) * (a3 |^ 2) is complex set
(27 * (a3 |^ 3)) - ((27 * a2) * (a3 |^ 2)) is complex set
9 * (a2 |^ 2) is complex set
(9 * (a2 |^ 2)) * a3 is complex set
((27 * (a3 |^ 3)) - ((27 * a2) * (a3 |^ 2))) + ((9 * (a2 |^ 2)) * a3) is complex set
(((27 * (a3 |^ 3)) - ((27 * a2) * (a3 |^ 2))) + ((9 * (a2 |^ 2)) * a3)) - (a2 |^ 3) is complex set
27 * a1 is complex set
(27 * a1) * z is complex set
(27 * a1) * a3 is complex set
((27 * a1) * a3) - ((9 * a2) * a1) is complex set
27 * 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(27 * 1) * a2 is complex set
((27 * 1) * a2) * (z |^ 2) is complex set
3 * a2 is complex set
(3 * a2) * (3 * 3) is complex set
1 * 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
((3 * a2) * (3 * 3)) * (1 * 1) is complex set
(((3 * a2) * (3 * 3)) * (1 * 1)) * (z |^ 2) is complex set
(3 * a2) * (3 |^ 2) is complex set
((3 * a2) * (3 |^ 2)) * (z |^ 2) is complex set
(3 |^ 2) * (z |^ 2) is complex set
(3 * a2) * ((3 |^ 2) * (z |^ 2)) is complex set
(3 * z) |^ 2 is complex set
(3 * a2) * ((3 * z) |^ 2) is complex set
2 * (3 * a3) is complex set
(2 * (3 * a3)) * a2 is complex set
((3 * a3) |^ 2) - ((2 * (3 * a3)) * a2) is complex set
(((3 * a3) |^ 2) - ((2 * (3 * a3)) * a2)) + (a2 |^ 2) is complex set
(3 * a2) * ((((3 * a3) |^ 2) - ((2 * (3 * a3)) * a2)) + (a2 |^ 2)) is complex set
(3 * a3) * (3 * a3) is complex set
((3 * a3) * (3 * a3)) - ((2 * (3 * a3)) * a2) is complex set
(((3 * a3) * (3 * a3)) - ((2 * (3 * a3)) * a2)) + (a2 |^ 2) is complex set
(3 * a2) * ((((3 * a3) * (3 * a3)) - ((2 * (3 * a3)) * a2)) + (a2 |^ 2)) is complex set
(27 * a2) * a3 is complex set
((27 * a2) * a3) * a3 is complex set
((2 * (3 * a3)) * a2) * (3 * a2) is complex set
(((27 * a2) * a3) * a3) - (((2 * (3 * a3)) * a2) * (3 * a2)) is complex set
(a2 |^ 2) * (3 * a2) is complex set
((((27 * a2) * a3) * a3) - (((2 * (3 * a3)) * a2) * (3 * a2))) + ((a2 |^ 2) * (3 * a2)) is complex set
a3 * a3 is complex set
(27 * a2) * (a3 * a3) is complex set
18 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
a2 * a2 is complex set
18 * (a2 * a2) is complex set
(18 * (a2 * a2)) * a3 is complex set
((27 * a2) * (a3 * a3)) - ((18 * (a2 * a2)) * a3) is complex set
(3 * a2) * (a2 * a2) is complex set
(((27 * a2) * (a3 * a3)) - ((18 * (a2 * a2)) * a3)) + ((3 * a2) * (a2 * a2)) is complex set
((27 * a2) * (a3 |^ 2)) - ((18 * (a2 * a2)) * a3) is complex set
(3 * a2) * a2 is complex set
((3 * a2) * a2) * a2 is complex set
(((27 * a2) * (a3 |^ 2)) - ((18 * (a2 * a2)) * a3)) + (((3 * a2) * a2) * a2) is complex set
18 * (a2 |^ 2) is complex set
(18 * (a2 |^ 2)) * a3 is complex set
((27 * a2) * (a3 |^ 2)) - ((18 * (a2 |^ 2)) * a3) is complex set
(a2 * a2) * a2 is complex set
3 * ((a2 * a2) * a2) is complex set
(((27 * a2) * (a3 |^ 2)) - ((18 * (a2 |^ 2)) * a3)) + (3 * ((a2 * a2) * a2)) is complex set
3 * (a2 |^ 3) is complex set
(((27 * a2) * (a3 |^ 2)) - ((18 * (a2 |^ 2)) * a3)) + (3 * (a2 |^ 3)) is complex set
27 * ((((z |^ 3) + (a2 * (z |^ 2))) + (a1 * z)) + a0) is complex set
- (9 * (a2 |^ 2)) is complex set
(- (9 * (a2 |^ 2))) + (27 * a1) is complex set
((- (9 * (a2 |^ 2))) + (27 * a1)) * a3 is complex set
(27 * (a3 |^ 3)) + (((- (9 * (a2 |^ 2))) + (27 * a1)) * a3) is complex set
(2 * (a2 |^ 3)) - ((9 * a2) * a1) is complex set
((2 * (a2 |^ 3)) - ((9 * a2) * a1)) + (27 * a0) is complex set
((27 * (a3 |^ 3)) + (((- (9 * (a2 |^ 2))) + (27 * a1)) * a3)) + (((2 * (a2 |^ 3)) - ((9 * a2) * a1)) + (27 * a0)) is complex set
27 * (((a3 |^ 3) + ((3 * a4) * a3)) - (2 * s4)) is complex set
z is complex set
z |^ 3 is complex set
z |^ 2 is complex set
a2 is complex set
a2 * (z |^ 2) is complex set
(z |^ 3) + (a2 * (z |^ 2)) is complex set
a1 is complex set
a0 is complex set
a1 + a0 is complex set
a1 * a0 is complex set
a3 is complex set
a3 * z is complex set
((z |^ 3) + (a2 * (z |^ 2))) + (a3 * z) is complex set
a4 is complex set
(((z |^ 3) + (a2 * (z |^ 2))) + (a3 * z)) + a4 is complex set
s4 is complex set
(a1 + a0) + s4 is complex set
- ((a1 + a0) + s4) is complex set
a1 * s4 is complex set
(a1 * a0) + (a1 * s4) is complex set
a0 * s4 is complex set
((a1 * a0) + (a1 * s4)) + (a0 * s4) is complex set
(a1 * a0) * s4 is complex set
- ((a1 * a0) * s4) is complex set
z - a1 is complex set
z - a0 is complex set
(z - a1) * (z - a0) is complex set
z - s4 is complex set
((z - a1) * (z - a0)) * (z - s4) is complex set
z * z is complex set
(z * z) * z is complex set
a2 * z is complex set
(a2 * z) * z is complex set
((z * z) * z) + ((a2 * z) * z) is complex set
(((z * z) * z) + ((a2 * z) * z)) + (a3 * z) is complex set
((((z * z) * z) + ((a2 * z) * z)) + (a3 * z)) + a4 is complex set
a2 * (z * z) is complex set
(z |^ 3) + (a2 * (z * z)) is complex set
((z |^ 3) + (a2 * (z * z))) + (a3 * z) is complex set
(((z |^ 3) + (a2 * (z * z))) + (a3 * z)) + a4 is complex set
(2,3) is complex set
|.3.| is complex real ext-real Element of REAL
2 -root |.3.| is complex real ext-real set
Arg 3 is complex real ext-real Element of REAL
(Arg 3) / 2 is complex real ext-real Element of COMPLEX
cos ((Arg 3) / 2) is complex real ext-real set
sin ((Arg 3) / 2) is complex real ext-real set
(sin ((Arg 3) / 2)) * <i> is complex set
(cos ((Arg 3) / 2)) + ((sin ((Arg 3) / 2)) * <i>) is complex set
(2 -root |.3.|) * ((cos ((Arg 3) / 2)) + ((sin ((Arg 3) / 2)) * <i>)) is complex set
z is complex set
z |^ 3 is complex set
z |^ 2 is complex set
a2 is complex set
3 * a2 is complex set
a2 * z is complex set
a1 is complex set
a1 |^ 2 is complex set
(3 * a2) - (a1 |^ 2) is complex set
((3 * a2) - (a1 |^ 2)) / 9 is complex Element of COMPLEX
9 * a1 is complex set
(9 * a1) * a2 is complex set
a1 |^ 3 is complex set
2 * (a1 |^ 3) is complex set
((9 * a1) * a2) - (2 * (a1 |^ 3)) is complex set
a1 * (z |^ 2) is complex set
(z |^ 3) + (a1 * (z |^ 2)) is complex set
((z |^ 3) + (a1 * (z |^ 2))) + (a2 * z) is complex set
a1 / 3 is complex Element of COMPLEX
a0 is complex set
27 * a0 is complex set
(((9 * a1) * a2) - (2 * (a1 |^ 3))) - (27 * a0) is complex set
((((9 * a1) * a2) - (2 * (a1 |^ 3))) - (27 * a0)) / 54 is complex Element of COMPLEX
(((z |^ 3) + (a1 * (z |^ 2))) + (a2 * z)) + a0 is complex set
a3 is complex set
a4 is complex set
a3 + a4 is complex set
(a3 + a4) - (a1 / 3) is complex set
(a3 + a4) / 2 is complex Element of COMPLEX
- ((a3 + a4) / 2) is complex Element of COMPLEX
(- ((a3 + a4) / 2)) - (a1 / 3) is complex Element of COMPLEX
a3 - a4 is complex set
(a3 - a4) * (2,3) is complex set
((a3 - a4) * (2,3)) * <i> is complex set
(((a3 - a4) * (2,3)) * <i>) / 2 is complex Element of COMPLEX
((- ((a3 + a4) / 2)) - (a1 / 3)) + ((((a3 - a4) * (2,3)) * <i>) / 2) is complex Element of COMPLEX
((- ((a3 + a4) / 2)) - (a1 / 3)) - ((((a3 - a4) * (2,3)) * <i>) / 2) is complex Element of COMPLEX
s4 is complex set
s4 |^ 3 is complex set
s4 / a3 is complex Element of COMPLEX
- (s4 / a3) is complex Element of COMPLEX
s3 is complex set
s3 |^ 2 is complex set
(s4 |^ 3) + (s3 |^ 2) is complex set
(2,((s4 |^ 3) + (s3 |^ 2))) is complex set
|.((s4 |^ 3) + (s3 |^ 2)).| is complex real ext-real Element of REAL
2 -root |.((s4 |^ 3) + (s3 |^ 2)).| is complex real ext-real set
Arg ((s4 |^ 3) + (s3 |^ 2)) is complex real ext-real Element of REAL
(Arg ((s4 |^ 3) + (s3 |^ 2))) / 2 is complex real ext-real Element of COMPLEX
cos ((Arg ((s4 |^ 3) + (s3 |^ 2))) / 2) is complex real ext-real set
sin ((Arg ((s4 |^ 3) + (s3 |^ 2))) / 2) is complex real ext-real set
(sin ((Arg ((s4 |^ 3) + (s3 |^ 2))) / 2)) * <i> is complex set
(cos ((Arg ((s4 |^ 3) + (s3 |^ 2))) / 2)) + ((sin ((Arg ((s4 |^ 3) + (s3 |^ 2))) / 2)) * <i>) is complex set
(2 -root |.((s4 |^ 3) + (s3 |^ 2)).|) * ((cos ((Arg ((s4 |^ 3) + (s3 |^ 2))) / 2)) + ((sin ((Arg ((s4 |^ 3) + (s3 |^ 2))) / 2)) * <i>)) is complex set
s2 is complex set
s3 + s2 is complex set
(3,(s3 + s2)) is complex set
|.(s3 + s2).| is complex real ext-real Element of REAL
3 -root |.(s3 + s2).| is complex real ext-real set
Arg (s3 + s2) is complex real ext-real Element of REAL
(Arg (s3 + s2)) / 3 is complex real ext-real Element of COMPLEX
cos ((Arg (s3 + s2)) / 3) is complex real ext-real set
sin ((Arg (s3 + s2)) / 3) is complex real ext-real set
(sin ((Arg (s3 + s2)) / 3)) * <i> is complex set
(cos ((Arg (s3 + s2)) / 3)) + ((sin ((Arg (s3 + s2)) / 3)) * <i>) is complex set
(3 -root |.(s3 + s2).|) * ((cos ((Arg (s3 + s2)) / 3)) + ((sin ((Arg (s3 + s2)) / 3)) * <i>)) is complex set
(a3 - a4) / 2 is complex Element of COMPLEX
z + (a1 / 3) is complex set
2 * ((a3 + a4) / 2) is complex set
((a3 - a4) / 2) * (2,3) is complex set
(((a3 - a4) / 2) * (2,3)) * <i> is complex set
(- ((a3 + a4) / 2)) + ((((a3 - a4) / 2) * (2,3)) * <i>) is complex set
(- ((a3 + a4) / 2)) - ((((a3 - a4) / 2) * (2,3)) * <i>) is complex set
(2 * ((a3 + a4) / 2)) + ((- ((a3 + a4) / 2)) + ((((a3 - a4) / 2) * (2,3)) * <i>)) is complex set
((2 * ((a3 + a4) / 2)) + ((- ((a3 + a4) / 2)) + ((((a3 - a4) / 2) * (2,3)) * <i>))) + ((- ((a3 + a4) / 2)) - ((((a3 - a4) / 2) * (2,3)) * <i>)) is complex set
- (((2 * ((a3 + a4) / 2)) + ((- ((a3 + a4) / 2)) + ((((a3 - a4) / 2) * (2,3)) * <i>))) + ((- ((a3 + a4) / 2)) - ((((a3 - a4) / 2) * (2,3)) * <i>))) is complex set
a3 |^ 3 is complex set
s2 |^ 2 is complex set
s2 * s2 is complex set
- s2 is complex set
(- s2) * (- s2) is complex set
s4 * s4 is complex set
(s4 * s4) * s4 is complex set
a4 * a4 is complex set
(a4 * a4) * a4 is complex set
(s4 / a3) * (s4 / a3) is complex Element of COMPLEX
((s4 / a3) * (s4 / a3)) * (s4 / a3) is complex Element of COMPLEX
- (((s4 / a3) * (s4 / a3)) * (s4 / a3)) is complex Element of COMPLEX
s4 * s4 is complex set
a3 * a3 is complex set
(s4 * s4) / (a3 * a3) is complex Element of COMPLEX
((s4 * s4) / (a3 * a3)) * (s4 / a3) is complex Element of COMPLEX
- (((s4 * s4) / (a3 * a3)) * (s4 / a3)) is complex Element of COMPLEX
(s4 * s4) * s4 is complex set
(a3 * a3) * a3 is complex set
((s4 * s4) * s4) / ((a3 * a3) * a3) is complex Element of COMPLEX
- (((s4 * s4) * s4) / ((a3 * a3) * a3)) is complex Element of COMPLEX
(3,(s3 + s2)) |^ 3 is complex set
((s4 * s4) * s4) / ((3,(s3 + s2)) |^ 3) is complex Element of COMPLEX
- (((s4 * s4) * s4) / ((3,(s3 + s2)) |^ 3)) is complex Element of COMPLEX
((s4 * s4) * s4) / (s3 + s2) is complex Element of COMPLEX
- (((s4 * s4) * s4) / (s3 + s2)) is complex Element of COMPLEX
(s4 |^ 3) / (s3 + s2) is complex Element of COMPLEX
- ((s4 |^ 3) / (s3 + s2)) is complex Element of COMPLEX
a3 |^ 3 is complex set
(2 * ((a3 + a4) / 2)) * ((- ((a3 + a4) / 2)) + ((((a3 - a4) / 2) * (2,3)) * <i>)) is complex set
(2 * ((a3 + a4) / 2)) * ((- ((a3 + a4) / 2)) - ((((a3 - a4) / 2) * (2,3)) * <i>)) is complex set
((2 * ((a3 + a4) / 2)) * ((- ((a3 + a4) / 2)) + ((((a3 - a4) / 2) * (2,3)) * <i>))) + ((2 * ((a3 + a4) / 2)) * ((- ((a3 + a4) / 2)) - ((((a3 - a4) / 2) * (2,3)) * <i>))) is complex set
((- ((a3 + a4) / 2)) + ((((a3 - a4) / 2) * (2,3)) * <i>)) *