:: PEPIN semantic presentation

REAL is set
NAT is non empty V2() epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of K6(REAL)
K6(REAL) is V35() V37() V38() set
COMPLEX is set
omega is non empty V2() epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
K6(omega) is V2() V35() V37() V38() non finite set
K6(NAT) is V2() V35() V37() V38() non finite set
K163(NAT) is non empty V35() V37() V38() set
RAT is set
INT is set
K7(NAT,REAL) is set
K6(K7(NAT,REAL)) is V35() V37() V38() set
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is V35() V37() V38() set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is V35() V37() V38() set
K7(REAL,REAL) is set
K6(K7(REAL,REAL)) is V35() V37() V38() set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is V35() V37() V38() set
K7(RAT,RAT) is set
K6(K7(RAT,RAT)) is V35() V37() V38() set
K7(K7(RAT,RAT),RAT) is set
K6(K7(K7(RAT,RAT),RAT)) is V35() V37() V38() set
K7(INT,INT) is set
K6(K7(INT,INT)) is V35() V37() V38() set
K7(K7(INT,INT),INT) is set
K6(K7(K7(INT,INT),INT)) is V35() V37() V38() set
K7(NAT,NAT) is V2() non finite set
K7(K7(NAT,NAT),NAT) is V2() non finite set
K6(K7(K7(NAT,NAT),NAT)) is V2() V35() V37() V38() non finite set
K389() is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 to_power 3 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ 3 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
8 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 to_power 4 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ 4 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
16 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m * n) * r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((m * n) * r) + m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(((m * n) * r) + m) + n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
1 * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 * (m * n) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
0 + m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ (m + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ m)) |^ 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ m) * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ (2 |^ 0) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ 0) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r - 1 is V11() ext-real real integer set
1 - 1 is V11() ext-real real integer set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r -' 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(r + 1) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 - 1 is V11() ext-real real integer set
r - 1 is V11() ext-real real integer set
- 1 is V11() ext-real non positive real integer set
r + (- 1) is V11() ext-real real integer set
(r + (- 1)) + 1 is V11() ext-real real integer set
(r + 1) - 1 is V11() ext-real real integer set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r gcd (r + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r * 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 + (r * 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(1 + (r * 1)) gcd r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 gcd r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r gcd m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
i gcd m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
i * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(i * n) gcd (m * n) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r * n) * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is V11() ext-real real integer set
r ^2 is set
r * r is V11() ext-real real integer set
r is V11() ext-real real integer set
1 mod r is V11() ext-real real integer set
1 div r is V11() ext-real real integer set
1 / r is V11() ext-real real set
[\(1 / r)/] is V11() ext-real real integer set
0 * r is V11() ext-real real integer set
1 - (0 * r) is V11() ext-real real integer set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r * n) + 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m div r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m / r is V11() ext-real non negative real set
[\(m / r)/] is V11() ext-real real integer set
r * (m div r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m mod r) + (r * (m div r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n + (m div r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r * (n + (m div r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r - n is V11() ext-real real integer set
r div m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r / m is V11() ext-real non negative real set
[\(r / m)/] is V11() ext-real real integer set
m * (r div m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * (r div m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m * (r div m)) + n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n mod (r * m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r * m) * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((r * m) * n) + (n mod (r * m)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * (r * n) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m * (r * n)) + (n mod (r * m)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(n mod (r * m)) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
1 mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is V11() ext-real real integer set
m * r is V11() ext-real real integer set
(m * r) + 1 is V11() ext-real real integer set
((m * r) + 1) mod r is V11() ext-real real integer set
n is V11() ext-real real integer set
m * n is V11() ext-real real integer set
(m * n) + 1 is V11() ext-real real integer set
((m * n) + 1) mod n is V11() ext-real real integer set
((m * n) + 1) div n is V11() ext-real real integer set
((m * n) + 1) / n is V11() ext-real real set
[\(((m * n) + 1) / n)/] is V11() ext-real real integer set
(((m * n) + 1) div n) * n is V11() ext-real real integer set
((m * n) + 1) - ((((m * n) + 1) div n) * n) is V11() ext-real real integer set
(m * n) / n is V11() ext-real real set
1 / n is V11() ext-real real set
((m * n) / n) + (1 / n) is V11() ext-real real set
[\(((m * n) / n) + (1 / n))/] is V11() ext-real real integer set
[\(((m * n) / n) + (1 / n))/] * n is V11() ext-real real integer set
((m * n) + 1) - ([\(((m * n) / n) + (1 / n))/] * n) is V11() ext-real real integer set
m + (1 / n) is V11() ext-real real set
[\(m + (1 / n))/] is V11() ext-real real integer set
[\(m + (1 / n))/] * n is V11() ext-real real integer set
((m * n) + 1) - ([\(m + (1 / n))/] * n) is V11() ext-real real integer set
[\(1 / n)/] is V11() ext-real real integer set
m + [\(1 / n)/] is V11() ext-real real integer set
(m + [\(1 / n)/]) * n is V11() ext-real real integer set
((m * n) + 1) - ((m + [\(1 / n)/]) * n) is V11() ext-real real integer set
1 div n is V11() ext-real real integer set
(1 div n) * n is V11() ext-real real integer set
1 - ((1 div n) * n) is V11() ext-real real integer set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m * n) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r * m) + (n mod r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r * n) + ((m * n) mod r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m * n) - (1 * n) is V11() ext-real real integer set
n - m is V11() ext-real real integer set
r * (n - m) is V11() ext-real real integer set
m - 1 is V11() ext-real real integer set
n * (m - 1) is V11() ext-real real integer set
x is V11() ext-real real integer set
i is V11() ext-real real integer set
i - 1 is V11() ext-real real integer set
y is V11() ext-real real integer set
x * y is V11() ext-real real integer set
(x * y) + 1 is V11() ext-real real integer set
i mod x is V11() ext-real real integer set
1 mod x is V11() ext-real real integer set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ m) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r mod n) |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((r mod n) |^ m) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ m) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r mod n) |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((r mod n) |^ m) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r |^ (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ (m + 1)) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r mod n) |^ (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((r mod n) |^ (m + 1)) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ m) * (r |^ 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((r |^ m) * (r |^ 1)) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r |^ m) * r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((r |^ m) * r) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((r |^ m) mod n) * (r mod n) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((r |^ m) mod n) * (r mod n)) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((r mod n) |^ m) * (r mod n) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((r mod n) |^ m) * (r mod n)) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r mod n) |^ (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((r mod n) |^ (m + 1)) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ 0) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r mod n) |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((r mod n) |^ 0) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r * (2 |^ (m + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r * (2 |^ (m + 1))) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r * (2 |^ (m + 1))) / 2 is V11() ext-real non negative real set
[\((r * (2 |^ (m + 1))) / 2)/] is V11() ext-real real integer set
2 |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
r * (2 |^ m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(2 |^ m) * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
r * ((2 |^ m) * 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
(r * (2 |^ m)) * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r + m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(n |^ r) * (n |^ m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ 8 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
256 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
4 + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (4 + 4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
16 * 16 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r ^2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(r ^2) mod (r + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
1 - 1 is V11() ext-real real integer set
r - 1 is V11() ext-real real integer set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r + 1) * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(n + 1) mod (r + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n mod (r + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(n mod (r + 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
((n mod (r + 1)) + 1) mod (r + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(0 + 1) mod (r + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r ^2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n ^2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(n ^2) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m * m) + r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m * m) * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((m * m) * m) + (r * m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(((m * m) * m) + (r * m)) + (m * r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * ((((m * m) * m) + (r * m)) + (m * r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m * ((((m * m) * m) + (r * m)) + (m * r))) + (r ^2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r ^2) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
- 1 is V11() ext-real non positive real integer set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m ^2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m ^2) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m div r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m / r is V11() ext-real non negative real set
[\(m / r)/] is V11() ext-real real integer set
(m div r) * r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m - ((m div r) * r) is V11() ext-real real integer set
((m div r) * r) - 1 is V11() ext-real real integer set
((m div r) * r) - 2 is V11() ext-real real integer set
(((m div r) * r) - 2) * (m div r) is V11() ext-real real integer set
((((m div r) * r) - 2) * (m div r)) * r is V11() ext-real real integer set
(((((m div r) * r) - 2) * (m div r)) * r) + 1 is V11() ext-real real integer set
1 mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r mod 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
(2 * m) + 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 to_power r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(2 to_power r) mod 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r |^ (n + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ n) * r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
1 mod 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
m |^ (n + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m |^ n) * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r mod 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
(2 * m) + 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r ^2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r |^ (1 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ 1) * (r |^ 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * (r |^ 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r |^ (n + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ n) * (r |^ 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ n) * r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
1 * r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ r)) ^2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ r)) * (2 |^ (2 |^ r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (r + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ (2 |^ (r + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ (2 |^ (0 + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 to_power 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 ^2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ m)) ^2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ m)) * (2 |^ (2 |^ m)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ (2 |^ (m + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ (m + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ (m + 1))) ^2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ (m + 1))) * (2 |^ (2 |^ (m + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ ((m + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ (2 |^ ((m + 1) + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ (2 |^ (m + 1))) ^2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ (m + 1))) * (2 |^ (2 |^ (m + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(2 |^ m) * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
2 |^ ((2 |^ m) * 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ ((2 |^ m) * 2)) ^2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ ((2 |^ m) * 2)) * (2 |^ ((2 |^ m) * 2)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(2 |^ (2 |^ m)) |^ 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
((2 |^ (2 |^ m)) |^ 2) ^2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
((2 |^ (2 |^ m)) |^ 2) * ((2 |^ (2 |^ m)) |^ 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((2 |^ (2 |^ m)) ^2) ^2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
((2 |^ (2 |^ m)) ^2) * ((2 |^ (2 |^ m)) ^2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(2 |^ (2 |^ (m + 1))) |^ 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ (m + 1)) * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
2 |^ ((2 |^ (m + 1)) * 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ ((m + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ (2 |^ ((m + 1) + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ 0) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ 0)) ^2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ 0)) * (2 |^ (2 |^ 0)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ (2 |^ (0 + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ (m -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * (r |^ (m -' 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ (n -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * (r |^ (n -' 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r |^ (n + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(n + 1) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ ((n + 1) -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * (r |^ ((n + 1) -' 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(0 + 1) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ ((0 + 1) -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * (r |^ ((0 + 1) -' 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * (r |^ 0) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r |^ n) * r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(n -' 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r |^ ((n -' 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ ((n -' 1) + 1)) * r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
0 -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ (0 -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * (r |^ (0 -' 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m mod 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m / 2 is V11() ext-real non negative real set
[\(m / 2)/] is V11() ext-real real integer set
r |^ (m div 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ (m div 2)) ^2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ (m div 2)) * (r |^ (m div 2)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m div 2) + (m div 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ ((m div 2) + (m div 2)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m + m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m + m) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m + m) / 2 is V11() ext-real non negative real set
[\((m + m) / 2)/] is V11() ext-real real integer set
r |^ ((m + m) div 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
(2 * m) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 * m) / 2 is V11() ext-real non negative real set
[\((2 * m) / 2)/] is V11() ext-real real integer set
r |^ ((2 * m) div 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ m) div r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r |^ m) / r is V11() ext-real non negative real set
[\((r |^ m) / r)/] is V11() ext-real real integer set
m -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ (m -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
1 - 1 is V11() ext-real real integer set
m - 1 is V11() ext-real real integer set
(m - 1) + 1 is V11() ext-real real integer set
(m -' 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r * (r |^ (m -' 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (r + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ r) + (2 |^ r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ m) + (2 |^ m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ ((m + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (m + 1)) + (2 |^ (m + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(2 |^ (m + 1)) + (2 |^ (m + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 * (2 |^ m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
(2 * (2 |^ m)) + (2 |^ (m + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 * (2 |^ m)) + (2 * (2 |^ m)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
2 * ((2 |^ m) + (2 |^ m)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
(m + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ ((m + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(2 |^ 0) + (2 |^ 0) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ 0) + (2 |^ 0) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r to_power n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r to_power m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m + m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m + m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m + m) - m is V11() ext-real real integer set
m - m is V11() ext-real real integer set
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(m + 1) - 1 is V11() ext-real real integer set
1 - 1 is V11() ext-real real integer set
1 |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
n |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(n |^ m) * (n |^ m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ m) div (2 |^ r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ m) / (2 |^ r) is V11() ext-real non negative real set
[\((2 |^ m) / (2 |^ r))/] is V11() ext-real real integer set
(2 |^ r) * ((2 |^ m) div (2 |^ r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r |^ (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * (r |^ m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * (m * i) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r * (m * i)) div r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r * (m * i)) / r is V11() ext-real non negative real set
[\((r * (m * i)) / r)/] is V11() ext-real real integer set
x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r * x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r * i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r |^ (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r * m) * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r * (r |^ m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r * (m * n) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r * (m * n)) div r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r * (m * n)) / r is V11() ext-real non negative real set
[\((r * (m * n)) / r)/] is V11() ext-real real integer set
i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r * i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n * i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r |^ m) * r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r |^ (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m |^ n) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m |^ m) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
m |^ (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m |^ (m + 1)) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m |^ m) * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((m |^ m) * m) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((m |^ m) mod r) * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((m |^ m) mod r) * m) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m |^ 0) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m |^ r) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m |^ n) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
m |^ (n + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m |^ (n + 1)) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n * (n |^ m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(n * (n |^ m)) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(n mod n) * (n |^ m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((n mod n) * (n |^ m)) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
0 * (n |^ m) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(0 * (n |^ m)) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m |^ 0) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ (m -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ (m -' 1)) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r gcd m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ m) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r |^ (m -' 1)) * r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((r |^ (m -' 1)) * r) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ n) div r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r |^ n) / r is V11() ext-real non negative real set
[\((r |^ n) / r)/] is V11() ext-real real integer set
1 - 1 is V11() ext-real real integer set
n - 1 is V11() ext-real real integer set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n + (- 1) is V11() ext-real real integer set
(n + (- 1)) + 1 is V11() ext-real real integer set
n -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(n -' 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r |^ (n -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is V11() ext-real real integer set
r ^2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * r is V11() ext-real real integer set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r - 1 is V11() ext-real real integer set
n is V11() ext-real real integer set
m * n is V11() ext-real real integer set
m is V11() ext-real real integer set
n is V11() ext-real real integer set
m mod n is V11() ext-real real integer set
n * n is V11() ext-real real integer set
(n * n) + 1 is V11() ext-real real integer set
((n * n) + 1) mod n is V11() ext-real real integer set
1 mod n is V11() ext-real real integer set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m * n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r - 1 is V11() ext-real real integer set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m - 1 is V11() ext-real real integer set
n is V11() ext-real real integer set
r * n is V11() ext-real real integer set
1 - 1 is V11() ext-real real integer set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r * m) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
1 mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is V11() ext-real real integer set
m is V11() ext-real real integer set
n is V11() ext-real real integer set
m is V11() ext-real real integer set
m - r is V11() ext-real real integer set
n is V11() ext-real real integer set
n * n is V11() ext-real real integer set
m - r is V11() ext-real real integer set
i is V11() ext-real real integer set
n * i is V11() ext-real real integer set
m - m is V11() ext-real real integer set
n - i is V11() ext-real real integer set
n * (n - i) is V11() ext-real real integer set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
3 mod 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 * 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
(2 * 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal non even Element of NAT
((2 * 1) + 1) mod 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 mod 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
Euler r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT : ( r,b₁ are_relative_prime & 1 <= b₁ & b₁ <= r ) } is set
finSeg r is finite Element of K163(NAT)
n is set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT : ( r,b₁ are_relative_prime & 1 <= b₁ & b₁ <= r ) } is epsilon-transitive epsilon-connected ordinal cardinal set
n is finite set
r gcd 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
- r is V11() ext-real non positive real integer set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r div r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r / r is V11() ext-real non negative real set
[\(r / r)/] is V11() ext-real real integer set
r * 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r * 1) div r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r * 1) / r is V11() ext-real non negative real set
[\((r * 1) / r)/] is V11() ext-real real integer set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m |^ r) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
Euler n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m * n) mod (Euler n) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
Euler r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
Euler m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(Euler r) * (Euler m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r - 1 is V11() ext-real real integer set
(r - 1) * (Euler m) is V11() ext-real real integer set
m - 1 is V11() ext-real real integer set
(r - 1) * (m - 1) is V11() ext-real real integer set
i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
i * x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m gcd (Euler n) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m,y,n) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(y |^ m) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(n,(m,y,n),n) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m,y,n) |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((m,y,n) |^ n) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y * i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(y * i) * x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((y * i) * x) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
y |^ (((y * i) * x) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(y |^ (((y * i) * x) + 1)) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y |^ ((y * i) * x) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 - 1 is V11() ext-real real integer set
(y |^ ((y * i) * x)) - 1 is V11() ext-real real integer set
a is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y * a is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y gcd r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y * x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y |^ (y * x) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(y |^ (y * x)) |^ (i + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((y |^ (y * x)) |^ (i + 1)) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(y |^ (y * x)) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(y |^ (y * x)) |^ i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((y |^ (y * x)) |^ i) * (y |^ (y * x)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((y |^ (y * x)) |^ i) * (y |^ (y * x))) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((y |^ (y * x)) |^ i) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(y * x) * i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y |^ ((y * x) * i) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(y |^ ((y * x) * i)) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(y |^ ((y * i) * x)) div r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(y |^ ((y * i) * x)) / r is V11() ext-real non negative real set
[\((y |^ ((y * i) * x)) / r)/] is V11() ext-real real integer set
r * ((y |^ ((y * i) * x)) div r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r * ((y |^ ((y * i) * x)) div r)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
y gcd r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y gcd r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y gcd m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y |^ (y * i) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(y |^ (y * i)) |^ (x + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((y |^ (y * i)) |^ (x + 1)) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(y |^ (y * i)) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(y |^ (y * i)) |^ x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((y |^ (y * i)) |^ x) * (y |^ (y * i)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((y |^ (y * i)) |^ x) * (y |^ (y * i))) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((y |^ (y * i)) |^ x) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(y |^ ((y * i) * x)) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(y |^ ((y * i) * x)) div m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(y |^ ((y * i) * x)) / m is V11() ext-real non negative real set
[\((y |^ ((y * i) * x)) / m)/] is V11() ext-real real integer set
m * ((y |^ ((y * i) * x)) div m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m * ((y |^ ((y * i) * x)) div m)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
y gcd m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y gcd m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r * m) * k is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
y * ((y |^ ((y * i) * x)) - 1) is V11() ext-real real integer set
y * (y |^ ((y * i) * x)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y * 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(y * (y |^ ((y * i) * x))) - (y * 1) is V11() ext-real real integer set
(y |^ (((y * i) * x) + 1)) - y is V11() ext-real real integer set
y - y is V11() ext-real real integer set
(y |^ (((y * i) * x) + 1)) - (y - y) is V11() ext-real real integer set
n * k is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(n * k) + y is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m * n) div (Euler n) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m * n) / (Euler n) is V11() ext-real non negative real set
[\((m * n) / (Euler n))/] is V11() ext-real real integer set
y is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(i * x) * y is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((i * x) * y) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
y * i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(y * i) * x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((y * i) * x) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
y |^ (m * n) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(y |^ (m * n)) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(y |^ m) |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((y |^ m) |^ n) mod n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT : ( not b₁ <= 0 & (r |^ b₁) mod m = 1 ) } is set
m is set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ n) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r gcd m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
Euler m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ (Euler m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ (Euler m)) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is non empty Element of K6(NAT)
the Element of m is Element of m
i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ i) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ x) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ x) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ y is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ y) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ n) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ m) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(1,r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r gcd 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(1 |^ 1) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m,r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m |^ n) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m |^ (m,r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m |^ (m,r)) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n mod (m,r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m,r) * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((m,r) * n) + (n mod (m,r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m,r) * i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m |^ ((m,r) * i) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m |^ (n mod (m,r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m |^ ((m,r) * i)) * (m |^ (n mod (m,r))) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((m |^ ((m,r) * i)) * (m |^ (n mod (m,r)))) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m |^ (m,r)) |^ i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((m |^ (m,r)) |^ i) * (m |^ (n mod (m,r))) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(((m |^ (m,r)) |^ i) * (m |^ (n mod (m,r)))) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((m |^ (m,r)) |^ i) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((m |^ (m,r)) |^ i) mod r) * (m |^ (n mod (m,r))) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((((m |^ (m,r)) |^ i) mod r) * (m |^ (n mod (m,r)))) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 * (m |^ (n mod (m,r))) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(1 * (m |^ (n mod (m,r)))) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m,r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m |^ n) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m,r) * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m |^ (m,r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m |^ (m,r)) |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((m |^ (m,r)) |^ n) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m |^ (m,r)) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((m |^ (m,r)) mod r) |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((m |^ (m,r)) mod r) |^ n) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(1 |^ n) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m,r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m |^ (r -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m |^ (r -' 1)) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ r)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(0) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ 0) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ 0)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (1 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ (1 + 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ 1) * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
((2 |^ 1) * 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal non even Element of NAT
2 * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
(2 * 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal non even Element of NAT
(2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ 2)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
17 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (1 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ (2 |^ (1 + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ (2 |^ (1 + 1))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ 1) * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
2 |^ ((2 |^ 1) * 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ ((2 |^ 1) * 2)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
2 |^ (2 * 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ (2 * 2)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (3 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ (3 + 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (2 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ (2 + 1)) * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
((2 |^ (2 + 1)) * 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal non even Element of NAT
(2 |^ (1 + 1)) * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
((2 |^ (1 + 1)) * 2) * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
(((2 |^ (1 + 1)) * 2) * 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal non even Element of NAT
((2 |^ 1) * 2) * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
(((2 |^ 1) * 2) * 2) * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
((((2 |^ 1) * 2) * 2) * 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal non even Element of NAT
(2 * 2) * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
((2 * 2) * 2) * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
(((2 * 2) * 2) * 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal non even Element of NAT
(3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ 3 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ 3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ 3)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
257 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
4 + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (4 + 4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ (4 + 4)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ 4 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ 4) * (2 |^ 4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((2 |^ 4) * (2 |^ 4)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ 4 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ 4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ 4)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
256 * 256 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(256 * 256) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
8 + 8 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (8 + 8) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ (8 + 8)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(2 |^ 8) * (2 |^ 8) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((2 |^ 8) * (2 |^ 8)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ 4 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ 4) * (2 |^ 4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
4 + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (4 + 4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((2 |^ 4) * (2 |^ 4)) * (2 |^ (4 + 4)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((2 |^ 4) * (2 |^ 4)) * (2 |^ (4 + 4))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ r)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ r)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ r)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(r) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((r) -' 1) mod 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 mod 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ r)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(r) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r) - 1 is V11() ext-real real integer set
1 - 1 is V11() ext-real real integer set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ r)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(r) mod (2 |^ (2 |^ r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ (2 |^ r)) * 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((2 |^ (2 |^ r)) * 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(((2 |^ (2 |^ r)) * 1) + 1) mod (2 |^ (2 |^ r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 mod (2 |^ (2 |^ r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ r)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(r) - 1 is V11() ext-real real integer set
(r) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((r) -' 1) mod 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ m)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m) div r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m) / r is V11() ext-real non negative real set
[\((m) / r)/] is V11() ext-real real integer set
r * ((m) div r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r * ((m) div r)) - 0 is V11() ext-real non negative real integer set
(r * ((m) div r)) + (- 1) is V11() ext-real real integer set
0 + (- 1) is V11() ext-real non positive real integer set
(2 |^ (2 |^ m)) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 - (- 1) is non empty V11() ext-real positive non negative real integer set
(2,r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ (2 |^ m)) * (2 |^ (2 |^ m)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
1 * (2 |^ (2 |^ m)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((2 |^ (2 |^ m))) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((- 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(- 1) * (- 1) is V11() ext-real non negative real integer set
((2 |^ (2 |^ m))) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ (2 |^ (m + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ (2 |^ (m + 1))) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ (m + 1)) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ (m + 1)) / 2 is V11() ext-real non negative real set
[\((2 |^ (m + 1)) / 2)/] is V11() ext-real real integer set
2 * (2 |^ m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
(2 * (2 |^ m)) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 * (2 |^ m)) / 2 is V11() ext-real non negative real set
[\((2 * (2 |^ m)) / 2)/] is V11() ext-real real integer set
r -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(2 |^ (m + 1)) * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r - 1 is V11() ext-real real integer set
1 - 1 is V11() ext-real real integer set
i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ (m + 1)) * i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
i * (2 |^ (m + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(i * (2 |^ (m + 1))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ r)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(r) gcd 3 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (r + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m * (2 |^ (r + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m * (2 |^ (r + 1))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(m * (2 |^ (r + 1))) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m * (2 |^ (r + 1))) / 2 is V11() ext-real non negative real set
[\((m * (2 |^ (r + 1))) / 2)/] is V11() ext-real real integer set
m * (2 |^ r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ r)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(r) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((r) -' 1) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((r) -' 1) / 2 is V11() ext-real non negative real set
[\(((r) -' 1) / 2)/] is V11() ext-real real integer set
3 |^ (((r) -' 1) div 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3,m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(r) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r) - 1 is V11() ext-real real integer set
((3 |^ (((r) -' 1) div 2))) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (((r) -' 1) div 2)) * (3 |^ (((r) -' 1) div 2)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((- 1)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(- 1) * (- 1) is V11() ext-real non negative real integer set
((r) -' 1) mod 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ ((r) -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 gcd i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 * 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 * i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 * 1) gcd (3 * i) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(3,m) * x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (((r) -' 1) div 2)) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 - (- 1) is non empty V11() ext-real positive non negative real integer set
(2 |^ (2 |^ r)) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ (2 |^ r)) / 2 is V11() ext-real non negative real set
[\((2 |^ (2 |^ r)) / 2)/] is V11() ext-real real integer set
(3 |^ ((r) -' 1)) mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m * i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m * i) mod (2 |^ (2 |^ r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m - 1 is V11() ext-real real integer set
1 - 1 is V11() ext-real real integer set
x * (3,m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
x * (2 |^ (2 |^ r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(x * (2 |^ (2 |^ r))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
m mod (2 |^ (2 |^ r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 mod (2 |^ (2 |^ r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 * i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(1 * i) mod (2 |^ (2 |^ r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(2 |^ (2 |^ r)) * y is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
((2 |^ (2 |^ r)) * y) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
0 * (2 |^ (2 |^ r)) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(0 * (2 |^ (2 |^ r))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
y * (2 |^ (2 |^ r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(y * (2 |^ (2 |^ r))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
((x * (2 |^ (2 |^ r))) + 1) * ((y * (2 |^ (2 |^ r))) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
x * y is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(x * y) * (2 |^ (2 |^ r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((x * y) * (2 |^ (2 |^ r))) + x is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((x * y) * (2 |^ (2 |^ r))) + x) + y is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ (2 |^ r)) * ((((x * y) * (2 |^ (2 |^ r))) + x) + y) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((2 |^ (2 |^ r)) * ((((x * y) * (2 |^ (2 |^ r))) + x) + y)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
((2 |^ (2 |^ r)) * ((((x * y) * (2 |^ (2 |^ r))) + x) + y)) div (2 |^ (2 |^ r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((2 |^ (2 |^ r)) * ((((x * y) * (2 |^ (2 |^ r))) + x) + y)) / (2 |^ (2 |^ r)) is V11() ext-real non negative real set
[\(((2 |^ (2 |^ r)) * ((((x * y) * (2 |^ (2 |^ r))) + x) + y)) / (2 |^ (2 |^ r)))/] is V11() ext-real real integer set
1 * (2 |^ (2 |^ r)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(1 * (2 |^ (2 |^ r))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
9 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (1 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 1) * (3 |^ 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 * (3 |^ 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 * 3 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ 4 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
81 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (2 + 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 2) * (3 |^ 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ 8 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
6561 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
4 + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (4 + 4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 4) * (3 |^ 4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ 16 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
6561 * 6561 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
8 + 8 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (8 + 8) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 8) * (3 |^ 8) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
4 * r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(4 * r) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ ((4 * r) + 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ ((4 * r) + 2)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
4 * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(4 * m) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ ((4 * m) + 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ ((4 * m) + 2)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
4 * (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(4 * (m + 1)) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ ((4 * (m + 1)) + 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ ((4 * (m + 1)) + 2)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(1) * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ (4 * m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (4 * m)) * (3 |^ 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
0 * (3 |^ 2) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
((1) * n) * 81 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 * 81 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((1) * n) * 81) / (1) is V11() ext-real non negative real set
(1 * 81) / (1) is V11() ext-real non negative real set
n * (1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(n * (1)) * 81 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(1) " is V11() ext-real non negative real set
((n * (1)) * 81) * ((1) ") is V11() ext-real non negative real set
n * 81 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(n * 81) * ((1) ") is V11() ext-real non negative real set
((n * 81) * ((1) ")) * (1) is V11() ext-real non negative real set
(n * 81) / (1) is V11() ext-real non negative real set
((n * 81) / (1)) * (1) is V11() ext-real non negative real set
81 / 5 is V11() ext-real non negative real set
- 16 is V11() ext-real non positive real integer set
(n * 81) + (- 16) is V11() ext-real real integer set
16 + (- 16) is V11() ext-real real integer set
((4 * m) + 2) + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (((4 * m) + 2) + 4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (((4 * m) + 2) + 4)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
((1) * n) - 1 is V11() ext-real real integer set
(((1) * n) - 1) * (3 |^ 4) is V11() ext-real real integer set
((((1) * n) - 1) * (3 |^ 4)) + 1 is V11() ext-real real integer set
(n * 81) - 16 is V11() ext-real real integer set
(1) * ((n * 81) - 16) is V11() ext-real real integer set
(n * 81) -' 16 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(1) * ((n * 81) -' 16) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
4 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(4 * 0) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ ((4 * 0) + 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ ((4 * 0) + 2)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
5 * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ (2 |^ r) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
(2 |^ (2 |^ r)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(r) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((r) -' 1) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((r) -' 1) / 2 is V11() ext-real non negative real set
[\(((r) -' 1) / 2)/] is V11() ext-real real integer set
3 |^ (((r) -' 1) div 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 - 1 is V11() ext-real real integer set
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
5 -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
5 - 1 is V11() ext-real real integer set
4 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 to_power 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (1 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2 |^ 1) * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
2 * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
2 to_power 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
4 div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
4 / 2 is V11() ext-real non negative real set
[\(4 / 2)/] is V11() ext-real real integer set
2 to_power (2 -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ (2 -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(1) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((1) -' 1) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((1) -' 1) / 2 is V11() ext-real non negative real set
[\(((1) -' 1) / 2)/] is V11() ext-real real integer set
4 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(4 * 0) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(3 |^ (((r) -' 1) div 2)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(3 |^ (((r) -' 1) div 2)) - (- 1) is V11() ext-real non negative real integer set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
16 * r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(16 * r) + 8 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ ((16 * r) + 8) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ ((16 * r) + 8)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
16 * m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(16 * m) + 8 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ ((16 * m) + 8) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ ((16 * m) + 8)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
16 * (m + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(16 * (m + 1)) + 8 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ ((16 * (m + 1)) + 8) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ ((16 * (m + 1)) + 8)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(2) * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ (16 * m) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (16 * m)) * (3 |^ 8) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
0 * (3 |^ 8) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
((2) * n) * 6561 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 * 6561 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((2) * n) * 6561) * 6561 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
6562 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
6560 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
6562 * 6560 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((((2) * n) * 6561) * 6561) / (2) is V11() ext-real non negative real set
6560 * 6562 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(6560 * 6562) / (2) is V11() ext-real non negative real set
n * 6561 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(n * 6561) * (2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((n * 6561) * (2)) * 6561 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2) " is V11() ext-real non negative real set
(((n * 6561) * (2)) * 6561) * ((2) ") is V11() ext-real non negative real set
(n * 6561) * 6561 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((n * 6561) * 6561) * ((2) ") is V11() ext-real non negative real set
(((n * 6561) * 6561) * ((2) ")) * (2) is V11() ext-real non negative real set
((n * 6561) * 6561) / (2) is V11() ext-real non negative real set
(((n * 6561) * 6561) / (2)) * (2) is V11() ext-real non negative real set
(6560 * 6562) / 17 is V11() ext-real non negative real set
386 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
386 * 6560 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((n * 6561) * 6561) - (386 * 6560) is V11() ext-real real integer set
(386 * 6560) - (386 * 6560) is V11() ext-real real integer set
((16 * m) + 8) + 16 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (((16 * m) + 8) + 16) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (((16 * m) + 8) + 16)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
((2) * n) - 1 is V11() ext-real real integer set
(((2) * n) - 1) * (3 |^ 16) is V11() ext-real real integer set
((((2) * n) - 1) * (3 |^ 16)) + 1 is V11() ext-real real integer set
(2) * (((n * 6561) * 6561) - (386 * 6560)) is V11() ext-real real integer set
((n * 6561) * 6561) -' (386 * 6560) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2) * (((n * 6561) * 6561) -' (386 * 6560)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
16 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(16 * 0) + 8 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ ((16 * 0) + 8) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ ((16 * 0) + 8)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
386 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
17 * 386 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 1) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
0 * 257 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(0 * 257) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 2) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
0 * 257 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(0 * 257) + 9 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (1 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (1 + 1)) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 1) * (3 |^ 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 1) * (3 |^ 1)) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 1) mod (3)) * ((3 |^ 1) mod (3)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((3 |^ 1) mod (3)) * ((3 |^ 1) mod (3))) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 4) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
0 * 257 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(0 * 257) + 81 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (2 + 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (2 + 2)) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 2) * (3 |^ 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 2) * (3 |^ 2)) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 2) mod (3)) * ((3 |^ 2) mod (3)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((3 |^ 2) mod (3)) * ((3 |^ 2) mod (3))) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 8) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
136 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
25 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
25 * 257 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(25 * 257) + 136 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
4 + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (4 + 4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (4 + 4)) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 4) * (3 |^ 4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 4) * (3 |^ 4)) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 4) mod (3)) * ((3 |^ 4) mod (3)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((3 |^ 4) mod (3)) * ((3 |^ 4) mod (3))) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 16) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
83 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
83 * 3 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
18496 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
71 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
71 * 257 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
249 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(71 * 257) + 249 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
8 + 8 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (8 + 8) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (8 + 8)) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 8) * (3 |^ 8) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 8) * (3 |^ 8)) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
136 * 136 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(136 * 136) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
32 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ 32 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 32) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
64 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(83 * 3) * 83 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((83 * 3) * 83) * 3 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
241 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
241 * 257 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(241 * 257) + 64 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
16 + 16 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (16 + 16) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (16 + 16)) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 16) * (3 |^ 16) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 16) * (3 |^ 16)) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(83 * 3) * (83 * 3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((83 * 3) * (83 * 3)) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ 64 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 64) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
241 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
4096 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
15 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
15 * 257 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(15 * 257) + 241 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
32 + 32 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (32 + 32) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (32 + 32)) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 32) * (3 |^ 32) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 32) * (3 |^ 32)) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
64 * 64 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(64 * 64) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
128 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ 128 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 128) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
241 * 241 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
225 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
225 * 257 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(225 * 257) + 256 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
64 + 64 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (64 + 64) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (64 + 64)) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 64) * (3 |^ 64) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 64) * (3 |^ 64)) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(241 * 241) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 1) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
0 * ((256 * 256) + 1) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(0 * ((256 * 256) + 1)) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 2) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
0 * ((256 * 256) + 1) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(0 * ((256 * 256) + 1)) + 9 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (1 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (1 + 1)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 1) * (3 |^ 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 1) * (3 |^ 1)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 * 3 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 * 3) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 4) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
0 * ((256 * 256) + 1) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(0 * ((256 * 256) + 1)) + 81 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (2 + 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (2 + 2)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 2) * (3 |^ 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 2) * (3 |^ 2)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
9 * 9 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(9 * 9) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 8) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
0 * ((256 * 256) + 1) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(0 * ((256 * 256) + 1)) + 6561 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
4 + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (4 + 4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (4 + 4)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 4) * (3 |^ 4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 4) * (3 |^ 4)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
81 * 81 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(81 * 81) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 16) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
164 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
332 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
164 * 332 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(164 * 332) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
656 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
656 * ((256 * 256) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(656 * ((256 * 256) + 1)) + ((164 * 332) + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
8 + 8 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (8 + 8) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (8 + 8)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 8) * (3 |^ 8) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 8) * (3 |^ 8)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(6561 * 6561) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 32) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
123 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
503 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
123 * 503 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((164 * 332) + 1) * ((164 * 332) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
263 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
172 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
263 * 172 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(263 * 172) * ((256 * 256) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((263 * 172) * ((256 * 256) + 1)) + (123 * 503) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
16 + 16 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (16 + 16) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (16 + 16)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 16) * (3 |^ 16) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 16) * (3 |^ 16)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((164 * 332) + 1) * ((164 * 332) + 1)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 64) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
14 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
1367 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
14 * 1367 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(14 * 1367) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(123 * 503) * (123 * 503) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
325 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
241 * 241 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
325 + (241 * 241) is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(325 + (241 * 241)) * ((256 * 256) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((325 + (241 * 241)) * ((256 * 256) + 1)) + ((14 * 1367) + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
32 + 32 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (32 + 32) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (32 + 32)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 32) * (3 |^ 32) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 32) * (3 |^ 32)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((123 * 503) * (123 * 503)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 128) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
52 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
289 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
52 * 289 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((14 * 1367) + 1) * ((14 * 1367) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
5589 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
5589 * ((256 * 256) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(5589 * ((256 * 256) + 1)) + (52 * 289) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
64 + 64 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (64 + 64) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (64 + 64)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 64) * (3 |^ 64) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 64) * (3 |^ 64)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((14 * 1367) + 1) * ((14 * 1367) + 1)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ 256 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 256) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
282 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(52 * 289) * (52 * 289) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3446 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3446 * ((256 * 256) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3446 * ((256 * 256) + 1)) + 282 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
128 + 128 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (128 + 128) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (128 + 128)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 128) * (3 |^ 128) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ 128) * (3 |^ 128)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((52 * 289) * (52 * 289)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
256 * 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
3 |^ (256 * 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (256 * 2)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
71 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
197 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
71 * 197 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
282 * 282 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1 * ((256 * 256) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(1 * ((256 * 256) + 1)) + (71 * 197) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ 256) * (3 |^ 256) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
256 + 256 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (256 + 256) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
512 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ 512 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(282 * 282) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
256 * 4 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ (256 * 4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (256 * 4)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
32 * 257 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(71 * 197) * (71 * 197) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2985 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2985 * ((256 * 256) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(2985 * ((256 * 256) + 1)) + (32 * 257) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (256 * 2)) * (3 |^ (256 * 2)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(256 * 2) + (256 * 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal even Element of NAT
3 |^ ((256 * 2) + (256 * 2)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1024 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ 1024 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((71 * 197) * (71 * 197)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
256 * 8 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ (256 * 8) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (256 * 8)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
809 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
81 * 809 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(32 * 257) * (32 * 257) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
1031 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
1031 * ((256 * 256) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(1031 * ((256 * 256) + 1)) + (81 * 809) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (256 * 4)) * (3 |^ (256 * 4)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(256 * 4) + (256 * 4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ ((256 * 4) + (256 * 4)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2048 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ 2048 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((32 * 257) * (32 * 257)) mod ((256 * 256) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
256 * 16 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ (256 * 16) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (256 * 16)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(81 * 809) * (81 * 809) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
255 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
256 * 255 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(256 * 255) + 241 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
((256 * 255) + 241) * ((256 * 256) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((256 * 255) + 241) * ((256 * 256) + 1)) + 64 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(3 |^ (256 * 8)) * (3 |^ (256 * 8)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(256 * 8) + (256 * 8) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ ((256 * 8) + (256 * 8)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
4096 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ 4096 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((81 * 809) * (81 * 809)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
256 * 32 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ (256 * 32) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (256 * 32)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
64 * 64 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
0 * ((256 * 256) + 1) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(0 * ((256 * 256) + 1)) + (256 * 16) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (256 * 16)) * (3 |^ (256 * 16)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(256 * 16) + (256 * 16) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ ((256 * 16) + (256 * 16)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
8192 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ 8192 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(64 * 64) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
256 * 64 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ (256 * 64) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (256 * 64)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
673 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
97 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
673 * 97 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(256 * 16) * (256 * 16) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
255 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
255 * ((256 * 256) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(255 * ((256 * 256) + 1)) + (673 * 97) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (256 * 32)) * (3 |^ (256 * 32)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(256 * 32) + (256 * 32) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ ((256 * 32) + (256 * 32)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
32 + 32 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
256 * (32 + 32) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ (256 * (32 + 32)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((256 * 16) * (256 * 16)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
256 * 128 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ (256 * 128) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (256 * 128)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
255 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
255 * 256 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(255 * 256) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
((255 * 256) + 1) * ((255 * 256) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
255 * 255 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(255 * 255) * ((256 * 256) + 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((255 * 255) * ((256 * 256) + 1)) + (256 * 256) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (256 * 64)) * (3 |^ (256 * 64)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(256 * 64) + (256 * 64) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ ((256 * 64) + (256 * 64)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
64 + 64 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
256 * (64 + 64) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ (256 * (64 + 64)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(673 * 97) * (673 * 97) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((673 * 97) * (673 * 97)) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
32 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(32 * 0) + 128 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ ((32 * 0) + 128) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ ((32 * 0) + 128)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
257 * 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(257 * 1) + 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
257 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(257 * 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
1 mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ ((32 * 0) + 128)) + 1) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
256 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(256 + 1) mod (3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
64 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(64 * 0) + (256 * 128) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
3 |^ ((64 * 0) + (256 * 128)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ ((64 * 0) + (256 * 128))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
((256 * 256) + 1) * 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(((256 * 256) + 1) * 1) + 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((256 * 256) + 1) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((256 * 256) + 1) * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(((256 * 256) + 1) * 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
1 mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3 |^ ((64 * 0) + (256 * 128))) + 1) mod (4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(1) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((1) -' 1) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((1) -' 1) / 2 is V11() ext-real non negative real set
[\(((1) -' 1) / 2)/] is V11() ext-real real integer set
3 |^ (((1) -' 1) div 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
4 -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
4 - 1 is V11() ext-real real integer set
3 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
17 -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
17 - 1 is V11() ext-real real integer set
16 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 to_power 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
16 div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
16 / 2 is V11() ext-real non negative real set
[\(16 / 2)/] is V11() ext-real real integer set
2 to_power (4 -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ (4 -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(2) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((2) -' 1) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((2) -' 1) / 2 is V11() ext-real non negative real set
[\(((2) -' 1) / 2)/] is V11() ext-real real integer set
16 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real non positive non negative real integer finite V43() cardinal {} -element Element of NAT
(16 * 0) + 8 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
3 |^ (((2) -' 1) div 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (((2) -' 1) div 2)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
(3 |^ (((2) -' 1) div 2)) - (- 1) is V11() ext-real non negative real integer set
2 to_power 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
8 -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
8 - 1 is V11() ext-real real integer set
7 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
7 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
257 -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
257 - 1 is V11() ext-real real integer set
256 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 to_power 8 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ 8 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
4 + 4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (4 + 4) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
16 * 16 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
256 div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
256 / 2 is V11() ext-real non negative real set
[\(256 / 2)/] is V11() ext-real real integer set
2 to_power (8 -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ (8 -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
4 + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (4 + 3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
16 * 8 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3) -' 1) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((3) -' 1) / 2 is V11() ext-real non negative real set
[\(((3) -' 1) / 2)/] is V11() ext-real real integer set
3 |^ (((3) -' 1) div 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (((3) -' 1) div 2)) - (- 1) is V11() ext-real non negative real integer set
2 to_power 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
16 -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
16 - 1 is V11() ext-real real integer set
15 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
15 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
((256 * 256) + 1) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((256 * 256) + 1) - 1 is V11() ext-real real integer set
(256 * 256) + 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
2 to_power 16 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of REAL
2 |^ 16 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
8 + 8 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (8 + 8) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(256 * 256) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(256 * 256) / 2 is V11() ext-real non negative real set
[\((256 * 256) / 2)/] is V11() ext-real real integer set
2 to_power (16 -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
2 |^ (16 -' 1) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
7 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
8 + 7 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (8 + 7) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
4 + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
2 |^ (4 + 3) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
256 * (2 |^ (4 + 3)) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
16 * 8 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
256 * (16 * 8) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(4) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((4) -' 1) div 2 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
((4) -' 1) / 2 is V11() ext-real non negative real set
[\(((4) -' 1) / 2)/] is V11() ext-real real integer set
3 |^ (((4) -' 1) div 2) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(3 |^ (((4) -' 1) div 2)) - (- 1) is V11() ext-real non negative real integer set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r mod m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r div m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r / m is V11() ext-real non negative real set
[\(r / m)/] is V11() ext-real real integer set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
m * n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(m * n) + 0 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
(r |^ m) div r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(r |^ m) / r is V11() ext-real non negative real set
[\((r |^ m) / r)/] is V11() ext-real real integer set
(r |^ m) mod r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r is V11() ext-real real set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ m is V11() ext-real real set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ n is V11() ext-real real set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real positive non negative real integer finite cardinal Element of NAT
r |^ (n + 1) is V11() ext-real real set
(r |^ n) * r is V11() ext-real real set
1 * r is V11() ext-real real set
r |^ 0 is V11() ext-real real set
r is V11() ext-real real set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal set
r |^ m is V11() ext-real real set
r |^ n is V11() ext-real real set
m is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
m -' n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
(m -' n) + n is epsilon-transitive epsilon-connected ordinal natural V11() ext-real non negative real integer finite cardinal Element of NAT
r |^ m is V11() ext-real real set
r |^ (m -' n) is V11() ext-real real set
r |^ n is V11() ext-real real set
(r |^ (m -' n)) * (r |^ n) is V11() ext-real real set