:: INT_2 semantic presentation

REAL is set
NAT is non zero epsilon-transitive epsilon-connected ordinal Element of K11(REAL)
K11(REAL) is set
COMPLEX is set
INT is set
0 is ext-real non negative zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V15() integer Element of NAT
1 is ext-real positive non negative non zero epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
K48(1) is ext-real non positive complex V15() integer Element of REAL
2 is ext-real positive non negative non zero epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
NAT is non zero epsilon-transitive epsilon-connected ordinal set
a is ext-real complex V15() integer set
|.a.| is ext-real complex V15() set
abs a is ext-real complex V15() Element of REAL
abs a is ext-real complex V15() Element of REAL
- a is ext-real complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
m is ext-real complex V15() integer set
b + m is ext-real complex V15() integer set
c₄ is ext-real complex V15() integer set
a * c₄ is ext-real complex V15() integer set
p1 is ext-real complex V15() integer set
a * p1 is ext-real complex V15() integer set
p1 - c₄ is ext-real complex V15() integer set
a * (p1 - c₄) is ext-real complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
m is ext-real complex V15() integer set
b * m is ext-real complex V15() integer set
c₄ is ext-real complex V15() integer set
a * c₄ is ext-real complex V15() integer set
(a * c₄) * m is ext-real complex V15() integer set
c₄ * m is ext-real complex V15() integer set
a * (c₄ * m) is ext-real complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
0 * b is ext-real complex V15() integer set
a is ext-real complex V15() integer set
- a is ext-real complex V15() integer set
- 1 is ext-real non positive complex V15() integer set
a * (- 1) is ext-real complex V15() integer set
(- a) * (- 1) is ext-real complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
m is ext-real complex V15() integer set
c₄ is ext-real complex V15() integer set
a * c₄ is ext-real complex V15() integer set
p1 is ext-real complex V15() integer set
b * p1 is ext-real complex V15() integer set
c₄ * p1 is ext-real complex V15() integer set
a * (c₄ * p1) is ext-real complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
- b is ext-real complex V15() integer set
a is ext-real complex V15() integer set
- a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
- 1 is ext-real non positive complex V15() integer set
a is ext-real complex V15() integer set
a * 0 is ext-real complex V15() integer set
1 * a is ext-real complex V15() integer set
- a is ext-real complex V15() integer set
(- 1) * (- a) is ext-real complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
m is ext-real complex V15() integer set
b mod m is ext-real complex V15() integer set
b div m is ext-real complex V15() integer set
b / m is ext-real complex V15() set
[\(b / m)/] is ext-real complex V15() integer set
m * (b div m) is ext-real complex V15() integer set
(m * (b div m)) + (b mod m) is ext-real complex V15() integer set
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
m is ext-real complex V15() integer set
a * m is ext-real complex V15() integer set
c₄ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
a * c₄ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
a * c₄ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
a * 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
a * 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
a * m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
m is ext-real complex V15() integer set
a * m is ext-real complex V15() integer set
c₄ is ext-real complex V15() integer set
b * c₄ is ext-real complex V15() integer set
1 * a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
m * c₄ is ext-real complex V15() integer set
a * (m * c₄) is ext-real complex V15() integer set
b * 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
b * (- 1) is ext-real non positive complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
m is ext-real complex V15() integer set
a * b is ext-real complex V15() integer set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
- m is ext-real non positive complex V15() integer set
c₄ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
p1 is ext-real complex V15() integer set
c₆ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
- c₆ is ext-real non positive complex V15() integer set
c₆ mod c₄ is ext-real complex V15() integer set
c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
c₆ div c₄ is ext-real complex V15() integer set
c₆ / c₄ is ext-real non negative complex V15() set
[\(c₆ / c₄)/] is ext-real complex V15() integer set
(c₆ div c₄) * c₄ is ext-real complex V15() integer set
c₆ - ((c₆ div c₄) * c₄) is ext-real complex V15() integer set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
c₄ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
c₄ is ext-real complex V15() integer set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
p1 is ext-real complex V15() integer set
c₆ is ext-real complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
(a,b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
b * a is ext-real complex V15() integer set
a * b is ext-real complex V15() integer set
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
b * m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
c₄ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
c₄ + 1 is ext-real positive non negative non zero epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
b * (c₄ + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
b * c₄ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
b + (b * c₄) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
- m is ext-real non positive complex V15() integer set
c₄ is ext-real complex V15() integer set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
- m is ext-real non positive complex V15() integer set
c₄ is ext-real complex V15() integer set
a * b is ext-real complex V15() integer set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
- m is ext-real non positive complex V15() integer set
c₄ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
c₄ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
p1 is ext-real complex V15() integer set
c₆ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
- c₆ is ext-real non positive complex V15() integer set
(c₆,c₄) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
c₄ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
c₄ is ext-real complex V15() integer set
p1 is ext-real complex V15() integer set
c₆ is ext-real complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
(a,b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
(0,0) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
- a is ext-real non positive complex V15() integer set
0 + a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
a + (- a) is ext-real complex V15() integer set
a is ext-real non negative non zero epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
- a is ext-real non positive complex V15() integer set
a is ext-real complex V15() integer set
- a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
- b is ext-real complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
m is ext-real complex V15() integer set
a is ext-real complex V15() integer set
- a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
- b is ext-real complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
- b is ext-real complex V15() integer set
m is ext-real complex V15() integer set
a * m is ext-real complex V15() integer set
c₄ is ext-real complex V15() integer set
b * c₄ is ext-real complex V15() integer set
1 * a is ext-real complex V15() integer set
m * c₄ is ext-real complex V15() integer set
a * (m * c₄) is ext-real complex V15() integer set
b * 1 is ext-real complex V15() integer set
b * (- 1) is ext-real complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
m is ext-real complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
a * b is ext-real complex V15() integer set
b is ext-real complex V15() integer set
a * b is ext-real complex V15() integer set
a is ext-real complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
a - b is ext-real complex V15() integer set
m is ext-real complex V15() integer set
c₄ is ext-real complex V15() integer set
m * c₄ is ext-real complex V15() integer set
c₄ is ext-real complex V15() integer set
m * c₄ is ext-real complex V15() integer set
a is ext-real complex V15() integer set
(a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
b is ext-real complex V15() integer set
(b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
m is ext-real complex V15() integer set
a * m is ext-real complex V15() integer set
(m) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
(a) * (m) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
m is ext-real complex V15() integer set
(a) * m is ext-real complex V15() integer set
a * m is ext-real complex V15() integer set
- b is ext-real complex V15() integer set
- m is ext-real complex V15() integer set
a * (- m) is ext-real complex V15() integer set
- a is ext-real complex V15() integer set
(- a) * m is ext-real complex V15() integer set
- b is ext-real complex V15() integer set
a * m is ext-real complex V15() integer set
- (a * m) is ext-real complex V15() integer set
- m is ext-real complex V15() integer set
a * (- m) is ext-real complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
(a,b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
(a,b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
a is ext-real complex V15() integer set
m is ext-real complex V15() integer set
b is ext-real complex V15() integer set
(a,b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
(a,b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
(a,b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
m is ext-real complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
(a,b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
m is ext-real complex V15() integer set
c₄ is ext-real complex V15() integer set
(m,c₄) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
(c₄,m) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
(a,b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
m is ext-real complex V15() integer set
(a,b) * m is ext-real complex V15() integer set
c₄ is ext-real complex V15() integer set
(a,b) * c₄ is ext-real complex V15() integer set
(m,c₄) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
p1 is ext-real complex V15() integer set
(m,c₄) * p1 is ext-real complex V15() integer set
(a,b) * (m,c₄) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
((a,b) * (m,c₄)) * p1 is ext-real complex V15() integer set
c₆ is ext-real complex V15() integer set
(m,c₄) * c₆ is ext-real complex V15() integer set
((a,b) * (m,c₄)) * c₆ is ext-real complex V15() integer set
c is ext-real complex V15() integer set
((a,b) * (m,c₄)) * c is ext-real complex V15() integer set
(a,b) * 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
(m,c₄) * c is ext-real complex V15() integer set
(a,b) * ((m,c₄) * c) is ext-real complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
m is ext-real complex V15() integer set
m * a is ext-real complex V15() integer set
m * b is ext-real complex V15() integer set
((m * a),(m * b)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
(m) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
b * m is ext-real complex V15() integer set
((m * a),(b * m)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
a * m is ext-real complex V15() integer set
((a * m),(m * b)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
((a * m),(b * m)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
(a,b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
c₄ is ext-real complex V15() integer set
((m * a),(m * b)) * c₄ is ext-real complex V15() integer set
p1 is ext-real complex V15() integer set
((m * a),(m * b)) * p1 is ext-real complex V15() integer set
c₆ is ext-real complex V15() integer set
m * c₆ is ext-real complex V15() integer set
c₆ * c₄ is ext-real complex V15() integer set
m * (c₆ * c₄) is ext-real complex V15() integer set
c₆ * p1 is ext-real complex V15() integer set
m * (c₆ * p1) is ext-real complex V15() integer set
m * 1 is ext-real complex V15() integer set
m * (- 1) is ext-real complex V15() integer set
- m is ext-real complex V15() integer set
(- m) * 1 is ext-real complex V15() integer set
(((m * a),(m * b))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
0 * a is ext-real complex V15() integer set
0 * b is ext-real complex V15() integer set
((0 * a),(0 * b)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
(0) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
m is ext-real complex V15() integer set
b * m is ext-real complex V15() integer set
a * m is ext-real complex V15() integer set
((b * m),(a * m)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
(m) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
- m is ext-real complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
m is ext-real complex V15() integer set
a * m is ext-real complex V15() integer set
(a,b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
((a * m),b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
(((a * m),b),a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
(m,b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
m is ext-real complex V15() integer set
b * m is ext-real complex V15() integer set
0 + 1 is ext-real positive non negative non zero epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
4 is ext-real positive non negative non zero epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
2 * 2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
(a,b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
b + 1 is ext-real positive non negative non zero epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
(b + 1) - 1 is ext-real complex V15() integer set
1 + 1 is ext-real positive non negative non zero epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
(1 + 1) - 1 is ext-real complex V15() integer set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
0 + 1 is ext-real positive non negative non zero epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
c₄ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
p1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
a is ext-real complex V15() integer set
b is ext-real complex V15() integer set
(a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
(b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
(a) mod (b) is ext-real complex V15() integer set
a mod b is ext-real complex V15() integer set
(a) div (b) is ext-real complex V15() integer set
(a) / (b) is ext-real non negative complex V15() set
[\((a) / (b))/] is ext-real complex V15() integer set
a div b is ext-real complex V15() integer set
a / b is ext-real complex V15() set
[\(a / b)/] is ext-real complex V15() integer set
(0) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
(a) mod (0) is ext-real complex V15() integer set
(a) div (0) is ext-real complex V15() integer set
(a) / (0) is ext-real non negative complex V15() set
[\((a) / (0))/] is ext-real complex V15() integer set
a is ext-real complex V15() integer set
(a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
b is ext-real complex V15() integer set
(a,b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
(b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
((a),(b)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
- b is ext-real complex V15() integer set
- a is ext-real complex V15() integer set
m is ext-real complex V15() integer set
a is ext-real complex V15() integer set
(a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
b is ext-real complex V15() integer set
(a,b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
(b) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT
((a),(b)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set
- b is ext-real complex V15() integer set
- a is ext-real complex V15() integer set
m is ext-real complex V15() integer set