:: ARITHM semantic presentation

REAL is set

NAT is non zero epsilon-transitive epsilon-connected ordinal Element of K19(REAL)

K19(REAL) is set

COMPLEX is set

0 is epsilon-transitive epsilon-connected ordinal natural complex Element of NAT

1 is non zero epsilon-transitive epsilon-connected ordinal natural complex Element of NAT

x is complex set

x + 0 is complex set

x1 is complex Element of REAL

x2 is complex Element of REAL

[*x1,x2*] is complex Element of COMPLEX

[*0,0*] is complex Element of COMPLEX

+ (x1,0) is complex Element of REAL

+ (x2,0) is complex Element of REAL

[*(+ (x1,0)),(+ (x2,0))*] is complex Element of COMPLEX

[*x1,(+ (x2,0))*] is complex Element of COMPLEX

- 0 is complex set

0 + (- 0) is complex set

opp 0 is complex Element of REAL

+ (0,0) is complex Element of REAL

x is complex set

x * 0 is complex set

x1 is complex Element of REAL

x2 is complex Element of REAL

[*x1,x2*] is complex Element of COMPLEX

[*0,0*] is complex Element of COMPLEX

* (x1,0) is complex Element of REAL

* (x2,0) is complex Element of REAL

opp (* (x2,0)) is complex Element of REAL

+ ((* (x1,0)),(opp (* (x2,0)))) is complex Element of REAL

+ ((* (x1,0)),(* (x2,0))) is complex Element of REAL

[*(+ ((* (x1,0)),(opp (* (x2,0))))),(+ ((* (x1,0)),(* (x2,0))))*] is complex Element of COMPLEX

+ ((* (x1,0)),(opp 0)) is complex Element of REAL

[*(+ ((* (x1,0)),(opp 0))),(+ ((* (x1,0)),(* (x2,0))))*] is complex Element of COMPLEX

+ ((* (x1,0)),0) is complex Element of REAL

[*(+ ((* (x1,0)),(opp 0))),(+ ((* (x1,0)),0))*] is complex Element of COMPLEX

+ (0,(opp 0)) is complex Element of REAL

[*(+ (0,(opp 0))),(+ ((* (x1,0)),0))*] is complex Element of COMPLEX

+ (0,0) is complex Element of REAL

[*(+ (0,(opp 0))),(+ (0,0))*] is complex Element of COMPLEX

[*(+ (0,(opp 0))),0*] is complex Element of COMPLEX

[*(opp 0),0*] is complex Element of COMPLEX

x is complex set

1 * x is complex set

x1 is complex Element of REAL

x2 is complex Element of REAL

[*x1,x2*] is complex Element of COMPLEX

[*1,0*] is complex Element of COMPLEX

x * 1 is complex set

* (x1,1) is complex Element of REAL

* (x2,0) is complex Element of REAL

opp (* (x2,0)) is complex Element of REAL

+ ((* (x1,1)),(opp (* (x2,0)))) is complex Element of REAL

* (x1,0) is complex Element of REAL

* (x2,1) is complex Element of REAL

+ ((* (x1,0)),(* (x2,1))) is complex Element of REAL

[*(+ ((* (x1,1)),(opp (* (x2,0))))),(+ ((* (x1,0)),(* (x2,1))))*] is complex Element of COMPLEX

+ ((* (x1,1)),(opp 0)) is complex Element of REAL

[*(+ ((* (x1,1)),(opp 0))),(+ ((* (x1,0)),(* (x2,1))))*] is complex Element of COMPLEX

+ (x1,(opp 0)) is complex Element of REAL

[*(+ (x1,(opp 0))),(+ ((* (x1,0)),(* (x2,1))))*] is complex Element of COMPLEX

+ ((* (x1,0)),x2) is complex Element of REAL

[*(+ (x1,(opp 0))),(+ ((* (x1,0)),x2))*] is complex Element of COMPLEX

+ (x1,0) is complex Element of REAL

+ (0,x2) is complex Element of REAL

[*(+ (x1,0)),(+ (0,x2))*] is complex Element of COMPLEX

[*x1,(+ (0,x2))*] is complex Element of COMPLEX

x is complex set

x - 0 is complex set

x + 0 is complex set

x is complex set

0 / x is complex set

x " is complex set

0 * (x ") is complex set

1 " is non zero complex set

1 * (1 ") is non zero complex set

x is complex set

x / 1 is complex set

x * 1 is complex set