:: 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