:: POWER semantic presentation

REAL is V1() V48() V49() V50() V54() V55() set
NAT is V48() V49() V50() V51() V52() V53() V54() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V1() V48() V54() V55() set
RAT is V1() V48() V49() V50() V51() V54() V55() set
INT is V1() V48() V49() V50() V51() V52() V54() V55() set
omega is V48() V49() V50() V51() V52() V53() V54() set
K6(omega) is set
K6(NAT) is set
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is set
K7(COMPLEX,REAL) is set
K6(K7(COMPLEX,REAL)) is set
K7(NAT,REAL) is set
K6(K7(NAT,REAL)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is set
K7(K7(NAT,NAT),NAT) is set
K6(K7(K7(NAT,NAT),NAT)) is set
0 is V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() Element of NAT
1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
- 1 is V11() real ext-real non positive integer rational Element of REAL
2 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
a is V11() real ext-real set
- a is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(- a) |^ b is V11() real ext-real set
a |^ b is V11() real ext-real set
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
1 + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(- a) |^ (1 + 1) is V11() real ext-real set
((- a) |^ (1 + 1)) |^ s1 is V11() real ext-real set
0 + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(- a) |^ (0 + 1) is V11() real ext-real set
((- a) |^ (0 + 1)) * ((- a) |^ (0 + 1)) is V11() real ext-real set
(((- a) |^ (0 + 1)) * ((- a) |^ (0 + 1))) |^ s1 is V11() real ext-real set
(- a) |^ 0 is V11() real ext-real set
((- a) |^ 0) * (- a) is V11() real ext-real set
(((- a) |^ 0) * (- a)) * ((- a) |^ (0 + 1)) is V11() real ext-real set
((((- a) |^ 0) * (- a)) * ((- a) |^ (0 + 1))) |^ s1 is V11() real ext-real set
(((- a) |^ 0) * (- a)) * (((- a) |^ 0) * (- a)) is V11() real ext-real set
((((- a) |^ 0) * (- a)) * (((- a) |^ 0) * (- a))) |^ s1 is V11() real ext-real set
(- a) GeoSeq is V21() V30( NAT , REAL ) Element of K6(K7(NAT,REAL))
((- a) GeoSeq) . 0 is V11() real ext-real Element of REAL
(((- a) GeoSeq) . 0) * (- a) is V11() real ext-real Element of REAL
((((- a) GeoSeq) . 0) * (- a)) * (((- a) |^ 0) * (- a)) is V11() real ext-real Element of REAL
(((((- a) GeoSeq) . 0) * (- a)) * (((- a) |^ 0) * (- a))) |^ s1 is V11() real ext-real Element of REAL
((((- a) GeoSeq) . 0) * (- a)) * ((((- a) GeoSeq) . 0) * (- a)) is V11() real ext-real Element of REAL
(((((- a) GeoSeq) . 0) * (- a)) * ((((- a) GeoSeq) . 0) * (- a))) |^ s1 is V11() real ext-real Element of REAL
1 * (- a) is V11() real ext-real Element of REAL
((((- a) GeoSeq) . 0) * (- a)) * (1 * (- a)) is V11() real ext-real Element of REAL
(((((- a) GeoSeq) . 0) * (- a)) * (1 * (- a))) |^ s1 is V11() real ext-real Element of REAL
(1 * (- a)) * (1 * (- a)) is V11() real ext-real Element of REAL
((1 * (- a)) * (1 * (- a))) |^ s1 is V11() real ext-real Element of REAL
a * a is V11() real ext-real set
(a * a) |^ s1 is V11() real ext-real set
a GeoSeq is V21() V30( NAT , REAL ) Element of K6(K7(NAT,REAL))
(a GeoSeq) . 0 is V11() real ext-real Element of REAL
((a GeoSeq) . 0) * a is V11() real ext-real Element of REAL
1 * a is V11() real ext-real Element of REAL
(((a GeoSeq) . 0) * a) * (1 * a) is V11() real ext-real Element of REAL
((((a GeoSeq) . 0) * a) * (1 * a)) |^ s1 is V11() real ext-real Element of REAL
(((a GeoSeq) . 0) * a) * (((a GeoSeq) . 0) * a) is V11() real ext-real Element of REAL
((((a GeoSeq) . 0) * a) * (((a GeoSeq) . 0) * a)) |^ s1 is V11() real ext-real Element of REAL
a |^ 0 is V11() real ext-real set
(a |^ 0) * a is V11() real ext-real set
(((a GeoSeq) . 0) * a) * ((a |^ 0) * a) is V11() real ext-real Element of REAL
((((a GeoSeq) . 0) * a) * ((a |^ 0) * a)) |^ s1 is V11() real ext-real Element of REAL
((a |^ 0) * a) * ((a |^ 0) * a) is V11() real ext-real set
(((a |^ 0) * a) * ((a |^ 0) * a)) |^ s1 is V11() real ext-real set
a |^ (0 + 1) is V11() real ext-real set
((a |^ 0) * a) * (a |^ (0 + 1)) is V11() real ext-real set
(((a |^ 0) * a) * (a |^ (0 + 1))) |^ s1 is V11() real ext-real set
(a |^ (0 + 1)) * (a |^ (0 + 1)) is V11() real ext-real set
((a |^ (0 + 1)) * (a |^ (0 + 1))) |^ s1 is V11() real ext-real set
a |^ (1 + 1) is V11() real ext-real set
(a |^ (1 + 1)) |^ s1 is V11() real ext-real set
a is V11() real ext-real set
- a is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(- a) |^ b is V11() real ext-real set
a |^ b is V11() real ext-real set
- (a |^ b) is V11() real ext-real set
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(2 * s1) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
(- a) |^ (2 * s1) is V11() real ext-real set
((- a) |^ (2 * s1)) * (- a) is V11() real ext-real set
a |^ (2 * s1) is V11() real ext-real set
(a |^ (2 * s1)) * (- a) is V11() real ext-real set
(a |^ (2 * s1)) * a is V11() real ext-real set
- ((a |^ (2 * s1)) * a) is V11() real ext-real set
a is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
a |^ b is V11() real ext-real set
s1 is V11() real ext-real set
b1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
s1 |^ b1 is V11() real ext-real set
b1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
s1 |^ b1 is V11() real ext-real set
s1 GeoSeq is V21() V30( NAT , REAL ) Element of K6(K7(NAT,REAL))
(s1 GeoSeq) . b1 is V11() real ext-real Element of REAL
b1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
X is ordinal natural V11() real ext-real non negative integer rational set
X + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
X is ordinal natural V11() real ext-real non negative integer rational set
X + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
s1 |^ b1 is V11() real ext-real set
s1 |^ X is V11() real ext-real set
(s1 |^ X) * s1 is V11() real ext-real set
b1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
s1 |^ b1 is V11() real ext-real set
b1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
s1 |^ b1 is V11() real ext-real set
b1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
s1 |^ b1 is V11() real ext-real set
b1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
s1 |^ b1 is V11() real ext-real set
- a is V11() real ext-real set
(- a) |^ b is V11() real ext-real set
b is V11() real ext-real set
a is ordinal natural V11() real ext-real non negative integer rational set
a -Root b is V11() real ext-real set
- b is V11() real ext-real set
a -Root (- b) is V11() real ext-real set
- (a -Root (- b)) is V11() real ext-real set
s1 is V11() real ext-real set
a is ordinal natural V11() real ext-real non negative integer rational set
b is V11() real ext-real Element of REAL
(a,b) is V11() real ext-real set
a is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational set
(b,a) is V11() real ext-real set
(b,a) |^ b is V11() real ext-real set
a |^ b is V11() real ext-real set
(b,(a |^ b)) is V11() real ext-real set
b -Root a is V11() real ext-real set
b -Root (a |^ b) is V11() real ext-real set
- a is V11() real ext-real set
b -Root (- a) is V11() real ext-real set
- (b -Root (- a)) is V11() real ext-real set
(- (b -Root (- a))) |^ b is V11() real ext-real set
(b -Root (- a)) |^ b is V11() real ext-real set
- ((b -Root (- a)) |^ b) is V11() real ext-real set
- (- a) is V11() real ext-real set
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(2 * s1) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(2 * s1) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
(- a) |^ b is V11() real ext-real set
- (a |^ b) is V11() real ext-real set
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(2 * s1) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
b -Root (- (a |^ b)) is V11() real ext-real set
- (b -Root (- (a |^ b))) is V11() real ext-real set
b -Root ((- a) |^ b) is V11() real ext-real set
- (b -Root ((- a) |^ b)) is V11() real ext-real set
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(2 * s1) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(2 * s1) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
a is ordinal natural V11() real ext-real non negative integer rational set
(a,0) is V11() real ext-real Element of REAL
a -Root 0 is V11() real ext-real set
a is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(a,1) is V11() real ext-real Element of REAL
a -Root 1 is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(b,a) is V11() real ext-real set
b -Root a is V11() real ext-real set
b -Root a is V11() real ext-real set
a is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(a,(- 1)) is V11() real ext-real Element of REAL
- (- 1) is V11() real ext-real non negative integer rational Element of REAL
a -Root (- (- 1)) is V11() real ext-real Element of REAL
- (a -Root (- (- 1))) is V11() real ext-real Element of REAL
a is V11() real ext-real set
(1,a) is V11() real ext-real set
1 -Root a is V11() real ext-real set
2 * 0 is V1() ordinal natural V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() even Element of NAT
(2 * 0) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
- a is V11() real ext-real set
1 -Root (- a) is V11() real ext-real set
- (1 -Root (- a)) is V11() real ext-real set
- (- a) is V11() real ext-real set
a is V11() real ext-real set
- a is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(b,a) is V11() real ext-real set
(b,(- a)) is V11() real ext-real set
- (b,(- a)) is V11() real ext-real set
b -Root (- a) is V11() real ext-real set
- (b -Root (- a)) is V11() real ext-real set
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(2 * s1) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
- 0 is V1() V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() Element of REAL
- (- a) is V11() real ext-real set
b -Root (- (- a)) is V11() real ext-real set
- (b -Root (- (- a))) is V11() real ext-real set
- (- (b -Root (- (- a)))) is V11() real ext-real set
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(2 * s1) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
a is V11() real ext-real set
b is V11() real ext-real set
a * b is V11() real ext-real set
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(s1,(a * b)) is V11() real ext-real set
(s1,a) is V11() real ext-real set
(s1,b) is V11() real ext-real set
(s1,a) * (s1,b) is V11() real ext-real set
X is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
b1 is V11() real ext-real set
X is V11() real ext-real set
b1 * X is V11() real ext-real set
(X,(b1 * X)) is V11() real ext-real set
X -Root (b1 * X) is V11() real ext-real set
X -Root b1 is V11() real ext-real set
X -Root X is V11() real ext-real set
(X -Root b1) * (X -Root X) is V11() real ext-real set
(X,b1) is V11() real ext-real set
(X,b1) * (X -Root X) is V11() real ext-real set
(X,X) is V11() real ext-real set
(X,b1) * (X,X) is V11() real ext-real set
- a is V11() real ext-real set
- b is V11() real ext-real set
(- a) * (- b) is V11() real ext-real set
s1 -Root ((- a) * (- b)) is V11() real ext-real set
s1 -Root (- a) is V11() real ext-real set
- (s1 -Root (- a)) is V11() real ext-real set
- (- (s1 -Root (- a))) is V11() real ext-real set
s1 -Root (- b) is V11() real ext-real set
(- (- (s1 -Root (- a)))) * (s1 -Root (- b)) is V11() real ext-real set
- (s1,a) is V11() real ext-real set
- (s1 -Root (- b)) is V11() real ext-real set
- (- (s1 -Root (- b))) is V11() real ext-real set
(- (s1,a)) * (- (- (s1 -Root (- b)))) is V11() real ext-real set
- (s1,b) is V11() real ext-real set
(- (s1,a)) * (- (s1,b)) is V11() real ext-real set
- (a * b) is V11() real ext-real set
(s1,(- (a * b))) is V11() real ext-real set
- (s1,(- (a * b))) is V11() real ext-real set
- b is V11() real ext-real set
a * (- b) is V11() real ext-real set
(s1,(a * (- b))) is V11() real ext-real set
- (s1,(a * (- b))) is V11() real ext-real set
(s1,(- b)) is V11() real ext-real set
(s1,a) * (s1,(- b)) is V11() real ext-real set
- ((s1,a) * (s1,(- b))) is V11() real ext-real set
- (s1,(- b)) is V11() real ext-real set
(s1,a) * (- (s1,(- b))) is V11() real ext-real set
- (a * b) is V11() real ext-real set
(s1,(- (a * b))) is V11() real ext-real set
- (s1,(- (a * b))) is V11() real ext-real set
- a is V11() real ext-real set
(- a) * b is V11() real ext-real set
(s1,((- a) * b)) is V11() real ext-real set
- (s1,((- a) * b)) is V11() real ext-real set
(s1,(- a)) is V11() real ext-real set
(s1,(- a)) * (s1,b) is V11() real ext-real set
- ((s1,(- a)) * (s1,b)) is V11() real ext-real set
- (s1,(- a)) is V11() real ext-real set
(- (s1,(- a))) * (s1,b) is V11() real ext-real set
a is V11() real ext-real set
1 / a is V11() real ext-real Element of REAL
a " is V11() real ext-real set
1 * (a ") is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(b,(1 / a)) is V11() real ext-real Element of REAL
(b,a) is V11() real ext-real set
1 / (b,a) is V11() real ext-real Element of REAL
(b,a) " is V11() real ext-real set
1 * ((b,a) ") is V11() real ext-real set
s1 is V11() real ext-real set
b1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / s1 is V11() real ext-real Element of REAL
s1 " is V11() real ext-real set
1 * (s1 ") is V11() real ext-real set
(b1,(1 / s1)) is V11() real ext-real Element of REAL
b1 -Root (1 / s1) is V11() real ext-real Element of REAL
b1 -Root s1 is V11() real ext-real set
1 / (b1 -Root s1) is V11() real ext-real Element of REAL
(b1 -Root s1) " is V11() real ext-real set
1 * ((b1 -Root s1) ") is V11() real ext-real set
(b1,s1) is V11() real ext-real set
1 / (b1,s1) is V11() real ext-real Element of REAL
(b1,s1) " is V11() real ext-real set
1 * ((b1,s1) ") is V11() real ext-real set
- a is V11() real ext-real set
(b,(- a)) is V11() real ext-real set
- (b,(- a)) is V11() real ext-real set
1 / (- (b,(- a))) is V11() real ext-real Element of REAL
(- (b,(- a))) " is V11() real ext-real set
1 * ((- (b,(- a))) ") is V11() real ext-real set
1 / (b,(- a)) is V11() real ext-real Element of REAL
(b,(- a)) " is V11() real ext-real set
1 * ((b,(- a)) ") is V11() real ext-real set
- (1 / (b,(- a))) is V11() real ext-real Element of REAL
1 / (- a) is V11() real ext-real Element of REAL
(- a) " is V11() real ext-real set
1 * ((- a) ") is V11() real ext-real set
(b,(1 / (- a))) is V11() real ext-real Element of REAL
- (b,(1 / (- a))) is V11() real ext-real Element of REAL
- (1 / a) is V11() real ext-real Element of REAL
(b,(- (1 / a))) is V11() real ext-real Element of REAL
- (b,(- (1 / a))) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
a / b is V11() real ext-real Element of COMPLEX
b " is V11() real ext-real set
a * (b ") is V11() real ext-real set
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(s1,(a / b)) is V11() real ext-real set
(s1,a) is V11() real ext-real set
(s1,b) is V11() real ext-real set
(s1,a) / (s1,b) is V11() real ext-real Element of COMPLEX
(s1,b) " is V11() real ext-real set
(s1,a) * ((s1,b) ") is V11() real ext-real set
s1 -Root (a / b) is V11() real ext-real set
s1 -Root a is V11() real ext-real set
s1 -Root b is V11() real ext-real set
(s1 -Root a) / (s1 -Root b) is V11() real ext-real Element of COMPLEX
(s1 -Root b) " is V11() real ext-real set
(s1 -Root a) * ((s1 -Root b) ") is V11() real ext-real set
(s1,a) / (s1 -Root b) is V11() real ext-real Element of COMPLEX
(s1,a) * ((s1 -Root b) ") is V11() real ext-real set
1 / b is V11() real ext-real Element of REAL
1 * (b ") is V11() real ext-real set
a * (1 / b) is V11() real ext-real Element of REAL
(s1,(a * (1 / b))) is V11() real ext-real Element of REAL
(s1,(1 / b)) is V11() real ext-real Element of REAL
(s1,a) * (s1,(1 / b)) is V11() real ext-real Element of REAL
1 / (s1,b) is V11() real ext-real Element of REAL
1 * ((s1,b) ") is V11() real ext-real set
(s1,a) * (1 / (s1,b)) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(s1,a) is V11() real ext-real set
(b,(s1,a)) is V11() real ext-real set
b * s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((b * s1),a) is V11() real ext-real set
b1 is V11() real ext-real set
X is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
X is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
X * X is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(X,b1) is V11() real ext-real set
X -Root b1 is V11() real ext-real set
(X,(X,b1)) is V11() real ext-real set
(X,(X -Root b1)) is V11() real ext-real set
X -Root (X -Root b1) is V11() real ext-real set
(X * X) -Root b1 is V11() real ext-real set
((X * X),b1) is V11() real ext-real set
b1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * b1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(2 * b1) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
X is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * X is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(2 * X) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
0 + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
b1 * (2 * X) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(b1 * (2 * X)) + b1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((b1 * (2 * X)) + b1) + X is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * (((b1 * (2 * X)) + b1) + X) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(2 * (((b1 * (2 * X)) + b1) + X)) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
- a is V11() real ext-real set
(s1,(- a)) is V11() real ext-real set
s1 -Root (- a) is V11() real ext-real set
- (s1 -Root (- a)) is V11() real ext-real set
(b,(- (s1 -Root (- a)))) is V11() real ext-real set
- (- (s1 -Root (- a))) is V11() real ext-real set
(b,(- (- (s1 -Root (- a))))) is V11() real ext-real set
- (b,(- (- (s1 -Root (- a))))) is V11() real ext-real set
b -Root (s1 -Root (- a)) is V11() real ext-real set
- (b -Root (s1 -Root (- a))) is V11() real ext-real set
(b * s1) -Root (- a) is V11() real ext-real set
- ((b * s1) -Root (- a)) is V11() real ext-real set
((b * s1),(- a)) is V11() real ext-real set
- ((b * s1),(- a)) is V11() real ext-real set
a is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(b,a) is V11() real ext-real set
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(s1,a) is V11() real ext-real set
(b,a) * (s1,a) is V11() real ext-real set
b * s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
b + s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
a |^ (b + s1) is V11() real ext-real set
((b * s1),(a |^ (b + s1))) is V11() real ext-real set
b1 is V11() real ext-real set
X is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
X is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
X * X is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
X + X is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
b1 |^ (X + X) is V11() real ext-real set
(X,b1) is V11() real ext-real set
(X,b1) is V11() real ext-real set
(X,b1) * (X,b1) is V11() real ext-real set
X -Root b1 is V11() real ext-real set
(X,b1) * (X -Root b1) is V11() real ext-real set
X -Root b1 is V11() real ext-real set
(X -Root b1) * (X -Root b1) is V11() real ext-real set
(X * X) -Root (b1 |^ (X + X)) is V11() real ext-real set
((X * X),(b1 |^ (X + X))) is V11() real ext-real set
b1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * b1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(2 * b1) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
X is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * X is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(2 * X) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
0 + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 + X is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
b1 + (1 + X) is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * (b1 + (1 + X)) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
- a is V11() real ext-real set
s1 -Root (- a) is V11() real ext-real set
- (s1 -Root (- a)) is V11() real ext-real set
(b,a) * (- (s1 -Root (- a))) is V11() real ext-real set
b -Root (- a) is V11() real ext-real set
- (b -Root (- a)) is V11() real ext-real set
(- (b -Root (- a))) * (- (s1 -Root (- a))) is V11() real ext-real set
(b -Root (- a)) * (s1 -Root (- a)) is V11() real ext-real set
(- a) |^ (b + s1) is V11() real ext-real set
(b * s1) -Root ((- a) |^ (b + s1)) is V11() real ext-real set
(b * s1) -Root (a |^ (b + s1)) is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(s1,a) is V11() real ext-real set
(s1,b) is V11() real ext-real set
b1 is V11() real ext-real set
X is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
X is V11() real ext-real set
X -Root b1 is V11() real ext-real set
X -Root X is V11() real ext-real set
(X,X) is V11() real ext-real set
(X,b1) is V11() real ext-real set
- a is V11() real ext-real set
(s1,(- a)) is V11() real ext-real set
- (s1,(- a)) is V11() real ext-real set
- 0 is V1() V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() Element of REAL
- b is V11() real ext-real set
- a is V11() real ext-real set
(s1,(- b)) is V11() real ext-real set
(s1,(- a)) is V11() real ext-real set
- (s1,(- a)) is V11() real ext-real set
- (s1,(- b)) is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(s1,b) is V11() real ext-real set
(s1,a) is V11() real ext-real set
b1 is V11() real ext-real set
X is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
X is V11() real ext-real set
X -Root X is V11() real ext-real set
X -Root b1 is V11() real ext-real set
(X,X) is V11() real ext-real set
(X,b1) is V11() real ext-real set
- a is V11() real ext-real set
s1 -Root (- a) is V11() real ext-real set
- 0 is V1() V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() Element of REAL
- (s1 -Root (- a)) is V11() real ext-real set
- b is V11() real ext-real set
(s1,(- a)) is V11() real ext-real set
(s1,(- b)) is V11() real ext-real set
- (s1,(- b)) is V11() real ext-real set
- (s1,(- a)) is V11() real ext-real set
a is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(b,a) is V11() real ext-real set
b -Root a is V11() real ext-real set
a is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(b,a) is V11() real ext-real set
- a is V11() real ext-real set
(b,(- a)) is V11() real ext-real set
- (b,(- a)) is V11() real ext-real set
a is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(b,a) is V11() real ext-real set
b -Root a is V11() real ext-real set
a is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(b,a) is V11() real ext-real set
- a is V11() real ext-real set
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(2 * s1) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
(b,(- a)) is V11() real ext-real set
- (b,(- a)) is V11() real ext-real set
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(2 * s1) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
a is V11() real ext-real set
a - 1 is V11() real ext-real Element of REAL
- 1 is V11() real ext-real non positive integer rational set
a + (- 1) is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(b,a) is V11() real ext-real set
(b,a) - 1 is V11() real ext-real Element of REAL
(b,a) + (- 1) is V11() real ext-real set
(a - 1) / b is V11() real ext-real Element of REAL
b " is V11() real ext-real non negative rational set
(a - 1) * (b ") is V11() real ext-real set
b -Root a is V11() real ext-real set
(b -Root a) - 1 is V11() real ext-real Element of REAL
(b -Root a) + (- 1) is V11() real ext-real set
a is V21() V30( NAT , REAL ) Element of K6(K7(NAT,REAL))
lim a is V11() real ext-real Element of REAL
b is V11() real ext-real set
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
a . s1 is V11() real ext-real Element of REAL
(s1,b) is V11() real ext-real set
s1 -Root b is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
a #R b is V11() real ext-real set
s1 is V11() real ext-real set
b1 is V11() real ext-real integer rational set
a #R b1 is V11() real ext-real set
a #Q b1 is V11() real ext-real set
a #Z b1 is V11() real ext-real set
X is V11() real ext-real integer rational set
a #Z X is V11() real ext-real set
b1 is ordinal natural V11() real ext-real non negative integer rational set
a #Z b1 is V11() real ext-real set
a |^ b1 is V11() real ext-real set
X is V11() real ext-real integer rational set
a #Z X is V11() real ext-real set
b1 is V11() real ext-real integer rational set
a #Z b1 is V11() real ext-real set
X is V11() real ext-real integer rational set
a #Z X is V11() real ext-real set
s1 is V11() real ext-real integer rational set
a #Z s1 is V11() real ext-real set
b1 is V11() real ext-real set
b1 is V11() real ext-real integer rational set
s1 is V11() real ext-real set
a #Z b1 is V11() real ext-real set
s1 is V11() real ext-real set
b1 is V11() real ext-real set
X is V11() real ext-real set
X is V11() real ext-real set
e is V11() real ext-real integer rational set
d is V11() real ext-real set
a #Z e is V11() real ext-real set
s is V11() real ext-real integer rational set
e is V11() real ext-real set
a #Z s is V11() real ext-real set
a is V11() real ext-real Element of REAL
b is V11() real ext-real Element of REAL
(a,b) is V11() real ext-real set
a is V11() real ext-real set
(a,0) is V11() real ext-real set
a #Z 0 is V11() real ext-real set
a is V11() real ext-real set
(a,1) is V11() real ext-real set
a #Z 1 is V11() real ext-real set
a is V11() real ext-real set
(1,a) is V11() real ext-real set
1 #R a is V11() real ext-real set
1 / 1 is V11() real ext-real non negative rational Element of REAL
1 " is V1() V11() real ext-real positive non negative rational set
1 * (1 ") is V11() real ext-real non negative rational set
(1 / 1) #R a is V11() real ext-real set
(1 #R a) / (1 #R a) is V11() real ext-real Element of COMPLEX
(1 #R a) " is V11() real ext-real set
(1 #R a) * ((1 #R a) ") is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
(a,b) is V11() real ext-real set
s1 is V11() real ext-real set
b + s1 is V11() real ext-real set
(a,(b + s1)) is V11() real ext-real set
(a,s1) is V11() real ext-real set
(a,b) * (a,s1) is V11() real ext-real set
a #R (b + s1) is V11() real ext-real set
a #R b is V11() real ext-real set
a #R s1 is V11() real ext-real set
(a #R b) * (a #R s1) is V11() real ext-real set
(a #R b) * (a,s1) is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
- b is V11() real ext-real set
(a,(- b)) is V11() real ext-real set
(a,b) is V11() real ext-real set
1 / (a,b) is V11() real ext-real Element of REAL
(a,b) " is V11() real ext-real set
1 * ((a,b) ") is V11() real ext-real set
a #R (- b) is V11() real ext-real set
a #R b is V11() real ext-real set
1 / (a #R b) is V11() real ext-real Element of REAL
(a #R b) " is V11() real ext-real set
1 * ((a #R b) ") is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
(a,b) is V11() real ext-real set
s1 is V11() real ext-real set
b - s1 is V11() real ext-real set
- s1 is V11() real ext-real set
b + (- s1) is V11() real ext-real set
(a,(b - s1)) is V11() real ext-real set
(a,s1) is V11() real ext-real set
(a,b) / (a,s1) is V11() real ext-real Element of COMPLEX
(a,s1) " is V11() real ext-real set
(a,b) * ((a,s1) ") is V11() real ext-real set
a #R (b - s1) is V11() real ext-real set
a #R b is V11() real ext-real set
a #R s1 is V11() real ext-real set
(a #R b) / (a #R s1) is V11() real ext-real Element of COMPLEX
(a #R s1) " is V11() real ext-real set
(a #R b) * ((a #R s1) ") is V11() real ext-real set
(a #R b) / (a,s1) is V11() real ext-real Element of COMPLEX
(a #R b) * ((a,s1) ") is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
a * b is V11() real ext-real set
s1 is V11() real ext-real set
((a * b),s1) is V11() real ext-real set
(a,s1) is V11() real ext-real set
(b,s1) is V11() real ext-real set
(a,s1) * (b,s1) is V11() real ext-real set
(a * b) #R s1 is V11() real ext-real set
a #R s1 is V11() real ext-real set
b #R s1 is V11() real ext-real set
(a #R s1) * (b #R s1) is V11() real ext-real set
(a #R s1) * (b,s1) is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
a / b is V11() real ext-real Element of COMPLEX
b " is V11() real ext-real set
a * (b ") is V11() real ext-real set
s1 is V11() real ext-real set
((a / b),s1) is V11() real ext-real set
(a,s1) is V11() real ext-real set
(b,s1) is V11() real ext-real set
(a,s1) / (b,s1) is V11() real ext-real Element of COMPLEX
(b,s1) " is V11() real ext-real set
(a,s1) * ((b,s1) ") is V11() real ext-real set
(a / b) #R s1 is V11() real ext-real set
a #R s1 is V11() real ext-real set
b #R s1 is V11() real ext-real set
(a #R s1) / (b #R s1) is V11() real ext-real Element of COMPLEX
(b #R s1) " is V11() real ext-real set
(a #R s1) * ((b #R s1) ") is V11() real ext-real set
(a #R s1) / (b,s1) is V11() real ext-real Element of COMPLEX
(a #R s1) * ((b,s1) ") is V11() real ext-real set
a is V11() real ext-real set
1 / a is V11() real ext-real Element of REAL
a " is V11() real ext-real set
1 * (a ") is V11() real ext-real set
b is V11() real ext-real set
((1 / a),b) is V11() real ext-real set
- b is V11() real ext-real set
(a,(- b)) is V11() real ext-real set
(1 / a) #R b is V11() real ext-real set
a #R b is V11() real ext-real set
1 / (a #R b) is V11() real ext-real Element of REAL
(a #R b) " is V11() real ext-real set
1 * ((a #R b) ") is V11() real ext-real set
(a,b) is V11() real ext-real set
1 / (a,b) is V11() real ext-real Element of REAL
(a,b) " is V11() real ext-real set
1 * ((a,b) ") is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
(a,b) is V11() real ext-real set
s1 is V11() real ext-real set
((a,b),s1) is V11() real ext-real set
b * s1 is V11() real ext-real set
(a,(b * s1)) is V11() real ext-real set
a #R b is V11() real ext-real set
(a #R b) #R s1 is V11() real ext-real set
a #R (b * s1) is V11() real ext-real set
((a #R b),s1) is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
(a,b) is V11() real ext-real set
a #R b is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
(a,b) is V11() real ext-real set
a #R b is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
(a,b) is V11() real ext-real set
a #R b is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
s1 is V11() real ext-real set
(b,s1) is V11() real ext-real set
(a,s1) is V11() real ext-real set
b / a is V11() real ext-real Element of COMPLEX
a " is V11() real ext-real set
b * (a ") is V11() real ext-real set
a / a is V11() real ext-real Element of COMPLEX
a * (a ") is V11() real ext-real set
((b / a),s1) is V11() real ext-real set
(b,s1) / (a,s1) is V11() real ext-real Element of COMPLEX
(a,s1) " is V11() real ext-real set
(b,s1) * ((a,s1) ") is V11() real ext-real set
((b,s1) / (a,s1)) * (a,s1) is V11() real ext-real set
1 * (a,s1) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
s1 is V11() real ext-real set
(a,s1) is V11() real ext-real set
(b,s1) is V11() real ext-real set
b / a is V11() real ext-real Element of COMPLEX
a " is V11() real ext-real set
b * (a ") is V11() real ext-real set
a / a is V11() real ext-real Element of COMPLEX
a * (a ") is V11() real ext-real set
((b / a),s1) is V11() real ext-real set
(b,s1) / (a,s1) is V11() real ext-real Element of COMPLEX
(a,s1) " is V11() real ext-real set
(b,s1) * ((a,s1) ") is V11() real ext-real set
1 * (a,s1) is V11() real ext-real Element of REAL
((b,s1) / (a,s1)) * (a,s1) is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
s1 is V11() real ext-real set
(s1,b) is V11() real ext-real set
(s1,a) is V11() real ext-real set
b - a is V11() real ext-real set
- a is V11() real ext-real set
b + (- a) is V11() real ext-real set
(s1,(b - a)) is V11() real ext-real set
(s1,b) / (s1,a) is V11() real ext-real Element of COMPLEX
(s1,a) " is V11() real ext-real set
(s1,b) * ((s1,a) ") is V11() real ext-real set
((s1,b) / (s1,a)) * (s1,a) is V11() real ext-real set
1 * (s1,a) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
s1 is V11() real ext-real set
(s1,a) is V11() real ext-real set
(s1,b) is V11() real ext-real set
1 / s1 is V11() real ext-real Element of REAL
s1 " is V11() real ext-real set
1 * (s1 ") is V11() real ext-real set
((1 / s1),a) is V11() real ext-real set
s1 / s1 is V11() real ext-real Element of COMPLEX
s1 * (s1 ") is V11() real ext-real set
b - a is V11() real ext-real set
- a is V11() real ext-real set
b + (- a) is V11() real ext-real set
((1 / s1),(b - a)) is V11() real ext-real set
((1 / s1),b) is V11() real ext-real set
((1 / s1),b) / ((1 / s1),a) is V11() real ext-real Element of COMPLEX
((1 / s1),a) " is V11() real ext-real set
((1 / s1),b) * (((1 / s1),a) ") is V11() real ext-real set
(((1 / s1),b) / ((1 / s1),a)) * ((1 / s1),a) is V11() real ext-real set
1 * ((1 / s1),a) is V11() real ext-real Element of REAL
(1,b) is V11() real ext-real set
(1,b) / (s1,b) is V11() real ext-real Element of COMPLEX
(s1,b) " is V11() real ext-real set
(1,b) * ((s1,b) ") is V11() real ext-real set
1 / (s1,b) is V11() real ext-real Element of REAL
1 * ((s1,b) ") is V11() real ext-real set
(1,a) is V11() real ext-real set
(1,a) / (s1,a) is V11() real ext-real Element of COMPLEX
(s1,a) " is V11() real ext-real set
(1,a) * ((s1,a) ") is V11() real ext-real set
1 / (s1,a) is V11() real ext-real Element of REAL
1 * ((s1,a) ") is V11() real ext-real set
a is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational set
(a,b) is V11() real ext-real set
a |^ b is V11() real ext-real set
a #Z b is V11() real ext-real set
a is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational set
(a,b) is V11() real ext-real set
a |^ b is V11() real ext-real set
a is V11() real ext-real integer rational set
(0,a) is V11() real ext-real set
0 #Z a is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real integer rational set
(a,b) is V11() real ext-real set
a #Z b is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real rational set
(a,b) is V11() real ext-real set
a #Q b is V11() real ext-real set
a #R b is V11() real ext-real set
a is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / b is V11() real ext-real non negative rational Element of REAL
b " is V11() real ext-real non negative rational set
1 * (b ") is V11() real ext-real non negative rational set
(a,(1 / b)) is V11() real ext-real set
(b,a) is V11() real ext-real set
s1 is V11() real ext-real rational set
a #Q s1 is V11() real ext-real set
b -Root a is V11() real ext-real set
b -Root a is V11() real ext-real set
b -Root a is V11() real ext-real set
b -Root a is V11() real ext-real set
a is V11() real ext-real set
(a,2) is V11() real ext-real set
a |^ 2 is V11() real ext-real set
a ^2 is V11() real ext-real set
a * a is V11() real ext-real set
1 + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(a,(1 + 1)) is V11() real ext-real set
a |^ (1 + 1) is V11() real ext-real set
(a,1) is V11() real ext-real set
a |^ 1 is V11() real ext-real set
(a,1) * (a,1) is V11() real ext-real set
(a,1) * a is V11() real ext-real set
b is V11() real ext-real integer rational set
b + b is V11() real ext-real integer rational set
a #Z (b + b) is V11() real ext-real set
a #Z b is V11() real ext-real set
(a #Z b) * (a #Z b) is V11() real ext-real set
a * (a #Z b) is V11() real ext-real set
a is V11() real ext-real set
- a is V11() real ext-real set
b is V11() real ext-real integer rational set
((- a),b) is V11() real ext-real set
(a,b) is V11() real ext-real set
s1 is V11() real ext-real integer rational set
2 * s1 is V11() real ext-real integer rational even Element of REAL
(a,2) is V11() real ext-real set
a |^ 2 is V11() real ext-real set
((a,2),s1) is V11() real ext-real set
a ^2 is V11() real ext-real set
a * a is V11() real ext-real set
((a ^2),s1) is V11() real ext-real set
(- a) ^2 is V11() real ext-real set
(- a) * (- a) is V11() real ext-real set
(((- a) ^2),s1) is V11() real ext-real set
((- a),2) is V11() real ext-real set
(- a) |^ 2 is V11() real ext-real set
(((- a),2),s1) is V11() real ext-real set
(- a) #Z 2 is V11() real ext-real set
(((- a) #Z 2),s1) is V11() real ext-real set
((- a) #Z 2) #Z s1 is V11() real ext-real set
(- a) #Z (2 * s1) is V11() real ext-real set
((- a),2) is V11() real ext-real set
(- a) |^ 2 is V11() real ext-real set
(((- a),2),s1) is V11() real ext-real set
(- a) ^2 is V11() real ext-real set
(- a) * (- a) is V11() real ext-real set
(((- a) ^2),s1) is V11() real ext-real set
a ^2 is V11() real ext-real set
a * a is V11() real ext-real set
((a ^2),s1) is V11() real ext-real set
(a,2) is V11() real ext-real set
a |^ 2 is V11() real ext-real set
((a,2),s1) is V11() real ext-real set
a #Z 2 is V11() real ext-real set
((a #Z 2),s1) is V11() real ext-real set
(a #Z 2) #Z s1 is V11() real ext-real set
a #Z (2 * s1) is V11() real ext-real set
a is V11() real ext-real set
- a is V11() real ext-real set
b is V11() real ext-real integer rational set
((- a),b) is V11() real ext-real set
(a,b) is V11() real ext-real set
- (a,b) is V11() real ext-real set
s1 is V11() real ext-real integer rational set
2 * s1 is V11() real ext-real integer rational even Element of REAL
(2 * s1) + 1 is V1() V11() real ext-real integer rational non even Element of REAL
- 0 is V1() V11() real ext-real non positive non negative integer rational V48() V49() V50() V51() V52() V53() V54() Element of REAL
(a,(2 * s1)) is V11() real ext-real set
(a,1) is V11() real ext-real set
a |^ 1 is V11() real ext-real set
(a,(2 * s1)) * (a,1) is V11() real ext-real set
(a,(2 * s1)) * a is V11() real ext-real set
((- a),(2 * s1)) is V11() real ext-real set
((- a),(2 * s1)) * a is V11() real ext-real set
((- a),(2 * s1)) * (- a) is V11() real ext-real set
- (((- a),(2 * s1)) * (- a)) is V11() real ext-real set
(- a) #Z (2 * s1) is V11() real ext-real set
((- a) #Z (2 * s1)) * (- a) is V11() real ext-real set
- (((- a) #Z (2 * s1)) * (- a)) is V11() real ext-real set
(- a) #Z 1 is V11() real ext-real set
((- a) #Z (2 * s1)) * ((- a) #Z 1) is V11() real ext-real set
- (((- a) #Z (2 * s1)) * ((- a) #Z 1)) is V11() real ext-real set
(- a) #Z b is V11() real ext-real set
- ((- a) #Z b) is V11() real ext-real set
- ((- a),b) is V11() real ext-real set
((- a),(2 * s1)) is V11() real ext-real set
((- a),1) is V11() real ext-real set
(- a) |^ 1 is V11() real ext-real set
((- a),(2 * s1)) * ((- a),1) is V11() real ext-real set
((- a),(2 * s1)) * (- a) is V11() real ext-real set
(a,(2 * s1)) is V11() real ext-real set
(a,(2 * s1)) * (- a) is V11() real ext-real set
(a,(2 * s1)) * a is V11() real ext-real set
- ((a,(2 * s1)) * a) is V11() real ext-real set
a #Z (2 * s1) is V11() real ext-real set
(a #Z (2 * s1)) * a is V11() real ext-real set
- ((a #Z (2 * s1)) * a) is V11() real ext-real set
a #Z 1 is V11() real ext-real set
(a #Z (2 * s1)) * (a #Z 1) is V11() real ext-real set
- ((a #Z (2 * s1)) * (a #Z 1)) is V11() real ext-real set
a #Z b is V11() real ext-real set
- (a #Z b) is V11() real ext-real set
a is V11() real ext-real set
b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
b * a is V11() real ext-real set
1 + (b * a) is V11() real ext-real Element of REAL
1 + a is V11() real ext-real Element of REAL
((1 + a),b) is V11() real ext-real set
(1 + a) |^ b is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
(a,b) is V11() real ext-real set
s1 is V11() real ext-real set
(a,s1) is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
{ b₁ where b₁ is V11() real ext-real Element of REAL : (a,b₁) <= b } is set
X is set
d is V11() real ext-real Element of REAL
(a,d) is V11() real ext-real set
X is V48() V49() V50() Element of K6(REAL)
d is V11() real ext-real set
e is V11() real ext-real set
e is V11() real ext-real Element of REAL
e - 1 is V11() real ext-real Element of REAL
- 1 is V11() real ext-real non positive integer rational set
e + (- 1) is V11() real ext-real set
e * (e - 1) is V11() real ext-real Element of REAL
1 / (e * (e - 1)) is V11() real ext-real Element of REAL
(e * (e - 1)) " is V11() real ext-real set
1 * ((e * (e - 1)) ") is V11() real ext-real set
m is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
0 - 1 is V1() V11() real ext-real non positive negative integer rational Element of REAL
0 + (- 1) is V11() real ext-real non positive integer rational set
m * (e - 1) is V11() real ext-real Element of REAL
1 + (m * (e - 1)) is V11() real ext-real Element of REAL
1 + (e - 1) is V11() real ext-real Element of REAL
((1 + (e - 1)),m) is V11() real ext-real set
(1 + (e - 1)) |^ m is V11() real ext-real set
0 + (m * (e - 1)) is V11() real ext-real Element of REAL
1 - 1 is V11() real ext-real integer rational Element of REAL
1 + (- 1) is V11() real ext-real integer rational set
(1 / (e * (e - 1))) * (e - 1) is V11() real ext-real Element of REAL
1 / e is V11() real ext-real Element of REAL
e " is V11() real ext-real set
1 * (e ") is V11() real ext-real set
(d,m) is V11() real ext-real set
d |^ m is V11() real ext-real set
1 / (d,m) is V11() real ext-real Element of REAL
(d,m) " is V11() real ext-real set
1 * ((d,m) ") is V11() real ext-real set
1 / (1 / e) is V11() real ext-real Element of REAL
(1 / e) " is V11() real ext-real set
1 * ((1 / e) ") is V11() real ext-real set
- m is V11() real ext-real non positive integer rational set
(e,(- m)) is V11() real ext-real set
s is V11() real ext-real Element of REAL
1 / a is V11() real ext-real Element of REAL
a " is V11() real ext-real set
1 * (a ") is V11() real ext-real set
1 / 1 is V11() real ext-real non negative rational Element of REAL
1 " is V1() V11() real ext-real positive non negative rational set
1 * (1 ") is V11() real ext-real non negative rational set
d is V11() real ext-real set
((1 / a),d) is V11() real ext-real set
s1 is V11() real ext-real Element of REAL
- d is V11() real ext-real set
(s1,(- d)) is V11() real ext-real set
b1 is V11() real ext-real Element of REAL
d is V11() real ext-real set
(a,d) is V11() real ext-real set
d is V11() real ext-real set
(a,d) is V11() real ext-real set
b1 is V11() real ext-real Element of REAL
b1 - 1 is V11() real ext-real Element of REAL
- 1 is V11() real ext-real non positive integer rational set
b1 + (- 1) is V11() real ext-real set
s1 is V11() real ext-real Element of REAL
s1 - 1 is V11() real ext-real Element of REAL
s1 + (- 1) is V11() real ext-real set
(b1 - 1) / (s1 - 1) is V11() real ext-real Element of REAL
(s1 - 1) " is V11() real ext-real set
(b1 - 1) * ((s1 - 1) ") is V11() real ext-real set
d is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
a - 1 is V11() real ext-real Element of REAL
a + (- 1) is V11() real ext-real set
1 - 1 is V11() real ext-real integer rational Element of REAL
1 + (- 1) is V11() real ext-real integer rational set
d * (a - 1) is V11() real ext-real Element of REAL
b - 1 is V11() real ext-real Element of REAL
b + (- 1) is V11() real ext-real set
1 + (d * (a - 1)) is V11() real ext-real Element of REAL
1 + (b - 1) is V11() real ext-real Element of REAL
0 - 1 is V1() V11() real ext-real non positive negative integer rational Element of REAL
0 + (- 1) is V11() real ext-real non positive integer rational set
d * (s1 - 1) is V11() real ext-real Element of REAL
1 + (d * (s1 - 1)) is V11() real ext-real Element of REAL
1 + (s1 - 1) is V11() real ext-real Element of REAL
((1 + (s1 - 1)),d) is V11() real ext-real set
(1 + (s1 - 1)) |^ d is V11() real ext-real set
(a,d) is V11() real ext-real set
a |^ d is V11() real ext-real set
e is ext-real set
e is V11() real ext-real Element of REAL
(a,e) is V11() real ext-real set
(s1,e) is V11() real ext-real Element of REAL
(s1,d) is V11() real ext-real set
s1 |^ d is V11() real ext-real set
upper_bound X is V11() real ext-real Element of REAL
d is V11() real ext-real Element of REAL
(a,d) is V11() real ext-real set
e is V11() real ext-real set
s1 is V11() real ext-real Element of REAL
s1 - 1 is V11() real ext-real Element of REAL
- 1 is V11() real ext-real non positive integer rational set
s1 + (- 1) is V11() real ext-real set
e is V11() real ext-real Element of REAL
b1 is V11() real ext-real Element of REAL
e / b1 is V11() real ext-real Element of REAL
b1 " is V11() real ext-real set
e * (b1 ") is V11() real ext-real set
(e / b1) - 1 is V11() real ext-real Element of REAL
(e / b1) + (- 1) is V11() real ext-real set
(s1 - 1) / ((e / b1) - 1) is V11() real ext-real Element of REAL
((e / b1) - 1) " is V11() real ext-real set
(s1 - 1) * (((e / b1) - 1) ") is V11() real ext-real set
s is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
max (1,s) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
a - 1 is V11() real ext-real Element of REAL
a + (- 1) is V11() real ext-real set
e / b is V11() real ext-real Element of REAL
b " is V11() real ext-real set
e * (b ") is V11() real ext-real set
(e / b) - 1 is V11() real ext-real Element of REAL
(e / b) + (- 1) is V11() real ext-real set
(a - 1) / ((e / b) - 1) is V11() real ext-real Element of REAL
((e / b) - 1) " is V11() real ext-real set
(a - 1) * (((e / b) - 1) ") is V11() real ext-real set
1 - 1 is V11() real ext-real integer rational Element of REAL
1 + (- 1) is V11() real ext-real integer rational set
n * ((e / b) - 1) is V11() real ext-real Element of REAL
(a - 1) / n is V11() real ext-real Element of REAL
n " is V11() real ext-real non negative rational set
(a - 1) * (n ") is V11() real ext-real set
((e / b) - 1) + 1 is V11() real ext-real Element of REAL
((a - 1) / n) + 1 is V11() real ext-real Element of REAL
(n,s1) is V11() real ext-real Element of REAL
(n,s1) - 1 is V11() real ext-real Element of REAL
(n,s1) + (- 1) is V11() real ext-real set
(s1 - 1) / n is V11() real ext-real Element of REAL
(s1 - 1) * (n ") is V11() real ext-real set
(n,a) is V11() real ext-real set
(n,a) - 1 is V11() real ext-real Element of REAL
(n,a) + (- 1) is V11() real ext-real set
((n,a) - 1) + 1 is V11() real ext-real Element of REAL
1 / n is V11() real ext-real non negative rational Element of REAL
1 * (n ") is V11() real ext-real non negative rational set
(s1,(1 / n)) is V11() real ext-real Element of REAL
(a,(1 / n)) is V11() real ext-real set
(a,(1 / n)) * b is V11() real ext-real set
d - (1 / n) is V11() real ext-real Element of REAL
- (1 / n) is V11() real ext-real non positive rational set
d + (- (1 / n)) is V11() real ext-real set
m is V11() real ext-real set
m is V11() real ext-real set
c is V11() real ext-real Element of REAL
(a,c) is V11() real ext-real set
(a,c) * (a,(1 / n)) is V11() real ext-real set
c₁₄ is V11() real ext-real Element of REAL
(a,c₁₄) is V11() real ext-real set
c + (1 / n) is V11() real ext-real Element of REAL
(s1,(c + (1 / n))) is V11() real ext-real Element of REAL
(s1,d) is V11() real ext-real Element of REAL
e is V11() real ext-real set
s1 is V11() real ext-real Element of REAL
(s1,d) is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
b / e is V11() real ext-real Element of REAL
e " is V11() real ext-real set
b * (e ") is V11() real ext-real set
(b / e) - 1 is V11() real ext-real Element of REAL
- 1 is V11() real ext-real non positive integer rational set
(b / e) + (- 1) is V11() real ext-real set
1 - 1 is V11() real ext-real integer rational Element of REAL
1 + (- 1) is V11() real ext-real integer rational set
s is V21() V30( NAT , REAL ) Element of K6(K7(NAT,REAL))
n is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
s . n is V11() real ext-real Element of REAL
(n,s1) is V11() real ext-real Element of REAL
lim s is V11() real ext-real Element of REAL
n is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
max (1,n) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
m is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
s . m is V11() real ext-real Element of REAL
(s . m) - 1 is V11() real ext-real Element of REAL
(s . m) + (- 1) is V11() real ext-real set
abs ((s . m) - 1) is V11() real ext-real Element of REAL
(m,a) is V11() real ext-real set
(m,a) - 1 is V11() real ext-real Element of REAL
(m,a) + (- 1) is V11() real ext-real set
abs ((m,a) - 1) is V11() real ext-real Element of REAL
b1 is V11() real ext-real Element of REAL
b1 / e is V11() real ext-real Element of REAL
b1 * (e ") is V11() real ext-real set
1 / m is V11() real ext-real non negative rational Element of REAL
m " is V11() real ext-real non negative rational set
1 * (m ") is V11() real ext-real non negative rational set
(s1,(1 / m)) is V11() real ext-real Element of REAL
(b / e) * (a,d) is V11() real ext-real Element of REAL
(a,(1 / m)) is V11() real ext-real set
(a,d) * (a,(1 / m)) is V11() real ext-real set
b * (a,d) is V11() real ext-real set
(b * (a,d)) / e is V11() real ext-real Element of REAL
(b * (a,d)) * (e ") is V11() real ext-real set
d + (1 / m) is V11() real ext-real Element of REAL
(a,(d + (1 / m))) is V11() real ext-real set
(a,d) / e is V11() real ext-real Element of REAL
(a,d) * (e ") is V11() real ext-real set
1 * b is V11() real ext-real Element of REAL
((a,d) / e) * b is V11() real ext-real Element of REAL
b1 is V11() real ext-real Element of REAL
b1 - 1 is V11() real ext-real Element of REAL
- 1 is V11() real ext-real non positive integer rational set
b1 + (- 1) is V11() real ext-real set
s1 is V11() real ext-real Element of REAL
1 / s1 is V11() real ext-real Element of REAL
s1 " is V11() real ext-real set
1 * (s1 ") is V11() real ext-real set
(1 / s1) - 1 is V11() real ext-real Element of REAL
(1 / s1) + (- 1) is V11() real ext-real set
(b1 - 1) / ((1 / s1) - 1) is V11() real ext-real Element of REAL
((1 / s1) - 1) " is V11() real ext-real set
(b1 - 1) * (((1 / s1) - 1) ") is V11() real ext-real set
d is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / a is V11() real ext-real Element of REAL
a " is V11() real ext-real set
1 * (a ") is V11() real ext-real set
1 / 1 is V11() real ext-real non negative rational Element of REAL
1 " is V1() V11() real ext-real positive non negative rational set
1 * (1 ") is V11() real ext-real non negative rational set
(1 / a) - 1 is V11() real ext-real Element of REAL
(1 / a) + (- 1) is V11() real ext-real set
1 - 1 is V11() real ext-real integer rational Element of REAL
1 + (- 1) is V11() real ext-real integer rational set
d * ((1 / a) - 1) is V11() real ext-real Element of REAL
b - 1 is V11() real ext-real Element of REAL
b + (- 1) is V11() real ext-real set
1 + (d * ((1 / a) - 1)) is V11() real ext-real Element of REAL
1 + (b - 1) is V11() real ext-real Element of REAL
0 - 1 is V1() V11() real ext-real non positive negative integer rational Element of REAL
0 + (- 1) is V11() real ext-real non positive integer rational set
d * ((1 / s1) - 1) is V11() real ext-real Element of REAL
1 + (d * ((1 / s1) - 1)) is V11() real ext-real Element of REAL
1 + ((1 / s1) - 1) is V11() real ext-real Element of REAL
((1 + ((1 / s1) - 1)),d) is V11() real ext-real set
(1 + ((1 / s1) - 1)) |^ d is V11() real ext-real set
((1 / a),d) is V11() real ext-real set
(1 / a) |^ d is V11() real ext-real set
- d is V11() real ext-real non positive integer rational set
(s1,(- d)) is V11() real ext-real set
e is ext-real set
e is V11() real ext-real Element of REAL
(a,e) is V11() real ext-real set
(s1,e) is V11() real ext-real Element of REAL
lower_bound X is V11() real ext-real Element of REAL
d is V11() real ext-real Element of REAL
(a,d) is V11() real ext-real set
e is V11() real ext-real set
s1 is V11() real ext-real Element of REAL
1 / s1 is V11() real ext-real Element of REAL
s1 " is V11() real ext-real set
1 * (s1 ") is V11() real ext-real set
(1 / s1) - 1 is V11() real ext-real Element of REAL
- 1 is V11() real ext-real non positive integer rational set
(1 / s1) + (- 1) is V11() real ext-real set
e is V11() real ext-real Element of REAL
b1 is V11() real ext-real Element of REAL
e / b1 is V11() real ext-real Element of REAL
b1 " is V11() real ext-real set
e * (b1 ") is V11() real ext-real set
(e / b1) - 1 is V11() real ext-real Element of REAL
(e / b1) + (- 1) is V11() real ext-real set
((1 / s1) - 1) / ((e / b1) - 1) is V11() real ext-real Element of REAL
((e / b1) - 1) " is V11() real ext-real set
((1 / s1) - 1) * (((e / b1) - 1) ") is V11() real ext-real set
s is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
max (1,s) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / a is V11() real ext-real Element of REAL
a " is V11() real ext-real set
1 * (a ") is V11() real ext-real set
(1 / a) - 1 is V11() real ext-real Element of REAL
(1 / a) + (- 1) is V11() real ext-real set
e / b is V11() real ext-real Element of REAL
b " is V11() real ext-real set
e * (b ") is V11() real ext-real set
(e / b) - 1 is V11() real ext-real Element of REAL
(e / b) + (- 1) is V11() real ext-real set
((1 / a) - 1) / ((e / b) - 1) is V11() real ext-real Element of REAL
((e / b) - 1) " is V11() real ext-real set
((1 / a) - 1) * (((e / b) - 1) ") is V11() real ext-real set
1 - 1 is V11() real ext-real integer rational Element of REAL
1 + (- 1) is V11() real ext-real integer rational set
n * ((e / b) - 1) is V11() real ext-real Element of REAL
((1 / a) - 1) / n is V11() real ext-real Element of REAL
n " is V11() real ext-real non negative rational set
((1 / a) - 1) * (n ") is V11() real ext-real set
((e / b) - 1) + 1 is V11() real ext-real Element of REAL
(((1 / a) - 1) / n) + 1 is V11() real ext-real Element of REAL
(n,(1 / s1)) is V11() real ext-real Element of REAL
(n,(1 / s1)) - 1 is V11() real ext-real Element of REAL
(n,(1 / s1)) + (- 1) is V11() real ext-real set
((1 / s1) - 1) / n is V11() real ext-real Element of REAL
((1 / s1) - 1) * (n ") is V11() real ext-real set
(n,(1 / a)) is V11() real ext-real Element of REAL
(n,(1 / a)) - 1 is V11() real ext-real Element of REAL
(n,(1 / a)) + (- 1) is V11() real ext-real set
((n,(1 / a)) - 1) + 1 is V11() real ext-real Element of REAL
1 / n is V11() real ext-real non negative rational Element of REAL
1 * (n ") is V11() real ext-real non negative rational set
((1 / s1),(1 / n)) is V11() real ext-real Element of REAL
((1 / a),(1 / n)) is V11() real ext-real Element of REAL
((1 / a),(1 / n)) * b is V11() real ext-real Element of REAL
- (1 / n) is V11() real ext-real non positive rational Element of REAL
(s1,(- (1 / n))) is V11() real ext-real Element of REAL
(s1,(- (1 / n))) * b1 is V11() real ext-real Element of REAL
d + (1 / n) is V11() real ext-real Element of REAL
m is V11() real ext-real set
m is V11() real ext-real set
c is V11() real ext-real Element of REAL
(a,c) is V11() real ext-real set
(a,(- (1 / n))) is V11() real ext-real set
(a,c) * (a,(- (1 / n))) is V11() real ext-real set
(a,(- (1 / n))) * b is V11() real ext-real set
c₁₄ is V11() real ext-real Element of REAL
(a,c₁₄) is V11() real ext-real set
c + (- (1 / n)) is V11() real ext-real Element of REAL
(s1,(c + (- (1 / n)))) is V11() real ext-real Element of REAL
c - (1 / n) is V11() real ext-real Element of REAL
- (1 / n) is V11() real ext-real non positive rational set
c + (- (1 / n)) is V11() real ext-real set
(s1,d) is V11() real ext-real Element of REAL
(s1,(c - (1 / n))) is V11() real ext-real Element of REAL
e is V11() real ext-real set
s1 is V11() real ext-real Element of REAL
(s1,d) is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
b / e is V11() real ext-real Element of REAL
e " is V11() real ext-real set
b * (e ") is V11() real ext-real set
(b / e) - 1 is V11() real ext-real Element of REAL
- 1 is V11() real ext-real non positive integer rational set
(b / e) + (- 1) is V11() real ext-real set
1 - 1 is V11() real ext-real integer rational Element of REAL
1 + (- 1) is V11() real ext-real integer rational set
1 / a is V11() real ext-real Element of REAL
a " is V11() real ext-real set
1 * (a ") is V11() real ext-real set
s is V21() V30( NAT , REAL ) Element of K6(K7(NAT,REAL))
1 / s1 is V11() real ext-real Element of REAL
s1 " is V11() real ext-real set
1 * (s1 ") is V11() real ext-real set
n is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
s . n is V11() real ext-real Element of REAL
(n,(1 / s1)) is V11() real ext-real Element of REAL
lim s is V11() real ext-real Element of REAL
n is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
max (1,n) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
m is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
s . m is V11() real ext-real Element of REAL
(s . m) - 1 is V11() real ext-real Element of REAL
(s . m) + (- 1) is V11() real ext-real set
abs ((s . m) - 1) is V11() real ext-real Element of REAL
(m,(1 / a)) is V11() real ext-real Element of REAL
(m,(1 / a)) - 1 is V11() real ext-real Element of REAL
(m,(1 / a)) + (- 1) is V11() real ext-real set
abs ((m,(1 / a)) - 1) is V11() real ext-real Element of REAL
b1 is V11() real ext-real Element of REAL
b1 / e is V11() real ext-real Element of REAL
b1 * (e ") is V11() real ext-real set
1 / m is V11() real ext-real non negative rational Element of REAL
m " is V11() real ext-real non negative rational set
1 * (m ") is V11() real ext-real non negative rational set
((1 / s1),(1 / m)) is V11() real ext-real Element of REAL
(b / e) * (a,d) is V11() real ext-real Element of REAL
((1 / a),(1 / m)) is V11() real ext-real Element of REAL
(a,d) * ((1 / a),(1 / m)) is V11() real ext-real Element of REAL
(b1 / e) * (s1,d) is V11() real ext-real Element of REAL
- (1 / m) is V11() real ext-real non positive rational Element of REAL
(s1,(- (1 / m))) is V11() real ext-real Element of REAL
(s1,d) * (s1,(- (1 / m))) is V11() real ext-real Element of REAL
b * (a,d) is V11() real ext-real set
(b * (a,d)) / e is V11() real ext-real Element of REAL
(b * (a,d)) * (e ") is V11() real ext-real set
d - (1 / m) is V11() real ext-real Element of REAL
- (1 / m) is V11() real ext-real non positive rational set
d + (- (1 / m)) is V11() real ext-real set
(a,(d - (1 / m))) is V11() real ext-real set
(a,d) / e is V11() real ext-real Element of REAL
(a,d) * (e ") is V11() real ext-real set
1 * b is V11() real ext-real Element of REAL
((a,d) / e) * b is V11() real ext-real Element of REAL
d is V11() real ext-real Element of REAL
(a,d) is V11() real ext-real set
s1 is V11() real ext-real set
(a,s1) is V11() real ext-real set
b1 is V11() real ext-real set
(a,b1) is V11() real ext-real set
a is V11() real ext-real Element of REAL
b is V11() real ext-real Element of REAL
(a,b) is V11() real ext-real set
a is V11() real ext-real set
(a,1) is V11() real ext-real set
(a,0) is V11() real ext-real set
a |^ 0 is V11() real ext-real set
a is V11() real ext-real set
(a,a) is V11() real ext-real set
(a,1) is V11() real ext-real set
a |^ 1 is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
(a,b) is V11() real ext-real set
s1 is V11() real ext-real set
(a,s1) is V11() real ext-real set
(a,b) + (a,s1) is V11() real ext-real set
b * s1 is V11() real ext-real set
(a,(b * s1)) is V11() real ext-real set
(a,((a,b) + (a,s1))) is V11() real ext-real set
(a,(a,b)) is V11() real ext-real set
(a,(a,s1)) is V11() real ext-real set
(a,(a,b)) * (a,(a,s1)) is V11() real ext-real set
b * (a,(a,s1)) is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
(a,b) is V11() real ext-real set
s1 is V11() real ext-real set
(a,s1) is V11() real ext-real set
(a,b) - (a,s1) is V11() real ext-real set
- (a,s1) is V11() real ext-real set
(a,b) + (- (a,s1)) is V11() real ext-real set
b / s1 is V11() real ext-real Element of COMPLEX
s1 " is V11() real ext-real set
b * (s1 ") is V11() real ext-real set
(a,(b / s1)) is V11() real ext-real set
(a,((a,b) - (a,s1))) is V11() real ext-real set
(a,(a,b)) is V11() real ext-real set
(a,(a,s1)) is V11() real ext-real set
(a,(a,b)) / (a,(a,s1)) is V11() real ext-real Element of COMPLEX
(a,(a,s1)) " is V11() real ext-real set
(a,(a,b)) * ((a,(a,s1)) ") is V11() real ext-real set
b / (a,(a,s1)) is V11() real ext-real Element of COMPLEX
b * ((a,(a,s1)) ") is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
(a,b) is V11() real ext-real set
s1 is V11() real ext-real set
(b,s1) is V11() real ext-real set
(a,(b,s1)) is V11() real ext-real set
s1 * (a,b) is V11() real ext-real set
(a,(s1 * (a,b))) is V11() real ext-real set
(a,(a,b)) is V11() real ext-real set
((a,(a,b)),s1) is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
(a,b) is V11() real ext-real set
s1 is V11() real ext-real set
(a,s1) is V11() real ext-real set
(b,s1) is V11() real ext-real set
(a,b) * (b,s1) is V11() real ext-real set
(a,((a,b) * (b,s1))) is V11() real ext-real set
(a,(a,b)) is V11() real ext-real set
((a,(a,b)),(b,s1)) is V11() real ext-real set
(b,(b,s1)) is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
(a,b) is V11() real ext-real set
s1 is V11() real ext-real set
(a,s1) is V11() real ext-real set
(a,(a,b)) is V11() real ext-real set
(a,(a,s1)) is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
(a,b) is V11() real ext-real set
s1 is V11() real ext-real set
(a,s1) is V11() real ext-real set
(a,(a,b)) is V11() real ext-real set
(a,(a,s1)) is V11() real ext-real set
a is V21() V30( NAT , REAL ) Element of K6(K7(NAT,REAL))
b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
b + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / (b + 1) is V11() real ext-real non negative rational Element of REAL
(b + 1) " is V1() V11() real ext-real positive non negative rational set
1 * ((b + 1) ") is V11() real ext-real non negative rational set
1 + (1 / (b + 1)) is V1() V11() real ext-real positive non negative rational Element of REAL
((1 + (1 / (b + 1))),(b + 1)) is V11() real ext-real Element of REAL
(1 + (1 / (b + 1))) |^ (b + 1) is V11() real ext-real set
a . (b + 1) is V11() real ext-real Element of REAL
a . b is V11() real ext-real Element of REAL
(a . (b + 1)) / (a . b) is V11() real ext-real Element of REAL
(a . b) " is V11() real ext-real set
(a . (b + 1)) * ((a . b) ") is V11() real ext-real set
(b + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / ((b + 1) + 1) is V11() real ext-real non negative rational Element of REAL
((b + 1) + 1) " is V1() V11() real ext-real positive non negative rational set
1 * (((b + 1) + 1) ") is V11() real ext-real non negative rational set
1 + (1 / ((b + 1) + 1)) is V1() V11() real ext-real positive non negative rational Element of REAL
((1 + (1 / ((b + 1) + 1))),((b + 1) + 1)) is V11() real ext-real Element of REAL
(1 + (1 / ((b + 1) + 1))) |^ ((b + 1) + 1) is V11() real ext-real set
((1 + (1 / ((b + 1) + 1))),((b + 1) + 1)) / (a . b) is V11() real ext-real Element of REAL
((1 + (1 / ((b + 1) + 1))),((b + 1) + 1)) * ((a . b) ") is V11() real ext-real set
((1 + (1 / ((b + 1) + 1))),((b + 1) + 1)) / ((1 + (1 / (b + 1))),(b + 1)) is V11() real ext-real Element of REAL
((1 + (1 / (b + 1))),(b + 1)) " is V11() real ext-real set
((1 + (1 / ((b + 1) + 1))),((b + 1) + 1)) * (((1 + (1 / (b + 1))),(b + 1)) ") is V11() real ext-real set
(((1 + (1 / ((b + 1) + 1))),((b + 1) + 1)) / ((1 + (1 / (b + 1))),(b + 1))) * 1 is V11() real ext-real Element of REAL
(1 + (1 / (b + 1))) / (1 + (1 / (b + 1))) is V11() real ext-real non negative rational Element of REAL
(1 + (1 / (b + 1))) " is V1() V11() real ext-real positive non negative rational set
(1 + (1 / (b + 1))) * ((1 + (1 / (b + 1))) ") is V11() real ext-real non negative rational set
(((1 + (1 / ((b + 1) + 1))),((b + 1) + 1)) / ((1 + (1 / (b + 1))),(b + 1))) * ((1 + (1 / (b + 1))) / (1 + (1 / (b + 1)))) is V11() real ext-real Element of REAL
(1 + (1 / (b + 1))) * ((1 + (1 / ((b + 1) + 1))),((b + 1) + 1)) is V11() real ext-real Element of REAL
((1 + (1 / (b + 1))),(b + 1)) * (1 + (1 / (b + 1))) is V11() real ext-real Element of REAL
((1 + (1 / (b + 1))) * ((1 + (1 / ((b + 1) + 1))),((b + 1) + 1))) / (((1 + (1 / (b + 1))),(b + 1)) * (1 + (1 / (b + 1)))) is V11() real ext-real Element of REAL
(((1 + (1 / (b + 1))),(b + 1)) * (1 + (1 / (b + 1)))) " is V11() real ext-real set
((1 + (1 / (b + 1))) * ((1 + (1 / ((b + 1) + 1))),((b + 1) + 1))) * ((((1 + (1 / (b + 1))),(b + 1)) * (1 + (1 / (b + 1)))) ") is V11() real ext-real set
((1 + (1 / (b + 1))),1) is V11() real ext-real Element of REAL
(1 + (1 / (b + 1))) |^ 1 is V11() real ext-real set
((1 + (1 / (b + 1))),(b + 1)) * ((1 + (1 / (b + 1))),1) is V11() real ext-real Element of REAL
((1 + (1 / (b + 1))) * ((1 + (1 / ((b + 1) + 1))),((b + 1) + 1))) / (((1 + (1 / (b + 1))),(b + 1)) * ((1 + (1 / (b + 1))),1)) is V11() real ext-real Element of REAL
(((1 + (1 / (b + 1))),(b + 1)) * ((1 + (1 / (b + 1))),1)) " is V11() real ext-real set
((1 + (1 / (b + 1))) * ((1 + (1 / ((b + 1) + 1))),((b + 1) + 1))) * ((((1 + (1 / (b + 1))),(b + 1)) * ((1 + (1 / (b + 1))),1)) ") is V11() real ext-real set
((1 + (1 / (b + 1))),((b + 1) + 1)) is V11() real ext-real Element of REAL
(1 + (1 / (b + 1))) |^ ((b + 1) + 1) is V11() real ext-real set
((1 + (1 / (b + 1))) * ((1 + (1 / ((b + 1) + 1))),((b + 1) + 1))) / ((1 + (1 / (b + 1))),((b + 1) + 1)) is V11() real ext-real Element of REAL
((1 + (1 / (b + 1))),((b + 1) + 1)) " is V11() real ext-real set
((1 + (1 / (b + 1))) * ((1 + (1 / ((b + 1) + 1))),((b + 1) + 1))) * (((1 + (1 / (b + 1))),((b + 1) + 1)) ") is V11() real ext-real set
((1 + (1 / ((b + 1) + 1))),((b + 1) + 1)) / ((1 + (1 / (b + 1))),((b + 1) + 1)) is V11() real ext-real Element of REAL
((1 + (1 / ((b + 1) + 1))),((b + 1) + 1)) * (((1 + (1 / (b + 1))),((b + 1) + 1)) ") is V11() real ext-real set
(1 + (1 / (b + 1))) * (((1 + (1 / ((b + 1) + 1))),((b + 1) + 1)) / ((1 + (1 / (b + 1))),((b + 1) + 1))) is V11() real ext-real Element of REAL
(1 + (1 / ((b + 1) + 1))) / (1 + (1 / (b + 1))) is V11() real ext-real non negative rational Element of REAL
(1 + (1 / ((b + 1) + 1))) * ((1 + (1 / (b + 1))) ") is V11() real ext-real non negative rational set
(((1 + (1 / ((b + 1) + 1))) / (1 + (1 / (b + 1)))),((b + 1) + 1)) is V11() real ext-real Element of REAL
((1 + (1 / ((b + 1) + 1))) / (1 + (1 / (b + 1)))) |^ ((b + 1) + 1) is V11() real ext-real set
(1 + (1 / (b + 1))) * (((1 + (1 / ((b + 1) + 1))) / (1 + (1 / (b + 1)))),((b + 1) + 1)) is V11() real ext-real Element of REAL
1 * ((b + 1) + 1) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(1 * ((b + 1) + 1)) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((1 * ((b + 1) + 1)) + 1) / ((b + 1) + 1) is V11() real ext-real non negative rational Element of REAL
((1 * ((b + 1) + 1)) + 1) * (((b + 1) + 1) ") is V11() real ext-real non negative rational set
(((1 * ((b + 1) + 1)) + 1) / ((b + 1) + 1)) / (1 + (1 / (b + 1))) is V11() real ext-real non negative rational Element of REAL
(((1 * ((b + 1) + 1)) + 1) / ((b + 1) + 1)) * ((1 + (1 / (b + 1))) ") is V11() real ext-real non negative rational set
((b + 1) + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(((b + 1) + 1) + 1) / ((b + 1) + 1) is V11() real ext-real non negative rational Element of REAL
(((b + 1) + 1) + 1) * (((b + 1) + 1) ") is V11() real ext-real non negative rational set
1 * (b + 1) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(1 * (b + 1)) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((1 * (b + 1)) + 1) / (b + 1) is V11() real ext-real non negative rational Element of REAL
((1 * (b + 1)) + 1) * ((b + 1) ") is V11() real ext-real non negative rational set
((((b + 1) + 1) + 1) / ((b + 1) + 1)) / (((1 * (b + 1)) + 1) / (b + 1)) is V11() real ext-real non negative rational Element of REAL
(((1 * (b + 1)) + 1) / (b + 1)) " is V11() real ext-real non negative rational set
((((b + 1) + 1) + 1) / ((b + 1) + 1)) * ((((1 * (b + 1)) + 1) / (b + 1)) ") is V11() real ext-real non negative rational set
1 + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
b + (1 + 1) is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(b + (1 + 1)) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((b + (1 + 1)) + 1) * (b + 1) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
b + 2 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(b + 2) * (b + 2) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(((b + (1 + 1)) + 1) * (b + 1)) / ((b + 2) * (b + 2)) is V11() real ext-real non negative rational Element of REAL
((b + 2) * (b + 2)) " is V11() real ext-real non negative rational set
(((b + (1 + 1)) + 1) * (b + 1)) * (((b + 2) * (b + 2)) ") is V11() real ext-real non negative rational set
b * b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
b * 2 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(b * b) + (b * 2) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
((b * b) + (b * 2)) + (2 * b) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
3 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(((b * b) + (b * 2)) + (2 * b)) + 3 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((((b * b) + (b * 2)) + (2 * b)) + 3) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(((((b * b) + (b * 2)) + (2 * b)) + 3) + 1) - 1 is V11() real ext-real integer rational Element of REAL
- 1 is V11() real ext-real non positive integer rational set
(((((b * b) + (b * 2)) + (2 * b)) + 3) + 1) + (- 1) is V11() real ext-real integer rational set
((((((b * b) + (b * 2)) + (2 * b)) + 3) + 1) - 1) / ((b + 2) * (b + 2)) is V11() real ext-real rational Element of REAL
((((((b * b) + (b * 2)) + (2 * b)) + 3) + 1) - 1) * (((b + 2) * (b + 2)) ") is V11() real ext-real rational set
((b + 2) * (b + 2)) / ((b + 2) * (b + 2)) is V11() real ext-real non negative rational Element of REAL
((b + 2) * (b + 2)) * (((b + 2) * (b + 2)) ") is V11() real ext-real non negative rational set
1 / ((b + 2) * (b + 2)) is V11() real ext-real non negative rational Element of REAL
1 * (((b + 2) * (b + 2)) ") is V11() real ext-real non negative rational set
(((b + 2) * (b + 2)) / ((b + 2) * (b + 2))) - (1 / ((b + 2) * (b + 2))) is V11() real ext-real rational Element of REAL
- (1 / ((b + 2) * (b + 2))) is V11() real ext-real non positive rational set
(((b + 2) * (b + 2)) / ((b + 2) * (b + 2))) + (- (1 / ((b + 2) * (b + 2)))) is V11() real ext-real rational set
1 - (1 / ((b + 2) * (b + 2))) is V11() real ext-real rational Element of REAL
1 + (- (1 / ((b + 2) * (b + 2)))) is V11() real ext-real rational set
0 + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
- (1 / ((b + 2) * (b + 2))) is V11() real ext-real non positive rational Element of REAL
((b + 1) + 1) * (- (1 / ((b + 2) * (b + 2)))) is V11() real ext-real non positive rational Element of REAL
1 + (((b + 1) + 1) * (- (1 / ((b + 2) * (b + 2))))) is V11() real ext-real rational Element of REAL
1 + (- (1 / ((b + 2) * (b + 2)))) is V11() real ext-real rational Element of REAL
((1 + (- (1 / ((b + 2) * (b + 2))))),((b + 1) + 1)) is V11() real ext-real Element of REAL
(1 + (- (1 / ((b + 2) * (b + 2))))) |^ ((b + 1) + 1) is V11() real ext-real set
(b + 2) * 1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((b + 2) * 1) / ((b + 2) * (b + 2)) is V11() real ext-real non negative rational Element of REAL
((b + 2) * 1) * (((b + 2) * (b + 2)) ") is V11() real ext-real non negative rational set
1 - (((b + 2) * 1) / ((b + 2) * (b + 2))) is V11() real ext-real rational Element of REAL
- (((b + 2) * 1) / ((b + 2) * (b + 2))) is V11() real ext-real non positive rational set
1 + (- (((b + 2) * 1) / ((b + 2) * (b + 2)))) is V11() real ext-real rational set
((1 - (1 / ((b + 2) * (b + 2)))),((b + 1) + 1)) is V11() real ext-real Element of REAL
(1 - (1 / ((b + 2) * (b + 2)))) |^ ((b + 1) + 1) is V11() real ext-real set
(b + 2) / (b + 2) is V11() real ext-real non negative rational Element of REAL
(b + 2) " is V1() V11() real ext-real positive non negative rational set
(b + 2) * ((b + 2) ") is V11() real ext-real non negative rational set
((b + 2) / (b + 2)) * 1 is V11() real ext-real non negative rational Element of REAL
(((b + 2) / (b + 2)) * 1) / (b + 2) is V11() real ext-real non negative rational Element of REAL
(((b + 2) / (b + 2)) * 1) * ((b + 2) ") is V11() real ext-real non negative rational set
1 - ((((b + 2) / (b + 2)) * 1) / (b + 2)) is V11() real ext-real rational Element of REAL
- ((((b + 2) / (b + 2)) * 1) / (b + 2)) is V11() real ext-real non positive rational set
1 + (- ((((b + 2) / (b + 2)) * 1) / (b + 2))) is V11() real ext-real rational set
1 * 1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(1 * 1) / (b + 2) is V11() real ext-real non negative rational Element of REAL
(1 * 1) * ((b + 2) ") is V11() real ext-real non negative rational set
1 - ((1 * 1) / (b + 2)) is V11() real ext-real rational Element of REAL
- ((1 * 1) / (b + 2)) is V11() real ext-real non positive rational set
1 + (- ((1 * 1) / (b + 2))) is V11() real ext-real rational set
1 / (b + 2) is V11() real ext-real non negative rational Element of REAL
1 * ((b + 2) ") is V11() real ext-real non negative rational set
1 - (1 / (b + 2)) is V11() real ext-real rational Element of REAL
- (1 / (b + 2)) is V11() real ext-real non positive rational set
1 + (- (1 / (b + 2))) is V11() real ext-real rational set
(1 + (1 / (b + 1))) * (1 - (1 / (b + 2))) is V11() real ext-real rational Element of REAL
(((1 * (b + 1)) + 1) / (b + 1)) * (1 - (1 / (b + 2))) is V11() real ext-real rational Element of REAL
(b + 2) / (b + 1) is V11() real ext-real non negative rational Element of REAL
(b + 2) * ((b + 1) ") is V11() real ext-real non negative rational set
1 * (b + 2) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(1 * (b + 2)) - 1 is V11() real ext-real integer rational Element of REAL
(1 * (b + 2)) + (- 1) is V11() real ext-real integer rational set
((1 * (b + 2)) - 1) / (b + 2) is V11() real ext-real rational Element of REAL
((1 * (b + 2)) - 1) * ((b + 2) ") is V11() real ext-real rational set
((b + 2) / (b + 1)) * (((1 * (b + 2)) - 1) / (b + 2)) is V11() real ext-real rational Element of REAL
(b + 1) * (b + 2) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((b + 1) * (b + 2)) / ((b + 1) * (b + 2)) is V11() real ext-real non negative rational Element of REAL
((b + 1) * (b + 2)) " is V11() real ext-real non negative rational set
((b + 1) * (b + 2)) * (((b + 1) * (b + 2)) ") is V11() real ext-real non negative rational set
b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
b + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 * (b + 1) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
b + (b + 1) is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
a . (b + (b + 1)) is V11() real ext-real Element of REAL
2 * b is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(2 * b) + (1 + 1) is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / ((2 * b) + (1 + 1)) is V11() real ext-real non negative rational Element of REAL
((2 * b) + (1 + 1)) " is V1() V11() real ext-real positive non negative rational set
1 * (((2 * b) + (1 + 1)) ") is V11() real ext-real non negative rational set
1 + (1 / ((2 * b) + (1 + 1))) is V1() V11() real ext-real positive non negative rational Element of REAL
(2 * b) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
((2 * b) + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
((1 + (1 / ((2 * b) + (1 + 1)))),(((2 * b) + 1) + 1)) is V11() real ext-real Element of REAL
(1 + (1 / ((2 * b) + (1 + 1)))) |^ (((2 * b) + 1) + 1) is V11() real ext-real set
1 / (2 * (b + 1)) is V11() real ext-real non negative rational Element of REAL
(2 * (b + 1)) " is V11() real ext-real non negative rational set
1 * ((2 * (b + 1)) ") is V11() real ext-real non negative rational set
1 + (1 / (2 * (b + 1))) is V1() V11() real ext-real positive non negative rational Element of REAL
((1 + (1 / (2 * (b + 1)))),(b + 1)) is V11() real ext-real Element of REAL
(1 + (1 / (2 * (b + 1)))) |^ (b + 1) is V11() real ext-real set
(((1 + (1 / (2 * (b + 1)))),(b + 1)),2) is V11() real ext-real Element of REAL
((1 + (1 / (2 * (b + 1)))),(b + 1)) |^ 2 is V11() real ext-real set
(2 * (b + 1)) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
1 / ((2 * (b + 1)) + 1) is V11() real ext-real non negative rational Element of REAL
((2 * (b + 1)) + 1) " is V1() V11() real ext-real positive non negative rational set
1 * (((2 * (b + 1)) + 1) ") is V11() real ext-real non negative rational set
- (1 / ((2 * (b + 1)) + 1)) is V11() real ext-real non positive rational Element of REAL
(- (1 / ((2 * (b + 1)) + 1))) + 1 is V11() real ext-real rational Element of REAL
(- 1) + 1 is V11() real ext-real integer rational Element of REAL
1 / (1 + (1 / (2 * (b + 1)))) is V11() real ext-real non negative rational Element of REAL
(1 + (1 / (2 * (b + 1)))) " is V1() V11() real ext-real positive non negative rational set
1 * ((1 + (1 / (2 * (b + 1)))) ") is V11() real ext-real non negative rational set
1 / (1 / (1 + (1 / (2 * (b + 1))))) is V11() real ext-real non negative rational Element of REAL
(1 / (1 + (1 / (2 * (b + 1))))) " is V11() real ext-real non negative rational set
1 * ((1 / (1 + (1 / (2 * (b + 1))))) ") is V11() real ext-real non negative rational set
((1 / (1 / (1 + (1 / (2 * (b + 1)))))),(b + 1)) is V11() real ext-real Element of REAL
(1 / (1 / (1 + (1 / (2 * (b + 1)))))) |^ (b + 1) is V11() real ext-real set
- (b + 1) is V11() real ext-real non positive integer rational Element of REAL
((1 / (1 + (1 / (2 * (b + 1))))),(- (b + 1))) is V11() real ext-real Element of REAL
1 * (2 * (b + 1)) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(1 * (2 * (b + 1))) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
((1 * (2 * (b + 1))) + 1) / (2 * (b + 1)) is V11() real ext-real non negative rational Element of REAL
((1 * (2 * (b + 1))) + 1) * ((2 * (b + 1)) ") is V11() real ext-real non negative rational set
1 / (((1 * (2 * (b + 1))) + 1) / (2 * (b + 1))) is V11() real ext-real non negative rational Element of REAL
(((1 * (2 * (b + 1))) + 1) / (2 * (b + 1))) " is V11() real ext-real non negative rational set
1 * ((((1 * (2 * (b + 1))) + 1) / (2 * (b + 1))) ") is V11() real ext-real non negative rational set
((1 / (((1 * (2 * (b + 1))) + 1) / (2 * (b + 1)))),(- (b + 1))) is V11() real ext-real Element of REAL
((2 * (b + 1)) + 1) - 1 is V11() real ext-real integer rational even Element of REAL
((2 * (b + 1)) + 1) + (- 1) is V11() real ext-real integer rational set
(((2 * (b + 1)) + 1) - 1) / ((2 * (b + 1)) + 1) is V11() real ext-real rational Element of REAL
(((2 * (b + 1)) + 1) - 1) * (((2 * (b + 1)) + 1) ") is V11() real ext-real rational set
(((((2 * (b + 1)) + 1) - 1) / ((2 * (b + 1)) + 1)),(- (b + 1))) is V11() real ext-real Element of REAL
((2 * (b + 1)) + 1) / ((2 * (b + 1)) + 1) is V11() real ext-real non negative rational Element of REAL
((2 * (b + 1)) + 1) * (((2 * (b + 1)) + 1) ") is V11() real ext-real non negative rational set
(((2 * (b + 1)) + 1) / ((2 * (b + 1)) + 1)) - (1 / ((2 * (b + 1)) + 1)) is V11() real ext-real rational Element of REAL
- (1 / ((2 * (b + 1)) + 1)) is V11() real ext-real non positive rational set
(((2 * (b + 1)) + 1) / ((2 * (b + 1)) + 1)) + (- (1 / ((2 * (b + 1)) + 1))) is V11() real ext-real rational set
(((((2 * (b + 1)) + 1) / ((2 * (b + 1)) + 1)) - (1 / ((2 * (b + 1)) + 1))),(- (b + 1))) is V11() real ext-real Element of REAL
1 - (1 / ((2 * (b + 1)) + 1)) is V11() real ext-real rational Element of REAL
1 + (- (1 / ((2 * (b + 1)) + 1))) is V11() real ext-real rational set
((1 - (1 / ((2 * (b + 1)) + 1))),(- (b + 1))) is V11() real ext-real Element of REAL
((1 - (1 / ((2 * (b + 1)) + 1))),(b + 1)) is V11() real ext-real Element of REAL
(1 - (1 / ((2 * (b + 1)) + 1))) |^ (b + 1) is V11() real ext-real set
1 / ((1 - (1 / ((2 * (b + 1)) + 1))),(b + 1)) is V11() real ext-real Element of REAL
((1 - (1 / ((2 * (b + 1)) + 1))),(b + 1)) " is V11() real ext-real set
1 * (((1 - (1 / ((2 * (b + 1)) + 1))),(b + 1)) ") is V11() real ext-real set
(b + 1) * (- (1 / ((2 * (b + 1)) + 1))) is V11() real ext-real non positive rational Element of REAL
1 + ((b + 1) * (- (1 / ((2 * (b + 1)) + 1)))) is V11() real ext-real rational Element of REAL
1 + (- (1 / ((2 * (b + 1)) + 1))) is V11() real ext-real rational Element of REAL
((1 + (- (1 / ((2 * (b + 1)) + 1)))),(b + 1)) is V11() real ext-real Element of REAL
(1 + (- (1 / ((2 * (b + 1)) + 1)))) |^ (b + 1) is V11() real ext-real set
(b + 1) / ((2 * (b + 1)) + 1) is V11() real ext-real non negative rational Element of REAL
(b + 1) * (((2 * (b + 1)) + 1) ") is V11() real ext-real non negative rational set
1 - ((b + 1) / ((2 * (b + 1)) + 1)) is V11() real ext-real rational Element of REAL
- ((b + 1) / ((2 * (b + 1)) + 1)) is V11() real ext-real non positive rational set
1 + (- ((b + 1) / ((2 * (b + 1)) + 1))) is V11() real ext-real rational set
1 * ((2 * (b + 1)) + 1) is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(1 * ((2 * (b + 1)) + 1)) - (b + 1) is V11() real ext-real integer rational Element of REAL
- (b + 1) is V11() real ext-real non positive integer rational set
(1 * ((2 * (b + 1)) + 1)) + (- (b + 1)) is V11() real ext-real integer rational set
((1 * ((2 * (b + 1)) + 1)) - (b + 1)) / ((2 * (b + 1)) + 1) is V11() real ext-real rational Element of REAL
((1 * ((2 * (b + 1)) + 1)) - (b + 1)) * (((2 * (b + 1)) + 1) ") is V11() real ext-real rational set
1 / 2 is V11() real ext-real non negative rational Element of REAL
2 " is V1() V11() real ext-real positive non negative rational set
1 * (2 ") is V11() real ext-real non negative rational set
(2 * (b + 1)) - b is V11() real ext-real integer rational Element of REAL
- b is V11() real ext-real non positive integer rational set
(2 * (b + 1)) + (- b) is V11() real ext-real integer rational set
((2 * (b + 1)) - b) / ((2 * (b + 1)) + 1) is V11() real ext-real rational Element of REAL
((2 * (b + 1)) - b) * (((2 * (b + 1)) + 1) ") is V11() real ext-real rational set
((2 * (b + 1)) + 1) * 1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((2 * (b + 1)) - b) * 2 is V11() real ext-real integer rational even Element of REAL
(- b) + ((2 * (b + 1)) - b) is V11() real ext-real integer rational Element of REAL
(2 * (b + 1)) + ((- b) + ((2 * (b + 1)) - b)) is V11() real ext-real integer rational Element of REAL
1 / (1 / 2) is V11() real ext-real non negative rational Element of REAL
(1 / 2) " is V11() real ext-real non negative rational set
1 * ((1 / 2) ") is V11() real ext-real non negative rational set
((1 + (1 / (2 * (b + 1)))),(b + 1)) ^2 is V11() real ext-real Element of REAL
((1 + (1 / (2 * (b + 1)))),(b + 1)) * ((1 + (1 / (2 * (b + 1)))),(b + 1)) is V11() real ext-real set
2 * 2 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
a . b is V11() real ext-real Element of REAL
(2 * 2) + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() non even Element of NAT
a is V21() V30( NAT , REAL ) Element of K6(K7(NAT,REAL))
lim a is V11() real ext-real Element of REAL
b is V21() V30( NAT , REAL ) Element of K6(K7(NAT,REAL))
lim b is V11() real ext-real Element of REAL
s1 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
a . s1 is V11() real ext-real Element of REAL
s1 + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / (s1 + 1) is V11() real ext-real non negative rational Element of REAL
(s1 + 1) " is V1() V11() real ext-real positive non negative rational set
1 * ((s1 + 1) ") is V11() real ext-real non negative rational set
1 + (1 / (s1 + 1)) is V1() V11() real ext-real positive non negative rational Element of REAL
((1 + (1 / (s1 + 1))),(s1 + 1)) is V11() real ext-real Element of REAL
(1 + (1 / (s1 + 1))) |^ (s1 + 1) is V11() real ext-real set
b . s1 is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
s1 is V21() V30( NAT , REAL ) Element of K6(K7(NAT,REAL))
lim s1 is V11() real ext-real Element of REAL
() is V11() real ext-real set
(2,2) is V11() real ext-real Element of REAL
2 |^ 2 is ordinal natural V11() real ext-real non negative integer rational set
4 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 ^2 is V11() real ext-real Element of REAL
2 * 2 is ordinal natural V11() real ext-real non negative integer rational even set
3 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(2,3) is V11() real ext-real Element of REAL
2 |^ 3 is ordinal natural V11() real ext-real non negative integer rational set
8 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 + 1 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(2,(2 + 1)) is V11() real ext-real Element of REAL
2 |^ (2 + 1) is ordinal natural V11() real ext-real non negative integer rational set
(2,1) is V11() real ext-real Element of REAL
2 |^ 1 is ordinal natural V11() real ext-real non negative integer rational set
(2,2) * (2,1) is V11() real ext-real Element of REAL
4 * 2 is ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() even Element of NAT
(2,4) is V11() real ext-real Element of REAL
2 |^ 4 is ordinal natural V11() real ext-real non negative integer rational set
16 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 + 2 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(2,(2 + 2)) is V11() real ext-real Element of REAL
2 |^ (2 + 2) is ordinal natural V11() real ext-real non negative integer rational set
(2,2) * (2,2) is V11() real ext-real Element of REAL
5 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(2,5) is V11() real ext-real Element of REAL
2 |^ 5 is ordinal natural V11() real ext-real non negative integer rational set
32 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
3 + 2 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(2,(3 + 2)) is V11() real ext-real Element of REAL
2 |^ (3 + 2) is ordinal natural V11() real ext-real non negative integer rational set
(2,3) * (2,2) is V11() real ext-real Element of REAL
6 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(2,6) is V11() real ext-real Element of REAL
2 |^ 6 is ordinal natural V11() real ext-real non negative integer rational set
64 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
3 + 3 is V1() ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(2,(3 + 3)) is V11() real ext-real Element of REAL
2 |^ (3 + 3) is ordinal natural V11() real ext-real non negative integer rational set
(2,3) * (2,3) is V11() real ext-real Element of REAL