REAL is non empty non trivial non finite V73() V74() V75() V79() V210() V211() V213() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V73() V74() V75() V76() V77() V78() V79() V208() V210() Element of bool REAL
bool REAL is non trivial non finite set
bool NAT is non trivial non finite set
COMPLEX is non empty non trivial non finite V73() V79() set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V73() V74() V75() V76() V77() V78() V79() V208() V210() set
bool omega is non trivial non finite set
K148(NAT) is V35() set
RAT is non empty non trivial non finite V73() V74() V75() V76() V79() set
INT is non empty non trivial non finite V73() V74() V75() V76() V77() V79() set
[:REAL,REAL:] is non trivial non finite complex-valued ext-real-valued real-valued 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 V13() Function-like functional finite V40() cardinal {} -element FinSequence-membered ext-real non positive non negative V73() V74() V75() V76() V77() V78() V79() V210() V211() V212() V213() set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() Function-like functional finite V40() cardinal {} -element FinSequence-membered ext-real non positive non negative V73() V74() V75() V76() V77() V78() V79() V210() V211() V212() V213() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() Function-like functional finite V40() cardinal {} -element FinSequence-membered ext-real non positive non negative V73() V74() V75() V76() V77() V78() V79() V210() V211() V212() V213() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
{{},1} is non empty finite V40() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() set
K375() is set
bool K375() is set
K376() is Element of bool K375()
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
[:NAT,NAT:] is non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set
bool [:NAT,NAT:] is non trivial non finite set
[:NAT,REAL:] is non trivial non finite complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non trivial non finite set
K219(1,NAT) is M10( NAT )
SetPrimes is non empty non trivial non finite V73() V74() V75() V76() V77() V78() V208() V210() Element of bool NAT
[:COMPLEX,COMPLEX:] is non trivial non finite complex-valued set
bool [:COMPLEX,COMPLEX:] is non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non trivial non finite complex-valued set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non trivial non finite set
[:[:REAL,REAL:],REAL:] is non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:REAL,REAL:],REAL:] is non trivial non finite set
[:RAT,RAT:] is non trivial RAT -valued non finite complex-valued ext-real-valued real-valued set
bool [:RAT,RAT:] is non trivial non finite set
[:[:RAT,RAT:],RAT:] is non trivial RAT -valued non finite complex-valued ext-real-valued real-valued set
bool [:[:RAT,RAT:],RAT:] is non trivial non finite set
[:INT,INT:] is non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued set
bool [:INT,INT:] is non trivial non finite set
[:[:INT,INT:],INT:] is non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued set
bool [:[:INT,INT:],INT:] is non trivial non finite set
[:[:NAT,NAT:],NAT:] is non trivial RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set
bool [:[:NAT,NAT:],NAT:] is non trivial non finite set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() Function-like functional finite V40() cardinal {} -element FinSequence-membered ext-real non positive non negative V50() V73() V74() V75() V76() V77() V78() V79() V210() V211() V212() V213() Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
K38(1) is non empty V11() real V13() ext-real non positive negative set
Seg 1 is non empty trivial finite 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
{1} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() set
Seg 2 is non empty finite 2 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
{1,2} is non empty finite V40() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() set
n is set
x is set
k is set
k1 is set
n /\ k1 is set
x /\ k1 is set
F1() is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
F2() is set
[:NAT,F2():] is set
bool [:NAT,F2():] is set
n is set
F3(n) is set
n is Relation-like NAT -defined F2() -valued Function-like V29( NAT ,F2()) Element of bool [:NAT,F2():]
n is Relation-like NAT -defined F2() -valued Function-like V29( NAT ,F2()) Element of bool [:NAT,F2():]
n . 0 is Element of F2()
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n . x is Element of F2()
F3(x) is set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
Seg x is finite x -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
n * k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n * x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
Seg (n * x) is finite n * x -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
1 * 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() non prime finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
n |-count x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n |^ (0 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
n |^ k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n |^ (0 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
prime_factorization 1 is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization 1) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
bool SetPrimes is non trivial non finite set
prime_exponents 1 is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents 1) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() Function-like functional finite V40() cardinal {} -element FinSequence-membered ext-real non positive non negative V73() V74() V75() V76() V77() V78() V79() V210() V211() V212() V213() Element of bool SetPrimes
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
prime_factorization n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
{n} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() set
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents n) is non empty trivial finite 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool SetPrimes
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
k1 |-count n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 |^ x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
k1 |^ (k1 |-count n) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
x |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(x |^ 2) * k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x * x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(x * x) * k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x * k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x * (x * k1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
x * k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n gcd k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n * n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n gcd x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n * n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
{n} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() set
x is Relation-like NAT -defined Function-like V25( NAT ) complex-valued ext-real-valued real-valued finite-support set
support x is finite set
Sum x is V11() real ext-real set
x . n is V11() real ext-real Element of REAL
<*(x . n)*> is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V67() decreasing non-decreasing non-increasing finite-support M11( REAL ,K218(REAL))
K218(REAL) is non empty functional FinSequence-membered M10( REAL )
dom x is set
k1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
<*n*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support set
<*n*> * x is Relation-like Function-like finite complex-valued ext-real-valued real-valued finite-support set
canFS (support x) is Relation-like NAT -defined support x -valued Function-like one-to-one V30( support x) finite FinSequence-like FinSubsequence-like finite-support FinSequence of support x
(canFS (support x)) * x is Relation-like Function-like finite complex-valued ext-real-valued real-valued finite-support set
Sum k1 is V11() real ext-real Element of REAL
K625() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like V29([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
K174(REAL,k1,K625()) is V11() real ext-real Element of REAL
canFS {} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() Relation-like NAT -defined {} -valued Function-like one-to-one constant functional V30( {} ) finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V73() V74() V75() V76() V77() V78() V79() Function-yielding FinSequence-yielding finite-support V210() V211() V212() V213() FinSequence of {}
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT : ( not b1 <= 0 & b1 divides n & x divides b1 ) } is set
n div x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
{ (x * b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT : ( not b1 <= 0 & b1 divides n div x ) } is set
p is set
r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
x * e is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
r * s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e * s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x * (e * s) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x * (n div x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
p is set
r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x * r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
r * s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(n div x) * x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(r * s) * x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
r * x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s * (r * x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
prime_factorization n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
Seg 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() Function-like functional finite V40() cardinal 0 -element {} -element FinSequence-membered ext-real non positive non negative V73() V74() V75() V76() V77() V78() V79() V210() V211() V212() V213() Element of bool NAT
x is non empty finite V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
max x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() set
Seg (max x) is finite max x -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
k1 is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
prime_factorization n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
x |-count n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(prime_factorization n) . x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x |^ (x |-count n) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Seg (n + 1) is non empty finite n + 1 -element n + 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Seg n is finite n -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
prime_factorization x is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
{(n + 1)} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
(support (prime_factorization x)) \ {(n + 1)} is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(Seg (n + 1)) \ {(n + 1)} is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
prime_exponents x is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
prime_factorization n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
prime_factorization x is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
k1 is set
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
(prime_factorization n) . k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k |-count n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k |-count x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(prime_factorization x) . k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k |^ (k |-count x) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Seg (n + 1) is non empty finite n + 1 -element n + 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Seg n is finite n -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
prime_factorization x is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
k1 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() Function-like functional finite V40() cardinal {} -element FinSequence-membered ext-real non positive non negative V50() V73() V74() V75() V76() V77() V78() V79() V210() V211() V212() V213() Element of NAT
(n + 1) |^ k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
x * ((n + 1) |^ k1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
k |-count x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
p is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
p |-count x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
k1 |-count x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 |^ (k1 |-count x) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
r is set
prime_exponents x is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
e is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
prime_exponents x is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(k1 |^ (k1 |-count x)) * r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
prime_factorization s is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization s) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
prime_exponents s is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents s) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
k1 |-count s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s is set
t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(prime_exponents s) . k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
s1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
1 + s1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
k1 |^ (k1 |-count s) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
t1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(k1 |^ (k1 |-count s)) * t1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
u is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 |^ u is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(k1 |^ u) * k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
((k1 |^ u) * k1) * t1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e * (((k1 |^ u) * k1) * t1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e * k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(k1 |^ u) * t1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(e * k1) * ((k1 |^ u) * t1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(k1 |-count x) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
k1 |^ ((k1 |-count x) + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(k1 |^ ((k1 |-count x) + 1)) * ((k1 |^ u) * t1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
1 * s is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
prime_factorization t is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization t) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(n + 1) |-count x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(n + 1) |^ s is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
t * ((n + 1) |^ s) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
e is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
prime_factorization e is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization e) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
prime_exponents e is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents e) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
{k1} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
t is set
t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
t |-count t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t |-count x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t |-count e is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 |^ s is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
t |-count (k1 |^ s) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t |-count s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(t |-count (k1 |^ s)) + (t |-count s) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
t |-count t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t |-count x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
s1 |-count t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s1 |-count x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
prime_factorization x is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
Seg k1 is finite k1 -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
Seg k is finite k -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Seg (k + 1) is non empty finite k + 1 -element k + 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
p is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
prime_factorization p is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization p) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
r is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
prime_factorization r is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization r) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
e is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
e |-count r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e |^ (e |-count r) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
s is set
prime_exponents r is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents r) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
prime_exponents r is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents r) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(e |^ (e |-count r)) * s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
prime_factorization s1 is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization s1) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
prime_exponents s1 is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents s1) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
e |-count s1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
u is set
w is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(prime_exponents s1) . e is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
1 + m is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
e |^ (e |-count s1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(e |^ (e |-count s1)) * g is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
u is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e |^ u is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(e |^ u) * e is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
((e |^ u) * e) * g is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t * (((e |^ u) * e) * g) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t * e is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(e |^ u) * g is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(t * e) * ((e |^ u) * g) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(e |-count r) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
e |^ ((e |-count r) + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(e |^ ((e |-count r) + 1)) * ((e |^ u) * g) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
prime_factorization t is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization t) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
prime_exponents t is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents t) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
{e} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
t1 is set
(support (prime_factorization t)) \/ (support (prime_factorization s1)) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
t1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
t1 |-count p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t1 |-count s1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t1 |-count r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t1 |-count (e |^ (e |-count r)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(t1 |-count (e |^ (e |-count r))) + (t1 |-count s1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t1 |-count t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
t1 |-count p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
t1 |-count s1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
prime_factorization s is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization s) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(k + 1) |^ t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
s * ((k + 1) |^ t) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
s is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
prime_factorization s is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization s) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(k + 1) |^ t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
s * ((k + 1) |^ t) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
e is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
prime_exponents s is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents s) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
s1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
s1 |-count s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s1 |-count s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s1 |-count p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s1 |-count r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s1 |-count p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
prime_exponents s is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents s) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
s1 |-count r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
prime_exponents s is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents s) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
e |^ t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
e |-count (e |^ t) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e |-count r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e |-count s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(e |-count s) + t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
0 + t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e |^ t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
e |-count (e |^ t) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e |-count p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e |-count s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(e |-count s) + t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
0 + t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
Seg 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() Function-like functional finite V40() cardinal 0 -element {} -element FinSequence-membered ext-real non positive non negative V73() V74() V75() V76() V77() V78() V79() V210() V211() V212() V213() Element of bool NAT
k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
prime_factorization k is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization k) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
p is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
prime_factorization p is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization p) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
prime_exponents k is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents k) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
r is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
prime_factorization n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
x |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
k1 |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
the non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
the non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
n |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
n * n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
- 1 is non empty V11() real V13() ext-real non positive negative Element of REAL
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
x |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
x |^ 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is V73() V74() V75() V76() V77() V78() V210() Element of bool NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
n is V73() V74() V75() V76() V77() V78() V210() Element of bool NAT
x is V73() V74() V75() V76() V77() V78() V210() Element of bool NAT
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
() is V73() V74() V75() V76() V77() V78() V210() Element of bool NAT
2 |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
2 * 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
x ^2 is set
K37(x,x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
x |^ 2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
1 ^2 is V11() real ext-real Element of REAL
K37(1,1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
0 ^2 is V11() real ext-real Element of REAL
K37(0,0) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() Function-like functional finite V40() cardinal {} -element FinSequence-membered ext-real non positive non negative V73() V74() V75() V76() V77() V78() V79() V210() V211() V212() V213() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
x |-count n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
x |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
n * x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
k1 |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
x * k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
x div n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
k1 * k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(x div n) * n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(k1 * k) * n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k * n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 * (k * n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
n * p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n * n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
p * (n * n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(p * (n * n)) * k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
p * (n |^ 2) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(p * (n |^ 2)) * k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
p * k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(n |^ 2) * (p * k) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
x div n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
k1 * k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
n * p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 * p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(k1 * p) * n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT : ( not b1 <= 0 & b1 divides x & not n divides b1 ) } is set
x div n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT : ( not b1 <= 0 & b1 divides x div n ) } is set
p is set
r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
p is set
r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
- 1 is non empty V11() real V13() ext-real non positive negative Element of REAL
the non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
the non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
prime_factorization x is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
card (support (prime_factorization x)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of omega
(- 1) |^ (card (support (prime_factorization x))) is V11() real ext-real Element of REAL
k1 is V11() real ext-real set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
k1 is V11() real ext-real set
prime_factorization x is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
card (support (prime_factorization x)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of omega
(- 1) |^ (card (support (prime_factorization x))) is V11() real ext-real Element of REAL
x is V11() real ext-real set
k1 is V11() real ext-real set
r is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
k is V11() real ext-real set
prime_factorization r is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization r) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
card (support (prime_factorization r)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of omega
(- 1) |^ (card (support (prime_factorization r))) is V11() real ext-real Element of REAL
e is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
p is V11() real ext-real set
prime_factorization e is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization e) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
card (support (prime_factorization e)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of omega
(- 1) |^ (card (support (prime_factorization e))) is V11() real ext-real Element of REAL
(1) is V11() real ext-real set
card 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() Function-like functional finite V40() cardinal {} -element FinSequence-membered ext-real non positive non negative V50() V73() V74() V75() V76() V77() V78() V79() V210() V211() V212() V213() Element of omega
(- 1) |^ (card 0) is V11() real ext-real Element of REAL
(2) is V11() real ext-real set
prime_factorization 2 is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization 2) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
card (support (prime_factorization 2)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of omega
(- 1) |^ (card (support (prime_factorization 2))) is V11() real ext-real Element of REAL
{2} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
card {2} is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of omega
(- 1) |^ (card {2}) is V11() real ext-real Element of REAL
(- 1) |^ 1 is V11() real ext-real Element of REAL
(3) is V11() real ext-real set
prime_factorization 3 is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization 3) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
card (support (prime_factorization 3)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of omega
(- 1) |^ (card (support (prime_factorization 3))) is V11() real ext-real Element of REAL
{3} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
card {3} is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of omega
(- 1) |^ (card {3}) is V11() real ext-real Element of REAL
(- 1) |^ 1 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(n) is V11() real ext-real set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
prime_factorization x is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
card (support (prime_factorization x)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of omega
(- 1) |^ (card (support (prime_factorization x))) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative () set
(n) is V11() real ext-real set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
(n) is V11() real ext-real set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
prime_factorization x is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
card (support (prime_factorization x)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of omega
(- 1) |^ (card (support (prime_factorization x))) is V11() real ext-real Element of REAL
{n} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() set
card {n} is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of omega
(- 1) |^ (card {n}) is V11() real ext-real Element of REAL
(- 1) |^ 1 is V11() real ext-real Element of REAL
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n * x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
((n * x)) is V11() real ext-real set
(n) is V11() real ext-real set
(x) is V11() real ext-real set
(n) * (x) is V11() real ext-real Element of REAL
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
k1 |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
prime_factorization n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
card (support (prime_factorization n)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of omega
(- 1) |^ (card (support (prime_factorization n))) is V11() real ext-real Element of REAL
prime_exponents (n * x) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents (n * x)) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
card (support (prime_exponents (n * x))) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of omega
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
card (support (prime_exponents n)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of omega
prime_exponents x is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
card (support (prime_exponents x)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of omega
(card (support (prime_exponents n))) + (card (support (prime_exponents x))) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
prime_factorization (n * x) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization (n * x)) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
card (support (prime_factorization (n * x))) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of omega
prime_factorization x is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
card (support (prime_factorization x)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of omega
(card (support (prime_exponents n))) + (card (support (prime_factorization x))) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(card (support (prime_factorization n))) + (card (support (prime_factorization x))) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(- 1) |^ ((card (support (prime_factorization n))) + (card (support (prime_factorization x)))) is V11() real ext-real Element of REAL
(- 1) |^ (card (support (prime_factorization x))) is V11() real ext-real Element of REAL
((- 1) |^ (card (support (prime_factorization n)))) * ((- 1) |^ (card (support (prime_factorization x)))) is V11() real ext-real Element of REAL
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
k1 |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
k1 |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
k1 |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x * n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
((x * n)) is V11() real ext-real set
(x) is V11() real ext-real set
- (x) is V11() real ext-real Element of REAL
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
n * n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(n) is V11() real ext-real set
(x) * (n) is V11() real ext-real Element of REAL
(x) * (- 1) is V11() real ext-real Element of REAL
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n * x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
((n * x)) is V11() real ext-real set
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
k * k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
k |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(n) is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT : ( not b1 = 0 & b1 divides n ) } is set
x is set
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(n) is V73() V74() V75() V76() V77() V78() V210() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT : ( not b1 = 0 & b1 divides n ) } is set
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(n) is V73() V74() V75() V76() V77() V78() V210() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT : ( not b1 = 0 & b1 divides n ) } is set
Seg n is non empty finite n -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
x is set
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(n) is V73() V74() V75() V76() V77() V78() V210() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT : ( not b1 = 0 & b1 divides n ) } is set
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
Seg n is non empty finite n -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
(1) is finite with_non-empty_elements V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT : ( not b1 = 0 & b1 divides 1 ) } is set
{1} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
n is set
x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is set
x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is set
n /\ () is V73() V74() V75() V76() V77() V78() V210() Element of bool NAT
x is Relation-like NAT -defined Function-like V25( NAT ) set
x is Relation-like NAT -defined Function-like V25( NAT ) set
support x is set
dom x is set
k1 is set
x . k1 is set
k1 is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x . k is set
k1 is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(k) is V11() real ext-real set
x . k is set
k1 is Relation-like NAT -defined Function-like V25( NAT ) set
support k1 is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 . k is set
(k) is V11() real ext-real set
x is Relation-like NAT -defined Function-like V25( NAT ) set
support x is set
k1 is Relation-like NAT -defined Function-like V25( NAT ) set
support k1 is set
k is set
x . k is set
k1 . k is set
p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(p) is V11() real ext-real set
p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is set
(n) is Relation-like NAT -defined Function-like V25( NAT ) set
rng (n) is set
x is set
dom (n) is set
k1 is set
(n) . k1 is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
support (n) is set
n /\ () is V73() V74() V75() V76() V77() V78() V210() Element of bool NAT
(k) is V11() real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
support (n) is set
(n) . k is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
support (n) is set
n is finite set
(n) is Relation-like NAT -defined Function-like V25( NAT ) complex-valued ext-real-valued real-valued set
support (n) is set
n /\ () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
((1)) is Relation-like NAT -defined Function-like V25( NAT ) complex-valued ext-real-valued real-valued finite-support set
Sum ((1)) is V11() real ext-real set
({1},1) -bag is Relation-like NAT -defined RAT -valued Function-like V25( NAT ) complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags NAT
Bags NAT is non empty set
Bags NAT is non empty functional Element of bool (Bags NAT)
bool (Bags NAT) is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
{1} /\ () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
({1}) is Relation-like NAT -defined Function-like V25( NAT ) complex-valued ext-real-valued real-valued finite-support set
support ({1}) is finite set
({1}) . 1 is V11() real ext-real Element of REAL
x is Relation-like NAT -defined Function-like V25( NAT ) complex-valued ext-real-valued real-valued finite-support set
k1 is set
({1}) . k1 is V11() real ext-real Element of REAL
x . k1 is V11() real ext-real Element of REAL
support x is finite set
x . 1 is V11() real ext-real Element of REAL
n is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
x is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
(n) is Relation-like NAT -defined Function-like V25( NAT ) complex-valued ext-real-valued real-valued finite-support set
support (n) is finite set
(x) is Relation-like NAT -defined Function-like V25( NAT ) complex-valued ext-real-valued real-valued finite-support set
support (x) is finite set
(support (n)) \/ (support (x)) is finite set
(n) + (x) is Relation-like NAT -defined Function-like V25( NAT ) set
support ((n) + (x)) is set
k1 is set
n /\ () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
x /\ () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
(x) . k1 is V11() real ext-real Element of REAL
(n) . k1 is V11() real ext-real Element of REAL
((n) . k1) + ((x) . k1) is V11() real ext-real Element of REAL
((n) + (x)) . k1 is set
(n) . k1 is V11() real ext-real Element of REAL
(x) . k1 is V11() real ext-real Element of REAL
((n) . k1) + ((x) . k1) is V11() real ext-real Element of REAL
((n) + (x)) . k1 is set
n is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
x is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
n \/ x is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
((n \/ x)) is Relation-like NAT -defined Function-like V25( NAT ) complex-valued ext-real-valued real-valued finite-support set
(n) is Relation-like NAT -defined Function-like V25( NAT ) complex-valued ext-real-valued real-valued finite-support set
(x) is Relation-like NAT -defined Function-like V25( NAT ) complex-valued ext-real-valued real-valued finite-support set
(n) + (x) is Relation-like NAT -defined Function-like V25( NAT ) set
support ((n \/ x)) is finite set
(n \/ x) /\ () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
n /\ () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
x /\ () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
(n /\ ()) \/ (x /\ ()) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
k1 is set
((n \/ x)) . k1 is V11() real ext-real Element of REAL
((n) + (x)) . k1 is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
support (n) is finite set
support (x) is finite set
(k) is V11() real ext-real set
(k) + 0 is V11() real ext-real Element of REAL
(x) . k is V11() real ext-real Element of REAL
(k) + ((x) . k) is V11() real ext-real Element of REAL
(n) . k is V11() real ext-real Element of REAL
((n) . k) + ((x) . k) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
support (n) is finite set
support (x) is finite set
(k) is V11() real ext-real set
(k) + 0 is V11() real ext-real Element of REAL
(n) . k is V11() real ext-real Element of REAL
(k) + ((n) . k) is V11() real ext-real Element of REAL
(x) . k is V11() real ext-real Element of REAL
((x) . k) + ((n) . k) is V11() real ext-real Element of REAL
support (x) is finite set
support (n) is finite set
(x) . k1 is V11() real ext-real Element of REAL
((x) . k1) + 0 is V11() real ext-real Element of REAL
(n) . k1 is V11() real ext-real Element of REAL
((x) . k1) + ((n) . k1) is V11() real ext-real Element of REAL
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
x is set
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
x is Relation-like Function-like set
dom x is set
support x is set
k1 is set
k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
x . k is set
k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
x . k is set
k1 is Relation-like SetPrimes -defined Function-like V25( SetPrimes ) set
support k1 is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
k1 . k is set
x is Relation-like SetPrimes -defined Function-like V25( SetPrimes ) set
support x is set
k1 is Relation-like SetPrimes -defined Function-like V25( SetPrimes ) set
support k1 is set
k is set
p is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
x . k is set
k1 . k is set
p is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
x . k is set
k1 . k is set
p is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined Function-like V25( SetPrimes ) set
rng (n) is set
x is set
dom (n) is set
k1 is set
(n) . k1 is set
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
support (n) is set
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
support (n) is set
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(1) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
EmptyBag SetPrimes is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags SetPrimes
Bags SetPrimes is non empty set
Bags SetPrimes is non empty functional Element of bool (Bags SetPrimes)
bool (Bags SetPrimes) is set
dom (1) is set
x is set
(1) . x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
prime_exponents 1 is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents 1) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() Function-like functional finite V40() cardinal {} -element FinSequence-membered ext-real non positive non negative V73() V74() V75() V76() V77() V78() V79() V210() V211() V212() V213() Element of bool SetPrimes
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
support (1) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(dom (1)) --> 0 is Relation-like dom (1) -defined NAT -valued RAT -valued INT -valued Function-like V29( dom (1), NAT ) complex-valued ext-real-valued real-valued natural-valued Element of bool [:(dom (1)),NAT:]
[:(dom (1)),NAT:] is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:(dom (1)),NAT:] is set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
<*n*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
<*n*> * (n) is Relation-like RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
dom (<*n*> * (n)) is finite set
k is set
dom <*n*> is non empty trivial finite 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
k is set
<*n*> . k is set
dom (n) is set
dom <*n*> is non empty trivial finite 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
k is set
(<*n*> * (n)) . k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
<*n*> . k is set
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(prime_exponents n) . n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
support (prime_exponents n) is non empty trivial finite 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool SetPrimes
(<*n*> * (n)) . 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
<*n*> . 1 is set
(n) . (<*n*> . 1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(n) . n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
dom <*n*> is non empty trivial finite 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
<*n*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
n |^ x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
((n |^ x)) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
<*n*> * ((n |^ x)) is Relation-like RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
dom <*n*> is non empty trivial finite 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
dom (<*n*> * ((n |^ x))) is finite set
r is set
r is set
<*n*> . r is set
dom ((n |^ x)) is set
r is set
(<*n*> * ((n |^ x))) . r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
<*n*> . r is set
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(prime_exponents n) . n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
support (prime_exponents n) is non empty trivial finite 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool SetPrimes
prime_exponents (n |^ x) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents (n |^ x)) is non empty trivial finite 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool SetPrimes
(<*n*> * ((n |^ x))) . 1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
<*n*> . 1 is set
((n |^ x)) . (<*n*> . 1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
((n |^ x)) . n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
n |-count x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(x) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(x) . n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
prime_exponents x is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(prime_exponents x) . n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
support (prime_exponents x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
support (x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
x |-count n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(n) . x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(prime_exponents n) . x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
support (prime_exponents n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n * x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
((n * x)) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(x) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
(n) + (x) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
p is set
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
k1 * k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
r is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
r |-count (k1 * k) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
r |-count n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
r |-count x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(r |-count n) + (r |-count x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n gcd x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
r |-count (n * x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
((n * x)) . p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(x) . p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
0 + ((x) . p) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(n) . p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
((n) . p) + ((x) . p) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
((n) + (x)) . p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
r |-count (n * x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
((n * x)) . p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
((n) + (x)) . p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
r |^ (r |-count n) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
r |^ s is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
r * (r |^ s) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(r * (r |^ s)) * t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(r |^ s) * t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
r * ((r |^ s) * t) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
r |^ (r |-count x) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
r |^ t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
r * (r |^ t) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
s1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(r * (r |^ t)) * s1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(r |^ t) * s1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
r * ((r |^ t) * s1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(n) . r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
((n) . r) + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(x) . r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
((n) . r) + ((x) . r) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
r |^ (r |-count n) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
r |^ s is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
r * (r |^ s) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(r * (r |^ s)) * t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(r |^ s) * t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
r * ((r |^ s) * t) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
r |^ (r |-count x) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
r |^ t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
r * (r |^ t) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
s1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(r * (r |^ t)) * s1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(r |^ t) * s1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
r * ((r |^ t) * s1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(x) . r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
0 + ((x) . r) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(n) . r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
((n) . r) + ((x) . r) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
r |-count (n * x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
EmptyBag NAT is Relation-like NAT -defined RAT -valued Function-like V25( NAT ) complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags NAT
Bags NAT is non empty set
Bags NAT is non empty functional Element of bool (Bags NAT)
bool (Bags NAT) is set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT : ( not b1 <= 0 & b1 divides n & b1 is () ) } is set
x is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
(x) is Relation-like NAT -defined Function-like V25( NAT ) complex-valued ext-real-valued real-valued finite-support set
k1 is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 is set
(x) . k1 is V11() real ext-real Element of REAL
(EmptyBag NAT) . k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
support (x) is finite set
x /\ () is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(x) . k is V11() real ext-real Element of REAL
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
support (n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
canFS (support (n)) is Relation-like NAT -defined support (n) -valued Function-like one-to-one V30( support (n)) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of support (n)
(canFS (support (n))) * (n) is Relation-like RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
x is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued finite-support FinSequence of COMPLEX
Product x is V11() Element of COMPLEX
K621() is Relation-like [:COMPLEX,COMPLEX:] -defined COMPLEX -valued Function-like V29([:COMPLEX,COMPLEX:], COMPLEX ) complex-valued Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
K174(COMPLEX,x,K621()) is V11() Element of COMPLEX
dom x is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
x . k1 is V11() set
dom (canFS (support (n))) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
rng (canFS (support (n))) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool REAL
(canFS (support (n))) . k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(n) . k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
(n) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
support (n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents n) is non empty trivial finite 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool SetPrimes
{n} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
<*x*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V67() decreasing non-decreasing non-increasing V104() finite-support M11( NAT ,K218(NAT))
K218(NAT) is non empty functional FinSequence-membered M10( NAT )
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V104() finite-support FinSequence of NAT
rng k1 is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool REAL
Product k1 is V11() set
(x) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
<*x*> * (x) is Relation-like RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
{x} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
canFS {x} is non empty Relation-like NAT -defined {x} -valued Function-like one-to-one V30({x}) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of {x}
(canFS {x}) * (x) is Relation-like RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n |^ x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
((n |^ x)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
((n |^ x)) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product ((n |^ x)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
<*k1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V67() decreasing non-decreasing non-increasing V104() finite-support M11( NAT ,K218(NAT))
K218(NAT) is non empty functional FinSequence-membered M10( NAT )
k1 |^ x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
k is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V104() finite-support FinSequence of NAT
((k1 |^ x)) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
<*k1*> * ((k1 |^ x)) is Relation-like RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
{k1} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
canFS {k1} is non empty Relation-like NAT -defined {k1} -valued Function-like one-to-one V30({k1}) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of {k1}
(canFS {k1}) * ((k1 |^ x)) is Relation-like RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
rng k is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool REAL
Product k is V11() set
support ((k1 |^ x)) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
prime_exponents (k1 |^ x) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents (k1 |^ x)) is non empty trivial finite 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool SetPrimes
prime_exponents k1 is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents k1) is non empty trivial finite 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool SetPrimes
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(n) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
prime_factorization n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
support (n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
Seg x is finite x -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Seg (x + 1) is non empty finite x + 1 -element x + 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(k1) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (k1) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(k1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Product (k1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
prime_exponents k1 is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents k1) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(x + 1) |-count k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(x + 1) |^ ((x + 1) |-count k1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
e is set
s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
e is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
((x + 1) |^ ((x + 1) |-count k1)) * e is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(s) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (s) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
support (s) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
canFS (support (s)) is Relation-like NAT -defined support (s) -valued Function-like one-to-one V30( support (s)) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of support (s)
(canFS (support (s))) * (s) is Relation-like RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
s is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued finite-support FinSequence of COMPLEX
Product s is V11() Element of COMPLEX
K621() is Relation-like [:COMPLEX,COMPLEX:] -defined COMPLEX -valued Function-like V29([:COMPLEX,COMPLEX:], COMPLEX ) complex-valued Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
K174(COMPLEX,s,K621()) is V11() Element of COMPLEX
dom (s) is set
prime_factorization s is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization s) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
prime_exponents s is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents s) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(prime_exponents k1) . (x + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
{(x + 1)} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(t) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (t) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(x + 1) |-count t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s1 is set
prime_exponents t is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents t) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
t1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(prime_exponents t) . (x + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
u is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
1 + u is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(x + 1) |^ ((x + 1) |-count t) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
w is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
((x + 1) |^ ((x + 1) |-count t)) * w is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(x + 1) |^ m is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
((x + 1) |^ m) * (x + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(((x + 1) |^ m) * (x + 1)) * w is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s * ((((x + 1) |^ m) * (x + 1)) * w) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s * (x + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
((x + 1) |^ m) * w is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(s * (x + 1)) * (((x + 1) |^ m) * w) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
((x + 1) |-count k1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(x + 1) |^ (((x + 1) |-count k1) + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
((x + 1) |^ (((x + 1) |-count k1) + 1)) * (((x + 1) |^ m) * w) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(t) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Product (t) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
<*(x + 1)*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V67() decreasing non-decreasing non-increasing V104() finite-support M11( NAT ,K218(NAT))
K218(NAT) is non empty functional FinSequence-membered M10( NAT )
<*(x + 1)*> * (s) is Relation-like RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
(s) . (x + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
<*((s) . (x + 1))*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V67() decreasing non-decreasing non-increasing V104() finite-support M11( NAT ,K218(NAT))
(s) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
prime_factorization t is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization t) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
prime_exponents t is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents t) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
t1 is set
t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
s1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
t gcd s1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
u is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(s) + (t) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product ((s) + (t)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(s) * (t) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Seg 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() Function-like functional finite V40() cardinal 0 -element {} -element FinSequence-membered ext-real non positive non negative V73() V74() V75() V76() V77() V78() V79() V210() V211() V212() V213() Element of bool NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(x) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(x) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Product (x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
Seg x is finite x -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(x) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(x) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
prime_exponents x is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
support (x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
canFS (support (x)) is Relation-like NAT -defined support (x) -valued Function-like one-to-one V30( support (x)) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of support (x)
rng (canFS (support (x))) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool REAL
dom (canFS (support (x))) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
k1 is set
(canFS (support (x))) . k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(canFS (support (x))) * (x) is Relation-like RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
k is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued finite-support FinSequence of COMPLEX
Product k is V11() Element of COMPLEX
K621() is Relation-like [:COMPLEX,COMPLEX:] -defined COMPLEX -valued Function-like V29([:COMPLEX,COMPLEX:], COMPLEX ) complex-valued Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
K174(COMPLEX,k,K621()) is V11() Element of COMPLEX
rng (x) is V73() V74() V75() V76() V77() V78() V210() Element of bool REAL
rng k is finite V73() set
dom (x) is set
dom k is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
(x) . n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
p is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V104() finite-support FinSequence of NAT
p . k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
rng p is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool REAL
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(n) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
prime_factorization n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
x is set
(n) . x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(prime_factorization n) . x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
k1 |-count n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(prime_factorization n) . k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 |^ 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
support (n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(n) . k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
support (prime_factorization n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(n) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(x) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(x) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
n |-count (x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n |-count x is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(n) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
rng (n) is V73() V74() V75() V76() V77() V78() V210() Element of bool REAL
support (n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
canFS (support (n)) is Relation-like NAT -defined support (n) -valued Function-like one-to-one V30( support (n)) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support FinSequence of support (n)
(canFS (support (n))) * (n) is Relation-like RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support set
x is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued finite-support FinSequence of COMPLEX
Product x is V11() Element of COMPLEX
K621() is Relation-like [:COMPLEX,COMPLEX:] -defined COMPLEX -valued Function-like V29([:COMPLEX,COMPLEX:], COMPLEX ) complex-valued Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
K174(COMPLEX,x,K621()) is V11() Element of COMPLEX
rng x is finite V73() set
k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
prime_exponents n is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents n) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
rng (canFS (support (n))) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool REAL
dom (canFS (support (n))) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
p is set
(canFS (support (n))) . p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(n) . k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V104() finite-support FinSequence of NAT
k1 . p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
dom (n) is set
dom k1 is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
rng k1 is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool REAL
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(x) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(x) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n |-count (x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
prime_factorization x is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
prime_exponents x is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
support (x) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
Seg k1 is finite k1 -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
k1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Seg (k1 + 1) is non empty finite k1 + 1 -element k1 + 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(k) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (k) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(k) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Product (k) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
prime_exponents k is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents k) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
p is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
p |-count (k) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
r is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
r |-count k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
r |^ (r |-count k) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
t is set
s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(r |^ (r |-count k)) * t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
t is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
prime_factorization s is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization s) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
prime_exponents s is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents s) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(s) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (s) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(t) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (t) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
r |-count t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
w is set
prime_exponents t is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents t) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
m is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(prime_exponents t) . r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
1 + g is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
r |^ (r |-count t) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
u is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
(r |^ (r |-count t)) * u is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
r |^ g is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(r |^ g) * r is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
((r |^ g) * r) * u is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s * (((r |^ g) * r) * u) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s * r is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(r |^ g) * u is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(s * r) * ((r |^ g) * u) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(r |-count k) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
r |^ ((r |-count k) + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(r |^ ((r |-count k) + 1)) * ((r |^ g) * u) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(prime_exponents k) . r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(s) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Product (s) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
p |-count (s) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
p |-count s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
p |-count r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(r |-count k) * (p |-count r) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(r |-count k) * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() Function-like functional finite V40() cardinal {} -element FinSequence-membered ext-real non positive non negative V50() V73() V74() V75() V76() V77() V78() V79() V210() V211() V212() V213() Element of NAT
{r} is non empty trivial finite V40() 1 -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
prime_factorization t is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_factorization t) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
u is set
prime_exponents t is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (prime_exponents t) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(t) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Product (t) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
p |-count (t) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
p |-count t is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(t) . p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
p |-count s is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(s) . p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
s1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
t1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
s1 gcd t1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
w is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(s) + (t) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product ((s) + (t)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
(s) * (t) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(p |-count (t)) + (p |-count (s)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
p is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
p |-count (k) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
Seg 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() Function-like functional finite V40() cardinal 0 -element {} -element FinSequence-membered ext-real non positive non negative V73() V74() V75() V76() V77() V78() V79() V210() V211() V212() V213() Element of bool NAT
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(k1) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
support (k1) is finite V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool SetPrimes
(k1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
Product (k1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
k |-count (k1) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
Seg k1 is finite k1 -element V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of bool NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(n) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
x |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
x |-count (n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
x |^ (0 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
x |^ (1 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(n) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
x |^ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(n) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(n) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
((n)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
((n)) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product ((n)) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(n) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
Seg n is non empty finite n -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT : ( not b1 <= 0 & b1 divides (n) & x divides b1 ) } is set
k1 is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(n) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
Seg n is non empty finite n -element V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of bool NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT : ( not b1 <= 0 & b1 divides (n) & not x divides b1 ) } is set
k1 is set
k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
(x) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
(x) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() prime finite cardinal ext-real positive non negative set
k1 |-count n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
k1 |-count (x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
(x) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
(x) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (x) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT : ( not b1 <= 0 & b1 divides n & b1 is () ) } is set
(n) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real positive non negative V50() V73() V74() V75() V76() V77() V78() V208() V209() V210() V211() V212() () Element of NAT
(n) is Relation-like SetPrimes -defined RAT -valued Function-like V25( SetPrimes ) complex-valued ext-real-valued real-valued natural-valued finite-support set
Product (n) is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT : ( not b1 <= 0 & b1 divides (n) ) } is set
x is set
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT
x is set
k1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() finite cardinal ext-real non negative V50() V73() V74() V75() V76() V77() V78() V210() V211() V212() Element of NAT