:: 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
COMPLEX is 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
the functional empty ext-real non positive non negative V27() V28() V29() V31() V32() V33() V34() V35() integer finite V42() cardinal {} -element FinSequence-membered set is functional empty ext-real non positive non negative V27() V28() V29() V31() V32() V33() V34() V35() integer finite V42() cardinal {} -element FinSequence-membered 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
{0} 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
{ b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( X,b₁ are_relative_prime & 1 <= b₁ & b₁ <= 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) - (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
m is Relation-like X -defined X -valued Function-like quasi_total Element of bool [:X,X:]
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
{ b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( X,b₁ are_relative_prime & 1 <= b₁ & b₁ <= X ) } is set
card { b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( X,b₁ are_relative_prime & 1 <= b₁ & b₁ <= X ) } is V27() V28() V29() cardinal set
Seg X is finite X -element Element of bool NAT
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
{ b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( 1,b₁ are_relative_prime & 1 <= b₁ & b₁ <= 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 { b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( 1,b₁ are_relative_prime & 1 <= b₁ & b₁ <= 1 ) } is V27() V28() V29() cardinal set
{ b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( 2,b₁ are_relative_prime & 1 <= b₁ & b₁ <= 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 { b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( 2,b₁ are_relative_prime & 1 <= b₁ & b₁ <= 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
{ b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( m,b₁ are_relative_prime & 1 <= b₁ & b₁ <= m ) } is set
card { b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( m,b₁ are_relative_prime & 1 <= b₁ & b₁ <= m ) } is V27() V28() V29() cardinal set
m - 1 is ext-real V34() V35() integer set
Seg m is finite m -element Element of bool NAT
X is set
C is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
{ b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : not m <= b₁ } is set
m \ {0} is finite Element of bool m
bool m is non empty finite V42() set
card (m \ {0}) 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 {0} is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(card m) - (card {0}) 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
{ b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( m,b₁ are_relative_prime & 1 <= b₁ & b₁ <= m ) } is set
card { b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( m,b₁ are_relative_prime & 1 <= b₁ & b₁ <= m ) } is V27() V28() V29() cardinal set
m - 1 is ext-real V34() V35() integer set
Seg m is finite m -element Element of bool NAT
X is set
C is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
SetPrimenumber 2 is functional empty proper ext-real non positive non negative V27() V28() V29() V31() V32() V33() V34() V35() integer finite V42() cardinal {} -element FinSequence-membered Element of bool NAT
{ b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : not m <= b₁ } is set
m \ {0} 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 \ {0}) 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 {0} 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
{ b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( m,b₁ are_relative_prime & 1 <= b₁ & b₁ <= m ) } is set
card { b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( m,b₁ are_relative_prime & 1 <= b₁ & b₁ <= 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
{ b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( m * n,b₁ are_relative_prime & 1 <= b₁ & b₁ <= m * n ) } is set
card { b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( m * n,b₁ are_relative_prime & 1 <= b₁ & b₁ <= 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
{ b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( n,b₁ are_relative_prime & 1 <= b₁ & b₁ <= n ) } is set
card { b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ( n,b₁ are_relative_prime & 1 <= b₁ & b₁ <= 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
{ b₁ where b₁ is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT : ex b₂, b₃ being ext-real V34() V35() integer set st
( b₁ = ((m * b₃) + (n * b₂)) mod (m * n) & m * n,b₁ are_relative_prime & b₃ <= n & b₂ <= m & 0 <= b₁ ) } is set
Seg (m * n) is finite m * n -element Element of bool NAT
(Seg (m * n)) \/ {0} 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
Seg n is finite n -element Element of bool NAT
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
Seg m is finite m -element Element of bool NAT
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
f is Relation-like [:A,B:] -defined C -valued Function-like quasi_total finite Element of bool [:[:A,B:],C:]
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 0 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
m gcd xx1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
y2 is ext-real V34() V35() integer set
(m gcd xx1) * y2 is ext-real V34() V35() integer set
y1 is ext-real V34() V35() integer set
(m gcd xx1) * y1 is ext-real V34() V35() integer set
y2 * n is ext-real V34() V35() integer set
((m gcd xx1) * y2) * xx2 is ext-real V34() V35() integer set
n * ((m gcd xx1) * y1) is ext-real V34() V35() integer set
(((m gcd xx1) * y2) * xx2) + (n * ((m gcd xx1) * y1)) is ext-real V34() V35() integer set
((m gcd xx1) * y2) * n is ext-real V34() V35() integer set
((((m gcd xx1) * y2) * xx2) + (n * ((m gcd xx1) * y1))) div (((m gcd xx1) * y2) * n) is ext-real V34() V35() integer set
y2 * xx2 is ext-real V34() V35() integer set
n * y1 is ext-real V34() V35() integer set
(y2 * xx2) + (n * y1) is ext-real V34() V35() integer set
y2 * (((((m gcd xx1) * y2) * xx2) + (n * ((m gcd xx1) * y1))) div (((m gcd xx1) * y2) * n)) is ext-real V34() V35() integer set
(y2 * (((((m gcd xx1) * y2) * xx2) + (n * ((m gcd xx1) * y1))) div (((m gcd xx1) * y2) * n))) * n is ext-real V34() V35() integer set
((y2 * xx2) + (n * y1)) - ((y2 * (((((m gcd xx1) * y2) * xx2) + (n * ((m gcd xx1) * y1))) div (((m gcd xx1) * y2) * n))) * n) is ext-real V34() V35() integer set
(((((m gcd xx1) * y2) * xx2) + (n * ((m gcd xx1) * y1))) div (((m gcd xx1) * y2) * n)) * (((m gcd xx1) * y2) * n) is ext-real V34() V35() integer set
((((m gcd xx1) * y2) * xx2) + (n * ((m gcd xx1) * y1))) - ((((((m gcd xx1) * y2) * xx2) + (n * ((m gcd xx1) * y1))) div (((m gcd xx1) * y2) * n)) * (((m gcd xx1) * y2) * n)) is ext-real V34() V35() integer set
(m gcd xx1) * (((y2 * xx2) + (n * y1)) - ((y2 * (((((m gcd xx1) * y2) * xx2) + (n * ((m gcd xx1) * y1))) div (((m gcd xx1) * y2) * n))) * n)) is ext-real V34() V35() integer set
0 * (((y2 * xx2) + (n * y1)) - ((y2 * (((((m gcd xx1) * y2) * xx2) + (n * ((m gcd xx1) * y1))) div (((m gcd xx1) * y2) * n))) * n)) is ext-real V34() V35() integer set
0 * (y2 * n) is ext-real V34() V35() integer set
x2 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
x2 * (y2 * n) is ext-real V34() V35() integer set
x2 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
x2 * (y2 * n) is ext-real V34() V35() integer set
w is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
k is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
x2 * w is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
x2 * k is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(x2 * w) gcd (x2 * k) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
w gcd k is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
x2 * (w gcd k) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
w is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
k is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
x2 * w is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(x2 * w) gcd 0 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
w is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
k is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
n gcd xx2 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
y2 is ext-real V34() V35() integer set
(n gcd xx2) * y2 is ext-real V34() V35() integer set
y1 is ext-real V34() V35() integer set
(n gcd xx2) * y1 is ext-real V34() V35() integer set
y2 * m is ext-real V34() V35() integer set
m * ((n gcd xx2) * y1) is ext-real V34() V35() integer set
((n gcd xx2) * y2) * xx1 is ext-real V34() V35() integer set
(m * ((n gcd xx2) * y1)) + (((n gcd xx2) * y2) * xx1) is ext-real V34() V35() integer set
m * ((n gcd xx2) * y2) is ext-real V34() V35() integer set
((m * ((n gcd xx2) * y1)) + (((n gcd xx2) * y2) * xx1)) div (m * ((n gcd xx2) * y2)) is ext-real V34() V35() integer set
m * y1 is ext-real V34() V35() integer set
y2 * xx1 is ext-real V34() V35() integer set
(m * y1) + (y2 * xx1) is ext-real V34() V35() integer set
y2 * (((m * ((n gcd xx2) * y1)) + (((n gcd xx2) * y2) * xx1)) div (m * ((n gcd xx2) * y2))) is ext-real V34() V35() integer set
(y2 * (((m * ((n gcd xx2) * y1)) + (((n gcd xx2) * y2) * xx1)) div (m * ((n gcd xx2) * y2)))) * m is ext-real V34() V35() integer set
((m * y1) + (y2 * xx1)) - ((y2 * (((m * ((n gcd xx2) * y1)) + (((n gcd xx2) * y2) * xx1)) div (m * ((n gcd xx2) * y2)))) * m) is ext-real V34() V35() integer set
(((m * ((n gcd xx2) * y1)) + (((n gcd xx2) * y2) * xx1)) div (m * ((n gcd xx2) * y2))) * (m * ((n gcd xx2) * y2)) is ext-real V34() V35() integer set
((m * ((n gcd xx2) * y1)) + (((n gcd xx2) * y2) * xx1)) - ((((m * ((n gcd xx2) * y1)) + (((n gcd xx2) * y2) * xx1)) div (m * ((n gcd xx2) * y2))) * (m * ((n gcd xx2) * y2))) is ext-real V34() V35() integer set
(n gcd xx2) * (((m * y1) + (y2 * xx1)) - ((y2 * (((m * ((n gcd xx2) * y1)) + (((n gcd xx2) * y2) * xx1)) div (m * ((n gcd xx2) * y2)))) * m)) is ext-real V34() V35() integer set
0 * (((m * y1) + (y2 * xx1)) - ((y2 * (((m * ((n gcd xx2) * y1)) + (((n gcd xx2) * y2) * xx1)) div (m * ((n gcd xx2) * y2)))) * m)) is ext-real V34() V35() integer set
0 * (y2 * m) is ext-real V34() V35() integer set
x2 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
x2 * (y2 * m) is ext-real V34() V35() integer set
x2 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
x2 * (y2 * m) is ext-real V34() V35() integer set
w is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
k is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
x2 * w is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
x2 * k is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(x2 * w) gcd (x2 * k) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
w gcd k is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
x2 * (w gcd k) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
w is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
k is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
x2 * w is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(x2 * w) gcd 0 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
w is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
k is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
xx2 gcd n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal 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
xx1 gcd m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
x1 + ((xx1 div m) * m) is ext-real V34() V35() integer set
(x1 + ((xx1 div m) * m)) gcd m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
x1 gcd m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
m gcd x1 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
xx2 div 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
x2 + ((xx2 div n) * n) is ext-real V34() V35() integer set
(x2 + ((xx2 div n) * n)) gcd n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
x2 gcd n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal set
p is Element of A
y2 is Element of B
f . (p,y2) is Element of C
[p,y2] is set
{p,y2} is finite set
{p} is non empty trivial finite 1 -element set
{{p,y2},{p}} is finite V42() set
f . [p,y2] is set
y1 is set
dom f is Relation-like finite set
x is set
dom f is Relation-like finite set
y is set
f . x is set
f . y is set
xx1 is Element of A
xx2 is Element of B
[xx1,xx2] is set
{xx1,xx2} is finite set
{xx1} is non empty trivial finite 1 -element set
{{xx1,xx2},{xx1}} is finite V42() set
yy1 is Element of A
yy2 is Element of B
[yy1,yy2] is set
{yy1,yy2} is finite set
{yy1} is non empty trivial finite 1 -element set
{{yy1,yy2},{yy1}} is finite V42() set
x1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
x2 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
p is ext-real V34() V35() integer set
y2 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
y1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
x1 * m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
x2 * n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(x1 * m) + (x2 * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
((x1 * m) + (x2 * n)) mod (m * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
f . (xx1,xx2) is Element of C
f . [xx1,xx2] is set
f . (yy1,yy2) is Element of C
f . [yy1,yy2] is set
y1 * m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
y2 * n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(y1 * m) + (y2 * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
((y1 * m) + (y2 * n)) 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
x1 * m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
x2 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
x2 * n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(x1 * m) + (x2 * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
((x1 * m) + (x2 * n)) mod (m * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
y1 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
y1 * m is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
y2 is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
y2 * n is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(y1 * m) + (y2 * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
((x1 * m) + (x2 * n)) - ((y1 * m) + (y2 * n)) is ext-real V34() V35() integer set
x1 - y1 is ext-real V34() V35() integer set
m * (x1 - y1) is ext-real V34() V35() integer set
x2 - y2 is ext-real V34() V35() integer set
n * (x2 - y2) is ext-real V34() V35() integer set
(m * (x1 - y1)) + (n * (x2 - y2)) is ext-real V34() V35() integer set
((x1 * m) + (x2 * n)) div (m * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(((x1 * m) + (x2 * n)) div (m * n)) * (m * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(((x1 * m) + (x2 * n)) mod (m * n)) + ((((x1 * m) + (x2 * n)) div (m * n)) * (m * n)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
((y1 * m) + (y2 * n)) div (m * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(((y1 * m) + (y2 * n)) div (m * n)) * (m * n) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
(((x1 * m) + (x2 * n)) mod (m * n)) + ((((y1 * m) + (y2 * n)) div (m * n)) * (m * n)) is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
((((x1 * m) + (x2 * n)) mod (m * n)) + ((((x1 * m) + (x2 * n)) div (m * n)) * (m * n))) - ((((x1 * m) + (x2 * n)) mod (m * n)) + ((((y1 * m) + (y2 * n)) div (m * n)) * (m * n))) is ext-real V34() V35() integer set
(((x1 * m) + (x2 * n)) div (m * n)) - (((y1 * m) + (y2 * n)) div (m * n)) is ext-real V34() V35() integer set
(m * n) * ((((x1 * m) + (x2 * n)) div (m * n)) - (((y1 * m) + (y2 * n)) div (m * n))) is ext-real V34() V35() integer set
n * ((((x1 * m) + (x2 * n)) div (m * n)) - (((y1 * m) + (y2 * n)) div (m * n))) is ext-real V34() V35() integer set
(n * ((((x1 * m) + (x2 * n)) div (m * n)) - (((y1 * m) + (y2 * n)) div (m * n)))) - (x1 - y1) is ext-real V34() V35() integer set
m * ((n * ((((x1 * m) + (x2 * n)) div (m * n)) - (((y1 * m) + (y2 * n)) div (m * n)))) - (x1 - y1)) is ext-real V34() V35() integer set
p is ext-real V34() V35() integer set
m * ((((x1 * m) + (x2 * n)) div (m * n)) - (((y1 * m) + (y2 * n)) div (m * n))) is ext-real V34() V35() integer set
(m * ((((x1 * m) + (x2 * n)) div (m * n)) - (((y1 * m) + (y2 * n)) div (m * n)))) - (x2 - y2) is ext-real V34() V35() integer set
n * ((m * ((((x1 * m) + (x2 * n)) div (m * n)) - (((y1 * m) + (y2 * n)) div (m * n)))) - (x2 - y2)) is ext-real V34() V35() integer set
k is ext-real V34() V35() integer set
k is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
- 1 is ext-real non positive V34() V35() integer set
n + (- 1) is ext-real V34() V35() integer set
- y1 is ext-real non positive V34() V35() integer set
x1 + (- y1) is ext-real V34() V35() integer set
(n + (- 1)) + 1 is ext-real V34() V35() integer set
- (x1 - y1) is ext-real V34() V35() integer set
k is ext-real V34() V35() integer set
- 0 is ext-real non positive V34() V35() integer set
k is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
- 1 is ext-real non positive V34() V35() integer set
n + (- 1) is ext-real V34() V35() integer set
- x1 is ext-real non positive V34() V35() integer set
(- x1) + y1 is ext-real V34() V35() integer set
(n + (- 1)) + 1 is ext-real V34() V35() integer set
k is ext-real V34() V35() integer set
k is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
- 1 is ext-real non positive V34() V35() integer set
m + (- 1) is ext-real V34() V35() integer set
- y2 is ext-real non positive V34() V35() integer set
x2 + (- y2) is ext-real V34() V35() integer set
(m + (- 1)) + 1 is ext-real V34() V35() integer set
- (x2 - y2) is ext-real V34() V35() integer set
k is ext-real V34() V35() integer set
- 0 is ext-real non positive V34() V35() integer set
k is ext-real non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
- 1 is ext-real non positive V34() V35() integer set
m + (- 1) is ext-real V34() V35() integer set
- x2 is ext-real non positive V34() V35() integer set
(- x2) + y2 is ext-real V34() V35() integer set
(m + (- 1)) + 1 is ext-real V34() V35() integer set
card [:A,B:] is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT
card C is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() integer finite cardinal Element of NAT