REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V75() V193() V194() V196() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V75() V191() V193() Element of bool REAL
bool REAL is non trivial non finite set
INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V75() set
COMPLEX is non empty non trivial non finite complex-membered V75() set
[:NAT,REAL:] is non trivial Relation-like non finite V59() V60() V61() set
bool [:NAT,REAL:] is non trivial non finite set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V75() V191() V193() set
bool omega is non trivial non finite set
bool NAT is non trivial non finite set
RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V75() set
[:REAL,REAL:] is non trivial Relation-like non finite V59() V60() V61() set
bool [:REAL,REAL:] is non trivial non finite set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V75() V80() FinSequence-yielding finite-support V193() V194() V195() V196() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
{{},1} is non empty finite V40() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() set
K388() is set
bool K388() is set
K389() is Element of bool K388()
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
[:NAT,NAT:] is non trivial Relation-like RAT -valued INT -valued non finite V59() V60() V61() V62() set
bool [:NAT,NAT:] is non trivial non finite set
SetPrimes is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V193() Element of bool NAT
[:COMPLEX,COMPLEX:] is non trivial Relation-like non finite V59() set
bool [:COMPLEX,COMPLEX:] is non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non trivial Relation-like non finite V59() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non trivial non finite set
[:[:REAL,REAL:],REAL:] is non trivial Relation-like non finite V59() V60() V61() set
bool [:[:REAL,REAL:],REAL:] is non trivial non finite set
[:RAT,RAT:] is non trivial Relation-like RAT -valued non finite V59() V60() V61() set
bool [:RAT,RAT:] is non trivial non finite set
[:[:RAT,RAT:],RAT:] is non trivial Relation-like RAT -valued non finite V59() V60() V61() set
bool [:[:RAT,RAT:],RAT:] is non trivial non finite set
[:INT,INT:] is non trivial Relation-like RAT -valued INT -valued non finite V59() V60() V61() set
bool [:INT,INT:] is non trivial non finite set
[:[:INT,INT:],INT:] is non trivial Relation-like RAT -valued INT -valued non finite V59() V60() V61() set
bool [:[:INT,INT:],INT:] is non trivial non finite set
[:[:NAT,NAT:],NAT:] is non trivial Relation-like RAT -valued INT -valued non finite V59() V60() V61() V62() set
bool [:[:NAT,NAT:],NAT:] is non trivial non finite set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() ext-real non positive non negative finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V75() V80() FinSequence-yielding finite-support V193() V194() V195() V196() Element of NAT
Seg 1 is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of bool NAT
{1} is non empty trivial finite V40() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() set
Seg 2 is non empty finite 2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of bool NAT
{1,2} is non empty finite V40() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() set
card {} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V75() V80() FinSequence-yielding finite-support V193() V194() V195() V196() set
0 ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real positive non negative finite cardinal Element of REAL
idseq 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative finite finite-yielding V40() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V75() V80() FinSequence-yielding finite-support V193() V194() V195() V196() set
Seg 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative finite finite-yielding V40() cardinal 0 -element {} -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V75() V80() FinSequence-yielding finite-support V193() V194() V195() V196() Element of bool NAT
K105((Seg 0)) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real integer Relation-like non-empty empty-yielding Seg 0 -defined Seg 0 -valued INT -valued RAT -valued Function-like one-to-one constant functional V25( Seg 0) ext-real non positive non negative finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V75() V80() FinSequence-yielding finite-support V193() V194() V195() V196() Element of bool [:(Seg 0),(Seg 0):]
[:(Seg 0),(Seg 0):] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg 0),(Seg 0):] is finite V40() set
Product (idseq 0) is V11() real ext-real set
5 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
Sgm {} is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() V101() finite-support FinSequence of NAT
<*> REAL is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real integer Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional ext-real non positive non negative finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() V65() V66() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V75() V80() FinSequence-yielding finite-support V193() V194() V195() V196() FinSequence of REAL
Sum (<*> REAL) is V11() real ext-real Element of REAL
Product (<*> REAL) is V11() real ext-real Element of REAL
n is V11() real ext-real set
n * n is V11() real ext-real Element of REAL
m is V11() real ext-real set
m * m is V11() real ext-real Element of REAL
n * m is V11() real ext-real Element of REAL
m * n is V11() real ext-real Element of REAL
n is V11() real ext-real set
n * n is V11() real ext-real Element of REAL
m is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
2 * n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
m * n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
m |^ (n + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
(n + 1) |-> m is Relation-like NAT -defined Function-like finite n + 1 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Seg (n + 1) is non empty finite n + 1 -element n + 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of bool NAT
K334((Seg (n + 1)),m) is Relation-like NAT -defined INT -valued Function-like V29( Seg (n + 1),{m}) finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support Element of bool [:(Seg (n + 1)),{m}:]
{m} is non empty trivial finite V40() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() set
[:(Seg (n + 1)),{m}:] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg (n + 1)),{m}:] is finite V40() set
Product ((n + 1) |-> m) is V11() real ext-real set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
n + n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
m |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
n |-> m is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Seg n is finite n -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of bool NAT
K334((Seg n),m) is Relation-like NAT -defined INT -valued Function-like V29( Seg n,{m}) finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support Element of bool [:(Seg n),{m}:]
{m} is non empty trivial finite V40() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() set
[:(Seg n),{m}:] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg n),{m}:] is finite V40() set
Product (n |-> m) is V11() real ext-real set
(m |^ n) * m is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
n * m is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
m |^ (n + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
(n + 1) |-> m is Relation-like NAT -defined Function-like finite n + 1 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Seg (n + 1) is non empty finite n + 1 -element n + 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of bool NAT
K334((Seg (n + 1)),m) is Relation-like NAT -defined INT -valued Function-like V29( Seg (n + 1),{m}) finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support Element of bool [:(Seg (n + 1)),{m}:]
[:(Seg (n + 1)),{m}:] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg (n + 1)),{m}:] is finite V40() set
Product ((n + 1) |-> m) is V11() real ext-real set
m is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
m |^ (n + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
(n + 1) |-> m is Relation-like NAT -defined Function-like finite n + 1 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Seg (n + 1) is non empty finite n + 1 -element n + 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of bool NAT
K334((Seg (n + 1)),m) is Relation-like NAT -defined INT -valued Function-like V29( Seg (n + 1),{m}) finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support Element of bool [:(Seg (n + 1)),{m}:]
{m} is non empty trivial finite V40() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() set
[:(Seg (n + 1)),{m}:] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg (n + 1)),{m}:] is finite V40() set
Product ((n + 1) |-> m) is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
n |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
0 |-> n is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative finite finite-yielding V40() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V75() V80() FinSequence-yielding finite-support V193() V194() V195() V196() set
K334((Seg 0),n) is T-Sequence-like Relation-like NAT -defined INT -valued Function-like V29( Seg 0,{n}) finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support Element of bool [:(Seg 0),{n}:]
{n} is non empty trivial finite V40() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() set
[:(Seg 0),{n}:] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg 0),{n}:] is finite V40() set
Product (0 |-> n) is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
n |^ m is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
m |-> n is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Seg m is finite m -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of bool NAT
K334((Seg m),n) is Relation-like NAT -defined INT -valued Function-like V29( Seg m,{n}) finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support Element of bool [:(Seg m),{n}:]
{n} is non empty trivial finite V40() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() set
[:(Seg m),{n}:] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg m),{n}:] is finite V40() set
Product (m |-> n) is V11() real ext-real set
1 / 2 is non empty V11() real ext-real positive non negative Element of REAL
(1 / 2) - 1 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
n / 2 is V11() real ext-real non negative Element of REAL
[\(n / 2)/] is V11() real integer ext-real set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
(n + 1) / 2 is non empty V11() real ext-real positive non negative Element of REAL
[\((n + 1) / 2)/] is V11() real integer ext-real set
(n + 1) / 2 is non empty V11() real ext-real positive non negative Element of REAL
[\((n + 1) / 2)/] is V11() real integer ext-real set
- (n / 2) is V11() real ext-real non positive Element of REAL
- [\(n / 2)/] is V11() real integer V32() ext-real Element of INT
(- (n / 2)) + (n + 1) is V11() real ext-real Element of REAL
(- [\(n / 2)/]) + (n + 1) is V11() real integer ext-real Element of REAL
X1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
X2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
(n + 1) choose X1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
(n + 1) choose X2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
(n + 1) - X1 is V11() real integer ext-real Element of REAL
n - [\(n / 2)/] is V11() real integer V32() ext-real Element of INT
1 * n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
2 * n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
(2 * n) / 2 is V11() real ext-real non negative Element of REAL
mm is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
n - mm is V11() real integer ext-real Element of REAL
n -' mm is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
(n + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
idseq (n + 1) is Relation-like NAT -defined RAT -valued Function-like finite n + 1 -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support set
Seg (n + 1) is non empty finite n + 1 -element n + 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of bool NAT
K105((Seg (n + 1))) is Relation-like Seg (n + 1) -defined Seg (n + 1) -valued INT -valued RAT -valued Function-like one-to-one V25( Seg (n + 1)) finite V59() V60() V61() V62() finite-support Element of bool [:(Seg (n + 1)),(Seg (n + 1)):]
[:(Seg (n + 1)),(Seg (n + 1)):] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg (n + 1)),(Seg (n + 1)):] is finite V40() set
Product (idseq (n + 1)) is V11() real ext-real set
n ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
idseq n is Relation-like NAT -defined RAT -valued Function-like finite n -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support set
Seg n is finite n -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of bool NAT
K105((Seg n)) is Relation-like Seg n -defined Seg n -valued INT -valued RAT -valued Function-like one-to-one V25( Seg n) finite V59() V60() V61() V62() finite-support Element of bool [:(Seg n),(Seg n):]
[:(Seg n),(Seg n):] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg n),(Seg n):] is finite V40() set
Product (idseq n) is V11() real ext-real set
((n + 1) !) / (n !) is non empty V11() real ext-real positive non negative Element of REAL
(n + 1) * (n !) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
((n + 1) * (n !)) / (n !) is non empty V11() real ext-real positive non negative Element of REAL
(n !) / (n !) is non empty V11() real ext-real positive non negative Element of REAL
(n + 1) * ((n !) / (n !)) is non empty V11() real ext-real positive non negative Element of REAL
(n + 1) * 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
(n !) / ((n + 1) !) is non empty V11() real ext-real positive non negative Element of REAL
1 / (n + 1) is non empty V11() real ext-real positive non negative Element of REAL
(n / 2) + 1 is non empty V11() real ext-real positive non negative Element of REAL
n - X1 is V11() real integer V32() ext-real Element of INT
(n + 1) -' X2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
1 * X2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
2 * X2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
X2 * 2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
((n + 1) / 2) * 2 is non empty V11() real ext-real positive non negative Element of REAL
(n + 1) - X2 is V11() real integer ext-real Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
1 + n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
n + n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
n -' X1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
(n / 2) - 1 is V11() real ext-real Element of REAL
[\(n / 2)/] + 1 is V11() real integer ext-real Element of REAL
((n / 2) - 1) + 1 is V11() real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
n1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
0 + n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
1 + n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
n1 ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
idseq n1 is Relation-like NAT -defined RAT -valued Function-like finite n1 -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support set
Seg n1 is finite n1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of bool NAT
K105((Seg n1)) is Relation-like Seg n1 -defined Seg n1 -valued INT -valued RAT -valued Function-like one-to-one V25( Seg n1) finite V59() V60() V61() V62() finite-support Element of bool [:(Seg n1),(Seg n1):]
[:(Seg n1),(Seg n1):] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg n1),(Seg n1):] is finite V40() set
Product (idseq n1) is V11() real ext-real set
X1 ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
idseq X1 is Relation-like NAT -defined RAT -valued Function-like finite X1 -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support set
Seg X1 is finite X1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of bool NAT
K105((Seg X1)) is Relation-like Seg X1 -defined Seg X1 -valued INT -valued RAT -valued Function-like one-to-one V25( Seg X1) finite V59() V60() V61() V62() finite-support Element of bool [:(Seg X1),(Seg X1):]
[:(Seg X1),(Seg X1):] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg X1),(Seg X1):] is finite V40() set
Product (idseq X1) is V11() real ext-real set
(n1 !) * (X1 !) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
((n + 1) !) / ((n1 !) * (X1 !)) is non empty V11() real ext-real positive non negative Element of REAL
n1 ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
idseq n1 is Relation-like NAT -defined RAT -valued Function-like finite n1 -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support set
Seg n1 is finite n1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of bool NAT
K105((Seg n1)) is Relation-like Seg n1 -defined Seg n1 -valued INT -valued RAT -valued Function-like one-to-one V25( Seg n1) finite V59() V60() V61() V62() finite-support Element of bool [:(Seg n1),(Seg n1):]
[:(Seg n1),(Seg n1):] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg n1),(Seg n1):] is finite V40() set
Product (idseq n1) is V11() real ext-real set
(n1 !) / (n1 !) is non empty V11() real ext-real positive non negative Element of REAL
(n1 + 1) * (n1 !) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
((n1 + 1) * (n1 !)) / (n1 !) is non empty V11() real ext-real positive non negative Element of REAL
(n1 !) / (n1 !) is non empty V11() real ext-real positive non negative Element of REAL
(n1 + 1) * ((n1 !) / (n1 !)) is non empty V11() real ext-real positive non negative Element of REAL
(n1 + 1) * 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
n choose X1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
(n1 !) * (X1 !) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
(n !) / ((n1 !) * (X1 !)) is non empty V11() real ext-real positive non negative Element of REAL
(n choose X1) / ((n + 1) choose X1) is V11() real ext-real non negative Element of REAL
((n !) / ((n1 !) * (X1 !))) / (((n + 1) !) / ((n1 !) * (X1 !))) is non empty V11() real ext-real positive non negative Element of REAL
((n !) / ((n1 !) * (X1 !))) / ((n + 1) !) is non empty V11() real ext-real positive non negative Element of REAL
(((n !) / ((n1 !) * (X1 !))) / ((n + 1) !)) * ((n1 !) * (X1 !)) is non empty V11() real ext-real positive non negative Element of REAL
((n + 1) !) * ((n1 !) * (X1 !)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
(n !) / (((n + 1) !) * ((n1 !) * (X1 !))) is non empty V11() real ext-real positive non negative Element of REAL
((n !) / (((n + 1) !) * ((n1 !) * (X1 !)))) * ((n1 !) * (X1 !)) is non empty V11() real ext-real positive non negative Element of REAL
(1 / (n + 1)) / ((n1 !) * (X1 !)) is non empty V11() real ext-real positive non negative Element of REAL
((1 / (n + 1)) / ((n1 !) * (X1 !))) * ((n1 !) * (X1 !)) is non empty V11() real ext-real positive non negative Element of REAL
((n1 !) * (X1 !)) / ((n1 !) * (X1 !)) is non empty V11() real ext-real positive non negative Element of REAL
(1 / (n + 1)) / (((n1 !) * (X1 !)) / ((n1 !) * (X1 !))) is non empty V11() real ext-real positive non negative Element of REAL
(n1 !) / (n1 !) is non empty V11() real ext-real positive non negative Element of REAL
(X1 !) / (X1 !) is non empty V11() real ext-real positive non negative Element of REAL
((n1 !) / (n1 !)) / ((X1 !) / (X1 !)) is non empty V11() real ext-real positive non negative Element of REAL
(1 / (n + 1)) / (((n1 !) / (n1 !)) / ((X1 !) / (X1 !))) is non empty V11() real ext-real positive non negative Element of REAL
((n1 !) / (n1 !)) / 1 is non empty V11() real ext-real positive non negative Element of REAL
(1 / (n + 1)) / (((n1 !) / (n1 !)) / 1) is non empty V11() real ext-real positive non negative Element of REAL
1 / (n1 + 1) is non empty V11() real ext-real positive non negative Element of REAL
(1 / (n + 1)) / (1 / (n1 + 1)) is non empty V11() real ext-real positive non negative Element of REAL
1 * (n1 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
1 * (n + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
(1 * (n1 + 1)) / (1 * (n + 1)) is non empty V11() real ext-real positive non negative Element of REAL
(n1 + 1) / (n + 1) is non empty V11() real ext-real positive non negative Element of REAL
((n + 1) choose X1) / ((n + 1) choose X1) is V11() real ext-real non negative Element of REAL
(n choose X1) / (((n + 1) choose X1) / ((n + 1) choose X1)) is V11() real ext-real non negative Element of REAL
((n1 + 1) / (n + 1)) * ((n + 1) choose X1) is V11() real ext-real non negative Element of REAL
(n choose X1) / 1 is V11() real ext-real non negative Element of REAL
mm is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
mm + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
(n + 1) / (mm + 1) is non empty V11() real ext-real positive non negative Element of REAL
(n choose X1) * ((n + 1) / (mm + 1)) is V11() real ext-real non negative Element of REAL
(((n1 + 1) / (n + 1)) * ((n + 1) choose X1)) * (n + 1) is V11() real ext-real non negative Element of REAL
((((n1 + 1) / (n + 1)) * ((n + 1) choose X1)) * (n + 1)) / (mm + 1) is V11() real ext-real non negative Element of REAL
((n1 + 1) / (n + 1)) * (n + 1) is non empty V11() real ext-real positive non negative Element of REAL
(((n1 + 1) / (n + 1)) * (n + 1)) * ((n + 1) choose X1) is V11() real ext-real non negative Element of REAL
((((n1 + 1) / (n + 1)) * (n + 1)) * ((n + 1) choose X1)) / (mm + 1) is V11() real ext-real non negative Element of REAL
(n + 1) / (n + 1) is non empty V11() real ext-real positive non negative Element of REAL
((n + 1) / (n + 1)) * (n1 + 1) is non empty V11() real ext-real positive non negative Element of REAL
(((n + 1) / (n + 1)) * (n1 + 1)) * ((n + 1) choose X1) is V11() real ext-real non negative Element of REAL
((((n + 1) / (n + 1)) * (n1 + 1)) * ((n + 1) choose X1)) / (mm + 1) is V11() real ext-real non negative Element of REAL
(1 * (n1 + 1)) * ((n + 1) choose X1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
((1 * (n1 + 1)) * ((n + 1) choose X1)) / (mm + 1) is V11() real ext-real non negative Element of REAL
(n1 + 1) / (mm + 1) is non empty V11() real ext-real positive non negative Element of REAL
((n + 1) choose X1) * ((n1 + 1) / (mm + 1)) is V11() real ext-real non negative Element of REAL
mm + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
(n + 1) / (mm + 1) is non empty V11() real ext-real positive non negative Element of REAL
(n choose X1) * ((n + 1) / (mm + 1)) is V11() real ext-real non negative Element of REAL
((((n1 + 1) / (n + 1)) * ((n + 1) choose X1)) * (n + 1)) / (mm + 1) is V11() real ext-real non negative Element of REAL
((((n1 + 1) / (n + 1)) * (n + 1)) * ((n + 1) choose X1)) / (mm + 1) is V11() real ext-real non negative Element of REAL
((((n + 1) / (n + 1)) * (n1 + 1)) * ((n + 1) choose X1)) / (mm + 1) is V11() real ext-real non negative Element of REAL
((1 * (n1 + 1)) * ((n + 1) choose X1)) / (mm + 1) is V11() real ext-real non negative Element of REAL
(n1 + 1) / (mm + 1) is non empty V11() real ext-real positive non negative Element of REAL
((n + 1) choose X1) * ((n1 + 1) / (mm + 1)) is V11() real ext-real non negative Element of REAL
p1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
2 * p1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
(2 * p1) / 2 is V11() real ext-real non negative Element of REAL
((2 * p1) / 2) + (1 / 2) is non empty V11() real ext-real positive non negative Element of REAL
[\(((2 * p1) / 2) + (1 / 2))/] is V11() real integer ext-real set
[\(1 / 2)/] is V11() real integer ext-real set
p1 + [\(1 / 2)/] is V11() real integer ext-real Element of REAL
p1 + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
n choose mm is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
- X1 is V11() real integer V32() ext-real non positive Element of INT
(- X1) + (n + 1) is V11() real integer ext-real Element of REAL
(n - [\(n / 2)/]) + 1 is V11() real integer ext-real Element of REAL
((n - [\(n / 2)/]) + 1) / ((n - [\(n / 2)/]) + 1) is V11() real ext-real Element of REAL
(n - X1) + 1 is V11() real integer ext-real Element of REAL
((n - X1) + 1) / ((n - [\(n / 2)/]) + 1) is V11() real ext-real Element of REAL
1 * ((n + 1) choose X1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
(((n - X1) + 1) / ((n - [\(n / 2)/]) + 1)) * ((n + 1) choose X1) is V11() real ext-real Element of REAL
X2 ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
idseq X2 is Relation-like NAT -defined RAT -valued Function-like finite X2 -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support set
Seg X2 is finite X2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of bool NAT
K105((Seg X2)) is Relation-like Seg X2 -defined Seg X2 -valued INT -valued RAT -valued Function-like one-to-one V25( Seg X2) finite V59() V60() V61() V62() finite-support Element of bool [:(Seg X2),(Seg X2):]
[:(Seg X2),(Seg X2):] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg X2),(Seg X2):] is finite V40() set
Product (idseq X2) is V11() real ext-real set
((n + 1) -' X2) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
idseq ((n + 1) -' X2) is Relation-like NAT -defined RAT -valued Function-like finite (n + 1) -' X2 -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support set
Seg ((n + 1) -' X2) is finite (n + 1) -' X2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of bool NAT
K105((Seg ((n + 1) -' X2))) is Relation-like Seg ((n + 1) -' X2) -defined Seg ((n + 1) -' X2) -valued INT -valued RAT -valued Function-like one-to-one V25( Seg ((n + 1) -' X2)) finite V59() V60() V61() V62() finite-support Element of bool [:(Seg ((n + 1) -' X2)),(Seg ((n + 1) -' X2)):]
[:(Seg ((n + 1) -' X2)),(Seg ((n + 1) -' X2)):] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg ((n + 1) -' X2)),(Seg ((n + 1) -' X2)):] is finite V40() set
Product (idseq ((n + 1) -' X2)) is V11() real ext-real set
(X2 !) * (((n + 1) -' X2) !) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
((n + 1) !) / ((X2 !) * (((n + 1) -' X2) !)) is non empty V11() real ext-real positive non negative Element of REAL
mm ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
idseq mm is Relation-like NAT -defined RAT -valued Function-like finite mm -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support set
Seg mm is finite mm -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of bool NAT
K105((Seg mm)) is Relation-like Seg mm -defined Seg mm -valued INT -valued RAT -valued Function-like one-to-one V25( Seg mm) finite V59() V60() V61() V62() finite-support Element of bool [:(Seg mm),(Seg mm):]
[:(Seg mm),(Seg mm):] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg mm),(Seg mm):] is finite V40() set
Product (idseq mm) is V11() real ext-real set
(mm + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
idseq (mm + 1) is Relation-like NAT -defined RAT -valued Function-like finite mm + 1 -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support set
Seg (mm + 1) is non empty finite mm + 1 -element mm + 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of bool NAT
mm + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
K105((Seg (mm + 1))) is Relation-like Seg (mm + 1) -defined Seg (mm + 1) -valued INT -valued RAT -valued Function-like one-to-one V25( Seg (mm + 1)) finite V59() V60() V61() V62() finite-support Element of bool [:(Seg (mm + 1)),(Seg (mm + 1)):]
[:(Seg (mm + 1)),(Seg (mm + 1)):] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg (mm + 1)),(Seg (mm + 1)):] is finite V40() set
Product (idseq (mm + 1)) is V11() real ext-real set
(mm !) * ((mm + 1) !) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
((n + 1) * (n !)) / ((mm !) * ((mm + 1) !)) is non empty V11() real ext-real positive non negative Element of REAL
mm ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
idseq mm is Relation-like NAT -defined RAT -valued Function-like finite mm -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support set
Seg mm is finite mm -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of bool NAT
K105((Seg mm)) is Relation-like Seg mm -defined Seg mm -valued INT -valued RAT -valued Function-like one-to-one V25( Seg mm) finite V59() V60() V61() V62() finite-support Element of bool [:(Seg mm),(Seg mm):]
[:(Seg mm),(Seg mm):] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg mm),(Seg mm):] is finite V40() set
Product (idseq mm) is V11() real ext-real set
(mm + 1) * (mm !) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
(mm !) * ((mm + 1) * (mm !)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
((n + 1) * (n !)) / ((mm !) * ((mm + 1) * (mm !))) is non empty V11() real ext-real positive non negative Element of REAL
(mm !) * (mm !) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
(mm + 1) * ((mm !) * (mm !)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
((n + 1) * (n !)) / ((mm + 1) * ((mm !) * (mm !))) is non empty V11() real ext-real positive non negative Element of REAL
((mm !) * (mm !)) / (n !) is non empty V11() real ext-real positive non negative Element of REAL
((n + 1) / (mm + 1)) / (((mm !) * (mm !)) / (n !)) is non empty V11() real ext-real positive non negative Element of REAL
(n !) / ((mm !) * (mm !)) is non empty V11() real ext-real positive non negative Element of REAL
((n !) / ((mm !) * (mm !))) * ((n + 1) / (mm + 1)) is non empty V11() real ext-real positive non negative Element of REAL
(n choose mm) * ((n + 1) / (mm + 1)) is V11() real ext-real non negative Element of REAL
(n + 1) choose mm is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
p1 is V11() real integer ext-real set
2 * p1 is V11() real integer ext-real Element of REAL
(2 * p1) + 1 is V11() real integer ext-real Element of REAL
p1 + 0 is V11() real integer ext-real Element of REAL
(p1 + 0) + 1 is V11() real integer ext-real Element of REAL
[\(1 / 2)/] is V11() real integer ext-real set
p1 + [\(1 / 2)/] is V11() real integer V32() ext-real Element of INT
(p1 + [\(1 / 2)/]) + 1 is V11() real integer ext-real Element of REAL
p1 + (1 / 2) is V11() real ext-real Element of REAL
[\(p1 + (1 / 2))/] is V11() real integer ext-real set
[\(p1 + (1 / 2))/] + 1 is V11() real integer ext-real Element of REAL
n choose mm is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
[\(n / 2)/] * 2 is V11() real integer ext-real Element of REAL
(n / 2) * 2 is V11() real ext-real non negative Element of REAL
([\(n / 2)/] * 2) - [\(n / 2)/] is V11() real integer ext-real Element of REAL
X1 - [\(n / 2)/] is V11() real integer V32() ext-real Element of INT
X1 - (X1 - [\(n / 2)/]) is V11() real integer V32() ext-real Element of INT
(n - [\(n / 2)/]) - (X1 - [\(n / 2)/]) is V11() real integer V32() ext-real Element of INT
(n - X1) + 1 is V11() real integer ext-real Element of REAL
([\(n / 2)/] + 1) / ([\(n / 2)/] + 1) is V11() real ext-real Element of REAL
((n - X1) + 1) / ([\(n / 2)/] + 1) is V11() real ext-real Element of REAL
1 * ((n + 1) choose X1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
(((n - X1) + 1) / ([\(n / 2)/] + 1)) * ((n + 1) choose X1) is V11() real ext-real Element of REAL
X2 ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
idseq X2 is Relation-like NAT -defined RAT -valued Function-like finite X2 -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support set
Seg X2 is finite X2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of bool NAT
K105((Seg X2)) is Relation-like Seg X2 -defined Seg X2 -valued INT -valued RAT -valued Function-like one-to-one V25( Seg X2) finite V59() V60() V61() V62() finite-support Element of bool [:(Seg X2),(Seg X2):]
[:(Seg X2),(Seg X2):] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg X2),(Seg X2):] is finite V40() set
Product (idseq X2) is V11() real ext-real set
((n + 1) -' X2) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
idseq ((n + 1) -' X2) is Relation-like NAT -defined RAT -valued Function-like finite (n + 1) -' X2 -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support set
Seg ((n + 1) -' X2) is finite (n + 1) -' X2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of bool NAT
K105((Seg ((n + 1) -' X2))) is Relation-like Seg ((n + 1) -' X2) -defined Seg ((n + 1) -' X2) -valued INT -valued RAT -valued Function-like one-to-one V25( Seg ((n + 1) -' X2)) finite V59() V60() V61() V62() finite-support Element of bool [:(Seg ((n + 1) -' X2)),(Seg ((n + 1) -' X2)):]
[:(Seg ((n + 1) -' X2)),(Seg ((n + 1) -' X2)):] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg ((n + 1) -' X2)),(Seg ((n + 1) -' X2)):] is finite V40() set
Product (idseq ((n + 1) -' X2)) is V11() real ext-real set
(X2 !) * (((n + 1) -' X2) !) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
((n + 1) !) / ((X2 !) * (((n + 1) -' X2) !)) is non empty V11() real ext-real positive non negative Element of REAL
(mm + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
idseq (mm + 1) is Relation-like NAT -defined RAT -valued Function-like finite mm + 1 -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support set
Seg (mm + 1) is non empty finite mm + 1 -element mm + 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of bool NAT
mm + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
K105((Seg (mm + 1))) is Relation-like Seg (mm + 1) -defined Seg (mm + 1) -valued INT -valued RAT -valued Function-like one-to-one V25( Seg (mm + 1)) finite V59() V60() V61() V62() finite-support Element of bool [:(Seg (mm + 1)),(Seg (mm + 1)):]
[:(Seg (mm + 1)),(Seg (mm + 1)):] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg (mm + 1)),(Seg (mm + 1)):] is finite V40() set
Product (idseq (mm + 1)) is V11() real ext-real set
mm ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
idseq mm is Relation-like NAT -defined RAT -valued Function-like finite mm -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support set
Seg mm is finite mm -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of bool NAT
K105((Seg mm)) is Relation-like Seg mm -defined Seg mm -valued INT -valued RAT -valued Function-like one-to-one V25( Seg mm) finite V59() V60() V61() V62() finite-support Element of bool [:(Seg mm),(Seg mm):]
[:(Seg mm),(Seg mm):] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg mm),(Seg mm):] is finite V40() set
Product (idseq mm) is V11() real ext-real set
((mm + 1) !) * (mm !) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
((n + 1) * (n !)) / (((mm + 1) !) * (mm !)) is non empty V11() real ext-real positive non negative Element of REAL
mm ! is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
idseq mm is Relation-like NAT -defined RAT -valued Function-like finite mm -element FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support set
Seg mm is finite mm -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of bool NAT
K105((Seg mm)) is Relation-like Seg mm -defined Seg mm -valued INT -valued RAT -valued Function-like one-to-one V25( Seg mm) finite V59() V60() V61() V62() finite-support Element of bool [:(Seg mm),(Seg mm):]
[:(Seg mm),(Seg mm):] is Relation-like INT -valued RAT -valued finite V59() V60() V61() V62() set
bool [:(Seg mm),(Seg mm):] is finite V40() set
Product (idseq mm) is V11() real ext-real set
(mm !) * (mm + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
((mm !) * (mm + 1)) * (mm !) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
((n + 1) * (n !)) / (((mm !) * (mm + 1)) * (mm !)) is non empty V11() real ext-real positive non negative Element of REAL
(mm !) * (mm !) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
(mm + 1) * ((mm !) * (mm !)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V191() V192() V193() V194() V195() Element of NAT
((n + 1) * (n !)) / ((mm + 1) * ((mm !) * (mm !))) is non empty V11() real ext-real positive non negative Element of REAL
((mm !) * (mm !)) / (n !) is non empty V11() real ext-real positive non negative Element of REAL
((n + 1) / (mm + 1)) / (((mm !) * (mm !)) / (n !)) is non empty V11() real ext-real positive non negative Element of REAL
(n !) / ((mm !) * (mm !)) is non empty V11() real ext-real positive non negative Element of REAL
((n !) / ((mm !) * (mm !))) * ((n + 1) / (mm + 1)) is non empty V11() real ext-real positive non negative Element of REAL
(n choose mm) * ((n + 1) / (mm + 1)) is V11() real ext-real non negative Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
X1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
(n + 1) choose m is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
(n + 1) choose X1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
0 / 2 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V75() V80() FinSequence-yielding finite-support V193() V194() V195() V196() Element of REAL
[\(0 / 2)/] is V11() real integer ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
0 choose n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
0 choose m is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
0 / 2 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real integer Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V61() V62() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V75() V80() FinSequence-yielding finite-support V193() V194() V195() V196() Element of REAL
[\(0 / 2)/] is V11() real integer ext-real set
m is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
X1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative finite cardinal set
n / 2 is V11() real ext-real non negative Element of REAL
[\(n / 2)/] is V11() real integer ext-real set
n choose m is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
n choose X1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT
n -' m is epsilon-transitive epsilon-connected ordinal natural V11() real integer V32() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V193() V194() V195() Element of NAT