:: NAT_5 semantic presentation

REAL is non empty non trivial non finite V69() V70() V71() V75() set
NAT is ordinal non empty non trivial non finite cardinal limit_cardinal V69() V70() V71() V72() V73() V74() V75() Element of bool REAL
bool REAL is non empty non trivial non finite V48() set
COMPLEX is non empty non trivial non finite V69() V75() set
RAT is non empty non trivial non finite V69() V70() V71() V72() V75() set
INT is non empty non trivial non finite V69() V70() V71() V72() V73() V75() set
[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial non finite V59() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite V48() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial non finite V59() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite V48() set
[:REAL,REAL:] is Relation-like non empty non trivial non finite V59() V60() V61() set
bool [:REAL,REAL:] is non empty non trivial non finite V48() set
[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial non finite V59() V60() V61() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite V48() set
[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial non finite V59() V60() V61() set
bool [:RAT,RAT:] is non empty non trivial non finite V48() set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial non finite V59() V60() V61() set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite V48() set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V59() V60() V61() set
bool [:INT,INT:] is non empty non trivial non finite V48() set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V59() V60() V61() set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite V48() set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V59() V60() V61() V62() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V59() V60() V61() V62() set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite V48() set
omega is ordinal non empty non trivial non finite cardinal limit_cardinal V69() V70() V71() V72() V73() V74() V75() set
bool omega is non empty non trivial non finite V48() set
bool NAT is non empty non trivial non finite V48() set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural empty trivial V16() V17() integer 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() V63() V64() V65() V66() V69() V70() V71() V72() V73() V74() V75() Function-yielding FinSequence-yielding finite-support set
1 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
{{},1} is non empty finite V40() V69() V70() V71() V72() V73() V74() set
K420() is set
bool K420() is non empty set
K421() is Element of bool K420()
SetPrimes is non empty non trivial non finite V69() V70() V71() V72() V73() V74() Element of bool NAT
ExtREAL is non empty V70() set
2 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
[:NAT,REAL:] is Relation-like non empty non trivial non finite V59() V60() V61() set
bool [:NAT,REAL:] is non empty non trivial non finite V48() set
1 -tuples_on NAT is FinSequenceSet of NAT
3 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
[:NAT,{}:] is Relation-like non-empty empty-yielding NAT -defined RAT -valued INT -valued ordinal natural empty trivial V16() V17() integer 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() V63() V64() V65() V66() V69() V70() V71() V72() V73() V74() V75() Function-yielding FinSequence-yielding finite-support set
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural empty trivial V16() V17() integer 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() V63() V64() V65() V66() V69() V70() V71() V72() V73() V74() V75() Function-yielding FinSequence-yielding finite-support Element of NAT
dom {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural empty trivial V16() V17() integer 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() V63() V64() V65() V66() V69() V70() V71() V72() V73() V74() V75() Function-yielding FinSequence-yielding finite-support set
rng {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural empty trivial V16() V17() integer 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 V47() V59() V60() V61() V62() V63() V64() V65() V66() V69() V70() V71() V72() V73() V74() V75() Function-yielding FinSequence-yielding finite-support set
4 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
K50(1) is non empty V16() V17() integer ext-real non positive negative set
Sgm {} is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() V97() finite-support FinSequence of NAT
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued RAT -valued ordinal natural empty trivial proper V16() V17() integer 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() V63() V64() V65() V66() V69() V70() V71() V72() V73() V74() V75() Function-yielding FinSequence-yielding finite-support FinSequence of REAL
Sum (<*> REAL) is V16() V17() ext-real Element of REAL
Product (<*> REAL) is V16() V17() ext-real Element of REAL
card {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural empty trivial V16() V17() integer 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() V63() V64() V65() V66() V69() V70() V71() V72() V73() V74() V75() Function-yielding FinSequence-yielding finite-support set
NatDivisors 1 is finite V47() V69() V70() V71() V72() V73() V74() Element of bool NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( not b₁ = 0 & b₁ divides 1 ) } is set
{1} is non empty trivial finite V40() 1 -element V69() V70() V71() V72() V73() V74() Element of bool NAT
K776() is non empty V17() ext-real non positive negative Element of ExtREAL
multnat is Relation-like [:NAT,NAT:] -defined NAT -valued RAT -valued non empty Function-like total quasi_total V59() V60() V61() V62() Element of bool [:[:NAT,NAT:],NAT:]
n0 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
EU9 is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
n0 |-count EU9 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
X is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
EU9 gcd X is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
n0 |-count (EU9 gcd X) is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
n0 |-count X is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
min ((n0 |-count EU9),(n0 |-count X)) is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
fp is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
f1 is ordinal natural non empty V16() V17() integer prime ext-real positive non negative finite cardinal set
f1 |-count fp is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f1 |-count EU9 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f1 |-count X is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f1 |^ (f1 |-count EU9) is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
(f1 |-count EU9) |-> f1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product ((f1 |-count EU9) |-> f1) is V16() V17() ext-real set
f1 |^ (n0 |-count EU9) is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
(n0 |-count EU9) |-> f1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product ((n0 |-count EU9) |-> f1) is V16() V17() ext-real set
f1 |-count (f1 |^ (f1 |-count EU9)) is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f1 |^ (f1 |-count X) is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
(f1 |-count X) |-> f1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product ((f1 |-count X) |-> f1) is V16() V17() ext-real set
f1 |^ (n0 |-count X) is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
(n0 |-count X) |-> f1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product ((n0 |-count X) |-> f1) is V16() V17() ext-real set
f1 |-count (f1 |^ (f1 |-count X)) is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
n0 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
n0 + 2 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (n0 + 2) is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
(n0 + 2) |-> 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product ((n0 + 2) |-> 2) is V16() V17() ext-real set
(2 |^ (n0 + 2)) - 1 is V16() V17() integer V32() ext-real Element of INT
n0 + 1 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (n0 + 1) is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
(n0 + 1) |-> 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product ((n0 + 1) |-> 2) is V16() V17() ext-real set
EU9 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
EU9 + 2 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (EU9 + 2) is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
(EU9 + 2) |-> 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product ((EU9 + 2) |-> 2) is V16() V17() ext-real set
(2 |^ (EU9 + 2)) - 1 is V16() V17() integer V32() ext-real Element of INT
EU9 + 1 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (EU9 + 1) is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
(EU9 + 1) |-> 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product ((EU9 + 1) |-> 2) is V16() V17() ext-real set
(EU9 + 1) + 2 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ ((EU9 + 1) + 2) is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
((EU9 + 1) + 2) |-> 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product (((EU9 + 1) + 2) |-> 2) is V16() V17() ext-real set
(2 |^ ((EU9 + 1) + 2)) - 1 is V16() V17() integer V32() ext-real Element of INT
(EU9 + 1) + 1 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ ((EU9 + 1) + 1) is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
((EU9 + 1) + 1) |-> 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product (((EU9 + 1) + 1) |-> 2) is V16() V17() ext-real set
((2 |^ (EU9 + 2)) - 1) * 2 is V16() V17() integer V32() ext-real even Element of INT
(2 |^ (EU9 + 1)) * 2 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() even Element of NAT
(2 |^ (EU9 + 2)) * 2 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() even Element of NAT
1 * 2 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() even Element of NAT
((2 |^ (EU9 + 2)) * 2) - (1 * 2) is V16() V17() integer V32() ext-real Element of INT
(EU9 + 2) + 1 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ ((EU9 + 2) + 1) is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
((EU9 + 2) + 1) |-> 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product (((EU9 + 2) + 1) |-> 2) is V16() V17() ext-real set
(2 |^ ((EU9 + 2) + 1)) - 2 is V16() V17() integer V32() ext-real Element of INT
- 1 is non empty V16() V17() integer V32() ext-real non positive negative Element of INT
(- 1) + (2 |^ ((EU9 + 1) + 2)) is V16() V17() integer V32() ext-real Element of INT
- 2 is non empty V16() V17() integer V32() ext-real non positive negative Element of INT
(- 2) + (2 |^ ((EU9 + 1) + 2)) is V16() V17() integer V32() ext-real Element of INT
2 * 2 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() even Element of NAT
(2 * 2) - 1 is non empty V16() V17() integer V32() ext-real non even Element of INT
2 |^ 1 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
1 |-> 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product (1 |-> 2) is V16() V17() ext-real set
(2 |^ 1) * 2 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() even Element of NAT
((2 |^ 1) * 2) - 1 is non empty V16() V17() integer V32() ext-real non even Element of INT
1 + 1 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (1 + 1) is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
(1 + 1) |-> 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product ((1 + 1) |-> 2) is V16() V17() ext-real set
(2 |^ (1 + 1)) - 1 is V16() V17() integer V32() ext-real Element of INT
0 + 2 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (0 + 2) is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
(0 + 2) |-> 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product ((0 + 2) |-> 2) is V16() V17() ext-real set
(2 |^ (0 + 2)) - 1 is V16() V17() integer V32() ext-real Element of INT
0 + 1 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (0 + 1) is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
(0 + 1) |-> 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product ((0 + 1) |-> 2) is V16() V17() ext-real set
n0 is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
2 |-count n0 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (2 |-count n0) is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
(2 |-count n0) |-> 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product ((2 |-count n0) |-> 2) is V16() V17() ext-real set
X is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
(2 |^ (2 |-count n0)) * X is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (2 |-count n0) is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal Element of REAL
(2 |^ (2 |-count n0)) * X is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
fp is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f1 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
2 * f1 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() even Element of NAT
(2 |^ (2 |-count n0)) * 2 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() even Element of NAT
((2 |^ (2 |-count n0)) * 2) * f1 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() even Element of NAT
(2 |-count n0) + 1 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ ((2 |-count n0) + 1) is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
((2 |-count n0) + 1) |-> 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product (((2 |-count n0) + 1) |-> 2) is V16() V17() ext-real set
(2 |^ ((2 |-count n0) + 1)) * f1 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
1 * X is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
n0 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
EU9 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
2 |^ EU9 is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal Element of REAL
EU9 |-> 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support set
Product (EU9 |-> 2) is V16() V17() ext-real set
X is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
n0 gcd X is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
fp is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
f29 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f29 |-count fp is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f29 |-count 1 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f29 |-count n0 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f29 |-count X is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
min ((f29 |-count n0),(f29 |-count X)) is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
f19 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
f29 * f19 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f29 |-count 2 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
EU9 * (f29 |-count 2) is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
EU9 * 0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural empty trivial V16() V17() integer 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() V63() V64() V65() V66() V69() V70() V71() V72() V73() V74() V75() Function-yielding FinSequence-yielding finite-support Element of NAT
f1 is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
k is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
f1 gcd k is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f29 |-count (f1 gcd k) is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f29 |-count f1 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f29 |-count k is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
min ((f29 |-count f1),(f29 |-count k)) is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
n0 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
{n0} is non empty trivial finite V40() 1 -element V69() V70() V71() V72() V73() V74() set
n0 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
EU9 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
{n0,EU9} is non empty finite V40() V69() V70() V71() V72() V73() V74() set
n0 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
EU9 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
X is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
{n0,EU9,X} is non empty finite V69() V70() V71() V72() V73() V74() set
{EU9,X} is non empty finite V40() V69() V70() V71() V72() V73() V74() set
{n0} is non empty trivial finite V40() 1 -element V69() V70() V71() V72() V73() V74() set
f1 is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
fp is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
f1 \/ fp is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
n0 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
EU9 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
X is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
fp is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
{n0,EU9,X,fp} is non empty finite set
{X,fp} is non empty finite V40() V69() V70() V71() V72() V73() V74() set
{n0,EU9} is non empty finite V40() V69() V70() V71() V72() V73() V74() set
k is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
f1 is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
k \/ f1 is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
n0 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
EU9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
Del (EU9,n0) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom EU9 is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
{n0} is non empty trivial finite V40() 1 -element V69() V70() V71() V72() V73() V74() set
(dom EU9) \ {n0} is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Sgm ((dom EU9) \ {n0}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() V97() finite-support FinSequence of NAT
(Sgm ((dom EU9) \ {n0})) * EU9 is Relation-like NAT -defined Function-like finite finite-support set
dom EU9 is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
len EU9 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
Seg (len EU9) is finite len EU9 -element V69() V70() V71() V72() V73() V74() Element of bool NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= len EU9 ) } is set
(dom EU9) \ {n0} is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Sgm ((dom EU9) \ {n0}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() V97() finite-support FinSequence of NAT
n0 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
EU9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom EU9 is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
EU9 . n0 is set
Del (EU9,n0) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom EU9 is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
{n0} is non empty trivial finite V40() 1 -element V69() V70() V71() V72() V73() V74() set
(dom EU9) \ {n0} is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Sgm ((dom EU9) \ {n0}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() V97() finite-support FinSequence of NAT
(Sgm ((dom EU9) \ {n0})) * EU9 is Relation-like NAT -defined Function-like finite finite-support set
rng (Del (EU9,n0)) is finite set
X is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
Del (EU9,X) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
{X} is non empty trivial finite V40() 1 -element V69() V70() V71() V72() V73() V74() set
(dom EU9) \ {X} is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Sgm ((dom EU9) \ {X}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() V97() finite-support FinSequence of NAT
(Sgm ((dom EU9) \ {X})) * EU9 is Relation-like NAT -defined Function-like finite finite-support set
dom (Del (EU9,X)) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
len EU9 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
len (Del (EU9,n0)) is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
fp is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
fp + 1 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
dom (Del (EU9,n0)) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
f1 is set
(Del (EU9,n0)) . f1 is set
Seg fp is finite fp -element V69() V70() V71() V72() V73() V74() Element of bool NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= fp ) } is set
k is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
EU9 . k is set
k is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
0 + 1 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
k + 1 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
Seg (fp + 1) is non empty finite fp + 1 -element K204(fp,1) -element V69() V70() V71() V72() V73() V74() Element of bool NAT
K204(fp,1) is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= fp + 1 ) } is set
EU9 . (k + 1) is set
k is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
n0 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
EU9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng EU9 is finite set
Del (EU9,n0) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom EU9 is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
{n0} is non empty trivial finite V40() 1 -element V69() V70() V71() V72() V73() V74() set
(dom EU9) \ {n0} is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Sgm ((dom EU9) \ {n0}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() V97() finite-support FinSequence of NAT
(Sgm ((dom EU9) \ {n0})) * EU9 is Relation-like NAT -defined Function-like finite finite-support set
rng (Del (EU9,n0)) is finite set
EU9 . n0 is set
X is set
dom EU9 is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
f1 is set
EU9 . f1 is set
k is set
card k is ordinal cardinal set
len EU9 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
k is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
k + 1 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
Seg (k + 1) is non empty finite k + 1 -element K204(k,1) -element V69() V70() V71() V72() V73() V74() Element of bool NAT
K204(k,1) is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= k + 1 ) } is set
len (Del (EU9,n0)) is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
fp is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f29 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
Del (EU9,fp) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
{fp} is non empty trivial finite V40() 1 -element V69() V70() V71() V72() V73() V74() set
(dom EU9) \ {fp} is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Sgm ((dom EU9) \ {fp}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() V97() finite-support FinSequence of NAT
(Sgm ((dom EU9) \ {fp})) * EU9 is Relation-like NAT -defined Function-like finite finite-support set
(Del (EU9,fp)) . f29 is set
EU9 . f29 is set
dom (Del (EU9,n0)) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Seg k is finite k -element V69() V70() V71() V72() V73() V74() Element of bool NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= k ) } is set
fp is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f29 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f29 -' 1 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f29 - 1 is V16() V17() integer V32() ext-real Element of INT
(k + 1) - 1 is V16() V17() integer V32() ext-real Element of INT
f19 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
fp + 1 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
(fp + 1) - 1 is V16() V17() integer V32() ext-real Element of INT
Seg k is finite k -element V69() V70() V71() V72() V73() V74() Element of bool NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= k ) } is set
dom (Del (EU9,n0)) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Del (EU9,fp) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
{fp} is non empty trivial finite V40() 1 -element V69() V70() V71() V72() V73() V74() set
(dom EU9) \ {fp} is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Sgm ((dom EU9) \ {fp}) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() V97() finite-support FinSequence of NAT
(Sgm ((dom EU9) \ {fp})) * EU9 is Relation-like NAT -defined Function-like finite finite-support set
(Del (EU9,fp)) . (f29 -' 1) is set
(f29 -' 1) + 1 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
EU9 . ((f29 -' 1) + 1) is set
EU9 . f29 is set
(f29 - 1) + 1 is V16() V17() integer V32() ext-real Element of INT
EU9 . ((f29 - 1) + 1) is set
fp is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f29 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
n0 is set
EU9 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() V97() finite-support FinSequence of NAT
rng EU9 is finite V69() V70() V71() V72() V73() V74() Element of bool REAL
X is Relation-like NAT -defined n0 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of n0
dom X is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
X * EU9 is Relation-like NAT -defined n0 -valued Function-like finite finite-support Element of bool [:NAT,n0:]
[:NAT,n0:] is Relation-like set
bool [:NAT,n0:] is non empty set
dom EU9 is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
fp is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
Seg fp is finite fp -element V69() V70() V71() V72() V73() V74() Element of bool NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= fp ) } is set
dom (X * EU9) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
rng (X * EU9) is finite Element of bool n0
bool n0 is non empty set
n0 is set
Sgm n0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() V97() finite-support FinSequence of NAT
EU9 is set
n0 \/ EU9 is set
Sgm EU9 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() V97() finite-support FinSequence of NAT
X is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
dom X is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
X * (Sgm n0) is Relation-like NAT -defined REAL -valued Function-like finite V59() V60() V61() finite-support Element of bool [:NAT,REAL:]
X * (Sgm EU9) is Relation-like NAT -defined REAL -valued Function-like finite V59() V60() V61() finite-support Element of bool [:NAT,REAL:]
Sum X is V16() V17() ext-real Element of REAL
fp is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
Sum fp is V16() V17() ext-real Element of REAL
f1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
Sum f1 is V16() V17() ext-real Element of REAL
(Sum fp) + (Sum f1) is V16() V17() ext-real Element of REAL
len X is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
Seg (len X) is finite len X -element V69() V70() V71() V72() V73() V74() Element of bool NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= len X ) } is set
id (dom X) is Relation-like dom X -defined dom X -valued RAT -valued INT -valued Function-like one-to-one total quasi_total finite V59() V60() V61() V62() V63() V65() finite-support Element of bool [:(dom X),(dom X):]
[:(dom X),(dom X):] is Relation-like RAT -valued INT -valued finite V59() V60() V61() V62() set
bool [:(dom X),(dom X):] is non empty finite V40() set
f19 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V60() finite-support FinSequence of ExtREAL
dom f19 is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom k is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
rng (Sgm EU9) is finite V69() V70() V71() V72() V73() V74() Element of bool REAL
f29 is non empty set
(dom X) \ n0 is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
rng k is finite set
(rng k) \ n0 is finite Element of bool (rng k)
bool (rng k) is non empty finite V40() set
k " ((rng k) \ n0) is finite set
rng (Sgm n0) is finite V69() V70() V71() V72() V73() V74() Element of bool REAL
k " n0 is finite set
[:(dom f19),(dom f19):] is Relation-like RAT -valued INT -valued finite V59() V60() V61() V62() set
bool [:(dom f19),(dom f19):] is non empty finite V40() set
(Sgm n0) ^ (Sgm EU9) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V97() finite-support M24( REAL , NAT )
h is Relation-like dom f19 -defined dom f19 -valued Function-like one-to-one total quasi_total onto bijective finite V59() V60() V61() V62() finite-support Element of bool [:(dom f19),(dom f19):]
rng h is finite V69() V70() V71() V72() V73() V74() Element of bool REAL
X * h is Relation-like dom f19 -defined REAL -valued Function-like finite V59() V60() V61() finite-support Element of bool [:(dom f19),REAL:]
[:(dom f19),REAL:] is Relation-like V59() V60() V61() set
bool [:(dom f19),REAL:] is non empty set
[:f29,REAL:] is Relation-like non empty non trivial non finite V59() V60() V61() set
bool [:f29,REAL:] is non empty non trivial non finite V48() set
Y is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
-infty is non empty V17() ext-real non positive negative set
rng f19 is finite V70() Element of bool ExtREAL
bool ExtREAL is non empty V48() set
Sum f19 is ext-real Element of ExtREAL
x19 is Relation-like NAT -defined ExtREAL -valued Function-like finite FinSequence-like FinSubsequence-like V60() finite-support FinSequence of ExtREAL
Sum x19 is ext-real Element of ExtREAL
i is Relation-like NAT -defined f29 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of f29
x2 is Relation-like f29 -defined REAL -valued non empty Function-like total quasi_total V59() V60() V61() Element of bool [:f29,REAL:]
x2 * i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
x is Relation-like NAT -defined f29 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of f29
x2 * x is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
(x2 * i) ^ (x2 * x) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
Sum Y is V16() V17() ext-real Element of REAL
Sum (x2 * i) is V16() V17() ext-real Element of REAL
Sum (x2 * x) is V16() V17() ext-real Element of REAL
(Sum (x2 * i)) + (Sum (x2 * x)) is V16() V17() ext-real Element of REAL
{0} is non empty trivial functional finite V40() 1 -element V69() V70() V71() V72() V73() V74() Element of bool NAT
n0 is set
Sgm n0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() V97() finite-support FinSequence of NAT
EU9 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
Sum EU9 is V16() V17() ext-real Element of REAL
X is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
X * (Sgm n0) is Relation-like NAT -defined REAL -valued Function-like finite V59() V60() V61() finite-support Element of bool [:NAT,REAL:]
dom X is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
X " {0} is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
(dom X) \ (X " {0}) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Sum X is V16() V17() ext-real Element of REAL
(dom X) \ n0 is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
n0 \ (dom X) is Element of bool n0
bool n0 is non empty set
len X is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
Seg (len X) is finite len X -element V69() V70() V71() V72() V73() V74() Element of bool NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= len X ) } is set
idseq (len X) is Relation-like NAT -defined RAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() finite-support set
Sgm ((dom X) \ n0) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() V97() finite-support FinSequence of NAT
X * (Sgm ((dom X) \ n0)) is Relation-like NAT -defined REAL -valued Function-like finite V59() V60() V61() finite-support Element of bool [:NAT,REAL:]
len X is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
Seg (len X) is finite len X -element V69() V70() V71() V72() V73() V74() Element of bool NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= len X ) } is set
rng (Sgm ((dom X) \ n0)) is finite V69() V70() V71() V72() V73() V74() Element of bool REAL
f29 is set
n0 /\ ((dom X) \ n0) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
k is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
rng k is finite V69() V70() V71() Element of bool REAL
f29 is set
f19 is set
dom k is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
x is set
k . x is V16() V17() ext-real set
dom (Sgm ((dom X) \ n0)) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
(Sgm ((dom X) \ n0)) . x is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
X . ((Sgm ((dom X) \ n0)) . x) is V16() V17() ext-real set
x is set
(Sgm ((dom X) \ n0)) . x is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
X . f19 is V16() V17() ext-real set
X . ((Sgm ((dom X) \ n0)) . x) is V16() V17() ext-real set
k . x is V16() V17() ext-real set
dom k is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
len k is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
Seg (len k) is finite len k -element V69() V70() V71() V72() V73() V74() Element of bool NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( 1 <= b₁ & b₁ <= len k ) } is set
(Seg (len k)) --> 0 is Relation-like NAT -defined NAT -valued RAT -valued INT -valued Function-like V59() V60() V61() V62() Element of PFuncs (NAT,NAT)
PFuncs (NAT,NAT) is PartFunc-set of NAT , NAT
(len k) |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() Function-yielding V97() FinSequence-yielding finite-support Element of (len k) -tuples_on NAT
(len k) -tuples_on NAT is FinSequenceSet of NAT
n0 \/ ((dom X) \ n0) is set
f29 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() V97() finite-support FinSequence of NAT
Sum f29 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
(Sum EU9) + (Sum f29) is V16() V17() ext-real Element of REAL
n0 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
Sum n0 is V16() V17() ext-real Element of REAL
EU9 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
EU9 - {0} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom EU9 is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
EU9 " {0} is finite set
(dom EU9) \ (EU9 " {0}) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Sgm ((dom EU9) \ (EU9 " {0})) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() V97() finite-support FinSequence of NAT
(Sgm ((dom EU9) \ (EU9 " {0}))) * EU9 is Relation-like NAT -defined REAL -valued Function-like finite V59() V60() V61() finite-support set
Sum EU9 is V16() V17() ext-real Element of REAL
dom EU9 is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
EU9 " {0} is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
(dom EU9) \ (EU9 " {0}) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
n0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() V62() V97() finite-support FinSequence of NAT
dom n0 is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
EU9 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
n0 . EU9 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
n0 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
NatDivisors n0 is V69() V70() V71() V72() V73() V74() Element of bool NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( not b₁ = 0 & b₁ divides n0 ) } is set
EU9 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
NatDivisors EU9 is V69() V70() V71() V72() V73() V74() Element of bool NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( not b₁ = 0 & b₁ divides EU9 ) } is set
X is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
fp is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
X gcd fp is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
(X gcd fp) + 1 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
0 + 1 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
n0 gcd EU9 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
n0 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
NatDivisors n0 is V69() V70() V71() V72() V73() V74() Element of bool NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( not b₁ = 0 & b₁ divides n0 ) } is set
EU9 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
NatDivisors EU9 is V69() V70() V71() V72() V73() V74() Element of bool NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( not b₁ = 0 & b₁ divides EU9 ) } is set
X is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
fp is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
X * fp is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f1 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
k is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
f1 * k is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
n0 gcd EU9 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
x is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
i is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
h is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
h |-count x is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
h |-count i is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
Y is ordinal natural non empty V16() V17() integer prime ext-real positive non negative finite cardinal set
Y |-count x is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f29 is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
Y |-count f29 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
(Y |-count x) + (Y |-count f29) is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
x * f29 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
Y |-count (x * f29) is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
Y |-count i is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f19 is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
Y |-count f19 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
(Y |-count i) + (Y |-count f19) is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
n0 is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
NatDivisors n0 is finite V47() V69() V70() V71() V72() V73() V74() Element of bool NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( not b₁ = 0 & b₁ divides n0 ) } is set
EU9 is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
NatDivisors EU9 is finite V47() V69() V70() V71() V72() V73() V74() Element of bool NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( not b₁ = 0 & b₁ divides EU9 ) } is set
n0 * EU9 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
NatDivisors (n0 * EU9) is finite V47() V69() V70() V71() V72() V73() V74() Element of bool NAT
{ b₁ where b₁ is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT : ( not b₁ = 0 & b₁ divides n0 * EU9 ) } is set
X is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
fp is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
X * fp is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
k is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
f1 is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
x is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
x |-count k is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
x |-count f1 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f29 is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
f19 is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
f29 * f19 is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
i is ordinal natural non empty V16() V17() integer prime ext-real positive non negative finite cardinal set
i |-count (f29 * f19) is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
i |-count f29 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
i |-count f19 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
(i |-count f29) + (i |-count f19) is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
i |-count (n0 * EU9) is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
i |-count n0 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
i |-count EU9 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
(i |-count n0) + (i |-count EU9) is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
f29 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
(X * fp) * f29 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
n0 is ordinal natural V16() V17() integer ext-real non negative finite cardinal set
EU9 is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
n0 gcd EU9 is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
X is ordinal natural non empty V16() V17() integer ext-real positive non negative finite cardinal set
EU9 * X is ordinal natural non empty V16() V17() integer V32() ext-real positive non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
n0 gcd (EU9 * X) is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
n0 gcd X is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
(n0 gcd EU9) * (n0 gcd X) is ordinal natural V16() V17() integer V32() ext-real non negative finite cardinal V69() V70() V71() V72() V73() V74() Element of NAT
abs (EU9 * X) is ordinal natural V16() V17() integer ext-real non negative finite cardinal Element of REAL
abs EU9 is ordinal natural V16() V17() integer ext-real non negative finite cardinal Element of REAL
abs X is ordinal natural V16() V17() integer ext-real non negative finite cardinal Element of REAL
(abs EU9) * (abs X) is ordinal