REAL is non zero set
NAT is non zero epsilon-transitive epsilon-connected ordinal Element of K6(REAL)
K6(REAL) is set
COMPLEX is non zero set
0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real Element of NAT
1 is non zero epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real Element of NAT
{ b1 where b1 is complex ext-real real Element of REAL : P2[b1] } is set
{ b1 where b1 is complex ext-real real Element of REAL : P1[b1] } is set
b is set
eps is complex ext-real real Element of REAL
b is set
eps is complex ext-real real Element of REAL
b is Element of K6(REAL)
eps is Element of K6(REAL)
eps is complex ext-real real set
x is complex ext-real real set
y is complex ext-real real Element of REAL
c8 is complex ext-real real Element of REAL
eps is complex ext-real real set
x is complex ext-real real set
y is complex ext-real real set
a is complex ext-real real Element of REAL
b is complex ext-real real Element of REAL
min (a,b) is complex ext-real real set
max (a,b) is complex ext-real real set
a is complex ext-real real set
b is complex ext-real real set
min (a,b) is complex ext-real real set
max (a,b) is complex ext-real real set
(min (a,b)) + (max (a,b)) is complex ext-real real set
a + b is complex ext-real real set
a is complex ext-real real set
b is complex ext-real real set
max (a,b) is complex ext-real real set
a + b is complex ext-real real set
a + 0 is complex ext-real real set
b + 0 is complex ext-real real set
b + a is complex ext-real real set
a is complex set
a * a is complex set
a is complex set
(a) is set
a * a is complex set
a is complex ext-real real set
(a) is complex set
a * a is complex ext-real real set
a is complex Element of COMPLEX
(a) is complex set
a * a is complex set
a is complex ext-real real Element of REAL
(a) is complex ext-real real set
a * a is complex ext-real real set
a is complex set
(a) is complex set
a * a is complex set
- a is complex set
((- a)) is complex set
(- a) * (- a) is complex set
2 is non zero epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real Element of NAT
a is complex set
b is complex set
a + b is complex set
((a + b)) is complex set
(a + b) * (a + b) is complex set
(a) is complex set
a * a is complex set
2 * a is complex set
(2 * a) * b is complex set
(a) + ((2 * a) * b) is complex set
(b) is complex set
b * b is complex set
((a) + ((2 * a) * b)) + (b) is complex set
a is complex set
b is complex set
a - b is complex set
- b is complex set
a + (- b) is complex set
((a - b)) is complex set
(a - b) * (a - b) is complex set
(a) is complex set
a * a is complex set
2 * a is complex set
(2 * a) * b is complex set
(a) - ((2 * a) * b) is complex set
- ((2 * a) * b) is complex set
(a) + (- ((2 * a) * b)) is complex set
(b) is complex set
b * b is complex set
((a) - ((2 * a) * b)) + (b) is complex set
a is complex set
a + 1 is complex set
((a + 1)) is complex set
(a + 1) * (a + 1) is complex set
(a) is complex set
a * a is complex set
2 * a is complex set
(a) + (2 * a) is complex set
((a) + (2 * a)) + 1 is complex set
a is complex set
a - 1 is complex set
- 1 is non zero complex ext-real non positive negative real set
a + (- 1) is complex set
((a - 1)) is complex set
(a - 1) * (a - 1) is complex set
(a) is complex set
a * a is complex set
2 * a is complex set
(a) - (2 * a) is complex set
- (2 * a) is complex set
(a) + (- (2 * a)) is complex set
((a) - (2 * a)) + 1 is complex set
a is complex set
b is complex set
a - b is complex set
- b is complex set
a + (- b) is complex set
a + b is complex set
(a - b) * (a + b) is complex set
(a) is complex set
a * a is complex set
(b) is complex set
b * b is complex set
(a) - (b) is complex set
- (b) is complex set
(a) + (- (b)) is complex set
a is complex set
b is complex set
a * b is complex set
((a * b)) is complex set
(a * b) * (a * b) is complex set
(a) is complex set
a * a is complex set
(b) is complex set
b * b is complex set
(a) * (b) is complex set
a is complex set
(a) is complex set
a * a is complex set
b is complex set
(b) is complex set
b * b is complex set
(a) - (b) is complex set
- (b) is complex set
(a) + (- (b)) is complex set
a + b is complex set
1 / (a + b) is complex set
(a + b) " is complex set
1 * ((a + b) ") is complex set
a - b is complex set
- b is complex set
a + (- b) is complex set
(a - b) / ((a) - (b)) is complex set
((a) - (b)) " is complex set
(a - b) * (((a) - (b)) ") is complex set
1 * (a - b) is complex set
(a + b) * (a - b) is complex set
(1 * (a - b)) / ((a + b) * (a - b)) is complex set
((a + b) * (a - b)) " is complex set
(1 * (a - b)) * (((a + b) * (a - b)) ") is complex set
a is complex set
(a) is complex set
a * a is complex set
b is complex set
(b) is complex set
b * b is complex set
(a) - (b) is complex set
- (b) is complex set
(a) + (- (b)) is complex set
a - b is complex set
- b is complex set
a + (- b) is complex set
1 / (a - b) is complex set
(a - b) " is complex set
1 * ((a - b) ") is complex set
a + b is complex set
(a + b) / ((a) - (b)) is complex set
((a) - (b)) " is complex set
(a + b) * (((a) - (b)) ") is complex set
(a + b) * (a - b) is complex set
1 * (a + b) is complex set
(a - b) * (a + b) is complex set
(1 * (a + b)) / ((a - b) * (a + b)) is complex set
((a - b) * (a + b)) " is complex set
(1 * (a + b)) * (((a - b) * (a + b)) ") is complex set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
a * 1 is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
a * 1 is complex ext-real real set
a is complex ext-real real set
2 " is non zero complex ext-real positive non negative real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
a * b is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
a * b is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
a is complex ext-real real set
a + 1 is complex ext-real real set
0 + a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
(a) + a is complex ext-real real set
((a) + a) + (a + 1) is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
((a + 1)) is complex ext-real real set
(a + 1) * (a + 1) is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
a - (b) is complex ext-real real set
- (b) is complex ext-real real set
a + (- (b)) is complex ext-real real set
(a - (b)) / 2 is complex ext-real real set
2 " is non zero complex ext-real positive non negative real set
(a - (b)) * (2 ") is complex ext-real real set
eps is complex ext-real real set
(eps) is complex ext-real real set
eps * eps is complex ext-real real set
4 is non zero epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real Element of NAT
4 * b is complex ext-real real set
(a - (b)) / (4 * b) is complex ext-real real set
(4 * b) " is complex ext-real real set
(a - (b)) * ((4 * b) ") is complex ext-real real set
min (eps,((a - (b)) / (4 * b))) is complex ext-real real set
b + (min (eps,((a - (b)) / (4 * b)))) is complex ext-real real set
2 * b is complex ext-real real set
(min (eps,((a - (b)) / (4 * b)))) * (2 * b) is complex ext-real real set
2 * (2 * b) is complex ext-real real set
(a - (b)) / (2 * (2 * b)) is complex ext-real real set
(2 * (2 * b)) " is complex ext-real real set
(a - (b)) * ((2 * (2 * b)) ") is complex ext-real real set
((a - (b)) / (2 * (2 * b))) * (2 * b) is complex ext-real real set
((a - (b)) / 2) / (2 * b) is complex ext-real real set
(2 * b) " is complex ext-real real set
((a - (b)) / 2) * ((2 * b) ") is complex ext-real real set
(((a - (b)) / 2) / (2 * b)) * (2 * b) is complex ext-real real set
(2 * b) * (min (eps,((a - (b)) / (4 * b)))) is complex ext-real real set
((min (eps,((a - (b)) / (4 * b))))) is complex ext-real real set
(min (eps,((a - (b)) / (4 * b)))) * (min (eps,((a - (b)) / (4 * b)))) is complex ext-real real set
((2 * b) * (min (eps,((a - (b)) / (4 * b))))) + ((min (eps,((a - (b)) / (4 * b))))) is complex ext-real real set
((a - (b)) / 2) + ((a - (b)) / 2) is complex ext-real real set
((b + (min (eps,((a - (b)) / (4 * b)))))) is complex ext-real real set
(b + (min (eps,((a - (b)) / (4 * b))))) * (b + (min (eps,((a - (b)) / (4 * b))))) is complex ext-real real set
(b) + (((2 * b) * (min (eps,((a - (b)) / (4 * b))))) + ((min (eps,((a - (b)) / (4 * b)))))) is complex ext-real real set
(b) + (a - (b)) is complex ext-real real set
(b) - a is complex ext-real real set
- a is complex ext-real real set
(b) + (- a) is complex ext-real real set
2 * b is complex ext-real real set
((b) - a) / (2 * b) is complex ext-real real set
(2 * b) " is complex ext-real real set
((b) - a) * ((2 * b) ") is complex ext-real real set
min ((((b) - a) / (2 * b)),b) is complex ext-real real set
b - (min ((((b) - a) / (2 * b)),b)) is complex ext-real real set
- (min ((((b) - a) / (2 * b)),b)) is complex ext-real real set
b + (- (min ((((b) - a) / (2 * b)),b))) is complex ext-real real set
((b - (min ((((b) - a) / (2 * b)),b)))) is complex ext-real real set
(b - (min ((((b) - a) / (2 * b)),b))) * (b - (min ((((b) - a) / (2 * b)),b))) is complex ext-real real set
(2 * b) * (min ((((b) - a) / (2 * b)),b)) is complex ext-real real set
((min ((((b) - a) / (2 * b)),b))) is complex ext-real real set
(min ((((b) - a) / (2 * b)),b)) * (min ((((b) - a) / (2 * b)),b)) is complex ext-real real set
((2 * b) * (min ((((b) - a) / (2 * b)),b))) - ((min ((((b) - a) / (2 * b)),b))) is complex ext-real real set
- ((min ((((b) - a) / (2 * b)),b))) is complex ext-real real set
((2 * b) * (min ((((b) - a) / (2 * b)),b))) + (- ((min ((((b) - a) / (2 * b)),b)))) is complex ext-real real set
(b) - (((2 * b) * (min ((((b) - a) / (2 * b)),b))) - ((min ((((b) - a) / (2 * b)),b)))) is complex ext-real real set
- (((2 * b) * (min ((((b) - a) / (2 * b)),b))) - ((min ((((b) - a) / (2 * b)),b)))) is complex ext-real real set
(b) + (- (((2 * b) * (min ((((b) - a) / (2 * b)),b))) - ((min ((((b) - a) / (2 * b)),b))))) is complex ext-real real set
((2 * b) * (min ((((b) - a) / (2 * b)),b))) - 0 is complex ext-real real set
- 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real set
((2 * b) * (min ((((b) - a) / (2 * b)),b))) + (- 0) is complex ext-real real set
(min ((((b) - a) / (2 * b)),b)) * (2 * b) is complex ext-real real set
(((b) - a) / (2 * b)) * (2 * b) is complex ext-real real set
(b) - ((b) - a) is complex ext-real real set
- ((b) - a) is complex ext-real real set
(b) + (- ((b) - a)) is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
a is complex ext-real real Element of REAL
(a) is complex ext-real real set
(0) is complex ext-real real Element of REAL
(0) is complex ext-real real Element of REAL
0 * 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real set
((0)) is complex ext-real real Element of REAL
(1) is complex ext-real real Element of REAL
(1) is complex ext-real real Element of REAL
1 * 1 is non zero complex ext-real positive non negative real set
((1)) is complex ext-real real Element of REAL
a is complex ext-real real set
(a) is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
((b)) is complex ext-real real set
(b) * (b) is complex ext-real real set
((a)) is complex ext-real real set
(a) * (a) is complex ext-real real set
(2) is complex ext-real real Element of REAL
(2) is complex ext-real real Element of REAL
2 * 2 is non zero complex ext-real positive non negative real set
4 is non zero epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real Element of NAT
(4) is complex ext-real real Element of REAL
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
((a)) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
((a)) is complex ext-real real set
- a is complex ext-real real set
((- a)) is complex ext-real real set
(- a) * (- a) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
(0) is complex ext-real real Element of REAL
0 * 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real set
a is complex ext-real real set
(a) is complex ext-real real set
(0) is complex ext-real real Element of REAL
0 * 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real set
a is complex ext-real real set
(a) is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
a is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
(a) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
b is complex ext-real real set
a * b is complex ext-real real set
((a * b)) is complex ext-real real set
(b) is complex ext-real real set
(a) * (b) is complex ext-real real set
(((a * b))) is complex ext-real real set
((a * b)) * ((a * b)) is complex ext-real real set
((a)) is complex ext-real real set
(a) * (a) is complex ext-real real set
((a)) * b is complex ext-real real set
((b)) is complex ext-real real set
(b) * (b) is complex ext-real real set
((a)) * ((b)) is complex ext-real real set
(((a) * (b))) is complex ext-real real set
((a) * (b)) * ((a) * (b)) is complex ext-real real set
((((a) * (b)))) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
b is complex ext-real real set
a / b is complex ext-real real set
b " is complex ext-real real set
a * (b ") is complex ext-real real set
((a / b)) is complex ext-real real set
(b) is complex ext-real real set
(a) / (b) is complex ext-real real set
(b) " is complex ext-real real set
(a) * ((b) ") is complex ext-real real set
((b)) is complex ext-real real set
(b) * (b) is complex ext-real real set
((a)) is complex ext-real real set
(a) * (a) is complex ext-real real set
(((a) / (b))) is complex ext-real real set
((a) / (b)) * ((a) / (b)) is complex ext-real real set
a is complex ext-real real set
b is complex ext-real real set
a + b is complex ext-real real set
((a + b)) is complex ext-real real set
a is complex ext-real real set
1 / a is complex ext-real real set
a " is complex ext-real real set
1 * (a ") is complex ext-real real set
((1 / a)) is complex ext-real real set
(a) is complex ext-real real set
1 / (a) is complex ext-real real set
(a) " is complex ext-real real set
1 * ((a) ") is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
(a) / a is complex ext-real real set
a " is complex ext-real real set
(a) * (a ") is complex ext-real real set
1 / (a) is complex ext-real real set
(a) " is complex ext-real real set
1 * ((a) ") is complex ext-real real set
(0) is complex ext-real real Element of REAL
0 * 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real set
((a)) is complex ext-real real set
(a) * (a) is complex ext-real real set
a * (a) is complex ext-real real set
((a)) / (a * (a)) is complex ext-real real set
(a * (a)) " is complex ext-real real set
((a)) * ((a * (a)) ") is complex ext-real real set
1 * a is complex ext-real real set
(a) * a is complex ext-real real set
(1 * a) / ((a) * a) is complex ext-real real set
((a) * a) " is complex ext-real real set
(1 * a) * (((a) * a) ") is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a / (a) is complex ext-real real set
(a) " is complex ext-real real set
a * ((a) ") is complex ext-real real set
(0) is complex ext-real real Element of REAL
0 * 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real set
a * (a) is complex ext-real real set
((a)) is complex ext-real real set
(a) * (a) is complex ext-real real set
(a * (a)) / ((a)) is complex ext-real real set
((a)) " is complex ext-real real set
(a * (a)) * (((a)) ") is complex ext-real real set
(a) * a is complex ext-real real set
1 * a is complex ext-real real set
((a) * a) / (1 * a) is complex ext-real real set
(1 * a) " is complex ext-real real set
((a) * a) * ((1 * a) ") is complex ext-real real set
(a) / 1 is complex ext-real real set
1 " is non zero complex ext-real positive non negative real set
(a) * (1 ") is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
(a) - (b) is complex ext-real real set
- (b) is complex ext-real real set
(a) + (- (b)) is complex ext-real real set
(a) + (b) is complex ext-real real set
((a) - (b)) * ((a) + (b)) is complex ext-real real set
a - b is complex ext-real real set
- b is complex ext-real real set
a + (- b) is complex ext-real real set
((a)) is complex ext-real real set
(a) * (a) is complex ext-real real set
((b)) is complex ext-real real set
(b) * (b) is complex ext-real real set
((a)) - ((b)) is complex ext-real real set
- ((b)) is complex ext-real real set
((a)) + (- ((b))) is complex ext-real real set
a - ((b)) is complex ext-real real set
a + (- ((b))) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
((a)) is complex ext-real real set
(a) * (a) is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
((b)) is complex ext-real real set
(b) * (b) is complex ext-real real set
((a)) - ((b)) is complex ext-real real set
- ((b)) is complex ext-real real set
((a)) + (- ((b))) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
(a) + (b) is complex ext-real real set
1 / ((a) + (b)) is complex ext-real real set
((a) + (b)) " is complex ext-real real set
1 * (((a) + (b)) ") is complex ext-real real set
(a) - (b) is complex ext-real real set
- (b) is complex ext-real real set
(a) + (- (b)) is complex ext-real real set
a - b is complex ext-real real set
- b is complex ext-real real set
a + (- b) is complex ext-real real set
((a) - (b)) / (a - b) is complex ext-real real set
(a - b) " is complex ext-real real set
((a) - (b)) * ((a - b) ") is complex ext-real real set
((a)) is complex ext-real real set
(a) * (a) is complex ext-real real set
((b)) is complex ext-real real set
(b) * (b) is complex ext-real real set
((a)) - ((b)) is complex ext-real real set
- ((b)) is complex ext-real real set
((a)) + (- ((b))) is complex ext-real real set
((a) - (b)) / (((a)) - ((b))) is complex ext-real real set
(((a)) - ((b))) " is complex ext-real real set
((a) - (b)) * ((((a)) - ((b))) ") is complex ext-real real set
a - ((b)) is complex ext-real real set
a + (- ((b))) is complex ext-real real set
((a) - (b)) / (a - ((b))) is complex ext-real real set
(a - ((b))) " is complex ext-real real set
((a) - (b)) * ((a - ((b))) ") is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
(b) + (a) is complex ext-real real set
1 / ((b) + (a)) is complex ext-real real set
((b) + (a)) " is complex ext-real real set
1 * (((b) + (a)) ") is complex ext-real real set
(b) - (a) is complex ext-real real set
- (a) is complex ext-real real set
(b) + (- (a)) is complex ext-real real set
b - a is complex ext-real real set
- a is complex ext-real real set
b + (- a) is complex ext-real real set
((b) - (a)) / (b - a) is complex ext-real real set
(b - a) " is complex ext-real real set
((b) - (a)) * ((b - a) ") is complex ext-real real set
((b)) is complex ext-real real set
(b) * (b) is complex ext-real real set
((a)) is complex ext-real real set
(a) * (a) is complex ext-real real set
((b)) - ((a)) is complex ext-real real set
- ((a)) is complex ext-real real set
((b)) + (- ((a))) is complex ext-real real set
((b) - (a)) / (((b)) - ((a))) is complex ext-real real set
(((b)) - ((a))) " is complex ext-real real set
((b) - (a)) * ((((b)) - ((a))) ") is complex ext-real real set
b - ((a)) is complex ext-real real set
b + (- ((a))) is complex ext-real real set
((b) - (a)) / (b - ((a))) is complex ext-real real set
(b - ((a))) " is complex ext-real real set
((b) - (a)) * ((b - ((a))) ") is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
(a) - (b) is complex ext-real real set
- (b) is complex ext-real real set
(a) + (- (b)) is complex ext-real real set
1 / ((a) - (b)) is complex ext-real real set
((a) - (b)) " is complex ext-real real set
1 * (((a) - (b)) ") is complex ext-real real set
(a) + (b) is complex ext-real real set
a - b is complex ext-real real set
- b is complex ext-real real set
a + (- b) is complex ext-real real set
((a) + (b)) / (a - b) is complex ext-real real set
(a - b) " is complex ext-real real set
((a) + (b)) * ((a - b) ") is complex ext-real real set
((a)) is complex ext-real real set
(a) * (a) is complex ext-real real set
((b)) is complex ext-real real set
(b) * (b) is complex ext-real real set
((a)) - ((b)) is complex ext-real real set
- ((b)) is complex ext-real real set
((a)) + (- ((b))) is complex ext-real real set
((a) + (b)) / (((a)) - ((b))) is complex ext-real real set
(((a)) - ((b))) " is complex ext-real real set
((a) + (b)) * ((((a)) - ((b))) ") is complex ext-real real set
a - ((b)) is complex ext-real real set
a + (- ((b))) is complex ext-real real set
((a) + (b)) / (a - ((b))) is complex ext-real real set
(a - ((b))) " is complex ext-real real set
((a) + (b)) * ((a - ((b))) ") is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
(b) - (a) is complex ext-real real set
- (a) is complex ext-real real set
(b) + (- (a)) is complex ext-real real set
1 / ((b) - (a)) is complex ext-real real set
((b) - (a)) " is complex ext-real real set
1 * (((b) - (a)) ") is complex ext-real real set
(b) + (a) is complex ext-real real set
b - a is complex ext-real real set
- a is complex ext-real real set
b + (- a) is complex ext-real real set
((b) + (a)) / (b - a) is complex ext-real real set
(b - a) " is complex ext-real real set
((b) + (a)) * ((b - a) ") is complex ext-real real set
((b)) is complex ext-real real set
(b) * (b) is complex ext-real real set
((a)) is complex ext-real real set
(a) * (a) is complex ext-real real set
((b)) - ((a)) is complex ext-real real set
- ((a)) is complex ext-real real set
((b)) + (- ((a))) is complex ext-real real set
((b) + (a)) / (((b)) - ((a))) is complex ext-real real set
(((b)) - ((a))) " is complex ext-real real set
((b) + (a)) * ((((b)) - ((a))) ") is complex ext-real real set
b - ((a)) is complex ext-real real set
b + (- ((a))) is complex ext-real real set
((b) + (a)) / (b - ((a))) is complex ext-real real set
(b - ((a))) " is complex ext-real real set
((b) + (a)) * ((b - ((a))) ") is complex ext-real real set
a is complex set
(a) is complex set
a * a is complex set
b is complex set
(b) is complex set
b * b is complex set
- b is complex set
a - b is complex set
a + (- b) is complex set
a + b is complex set
(a - b) * (a + b) is complex set
- 1 is non zero complex ext-real non positive negative real set
a is complex set
(a) is complex set
a * a is complex set
a - 1 is complex set
a + (- 1) is complex set
a + 1 is complex set
(a - 1) * (a + 1) is complex set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
(a) - 1 is complex ext-real real set
(a) + (- 1) is complex ext-real real set
a - 1 is complex ext-real real set
a + (- 1) is complex ext-real real set
a + 1 is complex ext-real real set
(a - 1) * (a + 1) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
- b is complex ext-real real set
- a is complex ext-real real set
((- b)) is complex ext-real real set
(- b) * (- b) is complex ext-real real set
((- a)) is complex ext-real real set
(- a) * (- a) is complex ext-real real set
a is complex ext-real real set
- a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
- (- 1) is non zero complex ext-real positive non negative real set
((- a)) is complex ext-real real set
(- a) * (- a) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
- a is complex ext-real real set
- (- 1) is non zero complex ext-real positive non negative real set
((- a)) is complex ext-real real set
(- a) * (- a) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
- b is complex ext-real real set
- a is complex ext-real real set
- (- b) is complex ext-real real set
((- a)) is complex ext-real real set
(- a) * (- a) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
- b is complex ext-real real set
- (- b) is complex ext-real real set
- a is complex ext-real real set
((- a)) is complex ext-real real set
(- a) * (- a) is complex ext-real real set
a is complex ext-real real set
- a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
- b is complex ext-real real set
- (- a) is complex ext-real real set
((- b)) is complex ext-real real set
(- b) * (- b) is complex ext-real real set
a is complex ext-real real set
- a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
- (- a) is complex ext-real real set
- b is complex ext-real real set
((- b)) is complex ext-real real set
(- b) * (- b) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
(1) is complex ext-real real Element of REAL
1 * 1 is non zero complex ext-real positive non negative real set
(a) - (1) is complex ext-real real set
- (1) is complex ext-real real set
(a) + (- (1)) is complex ext-real real set
(1) - (1) is complex ext-real real set
(1) + (- (1)) is complex ext-real real set
a - 1 is complex ext-real real set
a + (- 1) is complex ext-real real set
a + 1 is complex ext-real real set
(a - 1) * (a + 1) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
(1) is complex ext-real real Element of REAL
1 * 1 is non zero complex ext-real positive non negative real set
(1) - (1) is complex ext-real real set
- (1) is complex ext-real real set
(1) + (- (1)) is complex ext-real real set
(a) - (1) is complex ext-real real set
(a) + (- (1)) is complex ext-real real set
a - 1 is complex ext-real real set
a + (- 1) is complex ext-real real set
a + 1 is complex ext-real real set
(a - 1) * (a + 1) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
(a) * (b) is complex ext-real real set
(1) is complex ext-real real Element of REAL
1 * 1 is non zero complex ext-real positive non negative real set
1 * (b) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
a * (b) is complex ext-real real set
(a) * b is complex ext-real real set
(((a) * b)) is complex ext-real real set
((a)) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
1 + (a) is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
(1 + (a)) * (b) is complex ext-real real set
1 + (b) is complex ext-real real set
(a) * (b) is complex ext-real real set
1 * (b) is complex ext-real real set
(1 * (b)) + ((a) * (b)) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
1 + (a) is complex ext-real real set
((1 + (a))) is complex ext-real real set
b is complex ext-real real set
- b is complex ext-real real set
(- b) * ((1 + (a))) is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
1 + (b) is complex ext-real real set
((1 + (b))) is complex ext-real real set
- ((1 + (b))) is complex ext-real real set
b * ((1 + (a))) is complex ext-real real set
1 + 0 is non zero complex ext-real positive non negative real set
((- b)) is complex ext-real real set
(- b) * (- b) is complex ext-real real set
((- b)) * (1 + (a)) is complex ext-real real set
((((- b)) * (1 + (a)))) is complex ext-real real set
- ((- b) * ((1 + (a)))) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
1 + (a) is complex ext-real real set
((1 + (a))) is complex ext-real real set
b is complex ext-real real set
b * ((1 + (a))) is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
1 + (b) is complex ext-real real set
((1 + (b))) is complex ext-real real set
- b is complex ext-real real set
- (- 1) is non zero complex ext-real positive non negative real set
- (- b) is complex ext-real real set
(- (- b)) * ((1 + (a))) is complex ext-real real set
((- b)) is complex ext-real real set
(- b) * (- b) is complex ext-real real set
1 + ((- b)) is complex ext-real real set
((1 + ((- b)))) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
1 + (a) is complex ext-real real set
((1 + (a))) is complex ext-real real set
b is complex ext-real real set
b * ((1 + (a))) is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
1 + (b) is complex ext-real real set
((1 + (b))) is complex ext-real real set
a * ((1 + (b))) is complex ext-real real set
- b is complex ext-real real set
(- b) * ((1 + (a))) is complex ext-real real set
((- b)) is complex ext-real real set
(- b) * (- b) is complex ext-real real set
((- b)) * (1 + (a)) is complex ext-real real set
((((- b)) * (1 + (a)))) is complex ext-real real set
(a) * 1 is complex ext-real real set
(a) * (b) is complex ext-real real set
((a) * 1) + ((a) * (b)) is complex ext-real real set
(b) * 1 is complex ext-real real set
(b) * (a) is complex ext-real real set
((b) * 1) + ((b) * (a)) is complex ext-real real set
- a is complex ext-real real set
(- a) * ((1 + (b))) is complex ext-real real set
((- a)) is complex ext-real real set
(- a) * (- a) is complex ext-real real set
((- a)) * (1 + (b)) is complex ext-real real set
((((- a)) * (1 + (b)))) is complex ext-real real set
- (a * ((1 + (b)))) is complex ext-real real set
- (b * ((1 + (a)))) is complex ext-real real set
a is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
1 + (b) is complex ext-real real set
((1 + (b))) is complex ext-real real set
a * ((1 + (b))) is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
1 + (a) is complex ext-real real set
((1 + (a))) is complex ext-real real set
b * ((1 + (a))) is complex ext-real real set
a is complex ext-real real set
b is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
1 + (a) is complex ext-real real set
((1 + (a))) is complex ext-real real set
b * ((1 + (a))) is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
1 + (b) is complex ext-real real set
((1 + (b))) is complex ext-real real set
a * ((1 + (b))) is complex ext-real real set
- a is complex ext-real real set
- b is complex ext-real real set
((- b)) is complex ext-real real set
(- b) * (- b) is complex ext-real real set
1 + ((- b)) is complex ext-real real set
((1 + ((- b)))) is complex ext-real real set
(- a) * ((1 + ((- b)))) is complex ext-real real set
((- a)) is complex ext-real real set
(- a) * (- a) is complex ext-real real set
1 + ((- a)) is complex ext-real real set
((1 + ((- a)))) is complex ext-real real set
(- b) * ((1 + ((- a)))) is complex ext-real real set
- (a * ((1 + (b)))) is complex ext-real real set
- (b * ((1 + (a)))) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
a * a is complex ext-real real set
1 + (a) is complex ext-real real set
((1 + (a))) is complex ext-real real set
b is complex ext-real real set
b * ((1 + (a))) is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
1 + (b) is complex ext-real real set
((1 + (b))) is complex ext-real real set
a * ((1 + (b))) is complex ext-real real set
a is complex ext-real real set
b is complex ext-real real set
(b) is complex ext-real real set
b * b is complex ext-real real set
a + (b) is complex ext-real real set
((a + (b))) is complex ext-real real set
0 + (b) is complex ext-real real set
((b)) is complex ext-real real set
a is complex ext-real real set
(a) is complex ext-real real set
b is complex ext-real real set
a + b is complex ext-real real set
((a + b)) is complex ext-real real set
(b) is complex ext-real real set
(a) + (b) is complex ext-real real set
a * b is complex ext-real real set
((a * b)) is complex ext-real real set
(a) * (b) is complex ext-real real set
2 * ((a) * (b)) is complex ext-real real set
a + 0 is complex ext-real real set
2 * (a) is complex ext-real real set
(2 * (a)) * (b) is complex ext-real real set
a + ((2 * (a)) * (b)) is complex ext-real real set
(a + ((2 * (a)) * (b))) + b is complex ext-real real set
(((a + ((2 * (a)) * (b))) + b)) is complex ext-real real set
((a)) is complex ext-real real set
(a) * (a) is complex ext-real real set
((a)) + ((2 * (a)) * (b)) is complex ext-real real set
(((a)) + ((2 * (a)) * (b))) + b is complex ext-real real set
(((((a)) + ((2 * (a)) * (b))) + b)) is complex ext-real real set
((b)) is complex ext-real real set
(b) * (b) is complex ext-real real set
(((a)) + ((2 * (a)) * (b))) + ((b)) is complex ext-real real set
(((((a)) + ((2 * (a)) * (b))) + ((b)))) is complex ext-real real set
(((a) + (b))) is complex ext-real real set
((a) + (b)) * ((a) + (b)) is complex ext-real real set
((((a) + (b)))) is complex ext-real real set