:: PYTHTRIP semantic presentation

REAL is set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K32(REAL)
K32(REAL) is set
COMPLEX is set
NAT is non empty epsilon-transitive epsilon-connected ordinal set
K32(NAT) is set
K32(NAT) is set
RAT is set
INT is set
0 is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() ext-real non positive non negative integer finite finite-yielding V55() Element of NAT
1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer Element of NAT
{} is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() ext-real non positive non negative integer finite finite-yielding V55() set
T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
T gcd X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer prime set
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer prime Element of NAT
T is set
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
X ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
T ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T * T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
0 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
0 * 0 is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() ext-real non positive non negative integer finite finite-yielding V55() set
2 * (0 ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
1 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
1 * 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
2 * 0 is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() ext-real non positive non negative integer finite finite-yielding V55() even Element of NAT
(2 * 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even Element of NAT
the epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even () Element of NAT is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even () Element of NAT
the non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even () Element of NAT is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even () Element of NAT
T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () set
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () set
T * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m9 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
m9 * m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
n ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
n * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
n * m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(n * m9) ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
(n * m9) * (n * m9) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
c₆ is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
c₆ ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
c₆ * c₆ is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
n gcd X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
1 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
1 * 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
0 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
0 * 0 is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() ext-real non positive non negative integer finite finite-yielding V55() set
0 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
0 * 0 is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() ext-real non positive non negative integer finite finite-yielding V55() set
0 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
0 * 0 is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() ext-real non positive non negative integer finite finite-yielding V55() set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer prime Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
k1 * b is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k1 * k1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
k1 * c is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
c * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k1 * (c * X) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
b * b is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
k1 * (b * b) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k1 * (k1 * (b * b)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
c9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
k1 * c9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k1 * (m * X) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k1 * (k1 * (m * X)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
b ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
(k1 * k1) * m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m gcd X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
1 * m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
n ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
n * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
k1 * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(k1 * n) ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
(k1 * n) * (k1 * n) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
k1 * c is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n * c is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k1 * (n * c) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
b * b is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
k1 * (b * b) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k1 * (k1 * (b * b)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
c9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
k1 * c9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n * m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k1 * (n * m) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k1 * (k1 * (n * m)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
b ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
(k1 * k1) * m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n gcd m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
1 * m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
n ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
n * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
k1 * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(k1 * n) ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
(k1 * n) * (k1 * n) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
T is V24() V25() ext-real integer set
T ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T * T is V24() V25() ext-real integer set
T is V24() V25() ext-real integer even set
T ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T * T is V24() V25() ext-real integer even set
T is non empty V24() V25() ext-real integer non even set
T ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T * T is non empty V24() V25() ext-real integer non even set
T is V24() V25() ext-real integer set
T ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T * T is V24() V25() ext-real integer set
X is V24() V25() ext-real integer set
X ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X * X is V24() V25() ext-real integer set
4 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer Element of NAT
T is V24() V25() ext-real integer set
T ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T * T is V24() V25() ext-real integer set
(T ^2) mod 4 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X is V24() V25() ext-real integer set
2 * X is V24() V25() ext-real integer even set
X ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X * X is V24() V25() ext-real integer set
4 * (X ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(4 * (X ^2)) + 0 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
0 mod 4 is V24() V25() ext-real integer set
T is V24() V25() ext-real integer set
T ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T * T is V24() V25() ext-real integer set
(T ^2) mod 4 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X is V24() V25() ext-real integer set
2 * X is V24() V25() ext-real integer even set
(2 * X) + 1 is non empty V24() V25() ext-real integer non even set
X ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X * X is V24() V25() ext-real integer set
(X ^2) + X is V24() V25() ext-real integer set
4 * ((X ^2) + X) is V24() V25() ext-real integer set
(4 * ((X ^2) + X)) + 1 is V24() V25() ext-real integer set
1 mod 4 is V24() V25() ext-real integer set
T is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even () set
X is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even () set
T + X is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer even set
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
X ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
X * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
c₆ is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
c₆ ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
c₆ * c₆ is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n + m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(n + m9) mod 4 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n mod 4 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 mod 4 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(n mod 4) + (m9 mod 4) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
((n mod 4) + (m9 mod 4)) mod 4 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
1 + (m9 mod 4) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer Element of NAT
(1 + (m9 mod 4)) mod 4 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer Element of NAT
(1 + 1) mod 4 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
k ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
k * k is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
T * T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
X * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
- X is V24() V25() ext-real non positive integer set
- 0 is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() ext-real non positive non negative integer finite finite-yielding V55() set
- X is V24() V25() ext-real non positive integer set
T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
T * T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
X * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m9 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
m9 * m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
n * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m9 * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
X ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
X * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(m9 ^2) * (X ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(m9 ^2) * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer Element of NAT
c₆ is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer prime Element of NAT
k1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
k * k1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 * b is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(m9 * b) * k is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
k * c is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
k * k is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
c9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
c9 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
c9 * c9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(k ^2) * (c9 ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
b ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
b * b is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(b ^2) * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(k ^2) * ((b ^2) * X) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k * b is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
1 * b is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
b * m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 * m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 * T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
T * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(m9 * T) * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(m9 * T) * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 * (T * n) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T * m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(T * X) gcd (T * m9) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X gcd m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T * (X gcd m9) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
T * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
c₆ is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
k is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T * k is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T * c₆ is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T is set
X is Relation-like Function-like set
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X .: m9 is set
m9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer Element of NAT
X .: (m9 + 1) is set
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
succ m9 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer set
{m9} is non empty finite Element of K32(NAT)
m9 \/ {m9} is non empty set
Im (X,m9) is set
{m9} is non empty finite set
X .: {m9} is finite set
(X .: m9) \/ (Im (X,m9)) is set
dom X is set
X . m9 is set
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer Element of NAT
max (n,(X + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
c₆ is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
{X} is non empty finite Element of K32(NAT)
(X .: m9) \/ {X} is non empty set
dom X is set
X . m9 is set
c₆ is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
{(X . m9)} is non empty finite set
(X .: m9) \/ {(X . m9)} is non empty set
dom X is set
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(dom X) /\ {m9} is finite Element of K32(NAT)
X .: ((dom X) /\ {m9}) is finite set
X .: {} is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() ext-real non positive non negative integer finite finite-yielding V55() set
dom X is set
X . m9 is set
X .: 0 is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() ext-real non positive non negative integer finite finite-yielding V55() set
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X is Relation-like Function-like set
rng X is set
dom X is set
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X .: m9 is set
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
T * T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
X * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(T ^2) + (X ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
m9 * m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
n is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even Element of NAT
n ^2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even () Element of NAT
n * n is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even set
X is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even Element of NAT
X ^2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even () Element of NAT
X * X is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even set
(n ^2) + (X ^2) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer even () Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even Element of NAT
n ^2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even () Element of NAT
n * n is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even set
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
X ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even () Element of NAT
X * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even set
(n ^2) + (X ^2) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even Element of NAT
c₆ is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even Element of NAT
c₆ - n is V24() V25() ext-real integer even set
k is V24() V25() ext-real integer set
2 * k is V24() V25() ext-real integer even set
(T ^2) + 0 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
2 * 0 is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() ext-real non positive non negative integer finite finite-yielding V55() even Element of NAT
c₆ + n is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer even Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
2 * b is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
2 * c is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
k1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
b * k1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 + T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(m9 + T) / 2 is V24() V25() ext-real non negative set
m9 - T is V24() V25() ext-real integer set
(m9 - T) / 2 is V24() V25() ext-real set
((m9 + T) / 2) * ((m9 - T) / 2) is V24() V25() ext-real set
X / 2 is V24() V25() ext-real non negative set
(X / 2) ^2 is set
(X / 2) * (X / 2) is V24() V25() ext-real non negative set
c ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
c * c is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
b + k1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
c9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer prime set
m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer prime Element of NAT
m9 * m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
- k1 is V24() V25() ext-real non positive integer set
b + (- k1) is V24() V25() ext-real integer set
T * T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
- (T * T) is V24() V25() ext-real non positive integer set
X * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(m9 * m9) + (- (T * T)) is V24() V25() ext-real integer set
c9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
c9 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
c9 * c9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
m * m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
n * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
2 * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
c₁₄ is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
c₁₄ ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
c₁₄ * c₁₄ is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(c₁₄ ^2) - (n ^2) is V24() V25() ext-real integer set
(2 * n) * c₁₄ is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(c₁₄ ^2) + (n ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
b - k1 is V24() V25() ext-real integer set
2 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
2 * 2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even set
c₁₄ * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(c₁₄ * n) ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
(c₁₄ * n) * (c₁₄ * n) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(2 ^2) * ((c₁₄ * n) ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
((2 * n) * c₁₄) ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even () Element of NAT
((2 * n) * c₁₄) * ((2 * n) * c₁₄) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even set
T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
X * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
m9 * m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(X ^2) - (m9 ^2) is V24() V25() ext-real integer set
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
2 * m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(2 * m9) * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(X ^2) + (m9 ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
T * T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
n ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
n * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(T ^2) + (n ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
X * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
{0,0,0} is finite Element of K32(NAT)
0 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
0 * 0 is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() ext-real non positive non negative integer finite finite-yielding V55() set
(0 ^2) + (0 ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T is ()
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
X * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
m9 * m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(X ^2) + (m9 ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
n * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
{X,m9,n} is finite Element of K32(NAT)
T is Element of K32(NAT)
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
X * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
m9 * m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(X ^2) + (m9 ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
n * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
{X,m9,n} is finite Element of K32(NAT)
X gcd m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
0 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
0 * 0 is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() ext-real non positive non negative integer finite finite-yielding V55() set
2 * 0 is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() ext-real non positive non negative integer finite finite-yielding V55() even Element of NAT
(0 ^2) - (0 ^2) is V24() V25() ext-real integer set
0 * ((0 ^2) - (0 ^2)) is V24() V25() ext-real integer set
(2 * 0) * 0 is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() ext-real non positive non negative integer finite finite-yielding V55() even Element of NAT
0 * ((2 * 0) * 0) is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() ext-real non positive non negative integer finite finite-yielding V55() even Element of NAT
(0 ^2) + (0 ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
0 * ((0 ^2) + (0 ^2)) is empty Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V24() V25() ext-real non positive non negative integer finite finite-yielding V55() Element of NAT
{(0 * ((0 ^2) - (0 ^2))),(0 * ((2 * 0) * 0)),(0 * ((0 ^2) + (0 ^2)))} is finite set
(X gcd m9) * (X gcd m9) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
c₆ is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(X gcd m9) * c₆ is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(X gcd m9) * k is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k1 gcd b is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(X gcd m9) * (k1 gcd b) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(X gcd m9) * 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(X gcd m9) ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
(X gcd m9) * (X gcd m9) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
k1 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
k1 * k1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
b ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
b * b is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(k1 ^2) + (b ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
((X gcd m9) ^2) * ((k1 ^2) + (b ^2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
c is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(X gcd m9) * c is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
c9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
c9 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
c9 * c9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
((X gcd m9) ^2) * (c9 ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
n * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
m * m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(n ^2) - (m ^2) is V24() V25() ext-real integer set
2 * m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(2 * m) * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(n ^2) + (m ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(X gcd m9) * ((n ^2) - (m ^2)) is V24() V25() ext-real integer set
(X gcd m9) * ((2 * m) * n) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(X gcd m9) * ((n ^2) + (m ^2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
{((X gcd m9) * ((n ^2) - (m ^2))),((X gcd m9) * ((2 * m) * n)),((X gcd m9) * ((n ^2) + (m ^2)))} is finite set
m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
n * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
m * m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(n ^2) - (m ^2) is V24() V25() ext-real integer set
2 * m is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(2 * m) * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(n ^2) + (m ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(X gcd m9) * ((n ^2) - (m ^2)) is V24() V25() ext-real integer set
(X gcd m9) * ((2 * m) * n) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(X gcd m9) * ((n ^2) + (m ^2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
{((X gcd m9) * ((n ^2) - (m ^2))),((X gcd m9) * ((2 * m) * n)),((X gcd m9) * ((n ^2) + (m ^2)))} is finite set
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
n * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m9 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
m9 * m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(n ^2) - (m9 ^2) is V24() V25() ext-real integer set
X * ((n ^2) - (m9 ^2)) is V24() V25() ext-real integer set
2 * m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(2 * m9) * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
X * ((2 * m9) * n) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(n ^2) + (m9 ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X * ((n ^2) + (m9 ^2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
{(X * ((n ^2) - (m9 ^2))),(X * ((2 * m9) * n)),(X * ((n ^2) + (m9 ^2)))} is finite set
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
n * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m9 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
m9 * m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(n ^2) - (m9 ^2) is V24() V25() ext-real integer set
X * ((n ^2) - (m9 ^2)) is V24() V25() ext-real integer set
2 * m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(2 * m9) * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
X * ((2 * m9) * n) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(n ^2) + (m9 ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X * ((n ^2) + (m9 ^2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
{(X * ((n ^2) - (m9 ^2))),(X * ((2 * m9) * n)),(X * ((n ^2) + (m9 ^2)))} is finite set
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(X * X) ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
(X * X) * (X * X) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(X * ((2 * m9) * n)) ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even () Element of NAT
(X * ((2 * m9) * n)) * (X * ((2 * m9) * n)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even set
((X * X) ^2) + ((X * ((2 * m9) * n)) ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(X * ((n ^2) + (m9 ^2))) ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
(X * ((n ^2) + (m9 ^2))) * (X * ((n ^2) + (m9 ^2))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
2 * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
X ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
X * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
1 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
1 * 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(X ^2) + (1 ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
1 * ((X ^2) + (1 ^2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
2 * 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(2 * 1) * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
1 * ((2 * 1) * X) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(X ^2) - (1 ^2) is V24() V25() ext-real integer set
1 * ((X ^2) - (1 ^2)) is V24() V25() ext-real integer set
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
{X,(1 * ((2 * 1) * X)),(1 * ((X ^2) + (1 ^2)))} is finite Element of K32(NAT)
c₆ is finite ()
X is V24() V25() ext-real integer set
2 * X is V24() V25() ext-real integer even set
(2 * X) + 1 is non empty V24() V25() ext-real integer non even set
2 * 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer Element of NAT
(m9 + 1) ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
(m9 + 1) * (m9 + 1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m9 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
m9 * m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
((m9 + 1) ^2) - (m9 ^2) is V24() V25() ext-real integer set
1 * (((m9 + 1) ^2) - (m9 ^2)) is V24() V25() ext-real integer set
2 * m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(2 * m9) * (m9 + 1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
1 * ((2 * m9) * (m9 + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
((m9 + 1) ^2) + (m9 ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
1 * (((m9 + 1) ^2) + (m9 ^2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
{n,(1 * ((2 * m9) * (m9 + 1))),(1 * (((m9 + 1) ^2) + (m9 ^2)))} is finite Element of K32(NAT)
k is finite ()
(2 * m9) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even Element of NAT
(m9 ^2) + (2 * m9) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
((m9 ^2) + (2 * m9)) + (m9 ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(((m9 ^2) + (2 * m9)) + (m9 ^2)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer Element of NAT
T is finite ()
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
X * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
m9 * m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(X ^2) + (m9 ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
n * n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
{X,m9,n} is finite Element of K32(NAT)
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
c₆ is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
k1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
k1 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
k1 * k1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
X ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
X * X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
c₆ ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
c₆ * c₆ is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
k ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
k * k is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
b is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X gcd m9 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
4 * T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
2 * 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
2 * T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(2 * 1) * (2 * T) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
1 * ((2 * 1) * (2 * T)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(2 * T) ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even () Element of NAT
(2 * T) * (2 * T) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even set
1 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
1 * 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
((2 * T) ^2) + (1 ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
1 * (((2 * T) ^2) + (1 ^2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer Element of NAT
T + T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
((2 * T) ^2) - (1 ^2) is V24() V25() ext-real integer set
1 * (((2 * T) ^2) - (1 ^2)) is V24() V25() ext-real integer set
n is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
{n,(1 * ((2 * 1) * (2 * T))),(1 * (((2 * T) ^2) + (1 ^2)))} is finite Element of K32(NAT)
X is finite ()
n - (1 * (((2 * T) ^2) + (1 ^2))) is V24() V25() ext-real integer set
- 2 is V24() V25() ext-real non positive integer set
n gcd (1 * (((2 * T) ^2) + (1 ^2))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(1 * (((2 * T) ^2) + (1 ^2))) gcd (- 2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
abs (1 * (((2 * T) ^2) + (1 ^2))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
abs (- 2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(abs (1 * (((2 * T) ^2) + (1 ^2)))) gcd (abs (- 2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
abs 2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(abs (1 * (((2 * T) ^2) + (1 ^2)))) gcd (abs 2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
T * T is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
2 * (T ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
2 * (2 * (T ^2)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even Element of NAT
(2 * (2 * (T ^2))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer non even Element of NAT
((2 * (2 * (T ^2))) + 1) gcd 2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
1 gcd 2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
4 * 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
T is finite ()
3 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer Element of NAT
{3,4,5} is finite Element of K32(NAT)
3 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
3 * 3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
4 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
4 * 4 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
(3 ^2) + (4 ^2) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
5 ^2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer () Element of NAT
5 * 5 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
3 gcd 4 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
4 - 3 is V24() V25() ext-real integer set
3 gcd (4 - 3) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer set
T is finite ()
{ b₁ where b₁ is () : ( b₁ is () & b₁ is () ) } is set
union { b₁ where b₁ is () : ( b₁ is () & b₁ is () ) } is set
X is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer Element of NAT
4 * (X + 1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
X is finite ()
(4 * (X + 1)) + 0 is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
1 * (X + 1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
3 * (X + 1) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(1 * (X + 1)) + (3 * (X + 1)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer Element of NAT
(X + 1) + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real positive non negative integer Element of NAT
X is set
m9 is finite ()