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

a * c

p1 is ext-real complex V15() integer set

a * p1 is ext-real complex V15() integer set

p1 - c

a * (p1 - c

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

a * c

(a * c

c

a * (c

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

a * c

p1 is ext-real complex V15() integer set

b * p1 is ext-real complex V15() integer set

c

a * (c

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

a * c

a * c

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

b * c

1 * a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT

m * c

a * (m * c

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

p1 is ext-real complex V15() integer set

c

- c

c

c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set

c

c

[\(c

(c

c

m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer set

c

c

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

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

c

b * (c

b * c

b + (b * c

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

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

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

c

p1 is ext-real complex V15() integer set

c

- c

(c

m 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

c

p1 is ext-real complex V15() integer set

c

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

b * c

1 * a is ext-real complex V15() integer set

m * c

a * (m * c

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

m * c

c

m * c

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

(m,c

(c

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

(a,b) * c

(m,c

p1 is ext-real complex V15() integer set

(m,c

(a,b) * (m,c

((a,b) * (m,c

c

(m,c

((a,b) * (m,c

c is ext-real complex V15() integer set

((a,b) * (m,c

(a,b) * 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex V15() integer Element of NAT

(m,c

(a,b) * ((m,c

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

((m * a),(m * b)) * c

p1 is ext-real complex V15() integer set

((m * a),(m * b)) * p1 is ext-real complex V15() integer set

c

m * c

c

m * (c

c

m * (c

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

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