:: INT_4 semantic presentation

REAL is non empty V2() non finite complex-membered ext-real-membered real-membered V87() set
NAT is non empty V2() epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() Element of K6(REAL)
K6(REAL) is V2() non finite set
COMPLEX is non empty V2() non finite complex-membered V87() set
RAT is non empty V2() non finite complex-membered ext-real-membered real-membered rational-membered V87() set
INT is non empty V2() non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V87() set
K7(COMPLEX,COMPLEX) is V2() Relation-like non finite V71() set
K6(K7(COMPLEX,COMPLEX)) is V2() non finite set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V2() Relation-like non finite V71() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is V2() non finite set
K7(REAL,REAL) is V2() Relation-like non finite V71() V72() V73() set
K6(K7(REAL,REAL)) is V2() non finite set
K7(K7(REAL,REAL),REAL) is V2() Relation-like non finite V71() V72() V73() set
K6(K7(K7(REAL,REAL),REAL)) is V2() non finite set
K7(RAT,RAT) is V2() Relation-like RAT -valued non finite V71() V72() V73() set
K6(K7(RAT,RAT)) is V2() non finite set
K7(K7(RAT,RAT),RAT) is V2() Relation-like RAT -valued non finite V71() V72() V73() set
K6(K7(K7(RAT,RAT),RAT)) is V2() non finite set
K7(INT,INT) is V2() Relation-like RAT -valued INT -valued non finite V71() V72() V73() set
K6(K7(INT,INT)) is V2() non finite set
K7(K7(INT,INT),INT) is V2() Relation-like RAT -valued INT -valued non finite V71() V72() V73() set
K6(K7(K7(INT,INT),INT)) is V2() non finite set
K7(NAT,NAT) is V2() Relation-like RAT -valued INT -valued non finite V71() V72() V73() V74() set
K7(K7(NAT,NAT),NAT) is V2() Relation-like RAT -valued INT -valued non finite V71() V72() V73() V74() set
K6(K7(K7(NAT,NAT),NAT)) is V2() non finite set
NAT is non empty V2() epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() set
K6(NAT) is V2() non finite set
K6(NAT) is V2() non finite set
K251() is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() set
{{},1} is finite set
K446() is set
K6(K446()) is set
K447() is Element of K6(K446())
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
K6(K7(NAT,NAT)) is V2() non finite set
K7(NAT,REAL) is V2() Relation-like non finite V71() V72() V73() set
K6(K7(NAT,REAL)) is V2() non finite set
K242(1,NAT) is M8( NAT )
SetPrimes is non empty V2() non finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
ExtREAL is non empty ext-real-membered set
3 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
card {} is epsilon-transitive epsilon-connected ordinal cardinal set
Seg 1 is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty V2() finite V38() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
Seg 2 is non empty finite 2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{1,2} is finite V38() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
<*> REAL is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional integer finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() V77() V78() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() FinSequence of REAL
Sum (<*> REAL) is complex real ext-real Element of REAL
Product (<*> REAL) is complex real ext-real Element of REAL
m is complex-membered ext-real-membered real-membered set
a is complex real ext-real set
a ++ m is complex-membered ext-real-membered real-membered Element of K6(REAL)
X is Relation-like Function-like set
dom X is set
rng X is set
x is set
y is set
X . y is set
y1 is complex real ext-real set
x1 is complex real ext-real Element of REAL
a + x1 is complex real ext-real Element of REAL
u9 is complex real ext-real Element of REAL
x is set
y is complex real ext-real Element of REAL
y1 is complex Element of COMPLEX
a + y1 is set
x1 is complex real ext-real Element of REAL
X . x1 is set
x is set
y is set
X . x is set
X . y is set
y1 is complex real ext-real Element of REAL
X . y1 is set
a + y1 is complex real ext-real Element of REAL
x1 is complex real ext-real Element of REAL
a + x1 is complex real ext-real Element of REAL
m is finite complex-membered ext-real-membered real-membered set
a is complex real ext-real set
a ++ m is complex-membered ext-real-membered real-membered Element of K6(REAL)
m is complex-membered ext-real-membered real-membered set
card m is epsilon-transitive epsilon-connected ordinal cardinal set
a is complex real ext-real set
a ++ m is complex-membered ext-real-membered real-membered Element of K6(REAL)
card (a ++ m) is epsilon-transitive epsilon-connected ordinal cardinal set
K6(INT) is V2() non finite set
m is complex real integer ext-real set
a is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
m ++ a is complex-membered ext-real-membered real-membered Element of K6(REAL)
X is set
x is complex real ext-real Element of REAL
y is complex Element of COMPLEX
m + y is set
y1 is complex real integer ext-real set
m + y1 is complex real integer ext-real set
m is complex real integer ext-real set
a is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
m ** a is complex-membered ext-real-membered real-membered Element of K6(REAL)
X is set
x is complex real ext-real Element of REAL
y is complex Element of COMPLEX
m * y is set
y1 is complex real integer ext-real set
m * y1 is complex real integer ext-real set
m is complex real integer ext-real set
a is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
X is complex real integer ext-real set
X ** a is complex-membered ext-real-membered real-membered Element of K6(REAL)
x is complex Element of COMPLEX
X * x is set
y is complex real integer ext-real set
y1 is complex real integer ext-real set
X * y1 is complex real integer ext-real set
x is complex real integer ext-real set
X * x is complex real integer ext-real set
y is complex real ext-real Element of REAL
y1 is complex real ext-real Element of REAL
X * y1 is complex real ext-real Element of REAL
x1 is complex real ext-real Element of REAL
X * x1 is complex real ext-real Element of REAL
m is complex-membered ext-real-membered real-membered set
a is complex real ext-real set
a ** m is complex-membered ext-real-membered real-membered Element of K6(REAL)
X is Relation-like Function-like set
dom X is set
x is set
y is set
X . x is set
X . y is set
y1 is complex real ext-real Element of REAL
X . y1 is set
a * y1 is complex real ext-real Element of REAL
x1 is complex real ext-real Element of REAL
X . x1 is set
a * x1 is complex real ext-real Element of REAL
rng X is set
x is set
y is set
X . y is set
y1 is complex real ext-real Element of REAL
a * y1 is complex real ext-real Element of REAL
x is set
y is complex real ext-real Element of REAL
y1 is complex Element of COMPLEX
a * y1 is set
x1 is complex real ext-real Element of REAL
X . x1 is set
{0} is non empty V2() finite V38() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
m is complex-membered ext-real-membered real-membered set
a is complex real ext-real set
a ** m is complex-membered ext-real-membered real-membered Element of K6(REAL)
X is set
x is complex real ext-real Element of REAL
y is complex Element of COMPLEX
a * y is set
X is set
{X} is non empty V2() finite 1 -element set
x is complex real ext-real set
a * x is complex real ext-real set
m is finite complex-membered ext-real-membered real-membered set
a is complex real ext-real set
a ** m is complex-membered ext-real-membered real-membered Element of K6(REAL)
m is complex-membered ext-real-membered real-membered set
card m is epsilon-transitive epsilon-connected ordinal cardinal set
a is complex real ext-real set
a ** m is complex-membered ext-real-membered real-membered Element of K6(REAL)
card (a ** m) is epsilon-transitive epsilon-connected ordinal cardinal set
m is complex real integer ext-real set
a is complex real integer ext-real set
X is complex real integer ext-real set
a - X is complex real integer ext-real set
- X is complex real integer ext-real set
a + (- X) is complex real integer ext-real set
x is complex real integer ext-real set
m * x is complex real integer ext-real set
y is complex real integer ext-real set
m * y is complex real integer ext-real set
x - y is complex real integer ext-real set
- y is complex real integer ext-real set
x + (- y) is complex real integer ext-real set
m * (x - y) is complex real integer ext-real set
m is complex real integer ext-real set
a is complex real integer ext-real set
X is complex real integer ext-real set
a - X is complex real integer ext-real set
- X is complex real integer ext-real set
a + (- X) is complex real integer ext-real set
- (a - X) is complex real integer ext-real set
(- (a - X)) + a is complex real integer ext-real set
m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a gcd m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m is complex real integer ext-real set
abs m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is complex real integer ext-real set
abs a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m is complex real integer ext-real set
a is complex real integer ext-real set
X is complex real integer ext-real set
m * X is complex real integer ext-real set
a * X is complex real integer ext-real set
x is complex real integer ext-real set
m * x is complex real integer ext-real set
(m * X) * x is complex real integer ext-real set
x is complex real integer ext-real set
(m * X) * x is complex real integer ext-real set
m * x is complex real integer ext-real set
(m * x) * X is complex real integer ext-real set
m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m mod X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a mod X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m |^ x is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(m |^ x) mod X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a |^ x is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(a |^ x) mod X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m |^ y is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(m |^ y) mod X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a |^ y is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(a |^ y) mod X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
m |^ (y + 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(m |^ (y + 1)) mod X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a |^ (y + 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(a |^ (y + 1)) mod X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
u9 |^ (y + 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(u9 |^ (y + 1)) mod ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
u9 |^ y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(u9 |^ y) * u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
((u9 |^ y) * u9) mod ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 mod ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
u9 mod ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(y1 mod ll) * (u9 mod ll) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
((y1 mod ll) * (u9 mod ll)) mod ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x1 * w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
(x1 * w9) mod ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w9 |^ (y + 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
(w9 |^ (y + 1)) mod ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m |^ 0 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(m |^ 0) mod X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a |^ 0 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(a |^ 0) mod X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m is complex real integer ext-real set
a is complex real integer ext-real set
m * a is complex real integer ext-real set
X is complex real integer ext-real set
X * a is complex real integer ext-real set
x is complex real integer ext-real set
(m * a) - (X * a) is complex real integer ext-real set
- (X * a) is complex real integer ext-real set
(m * a) + (- (X * a)) is complex real integer ext-real set
m - X is complex real integer ext-real set
- X is complex real integer ext-real set
m + (- X) is complex real integer ext-real set
(m - X) * a is complex real integer ext-real set
m is complex real integer ext-real set
a is complex real integer ext-real set
X is complex real integer ext-real set
x is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m * x is complex real integer ext-real set
a * x is complex real integer ext-real set
X * x is complex real integer ext-real set
m - a is complex real integer ext-real set
- a is complex real integer ext-real set
m + (- a) is complex real integer ext-real set
y is complex real integer ext-real set
X * y is complex real integer ext-real set
(X * x) * y is complex real integer ext-real set
(X * y) * x is complex real integer ext-real set
(m + (- a)) * x is complex real integer ext-real set
(m * x) - (a * x) is complex real integer ext-real set
- (a * x) is complex real integer ext-real set
(m * x) + (- (a * x)) is complex real integer ext-real set
m is complex real integer ext-real set
a is complex real integer ext-real set
X is complex real integer ext-real set
x is complex real integer ext-real set
m * x is complex real integer ext-real set
a * x is complex real integer ext-real set
m - a is complex real integer ext-real set
- a is complex real integer ext-real set
m + (- a) is complex real integer ext-real set
(m - a) * x is complex real integer ext-real set
(m * x) - (a * x) is complex real integer ext-real set
- (a * x) is complex real integer ext-real set
(m * x) + (- (a * x)) is complex real integer ext-real set
m is complex real integer ext-real set
0 mod m is complex real integer ext-real set
0 div m is complex real integer ext-real set
0 / m is complex real ext-real set
m " is complex real ext-real set
0 * (m ") is complex real ext-real set
[\(0 / m)/] is complex real integer ext-real set
m * 0 is complex real integer ext-real set
0 - (m * 0) is complex real integer ext-real Element of REAL
- (m * 0) is complex real integer ext-real set
0 + (- (m * 0)) is complex real integer ext-real set
m is complex real integer ext-real set
a is complex real integer ext-real set
X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m * X is complex real integer ext-real set
x is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(m * X) + x is complex real integer ext-real set
- a is complex real integer ext-real set
X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m * X is complex real integer ext-real set
x is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(m * X) + x is complex real integer ext-real set
- X is complex real integer ext-real non positive set
y is complex real integer ext-real non positive set
m * y is complex real integer ext-real set
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(m * y) + y1 is complex real integer ext-real set
m * (- X) is complex real integer ext-real set
(m * y) + y1 is complex real integer ext-real Element of REAL
- X is complex real integer ext-real non positive set
(- X) - 1 is non empty complex real integer ext-real non positive negative Element of REAL
- 1 is complex real integer ext-real non positive set
(- X) + (- 1) is complex real integer ext-real non positive set
y is non empty complex real integer ext-real non positive negative Element of REAL
m * y is complex real integer ext-real set
m - x is complex real integer ext-real set
- x is complex real integer ext-real non positive set
m + (- x) is complex real integer ext-real set
y1 is complex real integer ext-real set
(m * y) + y1 is complex real integer ext-real set
m * ((- X) - 1) is complex real integer ext-real Element of REAL
(m * ((- X) - 1)) + (m - x) is complex real integer ext-real Element of REAL
m * y is complex real integer ext-real Element of REAL
(m * y) + y1 is complex real integer ext-real Element of REAL
m is complex real integer ext-real set
a is complex real integer ext-real set
X is complex real integer ext-real set
m gcd X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a gcd X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m - a is complex real integer ext-real set
- a is complex real integer ext-real set
m + (- a) is complex real integer ext-real set
y1 is complex real integer ext-real set
X * y1 is complex real integer ext-real set
y is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
abs a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
abs X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(abs a) gcd (abs X) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
abs y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m - (X * y1) is complex real integer ext-real set
- (X * y1) is complex real integer ext-real set
m + (- (X * y1)) is complex real integer ext-real set
abs m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
abs x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X * y1) + a is complex real integer ext-real set
(abs m) gcd (abs X) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m is complex real integer ext-real set
a is complex real integer ext-real set
X is complex real integer ext-real set
m gcd a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
x is complex real integer ext-real set
x * m is complex real integer ext-real set
y is complex real integer ext-real set
y * a is complex real integer ext-real set
(x * m) + (y * a) is complex real integer ext-real set
X * x is complex real integer ext-real set
m * (X * x) is complex real integer ext-real set
(m * (X * x)) - X is complex real integer ext-real set
- X is complex real integer ext-real set
(m * (X * x)) + (- X) is complex real integer ext-real set
((m * (X * x)) - X) mod a is complex real integer ext-real set
m * X is complex real integer ext-real set
(m * X) * x is complex real integer ext-real set
((m * X) * x) - X is complex real integer ext-real set
((m * X) * x) + (- X) is complex real integer ext-real set
(((m * X) * x) - X) mod a is complex real integer ext-real set
m * x is complex real integer ext-real set
(m * x) - 1 is complex real integer ext-real Element of REAL
- 1 is complex real integer ext-real non positive set
(m * x) + (- 1) is complex real integer ext-real set
((m * x) - 1) * X is complex real integer ext-real Element of REAL
(((m * x) - 1) * X) mod a is complex real integer ext-real set
a * y is complex real integer ext-real set
- (a * y) is complex real integer ext-real set
(- (a * y)) * X is complex real integer ext-real set
((- (a * y)) * X) mod a is complex real integer ext-real set
- y is complex real integer ext-real set
(- y) * X is complex real integer ext-real set
a * ((- y) * X) is complex real integer ext-real set
0 + (a * ((- y) * X)) is complex real integer ext-real Element of REAL
(0 + (a * ((- y) * X))) mod a is complex real integer ext-real set
0 mod a is complex real integer ext-real set
m is complex real integer ext-real set
a is complex real integer ext-real set
X is complex real integer ext-real set
x is complex real integer ext-real set
a * x is complex real integer ext-real set
(a * x) - X is complex real integer ext-real set
- X is complex real integer ext-real set
(a * x) + (- X) is complex real integer ext-real set
((a * x) - X) mod m is complex real integer ext-real set
y is complex real integer ext-real set
m * y is complex real integer ext-real set
y1 is complex real integer ext-real set
(m * y) + y1 is complex real integer ext-real set
a * y is complex real integer ext-real set
(a * y) * m is complex real integer ext-real set
a * y1 is complex real integer ext-real set
(a * y1) - X is complex real integer ext-real set
(a * y1) + (- X) is complex real integer ext-real set
((a * y) * m) + ((a * y1) - X) is complex real integer ext-real set
(((a * y) * m) + ((a * y1) - X)) mod m is complex real integer ext-real set
((a * y1) - X) mod m is complex real integer ext-real set
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a * x1 is complex real integer ext-real set
(a * x1) - X is complex real integer ext-real set
(a * x1) + (- X) is complex real integer ext-real set
((a * x1) - X) mod m is complex real integer ext-real set
m is complex real integer ext-real set
a is complex real integer ext-real set
a gcd m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X is complex real integer ext-real set
x is complex real integer ext-real set
a * x is complex real integer ext-real set
(a * x) - X is complex real integer ext-real set
- X is complex real integer ext-real set
(a * x) + (- X) is complex real integer ext-real set
((a * x) - X) mod m is complex real integer ext-real set
0 mod m is complex real integer ext-real set
y is complex real integer ext-real set
(a gcd m) * y is complex real integer ext-real set
((a * x) - X) - 0 is complex real integer ext-real Element of REAL
- 0 is complex real integer ext-real non positive set
((a * x) - X) + (- 0) is complex real integer ext-real set
m is complex real integer ext-real set
a is complex real integer ext-real set
a gcd m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X is complex real integer ext-real set
x is complex real integer ext-real set
(a gcd m) * x is complex real integer ext-real set
y is complex real integer ext-real set
(a gcd m) * y is complex real integer ext-real set
y1 is complex real integer ext-real set
(a gcd m) * y1 is complex real integer ext-real set
x1 is complex real integer ext-real set
x * x1 is complex real integer ext-real set
(x * x1) - y1 is complex real integer ext-real set
- y1 is complex real integer ext-real set
(x * x1) + (- y1) is complex real integer ext-real set
((x * x1) - y1) mod y is complex real integer ext-real set
a * x1 is complex real integer ext-real set
(a * x1) - X is complex real integer ext-real set
- X is complex real integer ext-real set
(a * x1) + (- X) is complex real integer ext-real set
((a * x1) - X) mod m is complex real integer ext-real set
0 mod y is complex real integer ext-real set
((x * x1) - y1) * (a gcd m) is complex real integer ext-real set
(a gcd m) * 0 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
y * (a gcd m) is complex real integer ext-real set
0 mod m is complex real integer ext-real set
m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a |^ m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a |^ (m -' 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a * X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(a * X) mod (a |^ m) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X mod (a |^ (m -' 1)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a * (X mod (a |^ (m -' 1))) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
X div (a |^ (m -' 1)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X / (a |^ (m -' 1)) is complex real ext-real non negative set
(a |^ (m -' 1)) " is complex real ext-real non negative set
X * ((a |^ (m -' 1)) ") is complex real ext-real non negative set
[\(X / (a |^ (m -' 1)))/] is complex real integer ext-real set
(X div (a |^ (m -' 1))) * (a |^ (m -' 1)) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X - ((X div (a |^ (m -' 1))) * (a |^ (m -' 1))) is complex real integer ext-real set
- ((X div (a |^ (m -' 1))) * (a |^ (m -' 1))) is complex real integer ext-real non positive set
X + (- ((X div (a |^ (m -' 1))) * (a |^ (m -' 1)))) is complex real integer ext-real set
a * (X - ((X div (a |^ (m -' 1))) * (a |^ (m -' 1)))) is complex real integer ext-real set
a * (a |^ (m -' 1)) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(X div (a |^ (m -' 1))) * (a * (a |^ (m -' 1))) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(a * X) - ((X div (a |^ (m -' 1))) * (a * (a |^ (m -' 1)))) is complex real integer ext-real set
- ((X div (a |^ (m -' 1))) * (a * (a |^ (m -' 1)))) is complex real integer ext-real non positive set
(a * X) + (- ((X div (a |^ (m -' 1))) * (a * (a |^ (m -' 1))))) is complex real integer ext-real set
(m -' 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
a |^ ((m -' 1) + 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(X div (a |^ (m -' 1))) * (a |^ ((m -' 1) + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(a * X) - ((X div (a |^ (m -' 1))) * (a |^ ((m -' 1) + 1))) is complex real integer ext-real set
- ((X div (a |^ (m -' 1))) * (a |^ ((m -' 1) + 1))) is complex real integer ext-real non positive set
(a * X) + (- ((X div (a |^ (m -' 1))) * (a |^ ((m -' 1) + 1)))) is complex real integer ext-real set
(X div (a |^ (m -' 1))) * (a |^ m) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(a * X) - ((X div (a |^ (m -' 1))) * (a |^ m)) is complex real integer ext-real set
- ((X div (a |^ (m -' 1))) * (a |^ m)) is complex real integer ext-real non positive set
(a * X) + (- ((X div (a |^ (m -' 1))) * (a |^ m))) is complex real integer ext-real set
((X div (a |^ (m -' 1))) * (a |^ m)) + (a * (X mod (a |^ (m -' 1)))) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m * a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m * X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(m * a) mod (m * X) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a mod X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m * (a mod X) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a div X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a / X is complex real ext-real non negative set
X " is complex real ext-real non negative set
a * (X ") is complex real ext-real non negative set
[\(a / X)/] is complex real integer ext-real set
X * (a div X) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(X * (a div X)) + (a mod X) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m * ((X * (a div X)) + (a mod X)) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(m * X) * (a div X) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
((m * X) * (a div X)) + (m * (a mod X)) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a |^ m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X mod (a |^ m) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
a |^ 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X div (a |^ m) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X / (a |^ m) is complex real ext-real non negative set
(a |^ m) " is complex real ext-real non negative set
X * ((a |^ m) ") is complex real ext-real non negative set
[\(X / (a |^ m))/] is complex real integer ext-real set
(a |^ m) * (X div (a |^ m)) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
((a |^ m) * (X div (a |^ m))) + (X mod (a |^ m)) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m - a is complex real integer ext-real set
- a is complex real integer ext-real non positive set
m + (- a) is complex real integer ext-real set
(m - a) mod X is complex real integer ext-real set
m mod X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a mod X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is complex real integer ext-real set
X * x is complex real integer ext-real set
y is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X * y is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(X * y) + a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
((X * y) + a) mod X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a - m is complex real integer ext-real set
- m is complex real integer ext-real non positive set
a + (- m) is complex real integer ext-real set
- x is complex real integer ext-real set
X * (- x) is complex real integer ext-real set
y is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X * y is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(X * y) + m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
((X * y) + m) mod X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m div X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m / X is complex real ext-real non negative set
X " is complex real ext-real non negative set
m * (X ") is complex real ext-real non negative set
[\(m / X)/] is complex real integer ext-real set
X * (m div X) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(X * (m div X)) + (m mod X) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a div X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a / X is complex real ext-real non negative set
a * (X ") is complex real ext-real non negative set
[\(a / X)/] is complex real integer ext-real set
X * (a div X) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a - (X * (a div X)) is complex real integer ext-real set
- (X * (a div X)) is complex real integer ext-real non positive set
a + (- (X * (a div X))) is complex real integer ext-real set
(X * (m div X)) + (a - (X * (a div X))) is complex real integer ext-real set
(m div X) - (a div X) is complex real integer ext-real set
- (a div X) is complex real integer ext-real non positive set
(m div X) + (- (a div X)) is complex real integer ext-real set
X * ((m div X) - (a div X)) is complex real integer ext-real set
a + (X * ((m div X) - (a div X))) is complex real integer ext-real set
X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m mod X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a mod X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m - a is complex real integer ext-real set
- a is complex real integer ext-real non positive set
m + (- a) is complex real integer ext-real set
(m - a) mod X is complex real integer ext-real set
(m - a) mod X is complex real integer ext-real set
m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a |^ m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
x is complex real integer ext-real set
x ^2 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a * (x ^2) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(a * (x ^2)) - X is complex real integer ext-real set
- X is complex real integer ext-real non positive set
(a * (x ^2)) + (- X) is complex real integer ext-real set
((a * (x ^2)) - X) mod (a |^ m) is complex real integer ext-real set
(a * (x ^2)) mod (a |^ m) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X mod (a |^ m) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a |^ (m -' 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(x ^2) mod (a |^ (m -' 1)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a * ((x ^2) mod (a |^ (m -' 1))) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a |^ m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
x is complex real integer ext-real set
a * x is complex real integer ext-real set
(a * x) - X is complex real integer ext-real set
- X is complex real integer ext-real non positive set
(a * x) + (- X) is complex real integer ext-real set
((a * x) - X) mod (a |^ m) is complex real integer ext-real set
y is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a * y is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(a * y) mod (a |^ m) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X mod (a |^ m) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a |^ (m -' 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
y mod (a |^ (m -' 1)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a * (y mod (a |^ (m -' 1))) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
- x is complex real integer ext-real set
y is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a * y is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
- 1 is complex real integer ext-real non positive Element of REAL
(- 1) * ((a * x) - X) is complex real integer ext-real Element of REAL
(a * y) + X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
y1 is complex real integer ext-real set
(a |^ m) * y1 is complex real integer ext-real set
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(a |^ m) * x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
u9 gcd w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m is complex real integer ext-real set
a is Relation-like INT -defined INT -valued V71() V72() V73() Element of K6(K7(INT,INT))
X is complex real integer ext-real set
x is complex real integer ext-real set
[X,x] is set
{X,x} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{X} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{X,x},{X}} is finite V38() set
y is complex real integer ext-real set
y1 is complex real integer ext-real set
[y,y1] is set
{y,y1} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{y} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{y,y1},{y}} is finite V38() set
x1 is complex real integer V31() ext-real Element of INT
u9 is complex real integer V31() ext-real Element of INT
[x1,u9] is set
{x1,u9} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{x1} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{x1,u9},{x1}} is finite V38() set
a is Relation-like INT -defined INT -valued V71() V72() V73() Element of K6(K7(INT,INT))
X is Relation-like INT -defined INT -valued V71() V72() V73() Element of K6(K7(INT,INT))
x is complex real integer ext-real set
y is complex real integer ext-real set
[x,y] is set
{x,y} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{x} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{x,y},{x}} is finite V38() set
x is set
y is set
y1 is set
[y,y1] is set
{y,y1} is finite set
{y} is non empty V2() finite 1 -element set
{{y,y1},{y}} is finite V38() set
x1 is complex real integer ext-real set
u9 is complex real integer ext-real set
[x1,u9] is set
{x1,u9} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{x1} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{x1,u9},{x1}} is finite V38() set
x is set
y is set
y1 is set
[y,y1] is set
{y,y1} is finite set
{y} is non empty V2() finite 1 -element set
{{y,y1},{y}} is finite V38() set
x1 is complex real integer ext-real set
u9 is complex real integer ext-real set
[x1,u9] is set
{x1,u9} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{x1} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{x1,u9},{x1}} is finite V38() set
m is complex real integer ext-real set
(m) is Relation-like INT -defined INT -valued V71() V72() V73() Element of K6(K7(INT,INT))
dom (m) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
a is set
X is complex real integer ext-real set
[X,X] is set
{X,X} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{X} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{X,X},{X}} is finite V38() set
m is complex real integer ext-real set
(m) is Relation-like INT -defined INT -valued total V71() V72() V73() Element of K6(K7(INT,INT))
a is set
X is set
[a,X] is set
{a,X} is finite set
{a} is non empty V2() finite 1 -element set
{{a,X},{a}} is finite V38() set
[X,a] is set
{X,a} is finite set
{X} is non empty V2() finite 1 -element set
{{X,a},{X}} is finite V38() set
y is complex real integer ext-real set
x is complex real integer ext-real set
a is set
X is set
x is set
[a,X] is set
{a,X} is finite set
{a} is non empty V2() finite 1 -element set
{{a,X},{a}} is finite V38() set
[X,x] is set
{X,x} is finite set
{X} is non empty V2() finite 1 -element set
{{X,x},{X}} is finite V38() set
[a,x] is set
{a,x} is finite set
{{a,x},{a}} is finite V38() set
y is complex real integer ext-real set
y1 is complex real integer ext-real set
x1 is complex real integer ext-real set
field (m) is set
m is complex real integer ext-real set
(m) is Relation-like INT -defined INT -valued total V71() V72() V73() Element of K6(K7(INT,INT))
m is complex real integer ext-real set
(m) is Relation-like INT -defined INT -valued total reflexive symmetric transitive V71() V72() V73() Element of K6(K7(INT,INT))
a is complex real integer ext-real set
X is complex real integer ext-real set
a * X is complex real integer ext-real set
Class ((m),X) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
x is complex real integer ext-real set
(a * X) - x is complex real integer ext-real set
- x is complex real integer ext-real set
(a * X) + (- x) is complex real integer ext-real set
((a * X) - x) mod m is complex real integer ext-real set
y is complex real integer ext-real set
a * y is complex real integer ext-real set
(a * y) - x is complex real integer ext-real set
(a * y) + (- x) is complex real integer ext-real set
((a * y) - x) mod m is complex real integer ext-real set
((a * X) - x) + x is complex real integer ext-real set
[X,y] is set
{X,y} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{X} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{X,y},{X}} is finite V38() set
X * a is complex real integer ext-real set
y * a is complex real integer ext-real set
0 mod m is complex real integer ext-real set
0 + x is complex real integer ext-real Element of REAL
m is complex real integer ext-real set
a is complex real integer ext-real set
X is complex real integer ext-real set
(X) is Relation-like INT -defined INT -valued total reflexive symmetric transitive V71() V72() V73() Element of K6(K7(INT,INT))
x is complex real integer ext-real set
m * x is complex real integer ext-real set
(m * x) - a is complex real integer ext-real set
- a is complex real integer ext-real set
(m * x) + (- a) is complex real integer ext-real set
((m * x) - a) mod X is complex real integer ext-real set
m gcd X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
y is complex real integer ext-real set
y * m is complex real integer ext-real set
y1 is complex real integer ext-real set
y1 * X is complex real integer ext-real set
(y * m) + (y1 * X) is complex real integer ext-real set
0 mod X is complex real integer ext-real set
((m * x) - a) * y is complex real integer ext-real set
0 * y is complex real integer ext-real Element of REAL
m * y is complex real integer ext-real set
x * (m * y) is complex real integer ext-real set
a * y is complex real integer ext-real set
(x * (m * y)) - (a * y) is complex real integer ext-real set
- (a * y) is complex real integer ext-real set
(x * (m * y)) + (- (a * y)) is complex real integer ext-real set
1 - (y1 * X) is complex real integer ext-real Element of REAL
- (y1 * X) is complex real integer ext-real set
1 + (- (y1 * X)) is complex real integer ext-real set
x * (1 - (y1 * X)) is complex real integer ext-real Element of REAL
(x * (1 - (y1 * X))) - (a * y) is complex real integer ext-real Element of REAL
(x * (1 - (y1 * X))) + (- (a * y)) is complex real integer ext-real set
x1 is complex real integer ext-real set
a * x1 is complex real integer ext-real set
[x,(a * x1)] is set
{x,(a * x1)} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{x} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{x,(a * x1)},{x}} is finite V38() set
x * y1 is complex real integer ext-real set
(x * y1) * X is complex real integer ext-real set
x - ((x * y1) * X) is complex real integer ext-real set
- ((x * y1) * X) is complex real integer ext-real set
x + (- ((x * y1) * X)) is complex real integer ext-real set
(x - ((x * y1) * X)) - (a * y) is complex real integer ext-real set
(x - ((x * y1) * X)) + (- (a * y)) is complex real integer ext-real set
((x - ((x * y1) * X)) - (a * y)) mod X is complex real integer ext-real set
x - (a * y) is complex real integer ext-real set
x + (- (a * y)) is complex real integer ext-real set
- x is complex real integer ext-real set
(- x) * y1 is complex real integer ext-real set
((- x) * y1) * X is complex real integer ext-real set
(x - (a * y)) + (((- x) * y1) * X) is complex real integer ext-real set
((x - (a * y)) + (((- x) * y1) * X)) mod X is complex real integer ext-real set
(x - (a * y)) mod X is complex real integer ext-real set
0 + (a * y) is complex real integer ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Euler a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( a,b₁ are_relative_prime & 1 <= b₁ & b₁ <= a ) } is set
card { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( a,b₁ are_relative_prime & 1 <= b₁ & b₁ <= a ) } is epsilon-transitive epsilon-connected ordinal cardinal set
(Euler a) -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m |^ ((Euler a) -' 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a) is Relation-like INT -defined INT -valued total reflexive symmetric transitive V71() V72() V73() Element of K6(K7(INT,INT))
x is complex real integer ext-real set
m * x is complex real integer ext-real Element of REAL
X is complex real integer ext-real set
(m * x) - X is complex real integer ext-real Element of REAL
- X is complex real integer ext-real set
(m * x) + (- X) is complex real integer ext-real set
((m * x) - X) mod a is complex real integer ext-real set
X * (m |^ ((Euler a) -' 1)) is complex real integer ext-real Element of REAL
[x,(X * (m |^ ((Euler a) -' 1)))] is set
{x,(X * (m |^ ((Euler a) -' 1)))} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{x} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{x,(X * (m |^ ((Euler a) -' 1)))},{x}} is finite V38() set
m |^ (Euler a) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(m |^ (Euler a)) mod a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(m |^ (Euler a)) div a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(m |^ (Euler a)) / a is complex real ext-real non negative set
a " is complex real ext-real non negative set
(m |^ (Euler a)) * (a ") is complex real ext-real non negative set
[\((m |^ (Euler a)) / a)/] is complex real integer ext-real set
a * ((m |^ (Euler a)) div a) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
(a * ((m |^ (Euler a)) div a)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
(m |^ (Euler a)) - 1 is complex real integer ext-real Element of REAL
- 1 is complex real integer ext-real non positive set
(m |^ (Euler a)) + (- 1) is complex real integer ext-real set
(m |^ (Euler a)) * x is complex real integer ext-real Element of REAL
1 * x is complex real integer ext-real Element of REAL
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( a,b₁ are_relative_prime & 1 <= b₁ & b₁ <= a ) } is set
1 gcd a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((Euler a) -' 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
(Euler a) - 1 is complex real integer ext-real Element of REAL
(Euler a) + (- 1) is complex real integer ext-real set
((Euler a) - 1) + 1 is complex real integer ext-real Element of REAL
((m * x) - X) - 0 is complex real integer ext-real Element of REAL
- 0 is complex real integer ext-real non positive set
((m * x) - X) + (- 0) is complex real integer ext-real set
(m |^ ((Euler a) -' 1)) * 0 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
(m |^ ((Euler a) -' 1)) * ((m * x) - X) is complex real integer ext-real Element of REAL
(m |^ ((Euler a) -' 1)) * m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
((m |^ ((Euler a) -' 1)) * m) * x is complex real integer ext-real Element of REAL
(m |^ ((Euler a) -' 1)) * X is complex real integer ext-real Element of REAL
(((m |^ ((Euler a) -' 1)) * m) * x) - ((m |^ ((Euler a) -' 1)) * X) is complex real integer ext-real Element of REAL
- ((m |^ ((Euler a) -' 1)) * X) is complex real integer ext-real set
(((m |^ ((Euler a) -' 1)) * m) * x) + (- ((m |^ ((Euler a) -' 1)) * X)) is complex real integer ext-real set
m |^ (((Euler a) -' 1) + 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
(m |^ (((Euler a) -' 1) + 1)) * x is complex real integer ext-real Element of REAL
((m |^ (((Euler a) -' 1) + 1)) * x) - ((m |^ ((Euler a) -' 1)) * X) is complex real integer ext-real Element of REAL
((m |^ (((Euler a) -' 1) + 1)) * x) + (- ((m |^ ((Euler a) -' 1)) * X)) is complex real integer ext-real set
0 + ((m |^ ((Euler a) -' 1)) * X) is complex real integer ext-real Element of REAL
m is complex real integer ext-real set
a is complex real integer ext-real set
a gcd m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X is complex real integer ext-real set
y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 is complex real integer ext-real set
y * y1 is complex real integer ext-real Element of REAL
x1 is complex real integer ext-real set
y * x1 is complex real integer ext-real Element of REAL
u9 is complex real integer ext-real set
y * u9 is complex real integer ext-real Element of REAL
w9 is complex real integer ext-real set
y1 * w9 is complex real integer ext-real set
(y1 * w9) - u9 is complex real integer ext-real set
- u9 is complex real integer ext-real set
(y1 * w9) + (- u9) is complex real integer ext-real set
((y1 * w9) - u9) mod x1 is complex real integer ext-real set
ll is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom ll is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
w is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
ll . w is set
w - 1 is complex real integer ext-real Element of REAL
- 1 is complex real integer ext-real non positive set
w + (- 1) is complex real integer ext-real set
(w - 1) * x1 is complex real integer ext-real Element of REAL
w9 + ((w - 1) * x1) is complex real integer ext-real Element of REAL
w is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() FinSequence of INT
dom w is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w . w is complex real integer ext-real set
y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w . y is complex real integer ext-real set
w - 1 is complex real integer ext-real Element of REAL
- 1 is complex real integer ext-real non positive set
w + (- 1) is complex real integer ext-real set
(w - 1) * x1 is complex real integer ext-real Element of REAL
w9 + ((w - 1) * x1) is complex real integer ext-real Element of REAL
y - 1 is complex real integer ext-real Element of REAL
y + (- 1) is complex real integer ext-real set
(y - 1) * x1 is complex real integer ext-real Element of REAL
w9 + ((y - 1) * x1) is complex real integer ext-real Element of REAL
((w - 1) * x1) + w9 is complex real integer ext-real Element of REAL
((y - 1) * x1) + w9 is complex real integer ext-real Element of REAL
(((w - 1) * x1) + w9) - (((y - 1) * x1) + w9) is complex real integer ext-real Element of REAL
- (((y - 1) * x1) + w9) is complex real integer ext-real set
(((w - 1) * x1) + w9) + (- (((y - 1) * x1) + w9)) is complex real integer ext-real set
w - y is complex real integer ext-real Element of REAL
- y is complex real integer ext-real non positive set
w + (- y) is complex real integer ext-real set
(w - y) * x1 is complex real integer ext-real Element of REAL
c₁₄ is complex real integer ext-real set
(y * x1) * c₁₄ is complex real integer ext-real Element of REAL
y * c₁₄ is complex real integer ext-real Element of REAL
(y * c₁₄) * x1 is complex real integer ext-real Element of REAL
Seg y is finite y -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= y ) } is set
y - 1 is complex real integer ext-real Element of REAL
y + (- 1) is complex real integer ext-real set
1 - y is complex real integer ext-real Element of REAL
- y is complex real integer ext-real non positive set
1 + (- y) is complex real integer ext-real set
- y is complex real integer ext-real non positive Element of REAL
abs (w - y) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
abs y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
0 mod x1 is complex real integer ext-real set
((y1 * w9) - u9) * y is complex real integer ext-real Element of REAL
0 * y is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
x1 * y is complex real integer ext-real Element of REAL
a * w9 is complex real integer ext-real set
(a * w9) - X is complex real integer ext-real set
- X is complex real integer ext-real set
(a * w9) + (- X) is complex real integer ext-real set
((a * w9) - X) mod m is complex real integer ext-real set
0 mod m is complex real integer ext-real set
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w . w is complex real integer ext-real set
a * (w . w) is complex real integer ext-real set
(a * (w . w)) - X is complex real integer ext-real set
(a * (w . w)) + (- X) is complex real integer ext-real set
((a * (w . w)) - X) mod m is complex real integer ext-real set
w - 1 is complex real integer ext-real Element of REAL
- 1 is complex real integer ext-real non positive set
w + (- 1) is complex real integer ext-real set
(w - 1) * x1 is complex real integer ext-real Element of REAL
w9 + ((w - 1) * x1) is complex real integer ext-real Element of REAL
a * (w9 + ((w - 1) * x1)) is complex real integer ext-real Element of REAL
(a * (w9 + ((w - 1) * x1))) - X is complex real integer ext-real Element of REAL
(a * (w9 + ((w - 1) * x1))) + (- X) is complex real integer ext-real set
((a * (w9 + ((w - 1) * x1))) - X) mod m is complex real integer ext-real set
y1 * (w - 1) is complex real integer ext-real Element of REAL
(y1 * (w - 1)) * m is complex real integer ext-real Element of REAL
((a * w9) - X) + ((y1 * (w - 1)) * m) is complex real integer ext-real Element of REAL
(((a * w9) - X) + ((y1 * (w - 1)) * m)) mod m is complex real integer ext-real set
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w . w is complex real integer ext-real set
a * (w . w) is complex real integer ext-real set
(a * (w . w)) - X is complex real integer ext-real set
(a * (w . w)) + (- X) is complex real integer ext-real set
((a * (w . w)) - X) mod m is complex real integer ext-real set
y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c₁₄ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w . y is complex real integer ext-real set
w . c₁₄ is complex real integer ext-real set
m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
dom m is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
len m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
<*a*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V71() V72() V73() V74() V75() V76() V77() V78() FinSequence of NAT
[1,a] is set
{1,a} is finite V38() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{1,a},{1}} is finite V38() set
{[1,a]} is non empty V2() Relation-like Function-like constant finite 1 -element set
m ^ <*a*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Del ((m ^ <*a*>),X) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Del (m,X) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
(Del (m,X)) ^ <*a*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
len (Del (m,X)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len ((Del (m,X)) ^ <*a*>) is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (m ^ <*a*>) is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(x + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
dom (m ^ <*a*>) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
len (Del ((m ^ <*a*>),X)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(Del ((m ^ <*a*>),X)) . y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((Del (m,X)) ^ <*a*>) . y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom (Del (m,X)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
(Del (m,X)) . y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(m ^ <*a*>) . y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
(m ^ <*a*>) . (y + 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom (Del (m,X)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
(Del (m,X)) . y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . (y + 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
len m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom m is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
a is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
len a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
<*X*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V71() V72() V73() V74() V75() V76() V77() V78() FinSequence of NAT
[1,X] is set
{1,X} is finite V38() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{1,X},{1}} is finite V38() set
{[1,X]} is non empty V2() Relation-like Function-like constant finite 1 -element set
a ^ <*X*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
len (a ^ <*X*>) is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom (a ^ <*X*>) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
(len a) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
(a ^ <*X*>) . 2 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a ^ <*X*>) . 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((a ^ <*X*>) . 2) gcd ((a ^ <*X*>) . 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
<*((a ^ <*X*>) . 1),((a ^ <*X*>) . 2)*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<*((a ^ <*X*>) . 1)*> is non empty V2() Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,((a ^ <*X*>) . 1)] is set
{1,((a ^ <*X*>) . 1)} is finite V38() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{1,((a ^ <*X*>) . 1)},{1}} is finite V38() set
{[1,((a ^ <*X*>) . 1)]} is non empty V2() Relation-like Function-like constant finite 1 -element set
<*((a ^ <*X*>) . 2)*> is non empty V2() Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,((a ^ <*X*>) . 2)] is set
{1,((a ^ <*X*>) . 2)} is finite V38() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{1,((a ^ <*X*>) . 2)},{1}} is finite V38() set
{[1,((a ^ <*X*>) . 2)]} is non empty V2() Relation-like Function-like constant finite 1 -element set
<*((a ^ <*X*>) . 1)*> ^ <*((a ^ <*X*>) . 2)*> is non empty Relation-like NAT -defined Function-like finite K280(1,1) -element FinSequence-like FinSubsequence-like set
K280(1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Del ((a ^ <*X*>),y1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Product (Del ((a ^ <*X*>),y1)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a ^ <*X*>) . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product (Del ((a ^ <*X*>),y1))) gcd ((a ^ <*X*>) . y1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg (len (a ^ <*X*>)) is non empty finite len (a ^ <*X*>) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= len (a ^ <*X*>) ) } is set
<*((a ^ <*X*>) . 2)*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V71() V72() V73() V74() V75() V76() V77() V78() FinSequence of NAT
Product <*((a ^ <*X*>) . 2)*> is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product <*((a ^ <*X*>) . 2)*>) gcd ((a ^ <*X*>) . 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
<*((a ^ <*X*>) . 1)*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V71() V72() V73() V74() V75() V76() V77() V78() FinSequence of NAT
Product <*((a ^ <*X*>) . 1)*> is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product <*((a ^ <*X*>) . 1)*>) gcd ((a ^ <*X*>) . 2) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Del ((a ^ <*X*>),y1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Product (Del ((a ^ <*X*>),y1)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a ^ <*X*>) . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product (Del ((a ^ <*X*>),y1))) gcd ((a ^ <*X*>) . y1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
y1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
dom a is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a . x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a . u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a . x1) gcd (a . u9) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a ^ <*X*>) . x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a ^ <*X*>) . u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a . x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a . x1) gcd X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a ^ <*X*>) . ((len a) + 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a ^ <*X*>) . x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Del ((a ^ <*X*>),u9) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Product (Del ((a ^ <*X*>),u9)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a ^ <*X*>) . u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product (Del ((a ^ <*X*>),u9))) gcd ((a ^ <*X*>) . u9) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Del (a,u9) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Product (Del (a,u9)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a . u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product (Del (a,u9))) gcd (a . u9) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a . u9) gcd X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w9 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
len w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom w9 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w9 . ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w9 . w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(w9 . ll) gcd (w9 . w) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product (Del (a,u9))) * X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
((Product (Del (a,u9))) * X) gcd (a . u9) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Del (a,u9)) ^ <*X*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Product ((Del (a,u9)) ^ <*X*>) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product ((Del (a,u9)) ^ <*X*>)) gcd (a . u9) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Del ((a ^ <*X*>),((len a) + 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Product (Del ((a ^ <*X*>),((len a) + 1))) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product (Del ((a ^ <*X*>),((len a) + 1)))) gcd X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Product a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product a) gcd X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Del ((a ^ <*X*>),u9) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Product (Del ((a ^ <*X*>),u9)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a ^ <*X*>) . u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product (Del ((a ^ <*X*>),u9))) gcd ((a ^ <*X*>) . u9) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Del ((a ^ <*X*>),y1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Product (Del ((a ^ <*X*>),y1)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a ^ <*X*>) . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product (Del ((a ^ <*X*>),y1))) gcd ((a ^ <*X*>) . y1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a ^ <*X*>) . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(a ^ <*X*>) . x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((a ^ <*X*>) . y1) gcd ((a ^ <*X*>) . x1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
<*> NAT is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional integer finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() FinSequence of NAT
len (<*> NAT) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer V31() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() Element of NAT
dom (<*> NAT) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() Element of K6(NAT)
a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Del ((<*> NAT),a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Product (Del ((<*> NAT),a)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(<*> NAT) . a is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer V31() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() Element of NAT
(Product (Del ((<*> NAT),a))) gcd ((<*> NAT) . a) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Del (m,a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Product (Del (m,a)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product (Del (m,a))) gcd (m . a) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
len X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom X is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X . x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X . y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X . x) gcd (X . y) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
dom m is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
Product m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m . a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
rng m is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(REAL)
m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
dom a is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
Product a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a . X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
len m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . (len m) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
Del (m,X) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
(Del (m,X)) . a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom m is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
dom m is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
len m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
Del (m,a) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Product (Del (m,a)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
len (Del (m,a)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len (Del (m,a))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
dom (Del (m,a)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
(Del (m,a)) . X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
X - 1 is complex real integer ext-real Element of REAL
- 1 is complex real integer ext-real non positive set
X + (- 1) is complex real integer ext-real set
X -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Del (m,a)) . (X -' 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X -' 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
m . ((X -' 1) + 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(x + 1) - 1 is complex real integer ext-real Element of REAL
(x + 1) + (- 1) is complex real integer ext-real set
dom (Del (m,a)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
dom (Del (m,a)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
(Del (m,a)) . X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m is complex real integer ext-real set
a is complex real integer ext-real set
m * a is complex real integer ext-real set
X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m mod X is complex real integer ext-real set
(m * a) mod X is complex real integer ext-real set
m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
dom m is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
Sum m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
<*x*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V71() V72() V73() V74() V75() V76() V77() V78() FinSequence of NAT
[1,x] is set
{1,x} is finite V38() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{1,x},{1}} is finite V38() set
{[1,x]} is non empty V2() Relation-like Function-like constant finite 1 -element set
X ^ <*x*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
dom (X ^ <*x*>) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
dom X is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X ^ <*x*>) . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (X ^ <*x*>) is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X ^ <*x*>) . (len (X ^ <*x*>)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len X) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
(X ^ <*x*>) . ((len X) + 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Sum X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Sum X) + x is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
y1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
dom y1 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
y1 . x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Sum y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Sum (X ^ <*x*>) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(X ^ <*x*>) . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
<*> NAT is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional integer finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() FinSequence of NAT
X is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
dom X is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
X . x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Sum X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
len m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom m is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
a is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
<*X*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V71() V72() V73() V74() V75() V76() V77() V78() FinSequence of NAT
[1,X] is set
{1,X} is finite V38() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{1,X},{1}} is finite V38() set
{[1,X]} is non empty V2() Relation-like Function-like constant finite 1 -element set
a ^ <*X*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : (((Product (Del (m,a₁))) * b₁) - 1) mod (m . a₁) = 0 } is set
Seg (len m) is finite len m -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= len m ) } is set
x is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
Del (m,x) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Product (Del (m,x)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : (((Product (Del (m,x))) * b₁) - 1) mod (m . x) = 0 } is set
(Product (Del (m,x))) gcd (m . x) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y is complex real integer ext-real set
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(Product (Del (m,x))) * y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
((Product (Del (m,x))) * y1) - 1 is complex real integer ext-real Element of REAL
- 1 is complex real integer ext-real non positive set
((Product (Del (m,x))) * y1) + (- 1) is complex real integer ext-real set
(((Product (Del (m,x))) * y1) - 1) mod y is complex real integer ext-real set
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
dom x is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
y is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
len a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len a) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom x1 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
x1 . u9 is set
w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x1 . w9 is set
Del (m,w9) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Product (Del (m,w9)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x . w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product (Del (m,w9))) * (x . w9) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
y . w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((Product (Del (m,w9))) * (x . w9)) * (y . w9) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
u9 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Sum u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
ll is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
u9 . ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Del (m,ll) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Product (Del (m,ll)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x . ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y . ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(x . ll) * (y . ll) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
(Product (Del (m,ll))) * ((x . ll) * (y . ll)) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
(Product (Del (m,ll))) * (x . ll) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
((Product (Del (m,ll))) * (x . ll)) * (y . ll) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
dom u9 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m . ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Del (u9,ll) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Sum (Del (u9,ll)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg (len u9) is finite len u9 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= len u9 ) } is set
dom u9 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
len (Del (u9,ll)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len (Del (u9,ll))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
dom (Del (u9,ll)) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
w is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(Del (u9,ll)) . w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg ((len a) + 1) is non empty finite (len a) + 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= (len a) + 1 ) } is set
u9 . w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
u9 . (w + 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y . ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Sum u9) - (y . ll) is complex real integer ext-real Element of REAL
- (y . ll) is complex real integer ext-real non positive set
(Sum u9) + (- (y . ll)) is complex real integer ext-real set
m . ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((Sum u9) - (y . ll)) mod (m . ll) is complex real integer ext-real set
Del (u9,ll) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Sum (Del (u9,ll)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
u9 . ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(u9 . ll) - (y . ll) is complex real integer ext-real Element of REAL
(u9 . ll) + (- (y . ll)) is complex real integer ext-real set
(Sum (Del (u9,ll))) + ((u9 . ll) - (y . ll)) is complex real integer ext-real Element of REAL
((Sum (Del (u9,ll))) + ((u9 . ll) - (y . ll))) mod (m . ll) is complex real integer ext-real set
((u9 . ll) - (y . ll)) mod (m . ll) is complex real integer ext-real set
w is complex real integer ext-real set
w mod (m . ll) is complex real integer ext-real set
(w mod (m . ll)) + (((u9 . ll) - (y . ll)) mod (m . ll)) is complex real integer ext-real set
((w mod (m . ll)) + (((u9 . ll) - (y . ll)) mod (m . ll))) mod (m . ll) is complex real integer ext-real set
Seg ((len a) + 1) is non empty finite (len a) + 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= (len a) + 1 ) } is set
dom u9 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
Del (m,ll) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
Product (Del (m,ll)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x . ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product (Del (m,ll))) * (x . ll) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
((Product (Del (m,ll))) * (x . ll)) * (y . ll) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
1 * (y . ll) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
(((Product (Del (m,ll))) * (x . ll)) * (y . ll)) - (1 * (y . ll)) is complex real integer ext-real Element of REAL
- (1 * (y . ll)) is complex real integer ext-real non positive set
(((Product (Del (m,ll))) * (x . ll)) * (y . ll)) + (- (1 * (y . ll))) is complex real integer ext-real set
((Product (Del (m,ll))) * (x . ll)) - 1 is complex real integer ext-real Element of REAL
- 1 is complex real integer ext-real non positive set
((Product (Del (m,ll))) * (x . ll)) + (- 1) is complex real integer ext-real set
(((Product (Del (m,ll))) * (x . ll)) - 1) * (y . ll) is complex real integer ext-real Element of REAL
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : (((Product (Del (m,ll))) * b₁) - 1) mod (m . ll) = 0 } is set
(Sum (Del (u9,ll))) + (u9 . ll) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
((Sum (Del (u9,ll))) + (u9 . ll)) - (y . ll) is complex real integer ext-real Element of REAL
((Sum (Del (u9,ll))) + (u9 . ll)) + (- (y . ll)) is complex real integer ext-real set
(((Sum (Del (u9,ll))) + (u9 . ll)) - (y . ll)) mod (m . ll) is complex real integer ext-real set
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product (Del (m,ll))) * w is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
((Product (Del (m,ll))) * w) - 1 is complex real integer ext-real Element of REAL
((Product (Del (m,ll))) * w) + (- 1) is complex real integer ext-real set
(((Product (Del (m,ll))) * w) - 1) mod (m . ll) is complex real integer ext-real set
ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y . ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Sum u9) - (y . ll) is complex real integer ext-real Element of REAL
- (y . ll) is complex real integer ext-real non positive set
(Sum u9) + (- (y . ll)) is complex real integer ext-real set
m . ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((Sum u9) - (y . ll)) mod (m . ll) is complex real integer ext-real set
m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
dom m is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
Product m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
<*x*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V71() V72() V73() V74() V75() V76() V77() V78() FinSequence of NAT
[1,x] is set
{1,x} is finite V38() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{1,x},{1}} is finite V38() set
{[1,x]} is non empty V2() Relation-like Function-like constant finite 1 -element set
X ^ <*x*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
len X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(len X) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
len (X ^ <*x*>) is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom (X ^ <*x*>) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
dom X is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X . y1) gcd x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X ^ <*x*>) . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X ^ <*x*>) . (len (X ^ <*x*>)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((X ^ <*x*>) . y1) gcd ((X ^ <*x*>) . (len (X ^ <*x*>))) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X ^ <*x*>) . ((len X) + 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((X ^ <*x*>) . y1) gcd ((X ^ <*x*>) . ((len X) + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Product X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product X) gcd x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X . x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X . y1) gcd (X . x1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X ^ <*x*>) . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X ^ <*x*>) . x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X ^ <*x*>) . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X ^ <*x*>) . (len (X ^ <*x*>)) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X ^ <*x*>) . ((len X) + 1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(Product X) * x is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative Element of REAL
y1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom y1 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 . x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 . u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(y1 . x1) gcd (y1 . u9) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 . w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Product y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Product (X ^ <*x*>) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X ^ <*x*>) . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X ^ <*x*>) . x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((X ^ <*x*>) . y1) gcd ((X ^ <*x*>) . x1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X ^ <*x*>) . u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
<*> NAT is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional integer finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() FinSequence of NAT
dom (<*> NAT) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() Element of K6(NAT)
Product (<*> NAT) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom X is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X . x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X . y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(X . x) gcd (X . y) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Product X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m is complex real integer ext-real set
a is complex real integer ext-real set
X is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
dom X is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
Product X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
m - a is complex real integer ext-real set
- a is complex real integer ext-real set
m + (- a) is complex real integer ext-real set
y is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a - (x . y1) is complex real integer ext-real Element of REAL
- (x . y1) is complex real integer ext-real non positive set
a + (- (x . y1)) is complex real integer ext-real set
(a - (x . y1)) mod (X . y1) is complex real integer ext-real set
m - (x . y1) is complex real integer ext-real Element of REAL
m + (- (x . y1)) is complex real integer ext-real set
(m - (x . y1)) mod (X . y1) is complex real integer ext-real set
(m - (x . y1)) - (a - (x . y1)) is complex real integer ext-real Element of REAL
- (a - (x . y1)) is complex real integer ext-real set
(m - (x . y1)) + (- (a - (x . y1))) is complex real integer ext-real set
x1 is complex real integer ext-real set
(X . y1) * x1 is complex real integer ext-real Element of REAL
u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a - m is complex real integer ext-real set
- m is complex real integer ext-real set
a + (- m) is complex real integer ext-real set
y is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x . y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a - (x . y1) is complex real integer ext-real Element of REAL
- (x . y1) is complex real integer ext-real non positive set
a + (- (x . y1)) is complex real integer ext-real set
(a - (x . y1)) mod (X . y1) is complex real integer ext-real set
m - (x . y1) is complex real integer ext-real Element of REAL
m + (- (x . y1)) is complex real integer ext-real set
(m - (x . y1)) mod (X . y1) is complex real integer ext-real set
(a - (x . y1)) - (m - (x . y1)) is complex real integer ext-real Element of REAL
- (m - (x . y1)) is complex real integer ext-real set
(a - (x . y1)) + (- (m - (x . y1))) is complex real integer ext-real set
x1 is complex real integer ext-real set
(X . y1) * x1 is complex real integer ext-real Element of REAL
u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m is complex real integer ext-real set
a is complex real integer ext-real set
a mod m is complex real integer ext-real set
X is complex real integer ext-real set
m * X is complex real integer ext-real set
(m * X) + 0 is complex real integer ext-real Element of REAL
((m * X) + 0) mod m is complex real integer ext-real set
0 mod m is complex real integer ext-real set
a div m is complex real integer ext-real set
a / m is complex real ext-real set
m " is complex real ext-real set
a * (m ") is complex real ext-real set
[\(a / m)/] is complex real integer ext-real set
(a div m) * m is complex real integer ext-real set
((a div m) * m) + (a mod m) is complex real integer ext-real set
m is complex real integer ext-real set
a is complex real integer ext-real set
a div m is complex real integer ext-real set
a / m is complex real ext-real set
m " is complex real ext-real set
a * (m ") is complex real ext-real set
[\(a / m)/] is complex real integer ext-real set
(a div m) * m is complex real integer ext-real set
a mod m is complex real integer ext-real set
((a div m) * m) + (a mod m) is complex real integer ext-real set
m is complex real integer ext-real set
a is complex real integer ext-real set
m gcd a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m div (m gcd a) is complex real integer ext-real set
m / (m gcd a) is complex real ext-real set
(m gcd a) " is complex real ext-real non negative set
m * ((m gcd a) ") is complex real ext-real set
[\(m / (m gcd a))/] is complex real integer ext-real set
a div (m gcd a) is complex real integer ext-real set
a / (m gcd a) is complex real ext-real set
a * ((m gcd a) ") is complex real ext-real set
[\(a / (m gcd a))/] is complex real integer ext-real set
(a div (m gcd a)) * (m gcd a) is complex real integer ext-real set
X is complex real integer ext-real set
(m gcd a) * X is complex real integer ext-real set
x is complex real integer ext-real set
(m gcd a) * x is complex real integer ext-real set
(m div (m gcd a)) * (m gcd a) is complex real integer ext-real set
m is complex real integer ext-real set
a is complex real integer ext-real set
X is complex real integer ext-real set
m * X is complex real integer ext-real set
x is complex real integer ext-real set
m * x is complex real integer ext-real set
y is complex real integer ext-real set
X * y is complex real integer ext-real set
(m * X) * y is complex real integer ext-real set
m is complex real integer ext-real set
a is complex real integer ext-real set
m * a is complex real integer ext-real set
X is complex real integer ext-real set
x is complex real integer ext-real set
x - X is complex real integer ext-real set
- X is complex real integer ext-real set
x + (- X) is complex real integer ext-real set
y is complex real integer ext-real set
m * y is complex real integer ext-real set
(m * y) - (x - X) is complex real integer ext-real set
- (x - X) is complex real integer ext-real set
(m * y) + (- (x - X)) is complex real integer ext-real set
((m * y) - (x - X)) mod a is complex real integer ext-real set
X + (m * y) is complex real integer ext-real set
y1 is complex real integer ext-real set
y1 - X is complex real integer ext-real set
y1 + (- X) is complex real integer ext-real set
(y1 - X) mod m is complex real integer ext-real set
y1 - x is complex real integer ext-real set
- x is complex real integer ext-real set
y1 + (- x) is complex real integer ext-real set
(y1 - x) mod a is complex real integer ext-real set
(y1 - X) div m is complex real integer ext-real set
(y1 - X) / m is complex real ext-real set
m " is complex real ext-real set
(y1 - X) * (m ") is complex real ext-real set
[\((y1 - X) / m)/] is complex real integer ext-real set
((y1 - X) div m) * m is complex real integer ext-real set
(((y1 - X) div m) * m) + ((y1 - X) mod m) is complex real integer ext-real set
m * ((y1 - X) div m) is complex real integer ext-real set
(m * ((y1 - X) div m)) - (x - X) is complex real integer ext-real set
(m * ((y1 - X) div m)) + (- (x - X)) is complex real integer ext-real set
((m * ((y1 - X) div m)) - (x - X)) mod a is complex real integer ext-real set
(a) is Relation-like INT -defined INT -valued total reflexive symmetric transitive V71() V72() V73() Element of K6(K7(INT,INT))
Class ((a),y) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
[y,((y1 - X) div m)] is set
{y,((y1 - X) div m)} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{y} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{y,((y1 - X) div m)},{y}} is finite V38() set
((y1 - X) div m) - y is complex real integer ext-real set
- y is complex real integer ext-real set
((y1 - X) div m) + (- y) is complex real integer ext-real set
u9 is complex real integer ext-real set
a * u9 is complex real integer ext-real set
X + (((y1 - X) div m) * m) is complex real integer ext-real set
y + (a * u9) is complex real integer ext-real set
(y + (a * u9)) * m is complex real integer ext-real set
X + ((y + (a * u9)) * m) is complex real integer ext-real set
y * m is complex real integer ext-real set
X + (y * m) is complex real integer ext-real set
(m * a) * u9 is complex real integer ext-real set
(X + (y * m)) + ((m * a) * u9) is complex real integer ext-real set
y1 - (X + (y * m)) is complex real integer ext-real set
- (X + (y * m)) is complex real integer ext-real set
y1 + (- (X + (y * m))) is complex real integer ext-real set
y1 is complex real integer ext-real set
y1 - X is complex real integer ext-real set
y1 + (- X) is complex real integer ext-real set
(y1 - X) mod m is complex real integer ext-real set
y1 - x is complex real integer ext-real set
- x is complex real integer ext-real set
y1 + (- x) is complex real integer ext-real set
(y1 - x) mod a is complex real integer ext-real set
m is complex real integer ext-real set
a is complex real integer ext-real set
m gcd a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X is complex real integer ext-real set
x is complex real integer ext-real set
X - x is complex real integer ext-real set
- x is complex real integer ext-real set
X + (- x) is complex real integer ext-real set
y is complex real integer ext-real set
y - X is complex real integer ext-real set
- X is complex real integer ext-real set
y + (- X) is complex real integer ext-real set
(y - X) mod m is complex real integer ext-real set
y - x is complex real integer ext-real set
y + (- x) is complex real integer ext-real set
(y - x) mod a is complex real integer ext-real set
(y - x) - (y - X) is complex real integer ext-real set
- (y - X) is complex real integer ext-real set
(y - x) + (- (y - X)) is complex real integer ext-real set
m is complex real integer ext-real set
a is complex real integer ext-real set
m gcd a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m lcm a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m div (m gcd a) is complex real integer ext-real set
m / (m gcd a) is complex real ext-real set
(m gcd a) " is complex real ext-real non negative set
m * ((m gcd a) ") is complex real ext-real set
[\(m / (m gcd a))/] is complex real integer ext-real set
a div (m gcd a) is complex real integer ext-real set
a / (m gcd a) is complex real ext-real set
a * ((m gcd a) ") is complex real ext-real set
[\(a / (m gcd a))/] is complex real integer ext-real set
X is complex real integer ext-real set
x is complex real integer ext-real set
X - x is complex real integer ext-real set
- x is complex real integer ext-real set
X + (- x) is complex real integer ext-real set
(X - x) div (m gcd a) is complex real integer ext-real set
(X - x) / (m gcd a) is complex real ext-real set
(X - x) * ((m gcd a) ") is complex real ext-real set
[\((X - x) / (m gcd a))/] is complex real integer ext-real set
w9 is complex real integer ext-real set
(m div (m gcd a)) * w9 is complex real integer ext-real set
((m div (m gcd a)) * w9) - ((X - x) div (m gcd a)) is complex real integer ext-real set
- ((X - x) div (m gcd a)) is complex real integer ext-real set
((m div (m gcd a)) * w9) + (- ((X - x) div (m gcd a))) is complex real integer ext-real set
(((m div (m gcd a)) * w9) - ((X - x) div (m gcd a))) mod (a div (m gcd a)) is complex real integer ext-real set
m * w9 is complex real integer ext-real set
x + (m * w9) is complex real integer ext-real set
(m div (m gcd a)) * (m gcd a) is complex real integer ext-real set
(a div (m gcd a)) * (m gcd a) is complex real integer ext-real set
ll is complex real integer ext-real set
ll - x is complex real integer ext-real set
ll + (- x) is complex real integer ext-real set
(ll - x) mod m is complex real integer ext-real set
ll - X is complex real integer ext-real set
- X is complex real integer ext-real set
ll + (- X) is complex real integer ext-real set
(ll - X) mod a is complex real integer ext-real set
(ll - x) div m is complex real integer ext-real set
(ll - x) / m is complex real ext-real set
m " is complex real ext-real set
(ll - x) * (m ") is complex real ext-real set
[\((ll - x) / m)/] is complex real integer ext-real set
((ll - x) div m) * m is complex real integer ext-real set
(((ll - x) div m) * m) + ((ll - x) mod m) is complex real integer ext-real set
(m * w9) + x is complex real integer ext-real set
ll - ((m * w9) + x) is complex real integer ext-real set
- ((m * w9) + x) is complex real integer ext-real set
ll + (- ((m * w9) + x)) is complex real integer ext-real set
((ll - x) div m) - w9 is complex real integer ext-real set
- w9 is complex real integer ext-real set
((ll - x) div m) + (- w9) is complex real integer ext-real set
m * (((ll - x) div m) - w9) is complex real integer ext-real set
m * ((ll - x) div m) is complex real integer ext-real set
(m * ((ll - x) div m)) - (X - x) is complex real integer ext-real set
- (X - x) is complex real integer ext-real set
(m * ((ll - x) div m)) + (- (X - x)) is complex real integer ext-real set
((m * ((ll - x) div m)) - (X - x)) mod a is complex real integer ext-real set
(m gcd a) * (m div (m gcd a)) is complex real integer ext-real set
((m gcd a) * (m div (m gcd a))) * ((ll - x) div m) is complex real integer ext-real set
(m gcd a) * ((X - x) div (m gcd a)) is complex real integer ext-real set
(((m gcd a) * (m div (m gcd a))) * ((ll - x) div m)) - ((m gcd a) * ((X - x) div (m gcd a))) is complex real integer ext-real set
- ((m gcd a) * ((X - x) div (m gcd a))) is complex real integer ext-real set
(((m gcd a) * (m div (m gcd a))) * ((ll - x) div m)) + (- ((m gcd a) * ((X - x) div (m gcd a)))) is complex real integer ext-real set
(m gcd a) * (a div (m gcd a)) is complex real integer ext-real set
((((m gcd a) * (m div (m gcd a))) * ((ll - x) div m)) - ((m gcd a) * ((X - x) div (m gcd a)))) mod ((m gcd a) * (a div (m gcd a))) is complex real integer ext-real set
(m div (m gcd a)) * ((ll - x) div m) is complex real integer ext-real set
((m div (m gcd a)) * ((ll - x) div m)) - ((X - x) div (m gcd a)) is complex real integer ext-real set
((m div (m gcd a)) * ((ll - x) div m)) + (- ((X - x) div (m gcd a))) is complex real integer ext-real set
(((m div (m gcd a)) * ((ll - x) div m)) - ((X - x) div (m gcd a))) * (m gcd a) is complex real integer ext-real set
(((m div (m gcd a)) * ((ll - x) div m)) - ((X - x) div (m gcd a))) mod (a div (m gcd a)) is complex real integer ext-real set
((a div (m gcd a))) is Relation-like INT -defined INT -valued total reflexive symmetric transitive V71() V72() V73() Element of K6(K7(INT,INT))
Class (((a div (m gcd a))),((ll - x) div m)) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
[((ll - x) div m),w9] is set
{((ll - x) div m),w9} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{((ll - x) div m)} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{((ll - x) div m),w9},{((ll - x) div m)}} is finite V38() set
w is complex real integer ext-real set
(a div (m gcd a)) * w is complex real integer ext-real set
x + (((ll - x) div m) * m) is complex real integer ext-real set
((a div (m gcd a)) * w) + w9 is complex real integer ext-real set
(((a div (m gcd a)) * w) + w9) * m is complex real integer ext-real set
x + ((((a div (m gcd a)) * w) + w9) * m) is complex real integer ext-real set
w * (m div (m gcd a)) is complex real integer ext-real set
(w * (m div (m gcd a))) * a is complex real integer ext-real set
((m * w9) + x) + ((w * (m div (m gcd a))) * a) is complex real integer ext-real set
ll is complex real integer ext-real set
ll - x is complex real integer ext-real set
ll + (- x) is complex real integer ext-real set
(ll - x) mod m is complex real integer ext-real set
ll - X is complex real integer ext-real set
- X is complex real integer ext-real set
ll + (- X) is complex real integer ext-real set
(ll - X) mod a is complex real integer ext-real set
m is complex real integer ext-real set
a is complex real integer ext-real set
X is complex real integer ext-real set
X gcd m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
m div (X gcd m) is complex real integer ext-real set
m / (X gcd m) is complex real ext-real set
(X gcd m) " is complex real ext-real non negative set
m * ((X gcd m) ") is complex real ext-real set
[\(m / (X gcd m))/] is complex real integer ext-real set
X div (X gcd m) is complex real integer ext-real set
X / (X gcd m) is complex real ext-real set
X * ((X gcd m) ") is complex real ext-real set
[\(X / (X gcd m))/] is complex real integer ext-real set
x is complex real integer ext-real set
x div (X gcd m) is complex real integer ext-real set
x / (X gcd m) is complex real ext-real set
x * ((X gcd m) ") is complex real ext-real set
[\(x / (X gcd m))/] is complex real integer ext-real set
y is complex real integer ext-real set
y gcd a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a div (y gcd a) is complex real integer ext-real set
a / (y gcd a) is complex real ext-real set
(y gcd a) " is complex real ext-real non negative set
a * ((y gcd a) ") is complex real ext-real set
[\(a / (y gcd a))/] is complex real integer ext-real set
(m div (X gcd m)) * (a div (y gcd a)) is complex real integer ext-real set
y div (y gcd a) is complex real integer ext-real set
y / (y gcd a) is complex real ext-real set
y * ((y gcd a) ") is complex real ext-real set
[\(y / (y gcd a))/] is complex real integer ext-real set
y1 is complex real integer ext-real set
y1 div (y gcd a) is complex real integer ext-real set
y1 / (y gcd a) is complex real ext-real set
y1 * ((y gcd a) ") is complex real ext-real set
[\(y1 / (y gcd a))/] is complex real integer ext-real set
w9 is complex real integer ext-real set
(X div (X gcd m)) * w9 is complex real integer ext-real set
((X div (X gcd m)) * w9) - (x div (X gcd m)) is complex real integer ext-real set
- (x div (X gcd m)) is complex real integer ext-real set
((X div (X gcd m)) * w9) + (- (x div (X gcd m))) is complex real integer ext-real set
(((X div (X gcd m)) * w9) - (x div (X gcd m))) mod (m div (X gcd m)) is complex real integer ext-real set
(y1 div (y gcd a)) * (y gcd a) is complex real integer ext-real set
(y div (y gcd a)) * (y gcd a) is complex real integer ext-real set
(a div (y gcd a)) * (y gcd a) is complex real integer ext-real set
(x div (X gcd m)) * (X gcd m) is complex real integer ext-real set
(X div (X gcd m)) * (X gcd m) is complex real integer ext-real set
ll is complex real integer ext-real set
(y div (y gcd a)) * ll is complex real integer ext-real set
((y div (y gcd a)) * ll) - (y1 div (y gcd a)) is complex real integer ext-real set
- (y1 div (y gcd a)) is complex real integer ext-real set
((y div (y gcd a)) * ll) + (- (y1 div (y gcd a))) is complex real integer ext-real set
(((y div (y gcd a)) * ll) - (y1 div (y gcd a))) mod (a div (y gcd a)) is complex real integer ext-real set
(m div (X gcd m)) * (X gcd m) is complex real integer ext-real set
(m div (X gcd m)) gcd (a div (y gcd a)) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m gcd a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
ll - w9 is complex real integer ext-real set
- w9 is complex real integer ext-real set
ll + (- w9) is complex real integer ext-real set
w is complex real integer ext-real set
(m div (X gcd m)) * w is complex real integer ext-real set
((m div (X gcd m)) * w) - (ll - w9) is complex real integer ext-real set
- (ll - w9) is complex real integer ext-real set
((m div (X gcd m)) * w) + (- (ll - w9)) is complex real integer ext-real set
(((m div (X gcd m)) * w) - (ll - w9)) mod (a div (y gcd a)) is complex real integer ext-real set
w9 + ((m div (X gcd m)) * w) is complex real integer ext-real set
w is complex real integer ext-real set
X * w is complex real integer ext-real set
(X * w) - x is complex real integer ext-real set
- x is complex real integer ext-real set
(X * w) + (- x) is complex real integer ext-real set
((X * w) - x) mod m is complex real integer ext-real set
y * w is complex real integer ext-real set
(y * w) - y1 is complex real integer ext-real set
- y1 is complex real integer ext-real set
(y * w) + (- y1) is complex real integer ext-real set
((y * w) - y1) mod a is complex real integer ext-real set
(X div (X gcd m)) * w is complex real integer ext-real set
((X div (X gcd m)) * w) - (x div (X gcd m)) is complex real integer ext-real set
((X div (X gcd m)) * w) + (- (x div (X gcd m))) is complex real integer ext-real set
(((X div (X gcd m)) * w) - (x div (X gcd m))) * (X gcd m) is complex real integer ext-real set
(((X div (X gcd m)) * w) - (x div (X gcd m))) mod (m div (X gcd m)) is complex real integer ext-real set
((m div (X gcd m))) is Relation-like INT -defined INT -valued total reflexive symmetric transitive V71() V72() V73() Element of K6(K7(INT,INT))
Class (((m div (X gcd m))),w) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
[w,w9] is set
{w,w9} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{w} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{w,w9},{w}} is finite V38() set
w - w9 is complex real integer ext-real set
w + (- w9) is complex real integer ext-real set
(y div (y gcd a)) * w is complex real integer ext-real set
((y div (y gcd a)) * w) - (y1 div (y gcd a)) is complex real integer ext-real set
((y div (y gcd a)) * w) + (- (y1 div (y gcd a))) is complex real integer ext-real set
(((y div (y gcd a)) * w) - (y1 div (y gcd a))) * (y gcd a) is complex real integer ext-real set
(((y div (y gcd a)) * w) - (y1 div (y gcd a))) mod (a div (y gcd a)) is complex real integer ext-real set
((a div (y gcd a))) is Relation-like INT -defined INT -valued total reflexive symmetric transitive V71() V72() V73() Element of K6(K7(INT,INT))
Class (((a div (y gcd a))),w) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
[w,ll] is set
{w,ll} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{w,ll},{w}} is finite V38() set
w - ll is complex real integer ext-real set
- ll is complex real integer ext-real set
w + (- ll) is complex real integer ext-real set
((m div (X gcd m)) * w) + w9 is complex real integer ext-real set
(((m div (X gcd m)) * w) + w9) - ll is complex real integer ext-real set
(((m div (X gcd m)) * w) + w9) + (- ll) is complex real integer ext-real set
(w - ll) - ((((m div (X gcd m)) * w) + w9) - ll) is complex real integer ext-real set
- ((((m div (X gcd m)) * w) + w9) - ll) is complex real integer ext-real set
(w - ll) + (- ((((m div (X gcd m)) * w) + w9) - ll)) is complex real integer ext-real set
(w - w9) - ((m div (X gcd m)) * w) is complex real integer ext-real set
- ((m div (X gcd m)) * w) is complex real integer ext-real set
(w - w9) + (- ((m div (X gcd m)) * w)) is complex real integer ext-real set
w - (w9 + ((m div (X gcd m)) * w)) is complex real integer ext-real set
- (w9 + ((m div (X gcd m)) * w)) is complex real integer ext-real set
w + (- (w9 + ((m div (X gcd m)) * w))) is complex real integer ext-real set
w is complex real integer ext-real set
X * w is complex real integer ext-real set
(X * w) - x is complex real integer ext-real set
- x is complex real integer ext-real set
(X * w) + (- x) is complex real integer ext-real set
((X * w) - x) mod m is complex real integer ext-real set
y * w is complex real integer ext-real set
(y * w) - y1 is complex real integer ext-real set
- y1 is complex real integer ext-real set
(y * w) + (- y1) is complex real integer ext-real set
((y * w) - y1) mod a is complex real integer ext-real set
m is complex real integer ext-real set
a is complex real integer ext-real set
m * a is complex real integer ext-real set
X is complex real integer ext-real set
(m * a) * X is complex real integer ext-real set
x is complex real integer ext-real set
y is complex real integer ext-real set
y - x is complex real integer ext-real set
- x is complex real integer ext-real set
y + (- x) is complex real integer ext-real set
y1 is complex real integer ext-real set
y1 - x is complex real integer ext-real set
y1 + (- x) is complex real integer ext-real set
x1 is complex real integer ext-real set
m * x1 is complex real integer ext-real set
x + (m * x1) is complex real integer ext-real set
(m * x1) - (y - x) is complex real integer ext-real set
- (y - x) is complex real integer ext-real set
(m * x1) + (- (y - x)) is complex real integer ext-real set
((m * x1) - (y - x)) mod a is complex real integer ext-real set
y1 - (x + (m * x1)) is complex real integer ext-real set
- (x + (m * x1)) is complex real integer ext-real set
y1 + (- (x + (m * x1))) is complex real integer ext-real set
u9 is complex real integer ext-real set
(m * a) * u9 is complex real integer ext-real set
(x + (m * x1)) + ((m * a) * u9) is complex real integer ext-real set
((m * a) * u9) - (y1 - (x + (m * x1))) is complex real integer ext-real set
- (y1 - (x + (m * x1))) is complex real integer ext-real set
((m * a) * u9) + (- (y1 - (x + (m * x1)))) is complex real integer ext-real set
(((m * a) * u9) - (y1 - (x + (m * x1)))) mod X is complex real integer ext-real set
(y1 - x) - (m * x1) is complex real integer ext-real set
- (m * x1) is complex real integer ext-real set
(y1 - x) + (- (m * x1)) is complex real integer ext-real set
((m * a) * u9) - ((y1 - x) - (m * x1)) is complex real integer ext-real set
- ((y1 - x) - (m * x1)) is complex real integer ext-real set
((m * a) * u9) + (- ((y1 - x) - (m * x1))) is complex real integer ext-real set
(((m * a) * u9) - ((y1 - x) - (m * x1))) mod X is complex real integer ext-real set
w9 is complex real integer ext-real set
w9 - x is complex real integer ext-real set
w9 + (- x) is complex real integer ext-real set
(w9 - x) mod m is complex real integer ext-real set
w9 - y is complex real integer ext-real set
- y is complex real integer ext-real set
w9 + (- y) is complex real integer ext-real set
(w9 - y) mod a is complex real integer ext-real set
w9 - y1 is complex real integer ext-real set
- y1 is complex real integer ext-real set
w9 + (- y1) is complex real integer ext-real set
(w9 - y1) mod X is complex real integer ext-real set
w9 - (x + (m * x1)) is complex real integer ext-real set
w9 + (- (x + (m * x1))) is complex real integer ext-real set
(w9 - (x + (m * x1))) mod (m * a) is complex real integer ext-real set
w9 is complex real integer ext-real set
w9 - x is complex real integer ext-real set
w9 + (- x) is complex real integer ext-real set
(w9 - x) mod m is complex real integer ext-real set
w9 - y is complex real integer ext-real set
- y is complex real integer ext-real set
w9 + (- y) is complex real integer ext-real set
(w9 - y) mod a is complex real integer ext-real set
w9 - y1 is complex real integer ext-real set
- y1 is complex real integer ext-real set
w9 + (- y1) is complex real integer ext-real set
(w9 - y1) mod X is complex real integer ext-real set
m is complex real integer ext-real set
a is complex real integer ext-real set
X is complex real integer ext-real set
m gcd a is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
x is complex real integer ext-real set
y is complex real integer ext-real set
x - y is complex real integer ext-real set
- y is complex real integer ext-real set
x + (- y) is complex real integer ext-real set
m gcd X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
y1 is complex real integer ext-real set
x - y1 is complex real integer ext-real set
- y1 is complex real integer ext-real set
x + (- y1) is complex real integer ext-real set
a gcd X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
y - y1 is complex real integer ext-real set
y + (- y1) is complex real integer ext-real set
x1 is complex real integer ext-real set
x1 - x is complex real integer ext-real set
- x is complex real integer ext-real set
x1 + (- x) is complex real integer ext-real set
(x1 - x) mod m is complex real integer ext-real set
x1 - y is complex real integer ext-real set
x1 + (- y) is complex real integer ext-real set
(x1 - y) mod a is complex real integer ext-real set
x1 - y1 is complex real integer ext-real set
x1 + (- y1) is complex real integer ext-real set
(x1 - y1) mod X is complex real integer ext-real set
m is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative set
X is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative set
m gcd X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative set
a gcd X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(m gcd X) lcm (a gcd X) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m lcm a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(m lcm a) gcd X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
u9 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative set
x1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative set
prime_exponents x1 is Relation-like SetPrimes -defined RAT -valued Function-like total V71() V72() V73() V74() V189() set
support (prime_exponents x1) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(SetPrimes)
K6(SetPrimes) is V2() non finite set
prime_factorization x1 is Relation-like SetPrimes -defined RAT -valued Function-like total V71() V72() V73() V74() V189() set
w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(prime_factorization x1) . w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w9 |-count x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w9 |^ (w9 |-count x1) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
w9 |-count u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
prime_exponents u9 is Relation-like SetPrimes -defined RAT -valued Function-like total V71() V72() V73() V74() V189() set
(prime_exponents u9) . w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
prime_exponents m is Relation-like SetPrimes -defined RAT -valued Function-like total V71() V72() V73() V74() V189() set
prime_exponents a is Relation-like SetPrimes -defined RAT -valued Function-like total V71() V72() V73() V74() V189() set
max ((prime_exponents m),(prime_exponents a)) is Relation-like SetPrimes -defined RAT -valued Function-like total V71() V72() V73() V74() V189() set
(max ((prime_exponents m),(prime_exponents a))) . w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(prime_exponents m) . w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(prime_exponents a) . w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w9 |-count a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(prime_exponents m) . w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(prime_exponents a) . w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w9 |-count m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(prime_exponents m) . w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(prime_exponents a) . w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(prime_factorization x1) . w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w9 |-count x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w9 |-count X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w9 |^ (w9 |-count x1) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
w9 |^ (w9 |-count X) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
Product (prime_factorization x1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
support (prime_factorization x1) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(SetPrimes)
canFS (support (prime_factorization x1)) is Relation-like NAT -defined support (prime_factorization x1) -valued Function-like one-to-one V28( support (prime_factorization x1)) finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of support (prime_factorization x1)
(canFS (support (prime_factorization x1))) * (prime_factorization x1) is Relation-like NAT -defined RAT -valued Function-like finite V71() V72() V73() V74() set
w is Relation-like NAT -defined COMPLEX -valued Function-like finite FinSequence-like FinSubsequence-like V71() FinSequence of COMPLEX
Product w is complex Element of COMPLEX
rng w is finite complex-membered Element of K6(COMPLEX)
K6(COMPLEX) is V2() non finite set
rng (canFS (support (prime_factorization x1))) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(REAL)
w is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
dom w is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
c₁₄ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w . c₁₄ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w . x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(w . c₁₄) gcd (w . x) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
dom y is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
y . c₁₄ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y . x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(prime_factorization x1) . (y . x) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(y . x) |-count x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(y . x) |^ ((y . x) |-count x1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(prime_factorization x1) . (y . c₁₄) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(y . c₁₄) |-count x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(y . c₁₄) |^ ((y . c₁₄) |-count x1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c₁₄ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w . c₁₄ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() V74() FinSequence of NAT
dom y is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
y . c₁₄ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(prime_factorization x1) . (y . c₁₄) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m is complex real integer ext-real set
a is complex real integer ext-real set
m - a is complex real integer ext-real set
- a is complex real integer ext-real set
m + (- a) is complex real integer ext-real set
a - m is complex real integer ext-real set
- m is complex real integer ext-real set
a + (- m) is complex real integer ext-real set
X is complex real integer ext-real set
x is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative set
y is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative set
x gcd y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative set
x lcm y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(x lcm y) lcm y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x div (x gcd y) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x / (x gcd y) is complex real ext-real non negative set
(x gcd y) " is complex real ext-real non negative set
x * ((x gcd y) ") is complex real ext-real non negative set
[\(x / (x gcd y))/] is complex real integer ext-real set
(a - m) div (x gcd y) is complex real integer ext-real set
(a - m) / (x gcd y) is complex real ext-real set
(a - m) * ((x gcd y) ") is complex real ext-real set
[\((a - m) / (x gcd y))/] is complex real integer ext-real set
y div (x gcd y) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y / (x gcd y) is complex real ext-real non negative set
y * ((x gcd y) ") is complex real ext-real non negative set
[\(y / (x gcd y))/] is complex real integer ext-real set
(x lcm y) gcd y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(x lcm y) div ((x lcm y) gcd y1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(x lcm y) / ((x lcm y) gcd y1) is complex real ext-real non negative set
((x lcm y) gcd y1) " is complex real ext-real non negative set
(x lcm y) * (((x lcm y) gcd y1) ") is complex real ext-real non negative set
[\((x lcm y) / ((x lcm y) gcd y1))/] is complex real integer ext-real set
y1 div ((x lcm y) gcd y1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 / ((x lcm y) gcd y1) is complex real ext-real non negative set
y1 * (((x lcm y) gcd y1) ") is complex real ext-real non negative set
[\(y1 / ((x lcm y) gcd y1))/] is complex real integer ext-real set
x gcd y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y gcd y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
- (m - a) is complex real integer ext-real set
w is complex real integer ext-real set
x * w is complex real integer ext-real set
m + (x * w) is complex real integer ext-real set
(x div (x gcd y)) * w is complex real integer ext-real set
((x div (x gcd y)) * w) - ((a - m) div (x gcd y)) is complex real integer ext-real set
- ((a - m) div (x gcd y)) is complex real integer ext-real set
((x div (x gcd y)) * w) + (- ((a - m) div (x gcd y))) is complex real integer ext-real set
(((x div (x gcd y)) * w) - ((a - m) div (x gcd y))) mod (y div (x gcd y)) is complex real integer ext-real set
X - (m + (x * w)) is complex real integer ext-real set
- (m + (x * w)) is complex real integer ext-real set
X + (- (m + (x * w))) is complex real integer ext-real set
(X - (m + (x * w))) div ((x lcm y) gcd y1) is complex real integer ext-real set
(X - (m + (x * w))) / ((x lcm y) gcd y1) is complex real ext-real set
(X - (m + (x * w))) * (((x lcm y) gcd y1) ") is complex real ext-real set
[\((X - (m + (x * w))) / ((x lcm y) gcd y1))/] is complex real integer ext-real set
c₁₄ is complex real integer ext-real set
((x lcm y) div ((x lcm y) gcd y1)) * c₁₄ is complex real integer ext-real set
(((x lcm y) div ((x lcm y) gcd y1)) * c₁₄) - ((X - (m + (x * w))) div ((x lcm y) gcd y1)) is complex real integer ext-real set
- ((X - (m + (x * w))) div ((x lcm y) gcd y1)) is complex real integer ext-real set
(((x lcm y) div ((x lcm y) gcd y1)) * c₁₄) + (- ((X - (m + (x * w))) div ((x lcm y) gcd y1))) is complex real integer ext-real set
((((x lcm y) div ((x lcm y) gcd y1)) * c₁₄) - ((X - (m + (x * w))) div ((x lcm y) gcd y1))) mod (y1 div ((x lcm y) gcd y1)) is complex real integer ext-real set
(x lcm y) * c₁₄ is complex real integer ext-real set
(m + (x * w)) + ((x lcm y) * c₁₄) is complex real integer ext-real set
(m + (x * w)) - X is complex real integer ext-real set
- X is complex real integer ext-real set
(m + (x * w)) + (- X) is complex real integer ext-real set
x is complex real integer ext-real set
x - m is complex real integer ext-real set
x + (- m) is complex real integer ext-real set
(x - m) mod x is complex real integer ext-real set
x - a is complex real integer ext-real set
x + (- a) is complex real integer ext-real set
(x - a) mod y is complex real integer ext-real set
x - X is complex real integer ext-real set
x + (- X) is complex real integer ext-real set
(x - X) mod y1 is complex real integer ext-real set
x - (m + (x * w)) is complex real integer ext-real set
x + (- (m + (x * w))) is complex real integer ext-real set
- (x - (m + (x * w))) is complex real integer ext-real set
(m + (x * w)) - x is complex real integer ext-real set
- x is complex real integer ext-real set
(m + (x * w)) + (- x) is complex real integer ext-real set
w is complex real integer ext-real set
x * w is complex real integer ext-real set
t2 is complex real integer ext-real set
y * t2 is complex real integer ext-real set
(x - X) + (y * t2) is complex real integer ext-real set
(x - X) + (x * w) is complex real integer ext-real set
(x gcd y1) lcm (y gcd y1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is complex real integer ext-real set
x - m is complex real integer ext-real set
x + (- m) is complex real integer ext-real set
(x - m) mod x is complex real integer ext-real set
x - a is complex real integer ext-real set
x + (- a) is complex real integer ext-real set
(x - a) mod y is complex real integer ext-real set
x - X is complex real integer ext-real set
x + (- X) is complex real integer ext-real set
(x - X) mod y1 is complex real integer ext-real set
- ((m + (x * w)) - X) is complex real integer ext-real set
w is complex real integer ext-real set
(x lcm y) * w is complex real integer ext-real set
(m + (x * w)) + ((x lcm y) * w) is complex real integer ext-real set
((x lcm y) div ((x lcm y) gcd y1)) * w is complex real integer ext-real set
(((x lcm y) div ((x lcm y) gcd y1)) * w) - ((X - (m + (x * w))) div ((x lcm y) gcd y1)) is complex real integer ext-real set
(((x lcm y) div ((x lcm y) gcd y1)) * w) + (- ((X - (m + (x * w))) div ((x lcm y) gcd y1))) is complex real integer ext-real set
((((x lcm y) div ((x lcm y) gcd y1)) * w) - ((X - (m + (x * w))) div ((x lcm y) gcd y1))) mod (y1 div ((x lcm y) gcd y1)) is complex real integer ext-real set
(y1 div ((x lcm y) gcd y1)) * ((x lcm y) gcd y1) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
((y1 div ((x lcm y) gcd y1))) is Relation-like INT -defined INT -valued total reflexive symmetric transitive V71() V72() V73() Element of K6(K7(INT,INT))
Class (((y1 div ((x lcm y) gcd y1))),c₁₄) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
[c₁₄,w] is set
{c₁₄,w} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{c₁₄} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{c₁₄,w},{c₁₄}} is finite V38() set
(x lcm y) * (y1 div ((x lcm y) gcd y1)) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
((x lcm y) div ((x lcm y) gcd y1)) * ((x lcm y) gcd y1) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(((x lcm y) div ((x lcm y) gcd y1)) * ((x lcm y) gcd y1)) * (y1 div ((x lcm y) gcd y1)) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
y1 * ((x lcm y) div ((x lcm y) gcd y1)) is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
((x lcm y) * c₁₄) - ((x lcm y) * w) is complex real integer ext-real set
- ((x lcm y) * w) is complex real integer ext-real set
((x lcm y) * c₁₄) + (- ((x lcm y) * w)) is complex real integer ext-real set
c₁₄ - w is complex real integer ext-real set
- w is complex real integer ext-real set
c₁₄ + (- w) is complex real integer ext-real set
(x lcm y) * (c₁₄ - w) is complex real integer ext-real set
((x lcm y) * c₁₄) + (m + (x * w)) is complex real integer ext-real set
((x lcm y) * w) + (m + (x * w)) is complex real integer ext-real set
(((x lcm y) * c₁₄) + (m + (x * w))) - (((x lcm y) * w) + (m + (x * w))) is complex real integer ext-real set
- (((x lcm y) * w) + (m + (x * w))) is complex real integer ext-real set
(((x lcm y) * c₁₄) + (m + (x * w))) + (- (((x lcm y) * w) + (m + (x * w)))) is complex real integer ext-real set
x - (m + (x * w)) is complex real integer ext-real set
x + (- (m + (x * w))) is complex real integer ext-real set
(x - (m + (x * w))) mod (x lcm y) is complex real integer ext-real set
x is complex real integer ext-real set
x - m is complex real integer ext-real set
x + (- m) is complex real integer ext-real set
(x - m) mod x is complex real integer ext-real set
x - a is complex real integer ext-real set
x + (- a) is complex real integer ext-real set
(x - a) mod y is complex real integer ext-real set
x - X is complex real integer ext-real set
x + (- X) is complex real integer ext-real set
(x - X) mod y1 is complex real integer ext-real set
m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : not m <= b₁ } is set
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom a is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
a . X is set
X -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() FinSequence of INT
rng X is finite complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(REAL)
y is set
dom X is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
y1 is set
X . y1 is complex real integer ext-real set
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg m is finite m -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= m ) } is set
x1 - 1 is complex real integer ext-real Element of REAL
- 1 is complex real integer ext-real non positive set
x1 + (- 1) is complex real integer ext-real set
x1 -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
u9 is complex real integer ext-real set
y is set
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
dom X is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
X . (y1 + 1) is complex real integer ext-real set
(y1 + 1) -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom X is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
(m) is Relation-like INT -defined INT -valued total reflexive symmetric transitive V71() V72() V73() Element of K6(K7(INT,INT))
x is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
X . x is complex real integer ext-real set
x -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Class ((m),(x -' 1)) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
[(x -' 1),(x -' 1)] is set
{(x -' 1),(x -' 1)} is finite V38() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{(x -' 1)} is non empty V2() finite V38() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(x -' 1),(x -' 1)},{(x -' 1)}} is finite V38() set
m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(m) is Relation-like INT -defined INT -valued total reflexive symmetric transitive V71() V72() V73() Element of K6(K7(INT,INT))
a is finite set
card a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() FinSequence of INT
rng X is finite complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(REAL)
len X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom X is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
x is complex real integer ext-real set
y is complex real integer ext-real set
[x,y] is set
{x,y} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{x} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{x,y},{x}} is finite V38() set
y1 is set
X . y1 is complex real integer ext-real set
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x1 -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Class ((m),(x1 -' 1)) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
[(x1 -' 1),x] is set
{(x1 -' 1),x} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{(x1 -' 1)} is non empty V2() finite V38() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(x1 -' 1),x},{(x1 -' 1)}} is finite V38() set
u9 is set
X . u9 is complex real integer ext-real set
w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg m is finite m -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= m ) } is set
w9 -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Class ((m),(w9 -' 1)) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
[(w9 -' 1),y] is set
{(w9 -' 1),y} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{(w9 -' 1)} is non empty V2() finite V38() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(w9 -' 1),y},{(w9 -' 1)}} is finite V38() set
(x1 -' 1) - (w9 -' 1) is complex real integer ext-real set
- (w9 -' 1) is complex real integer ext-real non positive set
(x1 -' 1) + (- (w9 -' 1)) is complex real integer ext-real set
1 - m is complex real integer ext-real Element of REAL
- m is complex real integer ext-real non positive set
1 + (- m) is complex real integer ext-real set
x1 - w9 is complex real integer ext-real Element of REAL
- w9 is complex real integer ext-real non positive set
x1 + (- w9) is complex real integer ext-real set
- m is complex real integer ext-real non positive Element of REAL
m - 1 is complex real integer ext-real Element of REAL
- 1 is complex real integer ext-real non positive set
m + (- 1) is complex real integer ext-real set
abs (x1 - w9) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
abs m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x1 - 1 is complex real integer ext-real Element of REAL
x1 + (- 1) is complex real integer ext-real set
(x1 - 1) - (w9 -' 1) is complex real integer ext-real Element of REAL
(x1 - 1) + (- (w9 -' 1)) is complex real integer ext-real set
w9 - 1 is complex real integer ext-real Element of REAL
w9 + (- 1) is complex real integer ext-real set
(x1 - 1) - (w9 - 1) is complex real integer ext-real Element of REAL
- (w9 - 1) is complex real integer ext-real set
(x1 - 1) + (- (w9 - 1)) is complex real integer ext-real set
x is set
y is set
X . x is complex real integer ext-real set
X . y is complex real integer ext-real set
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg m is finite m -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= m ) } is set
y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X . y1 is complex real integer ext-real set
X . x1 is complex real integer ext-real set
x1 -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Class ((m),(x1 -' 1)) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
[(x1 -' 1),(X . x1)] is set
{(x1 -' 1),(X . x1)} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{(x1 -' 1)} is non empty V2() finite V38() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(x1 -' 1),(X . x1)},{(x1 -' 1)}} is finite V38() set
w9 is complex real integer V31() ext-real Element of INT
u9 is complex real integer V31() ext-real Element of INT
y1 -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(y1 -' 1) - (x1 -' 1) is complex real integer ext-real set
- (x1 -' 1) is complex real integer ext-real non positive set
(y1 -' 1) + (- (x1 -' 1)) is complex real integer ext-real set
y1 - 1 is complex real integer ext-real Element of REAL
- 1 is complex real integer ext-real non positive set
y1 + (- 1) is complex real integer ext-real set
(y1 - 1) - (x1 -' 1) is complex real integer ext-real Element of REAL
(y1 - 1) + (- (x1 -' 1)) is complex real integer ext-real set
x1 - 1 is complex real integer ext-real Element of REAL
x1 + (- 1) is complex real integer ext-real set
(y1 - 1) - (x1 - 1) is complex real integer ext-real Element of REAL
- (x1 - 1) is complex real integer ext-real set
(y1 - 1) + (- (x1 - 1)) is complex real integer ext-real set
y1 - x1 is complex real integer ext-real Element of REAL
- x1 is complex real integer ext-real non positive set
y1 + (- x1) is complex real integer ext-real set
1 - m is complex real integer ext-real Element of REAL
- m is complex real integer ext-real non positive set
1 + (- m) is complex real integer ext-real set
- m is complex real integer ext-real non positive Element of REAL
m - 1 is complex real integer ext-real Element of REAL
m + (- 1) is complex real integer ext-real set
abs (y1 - x1) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
abs m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Class ((m),(y1 -' 1)) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
[(y1 -' 1),(X . y1)] is set
{(y1 -' 1),(X . y1)} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{(y1 -' 1)} is non empty V2() finite V38() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(y1 -' 1),(X . y1)},{(y1 -' 1)}} is finite V38() set
x is complex real integer ext-real set
y is complex real integer ext-real set
[x,y] is set
{x,y} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{x} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{x,y},{x}} is finite V38() set
m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
<*> INT is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined INT -valued Function-like one-to-one constant functional integer finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() FinSequence of INT
len (<*> INT) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer V31() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() Element of NAT
rng (<*> INT) is empty V2() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V59() V71() V72() V73() V74() V75() V76() V77() V78() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() Element of K6(REAL)
dom (<*> INT) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() Element of K6(NAT)
(m) is Relation-like INT -defined INT -valued total reflexive symmetric transitive V71() V72() V73() Element of K6(K7(INT,INT))
X is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
(<*> INT) . X is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer V31() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() Element of NAT
X -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Class ((m),(X -' 1)) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is finite set
card a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real positive non negative Element of REAL
x is finite set
card x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y is set
{y} is non empty V2() finite 1 -element set
x \ {y} is finite Element of K6(x)
K6(x) is finite V38() set
card (x \ {y}) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
card {y} is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(card x) - (card {y}) is complex real integer ext-real set
- (card {y}) is complex real integer ext-real non positive set
(card x) + (- (card {y})) is complex real integer ext-real set
(X + 1) - 1 is complex real integer ext-real Element of REAL
- 1 is complex real integer ext-real non positive set
(X + 1) + (- 1) is complex real integer ext-real set
x1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom x1 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
<*y*> is non empty V2() Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,y] is set
{1,y} is finite set
{{1,y},{1}} is finite V38() set
{[1,y]} is non empty V2() Relation-like Function-like constant finite 1 -element set
x1 ^ <*y*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (x1 ^ <*y*>) is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom (x1 ^ <*y*>) is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
w9 is set
ll is set
(x1 ^ <*y*>) . w9 is set
(x1 ^ <*y*>) . ll is set
Seg (X + 1) is non empty finite X + 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= X + 1 ) } is set
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg X is finite X -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= X ) } is set
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(x1 ^ <*y*>) . w is set
x1 . w is set
(x1 ^ <*y*>) . w is set
x1 . w is set
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x1 . w is set
(x1 ^ <*y*>) . w is set
(x1 ^ <*y*>) . w is set
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg X is finite X -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= X ) } is set
x1 . w is set
(x1 ^ <*y*>) . w is set
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Seg X is finite X -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= X ) } is set
w9 is set
ll is set
(x1 ^ <*y*>) . w9 is set
(x1 ^ <*y*>) . ll is set
w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(x1 ^ <*y*>) . w9 is set
Seg (X + 1) is non empty finite X + 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= X + 1 ) } is set
Seg X is finite X -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= X ) } is set
x1 . w9 is set
Seg X is finite X -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= X ) } is set
w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(x1 ^ <*y*>) . w9 is set
<*> NAT is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional integer finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() FinSequence of NAT
x is finite set
card x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len (<*> NAT) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer V31() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() Element of NAT
dom (<*> NAT) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() Element of K6(NAT)
y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(<*> NAT) . y is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V71() V72() V73() V74() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V87() set
m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(m) is Relation-like INT -defined INT -valued total reflexive symmetric transitive V71() V72() V73() Element of K6(K7(INT,INT))
a is finite complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
card a is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
X is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
Seg m is finite m -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : ( 1 <= b₁ & b₁ <= m ) } is set
Segm m is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
y is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
y -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Class ((m),(y -' 1)) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
y - 1 is complex real integer ext-real Element of REAL
- 1 is complex real integer ext-real non positive set
y + (- 1) is complex real integer ext-real set
y1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len y1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom y1 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
y1 . x1 is set
x1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() FinSequence of X
u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x1 . u9 is complex real integer ext-real set
w9 is complex real integer ext-real set
m * w9 is complex real integer ext-real Element of REAL
ll is complex real integer ext-real set
(m * w9) + ll is complex real integer ext-real Element of REAL
(x1 . u9) mod m is complex real integer ext-real set
ll mod m is complex real integer ext-real set
[ll,(x1 . u9)] is set
{ll,(x1 . u9)} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{ll} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{ll,(x1 . u9)},{ll}} is finite V38() set
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative Element of Segm m
Class ((m),w) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
u9 is non empty set
w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
x1 . w9 is complex real integer ext-real set
w9 is Relation-like NAT -defined u9 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of u9
dom w9 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
ll is set
w is set
w9 . ll is set
w9 . w is set
x1 . ll is complex real integer ext-real set
Class ((m),(w9 . ll)) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
x1 . w is complex real integer ext-real set
[(x1 . ll),(x1 . w)] is set
{(x1 . ll),(x1 . w)} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{(x1 . ll)} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{(x1 . ll),(x1 . w)},{(x1 . ll)}} is finite V38() set
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom x1 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
x1 . w is complex real integer ext-real set
y is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x1 . y is complex real integer ext-real set
rng w9 is finite Element of K6(u9)
K6(u9) is set
card (rng w9) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
len w9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
ll is finite set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT : not m <= b₁ } is set
card ll is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
w is set
w9 . w is set
w is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
dom x1 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
x1 . w is complex real integer ext-real set
y is complex real integer V31() ext-real Element of X
x is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like V71() V72() V73() FinSequence of X
dom x is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K6(NAT)
rng x is finite complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(REAL)
len x is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y is set
y1 is set
x . y is complex real integer ext-real set
x . y1 is complex real integer ext-real set
u9 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x1 -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
u9 -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(x1 -' 1) - (u9 -' 1) is complex real integer ext-real set
- (u9 -' 1) is complex real integer ext-real non positive set
(x1 -' 1) + (- (u9 -' 1)) is complex real integer ext-real set
x1 - 1 is complex real integer ext-real Element of REAL
- 1 is complex real integer ext-real non positive set
x1 + (- 1) is complex real integer ext-real set
(x1 - 1) - (u9 -' 1) is complex real integer ext-real Element of REAL
(x1 - 1) + (- (u9 -' 1)) is complex real integer ext-real set
u9 - 1 is complex real integer ext-real Element of REAL
u9 + (- 1) is complex real integer ext-real set
(x1 - 1) - (u9 - 1) is complex real integer ext-real Element of REAL
- (u9 - 1) is complex real integer ext-real set
(x1 - 1) + (- (u9 - 1)) is complex real integer ext-real set
x1 - u9 is complex real integer ext-real Element of REAL
- u9 is complex real integer ext-real non positive set
x1 + (- u9) is complex real integer ext-real set
x . x1 is complex real integer ext-real set
x . u9 is complex real integer ext-real set
Class ((m),(u9 -' 1)) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
[(u9 -' 1),(x . u9)] is set
{(u9 -' 1),(x . u9)} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{(u9 -' 1)} is non empty V2() finite V38() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(u9 -' 1),(x . u9)},{(u9 -' 1)}} is finite V38() set
ll is complex real integer V31() ext-real Element of INT
w9 is complex real integer V31() ext-real Element of INT
1 - m is complex real integer ext-real Element of REAL
- m is complex real integer ext-real non positive set
1 + (- m) is complex real integer ext-real set
- m is complex real integer ext-real non positive Element of REAL
m - 1 is complex real integer ext-real Element of REAL
m + (- 1) is complex real integer ext-real set
abs (x1 - u9) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
abs m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
Class ((m),(x1 -' 1)) is complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
[(x1 -' 1),(x . x1)] is set
{(x1 -' 1),(x . x1)} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{(x1 -' 1)} is non empty V2() finite V38() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(x1 -' 1),(x . x1)},{(x1 -' 1)}} is finite V38() set
card X is non empty epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
card (rng x) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is complex real integer ext-real set
X is finite complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
a ++ X is finite complex-membered ext-real-membered real-membered Element of K6(REAL)
card X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
card (a ++ X) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(m) is Relation-like INT -defined INT -valued total reflexive symmetric transitive V71() V72() V73() Element of K6(K7(INT,INT))
x is complex real integer ext-real set
y is complex real integer ext-real set
[x,y] is set
{x,y} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{x} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{x,y},{x}} is finite V38() set
y1 is complex Element of COMPLEX
a + y1 is set
x1 is complex Element of COMPLEX
a + x1 is set
u9 is complex real integer ext-real set
a + u9 is complex real integer ext-real set
w9 is complex real integer ext-real set
a + w9 is complex real integer ext-real set
(a + u9) - (a + w9) is complex real integer ext-real set
- (a + w9) is complex real integer ext-real set
(a + u9) + (- (a + w9)) is complex real integer ext-real set
u9 - w9 is complex real integer ext-real set
- w9 is complex real integer ext-real set
u9 + (- w9) is complex real integer ext-real set
[u9,w9] is set
{u9,w9} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{u9} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{u9,w9},{u9}} is finite V38() set
m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a is complex real integer ext-real set
X is finite complex-membered ext-real-membered real-membered rational-membered integer-membered Element of K6(INT)
a ** X is finite complex-membered ext-real-membered real-membered Element of K6(REAL)
card X is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
a gcd m is epsilon-transitive epsilon-connected ordinal natural complex real integer finite cardinal ext-real non negative set
abs m is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is set
{x} is non empty V2() finite 1 -element set
(m) is Relation-like INT -defined INT -valued total reflexive symmetric transitive V71() V72() V73() Element of K6(K7(INT,INT))
x is complex real integer ext-real set
y is complex real integer ext-real set
[x,y] is set
{x,y} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{x} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{x,y},{x}} is finite V38() set
card (a ** X) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(m) is Relation-like INT -defined INT -valued total reflexive symmetric transitive V71() V72() V73() Element of K6(K7(INT,INT))
x is complex real integer ext-real set
y is complex real integer ext-real set
[x,y] is set
{x,y} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{x} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{x,y},{x}} is finite V38() set
y1 is complex real integer ext-real set
a * y1 is complex real integer ext-real set
x1 is complex real integer ext-real set
a * x1 is complex real integer ext-real set
[x1,y1] is set
{x1,y1} is finite complex-membered ext-real-membered real-membered rational-membered integer-membered set
{x1} is non empty V2() finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered set
{{x1,y1},{x1}} is finite V38() set
card (a ** X) is epsilon-transitive epsilon-connected ordinal natural complex real integer V31() finite cardinal ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT