:: POLYEQ_3 semantic presentation

REAL is V69() V70() V71() V75() set
NAT is V69() V70() V71() V72() V73() V74() V75() Element of K19(REAL)
K19(REAL) is set
COMPLEX is V69() V75() set
K20(NAT,REAL) is V33() V34() V35() set
K19(K20(NAT,REAL)) is set
RAT is V69() V70() V71() V72() V75() set
INT is V69() V70() V71() V72() V73() V75() set
K20(COMPLEX,COMPLEX) is V33() set
K19(K20(COMPLEX,COMPLEX)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is V33() set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(REAL,REAL) is V33() V34() V35() set
K19(K20(REAL,REAL)) is set
K20(K20(REAL,REAL),REAL) is V33() V34() V35() set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is V5( RAT ) V33() V34() V35() set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is V5( RAT ) V33() V34() V35() set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is V5( RAT ) V5( INT ) V33() V34() V35() set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is V5( RAT ) V5( INT ) V33() V34() V35() set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is V5( RAT ) V5( INT ) V33() V34() V35() V36() set
K20(K20(NAT,NAT),NAT) is V5( RAT ) V5( INT ) V33() V34() V35() V36() set
K19(K20(K20(NAT,NAT),NAT)) is set
NAT is V69() V70() V71() V72() V73() V74() V75() set
K19(NAT) is set
K19(NAT) is set
K315() is set
1 is non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() Element of NAT
K20(NAT,COMPLEX) is V33() set
K19(K20(NAT,COMPLEX)) is set
1r is complex Element of COMPLEX
0 is empty ordinal natural complex real ext-real non positive non negative V43() V44() V69() V70() V71() V72() V73() V74() V75() Element of NAT
Re 0 is complex real ext-real Element of REAL
Im 0 is complex real ext-real Element of REAL
<i> is complex Element of COMPLEX
K88(REAL,0,1,0,1) is V1() V4(K81(0,1)) V5( REAL ) V6() V18(K81(0,1), REAL ) V33() V34() V35() Element of K19(K20(K81(0,1),REAL))
K81(0,1) is non empty V69() V70() V71() V72() V73() V74() set
K20(K81(0,1),REAL) is V33() V34() V35() set
K19(K20(K81(0,1),REAL)) is set
|.0.| is complex real ext-real Element of REAL
2 is non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() Element of NAT
3 is non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() Element of NAT
4 is non empty ordinal natural complex real ext-real positive non negative V43() V44() V69() V70() V71() V72() V73() V74() Element of NAT
sqrt 0 is complex real ext-real Element of REAL
sqrt 4 is complex real ext-real Element of REAL
sin is V1() V4( REAL ) V5( REAL ) V6() V18( REAL , REAL ) V33() V34() V35() Element of K19(K20(REAL,REAL))
cos is V1() V4( REAL ) V5( REAL ) V6() V18( REAL , REAL ) V33() V34() V35() Element of K19(K20(REAL,REAL))
cos . 0 is complex real ext-real Element of REAL
sin . 0 is complex real ext-real Element of REAL
cos 0 is complex real ext-real Element of REAL
sin 0 is complex real ext-real Element of REAL
PI is complex real ext-real Element of REAL
2 * PI is complex real ext-real Element of REAL
z is complex Element of COMPLEX
z ^2 is complex set
z * z is complex set
Re z is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
Im z is complex real ext-real Element of REAL
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) - ((Im z) ^2) is complex real ext-real Element of REAL
- ((Im z) ^2) is complex real ext-real set
((Re z) ^2) + (- ((Im z) ^2)) is complex real ext-real set
(Re z) * (Im z) is complex real ext-real Element of REAL
2 * ((Re z) * (Im z)) is complex real ext-real Element of REAL
(2 * ((Re z) * (Im z))) * <i> is complex Element of COMPLEX
(((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * <i>) is complex Element of COMPLEX
(Im z) * <i> is complex Element of COMPLEX
(Re z) + ((Im z) * <i>) is complex Element of COMPLEX
s is complex Element of COMPLEX
n is complex Element of COMPLEX
z is complex real ext-real Element of REAL
s is complex real ext-real Element of REAL
n is complex real ext-real Element of REAL
t is complex Element of COMPLEX
Polynom (z,s,n,t) is complex set
t ^2 is complex set
t * t is complex set
z * (t ^2) is complex set
s * t is complex set
(z * (t ^2)) + (s * t) is complex set
((z * (t ^2)) + (s * t)) + n is complex set
z is complex real ext-real Element of REAL
2 * z is complex real ext-real Element of REAL
s is complex real ext-real Element of REAL
- s is complex real ext-real Element of REAL
s / (2 * z) is complex real ext-real Element of REAL
(2 * z) " is complex real ext-real set
s * ((2 * z) ") is complex real ext-real set
- (s / (2 * z)) is complex real ext-real Element of REAL
n is complex real ext-real Element of REAL
delta (z,s,n) is complex real ext-real Element of REAL
s ^2 is complex real ext-real set
s * s is complex real ext-real set
4 * z is complex real ext-real set
(4 * z) * n is complex real ext-real set
(s ^2) - ((4 * z) * n) is complex real ext-real set
- ((4 * z) * n) is complex real ext-real set
(s ^2) + (- ((4 * z) * n)) is complex real ext-real set
sqrt (delta (z,s,n)) is complex real ext-real Element of REAL
(- s) + (sqrt (delta (z,s,n))) is complex real ext-real Element of REAL
((- s) + (sqrt (delta (z,s,n)))) / (2 * z) is complex real ext-real Element of REAL
((- s) + (sqrt (delta (z,s,n)))) * ((2 * z) ") is complex real ext-real set
(- s) - (sqrt (delta (z,s,n))) is complex real ext-real Element of REAL
- (sqrt (delta (z,s,n))) is complex real ext-real set
(- s) + (- (sqrt (delta (z,s,n)))) is complex real ext-real set
((- s) - (sqrt (delta (z,s,n)))) / (2 * z) is complex real ext-real Element of REAL
((- s) - (sqrt (delta (z,s,n)))) * ((2 * z) ") is complex real ext-real set
t is complex Element of COMPLEX
(z,s,n,t) is complex Element of COMPLEX
t ^2 is complex set
t * t is complex set
z * (t ^2) is complex set
s * t is complex set
(z * (t ^2)) + (s * t) is complex set
((z * (t ^2)) + (s * t)) + n is complex set
0 * <i> is complex Element of COMPLEX
z + (0 * <i>) is complex Element of COMPLEX
Im t is complex real ext-real Element of REAL
Re t is complex real ext-real Element of REAL
(Im t) * <i> is complex Element of COMPLEX
(Re t) + ((Im t) * <i>) is complex Element of COMPLEX
(Re t) ^2 is complex real ext-real Element of REAL
(Re t) * (Re t) is complex real ext-real set
(Im t) ^2 is complex real ext-real Element of REAL
(Im t) * (Im t) is complex real ext-real set
((Re t) ^2) - ((Im t) ^2) is complex real ext-real Element of REAL
- ((Im t) ^2) is complex real ext-real set
((Re t) ^2) + (- ((Im t) ^2)) is complex real ext-real set
(Re t) * (Im t) is complex real ext-real Element of REAL
2 * ((Re t) * (Im t)) is complex real ext-real Element of REAL
(2 * ((Re t) * (Im t))) * <i> is complex Element of COMPLEX
(((Re t) ^2) - ((Im t) ^2)) + ((2 * ((Re t) * (Im t))) * <i>) is complex Element of COMPLEX
(z + (0 * <i>)) * ((((Re t) ^2) - ((Im t) ^2)) + ((2 * ((Re t) * (Im t))) * <i>)) is complex Element of COMPLEX
s * t is complex Element of COMPLEX
((z + (0 * <i>)) * ((((Re t) ^2) - ((Im t) ^2)) + ((2 * ((Re t) * (Im t))) * <i>))) + (s * t) is complex Element of COMPLEX
(((z + (0 * <i>)) * ((((Re t) ^2) - ((Im t) ^2)) + ((2 * ((Re t) * (Im t))) * <i>))) + (s * t)) + n is complex Element of COMPLEX
Re z is complex real ext-real Element of REAL
2 * (Re t) is complex real ext-real Element of REAL
(2 * (Re t)) * (Im t) is complex real ext-real Element of REAL
((2 * (Re t)) * (Im t)) * <i> is complex Element of COMPLEX
(((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>) is complex Element of COMPLEX
Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)) is complex real ext-real Element of REAL
(Re z) * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) is complex real ext-real Element of REAL
Im z is complex real ext-real Element of REAL
Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)) is complex real ext-real Element of REAL
(Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) is complex real ext-real Element of REAL
((Re z) * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) is complex real ext-real Element of REAL
- ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) is complex real ext-real set
((Re z) * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + (- ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) is complex real ext-real set
(Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) is complex real ext-real Element of REAL
(Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z) is complex real ext-real Element of REAL
((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z)) is complex real ext-real Element of REAL
(((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i> is complex Element of COMPLEX
(((Re z) * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>) is complex Element of COMPLEX
((((Re z) * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>)) + (s * t) is complex Element of COMPLEX
(((((Re z) * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>)) + (s * t)) + n is complex Element of COMPLEX
z * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) is complex real ext-real Element of REAL
(z * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) is complex real ext-real Element of REAL
(z * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + (- ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) is complex real ext-real set
((z * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>) is complex Element of COMPLEX
(((z * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>)) + (s * t) is complex Element of COMPLEX
((((z * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>)) + (s * t)) + n is complex Element of COMPLEX
z * (((Re t) ^2) - ((Im t) ^2)) is complex real ext-real Element of REAL
(z * (((Re t) ^2) - ((Im t) ^2))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) is complex real ext-real Element of REAL
(z * (((Re t) ^2) - ((Im t) ^2))) + (- ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) is complex real ext-real set
((z * (((Re t) ^2) - ((Im t) ^2))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>) is complex Element of COMPLEX
(((z * (((Re t) ^2) - ((Im t) ^2))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>)) + (s * t) is complex Element of COMPLEX
((((z * (((Re t) ^2) - ((Im t) ^2))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>)) + (s * t)) + n is complex Element of COMPLEX
0 * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) is complex real ext-real Element of REAL
(z * (((Re t) ^2) - ((Im t) ^2))) - (0 * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) is complex real ext-real Element of REAL
- (0 * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) is complex real ext-real set
(z * (((Re t) ^2) - ((Im t) ^2))) + (- (0 * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) is complex real ext-real set
((z * (((Re t) ^2) - ((Im t) ^2))) - (0 * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>) is complex Element of COMPLEX
(((z * (((Re t) ^2) - ((Im t) ^2))) - (0 * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>)) + (s * t) is complex Element of COMPLEX
((((z * (((Re t) ^2) - ((Im t) ^2))) - (0 * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>)) + (s * t)) + n is complex Element of COMPLEX
(z * (((Re t) ^2) - ((Im t) ^2))) - 0 is complex real ext-real Element of REAL
- 0 is empty complex real ext-real non positive non negative V69() V70() V71() V72() V73() V74() V75() set
(z * (((Re t) ^2) - ((Im t) ^2))) + (- 0) is complex real ext-real set
(Re z) * ((2 * (Re t)) * (Im t)) is complex real ext-real Element of REAL
((Re z) * ((2 * (Re t)) * (Im t))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z)) is complex real ext-real Element of REAL
(((Re z) * ((2 * (Re t)) * (Im t))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i> is complex Element of COMPLEX
((z * (((Re t) ^2) - ((Im t) ^2))) - 0) + ((((Re z) * ((2 * (Re t)) * (Im t))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>) is complex Element of COMPLEX
(((z * (((Re t) ^2) - ((Im t) ^2))) - 0) + ((((Re z) * ((2 * (Re t)) * (Im t))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>)) + (s * t) is complex Element of COMPLEX
((((z * (((Re t) ^2) - ((Im t) ^2))) - 0) + ((((Re z) * ((2 * (Re t)) * (Im t))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>)) + (s * t)) + n is complex Element of COMPLEX
z * ((2 * (Re t)) * (Im t)) is complex real ext-real Element of REAL
(z * ((2 * (Re t)) * (Im t))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z)) is complex real ext-real Element of REAL
((z * ((2 * (Re t)) * (Im t))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i> is complex Element of COMPLEX
((z * (((Re t) ^2) - ((Im t) ^2))) - 0) + (((z * ((2 * (Re t)) * (Im t))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>) is complex Element of COMPLEX
(((z * (((Re t) ^2) - ((Im t) ^2))) - 0) + (((z * ((2 * (Re t)) * (Im t))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>)) + (s * t) is complex Element of COMPLEX
((((z * (((Re t) ^2) - ((Im t) ^2))) - 0) + (((z * ((2 * (Re t)) * (Im t))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>)) + (s * t)) + n is complex Element of COMPLEX
(((Re t) ^2) - ((Im t) ^2)) * (Im z) is complex real ext-real Element of REAL
(z * ((2 * (Re t)) * (Im t))) + ((((Re t) ^2) - ((Im t) ^2)) * (Im z)) is complex real ext-real Element of REAL
((z * ((2 * (Re t)) * (Im t))) + ((((Re t) ^2) - ((Im t) ^2)) * (Im z))) * <i> is complex Element of COMPLEX
((z * (((Re t) ^2) - ((Im t) ^2))) - 0) + (((z * ((2 * (Re t)) * (Im t))) + ((((Re t) ^2) - ((Im t) ^2)) * (Im z))) * <i>) is complex Element of COMPLEX
(((z * (((Re t) ^2) - ((Im t) ^2))) - 0) + (((z * ((2 * (Re t)) * (Im t))) + ((((Re t) ^2) - ((Im t) ^2)) * (Im z))) * <i>)) + (s * t) is complex Element of COMPLEX
((((z * (((Re t) ^2) - ((Im t) ^2))) - 0) + (((z * ((2 * (Re t)) * (Im t))) + ((((Re t) ^2) - ((Im t) ^2)) * (Im z))) * <i>)) + (s * t)) + n is complex Element of COMPLEX
(((Re t) ^2) - ((Im t) ^2)) * 0 is complex real ext-real Element of REAL
(z * ((2 * (Re t)) * (Im t))) + ((((Re t) ^2) - ((Im t) ^2)) * 0) is complex real ext-real Element of REAL
((z * ((2 * (Re t)) * (Im t))) + ((((Re t) ^2) - ((Im t) ^2)) * 0)) * <i> is complex Element of COMPLEX
((z * (((Re t) ^2) - ((Im t) ^2))) - 0) + (((z * ((2 * (Re t)) * (Im t))) + ((((Re t) ^2) - ((Im t) ^2)) * 0)) * <i>) is complex Element of COMPLEX
(((z * (((Re t) ^2) - ((Im t) ^2))) - 0) + (((z * ((2 * (Re t)) * (Im t))) + ((((Re t) ^2) - ((Im t) ^2)) * 0)) * <i>)) + (s * t) is complex Element of COMPLEX
((((z * (((Re t) ^2) - ((Im t) ^2))) - 0) + (((z * ((2 * (Re t)) * (Im t))) + ((((Re t) ^2) - ((Im t) ^2)) * 0)) * <i>)) + (s * t)) + n is complex Element of COMPLEX
0 * ((2 * (Re t)) * (Im t)) is complex real ext-real Element of REAL
(z * (((Re t) ^2) - ((Im t) ^2))) - (0 * ((2 * (Re t)) * (Im t))) is complex real ext-real Element of REAL
- (0 * ((2 * (Re t)) * (Im t))) is complex real ext-real set
(z * (((Re t) ^2) - ((Im t) ^2))) + (- (0 * ((2 * (Re t)) * (Im t)))) is complex real ext-real set
0 + (z * ((2 * (Re t)) * (Im t))) is complex real ext-real Element of REAL
(0 + (z * ((2 * (Re t)) * (Im t)))) * <i> is complex Element of COMPLEX
((z * (((Re t) ^2) - ((Im t) ^2))) - (0 * ((2 * (Re t)) * (Im t)))) + ((0 + (z * ((2 * (Re t)) * (Im t)))) * <i>) is complex Element of COMPLEX
s + (0 * <i>) is complex Element of COMPLEX
(s + (0 * <i>)) * ((Re t) + ((Im t) * <i>)) is complex Element of COMPLEX
(((z * (((Re t) ^2) - ((Im t) ^2))) - (0 * ((2 * (Re t)) * (Im t)))) + ((0 + (z * ((2 * (Re t)) * (Im t)))) * <i>)) + ((s + (0 * <i>)) * ((Re t) + ((Im t) * <i>))) is complex Element of COMPLEX
((((z * (((Re t) ^2) - ((Im t) ^2))) - (0 * ((2 * (Re t)) * (Im t)))) + ((0 + (z * ((2 * (Re t)) * (Im t)))) * <i>)) + ((s + (0 * <i>)) * ((Re t) + ((Im t) * <i>)))) + n is complex Element of COMPLEX
s * (Re t) is complex real ext-real Element of REAL
(z * (((Re t) ^2) - ((Im t) ^2))) + (s * (Re t)) is complex real ext-real Element of REAL
((z * (((Re t) ^2) - ((Im t) ^2))) + (s * (Re t))) + n is complex real ext-real Element of REAL
s * (Im t) is complex real ext-real Element of REAL
(z * ((2 * (Re t)) * (Im t))) + (s * (Im t)) is complex real ext-real Element of REAL
((z * ((2 * (Re t)) * (Im t))) + (s * (Im t))) * <i> is complex Element of COMPLEX
(((z * (((Re t) ^2) - ((Im t) ^2))) + (s * (Re t))) + n) + (((z * ((2 * (Re t)) * (Im t))) + (s * (Im t))) * <i>) is complex Element of COMPLEX
(2 * z) * (Re t) is complex real ext-real Element of REAL
((2 * z) * (Re t)) + s is complex real ext-real Element of REAL
(((2 * z) * (Re t)) + s) * (Im t) is complex real ext-real Element of REAL
Polynom (z,s,n,(Re t)) is complex real ext-real Element of REAL
(Re t) ^2 is complex real ext-real set
z * ((Re t) ^2) is complex real ext-real set
s * (Re t) is complex real ext-real set
(z * ((Re t) ^2)) + (s * (Re t)) is complex real ext-real set
((z * ((Re t) ^2)) + (s * (Re t))) + n is complex real ext-real set
(((- s) + (sqrt (delta (z,s,n)))) / (2 * z)) + (0 * <i>) is complex Element of COMPLEX
(((- s) - (sqrt (delta (z,s,n)))) / (2 * z)) + (0 * <i>) is complex Element of COMPLEX
(- s) / (2 * z) is complex real ext-real Element of REAL
(- s) * ((2 * z) ") is complex real ext-real set
(s / (2 * z)) ^2 is complex real ext-real Element of REAL
(s / (2 * z)) * (s / (2 * z)) is complex real ext-real set
((s / (2 * z)) ^2) - ((Im t) ^2) is complex real ext-real Element of REAL
((s / (2 * z)) ^2) + (- ((Im t) ^2)) is complex real ext-real set
z * (((s / (2 * z)) ^2) - ((Im t) ^2)) is complex real ext-real Element of REAL
s * (- (s / (2 * z))) is complex real ext-real Element of REAL
(z * (((s / (2 * z)) ^2) - ((Im t) ^2))) + (s * (- (s / (2 * z)))) is complex real ext-real Element of REAL
((z * (((s / (2 * z)) ^2) - ((Im t) ^2))) + (s * (- (s / (2 * z))))) + n is complex real ext-real Element of REAL
(s * (- (s / (2 * z)))) + n is complex real ext-real Element of REAL
- ((s * (- (s / (2 * z)))) + n) is complex real ext-real Element of REAL
(- ((s * (- (s / (2 * z)))) + n)) / z is complex real ext-real Element of REAL
z " is complex real ext-real set
(- ((s * (- (s / (2 * z)))) + n)) * (z ") is complex real ext-real set
((- ((s * (- (s / (2 * z)))) + n)) / z) - 0 is complex real ext-real Element of REAL
((- ((s * (- (s / (2 * z)))) + n)) / z) + (- 0) is complex real ext-real set
((s / (2 * z)) ^2) - ((- ((s * (- (s / (2 * z)))) + n)) / z) is complex real ext-real Element of REAL
- ((- ((s * (- (s / (2 * z)))) + n)) / z) is complex real ext-real set
((s / (2 * z)) ^2) + (- ((- ((s * (- (s / (2 * z)))) + n)) / z)) is complex real ext-real set
((Im t) ^2) - 0 is complex real ext-real Element of REAL
((Im t) ^2) + (- 0) is complex real ext-real set
z " is complex real ext-real Element of REAL
n * (z ") is complex real ext-real Element of REAL
((s / (2 * z)) ^2) + (n * (z ")) is complex real ext-real Element of REAL
s ^2 is complex real ext-real Element of REAL
(s ^2) / (2 * z) is complex real ext-real Element of REAL
(s ^2) * ((2 * z) ") is complex real ext-real set
((s ^2) / (2 * z)) * (z ") is complex real ext-real Element of REAL
(((s / (2 * z)) ^2) + (n * (z "))) - (((s ^2) / (2 * z)) * (z ")) is complex real ext-real Element of REAL
- (((s ^2) / (2 * z)) * (z ")) is complex real ext-real set
(((s / (2 * z)) ^2) + (n * (z "))) + (- (((s ^2) / (2 * z)) * (z "))) is complex real ext-real set
(2 * z) ^2 is complex real ext-real Element of REAL
(2 * z) * (2 * z) is complex real ext-real set
((Im t) ^2) * ((2 * z) ^2) is complex real ext-real Element of REAL
(s ^2) / ((2 * z) ^2) is complex real ext-real Element of REAL
((2 * z) ^2) " is complex real ext-real set
(s ^2) * (((2 * z) ^2) ") is complex real ext-real set
((s ^2) / ((2 * z) ^2)) + (n * (z ")) is complex real ext-real Element of REAL
(((s ^2) / ((2 * z) ^2)) + (n * (z "))) - (((s ^2) / (2 * z)) * (z ")) is complex real ext-real Element of REAL
(((s ^2) / ((2 * z) ^2)) + (n * (z "))) + (- (((s ^2) / (2 * z)) * (z "))) is complex real ext-real set
((((s ^2) / ((2 * z) ^2)) + (n * (z "))) - (((s ^2) / (2 * z)) * (z "))) * ((2 * z) ^2) is complex real ext-real Element of REAL
((s ^2) / ((2 * z) ^2)) * ((2 * z) ^2) is complex real ext-real Element of REAL
(n * (z ")) * ((2 * z) ^2) is complex real ext-real Element of REAL
(((s ^2) / ((2 * z) ^2)) * ((2 * z) ^2)) + ((n * (z ")) * ((2 * z) ^2)) is complex real ext-real Element of REAL
(2 * z) " is complex real ext-real Element of REAL
(s ^2) * ((2 * z) ") is complex real ext-real Element of REAL
((s ^2) * ((2 * z) ")) * (z ") is complex real ext-real Element of REAL
(((s ^2) * ((2 * z) ")) * (z ")) * ((2 * z) ^2) is complex real ext-real Element of REAL
((((s ^2) / ((2 * z) ^2)) * ((2 * z) ^2)) + ((n * (z ")) * ((2 * z) ^2))) - ((((s ^2) * ((2 * z) ")) * (z ")) * ((2 * z) ^2)) is complex real ext-real Element of REAL
- ((((s ^2) * ((2 * z) ")) * (z ")) * ((2 * z) ^2)) is complex real ext-real set
((((s ^2) / ((2 * z) ^2)) * ((2 * z) ^2)) + ((n * (z ")) * ((2 * z) ^2))) + (- ((((s ^2) * ((2 * z) ")) * (z ")) * ((2 * z) ^2))) is complex real ext-real set
(s ^2) + ((n * (z ")) * ((2 * z) ^2)) is complex real ext-real Element of REAL
((2 * z) ") * (z ") is complex real ext-real Element of REAL
(s ^2) * (((2 * z) ") * (z ")) is complex real ext-real Element of REAL
((s ^2) * (((2 * z) ") * (z "))) * ((2 * z) ^2) is complex real ext-real Element of REAL
((s ^2) + ((n * (z ")) * ((2 * z) ^2))) - (((s ^2) * (((2 * z) ") * (z "))) * ((2 * z) ^2)) is complex real ext-real Element of REAL
- (((s ^2) * (((2 * z) ") * (z "))) * ((2 * z) ^2)) is complex real ext-real set
((s ^2) + ((n * (z ")) * ((2 * z) ^2))) + (- (((s ^2) * (((2 * z) ") * (z "))) * ((2 * z) ^2))) is complex real ext-real set
(2 * z) * z is complex real ext-real Element of REAL
((2 * z) * z) " is complex real ext-real Element of REAL
(s ^2) * (((2 * z) * z) ") is complex real ext-real Element of REAL
((s ^2) * (((2 * z) * z) ")) * ((2 * z) ^2) is complex real ext-real Element of REAL
((s ^2) + ((n * (z ")) * ((2 * z) ^2))) - (((s ^2) * (((2 * z) * z) ")) * ((2 * z) ^2)) is complex real ext-real Element of REAL
- (((s ^2) * (((2 * z) * z) ")) * ((2 * z) ^2)) is complex real ext-real set
((s ^2) + ((n * (z ")) * ((2 * z) ^2))) + (- (((s ^2) * (((2 * z) * z) ")) * ((2 * z) ^2))) is complex real ext-real set
z * z is complex real ext-real Element of REAL
2 * (z * z) is complex real ext-real Element of REAL
(2 * (z * z)) " is complex real ext-real Element of REAL
(s ^2) * ((2 * (z * z)) ") is complex real ext-real Element of REAL
((s ^2) * ((2 * (z * z)) ")) * ((2 * z) ^2) is complex real ext-real Element of REAL
((s ^2) + ((n * (z ")) * ((2 * z) ^2))) - (((s ^2) * ((2 * (z * z)) ")) * ((2 * z) ^2)) is complex real ext-real Element of REAL
- (((s ^2) * ((2 * (z * z)) ")) * ((2 * z) ^2)) is complex real ext-real set
((s ^2) + ((n * (z ")) * ((2 * z) ^2))) + (- (((s ^2) * ((2 * (z * z)) ")) * ((2 * z) ^2))) is complex real ext-real set
((2 * z) ^2) " is complex real ext-real Element of REAL
(((s ^2) * ((2 * (z * z)) ")) * ((2 * z) ^2)) * (((2 * z) ^2) ") is complex real ext-real Element of REAL
1 / ((2 * z) ^2) is complex real ext-real Element of REAL
1 * (((2 * z) ^2) ") is complex real ext-real set
((2 * z) ^2) * (1 / ((2 * z) ^2)) is complex real ext-real Element of REAL
((s ^2) * ((2 * (z * z)) ")) * (((2 * z) ^2) * (1 / ((2 * z) ^2))) is complex real ext-real Element of REAL
((s ^2) * ((2 * (z * z)) ")) * 1 is complex real ext-real Element of REAL
2 " is non empty complex real ext-real positive non negative V44() Element of RAT
((((s ^2) * ((2 * (z * z)) ")) * ((2 * z) ^2)) * (((2 * z) ^2) ")) * (2 ") is complex real ext-real Element of REAL
z ^2 is complex real ext-real Element of REAL
z * z is complex real ext-real set
2 * (z ^2) is complex real ext-real Element of REAL
(2 * (z ^2)) " is complex real ext-real Element of REAL
(s ^2) * ((2 * (z ^2)) ") is complex real ext-real Element of REAL
((s ^2) * ((2 * (z ^2)) ")) * (2 ") is complex real ext-real Element of REAL
((2 * (z ^2)) ") * (2 ") is complex real ext-real Element of REAL
(s ^2) * (((2 * (z ^2)) ") * (2 ")) is complex real ext-real Element of REAL
(z ^2) * 2 is complex real ext-real Element of REAL
2 * ((z ^2) * 2) is complex real ext-real Element of REAL
(2 * ((z ^2) * 2)) " is complex real ext-real Element of REAL
(s ^2) * ((2 * ((z ^2) * 2)) ") is complex real ext-real Element of REAL
(((s ^2) * ((2 * (z * z)) ")) * ((2 * z) ^2)) * (2 ") is complex real ext-real Element of REAL
((((s ^2) * ((2 * (z * z)) ")) * ((2 * z) ^2)) * (2 ")) / ((2 * z) ^2) is complex real ext-real Element of REAL
((((s ^2) * ((2 * (z * z)) ")) * ((2 * z) ^2)) * (2 ")) * (((2 * z) ^2) ") is complex real ext-real set
(((((s ^2) * ((2 * (z * z)) ")) * ((2 * z) ^2)) * (2 ")) / ((2 * z) ^2)) * ((2 * z) ^2) is complex real ext-real Element of REAL
(((s ^2) * ((2 * (z * z)) ")) * ((2 * z) ^2)) / 2 is complex real ext-real Element of REAL
2 " is non empty complex real ext-real positive non negative set
(((s ^2) * ((2 * (z * z)) ")) * ((2 * z) ^2)) * (2 ") is complex real ext-real set
n / z is complex real ext-real Element of REAL
n * (z ") is complex real ext-real set
(n / z) * z is complex real ext-real Element of REAL
((n / z) * z) * 2 is complex real ext-real Element of REAL
(((n / z) * z) * 2) * (2 * z) is complex real ext-real Element of REAL
n * 2 is complex real ext-real Element of REAL
(n * 2) * (2 * z) is complex real ext-real Element of REAL
- (delta (z,s,n)) is complex real ext-real Element of REAL
(Im t) * (2 * z) is complex real ext-real Element of REAL
((Im t) * (2 * z)) ^2 is complex real ext-real Element of REAL
((Im t) * (2 * z)) * ((Im t) * (2 * z)) is complex real ext-real set
(- (s / (2 * z))) + (0 * <i>) is complex Element of COMPLEX
z is complex real ext-real Element of REAL
2 * z is complex real ext-real Element of REAL
s is complex real ext-real Element of REAL
s / (2 * z) is complex real ext-real Element of REAL
(2 * z) " is complex real ext-real set
s * ((2 * z) ") is complex real ext-real set
- (s / (2 * z)) is complex real ext-real Element of REAL
n is complex real ext-real Element of REAL
delta (z,s,n) is complex real ext-real Element of REAL
s ^2 is complex real ext-real set
s * s is complex real ext-real set
4 * z is complex real ext-real set
(4 * z) * n is complex real ext-real set
(s ^2) - ((4 * z) * n) is complex real ext-real set
- ((4 * z) * n) is complex real ext-real set
(s ^2) + (- ((4 * z) * n)) is complex real ext-real set
- (delta (z,s,n)) is complex real ext-real Element of REAL
sqrt (- (delta (z,s,n))) is complex real ext-real Element of REAL
(sqrt (- (delta (z,s,n)))) / (2 * z) is complex real ext-real Element of REAL
(sqrt (- (delta (z,s,n)))) * ((2 * z) ") is complex real ext-real set
((sqrt (- (delta (z,s,n)))) / (2 * z)) * <i> is complex Element of COMPLEX
(- (s / (2 * z))) + (((sqrt (- (delta (z,s,n)))) / (2 * z)) * <i>) is complex Element of COMPLEX
- ((sqrt (- (delta (z,s,n)))) / (2 * z)) is complex real ext-real Element of REAL
(- ((sqrt (- (delta (z,s,n)))) / (2 * z))) * <i> is complex Element of COMPLEX
(- (s / (2 * z))) + ((- ((sqrt (- (delta (z,s,n)))) / (2 * z))) * <i>) is complex Element of COMPLEX
t is complex Element of COMPLEX
(z,s,n,t) is complex Element of COMPLEX
t ^2 is complex set
t * t is complex set
z * (t ^2) is complex set
s * t is complex set
(z * (t ^2)) + (s * t) is complex set
((z * (t ^2)) + (s * t)) + n is complex set
0 * <i> is complex Element of COMPLEX
z + (0 * <i>) is complex Element of COMPLEX
s ^2 is complex real ext-real Element of REAL
- (s ^2) is complex real ext-real Element of REAL
n * z is complex real ext-real Element of REAL
(n * z) * 4 is complex real ext-real Element of REAL
(- (s ^2)) + ((n * z) * 4) is complex real ext-real Element of REAL
((- (s ^2)) + ((n * z) * 4)) / 4 is complex real ext-real Element of REAL
4 " is non empty complex real ext-real positive non negative set
((- (s ^2)) + ((n * z) * 4)) * (4 ") is complex real ext-real set
t is complex Element of COMPLEX
Re t is complex real ext-real Element of REAL
Im t is complex real ext-real Element of REAL
(Im t) * <i> is complex Element of COMPLEX
(Re t) + ((Im t) * <i>) is complex Element of COMPLEX
(z,s,n,t) is complex Element of COMPLEX
t ^2 is complex set
t * t is complex set
z * (t ^2) is complex set
s * t is complex set
(z * (t ^2)) + (s * t) is complex set
((z * (t ^2)) + (s * t)) + n is complex set
(Re t) ^2 is complex real ext-real Element of REAL
(Re t) * (Re t) is complex real ext-real set
(Im t) ^2 is complex real ext-real Element of REAL
(Im t) * (Im t) is complex real ext-real set
((Re t) ^2) - ((Im t) ^2) is complex real ext-real Element of REAL
- ((Im t) ^2) is complex real ext-real set
((Re t) ^2) + (- ((Im t) ^2)) is complex real ext-real set
2 * (Re t) is complex real ext-real Element of REAL
(2 * (Re t)) * (Im t) is complex real ext-real Element of REAL
((2 * (Re t)) * (Im t)) * <i> is complex Element of COMPLEX
(((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>) is complex Element of COMPLEX
(z + (0 * <i>)) * ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)) is complex Element of COMPLEX
s * t is complex Element of COMPLEX
((z + (0 * <i>)) * ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) + (s * t) is complex Element of COMPLEX
(((z + (0 * <i>)) * ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) + (s * t)) + n is complex Element of COMPLEX
Re z is complex real ext-real Element of REAL
Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)) is complex real ext-real Element of REAL
(Re z) * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) is complex real ext-real Element of REAL
Im z is complex real ext-real Element of REAL
Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)) is complex real ext-real Element of REAL
(Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) is complex real ext-real Element of REAL
((Re z) * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) is complex real ext-real Element of REAL
- ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) is complex real ext-real set
((Re z) * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + (- ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) is complex real ext-real set
(Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) is complex real ext-real Element of REAL
(Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z) is complex real ext-real Element of REAL
((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z)) is complex real ext-real Element of REAL
(((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i> is complex Element of COMPLEX
(((Re z) * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>) is complex Element of COMPLEX
((((Re z) * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>)) + (s * t) is complex Element of COMPLEX
(((((Re z) * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>)) + (s * t)) + n is complex Element of COMPLEX
z * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) is complex real ext-real Element of REAL
(z * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) is complex real ext-real Element of REAL
(z * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + (- ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) is complex real ext-real set
((z * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>) is complex Element of COMPLEX
(((z * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>)) + (s * t) is complex Element of COMPLEX
((((z * (Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>)) + (s * t)) + n is complex Element of COMPLEX
z * (((Re t) ^2) - ((Im t) ^2)) is complex real ext-real Element of REAL
(z * (((Re t) ^2) - ((Im t) ^2))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) is complex real ext-real Element of REAL
(z * (((Re t) ^2) - ((Im t) ^2))) + (- ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) is complex real ext-real set
((z * (((Re t) ^2) - ((Im t) ^2))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>) is complex Element of COMPLEX
(((z * (((Re t) ^2) - ((Im t) ^2))) - ((Im z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))))) + ((((Re z) * (Im ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>)))) + ((Re ((((Re t) ^2) - ((Im t) ^2)) + (((2 * (Re t)) * (Im t)) * <i>))) * (Im z))) * <i>)) + (s * t) is complex Element of