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