:: SERIES_1 semantic presentation

REAL is non empty V50() complex-membered ext-real-membered real-membered add-closed set
NAT is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V50() complex-membered add-closed set
omega is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed set
K19(omega) is set
K19(NAT) is set
K20(NAT,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
RAT is non empty V50() complex-membered ext-real-membered real-membered rational-membered add-closed set
INT is non empty V50() complex-membered ext-real-membered real-membered rational-membered integer-membered add-closed 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 non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
{} is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed set
0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed Element of NAT
- 1 is non empty ext-real non positive negative V33() real integer Element of REAL
|.0.| is ext-real V33() real V61() Element of REAL
1r is V33() Element of COMPLEX
|.1r.| is ext-real V33() real Element of REAL
s is ext-real V33() real set
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim n is ext-real V33() real Element of REAL
1 / s is ext-real V33() real Element of REAL
s " is ext-real V33() real set
1 * (s ") is ext-real V33() real set
(1 / s) - 1 is ext-real V33() real Element of REAL
- 1 is non empty ext-real non positive negative V33() real integer set
(1 / s) + (- 1) is ext-real V33() real set
1 / 1 is non empty ext-real positive non negative V33() real Element of REAL
1 " is non empty ext-real positive non negative V33() real set
1 * (1 ") is non empty ext-real positive non negative V33() real set
n is ext-real V33() real set
n * ((1 / s) - 1) is ext-real V33() real Element of REAL
1 / (n * ((1 / s) - 1)) is ext-real V33() real Element of REAL
(n * ((1 / s) - 1)) " is ext-real V33() real set
1 * ((n * ((1 / s) - 1)) ") is ext-real V33() real set
[\(1 / (n * ((1 / s) - 1)))/] is ext-real V33() real integer set
[\(1 / (n * ((1 / s) - 1)))/] + 1 is ext-real V33() real integer Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 / n is ext-real V33() real Element of REAL
n " is ext-real V33() real set
1 * (n ") is ext-real V33() real set
(1 / n) / ((1 / s) - 1) is ext-real V33() real Element of REAL
((1 / s) - 1) " is ext-real V33() real set
(1 / n) * (((1 / s) - 1) ") is ext-real V33() real set
(1 / (n * ((1 / s) - 1))) - 1 is ext-real V33() real Element of REAL
(1 / (n * ((1 / s) - 1))) + (- 1) is ext-real V33() real set
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s2 + 1) * ((1 / s) - 1) is ext-real V33() real Element of REAL
1 + ((s2 + 1) * ((1 / s) - 1)) is ext-real V33() real Element of REAL
0 + ((s2 + 1) * ((1 / s) - 1)) is ext-real V33() real Element of REAL
1 + ((1 / s) - 1) is ext-real V33() real Element of REAL
(1 + ((1 / s) - 1)) to_power (s2 + 1) is ext-real V33() real Element of REAL
(1 + ((1 / s) - 1)) |^ (s2 + 1) is ext-real V33() real set
1 to_power (s2 + 1) is ext-real V33() real Element of REAL
1 |^ (s2 + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
s to_power (s2 + 1) is ext-real V33() real set
s |^ (s2 + 1) is ext-real V33() real set
(1 to_power (s2 + 1)) / (s to_power (s2 + 1)) is ext-real V33() real Element of REAL
(s to_power (s2 + 1)) " is ext-real V33() real set
(1 to_power (s2 + 1)) * ((s to_power (s2 + 1)) ") is ext-real V33() real set
1 / (s to_power (s2 + 1)) is ext-real V33() real Element of REAL
1 * ((s to_power (s2 + 1)) ") is ext-real V33() real set
abs (s to_power (s2 + 1)) is ext-real V33() real Element of REAL
n . s2 is ext-real V33() real Element of REAL
(n . s2) - 0 is ext-real V33() real Element of REAL
- 0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed set
(n . s2) + (- 0) is ext-real V33() real set
abs ((n . s2) - 0) is ext-real V33() real Element of REAL
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n . s2 is ext-real V33() real Element of REAL
(n . s2) - 0 is ext-real V33() real Element of REAL
(n . s2) + (- 0) is ext-real V33() real set
abs ((n . s2) - 0) is ext-real V33() real Element of REAL
s is ext-real V33() real set
abs s is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(abs s) to_power n is ext-real V33() real set
(abs s) |^ n is ext-real V33() real set
s to_power n is ext-real V33() real set
s |^ n is ext-real V33() real set
abs (s to_power n) is ext-real V33() real Element of REAL
m is ext-real V33() real integer set
- s is ext-real V33() real set
(- s) to_power m is ext-real V33() real set
s to_power m is ext-real V33() real set
m is ext-real V33() real integer set
- s is ext-real V33() real set
(- s) to_power m is ext-real V33() real set
s to_power m is ext-real V33() real set
- (s to_power m) is ext-real V33() real set
- (s to_power n) is ext-real V33() real set
abs (- (s to_power n)) is ext-real V33() real Element of REAL
m is ext-real V33() real integer set
s is ext-real V33() real set
abs s is ext-real V33() real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s to_power (m + 1) is ext-real V33() real set
s |^ (m + 1) is ext-real V33() real set
n . m is ext-real V33() real Element of REAL
n . 0 is ext-real V33() real Element of REAL
m is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . n is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(abs s) to_power (n + 1) is ext-real V33() real Element of REAL
(abs s) |^ (n + 1) is ext-real V33() real set
s to_power (n + 1) is ext-real V33() real set
s |^ (n + 1) is ext-real V33() real set
abs (s to_power (n + 1)) is ext-real V33() real Element of REAL
n . n is ext-real V33() real Element of REAL
abs (n . n) is ext-real V33() real Element of REAL
lim m is ext-real V33() real Element of REAL
abs n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (abs n) is ext-real V33() real Element of REAL
s is non empty complex-membered add-closed set
K20(NAT,s) is complex-valued set
K19(K20(NAT,s)) is set
n is Relation-like NAT -defined s -valued Function-like non empty V14( NAT ) V18( NAT ,s) complex-valued Element of K19(K20(NAT,s))
m is Relation-like NAT -defined s -valued Function-like non empty V14( NAT ) V18( NAT ,s) complex-valued Element of K19(K20(NAT,s))
n + m is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n + m is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
K20(NAT,COMPLEX) is complex-valued set
K19(K20(NAT,COMPLEX)) is set
dom (n + m) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
dom n is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
dom m is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
(dom n) /\ (dom m) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
NAT /\ (dom m) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
NAT /\ NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(REAL)
n is set
n . n is V33() set
m . n is V33() set
(n + m) . n is V33() set
(n . n) + (m . n) is V33() set
s is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
s . 0 is V33() set
dom s is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
rng s is complex-membered set
K20(NAT,COMPLEX) is complex-valued set
K19(K20(NAT,COMPLEX)) is set
m is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
k is V33() Element of COMPLEX
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . (n + 1) is V33() Element of COMPLEX
k + (m . (n + 1)) is V33() Element of COMPLEX
m . 0 is V33() Element of COMPLEX
n is Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n . 0 is V33() Element of COMPLEX
n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n . 0 is V33() set
m is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
m . 0 is V33() set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n . n is V33() set
m . n is V33() set
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n . (n + 1) is V33() set
m . (n + 1) is V33() set
s . (n + 1) is V33() set
(m . n) + (s . (n + 1)) is V33() set
s is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
(s) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
m is set
dom (s) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
(s) . m is V33() set
dom (s) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
(s) . 0 is V33() set
s . 0 is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(s) . k is V33() set
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . (k + 1) is V33() set
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . (s2 + 1) is V33() set
(s) . s2 is V33() set
s . (s2 + 1) is ext-real V33() real Element of REAL
((s) . s2) + (s . (s2 + 1)) is V33() set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . n is V33() set
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
dom (s) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
rng (s) is complex-membered ext-real-membered real-membered set
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (s) is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is ext-real V33() real Element of REAL
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . (n + 1) is ext-real V33() real Element of REAL
(s) . n is ext-real V33() real Element of REAL
s . (n + 1) is ext-real V33() real Element of REAL
((s) . n) + (s . (n + 1)) is ext-real V33() real Element of REAL
s ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s
(s ^\ 1) . n is ext-real V33() real Element of REAL
((s) . n) + ((s ^\ 1) . n) is ext-real V33() real Element of REAL
(s) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (s)
((s) ^\ 1) . n is ext-real V33() real Element of REAL
(REAL,(s),(s ^\ 1)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) - (s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (s) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
- 1 is non empty ext-real non positive negative V33() real integer set
(- 1) (#) (s) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
(s) + (- (s)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
(REAL,(s ^\ 1),((s) - (s))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(REAL,(s ^\ 1),((s) - (s))) . n is ext-real V33() real Element of REAL
(s ^\ 1) . n is ext-real V33() real Element of REAL
- (s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(REAL,(s),(- (s))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(REAL,(s),(- (s))) . n is ext-real V33() real Element of REAL
((s ^\ 1) . n) + ((REAL,(s),(- (s))) . n) is ext-real V33() real Element of REAL
(s) . n is ext-real V33() real Element of REAL
(- (s)) . n is ext-real V33() real Element of REAL
((s) . n) + ((- (s)) . n) is ext-real V33() real Element of REAL
((s ^\ 1) . n) + (((s) . n) + ((- (s)) . n)) is ext-real V33() real Element of REAL
- ((s) . n) is ext-real V33() real Element of REAL
((s) . n) + (- ((s) . n)) is ext-real V33() real Element of REAL
((s ^\ 1) . n) + (((s) . n) + (- ((s) . n))) is ext-real V33() real Element of REAL
((s) ^\ 1) - (s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((s) ^\ 1) + (- (s)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
lim ((s) ^\ 1) is ext-real V33() real Element of REAL
lim (s) is ext-real V33() real Element of REAL
lim (((s) ^\ 1) - (s)) is ext-real V33() real Element of REAL
(lim (s)) - (lim (s)) is ext-real V33() real Element of REAL
- (lim (s)) is ext-real V33() real set
(lim (s)) + (- (lim (s))) is ext-real V33() real set
s is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
m is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n + m is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . n is V33() set
n . n is V33() set
m . n is V33() set
(n . n) + (m . n) is V33() set
dom s is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
dom s is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
n is set
s . n is V33() set
n . n is V33() set
m . n is V33() set
(n . n) + (m . n) is V33() set
NAT /\ NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(REAL)
dom m is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
NAT /\ (dom m) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
dom n is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
(dom n) /\ (dom m) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)
s is non empty complex-membered add-closed set
K20(NAT,s) is complex-valued set
K19(K20(NAT,s)) is set
n is Relation-like NAT -defined s -valued Function-like non empty V14( NAT ) V18( NAT ,s) complex-valued Element of K19(K20(NAT,s))
(n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
m is Relation-like NAT -defined s -valued Function-like non empty V14( NAT ) V18( NAT ,s) complex-valued Element of K19(K20(NAT,s))
(m) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(n) + (m) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
(s,n,m) is Relation-like NAT -defined s -valued Function-like non empty V14( NAT ) V18( NAT ,s) complex-valued Element of K19(K20(NAT,s))
((s,n,m)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((n) + (m)) . (n + 1) is V33() set
(n) . (n + 1) is V33() set
(m) . (n + 1) is V33() set
((n) . (n + 1)) + ((m) . (n + 1)) is V33() set
(n) . n is V33() set
n . (n + 1) is V33() Element of s
((n) . n) + (n . (n + 1)) is V33() set
(((n) . n) + (n . (n + 1))) + ((m) . (n + 1)) is V33() set
m . (n + 1) is V33() Element of s
(m) . n is V33() set
(m . (n + 1)) + ((m) . n) is V33() set
(((n) . n) + (n . (n + 1))) + ((m . (n + 1)) + ((m) . n)) is V33() set
(n . (n + 1)) + (m . (n + 1)) is V33() set
((n) . n) + ((n . (n + 1)) + (m . (n + 1))) is V33() set
(((n) . n) + ((n . (n + 1)) + (m . (n + 1)))) + ((m) . n) is V33() set
(s,n,m) . (n + 1) is V33() Element of s
((n) . n) + ((s,n,m) . (n + 1)) is V33() set
(((n) . n) + ((s,n,m) . (n + 1))) + ((m) . n) is V33() set
((n) . n) + ((m) . n) is V33() set
(((n) . n) + ((m) . n)) + ((s,n,m) . (n + 1)) is V33() set
((n) + (m)) . n is V33() set
(((n) + (m)) . n) + ((s,n,m) . (n + 1)) is V33() set
((n) + (m)) . 0 is V33() set
(n) . 0 is V33() set
(m) . 0 is V33() set
((n) . 0) + ((m) . 0) is V33() set
n . 0 is V33() Element of s
(n . 0) + ((m) . 0) is V33() set
m . 0 is V33() Element of s
(n . 0) + (m . 0) is V33() set
(s,n,m) . 0 is V33() Element of s
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) - (n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
- 1 is non empty ext-real non positive negative V33() real integer set
(- 1) (#) (n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
(s) + (- (n)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
s - n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
(- 1) (#) n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
s + (- n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
((s - n)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((s) - (n)) . (m + 1) is ext-real V33() real Element of REAL
(s) . (m + 1) is ext-real V33() real Element of REAL
(n) . (m + 1) is ext-real V33() real Element of REAL
((s) . (m + 1)) - ((n) . (m + 1)) is ext-real V33() real Element of REAL
- ((n) . (m + 1)) is ext-real V33() real set
((s) . (m + 1)) + (- ((n) . (m + 1))) is ext-real V33() real set
(s) . m is ext-real V33() real Element of REAL
s . (m + 1) is ext-real V33() real Element of REAL
((s) . m) + (s . (m + 1)) is ext-real V33() real Element of REAL
(((s) . m) + (s . (m + 1))) - ((n) . (m + 1)) is ext-real V33() real Element of REAL
(((s) . m) + (s . (m + 1))) + (- ((n) . (m + 1))) is ext-real V33() real set
n . (m + 1) is ext-real V33() real Element of REAL
(n) . m is ext-real V33() real Element of REAL
(n . (m + 1)) + ((n) . m) is ext-real V33() real Element of REAL
(((s) . m) + (s . (m + 1))) - ((n . (m + 1)) + ((n) . m)) is ext-real V33() real Element of REAL
- ((n . (m + 1)) + ((n) . m)) is ext-real V33() real set
(((s) . m) + (s . (m + 1))) + (- ((n . (m + 1)) + ((n) . m))) is ext-real V33() real set
(s . (m + 1)) - (n . (m + 1)) is ext-real V33() real Element of REAL
- (n . (m + 1)) is ext-real V33() real set
(s . (m + 1)) + (- (n . (m + 1))) is ext-real V33() real set
((s) . m) + ((s . (m + 1)) - (n . (m + 1))) is ext-real V33() real Element of REAL
(((s) . m) + ((s . (m + 1)) - (n . (m + 1)))) - ((n) . m) is ext-real V33() real Element of REAL
- ((n) . m) is ext-real V33() real set
(((s) . m) + ((s . (m + 1)) - (n . (m + 1)))) + (- ((n) . m)) is ext-real V33() real set
(s - n) . (m + 1) is ext-real V33() real Element of REAL
((s - n) . (m + 1)) + ((s) . m) is ext-real V33() real Element of REAL
(((s - n) . (m + 1)) + ((s) . m)) - ((n) . m) is ext-real V33() real Element of REAL
(((s - n) . (m + 1)) + ((s) . m)) + (- ((n) . m)) is ext-real V33() real set
((s) . m) - ((n) . m) is ext-real V33() real Element of REAL
((s) . m) + (- ((n) . m)) is ext-real V33() real set
((s - n) . (m + 1)) + (((s) . m) - ((n) . m)) is ext-real V33() real Element of REAL
((s) - (n)) . m is ext-real V33() real Element of REAL
(((s) - (n)) . m) + ((s - n) . (m + 1)) is ext-real V33() real Element of REAL
((s) - (n)) . 0 is ext-real V33() real Element of REAL
(s) . 0 is ext-real V33() real Element of REAL
(n) . 0 is ext-real V33() real Element of REAL
((s) . 0) - ((n) . 0) is ext-real V33() real Element of REAL
- ((n) . 0) is ext-real V33() real set
((s) . 0) + (- ((n) . 0)) is ext-real V33() real set
s . 0 is ext-real V33() real Element of REAL
(s . 0) - ((n) . 0) is ext-real V33() real Element of REAL
(s . 0) + (- ((n) . 0)) is ext-real V33() real set
n . 0 is ext-real V33() real Element of REAL
(s . 0) - (n . 0) is ext-real V33() real Element of REAL
- (n . 0) is ext-real V33() real set
(s . 0) + (- (n . 0)) is ext-real V33() real set
(s - n) . 0 is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) is ext-real V33() real Element of REAL
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (s) is ext-real V33() real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(REAL,s,n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((REAL,s,n)) is ext-real V33() real Element of REAL
((REAL,s,n)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((REAL,s,n)) is ext-real V33() real Element of REAL
(n) is ext-real V33() real Element of REAL
(n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (n) is ext-real V33() real Element of REAL
(s) + (n) is ext-real V33() real Element of REAL
(REAL,(s),(n)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (REAL,(s),(n)) is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) is ext-real V33() real Element of REAL
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (s) is ext-real V33() real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s - n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
- 1 is non empty ext-real non positive negative V33() real integer set
(- 1) (#) n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
s + (- n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
((s - n)) is ext-real V33() real Element of REAL
((s - n)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((s - n)) is ext-real V33() real Element of REAL
(n) is ext-real V33() real Element of REAL
(n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (n) is ext-real V33() real Element of REAL
(s) - (n) is ext-real V33() real Element of REAL
- (n) is ext-real V33() real set
(s) + (- (n)) is ext-real V33() real set
(s) - (n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
(- 1) (#) (n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
(s) + (- (n)) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
lim ((s) - (n)) is ext-real V33() real Element of REAL
s is ext-real V33() real set
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s (#) n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((s (#) n)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s (#) (n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s (#) (n)) . (m + 1) is ext-real V33() real Element of REAL
(n) . (m + 1) is ext-real V33() real Element of REAL
s * ((n) . (m + 1)) is ext-real V33() real Element of REAL
(n) . m is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
((n) . m) + (n . (m + 1)) is ext-real V33() real Element of REAL
s * (((n) . m) + (n . (m + 1))) is ext-real V33() real Element of REAL
s * ((n) . m) is ext-real V33() real Element of REAL
s * (n . (m + 1)) is ext-real V33() real Element of REAL
(s * ((n) . m)) + (s * (n . (m + 1))) is ext-real V33() real Element of REAL
(s (#) (n)) . m is ext-real V33() real Element of REAL
((s (#) (n)) . m) + (s * (n . (m + 1))) is ext-real V33() real Element of REAL
(s (#) n) . (m + 1) is ext-real V33() real Element of REAL
((s (#) (n)) . m) + ((s (#) n) . (m + 1)) is ext-real V33() real Element of REAL
(s (#) (n)) . 0 is ext-real V33() real Element of REAL
(n) . 0 is ext-real V33() real Element of REAL
s * ((n) . 0) is ext-real V33() real Element of REAL
n . 0 is ext-real V33() real Element of REAL
s * (n . 0) is ext-real V33() real Element of REAL
(s (#) n) . 0 is ext-real V33() real Element of REAL
s is ext-real V33() real set
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s (#) n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((s (#) n)) is ext-real V33() real Element of REAL
((s (#) n)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((s (#) n)) is ext-real V33() real Element of REAL
(n) is ext-real V33() real Element of REAL
(n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (n) is ext-real V33() real Element of REAL
s * (n) is ext-real V33() real Element of REAL
s (#) (n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (s (#) (n)) is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s . 0 is ext-real V33() real Element of REAL
s ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s
((s ^\ 1)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (s)
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((s) ^\ 1) - n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
- 1 is non empty ext-real non positive negative V33() real integer set
(- 1) (#) n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
((s) ^\ 1) + (- n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(((s) ^\ 1) - n) . (m + 1) is ext-real V33() real Element of REAL
((s) ^\ 1) . (m + 1) is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
(((s) ^\ 1) . (m + 1)) - (n . (m + 1)) is ext-real V33() real Element of REAL
- (n . (m + 1)) is ext-real V33() real set
(((s) ^\ 1) . (m + 1)) + (- (n . (m + 1))) is ext-real V33() real set
(((s) ^\ 1) . (m + 1)) - (s . 0) is ext-real V33() real Element of REAL
- (s . 0) is ext-real V33() real set
(((s) ^\ 1) . (m + 1)) + (- (s . 0)) is ext-real V33() real set
(m + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . ((m + 1) + 1) is ext-real V33() real Element of REAL
((s) . ((m + 1) + 1)) - (s . 0) is ext-real V33() real Element of REAL
((s) . ((m + 1) + 1)) + (- (s . 0)) is ext-real V33() real set
s . ((m + 1) + 1) is ext-real V33() real Element of REAL
(s) . (m + 1) is ext-real V33() real Element of REAL
(s . ((m + 1) + 1)) + ((s) . (m + 1)) is ext-real V33() real Element of REAL
((s . ((m + 1) + 1)) + ((s) . (m + 1))) - (s . 0) is ext-real V33() real Element of REAL
((s . ((m + 1) + 1)) + ((s) . (m + 1))) + (- (s . 0)) is ext-real V33() real set
n . m is ext-real V33() real Element of REAL
((s . ((m + 1) + 1)) + ((s) . (m + 1))) - (n . m) is ext-real V33() real Element of REAL
- (n . m) is ext-real V33() real set
((s . ((m + 1) + 1)) + ((s) . (m + 1))) + (- (n . m)) is ext-real V33() real set
((s) . (m + 1)) - (n . m) is ext-real V33() real Element of REAL
((s) . (m + 1)) + (- (n . m)) is ext-real V33() real set
(s . ((m + 1) + 1)) + (((s) . (m + 1)) - (n . m)) is ext-real V33() real Element of REAL
((s) ^\ 1) . m is ext-real V33() real Element of REAL
(((s) ^\ 1) . m) - (n . m) is ext-real V33() real Element of REAL
(((s) ^\ 1) . m) + (- (n . m)) is ext-real V33() real set
(s . ((m + 1) + 1)) + ((((s) ^\ 1) . m) - (n . m)) is ext-real V33() real Element of REAL
(((s) ^\ 1) - n) . m is ext-real V33() real Element of REAL
(s . ((m + 1) + 1)) + ((((s) ^\ 1) - n) . m) is ext-real V33() real Element of REAL
(s ^\ 1) . (m + 1) is ext-real V33() real Element of REAL
((((s) ^\ 1) - n) . m) + ((s ^\ 1) . (m + 1)) is ext-real V33() real Element of REAL
(((s) ^\ 1) - n) . 0 is ext-real V33() real Element of REAL
((s) ^\ 1) . 0 is ext-real V33() real Element of REAL
n . 0 is ext-real V33() real Element of REAL
(((s) ^\ 1) . 0) - (n . 0) is ext-real V33() real Element of REAL
- (n . 0) is ext-real V33() real set
(((s) ^\ 1) . 0) + (- (n . 0)) is ext-real V33() real set
(((s) ^\ 1) . 0) - (s . 0) is ext-real V33() real Element of REAL
(((s) ^\ 1) . 0) + (- (s . 0)) is ext-real V33() real set
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . (0 + 1) is ext-real V33() real Element of REAL
((s) . (0 + 1)) - (s . 0) is ext-real V33() real Element of REAL
((s) . (0 + 1)) + (- (s . 0)) is ext-real V33() real set
(s) . 0 is ext-real V33() real Element of REAL
s . (0 + 1) is ext-real V33() real Element of REAL
((s) . 0) + (s . (0 + 1)) is ext-real V33() real Element of REAL
(((s) . 0) + (s . (0 + 1))) - (s . 0) is ext-real V33() real Element of REAL
(((s) . 0) + (s . (0 + 1))) + (- (s . 0)) is ext-real V33() real set
(s . (0 + 1)) + (s . 0) is ext-real V33() real Element of REAL
((s . (0 + 1)) + (s . 0)) - (s . 0) is ext-real V33() real Element of REAL
((s . (0 + 1)) + (s . 0)) + (- (s . 0)) is ext-real V33() real set
(s ^\ 1) . 0 is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s ^\ n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s ^\ (n + 1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s
(s ^\ n) . 0 is ext-real V33() real Element of REAL
NAT --> ((s ^\ n) . 0) is Relation-like NAT -defined REAL -valued Function-like constant non empty V14( NAT ) V18( NAT , REAL ) T-Sequence-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded convergent Element of K19(K20(NAT,REAL))
m is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . n is ext-real V33() real Element of REAL
(s ^\ n) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s ^\ n
(((s ^\ n) ^\ 1)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((s ^\ n)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((s ^\ n)) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of ((s ^\ n))
(((s ^\ n)) ^\ 1) - m is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- m is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
- 1 is non empty ext-real non positive negative V33() real integer set
(- 1) (#) m is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
(((s ^\ n)) ^\ 1) + (- m) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
s ^\ 0 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s ^\ n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) . n is ext-real V33() real Element of REAL
NAT --> ((s) . n) is Relation-like NAT -defined REAL -valued Function-like constant non empty V14( NAT ) V18( NAT , REAL ) T-Sequence-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded convergent Element of K19(K20(NAT,REAL))
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) ^\ (n + 1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (s)
s ^\ (n + 1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s
((s ^\ (n + 1))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((s ^\ (n + 1))) . 0 is ext-real V33() real Element of REAL
(s ^\ (n + 1)) . 0 is ext-real V33() real Element of REAL
0 + (n + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . (0 + (n + 1)) is ext-real V33() real Element of REAL
s . (n + 1) is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((s) ^\ (n + 1)) . n is ext-real V33() real Element of REAL
((s ^\ (n + 1))) . n is ext-real V33() real Element of REAL
m . n is ext-real V33() real Element of REAL
(((s ^\ (n + 1))) . n) + (m . n) is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((s) ^\ (n + 1)) . (n + 1) is ext-real V33() real Element of REAL
((s ^\ (n + 1))) . (n + 1) is ext-real V33() real Element of REAL
m . (n + 1) is ext-real V33() real Element of REAL
(((s ^\ (n + 1))) . (n + 1)) + (m . (n + 1)) is ext-real V33() real Element of REAL
(s ^\ (n + 1)) . (n + 1) is ext-real V33() real Element of REAL
(((s ^\ (n + 1))) . n) + ((s ^\ (n + 1)) . (n + 1)) is ext-real V33() real Element of REAL
(m . (n + 1)) + ((((s ^\ (n + 1))) . n) + ((s ^\ (n + 1)) . (n + 1))) is ext-real V33() real Element of REAL
(m . (n + 1)) + (((s ^\ (n + 1))) . n) is ext-real V33() real Element of REAL
((m . (n + 1)) + (((s ^\ (n + 1))) . n)) + ((s ^\ (n + 1)) . (n + 1)) is ext-real V33() real Element of REAL
((s) . n) + (((s ^\ (n + 1))) . n) is ext-real V33() real Element of REAL
(((s) . n) + (((s ^\ (n + 1))) . n)) + ((s ^\ (n + 1)) . (n + 1)) is ext-real V33() real Element of REAL
(((s) ^\ (n + 1)) . n) + ((s ^\ (n + 1)) . (n + 1)) is ext-real V33() real Element of REAL
n + (n + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . (n + (n + 1)) is ext-real V33() real Element of REAL
((s) . (n + (n + 1))) + ((s ^\ (n + 1)) . (n + 1)) is ext-real V33() real Element of REAL
(n + 1) + (n + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . ((n + 1) + (n + 1)) is ext-real V33() real Element of REAL
((s) . (n + (n + 1))) + (s . ((n + 1) + (n + 1))) is ext-real V33() real Element of REAL
(n + (n + 1)) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . ((n + (n + 1)) + 1) is ext-real V33() real Element of REAL
(s) . ((n + 1) + (n + 1)) is ext-real V33() real Element of REAL
((s) ^\ (n + 1)) . 0 is ext-real V33() real Element of REAL
(s) . (0 + (n + 1)) is ext-real V33() real Element of REAL
(s . (n + 1)) + ((s) . n) is ext-real V33() real Element of REAL
m . 0 is ext-real V33() real Element of REAL
(((s ^\ (n + 1))) . 0) + (m . 0) is ext-real V33() real Element of REAL
(REAL,((s ^\ (n + 1))),m) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s ^\ n) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s ^\ n
(((s ^\ n) ^\ 1)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(REAL,(((s ^\ n) ^\ 1)),m) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . m is ext-real V33() real Element of REAL
(n) . m is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . (m + 1) is ext-real V33() real Element of REAL
(n) . (m + 1) is ext-real V33() real Element of REAL
s . (m + 1) is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
((s) . m) + (s . (m + 1)) is ext-real V33() real Element of REAL
((n) . m) + (n . (m + 1)) is ext-real V33() real Element of REAL
(n) . 0 is ext-real V33() real Element of REAL
n . 0 is ext-real V33() real Element of REAL
(s) . 0 is ext-real V33() real Element of REAL
s . 0 is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) is ext-real V33() real Element of REAL
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (s) is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . n is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s ^\ (n + 1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s
((s ^\ (n + 1))) is ext-real V33() real Element of REAL
((s ^\ (n + 1))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((s ^\ (n + 1))) is ext-real V33() real Element of REAL
((s) . n) + ((s ^\ (n + 1))) is ext-real V33() real Element of REAL
(s) . (n + 1) is ext-real V33() real Element of REAL
(n + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s ^\ ((n + 1) + 1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s
((s ^\ ((n + 1) + 1))) is ext-real V33() real Element of REAL
((s ^\ ((n + 1) + 1))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((s ^\ ((n + 1) + 1))) is ext-real V33() real Element of REAL
((s) . (n + 1)) + ((s ^\ ((n + 1) + 1))) is ext-real V33() real Element of REAL
(s ^\ (n + 1)) . 0 is ext-real V33() real Element of REAL
NAT --> ((s ^\ (n + 1)) . 0) is Relation-like NAT -defined REAL -valued Function-like constant non empty V14( NAT ) V18( NAT , REAL ) T-Sequence-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded convergent Element of K19(K20(NAT,REAL))
m is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . n is ext-real V33() real Element of REAL
(s ^\ (n + 1)) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s ^\ (n + 1)
(((s ^\ (n + 1)) ^\ 1)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((s ^\ (n + 1))) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of ((s ^\ (n + 1)))
(((s ^\ (n + 1))) ^\ 1) - m is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- m is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
- 1 is non empty ext-real non positive negative V33() real integer set
(- 1) (#) m is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
(((s ^\ (n + 1))) ^\ 1) + (- m) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
lim (((s ^\ (n + 1)) ^\ 1)) is ext-real V33() real Element of REAL
lim (((s ^\ (n + 1))) ^\ 1) is ext-real V33() real Element of REAL
lim m is ext-real V33() real Element of REAL
(lim (((s ^\ (n + 1))) ^\ 1)) - (lim m) is ext-real V33() real Element of REAL
- (lim m) is ext-real V33() real set
(lim (((s ^\ (n + 1))) ^\ 1)) + (- (lim m)) is ext-real V33() real set
(lim ((s ^\ (n + 1)))) - (lim m) is ext-real V33() real Element of REAL
(lim ((s ^\ (n + 1)))) + (- (lim m)) is ext-real V33() real set
m . 0 is ext-real V33() real Element of REAL
((s ^\ (n + 1))) - (m . 0) is ext-real V33() real Element of REAL
- (m . 0) is ext-real V33() real set
((s ^\ (n + 1))) + (- (m . 0)) is ext-real V33() real set
((s ^\ (n + 1))) - ((s ^\ (n + 1)) . 0) is ext-real V33() real Element of REAL
- ((s ^\ (n + 1)) . 0) is ext-real V33() real set
((s ^\ (n + 1))) + (- ((s ^\ (n + 1)) . 0)) is ext-real V33() real set
((s) . n) + ((s ^\ (n + 1)) . 0) is ext-real V33() real Element of REAL
(s) - (((s) . n) + ((s ^\ (n + 1)) . 0)) is ext-real V33() real Element of REAL
- (((s) . n) + ((s ^\ (n + 1)) . 0)) is ext-real V33() real set
(s) + (- (((s) . n) + ((s ^\ (n + 1)) . 0))) is ext-real V33() real set
0 + (n + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . (0 + (n + 1)) is ext-real V33() real Element of REAL
((s) . n) + (s . (0 + (n + 1))) is ext-real V33() real Element of REAL
(s) - (((s) . n) + (s . (0 + (n + 1)))) is ext-real V33() real Element of REAL
- (((s) . n) + (s . (0 + (n + 1)))) is ext-real V33() real set
(s) + (- (((s) . n) + (s . (0 + (n + 1))))) is ext-real V33() real set
(s) - ((s) . (n + 1)) is ext-real V33() real Element of REAL
- ((s) . (n + 1)) is ext-real V33() real set
(s) + (- ((s) . (n + 1))) is ext-real V33() real set
(s) . 0 is ext-real V33() real Element of REAL
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s ^\ (0 + 1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s
((s ^\ (0 + 1))) is ext-real V33() real Element of REAL
((s ^\ (0 + 1))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((s ^\ (0 + 1))) is ext-real V33() real Element of REAL
((s) . 0) + ((s ^\ (0 + 1))) is ext-real V33() real Element of REAL
s . 0 is ext-real V33() real Element of REAL
NAT --> (s . 0) is Relation-like NAT -defined REAL -valued Function-like constant non empty V14( NAT ) V18( NAT , REAL ) T-Sequence-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded convergent Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n . m is ext-real V33() real Element of REAL
s ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s
((s ^\ 1)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (s)
((s) ^\ 1) - n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
- 1 is non empty ext-real non positive negative V33() real integer set
(- 1) (#) n is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
((s) ^\ 1) + (- n) is Relation-like NAT -defined Function-like V14( NAT ) complex-valued ext-real-valued real-valued set
lim ((s ^\ 1)) is ext-real V33() real Element of REAL
lim ((s) ^\ 1) is ext-real V33() real Element of REAL
lim n is ext-real V33() real Element of REAL
(lim ((s) ^\ 1)) - (lim n) is ext-real V33() real Element of REAL
- (lim n) is ext-real V33() real set
(lim ((s) ^\ 1)) + (- (lim n)) is ext-real V33() real set
(lim (s)) - (lim n) is ext-real V33() real Element of REAL
(lim (s)) + (- (lim n)) is ext-real V33() real set
n . 0 is ext-real V33() real Element of REAL
(s) - (n . 0) is ext-real V33() real Element of REAL
- (n . 0) is ext-real V33() real set
(s) + (- (n . 0)) is ext-real V33() real set
(s) - (s . 0) is ext-real V33() real Element of REAL
- (s . 0) is ext-real V33() real set
(s) + (- (s . 0)) is ext-real V33() real set
((s ^\ 1)) is ext-real V33() real Element of REAL
- (s . 0) is ext-real V33() real Element of REAL
- (- (s . 0)) is ext-real V33() real Element of REAL
((s ^\ 1)) + (- (- (s . 0))) is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . (n + 1) is ext-real V33() real Element of REAL
(s) . n is ext-real V33() real Element of REAL
0 + ((s) . n) is ext-real V33() real Element of REAL
(s . (n + 1)) + ((s) . n) is ext-real V33() real Element of REAL
(s) . (n + 1) is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) is ext-real V33() real Element of REAL
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (s) is ext-real V33() real Element of REAL
(s) . 0 is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . n is ext-real V33() real Element of REAL
s . 0 is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n ^\ m is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of n
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(n ^\ m) . n is ext-real V33() real Element of REAL
n + m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n . (n + m) is ext-real V33() real Element of REAL
s . (n + m) is ext-real V33() real Element of REAL
((n ^\ m)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real V33() real set
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k + m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . (k + m) is ext-real V33() real Element of REAL
n . (k + m) is ext-real V33() real Element of REAL
s ^\ m is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s
(s ^\ m) . k is ext-real V33() real Element of REAL
(n ^\ m) . k is ext-real V33() real Element of REAL
((s ^\ m)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((s ^\ m)) . k is ext-real V33() real Element of REAL
((n ^\ m)) . k is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s ^\ m) . k is ext-real V33() real Element of REAL
k + m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . (k + m) is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) is ext-real V33() real Element of REAL
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (s) is ext-real V33() real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(n) is ext-real V33() real Element of REAL
(n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (n) is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . m is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . m is ext-real V33() real Element of REAL
(n) . m is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real V33() real set
s is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n is ext-real V33() real set
n GeoSeq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((n GeoSeq)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((n GeoSeq)) . s is ext-real V33() real Element of REAL
n to_power (s + 1) is ext-real V33() real set
n |^ (s + 1) is ext-real V33() real set
1 - (n to_power (s + 1)) is ext-real V33() real Element of REAL
- (n to_power (s + 1)) is ext-real V33() real set
1 + (- (n to_power (s + 1))) is ext-real V33() real set
1 - n is ext-real V33() real Element of REAL
- n is ext-real V33() real set
1 + (- n) is ext-real V33() real set
(1 - (n to_power (s + 1))) / (1 - n) is ext-real V33() real Element of REAL
(1 - n) " is ext-real V33() real set
(1 - (n to_power (s + 1))) * ((1 - n) ") is ext-real V33() real set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((n GeoSeq)) . m is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n to_power (m + 1) is ext-real V33() real set
n |^ (m + 1) is ext-real V33() real set
1 - (n to_power (m + 1)) is ext-real V33() real Element of REAL
- (n to_power (m + 1)) is ext-real V33() real set
1 + (- (n to_power (m + 1))) is ext-real V33() real set
(1 - (n to_power (m + 1))) / (1 - n) is ext-real V33() real Element of REAL
(1 - (n to_power (m + 1))) * ((1 - n) ") is ext-real V33() real set
((n GeoSeq)) . (m + 1) is ext-real V33() real Element of REAL
(m + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n to_power ((m + 1) + 1) is ext-real V33() real set
n |^ ((m + 1) + 1) is ext-real V33() real set
1 - (n to_power ((m + 1) + 1)) is ext-real V33() real Element of REAL
- (n to_power ((m + 1) + 1)) is ext-real V33() real set
1 + (- (n to_power ((m + 1) + 1))) is ext-real V33() real set
(1 - (n to_power ((m + 1) + 1))) / (1 - n) is ext-real V33() real Element of REAL
(1 - (n to_power ((m + 1) + 1))) * ((1 - n) ") is ext-real V33() real set
(n GeoSeq) . (m + 1) is ext-real V33() real Element of REAL
((1 - (n to_power (m + 1))) / (1 - n)) + ((n GeoSeq) . (m + 1)) is ext-real V33() real Element of REAL
(n to_power (m + 1)) * 1 is ext-real V33() real Element of REAL
((1 - (n to_power (m + 1))) / (1 - n)) + ((n to_power (m + 1)) * 1) is ext-real V33() real Element of REAL
(1 - n) / (1 - n) is ext-real V33() real Element of REAL
(1 - n) * ((1 - n) ") is ext-real V33() real set
(n to_power (m + 1)) * ((1 - n) / (1 - n)) is ext-real V33() real Element of REAL
((1 - (n to_power (m + 1))) / (1 - n)) + ((n to_power (m + 1)) * ((1 - n) / (1 - n))) is ext-real V33() real Element of REAL
(n to_power (m + 1)) * (1 - n) is ext-real V33() real Element of REAL
((n to_power (m + 1)) * (1 - n)) / (1 - n) is ext-real V33() real Element of REAL
((n to_power (m + 1)) * (1 - n)) * ((1 - n) ") is ext-real V33() real set
((1 - (n to_power (m + 1))) / (1 - n)) + (((n to_power (m + 1)) * (1 - n)) / (1 - n)) is ext-real V33() real Element of REAL
(n |^ (m + 1)) * n is ext-real V33() real set
(n to_power (m + 1)) - ((n |^ (m + 1)) * n) is ext-real V33() real set
- ((n |^ (m + 1)) * n) is ext-real V33() real set
(n to_power (m + 1)) + (- ((n |^ (m + 1)) * n)) is ext-real V33() real set
(1 - (n to_power (m + 1))) + ((n to_power (m + 1)) - ((n |^ (m + 1)) * n)) is ext-real V33() real Element of REAL
((1 - (n to_power (m + 1))) + ((n to_power (m + 1)) - ((n |^ (m + 1)) * n))) / (1 - n) is ext-real V33() real Element of REAL
((1 - (n to_power (m + 1))) + ((n to_power (m + 1)) - ((n |^ (m + 1)) * n))) * ((1 - n) ") is ext-real V33() real set
(n to_power (m + 1)) - (n |^ ((m + 1) + 1)) is ext-real V33() real set
- (n |^ ((m + 1) + 1)) is ext-real V33() real set
(n to_power (m + 1)) + (- (n |^ ((m + 1) + 1))) is ext-real V33() real set
(1 - (n to_power (m + 1))) + ((n to_power (m + 1)) - (n |^ ((m + 1) + 1))) is ext-real V33() real Element of REAL
((1 - (n to_power (m + 1))) + ((n to_power (m + 1)) - (n |^ ((m + 1) + 1)))) / (1 - n) is ext-real V33() real Element of REAL
((1 - (n to_power (m + 1))) + ((n to_power (m + 1)) - (n |^ ((m + 1) + 1)))) * ((1 - n) ") is ext-real V33() real set
((n GeoSeq)) . 0 is ext-real V33() real Element of REAL
(n GeoSeq) . 0 is ext-real V33() real Element of REAL
(1 - n) / (1 - n) is ext-real V33() real Element of REAL
(1 - n) * ((1 - n) ") is ext-real V33() real set
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n to_power (0 + 1) is ext-real V33() real set
n |^ (0 + 1) is ext-real V33() real set
1 - (n to_power (0 + 1)) is ext-real V33() real Element of REAL
- (n to_power (0 + 1)) is ext-real V33() real set
1 + (- (n to_power (0 + 1))) is ext-real V33() real set
(1 - (n to_power (0 + 1))) / (1 - n) is ext-real V33() real Element of REAL
(1 - (n to_power (0 + 1))) * ((1 - n) ") is ext-real V33() real set
s is ext-real V33() real set
1 - s is ext-real V33() real Element of REAL
- s is ext-real V33() real set
1 + (- s) is ext-real V33() real set
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n . 0 is ext-real V33() real Element of REAL
s GeoSeq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n . m is ext-real V33() real Element of REAL
(s GeoSeq) . m is ext-real V33() real Element of REAL
(n . 0) * ((s GeoSeq) . m) is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n . (m + 1) is ext-real V33() real Element of REAL
(s GeoSeq) . (m + 1) is ext-real V33() real Element of REAL
(n . 0) * ((s GeoSeq) . (m + 1)) is ext-real V33() real Element of REAL
s * ((n . 0) * ((s GeoSeq) . m)) is ext-real V33() real Element of REAL
((s GeoSeq) . m) * s is ext-real V33() real Element of REAL
(n . 0) * (((s GeoSeq) . m) * s) is ext-real V33() real Element of REAL
(s GeoSeq) . 0 is ext-real V33() real Element of REAL
(n . 0) * ((s GeoSeq) . 0) is ext-real V33() real Element of REAL
(n . 0) (#) (s GeoSeq) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((s GeoSeq)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(n . 0) (#) ((s GeoSeq)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(n) . m is ext-real V33() real Element of REAL
((s GeoSeq)) . m is ext-real V33() real Element of REAL
(n . 0) * (((s GeoSeq)) . m) is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s to_power (m + 1) is ext-real V33() real set
s |^ (m + 1) is ext-real V33() real set
1 - (s to_power (m + 1)) is ext-real V33() real Element of REAL
- (s to_power (m + 1)) is ext-real V33() real set
1 + (- (s to_power (m + 1))) is ext-real V33() real set
(1 - (s to_power (m + 1))) / (1 - s) is ext-real V33() real Element of REAL
(1 - s) " is ext-real V33() real set
(1 - (s to_power (m + 1))) * ((1 - s) ") is ext-real V33() real set
(n . 0) * ((1 - (s to_power (m + 1))) / (1 - s)) is ext-real V33() real Element of REAL
(n . 0) * (1 - (s to_power (m + 1))) is ext-real V33() real Element of REAL
((n . 0) * (1 - (s to_power (m + 1)))) / (1 - s) is ext-real V33() real Element of REAL
((n . 0) * (1 - (s to_power (m + 1)))) * ((1 - s) ") is ext-real V33() real set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(n) . m is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s to_power (m + 1) is ext-real V33() real set
s |^ (m + 1) is ext-real V33() real set
1 - (s to_power (m + 1)) is ext-real V33() real Element of REAL
- (s to_power (m + 1)) is ext-real V33() real set
1 + (- (s to_power (m + 1))) is ext-real V33() real set
(n . 0) * (1 - (s to_power (m + 1))) is ext-real V33() real Element of REAL
((n . 0) * (1 - (s to_power (m + 1)))) / (1 - s) is ext-real V33() real Element of REAL
((n . 0) * (1 - (s to_power (m + 1)))) * ((1 - s) ") is ext-real V33() real set
s is ext-real V33() real set
abs s is ext-real V33() real Element of REAL
s GeoSeq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((s GeoSeq)) is ext-real V33() real Element of REAL
((s GeoSeq)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((s GeoSeq)) is ext-real V33() real Element of REAL
1 - s is ext-real V33() real Element of REAL
- s is ext-real V33() real set
1 + (- s) is ext-real V33() real set
1 / (1 - s) is ext-real V33() real Element of REAL
(1 - s) " is ext-real V33() real set
1 * ((1 - s) ") is ext-real V33() real set
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim n is ext-real V33() real Element of REAL
m is ext-real V33() real set
m * (1 - s) is ext-real V33() real Element of REAL
0 * m is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n . s2 is ext-real V33() real Element of REAL
(n . s2) - 0 is ext-real V33() real Element of REAL
- 0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed set
(n . s2) + (- 0) is ext-real V33() real set
abs ((n . s2) - 0) is ext-real V33() real Element of REAL
s2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s to_power (s2 + 1) is ext-real V33() real set
s |^ (s2 + 1) is ext-real V33() real set
(s to_power (s2 + 1)) - 0 is ext-real V33() real Element of REAL
(s to_power (s2 + 1)) + (- 0) is ext-real V33() real set
abs ((s to_power (s2 + 1)) - 0) is ext-real V33() real Element of REAL
(m * (1 - s)) / (1 - s) is ext-real V33() real Element of REAL
(m * (1 - s)) * ((1 - s) ") is ext-real V33() real set
abs (s to_power (s2 + 1)) is ext-real V33() real Element of REAL
(abs (s to_power (s2 + 1))) / (1 - s) is ext-real V33() real Element of REAL
(abs (s to_power (s2 + 1))) * ((1 - s) ") is ext-real V33() real set
((s GeoSeq)) . s2 is ext-real V33() real Element of REAL
(((s GeoSeq)) . s2) - (1 / (1 - s)) is ext-real V33() real Element of REAL
- (1 / (1 - s)) is ext-real V33() real set
(((s GeoSeq)) . s2) + (- (1 / (1 - s))) is ext-real V33() real set
abs ((((s GeoSeq)) . s2) - (1 / (1 - s))) is ext-real V33() real Element of REAL
1 - (s to_power (s2 + 1)) is ext-real V33() real Element of REAL
- (s to_power (s2 + 1)) is ext-real V33() real set
1 + (- (s to_power (s2 + 1))) is ext-real V33() real set
(1 - (s to_power (s2 + 1))) / (1 - s) is ext-real V33() real Element of REAL
(1 - (s to_power (s2 + 1))) * ((1 - s) ") is ext-real V33() real set
((1 - (s to_power (s2 + 1))) / (1 - s)) - (1 / (1 - s)) is ext-real V33() real Element of REAL
((1 - (s to_power (s2 + 1))) / (1 - s)) + (- (1 / (1 - s))) is ext-real V33() real set
abs (((1 - (s to_power (s2 + 1))) / (1 - s)) - (1 / (1 - s))) is ext-real V33() real Element of REAL
1 + (- (s to_power (s2 + 1))) is ext-real V33() real Element of REAL
(1 + (- (s to_power (s2 + 1)))) - 1 is ext-real V33() real Element of REAL
- 1 is non empty ext-real non positive negative V33() real integer set
(1 + (- (s to_power (s2 + 1)))) + (- 1) is ext-real V33() real set
((1 + (- (s to_power (s2 + 1)))) - 1) / (1 - s) is ext-real V33() real Element of REAL
((1 + (- (s to_power (s2 + 1)))) - 1) * ((1 - s) ") is ext-real V33() real set
abs (((1 + (- (s to_power (s2 + 1)))) - 1) / (1 - s)) is ext-real V33() real Element of REAL
(s to_power (s2 + 1)) / (1 - s) is ext-real V33() real Element of REAL
(s to_power (s2 + 1)) * ((1 - s) ") is ext-real V33() real set
- ((s to_power (s2 + 1)) / (1 - s)) is ext-real V33() real Element of REAL
abs (- ((s to_power (s2 + 1)) / (1 - s))) is ext-real V33() real Element of REAL
abs ((s to_power (s2 + 1)) / (1 - s)) is ext-real V33() real Element of REAL
abs (1 - s) is ext-real V33() real Element of REAL
(abs (s to_power (s2 + 1))) / (abs (1 - s)) is ext-real V33() real Element of REAL
(abs (1 - s)) " is ext-real V33() real set
(abs (s to_power (s2 + 1))) * ((abs (1 - s)) ") is ext-real V33() real set
s is ext-real V33() real set
abs s is ext-real V33() real Element of REAL
1 - s is ext-real V33() real Element of REAL
- s is ext-real V33() real set
1 + (- s) is ext-real V33() real set
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(n) is ext-real V33() real Element of REAL
(n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (n) is ext-real V33() real Element of REAL
n . 0 is ext-real V33() real Element of REAL
(n . 0) / (1 - s) is ext-real V33() real Element of REAL
(1 - s) " is ext-real V33() real set
(n . 0) * ((1 - s) ") is ext-real V33() real set
s GeoSeq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n . m is ext-real V33() real Element of REAL
(s GeoSeq) . m is ext-real V33() real Element of REAL
(n . 0) * ((s GeoSeq) . m) is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n . (m + 1) is ext-real V33() real Element of REAL
(s GeoSeq) . (m + 1) is ext-real V33() real Element of REAL
(n . 0) * ((s GeoSeq) . (m + 1)) is ext-real V33() real Element of REAL
s * ((n . 0) * ((s GeoSeq) . m)) is ext-real V33() real Element of REAL
((s GeoSeq) . m) * s is ext-real V33() real Element of REAL
(n . 0) * (((s GeoSeq) . m) * s) is ext-real V33() real Element of REAL
(s GeoSeq) . 0 is ext-real V33() real Element of REAL
(n . 0) * ((s GeoSeq) . 0) is ext-real V33() real Element of REAL
(n . 0) (#) (s GeoSeq) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((s GeoSeq)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(n . 0) (#) ((s GeoSeq)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((s GeoSeq)) is ext-real V33() real Element of REAL
lim ((s GeoSeq)) is ext-real V33() real Element of REAL
1 / (1 - s) is ext-real V33() real Element of REAL
1 * ((1 - s) ") is ext-real V33() real set
(n . 0) * (1 / (1 - s)) is ext-real V33() real Element of REAL
(n . 0) * 1 is ext-real V33() real Element of REAL
((n . 0) * 1) / (1 - s) is ext-real V33() real Element of REAL
((n . 0) * 1) * ((1 - s) ") is ext-real V33() real set
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim n is ext-real V33() real Element of REAL
1 - (lim n) is ext-real V33() real Element of REAL
- (lim n) is ext-real V33() real set
1 + (- (lim n)) is ext-real V33() real set
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(1 - (lim n)) / 2 is ext-real V33() real Element of REAL
2 " is non empty ext-real positive non negative V33() real set
(1 - (lim n)) * (2 ") is ext-real V33() real set
0 + (lim n) is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 - ((1 - (lim n)) / 2) is ext-real V33() real Element of REAL
- ((1 - (lim n)) / 2) is ext-real V33() real set
1 + (- ((1 - (lim n)) / 2)) is ext-real V33() real set
(1 - ((1 - (lim n)) / 2)) GeoSeq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s . n is ext-real V33() real Element of REAL
- n is ext-real non positive V33() real integer Element of REAL
(1 - ((1 - (lim n)) / 2)) to_power (- n) is ext-real V33() real Element of REAL
(s . n) * ((1 - ((1 - (lim n)) / 2)) to_power (- n)) is ext-real V33() real Element of REAL
((s . n) * ((1 - ((1 - (lim n)) / 2)) to_power (- n))) (#) ((1 - ((1 - (lim n)) / 2)) GeoSeq) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . s2 is ext-real V33() real Element of REAL
s2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . (s2 + 1) is ext-real V33() real Element of REAL
(s . (s2 + 1)) / (s . s2) is ext-real V33() real Element of REAL
(s . s2) " is ext-real V33() real set
(s . (s2 + 1)) * ((s . s2) ") is ext-real V33() real set
n . s2 is ext-real V33() real Element of REAL
1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
- (lim n) is ext-real V33() real Element of REAL
1 + (- (lim n)) is ext-real V33() real Element of REAL
2 / 2 is non empty ext-real positive non negative V33() real Element of REAL
2 * (2 ") is non empty ext-real positive non negative V33() real set
((1 - (lim n)) / 2) + (lim n) is ext-real V33() real Element of REAL
s1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + s1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . (n + s1) is ext-real V33() real Element of REAL
(((s . n) * ((1 - ((1 - (lim n)) / 2)) to_power (- n))) (#) ((1 - ((1 - (lim n)) / 2)) GeoSeq)) . (n + s1) is ext-real V33() real Element of REAL
s1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + (s1 + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . (n + (s1 + 1)) is ext-real V33() real Element of REAL
(((s . n) * ((1 - ((1 - (lim n)) / 2)) to_power (- n))) (#) ((1 - ((1 - (lim n)) / 2)) GeoSeq)) . (n + (s1 + 1)) is ext-real V33() real Element of REAL
n . (n + s1) is ext-real V33() real Element of REAL
(n . (n + s1)) - (lim n) is ext-real V33() real Element of REAL
(n . (n + s1)) + (- (lim n)) is ext-real V33() real set
abs ((n . (n + s1)) - (lim n)) is ext-real V33() real Element of REAL
(n . (n + s1)) * ((((s . n) * ((1 - ((1 - (lim n)) / 2)) to_power (- n))) (#) ((1 - ((1 - (lim n)) / 2)) GeoSeq)) . (n + s1)) is ext-real V33() real Element of REAL
(1 - ((1 - (lim n)) / 2)) * ((((s . n) * ((1 - ((1 - (lim n)) / 2)) to_power (- n))) (#) ((1 - ((1 - (lim n)) / 2)) GeoSeq)) . (n + s1)) is ext-real V33() real Element of REAL
(n + s1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . ((n + s1) + 1) is ext-real V33() real Element of REAL
(s . ((n + s1) + 1)) / (s . (n + s1)) is ext-real V33() real Element of REAL
(s . (n + s1)) " is ext-real V33() real set
(s . ((n + s1) + 1)) * ((s . (n + s1)) ") is ext-real V33() real set
((s . ((n + s1) + 1)) / (s . (n + s1))) * (s . (n + s1)) is ext-real V33() real Element of REAL
(n . (n + s1)) * (s . (n + s1)) is ext-real V33() real Element of REAL
((1 - ((1 - (lim n)) / 2)) GeoSeq) . (n + s1) is ext-real V33() real Element of REAL
((s . n) * ((1 - ((1 - (lim n)) / 2)) to_power (- n))) * (((1 - ((1 - (lim n)) / 2)) GeoSeq) . (n + s1)) is ext-real V33() real Element of REAL
(1 - ((1 - (lim n)) / 2)) * (((s . n) * ((1 - ((1 - (lim n)) / 2)) to_power (- n))) * (((1 - ((1 - (lim n)) / 2)) GeoSeq) . (n + s1))) is ext-real V33() real Element of REAL
(((1 - ((1 - (lim n)) / 2)) GeoSeq) . (n + s1)) * (1 - ((1 - (lim n)) / 2)) is ext-real V33() real Element of REAL
((s . n) * ((1 - ((1 - (lim n)) / 2)) to_power (- n))) * ((((1 - ((1 - (lim n)) / 2)) GeoSeq) . (n + s1)) * (1 - ((1 - (lim n)) / 2))) is ext-real V33() real Element of REAL
((1 - ((1 - (lim n)) / 2)) GeoSeq) . ((n + s1) + 1) is ext-real V33() real Element of REAL
((s . n) * ((1 - ((1 - (lim n)) / 2)) to_power (- n))) * (((1 - ((1 - (lim n)) / 2)) GeoSeq) . ((n + s1) + 1)) is ext-real V33() real Element of REAL
n + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(((s . n) * ((1 - ((1 - (lim n)) / 2)) to_power (- n))) (#) ((1 - ((1 - (lim n)) / 2)) GeoSeq)) . (n + 0) is ext-real V33() real Element of REAL
((1 - ((1 - (lim n)) / 2)) GeoSeq) . n is ext-real V33() real Element of REAL
((s . n) * ((1 - ((1 - (lim n)) / 2)) to_power (- n))) * (((1 - ((1 - (lim n)) / 2)) GeoSeq) . n) is ext-real V33() real Element of REAL
(1 - ((1 - (lim n)) / 2)) |^ n is ext-real V33() real Element of REAL
((s . n) * ((1 - ((1 - (lim n)) / 2)) to_power (- n))) * ((1 - ((1 - (lim n)) / 2)) |^ n) is ext-real V33() real Element of REAL
(1 - ((1 - (lim n)) / 2)) to_power n is ext-real V33() real Element of REAL
(1 - ((1 - (lim n)) / 2)) |^ n is ext-real V33() real set
((1 - ((1 - (lim n)) / 2)) to_power (- n)) * ((1 - ((1 - (lim n)) / 2)) to_power n) is ext-real V33() real Element of REAL
(s . n) * (((1 - ((1 - (lim n)) / 2)) to_power (- n)) * ((1 - ((1 - (lim n)) / 2)) to_power n)) is ext-real V33() real Element of REAL
(- n) + n is ext-real V33() real integer Element of REAL
(1 - ((1 - (lim n)) / 2)) to_power ((- n) + n) is ext-real V33() real Element of REAL
(s . n) * ((1 - ((1 - (lim n)) / 2)) to_power ((- n) + n)) is ext-real V33() real Element of REAL
(s . n) * 1 is ext-real V33() real Element of REAL
s . (n + 0) is ext-real V33() real Element of REAL
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
n + s1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . s2 is ext-real V33() real Element of REAL
(((s . n) * ((1 - ((1 - (lim n)) / 2)) to_power (- n))) (#) ((1 - ((1 - (lim n)) / 2)) GeoSeq)) . s2 is ext-real V33() real Element of REAL
1 - 0 is non empty ext-real positive non negative V33() real integer Element of REAL
- 0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed set
1 + (- 0) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
2 * 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2 * 2) / 2 is non empty ext-real positive non negative V33() real Element of REAL
(2 * 2) * (2 ") is non empty ext-real positive non negative V33() real set
((1 - (lim n)) / 2) - 1 is ext-real V33() real Element of REAL
- 1 is non empty ext-real non positive negative V33() real integer set
((1 - (lim n)) / 2) + (- 1) is ext-real V33() real set
- (((1 - (lim n)) / 2) - 1) is ext-real V33() real Element of REAL
abs (1 - ((1 - (lim n)) / 2)) is ext-real V33() real Element of REAL
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . s2 is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . (n + m) is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + (m + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . (n + (m + 1)) is ext-real V33() real Element of REAL
(n + m) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . ((n + m) + 1) is ext-real V33() real Element of REAL
(s . ((n + m) + 1)) / (s . (n + m)) is ext-real V33() real Element of REAL
(s . (n + m)) " is ext-real V33() real set
(s . ((n + m) + 1)) * ((s . (n + m)) ") is ext-real V33() real set
n + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . (n + 0) is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . n is ext-real V33() real Element of REAL
(s . n) - 0 is ext-real V33() real Element of REAL
- 0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed set
(s . n) + (- 0) is ext-real V33() real set
abs ((s . n) - 0) is ext-real V33() real Element of REAL
lim s is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim n is ext-real V33() real Element of REAL
n ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of n
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(n ^\ 1) . m is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n . (m + 1) is ext-real V33() real Element of REAL
s . (m + 1) is ext-real V33() real Element of REAL
(m + 1) -root (s . (m + 1)) is ext-real V33() real Element of REAL
1 - (lim n) is ext-real V33() real Element of REAL
- (lim n) is ext-real V33() real set
1 + (- (lim n)) is ext-real V33() real set
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(1 - (lim n)) / 2 is ext-real V33() real Element of REAL
2 " is non empty ext-real positive non negative V33() real set
(1 - (lim n)) * (2 ") is ext-real V33() real set
0 + (lim n) is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
lim (n ^\ 1) is ext-real V33() real Element of REAL
1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
- (lim n) is ext-real V33() real Element of REAL
1 + (- (lim n)) is ext-real V33() real Element of REAL
2 / 2 is non empty ext-real positive non negative V33() real Element of REAL
2 * (2 ") is non empty ext-real positive non negative V33() real set
1 - ((1 - (lim n)) / 2) is ext-real V33() real Element of REAL
- ((1 - (lim n)) / 2) is ext-real V33() real set
1 + (- ((1 - (lim n)) / 2)) is ext-real V33() real set
(1 - ((1 - (lim n)) / 2)) GeoSeq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((1 - (lim n)) / 2) + (lim n) is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . s2 is ext-real V33() real Element of REAL
(1 - ((1 - (lim n)) / 2)) to_power s2 is ext-real V33() real Element of REAL
(1 - ((1 - (lim n)) / 2)) |^ s2 is ext-real V33() real set
n . s2 is ext-real V33() real Element of REAL
(n . s2) - (lim n) is ext-real V33() real Element of REAL
(n . s2) + (- (lim n)) is ext-real V33() real set
abs ((n . s2) - (lim n)) is ext-real V33() real Element of REAL
s2 -root (s . s2) is ext-real V33() real Element of REAL
s2 -Root (s . s2) is ext-real V33() real Element of REAL
(s2 -root (s . s2)) to_power s2 is ext-real V33() real Element of REAL
(s2 -root (s . s2)) |^ s2 is ext-real V33() real set
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . s2 is ext-real V33() real Element of REAL
((1 - ((1 - (lim n)) / 2)) GeoSeq) . s2 is ext-real V33() real Element of REAL
(1 - ((1 - (lim n)) / 2)) to_power s2 is ext-real V33() real Element of REAL
(1 - ((1 - (lim n)) / 2)) |^ s2 is ext-real V33() real set
1 - 0 is non empty ext-real positive non negative V33() real integer Element of REAL
- 0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed set
1 + (- 0) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
2 * 2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2 * 2) / 2 is non empty ext-real positive non negative V33() real Element of REAL
(2 * 2) * (2 ") is non empty ext-real positive non negative V33() real set
((1 - (lim n)) / 2) - 1 is ext-real V33() real Element of REAL
- 1 is non empty ext-real non positive negative V33() real integer set
((1 - (lim n)) / 2) + (- 1) is ext-real V33() real set
- (((1 - (lim n)) / 2) - 1) is ext-real V33() real Element of REAL
abs (1 - ((1 - (lim n)) / 2)) is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . n is ext-real V33() real Element of REAL
1 + m is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n . n is ext-real V33() real Element of REAL
n -root (s . n) is ext-real V33() real Element of REAL
1 |^ n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(n -root (s . n)) to_power n is ext-real V33() real Element of REAL
(n -root (s . n)) |^ n is ext-real V33() real set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(m + 1) + n is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . k is ext-real V33() real Element of REAL
(s . k) - 0 is ext-real V33() real Element of REAL
- 0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed set
(s . k) + (- 0) is ext-real V33() real set
abs ((s . k) - 0) is ext-real V33() real Element of REAL
lim s is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim n is ext-real V33() real Element of REAL
(lim n) - 1 is ext-real V33() real Element of REAL
- 1 is non empty ext-real non positive negative V33() real integer set
(lim n) + (- 1) is ext-real V33() real set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n . k is ext-real V33() real Element of REAL
(n . k) - (lim n) is ext-real V33() real Element of REAL
- (lim n) is ext-real V33() real set
(n . k) + (- (lim n)) is ext-real V33() real set
abs ((n . k) - (lim n)) is ext-real V33() real Element of REAL
- ((lim n) - 1) is ext-real V33() real Element of REAL
((n . k) - (lim n)) + (lim n) is ext-real V33() real Element of REAL
(- ((lim n) - 1)) + (lim n) is ext-real V33() real Element of REAL
s is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
s to_power n is ext-real V33() real set
s |^ n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
s is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
s to_power n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
s |^ n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2,(0 + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ (0 + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(s) . (2,(0 + 1)) is ext-real V33() real Element of REAL
1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . (1 + 1) is ext-real V33() real Element of REAL
(s) . (0 + 1) is ext-real V33() real Element of REAL
s . 2 is ext-real V33() real Element of REAL
((s) . (0 + 1)) + (s . 2) is ext-real V33() real Element of REAL
(s) . 0 is ext-real V33() real Element of REAL
s . 1 is ext-real V33() real Element of REAL
((s) . 0) + (s . 1) is ext-real V33() real Element of REAL
(((s) . 0) + (s . 1)) + (s . 2) is ext-real V33() real Element of REAL
s . 0 is ext-real V33() real Element of REAL
(s . 0) + (s . 1) is ext-real V33() real Element of REAL
((s . 0) + (s . 1)) + (s . 2) is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2,m) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
s . (2,m) is ext-real V33() real Element of REAL
(2,m) * (s . (2,m)) is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
(n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(n) . m is ext-real V33() real Element of REAL
(2,m) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(s) . (2,m) is ext-real V33() real Element of REAL
2 * ((s) . (2,m)) is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(n) . (m + 1) is ext-real V33() real Element of REAL
(2,(m + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ (m + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(s) . (2,(m + 1)) is ext-real V33() real Element of REAL
2 * ((s) . (2,(m + 1))) is ext-real V33() real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s . (2,(m + 1)) is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k * (s . (2,(m + 1))) is ext-real V33() real Element of REAL
n . k is ext-real V33() real Element of REAL
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(k + 1) * (s . (2,(m + 1))) is ext-real V33() real Element of REAL
n . (k + 1) is ext-real V33() real Element of REAL
(2,m) + (k + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2,m) + (2,m) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2,m) + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((2,m) + k) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 * (2,m) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2,1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(2,1) * (2,m) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . (((2,m) + k) + 1) is ext-real V33() real Element of REAL
1 * (s . (2,(m + 1))) is ext-real V33() real Element of REAL
(k * (s . (2,(m + 1)))) + (1 * (s . (2,(m + 1)))) is ext-real V33() real Element of REAL
(n . k) + (s . (((2,m) + k) + 1)) is ext-real V33() real Element of REAL
(s) . ((2,m) + k) is ext-real V33() real Element of REAL
((s) . ((2,m) + k)) - ((s) . (2,m)) is ext-real V33() real Element of REAL
- ((s) . (2,m)) is ext-real V33() real set
((s) . ((2,m) + k)) + (- ((s) . (2,m))) is ext-real V33() real set
(((s) . ((2,m) + k)) - ((s) . (2,m))) + (s . (((2,m) + k) + 1)) is ext-real V33() real Element of REAL
((s) . ((2,m) + k)) + (s . (((2,m) + k) + 1)) is ext-real V33() real Element of REAL
(((s) . ((2,m) + k)) + (s . (((2,m) + k) + 1))) - ((s) . (2,m)) is ext-real V33() real Element of REAL
(((s) . ((2,m) + k)) + (s . (((2,m) + k) + 1))) + (- ((s) . (2,m))) is ext-real V33() real set
(s) . ((2,m) + (k + 1)) is ext-real V33() real Element of REAL
((s) . ((2,m) + (k + 1))) - ((s) . (2,m)) is ext-real V33() real Element of REAL
((s) . ((2,m) + (k + 1))) + (- ((s) . (2,m))) is ext-real V33() real set
n . 0 is ext-real V33() real Element of REAL
(2,m) + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . ((2,m) + 0) is ext-real V33() real Element of REAL
((s) . ((2,m) + 0)) - ((s) . (2,m)) is ext-real V33() real Element of REAL
- ((s) . (2,m)) is ext-real V33() real set
((s) . ((2,m) + 0)) + (- ((s) . (2,m))) is ext-real V33() real set
0 * (s . (2,(m + 1))) is ext-real V33() real Element of REAL
(2,m) * (s . (2,(m + 1))) is ext-real V33() real Element of REAL
2 * ((2,m) * (s . (2,(m + 1)))) is ext-real V33() real Element of REAL
n . (2,m) is ext-real V33() real Element of REAL
2 * (n . (2,m)) is ext-real V33() real Element of REAL
2 * (2,m) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2 * (2,m)) * (s . (2,(m + 1))) is ext-real V33() real Element of REAL
(2,1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(2,1) * (2,m) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((2,1) * (2,m)) * (s . (2,(m + 1))) is ext-real V33() real Element of REAL
(2,(m + 1)) * (s . (2,(m + 1))) is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
(2,m) + (2,m) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . ((2,m) + (2,m)) is ext-real V33() real Element of REAL
((s) . ((2,m) + (2,m))) - ((s) . (2,m)) is ext-real V33() real Element of REAL
((s) . ((2,m) + (2,m))) + (- ((s) . (2,m))) is ext-real V33() real set
2 * (((s) . ((2,m) + (2,m))) - ((s) . (2,m))) is ext-real V33() real Element of REAL
(2 * ((s) . (2,m))) + (n . (m + 1)) is ext-real V33() real Element of REAL
(2 * ((s) . (2,m))) + (2 * (((s) . ((2,m) + (2,m))) - ((s) . (2,m)))) is ext-real V33() real Element of REAL
((n) . m) + (n . (m + 1)) is ext-real V33() real Element of REAL
(2,0) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(s) . (2,0) is ext-real V33() real Element of REAL
2 * ((s) . (2,0)) is ext-real V33() real Element of REAL
2 * (((s) . 0) + (s . 1)) is ext-real V33() real Element of REAL
2 * ((s . 0) + (s . 1)) is ext-real V33() real Element of REAL
2 * (s . 0) is ext-real V33() real Element of REAL
2 * (s . 1) is ext-real V33() real Element of REAL
(2 * (s . 0)) + (2 * (s . 1)) is ext-real V33() real Element of REAL
m is ext-real V33() real set
(s . 1) + 0 is ext-real V33() real Element of REAL
(s . 1) + (s . 1) is ext-real V33() real Element of REAL
(n) . 0 is ext-real V33() real Element of REAL
n . 0 is ext-real V33() real Element of REAL
1 * (s . 1) is ext-real V33() real Element of REAL
2 * m is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2,n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(s) . (2,n) is ext-real V33() real Element of REAL
2 * ((s) . (2,n)) is ext-real V33() real Element of REAL
(n) . n is ext-real V33() real Element of REAL
(n) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real V33() real set
(2,0) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2,(n + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ (n + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(s) . (2,(n + 1)) is ext-real V33() real Element of REAL
(n) . n is ext-real V33() real Element of REAL
((n) . n) + (s . 0) is ext-real V33() real Element of REAL
(((n) . n) + (s . 0)) + (s . 2) is ext-real V33() real Element of REAL
(n + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2,((n + 1) + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ ((n + 1) + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(s) . (2,((n + 1) + 1)) is ext-real V33() real Element of REAL
(n) . (n + 1) is ext-real V33() real Element of REAL
((n) . (n + 1)) + (s . 0) is ext-real V33() real Element of REAL
(((n) . (n + 1)) + (s . 0)) + (s . 2) is ext-real V33() real Element of REAL
s . (2,(n + 1)) is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2,(n + 1)) + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . ((2,(n + 1)) + k) is ext-real V33() real Element of REAL
((s) . ((2,(n + 1)) + k)) - ((s) . (2,(n + 1))) is ext-real V33() real Element of REAL
- ((s) . (2,(n + 1))) is ext-real V33() real set
((s) . ((2,(n + 1)) + k)) + (- ((s) . (2,(n + 1)))) is ext-real V33() real set
k * (s . (2,(n + 1))) is ext-real V33() real Element of REAL
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2,(n + 1)) + (k + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . ((2,(n + 1)) + (k + 1)) is ext-real V33() real Element of REAL
((s) . ((2,(n + 1)) + (k + 1))) - ((s) . (2,(n + 1))) is ext-real V33() real Element of REAL
((s) . ((2,(n + 1)) + (k + 1))) + (- ((s) . (2,(n + 1)))) is ext-real V33() real set
(k + 1) * (s . (2,(n + 1))) is ext-real V33() real Element of REAL
s . ((2,(n + 1)) + (k + 1)) is ext-real V33() real Element of REAL
((2,(n + 1)) + k) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . (((2,(n + 1)) + k) + 1) is ext-real V33() real Element of REAL
(((s) . ((2,(n + 1)) + k)) - ((s) . (2,(n + 1)))) + (s . (((2,(n + 1)) + k) + 1)) is ext-real V33() real Element of REAL
(k * (s . (2,(n + 1)))) + (s . (2,(n + 1))) is ext-real V33() real Element of REAL
((s) . ((2,(n + 1)) + k)) + (s . (((2,(n + 1)) + k) + 1)) is ext-real V33() real Element of REAL
(((s) . ((2,(n + 1)) + k)) + (s . (((2,(n + 1)) + k) + 1))) - ((s) . (2,(n + 1))) is ext-real V33() real Element of REAL
(((s) . ((2,(n + 1)) + k)) + (s . (((2,(n + 1)) + k) + 1))) + (- ((s) . (2,(n + 1)))) is ext-real V33() real set
(2,(n + 1)) + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . ((2,(n + 1)) + 0) is ext-real V33() real Element of REAL
((s) . ((2,(n + 1)) + 0)) - ((s) . (2,(n + 1))) is ext-real V33() real Element of REAL
- ((s) . (2,(n + 1))) is ext-real V33() real set
((s) . ((2,(n + 1)) + 0)) + (- ((s) . (2,(n + 1)))) is ext-real V33() real set
0 * (s . (2,(n + 1))) is ext-real V33() real Element of REAL
(2,(n + 1)) + (2,(n + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . ((2,(n + 1)) + (2,(n + 1))) is ext-real V33() real Element of REAL
((s) . ((2,(n + 1)) + (2,(n + 1)))) - ((s) . (2,(n + 1))) is ext-real V33() real Element of REAL
((s) . ((2,(n + 1)) + (2,(n + 1)))) + (- ((s) . (2,(n + 1)))) is ext-real V33() real set
(2,(n + 1)) * (s . (2,(n + 1))) is ext-real V33() real Element of REAL
n . (n + 1) is ext-real V33() real Element of REAL
((s) . (2,(n + 1))) + (n . (n + 1)) is ext-real V33() real Element of REAL
(n . (n + 1)) + ((((n) . n) + (s . 0)) + (s . 2)) is ext-real V33() real Element of REAL
((n) . n) + (n . (n + 1)) is ext-real V33() real Element of REAL
(((n) . n) + (n . (n + 1))) + (s . 0) is ext-real V33() real Element of REAL
((((n) . n) + (n . (n + 1))) + (s . 0)) + (s . 2) is ext-real V33() real Element of REAL
2 * (2,(n + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2,1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(2,1) * (2,(n + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((s) . (2,((n + 1) + 1))) - ((s) . (2,(n + 1))) is ext-real V33() real Element of REAL
((s) . (2,((n + 1) + 1))) + (- ((s) . (2,(n + 1)))) is ext-real V33() real set
(((s) . (2,((n + 1) + 1))) - ((s) . (2,(n + 1)))) + ((s) . (2,(n + 1))) is ext-real V33() real Element of REAL
(n) . 0 is ext-real V33() real Element of REAL
((n) . 0) + (s . 0) is ext-real V33() real Element of REAL
(((n) . 0) + (s . 0)) + (s . 2) is ext-real V33() real Element of REAL
n . 0 is ext-real V33() real Element of REAL
(n . 0) + (s . 0) is ext-real V33() real Element of REAL
((n . 0) + (s . 0)) + (s . 2) is ext-real V33() real Element of REAL
s . (2,0) is ext-real V33() real Element of REAL
(2,0) * (s . (2,0)) is ext-real V33() real Element of REAL
((2,0) * (s . (2,0))) + (s . 0) is ext-real V33() real Element of REAL
(((2,0) * (s . (2,0))) + (s . 0)) + (s . 2) is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(n) . n is ext-real V33() real Element of REAL
(s . 0) + (s . 2) is ext-real V33() real Element of REAL
m + ((s . 0) + (s . 2)) is ext-real V33() real Element of REAL
((n) . n) + ((s . 0) + (s . 2)) is ext-real V33() real Element of REAL
n * 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 + (n * 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((1 + 1),n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(1 + 1) |^ n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
1 + n is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2,n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
n + n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2,n) + (2,n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 * (2,n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2,1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(2,1) * (2,n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2,(n + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ (n + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(s) . n is ext-real V33() real Element of REAL
(s) . (2,(n + 1)) is ext-real V33() real Element of REAL
((n) . n) + (s . 0) is ext-real V33() real Element of REAL
(((n) . n) + (s . 0)) + (s . 2) is ext-real V33() real Element of REAL
s is ext-real V33() real set
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m to_power s is ext-real V33() real set
1 / (m to_power s) is ext-real V33() real Element of REAL
(m to_power s) " is ext-real V33() real set
1 * ((m to_power s) ") is ext-real V33() real set
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m . 0 is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(k + 1) #R s is ext-real V33() real set
(k + 1) to_power s is ext-real V33() real set
m . (k + 1) is ext-real V33() real Element of REAL
1 / ((k + 1) to_power s) is ext-real V33() real Element of REAL
((k + 1) to_power s) " is ext-real V33() real set
1 * (((k + 1) to_power s) ") is ext-real V33() real set
m . k is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k to_power s is ext-real V33() real set
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
s2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 / (k to_power s) is ext-real V33() real Element of REAL
(k to_power s) " is ext-real V33() real set
1 * ((k to_power s) ") is ext-real V33() real set
m . k is ext-real V33() real Element of REAL
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k / (k + 1) is ext-real non negative V33() real Element of REAL
(k + 1) " is non empty ext-real positive non negative V33() real set
k * ((k + 1) ") is ext-real non negative V33() real set
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
s2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . (k + 1) is ext-real V33() real Element of REAL
(m . (k + 1)) / (m . k) is ext-real V33() real Element of REAL
(m . k) " is ext-real V33() real set
(m . (k + 1)) * ((m . k) ") is ext-real V33() real set
(k + 1) to_power s is ext-real V33() real set
1 / ((k + 1) to_power s) is ext-real V33() real Element of REAL
((k + 1) to_power s) " is ext-real V33() real set
1 * (((k + 1) to_power s) ") is ext-real V33() real set
(1 / ((k + 1) to_power s)) / (m . k) is ext-real V33() real Element of REAL
(1 / ((k + 1) to_power s)) * ((m . k) ") is ext-real V33() real set
(1 / ((k + 1) to_power s)) / (1 / (k to_power s)) is ext-real V33() real Element of REAL
(1 / (k to_power s)) " is ext-real V33() real set
(1 / ((k + 1) to_power s)) * ((1 / (k to_power s)) ") is ext-real V33() real set
(1 / ((k + 1) to_power s)) * (k to_power s) is ext-real V33() real Element of REAL
(k to_power s) / ((k + 1) to_power s) is ext-real V33() real Element of COMPLEX
(k to_power s) * (((k + 1) to_power s) ") is ext-real V33() real set
(k / (k + 1)) to_power s is ext-real V33() real set
(k / (k + 1)) #R s is ext-real V33() real set
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
s2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
s2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(k / (k + 1)) #R 0 is ext-real V33() real Element of REAL
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
s2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . (k + 1) is ext-real V33() real Element of REAL
m . k is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . (k + 1) is ext-real V33() real Element of REAL
m . k is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of n
(n ^\ 1) . k is ext-real V33() real Element of REAL
n . (k + 1) is ext-real V33() real Element of REAL
(k + 1) to_power s is ext-real V33() real set
1 / ((k + 1) to_power s) is ext-real V33() real Element of REAL
((k + 1) to_power s) " is ext-real V33() real set
1 * (((k + 1) to_power s) ") is ext-real V33() real set
m . (k + 1) is ext-real V33() real Element of REAL
m ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of m
(m ^\ 1) . k is ext-real V33() real Element of REAL
k is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(2,s2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
n . s2 is ext-real V33() real Element of REAL
m . (2,s2) is ext-real V33() real Element of REAL
(2,s2) * (m . (2,s2)) is ext-real V33() real Element of REAL
(2,s2) to_power s is ext-real V33() real set
1 / ((2,s2) to_power s) is ext-real V33() real Element of REAL
((2,s2) to_power s) " is ext-real V33() real set
1 * (((2,s2) to_power s) ") is ext-real V33() real set
(2,s2) * (1 / ((2,s2) to_power s)) is ext-real V33() real Element of REAL
s2 * s is ext-real V33() real Element of REAL
2 to_power (s2 * s) is ext-real V33() real Element of REAL
1 / (2 to_power (s2 * s)) is ext-real V33() real Element of REAL
(2 to_power (s2 * s)) " is ext-real V33() real set
1 * ((2 to_power (s2 * s)) ") is ext-real V33() real set
(2,s2) * (1 / (2 to_power (s2 * s))) is ext-real V33() real Element of REAL
- (s2 * s) is ext-real V33() real Element of REAL
2 to_power (- (s2 * s)) is ext-real V33() real Element of REAL
(2,s2) * (2 to_power (- (s2 * s))) is ext-real V33() real Element of REAL
s2 + (- (s2 * s)) is ext-real V33() real Element of REAL
2 to_power (s2 + (- (s2 * s))) is ext-real V33() real Element of REAL
1 - s is ext-real V33() real Element of REAL
- s is ext-real V33() real set
1 + (- s) is ext-real V33() real set
(1 - s) * s2 is ext-real V33() real Element of REAL
2 to_power ((1 - s) * s2) is ext-real V33() real Element of REAL
2 to_power (1 - s) is ext-real V33() real Element of REAL
(2 to_power (1 - s)) to_power s2 is ext-real V33() real Element of REAL
(2 to_power (1 - s)) |^ s2 is ext-real V33() real set
k . s2 is ext-real V33() real Element of REAL
s2 -root ((2 to_power (1 - s)) to_power s2) is ext-real V33() real Element of REAL
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
s2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of k
(k ^\ 1) . s2 is ext-real V33() real Element of REAL
k . (s2 + 1) is ext-real V33() real Element of REAL
(2 to_power (1 - s)) to_power (s2 + 1) is ext-real V33() real Element of REAL
(2 to_power (1 - s)) |^ (s2 + 1) is ext-real V33() real set
(s2 + 1) -root ((2 to_power (1 - s)) to_power (s2 + 1)) is ext-real V33() real Element of REAL
lim (k ^\ 1) is ext-real V33() real Element of REAL
(k ^\ 1) . 0 is ext-real V33() real Element of REAL
lim k is ext-real V33() real Element of REAL
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . s2 is ext-real V33() real Element of REAL
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s2 to_power s is ext-real V33() real set
s1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
s1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 / (s2 to_power s) is ext-real V33() real Element of REAL
(s2 to_power s) " is ext-real V33() real set
1 * ((s2 to_power s) ") is ext-real V33() real set
m . s2 is ext-real V33() real Element of REAL
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . s2 is ext-real V33() real Element of REAL
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . s2 is ext-real V33() real Element of REAL
n . s2 is ext-real V33() real Element of REAL
(2,s2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
m . (2,s2) is ext-real V33() real Element of REAL
(2,s2) * (m . (2,s2)) is ext-real V33() real Element of REAL
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . (s2 + 1) is ext-real V33() real Element of REAL
(n ^\ 1) . s2 is ext-real V33() real Element of REAL
n . (s2 + 1) is ext-real V33() real Element of REAL
(s2 + 1) to_power s is ext-real V33() real set
1 / ((s2 + 1) to_power s) is ext-real V33() real Element of REAL
((s2 + 1) to_power s) " is ext-real V33() real set
1 * (((s2 + 1) to_power s) ") is ext-real V33() real set
(m ^\ 1) . s2 is ext-real V33() real Element of REAL
s is ext-real V33() real set
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n . k is ext-real V33() real Element of REAL
(n . k) - 0 is ext-real V33() real Element of REAL
- 0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed set
(n . k) + (- 0) is ext-real V33() real set
abs ((n . k) - 0) is ext-real V33() real Element of REAL
k to_power s is ext-real V33() real set
1 / (k to_power s) is ext-real V33() real Element of REAL
(k to_power s) " is ext-real V33() real set
1 * ((k to_power s) ") is ext-real V33() real set
abs (1 / (k to_power s)) is ext-real V33() real Element of REAL
- s is ext-real V33() real set
k to_power (- s) is ext-real V33() real set
abs (k to_power (- s)) is ext-real V33() real Element of REAL
k #R (- s) is ext-real V33() real set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m to_power s is ext-real V33() real set
1 / (m to_power s) is ext-real V33() real Element of REAL
(m to_power s) " is ext-real V33() real set
1 * ((m to_power s) ") is ext-real V33() real set
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m . 0 is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(n + 1) #R s is ext-real V33() real set
(n + 1) to_power s is ext-real V33() real set
m . (n + 1) is ext-real V33() real Element of REAL
1 / ((n + 1) to_power s) is ext-real V33() real Element of REAL
((n + 1) to_power s) " is ext-real V33() real set
1 * (((n + 1) to_power s) ") is ext-real V33() real set
m . n is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n to_power s is ext-real V33() real set
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 / (n to_power s) is ext-real V33() real Element of REAL
(n to_power s) " is ext-real V33() real set
1 * ((n to_power s) ") is ext-real V33() real set
m . n is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n / (n + 1) is ext-real non negative V33() real Element of REAL
(n + 1) " is non empty ext-real positive non negative V33() real set
n * ((n + 1) ") is ext-real non negative V33() real set
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . (n + 1) is ext-real V33() real Element of REAL
(m . (n + 1)) / (m . n) is ext-real V33() real Element of REAL
(m . n) " is ext-real V33() real set
(m . (n + 1)) * ((m . n) ") is ext-real V33() real set
(n + 1) to_power s is ext-real V33() real set
1 / ((n + 1) to_power s) is ext-real V33() real Element of REAL
((n + 1) to_power s) " is ext-real V33() real set
1 * (((n + 1) to_power s) ") is ext-real V33() real set
(1 / ((n + 1) to_power s)) / (m . n) is ext-real V33() real Element of REAL
(1 / ((n + 1) to_power s)) * ((m . n) ") is ext-real V33() real set
(1 / ((n + 1) to_power s)) / (1 / (n to_power s)) is ext-real V33() real Element of REAL
(1 / (n to_power s)) " is ext-real V33() real set
(1 / ((n + 1) to_power s)) * ((1 / (n to_power s)) ") is ext-real V33() real set
(1 / ((n + 1) to_power s)) * (n to_power s) is ext-real V33() real Element of REAL
(n to_power s) / ((n + 1) to_power s) is ext-real V33() real Element of COMPLEX
(n to_power s) * (((n + 1) to_power s) ") is ext-real V33() real set
(n / (n + 1)) to_power s is ext-real V33() real set
(n / (n + 1)) #R s is ext-real V33() real set
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(n / (n + 1)) #R 0 is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . (n + 1) is ext-real V33() real Element of REAL
m . n is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . (n + 1) is ext-real V33() real Element of REAL
m . n is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n . n is ext-real V33() real Element of REAL
n to_power s is ext-real V33() real set
1 / (n to_power s) is ext-real V33() real Element of REAL
(n to_power s) " is ext-real V33() real set
1 * ((n to_power s) ") is ext-real V33() real set
m . n is ext-real V33() real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . k is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k to_power s is ext-real V33() real set
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
s2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 / (k to_power s) is ext-real V33() real Element of REAL
(k to_power s) " is ext-real V33() real set
1 * ((k to_power s) ") is ext-real V33() real set
m . k is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . k is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . k is ext-real V33() real Element of REAL
n . k is ext-real V33() real Element of REAL
(2,k) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
m . (2,k) is ext-real V33() real Element of REAL
(2,k) * (m . (2,k)) is ext-real V33() real Element of REAL
lim n is ext-real V33() real Element of REAL
1 / 2 is non empty ext-real positive non negative V33() real Element of REAL
2 " is non empty ext-real positive non negative V33() real set
1 * (2 ") is non empty ext-real positive non negative V33() real set
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n . s2 is ext-real V33() real Element of REAL
(n . s2) - 0 is ext-real V33() real Element of REAL
- 0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed set
(n . s2) + (- 0) is ext-real V33() real set
abs ((n . s2) - 0) is ext-real V33() real Element of REAL
(2,s2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ s2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
m . (2,s2) is ext-real V33() real Element of REAL
(2,s2) * (m . (2,s2)) is ext-real V33() real Element of REAL
abs ((2,s2) * (m . (2,s2))) is ext-real V33() real Element of REAL
(2,s2) to_power s is ext-real V33() real set
1 / ((2,s2) to_power s) is ext-real V33() real Element of REAL
((2,s2) to_power s) " is ext-real V33() real set
1 * (((2,s2) to_power s) ") is ext-real V33() real set
(2,s2) * (1 / ((2,s2) to_power s)) is ext-real V33() real Element of REAL
abs ((2,s2) * (1 / ((2,s2) to_power s))) is ext-real V33() real Element of REAL
s2 * s is ext-real V33() real Element of REAL
2 to_power (s2 * s) is ext-real V33() real Element of REAL
1 / (2 to_power (s2 * s)) is ext-real V33() real Element of REAL
(2 to_power (s2 * s)) " is ext-real V33() real set
1 * ((2 to_power (s2 * s)) ") is ext-real V33() real set
(2,s2) * (1 / (2 to_power (s2 * s))) is ext-real V33() real Element of REAL
abs ((2,s2) * (1 / (2 to_power (s2 * s)))) is ext-real V33() real Element of REAL
- (s2 * s) is ext-real V33() real Element of REAL
2 to_power (- (s2 * s)) is ext-real V33() real Element of REAL
(2,s2) * (2 to_power (- (s2 * s))) is ext-real V33() real Element of REAL
abs ((2,s2) * (2 to_power (- (s2 * s)))) is ext-real V33() real Element of REAL
s2 + (- (s2 * s)) is ext-real V33() real Element of REAL
2 to_power (s2 + (- (s2 * s))) is ext-real V33() real Element of REAL
abs (2 to_power (s2 + (- (s2 * s)))) is ext-real V33() real Element of REAL
s2 - (s2 * s) is ext-real V33() real Element of REAL
- (s2 * s) is ext-real V33() real set
s2 + (- (s2 * s)) is ext-real V33() real set
2 to_power (s2 - (s2 * s)) is ext-real V33() real Element of REAL
(1 / 2) * 2 is non empty ext-real positive non negative V33() real Element of REAL
(2 to_power (s2 - (s2 * s))) * 2 is ext-real V33() real Element of REAL
(2,1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
2 |^ 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(2 to_power (s2 - (s2 * s))) * (2,1) is ext-real V33() real Element of REAL
(s2 - (s2 * s)) + 1 is ext-real V33() real Element of REAL
2 to_power ((s2 - (s2 * s)) + 1) is ext-real V33() real Element of REAL
1 - s is ext-real V33() real Element of REAL
- s is ext-real V33() real set
1 + (- s) is ext-real V33() real set
s2 * (1 - s) is ext-real V33() real Element of REAL
2 #R ((s2 - (s2 * s)) + 1) is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((abs s)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . n is ext-real V33() real Element of REAL
((abs s)) . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . m is ext-real V33() real Element of REAL
((s) . m) - ((s) . n) is ext-real V33() real Element of REAL
- ((s) . n) is ext-real V33() real set
((s) . m) + (- ((s) . n)) is ext-real V33() real set
abs (((s) . m) - ((s) . n)) is ext-real V33() real Element of REAL
((abs s)) . m is ext-real V33() real Element of REAL
(((abs s)) . m) - (((abs s)) . n) is ext-real V33() real Element of REAL
- (((abs s)) . n) is ext-real V33() real set
(((abs s)) . m) + (- (((abs s)) . n)) is ext-real V33() real set
abs ((((abs s)) . m) - (((abs s)) . n)) is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . k is ext-real V33() real Element of REAL
abs (s . k) is ext-real V33() real Element of REAL
(abs s) . k is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . (n + k) is ext-real V33() real Element of REAL
((s) . (n + k)) - ((s) . n) is ext-real V33() real Element of REAL
((s) . (n + k)) + (- ((s) . n)) is ext-real V33() real set
abs (((s) . (n + k)) - ((s) . n)) is ext-real V33() real Element of REAL
((abs s)) . (n + k) is ext-real V33() real Element of REAL
(((abs s)) . (n + k)) - (((abs s)) . n) is ext-real V33() real Element of REAL
(((abs s)) . (n + k)) + (- (((abs s)) . n)) is ext-real V33() real set
abs ((((abs s)) . (n + k)) - (((abs s)) . n)) is ext-real V33() real Element of REAL
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + (k + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . (n + (k + 1)) is ext-real V33() real Element of REAL
((s) . (n + (k + 1))) - ((s) . n) is ext-real V33() real Element of REAL
((s) . (n + (k + 1))) + (- ((s) . n)) is ext-real V33() real set
abs (((s) . (n + (k + 1))) - ((s) . n)) is ext-real V33() real Element of REAL
((abs s)) . (n + (k + 1)) is ext-real V33() real Element of REAL
(((abs s)) . (n + (k + 1))) - (((abs s)) . n) is ext-real V33() real Element of REAL
(((abs s)) . (n + (k + 1))) + (- (((abs s)) . n)) is ext-real V33() real set
abs ((((abs s)) . (n + (k + 1))) - (((abs s)) . n)) is ext-real V33() real Element of REAL
(n + k) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . ((n + k) + 1) is ext-real V33() real Element of REAL
abs (s . ((n + k) + 1)) is ext-real V33() real Element of REAL
(abs (s . ((n + k) + 1))) + (abs (((s) . (n + k)) - ((s) . n))) is ext-real V33() real Element of REAL
(abs (s . ((n + k) + 1))) + (abs ((((abs s)) . (n + k)) - (((abs s)) . n))) is ext-real V33() real Element of REAL
(abs s) . ((n + k) + 1) is ext-real V33() real Element of REAL
(((abs s)) . (n + k)) + ((abs s) . ((n + k) + 1)) is ext-real V33() real Element of REAL
((((abs s)) . (n + k)) + ((abs s) . ((n + k) + 1))) - (((abs s)) . n) is ext-real V33() real Element of REAL
((((abs s)) . (n + k)) + ((abs s) . ((n + k) + 1))) + (- (((abs s)) . n)) is ext-real V33() real set
abs (((((abs s)) . (n + k)) + ((abs s) . ((n + k) + 1))) - (((abs s)) . n)) is ext-real V33() real Element of REAL
(abs (s . ((n + k) + 1))) + (((abs s)) . (n + k)) is ext-real V33() real Element of REAL
((abs (s . ((n + k) + 1))) + (((abs s)) . (n + k))) - (((abs s)) . n) is ext-real V33() real Element of REAL
((abs (s . ((n + k) + 1))) + (((abs s)) . (n + k))) + (- (((abs s)) . n)) is ext-real V33() real set
abs (((abs (s . ((n + k) + 1))) + (((abs s)) . (n + k))) - (((abs s)) . n)) is ext-real V33() real Element of REAL
(abs (s . ((n + k) + 1))) + ((((abs s)) . (n + k)) - (((abs s)) . n)) is ext-real V33() real Element of REAL
abs ((abs (s . ((n + k) + 1))) + ((((abs s)) . (n + k)) - (((abs s)) . n))) is ext-real V33() real Element of REAL
(s . ((n + k) + 1)) + ((s) . (n + k)) is ext-real V33() real Element of REAL
((s . ((n + k) + 1)) + ((s) . (n + k))) - ((s) . n) is ext-real V33() real Element of REAL
((s . ((n + k) + 1)) + ((s) . (n + k))) + (- ((s) . n)) is ext-real V33() real set
abs (((s . ((n + k) + 1)) + ((s) . (n + k))) - ((s) . n)) is ext-real V33() real Element of REAL
(s . ((n + k) + 1)) + (((s) . (n + k)) - ((s) . n)) is ext-real V33() real Element of REAL
abs ((s . ((n + k) + 1)) + (((s) . (n + k)) - ((s) . n))) is ext-real V33() real Element of REAL
k is ext-real V33() real integer set
n is ext-real V33() real integer set
k - n is ext-real V33() real integer set
- n is ext-real V33() real integer set
k + (- n) is ext-real V33() real integer set
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) . (n + 0) is ext-real V33() real Element of REAL
((s) . (n + 0)) - ((s) . n) is ext-real V33() real Element of REAL
((s) . (n + 0)) + (- ((s) . n)) is ext-real V33() real set
abs (((s) . (n + 0)) - ((s) . n)) is ext-real V33() real Element of REAL
((abs s)) . (n + 0) is ext-real V33() real Element of REAL
(((abs s)) . (n + 0)) - (((abs s)) . n) is ext-real V33() real Element of REAL
(((abs s)) . (n + 0)) + (- (((abs s)) . n)) is ext-real V33() real set
abs ((((abs s)) . (n + 0)) - (((abs s)) . n)) is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real V33() real set
((abs s)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((abs s)) . m is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) . k is ext-real V33() real Element of REAL
(s) . n is ext-real V33() real Element of REAL
((s) . k) - ((s) . n) is ext-real V33() real Element of REAL
- ((s) . n) is ext-real V33() real set
((s) . k) + (- ((s) . n)) is ext-real V33() real set
abs (((s) . k) - ((s) . n)) is ext-real V33() real Element of REAL
((abs s)) . k is ext-real V33() real Element of REAL
((abs s)) . n is ext-real V33() real Element of REAL
(((abs s)) . k) - (((abs s)) . n) is ext-real V33() real Element of REAL
- (((abs s)) . n) is ext-real V33() real set
(((abs s)) . k) + (- (((abs s)) . n)) is ext-real V33() real set
abs ((((abs s)) . k) - (((abs s)) . n)) is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . n is ext-real V33() real Element of REAL
abs (s . n) is ext-real V33() real Element of REAL
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((abs s)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(abs s) . m is ext-real V33() real Element of REAL
s . m is ext-real V33() real Element of REAL
abs (s . m) is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(abs s) . (m + 1) is ext-real V33() real Element of REAL
((abs s) . (m + 1)) / ((abs s) . m) is ext-real V33() real Element of REAL
((abs s) . m) " is ext-real V33() real set
((abs s) . (m + 1)) * (((abs s) . m) ") is ext-real V33() real set
s is ext-real V33() real set
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m + n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n . k is ext-real V33() real Element of REAL
(n . k) - 0 is ext-real V33() real Element of REAL
- 0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real integer complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered add-closed set
(n . k) + (- 0) is ext-real V33() real set
abs ((n . k) - 0) is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . n is ext-real V33() real Element of REAL
abs (s . n) is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . (n + m) is ext-real V33() real Element of REAL
abs (s . (n + m)) is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + (m + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . (n + (m + 1)) is ext-real V33() real Element of REAL
abs (s . (n + (m + 1))) is ext-real V33() real Element of REAL
(n + m) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(abs s) . ((n + m) + 1) is ext-real V33() real Element of REAL
(abs s) . (n + m) is ext-real V33() real Element of REAL
((abs s) . ((n + m) + 1)) / ((abs s) . (n + m)) is ext-real V33() real Element of REAL
((abs s) . (n + m)) " is ext-real V33() real set
((abs s) . ((n + m) + 1)) * (((abs s) . (n + m)) ") is ext-real V33() real set
s . ((n + m) + 1) is ext-real V33() real Element of REAL
abs (s . ((n + m) + 1)) is ext-real V33() real Element of REAL
(abs (s . ((n + m) + 1))) / ((abs s) . (n + m)) is ext-real V33() real Element of REAL
(abs (s . ((n + m) + 1))) * (((abs s) . (n + m)) ") is ext-real V33() real set
(abs (s . ((n + m) + 1))) / (abs (s . (n + m))) is ext-real V33() real Element of REAL
(abs (s . (n + m))) " is ext-real V33() real set
(abs (s . ((n + m) + 1))) * ((abs (s . (n + m))) ") is ext-real V33() real set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
n + n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . (n + 0) is ext-real V33() real Element of REAL
abs (s . (n + 0)) is ext-real V33() real Element of REAL
s . m is ext-real V33() real Element of REAL
abs (s . m) is ext-real V33() real Element of REAL
lim s is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is ext-real V33() real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(abs n) . m is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
abs (n . m) is ext-real V33() real Element of REAL
s . m is ext-real V33() real Element of REAL
m -root ((abs n) . m) is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . n is ext-real V33() real Element of REAL
(abs n) . n is ext-real V33() real Element of REAL
n -root ((abs n) . n) is ext-real V33() real Element of REAL
n . n is ext-real V33() real Element of REAL
abs (n . n) is ext-real V33() real Element of REAL
n -root (abs (n . n)) is ext-real V33() real Element of REAL
(n -root (abs (n . n))) |^ n is ext-real V33() real Element of REAL
lim n is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s is ext-real V33() real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs n is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(lim s) - 1 is ext-real V33() real Element of REAL
- 1 is non empty ext-real non positive negative V33() real integer set
(lim s) + (- 1) is ext-real V33() real set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer V61() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
s . n is ext-real V33() real Element of REAL
(abs n) . n is ext-real V33() real Element of REAL
n -root ((abs n) . n) is ext-real V33() real Element of REAL
n . n is ext-real V33() real Element of REAL
abs (n . n) is ext-real V33() real Element of REAL
n -root (abs (n . n)) is ext-real V33() real Element of REAL
(n -root (abs (n . n))) - (lim s) is ext-real V33() real Element of REAL
- (lim s) is ext-real V33() real set
(n -root (abs (n . n))) + (- (lim s)) is ext-real V33() real set
abs ((n -root (abs (n . n))) - (lim s)) is ext-real V33() real Element of REAL
- ((lim s) - 1) is ext-real V33() real Element of REAL
((n -root (abs (n . n))) - (lim s)) + (lim s) is ext-real V33() real Element of REAL
1 - (lim s) is ext-real V33() real Element of REAL
1 + (- (lim s)) is ext-real V33() real set
(1 - (lim s)) + (lim s) is ext-real V33() real Element of REAL
(n -root (abs (n . n))) |^ n is ext-real V33() real Element of REAL
lim n is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(s) . n is ext-real V33() real Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(s,n) is ext-real V33() real Element of REAL
(s) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s) . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real integer set
(s,m) is ext-real V33() real Element of REAL
(s) . m is ext-real V33() real Element of REAL
(s,n) - (s,m) is ext-real V33() real Element of REAL
- (s,m) is ext-real V33() real set
(s,n) + (- (s,m)) is ext-real V33() real set