:: ARITHM semantic presentation

REAL is set

K19(REAL) is set

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

+ (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 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

* (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)),()) is complex Element of REAL
[*(+ ((* (x1,0)),())),(+ ((* (x1,0)),(* (x2,0))))*] is complex Element of COMPLEX
+ ((* (x1,0)),0) is complex Element of REAL
[*(+ ((* (x1,0)),())),(+ ((* (x1,0)),0))*] is complex Element of COMPLEX
+ (0,()) is complex Element of REAL
[*(+ (0,())),(+ ((* (x1,0)),0))*] is complex Element of COMPLEX
+ (0,0) is complex Element of REAL
[*(+ (0,())),(+ (0,0))*] is complex Element of COMPLEX
[*(+ (0,())),0*] is complex Element of COMPLEX
[*(),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

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)),()) is complex Element of REAL
[*(+ ((* (x1,1)),())),(+ ((* (x1,0)),(* (x2,1))))*] is complex Element of COMPLEX
+ (x1,()) is complex Element of REAL
[*(+ (x1,())),(+ ((* (x1,0)),(* (x2,1))))*] is complex Element of COMPLEX
+ ((* (x1,0)),x2) is complex Element of REAL
[*(+ (x1,())),(+ ((* (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