:: COMPLEX1 semantic presentation

REAL is non zero V33() V34() V35() V39() set
NAT is V33() V34() V35() V36() V37() V38() V39() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non zero V33() V39() set
0 is zero natural complex real ext-real non positive non negative V33() V34() V35() V36() V37() V38() V39() Element of NAT
sqrt 0 is complex real ext-real Element of REAL
1 is non zero natural complex real ext-real positive non negative V33() V34() V35() V36() V37() V38() Element of NAT
sqrt 1 is complex real ext-real Element of REAL
0 is zero V33() V34() V35() V36() V37() V38() V39() set
{0,1} is non zero set
Funcs ({0,1},REAL) is non zero FUNCTION_DOMAIN of {0,1}, REAL
{ b₁ where b₁ is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of Funcs ({0,1},REAL) : b₁ . 1 = 0 } is set
(Funcs ({0,1},REAL)) \ { b₁ where b₁ is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of Funcs ({0,1},REAL) : b₁ . 1 = 0 } is Element of K19((Funcs ({0,1},REAL)))
K19((Funcs ({0,1},REAL))) is set
K15(((Funcs ({0,1},REAL)) \ { b₁ where b₁ is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of Funcs ({0,1},REAL) : b₁ . 1 = 0 } ),REAL) is non zero set
<i> is complex set
(0,1) --> (0,1) is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of K19(K20({0,1},REAL))
{0,1} is non zero V33() V34() V35() V36() V37() V38() set
K20({0,1},REAL) is set
K19(K20({0,1},REAL)) is set
2 is non zero natural complex real ext-real positive non negative V33() V34() V35() V36() V37() V38() Element of NAT
a is complex real ext-real set
a ^2 is complex real ext-real set
a * a is complex real ext-real set
b is complex real ext-real set
b ^2 is complex real ext-real set
b * b is complex real ext-real set
(a ^2) + (b ^2) is complex real ext-real set
a is complex real ext-real set
a ^2 is complex real ext-real set
a * a is complex real ext-real set
b is complex real ext-real set
b ^2 is complex real ext-real set
b * b is complex real ext-real set
(a ^2) + (b ^2) is complex real ext-real set
a is complex set
K20(2,REAL) is set
K19(K20(2,REAL)) is set
Funcs (2,REAL) is non zero FUNCTION_DOMAIN of 2, REAL
{ b₁ where b₁ is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of Funcs (2,REAL) : b₁ . 1 = 0 } is set
(Funcs (2,REAL)) \ { b₁ where b₁ is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of Funcs (2,REAL) : b₁ . 1 = 0 } is Element of K19((Funcs (2,REAL)))
K19((Funcs (2,REAL))) is set
b is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of K19(K20(2,REAL))
b . 0 is set
b is set
c is set
i2 is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of K19(K20(2,REAL))
d is set
i2 . 0 is set
y2 is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of K19(K20(2,REAL))
i1 is set
y2 . 0 is set
Funcs (2,REAL) is non zero FUNCTION_DOMAIN of 2, REAL
{ b₁ where b₁ is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of Funcs (2,REAL) : b₁ . 1 = 0 } is set
(Funcs (2,REAL)) \ { b₁ where b₁ is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of Funcs (2,REAL) : b₁ . 1 = 0 } is Element of K19((Funcs (2,REAL)))
K19((Funcs (2,REAL))) is set
b is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of K19(K20(2,REAL))
b . 1 is set
b is set
c is set
i2 is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of K19(K20(2,REAL))
d is set
i2 . 1 is set
y2 is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of K19(K20(2,REAL))
i1 is set
y2 . 1 is set
a is complex set
(a) is set
b is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of K19(K20(2,REAL))
b . 0 is set
(a) is set
b is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of K19(K20(2,REAL))
b . 1 is set
a is complex set
(a) is complex real ext-real set
(a) is complex real ext-real set
a is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of K19(K20(2,REAL))
a . 0 is set
a . 1 is set
b is complex real ext-real Element of REAL
c is complex real ext-real Element of REAL
(0,1) --> (b,c) is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of K19(K20({0,1},REAL))
dom a is set
a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
[*a,b*] is complex Element of COMPLEX
([*a,b*]) is complex real ext-real Element of REAL
([*a,b*]) is complex real ext-real Element of REAL
c is complex real ext-real Element of REAL
d is complex real ext-real Element of REAL
(0,1) --> (c,d) is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of K19(K20({0,1},REAL))
i1 is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of K19(K20(2,REAL))
i1 . 0 is set
c is complex real ext-real Element of REAL
d is complex real ext-real Element of REAL
(0,1) --> (c,d) is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of K19(K20({0,1},REAL))
i1 is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of K19(K20(2,REAL))
i1 . 1 is set
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
[*(a),(a)*] is complex Element of COMPLEX
b is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of K19(K20(2,REAL))
b . 1 is set
b is complex real ext-real Element of REAL
c is complex real ext-real Element of REAL
(0,1) --> (b,c) is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of K19(K20({0,1},REAL))
Funcs (2,REAL) is non zero FUNCTION_DOMAIN of 2, REAL
{ b₁ where b₁ is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of Funcs (2,REAL) : b₁ . 1 = 0 } is set
(Funcs (2,REAL)) \ { b₁ where b₁ is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of Funcs (2,REAL) : b₁ . 1 = 0 } is Element of K19((Funcs (2,REAL)))
K19((Funcs (2,REAL))) is set
d is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of Funcs (2,REAL)
d . 1 is set
i1 is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of K19(K20(2,REAL))
i1 . 0 is set
i1 is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of K19(K20(2,REAL))
i1 . 1 is set
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
(b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
[*(b),(b)*] is complex Element of COMPLEX
a is complex set
b is complex set
(a) is complex real ext-real Element of REAL
(b) 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
() is complex Element of COMPLEX
[*0,0*] is complex Element of COMPLEX
[*1,0*] is complex Element of COMPLEX
(0) is complex real ext-real Element of REAL
(0) is complex real ext-real Element of REAL
a is complex set
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
(()) is complex real ext-real Element of REAL
(()) is complex real ext-real Element of REAL
() is complex Element of COMPLEX
[*0,1*] is complex Element of COMPLEX
(()) is complex real ext-real Element of REAL
(()) is complex real ext-real Element of REAL
a is complex real ext-real set
b is complex real ext-real Element of REAL
c is complex real ext-real Element of REAL
[*b,c*] is complex Element of COMPLEX
(0,1) --> (b,c) is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of K19(K20({0,1},REAL))
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 Element of REAL
c is complex real ext-real set
d is complex real ext-real set
c + d is complex real ext-real set
i1 is complex real ext-real Element of REAL
i2 is complex real ext-real Element of REAL
[*i1,i2*] is complex Element of COMPLEX
y2 is complex real ext-real Element of REAL
y2 is complex real ext-real Element of REAL
[*y2,y2*] is complex Element of COMPLEX
+ (i1,y2) is complex real ext-real Element of REAL
+ (i2,y2) is complex real ext-real Element of REAL
[*(+ (i1,y2)),(+ (i2,y2))*] is complex Element of COMPLEX
a is complex real ext-real Element of REAL
opp a is complex real ext-real Element of REAL
- a is complex real ext-real Element of REAL
+ (a,(opp a)) is complex real ext-real Element of REAL
a + (opp a) 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,b) is complex real ext-real Element of REAL
c is complex real ext-real set
d is complex real ext-real set
c * d is complex real ext-real set
i1 is complex real ext-real Element of REAL
i2 is complex real ext-real Element of REAL
[*i1,i2*] is complex Element of COMPLEX
y2 is complex real ext-real Element of REAL
y2 is complex real ext-real Element of REAL
[*y2,y2*] is complex Element of COMPLEX
* (i1,y2) is complex real ext-real Element of REAL
* (i2,y2) is complex real ext-real Element of REAL
opp (* (i2,y2)) is complex real ext-real Element of REAL
+ ((* (i1,y2)),(opp (* (i2,y2)))) is complex real ext-real Element of REAL
* (i1,y2) is complex real ext-real Element of REAL
* (i2,y2) is complex real ext-real Element of REAL
+ ((* (i1,y2)),(* (i2,y2))) is complex real ext-real Element of REAL
[*(+ ((* (i1,y2)),(opp (* (i2,y2))))),(+ ((* (i1,y2)),(* (i2,y2))))*] is complex Element of COMPLEX
opp i2 is complex real ext-real Element of REAL
* ((opp i2),y2) is complex real ext-real Element of REAL
+ ((* (i1,y2)),(* ((opp i2),y2))) is complex real ext-real Element of REAL
c is complex set
a is complex set
b is complex set
a + b is complex set
(c) 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) + (b) is complex real ext-real Element of REAL
d is complex real ext-real Element of REAL
i1 is complex real ext-real Element of REAL
[*d,i1*] is complex Element of COMPLEX
i2 is complex real ext-real Element of REAL
y2 is complex real ext-real Element of REAL
[*i2,y2*] is complex Element of COMPLEX
+ (d,i2) is complex real ext-real Element of REAL
+ (i1,y2) is complex real ext-real Element of REAL
[*(+ (d,i2)),(+ (i1,y2))*] is complex Element of COMPLEX
c is complex set
a is complex set
b is complex set
a + b is complex set
(c) 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) + (b) is complex real ext-real Element of REAL
d is complex real ext-real Element of REAL
i1 is complex real ext-real Element of REAL
[*d,i1*] is complex Element of COMPLEX
i2 is complex real ext-real Element of REAL
y2 is complex real ext-real Element of REAL
[*i2,y2*] is complex Element of COMPLEX
+ (d,i2) is complex real ext-real Element of REAL
+ (i1,y2) is complex real ext-real Element of REAL
[*(+ (d,i2)),(+ (i1,y2))*] is complex Element of COMPLEX
c is complex set
a is complex set
b is complex set
a * b is complex set
(c) 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) * (b) 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) * (b) is complex real ext-real Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL
d is complex real ext-real Element of REAL
i1 is complex real ext-real Element of REAL
[*d,i1*] is complex Element of COMPLEX
i2 is complex real ext-real Element of REAL
y2 is complex real ext-real Element of REAL
[*i2,y2*] is complex Element of COMPLEX
* (d,i2) is complex real ext-real Element of REAL
* (i1,y2) is complex real ext-real Element of REAL
opp (* (i1,y2)) is complex real ext-real Element of REAL
+ ((* (d,i2)),(opp (* (i1,y2)))) is complex real ext-real Element of REAL
* (d,y2) is complex real ext-real Element of REAL
* (i1,i2) is complex real ext-real Element of REAL
+ ((* (d,y2)),(* (i1,i2))) is complex real ext-real Element of REAL
[*(+ ((* (d,i2)),(opp (* (i1,y2))))),(+ ((* (d,y2)),(* (i1,i2))))*] is complex Element of COMPLEX
(* (d,i2)) + (opp (* (i1,y2))) is complex real ext-real Element of REAL
d * i2 is complex real ext-real Element of REAL
(d * i2) + (opp (* (i1,y2))) is complex real ext-real Element of REAL
- (* (i1,y2)) is complex real ext-real Element of REAL
(d * i2) + (- (* (i1,y2))) is complex real ext-real Element of REAL
(d * i2) - (* (i1,y2)) is complex real ext-real Element of REAL
c is complex set
a is complex set
b is complex set
a * b is complex set
(c) 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) * (b) 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) * (b) is complex real ext-real Element of REAL
((a) * (b)) + ((a) * (b)) is complex real ext-real Element of REAL
d is complex real ext-real Element of REAL
i1 is complex real ext-real Element of REAL
[*d,i1*] is complex Element of COMPLEX
i2 is complex real ext-real Element of REAL
y2 is complex real ext-real Element of REAL
[*i2,y2*] is complex Element of COMPLEX
* (d,i2) is complex real ext-real Element of REAL
* (i1,y2) is complex real ext-real Element of REAL
opp (* (i1,y2)) is complex real ext-real Element of REAL
+ ((* (d,i2)),(opp (* (i1,y2)))) is complex real ext-real Element of REAL
* (d,y2) is complex real ext-real Element of REAL
* (i1,i2) is complex real ext-real Element of REAL
+ ((* (d,y2)),(* (i1,i2))) is complex real ext-real Element of REAL
[*(+ ((* (d,i2)),(opp (* (i1,y2))))),(+ ((* (d,y2)),(* (i1,i2))))*] is complex Element of COMPLEX
(* (d,y2)) + (* (i1,i2)) is complex real ext-real Element of REAL
d * y2 is complex real ext-real Element of REAL
(d * y2) + (* (i1,i2)) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
a + b is complex set
(b) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL
[*((a) + (b)),((a) + (b))*] is complex Element of COMPLEX
([*((a) + (b)),((a) + (b))*]) is complex real ext-real Element of REAL
d is complex Element of COMPLEX
(d) is complex real ext-real Element of REAL
([*((a) + (b)),((a) + (b))*]) is complex real ext-real Element of REAL
(d) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
a * b is complex set
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
((a) * (b)) + ((b) * (a)) is complex real ext-real Element of REAL
[*(((a) * (b)) - ((a) * (b))),(((a) * (b)) + ((b) * (a)))*] is complex Element of COMPLEX
([*(((a) * (b)) - ((a) * (b))),(((a) * (b)) + ((b) * (a)))*]) is complex real ext-real Element of REAL
d is complex Element of COMPLEX
(d) is complex real ext-real Element of REAL
([*(((a) * (b)) - ((a) * (b))),(((a) * (b)) + ((b) * (a)))*]) is complex real ext-real Element of REAL
(d) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
a * b is complex set
((a * b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL
((a * b)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
((a) * (b)) + ((b) * (a)) is complex real ext-real Element of REAL
[*(((a) * (b)) - ((a) * (b))),(((a) * (b)) + ((b) * (a)))*] is complex Element of COMPLEX
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
a + b is complex set
((a + b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL
((a + b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL
[*((a) + (b)),((a) + (b))*] is complex Element of COMPLEX
a is complex real ext-real Element of REAL
a * () is complex set
((a * ())) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * (()) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * (()) is complex real ext-real Element of REAL
((a) * (())) - ((a) * (())) is complex real ext-real Element of REAL
(a) * 0 is complex real ext-real Element of REAL
0 * (()) is complex real ext-real Element of REAL
((a) * 0) - (0 * (())) is complex real ext-real Element of REAL
a is complex real ext-real Element of REAL
a * () is complex set
((a * ())) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * (()) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * (()) is complex real ext-real Element of REAL
((a) * (())) + ((a) * (())) 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,b*] is complex Element of COMPLEX
b * () is complex set
a + (b * ()) is complex set
((a + (b * ()))) 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) + ((b * ())) is complex real ext-real Element of REAL
0 + ((b * ())) is complex real ext-real Element of REAL
((a + (b * ()))) 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) + ((b * ())) is complex real ext-real Element of REAL
(a) + 0 is complex real ext-real Element of REAL
a is complex Element of COMPLEX
b is complex Element of COMPLEX
a + b is complex 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 Element of REAL
(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 Element of REAL
((a) + (b)) * () is complex set
((a) + (b)) + (((a) + (b)) * ()) is complex set
[*((a) + (b)),((a) + (b))*] is complex Element of COMPLEX
c is complex Element of COMPLEX
d is complex Element of COMPLEX
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
a + b is complex set
((a + b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL
((a + b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL
[*((a) + (b)),((a) + (b))*] is complex Element of COMPLEX
a is complex Element of COMPLEX
b is complex Element of COMPLEX
a * b is complex 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 Element of REAL
(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 Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
((a) * (b)) + ((b) * (a)) is complex real ext-real Element of REAL
(((a) * (b)) + ((b) * (a))) * () is complex set
(((a) * (b)) - ((a) * (b))) + ((((a) * (b)) + ((b) * (a))) * ()) is complex set
[*(((a) * (b)) - ((a) * (b))),(((a) * (b)) + ((b) * (a)))*] is complex Element of COMPLEX
c is complex Element of COMPLEX
d is complex Element of COMPLEX
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
a * b is complex set
((a * b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL
((a * b)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
((a) * (b)) + ((b) * (a)) is complex real ext-real Element of REAL
[*(((a) * (b)) - ((a) * (b))),(((a) * (b)) + ((b) * (a)))*] is complex Element of COMPLEX
a is complex real ext-real set
a * () is complex set
((a * ())) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * (()) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * (()) is complex real ext-real Element of REAL
((a) * (())) - ((a) * (())) is complex real ext-real Element of REAL
(a) * 0 is complex real ext-real Element of REAL
0 * (()) is complex real ext-real Element of REAL
((a) * 0) - (0 * (())) is complex real ext-real Element of REAL
a is complex real ext-real set
a * () is complex set
((a * ())) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * (()) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * (()) is complex real ext-real Element of REAL
((a) * (())) + ((a) * (())) is complex real ext-real Element of REAL
a is complex real ext-real set
b is complex real ext-real set
b * () is complex set
a + (b * ()) is complex set
((a + (b * ()))) is complex real ext-real Element of REAL
((a + (b * ()))) is complex real ext-real Element of REAL
c is complex real ext-real Element of REAL
d is complex real ext-real Element of REAL
d * () is complex set
c + (d * ()) is complex set
[*c,d*] is complex Element of COMPLEX
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) + ((a) * ()) is complex set
[*(a),(a)*] is complex Element of COMPLEX
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
(b) is complex real ext-real Element of REAL
a * b is complex set
((a * b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a * b)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
((a) * (b)) + ((b) * (a)) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
(b) is complex real ext-real Element of REAL
a * b is complex set
((a * b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
- ((a) * (b)) is complex real ext-real Element of REAL
((a * b)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
((a) * (b)) + ((b) * (a)) is complex real ext-real Element of REAL
a is complex set
a * a is complex set
((a * a)) is complex real ext-real Element of REAL
(a) 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) 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) ^2) - ((a) ^2) is complex real ext-real Element of REAL
((a * a)) is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real Element of REAL
2 * ((a) * (a)) is complex real ext-real Element of REAL
((a) * (a)) + ((a) * (a)) is complex real ext-real Element of REAL
a is complex Element of COMPLEX
- a is complex set
(a) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(- (a)) * () is complex set
(- (a)) + ((- (a)) * ()) is complex set
[*(- (a)),(- (a))*] is complex Element of COMPLEX
([*(- (a)),(- (a))*],a) is complex Element of COMPLEX
([*(- (a)),(- (a))*]) is complex real ext-real Element of REAL
([*(- (a)),(- (a))*]) + (a) is complex real ext-real Element of REAL
([*(- (a)),(- (a))*]) is complex real ext-real Element of REAL
([*(- (a)),(- (a))*]) + (a) is complex real ext-real Element of REAL
[*(([*(- (a)),(- (a))*]) + (a)),(([*(- (a)),(- (a))*]) + (a))*] is complex Element of COMPLEX
(- (a)) + (a) is complex real ext-real Element of REAL
[*((- (a)) + (a)),(([*(- (a)),(- (a))*]) + (a))*] is complex Element of COMPLEX
(- (a)) + (a) is complex real ext-real Element of REAL
[*0,((- (a)) + (a))*] is complex Element of COMPLEX
c is complex Element of COMPLEX
d is complex Element of COMPLEX
a is complex set
- a is complex set
((- a)) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
((- a)) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(- (a)) * () is complex set
(- (a)) + ((- (a)) * ()) is complex set
((),()) is complex Element of COMPLEX
(()) is complex Element of COMPLEX
a is complex Element of COMPLEX
b is complex Element of COMPLEX
a - b is complex 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 Element of REAL
(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 Element of REAL
((a) - (b)) * () is complex set
((a) - (b)) + (((a) - (b)) * ()) is complex set
(a) * () is complex set
(a) + ((a) * ()) is complex set
(b) is complex Element of COMPLEX
(a,(b)) is complex Element of COMPLEX
- (b) is complex real ext-real Element of REAL
- (b) is complex real ext-real Element of REAL
(- (b)) * () is complex set
(- (b)) + ((- (b)) * ()) is complex set
a + ((- (b)) + ((- (b)) * ())) is complex set
c is complex Element of COMPLEX
d is complex Element of COMPLEX
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
a - b is complex set
((a - b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) - (b) is complex real ext-real Element of REAL
((a - b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) - (b) is complex real ext-real Element of REAL
((a) - (b)) * () is complex set
((a) - (b)) + (((a) - (b)) * ()) is complex set
((((a) - (b)) + (((a) - (b)) * ()))) is complex real ext-real Element of REAL
((((a) - (b)) + (((a) - (b)) * ()))) is complex real ext-real Element of REAL
a is complex Element of COMPLEX
a " is complex set
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
(a) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(- (a)) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
((- (a)) / (((a) ^2) + ((a) ^2))) * () is complex set
((a) / (((a) ^2) + ((a) ^2))) + (((- (a)) / (((a) ^2) + ((a) ^2))) * ()) is complex set
c is complex Element of COMPLEX
d is complex Element of COMPLEX
b is complex Element of COMPLEX
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
((a) * (b)) + ((b) * (a)) is complex real ext-real Element of REAL
(a) / 1 is complex real ext-real Element of REAL
((a) / 1) * ((- (a)) / (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
((a) / (((a) ^2) + ((a) ^2))) * (a) is complex real ext-real Element of REAL
(((a) / 1) * ((- (a)) / (((a) ^2) + ((a) ^2)))) + (((a) / (((a) ^2) + ((a) ^2))) * (a)) is complex real ext-real Element of REAL
(a) * (- (a)) is complex real ext-real Element of REAL
1 * (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
((a) * (- (a))) / (1 * (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(((a) / (((a) ^2) + ((a) ^2))) * (a)) / 1 is complex real ext-real Element of REAL
(((a) * (- (a))) / (1 * (((a) ^2) + ((a) ^2)))) + ((((a) / (((a) ^2) + ((a) ^2))) * (a)) / 1) is complex real ext-real Element of REAL
(a) / 1 is complex real ext-real Element of REAL
((a) / 1) * (a) is complex real ext-real Element of REAL
(((a) / 1) * (a)) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
(((a) * (- (a))) / (1 * (((a) ^2) + ((a) ^2)))) + ((((a) / 1) * (a)) / (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real Element of REAL
- ((a) * (a)) is complex real ext-real Element of REAL
(- ((a) * (a))) + ((a) * (a)) is complex real ext-real Element of REAL
((- ((a) * (a))) + ((a) * (a))) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL
((a) / 1) * ((a) / (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(a) * ((- (a)) / (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(((a) / 1) * ((a) / (((a) ^2) + ((a) ^2)))) - ((a) * ((- (a)) / (((a) ^2) + ((a) ^2)))) is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real Element of REAL
((a) * (a)) / (1 * (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
((a) / 1) * ((- (a)) / (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(((a) * (a)) / (1 * (((a) ^2) + ((a) ^2)))) - (((a) / 1) * ((- (a)) / (((a) ^2) + ((a) ^2)))) is complex real ext-real Element of REAL
((a) ^2) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
(a) * (- (a)) is complex real ext-real Element of REAL
((a) * (- (a))) / (1 * (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(((a) ^2) / (((a) ^2) + ((a) ^2))) - (((a) * (- (a))) / (1 * (((a) ^2) + ((a) ^2)))) is complex real ext-real Element of REAL
- ((a) ^2) is complex real ext-real Element of REAL
(- ((a) ^2)) / (1 * (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(((a) ^2) / (((a) ^2) + ((a) ^2))) - ((- ((a) ^2)) / (1 * (((a) ^2) + ((a) ^2)))) is complex real ext-real Element of REAL
((a) ^2) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
- (((a) ^2) / (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(((a) ^2) / (((a) ^2) + ((a) ^2))) - (- (((a) ^2) / (((a) ^2) + ((a) ^2)))) is complex real ext-real Element of REAL
((a) ^2) / (1 * (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(((a) ^2) / (((a) ^2) + ((a) ^2))) + (((a) ^2) / (1 * (((a) ^2) + ((a) ^2)))) is complex real ext-real Element of REAL
(((a) ^2) + ((a) ^2)) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
(a,b) is complex Element of COMPLEX
[*(((a) * (b)) - ((a) * (b))),(((a) * (b)) + ((b) * (a)))*] is complex Element of COMPLEX
c is complex Element of COMPLEX
d is complex Element of COMPLEX
a is complex set
a " is complex set
((a ")) is complex real ext-real Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
(a) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
((a ")) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(- (a)) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
((- (a)) / (((a) ^2) + ((a) ^2))) * () is complex set
((a) / (((a) ^2) + ((a) ^2))) + (((- (a)) / (((a) ^2) + ((a) ^2))) * ()) is complex set
(()) is complex Element of COMPLEX
(()) ^2 is complex real ext-real Element of REAL
(()) * (()) is complex real ext-real set
(()) ^2 is complex real ext-real Element of REAL
(()) * (()) is complex real ext-real set
((()) ^2) + ((()) ^2) is complex real ext-real Element of REAL
(()) / (((()) ^2) + ((()) ^2)) is complex real ext-real Element of REAL
- (()) is complex real ext-real Element of REAL
(- (())) / (((()) ^2) + ((()) ^2)) is complex real ext-real Element of REAL
((- (())) / (((()) ^2) + ((()) ^2))) * () is complex set
((()) / (((()) ^2) + ((()) ^2))) + (((- (())) / (((()) ^2) + ((()) ^2))) * ()) is complex set
(()) is complex Element of COMPLEX
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
a " is complex set
((a ")) is complex real ext-real Element of REAL
(a) " is complex real ext-real Element of REAL
((a ")) 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) ^2 is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real set
((a) ^2) + ((a) ^2) is complex real ext-real Element of REAL
(a) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
1 * (a) is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real Element of REAL
(1 * (a)) / ((a) * (a)) is complex real ext-real Element of REAL
1 / (a) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(- (a)) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
a " is complex set
((a ")) is complex real ext-real Element of REAL
((a ")) is complex real ext-real Element of REAL
(a) " is complex real ext-real Element of REAL
- ((a) ") 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) ^2 is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real set
((a) ^2) + ((a) ^2) is complex real ext-real Element of REAL
(a) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(- (a)) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
1 * (a) is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real Element of REAL
(1 * (a)) / ((a) * (a)) is complex real ext-real Element of REAL
- ((1 * (a)) / ((a) * (a))) is complex real ext-real Element of REAL
1 / (a) is complex real ext-real Element of REAL
- (1 / (a)) is complex real ext-real Element of REAL
a is complex set
b is complex set
a / b is complex 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 Element of REAL
(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 Element of REAL
((a) * (b)) + ((a) * (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
(b) ^2 is complex real ext-real Element of REAL
(b) * (b) is complex real ext-real set
((b) ^2) + ((b) ^2) is complex real ext-real Element of REAL
(((a) * (b)) + ((a) * (b))) / (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((b) * (a)) - ((a) * (b)) is complex real ext-real Element of REAL
(((b) * (a)) - ((a) * (b))) / (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
((((b) * (a)) - ((a) * (b))) / (((b) ^2) + ((b) ^2))) * () is complex set
((((a) * (b)) + ((a) * (b))) / (((b) ^2) + ((b) ^2))) + (((((b) * (a)) - ((a) * (b))) / (((b) ^2) + ((b) ^2))) * ()) is complex set
d is complex Element of COMPLEX
(d) is complex real ext-real Element of REAL
(d) ^2 is complex real ext-real Element of REAL
(d) * (d) is complex real ext-real set
(d) is complex real ext-real Element of REAL
(d) ^2 is complex real ext-real Element of REAL
(d) * (d) is complex real ext-real set
((d) ^2) + ((d) ^2) is complex real ext-real Element of REAL
(d) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
- (d) is complex real ext-real Element of REAL
(- (d)) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
[*((d) / (((d) ^2) + ((d) ^2))),((- (d)) / (((d) ^2) + ((d) ^2)))*] is complex Element of COMPLEX
([*((d) / (((d) ^2) + ((d) ^2))),((- (d)) / (((d) ^2) + ((d) ^2)))*]) is complex real ext-real Element of REAL
((- (d)) / (((d) ^2) + ((d) ^2))) * () is complex set
((d) / (((d) ^2) + ((d) ^2))) + (((- (d)) / (((d) ^2) + ((d) ^2))) * ()) is complex set
((((d) / (((d) ^2) + ((d) ^2))) + (((- (d)) / (((d) ^2) + ((d) ^2))) * ()))) is complex real ext-real Element of REAL
([*((d) / (((d) ^2) + ((d) ^2))),((- (d)) / (((d) ^2) + ((d) ^2)))*]) is complex real ext-real Element of REAL
((((d) / (((d) ^2) + ((d) ^2))) + (((- (d)) / (((d) ^2) + ((d) ^2))) * ()))) is complex real ext-real Element of REAL
c is complex Element of COMPLEX
c / d is complex set
(d) is complex Element of COMPLEX
(c,(d)) is complex Element of COMPLEX
(c,[*((d) / (((d) ^2) + ((d) ^2))),((- (d)) / (((d) ^2) + ((d) ^2)))*]) is complex Element of COMPLEX
(c) is complex real ext-real Element of REAL
(c) / 1 is complex real ext-real Element of REAL
((c) / 1) * ((d) / (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
(c) is complex real ext-real Element of REAL
(c) * ((- (d)) / (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
(((c) / 1) * ((d) / (((d) ^2) + ((d) ^2)))) - ((c) * ((- (d)) / (((d) ^2) + ((d) ^2)))) is complex real ext-real Element of REAL
(c) * ((- (d)) / (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
((d) / (((d) ^2) + ((d) ^2))) * (c) is complex real ext-real Element of REAL
((c) * ((- (d)) / (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * (c)) is complex real ext-real Element of REAL
[*((((c) / 1) * ((d) / (((d) ^2) + ((d) ^2)))) - ((c) * ((- (d)) / (((d) ^2) + ((d) ^2))))),(((c) * ((- (d)) / (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * (c)))*] is complex Element of COMPLEX
(((c) * ((- (d)) / (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * (c))) * () is complex set
((((c) / 1) * ((d) / (((d) ^2) + ((d) ^2)))) - ((c) * ((- (d)) / (((d) ^2) + ((d) ^2))))) + ((((c) * ((- (d)) / (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * (c))) * ()) is complex set
(c) * (d) is complex real ext-real Element of REAL
1 * (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
((c) * (d)) / (1 * (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
(c) / 1 is complex real ext-real Element of REAL
((c) / 1) * ((- (d)) / (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
(((c) * (d)) / (1 * (((d) ^2) + ((d) ^2)))) - (((c) / 1) * ((- (d)) / (((d) ^2) + ((d) ^2)))) is complex real ext-real Element of REAL
((((c) * (d)) / (1 * (((d) ^2) + ((d) ^2)))) - (((c) / 1) * ((- (d)) / (((d) ^2) + ((d) ^2))))) + ((((c) * ((- (d)) / (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * (c))) * ()) is complex set
((c) * (d)) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
(c) * (- (d)) is complex real ext-real Element of REAL
((c) * (- (d))) / (1 * (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
(((c) * (d)) / (((d) ^2) + ((d) ^2))) - (((c) * (- (d))) / (1 * (((d) ^2) + ((d) ^2)))) is complex real ext-real Element of REAL
((c) / 1) * ((- (d)) / (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
(((c) / 1) * ((- (d)) / (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * (c)) is complex real ext-real Element of REAL
((((c) / 1) * ((- (d)) / (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * (c))) * () is complex set
((((c) * (d)) / (((d) ^2) + ((d) ^2))) - (((c) * (- (d))) / (1 * (((d) ^2) + ((d) ^2))))) + (((((c) / 1) * ((- (d)) / (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * (c))) * ()) is complex set
((c) * (- (d))) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
(((c) * (d)) / (((d) ^2) + ((d) ^2))) - (((c) * (- (d))) / (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
(c) * (- (d)) is complex real ext-real Element of REAL
((c) * (- (d))) / (1 * (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
((d) / (((d) ^2) + ((d) ^2))) * ((c) / 1) is complex real ext-real Element of REAL
(((c) * (- (d))) / (1 * (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * ((c) / 1)) is complex real ext-real Element of REAL
((((c) * (- (d))) / (1 * (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * ((c) / 1))) * () is complex set
((((c) * (d)) / (((d) ^2) + ((d) ^2))) - (((c) * (- (d))) / (((d) ^2) + ((d) ^2)))) + (((((c) * (- (d))) / (1 * (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * ((c) / 1))) * ()) is complex set
((c) * (- (d))) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
(c) * (d) is complex real ext-real Element of REAL
((c) * (d)) / (1 * (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
(((c) * (- (d))) / (((d) ^2) + ((d) ^2))) + (((c) * (d)) / (1 * (((d) ^2) + ((d) ^2)))) is complex real ext-real Element of REAL
((((c) * (- (d))) / (((d) ^2) + ((d) ^2))) + (((c) * (d)) / (1 * (((d) ^2) + ((d) ^2))))) * () is complex set
((((c) * (d)) / (((d) ^2) + ((d) ^2))) - (((c) * (- (d))) / (((d) ^2) + ((d) ^2)))) + (((((c) * (- (d))) / (((d) ^2) + ((d) ^2))) + (((c) * (d)) / (1 * (((d) ^2) + ((d) ^2))))) * ()) is complex set
((c) * (d)) - ((c) * (- (d))) is complex real ext-real Element of REAL
(((c) * (d)) - ((c) * (- (d)))) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
((((c) * (d)) - ((c) * (- (d)))) / (((d) ^2) + ((d) ^2))) + (((((c) * (- (d))) / (((d) ^2) + ((d) ^2))) + (((c) * (d)) / (1 * (((d) ^2) + ((d) ^2))))) * ()) is complex set
(c) * (d) is complex real ext-real Element of REAL
((c) * (d)) + ((c) * (d)) is complex real ext-real Element of REAL
(((c) * (d)) + ((c) * (d))) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
(c) * (d) is complex real ext-real Element of REAL
- ((c) * (d)) is complex real ext-real Element of REAL
(- ((c) * (d))) + ((c) * (d)) is complex real ext-real Element of REAL
((- ((c) * (d))) + ((c) * (d))) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
(((- ((c) * (d))) + ((c) * (d))) / (((d) ^2) + ((d) ^2))) * () is complex set
((((c) * (d)) + ((c) * (d))) / (((d) ^2) + ((d) ^2))) + ((((- ((c) * (d))) + ((c) * (d))) / (((d) ^2) + ((d) ^2))) * ()) is complex set
(d) * (c) is complex real ext-real Element of REAL
((d) * (c)) - ((c) * (d)) is complex real ext-real Element of REAL
(((d) * (c)) - ((c) * (d))) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
((((d) * (c)) - ((c) * (d))) / (((d) ^2) + ((d) ^2))) * () is complex set
((((c) * (d)) + ((c) * (d))) / (((d) ^2) + ((d) ^2))) + (((((d) * (c)) - ((c) * (d))) / (((d) ^2) + ((d) ^2))) * ()) is complex set
i2 is complex Element of COMPLEX
y2 is complex Element of COMPLEX
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
(a,b) is complex Element of COMPLEX
((a,b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) + ((a) * (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
(b) ^2 is complex real ext-real Element of REAL
(b) * (b) is complex real ext-real set
((b) ^2) + ((b) ^2) is complex real ext-real Element of REAL
((((a) * (b)) + ((a) * (b))),(((b) ^2) + ((b) ^2))) is complex real ext-real Element of COMPLEX
((a,b)) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((b) * (a)) - ((a) * (b)) is complex real ext-real Element of REAL
((((b) * (a)) - ((a) * (b))),(((b) ^2) + ((b) ^2))) is complex real ext-real Element of COMPLEX
(((((b) * (a)) - ((a) * (b))),(((b) ^2) + ((b) ^2))),()) is complex Element of COMPLEX
(((((a) * (b)) + ((a) * (b))),(((b) ^2) + ((b) ^2))),(((((b) * (a)) - ((a) * (b))),(((b) ^2) + ((b) ^2))),())) is complex Element of COMPLEX
((((((a) * (b)) + ((a) * (b))),(((b) ^2) + ((b) ^2))),(((((b) * (a)) - ((a) * (b))),(((b) ^2) + ((b) ^2))),()))) is complex real ext-real Element of REAL
((((((a) * (b)) + ((a) * (b))),(((b) ^2) + ((b) ^2))),(((((b) * (a)) - ((a) * (b))),(((b) ^2) + ((b) ^2))),()))) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
(b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a,b) is complex Element of COMPLEX
((a,b)) is complex real ext-real Element of REAL
((a),(b)) is complex real ext-real Element of COMPLEX
((a,b)) is complex real ext-real Element of REAL
b " is complex set
a * (b ") is complex set
((b ")) is complex real ext-real Element of REAL
((b ")) is complex real ext-real Element of REAL
(a) * ((b ")) is complex real ext-real Element of REAL
(b) " is complex real ext-real Element of REAL
(a) * ((b) ") is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
(b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a,b) is complex Element of COMPLEX
((a,b)) is complex real ext-real Element of REAL
((a),(b)) is complex real ext-real Element of COMPLEX
((a,b)) is complex real ext-real Element of REAL
b " is complex set
a * (b ") is complex set
((b ")) is complex real ext-real Element of REAL
((b ")) is complex real ext-real Element of REAL
(a) * ((b ")) is complex real ext-real Element of REAL
- ((a) * ((b "))) is complex real ext-real Element of REAL
(b) " is complex real ext-real Element of REAL
- ((b) ") is complex real ext-real Element of REAL
(a) * (- ((b) ")) is complex real ext-real Element of REAL
- ((a) * (- ((b) "))) is complex real ext-real Element of REAL
(a) * ((b) ") is complex real ext-real Element of REAL
- ((a) * ((b) ")) is complex real ext-real Element of REAL
- (- ((a) * ((b) "))) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
b is complex set
c is complex set
(c) is complex real ext-real Element of REAL
(c) is complex real ext-real Element of REAL
(c) * () is complex set
(c) - ((c) * ()) is complex set
(b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(b) * () is complex set
(b) - ((b) * ()) is complex set
- (c) is complex real ext-real Element of REAL
(- (c)) * () is complex set
(c) + ((- (c)) * ()) is complex set
- (b) is complex real ext-real Element of REAL
- (- (c)) is complex real ext-real Element of REAL
(- (b)) * () is complex set
(b) + ((- (b)) * ()) is complex set
a is complex set
(a) is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
a is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
((a)) is complex real ext-real Element of REAL
((a)) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(- (a)) * () is complex set
(a) + ((- (a)) * ()) is complex set
(0) is complex Element of COMPLEX
(0) * () is complex set
(0) - ((0) * ()) is complex set
a is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
- (a) is complex real ext-real Element of REAL
(- (a)) * () is complex set
(a) + ((- (a)) * ()) is complex set
(()) is complex Element of COMPLEX
(()) * () is complex set
(()) - ((()) * ()) is complex set
(()) is complex Element of COMPLEX
(()) * () is complex set
(()) - ((()) * ()) is complex set
a is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
b is complex set
a + b is complex set
((a + b)) is complex Element of COMPLEX
((a + b)) is complex real ext-real Element of REAL
((a + b)) is complex real ext-real Element of REAL
((a + b)) * () is complex set
((a + b)) - (((a + b)) * ()) is complex set
(b) is complex Element of COMPLEX
(b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(b) * () is complex set
(b) - ((b) * ()) is complex set
((a),(b)) is complex Element of COMPLEX
(((a + b))) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL
((a)) is complex real ext-real Element of REAL
((a)) + (b) is complex real ext-real Element of REAL
((b)) is complex real ext-real Element of REAL
((a)) + ((b)) is complex real ext-real Element of REAL
(((a),(b))) is complex real ext-real Element of REAL
(((a + b))) is complex real ext-real Element of REAL
(((a),(b))) is complex real ext-real Element of REAL
- ((a + b)) is complex real ext-real Element of REAL
- (b) is complex real ext-real Element of REAL
- (- (b)) is complex real ext-real Element of REAL
(a) + (- (- (b))) is complex real ext-real Element of REAL
- ((a) + (- (- (b)))) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(- (a)) + (- (b)) is complex real ext-real Element of REAL
((a)) is complex real ext-real Element of REAL
((a)) + (- (b)) is complex real ext-real Element of REAL
((b)) is complex real ext-real Element of REAL
((a)) + ((b)) is complex real ext-real Element of REAL
a is complex set
- a is complex set
((- a)) is complex Element of COMPLEX
((- a)) is complex real ext-real Element of REAL
((- a)) is complex real ext-real Element of REAL
((- a)) * () is complex set
((- a)) - (((- a)) * ()) is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
((a)) is complex Element of COMPLEX
(((- a))) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
((a)) is complex real ext-real Element of REAL
- ((a)) is complex real ext-real Element of REAL
(((a))) is complex real ext-real Element of REAL
(((- a))) is complex real ext-real Element of REAL
(((a))) is complex real ext-real Element of REAL
- ((- a)) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
- (- (a)) is complex real ext-real Element of REAL
((a)) is complex real ext-real Element of REAL
- ((a)) is complex real ext-real Element of REAL
a is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
b is complex set
a - b is complex set
((a - b)) is complex Element of COMPLEX
((a - b)) is complex real ext-real Element of REAL
((a - b)) is complex real ext-real Element of REAL
((a - b)) * () is complex set
((a - b)) - (((a - b)) * ()) is complex set
(b) is complex Element of COMPLEX
(b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(b) * () is complex set
(b) - ((b) * ()) is complex set
((a),(b)) is complex Element of COMPLEX
- b is complex set
a + (- b) is complex set
((a + (- b))) is complex Element of COMPLEX
((a + (- b))) is complex real ext-real Element of REAL
((a + (- b))) is complex real ext-real Element of REAL
((a + (- b))) * () is complex set
((a + (- b))) - (((a + (- b))) * ()) is complex set
((- b)) is complex Element of COMPLEX
((- b)) is complex real ext-real Element of REAL
((- b)) is complex real ext-real Element of REAL
((- b)) * () is complex set
((- b)) - (((- b)) * ()) is complex set
((a),((- b))) is complex Element of COMPLEX
((b)) is complex Element of COMPLEX
((a),((b))) is complex Element of COMPLEX
a is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
b is complex set
a * b is complex set
((a * b)) is complex Element of COMPLEX
((a * b)) is complex real ext-real Element of REAL
((a * b)) is complex real ext-real Element of REAL
((a * b)) * () is complex set
((a * b)) - (((a * b)) * ()) is complex set
(b) is complex Element of COMPLEX
(b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(b) * () is complex set
(b) - ((b) * ()) is complex set
((a),(b)) is complex Element of COMPLEX
((a)) is complex real ext-real Element of REAL
((b)) is complex real ext-real Element of REAL
((a)) 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
- (b) is complex real ext-real Element of REAL
(((a * b))) is complex real ext-real Element of REAL
((a)) * ((b)) 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))) * (- ((b))) is complex real ext-real Element of REAL
(((a)) * ((b))) - ((- ((a))) * (- ((b)))) is complex real ext-real Element of REAL
((a)) * ((b)) is complex real ext-real Element of REAL
- (((a)) * ((b))) is complex real ext-real Element of REAL
- (- (((a)) * ((b)))) is complex real ext-real Element of REAL
(((a)) * ((b))) - (- (- (((a)) * ((b))))) is complex real ext-real Element of REAL
(((a),(b))) is complex real ext-real Element of REAL
(((a * b))) is complex real ext-real Element of REAL
(((a),(b))) is complex real ext-real Element of REAL
- ((a * b)) is complex real ext-real Element of REAL
((a)) * (- ((b))) is complex real ext-real Element of REAL
((b)) * (- ((a))) is complex real ext-real Element of REAL
(((a)) * (- ((b)))) + (((b)) * (- ((a)))) is complex real ext-real Element of REAL
- ((((a)) * (- ((b)))) + (((b)) * (- ((a))))) is complex real ext-real Element of REAL
((b)) * ((a)) is complex real ext-real Element of REAL
((a)) * ((b)) is complex real ext-real Element of REAL
- (((a)) * ((b))) is complex real ext-real Element of REAL
- (- (((a)) * ((b)))) is complex real ext-real Element of REAL
(((b)) * ((a))) + (- (- (((a)) * ((b))))) is complex real ext-real Element of REAL
a is complex set
a " is complex set
((a ")) is complex Element of COMPLEX
((a ")) is complex real ext-real Element of REAL
((a ")) is complex real ext-real Element of REAL
((a ")) * () is complex set
((a ")) - (((a ")) * ()) is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
((a)) is complex Element of COMPLEX
((a)) 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)) 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)) ^2) + (((a)) ^2) is complex real ext-real Element of REAL
((a)) / ((((a)) ^2) + (((a)) ^2)) is complex real ext-real Element of REAL
- ((a)) is complex real ext-real Element of REAL
(- ((a))) / ((((a)) ^2) + (((a)) ^2)) is complex real ext-real Element of REAL
((- ((a))) / ((((a)) ^2) + (((a)) ^2))) * () is complex set
(((a)) / ((((a)) ^2) + (((a)) ^2))) + (((- ((a))) / ((((a)) ^2) + (((a)) ^2))) * ()) is complex set
- (a) is complex real ext-real Element of REAL
(((a "))) 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) ^2 is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real set
((a) ^2) + ((a) ^2) is complex real ext-real Element of REAL
((a),(((a) ^2) + ((a) ^2))) is complex real ext-real Element of COMPLEX
(((a))) is complex real ext-real Element of REAL
(((a "))) is complex real ext-real Element of REAL
(((a))) is complex real ext-real Element of REAL
- ((a ")) is complex real ext-real Element of REAL
((- (a)),(((a) ^2) + ((a) ^2))) is complex real ext-real Element of COMPLEX
(((- (a)),(((a) ^2) + ((a) ^2)))) is complex real ext-real Element of COMPLEX
((- ((a))),((((a)) ^2) + (((a)) ^2))) is complex real ext-real Element of COMPLEX
a is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
b is complex set
(a,b) is complex Element of COMPLEX
((a,b)) is complex Element of COMPLEX
((a,b)) is complex real ext-real Element of REAL
((a,b)) is complex real ext-real Element of REAL
((a,b)) * () is complex set
((a,b)) - (((a,b)) * ()) is complex set
(b) is complex Element of COMPLEX
(b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(b) * () is complex set
(b) - ((b) * ()) is complex set
((a),(b)) is complex Element of COMPLEX
b " is complex set
a * (b ") is complex set
((a * (b "))) is complex Element of COMPLEX
((a * (b "))) is complex real ext-real Element of REAL
((a * (b "))) is complex real ext-real Element of REAL
((a * (b "))) * () is complex set
((a * (b "))) - (((a * (b "))) * ()) is complex set
((b ")) is complex Element of COMPLEX
((b ")) is complex real ext-real Element of REAL
((b ")) is complex real ext-real Element of REAL
((b ")) * () is complex set
((b ")) - (((b ")) * ()) is complex set
((a),((b "))) is complex Element of COMPLEX
((b)) is complex Element of COMPLEX
((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
((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
(((b)) ^2) + (((b)) ^2) is complex real ext-real Element of REAL
((b)) / ((((b)) ^2) + (((b)) ^2)) is complex real ext-real Element of REAL
- ((b)) is complex real ext-real Element of REAL
(- ((b))) / ((((b)) ^2) + (((b)) ^2)) is complex real ext-real Element of REAL
((- ((b))) / ((((b)) ^2) + (((b)) ^2))) * () is complex set
(((b)) / ((((b)) ^2) + (((b)) ^2))) + (((- ((b))) / ((((b)) ^2) + (((b)) ^2))) * ()) is complex set
((a),((b))) is complex Element of COMPLEX
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
((a)) is complex real ext-real Element of REAL
((a)) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
- a is complex set
- 0 is zero complex real ext-real non positive non negative V33() V34() V35() V36() V37() V38() V39() Element of REAL
- (a) is complex real ext-real Element of REAL
(- (a)) * () is complex set
(- 0) + ((- (a)) * ()) is complex set
a is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
a * (a) is complex set
((a * (a))) 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) ^2 is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real set
((a) ^2) + ((a) ^2) is complex real ext-real Element of REAL
((a * (a))) is complex real ext-real Element of REAL
((a)) is complex real ext-real Element of REAL
(a) * ((a)) is complex real ext-real Element of REAL
((a)) is complex real ext-real Element of REAL
(a) * ((a)) is complex real ext-real Element of REAL
((a) * ((a))) - ((a) * ((a))) is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real Element of REAL
((a) * (a)) - ((a) * ((a))) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(a) * (- (a)) is complex real ext-real Element of REAL
((a) * (a)) - ((a) * (- (a))) is complex real ext-real Element of REAL
(a) * ((a)) is complex real ext-real Element of REAL
((a)) * (a) is complex real ext-real Element of REAL
((a) * ((a))) + (((a)) * (a)) is complex real ext-real Element of REAL
(a) * (- (a)) is complex real ext-real Element of REAL
((a) * (- (a))) + (((a)) * (a)) is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real Element of REAL
- ((a) * (a)) is complex real ext-real Element of REAL
(- ((a) * (a))) + ((a) * (a)) is complex real ext-real Element of REAL
a is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
a + (a) is complex set
((a + (a))) is complex real ext-real Element of REAL
2 * (a) is complex real ext-real Element of REAL
((a + (a))) is complex real ext-real Element of REAL
((a)) is complex real ext-real Element of REAL
(a) + ((a)) is complex real ext-real Element of REAL
(a) + (a) is complex real ext-real Element of REAL
((a)) is complex real ext-real Element of REAL
(a) + ((a)) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(a) + (- (a)) is complex real ext-real Element of REAL
a is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
a - (a) is complex set
((a - (a))) is complex real ext-real Element of REAL
((a - (a))) is complex real ext-real Element of REAL
2 * (a) is complex real ext-real Element of REAL
((a)) is complex real ext-real Element of REAL
(a) - ((a)) is complex real ext-real Element of REAL
(a) - (a) is complex real ext-real Element of REAL
((a)) is complex real ext-real Element of REAL
(a) - ((a)) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(a) - (- (a)) is complex real ext-real Element of REAL
a is complex set
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
b 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
(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
((b) ^2) + ((b) ^2) is complex real ext-real Element of REAL
sqrt (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
c is complex set
(c) is complex real ext-real Element of REAL
(c) ^2 is complex real ext-real Element of REAL
(c) * (c) is complex real ext-real set
(c) is complex real ext-real Element of REAL
(c) ^2 is complex real ext-real Element of REAL
(c) * (c) is complex real ext-real set
((c) ^2) + ((c) ^2) is complex real ext-real Element of REAL
sqrt (((c) ^2) + ((c) ^2)) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real set
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
a is complex real ext-real set
(a) is complex real ext-real Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
(0) is complex real ext-real Element of REAL
(0) ^2 is complex real ext-real Element of REAL
(0) * (0) is complex real ext-real set
(0) ^2 is complex real ext-real Element of REAL
(0) * (0) is complex real ext-real set
((0) ^2) + ((0) ^2) is complex real ext-real Element of REAL
sqrt (((0) ^2) + ((0) ^2)) is complex real ext-real Element of REAL
a is non zero complex set
(a) is complex real ext-real Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
b is complex set
(b) is complex real ext-real non negative Element of REAL
(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
(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
((b) ^2) + ((b) ^2) is complex real ext-real Element of REAL
sqrt (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
(()) is complex real ext-real non negative Element of REAL
(()) ^2 is complex real ext-real Element of REAL
(()) * (()) is complex real ext-real set
(()) ^2 is complex real ext-real Element of REAL
(()) * (()) is complex real ext-real set
((()) ^2) + ((()) ^2) is complex real ext-real Element of REAL
sqrt (((()) ^2) + ((()) ^2)) is complex real ext-real Element of REAL
(()) is complex real ext-real non negative Element of REAL
sqrt (((()) ^2) + ((()) ^2)) is complex real ext-real Element of REAL
a is complex set
- a is complex set
((- a)) is complex real ext-real non negative Element of REAL
((- a)) 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)) 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)) ^2) + (((- a)) ^2) is complex real ext-real Element of REAL
sqrt ((((- a)) ^2) + (((- a)) ^2)) is complex real ext-real Element of REAL
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
- (a) 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)) ^2) + (((- a)) ^2) is complex real ext-real Element of REAL
sqrt (((- (a)) ^2) + (((- a)) ^2)) is complex real ext-real Element of REAL
- (a) 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)) ^2) + ((- (a)) ^2) is complex real ext-real Element of REAL
sqrt (((- (a)) ^2) + ((- (a)) ^2)) is complex real ext-real Element of REAL
a is complex real ext-real set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
- a is complex real ext-real set
((- a)) is complex real ext-real non negative Element of REAL
((- a)) 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)) 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)) ^2) + (((- a)) ^2) is complex real ext-real Element of REAL
sqrt ((((- a)) ^2) + (((- a)) ^2)) is complex real ext-real Element of REAL
a is complex real ext-real set
a ^2 is complex real ext-real set
a * a is complex real ext-real set
sqrt (a ^2) is complex real ext-real set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
- a is complex real ext-real set
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real non negative Element of REAL
(a) 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) ^2 is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real set
((a) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
((a)) is complex real ext-real non negative Element of REAL
((a)) 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)) 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)) ^2) + (((a)) ^2) is complex real ext-real Element of REAL
sqrt ((((a)) ^2) + (((a)) ^2)) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real non negative Element of REAL
(a) ^2 is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real set
(a) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
((a)) is complex real ext-real non negative Element of REAL
((a)) 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)) 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)) ^2) + (((a)) ^2) is complex real ext-real Element of REAL
sqrt ((((a)) ^2) + (((a)) ^2)) is complex real ext-real Element of REAL
a is complex set
- a is complex set
((- a)) is complex real ext-real non negative Element of REAL
((- a)) 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)) 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)) ^2) + (((- a)) ^2) is complex real ext-real Element of REAL
sqrt ((((- a)) ^2) + (((- a)) ^2)) is complex real ext-real Element of REAL
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
a is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
((a)) is complex real ext-real non negative Element of REAL
((a)) 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)) 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)) ^2) + (((a)) ^2) is complex real ext-real Element of REAL
sqrt ((((a)) ^2) + (((a)) ^2)) is complex real ext-real Element of REAL
(a) is complex real ext-real non negative Element of REAL
(a) ^2 is complex real ext-real Element of REAL
(a) * (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
((a) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
((a) ^2) + (((a)) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + (((a)) ^2)) is complex real ext-real Element of REAL
- (a) 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) ^2) + ((- (a)) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((- (a)) ^2)) is complex real ext-real Element of REAL
a is complex real ext-real set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
- (a) is complex real ext-real non positive Element of REAL
- a is complex real ext-real set
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real non negative Element of REAL
(a) ^2 is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real set
(a) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
((a) ^2) + 0 is complex real ext-real Element of REAL
sqrt ((a) ^2) is complex real ext-real Element of REAL
((a)) is complex real ext-real non negative Element of REAL
((a)) 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)) 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)) ^2) + (((a)) ^2) is complex real ext-real Element of REAL
sqrt ((((a)) ^2) + (((a)) ^2)) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real non negative Element of REAL
(a) 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) ^2 is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real set
((a) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
((a) ^2) + 0 is complex real ext-real Element of REAL
sqrt ((a) ^2) is complex real ext-real Element of REAL
((a)) is complex real ext-real non negative Element of REAL
((a)) 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)) 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)) ^2) + (((a)) ^2) is complex real ext-real Element of REAL
sqrt ((((a)) ^2) + (((a)) ^2)) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
b is complex set
a + b is complex set
((a + b)) is complex real ext-real non negative Element of REAL
((a + b)) is complex real ext-real Element of REAL
((a + b)) ^2 is complex real ext-real Element of REAL
((a + b)) * ((a + b)) is complex real ext-real set
((a + b)) is complex real ext-real Element of REAL
((a + b)) ^2 is complex real ext-real Element of REAL
((a + b)) * ((a + b)) is complex real ext-real set
(((a + b)) ^2) + (((a + b)) ^2) is complex real ext-real Element of REAL
sqrt ((((a + b)) ^2) + (((a + b)) ^2)) is complex real ext-real Element of REAL
(b) is complex real ext-real non negative Element of REAL
(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
(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
((b) ^2) + ((b) ^2) is complex real ext-real Element of REAL
sqrt (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real non negative Element of REAL
(a) + (b) is complex real ext-real Element of REAL
((a) + (b)) ^2 is complex real ext-real Element of REAL
((a) + (b)) * ((a) + (b)) is complex real ext-real set
2 * (a) is complex real ext-real Element of REAL
(2 * (a)) * (b) is complex real ext-real Element of REAL
((a) ^2) + ((2 * (a)) * (b)) is complex real ext-real Element of REAL
(((a) ^2) + ((2 * (a)) * (b))) + ((b) ^2) is complex real ext-real Element of REAL
(((a) ^2) + ((a) ^2)) * (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) + ((a) * (b)) is complex real ext-real Element of REAL
(((a) * (b)) + ((a) * (b))) ^2 is complex real ext-real Element of REAL
(((a) * (b)) + ((a) * (b))) * (((a) * (b)) + ((a) * (b))) is complex real ext-real set
((((a) ^2) + ((a) ^2)) * (((b) ^2) + ((b) ^2))) - ((((a) * (b)) + ((a) * (b))) ^2) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL
(((a) * (b)) - ((a) * (b))) ^2 is complex real ext-real Element of REAL
(((a) * (b)) - ((a) * (b))) * (((a) * (b)) - ((a) * (b))) is complex real ext-real set
((((a) * (b)) + ((a) * (b))) ^2) + 0 is complex real ext-real Element of REAL
((((a) * (b)) + ((a) * (b)))) is complex real ext-real non negative Element of REAL
((((a) * (b)) + ((a) * (b)))) is complex real ext-real Element of REAL
((((a) * (b)) + ((a) * (b)))) ^2 is complex real ext-real Element of REAL
((((a) * (b)) + ((a) * (b)))) * ((((a) * (b)) + ((a) * (b)))) is complex real ext-real set
((((a) * (b)) + ((a) * (b)))) is complex real ext-real Element of REAL
((((a) * (b)) + ((a) * (b)))) ^2 is complex real ext-real Element of REAL
((((a) * (b)) + ((a) * (b)))) * ((((a) * (b)) + ((a) * (b)))) is complex real ext-real set
(((((a) * (b)) + ((a) * (b)))) ^2) + (((((a) * (b)) + ((a) * (b)))) ^2) is complex real ext-real Element of REAL
sqrt ((((((a) * (b)) + ((a) * (b)))) ^2) + (((((a) * (b)) + ((a) * (b)))) ^2)) is complex real ext-real Element of REAL
sqrt ((((a) * (b)) + ((a) * (b))) ^2) is complex real ext-real Element of REAL
(sqrt (((b) ^2) + ((b) ^2))) ^2 is complex real ext-real Element of REAL
(sqrt (((b) ^2) + ((b) ^2))) * (sqrt (((b) ^2) + ((b) ^2))) is complex real ext-real set
sqrt ((((a) ^2) + ((a) ^2)) * (((b) ^2) + ((b) ^2))) is complex real ext-real Element of REAL
(sqrt (((a) ^2) + ((a) ^2))) * (sqrt (((b) ^2) + ((b) ^2))) is complex real ext-real Element of REAL
2 * (a) is complex real ext-real Element of REAL
(2 * (a)) * (b) is complex real ext-real Element of REAL
((2 * (a)) * (b)) + ((2 * (a)) * (b)) is complex real ext-real Element of REAL
2 * (((a) * (b)) + ((a) * (b))) is complex real ext-real Element of REAL
2 * ((sqrt (((a) ^2) + ((a) ^2))) * (sqrt (((b) ^2) + ((b) ^2)))) is complex real ext-real Element of REAL
(((a) ^2) + ((a) ^2)) + (((2 * (a)) * (b)) + ((2 * (a)) * (b))) is complex real ext-real Element of REAL
2 * (sqrt (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(2 * (sqrt (((a) ^2) + ((a) ^2)))) * (sqrt (((b) ^2) + ((b) ^2))) is complex real ext-real Element of REAL
(((a) ^2) + ((a) ^2)) + ((2 * (sqrt (((a) ^2) + ((a) ^2)))) * (sqrt (((b) ^2) + ((b) ^2)))) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL
((a) + (b)) ^2 is complex real ext-real Element of REAL
((a) + (b)) * ((a) + (b)) is complex real ext-real set
((a) ^2) + ((2 * (a)) * (b)) is complex real ext-real Element of REAL
(((a) ^2) + ((2 * (a)) * (b))) + ((b) ^2) is complex real ext-real Element of REAL
((((a) ^2) + ((a) ^2)) + (((2 * (a)) * (b)) + ((2 * (a)) * (b)))) + (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
((((a) ^2) + ((a) ^2)) + ((2 * (sqrt (((a) ^2) + ((a) ^2)))) * (sqrt (((b) ^2) + ((b) ^2))))) + (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
(sqrt (((a) ^2) + ((a) ^2))) ^2 is complex real ext-real Element of REAL
(sqrt (((a) ^2) + ((a) ^2))) * (sqrt (((a) ^2) + ((a) ^2))) is complex real ext-real set
(sqrt (((a) ^2) + ((a) ^2))) + (sqrt (((b) ^2) + ((b) ^2))) is complex real ext-real Element of REAL
((sqrt (((a) ^2) + ((a) ^2))) + (sqrt (((b) ^2) + ((b) ^2)))) ^2 is complex real ext-real Element of REAL
((sqrt (((a) ^2) + ((a) ^2))) + (sqrt (((b) ^2) + ((b) ^2)))) * ((sqrt (((a) ^2) + ((a) ^2))) + (sqrt (((b) ^2) + ((b) ^2)))) is complex real ext-real set
sqrt (((sqrt (((a) ^2) + ((a) ^2))) + (sqrt (((b) ^2) + ((b) ^2)))) ^2) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
b is complex set
a - b is complex set
((a - b)) is complex real ext-real non negative Element of REAL
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
(((a - b)) ^2) + (((a - b)) ^2) is complex real ext-real Element of REAL
sqrt ((((a - b)) ^2) + (((a - b)) ^2)) is complex real ext-real Element of REAL
(b) is complex real ext-real non negative Element of REAL
(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
(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
((b) ^2) + ((b) ^2) is complex real ext-real Element of REAL
sqrt (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real non negative Element of REAL
- b is complex set
a + (- b) is complex set
((a + (- b))) is complex real ext-real non negative Element of REAL
((a + (- b))) is complex real ext-real Element of REAL
((a + (- b))) ^2 is complex real ext-real Element of REAL
((a + (- b))) * ((a + (- b))) is complex real ext-real set
((a + (- b))) is complex real ext-real Element of REAL
((a + (- b))) ^2 is complex real ext-real Element of REAL
((a + (- b))) * ((a + (- b))) is complex real ext-real set
(((a + (- b))) ^2) + (((a + (- b))) ^2) is complex real ext-real Element of REAL
sqrt ((((a + (- b))) ^2) + (((a + (- b))) ^2)) is complex real ext-real Element of REAL
((- b)) is complex real ext-real non negative Element of REAL
((- 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
((- 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
(((- b)) ^2) + (((- b)) ^2) is complex real ext-real Element of REAL
sqrt ((((- b)) ^2) + (((- b)) ^2)) is complex real ext-real Element of REAL
(a) + ((- b)) is complex real ext-real non negative Element of REAL
a is complex set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
b is complex set
(b) is complex real ext-real non negative Element of REAL
(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
(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
((b) ^2) + ((b) ^2) is complex real ext-real Element of REAL
sqrt (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
(a) - (b) is complex real ext-real Element of REAL
a + b is complex set
((a + b)) is complex real ext-real non negative Element of REAL
((a + b)) is complex real ext-real Element of REAL
((a + b)) ^2 is complex real ext-real Element of REAL
((a + b)) * ((a + b)) is complex real ext-real set
((a + b)) is complex real ext-real Element of REAL
((a + b)) ^2 is complex real ext-real Element of REAL
((a + b)) * ((a + b)) is complex real ext-real set
(((a + b)) ^2) + (((a + b)) ^2) is complex real ext-real Element of REAL
sqrt ((((a + b)) ^2) + (((a + b)) ^2)) is complex real ext-real Element of REAL
(a + b) - b is complex set
((a + b)) + (b) is complex real ext-real non negative Element of REAL
a is complex set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
b is complex set
(b) is complex real ext-real non negative Element of REAL
(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
(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
((b) ^2) + ((b) ^2) is complex real ext-real Element of REAL
sqrt (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
(a) - (b) is complex real ext-real Element of REAL
a - b is complex set
((a - b)) is complex real ext-real non negative Element of REAL
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
(((a - b)) ^2) + (((a - b)) ^2) is complex real ext-real Element of REAL
sqrt ((((a - b)) ^2) + (((a - b)) ^2)) is complex real ext-real Element of REAL
(a - b) + b is complex set
((a - b)) + (b) is complex real ext-real non negative Element of REAL
a is complex set
b is complex set
a - b is complex set
((a - b)) is complex real ext-real non negative Element of REAL
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
(((a - b)) ^2) + (((a - b)) ^2) is complex real ext-real Element of REAL
sqrt ((((a - b)) ^2) + (((a - b)) ^2)) is complex real ext-real Element of REAL
b - a is complex set
((b - a)) is complex real ext-real non negative Element of REAL
((b - a)) is complex real ext-real Element of REAL
((b - a)) ^2 is complex real ext-real Element of REAL
((b - a)) * ((b - a)) is complex real ext-real set
((b - a)) is complex real ext-real Element of REAL
((b - a)) ^2 is complex real ext-real Element of REAL
((b - a)) * ((b - a)) is complex real ext-real set
(((b - a)) ^2) + (((b - a)) ^2) is complex real ext-real Element of REAL
sqrt ((((b - a)) ^2) + (((b - a)) ^2)) is complex real ext-real Element of REAL
- (b - a) is complex set
((- (b - a))) is complex real ext-real non negative Element of REAL
((- (b - a))) is complex real ext-real Element of REAL
((- (b - a))) ^2 is complex real ext-real Element of REAL
((- (b - a))) * ((- (b - a))) is complex real ext-real set
((- (b - a))) is complex real ext-real Element of REAL
((- (b - a))) ^2 is complex real ext-real Element of REAL
((- (b - a))) * ((- (b - a))) is complex real ext-real set
(((- (b - a))) ^2) + (((- (b - a))) ^2) is complex real ext-real Element of REAL
sqrt ((((- (b - a))) ^2) + (((- (b - a))) ^2)) is complex real ext-real Element of REAL
a is complex set
b is complex set
a - b is complex set
((a - b)) is complex real ext-real non negative Element of REAL
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
(((a - b)) ^2) + (((a - b)) ^2) is complex real ext-real Element of REAL
sqrt ((((a - b)) ^2) + (((a - b)) ^2)) is complex real ext-real Element of REAL
a is complex set
b is complex set
a - b is complex set
((a - b)) is complex real ext-real non negative Element of REAL
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
(((a - b)) ^2) + (((a - b)) ^2) is complex real ext-real Element of REAL
sqrt ((((a - b)) ^2) + (((a - b)) ^2)) is complex real ext-real Element of REAL
a is complex set
b is complex set
a - b is complex set
((a - b)) is complex real ext-real non negative Element of REAL
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
(((a - b)) ^2) + (((a - b)) ^2) is complex real ext-real Element of REAL
sqrt ((((a - b)) ^2) + (((a - b)) ^2)) is complex real ext-real Element of REAL
c is complex set
a - c is complex set
((a - c)) is complex real ext-real non negative Element of REAL
((a - c)) is complex real ext-real Element of REAL
((a - c)) ^2 is complex real ext-real Element of REAL
((a - c)) * ((a - c)) is complex real ext-real set
((a - c)) is complex real ext-real Element of REAL
((a - c)) ^2 is complex real ext-real Element of REAL
((a - c)) * ((a - c)) is complex real ext-real set
(((a - c)) ^2) + (((a - c)) ^2) is complex real ext-real Element of REAL
sqrt ((((a - c)) ^2) + (((a - c)) ^2)) is complex real ext-real Element of REAL
c - b is complex set
((c - b)) is complex real ext-real non negative Element of REAL
((c - b)) is complex real ext-real Element of REAL
((c - b)) ^2 is complex real ext-real Element of REAL
((c - b)) * ((c - b)) is complex real ext-real set
((c - b)) is complex real ext-real Element of REAL
((c - b)) ^2 is complex real ext-real Element of REAL
((c - b)) * ((c - b)) is complex real ext-real set
(((c - b)) ^2) + (((c - b)) ^2) is complex real ext-real Element of REAL
sqrt ((((c - b)) ^2) + (((c - b)) ^2)) is complex real ext-real Element of REAL
((a - c)) + ((c - b)) is complex real ext-real non negative Element of REAL
(a - c) + (c - b) is complex set
(((a - c) + (c - b))) is complex real ext-real non negative Element of REAL
(((a - c) + (c - b))) is complex real ext-real Element of REAL
(((a - c) + (c - b))) ^2 is complex real ext-real Element of REAL
(((a - c) + (c - b))) * (((a - c) + (c - b))) is complex real ext-real set
(((a - c) + (c - b))) is complex real ext-real Element of REAL
(((a - c) + (c - b))) ^2 is complex real ext-real Element of REAL
(((a - c) + (c - b))) * (((a - c) + (c - b))) is complex real ext-real set
((((a - c) + (c - b))) ^2) + ((((a - c) + (c - b))) ^2) is complex real ext-real Element of REAL
sqrt (((((a - c) + (c - b))) ^2) + ((((a - c) + (c - b))) ^2)) is complex real ext-real Element of REAL
a is complex real ext-real set
- a is complex real ext-real set
b is complex real ext-real set
(b) is complex real ext-real non negative Element of REAL
(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
(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
((b) ^2) + ((b) ^2) is complex real ext-real Element of REAL
sqrt (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
- 0 is zero complex real ext-real non positive non negative V33() V34() V35() V36() V37() V38() V39() Element of REAL
- b is complex real ext-real set
- (- b) is complex real ext-real set
- b is complex real ext-real set
- (- a) is complex real ext-real set
a is complex set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
b is complex set
(b) is complex real ext-real non negative Element of REAL
(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
(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
((b) ^2) + ((b) ^2) is complex real ext-real Element of REAL
sqrt (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
(a) - (b) is complex real ext-real Element of REAL
(((a) - (b))) is complex real ext-real non negative Element of REAL
(((a) - (b))) is complex real ext-real Element of REAL
(((a) - (b))) ^2 is complex real ext-real Element of REAL
(((a) - (b))) * (((a) - (b))) is complex real ext-real set
(((a) - (b))) is complex real ext-real Element of REAL
(((a) - (b))) ^2 is complex real ext-real Element of REAL
(((a) - (b))) * (((a) - (b))) is complex real ext-real set
((((a) - (b))) ^2) + ((((a) - (b))) ^2) is complex real ext-real Element of REAL
sqrt (((((a) - (b))) ^2) + ((((a) - (b))) ^2)) is complex real ext-real Element of REAL
a - b is complex set
((a - b)) is complex real ext-real non negative Element of REAL
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
(((a - b)) ^2) + (((a - b)) ^2) is complex real ext-real Element of REAL
sqrt ((((a - b)) ^2) + (((a - b)) ^2)) is complex real ext-real Element of REAL
(b) - (a) is complex real ext-real Element of REAL
b - a is complex set
((b - a)) is complex real ext-real non negative Element of REAL
((b - a)) is complex real ext-real Element of REAL
((b - a)) ^2 is complex real ext-real Element of REAL
((b - a)) * ((b - a)) is complex real ext-real set
((b - a)) is complex real ext-real Element of REAL
((b - a)) ^2 is complex real ext-real Element of REAL
((b - a)) * ((b - a)) is complex real ext-real set
(((b - a)) ^2) + (((b - a)) ^2) is complex real ext-real Element of REAL
sqrt ((((b - a)) ^2) + (((b - a)) ^2)) is complex real ext-real Element of REAL
- ((a) - (b)) is complex real ext-real Element of REAL
- ((a - b)) is complex real ext-real non positive Element of REAL
- (- ((a) - (b))) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
b is complex set
a * b is complex set
((a * b)) is complex real ext-real non negative Element of REAL
((a * b)) is complex real ext-real Element of REAL
((a * b)) ^2 is complex real ext-real Element of REAL
((a * b)) * ((a * b)) is complex real ext-real set
((a * b)) is complex real ext-real Element of REAL
((a * b)) ^2 is complex real ext-real Element of REAL
((a * b)) * ((a * b)) is complex real ext-real set
(((a * b)) ^2) + (((a * b)) ^2) is complex real ext-real Element of REAL
sqrt ((((a * b)) ^2) + (((a * b)) ^2)) is complex real ext-real Element of REAL
(b) is complex real ext-real non negative Element of REAL
(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
(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
((b) ^2) + ((b) ^2) is complex real ext-real Element of REAL
sqrt (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real non negative Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
((a) * (b)) + ((b) * (a)) is complex real ext-real Element of REAL
(((a) * (b)) + ((b) * (a))) ^2 is complex real ext-real Element of REAL
(((a) * (b)) + ((b) * (a))) * (((a) * (b)) + ((b) * (a))) is complex real ext-real set
(a) * (b) is complex real ext-real Element of REAL
2 * ((a) * (b)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(2 * ((a) * (b))) * ((a) * (b)) is complex real ext-real Element of REAL
((a) * (b)) ^2 is complex real ext-real Element of REAL
((a) * (b)) * ((a) * (b)) is complex real ext-real set
((b) * (a)) ^2 is complex real ext-real Element of REAL
((b) * (a)) * ((b) * (a)) is complex real ext-real set
(((a) * (b)) ^2) + (((b) * (a)) ^2) is complex real ext-real Element of REAL
((2 * ((a) * (b))) * ((a) * (b))) + ((((a) * (b)) ^2) + (((b) * (a)) ^2)) is complex real ext-real Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL
(((a) * (b)) - ((a) * (b))) ^2 is complex real ext-real Element of REAL
(((a) * (b)) - ((a) * (b))) * (((a) * (b)) - ((a) * (b))) is complex real ext-real set
((a) * (b)) ^2 is complex real ext-real Element of REAL
((a) * (b)) * ((a) * (b)) is complex real ext-real set
((a) * (b)) ^2 is complex real ext-real Element of REAL
((a) * (b)) * ((a) * (b)) is complex real ext-real set
(((a) * (b)) ^2) + (((a) * (b)) ^2) is complex real ext-real Element of REAL
- ((2 * ((a) * (b))) * ((a) * (b))) is complex real ext-real Element of REAL
((((a) * (b)) ^2) + (((a) * (b)) ^2)) + (- ((2 * ((a) * (b))) * ((a) * (b)))) is complex real ext-real Element of REAL
(((a) ^2) + ((a) ^2)) * (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
a is complex set
a " is complex set
((a ")) is complex real ext-real non negative Element of REAL
((a ")) 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 ")) 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 ")) ^2) + (((a ")) ^2) is complex real ext-real Element of REAL
sqrt ((((a ")) ^2) + (((a ")) ^2)) is complex real ext-real Element of REAL
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
(a) " is complex real ext-real non negative Element of REAL
((a),(((a) ^2) + ((a) ^2))) is complex real ext-real Element of COMPLEX
((a),(((a) ^2) + ((a) ^2))) ^2 is complex real ext-real Element of COMPLEX
((a),(((a) ^2) + ((a) ^2))) * ((a),(((a) ^2) + ((a) ^2))) is complex real ext-real set
(((a),(((a) ^2) + ((a) ^2))) ^2) + (((a ")) ^2) is complex real ext-real Element of REAL
sqrt ((((a),(((a) ^2) + ((a) ^2))) ^2) + (((a ")) ^2)) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
((- (a)),(((a) ^2) + ((a) ^2))) is complex real ext-real Element of COMPLEX
((- (a)),(((a) ^2) + ((a) ^2))) ^2 is complex real ext-real Element of COMPLEX
((- (a)),(((a) ^2) + ((a) ^2))) * ((- (a)),(((a) ^2) + ((a) ^2))) is complex real ext-real set
((((a),(((a) ^2) + ((a) ^2))) ^2),(((- (a)),(((a) ^2) + ((a) ^2))) ^2)) is complex real ext-real Element of COMPLEX
sqrt ((((a),(((a) ^2) + ((a) ^2))) ^2),(((- (a)),(((a) ^2) + ((a) ^2))) ^2)) is complex real ext-real set
(((a) ^2) + ((a) ^2)) ^2 is complex real ext-real Element of REAL
(((a) ^2) + ((a) ^2)) * (((a) ^2) + ((a) ^2)) is complex real ext-real set
(((a) ^2),((((a) ^2) + ((a) ^2)) ^2)) is complex real ext-real Element of COMPLEX
((((a) ^2),((((a) ^2) + ((a) ^2)) ^2)),(((- (a)),(((a) ^2) + ((a) ^2))) ^2)) is complex real ext-real Element of COMPLEX
sqrt ((((a) ^2),((((a) ^2) + ((a) ^2)) ^2)),(((- (a)),(((a) ^2) + ((a) ^2))) ^2)) is complex real ext-real set
(- (a)) ^2 is complex real ext-real Element of REAL
(- (a)) * (- (a)) is complex real ext-real set
(((- (a)) ^2),((((a) ^2) + ((a) ^2)) ^2)) is complex real ext-real Element of COMPLEX
((((a) ^2),((((a) ^2) + ((a) ^2)) ^2)),(((- (a)) ^2),((((a) ^2) + ((a) ^2)) ^2))) is complex real ext-real Element of COMPLEX
sqrt ((((a) ^2),((((a) ^2) + ((a) ^2)) ^2)),(((- (a)) ^2),((((a) ^2) + ((a) ^2)) ^2))) is complex real ext-real set
1 * (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
(((a) ^2) + ((a) ^2)) * (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
((1 * (((a) ^2) + ((a) ^2))),((((a) ^2) + ((a) ^2)) * (((a) ^2) + ((a) ^2)))) is complex real ext-real Element of COMPLEX
sqrt ((1 * (((a) ^2) + ((a) ^2))),((((a) ^2) + ((a) ^2)) * (((a) ^2) + ((a) ^2)))) is complex real ext-real set
(1,(((a) ^2) + ((a) ^2))) is complex real ext-real Element of COMPLEX
sqrt (1,(((a) ^2) + ((a) ^2))) is complex real ext-real set
(1,(a)) is complex real ext-real non negative Element of COMPLEX
0 " is zero complex real ext-real non positive non negative V33() V34() V35() V36() V37() V38() V39() Element of REAL
a is complex set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
b is complex set
(b) is complex real ext-real non negative Element of REAL
(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
(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
((b) ^2) + ((b) ^2) is complex real ext-real Element of REAL
sqrt (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
((a),(b)) is complex real ext-real non negative Element of COMPLEX
(a,b) is complex Element of COMPLEX
((a,b)) is complex real ext-real non negative Element of REAL
((a,b)) is complex real ext-real Element of REAL
((a,b)) ^2 is complex real ext-real Element of REAL
((a,b)) * ((a,b)) is complex real ext-real set
((a,b)) is complex real ext-real Element of REAL
((a,b)) ^2 is complex real ext-real Element of REAL
((a,b)) * ((a,b)) is complex real ext-real set
(((a,b)) ^2) + (((a,b)) ^2) is complex real ext-real Element of REAL
sqrt ((((a,b)) ^2) + (((a,b)) ^2)) is complex real ext-real Element of REAL
(b) " is complex real ext-real non negative Element of REAL
(a) * ((b) ") is complex real ext-real non negative Element of REAL
b " is complex set
((b ")) is complex real ext-real non negative Element of REAL
((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
((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
(((b ")) ^2) + (((b ")) ^2) is complex real ext-real Element of REAL
sqrt ((((b ")) ^2) + (((b ")) ^2)) is complex real ext-real Element of REAL
(a) * ((b ")) is complex real ext-real non negative Element of REAL
a * (b ") is complex set
((a * (b "))) is complex real ext-real non negative Element of REAL
((a * (b "))) is complex real ext-real Element of REAL
((a * (b "))) ^2 is complex real ext-real Element of REAL
((a * (b "))) * ((a * (b "))) is complex real ext-real set
((a * (b "))) is complex real ext-real Element of REAL
((a * (b "))) ^2 is complex real ext-real Element of REAL
((a * (b "))) * ((a * (b "))) is complex real ext-real set
(((a * (b "))) ^2) + (((a * (b "))) ^2) is complex real ext-real Element of REAL
sqrt ((((a * (b "))) ^2) + (((a * (b "))) ^2)) is complex real ext-real Element of REAL
a is complex set
a * a is complex set
((a * a)) is complex real ext-real non negative Element of REAL
((a * a)) is complex real ext-real Element of REAL
((a * a)) ^2 is complex real ext-real Element of REAL
((a * a)) * ((a * a)) is complex real ext-real set
((a * a)) is complex real ext-real Element of REAL
((a * a)) ^2 is complex real ext-real Element of REAL
((a * a)) * ((a * a)) is complex real ext-real set
(((a * a)) ^2) + (((a * a)) ^2) is complex real ext-real Element of REAL
sqrt ((((a * a)) ^2) + (((a * a)) ^2)) is complex real ext-real Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
(a) is complex real ext-real non negative Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real non negative Element of REAL
(((a) ^2) + ((a) ^2)) ^2 is complex real ext-real Element of REAL
(((a) ^2) + ((a) ^2)) * (((a) ^2) + ((a) ^2)) is complex real ext-real set
sqrt ((((a) ^2) + ((a) ^2)) ^2) is complex real ext-real Element of REAL
a is complex set
a * a is complex set
((a * a)) is complex real ext-real non negative Element of REAL
((a * a)) is complex real ext-real Element of REAL
((a * a)) ^2 is complex real ext-real Element of REAL
((a * a)) * ((a * a)) is complex real ext-real set
((a * a)) is complex real ext-real Element of REAL
((a * a)) ^2 is complex real ext-real Element of REAL
((a * a)) * ((a * a)) is complex real ext-real set
(((a * a)) ^2) + (((a * a)) ^2) is complex real ext-real Element of REAL
sqrt ((((a * a)) ^2) + (((a * a)) ^2)) is complex real ext-real Element of REAL
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
a * (a) is complex set
((a * (a))) is complex real ext-real non negative Element of REAL
((a * (a))) is complex real ext-real Element of REAL
((a * (a))) ^2 is complex real ext-real Element of REAL
((a * (a))) * ((a * (a))) is complex real ext-real set
((a * (a))) is complex real ext-real Element of REAL
((a * (a))) ^2 is complex real ext-real Element of REAL
((a * (a))) * ((a * (a))) is complex real ext-real set
(((a * (a))) ^2) + (((a * (a))) ^2) is complex real ext-real Element of REAL
sqrt ((((a * (a))) ^2) + (((a * (a))) ^2)) is complex real ext-real Element of REAL
(a) is complex real ext-real non negative Element of REAL
(a) ^2 is complex real ext-real Element of REAL
(a) * (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
((a) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real non negative Element of REAL
((a)) is complex real ext-real non negative Element of REAL
((a)) 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)) 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)) ^2) + (((a)) ^2) is complex real ext-real Element of REAL
sqrt ((((a)) ^2) + (((a)) ^2)) is complex real ext-real Element of REAL
(a) * ((a)) is complex real ext-real non negative Element of REAL
a is complex real ext-real set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
- a is complex real ext-real set
a is complex real ext-real set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
- a is complex real ext-real set
a is complex real ext-real set
a ^2 is complex real ext-real set
a * a is complex real ext-real set
sqrt (a ^2) is complex real ext-real set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
a is complex real ext-real set
b is complex real ext-real set
min (a,b) is complex real ext-real set
a + b is complex real ext-real set
a - b is complex real ext-real set
((a - b)) is complex real ext-real non negative Element of REAL
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
(((a - b)) ^2) + (((a - b)) ^2) is complex real ext-real Element of REAL
sqrt ((((a - b)) ^2) + (((a - b)) ^2)) is complex real ext-real Element of REAL
(a + b) - ((a - b)) is complex real ext-real Element of REAL
(((a + b) - ((a - b))),2) is complex real ext-real Element of COMPLEX
b - a is complex real ext-real set
- (b - a) is complex real ext-real set
((- (b - a))) is complex real ext-real non negative Element of REAL
((- (b - a))) is complex real ext-real Element of REAL
((- (b - a))) ^2 is complex real ext-real Element of REAL
((- (b - a))) * ((- (b - a))) is complex real ext-real set
((- (b - a))) is complex real ext-real Element of REAL
((- (b - a))) ^2 is complex real ext-real Element of REAL
((- (b - a))) * ((- (b - a))) is complex real ext-real set
(((- (b - a))) ^2) + (((- (b - a))) ^2) is complex real ext-real Element of REAL
sqrt ((((- (b - a))) ^2) + (((- (b - a))) ^2)) is complex real ext-real Element of REAL
((b - a)) is complex real ext-real non negative Element of REAL
((b - a)) is complex real ext-real Element of REAL
((b - a)) ^2 is complex real ext-real Element of REAL
((b - a)) * ((b - a)) is complex real ext-real set
((b - a)) is complex real ext-real Element of REAL
((b - a)) ^2 is complex real ext-real Element of REAL
((b - a)) * ((b - a)) is complex real ext-real set
(((b - a)) ^2) + (((b - a)) ^2) is complex real ext-real Element of REAL
sqrt ((((b - a)) ^2) + (((b - a)) ^2)) is complex real ext-real Element of REAL
(a + b) - (a - b) is complex real ext-real set
(((a + b) - (a - b)),2) is complex real ext-real Element of COMPLEX
a is complex real ext-real set
b is complex real ext-real set
max (a,b) is complex real ext-real set
a + b is complex real ext-real set
a - b is complex real ext-real set
((a - b)) is complex real ext-real non negative Element of REAL
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
((a - b)) is complex real ext-real Element of REAL
((a - b)) ^2 is complex real ext-real Element of REAL
((a - b)) * ((a - b)) is complex real ext-real set
(((a - b)) ^2) + (((a - b)) ^2) is complex real ext-real Element of REAL
sqrt ((((a - b)) ^2) + (((a - b)) ^2)) is complex real ext-real Element of REAL
(a + b) + ((a - b)) is complex real ext-real Element of REAL
(((a + b) + ((a - b))),2) is complex real ext-real Element of COMPLEX
(a + b) + (a - b) is complex real ext-real set
(((a + b) + (a - b)),2) is complex real ext-real Element of COMPLEX
b - a is complex real ext-real set
- (a - b) is complex real ext-real set
(a + b) + (- (a - b)) is complex real ext-real set
(((a + b) + (- (a - b))),2) is complex real ext-real Element of COMPLEX
((- (a - b))) is complex real ext-real non negative Element of REAL
((- (a - b))) is complex real ext-real Element of REAL
((- (a - b))) ^2 is complex real ext-real Element of REAL
((- (a - b))) * ((- (a - b))) is complex real ext-real set
((- (a - b))) is complex real ext-real Element of REAL
((- (a - b))) ^2 is complex real ext-real Element of REAL
((- (a - b))) * ((- (a - b))) is complex real ext-real set
(((- (a - b))) ^2) + (((- (a - b))) ^2) is complex real ext-real Element of REAL
sqrt ((((- (a - b))) ^2) + (((- (a - b))) ^2)) is complex real ext-real Element of REAL
(a + b) + ((- (a - b))) is complex real ext-real Element of REAL
(((a + b) + ((- (a - b)))),2) is complex real ext-real Element of COMPLEX
a is complex real ext-real set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) 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 non negative set
a ^2 is complex real ext-real set
a * a is complex real ext-real set
- a is complex real ext-real set
a is complex real ext-real set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
- (a) is complex real ext-real non positive Element of REAL
b is complex real ext-real set
(b) is complex real ext-real non negative Element of REAL
(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
(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
((b) ^2) + ((b) ^2) is complex real ext-real Element of REAL
sqrt (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real non negative set
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
a is complex real ext-real set
b is complex real ext-real set
b * () is complex set
a + (b * ()) is complex set
c is complex real ext-real set
d is complex real ext-real set
d * () is complex set
c + (d * ()) is complex set
a - c is complex real ext-real set
b - d is complex real ext-real set
(b - d) * () is complex set
(a - c) + ((b - d) * ()) is complex set
a is complex real ext-real set
a ^2 is complex real ext-real set
a * a is complex real ext-real set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
b is complex real ext-real set
b ^2 is complex real ext-real set
b * b is complex real ext-real set
(a ^2) + (b ^2) is complex real ext-real set
sqrt ((a ^2) + (b ^2)) is complex real ext-real set
(b) is complex real ext-real non negative Element of REAL
(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
(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
((b) ^2) + ((b) ^2) is complex real ext-real Element of REAL
sqrt (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real non negative Element of REAL
(sqrt ((a ^2) + (b ^2))) ^2 is complex real ext-real set
(sqrt ((a ^2) + (b ^2))) * (sqrt ((a ^2) + (b ^2))) is complex real ext-real set
((a) + (b)) ^2 is complex real ext-real Element of REAL
((a) + (b)) * ((a) + (b)) is complex real ext-real non negative set
(a) ^2 is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real non negative set
2 * (a) is complex real ext-real non negative Element of REAL
(2 * (a)) * (b) is complex real ext-real non negative Element of REAL
((a) ^2) + ((2 * (a)) * (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 non negative set
(((a) ^2) + ((2 * (a)) * (b))) + ((b) ^2) is complex real ext-real Element of REAL
(((a) + (b)) ^2) - ((sqrt ((a ^2) + (b ^2))) ^2) is complex real ext-real Element of REAL
(a ^2) + ((2 * (a)) * (b)) is complex real ext-real Element of REAL
((a ^2) + ((2 * (a)) * (b))) + (b ^2) is complex real ext-real Element of REAL
(((a ^2) + ((2 * (a)) * (b))) + (b ^2)) - ((a ^2) + (b ^2)) is complex real ext-real Element of REAL
sqrt ((sqrt ((a ^2) + (b ^2))) ^2) is complex real ext-real set
sqrt (((a) + (b)) ^2) is complex real ext-real Element of REAL
a is complex real ext-real set
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
a ^2 is complex real ext-real set
a * a is complex real ext-real set
b is complex real ext-real set
b ^2 is complex real ext-real set
b * b is complex real ext-real set
(a ^2) + (b ^2) is complex real ext-real set
sqrt ((a ^2) + (b ^2)) is complex real ext-real set
(a ^2) + 0 is complex real ext-real Element of REAL
sqrt (a ^2) is complex real ext-real set
a is complex set
(1,a) is complex Element of COMPLEX
((1,a)) is complex real ext-real non negative Element of REAL
((1,a)) is complex real ext-real Element of REAL
((1,a)) ^2 is complex real ext-real Element of REAL
((1,a)) * ((1,a)) is complex real ext-real set
((1,a)) is complex real ext-real Element of REAL
((1,a)) ^2 is complex real ext-real Element of REAL
((1,a)) * ((1,a)) is complex real ext-real set
(((1,a)) ^2) + (((1,a)) ^2) is complex real ext-real Element of REAL
sqrt ((((1,a)) ^2) + (((1,a)) ^2)) is complex real ext-real Element of REAL
(a) is complex real ext-real non negative Element of REAL
(a) 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) 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) ^2) + ((a) ^2) is complex real ext-real Element of REAL
sqrt (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
(1,(a)) is complex real ext-real non negative Element of COMPLEX