:: NAT_D semantic presentation

REAL is set
NAT is non empty V7() V8() V9() non finite cardinal limit_cardinal Element of bool REAL
bool REAL is set
COMPLEX is set
NAT is non empty V7() V8() V9() non finite cardinal limit_cardinal set
bool NAT is non finite set
{} is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() V32() integer finite cardinal {} -element set
1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
0 is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() V32() integer finite cardinal {} -element Element of NAT
2 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
INT is set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n div k is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n mod k is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n div k is ext-real V14() V32() integer set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k * K) + t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * (n div k) is ext-real V14() V32() integer set
n mod k is ext-real V14() V32() integer set
(k * (n div k)) + (n mod k) is ext-real V14() V32() integer set
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k * K) + t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n mod k is ext-real V14() V32() integer set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k * t) + K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * (n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k * (n,k)) + (n mod k) is ext-real V14() V32() integer set
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k * t) + K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n div k is ext-real V14() V32() integer set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n mod k is ext-real V14() V32() integer set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n * K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n * K) + (k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * (k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n * (k,n)) + (k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real V14() V32() integer set
n * K is ext-real V14() V32() integer set
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n * t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * 0 is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() V32() integer finite cardinal {} -element set
n * 0 is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() V32() integer finite cardinal {} -element Element of NAT
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n * K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K * 1 is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * (k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n * K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n * K) + 0 is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n * (k,n)) + (k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * (k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(K,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k * (K,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k,n) * (K,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * ((k,n) * (K,k)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * (k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k * (n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * 1 is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n * (k,n)) * (n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k,n) * (n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * ((k,n) * (n,k)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n * 0 is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() V32() integer finite cardinal {} -element Element of NAT
n * 1 is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k * (n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k * (K + 1) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k * K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k + (k * K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k + K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * (k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(K,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * (K,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k,n) + (K,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * ((k,n) + (K,n)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n * t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n * t) * K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
t * K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n * (t * K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k + K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n * t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n * a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(K,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * (K,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(K,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n * (K,n)) + (K,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k + ((n * (K,n)) + (K,n)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
a + (K,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * (a + (K,n)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n * (a + (K,n))) + (K,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n * t) + 0 is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k,K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K * (k,K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(K * (k,K)) + (k,K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n lcm k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
t is ext-real V14() V32() integer set
a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
- a is ext-real non positive V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n lcm k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n gcd k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
t is ext-real V14() V32() integer set
a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
- a is ext-real non positive V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n gcd k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
F₃() is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
F₂() is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
F₁(0) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
F₁(1) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(F₂(),F₃()) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁(k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁(k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁((k + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
t + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
a + 2 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁((a + 2)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
F₁(a) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
a + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁((a + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(F₁(a),F₁((a + 1))) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
b is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁(b) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
t is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁(t) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁(n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
F₁(n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁(K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁((K + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁((K + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
F₁(t) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
t + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁((t + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
a + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
b is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁(b) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
b + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁((b + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
b + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁((b + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
M is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
F₁(M) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
M + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁((M + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
g is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
g + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
G is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
G + 2 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁((G + 2)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
F₁(G) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
G + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁((G + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(F₁(G),F₁((G + 1))) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
b + 2 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁((b + 2)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(F₁(b),F₁((b + 1))) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(F₁(b),F₁((b + 1))) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁((b + 1)) * (F₁(b),F₁((b + 1))) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(F₁((b + 1)) * (F₁(b),F₁((b + 1)))) + F₁((b + 2)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
0 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁((0 + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁(a) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
a + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁((a + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
a + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁((a + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(a + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁(((a + 1) + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
a + 2 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁((a + 2)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(F₁(a),F₁((a + 1))) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(a + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁(((a + 1) + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,2) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n * k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
((n * k),n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n * k) + 0 is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(1,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * 0 is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() V32() integer finite cardinal {} -element Element of NAT
(n * 0) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(K,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
t * k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n - (t * k) is ext-real V14() V32() integer set
a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k * a) + 0 is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
a - t is ext-real V14() V32() integer set
k * (a - t) is ext-real V14() V32() integer set
(k * (a - t)) + 0 is ext-real V14() V32() integer set
t + 0 is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k * 0 is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() V32() integer finite cardinal {} -element Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k + K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
((k + K),n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n * t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n * t) + 0 is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n + K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
((n + K),k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(K,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k * t) + 0 is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k * a) + (K,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t + a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * (t + a) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k * (t + a)) + (K,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n * k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
((n * k),n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n * k) + 0 is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n + K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
((n + K),k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(K,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n,k) + (K,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k * (n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k * (n,k)) + 0 is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(K,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k * (K,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k * (K,k)) + (K,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k * ((n,k) + (K,k)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k * ((n,k) + (K,k))) + (K,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k * t) + (K,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
((k * n),n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n * k) + 0 is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k * K) + n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(((k * K) + n),k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k * a) + t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K + a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
b is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k * b is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k * b) + t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
b is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * b is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k * b) + t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n + k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
((n + k),K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n,K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n,K) + k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(((n,K) + k),K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n,K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K * (n,K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(K * (n,K)) + (n,K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((K * (n,K)) + (n,K)) + k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((((K * (n,K)) + (n,K)) + k),K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(K * (n,K)) + ((n,K) + k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(((K * (n,K)) + ((n,K) + k)),K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n + k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
((n + k),K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k,K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n + (k,K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((n + (k,K)),K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k * 0 is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() V32() integer finite cardinal {} -element Element of NAT
(k * 0) + n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * 1 is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n * 1) + 0 is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(0,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k * (n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k * (n,k)) + K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k * (n,k)) + K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
t + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k * t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k * t) + K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k + ((k * t) + K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * (n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n,(k,n)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
b is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n * b is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n * b) + (k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
M is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n * M is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁() is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₂() is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁() * 0 is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() V32() integer finite cardinal {} -element Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
F₁() * n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁() * (n + 1) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(F₁() * n) + F₁() is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(F₂(),F₁()) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(F₂(),F₁()) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁() * (F₂(),F₁()) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(F₁() * (F₂(),F₁())) + 0 is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(F₂(),F₁()) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(F₂(),F₁()) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
F₁() * (F₂(),F₁()) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(F₁() * (F₂(),F₁())) + (F₂(),F₁()) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(F₂(),F₁()) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n * k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n,k) * (n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k * n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) * K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n * t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K * t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n * (K * t) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K * a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * (K * a) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
b is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
M is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
b * M is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
g is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
b * g is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k * M is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
M * g is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(M * g) * b is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n * g is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
G is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) * G is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K * (n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
g * b is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
M * (g * b) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(M * (g * b)) * b is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
((n,k) * G) * b is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
G * b is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(G * b) * (n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
b * G is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
0 * (n,k) is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() V32() integer finite cardinal {} -element Element of NAT
n is ext-real V14() V32() integer set
k is ext-real V14() V32() integer set
n gcd k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n mod k is ext-real V14() V32() integer set
k gcd (n mod k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
abs k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
abs n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((abs n),(abs k)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((abs n),(abs k)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((abs k),((abs n),(abs k))) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
abs ((abs n),(abs k)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((abs k),(abs ((abs n),(abs k)))) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k gcd ((abs n),(abs k)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n / k is ext-real non negative V14() V32() set
K is ext-real V14() V32() integer set
[\K/] is ext-real V14() V32() integer set
n div k is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n -' k is ext-real non negative V14() V32() set
n - k is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n + k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
((n + k),k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n + k) - k is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n - k is ext-real V14() V32() integer set
n - 0 is ext-real non negative V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k + 1) - k is ext-real V14() V32() integer set
n - k is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k + K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
((k + K),n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k + K) - n is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k + K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
((k + K),n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k,n) + K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k + K) - n is ext-real V14() V32() integer set
k - n is ext-real V14() V32() integer set
(k - n) + K is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n - k is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,0) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n - 0 is ext-real non negative V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(K,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(K,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K - n is ext-real V14() V32() integer set
K - k is ext-real V14() V32() integer set
K - k is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k,K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n - K is ext-real V14() V32() integer set
k - K is ext-real V14() V32() integer set
n - K is ext-real V14() V32() integer set
n - K is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n - k is ext-real V14() V32() integer set
(n,k) + k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n - k) + k is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,1) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n - 1 is ext-real V14() V32() integer set
(n - 1) + 1 is ext-real V14() V32() integer set
n - 1 is ext-real V14() V32() integer set
n - 1 is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,2) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n,1) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((n,1),1) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n - 1 is ext-real V14() V32() integer set
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(1 + 1) - 1 is ext-real V14() V32() integer set
1 - 1 is ext-real V14() V32() integer set
(n - 1) - 1 is ext-real V14() V32() integer set
n - 2 is ext-real V14() V32() integer set
2 - 2 is ext-real V14() V32() integer set
n - 2 is ext-real V14() V32() integer set
n + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n + 1) - 1 is ext-real V14() V32() integer set
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(1 + 1) - 1 is ext-real V14() V32() integer set
(0,1) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
1 - 1 is ext-real V14() V32() integer set
n - 1 is ext-real V14() V32() integer set
(0,1) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n,1) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n,2) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
((n,1),1) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n + 2 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((n + 1),1) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((n + 1),2) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n,1) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n,1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(((n,1) + 1),1) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n,2) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,1) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k + 1) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k + 2 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
1 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k + (1 + 1) is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,1) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n + 1) - 1 is ext-real V14() V32() integer set
k - 1 is ext-real V14() V32() integer set
0 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n + 1) - 1 is ext-real V14() V32() integer set
k - 1 is ext-real V14() V32() integer set
0 + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k - n is ext-real V14() V32() integer set
(k,n) + n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((k,n) + n) - n is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K + k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) + k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k + K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((k + K),K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n + K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,K) + K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n + k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(K,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(K,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k,n) + n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(K,n) + n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n,K) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n - K is ext-real V14() V32() integer set
k - K is ext-real V14() V32() integer set
n - K is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k,(k,n)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k,(k,n)) + (k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n + (k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k,(n + 1)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k,(n + 1)) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(k,n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k - n is ext-real V14() V32() integer set
k - (n + 1) is ext-real V14() V32() integer set
n is finite set
card n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k is set
{k} is non empty trivial 1 -element set
n is ext-real V14() V32() integer set
k is ext-real V14() V32() integer set
K is ext-real V14() V32() integer set
n * K is ext-real V14() V32() integer set
k + (n * K) is ext-real V14() V32() integer set
(k + (n * K)) div n is ext-real V14() V32() integer set
k div n is ext-real V14() V32() integer set
(k div n) + K is ext-real V14() V32() integer set
(k + (n * K)) mod n is ext-real V14() V32() integer set
k mod n is ext-real V14() V32() integer set
(k + (n * K)) / n is ext-real V14() V32() set
[\((k + (n * K)) / n)/] is ext-real V14() V32() integer set
n " is ext-real V14() V32() set
(k + (n * K)) * (n ") is ext-real V14() V32() set
[\((k + (n * K)) * (n "))/] is ext-real V14() V32() integer set
k * (n ") is ext-real V14() V32() set
n * (n ") is ext-real V14() V32() set
(n * (n ")) * K is ext-real V14() V32() set
(k * (n ")) + ((n * (n ")) * K) is ext-real V14() V32() set
[\((k * (n ")) + ((n * (n ")) * K))/] is ext-real V14() V32() integer set
1 * K is ext-real V14() V32() integer set
(k * (n ")) + (1 * K) is ext-real V14() V32() set
[\((k * (n ")) + (1 * K))/] is ext-real V14() V32() integer set
[\(k * (n "))/] is ext-real V14() V32() integer set
[\(k * (n "))/] + K is ext-real V14() V32() integer set
k / n is ext-real V14() V32() set
[\(k / n)/] is ext-real V14() V32() integer set
[\(k / n)/] + K is ext-real V14() V32() integer set
((k div n) + K) * n is ext-real V14() V32() integer set
(k + (n * K)) - (((k div n) + K) * n) is ext-real V14() V32() integer set
(k div n) * n is ext-real V14() V32() integer set
k - ((k div n) * n) is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real V14() V32() integer set
k mod n is ext-real V14() V32() integer set
k div n is ext-real V14() V32() integer set
k / n is ext-real V14() V32() set
[\(k / n)/] is ext-real V14() V32() integer set
(k div n) * n is ext-real V14() V32() integer set
(k / n) * n is ext-real V14() V32() set
n " is ext-real non negative V14() V32() set
k * (n ") is ext-real V14() V32() set
(k * (n ")) * n is ext-real V14() V32() set
(n ") * n is ext-real non negative V14() V32() set
k * ((n ") * n) is ext-real V14() V32() set
k * 1 is ext-real V14() V32() integer set
((k div n) * n) - ((k div n) * n) is ext-real V14() V32() integer set
k - ((k div n) * n) is ext-real V14() V32() integer set
n + ((k div n) * n) is ext-real V14() V32() integer set
- ((k div n) * n) is ext-real V14() V32() integer set
k + (- ((k div n) * n)) is ext-real V14() V32() integer set
(k + (- ((k div n) * n))) + ((k div n) * n) is ext-real V14() V32() integer set
(n + ((k div n) * n)) - n is ext-real V14() V32() integer set
k - n is ext-real V14() V32() integer set
((k div n) * n) * (n ") is ext-real V14() V32() set
(k - n) * (n ") is ext-real V14() V32() set
n * (n ") is ext-real non negative V14() V32() set
(k div n) * (n * (n ")) is ext-real V14() V32() set
(k div n) * 1 is ext-real V14() V32() integer set
(k * (n ")) - (n * (n ")) is ext-real V14() V32() set
(k * (n ")) - 1 is ext-real V14() V32() set
(k / n) - 1 is ext-real V14() V32() set
k is ext-real V14() V32() integer set
n is ext-real V14() V32() integer set
k mod n is ext-real V14() V32() integer set
- n is ext-real V14() V32() integer set
n + k is ext-real V14() V32() integer set
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(K,t) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
t * a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(t * a) + (K,t) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
1 + 0 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
1 * n is ext-real V14() V32() integer set
a * n is ext-real V14() V32() integer set
- 1 is ext-real non positive V14() V32() integer set
k / n is ext-real V14() V32() set
(k / n) - 1 is ext-real V14() V32() set
(- 1) + 1 is ext-real V14() V32() integer set
((k / n) - 1) + 1 is ext-real V14() V32() set
n " is ext-real V14() V32() set
k * (n ") is ext-real V14() V32() set
0 * n is ext-real V14() V32() integer set
(k * (n ")) * n is ext-real V14() V32() set
(n ") * n is ext-real V14() V32() set
k * ((n ") * n) is ext-real V14() V32() set
k * 1 is ext-real V14() V32() integer set
n " is ext-real V14() V32() set
(- n) * (n ") is ext-real V14() V32() set
k * (n ") is ext-real V14() V32() set
n * (n ") is ext-real V14() V32() set
- (n * (n ")) is ext-real V14() V32() set
[\(k / n)/] is ext-real V14() V32() integer set
k div n is ext-real V14() V32() integer set
(k div n) * n is ext-real V14() V32() integer set
k - ((k div n) * n) is ext-real V14() V32() integer set
n is ext-real V14() V32() integer set
k is ext-real V14() V32() integer set
k mod n is ext-real V14() V32() integer set
K is ext-real V14() V32() integer set
K mod n is ext-real V14() V32() integer set
k div n is ext-real V14() V32() integer set
(k div n) * n is ext-real V14() V32() integer set
k - ((k div n) * n) is ext-real V14() V32() integer set
K div n is ext-real V14() V32() integer set
(K div n) * n is ext-real V14() V32() integer set
K - ((K div n) * n) is ext-real V14() V32() integer set
k - K is ext-real V14() V32() integer set
- (K div n) is ext-real V14() V32() integer set
(- (K div n)) + (k div n) is ext-real V14() V32() integer set
((- (K div n)) + (k div n)) * n is ext-real V14() V32() integer set
t is ext-real V14() V32() integer set
n * t is ext-real V14() V32() integer set
(n * t) + K is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k is ext-real V14() V32() integer set
k mod n is ext-real V14() V32() integer set
(k mod n) mod n is ext-real V14() V32() integer set
k is ext-real V14() V32() integer set
K is ext-real V14() V32() integer set
k + K is ext-real V14() V32() integer set
n is ext-real V14() V32() integer set
(k + K) mod n is ext-real V14() V32() integer set
k mod n is ext-real V14() V32() integer set
K mod n is ext-real V14() V32() integer set
(k mod n) + (K mod n) is ext-real V14() V32() integer set
((k mod n) + (K mod n)) mod n is ext-real V14() V32() integer set
k div n is ext-real V14() V32() integer set
(k div n) * n is ext-real V14() V32() integer set
(k mod n) + ((k div n) * n) is ext-real V14() V32() integer set
k - ((k div n) * n) is ext-real V14() V32() integer set
(k - ((k div n) * n)) + ((k div n) * n) is ext-real V14() V32() integer set
K div n is ext-real V14() V32() integer set
(K div n) * n is ext-real V14() V32() integer set
(K mod n) + ((K div n) * n) is ext-real V14() V32() integer set
K - ((K div n) * n) is ext-real V14() V32() integer set
(K - ((K div n) * n)) + ((K div n) * n) is ext-real V14() V32() integer set
(k + K) - ((k mod n) + (K mod n)) is ext-real V14() V32() integer set
(k div n) + (K div n) is ext-real V14() V32() integer set
((k div n) + (K div n)) * n is ext-real V14() V32() integer set
k is ext-real V14() V32() integer set
K is ext-real V14() V32() integer set
k * K is ext-real V14() V32() integer set
n is ext-real V14() V32() integer set
(k * K) mod n is ext-real V14() V32() integer set
k mod n is ext-real V14() V32() integer set
K mod n is ext-real V14() V32() integer set
(k mod n) * (K mod n) is ext-real V14() V32() integer set
((k mod n) * (K mod n)) mod n is ext-real V14() V32() integer set
k div n is ext-real V14() V32() integer set
(k div n) * n is ext-real V14() V32() integer set
(k mod n) + ((k div n) * n) is ext-real V14() V32() integer set
k - ((k div n) * n) is ext-real V14() V32() integer set
(k - ((k div n) * n)) + ((k div n) * n) is ext-real V14() V32() integer set
K div n is ext-real V14() V32() integer set
(K div n) * n is ext-real V14() V32() integer set
(K mod n) + ((K div n) * n) is ext-real V14() V32() integer set
K - ((K div n) * n) is ext-real V14() V32() integer set
(K - ((K div n) * n)) + ((K div n) * n) is ext-real V14() V32() integer set
(k * K) - ((k mod n) * (K mod n)) is ext-real V14() V32() integer set
(k mod n) * (K div n) is ext-real V14() V32() integer set
(k div n) * (K mod n) is ext-real V14() V32() integer set
((k div n) * n) * (K div n) is ext-real V14() V32() integer set
((k div n) * (K mod n)) + (((k div n) * n) * (K div n)) is ext-real V14() V32() integer set
((k mod n) * (K div n)) + (((k div n) * (K mod n)) + (((k div n) * n) * (K div n))) is ext-real V14() V32() integer set
(((k mod n) * (K div n)) + (((k div n) * (K mod n)) + (((k div n) * n) * (K div n)))) * n is ext-real V14() V32() integer set
n is ext-real V14() V32() integer set
k is ext-real V14() V32() integer set
n gcd k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real V14() V32() integer set
t is ext-real V14() V32() integer set
K gcd t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
b is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT : ex b₂, b₃ being ext-real V14() V32() integer set st b₁ = (b₂ * a) + (b₃ * b) } is set
1 * a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
0 * b is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() V32() integer finite cardinal {} -element Element of NAT
(1 * a) + (0 * b) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
g is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
{ b₁ where b₁ is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT : ex b₂ being ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT st b₁ = b₂ * g } is set
s is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t is ext-real V14() V32() integer set
t * a is ext-real V14() V32() integer set
s is ext-real V14() V32() integer set
s * b is ext-real V14() V32() integer set
(t * a) + (s * b) is ext-real V14() V32() integer set
s is ext-real V14() V32() integer set
s * a is ext-real V14() V32() integer set
t is ext-real V14() V32() integer set
t * b is ext-real V14() V32() integer set
(s * a) + (t * b) is ext-real V14() V32() integer set
s is set
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
m is ext-real V14() V32() integer set
m * a is ext-real V14() V32() integer set
u is ext-real V14() V32() integer set
u * b is ext-real V14() V32() integer set
(m * a) + (u * b) is ext-real V14() V32() integer set
m is ext-real V14() V32() integer set
m * a is ext-real V14() V32() integer set
u is ext-real V14() V32() integer set
u * b is ext-real V14() V32() integer set
(m * a) + (u * b) is ext-real V14() V32() integer set
(t,g) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
g * (t,g) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
v is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(g * (t,g)) + v is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t - (g * (t,g)) is ext-real V14() V32() integer set
s * (t,g) is ext-real V14() V32() integer set
- (s * (t,g)) is ext-real V14() V32() integer set
m + (- (s * (t,g))) is ext-real V14() V32() integer set
a * (m + (- (s * (t,g)))) is ext-real V14() V32() integer set
t * (t,g) is ext-real V14() V32() integer set
- (t * (t,g)) is ext-real V14() V32() integer set
u + (- (t * (t,g))) is ext-real V14() V32() integer set
b * (u + (- (t * (t,g)))) is ext-real V14() V32() integer set
(a * (m + (- (s * (t,g))))) + (b * (u + (- (t * (t,g))))) is ext-real V14() V32() integer set
s is set
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
m is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
m * g is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t is ext-real V14() V32() integer set
t * g is ext-real V14() V32() integer set
t * s is ext-real V14() V32() integer set
(t * s) * a is ext-real V14() V32() integer set
t * t is ext-real V14() V32() integer set
(t * t) * b is ext-real V14() V32() integer set
((t * s) * a) + ((t * t) * b) is ext-real V14() V32() integer set
m is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
u is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
u * g is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
abs b is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
abs a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
s is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t is ext-real V14() V32() integer set
t * a is ext-real V14() V32() integer set
m is ext-real V14() V32() integer set
m * b is ext-real V14() V32() integer set
(t * a) + (m * b) is ext-real V14() V32() integer set
s is ext-real V14() V32() integer set
s * a is ext-real V14() V32() integer set
t is ext-real V14() V32() integer set
t * b is ext-real V14() V32() integer set
(s * a) + (t * b) is ext-real V14() V32() integer set
m is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
u is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
m * u is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
v is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
m * v is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
s * u is ext-real V14() V32() integer set
t * v is ext-real V14() V32() integer set
(s * u) + (t * v) is ext-real V14() V32() integer set
m * ((s * u) + (t * v)) is ext-real V14() V32() integer set
0 * a is ext-real non positive non negative empty trivial V7() V8() V9() V11() V12() V13() V14() V32() integer finite cardinal {} -element Element of NAT
1 * b is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(0 * a) + (1 * b) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
s is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t * g is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
s is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
t * g is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((abs a),(abs b)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(a,b) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K is ext-real V14() V32() integer set
t is ext-real V14() V32() integer set
K gcd t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
abs t is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
abs K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((abs K),(abs t)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
a is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
abs k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
0 * n is ext-real V14() V32() integer set
1 * k is ext-real V14() V32() integer set
(0 * n) + (1 * k) is ext-real V14() V32() integer set
k * 1 is ext-real V14() V32() integer set
- (k * 1) is ext-real V14() V32() integer set
0 * n is ext-real V14() V32() integer set
- 1 is ext-real non positive V14() V32() integer set
(- 1) * k is ext-real V14() V32() integer set
(0 * n) + ((- 1) * k) is ext-real V14() V32() integer set
0 * n is ext-real V14() V32() integer set
1 * k is ext-real V14() V32() integer set
(0 * n) + (1 * k) is ext-real V14() V32() integer set
- 1 is ext-real non positive V14() V32() integer set
(- 1) * k is ext-real V14() V32() integer set
(0 * n) + ((- 1) * k) is ext-real V14() V32() integer set
0 * n is ext-real V14() V32() integer set
1 * k is ext-real V14() V32() integer set
(0 * n) + (1 * k) is ext-real V14() V32() integer set
- 1 is ext-real non positive V14() V32() integer set
(- 1) * k is ext-real V14() V32() integer set
(0 * n) + ((- 1) * k) is ext-real V14() V32() integer set
abs n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
1 * n is ext-real V14() V32() integer set
0 * k is ext-real V14() V32() integer set
(1 * n) + (0 * k) is ext-real V14() V32() integer set
n * 1 is ext-real V14() V32() integer set
- (n * 1) is ext-real V14() V32() integer set
0 * k is ext-real V14() V32() integer set
- 1 is ext-real non positive V14() V32() integer set
(- 1) * n is ext-real V14() V32() integer set
(0 * k) + ((- 1) * n) is ext-real V14() V32() integer set
1 * n is ext-real V14() V32() integer set
0 * k is ext-real V14() V32() integer set
(1 * n) + (0 * k) is ext-real V14() V32() integer set
- 1 is ext-real non positive V14() V32() integer set
(- 1) * n is ext-real V14() V32() integer set
(0 * k) + ((- 1) * n) is ext-real V14() V32() integer set
1 * n is ext-real V14() V32() integer set
0 * k is ext-real V14() V32() integer set
(1 * n) + (0 * k) is ext-real V14() V32() integer set
- 1 is ext-real non positive V14() V32() integer set
(- 1) * n is ext-real V14() V32() integer set
(0 * k) + ((- 1) * n) is ext-real V14() V32() integer set
K is ext-real V14() V32() integer set
K * n is ext-real V14() V32() integer set
t is ext-real V14() V32() integer set
t * k is ext-real V14() V32() integer set
(K * n) + (t * k) is ext-real V14() V32() integer set
a is ext-real V14() V32() integer set
a * n is ext-real V14() V32() integer set
b is ext-real V14() V32() integer set
b * k is ext-real V14() V32() integer set
(a * n) + (b * k) is ext-real V14() V32() integer set
- n is ext-real V14() V32() integer set
(- n) gcd k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real V14() V32() integer set
K * (- n) is ext-real V14() V32() integer set
t is ext-real V14() V32() integer set
t * k is ext-real V14() V32() integer set
(K * (- n)) + (t * k) is ext-real V14() V32() integer set
abs n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
abs k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((abs n),(abs k)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
abs (- n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((abs (- n)),(abs k)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
- K is ext-real V14() V32() integer set
(- K) * n is ext-real V14() V32() integer set
((- K) * n) + (t * k) is ext-real V14() V32() integer set
- k is ext-real V14() V32() integer set
n gcd (- k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real V14() V32() integer set
K * n is ext-real V14() V32() integer set
t is ext-real V14() V32() integer set
t * (- k) is ext-real V14() V32() integer set
(K * n) + (t * (- k)) is ext-real V14() V32() integer set
abs n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
abs k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((abs n),(abs k)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
abs (- k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((abs n),(abs (- k))) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
- t is ext-real V14() V32() integer set
(- t) * k is ext-real V14() V32() integer set
(K * n) + ((- t) * k) is ext-real V14() V32() integer set
- n is ext-real V14() V32() integer set
- k is ext-real V14() V32() integer set
(- n) gcd (- k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
K is ext-real V14() V32() integer set
K * (- n) is ext-real V14() V32() integer set
t is ext-real V14() V32() integer set
t * (- k) is ext-real V14() V32() integer set
(K * (- n)) + (t * (- k)) is ext-real V14() V32() integer set
abs n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
abs k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((abs n),(abs k)) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
abs (- k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((abs n),(abs (- k))) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
abs (- n) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((abs (- n)),(abs (- k))) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
- K is ext-real V14() V32() integer set
(- K) * n is ext-real V14() V32() integer set
- t is ext-real V14() V32() integer set
(- t) * k is ext-real V14() V32() integer set
((- K) * n) + ((- t) * k) is ext-real V14() V32() integer set
K is ext-real V14() V32() integer set
K * n is ext-real V14() V32() integer set
t is ext-real V14() V32() integer set
t * k is ext-real V14() V32() integer set
(K * n) + (t * k) is ext-real V14() V32() integer set
a is ext-real V14() V32() integer set
a * n is ext-real V14() V32() integer set
b is ext-real V14() V32() integer set
b * k is ext-real V14() V32() integer set
(a * n) + (b * k) is ext-real V14() V32() integer set
M is ext-real V14() V32() integer set
M * n is ext-real V14() V32() integer set
g is ext-real V14() V32() integer set
g * k is ext-real V14() V32() integer set
(M * n) + (g * k) is ext-real V14() V32() integer set
G is ext-real V14() V32() integer set
G * n is ext-real V14() V32() integer set
s is ext-real V14() V32() integer set
s * k is ext-real V14() V32() integer set
(G * n) + (s * k) is ext-real V14() V32() integer set
K is ext-real V14() V32() integer set
K * n is ext-real V14() V32() integer set
t is ext-real V14() V32() integer set
t * k is ext-real V14() V32() integer set
(K * n) + (t * k) is ext-real V14() V32() integer set
a is ext-real V14() V32() integer set
a * n is ext-real V14() V32() integer set
b is ext-real V14() V32() integer set
b * k is ext-real V14() V32() integer set
(a * n) + (b * k) is ext-real V14() V32() integer set
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k - 1 is ext-real V14() V32() integer set
((n + 1),k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
K + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k - 0 is ext-real non negative V14() V32() integer set
(k,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
n is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
n + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
k is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal set
k - 1 is ext-real V14() V32() integer set
(n,k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
((n + 1),k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(n,k) + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT
(((n,k) + 1),k) is ext-real non negative V7() V8() V9() V13() V14() V32() integer finite cardinal Element of NAT