:: NAT_2 semantic presentation

REAL is V35() V36() V37() V41() set
NAT is V35() V36() V37() V38() V39() V40() V41() Element of bool REAL
bool REAL is set
COMPLEX is V35() V41() set
RAT is V35() V36() V37() V38() V41() set
INT is V35() V36() V37() V38() V39() V41() set
[:NAT,REAL:] is set
bool [:NAT,REAL:] is set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is set
[:[:NAT,NAT:],NAT:] is set
bool [:[:NAT,NAT:],NAT:] is set
omega is V35() V36() V37() V38() V39() V40() V41() set
bool omega is set
bool NAT is set
K372() is set
1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
2 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
3 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
0 is ext-real non positive non negative empty trivial ordinal natural V14() real functional integer V35() V36() V37() V38() V39() V40() V41() V57() FinSequence-membered Element of NAT
{} is empty trivial functional V35() V36() V37() V38() V39() V40() V41() FinSequence-membered set
{{}} is non empty trivial set
F₁() is non empty set
F₃() is ext-real non negative ordinal natural V14() real integer set
F₂() is Element of F₁()
i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j is Element of F₁()
i is V16() V19( NAT ) V20(F₁()) Function-like V52() FinSequence-like FinSubsequence-like FinSequence of F₁()
len i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i . 1 is set
i /. 1 is Element of F₁()
0 + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j is ext-real non negative ordinal natural V14() real integer set
i /. j is Element of F₁()
j + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i /. (j + 1) is Element of F₁()
i . (j + 1) is set
i . j is set
i is ext-real V14() real set
j is ext-real V14() real set
i / j is ext-real V14() real set
[\(i / j)/] is ext-real V14() real integer set
[\(i / j)/] + 1 is ext-real V14() real integer set
i / ([\(i / j)/] + 1) is ext-real V14() real set
([\(i / j)/] + 1) * j is ext-real V14() real set
(i / j) * j is ext-real V14() real set
i is ext-real non negative ordinal natural V14() real integer set
0 div i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i * (0 div i) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j is ext-real non negative ordinal natural V14() real integer set
(i * (0 div i)) + j is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j is ext-real non negative ordinal natural V14() real integer set
(i * (0 div i)) + j is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i * (0 div i) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real positive non negative non empty ordinal natural V14() real integer set
i div i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i * 1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(i * 1) div i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real non negative ordinal natural V14() real integer set
i div 1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
1 * i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(1 * i) + 0 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real non negative ordinal natural V14() real integer set
j is ext-real non negative ordinal natural V14() real integer set
j -' i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
k is ext-real non negative ordinal natural V14() real integer set
j -' k is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
t2 is ext-real non negative ordinal natural V14() real integer set
(j -' k) + t2 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(j -' i) + t2 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i - t2 is ext-real V14() real integer set
j - k is ext-real V14() real integer set
j - i is ext-real V14() real integer set
(j - i) + t2 is ext-real V14() real integer set
i is ext-real non negative ordinal natural V14() real integer set
j is ext-real non negative ordinal natural V14() real integer set
Seg j is V35() V36() V37() V38() V39() V40() V52() V68(j) Element of bool NAT
j -' i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(j -' i) + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j - i is ext-real V14() real integer set
j - 1 is ext-real V14() real integer set
(j - i) + 1 is ext-real V14() real integer set
i is ext-real non negative ordinal natural V14() real integer set
i + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j is ext-real non negative ordinal natural V14() real integer set
j -' (i + 1) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(j -' (i + 1)) + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j -' i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j - (i + 1) is ext-real V14() real integer set
(j - (i + 1)) + 1 is ext-real V14() real integer set
j - i is ext-real V14() real integer set
i is ext-real non negative ordinal natural V14() real integer set
j is ext-real non negative ordinal natural V14() real integer set
j -' i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j - i is ext-real V14() real integer set
i is ext-real positive non negative non empty ordinal natural V14() real integer set
j is ext-real positive non negative non empty ordinal natural V14() real integer set
i -' j is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i - 0 is ext-real positive non negative non empty V14() real integer set
i - j is ext-real V14() real integer set
i is ext-real non negative ordinal natural V14() real integer set
2 to_power i is ext-real non negative ordinal natural V14() real integer set
j is ext-real non negative ordinal natural V14() real integer set
2 to_power j is ext-real non negative ordinal natural V14() real integer set
j -' i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
2 to_power (j -' i) is ext-real non negative ordinal natural V14() real integer set
(2 to_power i) * (2 to_power (j -' i)) is ext-real non negative ordinal natural V14() real integer set
i + (j -' i) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real non negative ordinal natural V14() real integer set
2 to_power i is ext-real non negative ordinal natural V14() real integer set
j is ext-real non negative ordinal natural V14() real integer set
2 to_power j is ext-real non negative ordinal natural V14() real integer set
j -' i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
2 to_power (j -' i) is ext-real non negative ordinal natural V14() real integer set
(2 to_power i) * (2 to_power (j -' i)) is ext-real non negative ordinal natural V14() real integer set
i is ext-real non negative ordinal natural V14() real integer set
j is ext-real non negative ordinal natural V14() real integer set
j div i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i * (j div i) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
k is ext-real non negative ordinal natural V14() real integer set
(i * (j div i)) + k is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real non negative ordinal natural V14() real integer set
j is ext-real non negative ordinal natural V14() real integer set
j div i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
0 + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real non negative ordinal natural V14() real integer set
j is ext-real non negative ordinal natural V14() real integer set
j + i is ext-real non negative ordinal natural V14() real integer set
(j + i) div i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j div i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(j div i) + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i * (j div i) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
k is ext-real non negative ordinal natural V14() real integer set
(i * (j div i)) + k is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i * ((j div i) + 1) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(i * ((j div i) + 1)) + k is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real non negative ordinal natural V14() real integer set
j is ext-real non negative ordinal natural V14() real integer set
j div i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(j div i) - 1 is ext-real V14() real integer set
k is ext-real non negative ordinal natural V14() real integer set
j -' k is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(j -' k) div i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i -' k is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
k + i is ext-real non negative ordinal natural V14() real integer set
i + j is ext-real non negative ordinal natural V14() real integer set
0 + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(j div i) -' 1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i * (j div i) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i * 1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(i * (j div i)) - (i * 1) is ext-real V14() real integer set
((i * (j div i)) - (i * 1)) + i is ext-real V14() real integer set
(((i * (j div i)) - (i * 1)) + i) - k is ext-real V14() real integer set
i * ((j div i) -' 1) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i - k is ext-real V14() real integer set
(i * ((j div i) -' 1)) + (i - k) is ext-real V14() real integer set
(i * ((j div i) -' 1)) + (i -' k) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real non negative ordinal natural V14() real integer set
2 to_power i is ext-real non negative ordinal natural V14() real integer set
j is ext-real non negative ordinal natural V14() real integer set
2 to_power j is ext-real non negative ordinal natural V14() real integer set
(2 to_power j) div (2 to_power i) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j -' i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
2 to_power (j -' i) is ext-real non negative ordinal natural V14() real integer set
(2 to_power i) * (2 to_power (j -' i)) is ext-real non negative ordinal natural V14() real integer set
i is ext-real non negative ordinal natural V14() real integer set
2 to_power i is ext-real non negative ordinal natural V14() real integer set
(2 to_power i) mod 2 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
0 + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i - 1 is ext-real V14() real integer set
(i - 1) + 1 is ext-real V14() real integer set
2 to_power ((i - 1) + 1) is ext-real V14() real set
i -' 1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(i -' 1) + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
2 to_power ((i -' 1) + 1) is ext-real non negative ordinal natural V14() real integer Element of REAL
2 to_power (i -' 1) is ext-real non negative ordinal natural V14() real integer set
2 to_power 1 is ext-real non negative ordinal natural V14() real integer Element of REAL
(2 to_power (i -' 1)) * (2 to_power 1) is ext-real non negative ordinal natural V14() real integer set
(2 to_power (i -' 1)) * 2 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
i is ext-real non negative ordinal natural V14() real integer set
i mod 2 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i -' 1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(i -' 1) mod 2 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j is ext-real non negative ordinal natural V14() real integer set
2 * j is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
(2 * j) + (i mod 2) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
0 + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j - 1 is ext-real V14() real integer set
(j - 1) + 1 is ext-real V14() real integer set
2 * ((j - 1) + 1) is ext-real V14() real integer even set
(2 * ((j - 1) + 1)) - 1 is ext-real non empty V14() real integer non even set
2 * (j - 1) is ext-real V14() real integer even set
1 + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(1 + 1) - 1 is ext-real V14() real integer set
(2 * (j - 1)) + ((1 + 1) - 1) is ext-real V14() real integer set
j -' 1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
2 * (j -' 1) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
(2 * (j -' 1)) + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() non even Element of NAT
j is ext-real non negative ordinal natural V14() real integer set
2 * j is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
(2 * j) + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() non even Element of NAT
0 + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
((2 * j) + 1) + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
j + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
2 * (j + 1) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
(2 * (j + 1)) + 0 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real positive non negative non empty ordinal natural V14() real integer set
i is ext-real non negative ordinal natural V14() real integer set
i + i is ext-real non negative ordinal natural V14() real integer set
j is ext-real non negative ordinal natural V14() real integer set
j div i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j - i is ext-real V14() real integer set
i + (j - i) is ext-real V14() real integer set
i * 1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j -' i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(i * 1) + (j -' i) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(i + i) - i is ext-real V14() real integer set
i is ext-real non negative ordinal natural V14() real integer set
i mod 2 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
2 * j is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
(2 * j) + 0 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j is ext-real non negative ordinal natural V14() real integer set
2 * j is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
(2 * j) + 0 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real non negative ordinal natural V14() real integer set
i mod 2 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real non negative ordinal natural V14() real integer set
2 * i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
j is ext-real non negative ordinal natural V14() real integer set
k is ext-real non negative ordinal natural V14() real integer set
k div i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
k -' j is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(k -' j) div i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
t2 is ext-real non negative ordinal natural V14() real integer set
(2 * i) * t2 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
t1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
2 * t1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
i * (2 * t1) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
q is ext-real non negative ordinal natural V14() real integer set
(i * (2 * t1)) + q is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
1 * i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(2 * i) + i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i + q is ext-real non negative ordinal natural V14() real integer set
q / (2 * i) is ext-real non negative V14() real set
t1 + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
t1 + (q / (2 * i)) is ext-real non negative V14() real set
r is ext-real non negative ordinal natural V14() real integer set
(2 * i) * r is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
(2 * i) * t1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
(q / (2 * i)) * (2 * i) is ext-real non negative V14() real set
((2 * i) * t1) + ((q / (2 * i)) * (2 * i)) is ext-real non negative V14() real set
(2 * i) * (t1 + (q / (2 * i))) is ext-real non negative V14() real set
(t1 + 1) + (t1 + (q / (2 * i))) is ext-real positive non negative non empty V14() real set
(t1 + (q / (2 * i))) + r is ext-real non negative V14() real set
((i * (2 * t1)) + q) - ((2 * i) * r) is ext-real V14() real integer set
t1 - r is ext-real V14() real integer set
2 * (t1 - r) is ext-real V14() real integer even set
i * (2 * (t1 - r)) is ext-real V14() real integer even set
(i * (2 * (t1 - r))) + q is ext-real V14() real integer set
t1 -' r is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
2 * (t1 -' r) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
i * (2 * (t1 -' r)) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
(i * (2 * (t1 -' r))) + q is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
t1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
2 * t1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
i * (2 * t1) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
q is ext-real non negative ordinal natural V14() real integer set
(i * (2 * t1)) + q is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
k - j is ext-real V14() real integer set
t1 + t2 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
2 * (t1 + t2) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
i * (2 * (t1 + t2)) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
(i * (2 * (t1 + t2))) + q is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real non negative ordinal natural V14() real integer set
j is ext-real non negative ordinal natural V14() real integer set
k is ext-real non negative ordinal natural V14() real integer set
i div k is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j div k is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(i div k) -' (j div k) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(i div k) - (j div k) is ext-real V14() real integer set
(j div k) - (j div k) is ext-real V14() real integer set
0 + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
k * 1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
k * ((i div k) -' (j div k)) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
k * (j div k) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
k + (k * (j div k)) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(k * ((i div k) -' (j div k))) + (k * (j div k)) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
t1 is ext-real non negative ordinal natural V14() real integer set
(k * (j div k)) + t1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(k + (k * (j div k))) - (k + (k * (j div k))) is ext-real V14() real integer set
k * (i div k) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j - (k * (i div k)) is ext-real V14() real integer set
t1 is ext-real non negative ordinal natural V14() real integer set
(k * (i div k)) + t1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(k * (i div k)) - (k * (i div k)) is ext-real V14() real integer set
j - i is ext-real V14() real integer set
0 + i is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real non negative ordinal natural V14() real integer set
i + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(i + 1) div 2 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j is ext-real non negative ordinal natural V14() real integer set
2 * j is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
(2 * j) + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() non even Element of NAT
((2 * j) + 1) div 2 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real non negative ordinal natural V14() real integer set
i div 2 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(i + 1) div 2 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
2 * (i div 2) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() even Element of NAT
i mod 2 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(2 * (i div 2)) + (i mod 2) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(2 * (i div 2)) + 0 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real non negative ordinal natural V14() real integer set
j is ext-real non negative ordinal natural V14() real integer set
i div j is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
k is ext-real non negative ordinal natural V14() real integer set
(i div j) div k is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j * k is ext-real non negative ordinal natural V14() real integer set
i div (j * k) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
k * ((i div j) div k) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
t2 is ext-real non negative ordinal natural V14() real integer set
(k * ((i div j) div k)) + t2 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
t2 + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j * (t2 + 1) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j * (i div j) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
t1 is ext-real non negative ordinal natural V14() real integer set
(j * (i div j)) + t1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j * t2 is ext-real non negative ordinal natural V14() real integer set
j * 1 is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(j * t2) + (j * 1) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(j * t2) + t1 is ext-real non negative ordinal natural V14() real integer set
(j * (t2 + 1)) - (j * (t2 + 1)) is ext-real V14() real integer set
((j * t2) + t1) - (j * k) is ext-real V14() real integer set
0 + (j * k) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
(j * k) * ((i div j) div k) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
((j * k) * ((i div j) div k)) + ((j * t2) + t1) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real non negative ordinal natural V14() real integer set
1 + 0 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j is ext-real non negative ordinal natural V14() real integer set
k is set
{k} is non empty trivial set
{ b₁ where b₁ is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT : not j <= b₁ } is set
i is ext-real non negative ordinal natural V14() real integer set
j is ext-real non negative ordinal natural V14() real integer set
i is ext-real positive non negative non empty non trivial ordinal natural V14() real integer set
1 + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real positive non negative non empty ordinal natural V14() real integer set
i + 1 is ext-real positive non negative non empty ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i is ext-real positive non negative non empty non trivial ordinal natural V14() real integer set
i is ext-real non negative ordinal natural V14() real integer set
j is ext-real non negative ordinal natural V14() real integer set
i -' j is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
k is ext-real non negative ordinal natural V14() real integer set
(i -' j) -' k is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
j + k is ext-real non negative ordinal natural V14() real integer set
i -' (j + k) is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
0 -' k is ext-real non negative ordinal natural V14() real integer V35() V36() V37() V38() V39() V40() V57() Element of NAT
i - j is ext-real V14() real integer set
i - j is ext-real V14() real integer set
k + j is ext-real non negative ordinal natural V14() real integer set
(i - j) - k is ext-real V14() real integer set
i - (j + k) is ext-real V14() real integer set
i - j is ext-real V14() real integer set