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