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