REAL is V11() V51() V52() V53() V57() V58() set
NAT is V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() Element of K19(REAL)
K19(REAL) is set
COMPLEX is V11() V51() V57() V58() set
RAT is V11() V51() V52() V53() V54() V57() V58() set
INT is V11() V51() V52() V53() V54() V55() V57() V58() set
omega is V11() epsilon-transitive epsilon-connected ordinal V51() V52() V53() V54() V55() V56() V57() set
K19(omega) is set
K19(NAT) is set
K20(COMPLEX,COMPLEX) is complex-valued set
K19(K20(COMPLEX,COMPLEX)) is set
K20(COMPLEX,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(COMPLEX,REAL)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(REAL,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) is set
K20(K20(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(K20(NAT,NAT),NAT)) is set
1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
0 is V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() set
0 is V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() Element of NAT
K20(NAT,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
2 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
0 " is V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() set
l is V30() real ext-real integer rational set
abs l is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l is V30() real ext-real set
k is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim k is V30() real ext-real Element of REAL
NAT --> l is Relation-like NAT -defined {l} -valued Function-like constant V11() V14( NAT ) V18( NAT ,{l}) T-Sequence-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,{l}))
{l} is V11() V51() V52() V53() set
K20(NAT,{l}) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,{l})) is set
y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
k . y is V30() real ext-real Element of REAL
x is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
x . y is V30() real ext-real Element of REAL
lim x is V30() real ext-real Element of REAL
x . 0 is V30() real ext-real Element of REAL
l is V30() real ext-real set
k is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim k is V30() real ext-real Element of REAL
NAT --> l is Relation-like NAT -defined {l} -valued Function-like constant V11() V14( NAT ) V18( NAT ,{l}) T-Sequence-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,{l}))
{l} is V11() V51() V52() V53() set
K20(NAT,{l}) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,{l})) is set
y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
k . y is V30() real ext-real Element of REAL
x is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
x . y is V30() real ext-real Element of REAL
lim x is V30() real ext-real Element of REAL
x . 0 is V30() real ext-real Element of REAL
l is V30() real ext-real set
k is V30() real ext-real Element of REAL
x is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
x is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
k . y is V30() real ext-real Element of REAL
x . y is V30() real ext-real Element of REAL
l |^ y is V30() real ext-real set
l is V30() real ext-real set
(l) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k . 0 is V30() real ext-real Element of REAL
l |^ 0 is V30() real ext-real set
x is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
x + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
k . (x + 1) is V30() real ext-real Element of REAL
l |^ (x + 1) is V30() real ext-real set
l |^ x is V30() real ext-real set
(l |^ x) * l is V30() real ext-real set
k . x is V30() real ext-real Element of REAL
(k . x) * l is V30() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
k . x is V30() real ext-real Element of REAL
(l) . x is V30() real ext-real Element of REAL
x + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
k . (x + 1) is V30() real ext-real Element of REAL
(l) . (x + 1) is V30() real ext-real Element of REAL
(k . x) * l is V30() real ext-real Element of REAL
l |^ x is V30() real ext-real set
(l |^ x) * l is V30() real ext-real set
l |^ (x + 1) is V30() real ext-real set
(l) . 0 is V30() real ext-real Element of REAL
l is V30() real ext-real set
(l) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(l) . k is V30() real ext-real Element of REAL
k + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(l) . (k + 1) is V30() real ext-real Element of REAL
((l) . k) * l is V30() real ext-real Element of REAL
(l) . 0 is V30() real ext-real Element of REAL
l is V30() real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
l |^ k is V30() real ext-real set
x is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
l |^ x is V30() real ext-real set
x + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ (x + 1) is V30() real ext-real set
(l |^ x) * l is V30() real ext-real set
l |^ 0 is V30() real ext-real set
l is V30() real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
l |^ k is V30() real ext-real set
x is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
l |^ x is V30() real ext-real set
x + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ (x + 1) is V30() real ext-real set
(l |^ x) * l is V30() real ext-real set
0 * l is V30() real ext-real Element of REAL
l |^ 0 is V30() real ext-real set
l is V30() real ext-real set
1 / l is V30() real ext-real Element of REAL
l " is V30() real ext-real set
1 * (l ") is V30() real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
(1 / l) |^ k is V30() real ext-real Element of REAL
l |^ k is V30() real ext-real set
1 / (l |^ k) is V30() real ext-real Element of REAL
(l |^ k) " is V30() real ext-real set
1 * ((l |^ k) ") is V30() real ext-real set
x is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
(1 / l) |^ x is V30() real ext-real Element of REAL
l |^ x is V30() real ext-real set
1 / (l |^ x) is V30() real ext-real Element of REAL
(l |^ x) " is V30() real ext-real set
1 * ((l |^ x) ") is V30() real ext-real set
x + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(1 / l) |^ (x + 1) is V30() real ext-real Element of REAL
l |^ (x + 1) is V30() real ext-real set
1 / (l |^ (x + 1)) is V30() real ext-real Element of REAL
(l |^ (x + 1)) " is V30() real ext-real set
1 * ((l |^ (x + 1)) ") is V30() real ext-real set
(1 / (l |^ x)) * (1 / l) is V30() real ext-real Element of REAL
1 * 1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(l |^ x) * l is V30() real ext-real set
(1 * 1) / ((l |^ x) * l) is V30() real ext-real Element of REAL
((l |^ x) * l) " is V30() real ext-real set
(1 * 1) * (((l |^ x) * l) ") is V30() real ext-real set
(1 / l) |^ 0 is V30() real ext-real Element of REAL
((1 / l)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((1 / l)) . 0 is V30() real ext-real Element of REAL
1 / 1 is V30() real ext-real non negative rational Element of REAL
1 " is V11() V30() real ext-real positive non negative rational set
1 * (1 ") is V30() real ext-real non negative rational set
(l) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(l) . 0 is V30() real ext-real Element of REAL
1 / ((l) . 0) is V30() real ext-real Element of REAL
((l) . 0) " is V30() real ext-real set
1 * (((l) . 0) ") is V30() real ext-real set
l |^ 0 is V30() real ext-real set
1 / (l |^ 0) is V30() real ext-real Element of REAL
(l |^ 0) " is V30() real ext-real set
1 * ((l |^ 0) ") is V30() real ext-real set
l is V30() real ext-real set
k is V30() real ext-real set
l / k is V30() real ext-real Element of COMPLEX
k " is V30() real ext-real set
l * (k ") is V30() real ext-real set
x is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
(l / k) |^ x is V30() real ext-real set
l |^ x is V30() real ext-real set
k |^ x is V30() real ext-real set
(l |^ x) / (k |^ x) is V30() real ext-real Element of COMPLEX
(k |^ x) " is V30() real ext-real set
(l |^ x) * ((k |^ x) ") is V30() real ext-real set
(l * (k ")) |^ x is V30() real ext-real set
(k ") |^ x is V30() real ext-real set
(l |^ x) * ((k ") |^ x) is V30() real ext-real set
1 / k is V30() real ext-real Element of REAL
1 * (k ") is V30() real ext-real set
(1 / k) |^ x is V30() real ext-real Element of REAL
(l |^ x) * ((1 / k) |^ x) is V30() real ext-real Element of REAL
1 / (k |^ x) is V30() real ext-real Element of REAL
1 * ((k |^ x) ") is V30() real ext-real set
(l |^ x) * (1 / (k |^ x)) is V30() real ext-real Element of REAL
(l |^ x) * 1 is V30() real ext-real Element of REAL
((l |^ x) * 1) / (k |^ x) is V30() real ext-real Element of REAL
((l |^ x) * 1) * ((k |^ x) ") is V30() real ext-real set
l is V30() real ext-real set
k is V30() real ext-real set
x is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
l |^ x is V30() real ext-real set
k |^ x is V30() real ext-real set
y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
l |^ y is V30() real ext-real set
k |^ y is V30() real ext-real set
y + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ (y + 1) is V30() real ext-real set
k |^ (y + 1) is V30() real ext-real set
(l |^ y) * l is V30() real ext-real set
(k |^ y) * k is V30() real ext-real set
k |^ 0 is V30() real ext-real set
(k) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(k) . 0 is V30() real ext-real Element of REAL
l |^ 0 is V30() real ext-real set
(l) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(l) . 0 is V30() real ext-real Element of REAL
l is V30() real ext-real set
k is V30() real ext-real set
x is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
k |^ x is V30() real ext-real set
l |^ x is V30() real ext-real set
y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
1 + y is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
nn is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
1 + nn is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
k |^ (1 + nn) is V30() real ext-real set
l |^ (1 + nn) is V30() real ext-real set
nn + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
1 + (nn + 1) is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
k |^ (1 + (nn + 1)) is V30() real ext-real set
l |^ (1 + (nn + 1)) is V30() real ext-real set
(k |^ (1 + nn)) * k is V30() real ext-real set
(l |^ (1 + nn)) * l is V30() real ext-real set
(1 + nn) + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ ((1 + nn) + 1) is V30() real ext-real set
1 + 0 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
k |^ (1 + 0) is V30() real ext-real set
(k) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
0 + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(k) . (0 + 1) is V30() real ext-real Element of REAL
(k) . 0 is V30() real ext-real Element of REAL
((k) . 0) * k is V30() real ext-real Element of REAL
1 * k is V30() real ext-real Element of REAL
l |^ (1 + 0) is V30() real ext-real set
(l) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(l) . (0 + 1) is V30() real ext-real Element of REAL
(l) . 0 is V30() real ext-real Element of REAL
((l) . 0) * l is V30() real ext-real Element of REAL
1 * l is V30() real ext-real Element of REAL
l is V30() real ext-real set
k is V30() real ext-real set
x is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
k |^ x is V30() real ext-real set
l |^ x is V30() real ext-real set
y is V30() real ext-real integer rational set
nn is V30() real ext-real integer rational set
y - nn is V30() real ext-real integer rational set
- nn is V30() real ext-real integer rational set
y + (- nn) is V30() real ext-real integer rational set
mn is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
mn + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ (mn + 1) is V30() real ext-real set
l |^ mn is V30() real ext-real set
l |^ 1 is V30() real ext-real set
(l |^ mn) * (l |^ 1) is V30() real ext-real set
(l) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
0 + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(l) . (0 + 1) is V30() real ext-real Element of REAL
(l |^ mn) * ((l) . (0 + 1)) is V30() real ext-real Element of REAL
(l) . 0 is V30() real ext-real Element of REAL
((l) . 0) * 0 is V30() real ext-real Element of REAL
(l |^ mn) * (((l) . 0) * 0) is V30() real ext-real Element of REAL
l is V30() real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
l |^ k is V30() real ext-real set
1 |^ k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational Element of REAL
l is V30() real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
l |^ k is V30() real ext-real set
x is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
x + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
y + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ (y + 1) is V30() real ext-real set
(y + 1) + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ ((y + 1) + 1) is V30() real ext-real set
l * 1 is V30() real ext-real Element of REAL
(l |^ (y + 1)) * l is V30() real ext-real set
1 * l is V30() real ext-real Element of REAL
(l) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(l) . 0 is V30() real ext-real Element of REAL
((l) . 0) * l is V30() real ext-real Element of REAL
l |^ 0 is V30() real ext-real set
(l |^ 0) * l is V30() real ext-real set
0 + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ (0 + 1) is V30() real ext-real set
l is V30() real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
l |^ k is V30() real ext-real set
x is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
2 + x is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l * l is V30() real ext-real set
l * 1 is V30() real ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
2 + y is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ (2 + y) is V30() real ext-real set
y + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
2 + (y + 1) is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ (2 + (y + 1)) is V30() real ext-real set
(l |^ (2 + y)) * l is V30() real ext-real set
(2 + y) + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ ((2 + y) + 1) is V30() real ext-real set
2 + 0 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ (2 + 0) is V30() real ext-real set
(l) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
1 + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(l) . (1 + 1) is V30() real ext-real Element of REAL
0 + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(l) . (0 + 1) is V30() real ext-real Element of REAL
((l) . (0 + 1)) * l is V30() real ext-real Element of REAL
(l) . 0 is V30() real ext-real Element of REAL
((l) . 0) * l is V30() real ext-real Element of REAL
(((l) . 0) * l) * l is V30() real ext-real Element of REAL
1 * l is V30() real ext-real Element of REAL
(1 * l) * l is V30() real ext-real Element of REAL
l is V30() real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
l |^ k is V30() real ext-real set
x is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
1 + x is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l * l is V30() real ext-real set
l * 1 is V30() real ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
1 + y is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ (1 + y) is V30() real ext-real set
y + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
1 + (y + 1) is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ (1 + (y + 1)) is V30() real ext-real set
(l |^ (1 + y)) * l is V30() real ext-real set
1 + 0 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ (1 + 0) is V30() real ext-real set
(l) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
0 + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(l) . (0 + 1) is V30() real ext-real Element of REAL
(l) . 0 is V30() real ext-real Element of REAL
((l) . 0) * l is V30() real ext-real Element of REAL
1 * l is V30() real ext-real Element of REAL
l is V30() real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
l |^ k is V30() real ext-real set
x is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
2 + x is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l * 1 is V30() real ext-real Element of REAL
l * l is V30() real ext-real set
y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
2 + y is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ (2 + y) is V30() real ext-real set
y + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
2 + (y + 1) is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ (2 + (y + 1)) is V30() real ext-real set
(l |^ (2 + y)) * l is V30() real ext-real set
(2 + y) + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ ((2 + y) + 1) is V30() real ext-real set
2 + 0 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l |^ (2 + 0) is V30() real ext-real set
(l) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
1 + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(l) . (1 + 1) is V30() real ext-real Element of REAL
0 + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(l) . (0 + 1) is V30() real ext-real Element of REAL
((l) . (0 + 1)) * l is V30() real ext-real Element of REAL
(l) . 0 is V30() real ext-real Element of REAL
((l) . 0) * l is V30() real ext-real Element of REAL
(((l) . 0) * l) * l is V30() real ext-real Element of REAL
1 * l is V30() real ext-real Element of REAL
(1 * l) * l is V30() real ext-real Element of REAL
- 1 is V30() real ext-real non positive integer rational Element of REAL
l is V30() real ext-real set
1 + l is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
k * l is V30() real ext-real set
1 + (k * l) is V30() real ext-real Element of REAL
(1 + l) |^ k is V30() real ext-real Element of REAL
(- 1) + 1 is V30() real ext-real integer rational Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
x * l is V30() real ext-real set
1 + (x * l) is V30() real ext-real Element of REAL
(1 + l) |^ x is V30() real ext-real Element of REAL
x + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(x + 1) * l is V30() real ext-real set
1 + ((x + 1) * l) is V30() real ext-real Element of REAL
(1 + l) |^ (x + 1) is V30() real ext-real Element of REAL
(1 + (x * l)) * (1 + l) is V30() real ext-real Element of REAL
((1 + l) |^ x) * (1 + l) is V30() real ext-real Element of REAL
1 * l is V30() real ext-real Element of REAL
1 + (1 * l) is V30() real ext-real Element of REAL
(1 + (1 * l)) + (x * l) is V30() real ext-real Element of REAL
(x * l) * l is V30() real ext-real set
((1 + (1 * l)) + (x * l)) + ((x * l) * l) is V30() real ext-real Element of REAL
l * l is V30() real ext-real set
(x + 1) * l is V30() real ext-real Element of REAL
1 + ((x + 1) * l) is V30() real ext-real Element of REAL
(1 + ((x + 1) * l)) + 0 is V30() real ext-real Element of REAL
x * (l * l) is V30() real ext-real set
(1 + ((x + 1) * l)) + (x * (l * l)) is V30() real ext-real Element of REAL
(1 + l) |^ 0 is V30() real ext-real Element of REAL
((1 + l)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((1 + l)) . 0 is V30() real ext-real Element of REAL
0 * l is V30() real ext-real set
1 + (0 * l) is V30() real ext-real Element of REAL
3 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
l is V30() real ext-real set
1 + l is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
(1 + l) |^ k is V30() real ext-real Element of REAL
3 |^ k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational Element of REAL
(3 |^ k) * l is V30() real ext-real Element of REAL
1 + ((3 |^ k) * l) is V30() real ext-real Element of REAL
1 + 0 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
(1 + l) |^ x is V30() real ext-real Element of REAL
3 |^ x is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational Element of REAL
(3 |^ x) * l is V30() real ext-real Element of REAL
1 + ((3 |^ x) * l) is V30() real ext-real Element of REAL
x + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(1 + l) |^ (x + 1) is V30() real ext-real Element of REAL
3 |^ (x + 1) is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational Element of REAL
(3 |^ (x + 1)) * l is V30() real ext-real Element of REAL
1 + ((3 |^ (x + 1)) * l) is V30() real ext-real Element of REAL
((1 + l) |^ x) * (1 + l) is V30() real ext-real Element of REAL
(1 + ((3 |^ x) * l)) * (1 + l) is V30() real ext-real Element of REAL
(3 |^ x) + (3 |^ x) is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational Element of REAL
((3 |^ x) + (3 |^ x)) * l is V30() real ext-real Element of REAL
(1 + ((3 |^ x) * l)) + (((3 |^ x) + (3 |^ x)) * l) is V30() real ext-real Element of REAL
1 + 2 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(3 |^ x) * (1 + 2) is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
((3 |^ x) * (1 + 2)) * l is V30() real ext-real Element of REAL
1 + (((3 |^ x) * (1 + 2)) * l) is V30() real ext-real Element of REAL
3 |^ (x + 1) is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(3 |^ (x + 1)) * l is V30() real ext-real Element of REAL
1 + ((3 |^ (x + 1)) * l) is V30() real ext-real Element of REAL
(3) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(3) . x is V30() real ext-real Element of REAL
0 + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
1 |^ x is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational Element of REAL
1 * l is V30() real ext-real Element of REAL
l * l is V30() real ext-real set
(3 |^ x) * (l * l) is V30() real ext-real Element of REAL
((3 |^ x) * l) + ((3 |^ x) * l) is V30() real ext-real Element of REAL
((3 |^ x) * l) + ((3 |^ x) * (l * l)) is V30() real ext-real Element of REAL
(1 + l) + (((3 |^ x) * l) + ((3 |^ x) * (l * l))) is V30() real ext-real Element of REAL
3 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(3 |^ 0) * l is V30() real ext-real Element of REAL
1 + ((3 |^ 0) * l) is V30() real ext-real Element of REAL
(3) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(3) . 0 is V30() real ext-real Element of REAL
((3) . 0) * l is V30() real ext-real Element of REAL
1 + (((3) . 0) * l) is V30() real ext-real Element of REAL
1 * l is V30() real ext-real Element of REAL
1 + (1 * l) is V30() real ext-real Element of REAL
(1 + l) |^ 0 is V30() real ext-real Element of REAL
((1 + l)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((1 + l)) . 0 is V30() real ext-real Element of REAL
3 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational Element of REAL
(3 |^ 0) * l is V30() real ext-real Element of REAL
1 + ((3 |^ 0) * l) is V30() real ext-real Element of REAL
l is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
k is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim k is V30() real ext-real Element of REAL
(lim k) |^ l is V30() real ext-real Element of REAL
x is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim x is V30() real ext-real Element of REAL
(lim k) |^ 0 is V30() real ext-real Element of REAL
y is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim y is V30() real ext-real Element of REAL
nn is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
y . nn is V30() real ext-real Element of REAL
k . nn is V30() real ext-real Element of REAL
(k . nn) |^ 0 is V30() real ext-real Element of REAL
((k . nn)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((k . nn)) . 0 is V30() real ext-real Element of REAL
y . 0 is V30() real ext-real Element of REAL
((lim k)) is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((lim k)) . 0 is V30() real ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(lim k) |^ y is V30() real ext-real Element of REAL
y + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(lim k) |^ (y + 1) is V30() real ext-real Element of REAL
nn is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim nn is V30() real ext-real Element of REAL
mn is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m3 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
nn . m3 is V30() real ext-real Element of REAL
k . m3 is V30() real ext-real Element of REAL
(k . m3) |^ (y + 1) is V30() real ext-real Element of REAL
(k . m3) |^ y is V30() real ext-real Element of REAL
((k . m3) |^ y) * (k . m3) is V30() real ext-real Element of REAL
mn . m3 is V30() real ext-real Element of REAL
(mn . m3) * (k . m3) is V30() real ext-real Element of REAL
mn (#) k is Relation-like NAT -defined REAL -valued Function-like V11() V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim mn is V30() real ext-real Element of REAL
((lim k) |^ y) * (lim k) is V30() real ext-real Element of REAL
l is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational set
k is V30() real ext-real set
x is V30() real ext-real set
x |^ l is V30() real ext-real set
{ b1 where b1 is V30() real ext-real Element of REAL : ( not b1 <= 0 & b1 |^ l <= k ) } is set
y is set
nn is V30() real ext-real Element of REAL
nn |^ l is V30() real ext-real Element of REAL
y is V51() V52() V53() Element of K19(REAL)
mn is V30() real ext-real set
mn |^ l is V30() real ext-real set
mn is V30() real ext-real set
m3 is ext-real set
n is V30() real ext-real Element of REAL
n |^ l is V30() real ext-real Element of REAL
1 |^ l is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational Element of REAL
mn is ext-real set
m3 is V30() real ext-real Element of REAL
m3 |^ l is V30() real ext-real Element of REAL
k |^ l is V30() real ext-real set
mn is V30() real ext-real set
m3 is V30() real ext-real set
upper_bound y is V30() real ext-real Element of REAL
m3 is V30() real ext-real Element of REAL
m3 |^ l is V30() real ext-real Element of REAL
mn is V30() real ext-real Element of REAL
m3 is V30() real ext-real set
n is V30() real ext-real set
m3 is V30() real ext-real set
n is V30() real ext-real Element of REAL
n |^ l is V30() real ext-real Element of REAL
mn |^ l is V30() real ext-real Element of REAL
k / (mn |^ l) is V30() real ext-real Element of REAL
(mn |^ l) " is V30() real ext-real set
k * ((mn |^ l) ") is V30() real ext-real set
1 - (k / (mn |^ l)) is V30() real ext-real Element of REAL
- (k / (mn |^ l)) is V30() real ext-real set
1 + (- (k / (mn |^ l))) is V30() real ext-real set
mn * (1 - (k / (mn |^ l))) is V30() real ext-real Element of REAL
l + 1 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
(mn * (1 - (k / (mn |^ l)))) / (l + 1) is V30() real ext-real Element of REAL
(l + 1) " is V11() V30() real ext-real positive non negative rational set
(mn * (1 - (k / (mn |^ l)))) * ((l + 1) ") is V30() real ext-real set
1 / (l + 1) is V30() real ext-real non negative rational Element of REAL
1 * ((l + 1) ") is V30() real ext-real non negative rational set
(1 / (l + 1)) * (mn |^ l) is V30() real ext-real Element of REAL
(1 / (l + 1)) * k is V30() real ext-real Element of REAL
(mn |^ l) " is V30() real ext-real Element of REAL
k * ((mn |^ l) ") is V30() real ext-real Element of REAL
0 * k is V30() real ext-real Element of REAL
- (k / (mn |^ l)) is V30() real ext-real Element of REAL
- (- (k / (mn |^ l))) is V30() real ext-real Element of REAL
1 + 0 is V11() epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative integer rational V51() V52() V53() V54() V55() V56() Element of NAT
1 + (- (k / (mn |^ l))) is V30() real ext-real Element of REAL
(l + 1) " is V11() V30() real ext-real positive non negative rational Element of REAL
1 * ((l + 1) ") is V30() real ext-real non negative rational Element of REAL
(1 - (k / (mn |^ l))) * ((l + 1) ") is V30() real ext-real Element of REAL
(1 - (k / (mn |^ l))) / (l + 1) is V30() real ext-real Element of REAL
(1 - (k / (mn |^ l))) * ((l + 1) ") is V30() real ext-real set
mn * 1 is V30() real ext-real Element of REAL
mn * ((1 - (k / (mn |^ l))) / (l + 1)) is V30() real ext-real Element of REAL
mn / mn is V30() real ext-real Element of REAL
mn " is V30() real ext-real set
mn * (mn ") is V30() real ext-real set
((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn is V30() real ext-real Element of REAL
((mn * (1 - (k / (mn |^ l)))) / (l + 1)) * (mn ") is V30() real ext-real set
- (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn) is V30() real ext-real Element of REAL
l * (- (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn)) is V30() real ext-real Element of REAL
1 + (l * (- (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn))) is V30() real ext-real Element of REAL
1 + (- (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn)) is V30() real ext-real Element of REAL
(1 + (- (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn))) |^ l is V30() real ext-real Element of REAL
(mn |^ l) / (mn |^ l) is V30() real ext-real Element of REAL
(mn |^ l) * ((mn |^ l) ") is V30() real ext-real set
0 + (k / (mn |^ l)) is V30() real ext-real Element of REAL
mn * 0 is V30() real ext-real Element of REAL
0 / (l + 1) is V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() Element of REAL
0 * ((l + 1) ") is V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() set
mn - ((mn * (1 - (k / (mn |^ l)))) / (l + 1)) is V30() real ext-real Element of REAL
- ((mn * (1 - (k / (mn |^ l)))) / (l + 1)) is V30() real ext-real set
mn + (- ((mn * (1 - (k / (mn |^ l)))) / (l + 1))) is V30() real ext-real set
n is V30() real ext-real set
n is V30() real ext-real set
n is V30() real ext-real set
n |^ l is V30() real ext-real set
(mn - ((mn * (1 - (k / (mn |^ l)))) / (l + 1))) |^ l is V30() real ext-real Element of REAL
(1 + (l * (- (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn)))) * (mn |^ l) is V30() real ext-real Element of REAL
l * (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn) is V30() real ext-real Element of REAL
1 - (l * (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn)) is V30() real ext-real Element of REAL
- (l * (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn)) is V30() real ext-real set
1 + (- (l * (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn))) is V30() real ext-real set
(1 - (l * (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn))) * (mn |^ l) is V30() real ext-real Element of REAL
(mn * ((1 - (k / (mn |^ l))) / (l + 1))) / mn is V30() real ext-real Element of REAL
(mn * ((1 - (k / (mn |^ l))) / (l + 1))) * (mn ") is V30() real ext-real set
l * ((mn * ((1 - (k / (mn |^ l))) / (l + 1))) / mn) is V30() real ext-real Element of REAL
1 - (l * ((mn * ((1 - (k / (mn |^ l))) / (l + 1))) / mn)) is V30() real ext-real Element of REAL
- (l * ((mn * ((1 - (k / (mn |^ l))) / (l + 1))) / mn)) is V30() real ext-real set
1 + (- (l * ((mn * ((1 - (k / (mn |^ l))) / (l + 1))) / mn))) is V30() real ext-real set
(1 - (l * ((mn * ((1 - (k / (mn |^ l))) / (l + 1))) / mn))) * (mn |^ l) is V30() real ext-real Element of REAL
((1 - (k / (mn |^ l))) / (l + 1)) / mn is V30() real ext-real Element of REAL
((1 - (k / (mn |^ l))) / (l + 1)) * (mn ") is V30() real ext-real set
(((1 - (k / (mn |^ l))) / (l + 1)) / mn) * mn is V30() real ext-real Element of REAL
l * ((((1 - (k / (mn |^ l))) / (l + 1)) / mn) * mn) is V30() real ext-real Element of REAL
1 - (l * ((((1 - (k / (mn |^ l))) / (l + 1)) / mn) * mn)) is V30() real ext-real Element of REAL
- (l * ((((1 - (k / (mn |^ l))) / (l + 1)) / mn) * mn)) is V30() real ext-real set
1 + (- (l * ((((1 - (k / (mn |^ l))) / (l + 1)) / mn) * mn))) is V30() real ext-real set
(1 - (l * ((((1 - (k / (mn |^ l))) / (l + 1)) / mn) * mn))) * (mn |^ l) is V30() real ext-real Element of REAL
l * ((1 - (k / (mn |^ l))) / (l + 1)) is V30() real ext-real Element of REAL
1 - (l * ((1 - (k / (mn |^ l))) / (l + 1))) is V30() real ext-real Element of REAL
- (l * ((1 - (k / (mn |^ l))) / (l + 1))) is V30() real ext-real set
1 + (- (l * ((1 - (k / (mn |^ l))) / (l + 1)))) is V30() real ext-real set
(1 - (l * ((1 - (k / (mn |^ l))) / (l + 1)))) * (mn |^ l) is V30() real ext-real Element of REAL
(1 - (k / (mn |^ l))) * l is V30() real ext-real Element of REAL
((1 - (k / (mn |^ l))) * l) / (l + 1) is V30() real ext-real Element of REAL
((1 - (k / (mn |^ l))) * l) * ((l + 1) ") is V30() real ext-real set
1 - (((1 - (k / (mn |^ l))) * l) / (l + 1)) is V30() real ext-real Element of REAL
- (((1 - (k / (mn |^ l))) * l) / (l + 1)) is V30() real ext-real set
1 + (- (((1 - (k / (mn |^ l))) * l) / (l + 1))) is V30() real ext-real set
(1 - (((1 - (k / (mn |^ l))) * l) / (l + 1))) * (mn |^ l) is V30() real ext-real Element of REAL
l / (l + 1) is V30() real ext-real non negative rational Element of REAL
l * ((l + 1) ") is V30() real ext-real non negative rational set
(1 - (k / (mn |^ l))) * (l / (l + 1)) is V30() real ext-real Element of REAL
1 - ((1 - (k / (mn |^ l))) * (l / (l + 1))) is V30() real ext-real Element of REAL
- ((1 - (k / (mn |^ l))) * (l / (l + 1))) is V30() real ext-real set
1 + (- ((1 - (k / (mn |^ l))) * (l / (l + 1)))) is V30() real ext-real set
(1 - ((1 - (k / (mn |^ l))) * (l / (l + 1)))) * (mn |^ l) is V30() real ext-real Element of REAL
1 - (l / (l + 1)) is V30() real ext-real rational Element of REAL
- (l / (l + 1)) is V30() real ext-real non positive rational set
1 + (- (l / (l + 1))) is V30() real ext-real rational set
(k / (mn |^ l)) * (l / (l + 1)) is V30() real ext-real Element of REAL
(1 - (l / (l + 1))) + ((k / (mn |^ l)) * (l / (l + 1))) is V30() real ext-real Element of REAL
((1 - (l / (l + 1))) + ((k / (mn |^ l)) * (l / (l + 1)))) * (mn |^ l) is V30() real ext-real Element of REAL
(l + 1) / (l + 1) is V30() real ext-real non negative rational Element of REAL
(l + 1) * ((l + 1) ") is V30() real ext-real non negative rational set
((l + 1) / (l + 1)) - (l / (l + 1)) is V30() real ext-real rational Element of REAL
((l + 1) / (l + 1)) + (- (l / (l + 1))) is V30() real ext-real rational set
(((l + 1) / (l + 1)) - (l / (l + 1))) + ((k / (mn |^ l)) * (l / (l + 1))) is V30() real ext-real Element of REAL
((((l + 1) / (l + 1)) - (l / (l + 1))) + ((k / (mn |^ l)) * (l / (l + 1)))) * (mn |^ l) is V30() real ext-real Element of REAL
(l + 1) - l is V30() real ext-real integer rational Element of REAL
- l is V30() real ext-real non positive integer rational set
(l + 1) + (- l) is V30() real ext-real integer rational set
((l + 1) - l) / (l + 1) is V30() real ext-real rational Element of REAL
((l + 1) - l) * ((l + 1) ") is V30() real ext-real rational set
(((l + 1) - l) / (l + 1)) + ((k / (mn |^ l)) * (l / (l + 1))) is V30() real ext-real Element of REAL
((((l + 1) - l) / (l + 1)) + ((k / (mn |^ l)) * (l / (l + 1)))) * (mn |^ l) is V30() real ext-real Element of REAL
(l / (l + 1)) * k is V30() real ext-real Element of REAL
((l / (l + 1)) * k) / (mn |^ l) is V30() real ext-real Element of REAL
((l / (l + 1)) * k) * ((mn |^ l) ") is V30() real ext-real set
(1 / (l + 1)) + (((l / (l + 1)) * k) / (mn |^ l)) is V30() real ext-real Element of REAL
((1 / (l + 1)) + (((l / (l + 1)) * k) / (mn |^ l))) * (mn |^ l) is V30() real ext-real Element of REAL
(((l / (l + 1)) * k) / (mn |^ l)) * (mn |^ l) is V30() real ext-real Element of REAL
((1 / (l + 1)) * (mn |^ l)) + ((((l / (l + 1)) * k) / (mn |^ l)) * (mn |^ l)) is V30() real ext-real Element of REAL
((1 / (l + 1)) * (mn |^ l)) + ((l / (l + 1)) * k) is V30() real ext-real Element of REAL
((1 / (l + 1)) * k) + ((l / (l + 1)) * k) is V30() real ext-real Element of REAL
(mn - ((mn * (1 - (k / (mn |^ l)))) / (l + 1))) * 1 is V30() real ext-real Element of REAL
((mn - ((mn * (1 - (k / (mn |^ l)))) / (l + 1))) * 1) |^ l is V30() real ext-real Element of REAL
mn " is V30() real ext-real Element of REAL
(mn ") * mn is V30() real ext-real Element of REAL
(mn - ((mn * (1 - (k / (mn |^ l)))) / (l + 1))) * ((mn ") * mn) is V30() real ext-real Element of REAL
((mn - ((mn * (1 - (k / (mn |^ l)))) / (l + 1))) * ((mn ") * mn)) |^ l is V30() real ext-real Element of REAL
(mn - ((mn * (1 - (k / (mn |^ l)))) / (l + 1))) * (mn ") is V30() real ext-real Element of REAL
((mn - ((mn * (1 - (k / (mn |^ l)))) / (l + 1))) * (mn ")) * mn is V30() real ext-real Element of REAL
(((mn - ((mn * (1 - (k / (mn |^ l)))) / (l + 1))) * (mn ")) * mn) |^ l is V30() real ext-real Element of REAL
(mn - ((mn * (1 - (k / (mn |^ l)))) / (l + 1))) / mn is V30() real ext-real Element of REAL
(mn - ((mn * (1 - (k / (mn |^ l)))) / (l + 1))) * (mn ") is V30() real ext-real set
((mn - ((mn * (1 - (k / (mn |^ l)))) / (l + 1))) / mn) * mn is V30() real ext-real Element of REAL
(((mn - ((mn * (1 - (k / (mn |^ l)))) / (l + 1))) / mn) * mn) |^ l is V30() real ext-real Element of REAL
(mn / mn) - (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn) is V30() real ext-real Element of REAL
- (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn) is V30() real ext-real set
(mn / mn) + (- (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn)) is V30() real ext-real set
((mn / mn) - (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn)) * mn is V30() real ext-real Element of REAL
(((mn / mn) - (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn)) * mn) |^ l is V30() real ext-real Element of REAL
1 - (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn) is V30() real ext-real Element of REAL
1 + (- (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn)) is V30() real ext-real set
(1 - (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn)) * mn is V30() real ext-real Element of REAL
((1 - (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn)) * mn) |^ l is V30() real ext-real Element of REAL
((1 + (- (((mn * (1 - (k / (mn |^ l)))) / (l + 1)) / mn))) |^ l) * (mn |^ l) is V30() real ext-real Element of REAL
((l + 1) / (l + 1)) * k is V30() real ext-real Element of REAL
1 * k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
n |^ l is V30() real ext-real Element of REAL
1 / 2 is V30() real ext-real non negative rational Element of REAL
2 " is V11() V30() real ext-real positive non negative rational set
1 * (2 ") is V30() real ext-real non negative rational set
nn is V30() real ext-real Element of REAL
nn / (mn |^ l) is V30() real ext-real Element of REAL
(mn |^ l) " is V30() real ext-real set
nn * ((mn |^ l) ") is V30() real ext-real set
(nn / (mn |^ l)) - 1 is V30() real ext-real Element of REAL
- 1 is V30() real ext-real non positive integer rational set
(nn / (mn |^ l)) + (- 1) is V30() real ext-real set
3 |^ l is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative integer rational Element of REAL
((nn / (mn |^ l)) - 1) / (3 |^ l) is V30() real ext-real Element of REAL
(3 |^ l) " is V30() real ext-real non negative rational set
((nn / (mn |^ l)) - 1) * ((3 |^ l) ") is V30() real ext-real set
min ((1 / 2),(((nn / (mn |^ l)) - 1) / (3 |^ l))) is V30() real ext-real Element of REAL
1 + (min ((1 / 2),(((nn / (mn |^ l)) - 1) / (3 |^ l)))) is V30() real ext-real Element of REAL
(1 + (min ((1 / 2),(((nn / (mn |^ l)) - 1) / (3 |^ l))))) * mn is V30() real ext-real Element of REAL
((1 + (min ((1 / 2),(((nn / (mn |^ l)) - 1) / (3 |^ l))))) * mn) |^ l is V30() real ext-real Element of REAL
(1 + (min ((1 / 2),(((nn / (mn |^ l)) - 1) / (3 |^ l))))) |^ l is V30() real ext-real Element of REAL
((1 + (min ((1 / 2),(((nn / (mn |^ l)) - 1) / (3 |^ l))))) |^ l) * (mn |^ l) is V30() real ext-real Element of REAL
(3 |^ l) * (min ((1 / 2),(((nn / (mn |^ l)) - 1) / (3 |^ l)))) is V30() real ext-real Element of REAL
k / (mn |^ l) is V30() real ext-real Element of REAL
k * ((mn |^ l) ") is V30() real ext-real set
(k / (mn |^ l)) - 1 is V30() real ext-real Element of REAL
(k / (mn |^ l)) + (- 1) is V30() real ext-real set
((k / (mn |^ l)) - 1) / (3 |^ l) is V30() real ext-real Element of REAL
((k / (mn |^ l)) - 1) * ((3 |^ l) ") is V30() real ext-real set
(((k / (mn |^ l)) - 1) / (3 |^ l)) * (3 |^ l) is V30() real ext-real Element of REAL
1 + ((3 |^ l) * (min ((1 / 2),(((nn / (mn |^ l)) - 1) / (3 |^ l))))) is V30() real ext-real Element of REAL
(mn |^ l) / (mn |^ l) is V30() real ext-real Element of REAL
(mn |^ l) * ((mn |^ l) ") is V30() real ext-real set
1 - 1 is V30() real ext-real integer rational Element of REAL
1 + (- 1) is V30() real ext-real integer rational set
0 / (3 |^ l) is V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54() V55() V56() V57() Element of REAL
0 * ((3 |^ l) ") is V11() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative integer rational V51() V52() V53() V54()