:: COMPLEX2 semantic presentation

REAL is non zero V50() V61() V62() V63() V67() set
NAT is V61() V62() V63() V64() V65() V66() V67() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non zero V50() V61() V67() set
RAT is non zero V50() V61() V62() V63() V64() V67() set
INT is non zero V50() V61() V62() V63() V64() V65() V67() set
K20(COMPLEX,COMPLEX) is V35() set
K19(K20(COMPLEX,COMPLEX)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is V35() set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(REAL,REAL) is V35() V36() V37() set
K19(K20(REAL,REAL)) is set
K20(K20(REAL,REAL),REAL) is V35() V36() V37() set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is RAT -valued V35() V36() V37() set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is RAT -valued V35() V36() V37() set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is RAT -valued INT -valued V35() V36() V37() set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is RAT -valued INT -valued V35() V36() V37() set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is RAT -valued INT -valued V35() V36() V37() V38() set
K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued V35() V36() V37() V38() set
K19(K20(K20(NAT,NAT),NAT)) is set
omega is V61() V62() V63() V64() V65() V66() V67() set
K19(omega) is set
K19(NAT) is set
K20(NAT,REAL) is V35() V36() V37() set
K19(K20(NAT,REAL)) is set
K20(NAT,COMPLEX) is V35() set
K19(K20(NAT,COMPLEX)) is set
0 is zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() Element of NAT
2 is non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() Element of NAT
K20(2,REAL) is V35() V36() V37() set
K19(K20(2,REAL)) is set
1 is non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() Element of NAT
1r is complex Element of COMPLEX
Re 0 is complex real ext-real Element of REAL
Im 0 is complex real ext-real Element of REAL
<i> is complex Element of COMPLEX
K88(REAL,0,1,0,1) is Relation-like {0,1} -defined REAL -valued V6() V18({0,1}, REAL ) V35() V36() V37() Element of K19(K20({0,1},REAL))
{0,1} is non zero V61() V62() V63() V64() V65() V66() set
K20({0,1},REAL) is V35() V36() V37() set
K19(K20({0,1},REAL)) is set
1r *' is complex Element of COMPLEX
|.0.| is complex real ext-real Element of REAL
sin is Relation-like REAL -defined REAL -valued V6() V18( REAL , REAL ) V35() V36() V37() Element of K19(K20(REAL,REAL))
cos is Relation-like REAL -defined REAL -valued V6() V18( REAL , REAL ) V35() V36() V37() Element of K19(K20(REAL,REAL))
K426(REAL,sin) is V61() V62() V63() Element of K19(REAL)
K426(REAL,cos) is V61() V62() V63() Element of K19(REAL)
cos . 0 is complex real ext-real Element of REAL
sin . 0 is complex real ext-real Element of REAL
cos 0 is complex real ext-real Element of REAL
sin 0 is complex real ext-real Element of REAL
PI is complex real ext-real Element of REAL
PI / 2 is complex real ext-real Element of REAL
2 " is non zero complex real ext-real positive non negative set
PI * (2 ") is complex real ext-real set
cos . (PI / 2) is complex real ext-real Element of REAL
sin . (PI / 2) is complex real ext-real Element of REAL
cos . PI is complex real ext-real Element of REAL
- 1 is non zero complex real ext-real non positive negative integer Element of REAL
sin . PI is complex real ext-real Element of REAL
PI + (PI / 2) is complex real ext-real Element of REAL
cos . (PI + (PI / 2)) is complex real ext-real Element of REAL
sin . (PI + (PI / 2)) is complex real ext-real Element of REAL
2 * PI is complex real ext-real Element of REAL
cos . (2 * PI) is complex real ext-real Element of REAL
sin . (2 * PI) is complex real ext-real Element of REAL
cos (PI / 2) is complex real ext-real Element of REAL
sin (PI / 2) is complex real ext-real Element of REAL
cos PI is complex real ext-real Element of REAL
sin PI is complex real ext-real Element of REAL
cos (PI + (PI / 2)) is complex real ext-real Element of REAL
sin (PI + (PI / 2)) is complex real ext-real Element of REAL
cos (2 * PI) is complex real ext-real Element of REAL
sin (2 * PI) is complex real ext-real Element of REAL
- (PI / 2) is complex real ext-real Element of REAL
3 is non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() Element of NAT
3 / 2 is non zero complex real ext-real positive non negative Element of REAL
3 * (2 ") is non zero complex real ext-real positive non negative set
(3 / 2) * PI is complex real ext-real Element of REAL
].0,(PI / 2).[ is V61() V62() V63() Element of K19(REAL)
].(PI / 2),PI.[ is V61() V62() V63() Element of K19(REAL)
K34(REAL,REAL,sin,].0,(PI / 2).[) is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
K34(REAL,REAL,sin,].(PI / 2),PI.[) is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of K19(K20(REAL,REAL))
b is complex real ext-real set
a is complex real ext-real set
a / b is complex real ext-real Element of COMPLEX
b " is complex real ext-real set
a * (b ") is complex real ext-real set
[\(a / b)/] is complex real ext-real integer set
- [\(a / b)/] is complex real ext-real integer set
b * (- [\(a / b)/]) is complex real ext-real set
(b * (- [\(a / b)/])) + a is complex real ext-real set
A is complex real ext-real set
[\(a / b)/] * b is complex real ext-real set
(a / b) * b is complex real ext-real set
- a is complex real ext-real set
- ([\(a / b)/] * b) is complex real ext-real set
a + (- a) is complex real ext-real set
(a / b) - 1 is complex real ext-real Element of REAL
- 1 is non zero complex real ext-real non positive negative integer set
(a / b) + (- 1) is complex real ext-real set
- ((a / b) - 1) is complex real ext-real Element of REAL
- (a / b) is complex real ext-real Element of COMPLEX
(- (a / b)) + 1 is complex real ext-real Element of REAL
((- (a / b)) + 1) * b is complex real ext-real Element of REAL
(- [\(a / b)/]) * b is complex real ext-real set
- ((a / b) * b) is complex real ext-real set
(- ((a / b) * b)) + b is complex real ext-real set
(- a) + b is complex real ext-real set
((- a) + b) + a is complex real ext-real set
a is complex real ext-real set
b is complex real ext-real set
c is complex real ext-real set
0 + a is complex real ext-real Element of REAL
c + a is complex real ext-real set
r is complex real ext-real integer set
a * r is complex real ext-real set
c + (a * r) is complex real ext-real set
a * (- 1) is complex real ext-real Element of REAL
c - a is complex real ext-real set
- a is complex real ext-real set
c + (- a) is complex real ext-real set
0 + 1 is non zero complex real ext-real positive non negative integer Element of REAL
a is complex real ext-real set
b is complex real ext-real set
a - b is complex real ext-real set
- b is complex real ext-real set
a + (- b) is complex real ext-real set
sin (a - b) is complex real ext-real set
sin a is complex real ext-real set
cos b is complex real ext-real set
(sin a) * (cos b) is complex real ext-real set
cos a is complex real ext-real set
sin b is complex real ext-real set
(cos a) * (sin b) is complex real ext-real set
((sin a) * (cos b)) - ((cos a) * (sin b)) is complex real ext-real set
- ((cos a) * (sin b)) is complex real ext-real set
((sin a) * (cos b)) + (- ((cos a) * (sin b))) is complex real ext-real set
cos (a - b) is complex real ext-real set
(cos a) * (cos b) is complex real ext-real set
(sin a) * (sin b) is complex real ext-real set
((cos a) * (cos b)) + ((sin a) * (sin b)) is complex real ext-real set
sin . (a + (- b)) is complex real ext-real Element of REAL
sin . a is complex real ext-real Element of REAL
cos . (- b) is complex real ext-real Element of REAL
(sin . a) * (cos . (- b)) is complex real ext-real Element of REAL
cos . a is complex real ext-real Element of REAL
sin . (- b) is complex real ext-real Element of REAL
(cos . a) * (sin . (- b)) is complex real ext-real Element of REAL
((sin . a) * (cos . (- b))) + ((cos . a) * (sin . (- b))) is complex real ext-real Element of REAL
cos . b is complex real ext-real Element of REAL
(sin . a) * (cos . b) is complex real ext-real Element of REAL
((sin . a) * (cos . b)) + ((cos . a) * (sin . (- b))) is complex real ext-real Element of REAL
sin . b is complex real ext-real Element of REAL
- (sin . b) is complex real ext-real Element of REAL
(cos . a) * (- (sin . b)) is complex real ext-real Element of REAL
((sin . a) * (cos . b)) + ((cos . a) * (- (sin . b))) is complex real ext-real Element of REAL
(sin a) * (cos . b) is complex real ext-real Element of REAL
(cos . a) * (sin . b) is complex real ext-real Element of REAL
((sin a) * (cos . b)) - ((cos . a) * (sin . b)) is complex real ext-real Element of REAL
- ((cos . a) * (sin . b)) is complex real ext-real set
((sin a) * (cos . b)) + (- ((cos . a) * (sin . b))) is complex real ext-real set
((sin a) * (cos b)) - ((cos . a) * (sin . b)) is complex real ext-real Element of REAL
((sin a) * (cos b)) + (- ((cos . a) * (sin . b))) is complex real ext-real set
(cos a) * (sin . b) is complex real ext-real Element of REAL
((sin a) * (cos b)) - ((cos a) * (sin . b)) is complex real ext-real Element of REAL
- ((cos a) * (sin . b)) is complex real ext-real set
((sin a) * (cos b)) + (- ((cos a) * (sin . b))) is complex real ext-real set
cos . (a + (- b)) is complex real ext-real Element of REAL
(cos . a) * (cos . (- b)) is complex real ext-real Element of REAL
(sin . a) * (sin . (- b)) is complex real ext-real Element of REAL
((cos . a) * (cos . (- b))) - ((sin . a) * (sin . (- b))) is complex real ext-real Element of REAL
- ((sin . a) * (sin . (- b))) is complex real ext-real set
((cos . a) * (cos . (- b))) + (- ((sin . a) * (sin . (- b)))) is complex real ext-real set
(cos . a) * (cos . b) is complex real ext-real Element of REAL
((cos . a) * (cos . b)) - ((sin . a) * (sin . (- b))) is complex real ext-real Element of REAL
((cos . a) * (cos . b)) + (- ((sin . a) * (sin . (- b)))) is complex real ext-real set
(sin . a) * (- (sin . b)) is complex real ext-real Element of REAL
((cos . a) * (cos . b)) - ((sin . a) * (- (sin . b))) is complex real ext-real Element of REAL
- ((sin . a) * (- (sin . b))) is complex real ext-real set
((cos . a) * (cos . b)) + (- ((sin . a) * (- (sin . b)))) is complex real ext-real set
(cos a) * (cos . b) is complex real ext-real Element of REAL
(sin . a) * (sin . b) is complex real ext-real Element of REAL
((cos a) * (cos . b)) + ((sin . a) * (sin . b)) is complex real ext-real Element of REAL
((cos a) * (cos b)) + ((sin . a) * (sin . b)) is complex real ext-real Element of REAL
(sin a) * (sin . b) is complex real ext-real Element of REAL
((cos a) * (cos b)) + ((sin a) * (sin . b)) is complex real ext-real Element of REAL
a is complex real ext-real set
a - PI is complex real ext-real Element of REAL
- PI is complex real ext-real set
a + (- PI) is complex real ext-real set
sin . (a - PI) is complex real ext-real Element of REAL
sin . a is complex real ext-real Element of REAL
- (sin . a) is complex real ext-real Element of REAL
cos . (a - PI) is complex real ext-real Element of REAL
cos . a is complex real ext-real Element of REAL
- (cos . a) is complex real ext-real Element of REAL
- PI is complex real ext-real Element of REAL
cos . (- PI) is complex real ext-real Element of REAL
(sin . a) * (cos . (- PI)) is complex real ext-real Element of REAL
sin . (- PI) is complex real ext-real Element of REAL
(cos . a) * (sin . (- PI)) is complex real ext-real Element of REAL
((sin . a) * (cos . (- PI))) + ((cos . a) * (sin . (- PI))) is complex real ext-real Element of REAL
(sin . a) * (cos . PI) is complex real ext-real Element of REAL
((sin . a) * (cos . PI)) + ((cos . a) * (sin . (- PI))) is complex real ext-real Element of REAL
- (sin . PI) is complex real ext-real Element of REAL
(cos . a) * (- (sin . PI)) is complex real ext-real Element of REAL
((sin . a) * (cos . PI)) + ((cos . a) * (- (sin . PI))) is complex real ext-real Element of REAL
(cos . a) * (cos . (- PI)) is complex real ext-real Element of REAL
(sin . a) * (sin . (- PI)) is complex real ext-real Element of REAL
((cos . a) * (cos . (- PI))) - ((sin . a) * (sin . (- PI))) is complex real ext-real Element of REAL
- ((sin . a) * (sin . (- PI))) is complex real ext-real set
((cos . a) * (cos . (- PI))) + (- ((sin . a) * (sin . (- PI)))) is complex real ext-real set
(cos . a) * (cos . PI) is complex real ext-real Element of REAL
((cos . a) * (cos . PI)) - ((sin . a) * (sin . (- PI))) is complex real ext-real Element of REAL
((cos . a) * (cos . PI)) + (- ((sin . a) * (sin . (- PI)))) is complex real ext-real set
(sin . a) * (- (sin . PI)) is complex real ext-real Element of REAL
((cos . a) * (cos . PI)) - ((sin . a) * (- (sin . PI))) is complex real ext-real Element of REAL
- ((sin . a) * (- (sin . PI))) is complex real ext-real set
((cos . a) * (cos . PI)) + (- ((sin . a) * (- (sin . PI)))) is complex real ext-real set
a is complex real ext-real set
a - PI is complex real ext-real Element of REAL
- PI is complex real ext-real set
a + (- PI) is complex real ext-real set
sin (a - PI) is complex real ext-real Element of REAL
sin a is complex real ext-real set
- (sin a) is complex real ext-real set
cos (a - PI) is complex real ext-real Element of REAL
cos a is complex real ext-real set
- (cos a) is complex real ext-real set
(sin a) * (cos PI) is complex real ext-real Element of REAL
(cos a) * (sin PI) is complex real ext-real Element of REAL
((sin a) * (cos PI)) - ((cos a) * (sin PI)) is complex real ext-real Element of REAL
- ((cos a) * (sin PI)) is complex real ext-real set
((sin a) * (cos PI)) + (- ((cos a) * (sin PI))) is complex real ext-real set
(cos a) * (cos PI) is complex real ext-real Element of REAL
(sin a) * (sin PI) is complex real ext-real Element of REAL
((cos a) * (cos PI)) + ((sin a) * (sin PI)) is complex real ext-real Element of REAL
PI / 2 is complex real ext-real Element of COMPLEX
].0,(PI / 2).[ is V61() V62() V63() Element of K19(REAL)
a is complex real ext-real set
b is complex real ext-real set
sin b is complex real ext-real set
sin a is complex real ext-real set
dom sin is set
].0,(PI / 2).[ /\ (dom sin) is V61() V62() V63() Element of K19(REAL)
sin . a is complex real ext-real Element of REAL
sin . b is complex real ext-real Element of REAL
].(PI / 2),PI.[ is V61() V62() V63() Element of K19(REAL)
a is complex real ext-real set
b is complex real ext-real set
sin a is complex real ext-real set
sin b is complex real ext-real set
dom sin is set
].(PI / 2),PI.[ /\ (dom sin) is V61() V62() V63() Element of K19(REAL)
sin . a is complex real ext-real Element of REAL
sin . b is complex real ext-real Element of REAL
a is complex real ext-real set
sin a is complex real ext-real set
b is complex real ext-real integer set
(2 * PI) * b is complex real ext-real Element of REAL
((2 * PI) * b) + a is complex real ext-real Element of REAL
sin (((2 * PI) * b) + a) is complex real ext-real Element of REAL
sin . a is complex real ext-real Element of REAL
sin . (((2 * PI) * b) + a) is complex real ext-real Element of REAL
- b is complex real ext-real integer set
(2 * PI) * (- b) is complex real ext-real Element of REAL
((2 * PI) * (- b)) + (((2 * PI) * b) + a) is complex real ext-real Element of REAL
sin . (((2 * PI) * (- b)) + (((2 * PI) * b) + a)) is complex real ext-real Element of REAL
sin (((2 * PI) * (- b)) + (((2 * PI) * b) + a)) is complex real ext-real Element of REAL
c is natural complex real ext-real integer V34() V61() V62() V63() V64() V65() V66() Element of NAT
(2 * PI) * c is complex real ext-real Element of REAL
((2 * PI) * c) + a is complex real ext-real Element of REAL
sin (((2 * PI) * c) + a) is complex real ext-real Element of REAL
r is complex real ext-real Element of REAL
sin r is complex real ext-real Element of REAL
c is natural complex real ext-real integer V34() V61() V62() V63() V64() V65() V66() Element of NAT
(2 * PI) * c is complex real ext-real Element of REAL
((2 * PI) * c) + r is complex real ext-real Element of REAL
sin (((2 * PI) * c) + r) is complex real ext-real Element of REAL
a is complex real ext-real set
cos a is complex real ext-real set
b is complex real ext-real integer set
(2 * PI) * b is complex real ext-real Element of REAL
((2 * PI) * b) + a is complex real ext-real Element of REAL
cos (((2 * PI) * b) + a) is complex real ext-real Element of REAL
cos . a is complex real ext-real Element of REAL
cos . (((2 * PI) * b) + a) is complex real ext-real Element of REAL
- b is complex real ext-real integer set
(2 * PI) * (- b) is complex real ext-real Element of REAL
((2 * PI) * (- b)) + (((2 * PI) * b) + a) is complex real ext-real Element of REAL
cos . (((2 * PI) * (- b)) + (((2 * PI) * b) + a)) is complex real ext-real Element of REAL
cos (((2 * PI) * (- b)) + (((2 * PI) * b) + a)) is complex real ext-real Element of REAL
c is natural complex real ext-real integer V34() V61() V62() V63() V64() V65() V66() Element of NAT
(2 * PI) * c is complex real ext-real Element of REAL
((2 * PI) * c) + a is complex real ext-real Element of REAL
cos (((2 * PI) * c) + a) is complex real ext-real Element of REAL
r is complex real ext-real Element of REAL
cos r is complex real ext-real Element of REAL
c is natural complex real ext-real integer V34() V61() V62() V63() V64() V65() V66() Element of NAT
(2 * PI) * c is complex real ext-real Element of REAL
((2 * PI) * c) + r is complex real ext-real Element of REAL
cos (((2 * PI) * c) + r) is complex real ext-real Element of REAL
a is complex real ext-real set
sin a is complex real ext-real set
cos a is complex real ext-real set
a / (2 * PI) is complex real ext-real Element of COMPLEX
(2 * PI) " is complex real ext-real set
a * ((2 * PI) ") is complex real ext-real set
[\(a / (2 * PI))/] is complex real ext-real integer set
- [\(a / (2 * PI))/] is complex real ext-real integer set
(2 * PI) * (- [\(a / (2 * PI))/]) is complex real ext-real Element of REAL
((2 * PI) * (- [\(a / (2 * PI))/])) + a is complex real ext-real Element of REAL
b is complex real ext-real set
cos b is complex real ext-real set
sin b is complex real ext-real set
a is complex real ext-real set
b is complex real ext-real set
sin a is complex real ext-real set
sin b is complex real ext-real set
cos a is complex real ext-real set
cos b is complex real ext-real set
a - b is complex real ext-real set
- b is complex real ext-real set
a + (- b) is complex real ext-real set
cos (a - b) is complex real ext-real set
(cos a) * (cos b) is complex real ext-real set
(sin a) * (sin b) is complex real ext-real set
((cos a) * (cos b)) + ((sin a) * (sin b)) is complex real ext-real set
sin (a - b) is complex real ext-real set
(sin a) * (cos b) is complex real ext-real set
(cos a) * (sin b) is complex real ext-real set
((sin a) * (cos b)) - ((cos a) * (sin b)) is complex real ext-real set
- ((cos a) * (sin b)) is complex real ext-real set
((sin a) * (cos b)) + (- ((cos a) * (sin b))) is complex real ext-real set
b - a is complex real ext-real set
- a is complex real ext-real set
b + (- a) is complex real ext-real set
cos (b - a) is complex real ext-real set
sin (b - a) is complex real ext-real set
(sin b) * (cos a) is complex real ext-real set
(cos b) * (sin a) is complex real ext-real set
((sin b) * (cos a)) - ((cos b) * (sin a)) is complex real ext-real set
- ((cos b) * (sin a)) is complex real ext-real set
((sin b) * (cos a)) + (- ((cos b) * (sin a))) is complex real ext-real set
(2 * PI) + b is complex real ext-real Element of REAL
a + 0 is complex real ext-real Element of REAL
b + 0 is complex real ext-real Element of REAL
a + 0 is complex real ext-real Element of REAL
(2 * PI) + a is complex real ext-real Element of REAL
b + 0 is complex real ext-real Element of REAL
a is complex set
|.a.| is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
cos (Arg a) is complex real ext-real Element of REAL
|.a.| * (cos (Arg a)) is complex real ext-real Element of REAL
sin (Arg a) is complex real ext-real Element of REAL
|.a.| * (sin (Arg a)) is complex real ext-real Element of REAL
(|.a.| * (sin (Arg a))) * <i> is complex set
(|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) is complex set
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
Arg 0 is complex real ext-real Element of REAL
a is complex set
Arg a is complex real ext-real Element of REAL
- a is complex set
Arg (- a) is complex real ext-real Element of REAL
(Arg a) + PI is complex real ext-real Element of REAL
(Arg a) - PI is complex real ext-real Element of REAL
- PI is complex real ext-real set
(Arg a) + (- PI) is complex real ext-real set
|.a.| is complex real ext-real Element of REAL
cos (Arg a) is complex real ext-real Element of REAL
|.a.| * (cos (Arg a)) is complex real ext-real Element of REAL
sin (Arg a) is complex real ext-real Element of REAL
|.a.| * (sin (Arg a)) is complex real ext-real Element of REAL
(|.a.| * (sin (Arg a))) * <i> is complex set
(|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) is complex set
- (|.a.| * (cos (Arg a))) is complex real ext-real Element of REAL
- (|.a.| * (sin (Arg a))) is complex real ext-real Element of REAL
(- (|.a.| * (sin (Arg a)))) * <i> is complex set
(- (|.a.| * (cos (Arg a)))) + ((- (|.a.| * (sin (Arg a)))) * <i>) is complex set
(2 * PI) + PI is complex real ext-real Element of REAL
(Arg a) + 0 is complex real ext-real Element of REAL
|.(- a).| is complex real ext-real Element of REAL
cos (Arg (- a)) is complex real ext-real Element of REAL
|.(- a).| * (cos (Arg (- a))) is complex real ext-real Element of REAL
sin (Arg (- a)) is complex real ext-real Element of REAL
|.(- a).| * (sin (Arg (- a))) is complex real ext-real Element of REAL
(|.(- a).| * (sin (Arg (- a)))) * <i> is complex set
(|.(- a).| * (cos (Arg (- a)))) + ((|.(- a).| * (sin (Arg (- a)))) * <i>) is complex set
|.a.| * (sin (Arg (- a))) is complex real ext-real Element of REAL
- (sin (Arg a)) is complex real ext-real Element of REAL
|.a.| * (- (sin (Arg a))) is complex real ext-real Element of REAL
sin ((Arg a) + PI) is complex real ext-real Element of REAL
|.a.| * (cos (Arg (- a))) is complex real ext-real Element of REAL
- (cos (Arg a)) is complex real ext-real Element of REAL
|.a.| * (- (cos (Arg a))) is complex real ext-real Element of REAL
cos ((Arg a) + PI) is complex real ext-real Element of REAL
PI + PI is complex real ext-real Element of REAL
PI - PI is complex real ext-real Element of REAL
PI + (- PI) is complex real ext-real set
sin ((Arg a) - PI) is complex real ext-real Element of REAL
cos ((Arg a) - PI) is complex real ext-real Element of REAL
a is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
|.a.| is complex real ext-real Element of REAL
0 * <i> is complex set
a + (0 * <i>) is complex set
cos (Arg a) is complex real ext-real Element of REAL
|.a.| * (cos (Arg a)) is complex real ext-real Element of REAL
sin (Arg a) is complex real ext-real Element of REAL
|.a.| * (sin (Arg a)) is complex real ext-real Element of REAL
(|.a.| * (sin (Arg a))) * <i> is complex set
(|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) is complex set
a is complex set
Arg a is complex real ext-real Element of REAL
|.a.| is complex real ext-real Element of REAL
|.a.| * (cos 0) is complex real ext-real Element of REAL
|.a.| * (sin 0) is complex real ext-real Element of REAL
(|.a.| * (sin 0)) * <i> is complex set
(|.a.| * (cos 0)) + ((|.a.| * (sin 0)) * <i>) is complex set
a is complex set
Arg a is complex real ext-real Element of REAL
- a is complex set
Arg (- a) is complex real ext-real Element of REAL
PI + 0 is complex real ext-real Element of REAL
PI + (Arg a) is complex real ext-real Element of REAL
PI + PI is complex real ext-real Element of REAL
(PI + PI) - PI is complex real ext-real Element of REAL
- PI is complex real ext-real set
(PI + PI) + (- PI) is complex real ext-real set
(Arg (- a)) - PI is complex real ext-real Element of REAL
(Arg (- a)) + (- PI) is complex real ext-real set
- (- a) is complex set
Arg (- (- a)) is complex real ext-real Element of REAL
a is complex set
b is complex set
a - b is complex set
- b is complex set
a + (- b) is complex set
Arg (a - b) is complex real ext-real Element of REAL
b - a is complex set
- a is complex set
b + (- a) is complex set
Arg (b - a) is complex real ext-real Element of REAL
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
- (a - b) is complex set
Arg (- (a - b)) is complex real ext-real Element of REAL
].0,PI.[ is V61() V62() V63() Element of K19(REAL)
a is complex set
Arg a is complex real ext-real Element of REAL
Im a is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
(Im a) * <i> is complex set
0 + ((Im a) * <i>) is complex set
Re a is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
a is complex set
Arg a is complex real ext-real Element of REAL
sin (Arg a) is complex real ext-real Element of REAL
Im a is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
(Im a) * <i> is complex set
0 + ((Im a) * <i>) is complex set
Re a is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
a is complex set
Arg a is complex real ext-real Element of REAL
b is complex set
Arg b is complex real ext-real Element of REAL
a + b is complex set
Arg (a + b) is complex real ext-real Element of REAL
|.b.| is complex real ext-real Element of REAL
0 * <i> is complex set
|.b.| + (0 * <i>) is complex set
|.a.| is complex real ext-real Element of REAL
|.a.| + (0 * <i>) is complex set
Im a is complex real ext-real Element of REAL
|.a.| + |.b.| is complex real ext-real Element of REAL
(|.a.| + |.b.|) + (0 * <i>) is complex set
Im b is complex real ext-real Element of REAL
Im (a + b) is complex real ext-real Element of REAL
(Im a) + (Im b) is complex real ext-real Element of REAL
Im a is complex real ext-real Element of REAL
Im b is complex real ext-real Element of REAL
Im (a + b) is complex real ext-real Element of REAL
(Im a) + (Im b) is complex real ext-real Element of REAL
Im b is complex real ext-real Element of REAL
Im (a + b) is complex real ext-real Element of REAL
(Im a) + (Im b) is complex real ext-real Element of REAL
a is complex set
Arg a is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
Im a is complex real ext-real Element of REAL
|.a.| is complex real ext-real Element of REAL
0 * <i> is complex set
|.a.| + (0 * <i>) is complex set
(Re a) + (0 * <i>) is complex set
a is complex set
Arg a is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
Im a is complex real ext-real Element of REAL
|.a.| is complex real ext-real Element of REAL
|.a.| * (cos PI) is complex real ext-real Element of REAL
|.a.| * (sin PI) is complex real ext-real Element of REAL
(|.a.| * (sin PI)) * <i> is complex set
(|.a.| * (cos PI)) + ((|.a.| * (sin PI)) * <i>) is complex set
- |.a.| is complex real ext-real Element of REAL
- (- |.a.|) is complex real ext-real Element of REAL
0 * <i> is complex set
(Re a) + (0 * <i>) is complex set
a is complex set
Im a is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
0 * <i> is complex set
(Re a) + (0 * <i>) is complex set
Arg ((Re a) + (0 * <i>)) is complex real ext-real Element of REAL
a is complex set
Arg a is complex real ext-real Element of REAL
Im a is complex real ext-real Element of REAL
a is complex Element of COMPLEX
- a is complex Element of COMPLEX
Arg (- a) is complex real ext-real Element of REAL
cos (Arg (- a)) is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
cos (Arg a) is complex real ext-real Element of REAL
- (cos (Arg a)) is complex real ext-real Element of REAL
sin (Arg (- a)) is complex real ext-real Element of REAL
sin (Arg a) is complex real ext-real Element of REAL
- (sin (Arg a)) is complex real ext-real Element of REAL
|.(- a).| is complex real ext-real Element of REAL
|.a.| is complex real ext-real Element of REAL
|.a.| * (cos (Arg a)) is complex real ext-real Element of REAL
|.a.| * (sin (Arg a)) is complex real ext-real Element of REAL
(|.a.| * (sin (Arg a))) * <i> is complex set
(|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) is complex set
|.(- a).| * (cos (Arg (- a))) is complex real ext-real Element of REAL
|.(- a).| * (sin (Arg (- a))) is complex real ext-real Element of REAL
(|.(- a).| * (sin (Arg (- a)))) * <i> is complex set
(|.(- a).| * (cos (Arg (- a)))) + ((|.(- a).| * (sin (Arg (- a)))) * <i>) is complex set
0 * <i> is complex set
0 + (0 * <i>) is complex set
|.a.| * (cos (Arg (- a))) is complex real ext-real Element of REAL
(|.a.| * (cos (Arg a))) + (|.a.| * (cos (Arg (- a)))) is complex real ext-real Element of REAL
|.a.| * (sin (Arg (- a))) is complex real ext-real Element of REAL
(|.a.| * (sin (Arg a))) + (|.a.| * (sin (Arg (- a)))) is complex real ext-real Element of REAL
((|.a.| * (sin (Arg a))) + (|.a.| * (sin (Arg (- a))))) * <i> is complex set
((|.a.| * (cos (Arg a))) + (|.a.| * (cos (Arg (- a))))) + (((|.a.| * (sin (Arg a))) + (|.a.| * (sin (Arg (- a))))) * <i>) is complex set
(sin (Arg a)) + (sin (Arg (- a))) is complex real ext-real Element of REAL
|.a.| * ((sin (Arg a)) + (sin (Arg (- a)))) is complex real ext-real Element of REAL
- (sin (Arg (- a))) is complex real ext-real Element of REAL
- (- (sin (Arg (- a)))) is complex real ext-real Element of REAL
(sin (Arg a)) + (- (- (sin (Arg (- a))))) is complex real ext-real Element of REAL
(cos (Arg a)) + (cos (Arg (- a))) is complex real ext-real Element of REAL
|.a.| * ((cos (Arg a)) + (cos (Arg (- a)))) is complex real ext-real Element of REAL
- (cos (Arg (- a))) is complex real ext-real Element of REAL
- (- (cos (Arg (- a)))) is complex real ext-real Element of REAL
(cos (Arg a)) + (- (- (cos (Arg (- a))))) is complex real ext-real Element of REAL
a is complex set
Arg a is complex real ext-real Element of REAL
cos (Arg a) is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
|.a.| is complex real ext-real Element of REAL
(Re a) / |.a.| is complex real ext-real Element of COMPLEX
|.a.| " is complex real ext-real set
(Re a) * (|.a.| ") is complex real ext-real set
sin (Arg a) is complex real ext-real Element of REAL
Im a is complex real ext-real Element of REAL
(Im a) / |.a.| is complex real ext-real Element of COMPLEX
(Im a) * (|.a.| ") is complex real ext-real set
|.a.| * (cos (Arg a)) is complex real ext-real Element of REAL
|.a.| * (sin (Arg a)) is complex real ext-real Element of REAL
(|.a.| * (sin (Arg a))) * <i> is complex set
(|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) is complex set
a is complex set
Arg a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
a * b is complex set
Arg (a * b) is complex real ext-real Element of REAL
sin (Arg a) is complex real ext-real Element of REAL
Im a is complex real ext-real Element of REAL
|.a.| is complex real ext-real Element of REAL
(Im a) / |.a.| is complex real ext-real Element of COMPLEX
|.a.| " is complex real ext-real set
(Im a) * (|.a.| ") is complex real ext-real set
|.(a * b).| is complex real ext-real Element of REAL
abs b is complex real ext-real Element of REAL
|.a.| * (abs b) is complex real ext-real Element of REAL
|.a.| * b is complex real ext-real Element of REAL
cos (Arg a) is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
(Re a) / |.a.| is complex real ext-real Element of COMPLEX
(Re a) * (|.a.| ") is complex real ext-real set
0 * <i> is complex set
b + (0 * <i>) is complex set
Re b is complex real ext-real Element of REAL
Im b is complex real ext-real Element of REAL
Im (a * b) is complex real ext-real Element of REAL
(Re a) * 0 is complex real ext-real Element of REAL
b * (Im a) is complex real ext-real Element of REAL
((Re a) * 0) + (b * (Im a)) is complex real ext-real Element of REAL
sin (Arg (a * b)) is complex real ext-real Element of REAL
(Im (a * b)) / |.(a * b).| is complex real ext-real Element of COMPLEX
|.(a * b).| " is complex real ext-real set
(Im (a * b)) * (|.(a * b).| ") is complex real ext-real set
Re (a * b) is complex real ext-real Element of REAL
(Re a) * b is complex real ext-real Element of REAL
0 * (Im a) is complex real ext-real Element of REAL
((Re a) * b) - (0 * (Im a)) is complex real ext-real Element of REAL
- (0 * (Im a)) is complex real ext-real set
((Re a) * b) + (- (0 * (Im a))) is complex real ext-real set
b * (Re a) is complex real ext-real Element of REAL
cos (Arg (a * b)) is complex real ext-real Element of REAL
(Re (a * b)) / |.(a * b).| is complex real ext-real Element of COMPLEX
(Re (a * b)) * (|.(a * b).| ") is complex real ext-real set
a is complex set
- a is complex set
Arg (- a) is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
a * b is complex set
Arg (a * b) is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
cos (Arg a) is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
|.a.| is complex real ext-real Element of REAL
(Re a) / |.a.| is complex real ext-real Element of COMPLEX
|.a.| " is complex real ext-real set
(Re a) * (|.a.| ") is complex real ext-real set
sin (Arg a) is complex real ext-real Element of REAL
Im a is complex real ext-real Element of REAL
(Im a) / |.a.| is complex real ext-real Element of COMPLEX
(Im a) * (|.a.| ") is complex real ext-real set
|.(a * b).| is complex real ext-real Element of REAL
abs b is complex real ext-real Element of REAL
|.a.| * (abs b) is complex real ext-real Element of REAL
- b is complex real ext-real Element of REAL
|.a.| * (- b) is complex real ext-real Element of REAL
0 * <i> is complex set
b + (0 * <i>) is complex set
Re b is complex real ext-real Element of REAL
Im b is complex real ext-real Element of REAL
Im (a * b) is complex real ext-real Element of REAL
(Re a) * 0 is complex real ext-real Element of REAL
b * (Im a) is complex real ext-real Element of REAL
((Re a) * 0) + (b * (Im a)) is complex real ext-real Element of REAL
sin (Arg (a * b)) is complex real ext-real Element of REAL
|.a.| * b is complex real ext-real Element of REAL
- (|.a.| * b) is complex real ext-real Element of REAL
(b * (Im a)) / (- (|.a.| * b)) is complex real ext-real Element of COMPLEX
(- (|.a.| * b)) " is complex real ext-real set
(b * (Im a)) * ((- (|.a.| * b)) ") is complex real ext-real set
(b * (Im a)) / (|.a.| * b) is complex real ext-real Element of COMPLEX
(|.a.| * b) " is complex real ext-real set
(b * (Im a)) * ((|.a.| * b) ") is complex real ext-real set
- ((b * (Im a)) / (|.a.| * b)) is complex real ext-real Element of COMPLEX
- (sin (Arg a)) is complex real ext-real Element of REAL
sin (Arg (- a)) is complex real ext-real Element of REAL
Re (a * b) is complex real ext-real Element of REAL
(Re a) * b is complex real ext-real Element of REAL
0 * (Im a) is complex real ext-real Element of REAL
((Re a) * b) - (0 * (Im a)) is complex real ext-real Element of REAL
- (0 * (Im a)) is complex real ext-real set
((Re a) * b) + (- (0 * (Im a))) is complex real ext-real set
b * (Re a) is complex real ext-real Element of REAL
cos (Arg (a * b)) is complex real ext-real Element of REAL
(b * (Re a)) / (- (|.a.| * b)) is complex real ext-real Element of COMPLEX
(b * (Re a)) * ((- (|.a.| * b)) ") is complex real ext-real set
(b * (Re a)) / (|.a.| * b) is complex real ext-real Element of COMPLEX
(b * (Re a)) * ((|.a.| * b) ") is complex real ext-real set
- ((b * (Re a)) / (|.a.| * b)) is complex real ext-real Element of COMPLEX
- (cos (Arg a)) is complex real ext-real Element of REAL
cos (Arg (- a)) is complex real ext-real Element of REAL
a is complex set
b is complex set
b *' is complex Element of COMPLEX
a * (b *') is complex set
a is complex Element of COMPLEX
Re a is complex real ext-real Element of REAL
Im a is complex real ext-real Element of REAL
b is complex Element of COMPLEX
(a,b) is complex Element of COMPLEX
b *' is complex Element of COMPLEX
a * (b *') is complex set
Re b is complex real ext-real Element of REAL
(Re a) * (Re b) is complex real ext-real Element of REAL
Im b is complex real ext-real Element of REAL
(Im a) * (Im b) is complex real ext-real Element of REAL
((Re a) * (Re b)) + ((Im a) * (Im b)) is complex real ext-real Element of REAL
(Re a) * (Im b) is complex real ext-real Element of REAL
- ((Re a) * (Im b)) is complex real ext-real Element of REAL
(Im a) * (Re b) is complex real ext-real Element of REAL
(- ((Re a) * (Im b))) + ((Im a) * (Re b)) is complex real ext-real Element of REAL
((- ((Re a) * (Im b))) + ((Im a) * (Re b))) * <i> is complex set
(((Re a) * (Re b)) + ((Im a) * (Im b))) + (((- ((Re a) * (Im b))) + ((Im a) * (Re b))) * <i>) is complex set
(Im a) * <i> is complex set
(Re a) + ((Im a) * <i>) is complex set
(Im b) * <i> is complex set
(Re b) - ((Im b) * <i>) is complex set
- ((Im b) * <i>) is complex set
(Re b) + (- ((Im b) * <i>)) is complex set
a is complex Element of COMPLEX
(a,a) is complex Element of COMPLEX
a *' is complex Element of COMPLEX
a * (a *') is complex set
Re a is complex real ext-real Element of REAL
(Re a) * (Re a) is complex real ext-real Element of REAL
Im a is complex real ext-real Element of REAL
(Im a) * (Im a) is complex real ext-real Element of REAL
((Re a) * (Re a)) + ((Im a) * (Im a)) is complex real ext-real Element of REAL
(Re a) ^2 is complex real ext-real Element of REAL
(Re a) * (Re a) is complex real ext-real set
(Im a) ^2 is complex real ext-real Element of REAL
(Im a) * (Im a) is complex real ext-real set
((Re a) ^2) + ((Im a) ^2) is complex real ext-real Element of REAL
(Im a) * (Re a) is complex real ext-real Element of REAL
- ((Im a) * (Re a)) is complex real ext-real Element of REAL
(- ((Im a) * (Re a))) + ((Im a) * (Re a)) is complex real ext-real Element of REAL
((- ((Im a) * (Re a))) + ((Im a) * (Re a))) * <i> is complex set
(((Re a) * (Re a)) + ((Im a) * (Im a))) + (((- ((Im a) * (Re a))) + ((Im a) * (Re a))) * <i>) is complex set
a is complex Element of COMPLEX
(a,a) is complex Element of COMPLEX
a *' is complex Element of COMPLEX
a * (a *') is complex set
|.a.| is complex real ext-real Element of REAL
|.a.| ^2 is complex real ext-real Element of REAL
|.a.| * |.a.| is complex real ext-real set
Re (a,a) is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
(Re a) ^2 is complex real ext-real Element of REAL
(Re a) * (Re a) is complex real ext-real set
Im a is complex real ext-real Element of REAL
(Im a) ^2 is complex real ext-real Element of REAL
(Im a) * (Im a) is complex real ext-real set
((Re a) ^2) + ((Im a) ^2) is complex real ext-real Element of REAL
sqrt (((Re a) ^2) + ((Im a) ^2)) is complex real ext-real Element of REAL
0 * <i> is complex set
(|.a.| ^2) + (0 * <i>) is complex set
a is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
b is complex Element of COMPLEX
(a,b) is complex Element of COMPLEX
b *' is complex Element of COMPLEX
a * (b *') is complex set
|.(a,b).| is complex real ext-real Element of REAL
|.b.| is complex real ext-real Element of REAL
|.a.| * |.b.| is complex real ext-real Element of REAL
|.(b *').| is complex real ext-real Element of REAL
|.a.| * |.(b *').| is complex real ext-real Element of REAL
a is complex Element of COMPLEX
(a,a) is complex Element of COMPLEX
a *' is complex Element of COMPLEX
a * (a *') is complex set
Re a is complex real ext-real Element of REAL
(Re a) ^2 is complex real ext-real Element of REAL
(Re a) * (Re a) is complex real ext-real set
Im a is complex real ext-real Element of REAL
(Im a) ^2 is complex real ext-real Element of REAL
(Im a) * (Im a) is complex real ext-real set
((Re a) ^2) + ((Im a) ^2) is complex real ext-real Element of REAL
a is complex Element of COMPLEX
b is complex Element of COMPLEX
(a,b) is complex Element of COMPLEX
b *' is complex Element of COMPLEX
a * (b *') is complex set
(b,a) is complex Element of COMPLEX
a *' is complex Element of COMPLEX
b * (a *') is complex set
(b,a) *' is complex Element of COMPLEX
a * (b *') is complex Element of COMPLEX
(a * (b *')) *' is complex Element of COMPLEX
((a * (b *')) *') *' is complex Element of COMPLEX
(b *') *' is complex Element of COMPLEX
((b *') *') * (a *') is complex Element of COMPLEX
(((b *') *') * (a *')) *' is complex Element of COMPLEX
a is complex Element of COMPLEX
b is complex Element of COMPLEX
a + b is complex Element of COMPLEX
c is complex Element of COMPLEX
((a + b),c) is complex Element of COMPLEX
c *' is complex Element of COMPLEX
(a + b) * (c *') is complex set
(a,c) is complex Element of COMPLEX
a * (c *') is complex set
(b,c) is complex Element of COMPLEX
b * (c *') is complex set
(a,c) + (b,c) is complex Element of COMPLEX
a is complex Element of COMPLEX
b is complex Element of COMPLEX
(a,b) is complex Element of COMPLEX
b *' is complex Element of COMPLEX
a * (b *') is complex set
c is complex Element of COMPLEX
b + c is complex Element of COMPLEX
(a,(b + c)) is complex Element of COMPLEX
(b + c) *' is complex Element of COMPLEX
a * ((b + c) *') is complex set
(a,c) is complex Element of COMPLEX
c *' is complex Element of COMPLEX
a * (c *') is complex set
(a,b) + (a,c) is complex Element of COMPLEX
(b *') + (c *') is complex Element of COMPLEX
a * ((b *') + (c *')) is complex Element of COMPLEX
a is complex Element of COMPLEX
b is complex Element of COMPLEX
a * b is complex Element of COMPLEX
c is complex Element of COMPLEX
((a * b),c) is complex Element of COMPLEX
c *' is complex Element of COMPLEX
(a * b) * (c *') is complex set
(b,c) is complex Element of COMPLEX
b * (c *') is complex set
a * (b,c) is complex Element of COMPLEX
a is complex Element of COMPLEX
b is complex Element of COMPLEX
b *' is complex Element of COMPLEX
c is complex Element of COMPLEX
b * c is complex Element of COMPLEX
(a,(b * c)) is complex Element of COMPLEX
(b * c) *' is complex Element of COMPLEX
a * ((b * c) *') is complex set
(a,c) is complex Element of COMPLEX
c *' is complex Element of COMPLEX
a * (c *') is complex set
(b *') * (a,c) is complex Element of COMPLEX
(b *') * (c *') is complex Element of COMPLEX
a * ((b *') * (c *')) is complex Element of COMPLEX
a is complex Element of COMPLEX
a *' is complex Element of COMPLEX
b is complex Element of COMPLEX
a * b is complex Element of COMPLEX
c is complex Element of COMPLEX
((a * b),c) is complex Element of COMPLEX
c *' is complex Element of COMPLEX
(a * b) * (c *') is complex set
(a *') * c is complex Element of COMPLEX
(b,((a *') * c)) is complex Element of COMPLEX
((a *') * c) *' is complex Element of COMPLEX
b * (((a *') * c) *') is complex set
(a *') *' is complex Element of COMPLEX
((a *') *') * (c *') is complex Element of COMPLEX
b * (((a *') *') * (c *')) is complex Element of COMPLEX
a is complex Element of COMPLEX
b is complex Element of COMPLEX
a * b is complex Element of COMPLEX
c is complex Element of COMPLEX
r is complex Element of COMPLEX
c * r is complex Element of COMPLEX
(a * b) + (c * r) is complex Element of COMPLEX
A is complex Element of COMPLEX
(((a * b) + (c * r)),A) is complex Element of COMPLEX
A *' is complex Element of COMPLEX
((a * b) + (c * r)) * (A *') is complex set
(b,A) is complex Element of COMPLEX
b * (A *') is complex set
a * (b,A) is complex Element of COMPLEX
(r,A) is complex Element of COMPLEX
r * (A *') is complex set
c * (r,A) is complex Element of COMPLEX
(a * (b,A)) + (c * (r,A)) is complex Element of COMPLEX
a is complex Element of COMPLEX
b is complex Element of COMPLEX
b *' is complex Element of COMPLEX
c is complex Element of COMPLEX
b * c is complex Element of COMPLEX
(a,c) is complex Element of COMPLEX
c *' is complex Element of COMPLEX
a * (c *') is complex set
(b *') * (a,c) is complex Element of COMPLEX
r is complex Element of COMPLEX
r *' is complex Element of COMPLEX
A is complex Element of COMPLEX
r * A is complex Element of COMPLEX
(b * c) + (r * A) is complex Element of COMPLEX
(a,((b * c) + (r * A))) is complex Element of COMPLEX
((b * c) + (r * A)) *' is complex Element of COMPLEX
a * (((b * c) + (r * A)) *') is complex set
(a,A) is complex Element of COMPLEX
A *' is complex Element of COMPLEX
a * (A *') is complex set
(r *') * (a,A) is complex Element of COMPLEX
((b *') * (a,c)) + ((r *') * (a,A)) is complex Element of COMPLEX
(a,(b * c)) is complex Element of COMPLEX
(b * c) *' is complex Element of COMPLEX
a * ((b * c) *') is complex set
(a,(r * A)) is complex Element of COMPLEX
(r * A) *' is complex Element of COMPLEX
a * ((r * A) *') is complex set
(a,(b * c)) + (a,(r * A)) is complex Element of COMPLEX
((b *') * (a,c)) + (a,(r * A)) is complex Element of COMPLEX
a is complex Element of COMPLEX
- a is complex Element of COMPLEX
b is complex Element of COMPLEX
((- a),b) is complex Element of COMPLEX
b *' is complex Element of COMPLEX
(- a) * (b *') is complex set
- b is complex Element of COMPLEX
(a,(- b)) is complex Element of COMPLEX
(- b) *' is complex Element of COMPLEX
a * ((- b) *') is complex set
- (1r *') is complex Element of COMPLEX
(a,b) is complex Element of COMPLEX
a * (b *') is complex set
(- (1r *')) * (a,b) is complex Element of COMPLEX
- 1r is complex Element of COMPLEX
(- 1r) *' is complex Element of COMPLEX
((- 1r) *') * (a,b) is complex Element of COMPLEX
(- 1r) * b is complex Element of COMPLEX
(a,((- 1r) * b)) is complex Element of COMPLEX
((- 1r) * b) *' is complex Element of COMPLEX
a * (((- 1r) * b) *') is complex set
a is complex Element of COMPLEX
- a is complex Element of COMPLEX
b is complex Element of COMPLEX
((- a),b) is complex Element of COMPLEX
b *' is complex Element of COMPLEX
(- a) * (b *') is complex set
(a,b) is complex Element of COMPLEX
a * (b *') is complex set
- (a,b) is complex Element of COMPLEX
a is complex Element of COMPLEX
b is complex Element of COMPLEX
(a,b) is complex Element of COMPLEX
b *' is complex Element of COMPLEX
a * (b *') is complex set
- (a,b) is complex Element of COMPLEX
- b is complex Element of COMPLEX
(a,(- b)) is complex Element of COMPLEX
(- b) *' is complex Element of COMPLEX
a * ((- b) *') is complex set
- a is complex Element of COMPLEX
((- a),b) is complex Element of COMPLEX
(- a) * (b *') is complex set
a is complex Element of COMPLEX
- a is complex Element of COMPLEX
b is complex Element of COMPLEX
- b is complex Element of COMPLEX
((- a),(- b)) is complex Element of COMPLEX
(- b) *' is complex Element of COMPLEX
(- a) * ((- b) *') is complex set
(a,b) is complex Element of COMPLEX
b *' is complex Element of COMPLEX
a * (b *') is complex set
(a,(- b)) is complex Element of COMPLEX
a * ((- b) *') is complex set
- (a,(- b)) is complex Element of COMPLEX
- (a,b) is complex Element of COMPLEX
- (- (a,b)) is complex Element of COMPLEX
a is complex Element of COMPLEX
b is complex Element of COMPLEX
a - b is complex Element of COMPLEX
- b is complex set
a + (- b) is complex set
c is complex Element of COMPLEX
((a - b),c) is complex Element of COMPLEX
c *' is complex Element of COMPLEX
(a - b) * (c *') is complex set
(a,c) is complex Element of COMPLEX
a * (c *') is complex set
(b,c) is complex Element of COMPLEX
b * (c *') is complex set
(a,c) - (b,c) is complex Element of COMPLEX
- (b,c) is complex set
(a,c) + (- (b,c)) is complex set
a is complex Element of COMPLEX
b is complex Element of COMPLEX
(a,b) is complex Element of COMPLEX
b *' is complex Element of COMPLEX
a * (b *') is complex set
c is complex Element of COMPLEX
b - c is complex Element of COMPLEX
- c is complex set
b + (- c) is complex set
(a,(b - c)) is complex Element of COMPLEX
(b - c) *' is complex Element of COMPLEX
a * ((b - c) *') is complex set
(a,c) is complex Element of COMPLEX
c *' is complex Element of COMPLEX
a * (c *') is complex set
(a,b) - (a,c) is complex Element of COMPLEX
- (a,c) is complex set
(a,b) + (- (a,c)) is complex set
(b *') - (c *') is complex Element of COMPLEX
- (c *') is complex set
(b *') + (- (c *')) is complex set
a * ((b *') - (c *')) is complex Element of COMPLEX
a is complex Element of COMPLEX
(a,a) is complex Element of COMPLEX
a *' is complex Element of COMPLEX
a * (a *') is complex set
b is complex Element of COMPLEX
a + b is complex Element of COMPLEX
((a + b),(a + b)) is complex Element of COMPLEX
(a + b) *' is complex Element of COMPLEX
(a + b) * ((a + b) *') is complex set
(a,b) is complex Element of COMPLEX
b *' is complex Element of COMPLEX
a * (b *') is complex set
(a,a) + (a,b) is complex Element of COMPLEX
(b,a) is complex Element of COMPLEX
b * (a *') is complex set
((a,a) + (a,b)) + (b,a) is complex Element of COMPLEX
(b,b) is complex Element of COMPLEX
b * (b *') is complex set
(((a,a) + (a,b)) + (b,a)) + (b,b) is complex Element of COMPLEX
(a,(a + b)) is complex Element of COMPLEX
a * ((a + b) *') is complex set
(b,(a + b)) is complex Element of COMPLEX
b * ((a + b) *') is complex set
(a,(a + b)) + (b,(a + b)) is complex Element of COMPLEX
((a,a) + (a,b)) + (b,(a + b)) is complex Element of COMPLEX
(b,a) + (b,b) is complex Element of COMPLEX
((a,a) + (a,b)) + ((b,a) + (b,b)) is complex Element of COMPLEX
a is complex Element of COMPLEX
(a,a) is complex Element of COMPLEX
a *' is complex Element of COMPLEX
a * (a *') is complex set
b is complex Element of COMPLEX
a - b is complex Element of COMPLEX
- b is complex set
a + (- b) is complex set
((a - b),(a - b)) is complex Element of COMPLEX
(a - b) *' is complex Element of COMPLEX
(a - b) * ((a - b) *') is complex set
(a,b) is complex Element of COMPLEX
b *' is complex Element of COMPLEX
a * (b *') is complex set
(a,a) - (a,b) is complex Element of COMPLEX
- (a,b) is complex set
(a,a) + (- (a,b)) is complex set
(b,a) is complex Element of COMPLEX
b * (a *') is complex set
((a,a) - (a,b)) - (b,a) is complex Element of COMPLEX
- (b,a) is complex set
((a,a) - (a,b)) + (- (b,a)) is complex set
(b,b) is complex Element of COMPLEX
b * (b *') is complex set
(((a,a) - (a,b)) - (b,a)) + (b,b) is complex Element of COMPLEX
(a,(a - b)) is complex Element of COMPLEX
a * ((a - b) *') is complex set
(b,(a - b)) is complex Element of COMPLEX
b * ((a - b) *') is complex set
(a,(a - b)) - (b,(a - b)) is complex Element of COMPLEX
- (b,(a - b)) is complex set
(a,(a - b)) + (- (b,(a - b))) is complex set
((a,a) - (a,b)) - (b,(a - b)) is complex Element of COMPLEX
((a,a) - (a,b)) + (- (b,(a - b))) is complex set
(b,a) - (b,b) is complex Element of COMPLEX
- (b,b) is complex set
(b,a) + (- (b,b)) is complex set
((a,a) - (a,b)) - ((b,a) - (b,b)) is complex Element of COMPLEX
- ((b,a) - (b,b)) is complex set
((a,a) - (a,b)) + (- ((b,a) - (b,b))) is complex set
a is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
|.a.| ^2 is complex real ext-real Element of REAL
|.a.| * |.a.| is complex real ext-real set
Re a is complex real ext-real Element of REAL
(Re a) ^2 is complex real ext-real Element of REAL
(Re a) * (Re a) is complex real ext-real set
Im a is complex real ext-real Element of REAL
(Im a) ^2 is complex real ext-real Element of REAL
(Im a) * (Im a) is complex real ext-real set
((Re a) ^2) + ((Im a) ^2) is complex real ext-real Element of REAL
a * a is complex Element of COMPLEX
|.(a * a).| is complex real ext-real Element of REAL
a is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
b is complex Element of COMPLEX
(a,b) is complex Element of COMPLEX
b *' is complex Element of COMPLEX
a * (b *') is complex set
Re (a,b) is complex real ext-real Element of REAL
Im (a,b) is complex real ext-real Element of REAL
|.b.| is complex real ext-real Element of REAL
|.a.| * |.b.| is complex real ext-real Element of REAL
- (|.a.| * |.b.|) is complex real ext-real Element of REAL
(|.a.| * |.b.|) ^2 is complex real ext-real Element of REAL
(|.a.| * |.b.|) * (|.a.| * |.b.|) is complex real ext-real set
|.(a,b).| is complex real ext-real Element of REAL
|.(a,b).| ^2 is complex real ext-real Element of REAL
|.(a,b).| * |.(a,b).| is complex real ext-real set
0 ^2 is complex real ext-real Element of REAL
0 * 0 is zero complex real ext-real non positive non negative integer V61() V62() V63() V64() V65() V66() V67() set
(Im (a,b)) ^2 is complex real ext-real Element of REAL
(Im (a,b)) * (Im (a,b)) is complex real ext-real set
(0 ^2) + ((Im (a,b)) ^2) is complex real ext-real Element of REAL
(Re (a,b)) ^2 is complex real ext-real Element of REAL
(Re (a,b)) * (Re (a,b)) is complex real ext-real set
((Re (a,b)) ^2) + ((Im (a,b)) ^2) is complex real ext-real Element of REAL
a is complex set
|.a.| is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
b + (Arg a) is complex real ext-real Element of REAL
cos (b + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (cos (b + (Arg a))) is complex real ext-real Element of REAL
sin (b + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (sin (b + (Arg a))) is complex real ext-real Element of REAL
(|.a.| * (sin (b + (Arg a)))) * <i> is complex set
(|.a.| * (cos (b + (Arg a)))) + ((|.a.| * (sin (b + (Arg a)))) * <i>) is complex set
a is complex Element of COMPLEX
(a,0) is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
0 + (Arg a) is complex real ext-real Element of REAL
cos (0 + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (cos (0 + (Arg a))) is complex real ext-real Element of REAL
sin (0 + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (sin (0 + (Arg a))) is complex real ext-real Element of REAL
(|.a.| * (sin (0 + (Arg a)))) * <i> is complex set
(|.a.| * (cos (0 + (Arg a)))) + ((|.a.| * (sin (0 + (Arg a)))) * <i>) is complex set
a is complex real ext-real Element of REAL
b is complex set
(b,a) is complex Element of COMPLEX
|.b.| is complex real ext-real Element of REAL
Arg b is complex real ext-real Element of REAL
a + (Arg b) is complex real ext-real Element of REAL
cos (a + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos (a + (Arg b))) is complex real ext-real Element of REAL
sin (a + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin (a + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin (a + (Arg b)))) * <i> is complex set
(|.b.| * (cos (a + (Arg b)))) + ((|.b.| * (sin (a + (Arg b)))) * <i>) is complex set
0 * <i> is complex set
0 + (0 * <i>) is complex set
a is complex real ext-real Element of REAL
b is complex set
(b,a) is complex Element of COMPLEX
|.b.| is complex real ext-real Element of REAL
Arg b is complex real ext-real Element of REAL
a + (Arg b) is complex real ext-real Element of REAL
cos (a + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos (a + (Arg b))) is complex real ext-real Element of REAL
sin (a + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin (a + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin (a + (Arg b)))) * <i> is complex set
(|.b.| * (cos (a + (Arg b)))) + ((|.b.| * (sin (a + (Arg b)))) * <i>) is complex set
|.(b,a).| is complex real ext-real Element of REAL
Re (b,a) is complex real ext-real Element of REAL
Im (b,a) is complex real ext-real Element of REAL
(|.b.| * (cos (a + (Arg b)))) ^2 is complex real ext-real Element of REAL
(|.b.| * (cos (a + (Arg b)))) * (|.b.| * (cos (a + (Arg b)))) is complex real ext-real set
(|.b.| * (sin (a + (Arg b)))) ^2 is complex real ext-real Element of REAL
(|.b.| * (sin (a + (Arg b)))) * (|.b.| * (sin (a + (Arg b)))) is complex real ext-real set
((|.b.| * (cos (a + (Arg b)))) ^2) + ((|.b.| * (sin (a + (Arg b)))) ^2) is complex real ext-real Element of REAL
sqrt (((|.b.| * (cos (a + (Arg b)))) ^2) + ((|.b.| * (sin (a + (Arg b)))) ^2)) is complex real ext-real Element of REAL
|.b.| ^2 is complex real ext-real Element of REAL
|.b.| * |.b.| is complex real ext-real set
(cos (a + (Arg b))) ^2 is complex real ext-real Element of REAL
(cos (a + (Arg b))) * (cos (a + (Arg b))) is complex real ext-real set
(sin (a + (Arg b))) ^2 is complex real ext-real Element of REAL
(sin (a + (Arg b))) * (sin (a + (Arg b))) is complex real ext-real set
((cos (a + (Arg b))) ^2) + ((sin (a + (Arg b))) ^2) is complex real ext-real Element of REAL
(|.b.| ^2) * (((cos (a + (Arg b))) ^2) + ((sin (a + (Arg b))) ^2)) is complex real ext-real Element of REAL
sqrt ((|.b.| ^2) * (((cos (a + (Arg b))) ^2) + ((sin (a + (Arg b))) ^2))) is complex real ext-real Element of REAL
(|.b.| ^2) * 1 is complex real ext-real Element of REAL
sqrt ((|.b.| ^2) * 1) is complex real ext-real Element of REAL
a is complex real ext-real Element of REAL
b is complex set
(b,a) is complex Element of COMPLEX
|.b.| is complex real ext-real Element of REAL
Arg b is complex real ext-real Element of REAL
a + (Arg b) is complex real ext-real Element of REAL
cos (a + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos (a + (Arg b))) is complex real ext-real Element of REAL
sin (a + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin (a + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin (a + (Arg b)))) * <i> is complex set
(|.b.| * (cos (a + (Arg b)))) + ((|.b.| * (sin (a + (Arg b)))) * <i>) is complex set
Arg (b,a) is complex real ext-real Element of REAL
|.(b,a).| is complex real ext-real Element of REAL
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
(a + (Arg b)) / (2 * PI) is complex real ext-real Element of COMPLEX
(2 * PI) " is complex real ext-real set
(a + (Arg b)) * ((2 * PI) ") is complex real ext-real set
[\((a + (Arg b)) / (2 * PI))/] is complex real ext-real integer set
- [\((a + (Arg b)) / (2 * PI))/] is complex real ext-real integer set
(2 * PI) * (- [\((a + (Arg b)) / (2 * PI))/]) is complex real ext-real Element of REAL
((2 * PI) * (- [\((a + (Arg b)) / (2 * PI))/])) + (a + (Arg b)) is complex real ext-real Element of REAL
c is complex real ext-real set
r is complex real ext-real Element of REAL
cos r is complex real ext-real Element of REAL
sin r is complex real ext-real Element of REAL
a is complex Element of COMPLEX
Arg a is complex real ext-real Element of REAL
- (Arg a) is complex real ext-real Element of REAL
(a,(- (Arg a))) is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
(- (Arg a)) + (Arg a) is complex real ext-real Element of REAL
cos ((- (Arg a)) + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (cos ((- (Arg a)) + (Arg a))) is complex real ext-real Element of REAL
sin ((- (Arg a)) + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (sin ((- (Arg a)) + (Arg a))) is complex real ext-real Element of REAL
(|.a.| * (sin ((- (Arg a)) + (Arg a)))) * <i> is complex set
(|.a.| * (cos ((- (Arg a)) + (Arg a)))) + ((|.a.| * (sin ((- (Arg a)) + (Arg a)))) * <i>) is complex set
a is complex Element of COMPLEX
Re a is complex real ext-real Element of REAL
Im a is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
(a,b) is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
b + (Arg a) is complex real ext-real Element of REAL
cos (b + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (cos (b + (Arg a))) is complex real ext-real Element of REAL
sin (b + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (sin (b + (Arg a))) is complex real ext-real Element of REAL
(|.a.| * (sin (b + (Arg a)))) * <i> is complex set
(|.a.| * (cos (b + (Arg a)))) + ((|.a.| * (sin (b + (Arg a)))) * <i>) is complex set
Re (a,b) is complex real ext-real Element of REAL
cos b is complex real ext-real Element of REAL
(Re a) * (cos b) is complex real ext-real Element of REAL
sin b is complex real ext-real Element of REAL
(Im a) * (sin b) is complex real ext-real Element of REAL
((Re a) * (cos b)) - ((Im a) * (sin b)) is complex real ext-real Element of REAL
- ((Im a) * (sin b)) is complex real ext-real set
((Re a) * (cos b)) + (- ((Im a) * (sin b))) is complex real ext-real set
Im (a,b) is complex real ext-real Element of REAL
(Re a) * (sin b) is complex real ext-real Element of REAL
(Im a) * (cos b) is complex real ext-real Element of REAL
((Re a) * (sin b)) + ((Im a) * (cos b)) is complex real ext-real Element of REAL
cos (Arg a) is complex real ext-real Element of REAL
|.a.| * (cos (Arg a)) is complex real ext-real Element of REAL
sin (Arg a) is complex real ext-real Element of REAL
|.a.| * (sin (Arg a)) is complex real ext-real Element of REAL
(|.a.| * (sin (Arg a))) * <i> is complex set
(|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) is complex set
(cos b) * (cos (Arg a)) is complex real ext-real Element of REAL
(sin b) * (sin (Arg a)) is complex real ext-real Element of REAL
((cos b) * (cos (Arg a))) - ((sin b) * (sin (Arg a))) is complex real ext-real Element of REAL
- ((sin b) * (sin (Arg a))) is complex real ext-real set
((cos b) * (cos (Arg a))) + (- ((sin b) * (sin (Arg a)))) is complex real ext-real set
|.a.| * (((cos b) * (cos (Arg a))) - ((sin b) * (sin (Arg a)))) is complex real ext-real Element of REAL
(sin b) * (cos (Arg a)) is complex real ext-real Element of REAL
(cos b) * (sin (Arg a)) is complex real ext-real Element of REAL
((sin b) * (cos (Arg a))) + ((cos b) * (sin (Arg a))) is complex real ext-real Element of REAL
|.a.| * (((sin b) * (cos (Arg a))) + ((cos b) * (sin (Arg a)))) is complex real ext-real Element of REAL
a is complex Element of COMPLEX
b is complex Element of COMPLEX
a + b is complex Element of COMPLEX
c is complex real ext-real Element of REAL
((a + b),c) is complex Element of COMPLEX
|.(a + b).| is complex real ext-real Element of REAL
Arg (a + b) is complex real ext-real Element of REAL
c + (Arg (a + b)) is complex real ext-real Element of REAL
cos (c + (Arg (a + b))) is complex real ext-real Element of REAL
|.(a + b).| * (cos (c + (Arg (a + b)))) is complex real ext-real Element of REAL
sin (c + (Arg (a + b))) is complex real ext-real Element of REAL
|.(a + b).| * (sin (c + (Arg (a + b)))) is complex real ext-real Element of REAL
(|.(a + b).| * (sin (c + (Arg (a + b))))) * <i> is complex set
(|.(a + b).| * (cos (c + (Arg (a + b))))) + ((|.(a + b).| * (sin (c + (Arg (a + b))))) * <i>) is complex set
(a,c) is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
c + (Arg a) is complex real ext-real Element of REAL
cos (c + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (cos (c + (Arg a))) is complex real ext-real Element of REAL
sin (c + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (sin (c + (Arg a))) is complex real ext-real Element of REAL
(|.a.| * (sin (c + (Arg a)))) * <i> is complex set
(|.a.| * (cos (c + (Arg a)))) + ((|.a.| * (sin (c + (Arg a)))) * <i>) is complex set
(b,c) is complex Element of COMPLEX
|.b.| is complex real ext-real Element of REAL
Arg b is complex real ext-real Element of REAL
c + (Arg b) is complex real ext-real Element of REAL
cos (c + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos (c + (Arg b))) is complex real ext-real Element of REAL
sin (c + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin (c + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin (c + (Arg b)))) * <i> is complex set
(|.b.| * (cos (c + (Arg b)))) + ((|.b.| * (sin (c + (Arg b)))) * <i>) is complex set
(a,c) + (b,c) is complex Element of COMPLEX
Re (a + b) is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
Re b is complex real ext-real Element of REAL
(Re a) + (Re b) is complex real ext-real Element of REAL
Im (a + b) is complex real ext-real Element of REAL
Im a is complex real ext-real Element of REAL
Im b is complex real ext-real Element of REAL
(Im a) + (Im b) is complex real ext-real Element of REAL
Im ((a + b),c) is complex real ext-real Element of REAL
sin c is complex real ext-real Element of REAL
(Re (a + b)) * (sin c) is complex real ext-real Element of REAL
cos c is complex real ext-real Element of REAL
(Im (a + b)) * (cos c) is complex real ext-real Element of REAL
((Re (a + b)) * (sin c)) + ((Im (a + b)) * (cos c)) is complex real ext-real Element of REAL
Im (a,c) is complex real ext-real Element of REAL
(Re a) * (sin c) is complex real ext-real Element of REAL
(Im a) * (cos c) is complex real ext-real Element of REAL
((Re a) * (sin c)) + ((Im a) * (cos c)) is complex real ext-real Element of REAL
Im (b,c) is complex real ext-real Element of REAL
(Re b) * (sin c) is complex real ext-real Element of REAL
(Im b) * (cos c) is complex real ext-real Element of REAL
((Re b) * (sin c)) + ((Im b) * (cos c)) is complex real ext-real Element of REAL
Im ((a,c) + (b,c)) is complex real ext-real Element of REAL
(((Re a) * (sin c)) + ((Im a) * (cos c))) + (((Re b) * (sin c)) + ((Im b) * (cos c))) is complex real ext-real Element of REAL
Re ((a + b),c) is complex real ext-real Element of REAL
(Re (a + b)) * (cos c) is complex real ext-real Element of REAL
(Im (a + b)) * (sin c) is complex real ext-real Element of REAL
((Re (a + b)) * (cos c)) - ((Im (a + b)) * (sin c)) is complex real ext-real Element of REAL
- ((Im (a + b)) * (sin c)) is complex real ext-real set
((Re (a + b)) * (cos c)) + (- ((Im (a + b)) * (sin c))) is complex real ext-real set
Re (a,c) is complex real ext-real Element of REAL
(Re a) * (cos c) is complex real ext-real Element of REAL
(Im a) * (sin c) is complex real ext-real Element of REAL
((Re a) * (cos c)) - ((Im a) * (sin c)) is complex real ext-real Element of REAL
- ((Im a) * (sin c)) is complex real ext-real set
((Re a) * (cos c)) + (- ((Im a) * (sin c))) is complex real ext-real set
Re (b,c) is complex real ext-real Element of REAL
(Re b) * (cos c) is complex real ext-real Element of REAL
(Im b) * (sin c) is complex real ext-real Element of REAL
((Re b) * (cos c)) - ((Im b) * (sin c)) is complex real ext-real Element of REAL
- ((Im b) * (sin c)) is complex real ext-real set
((Re b) * (cos c)) + (- ((Im b) * (sin c))) is complex real ext-real set
Re ((a,c) + (b,c)) is complex real ext-real Element of REAL
(((Re a) * (cos c)) - ((Im a) * (sin c))) + (((Re b) * (cos c)) - ((Im b) * (sin c))) is complex real ext-real Element of REAL
a is complex Element of COMPLEX
- a is complex Element of COMPLEX
b is complex real ext-real Element of REAL
((- a),b) is complex Element of COMPLEX
|.(- a).| is complex real ext-real Element of REAL
Arg (- a) is complex real ext-real Element of REAL
b + (Arg (- a)) is complex real ext-real Element of REAL
cos (b + (Arg (- a))) is complex real ext-real Element of REAL
|.(- a).| * (cos (b + (Arg (- a)))) is complex real ext-real Element of REAL
sin (b + (Arg (- a))) is complex real ext-real Element of REAL
|.(- a).| * (sin (b + (Arg (- a)))) is complex real ext-real Element of REAL
(|.(- a).| * (sin (b + (Arg (- a))))) * <i> is complex set
(|.(- a).| * (cos (b + (Arg (- a))))) + ((|.(- a).| * (sin (b + (Arg (- a))))) * <i>) is complex set
(a,b) is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
b + (Arg a) is complex real ext-real Element of REAL
cos (b + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (cos (b + (Arg a))) is complex real ext-real Element of REAL
sin (b + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (sin (b + (Arg a))) is complex real ext-real Element of REAL
(|.a.| * (sin (b + (Arg a)))) * <i> is complex set
(|.a.| * (cos (b + (Arg a)))) + ((|.a.| * (sin (b + (Arg a)))) * <i>) is complex set
- (a,b) is complex Element of COMPLEX
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
- (cos (b + (Arg a))) is complex real ext-real Element of REAL
- (sin (b + (Arg a))) is complex real ext-real Element of REAL
PI + (Arg a) is complex real ext-real Element of REAL
PI + (b + (Arg a)) is complex real ext-real Element of REAL
(Arg a) - PI is complex real ext-real Element of REAL
- PI is complex real ext-real set
(Arg a) + (- PI) is complex real ext-real set
(Arg a) + b is complex real ext-real Element of REAL
((Arg a) + b) - PI is complex real ext-real Element of REAL
((Arg a) + b) + (- PI) is complex real ext-real set
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
- 0 is zero complex real ext-real non positive non negative integer V61() V62() V63() V64() V65() V66() V67() Element of REAL
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
a is complex Element of COMPLEX
b is complex Element of COMPLEX
a - b is complex Element of COMPLEX
- b is complex set
a + (- b) is complex set
c is complex real ext-real Element of REAL
((a - b),c) is complex Element of COMPLEX
|.(a - b).| is complex real ext-real Element of REAL
Arg (a - b) is complex real ext-real Element of REAL
c + (Arg (a - b)) is complex real ext-real Element of REAL
cos (c + (Arg (a - b))) is complex real ext-real Element of REAL
|.(a - b).| * (cos (c + (Arg (a - b)))) is complex real ext-real Element of REAL
sin (c + (Arg (a - b))) is complex real ext-real Element of REAL
|.(a - b).| * (sin (c + (Arg (a - b)))) is complex real ext-real Element of REAL
(|.(a - b).| * (sin (c + (Arg (a - b))))) * <i> is complex set
(|.(a - b).| * (cos (c + (Arg (a - b))))) + ((|.(a - b).| * (sin (c + (Arg (a - b))))) * <i>) is complex set
(a,c) is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
c + (Arg a) is complex real ext-real Element of REAL
cos (c + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (cos (c + (Arg a))) is complex real ext-real Element of REAL
sin (c + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (sin (c + (Arg a))) is complex real ext-real Element of REAL
(|.a.| * (sin (c + (Arg a)))) * <i> is complex set
(|.a.| * (cos (c + (Arg a)))) + ((|.a.| * (sin (c + (Arg a)))) * <i>) is complex set
(b,c) is complex Element of COMPLEX
|.b.| is complex real ext-real Element of REAL
Arg b is complex real ext-real Element of REAL
c + (Arg b) is complex real ext-real Element of REAL
cos (c + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos (c + (Arg b))) is complex real ext-real Element of REAL
sin (c + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin (c + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin (c + (Arg b)))) * <i> is complex set
(|.b.| * (cos (c + (Arg b)))) + ((|.b.| * (sin (c + (Arg b)))) * <i>) is complex set
(a,c) - (b,c) is complex Element of COMPLEX
- (b,c) is complex set
(a,c) + (- (b,c)) is complex set
- b is complex Element of COMPLEX
((- b),c) is complex Element of COMPLEX
|.(- b).| is complex real ext-real Element of REAL
Arg (- b) is complex real ext-real Element of REAL
c + (Arg (- b)) is complex real ext-real Element of REAL
cos (c + (Arg (- b))) is complex real ext-real Element of REAL
|.(- b).| * (cos (c + (Arg (- b)))) is complex real ext-real Element of REAL
sin (c + (Arg (- b))) is complex real ext-real Element of REAL
|.(- b).| * (sin (c + (Arg (- b)))) is complex real ext-real Element of REAL
(|.(- b).| * (sin (c + (Arg (- b))))) * <i> is complex set
(|.(- b).| * (cos (c + (Arg (- b))))) + ((|.(- b).| * (sin (c + (Arg (- b))))) * <i>) is complex set
(a,c) + ((- b),c) is complex Element of COMPLEX
a is complex Element of COMPLEX
(a,PI) is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
PI + (Arg a) is complex real ext-real Element of REAL
cos (PI + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (cos (PI + (Arg a))) is complex real ext-real Element of REAL
sin (PI + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (sin (PI + (Arg a))) is complex real ext-real Element of REAL
(|.a.| * (sin (PI + (Arg a)))) * <i> is complex set
(|.a.| * (cos (PI + (Arg a)))) + ((|.a.| * (sin (PI + (Arg a)))) * <i>) is complex set
- a is complex Element of COMPLEX
cos (Arg a) is complex real ext-real Element of REAL
|.a.| * (cos (Arg a)) is complex real ext-real Element of REAL
sin (Arg a) is complex real ext-real Element of REAL
|.a.| * (sin (Arg a)) is complex real ext-real Element of REAL
(|.a.| * (sin (Arg a))) * <i> is complex set
(|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) is complex set
- (sin (Arg a)) is complex real ext-real Element of REAL
|.a.| * (- (sin (Arg a))) is complex real ext-real Element of REAL
- (|.a.| * (sin (Arg a))) is complex real ext-real Element of REAL
Im a is complex real ext-real Element of REAL
- (Im a) is complex real ext-real Element of REAL
- (cos (Arg a)) is complex real ext-real Element of REAL
|.a.| * (- (cos (Arg a))) is complex real ext-real Element of REAL
- (|.a.| * (cos (Arg a))) is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
- (Re a) is complex real ext-real Element of REAL
(|.a.| * (- (cos (Arg a)))) + ((|.a.| * (sin (PI + (Arg a)))) * <i>) is complex set
(|.a.| * (- (sin (Arg a)))) * <i> is complex set
(|.a.| * (- (cos (Arg a)))) + ((|.a.| * (- (sin (Arg a)))) * <i>) is complex set
a is complex set
Arg a is complex real ext-real Element of REAL
b is complex set
- (Arg a) is complex real ext-real Element of REAL
(b,(- (Arg a))) is complex Element of COMPLEX
|.b.| is complex real ext-real Element of REAL
Arg b is complex real ext-real Element of REAL
(- (Arg a)) + (Arg b) is complex real ext-real Element of REAL
cos ((- (Arg a)) + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos ((- (Arg a)) + (Arg b))) is complex real ext-real Element of REAL
sin ((- (Arg a)) + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin ((- (Arg a)) + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin ((- (Arg a)) + (Arg b)))) * <i> is complex set
(|.b.| * (cos ((- (Arg a)) + (Arg b)))) + ((|.b.| * (sin ((- (Arg a)) + (Arg b)))) * <i>) is complex set
Arg (b,(- (Arg a))) is complex real ext-real Element of REAL
(2 * PI) - (Arg a) is complex real ext-real Element of REAL
- (Arg a) is complex real ext-real set
(2 * PI) + (- (Arg a)) is complex real ext-real set
a is complex real ext-real Element of REAL
b is complex set
(a,b) is complex real ext-real Element of REAL
Arg b is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
- 0 is zero complex real ext-real non positive non negative integer V61() V62() V63() V64() V65() V66() V67() Element of REAL
(b,(- 0)) is complex Element of COMPLEX
|.b.| is complex real ext-real Element of REAL
(- 0) + (Arg b) is complex real ext-real Element of REAL
cos ((- 0) + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos ((- 0) + (Arg b))) is complex real ext-real Element of REAL
sin ((- 0) + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin ((- 0) + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin ((- 0) + (Arg b)))) * <i> is complex set
(|.b.| * (cos ((- 0) + (Arg b)))) + ((|.b.| * (sin ((- 0) + (Arg b)))) * <i>) is complex set
Arg (b,(- 0)) is complex real ext-real Element of REAL
a is complex real ext-real Element of REAL
b is complex set
Arg b is complex real ext-real Element of REAL
c is complex set
Arg c is complex real ext-real Element of REAL
(b,a) is complex Element of COMPLEX
|.b.| is complex real ext-real Element of REAL
a + (Arg b) is complex real ext-real Element of REAL
cos (a + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos (a + (Arg b))) is complex real ext-real Element of REAL
sin (a + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin (a + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin (a + (Arg b)))) * <i> is complex set
(|.b.| * (cos (a + (Arg b)))) + ((|.b.| * (sin (a + (Arg b)))) * <i>) is complex set
Arg (b,a) is complex real ext-real Element of REAL
(c,a) is complex Element of COMPLEX
|.c.| is complex real ext-real Element of REAL
a + (Arg c) is complex real ext-real Element of REAL
cos (a + (Arg c)) is complex real ext-real Element of REAL
|.c.| * (cos (a + (Arg c))) is complex real ext-real Element of REAL
sin (a + (Arg c)) is complex real ext-real Element of REAL
|.c.| * (sin (a + (Arg c))) is complex real ext-real Element of REAL
(|.c.| * (sin (a + (Arg c)))) * <i> is complex set
(|.c.| * (cos (a + (Arg c)))) + ((|.c.| * (sin (a + (Arg c)))) * <i>) is complex set
Arg (c,a) is complex real ext-real Element of REAL
r is complex real ext-real integer set
(2 * PI) * r is complex real ext-real Element of REAL
((2 * PI) * r) + (a + (Arg b)) is complex real ext-real Element of REAL
A is complex real ext-real integer set
(2 * PI) * A is complex real ext-real Element of REAL
((2 * PI) * A) + (a + (Arg c)) is complex real ext-real Element of REAL
A - r is complex real ext-real integer set
- r is complex real ext-real integer set
A + (- r) is complex real ext-real integer set
(2 * PI) * (A - r) is complex real ext-real Element of REAL
((2 * PI) * (A - r)) + (Arg (b,a)) is complex real ext-real Element of REAL
a is complex Element of COMPLEX
b is complex Element of COMPLEX
(a,b) is complex real ext-real Element of REAL
c is complex real ext-real Element of REAL
a * c is complex set
b * c is complex set
((a * c),(b * c)) is complex real ext-real Element of REAL
Arg (a * c) is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
- (Arg a) is complex real ext-real Element of REAL
(b,(- (Arg a))) is complex Element of COMPLEX
|.b.| is complex real ext-real Element of REAL
Arg b is complex real ext-real Element of REAL
(- (Arg a)) + (Arg b) is complex real ext-real Element of REAL
cos ((- (Arg a)) + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos ((- (Arg a)) + (Arg b))) is complex real ext-real Element of REAL
sin ((- (Arg a)) + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin ((- (Arg a)) + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin ((- (Arg a)) + (Arg b)))) * <i> is complex set
(|.b.| * (cos ((- (Arg a)) + (Arg b)))) + ((|.b.| * (sin ((- (Arg a)) + (Arg b)))) * <i>) is complex set
Arg (b,(- (Arg a))) is complex real ext-real Element of REAL
- (Arg (a * c)) is complex real ext-real Element of REAL
((b * c),(- (Arg (a * c)))) is complex Element of COMPLEX
|.(b * c).| is complex real ext-real Element of REAL
Arg (b * c) is complex real ext-real Element of REAL
(- (Arg (a * c))) + (Arg (b * c)) is complex real ext-real Element of REAL
cos ((- (Arg (a * c))) + (Arg (b * c))) is complex real ext-real Element of REAL
|.(b * c).| * (cos ((- (Arg (a * c))) + (Arg (b * c)))) is complex real ext-real Element of REAL
sin ((- (Arg (a * c))) + (Arg (b * c))) is complex real ext-real Element of REAL
|.(b * c).| * (sin ((- (Arg (a * c))) + (Arg (b * c)))) is complex real ext-real Element of REAL
(|.(b * c).| * (sin ((- (Arg (a * c))) + (Arg (b * c))))) * <i> is complex set
(|.(b * c).| * (cos ((- (Arg (a * c))) + (Arg (b * c))))) + ((|.(b * c).| * (sin ((- (Arg (a * c))) + (Arg (b * c))))) * <i>) is complex set
Arg ((b * c),(- (Arg (a * c)))) is complex real ext-real Element of REAL
- (Arg a) is complex real ext-real Element of REAL
(b,(- (Arg a))) is complex Element of COMPLEX
|.b.| is complex real ext-real Element of REAL
Arg b is complex real ext-real Element of REAL
(- (Arg a)) + (Arg b) is complex real ext-real Element of REAL
cos ((- (Arg a)) + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos ((- (Arg a)) + (Arg b))) is complex real ext-real Element of REAL
sin ((- (Arg a)) + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin ((- (Arg a)) + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin ((- (Arg a)) + (Arg b)))) * <i> is complex set
(|.b.| * (cos ((- (Arg a)) + (Arg b)))) + ((|.b.| * (sin ((- (Arg a)) + (Arg b)))) * <i>) is complex set
Arg (b,(- (Arg a))) is complex real ext-real Element of REAL
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
Arg 0c is complex real ext-real Element of REAL
- (Arg (a * c)) is complex real ext-real Element of REAL
((b * c),(- (Arg (a * c)))) is complex Element of COMPLEX
|.(b * c).| is complex real ext-real Element of REAL
Arg (b * c) is complex real ext-real Element of REAL
(- (Arg (a * c))) + (Arg (b * c)) is complex real ext-real Element of REAL
cos ((- (Arg (a * c))) + (Arg (b * c))) is complex real ext-real Element of REAL
|.(b * c).| * (cos ((- (Arg (a * c))) + (Arg (b * c)))) is complex real ext-real Element of REAL
sin ((- (Arg (a * c))) + (Arg (b * c))) is complex real ext-real Element of REAL
|.(b * c).| * (sin ((- (Arg (a * c))) + (Arg (b * c)))) is complex real ext-real Element of REAL
(|.(b * c).| * (sin ((- (Arg (a * c))) + (Arg (b * c))))) * <i> is complex set
(|.(b * c).| * (cos ((- (Arg (a * c))) + (Arg (b * c))))) + ((|.(b * c).| * (sin ((- (Arg (a * c))) + (Arg (b * c))))) * <i>) is complex set
Arg ((b * c),(- (Arg (a * c)))) is complex real ext-real Element of REAL
(2 * PI) - (Arg a) is complex real ext-real Element of REAL
- (Arg a) is complex real ext-real set
(2 * PI) + (- (Arg a)) is complex real ext-real set
a is complex Element of COMPLEX
Arg a is complex real ext-real Element of REAL
- a is complex Element of COMPLEX
Arg (- a) is complex real ext-real Element of REAL
b is complex Element of COMPLEX
Arg b is complex real ext-real Element of REAL
- b is complex Element of COMPLEX
Arg (- b) is complex real ext-real Element of REAL
(a,PI) is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
PI + (Arg a) is complex real ext-real Element of REAL
cos (PI + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (cos (PI + (Arg a))) is complex real ext-real Element of REAL
sin (PI + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (sin (PI + (Arg a))) is complex real ext-real Element of REAL
(|.a.| * (sin (PI + (Arg a)))) * <i> is complex set
(|.a.| * (cos (PI + (Arg a)))) + ((|.a.| * (sin (PI + (Arg a)))) * <i>) is complex set
Arg (a,PI) is complex real ext-real Element of REAL
(b,PI) is complex Element of COMPLEX
|.b.| is complex real ext-real Element of REAL
PI + (Arg b) is complex real ext-real Element of REAL
cos (PI + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos (PI + (Arg b))) is complex real ext-real Element of REAL
sin (PI + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin (PI + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin (PI + (Arg b)))) * <i> is complex set
(|.b.| * (cos (PI + (Arg b)))) + ((|.b.| * (sin (PI + (Arg b)))) * <i>) is complex set
Arg (b,PI) is complex real ext-real Element of REAL
a is complex Element of COMPLEX
b is complex Element of COMPLEX
(a,b) is complex real ext-real Element of REAL
c is complex real ext-real Element of REAL
(a,c) is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
c + (Arg a) is complex real ext-real Element of REAL
cos (c + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (cos (c + (Arg a))) is complex real ext-real Element of REAL
sin (c + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (sin (c + (Arg a))) is complex real ext-real Element of REAL
(|.a.| * (sin (c + (Arg a)))) * <i> is complex set
(|.a.| * (cos (c + (Arg a)))) + ((|.a.| * (sin (c + (Arg a)))) * <i>) is complex set
(b,c) is complex Element of COMPLEX
|.b.| is complex real ext-real Element of REAL
Arg b is complex real ext-real Element of REAL
c + (Arg b) is complex real ext-real Element of REAL
cos (c + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos (c + (Arg b))) is complex real ext-real Element of REAL
sin (c + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin (c + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin (c + (Arg b)))) * <i> is complex set
(|.b.| * (cos (c + (Arg b)))) + ((|.b.| * (sin (c + (Arg b)))) * <i>) is complex set
((a,c),(b,c)) is complex real ext-real Element of REAL
- (Arg a) is complex real ext-real Element of REAL
(b,(- (Arg a))) is complex Element of COMPLEX
(- (Arg a)) + (Arg b) is complex real ext-real Element of REAL
cos ((- (Arg a)) + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos ((- (Arg a)) + (Arg b))) is complex real ext-real Element of REAL
sin ((- (Arg a)) + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin ((- (Arg a)) + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin ((- (Arg a)) + (Arg b)))) * <i> is complex set
(|.b.| * (cos ((- (Arg a)) + (Arg b)))) + ((|.b.| * (sin ((- (Arg a)) + (Arg b)))) * <i>) is complex set
Arg (b,(- (Arg a))) is complex real ext-real Element of REAL
r is complex real ext-real integer set
(2 * PI) * r is complex real ext-real Element of REAL
((2 * PI) * r) + ((- (Arg a)) + (Arg b)) is complex real ext-real Element of REAL
Arg (b,c) is complex real ext-real Element of REAL
A is complex real ext-real integer set
(2 * PI) * A is complex real ext-real Element of REAL
((2 * PI) * A) + (c + (Arg b)) is complex real ext-real Element of REAL
Arg (a,c) is complex real ext-real Element of REAL
B is complex real ext-real integer set
(2 * PI) * B is complex real ext-real Element of REAL
((2 * PI) * B) + (c + (Arg a)) is complex real ext-real Element of REAL
- (Arg (a,c)) is complex real ext-real Element of REAL
((b,c),(- (Arg (a,c)))) is complex Element of COMPLEX
|.(b,c).| is complex real ext-real Element of REAL
(- (Arg (a,c))) + (Arg (b,c)) is complex real ext-real Element of REAL
cos ((- (Arg (a,c))) + (Arg (b,c))) is complex real ext-real Element of REAL
|.(b,c).| * (cos ((- (Arg (a,c))) + (Arg (b,c)))) is complex real ext-real Element of REAL
sin ((- (Arg (a,c))) + (Arg (b,c))) is complex real ext-real Element of REAL
|.(b,c).| * (sin ((- (Arg (a,c))) + (Arg (b,c)))) is complex real ext-real Element of REAL
(|.(b,c).| * (sin ((- (Arg (a,c))) + (Arg (b,c))))) * <i> is complex set
(|.(b,c).| * (cos ((- (Arg (a,c))) + (Arg (b,c))))) + ((|.(b,c).| * (sin ((- (Arg (a,c))) + (Arg (b,c))))) * <i>) is complex set
Arg ((b,c),(- (Arg (a,c)))) is complex real ext-real Element of REAL
BA is complex real ext-real integer set
(2 * PI) * BA is complex real ext-real Element of REAL
((2 * PI) * BA) + ((- (Arg (a,c))) + (Arg (b,c))) is complex real ext-real Element of REAL
BA - B is complex real ext-real integer set
- B is complex real ext-real integer set
BA + (- B) is complex real ext-real integer set
(BA - B) + A is complex real ext-real integer set
((BA - B) + A) - r is complex real ext-real integer set
- r is complex real ext-real integer set
((BA - B) + A) + (- r) is complex real ext-real integer set
(2 * PI) * (((BA - B) + A) - r) is complex real ext-real Element of REAL
((2 * PI) * (((BA - B) + A) - r)) + (Arg (b,(- (Arg a)))) is complex real ext-real Element of REAL
a is complex Element of COMPLEX
b is complex Element of COMPLEX
(a,b) is complex real ext-real Element of REAL
c is complex real ext-real Element of REAL
a * c is complex set
b * c is complex set
((a * c),(b * c)) is complex real ext-real Element of REAL
- b is complex Element of COMPLEX
- a is complex Element of COMPLEX
Arg (- a) is complex real ext-real Element of REAL
- (Arg (- a)) is complex real ext-real Element of REAL
((- b),(- (Arg (- a)))) is complex Element of COMPLEX
|.(- b).| is complex real ext-real Element of REAL
Arg (- b) is complex real ext-real Element of REAL
(- (Arg (- a))) + (Arg (- b)) is complex real ext-real Element of REAL
cos ((- (Arg (- a))) + (Arg (- b))) is complex real ext-real Element of REAL
|.(- b).| * (cos ((- (Arg (- a))) + (Arg (- b)))) is complex real ext-real Element of REAL
sin ((- (Arg (- a))) + (Arg (- b))) is complex real ext-real Element of REAL
|.(- b).| * (sin ((- (Arg (- a))) + (Arg (- b)))) is complex real ext-real Element of REAL
(|.(- b).| * (sin ((- (Arg (- a))) + (Arg (- b))))) * <i> is complex set
(|.(- b).| * (cos ((- (Arg (- a))) + (Arg (- b))))) + ((|.(- b).| * (sin ((- (Arg (- a))) + (Arg (- b))))) * <i>) is complex set
Arg ((- b),(- (Arg (- a)))) is complex real ext-real Element of REAL
r is complex real ext-real integer set
(2 * PI) * r is complex real ext-real Element of REAL
((2 * PI) * r) + ((- (Arg (- a))) + (Arg (- b))) is complex real ext-real Element of REAL
Arg (b * c) is complex real ext-real Element of REAL
Arg (a * c) is complex real ext-real Element of REAL
- (Arg (a * c)) is complex real ext-real Element of REAL
((b * c),(- (Arg (a * c)))) is complex Element of COMPLEX
|.(b * c).| is complex real ext-real Element of REAL
(- (Arg (a * c))) + (Arg (b * c)) is complex real ext-real Element of REAL
cos ((- (Arg (a * c))) + (Arg (b * c))) is complex real ext-real Element of REAL
|.(b * c).| * (cos ((- (Arg (a * c))) + (Arg (b * c)))) is complex real ext-real Element of REAL
sin ((- (Arg (a * c))) + (Arg (b * c))) is complex real ext-real Element of REAL
|.(b * c).| * (sin ((- (Arg (a * c))) + (Arg (b * c)))) is complex real ext-real Element of REAL
(|.(b * c).| * (sin ((- (Arg (a * c))) + (Arg (b * c))))) * <i> is complex set
(|.(b * c).| * (cos ((- (Arg (a * c))) + (Arg (b * c))))) + ((|.(b * c).| * (sin ((- (Arg (a * c))) + (Arg (b * c))))) * <i>) is complex set
Arg ((b * c),(- (Arg (a * c)))) is complex real ext-real Element of REAL
BA is complex real ext-real integer set
(2 * PI) * BA is complex real ext-real Element of REAL
((2 * PI) * BA) + ((- (Arg (- a))) + (Arg (- b))) is complex real ext-real Element of REAL
BA - r is complex real ext-real integer set
- r is complex real ext-real integer set
BA + (- r) is complex real ext-real integer set
(2 * PI) * (BA - r) is complex real ext-real Element of REAL
((2 * PI) * (BA - r)) + (Arg ((- b),(- (Arg (- a))))) is complex real ext-real Element of REAL
(a,PI) is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
PI + (Arg a) is complex real ext-real Element of REAL
cos (PI + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (cos (PI + (Arg a))) is complex real ext-real Element of REAL
sin (PI + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (sin (PI + (Arg a))) is complex real ext-real Element of REAL
(|.a.| * (sin (PI + (Arg a)))) * <i> is complex set
(|.a.| * (cos (PI + (Arg a)))) + ((|.a.| * (sin (PI + (Arg a)))) * <i>) is complex set
(b,PI) is complex Element of COMPLEX
|.b.| is complex real ext-real Element of REAL
Arg b is complex real ext-real Element of REAL
PI + (Arg b) is complex real ext-real Element of REAL
cos (PI + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos (PI + (Arg b))) is complex real ext-real Element of REAL
sin (PI + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin (PI + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin (PI + (Arg b)))) * <i> is complex set
(|.b.| * (cos (PI + (Arg b)))) + ((|.b.| * (sin (PI + (Arg b)))) * <i>) is complex set
((a,PI),(b,PI)) is complex real ext-real Element of REAL
((- a),(b,PI)) is complex real ext-real Element of REAL
((- a),(- b)) is complex real ext-real Element of REAL
a is complex Element of COMPLEX
- a is complex Element of COMPLEX
b is complex Element of COMPLEX
(a,b) is complex real ext-real Element of REAL
- b is complex Element of COMPLEX
((- a),(- b)) is complex real ext-real Element of REAL
(a,PI) is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
PI + (Arg a) is complex real ext-real Element of REAL
cos (PI + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (cos (PI + (Arg a))) is complex real ext-real Element of REAL
sin (PI + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (sin (PI + (Arg a))) is complex real ext-real Element of REAL
(|.a.| * (sin (PI + (Arg a)))) * <i> is complex set
(|.a.| * (cos (PI + (Arg a)))) + ((|.a.| * (sin (PI + (Arg a)))) * <i>) is complex set
(b,PI) is complex Element of COMPLEX
|.b.| is complex real ext-real Element of REAL
Arg b is complex real ext-real Element of REAL
PI + (Arg b) is complex real ext-real Element of REAL
cos (PI + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos (PI + (Arg b))) is complex real ext-real Element of REAL
sin (PI + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin (PI + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin (PI + (Arg b)))) * <i> is complex set
(|.b.| * (cos (PI + (Arg b)))) + ((|.b.| * (sin (PI + (Arg b)))) * <i>) is complex set
((a,PI),(b,PI)) is complex real ext-real Element of REAL
((- a),(b,PI)) is complex real ext-real Element of REAL
a is complex Element of COMPLEX
- a is complex Element of COMPLEX
b is complex Element of COMPLEX
(b,a) is complex real ext-real Element of REAL
(b,(- a)) is complex real ext-real Element of REAL
Arg b is complex real ext-real Element of REAL
- (Arg b) is complex real ext-real Element of REAL
(a,(- (Arg b))) is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
(- (Arg b)) + (Arg a) is complex real ext-real Element of REAL
cos ((- (Arg b)) + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (cos ((- (Arg b)) + (Arg a))) is complex real ext-real Element of REAL
sin ((- (Arg b)) + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (sin ((- (Arg b)) + (Arg a))) is complex real ext-real Element of REAL
(|.a.| * (sin ((- (Arg b)) + (Arg a)))) * <i> is complex set
(|.a.| * (cos ((- (Arg b)) + (Arg a)))) + ((|.a.| * (sin ((- (Arg b)) + (Arg a)))) * <i>) is complex set
Arg (a,(- (Arg b))) is complex real ext-real Element of REAL
((- a),(- (Arg b))) is complex Element of COMPLEX
|.(- a).| is complex real ext-real Element of REAL
Arg (- a) is complex real ext-real Element of REAL
(- (Arg b)) + (Arg (- a)) is complex real ext-real Element of REAL
cos ((- (Arg b)) + (Arg (- a))) is complex real ext-real Element of REAL
|.(- a).| * (cos ((- (Arg b)) + (Arg (- a)))) is complex real ext-real Element of REAL
sin ((- (Arg b)) + (Arg (- a))) is complex real ext-real Element of REAL
|.(- a).| * (sin ((- (Arg b)) + (Arg (- a)))) is complex real ext-real Element of REAL
(|.(- a).| * (sin ((- (Arg b)) + (Arg (- a))))) * <i> is complex set
(|.(- a).| * (cos ((- (Arg b)) + (Arg (- a))))) + ((|.(- a).| * (sin ((- (Arg b)) + (Arg (- a))))) * <i>) is complex set
Arg ((- a),(- (Arg b))) is complex real ext-real Element of REAL
- (a,(- (Arg b))) is complex Element of COMPLEX
Arg (- (a,(- (Arg b)))) is complex real ext-real Element of REAL
(Arg (a,(- (Arg b)))) + PI is complex real ext-real Element of REAL
a is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
b is complex Element of COMPLEX
(a,b) is complex real ext-real Element of REAL
cos (a,b) is complex real ext-real Element of REAL
(a,b) is complex Element of COMPLEX
b *' is complex Element of COMPLEX
a * (b *') is complex set
Re (a,b) is complex real ext-real Element of REAL
|.b.| is complex real ext-real Element of REAL
|.a.| * |.b.| is complex real ext-real Element of REAL
(Re (a,b)) / (|.a.| * |.b.|) is complex real ext-real Element of COMPLEX
(|.a.| * |.b.|) " is complex real ext-real set
(Re (a,b)) * ((|.a.| * |.b.|) ") is complex real ext-real set
sin (a,b) is complex real ext-real Element of REAL
Im (a,b) is complex real ext-real Element of REAL
(Im (a,b)) / (|.a.| * |.b.|) is complex real ext-real Element of COMPLEX
(Im (a,b)) * ((|.a.| * |.b.|) ") is complex real ext-real set
- ((Im (a,b)) / (|.a.| * |.b.|)) is complex real ext-real Element of COMPLEX
Arg a is complex real ext-real Element of REAL
- (Arg a) is complex real ext-real Element of REAL
(a,(- (Arg a))) is complex Element of COMPLEX
(- (Arg a)) + (Arg a) is complex real ext-real Element of REAL
cos ((- (Arg a)) + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (cos ((- (Arg a)) + (Arg a))) is complex real ext-real Element of REAL
sin ((- (Arg a)) + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (sin ((- (Arg a)) + (Arg a))) is complex real ext-real Element of REAL
(|.a.| * (sin ((- (Arg a)) + (Arg a)))) * <i> is complex set
(|.a.| * (cos ((- (Arg a)) + (Arg a)))) + ((|.a.| * (sin ((- (Arg a)) + (Arg a)))) * <i>) is complex set
(b,(- (Arg a))) is complex Element of COMPLEX
Arg b is complex real ext-real Element of REAL
(- (Arg a)) + (Arg b) is complex real ext-real Element of REAL
cos ((- (Arg a)) + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos ((- (Arg a)) + (Arg b))) is complex real ext-real Element of REAL
sin ((- (Arg a)) + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin ((- (Arg a)) + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin ((- (Arg a)) + (Arg b)))) * <i> is complex set
(|.b.| * (cos ((- (Arg a)) + (Arg b)))) + ((|.b.| * (sin ((- (Arg a)) + (Arg b)))) * <i>) is complex set
(|.a.| * |.b.|) " is complex real ext-real Element of REAL
((a,(- (Arg a))),(b,(- (Arg a)))) is complex real ext-real Element of REAL
|.a.| * ((|.a.| * |.b.|) ") is complex real ext-real Element of REAL
(b,(- (Arg a))) * ((|.a.| * |.b.|) ") is complex set
((|.a.| * ((|.a.| * |.b.|) ")),((b,(- (Arg a))) * ((|.a.| * |.b.|) "))) is complex real ext-real Element of REAL
Arg ((b,(- (Arg a))) * ((|.a.| * |.b.|) ")) is complex real ext-real Element of REAL
cos (Arg a) is complex real ext-real Element of REAL
|.a.| * (cos (Arg a)) is complex real ext-real Element of REAL
sin (Arg a) is complex real ext-real Element of REAL
|.a.| * (sin (Arg a)) is complex real ext-real Element of REAL
(|.a.| * (sin (Arg a))) * <i> is complex set
(|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) is complex set
Re a is complex real ext-real Element of REAL
(Re a) / |.a.| is complex real ext-real Element of COMPLEX
|.a.| " is complex real ext-real set
(Re a) * (|.a.| ") is complex real ext-real set
Im a is complex real ext-real Element of REAL
(Im a) / |.a.| is complex real ext-real Element of COMPLEX
(Im a) * (|.a.| ") is complex real ext-real set
Re b is complex real ext-real Element of REAL
(Re a) * (Re b) is complex real ext-real Element of REAL
Im b is complex real ext-real Element of REAL
(Im a) * (Im b) is complex real ext-real Element of REAL
((Re a) * (Re b)) + ((Im a) * (Im b)) is complex real ext-real Element of REAL
(Re a) * (Im b) is complex real ext-real Element of REAL
- ((Re a) * (Im b)) is complex real ext-real Element of REAL
(Im a) * (Re b) is complex real ext-real Element of REAL
(- ((Re a) * (Im b))) + ((Im a) * (Re b)) is complex real ext-real Element of REAL
((- ((Re a) * (Im b))) + ((Im a) * (Re b))) * <i> is complex set
(((Re a) * (Re b)) + ((Im a) * (Im b))) + (((- ((Re a) * (Im b))) + ((Im a) * (Re b))) * <i>) is complex set
Re (b,(- (Arg a))) is complex real ext-real Element of REAL
cos (- (Arg a)) is complex real ext-real Element of REAL
(Re b) * (cos (- (Arg a))) is complex real ext-real Element of REAL
sin (- (Arg a)) is complex real ext-real Element of REAL
(Im b) * (sin (- (Arg a))) is complex real ext-real Element of REAL
((Re b) * (cos (- (Arg a)))) - ((Im b) * (sin (- (Arg a)))) is complex real ext-real Element of REAL
- ((Im b) * (sin (- (Arg a)))) is complex real ext-real set
((Re b) * (cos (- (Arg a)))) + (- ((Im b) * (sin (- (Arg a))))) is complex real ext-real set
- (sin (Arg a)) is complex real ext-real Element of REAL
(Im b) * (- (sin (Arg a))) is complex real ext-real Element of REAL
((Re b) * (cos (- (Arg a)))) - ((Im b) * (- (sin (Arg a)))) is complex real ext-real Element of REAL
- ((Im b) * (- (sin (Arg a)))) is complex real ext-real set
((Re b) * (cos (- (Arg a)))) + (- ((Im b) * (- (sin (Arg a))))) is complex real ext-real set
(Re b) * ((Re a) / |.a.|) is complex real ext-real Element of REAL
(Im b) * ((Im a) / |.a.|) is complex real ext-real Element of REAL
((Re b) * ((Re a) / |.a.|)) + ((Im b) * ((Im a) / |.a.|)) is complex real ext-real Element of REAL
(Re (a,b)) / |.a.| is complex real ext-real Element of COMPLEX
(Re (a,b)) * (|.a.| ") is complex real ext-real set
Im (b,(- (Arg a))) is complex real ext-real Element of REAL
(Im (b,(- (Arg a)))) ^2 is complex real ext-real Element of REAL
(Im (b,(- (Arg a)))) * (Im (b,(- (Arg a)))) is complex real ext-real set
(Re b) * (sin (- (Arg a))) is complex real ext-real Element of REAL
(Im b) * (cos (- (Arg a))) is complex real ext-real Element of REAL
((Re b) * (sin (- (Arg a)))) + ((Im b) * (cos (- (Arg a)))) is complex real ext-real Element of REAL
(Re b) * (- (sin (Arg a))) is complex real ext-real Element of REAL
((Re b) * (- (sin (Arg a)))) + ((Im b) * (cos (- (Arg a)))) is complex real ext-real Element of REAL
- (Re b) is complex real ext-real Element of REAL
(- (Re b)) * ((Im a) / |.a.|) is complex real ext-real Element of REAL
(Im b) * ((Re a) / |.a.|) is complex real ext-real Element of REAL
((- (Re b)) * ((Im a) / |.a.|)) + ((Im b) * ((Re a) / |.a.|)) is complex real ext-real Element of REAL
(- (Re b)) * (Im a) is complex real ext-real Element of REAL
(Im b) * (Re a) is complex real ext-real Element of REAL
((- (Re b)) * (Im a)) + ((Im b) * (Re a)) is complex real ext-real Element of REAL
- (((- (Re b)) * (Im a)) + ((Im b) * (Re a))) is complex real ext-real Element of REAL
(- (((- (Re b)) * (Im a)) + ((Im b) * (Re a)))) / |.a.| is complex real ext-real Element of COMPLEX
(- (((- (Re b)) * (Im a)) + ((Im b) * (Re a)))) * (|.a.| ") is complex real ext-real set
- ((- (((- (Re b)) * (Im a)) + ((Im b) * (Re a)))) / |.a.|) is complex real ext-real Element of COMPLEX
(Im (a,b)) / |.a.| is complex real ext-real Element of COMPLEX
(Im (a,b)) * (|.a.| ") is complex real ext-real set
- ((Im (a,b)) / |.a.|) is complex real ext-real Element of COMPLEX
((|.a.| * |.b.|) ") ^2 is complex real ext-real Element of REAL
((|.a.| * |.b.|) ") * ((|.a.| * |.b.|) ") is complex real ext-real set
(Re (b,(- (Arg a)))) ^2 is complex real ext-real Element of REAL
(Re (b,(- (Arg a)))) * (Re (b,(- (Arg a)))) is complex real ext-real set
0 * <i> is complex set
((|.a.| * |.b.|) ") + (0 * <i>) is complex set
Re ((|.a.| * |.b.|) ") is complex real ext-real Element of REAL
Im ((|.a.| * |.b.|) ") is complex real ext-real Element of REAL
Re ((b,(- (Arg a))) * ((|.a.| * |.b.|) ")) is complex real ext-real Element of REAL
(Re (b,(- (Arg a)))) * ((|.a.| * |.b.|) ") is complex real ext-real Element of REAL
(Im (b,(- (Arg a)))) * 0 is complex real ext-real Element of REAL
((Re (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) - ((Im (b,(- (Arg a)))) * 0) is complex real ext-real Element of REAL
- ((Im (b,(- (Arg a)))) * 0) is complex real ext-real set
((Re (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) + (- ((Im (b,(- (Arg a)))) * 0)) is complex real ext-real set
Im ((b,(- (Arg a))) * ((|.a.| * |.b.|) ")) is complex real ext-real Element of REAL
(Re (b,(- (Arg a)))) * 0 is complex real ext-real Element of REAL
(Im (b,(- (Arg a)))) * ((|.a.| * |.b.|) ") is complex real ext-real Element of REAL
((Re (b,(- (Arg a)))) * 0) + ((Im (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) is complex real ext-real Element of REAL
|.((b,(- (Arg a))) * ((|.a.| * |.b.|) ")).| is complex real ext-real Element of REAL
((Re (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) ^2 is complex real ext-real Element of REAL
((Re (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) * ((Re (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) is complex real ext-real set
((Im (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) ^2 is complex real ext-real Element of REAL
((Im (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) * ((Im (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) is complex real ext-real set
(((Re (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) ^2) + (((Im (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) ^2) is complex real ext-real Element of REAL
sqrt ((((Re (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) ^2) + (((Im (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) ^2)) is complex real ext-real Element of REAL
((Re (b,(- (Arg a)))) ^2) + ((Im (b,(- (Arg a)))) ^2) is complex real ext-real Element of REAL
(((|.a.| * |.b.|) ") ^2) * (((Re (b,(- (Arg a)))) ^2) + ((Im (b,(- (Arg a)))) ^2)) is complex real ext-real Element of REAL
sqrt ((((|.a.| * |.b.|) ") ^2) * (((Re (b,(- (Arg a)))) ^2) + ((Im (b,(- (Arg a)))) ^2))) is complex real ext-real Element of REAL
sqrt (((|.a.| * |.b.|) ") ^2) is complex real ext-real Element of REAL
sqrt (((Re (b,(- (Arg a)))) ^2) + ((Im (b,(- (Arg a)))) ^2)) is complex real ext-real Element of REAL
(sqrt (((|.a.| * |.b.|) ") ^2)) * (sqrt (((Re (b,(- (Arg a)))) ^2) + ((Im (b,(- (Arg a)))) ^2))) is complex real ext-real Element of REAL
((|.a.| * |.b.|) ") * (sqrt (((Re (b,(- (Arg a)))) ^2) + ((Im (b,(- (Arg a)))) ^2))) is complex real ext-real Element of REAL
|.(b,(- (Arg a))).| is complex real ext-real Element of REAL
((|.a.| * |.b.|) ") * |.(b,(- (Arg a))).| is complex real ext-real Element of REAL
((|.a.| * |.b.|) ") * |.b.| is complex real ext-real Element of REAL
cos (Arg ((b,(- (Arg a))) * ((|.a.| * |.b.|) "))) is complex real ext-real Element of REAL
|.((b,(- (Arg a))) * ((|.a.| * |.b.|) ")).| * (cos (Arg ((b,(- (Arg a))) * ((|.a.| * |.b.|) ")))) is complex real ext-real Element of REAL
sin (Arg ((b,(- (Arg a))) * ((|.a.| * |.b.|) "))) is complex real ext-real Element of REAL
|.((b,(- (Arg a))) * ((|.a.| * |.b.|) ")).| * (sin (Arg ((b,(- (Arg a))) * ((|.a.| * |.b.|) ")))) is complex real ext-real Element of REAL
(|.((b,(- (Arg a))) * ((|.a.| * |.b.|) ")).| * (sin (Arg ((b,(- (Arg a))) * ((|.a.| * |.b.|) "))))) * <i> is complex set
(|.((b,(- (Arg a))) * ((|.a.| * |.b.|) ")).| * (cos (Arg ((b,(- (Arg a))) * ((|.a.| * |.b.|) "))))) + ((|.((b,(- (Arg a))) * ((|.a.| * |.b.|) ")).| * (sin (Arg ((b,(- (Arg a))) * ((|.a.| * |.b.|) "))))) * <i>) is complex set
((Re (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) / |.((b,(- (Arg a))) * ((|.a.| * |.b.|) ")).| is complex real ext-real Element of COMPLEX
|.((b,(- (Arg a))) * ((|.a.| * |.b.|) ")).| " is complex real ext-real set
((Re (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) * (|.((b,(- (Arg a))) * ((|.a.| * |.b.|) ")).| ") is complex real ext-real set
((|.a.| * |.b.|) ") / |.((b,(- (Arg a))) * ((|.a.| * |.b.|) ")).| is complex real ext-real Element of COMPLEX
((|.a.| * |.b.|) ") * (|.((b,(- (Arg a))) * ((|.a.| * |.b.|) ")).| ") is complex real ext-real set
(Re (b,(- (Arg a)))) * (((|.a.| * |.b.|) ") / |.((b,(- (Arg a))) * ((|.a.| * |.b.|) ")).|) is complex real ext-real Element of REAL
((|.a.| * |.b.|) ") / ((|.a.| * |.b.|) ") is complex real ext-real Element of COMPLEX
((|.a.| * |.b.|) ") " is complex real ext-real set
((|.a.| * |.b.|) ") * (((|.a.| * |.b.|) ") ") is complex real ext-real set
(((|.a.| * |.b.|) ") / ((|.a.| * |.b.|) ")) / |.b.| is complex real ext-real Element of COMPLEX
|.b.| " is complex real ext-real set
(((|.a.| * |.b.|) ") / ((|.a.| * |.b.|) ")) * (|.b.| ") is complex real ext-real set
((Re (a,b)) / |.a.|) * ((((|.a.| * |.b.|) ") / ((|.a.| * |.b.|) ")) / |.b.|) is complex real ext-real Element of COMPLEX
1 / |.b.| is complex real ext-real Element of COMPLEX
1 * (|.b.| ") is complex real ext-real set
((Re (a,b)) / |.a.|) * (1 / |.b.|) is complex real ext-real Element of COMPLEX
(Re (a,b)) * 1 is complex real ext-real Element of REAL
((Re (a,b)) * 1) / (|.a.| * |.b.|) is complex real ext-real Element of COMPLEX
((Re (a,b)) * 1) * ((|.a.| * |.b.|) ") is complex real ext-real set
((Im (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) / |.((b,(- (Arg a))) * ((|.a.| * |.b.|) ")).| is complex real ext-real Element of COMPLEX
((Im (b,(- (Arg a)))) * ((|.a.| * |.b.|) ")) * (|.((b,(- (Arg a))) * ((|.a.| * |.b.|) ")).| ") is complex real ext-real set
(Im (b,(- (Arg a)))) * (((|.a.| * |.b.|) ") / |.((b,(- (Arg a))) * ((|.a.| * |.b.|) ")).|) is complex real ext-real Element of REAL
(- ((Im (a,b)) / |.a.|)) * ((((|.a.| * |.b.|) ") / ((|.a.| * |.b.|) ")) / |.b.|) is complex real ext-real Element of COMPLEX
- (Im (a,b)) is complex real ext-real Element of REAL
(- (Im (a,b))) / |.a.| is complex real ext-real Element of COMPLEX
(- (Im (a,b))) * (|.a.| ") is complex real ext-real set
((- (Im (a,b))) / |.a.|) * (1 / |.b.|) is complex real ext-real Element of COMPLEX
(- (Im (a,b))) * 1 is complex real ext-real Element of REAL
((- (Im (a,b))) * 1) / (|.a.| * |.b.|) is complex real ext-real Element of COMPLEX
((- (Im (a,b))) * 1) * ((|.a.| * |.b.|) ") is complex real ext-real set
c is complex set
b is complex set
c - b is complex set
- b is complex set
c + (- b) is complex set
Arg (c - b) is complex real ext-real Element of REAL
a is complex set
a - b is complex set
a + (- b) is complex set
Arg (a - b) is complex real ext-real Element of REAL
(Arg (c - b)) - (Arg (a - b)) is complex real ext-real Element of REAL
- (Arg (a - b)) is complex real ext-real set
(Arg (c - b)) + (- (Arg (a - b))) is complex real ext-real set
(2 * PI) + ((Arg (c - b)) - (Arg (a - b))) is complex real ext-real Element of REAL
a is complex Element of COMPLEX
b is complex Element of COMPLEX
c is complex Element of COMPLEX
(a,b,c) is complex real ext-real set
c - b is complex Element of COMPLEX
- b is complex set
c + (- b) is complex set
Arg (c - b) is complex real ext-real Element of REAL
a - b is complex Element of COMPLEX
a + (- b) is complex set
Arg (a - b) is complex real ext-real Element of REAL
(Arg (c - b)) - (Arg (a - b)) is complex real ext-real Element of REAL
- (Arg (a - b)) is complex real ext-real set
(Arg (c - b)) + (- (Arg (a - b))) is complex real ext-real set
(Arg (c - b)) + 0 is complex real ext-real Element of REAL
(Arg (c - b)) + (Arg (a - b)) is complex real ext-real Element of REAL
c - b is complex Element of COMPLEX
- b is complex set
c + (- b) is complex set
Arg (c - b) is complex real ext-real Element of REAL
a - b is complex Element of COMPLEX
a + (- b) is complex set
Arg (a - b) is complex real ext-real Element of REAL
(Arg (c - b)) - (Arg (a - b)) is complex real ext-real Element of REAL
- (Arg (a - b)) is complex real ext-real set
(Arg (c - b)) + (- (Arg (a - b))) is complex real ext-real set
(Arg (a - b)) + 0 is complex real ext-real Element of REAL
(Arg (a - b)) + (Arg (c - b)) is complex real ext-real Element of REAL
(Arg (a - b)) - (Arg (c - b)) is complex real ext-real Element of REAL
- (Arg (c - b)) is complex real ext-real set
(Arg (a - b)) + (- (Arg (c - b))) is complex real ext-real set
(2 * PI) - ((Arg (a - b)) - (Arg (c - b))) is complex real ext-real Element of REAL
- ((Arg (a - b)) - (Arg (c - b))) is complex real ext-real set
(2 * PI) + (- ((Arg (a - b)) - (Arg (c - b)))) is complex real ext-real set
0 + (2 * PI) is complex real ext-real Element of REAL
((Arg (c - b)) - (Arg (a - b))) + (2 * PI) is complex real ext-real Element of REAL
c - b is complex Element of COMPLEX
- b is complex set
c + (- b) is complex set
Arg (c - b) is complex real ext-real Element of REAL
a - b is complex Element of COMPLEX
a + (- b) is complex set
Arg (a - b) is complex real ext-real Element of REAL
(Arg (c - b)) - (Arg (a - b)) is complex real ext-real Element of REAL
- (Arg (a - b)) is complex real ext-real set
(Arg (c - b)) + (- (Arg (a - b))) is complex real ext-real set
c - b is complex Element of COMPLEX
- b is complex set
c + (- b) is complex set
Arg (c - b) is complex real ext-real Element of REAL
a - b is complex Element of COMPLEX
a + (- b) is complex set
Arg (a - b) is complex real ext-real Element of REAL
(Arg (c - b)) - (Arg (a - b)) is complex real ext-real Element of REAL
- (Arg (a - b)) is complex real ext-real set
(Arg (c - b)) + (- (Arg (a - b))) is complex real ext-real set
a is complex Element of COMPLEX
b is complex Element of COMPLEX
a - b is complex Element of COMPLEX
- b is complex set
a + (- b) is complex set
c is complex Element of COMPLEX
(a,b,c) is complex real ext-real set
c - b is complex Element of COMPLEX
c + (- b) is complex set
((a - b),0,(c - b)) is complex real ext-real set
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
(c - b) - 0c is complex Element of COMPLEX
- 0c is complex set
(c - b) + (- 0c) is complex set
Arg ((c - b) - 0c) is complex real ext-real Element of REAL
(a - b) - 0c is complex Element of COMPLEX
(a - b) + (- 0c) is complex set
Arg ((a - b) - 0c) is complex real ext-real Element of REAL
(Arg ((c - b) - 0c)) - (Arg ((a - b) - 0c)) is complex real ext-real Element of REAL
- (Arg ((a - b) - 0c)) is complex real ext-real set
(Arg ((c - b) - 0c)) + (- (Arg ((a - b) - 0c))) is complex real ext-real set
((a - b),0c,(c - b)) is complex real ext-real set
Arg (c - b) is complex real ext-real Element of REAL
Arg (a - b) is complex real ext-real Element of REAL
(Arg (c - b)) - (Arg (a - b)) is complex real ext-real Element of REAL
- (Arg (a - b)) is complex real ext-real set
(Arg (c - b)) + (- (Arg (a - b))) is complex real ext-real set
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
(c - b) - 0c is complex Element of COMPLEX
- 0c is complex set
(c - b) + (- 0c) is complex set
Arg ((c - b) - 0c) is complex real ext-real Element of REAL
(a - b) - 0c is complex Element of COMPLEX
(a - b) + (- 0c) is complex set
Arg ((a - b) - 0c) is complex real ext-real Element of REAL
(Arg ((c - b) - 0c)) - (Arg ((a - b) - 0c)) is complex real ext-real Element of REAL
- (Arg ((a - b) - 0c)) is complex real ext-real set
(Arg ((c - b) - 0c)) + (- (Arg ((a - b) - 0c))) is complex real ext-real set
((a - b),0c,(c - b)) is complex real ext-real set
Arg (c - b) is complex real ext-real Element of REAL
Arg (a - b) is complex real ext-real Element of REAL
(Arg (c - b)) - (Arg (a - b)) is complex real ext-real Element of REAL
- (Arg (a - b)) is complex real ext-real set
(Arg (c - b)) + (- (Arg (a - b))) is complex real ext-real set
(2 * PI) + ((Arg (c - b)) - (Arg (a - b))) is complex real ext-real Element of REAL
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
(c - b) - 0c is complex Element of COMPLEX
- 0c is complex set
(c - b) + (- 0c) is complex set
Arg ((c - b) - 0c) is complex real ext-real Element of REAL
(a - b) - 0c is complex Element of COMPLEX
(a - b) + (- 0c) is complex set
Arg ((a - b) - 0c) is complex real ext-real Element of REAL
(Arg ((c - b) - 0c)) - (Arg ((a - b) - 0c)) is complex real ext-real Element of REAL
- (Arg ((a - b) - 0c)) is complex real ext-real set
(Arg ((c - b) - 0c)) + (- (Arg ((a - b) - 0c))) is complex real ext-real set
((a - b),0c,(c - b)) is complex real ext-real set
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
(c - b) - 0c is complex Element of COMPLEX
- 0c is complex set
(c - b) + (- 0c) is complex set
Arg ((c - b) - 0c) is complex real ext-real Element of REAL
(a - b) - 0c is complex Element of COMPLEX
(a - b) + (- 0c) is complex set
Arg ((a - b) - 0c) is complex real ext-real Element of REAL
(Arg ((c - b) - 0c)) - (Arg ((a - b) - 0c)) is complex real ext-real Element of REAL
- (Arg ((a - b) - 0c)) is complex real ext-real set
(Arg ((c - b) - 0c)) + (- (Arg ((a - b) - 0c))) is complex real ext-real set
((a - b),0c,(c - b)) is complex real ext-real set
a is complex Element of COMPLEX
b is complex Element of COMPLEX
c is complex Element of COMPLEX
(a,b,c) is complex real ext-real set
r is complex Element of COMPLEX
a + r is complex Element of COMPLEX
b + r is complex Element of COMPLEX
c + r is complex Element of COMPLEX
((a + r),(b + r),(c + r)) is complex real ext-real set
a - b is complex Element of COMPLEX
- b is complex set
a + (- b) is complex set
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
c - b is complex Element of COMPLEX
c + (- b) is complex set
((a - b),0c,(c - b)) is complex real ext-real set
(a + r) - (b + r) is complex Element of COMPLEX
- (b + r) is complex set
(a + r) + (- (b + r)) is complex set
(c + r) - (b + r) is complex Element of COMPLEX
(c + r) + (- (b + r)) is complex set
(((a + r) - (b + r)),0c,((c + r) - (b + r))) is complex real ext-real set
a is complex Element of COMPLEX
b is complex Element of COMPLEX
(a,b) is complex real ext-real Element of REAL
(a,0,b) is complex real ext-real set
Arg a is complex real ext-real Element of REAL
- (Arg a) is complex real ext-real Element of REAL
(b,(- (Arg a))) is complex Element of COMPLEX
|.b.| is complex real ext-real Element of REAL
Arg b is complex real ext-real Element of REAL
(- (Arg a)) + (Arg b) is complex real ext-real Element of REAL
cos ((- (Arg a)) + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos ((- (Arg a)) + (Arg b))) is complex real ext-real Element of REAL
sin ((- (Arg a)) + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin ((- (Arg a)) + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin ((- (Arg a)) + (Arg b)))) * <i> is complex set
(|.b.| * (cos ((- (Arg a)) + (Arg b)))) + ((|.b.| * (sin ((- (Arg a)) + (Arg b)))) * <i>) is complex set
Arg (b,(- (Arg a))) is complex real ext-real Element of REAL
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
b - 0c is complex Element of COMPLEX
- 0c is complex set
b + (- 0c) is complex set
Arg (b - 0c) is complex real ext-real Element of REAL
a - 0c is complex Element of COMPLEX
a + (- 0c) is complex set
Arg (a - 0c) is complex real ext-real Element of REAL
(Arg (b - 0c)) - (Arg (a - 0c)) is complex real ext-real Element of REAL
- (Arg (a - 0c)) is complex real ext-real set
(Arg (b - 0c)) + (- (Arg (a - 0c))) is complex real ext-real set
(a,0c,b) is complex real ext-real set
r is complex real ext-real integer set
(2 * PI) * r is complex real ext-real Element of REAL
((2 * PI) * r) + ((- (Arg a)) + (Arg b)) is complex real ext-real Element of REAL
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
b - 0c is complex Element of COMPLEX
- 0c is complex set
b + (- 0c) is complex set
Arg (b - 0c) is complex real ext-real Element of REAL
a - 0c is complex Element of COMPLEX
a + (- 0c) is complex set
Arg (a - 0c) is complex real ext-real Element of REAL
(Arg (b - 0c)) - (Arg (a - 0c)) is complex real ext-real Element of REAL
- (Arg (a - 0c)) is complex real ext-real set
(Arg (b - 0c)) + (- (Arg (a - 0c))) is complex real ext-real set
r is complex real ext-real integer set
(2 * PI) * r is complex real ext-real Element of REAL
((2 * PI) * r) + ((- (Arg a)) + (Arg b)) is complex real ext-real Element of REAL
r - 1 is complex real ext-real integer Element of REAL
- 1 is non zero complex real ext-real non positive negative integer set
r + (- 1) is complex real ext-real integer set
(2 * PI) * (r - 1) is complex real ext-real Element of REAL
(2 * PI) + ((- (Arg a)) + (Arg b)) is complex real ext-real Element of REAL
((2 * PI) * (r - 1)) + ((2 * PI) + ((- (Arg a)) + (Arg b))) is complex real ext-real Element of REAL
(a,0c,b) is complex real ext-real set
(Arg b) + (- (Arg a)) is complex real ext-real Element of REAL
(2 * PI) + ((Arg b) + (- (Arg a))) is complex real ext-real Element of REAL
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
b - 0c is complex Element of COMPLEX
- 0c is complex set
b + (- 0c) is complex set
Arg (b - 0c) is complex real ext-real Element of REAL
a - 0c is complex Element of COMPLEX
a + (- 0c) is complex set
Arg (a - 0c) is complex real ext-real Element of REAL
(Arg (b - 0c)) - (Arg (a - 0c)) is complex real ext-real Element of REAL
- (Arg (a - 0c)) is complex real ext-real set
(Arg (b - 0c)) + (- (Arg (a - 0c))) is complex real ext-real set
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
b - 0c is complex Element of COMPLEX
- 0c is complex set
b + (- 0c) is complex set
Arg (b - 0c) is complex real ext-real Element of REAL
a - 0c is complex Element of COMPLEX
a + (- 0c) is complex set
Arg (a - 0c) is complex real ext-real Element of REAL
(Arg (b - 0c)) - (Arg (a - 0c)) is complex real ext-real Element of REAL
- (Arg (a - 0c)) is complex real ext-real set
(Arg (b - 0c)) + (- (Arg (a - 0c))) is complex real ext-real set
- (- (Arg a)) is complex real ext-real Element of REAL
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
b - 0c is complex Element of COMPLEX
- 0c is complex set
b + (- 0c) is complex set
Arg (b - 0c) is complex real ext-real Element of REAL
a - 0c is complex Element of COMPLEX
a + (- 0c) is complex set
Arg (a - 0c) is complex real ext-real Element of REAL
(Arg (b - 0c)) - (Arg (a - 0c)) is complex real ext-real Element of REAL
- (Arg (a - 0c)) is complex real ext-real set
(Arg (b - 0c)) + (- (Arg (a - 0c))) is complex real ext-real set
(a,0c,b) is complex real ext-real set
(2 * PI) - (Arg a) is complex real ext-real Element of REAL
- (Arg a) is complex real ext-real set
(2 * PI) + (- (Arg a)) is complex real ext-real set
a is complex Element of COMPLEX
b is complex Element of COMPLEX
a - b is complex Element of COMPLEX
- b is complex set
a + (- b) is complex set
Arg (a - b) is complex real ext-real Element of REAL
c is complex Element of COMPLEX
(a,b,c) is complex real ext-real set
c - b is complex Element of COMPLEX
c + (- b) is complex set
Arg (c - b) is complex real ext-real Element of REAL
(c,b,a) is complex real ext-real set
(Arg (c - b)) - (Arg (a - b)) is complex real ext-real Element of REAL
- (Arg (a - b)) is complex real ext-real set
(Arg (c - b)) + (- (Arg (a - b))) is complex real ext-real set
(Arg (c - b)) - (Arg (a - b)) is complex real ext-real Element of REAL
- (Arg (a - b)) is complex real ext-real set
(Arg (c - b)) + (- (Arg (a - b))) is complex real ext-real set
- ((Arg (c - b)) - (Arg (a - b))) is complex real ext-real Element of REAL
(Arg (a - b)) - (Arg (c - b)) is complex real ext-real Element of REAL
- (Arg (c - b)) is complex real ext-real set
(Arg (a - b)) + (- (Arg (c - b))) is complex real ext-real set
(2 * PI) + ((Arg (c - b)) - (Arg (a - b))) is complex real ext-real Element of REAL
(Arg (c - b)) - (Arg (a - b)) is complex real ext-real Element of REAL
- (Arg (a - b)) is complex real ext-real set
(Arg (c - b)) + (- (Arg (a - b))) is complex real ext-real set
(Arg (c - b)) - (Arg (a - b)) is complex real ext-real Element of REAL
- (Arg (a - b)) is complex real ext-real set
(Arg (c - b)) + (- (Arg (a - b))) is complex real ext-real set
3 / 2 is non zero complex real ext-real positive non negative Element of COMPLEX
(3 / 2) * PI is complex real ext-real Element of REAL
a is complex Element of COMPLEX
b is complex Element of COMPLEX
(a,b) is complex Element of COMPLEX
b *' is complex Element of COMPLEX
a * (b *') is complex set
Re (a,b) is complex real ext-real Element of REAL
(a,0,b) is complex real ext-real set
Im (a,b) is complex real ext-real Element of REAL
|.a.| is complex real ext-real Element of REAL
|.b.| is complex real ext-real Element of REAL
|.a.| * |.b.| is complex real ext-real Element of REAL
(Im (a,b)) / (|.a.| * |.b.|) is complex real ext-real Element of COMPLEX
(|.a.| * |.b.|) " is complex real ext-real set
(Im (a,b)) * ((|.a.| * |.b.|) ") is complex real ext-real set
- ((Im (a,b)) / (|.a.| * |.b.|)) is complex real ext-real Element of COMPLEX
- (Im (a,b)) is complex real ext-real Element of REAL
(- (Im (a,b))) / (|.a.| * |.b.|) is complex real ext-real Element of COMPLEX
(- (Im (a,b))) * ((|.a.| * |.b.|) ") is complex real ext-real set
(a,b) is complex real ext-real Element of REAL
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
(a,0c,b) is complex real ext-real set
cos (a,b) is complex real ext-real Element of REAL
(Re (a,b)) / (|.a.| * |.b.|) is complex real ext-real Element of COMPLEX
(Re (a,b)) * ((|.a.| * |.b.|) ") is complex real ext-real set
sin (a,b) is complex real ext-real Element of REAL
- (|.a.| * |.b.|) is complex real ext-real Element of REAL
a is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
b is complex Element of COMPLEX
(a,b) is complex Element of COMPLEX
b *' is complex Element of COMPLEX
a * (b *') is complex set
Im (a,b) is complex real ext-real Element of REAL
|.b.| is complex real ext-real Element of REAL
|.a.| * |.b.| is complex real ext-real Element of REAL
- (|.a.| * |.b.|) is complex real ext-real Element of REAL
(a,0,b) is complex real ext-real set
Re (a,b) is complex real ext-real Element of REAL
a is complex Element of COMPLEX
b is complex Element of COMPLEX
c is complex Element of COMPLEX
a - b is complex Element of COMPLEX
- b is complex set
a + (- b) is complex set
c - b is complex Element of COMPLEX
c + (- b) is complex set
((a - b),(c - b)) is complex Element of COMPLEX
(c - b) *' is complex Element of COMPLEX
(a - b) * ((c - b) *') is complex set
Re ((a - b),(c - b)) is complex real ext-real Element of REAL
(a,b,c) is complex real ext-real set
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
((a - b),0c,(c - b)) is complex real ext-real set
a is complex Element of COMPLEX
b is complex Element of COMPLEX
a - b is complex Element of COMPLEX
- b is complex set
a + (- b) is complex set
|.(a - b).| is complex real ext-real Element of REAL
|.(a - b).| ^2 is complex real ext-real Element of REAL
|.(a - b).| * |.(a - b).| is complex real ext-real set
c is complex Element of COMPLEX
(a,b,c) is complex real ext-real set
c - b is complex Element of COMPLEX
c + (- b) is complex set
|.(c - b).| is complex real ext-real Element of REAL
|.(c - b).| ^2 is complex real ext-real Element of REAL
|.(c - b).| * |.(c - b).| is complex real ext-real set
(|.(a - b).| ^2) + (|.(c - b).| ^2) is complex real ext-real Element of REAL
a - c is complex Element of COMPLEX
- c is complex set
a + (- c) is complex set
|.(a - c).| is complex real ext-real Element of REAL
|.(a - c).| ^2 is complex real ext-real Element of REAL
|.(a - c).| * |.(a - c).| is complex real ext-real set
((a - b),(a - b)) is complex Element of COMPLEX
(a - b) *' is complex Element of COMPLEX
(a - b) * ((a - b) *') is complex set
Re ((a - b),(a - b)) is complex real ext-real Element of REAL
(Re ((a - b),(a - b))) + (|.(c - b).| ^2) is complex real ext-real Element of REAL
((c - b),(c - b)) is complex Element of COMPLEX
(c - b) *' is complex Element of COMPLEX
(c - b) * ((c - b) *') is complex set
Re ((c - b),(c - b)) is complex real ext-real Element of REAL
(Re ((a - b),(a - b))) + (Re ((c - b),(c - b))) is complex real ext-real Element of REAL
((a - b),(a - b)) + ((c - b),(c - b)) is complex Element of COMPLEX
Re (((a - b),(a - b)) + ((c - b),(c - b))) is complex real ext-real Element of REAL
(a - b) - (c - b) is complex Element of COMPLEX
- (c - b) is complex set
(a - b) + (- (c - b)) is complex set
((a - c),(a - c)) is complex Element of COMPLEX
(a - c) *' is complex Element of COMPLEX
(a - c) * ((a - c) *') is complex set
((a - b),(c - b)) is complex Element of COMPLEX
(a - b) * ((c - b) *') is complex set
((a - b),(a - b)) - ((a - b),(c - b)) is complex Element of COMPLEX
- ((a - b),(c - b)) is complex set
((a - b),(a - b)) + (- ((a - b),(c - b))) is complex set
((c - b),(a - b)) is complex Element of COMPLEX
(c - b) * ((a - b) *') is complex set
(((a - b),(a - b)) - ((a - b),(c - b))) - ((c - b),(a - b)) is complex Element of COMPLEX
- ((c - b),(a - b)) is complex set
(((a - b),(a - b)) - ((a - b),(c - b))) + (- ((c - b),(a - b))) is complex set
((((a - b),(a - b)) - ((a - b),(c - b))) - ((c - b),(a - b))) + ((c - b),(c - b)) is complex Element of COMPLEX
Re ((a - c),(a - c)) is complex real ext-real Element of REAL
((a - b),(c - b)) + ((c - b),(a - b)) is complex Element of COMPLEX
(((a - b),(a - b)) + ((c - b),(c - b))) - (((a - b),(c - b)) + ((c - b),(a - b))) is complex Element of COMPLEX
- (((a - b),(c - b)) + ((c - b),(a - b))) is complex set
(((a - b),(a - b)) + ((c - b),(c - b))) + (- (((a - b),(c - b)) + ((c - b),(a - b)))) is complex set
Re ((((a - b),(a - b)) + ((c - b),(c - b))) - (((a - b),(c - b)) + ((c - b),(a - b)))) is complex real ext-real Element of REAL
Re (((a - b),(c - b)) + ((c - b),(a - b))) is complex real ext-real Element of REAL
(Re (((a - b),(a - b)) + ((c - b),(c - b)))) - (Re (((a - b),(c - b)) + ((c - b),(a - b)))) is complex real ext-real Element of REAL
- (Re (((a - b),(c - b)) + ((c - b),(a - b)))) is complex real ext-real set
(Re (((a - b),(a - b)) + ((c - b),(c - b)))) + (- (Re (((a - b),(c - b)) + ((c - b),(a - b))))) is complex real ext-real set
Re ((a - b),(c - b)) is complex real ext-real Element of REAL
Re ((c - b),(a - b)) is complex real ext-real Element of REAL
(Re ((a - b),(c - b))) + (Re ((c - b),(a - b))) is complex real ext-real Element of REAL
(Re (((a - b),(a - b)) + ((c - b),(c - b)))) - ((Re ((a - b),(c - b))) + (Re ((c - b),(a - b)))) is complex real ext-real Element of REAL
- ((Re ((a - b),(c - b))) + (Re ((c - b),(a - b)))) is complex real ext-real set
(Re (((a - b),(a - b)) + ((c - b),(c - b)))) + (- ((Re ((a - b),(c - b))) + (Re ((c - b),(a - b))))) is complex real ext-real set
((a - b),(c - b)) *' is complex Element of COMPLEX
Re (((a - b),(c - b)) *') is complex real ext-real Element of REAL
(Re ((a - b),(c - b))) + (Re (((a - b),(c - b)) *')) is complex real ext-real Element of REAL
(Re (((a - b),(a - b)) + ((c - b),(c - b)))) - ((Re ((a - b),(c - b))) + (Re (((a - b),(c - b)) *'))) is complex real ext-real Element of REAL
- ((Re ((a - b),(c - b))) + (Re (((a - b),(c - b)) *'))) is complex real ext-real set
(Re (((a - b),(a - b)) + ((c - b),(c - b)))) + (- ((Re ((a - b),(c - b))) + (Re (((a - b),(c - b)) *')))) is complex real ext-real set
(Re ((a - b),(c - b))) + (Re ((a - b),(c - b))) is complex real ext-real Element of REAL
(Re (((a - b),(a - b)) + ((c - b),(c - b)))) - ((Re ((a - b),(c - b))) + (Re ((a - b),(c - b)))) is complex real ext-real Element of REAL
- ((Re ((a - b),(c - b))) + (Re ((a - b),(c - b)))) is complex real ext-real set
(Re (((a - b),(a - b)) + ((c - b),(c - b)))) + (- ((Re ((a - b),(c - b))) + (Re ((a - b),(c - b))))) is complex real ext-real set
0 + (Re ((a - b),(c - b))) is complex real ext-real Element of REAL
(Re (((a - b),(a - b)) + ((c - b),(c - b)))) - (0 + (Re ((a - b),(c - b)))) is complex real ext-real Element of REAL
- (0 + (Re ((a - b),(c - b)))) is complex real ext-real set
(Re (((a - b),(a - b)) + ((c - b),(c - b)))) + (- (0 + (Re ((a - b),(c - b))))) is complex real ext-real set
(Re (((a - b),(a - b)) + ((c - b),(c - b)))) - 0 is complex real ext-real Element of REAL
- 0 is zero complex real ext-real non positive non negative integer V61() V62() V63() V64() V65() V66() V67() set
(Re (((a - b),(a - b)) + ((c - b),(c - b)))) + (- 0) is complex real ext-real set
a is complex Element of COMPLEX
b is complex Element of COMPLEX
c is complex Element of COMPLEX
(a,b,c) is complex real ext-real set
r is complex real ext-real Element of REAL
(a,r) is complex Element of COMPLEX
|.a.| is complex real ext-real Element of REAL
Arg a is complex real ext-real Element of REAL
r + (Arg a) is complex real ext-real Element of REAL
cos (r + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (cos (r + (Arg a))) is complex real ext-real Element of REAL
sin (r + (Arg a)) is complex real ext-real Element of REAL
|.a.| * (sin (r + (Arg a))) is complex real ext-real Element of REAL
(|.a.| * (sin (r + (Arg a)))) * <i> is complex set
(|.a.| * (cos (r + (Arg a)))) + ((|.a.| * (sin (r + (Arg a)))) * <i>) is complex set
(b,r) is complex Element of COMPLEX
|.b.| is complex real ext-real Element of REAL
Arg b is complex real ext-real Element of REAL
r + (Arg b) is complex real ext-real Element of REAL
cos (r + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (cos (r + (Arg b))) is complex real ext-real Element of REAL
sin (r + (Arg b)) is complex real ext-real Element of REAL
|.b.| * (sin (r + (Arg b))) is complex real ext-real Element of REAL
(|.b.| * (sin (r + (Arg b)))) * <i> is complex set
(|.b.| * (cos (r + (Arg b)))) + ((|.b.| * (sin (r + (Arg b)))) * <i>) is complex set
(c,r) is complex Element of COMPLEX
|.c.| is complex real ext-real Element of REAL
Arg c is complex real ext-real Element of REAL
r + (Arg c) is complex real ext-real Element of REAL
cos (r + (Arg c)) is complex real ext-real Element of REAL
|.c.| * (cos (r + (Arg c))) is complex real ext-real Element of REAL
sin (r + (Arg c)) is complex real ext-real Element of REAL
|.c.| * (sin (r + (Arg c))) is complex real ext-real Element of REAL
(|.c.| * (sin (r + (Arg c)))) * <i> is complex set
(|.c.| * (cos (r + (Arg c)))) + ((|.c.| * (sin (r + (Arg c)))) * <i>) is complex set
((a,r),(b,r),(c,r)) is complex real ext-real set
c - b is complex Element of COMPLEX
- b is complex set
c + (- b) is complex set
a - b is complex Element of COMPLEX
a + (- b) is complex set
(c,r) - (b,r) is complex Element of COMPLEX
- (b,r) is complex set
(c,r) + (- (b,r)) is complex set
(a,r) - (b,r) is complex Element of COMPLEX
(a,r) + (- (b,r)) is complex set
((c - b),r) is complex Element of COMPLEX
|.(c - b).| is complex real ext-real Element of REAL
Arg (c - b) is complex real ext-real Element of REAL
r + (Arg (c - b)) is complex real ext-real Element of REAL
cos (r + (Arg (c - b))) is complex real ext-real Element of REAL
|.(c - b).| * (cos (r + (Arg (c - b)))) is complex real ext-real Element of REAL
sin (r + (Arg (c - b))) is complex real ext-real Element of REAL
|.(c - b).| * (sin (r + (Arg (c - b)))) is complex real ext-real Element of REAL
(|.(c - b).| * (sin (r + (Arg (c - b))))) * <i> is complex set
(|.(c - b).| * (cos (r + (Arg (c - b))))) + ((|.(c - b).| * (sin (r + (Arg (c - b))))) * <i>) is complex set
Arg ((c - b),r) is complex real ext-real Element of REAL
Ib is complex real ext-real integer set
(2 * PI) * Ib is complex real ext-real Element of REAL
((2 * PI) * Ib) + (r + (Arg (c - b))) is complex real ext-real Element of REAL
((a - b),r) is complex Element of COMPLEX
|.(a - b).| is complex real ext-real Element of REAL
Arg (a - b) is complex real ext-real Element of REAL
r + (Arg (a - b)) is complex real ext-real Element of REAL
cos (r + (Arg (a - b))) is complex real ext-real Element of REAL
|.(a - b).| * (cos (r + (Arg (a - b)))) is complex real ext-real Element of REAL
sin (r + (Arg (a - b))) is complex real ext-real Element of REAL
|.(a - b).| * (sin (r + (Arg (a - b)))) is complex real ext-real Element of REAL
(|.(a - b).| * (sin (r + (Arg (a - b))))) * <i> is complex set
(|.(a - b).| * (cos (r + (Arg (a - b))))) + ((|.(a - b).| * (sin (r + (Arg (a - b))))) * <i>) is complex set
Arg ((a - b),r) is complex real ext-real Element of REAL
Iba is complex real ext-real integer set
(2 * PI) * Iba is complex real ext-real Element of REAL
((2 * PI) * Iba) + (r + (Arg (a - b))) is complex real ext-real Element of REAL
Arg ((c,r) - (b,r)) is complex real ext-real Element of REAL
Arg ((a,r) - (b,r)) is complex real ext-real Element of REAL
(Arg ((c,r) - (b,r))) - (Arg ((a,r) - (b,r))) is complex real ext-real Element of REAL
- (Arg ((a,r) - (b,r))) is complex real ext-real set
(Arg ((c,r) - (b,r))) + (- (Arg ((a,r) - (b,r)))) is complex real ext-real set
((2 * PI) * Ib) + r is complex real ext-real Element of REAL
(((2 * PI) * Ib) + r) + (Arg (c - b)) is complex real ext-real Element of REAL
((2 * PI) * Iba) + r is complex real ext-real Element of REAL
(((2 * PI) * Iba) + r) + (Arg (a - b)) is complex real ext-real Element of REAL
((((2 * PI) * Ib) + r) + (Arg (c - b))) - ((((2 * PI) * Iba) + r) + (Arg (a - b))) is complex real ext-real Element of REAL
- ((((2 * PI) * Iba) + r) + (Arg (a - b))) is complex real ext-real set
((((2 * PI) * Ib) + r) + (Arg (c - b))) + (- ((((2 * PI) * Iba) + r) + (Arg (a - b)))) is complex real ext-real set
(Arg (c - b)) - (Arg (a - b)) is complex real ext-real Element of REAL
- (Arg (a - b)) is complex real ext-real set
(Arg (c - b)) + (- (Arg (a - b))) is complex real ext-real set
Ib - Iba is complex real ext-real integer set
- Iba is complex real ext-real integer set
Ib + (- Iba) is complex real ext-real integer set
(2 * PI) * (Ib - Iba) is complex real ext-real Element of REAL
((Arg (c - b)) - (Arg (a - b))) + ((2 * PI) * (Ib - Iba)) is complex real ext-real Element of REAL
(((Arg (c - b)) - (Arg (a - b))) + ((2 * PI) * (Ib - Iba))) + (2 * PI) is complex real ext-real Element of REAL
(Ib - Iba) + 1 is complex real ext-real integer Element of REAL
(2 * PI) * ((Ib - Iba) + 1) is complex real ext-real Element of REAL
((Arg (c - b)) - (Arg (a - b))) + ((2 * PI) * ((Ib - Iba) + 1)) is complex real ext-real Element of REAL
(2 * PI) + ((Arg (c - b)) - (Arg (a - b))) is complex real ext-real Element of REAL
(Ib - Iba) + (- 1) is complex real ext-real integer Element of REAL
(2 * PI) * ((Ib - Iba) + (- 1)) is complex real ext-real Element of REAL
((2 * PI) + ((Arg (c - b)) - (Arg (a - b)))) + ((2 * PI) * ((Ib - Iba) + (- 1))) is complex real ext-real Element of REAL
(((Arg (c - b)) - (Arg (a - b))) + ((2 * PI) * (Ib - Iba))) + (2 * PI) is complex real ext-real Element of REAL
((2 * PI) + ((Arg (c - b)) - (Arg (a - b)))) + ((2 * PI) * (Ib - Iba)) is complex real ext-real Element of REAL
a is complex Element of COMPLEX
b is complex Element of COMPLEX
(a,b,a) is complex real ext-real set
a - b is complex Element of COMPLEX
- b is complex set
a + (- b) is complex set
Arg (a - b) is complex real ext-real Element of REAL
(Arg (a - b)) - (Arg (a - b)) is complex real ext-real Element of REAL
- (Arg (a - b)) is complex real ext-real set
(Arg (a - b)) + (- (Arg (a - b))) is complex real ext-real set
a is complex Element of COMPLEX
b is complex Element of COMPLEX
c is complex Element of COMPLEX
(a,b,c) is complex real ext-real set
(c,b,a) is complex real ext-real set
(2 * PI) - (a,b,c) is complex real ext-real Element of REAL
- (a,b,c) is complex real ext-real set
(2 * PI) + (- (a,b,c)) is complex real ext-real set
a - b is complex Element of COMPLEX
- b is complex set
a + (- b) is complex set
Arg (a - b) is complex real ext-real Element of REAL
c - b is complex Element of COMPLEX
c + (- b) is complex set
Arg (c - b) is complex real ext-real Element of REAL
(Arg (a - b)) - (Arg (c - b)) is complex real ext-real Element of REAL
- (Arg (c - b)) is complex real ext-real set
(Arg (a - b)) + (- (Arg (c - b))) is complex real ext-real set
- ((Arg (a - b)) - (Arg (c - b))) is complex real ext-real Element of REAL
- (- ((Arg (a - b)) - (Arg (c - b)))) is complex real ext-real Element of REAL
(Arg (c - b)) - (Arg (a - b)) is complex real ext-real Element of REAL
- (Arg (a - b)) is complex real ext-real set
(Arg (c - b)) + (- (Arg (a - b))) is complex real ext-real set
(2 * PI) + ((Arg (c - b)) - (Arg (a - b))) is complex real ext-real Element of REAL
(2 * PI) - ((Arg (a - b)) - (Arg (c - b))) is complex real ext-real Element of REAL
- ((Arg (a - b)) - (Arg (c - b))) is complex real ext-real set
(2 * PI) + (- ((Arg (a - b)) - (Arg (c - b)))) is complex real ext-real set
a - b is complex Element of COMPLEX
- b is complex set
a + (- b) is complex set
Arg (a - b) is complex real ext-real Element of REAL
c - b is complex Element of COMPLEX
c + (- b) is complex set
Arg (c - b) is complex real ext-real Element of REAL
(Arg (a - b)) - (Arg (c - b)) is complex real ext-real Element of REAL
- (Arg (c - b)) is complex real ext-real set
(Arg (a - b)) + (- (Arg (c - b))) is complex real ext-real set
(Arg (c - b)) - (Arg (a - b)) is complex real ext-real Element of REAL
- (Arg (a - b)) is complex real ext-real set
(Arg (c - b)) + (- (Arg (a - b))) is complex real ext-real set
(2 * PI) - ((Arg (c - b)) - (Arg (a - b))) is complex real ext-real Element of REAL
- ((Arg (c - b)) - (Arg (a - b))) is complex real ext-real set
(2 * PI) + (- ((Arg (c - b)) - (Arg (a - b)))) is complex real ext-real set
- ((Arg (a - b)) - (Arg (c - b))) is complex real ext-real Element of REAL
- (- ((Arg (a - b)) - (Arg (c - b)))) is complex real ext-real Element of REAL
(a,b,c) + (c,b,a) is complex real ext-real set
((2 * PI) - ((Arg (c - b)) - (Arg (a - b)))) + ((Arg (c - b)) - (Arg (a - b))) is complex real ext-real Element of REAL
a - b is complex Element of COMPLEX
- b is complex set
a + (- b) is complex set
Arg (a - b) is complex real ext-real Element of REAL
c - b is complex Element of COMPLEX
c + (- b) is complex set
Arg (c - b) is complex real ext-real Element of REAL
(Arg (a - b)) - (Arg (c - b)) is complex real ext-real Element of REAL
- (Arg (c - b)) is complex real ext-real set
(Arg (a - b)) + (- (Arg (c - b))) is complex real ext-real set
a - b is complex Element of COMPLEX
- b is complex set
a + (- b) is complex set
Arg (a - b) is complex real ext-real Element of REAL
c - b is complex Element of COMPLEX
c + (- b) is complex set
Arg (c - b) is complex real ext-real Element of REAL
(Arg (a - b)) - (Arg (c - b)) is complex real ext-real Element of REAL
- (Arg (c - b)) is complex real ext-real set
(Arg (a - b)) + (- (Arg (c - b))) is complex real ext-real set
a is complex Element of COMPLEX
b is complex Element of COMPLEX
c is complex Element of COMPLEX
(a,b,c) is complex real ext-real set
(c,b,a) is complex real ext-real set
(a,b,c) + (c,b,a) is complex real ext-real set
(2 * PI) - (a,b,c) is complex real ext-real Element of REAL
- (a,b,c) is complex real ext-real set
(2 * PI) + (- (a,b,c)) is complex real ext-real set
a is complex Element of COMPLEX
b is complex Element of COMPLEX
c is complex Element of COMPLEX
(a,b,c) is complex real ext-real set
(c,b,a) is complex real ext-real set
(a,b,c) + (c,b,a) is complex real ext-real set
a is complex Element of COMPLEX
b is complex Element of COMPLEX
c is complex Element of COMPLEX
(a,b,c) is complex real ext-real set
(c,b,a) is complex real ext-real set
(a,b,c) + (c,b,a) is complex real ext-real set
0 + (2 * PI) is complex real ext-real Element of REAL
a is complex Element of COMPLEX
b is complex Element of COMPLEX
c is complex Element of COMPLEX
(a,b,c) is complex real ext-real set
(b,c,a) is complex real ext-real set
(c,a,b) is complex real ext-real set
b - a is complex Element of COMPLEX
- a is complex set
b + (- a) is complex set
a - c is complex Element of COMPLEX
- c is complex set
a + (- c) is complex set
c - b is complex Element of COMPLEX
- b is complex set
c + (- b) is complex set
Arg (c - b) is complex real ext-real Element of REAL
- (c - b) is complex Element of COMPLEX
Arg (- (c - b)) is complex real ext-real Element of REAL
- (b - a) is complex Element of COMPLEX
a - b is complex Element of COMPLEX
a + (- b) is complex set
- (a - c) is complex Element of COMPLEX
c - a is complex Element of COMPLEX
c + (- a) is complex set
- (c - a) is complex Element of COMPLEX
Arg (a - c) is complex real ext-real Element of REAL
b - c is complex Element of COMPLEX
b + (- c) is complex set
Arg (b - c) is complex real ext-real Element of REAL
Arg (b - a) is complex real ext-real Element of REAL
Arg (c - a) is complex real ext-real Element of REAL
Arg (a - b) is complex real ext-real Element of REAL
0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX
a is complex Element of COMPLEX
Im a is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
b is complex Element of COMPLEX
Arg b is complex real ext-real Element of REAL
(a,0c,b) is complex real ext-real set
(0c,b,a) is complex real ext-real set
(a,0c,b) + (0c,b,a) is complex real ext-real set
(b,a,0c) is complex real ext-real set
((a,0c,b) + (0c,b,a)) + (b,a,0c) is complex real ext-real set
0 * <i> is complex set
(Re a) + (0 * <i>) is complex set
Arg a is complex real ext-real Element of REAL
- a is complex Element of COMPLEX
Arg (- a) is complex real ext-real Element of REAL
(Arg a) - (Arg (- a)) is complex real ext-real Element of REAL
- (Arg (- a)) is complex real ext-real set
(Arg a) + (- (Arg (- a))) is complex real ext-real set
(Arg a) + PI is complex real ext-real Element of REAL
(Arg a) - ((Arg a) + PI) is complex real ext-real Element of REAL
- ((Arg a) + PI) is complex real ext-real set
(Arg a) + (- ((Arg a) + PI)) is complex real ext-real set
- PI is complex real ext-real Element of REAL
b - 0c is complex Element of COMPLEX
- 0c is complex set
b + (- 0c) is complex set
Arg (b - 0c) is complex real ext-real Element of REAL
a - 0c is complex Element of COMPLEX
a + (- 0c) is complex set
Arg (a - 0c) is complex real ext-real Element of REAL
(Arg (b - 0c)) - (Arg (a - 0c)) is complex real ext-real Element of REAL
- (Arg (a - 0c)) is complex real ext-real set
(Arg (b - 0c)) + (- (Arg (a - 0c))) is complex real ext-real set
(Arg b) - (Arg a) is complex real ext-real Element of REAL
- (Arg a) is complex real ext-real set
(Arg b) + (- (Arg a)) is complex real ext-real set
Im b is complex real ext-real Element of REAL
- b is complex Element of COMPLEX
Arg (- b) is complex real ext-real Element of REAL
(Arg b) - (Arg (- b)) is complex real ext-real Element of REAL
- (Arg (- b)) is complex real ext-real set
(Arg b) + (- (Arg (- b))) is complex real ext-real set
(Arg b) + PI is complex real ext-real Element of REAL
(Arg b) - ((Arg b) + PI) is complex real ext-real Element of REAL
- ((Arg b) + PI) is complex real ext-real set
(Arg b) + (- ((Arg b) + PI)) is complex real ext-real set
a - b is complex Element of COMPLEX
- b is complex set
a + (- b) is complex set
Im (a - b) is complex real ext-real Element of REAL
(Im a) - (Im b) is complex real ext-real Element of REAL
- (Im b) is complex real ext-real set
(Im a) + (- (Im b)) is complex real ext-real set
- (Im b) is complex real ext-real Element of REAL
Arg (a - b) is complex real ext-real Element of REAL
b - a is complex Element of COMPLEX
- a is complex set
b + (- a) is complex set
Arg (b - a) is complex real ext-real Element of REAL
- (Arg (b - a)) is complex real ext-real Element of REAL
(Arg (a - b)) - (Arg (b - a)) is complex real ext-real Element of REAL
- (Arg (b - a)) is complex real ext-real set
(Arg (a - b)) + (- (Arg (b - a))) is complex real ext-real set
- (a - b) is complex Element of COMPLEX
Arg (- (a - b)) is complex real ext-real Element of REAL
(Arg (a - b)) - (Arg (- (a - b))) is complex real ext-real Element of REAL
- (Arg (- (a - b))) is complex real ext-real set
(Arg (a - b)) + (- (Arg (- (a - b)))) is complex real ext-real set
(Arg (a - b)) - PI is complex real ext-real Element of REAL
- PI is complex real ext-real set
(Arg (a - b)) + (- PI) is complex real ext-real set
(Arg (a - b)) - ((Arg (a - b)) - PI) is complex real ext-real Element of REAL
- ((Arg (a - b)) - PI) is complex real ext-real set
(Arg (a - b)) + (- ((Arg (a - b)) - PI)) is complex real ext-real set
0 - PI is complex real ext-real Element of REAL
0 + (- PI) is complex real ext-real set
(0 - PI) + PI is complex real ext-real Element of REAL
(Arg (- a)) + (- (Arg (b - a))) is complex real ext-real Element of REAL
0c - a is complex Element of COMPLEX
0c + (- a) is complex set
Arg (0c - a) is complex real ext-real Element of REAL
(Arg (0c - a)) - (Arg (b - a)) is complex real ext-real Element of REAL
(Arg (0c - a)) + (- (Arg (b - a))) is complex real ext-real set
c is complex Element of COMPLEX
Im c is complex real ext-real Element of REAL
Re c is complex real ext-real Element of REAL
r is complex Element of COMPLEX
Arg r is complex real ext-real Element of REAL
Re r is complex real ext-real Element of REAL
(Re r) + 0 is complex real ext-real Element of REAL
- (Re c) is complex real ext-real Element of REAL
(Re r) + (- (Re c)) is complex real ext-real Element of REAL
r - c is complex Element of COMPLEX
- c is complex set
r + (- c) is complex set
Arg (r - c) is complex real ext-real Element of REAL
|.r.| is complex real ext-real Element of REAL
|.(r - c).| is complex real ext-real Element of REAL
Re (r - c) is complex real ext-real Element of REAL
(Re r) - (Re c) is complex real ext-real Element of REAL
- (Re c) is complex real ext-real set
(Re r) + (- (Re c)) is complex real ext-real set
cos (Arg (r - c)) is complex real ext-real Element of REAL
|.(r - c).| * (cos (Arg (r - c))) is complex real ext-real Element of REAL
sin (Arg (r - c)) is complex real ext-real Element of REAL
|.(r - c).| * (sin (Arg (r - c))) is complex real ext-real Element of REAL
(|.(r - c).| * (sin (Arg (r - c)))) * <i> is complex set
(|.(r - c).| * (cos (Arg (r - c)))) + ((|.(r - c).| * (sin (Arg (r - c)))) * <i>) is complex set
Im (r - c) is complex real ext-real Element of REAL
(Im (r - c)) * <i> is complex set
(Re (r - c)) + ((Im (r - c)) * <i>) is complex set
Im r is complex real ext-real Element of REAL
(Im r) - (Im c) is complex real ext-real Element of REAL
- (Im c) is complex real ext-real set
(Im r) + (- (Im c)) is complex real ext-real set
(Re r) ^2 is complex real ext-real Element of REAL
(Re r) * (Re r) is complex real ext-real set
(Im r) ^2 is complex real ext-real Element of REAL
(Im r) * (Im r) is complex real ext-real set
((Re r) ^2) + ((Im r) ^2) is complex real ext-real Element of REAL
sqrt (((Re r) ^2) + ((Im r) ^2)) is complex real ext-real Element of REAL
(Re (r - c)) ^2 is complex real ext-real Element of REAL
(Re (r - c)) * (Re (r - c)) is complex real ext-real set
((Re (r - c)) ^2) + ((Im r) ^2) is complex real ext-real Element of REAL
sqrt (((Re (r - c)) ^2) + ((Im r) ^2)) is complex real ext-real Element of REAL
cos (Arg r) is complex real ext-real Element of REAL
|.r.| * (cos (Arg r)) is complex real ext-real Element of REAL
sin (Arg r) is complex real ext-real Element of REAL
|.r.| * (sin (Arg r)) is complex real ext-real Element of REAL
(|.r.| * (sin (Arg r))) * <i> is complex set
(|.r.| * (cos (Arg r))) + ((|.r.| * (sin (Arg r))) * <i>) is complex set
(Im r) * <i> is complex set
(Re r) + ((Im r) * <i>) is complex set
|.(r - c).| / |.r.| is complex real ext-real Element of COMPLEX
|.r.| " is complex real ext-real set
|.(r - c).| * (|.r.| ") is complex real ext-real set
(sin (Arg r)) / (sin (Arg (r - c))) is complex real ext-real Element of COMPLEX
(sin (Arg (r - c))) " is complex real ext-real set
(sin (Arg r)) * ((sin (Arg (r - c))) ") is complex real ext-real set
1 * (sin (Arg (r - c))) is complex real ext-real Element of REAL
((sin (Arg r)) / (sin (Arg (r - c)))) * (sin (Arg (r - c))) is complex real ext-real Element of REAL
- (Arg r) is complex real ext-real Element of REAL
(Arg (r - c)) + (- (Arg r)) is complex real ext-real Element of REAL
(Arg r) + (- (Arg r)) is complex real ext-real Element of REAL
(Arg (r - c)) - (Arg r) is complex real ext-real Element of REAL
- (Arg r) is complex real ext-real set
(Arg (r - c)) + (- (Arg r)) is complex real ext-real set
0 + ((Im (r - c)) * <i>) is complex set
- (Arg r) is complex real ext-real Element of REAL
(Arg (r - c)) + (- (Arg r)) is complex real ext-real Element of REAL
(Arg r) + (- (Arg r)) is complex real ext-real Element of REAL
(Arg (r - c)) - (Arg r) is complex real ext-real Element of REAL
- (Arg r) is complex real ext-real set
(Arg (r - c)) + (- (Arg r)) is complex real ext-real set
(Arg (r - c)) - (Arg r) is complex real ext-real Element of REAL
- (Arg r) is complex real ext-real set
(Arg (r - c)) + (- (Arg r)) is complex real ext-real set
- (Arg r) is complex real ext-real Element of REAL
(Arg (r - c)) + (- (Arg r)) is complex real ext-real Element of REAL
(Arg r) + (- (Arg r)) is complex real ext-real Element of REAL
0 + ((Im r) * <i>) is complex set
- (Arg r) is complex real ext-real Element of REAL
(Arg (r - c)) + (- (Arg r)) is complex real ext-real Element of REAL
(Arg r) + (- (Arg r)) is complex real ext-real Element of REAL
((sin (Arg r)) / (sin (Arg (r - c)))) * (sin (Arg (r - c))) is complex real ext-real Element of REAL
1 * (sin (Arg (r - c))) is complex real ext-real Element of REAL
- (Arg r) is complex real ext-real Element of REAL
(Arg (r - c)) + (- (Arg r)) is complex real ext-real Element of REAL
(Arg r) + (- (Arg r)) is complex real ext-real Element of REAL
(Arg (b - a)) - (Arg b) is complex real ext-real Element of REAL
- (Arg b) is complex real ext-real set
(Arg (b - a)) + (- (Arg b)) is complex real ext-real set
(Arg (- (a - b))) - (Arg b) is complex real ext-real Element of REAL
(Arg (- (a - b))) + (- (Arg b)) is complex real ext-real set
((Arg (a - b)) - PI) - (Arg b) is complex real ext-real Element of REAL
((Arg (a - b)) - PI) + (- (Arg b)) is complex real ext-real set
(Arg (a - b)) - ((Arg b) + PI) is complex real ext-real Element of REAL
(Arg (a - b)) + (- ((Arg b) + PI)) is complex real ext-real set
(Arg (a - b)) - (Arg (- b)) is complex real ext-real Element of REAL
(Arg (a - b)) + (- (Arg (- b))) is complex real ext-real set
0c - b is complex Element of COMPLEX
0c + (- b) is complex set
Arg (0c - b) is complex real ext-real Element of REAL
(Arg (a - b)) - (Arg (0c - b)) is complex real ext-real Element of REAL
- (Arg (0c - b)) is complex real ext-real set
(Arg (a - b)) + (- (Arg (0c - b))) is complex real ext-real set
((Arg b) - (Arg (- b))) - (Arg a) is complex real ext-real Element of REAL
((Arg b) - (Arg (- b))) + (- (Arg a)) is complex real ext-real set
(((Arg b) - (Arg (- b))) - (Arg a)) + (Arg (a - b)) is complex real ext-real Element of REAL
(Arg (- a)) - (Arg (b - a)) is complex real ext-real Element of REAL
(Arg (- a)) + (- (Arg (b - a))) is complex real ext-real set
((((Arg b) - (Arg (- b))) - (Arg a)) + (Arg (a - b))) + ((Arg (- a)) - (Arg (b - a))) is complex real ext-real Element of REAL
0 + (Arg (a - b)) is complex real ext-real Element of REAL
(2 * PI) - (Arg (a - b)) is complex real ext-real Element of REAL
- (Arg (a - b)) is complex real ext-real set
(2 * PI) + (- (Arg (a - b))) is complex real ext-real set
(Arg (- a)) - ((Arg (a - b)) - PI) is complex real ext-real Element of REAL
(Arg (- a)) + (- ((Arg (a - b)) - PI)) is complex real ext-real set
(Arg a) + ((2 * PI) - (Arg (a - b))) is complex real ext-real Element of REAL
a is complex Element of COMPLEX
b is complex Element of COMPLEX
c is complex Element of COMPLEX
(a,b,c) is complex real ext-real set
(b,c,a) is complex real ext-real set
(a,b,c) + (b,c,a) is complex real ext-real set
(c,a,b) is complex real ext-real set
((a,b,c) + (b,c,a)) + (c,a,b) is complex real ext-real set
c - b is complex Element of COMPLEX
- b is complex set
c + (- b) is complex set
- b is complex Element of COMPLEX
a + (- b) is complex Element of COMPLEX
Arg (a + (- b)) is complex real ext-real Element of REAL
- (Arg (a + (- b))) is complex real ext-real Element of REAL
((a + (- b)),(- (Arg (a + (- b))))) is complex Element of COMPLEX
|.(a + (- b)).| is complex real ext-real Element of REAL
(- (Arg (a + (- b)))) + (Arg (a + (- b))) is complex real ext-real Element of REAL
cos ((- (Arg (a + (- b)))) + (Arg (a + (- b)))) is complex real ext-real Element of REAL
|.(a + (- b)).| * (cos ((- (Arg (a + (- b)))) + (Arg (a + (- b))))) is complex real ext-real Element of REAL
sin ((- (Arg (a + (- b)))) + (Arg (a + (- b)))) is complex real ext-real Element of REAL
|.(a + (- b)).| * (sin ((- (Arg (a + (- b)))) + (Arg (a + (- b))))) is complex real ext-real Element of REAL
(|.(a + (- b)).| * (sin ((- (Arg (a + (- b)))) + (Arg (a + (- b)))))) * <i> is complex set
(|.(a + (- b)).| * (cos ((- (Arg (a + (- b)))) + (Arg (a + (- b)))))) + ((|.(a + (- b)).| * (sin ((- (Arg (a + (- b)))) + (Arg (a + (- b)))))) * <i>) is complex set
c + (- b) is complex Element of COMPLEX
((c + (- b)),(- (Arg (a + (- b))))) is complex Element of COMPLEX
|.(c + (- b)).| is complex real ext-real Element of REAL
Arg (c + (- b)) is complex real ext-real Element of REAL
(- (Arg (a + (- b)))) + (Arg (c + (- b))) is complex real ext-real Element of REAL
cos ((- (Arg (a + (- b)))) + (Arg (c + (- b)))) is complex real ext-real Element of REAL
|.(c + (- b)).| * (cos ((- (Arg (a + (- b)))) + (Arg (c + (- b))))) is complex real ext-real Element of REAL
sin ((- (Arg (a + (- b)))) + (Arg (c + (- b)))) is complex real ext-real Element of REAL
|.(c + (- b)).| * (sin ((- (Arg (a + (- b)))) + (Arg (c + (- b))))) is complex real ext-real Element of REAL
(|.(c + (- b)).| * (sin ((- (Arg (a + (- b)))) + (Arg (c + (- b)))))) * <i> is complex set
(|.(c + (- b)).| * (cos ((- (Arg (a + (- b)))) + (Arg (c + (- b)))))) + ((|.(c + (- b)).| * (sin ((- (Arg (a + (- b)))) + (Arg (c + (- b)))))) * <i>) is complex set
(0c,(- (Arg (a + (- b))))) is complex Element of COMPLEX
|.0c.| is complex real ext-real Element of REAL
Arg 0c is complex real ext-real Element of REAL
(- (Arg (a + (- b)))) + (Arg 0c) is complex real ext-real Element of REAL
cos ((- (Arg (a + (- b)))) + (Arg 0c)) is complex real ext-real Element of REAL
|.0c.| * (cos ((- (Arg (a + (- b)))) + (Arg 0c))) is complex real ext-real Element of REAL
sin ((- (Arg (a + (- b)))) + (Arg 0c)) is complex real ext-real Element of REAL
|.0c.| * (sin ((- (Arg (a + (- b)))) + (Arg 0c))) is complex real ext-real Element of REAL
(|.0c.| * (sin ((- (Arg (a + (- b)))) + (Arg 0c)))) * <i> is complex set
(|.0c.| * (cos ((- (Arg (a + (- b)))) + (Arg 0c)))) + ((|.0c.| * (sin ((- (Arg (a + (- b)))) + (Arg 0c)))) * <i>) is complex set
b + (- b) is complex Element of COMPLEX
((b + (- b)),(c + (- b)),(a + (- b))) is complex real ext-real set
(0c,((c + (- b)),(- (Arg (a + (- b))))),((a + (- b)),(- (Arg (a + (- b)))))) is complex real ext-real set
((a + (- b)),0c,(c + (- b))) is complex real ext-real set
((a + (- b)),(b + (- b)),(c + (- b))) is complex real ext-real set
a - b is complex Element of COMPLEX
a + (- b) is complex set
(((a + (- b)),(- (Arg (a + (- b))))),0c,((c + (- b)),(- (Arg (a + (- b)))))) is complex real ext-real set
Im ((a + (- b)),(- (Arg (a + (- b))))) is complex real ext-real Element of REAL
Re ((a + (- b)),(- (Arg (a + (- b))))) is complex real ext-real Element of REAL
Arg ((a + (- b)),(- (Arg (a + (- b))))) is complex real ext-real Element of REAL
((c + (- b)),(- (Arg (a + (- b))))) - 0c is complex Element of COMPLEX
- 0c is complex set
((c + (- b)),(- (Arg (a + (- b))))) + (- 0c) is complex set
Arg (((c + (- b)),(- (Arg (a + (- b))))) - 0c) is complex real ext-real Element of REAL
((a + (- b)),(- (Arg (a + (- b))))) - 0c is complex Element of COMPLEX
((a + (- b)),(- (Arg (a + (- b))))) + (- 0c) is complex set
Arg (((a + (- b)),(- (Arg (a + (- b))))) - 0c) is complex real ext-real Element of REAL
(Arg (((c + (- b)),(- (Arg (a + (- b))))) - 0c)) - (Arg (((a + (- b)),(- (Arg (a + (- b))))) - 0c)) is complex real ext-real Element of REAL
- (Arg (((a + (- b)),(- (Arg (a + (- b))))) - 0c)) is complex real ext-real set
(Arg (((c + (- b)),(- (Arg (a + (- b))))) - 0c)) + (- (Arg (((a + (- b)),(- (Arg (a + (- b))))) - 0c))) is complex real ext-real set
Arg ((c + (- b)),(- (Arg (a + (- b))))) is complex real ext-real Element of REAL
((c + (- b)),(a + (- b)),(b + (- b))) is complex real ext-real set
(((c + (- b)),(- (Arg (a + (- b))))),((a + (- b)),(- (Arg (a + (- b))))),0c) is complex real ext-real set
5 is non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() Element of NAT
5 * PI is complex real ext-real Element of REAL
a is complex Element of COMPLEX
b is complex Element of COMPLEX
c is complex Element of COMPLEX
(a,b,c) is complex real ext-real set
(b,c,a) is complex real ext-real set
(a,b,c) + (b,c,a) is complex real ext-real set
(c,a,b) is complex real ext-real set
((a,b,c) + (b,c,a)) + (c,a,b) is complex real ext-real set
(c,b,a) is complex real ext-real set
(a,b,c) + (c,b,a) is complex real ext-real set
PI + PI is complex real ext-real Element of REAL
(a,b,c) + (c,b,a) is complex real ext-real set
(2 * PI) + 0 is complex real ext-real Element of REAL
(b,a,c) is complex real ext-real set
(c,a,b) + (b,a,c) is complex real ext-real set
(a,c,b) is complex real ext-real set
(b,c,a) + (a,c,b) is complex real ext-real set
(2 * PI) + (2 * PI) is complex real ext-real Element of REAL
((2 * PI) + (2 * PI)) + (2 * PI) is complex real ext-real Element of REAL
(c,b,a) + (b,a,c) is complex real ext-real set
((c,b,a) + (b,a,c)) + (a,c,b) is complex real ext-real set
(((2 * PI) + (2 * PI)) + (2 * PI)) - (((c,b,a) + (b,a,c)) + (a,c,b)) is complex real ext-real Element of REAL
- (((c,b,a) + (b,a,c)) + (a,c,b)) is complex real ext-real set
(((2 * PI) + (2 * PI)) + (2 * PI)) + (- (((c,b,a) + (b,a,c)) + (a,c,b))) is complex real ext-real set
((2 * PI) + (2 * PI)) + PI is complex real ext-real Element of REAL
(((2 * PI) + (2 * PI)) + PI) + PI is complex real ext-real Element of REAL
((((2 * PI) + (2 * PI)) + PI) + PI) - PI is complex real ext-real Element of REAL
- PI is complex real ext-real set
((((2 * PI) + (2 * PI)) + PI) + PI) + (- PI) is complex real ext-real set
(2 * PI) + PI is complex real ext-real Element of REAL
((2 * PI) + PI) + (2 * PI) is complex real ext-real Element of REAL
a is complex Element of COMPLEX
Im a is complex real ext-real Element of REAL
Re a is complex real ext-real Element of REAL
b is complex Element of COMPLEX
Arg b is complex real ext-real Element of REAL
(a,0,b) is complex real ext-real set
(0,b,a) is complex real ext-real set
(a,0,b) + (0,b,a) is complex real ext-real set
(b,a,0) is complex real ext-real set
((a,0,b) + (0,b,a)) + (b,a,0) is complex real ext-real set
a - b is complex Element of COMPLEX
- b is complex set
a + (- b) is complex set
Im (a - b) is complex real ext-real Element of REAL
Im b is complex real ext-real Element of REAL
(Im a) - (Im b) is complex real ext-real Element of REAL
- (Im b) is complex real ext-real set
(Im a) + (- (Im b)) is complex real ext-real set
- (Im b) is complex real ext-real Element of REAL
Re b is complex real ext-real Element of REAL
(Re b) + 0 is complex real ext-real Element of REAL
(Re a) - (Re b) is complex real ext-real Element of REAL
- (Re b) is complex real ext-real set
(Re a) + (- (Re b)) is complex real ext-real set
Re (a - b) is complex real ext-real Element of REAL
0 * <i> is complex set
(Re a) + (0 * <i>) is complex set
Arg a is complex real ext-real Element of REAL
b - 0c is complex Element of COMPLEX
- 0c is complex set
b + (- 0c) is complex set
Arg (b - 0c) is complex real ext-real Element of REAL
a - 0c is complex Element of COMPLEX
a + (- 0c) is complex set
Arg (a - 0c) is complex real ext-real Element of REAL
(Arg (b - 0c)) - (Arg (a - 0c)) is complex real ext-real Element of REAL
- (Arg (a - 0c)) is complex real ext-real set
(Arg (b - 0c)) + (- (Arg (a - 0c))) is complex real ext-real set
- ((Re a) - (Re b)) is complex real ext-real Element of REAL
- (- ((Re a) - (Re b))) is complex real ext-real Element of REAL
(Re b) - (Re a) is complex real ext-real Element of REAL
- (Re a) is complex real ext-real set
(Re b) + (- (Re a)) is complex real ext-real set
b - a is complex Element of COMPLEX
- a is complex set
b + (- a) is complex set
Re (b - a) is complex real ext-real Element of REAL
Im (b - a) is complex real ext-real Element of REAL
(Im b) - (Im a) is complex real ext-real Element of REAL
- (Im a) is complex real ext-real set
(Im b) + (- (Im a)) is complex real ext-real set
Arg (b - a) is complex real ext-real Element of REAL
- (Arg (b - a)) is complex real ext-real Element of REAL
- PI is complex real ext-real Element of REAL
- b is complex Element of COMPLEX
Arg (- b) is complex real ext-real Element of REAL
(Arg b) - PI is complex real ext-real Element of REAL
- PI is complex real ext-real set
(Arg b) + (- PI) is complex real ext-real set
Arg (a - b) is complex real ext-real Element of REAL
- a is complex Element of COMPLEX
Arg (- a) is complex real ext-real Element of REAL
(Arg a) + PI is complex real ext-real Element of REAL
(b,a,0c) is complex real ext-real set
0c - a is complex Element of COMPLEX
0c + (- a) is complex set
Arg (0c - a) is complex real ext-real Element of REAL
(Arg (0c - a)) - (Arg (b - a)) is complex real ext-real Element of REAL
- (Arg (b - a)) is complex real ext-real set
(Arg (0c - a)) + (- (Arg (b - a))) is complex real ext-real set
(Arg a) - (Arg (- a)) is complex real ext-real Element of REAL
- (Arg (- a)) is complex real ext-real set
(Arg a) + (- (Arg (- a))) is complex real ext-real set
(Arg a) - ((Arg a) + PI) is complex real ext-real Element of REAL
- ((Arg a) + PI) is complex real ext-real set
(Arg a) + (- ((Arg a) + PI)) is complex real ext-real set
0c - b is complex Element of COMPLEX
0c + (- b) is complex set
Arg (0c - b) is complex real ext-real Element of REAL
(Arg (a - b)) - (Arg (0c - b)) is complex real ext-real Element of REAL
- (Arg (0c - b)) is complex real ext-real set
(Arg (a - b)) + (- (Arg (0c - b))) is complex real ext-real set
(0c,b,a) is complex real ext-real set
(Arg (a - b)) - (Arg (- b)) is complex real ext-real Element of REAL
- (Arg (- b)) is complex real ext-real set
(Arg (a - b)) + (- (Arg (- b))) is complex real ext-real set
(Arg b) - (Arg a) is complex real ext-real Element of REAL
- (Arg a) is complex real ext-real set
(Arg b) + (- (Arg a)) is complex real ext-real set
((Arg b) - (Arg a)) + ((Arg (a - b)) - (Arg (- b))) is complex real ext-real Element of REAL
0 - a is complex set
0 + (- a) is complex set
Arg (0 - a) is complex real ext-real Element of REAL
(Arg (0 - a)) - (Arg (b - a)) is complex real ext-real Element of REAL
(Arg (0 - a)) + (- (Arg (b - a))) is complex real ext-real set
(((Arg b) - (Arg a)) + ((Arg (a - b)) - (Arg (- b)))) + ((Arg (0 - a)) - (Arg (b - a))) is complex real ext-real Element of REAL
(Arg b) - (Arg (- b)) is complex real ext-real Element of REAL
(Arg b) + (- (Arg (- b))) is complex real ext-real set
((Arg b) - (Arg (- b))) - (Arg a) is complex real ext-real Element of REAL
((Arg b) - (Arg (- b))) + (- (Arg a)) is complex real ext-real set
(((Arg b) - (Arg (- b))) - (Arg a)) + (Arg (a - b)) is complex real ext-real Element of REAL
(Arg (- a)) - (Arg (b - a)) is complex real ext-real Element of REAL
(Arg (- a)) + (- (Arg (b - a))) is complex real ext-real set
((((Arg b) - (Arg (- b))) - (Arg a)) + (Arg (a - b))) + ((Arg (- a)) - (Arg (b - a))) is complex real ext-real Element of REAL
(Arg (a - b)) + PI is complex real ext-real Element of REAL
((Arg (a - b)) + PI) - (Arg b) is complex real ext-real Element of REAL
- (Arg b) is complex real ext-real set
((Arg (a - b)) + PI) + (- (Arg b)) is complex real ext-real set
(a,0c,b) is complex real ext-real set
a is complex Element of COMPLEX
b is complex Element of COMPLEX
c is complex Element of COMPLEX
(a,b,c) is complex real ext-real set
(b,c,a) is complex real ext-real set
(c,a,b) is complex real ext-real set
c - b is complex Element of COMPLEX
- b is complex set
c + (- b) is complex set
- b is complex Element of COMPLEX
a + (- b) is complex Element of COMPLEX
Arg (a + (- b)) is complex real ext-real Element of REAL
- (Arg (a + (- b))) is complex real ext-real Element of REAL
((a + (- b)),(- (Arg (a + (- b))))) is complex Element of COMPLEX
|.(a + (- b)).| is complex real ext-real Element of REAL
(- (Arg (a + (- b)))) + (Arg (a + (- b))) is complex real ext-real Element of REAL
cos ((- (Arg (a + (- b)))) + (Arg (a + (- b)))) is complex real ext-real Element of REAL
|.(a + (- b)).| * (cos ((- (Arg (a + (- b)))) + (Arg (a + (- b))))) is complex real ext-real Element of REAL
sin ((- (Arg (a + (- b)))) + (Arg (a + (- b)))) is complex real ext-real Element of REAL
|.(a + (- b)).| * (sin ((- (Arg (a + (- b)))) + (Arg (a + (- b))))) is complex real ext-real Element of REAL
(|.(a + (- b)).| * (sin ((- (Arg (a + (- b)))) + (Arg (a + (- b)))))) * <i> is complex set
(|.(a + (- b)).| * (cos ((- (Arg (a + (- b)))) + (Arg (a + (- b)))))) + ((|.(a + (- b)).| * (sin ((- (Arg (a + (- b)))) + (Arg (a + (- b)))))) * <i>) is complex set
c + (- b) is complex Element of COMPLEX
((c + (- b)),(- (Arg (a + (- b))))) is complex Element of COMPLEX
|.(c + (- b)).| is complex real ext-real Element of REAL
Arg (c + (- b)) is complex real ext-real Element of REAL
(- (Arg (a + (- b)))) + (Arg (c + (- b))) is complex real ext-real Element of REAL
cos ((- (Arg (a + (- b)))) + (Arg (c + (- b)))) is complex real ext-real Element of REAL
|.(c + (- b)).| * (cos ((- (Arg (a + (- b)))) + (Arg (c + (- b))))) is complex real ext-real Element of REAL
sin ((- (Arg (a + (- b)))) + (Arg (c + (- b)))) is complex real ext-real Element of REAL
|.(c + (- b)).| * (sin ((- (Arg (a + (- b)))) + (Arg (c + (- b))))) is complex real ext-real Element of REAL
(|.(c + (- b)).| * (sin ((- (Arg (a + (- b)))) + (Arg (c + (- b)))))) * <i> is complex set
(|.(c + (- b)).| * (cos ((- (Arg (a + (- b)))) + (Arg (c + (- b)))))) + ((|.(c + (- b)).| * (sin ((- (Arg (a + (- b)))) + (Arg (c + (- b)))))) * <i>) is complex set
(0c,(- (Arg (a + (- b))))) is complex Element of COMPLEX
|.0c.| is complex real ext-real Element of REAL
Arg 0c is complex real ext-real Element of REAL
(- (Arg (a + (- b)))) + (Arg 0c) is complex real ext-real Element of REAL
cos ((- (Arg (a + (- b)))) + (Arg 0c)) is complex real ext-real Element of REAL
|.0c.| * (cos ((- (Arg (a + (- b)))) + (Arg 0c))) is complex real ext-real Element of REAL
sin ((- (Arg (a + (- b)))) + (Arg 0c)) is complex real ext-real Element of REAL
|.0c.| * (sin ((- (Arg (a + (- b)))) + (Arg 0c))) is complex real ext-real Element of REAL
(|.0c.| * (sin ((- (Arg (a + (- b)))) + (Arg 0c)))) * <i> is complex set
(|.0c.| * (cos ((- (Arg (a + (- b)))) + (Arg 0c)))) + ((|.0c.| * (sin ((- (Arg (a + (- b)))) + (Arg 0c)))) * <i>) is complex set
((a + (- b)),0c,(c + (- b))) is complex real ext-real set
b + (- b) is complex Element of COMPLEX
((a + (- b)),(b + (- b)),(c + (- b))) is complex real ext-real set
a - b is complex Element of COMPLEX
a + (- b) is complex set
(((a + (- b)),(- (Arg (a + (- b))))),0c,((c + (- b)),(- (Arg (a + (- b)))))) is complex real ext-real set
Im ((a + (- b)),(- (Arg (a + (- b))))) is complex real ext-real Element of REAL
Re ((a + (- b)),(- (Arg (a + (- b))))) is complex real ext-real Element of REAL
Arg ((a + (- b)),(- (Arg (a + (- b))))) is complex real ext-real Element of REAL
((c + (- b)),(- (Arg (a + (- b))))) - 0c is complex Element of COMPLEX
- 0c is complex set
((c + (- b)),(- (Arg (a + (- b))))) + (- 0c) is complex set
Arg (((c + (- b)),(- (Arg (a + (- b))))) - 0c) is complex real ext-real Element of REAL
((a + (- b)),(- (Arg (a + (- b))))) - 0c is complex Element of COMPLEX
((a + (- b)),(- (Arg (a + (- b))))) + (- 0c) is complex set
Arg (((a + (- b)),(- (Arg (a + (- b))))) - 0c) is complex real ext-real Element of REAL
(Arg (((c + (- b)),(- (Arg (a + (- b))))) - 0c)) - (Arg (((a + (- b)),(- (Arg (a + (- b))))) - 0c)) is complex real ext-real Element of REAL
- (Arg (((a + (- b)),(- (Arg (a + (- b))))) - 0c)) is complex real ext-real set
(Arg (((c + (- b)),(- (Arg (a + (- b))))) - 0c)) + (- (Arg (((a + (- b)),(- (Arg (a + (- b))))) - 0c))) is complex real ext-real set
Arg ((c + (- b)),(- (Arg (a + (- b))))) is complex real ext-real Element of REAL
((b + (- b)),(c + (- b)),(a + (- b))) is complex real ext-real set
(0c,((c + (- b)),(- (Arg (a + (- b))))),((a + (- b)),(- (Arg (a + (- b)))))) is complex real ext-real set
((c + (- b)),(a + (- b)),(b + (- b))) is complex real ext-real set
(((c + (- b)),(- (Arg (a + (- b))))),((a + (- b)),(- (Arg (a + (- b))))),0c) is complex real ext-real set
a is complex Element of COMPLEX
b is complex Element of COMPLEX
c is complex Element of COMPLEX
(a,b,c) is complex real ext-real set
(b,c,a) is complex real ext-real set
(c,a,b) is complex real ext-real set
a is complex Element of COMPLEX
b is complex Element of COMPLEX
c is complex Element of COMPLEX
(a,b,c) is complex real ext-real set
(b,c,a) is complex real ext-real set
(a,b,c) + (b,c,a) is complex real ext-real set
(c,a,b) is complex real ext-real set
((a,b,c) + (b,c,a)) + (c,a,b) is complex real ext-real set
(a,c,a) is complex real ext-real set
(a,a,c) is complex real ext-real set
(c,a,a) is complex real ext-real set
(a,b,a) is complex real ext-real set
(a,a,b) is complex real ext-real set
(b,a,a) is complex real ext-real set
(b,a,b) is complex real ext-real set
(a,b,b) is complex real ext-real set
(b,b,a) is complex real ext-real set
2 + 2 is non zero complex real ext-real positive non negative integer Element of REAL
(2 + 2) * PI is complex real ext-real Element of REAL
(2 * PI) + (2 * PI) is complex real ext-real Element of REAL
(b,c,a) + (c,a,b) is complex real ext-real set