:: EULER_1 semantic presentation

REAL is set
NAT is non empty non trivial V27() V28() V29() non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set

NAT is non empty non trivial V27() V28() V29() non finite cardinal limit_cardinal set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
{} is set

1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
2 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
3 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
0 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real V34() V35() integer set
X / X is ext-real V34() V35() set
[\(X / X)/] is ext-real V34() V35() integer set
[\(X / X)/] + 1 is ext-real V34() V35() integer set
[\(X / X)/] * X is ext-real V34() V35() integer set
X - ([\(X / X)/] * X) is ext-real V34() V35() integer set
- 1 is ext-real non positive V34() V35() integer set
(X / X) + (- 1) is ext-real V34() V35() set
([\(X / X)/] + 1) + (- 1) is ext-real V34() V35() integer set
(X / X) - 1 is ext-real V34() V35() set
((X / X) - 1) * X is ext-real V34() V35() set
- ([\(X / X)/] * X) is ext-real V34() V35() integer set
- (((X / X) - 1) * X) is ext-real V34() V35() set
X + (- ([\(X / X)/] * X)) is ext-real V34() V35() integer set
X + (- (((X / X) - 1) * X)) is ext-real V34() V35() set
(X / X) * X is ext-real V34() V35() set
1 * X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
((X / X) * X) - (1 * X) is ext-real V34() V35() set
X - (((X / X) * X) - (1 * X)) is ext-real V34() V35() set
X - X is ext-real V34() V35() integer set
X - (X - X) is ext-real V34() V35() integer set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
is non empty trivial finite V42() 1 -element set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
{ b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( X,b1 are_relative_prime & 1 <= b1 & b1 <= X ) } is set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X is finite set
card X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X is set
{X} is non empty trivial finite 1 -element set
X \ {X} is finite Element of bool X
bool X is non empty finite V42() set
card (X \ {X}) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
card {X} is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(card X) - () is ext-real V34() V35() integer set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(X * m) gcd (X * m) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
n is ext-real V34() V35() integer set
X is ext-real V34() V35() integer set
abs m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
abs (abs m) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
m * X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(X * X) gcd (m * X) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
0 * X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
n is ext-real V34() V35() integer set
((X * X) gcd (m * X)) * n is ext-real V34() V35() integer set
X is ext-real V34() V35() integer set
((X * X) gcd (m * X)) * X is ext-real V34() V35() integer set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X + X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(X + X) gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
1 + 0 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X + (X * m) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(X + (X * m)) gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X + (X * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(X + (X * n)) gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
n + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X * (n + 1) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X + (X * (n + 1)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(X + (X * (n + 1))) gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * (n + 1) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X + (X * (n + 1)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(X + (X * (n + 1))) gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(X + (X * n)) div (X gcd X) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(X gcd X) * ((X + (X * n)) div (X gcd X)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
0 gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * (n + 1) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X + (X * (n + 1)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(X + (X * (n + 1))) gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X div (X gcd X) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(X gcd X) * (X div (X gcd X)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
((X + (X * n)) div (X gcd X)) * (X gcd X) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(X div (X gcd X)) * (X gcd X) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(((X + (X * n)) div (X gcd X)) * (X gcd X)) gcd ((X div (X gcd X)) * (X gcd X)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
((X + (X * n)) div (X gcd X)) gcd (X div (X gcd X)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
((X + (X * n)) div (X gcd X)) + (X div (X gcd X)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(((X + (X * n)) div (X gcd X)) + (X div (X gcd X))) gcd (X div (X gcd X)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * (n + 1) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X + (X * (n + 1)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(X + (X * (n + 1))) gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(X + (X * n)) + X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
((X + (X * n)) + X) gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
((X gcd X) * ((X + (X * n)) div (X gcd X))) + ((X gcd X) * (X div (X gcd X))) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(((X gcd X) * ((X + (X * n)) div (X gcd X))) + ((X gcd X) * (X div (X gcd X)))) gcd ((X gcd X) * (X div (X gcd X))) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(X gcd X) * (((X + (X * n)) div (X gcd X)) + (X div (X gcd X))) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
((X gcd X) * (((X + (X * n)) div (X gcd X)) + (X div (X gcd X)))) gcd ((X gcd X) * (X div (X gcd X))) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * (n + 1) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X + (X * (n + 1)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(X + (X * (n + 1))) gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * (n + 1) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X + (X * (n + 1)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(X + (X * (n + 1))) gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * (n + 1) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X + (X * (n + 1)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(X + (X * (n + 1))) gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * (n + 1) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X + (X * (n + 1)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(X + (X * (n + 1))) gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * 0 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X + (X * 0) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(X + (X * 0)) gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
1 * X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
1 * X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(1 * X) + (1 * X) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
n is ext-real V34() V35() integer set
n * X is ext-real V34() V35() integer set
X is ext-real V34() V35() integer set
X * X is ext-real V34() V35() integer set
(n * X) + (X * X) is ext-real V34() V35() integer set
n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real V34() V35() integer set
X * X is ext-real V34() V35() integer set
C is ext-real V34() V35() integer set
C * X is ext-real V34() V35() integer set
(X * X) + (C * X) is ext-real V34() V35() integer set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
C is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
C is ext-real V34() V35() integer set
C * X is ext-real V34() V35() integer set
A is ext-real V34() V35() integer set
A * X is ext-real V34() V35() integer set
(C * X) + (A * X) is ext-real V34() V35() integer set
C is ext-real V34() V35() integer set
C * X is ext-real V34() V35() integer set
A is ext-real V34() V35() integer set
A * X is ext-real V34() V35() integer set
(C * X) + (A * X) is ext-real V34() V35() integer set
A is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
A mod X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
B is ext-real V34() V35() integer set
B * X is ext-real V34() V35() integer set
B is ext-real V34() V35() integer set
B * X is ext-real V34() V35() integer set
(B * X) + (B * X) is ext-real V34() V35() integer set
B is ext-real V34() V35() integer set
B * X is ext-real V34() V35() integer set
B is ext-real V34() V35() integer set
B * X is ext-real V34() V35() integer set
(B * X) + (B * X) is ext-real V34() V35() integer set
A div X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(A div X) * A is ext-real V34() V35() integer set
B - ((A div X) * A) is ext-real V34() V35() integer set
(A div X) * C is ext-real V34() V35() integer set
B - ((A div X) * C) is ext-real V34() V35() integer set
X * (A div X) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(A mod X) + (X * (A div X)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
((A mod X) + (X * (A div X))) - (X * (A div X)) is ext-real V34() V35() integer set
A - (X * (A div X)) is ext-real V34() V35() integer set
(B - ((A div X) * C)) * X is ext-real V34() V35() integer set
(B - ((A div X) * A)) * X is ext-real V34() V35() integer set
((B - ((A div X) * C)) * X) + ((B - ((A div X) * A)) * X) is ext-real V34() V35() integer set
C is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
n is ext-real V34() V35() integer set
n * X is ext-real V34() V35() integer set
m is ext-real V34() V35() integer set
m * X is ext-real V34() V35() integer set
(n * X) + (m * X) is ext-real V34() V35() integer set
X mod X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X div X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X * (X div X) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(X * (X div X)) + 0 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
A is ext-real V34() V35() integer set
A * X is ext-real V34() V35() integer set
B is ext-real V34() V35() integer set
B * X is ext-real V34() V35() integer set
(A * X) + (B * X) is ext-real V34() V35() integer set
m is ext-real V34() V35() integer set
m * X is ext-real V34() V35() integer set
n is ext-real V34() V35() integer set
n * X is ext-real V34() V35() integer set
(m * X) + (n * X) is ext-real V34() V35() integer set
X mod X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X div X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X * (X div X) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(X * (X div X)) + 0 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
A is ext-real V34() V35() integer set
A * X is ext-real V34() V35() integer set
B is ext-real V34() V35() integer set
B * X is ext-real V34() V35() integer set
(A * X) + (B * X) is ext-real V34() V35() integer set
X gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
A is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * A is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
C * ((C * X) + (A * X)) is ext-real V34() V35() integer set
C * C is ext-real V34() V35() integer set
(C * C) * X is ext-real V34() V35() integer set
C * (A * X) is ext-real V34() V35() integer set
((C * C) * X) + (C * (A * X)) is ext-real V34() V35() integer set
C * A is ext-real V34() V35() integer set
(C * A) * X is ext-real V34() V35() integer set
((C * C) * X) + ((C * A) * X) is ext-real V34() V35() integer set
X is set
card X is V27() V28() V29() cardinal set
X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
card X is non empty V27() V28() V29() cardinal set

dom m is set
rng m is set
X is ext-real V34() V35() integer set
X is ext-real V34() V35() integer set
m is ext-real V34() V35() integer set
X * m is ext-real V34() V35() integer set
X + (X * m) is ext-real V34() V35() integer set
(X + (X * m)) mod m is ext-real V34() V35() integer set
X mod m is ext-real V34() V35() integer set
(X + (X * m)) div m is ext-real V34() V35() integer set
((X + (X * m)) div m) * m is ext-real V34() V35() integer set
(X + (X * m)) - (((X + (X * m)) div m) * m) is ext-real V34() V35() integer set
(X + (X * m)) / m is ext-real V34() V35() set
[\((X + (X * m)) / m)/] is ext-real V34() V35() integer set
[\((X + (X * m)) / m)/] * m is ext-real V34() V35() integer set
(X + (X * m)) - ([\((X + (X * m)) / m)/] * m) is ext-real V34() V35() integer set
X / m is ext-real V34() V35() set
(X * m) / m is ext-real V34() V35() set
(X / m) + ((X * m) / m) is ext-real V34() V35() set
[\((X / m) + ((X * m) / m))/] is ext-real V34() V35() integer set
[\((X / m) + ((X * m) / m))/] * m is ext-real V34() V35() integer set
(X + (X * m)) - ([\((X / m) + ((X * m) / m))/] * m) is ext-real V34() V35() integer set
m / m is ext-real V34() V35() set
X / (m / m) is ext-real V34() V35() set
(X / m) + (X / (m / m)) is ext-real V34() V35() set
[\((X / m) + (X / (m / m)))/] is ext-real V34() V35() integer set
[\((X / m) + (X / (m / m)))/] * m is ext-real V34() V35() integer set
(X + (X * m)) - ([\((X / m) + (X / (m / m)))/] * m) is ext-real V34() V35() integer set
X / 1 is ext-real V34() V35() set
(X / m) + (X / 1) is ext-real V34() V35() set
[\((X / m) + (X / 1))/] is ext-real V34() V35() integer set
[\((X / m) + (X / 1))/] * m is ext-real V34() V35() integer set
(X + (X * m)) - ([\((X / m) + (X / 1))/] * m) is ext-real V34() V35() integer set
[\(X / m)/] is ext-real V34() V35() integer set
[\(X / m)/] + X is ext-real V34() V35() integer set
([\(X / m)/] + X) * m is ext-real V34() V35() integer set
(X + (X * m)) - (([\(X / m)/] + X) * m) is ext-real V34() V35() integer set
[\(X / m)/] * m is ext-real V34() V35() integer set
X - ([\(X / m)/] * m) is ext-real V34() V35() integer set
X div m is ext-real V34() V35() integer set
(X div m) * m is ext-real V34() V35() integer set
X - ((X div m) * m) is ext-real V34() V35() integer set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(X * m) gcd (X * m) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(X * m) gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
((X * m) gcd X) gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
0 + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
m gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real V34() V35() integer set
X is ext-real V34() V35() integer set
X * X is ext-real V34() V35() integer set
m is ext-real V34() V35() integer set
X * m is ext-real V34() V35() integer set
(X * X) gcd (X * m) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X gcd m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * (X gcd m) is ext-real V34() V35() integer set
n is ext-real V34() V35() integer set
(X gcd m) * n is ext-real V34() V35() integer set
X is ext-real V34() V35() integer set
(X gcd m) * X is ext-real V34() V35() integer set
(X * (X gcd m)) * n is ext-real V34() V35() integer set
(X * (X gcd m)) * X is ext-real V34() V35() integer set
abs (X * (X gcd m)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
abs X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
abs (X gcd m) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(abs X) * (abs (X gcd m)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
m is ext-real V34() V35() integer set
m * X is ext-real V34() V35() integer set
X + (m * X) is ext-real V34() V35() integer set
(X + (m * X)) gcd X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
abs X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
abs (X + (m * X)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
C is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X * C is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
C is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
A is ext-real V34() V35() integer set
C * A is ext-real V34() V35() integer set
m * C is ext-real V34() V35() integer set
C * (m * C) is ext-real V34() V35() integer set
(C * A) - (C * (m * C)) is ext-real V34() V35() integer set
A - (m * C) is ext-real V34() V35() integer set
C * (A - (m * C)) is ext-real V34() V35() integer set
A is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
C * A is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
- (X + (m * X)) is ext-real V34() V35() integer set
C is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
A is ext-real V34() V35() integer set
C * A is ext-real V34() V35() integer set
- (C * A) is ext-real V34() V35() integer set
m * C is ext-real V34() V35() integer set
C * (m * C) is ext-real V34() V35() integer set
(- (C * A)) - (C * (m * C)) is ext-real V34() V35() integer set
- A is ext-real V34() V35() integer set
(- A) - (m * C) is ext-real V34() V35() integer set
C * ((- A) - (m * C)) is ext-real V34() V35() integer set
A is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
C * A is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
C is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
C is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X div (X gcd X) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(X gcd X) * (X div (X gcd X)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
X div (X gcd X) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(X gcd X) * (X div (X gcd X)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
- (X + (m * X)) is ext-real V34() V35() integer set
m * (X div (X gcd X)) is ext-real V34() V35() integer set
(X div (X gcd X)) + (m * (X div (X gcd X))) is ext-real V34() V35() integer set
- ((X div (X gcd X)) + (m * (X div (X gcd X)))) is ext-real V34() V35() integer set
(X gcd X) * (- ((X div (X gcd X)) + (m * (X div (X gcd X))))) is ext-real V34() V35() integer set
m * (X div (X gcd X)) is ext-real V34() V35() integer set
(X div (X gcd X)) + (m * (X div (X gcd X))) is ext-real V34() V35() integer set
(X gcd X) * ((X div (X gcd X)) + (m * (X div (X gcd X)))) is ext-real V34() V35() integer set
(abs (X + (m * X))) gcd (abs X) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
{ b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( X,b1 are_relative_prime & 1 <= b1 & b1 <= X ) } is set
card { b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( X,b1 are_relative_prime & 1 <= b1 & b1 <= X ) } is V27() V28() V29() cardinal set

m is set
n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
m is finite set
card m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
{ b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( 1,b1 are_relative_prime & 1 <= b1 & b1 <= 1 ) } is set
X is set
m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
1 gcd 1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
{1} is non empty trivial finite V42() 1 -element set
card {1} is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(1) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
card { b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( 1,b1 are_relative_prime & 1 <= b1 & b1 <= 1 ) } is V27() V28() V29() cardinal set
{ b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( 2,b1 are_relative_prime & 1 <= b1 & b1 <= 2 ) } is set
m is set
n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
2 gcd 2 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
2 gcd 1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(2) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
card { b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( 2,b1 are_relative_prime & 1 <= b1 & b1 <= 2 ) } is V27() V28() V29() cardinal set
m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(m) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
{ b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( m,b1 are_relative_prime & 1 <= b1 & b1 <= m ) } is set
card { b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( m,b1 are_relative_prime & 1 <= b1 & b1 <= m ) } is V27() V28() V29() cardinal set
m - 1 is ext-real V34() V35() integer set

X is set
C is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
{ b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : not m <= b1 } is set
m \ is finite Element of bool m
bool m is non empty finite V42() set
card (m \ ) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
card m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
card is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(card m) - () is ext-real V34() V35() integer set
X is finite set
C is set
C is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(m) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
{ b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( m,b1 are_relative_prime & 1 <= b1 & b1 <= m ) } is set
card { b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( m,b1 are_relative_prime & 1 <= b1 & b1 <= m ) } is V27() V28() V29() cardinal set
m - 1 is ext-real V34() V35() integer set

X is set
C is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT

{ b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : not m <= b1 } is set
m \ is finite Element of bool m
bool m is non empty finite V42() set
X is finite set
C is set
C is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
card (m \ ) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
card X is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
card m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
card is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(m) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
{ b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( m,b1 are_relative_prime & 1 <= b1 & b1 <= m ) } is set
card { b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( m,b1 are_relative_prime & 1 <= b1 & b1 <= m ) } is V27() V28() V29() cardinal set
n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
m * n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
((m * n)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
{ b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( m * n,b1 are_relative_prime & 1 <= b1 & b1 <= m * n ) } is set
card { b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( m * n,b1 are_relative_prime & 1 <= b1 & b1 <= m * n ) } is V27() V28() V29() cardinal set
(n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
{ b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( n,b1 are_relative_prime & 1 <= b1 & b1 <= n ) } is set
card { b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( n,b1 are_relative_prime & 1 <= b1 & b1 <= n ) } is V27() V28() V29() cardinal set
(m) * (n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
{ b1 where b1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ex b2, b3 being ext-real V34() V35() integer set st
( b1 = ((m * b3) + (n * b2)) mod (m * n) & m * n,b1 are_relative_prime & b3 <= n & b2 <= m & 0 <= b1 )
}
is set

Seg (m * n) is finite m * n -element Element of bool NAT
(Seg (m * n)) \/ is finite set
C is set
A is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
B is ext-real V34() V35() integer set
m * B is ext-real V34() V35() integer set
A is ext-real V34() V35() integer set
n * A is ext-real V34() V35() integer set
(m * B) + (n * A) is ext-real V34() V35() integer set
((m * B) + (n * A)) mod (m * n) is ext-real V34() V35() integer set
B is ext-real V34() V35() integer set
m * B is ext-real V34() V35() integer set
A is ext-real V34() V35() integer set
n * A is ext-real V34() V35() integer set
(m * B) + (n * A) is ext-real V34() V35() integer set
((m * B) + (n * A)) mod (m * n) is ext-real V34() V35() integer set
((m * B) + (n * A)) / (m * n) is ext-real V34() V35() set
[\(((m * B) + (n * A)) / (m * n))/] is ext-real V34() V35() integer set
[\(((m * B) + (n * A)) / (m * n))/] + 1 is ext-real V34() V35() integer set
((m * B) + (n * A)) div (m * n) is ext-real V34() V35() integer set
(((m * B) + (n * A)) div (m * n)) * (m * n) is ext-real V34() V35() integer set
((m * B) + (n * A)) - ((((m * B) + (n * A)) div (m * n)) * (m * n)) is ext-real V34() V35() integer set
[\(((m * B) + (n * A)) / (m * n))/] * (m * n) is ext-real V34() V35() integer set
((m * B) + (n * A)) - ([\(((m * B) + (n * A)) / (m * n))/] * (m * n)) is ext-real V34() V35() integer set

A is set
B is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
C is finite set
A is ext-real V34() V35() integer set
m * A is ext-real V34() V35() integer set
B is ext-real V34() V35() integer set
n * B is ext-real V34() V35() integer set
(m * A) + (n * B) is ext-real V34() V35() integer set
((m * A) + (n * B)) mod (m * n) is ext-real V34() V35() integer set
m gcd n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
m + n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(m + n) gcd m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(m + n) gcd n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(m * n) gcd (m + n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
B is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
m * B is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
A is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
n * A is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(m * B) + (n * A) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
((m * B) + (n * A)) mod (m * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
B is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(m + n) mod (m * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
((m + n) mod (m * n)) gcd (m * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
C is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(m * n) * C is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
((m * n) * C) + ((m + n) mod (m * n)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
A is finite set
B is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
n gcd B is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set

B is set
A is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
B is set
A is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
C is ext-real V34() V35() integer set
m * C is ext-real V34() V35() integer set
B is ext-real V34() V35() integer set
n * B is ext-real V34() V35() integer set
(m * C) + (n * B) is ext-real V34() V35() integer set
((m * C) + (n * B)) mod (m * n) is ext-real V34() V35() integer set
C is ext-real V34() V35() integer set
m * C is ext-real V34() V35() integer set
B is ext-real V34() V35() integer set
n * B is ext-real V34() V35() integer set
(m * C) + (n * B) is ext-real V34() V35() integer set
((m * C) + (n * B)) mod (m * n) is ext-real V34() V35() integer set
((m * C) + (n * B)) / (m * n) is ext-real V34() V35() set
[\(((m * C) + (n * B)) / (m * n))/] is ext-real V34() V35() integer set
[\(((m * C) + (n * B)) / (m * n))/] + 1 is ext-real V34() V35() integer set
((m * C) + (n * B)) div (m * n) is ext-real V34() V35() integer set
(((m * C) + (n * B)) div (m * n)) * (m * n) is ext-real V34() V35() integer set
((m * C) + (n * B)) - ((((m * C) + (n * B)) div (m * n)) * (m * n)) is ext-real V34() V35() integer set
[\(((m * C) + (n * B)) / (m * n))/] * (m * n) is ext-real V34() V35() integer set
((m * C) + (n * B)) - ([\(((m * C) + (n * B)) / (m * n))/] * (m * n)) is ext-real V34() V35() integer set
(m * n) gcd 0 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
B is set
A is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(m * n) gcd (m * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
B is ext-real V34() V35() integer set
B * m is ext-real V34() V35() integer set
C is ext-real V34() V35() integer set
C * n is ext-real V34() V35() integer set
(B * m) + (C * n) is ext-real V34() V35() integer set
m * B is ext-real V34() V35() integer set
n * C is ext-real V34() V35() integer set
(m * B) + (n * C) is ext-real V34() V35() integer set
((m * B) + (n * C)) mod (m * n) is ext-real V34() V35() integer set
((m * B) + (n * C)) div (m * n) is ext-real V34() V35() integer set
(((m * B) + (n * C)) div (m * n)) * (m * n) is ext-real V34() V35() integer set
((m * B) + (n * C)) - ((((m * B) + (n * C)) div (m * n)) * (m * n)) is ext-real V34() V35() integer set
0 * (m * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
((m * B) + (n * C)) - (0 * (m * n)) is ext-real V34() V35() integer set
B div n is ext-real V34() V35() integer set
C div m is ext-real V34() V35() integer set
C mod m is ext-real V34() V35() integer set
B mod n is ext-real V34() V35() integer set
y is ext-real V34() V35() integer set
xx1 is ext-real V34() V35() integer set
(C div m) * m is ext-real V34() V35() integer set
C - ((C div m) * m) is ext-real V34() V35() integer set
(B div n) * n is ext-real V34() V35() integer set
B - ((B div n) * n) is ext-real V34() V35() integer set
m * xx1 is ext-real V34() V35() integer set
n * y is ext-real V34() V35() integer set
(m * xx1) + (n * y) is ext-real V34() V35() integer set
(B div n) + (C div m) is ext-real V34() V35() integer set
(m * n) * ((B div n) + (C div m)) is ext-real V34() V35() integer set
((m * xx1) + (n * y)) + ((m * n) * ((B div n) + (C div m))) is ext-real V34() V35() integer set
((m * xx1) + (n * y)) mod (m * n) is ext-real V34() V35() integer set
B / n is ext-real V34() V35() set
[\(B / n)/] is ext-real V34() V35() integer set
[\(B / n)/] + 1 is ext-real V34() V35() integer set
C / m is ext-real V34() V35() set
[\(C / m)/] is ext-real V34() V35() integer set
[\(C / m)/] + 1 is ext-real V34() V35() integer set
[\(B / n)/] * n is ext-real V34() V35() integer set
B - ([\(B / n)/] * n) is ext-real V34() V35() integer set
[\(C / m)/] * m is ext-real V34() V35() integer set
C - ([\(C / m)/] * m) is ext-real V34() V35() integer set
B is finite set
A is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
m gcd A is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
A is non empty finite Element of bool NAT
B is non empty finite Element of bool NAT
C is non empty finite Element of bool NAT
n * m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
x is Element of A
m * x is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
y is Element of B
n * y is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(m * x) + (n * y) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
((m * x) + (n * y)) mod (m * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
xx1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
xx2 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
xx1 * m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(xx1 * m) gcd n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
m * xx1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
n * xx2 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(m * xx1) + (n * xx2) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
((m * xx1) + (n * xx2)) gcd n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
xx2 * n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(xx2 * n) gcd m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
((m * xx1) + (n * xx2)) gcd m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
0 * m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(n * m) gcd ((m * xx1) + (n * xx2)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
yy1 is ext-real V34() V35() integer set
m * yy1 is ext-real V34() V35() integer set
yy2 is ext-real V34() V35() integer set
n * yy2 is ext-real V34() V35() integer set
(m * yy1) + (n * yy2) is ext-real V34() V35() integer set
((m * yy1) + (n * yy2)) mod (m * n) is ext-real V34() V35() integer set
((m * xx1) + (n * xx2)) mod (m * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
x1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
((m * xx1) + (n * xx2)) mod (n * m) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(((m * xx1) + (n * xx2)) mod (n * m)) gcd (n * m) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
x2 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(n * m) * x2 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
((n * m) * x2) + (((m * xx1) + (n * xx2)) mod (n * m)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
[:A,B:] is non empty finite set
[:[:A,B:],C:] is non empty finite set
bool [:[:A,B:],C:] is non empty finite V42() set

rng f is finite set
K208(C,f) is finite Element of bool C
bool C is non empty finite V42() set
x is set
y is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
xx2 is ext-real V34() V35() integer set
m * xx2 is ext-real V34() V35() integer set
xx1 is ext-real V34() V35() integer set
n * xx1 is ext-real V34() V35() integer set
(m * xx2) + (n * xx1) is ext-real V34() V35() integer set
((m * xx2) + (n * xx1)) mod (m * n) is ext-real V34() V35() integer set
xx2 is ext-real V34() V35() integer set
m * xx2 is ext-real V34() V35() integer set
xx1 is ext-real V34() V35() integer set
n * xx1 is ext-real V34() V35() integer set
(m * xx2) + (n * xx1) is ext-real V34() V35() integer set
((m * xx2) + (n * xx1)) mod (m * n) is ext-real V34() V35() integer set
xx1 mod m is ext-real V34() V35() integer set
xx2 mod n is ext-real V34() V35() integer set
yy1 is ext-real V34() V35() integer set
yy2 is ext-real V34() V35() integer set
m * yy2 is ext-real V34() V35() integer set
n * yy1 is ext-real V34() V35() integer set
(m * yy2) + (n * yy1) is ext-real V34() V35() integer set
((m * yy2) + (n * yy1)) mod (m * n) is ext-real V34() V35() integer set
xx2 div n is ext-real V34() V35() integer set
xx1 div m is ext-real V34() V35() integer set
(xx1 div m) * m is ext-real V34() V35() integer set
xx1 - ((xx1 div m) * m) is ext-real V34() V35() integer set
(xx2 div n) * n is ext-real V34() V35() integer set
xx2 - ((xx2 div n) * n) is ext-real V34() V35() integer set
(xx2 div n) + (xx1 div m) is ext-real V34() V35() integer set
(m * n) * ((xx2 div n) + (xx1 div m)) is ext-real V34() V35() integer set
((m * yy2) + (n * yy1)) + ((m * n) * ((xx2 div n) + (xx1 div m))) is ext-real V34() V35() integer set
x1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
xx1 div m is ext-real V34() V35() integer set
n * (xx1 div m) is ext-real V34() V35() integer set
xx2 + (n * (xx1 div m)) is ext-real V34() V35() integer set
m * (xx2 + (n * (xx1 div m))) is ext-real V34() V35() integer set
(m * (xx2 + (n * (xx1 div m)))) div (m * n) is ext-real V34() V35() integer set
n * ((m * (xx2 + (n * (xx1 div m)))) div (m * n)) is ext-real V34() V35() integer set
(xx2 + (n * (xx1 div m))) - (n * ((m * (xx2 + (n * (xx1 div m)))) div (m * n))) is ext-real V34() V35() integer set
(xx1 div m) * m is ext-real V34() V35() integer set
xx1 - ((xx1 div m) * m) is ext-real V34() V35() integer set
((m * (xx2 + (n * (xx1 div m)))) div (m * n)) * (m * n) is ext-real V34() V35() integer set
(m * (xx2 + (n * (xx1 div m)))) - (((m * (xx2 + (n * (xx1 div m)))) div (m * n)) * (m * n)) is ext-real V34() V35() integer set
m * ((xx2 + (n * (xx1 div m))) - (n * ((m * (xx2 + (n * (xx1 div m)))) div (m * n)))) is ext-real V34() V35() integer set
(m * n) gcd (m * ((xx2 + (n * (xx1 div m))) - (n * ((m * (xx2 + (n * (xx1 div m)))) div (m * n))))) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
y1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
0 * ((xx2 + (n * (xx1 div m))) - (n * ((m * (xx2 + (n * (xx1 div m)))) div (m * n)))) is ext-real V34() V35() integer set
y1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
n gcd y1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
m * (n gcd y1) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(m * n) gcd 0 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
x2 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
xx2 div n is ext-real V34() V35() integer set
m * (xx2 div n) is ext-real V34() V35() integer set
(m * (xx2 div n)) + xx1 is ext-real V34() V35() integer set
n * ((m * (xx2 div n)) + xx1) is ext-real V34() V35() integer set
(n * ((m * (xx2 div n)) + xx1)) div (m * n) is ext-real V34() V35() integer set
m * ((n * ((m * (xx2 div n)) + xx1)) div (m * n)) is ext-real V34() V35() integer set
((m * (xx2 div n)) + xx1) - (m * ((n * ((m * (xx2 div n)) + xx1)) div (m * n))) is ext-real V34() V35() integer set
(xx2 div n) * n is ext-real V34() V35() integer set
xx2 - ((xx2 div n) * n) is ext-real V34() V35() integer set
((n * ((m * (xx2 div n)) + xx1)) div (m * n)) * (m * n) is ext-real V34() V35() integer set
(n * ((m * (xx2 div n)) + xx1)) - (((n * ((m * (xx2 div n)) + xx1)) div (m * n)) * (m * n)) is ext-real V34() V35() integer set
n * (((m * (xx2 div n)) + xx1) - (m * ((n * ((m * (xx2 div n)) + xx1)) div (m * n)))) is ext-real V34() V35() integer set
(m * n) gcd (n * (((m * (xx2 div n)) + xx1) - (m * ((n * ((m * (xx2 div n)) + xx1)) div (m * n))))) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
y1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
0 * (((m * (xx2 div n)) + xx1) - (m * ((n * ((m * (xx2 div n)) + xx1)) div (m * n)))) is ext-real V34() V35() integer set
y1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
m gcd y1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
n * (m gcd y1) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
(m * n) gcd