:: IRRAT_1 semantic presentation

REAL is non empty V48() V49() V50() V54() V55() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non empty V48() V54() V55() set
RAT is non empty V48() V49() V50() V51() V54() V55() set
INT is non empty V48() V49() V50() V51() V52() V54() V55() set
omega is non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() set
K6(omega) is set
K6(NAT) is set
K7(REAL,REAL) is V35() V36() V37() set
K6(K7(REAL,REAL)) is set
K7(NAT,REAL) is V35() V36() V37() set
K6(K7(NAT,REAL)) is set
K7(NAT,COMPLEX) is V35() set
K6(K7(NAT,COMPLEX)) is set
K7(COMPLEX,COMPLEX) is V35() set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V35() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(K7(REAL,REAL),REAL) is V35() V36() V37() set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is V20( RAT ) V35() V36() V37() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V20( RAT ) V35() V36() V37() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V20( RAT ) V20( INT ) V35() V36() V37() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V20( RAT ) V20( INT ) V35() V36() V37() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V20( RAT ) V20( INT ) V35() V36() V37() V38() set
K7(K7(NAT,NAT),NAT) is V20( RAT ) V20( INT ) V35() V36() V37() V38() set
K6(K7(K7(NAT,NAT),NAT)) is set
K434() is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer rational V48() V49() V50() V51() V52() V53() V54() FinSequence-membered Element of NAT
number_e is V11() real ext-real set
0 ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of REAL
0 -tuples_on REAL is FinSequenceSet of REAL
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer V48() V49() V50() V51() V52() V53() V54() FinSequence-membered set
exp_R is non empty V16() V19( REAL ) V20( REAL ) Function-like total V30( REAL , REAL ) V35() V36() V37() Element of K6(K7(REAL,REAL))
sqrt 2 is V11() real ext-real Element of REAL
len {} is V64() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
sqrt n is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne is V11() real ext-real integer set
ne / x is V11() real ext-real Element of COMPLEX
x " is V11() real ext-real non negative set
ne * (x ") is V11() real ext-real set
(sqrt n) * x is V11() real ext-real set
ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne1 ^2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne1 * ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
(sqrt n) ^2 is V11() real ext-real Element of REAL
(sqrt n) * (sqrt n) is V11() real ext-real set
x ^2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
x * x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
((sqrt n) ^2) * (x ^2) is V11() real ext-real set
n * (x ^2) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
n * i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
i ^2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
i * i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
n * (i ^2) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n * (n * (i ^2)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n * (n * (i ^2))) / n is V11() real ext-real non negative Element of COMPLEX
n " is V11() real ext-real non negative set
(n * (n * (i ^2))) * (n ") is V11() real ext-real non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
n * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
i / n is V11() real ext-real non negative Element of COMPLEX
n " is V11() real ext-real non negative set
i * (n ") is V11() real ext-real non negative set
1 * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(sqrt 2) to_power (sqrt 2) is V11() real ext-real set
((sqrt 2) to_power (sqrt 2)) to_power (sqrt 2) is V11() real ext-real set
(sqrt 2) ^2 is V11() real ext-real Element of REAL
(sqrt 2) * (sqrt 2) is V11() real ext-real set
(sqrt 2) to_power ((sqrt 2) ^2) is V11() real ext-real set
(sqrt 2) to_power 2 is V11() real ext-real set
(sqrt 2) |^ 2 is V11() real ext-real set
n is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
ne is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n . x is V11() real ext-real Element of REAL
F₁(x) is V11() real ext-real set
ne . x is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
- n is V11() real ext-real non positive integer set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n) . ne is V11() real ext-real Element of REAL
(ne) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(ne) . n is V11() real ext-real Element of REAL
n choose ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
- ne is V11() real ext-real non positive integer set
n to_power (- ne) is V11() real ext-real set
(n choose ne) * (n to_power (- ne)) is V11() real ext-real set
() is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
() is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
- (ne + 1) is V11() real ext-real non positive integer set
n to_power (- (ne + 1)) is V11() real ext-real set
- ne is V11() real ext-real non positive integer set
n to_power (- ne) is V11() real ext-real set
(n to_power (- ne)) / n is V11() real ext-real Element of COMPLEX
n " is V11() real ext-real non negative set
(n to_power (- ne)) * (n ") is V11() real ext-real set
(- ne) - 1 is non empty V11() real ext-real non positive negative integer set
- 1 is V11() real ext-real non positive integer set
(- ne) + (- 1) is V11() real ext-real non positive integer set
n to_power ((- ne) - 1) is V11() real ext-real set
n to_power 1 is V11() real ext-real set
n |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
(n to_power (- ne)) / (n to_power 1) is V11() real ext-real Element of COMPLEX
(n to_power 1) " is V11() real ext-real set
(n to_power (- ne)) * ((n to_power 1) ") is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n choose (ne + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n - ne is V11() real ext-real integer set
- ne is V11() real ext-real non positive integer set
n + (- ne) is V11() real ext-real integer set
(n - ne) / (ne + 1) is V11() real ext-real Element of COMPLEX
(ne + 1) " is non empty V11() real ext-real positive non negative set
(n - ne) * ((ne + 1) ") is V11() real ext-real set
n choose ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((n - ne) / (ne + 1)) * (n choose ne) is V11() real ext-real set
n - (ne + 1) is V11() real ext-real integer set
- (ne + 1) is V11() real ext-real non positive integer set
n + (- (ne + 1)) is V11() real ext-real integer set
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(ne + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
x ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((ne + 1) !) * (x !) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n !) / (((ne + 1) !) * (x !)) is V11() real ext-real non negative Element of COMPLEX
(((ne + 1) !) * (x !)) " is V11() real ext-real non negative set
(n !) * ((((ne + 1) !) * (x !)) ") is V11() real ext-real non negative set
ne ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(ne !) * (ne + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((ne !) * (ne + 1)) * (x !) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n !) / (((ne !) * (ne + 1)) * (x !)) is V11() real ext-real non negative Element of COMPLEX
(((ne !) * (ne + 1)) * (x !)) " is V11() real ext-real non negative set
(n !) * ((((ne !) * (ne + 1)) * (x !)) ") is V11() real ext-real non negative set
(x !) * (x + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((x !) * (x + 1)) / (x + 1) is V11() real ext-real non negative Element of COMPLEX
(x + 1) " is non empty V11() real ext-real positive non negative set
((x !) * (x + 1)) * ((x + 1) ") is V11() real ext-real non negative set
((ne !) * (ne + 1)) * (((x !) * (x + 1)) / (x + 1)) is V11() real ext-real non negative set
(n !) / (((ne !) * (ne + 1)) * (((x !) * (x + 1)) / (x + 1))) is V11() real ext-real non negative Element of COMPLEX
(((ne !) * (ne + 1)) * (((x !) * (x + 1)) / (x + 1))) " is V11() real ext-real non negative set
(n !) * ((((ne !) * (ne + 1)) * (((x !) * (x + 1)) / (x + 1))) ") is V11() real ext-real non negative set
(x + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((x + 1) !) / (x + 1) is V11() real ext-real non negative Element of COMPLEX
((x + 1) !) * ((x + 1) ") is V11() real ext-real non negative set
((ne !) * (ne + 1)) * (((x + 1) !) / (x + 1)) is V11() real ext-real non negative set
(n !) / (((ne !) * (ne + 1)) * (((x + 1) !) / (x + 1))) is V11() real ext-real non negative Element of COMPLEX
(((ne !) * (ne + 1)) * (((x + 1) !) / (x + 1))) " is V11() real ext-real non negative set
(n !) * ((((ne !) * (ne + 1)) * (((x + 1) !) / (x + 1))) ") is V11() real ext-real non negative set
ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne1 / (ne + 1) is V11() real ext-real non negative Element of COMPLEX
ne1 * ((ne + 1) ") is V11() real ext-real non negative set
ne1 ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(ne !) * (ne1 !) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n !) / ((ne !) * (ne1 !)) is V11() real ext-real non negative Element of COMPLEX
((ne !) * (ne1 !)) " is V11() real ext-real non negative set
(n !) * (((ne !) * (ne1 !)) ") is V11() real ext-real non negative set
(ne1 / (ne + 1)) * ((n !) / ((ne !) * (ne1 !))) is V11() real ext-real non negative Element of COMPLEX
((n - ne) / (ne + 1)) * 0 is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((ne + 1)) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
((ne + 1)) . n is V11() real ext-real Element of REAL
1 / (ne + 1) is V11() real ext-real non negative Element of COMPLEX
(ne + 1) " is non empty V11() real ext-real positive non negative set
1 * ((ne + 1) ") is V11() real ext-real non negative set
(ne) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(ne) . n is V11() real ext-real Element of REAL
(1 / (ne + 1)) * ((ne) . n) is V11() real ext-real set
(ne) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(ne) . n is V11() real ext-real Element of REAL
((1 / (ne + 1)) * ((ne) . n)) * ((ne) . n) is V11() real ext-real set
n choose (ne + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
- (ne + 1) is V11() real ext-real non positive integer set
n to_power (- (ne + 1)) is V11() real ext-real set
(n choose (ne + 1)) * (n to_power (- (ne + 1))) is V11() real ext-real set
n - ne is V11() real ext-real integer set
- ne is V11() real ext-real non positive integer set
n + (- ne) is V11() real ext-real integer set
(n - ne) / (ne + 1) is V11() real ext-real Element of COMPLEX
(n - ne) * ((ne + 1) ") is V11() real ext-real set
n choose ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((n - ne) / (ne + 1)) * (n choose ne) is V11() real ext-real set
(((n - ne) / (ne + 1)) * (n choose ne)) * (n to_power (- (ne + 1))) is V11() real ext-real set
n to_power (- ne) is V11() real ext-real set
(n to_power (- ne)) / n is V11() real ext-real Element of COMPLEX
n " is V11() real ext-real non negative set
(n to_power (- ne)) * (n ") is V11() real ext-real set
(((n - ne) / (ne + 1)) * (n choose ne)) * ((n to_power (- ne)) / n) is V11() real ext-real set
((n - ne) * ((ne + 1) ")) * (n choose ne) is V11() real ext-real set
(((n - ne) * ((ne + 1) ")) * (n choose ne)) * ((n to_power (- ne)) / n) is V11() real ext-real set
(((n - ne) * ((ne + 1) ")) * (n choose ne)) * ((n to_power (- ne)) * (n ")) is V11() real ext-real set
(n choose ne) * (n to_power (- ne)) is V11() real ext-real set
((ne + 1) ") * ((n choose ne) * (n to_power (- ne))) is V11() real ext-real set
(n - ne) * (n ") is V11() real ext-real set
(((ne + 1) ") * ((n choose ne) * (n to_power (- ne)))) * ((n - ne) * (n ")) is V11() real ext-real set
(1 / (ne + 1)) * ((n choose ne) * (n to_power (- ne))) is V11() real ext-real set
((1 / (ne + 1)) * ((n choose ne) * (n to_power (- ne)))) * ((n - ne) * (n ")) is V11() real ext-real set
(n - ne) / n is V11() real ext-real Element of COMPLEX
((1 / (ne + 1)) * ((n choose ne) * (n to_power (- ne)))) * ((n - ne) / n) is V11() real ext-real set
((1 / (ne + 1)) * ((ne) . n)) * ((n - ne) / n) is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(ne) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(ne) . n is V11() real ext-real Element of REAL
ne / n is V11() real ext-real non negative Element of COMPLEX
n " is V11() real ext-real non negative set
ne * (n ") is V11() real ext-real non negative set
1 - (ne / n) is V11() real ext-real set
- (ne / n) is V11() real ext-real non positive set
1 + (- (ne / n)) is V11() real ext-real set
n - ne is V11() real ext-real integer set
- ne is V11() real ext-real non positive integer set
n + (- ne) is V11() real ext-real integer set
(n - ne) / n is V11() real ext-real Element of COMPLEX
(n - ne) * (n ") is V11() real ext-real set
n / n is V11() real ext-real non negative Element of COMPLEX
n * (n ") is V11() real ext-real non negative set
(n / n) - (ne / n) is V11() real ext-real Element of COMPLEX
(n / n) + (- (ne / n)) is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
lim (n) is V11() real ext-real Element of REAL
ne is V11() real ext-real set
n / ne is V11() real ext-real Element of COMPLEX
ne " is V11() real ext-real set
n * (ne ") is V11() real ext-real set
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n) . ne1 is V11() real ext-real Element of REAL
((n) . ne1) - 1 is V11() real ext-real set
- 1 is V11() real ext-real non positive integer set
((n) . ne1) + (- 1) is V11() real ext-real set
abs (((n) . ne1) - 1) is V11() real ext-real Element of REAL
ne1 * ne is V11() real ext-real set
(n / ne) * ne is V11() real ext-real set
n / ne1 is V11() real ext-real non negative Element of COMPLEX
ne1 " is V11() real ext-real non negative set
n * (ne1 ") is V11() real ext-real non negative set
1 - (n / ne1) is V11() real ext-real set
- (n / ne1) is V11() real ext-real non positive set
1 + (- (n / ne1)) is V11() real ext-real set
(1 - (n / ne1)) - 1 is V11() real ext-real set
(1 - (n / ne1)) + (- 1) is V11() real ext-real set
abs ((1 - (n / ne1)) - 1) is V11() real ext-real Element of REAL
- (n / ne1) is V11() real ext-real non positive Element of COMPLEX
abs (- (n / ne1)) is V11() real ext-real Element of REAL
abs (n / ne1) is V11() real ext-real Element of REAL
ne is V11() real ext-real set
n is V11() real ext-real set
ne is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
lim ne is V11() real ext-real Element of REAL
ne . 0 is V11() real ext-real Element of REAL
(0) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(0) . n is V11() real ext-real Element of REAL
n choose 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer V48() V49() V50() V51() V52() V53() V54() FinSequence-membered set
n to_power (- 0) is V11() real ext-real set
n |^ (- 0) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
(n choose 0) * (n to_power (- 0)) is V11() real ext-real set
1 * (n to_power (- 0)) is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / (n + 1) is V11() real ext-real non negative Element of COMPLEX
(n + 1) " is non empty V11() real ext-real positive non negative set
1 * ((n + 1) ") is V11() real ext-real non negative set
n ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / (n !) is V11() real ext-real non negative Element of COMPLEX
(n !) " is non empty V11() real ext-real positive non negative set
1 * ((n !) ") is V11() real ext-real non negative set
(1 / (n + 1)) * (1 / (n !)) is V11() real ext-real non negative Element of COMPLEX
(n + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / ((n + 1) !) is V11() real ext-real non negative Element of COMPLEX
((n + 1) !) " is non empty V11() real ext-real positive non negative set
1 * (((n + 1) !) ") is V11() real ext-real non negative set
(n + 1) * (n !) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / ((n + 1) * (n !)) is V11() real ext-real non negative Element of COMPLEX
((n + 1) * (n !)) " is V11() real ext-real non negative set
1 * (((n + 1) * (n !)) ") is V11() real ext-real non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
lim (n) is V11() real ext-real Element of REAL
n ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / (n !) is V11() real ext-real non negative Element of COMPLEX
(n !) " is non empty V11() real ext-real positive non negative set
1 * ((n !) ") is V11() real ext-real non negative set
() . n is V11() real ext-real Element of REAL
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(ne) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
lim (ne) is V11() real ext-real Element of REAL
ne ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / (ne !) is V11() real ext-real non negative Element of COMPLEX
(ne !) " is non empty V11() real ext-real positive non negative set
1 * ((ne !) ") is V11() real ext-real non negative set
ne + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((ne + 1)) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
lim ((ne + 1)) is V11() real ext-real Element of REAL
(ne + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / ((ne + 1) !) is V11() real ext-real non negative Element of COMPLEX
((ne + 1) !) " is non empty V11() real ext-real positive non negative set
1 * (((ne + 1) !) ") is V11() real ext-real non negative set
1 / (ne + 1) is V11() real ext-real non negative Element of COMPLEX
(ne + 1) " is non empty V11() real ext-real positive non negative set
1 * ((ne + 1) ") is V11() real ext-real non negative set
x is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(ne) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
ne1 is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((ne + 1)) . i is V11() real ext-real Element of REAL
ne1 . i is V11() real ext-real Element of REAL
(ne) . i is V11() real ext-real Element of REAL
(1 / (ne + 1)) * ((ne) . i) is V11() real ext-real set
(ne) . i is V11() real ext-real Element of REAL
((1 / (ne + 1)) * ((ne) . i)) * ((ne) . i) is V11() real ext-real set
x . i is V11() real ext-real Element of REAL
(x . i) * ((ne) . i) is V11() real ext-real set
(1 / (ne + 1)) (#) (ne) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
lim x is V11() real ext-real Element of REAL
(1 / (ne + 1)) * (1 / (ne !)) is V11() real ext-real non negative Element of COMPLEX
x (#) (ne) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
lim ne1 is V11() real ext-real Element of REAL
lim (ne) is V11() real ext-real Element of REAL
(lim x) * (lim (ne)) is V11() real ext-real set
lim (0) is V11() real ext-real Element of REAL
0 ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / (0 !) is V11() real ext-real non negative Element of COMPLEX
(0 !) " is non empty V11() real ext-real positive non negative set
1 * ((0 !) ") is V11() real ext-real non negative set
NAT --> 1 is non empty T-Sequence-like V16() V19( NAT ) V20( NAT ) V20( RAT ) V20( INT ) Function-like total V30( NAT , NAT ) V35() V36() V37() V38() Element of K6(K7(NAT,NAT))
K6(K7(NAT,NAT)) is set
ne is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
ne . x is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(0) . x is V11() real ext-real Element of REAL
ne . x is V11() real ext-real Element of REAL
lim ne is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n) . ne is V11() real ext-real Element of REAL
ne - n is V11() real ext-real integer set
- n is V11() real ext-real non positive integer set
ne + (- n) is V11() real ext-real integer set
(ne - n) / ne is V11() real ext-real Element of COMPLEX
ne " is V11() real ext-real non negative set
(ne - n) * (ne ") is V11() real ext-real set
n / ne is V11() real ext-real non negative Element of COMPLEX
n * (ne ") is V11() real ext-real non negative set
1 - (n / ne) is V11() real ext-real set
- (n / ne) is V11() real ext-real non positive set
1 + (- (n / ne)) is V11() real ext-real set
1 - 0 is non empty V11() real ext-real positive non negative integer set
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer V48() V49() V50() V51() V52() V53() V54() FinSequence-membered set
1 + (- 0) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(ne) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(ne) . n is V11() real ext-real Element of REAL
ne ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / (ne !) is V11() real ext-real non negative Element of COMPLEX
(ne !) " is non empty V11() real ext-real positive non negative set
1 * ((ne !) ") is V11() real ext-real non negative set
() . ne is V11() real ext-real Element of REAL
(n) . ne is V11() real ext-real Element of REAL
- ne is V11() real ext-real non positive integer set
n to_power (- ne) is V11() real ext-real set
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(x) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(x) . n is V11() real ext-real Element of REAL
x ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / (x !) is V11() real ext-real non negative Element of COMPLEX
(x !) " is non empty V11() real ext-real positive non negative set
1 * ((x !) ") is V11() real ext-real non negative set
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((x + 1)) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
((x + 1)) . n is V11() real ext-real Element of REAL
(x + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / ((x + 1) !) is V11() real ext-real non negative Element of COMPLEX
((x + 1) !) " is non empty V11() real ext-real positive non negative set
1 * (((x + 1) !) ") is V11() real ext-real non negative set
1 / (x + 1) is V11() real ext-real non negative Element of COMPLEX
(x + 1) " is non empty V11() real ext-real positive non negative set
1 * ((x + 1) ") is V11() real ext-real non negative set
(1 / (x + 1)) * ((x) . n) is V11() real ext-real set
(1 / (x + 1)) * (1 / (x !)) is V11() real ext-real non negative Element of COMPLEX
(x) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(x) . n is V11() real ext-real Element of REAL
((1 / (x + 1)) * ((x) . n)) * ((x) . n) is V11() real ext-real set
(1 / ((x + 1) !)) * ((x) . n) is V11() real ext-real set
n choose (x + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
- (x + 1) is V11() real ext-real non positive integer set
n to_power (- (x + 1)) is V11() real ext-real set
(n choose (x + 1)) * (n to_power (- (x + 1))) is V11() real ext-real set
0 * (n to_power (- (x + 1))) is V11() real ext-real set
n choose ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n choose ne) * (n to_power (- ne)) is V11() real ext-real set
(0) . n is V11() real ext-real Element of REAL
0 ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / (0 !) is V11() real ext-real non negative Element of COMPLEX
(0 !) " is non empty V11() real ext-real positive non negative set
1 * ((0 !) ") is V11() real ext-real non negative set
n is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
n ^\ 1 is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() M7( REAL ,n)
Sum n is V11() real ext-real Element of REAL
n . 0 is V11() real ext-real Element of REAL
Sum (n ^\ 1) is V11() real ext-real Element of REAL
(n . 0) + (Sum (n ^\ 1)) is V11() real ext-real set
Partial_Sums n is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(Partial_Sums n) . 0 is V11() real ext-real Element of REAL
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n ^\ (1 + 0) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() M7( REAL ,n)
Sum (n ^\ (1 + 0)) is V11() real ext-real Element of REAL
((Partial_Sums n) . 0) + (Sum (n ^\ (1 + 0))) is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne is non empty set
x is V16() V19( NAT ) V20(ne) Function-like V55() FinSequence-like FinSubsequence-like FinSequence of ne
len x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
x /^ 1 is V16() V19( NAT ) V20(ne) Function-like V55() FinSequence-like FinSubsequence-like FinSequence of ne
(x /^ 1) . n is set
x . (n + 1) is set
(len x) - 1 is V11() real ext-real integer set
- 1 is V11() real ext-real non positive integer set
(len x) + (- 1) is V11() real ext-real integer set
((len x) - 1) + 1 is V11() real ext-real integer set
len (x /^ 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
dom (x /^ 1) is V48() V49() V50() V51() V52() V53() Element of K6(NAT)
n is V16() V19( NAT ) V20( REAL ) Function-like V35() V36() V37() V55() FinSequence-like FinSubsequence-like FinSequence of REAL
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
Sum n is V11() real ext-real Element of REAL
n . 1 is V11() real ext-real Element of REAL
n /^ 1 is V16() V19( NAT ) V20( REAL ) Function-like V35() V36() V37() V55() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (n /^ 1) is V11() real ext-real Element of REAL
(n . 1) + (Sum (n /^ 1)) is V11() real ext-real set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
dom n is V48() V49() V50() V51() V52() V53() Element of K6(NAT)
n /. 1 is V11() real ext-real Element of REAL
<*(n /. 1)*> is non empty V16() V19( NAT ) V20( REAL ) Function-like V35() V36() V37() V55() V66(1) FinSequence-like FinSubsequence-like FinSequence of REAL
<*(n /. 1)*> ^ (n /^ 1) is non empty V16() V19( NAT ) V20( REAL ) Function-like V35() V36() V37() V55() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (<*(n /. 1)*> ^ (n /^ 1)) is V11() real ext-real Element of REAL
<*(n . 1)*> is non empty V16() V19( NAT ) V20( REAL ) Function-like V35() V36() V37() V55() V66(1) FinSequence-like FinSubsequence-like FinSequence of REAL
<*(n . 1)*> ^ (n /^ 1) is non empty V16() V19( NAT ) V20( REAL ) Function-like V35() V36() V37() V55() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (<*(n . 1)*> ^ (n /^ 1)) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
x is V16() V19( NAT ) V20( REAL ) Function-like V35() V36() V37() V55() FinSequence-like FinSubsequence-like FinSequence of REAL
len x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne ^\ 1 is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() M7( REAL ,ne)
(ne ^\ 1) . ne1 is V11() real ext-real Element of REAL
ne . (ne1 + 1) is V11() real ext-real Element of REAL
(ne1 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
x . ((ne1 + 1) + 1) is V11() real ext-real Element of REAL
x /^ 1 is V16() V19( NAT ) V20( REAL ) Function-like V35() V36() V37() V55() FinSequence-like FinSubsequence-like FinSequence of REAL
(x /^ 1) . (ne1 + 1) is V11() real ext-real Element of REAL
ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(ne ^\ 1) . ne1 is V11() real ext-real Element of REAL
ne . (ne1 + 1) is V11() real ext-real Element of REAL
len (x /^ 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(len x) - 1 is V11() real ext-real integer set
- 1 is V11() real ext-real non positive integer set
(len x) + (- 1) is V11() real ext-real integer set
Sum (ne ^\ 1) is V11() real ext-real Element of REAL
Sum (x /^ 1) is V11() real ext-real Element of REAL
Sum ne is V11() real ext-real Element of REAL
ne . 0 is V11() real ext-real Element of REAL
(ne . 0) + (Sum (ne ^\ 1)) is V11() real ext-real set
x . (0 + 1) is V11() real ext-real Element of REAL
(x . (0 + 1)) + (Sum (ne ^\ 1)) is V11() real ext-real set
Sum x is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
x is V16() V19( NAT ) V20( REAL ) Function-like V35() V36() V37() V55() FinSequence-like FinSubsequence-like FinSequence of REAL
len x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
Sum ne is V11() real ext-real Element of REAL
Sum x is V11() real ext-real Element of REAL
ne is V16() V19( NAT ) V20( REAL ) Function-like V35() V36() V37() V55() FinSequence-like FinSubsequence-like FinSequence of REAL
len ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
Sum ne is V11() real ext-real Element of REAL
Partial_Sums n is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(Partial_Sums n) . (x + 1) is V11() real ext-real Element of REAL
(Partial_Sums n) . x is V11() real ext-real Element of REAL
n . (x + 1) is V11() real ext-real Element of REAL
((Partial_Sums n) . x) + (n . (x + 1)) is V11() real ext-real set
n . 0 is V11() real ext-real Element of REAL
(Partial_Sums n) . 0 is V11() real ext-real Element of REAL
lim (Partial_Sums n) is V11() real ext-real Element of REAL
Sum n is V11() real ext-real Element of REAL
ne is V16() V19( NAT ) V20( REAL ) Function-like V35() V36() V37() V55() FinSequence-like FinSubsequence-like FinSequence of REAL
len ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
Sum n is V11() real ext-real Element of REAL
Sum ne is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne choose n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne - n is V11() real ext-real integer set
- n is V11() real ext-real non positive integer set
ne + (- n) is V11() real ext-real integer set
x is V11() real ext-real set
x to_power (ne - n) is V11() real ext-real set
(ne choose n) * (x to_power (ne - n)) is V11() real ext-real set
ne1 is V11() real ext-real set
(x,ne1) In_Power ne is V16() V19( NAT ) V20( REAL ) Function-like V35() V36() V37() V55() FinSequence-like FinSubsequence-like FinSequence of REAL
((x,ne1) In_Power ne) . (n + 1) is V11() real ext-real Element of REAL
ne1 to_power n is V11() real ext-real set
ne1 |^ n is V11() real ext-real set
((ne choose n) * (x to_power (ne - n))) * (ne1 to_power n) is V11() real ext-real set
(n + 1) - 1 is V11() real ext-real integer set
- 1 is V11() real ext-real non positive integer set
(n + 1) + (- 1) is V11() real ext-real integer set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
len ((x,ne1) In_Power ne) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne - i is V11() real ext-real integer set
- i is V11() real ext-real non positive integer set
ne + (- i) is V11() real ext-real integer set
dom ((x,ne1) In_Power ne) is V48() V49() V50() V51() V52() V53() Element of K6(NAT)
ne choose i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
x to_power n is V11() real ext-real set
x |^ n is V11() real ext-real set
(ne choose i) * (x to_power n) is V11() real ext-real set
ne1 |^ i is V11() real ext-real set
((ne choose i) * (x to_power n)) * (ne1 |^ i) is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
1 / n is V11() real ext-real non negative Element of COMPLEX
n " is V11() real ext-real non negative set
1 * (n ") is V11() real ext-real non negative set
(1,(1 / n)) In_Power n is V16() V19( NAT ) V20( REAL ) Function-like V35() V36() V37() V55() FinSequence-like FinSubsequence-like FinSequence of REAL
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n) . ne is V11() real ext-real Element of REAL
ne + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((1,(1 / n)) In_Power n) . (ne + 1) is V11() real ext-real Element of REAL
n choose ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n - ne is V11() real ext-real integer set
- ne is V11() real ext-real non positive integer set
n + (- ne) is V11() real ext-real integer set
1 to_power (n - ne) is V11() real ext-real set
(n choose ne) * (1 to_power (n - ne)) is V11() real ext-real set
(1 / n) to_power ne is V11() real ext-real set
(1 / n) |^ ne is V11() real ext-real set
((n choose ne) * (1 to_power (n - ne))) * ((1 / n) to_power ne) is V11() real ext-real set
(n choose ne) * 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((n choose ne) * 1) * ((1 / n) to_power ne) is V11() real ext-real set
n to_power (- ne) is V11() real ext-real set
(n choose ne) * (n to_power (- ne)) is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
Sum (n) is V11() real ext-real Element of REAL
1 / n is V11() real ext-real non negative Element of COMPLEX
n " is V11() real ext-real non negative set
1 * (n ") is V11() real ext-real non negative set
1 + (1 / n) is non empty V11() real ext-real positive non negative set
(1 + (1 / n)) to_power n is V11() real ext-real set
(1 + (1 / n)) |^ n is V11() real ext-real set
() . n is V11() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n) . ne is V11() real ext-real Element of REAL
n choose ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
- ne is V11() real ext-real non positive integer set
n to_power (- ne) is V11() real ext-real set
(n choose ne) * (n to_power (- ne)) is V11() real ext-real set
0 * (n to_power (- ne)) is V11() real ext-real set
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n) . ne is V11() real ext-real Element of REAL
(1,(1 / n)) In_Power n is V16() V19( NAT ) V20( REAL ) Function-like V35() V36() V37() V55() FinSequence-like FinSubsequence-like FinSequence of REAL
ne + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((1,(1 / n)) In_Power n) . (ne + 1) is V11() real ext-real Element of REAL
len ((1,(1 / n)) In_Power n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
Sum ((1,(1 / n)) In_Power n) is V11() real ext-real Element of REAL
lim () is V11() real ext-real Element of REAL
number_e is V11() real ext-real Element of REAL
() ^\ 1 is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() M7( REAL ,())
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(() ^\ 1) . n is V11() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
() . (n + 1) is V11() real ext-real Element of REAL
1 / (n + 1) is V11() real ext-real non negative Element of COMPLEX
(n + 1) " is non empty V11() real ext-real positive non negative set
1 * ((n + 1) ") is V11() real ext-real non negative set
1 + (1 / (n + 1)) is non empty V11() real ext-real positive non negative set
(1 + (1 / (n + 1))) to_power (n + 1) is V11() real ext-real set
(1 + (1 / (n + 1))) |^ (n + 1) is V11() real ext-real set
lim (() ^\ 1) is V11() real ext-real Element of REAL
Sum () is V11() real ext-real Element of REAL
exp_R 1 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
() . n is V11() real ext-real Element of REAL
n ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / (n !) is V11() real ext-real non negative Element of COMPLEX
(n !) " is non empty V11() real ext-real positive non negative set
1 * ((n !) ") is V11() real ext-real non negative set
1 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(1 |^ n) / (n !) is V11() real ext-real non negative Element of COMPLEX
(1 |^ n) * ((n !) ") is V11() real ext-real non negative set
1 rExpSeq is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(1 rExpSeq) . n is V11() real ext-real Element of REAL
exp_R . 1 is V11() real ext-real Element of REAL
Partial_Sums () is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(Partial_Sums ()) . n is V11() real ext-real Element of REAL
x is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
x . ne1 is V11() real ext-real Element of REAL
(ne1) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
Partial_Sums (ne1) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(Partial_Sums (ne1)) . (n + 1) is V11() real ext-real Element of REAL
(Partial_Sums (ne1)) . n is V11() real ext-real Element of REAL
(ne1) . (n + 1) is V11() real ext-real Element of REAL
((Partial_Sums (ne1)) . n) + ((ne1) . (n + 1)) is V11() real ext-real set
ne . ne1 is V11() real ext-real Element of REAL
(ne . ne1) + ((ne1) . (n + 1)) is V11() real ext-real set
((n + 1)) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
((n + 1)) . ne1 is V11() real ext-real Element of REAL
(ne . ne1) + (((n + 1)) . ne1) is V11() real ext-real set
ne + ((n + 1)) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(ne + ((n + 1))) . ne1 is V11() real ext-real Element of REAL
lim ne is V11() real ext-real Element of REAL
lim x is V11() real ext-real Element of REAL
lim ((n + 1)) is V11() real ext-real Element of REAL
(lim ne) + (lim ((n + 1))) is V11() real ext-real set
() . (n + 1) is V11() real ext-real Element of REAL
((Partial_Sums ()) . n) + (() . (n + 1)) is V11() real ext-real set
(Partial_Sums ()) . (n + 1) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(Partial_Sums ()) . n is V11() real ext-real Element of REAL
ne is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
lim ne is V11() real ext-real Element of REAL
(Partial_Sums ()) . (n + 1) is V11() real ext-real Element of REAL
n is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n . ne is V11() real ext-real Element of REAL
(ne) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
Partial_Sums (ne) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(Partial_Sums (ne)) . 0 is V11() real ext-real Element of REAL
(ne) . 0 is V11() real ext-real Element of REAL
(0) . ne is V11() real ext-real Element of REAL
lim n is V11() real ext-real Element of REAL
() . 0 is V11() real ext-real Element of REAL
(Partial_Sums ()) . 0 is V11() real ext-real Element of REAL
n is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
lim n is V11() real ext-real Element of REAL
n is V11() real ext-real set
ne is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
lim ne is V11() real ext-real Element of REAL
x is V11() real ext-real set
n - x is V11() real ext-real set
- x is V11() real ext-real set
n + (- x) is V11() real ext-real set
ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne . i is V11() real ext-real Element of REAL
(ne . i) - n is V11() real ext-real set
- n is V11() real ext-real set
(ne . i) + (- n) is V11() real ext-real set
abs ((ne . i) - n) is V11() real ext-real Element of REAL
((ne . i) - n) + n is V11() real ext-real set
(- x) + n is V11() real ext-real set
n is V11() real ext-real set
ne is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
lim ne is V11() real ext-real Element of REAL
x is V11() real ext-real set
n + x is V11() real ext-real set
n + 0 is V11() real ext-real set
ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n - x is V11() real ext-real set
- x is V11() real ext-real set
n + (- x) is V11() real ext-real set
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
max (i,ne1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne . n is V11() real ext-real Element of REAL
(ne . n) - n is V11() real ext-real set
- n is V11() real ext-real set
(ne . n) + (- n) is V11() real ext-real set
abs ((ne . n) - n) is V11() real ext-real Element of REAL
(n - x) - n is V11() real ext-real set
(n - x) + (- n) is V11() real ext-real set
n is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
Partial_Sums n is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
Sum n is V11() real ext-real Element of REAL
ne is V11() real ext-real set
(Sum n) - ne is V11() real ext-real set
- ne is V11() real ext-real set
(Sum n) + (- ne) is V11() real ext-real set
lim (Partial_Sums n) is V11() real ext-real Element of REAL
(lim (Partial_Sums n)) - ne is V11() real ext-real set
(lim (Partial_Sums n)) + (- ne) is V11() real ext-real set
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(Partial_Sums n) . x is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
() . n is V11() real ext-real Element of REAL
(n) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n) . ne is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n) . x is V11() real ext-real Element of REAL
() . x is V11() real ext-real Element of REAL
Sum (n) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
Partial_Sums ne is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(Partial_Sums ne) . n is V11() real ext-real Element of REAL
Sum ne is V11() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne ^\ (n + 1) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() M7( REAL ,ne)
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(ne ^\ (n + 1)) . x is V11() real ext-real Element of REAL
(n + 1) + x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne . ((n + 1) + x) is V11() real ext-real Element of REAL
Sum (ne ^\ (n + 1)) is V11() real ext-real Element of REAL
((Partial_Sums ne) . n) + 0 is V11() real ext-real set
((Partial_Sums ne) . n) + (Sum (ne ^\ (n + 1))) is V11() real ext-real set
n is V11() real ext-real set
(Sum ()) - n is V11() real ext-real set
- n is V11() real ext-real set
(Sum ()) + (- n) is V11() real ext-real set
n / 2 is V11() real ext-real Element of COMPLEX
2 " is non empty V11() real ext-real positive non negative set
n * (2 ") is V11() real ext-real set
(Sum ()) - (n / 2) is V11() real ext-real set
- (n / 2) is V11() real ext-real set
(Sum ()) + (- (n / 2)) is V11() real ext-real set
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(Partial_Sums ()) . ne is V11() real ext-real Element of REAL
((Partial_Sums ()) . ne) - (n / 2) is V11() real ext-real set
((Partial_Sums ()) . ne) + (- (n / 2)) is V11() real ext-real set
((Sum ()) - (n / 2)) - (n / 2) is V11() real ext-real set
((Sum ()) - (n / 2)) + (- (n / 2)) is V11() real ext-real set
x is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
lim x is V11() real ext-real Element of REAL
ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
i is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
() . n is V11() real ext-real Element of REAL
(n) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n) . n is V11() real ext-real Element of REAL
Partial_Sums (n) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(Partial_Sums (n)) . ne is V11() real ext-real Element of REAL
Sum (n) is V11() real ext-real Element of REAL
x . n is V11() real ext-real Element of REAL
ne1 + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n is V11() real ext-real set
ne is V11() real ext-real set
n is V11() real ext-real set
ne is V11() real ext-real set
n is V11() real ext-real set
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne is V11() real ext-real integer set
ne / x is V11() real ext-real Element of COMPLEX
x " is V11() real ext-real non negative set
ne * (x ") is V11() real ext-real set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
i is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
i ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(i !) * n is V11() real ext-real set
ne1 is V11() real ext-real integer set
(i !) * ne1 is V11() real ext-real integer set
x ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(x !) * n is V11() real ext-real set
x - 1 is V11() real ext-real integer set
- 1 is V11() real ext-real non positive integer set
x + (- 1) is V11() real ext-real integer set
ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne1 ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(ne1 + 1) * (ne1 !) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((ne1 + 1) * (ne1 !)) * n is V11() real ext-real set
x * n is V11() real ext-real set
(x * n) * (ne1 !) is V11() real ext-real set
ne * (ne1 !) is V11() real ext-real integer set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
() . ne is V11() real ext-real Element of REAL
(n !) * (() . ne) is V11() real ext-real set
ne ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n !) / (ne !) is V11() real ext-real non negative Element of COMPLEX
(ne !) " is non empty V11() real ext-real positive non negative set
(n !) * ((ne !) ") is V11() real ext-real non negative set
1 / (ne !) is V11() real ext-real non negative Element of COMPLEX
1 * ((ne !) ") is V11() real ext-real non negative set
(n !) * (1 / (ne !)) is V11() real ext-real non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n !) / (ne !) is V11() real ext-real non negative Element of COMPLEX
(ne !) " is non empty V11() real ext-real positive non negative set
(n !) * ((ne !) ") is V11() real ext-real non negative set
n is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
Sum n is V11() real ext-real Element of REAL
Partial_Sums n is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(Partial_Sums n) . 0 is V11() real ext-real Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n ^\ (0 + 1) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() M7( REAL ,n)
Sum (n ^\ (0 + 1)) is V11() real ext-real Element of REAL
((Partial_Sums n) . 0) + (Sum (n ^\ (0 + 1))) is V11() real ext-real set
n . 0 is V11() real ext-real Element of REAL
n ^\ 1 is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() M7( REAL ,n)
Sum (n ^\ 1) is V11() real ext-real Element of REAL
(n . 0) + (Sum (n ^\ 1)) is V11() real ext-real set
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n ^\ 1) . ne is V11() real ext-real Element of REAL
1 + ne is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n . (1 + ne) is V11() real ext-real Element of REAL
0 + 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer rational V48() V49() V50() V51() V52() V53() V54() FinSequence-membered Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
() ^\ (n + 1) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() M7( REAL ,())
Sum (() ^\ (n + 1)) is V11() real ext-real Element of REAL
(n !) * (Sum (() ^\ (n + 1))) is V11() real ext-real set
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(() ^\ (n + 1)) . ne is V11() real ext-real Element of REAL
(n + 1) + ne is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
() . ((n + 1) + ne) is V11() real ext-real Element of REAL
((n + 1) + ne) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / (((n + 1) + ne) !) is V11() real ext-real non negative Element of COMPLEX
(((n + 1) + ne) !) " is non empty V11() real ext-real positive non negative set
1 * ((((n + 1) + ne) !) ") is V11() real ext-real non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(ne !) / (n !) is V11() real ext-real non negative Element of COMPLEX
(n !) " is non empty V11() real ext-real positive non negative set
(ne !) * ((n !) ") is V11() real ext-real non negative set
ne - n is V11() real ext-real integer set
- n is V11() real ext-real non positive integer set
ne + (- n) is V11() real ext-real integer set
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
x + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(ne1 + 1) + n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((ne1 + 1) + n) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(((ne1 + 1) + n) !) / (n !) is V11() real ext-real non negative Element of COMPLEX
(((ne1 + 1) + n) !) * ((n !) ") is V11() real ext-real non negative set
ne1 + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(ne1 + n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(ne1 + n) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((ne1 + n) + 1) * ((ne1 + n) !) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(((ne1 + n) + 1) * ((ne1 + n) !)) * ((n !) ") is V11() real ext-real non negative set
((ne1 + n) !) * ((n !) ") is V11() real ext-real non negative set
((ne1 + n) + 1) * (((ne1 + n) !) * ((n !) ")) is V11() real ext-real non negative set
((ne1 + n) !) / (n !) is V11() real ext-real non negative Element of COMPLEX
((ne1 + n) + 1) * (((ne1 + n) !) / (n !)) is V11() real ext-real non negative set
i is V11() real ext-real integer set
((ne1 + n) + 1) * i is V11() real ext-real integer set
ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne1 + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(ne1 + n) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((ne1 + n) !) / (n !) is V11() real ext-real non negative Element of COMPLEX
((ne1 + n) !) * ((n !) ") is V11() real ext-real non negative set
ne1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(ne1 + 1) + n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((ne1 + 1) + n) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(((ne1 + 1) + n) !) / (n !) is V11() real ext-real non negative Element of COMPLEX
(((ne1 + 1) + n) !) * ((n !) ") is V11() real ext-real non negative set
0 + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(0 + n) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((0 + n) !) / (n !) is V11() real ext-real non negative Element of COMPLEX
((0 + n) !) * ((n !) ") is V11() real ext-real non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(Partial_Sums ()) . n is V11() real ext-real Element of REAL
(n !) * ((Partial_Sums ()) . n) is V11() real ext-real set
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(Partial_Sums ()) . ne is V11() real ext-real Element of REAL
(n !) * ((Partial_Sums ()) . ne) is V11() real ext-real set
ne + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
() . (ne + 1) is V11() real ext-real Element of REAL
(n !) * (() . (ne + 1)) is V11() real ext-real set
(ne + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n !) / ((ne + 1) !) is V11() real ext-real non negative Element of COMPLEX
((ne + 1) !) " is non empty V11() real ext-real positive non negative set
(n !) * (((ne + 1) !) ") is V11() real ext-real non negative set
x is V11() real ext-real integer set
ne1 is V11() real ext-real integer set
x + ne1 is V11() real ext-real integer set
(Partial_Sums ()) . (ne + 1) is V11() real ext-real Element of REAL
(n !) * ((Partial_Sums ()) . (ne + 1)) is V11() real ext-real set
((Partial_Sums ()) . ne) + (() . (ne + 1)) is V11() real ext-real set
(n !) * (((Partial_Sums ()) . ne) + (() . (ne + 1))) is V11() real ext-real set
((n !) * ((Partial_Sums ()) . ne)) + ((n !) * (() . (ne + 1))) is V11() real ext-real set
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(Partial_Sums ()) . ne is V11() real ext-real Element of REAL
(n !) * ((Partial_Sums ()) . ne) is V11() real ext-real set
ne + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(Partial_Sums ()) . (ne + 1) is V11() real ext-real Element of REAL
(n !) * ((Partial_Sums ()) . (ne + 1)) is V11() real ext-real set
(Partial_Sums ()) . 0 is V11() real ext-real Element of REAL
(n !) * ((Partial_Sums ()) . 0) is V11() real ext-real set
() . 0 is V11() real ext-real Element of REAL
(n !) * (() . 0) is V11() real ext-real set
0 ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n !) / (0 !) is V11() real ext-real non negative Element of COMPLEX
(0 !) " is non empty V11() real ext-real positive non negative set
(n !) * ((0 !) ") is V11() real ext-real non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / (n + 1) is V11() real ext-real non negative Element of COMPLEX
(n + 1) " is non empty V11() real ext-real positive non negative set
1 * ((n + 1) ") is V11() real ext-real non negative set
n ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n + ne is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n + ne) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((n + ne) + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n !) / (((n + ne) + 1) !) is V11() real ext-real non negative Element of COMPLEX
(((n + ne) + 1) !) " is non empty V11() real ext-real positive non negative set
(n !) * ((((n + ne) + 1) !) ") is V11() real ext-real non negative set
ne + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
x is V11() real ext-real set
x to_power (ne + 1) is V11() real ext-real set
x |^ (ne + 1) is V11() real ext-real set
ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n + ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n + ne1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((n + ne1) + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n !) / (((n + ne1) + 1) !) is V11() real ext-real non negative Element of COMPLEX
(((n + ne1) + 1) !) " is non empty V11() real ext-real positive non negative set
(n !) * ((((n + ne1) + 1) !) ") is V11() real ext-real non negative set
ne1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
x to_power (ne1 + 1) is V11() real ext-real set
x |^ (ne1 + 1) is V11() real ext-real set
n + (ne1 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n + (ne1 + 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((n + (ne1 + 1)) + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n !) / (((n + (ne1 + 1)) + 1) !) is V11() real ext-real non negative Element of COMPLEX
(((n + (ne1 + 1)) + 1) !) " is non empty V11() real ext-real positive non negative set
(n !) * ((((n + (ne1 + 1)) + 1) !) ") is V11() real ext-real non negative set
((n + (ne1 + 1)) + 1) * (((n + ne1) + 1) !) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(((n + (ne1 + 1)) + 1) * (((n + ne1) + 1) !)) " is V11() real ext-real non negative set
(n !) * ((((n + (ne1 + 1)) + 1) * (((n + ne1) + 1) !)) ") is V11() real ext-real non negative set
((n + (ne1 + 1)) + 1) " is non empty V11() real ext-real positive non negative set
(((n + (ne1 + 1)) + 1) ") * ((((n + ne1) + 1) !) ") is V11() real ext-real non negative set
(n !) * ((((n + (ne1 + 1)) + 1) ") * ((((n + ne1) + 1) !) ")) is V11() real ext-real non negative set
((n !) * ((((n + ne1) + 1) !) ")) * (((n + (ne1 + 1)) + 1) ") is V11() real ext-real non negative set
((n !) / (((n + ne1) + 1) !)) * (((n + (ne1 + 1)) + 1) ") is V11() real ext-real non negative set
n + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(x to_power (ne1 + 1)) * x is V11() real ext-real set
x to_power 1 is V11() real ext-real set
x |^ 1 is V11() real ext-real set
(x to_power (ne1 + 1)) * (x to_power 1) is V11() real ext-real set
(ne1 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
x to_power ((ne1 + 1) + 1) is V11() real ext-real set
x |^ ((ne1 + 1) + 1) is V11() real ext-real set
(n + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n !) / ((n + 1) !) is V11() real ext-real non negative Element of COMPLEX
((n + 1) !) " is non empty V11() real ext-real positive non negative set
(n !) * (((n + 1) !) ") is V11() real ext-real non negative set
(n + 1) * (n !) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n !) / ((n + 1) * (n !)) is V11() real ext-real non negative Element of COMPLEX
((n + 1) * (n !)) " is V11() real ext-real non negative set
(n !) * (((n + 1) * (n !)) ") is V11() real ext-real non negative set
(n !) " is non empty V11() real ext-real positive non negative set
((n + 1) ") * ((n !) ") is V11() real ext-real non negative set
(n !) * (((n + 1) ") * ((n !) ")) is V11() real ext-real non negative set
(n !) * ((n !) ") is V11() real ext-real non negative set
((n !) * ((n !) ")) * ((n + 1) ") is V11() real ext-real non negative set
(n + 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((n + 0) + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n !) / (((n + 0) + 1) !) is V11() real ext-real non negative Element of COMPLEX
(((n + 0) + 1) !) " is non empty V11() real ext-real positive non negative set
(n !) * ((((n + 0) + 1) !) ") is V11() real ext-real non negative set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
x to_power (0 + 1) is V11() real ext-real set
x |^ (0 + 1) is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / (n + 1) is V11() real ext-real non negative Element of COMPLEX
(n + 1) " is non empty V11() real ext-real positive non negative set
1 * ((n + 1) ") is V11() real ext-real non negative set
n ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
() ^\ (n + 1) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() M7( REAL ,())
Sum (() ^\ (n + 1)) is V11() real ext-real Element of REAL
(n !) * (Sum (() ^\ (n + 1))) is V11() real ext-real set
ne is V11() real ext-real set
1 - ne is V11() real ext-real set
- ne is V11() real ext-real set
1 + (- ne) is V11() real ext-real set
ne / (1 - ne) is V11() real ext-real Element of COMPLEX
(1 - ne) " is V11() real ext-real set
ne * ((1 - ne) ") is V11() real ext-real set
x is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
(n !) (#) (() ^\ (n + 1)) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() Element of K6(K7(NAT,REAL))
ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((n !) (#) (() ^\ (n + 1))) . ne1 is V11() real ext-real Element of REAL
(() ^\ (n + 1)) . ne1 is V11() real ext-real Element of REAL
(n !) * ((() ^\ (n + 1)) . ne1) is V11() real ext-real set
(n + 1) + ne1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
() . ((n + 1) + ne1) is V11() real ext-real Element of REAL
(n !) * (() . ((n + 1) + ne1)) is V11() real ext-real set
n + ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n + ne1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
((n + ne1) + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / (((n + ne1) + 1) !) is V11() real ext-real non negative Element of COMPLEX
(((n + ne1) + 1) !) " is non empty V11() real ext-real positive non negative set
1 * ((((n + ne1) + 1) !) ") is V11() real ext-real non negative set
(n !) * (1 / (((n + ne1) + 1) !)) is V11() real ext-real non negative set
(n !) / (((n + ne1) + 1) !) is V11() real ext-real non negative Element of COMPLEX
(n !) * ((((n + ne1) + 1) !) ") is V11() real ext-real non negative set
x . ne1 is V11() real ext-real Element of REAL
ne1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne to_power (ne1 + 1) is V11() real ext-real set
ne |^ (ne1 + 1) is V11() real ext-real set
x . 0 is V11() real ext-real Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne to_power (0 + 1) is V11() real ext-real set
ne |^ (0 + 1) is V11() real ext-real set
ne1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
x . (ne1 + 1) is V11() real ext-real Element of REAL
(ne1 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
ne to_power ((ne1 + 1) + 1) is V11() real ext-real set
ne |^ ((ne1 + 1) + 1) is V11() real ext-real set
ne to_power 1 is V11() real ext-real set
ne |^ 1 is V11() real ext-real set
ne to_power (ne1 + 1) is V11() real ext-real set
ne |^ (ne1 + 1) is V11() real ext-real set
(ne to_power 1) * (ne to_power (ne1 + 1)) is V11() real ext-real set
ne * (ne to_power (ne1 + 1)) is V11() real ext-real set
x . ne1 is V11() real ext-real Element of REAL
ne * (x . ne1) is V11() real ext-real set
abs ne is V11() real ext-real Element of REAL
Sum ((n !) (#) (() ^\ (n + 1))) is V11() real ext-real Element of REAL
Sum x is V11() real ext-real Element of REAL
n is V11() real ext-real set
1 - n is V11() real ext-real set
- n is V11() real ext-real set
1 + (- n) is V11() real ext-real set
n / (1 - n) is V11() real ext-real Element of COMPLEX
(1 - n) " is V11() real ext-real set
n * ((1 - n) ") is V11() real ext-real set
ne is V11() real ext-real set
ne + 1 is V11() real ext-real set
1 / (ne + 1) is V11() real ext-real Element of COMPLEX
(ne + 1) " is V11() real ext-real set
1 * ((ne + 1) ") is V11() real ext-real set
2 / (ne + 1) is V11() real ext-real Element of COMPLEX
2 * ((ne + 1) ") is V11() real ext-real set
n + n is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
n ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
(n !) * number_e is V11() real ext-real set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT
1 / (n + 1) is V11() real ext-real non negative Element of COMPLEX
(n + 1) " is non empty V11() real ext-real positive non negative set
1 * ((n + 1) ") is V11() real ext-real non negative set
(Partial_Sums ()) . n is V11() real ext-real Element of REAL
(n !) * ((Partial_Sums ()) . n) is V11() real ext-real set
() ^\ (n + 1) is non empty V16() V19( NAT ) V20( REAL ) Function-like total V30( NAT , REAL ) V35() V36() V37() M7( REAL ,())
Sum (() ^\ (n + 1)) is V11() real ext-real Element of REAL
((Partial_Sums ()) . n) + (Sum (() ^\ (n + 1))) is V11() real ext-real set
(n !) * (((Partial_Sums ()) . n) + (Sum (() ^\ (n + 1)))) is V11() real ext-real set
(n !) * (Sum (() ^\ (n + 1))) is V11() real ext-real set
((n !) * ((Partial_Sums ()) . n)) + ((n !) * (Sum (() ^\ (n + 1)))) is V11() real ext-real set
ne is V11() real ext-real integer set
ne1 is V11() real ext-real integer set
ne - ne1 is V11() real ext-real integer set
- ne1 is V11() real ext-real integer set
ne + (- ne1) is V11() real ext-real integer set
1 - (1 / (n + 1)) is V11() real ext-real set
- (1 / (n + 1)) is V11() real ext-real non positive set
1 + (- (1 / (n + 1))) is V11() real ext-real set
(1 / (n + 1)) / (1 - (1 / (n + 1))) is V11() real ext-real Element of COMPLEX
(1 - (1 / (n + 1))) " is V11() real ext-real set
(1 / (n + 1)) * ((1 - (1 / (n + 1))) ") is V11() real ext-real set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer rational V48() V49() V50() V51() V52() V53() Element of NAT