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

{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

{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