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)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real 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 <= b1 & b1 <= 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)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real 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 <= b1 & b1 <= 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