:: COMPTRIG semantic presentation

REAL is non empty V58() V70() V71() V72() V76() set
NAT is V70() V71() V72() V73() V74() V75() V76() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V58() V70() V76() set
K20(REAL,REAL) is V46() V47() V48() set
K19(K20(REAL,REAL)) is set
omega is V70() V71() V72() V73() V74() V75() V76() set
K19(omega) is set
K19(NAT) is set
RAT is non empty V58() V70() V71() V72() V73() V76() set
INT is non empty V58() V70() V71() V72() V73() V74() V76() set
K20(NAT,REAL) is V46() V47() V48() set
K19(K20(NAT,REAL)) is set
K20(NAT,COMPLEX) is V46() set
K19(K20(NAT,COMPLEX)) is set
K20(COMPLEX,COMPLEX) is V46() set
K19(K20(COMPLEX,COMPLEX)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is V46() set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(K20(REAL,REAL),REAL) is V46() V47() V48() set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is RAT -valued V46() V47() V48() set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is RAT -valued V46() V47() V48() set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is RAT -valued INT -valued V46() V47() V48() set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is RAT -valued INT -valued V46() V47() V48() set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is RAT -valued INT -valued V46() V47() V48() V49() set
K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued V46() V47() V48() V49() set
K19(K20(K20(NAT,NAT),NAT)) is set
K416() is set
1 is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
0 is Function-like functional empty ordinal natural complex real ext-real non positive non negative V56() V69() V70() V71() V72() V73() V74() V75() V76() Element of NAT
<i> is complex Element of COMPLEX
|.0.| is complex real ext-real Element of REAL
Re 0 is complex real ext-real Element of REAL
(Re 0) ^2 is complex real ext-real Element of REAL
(Re 0) * (Re 0) is complex real ext-real set
Im 0 is complex real ext-real Element of REAL
(Im 0) ^2 is complex real ext-real Element of REAL
(Im 0) * (Im 0) is complex real ext-real set
((Re 0) ^2) + ((Im 0) ^2) is complex real ext-real Element of REAL
sqrt (((Re 0) ^2) + ((Im 0) ^2)) is complex real ext-real Element of REAL
sin is Relation-like REAL -defined REAL -valued Function-like V30( REAL , REAL ) continuous V46() V47() V48() Element of K19(K20(REAL,REAL))
cos is Relation-like REAL -defined REAL -valued Function-like V30( REAL , REAL ) continuous V46() V47() V48() Element of K19(K20(REAL,REAL))
K496(REAL,sin) is V70() V71() V72() Element of K19(REAL)
K496(REAL,cos) is V70() V71() V72() 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 set
tan is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
4 is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
].0,4.[ is V70() V71() V72() Element of K19(REAL)
PI is complex real ext-real Element of REAL
2 is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
PI / 2 is complex real ext-real Element of REAL
2 " is non empty 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 empty complex real ext-real non positive negative 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
].0,(PI / 2).[ is V70() V71() V72() Element of K19(REAL)
- 1 is non empty complex real ext-real non positive negative set
z is non empty ordinal natural complex real ext-real positive non negative set
z is non empty ordinal natural complex real ext-real positive non negative set
x is ordinal natural complex real ext-real non negative set
x + 1 is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
0 + 1 is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
v is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
t is non empty ordinal natural complex real ext-real positive non negative set
t is ordinal natural complex real ext-real non negative set
t + 1 is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
t is ordinal natural complex real ext-real non negative set
t + 1 is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
x is ordinal natural complex real ext-real non negative set
x + 1 is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
0 + 1 is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
z is complex set
|.z.| is complex real ext-real Element of REAL
Re z is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
Im z is complex real ext-real Element of REAL
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) + ((Im z) ^2) is complex real ext-real Element of REAL
sqrt (((Re z) ^2) + ((Im z) ^2)) is complex real ext-real Element of REAL
- |.z.| is complex real ext-real Element of REAL
((Re z) ^2) + 0 is complex real ext-real Element of REAL
sqrt ((Re z) ^2) is complex real ext-real Element of REAL
- (sqrt ((Re z) ^2)) is complex real ext-real Element of REAL
abs (Re z) is complex real ext-real Element of REAL
Re (Re z) is complex real ext-real Element of REAL
(Re (Re z)) ^2 is complex real ext-real Element of REAL
(Re (Re z)) * (Re (Re z)) is complex real ext-real set
Im (Re z) is complex real ext-real Element of REAL
(Im (Re z)) ^2 is complex real ext-real Element of REAL
(Im (Re z)) * (Im (Re z)) is complex real ext-real set
((Re (Re z)) ^2) + ((Im (Re z)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (Re z)) ^2) + ((Im (Re z)) ^2)) is complex real ext-real Element of REAL
- (abs (Re z)) is complex real ext-real Element of REAL
z is complex set
|.z.| is complex real ext-real Element of REAL
Re z is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
Im z is complex real ext-real Element of REAL
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) + ((Im z) ^2) is complex real ext-real Element of REAL
sqrt (((Re z) ^2) + ((Im z) ^2)) is complex real ext-real Element of REAL
- |.z.| is complex real ext-real Element of REAL
((Im z) ^2) + 0 is complex real ext-real Element of REAL
sqrt ((Im z) ^2) is complex real ext-real Element of REAL
- (sqrt ((Im z) ^2)) is complex real ext-real Element of REAL
abs (Im z) is complex real ext-real Element of REAL
Re (Im z) is complex real ext-real Element of REAL
(Re (Im z)) ^2 is complex real ext-real Element of REAL
(Re (Im z)) * (Re (Im z)) is complex real ext-real set
Im (Im z) is complex real ext-real Element of REAL
(Im (Im z)) ^2 is complex real ext-real Element of REAL
(Im (Im z)) * (Im (Im z)) is complex real ext-real set
((Re (Im z)) ^2) + ((Im (Im z)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (Im z)) ^2) + ((Im (Im z)) ^2)) is complex real ext-real Element of REAL
- (abs (Im z)) is complex real ext-real Element of REAL
z is complex set
|.z.| is complex real ext-real Element of REAL
Re z is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
Im z is complex real ext-real Element of REAL
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) + ((Im z) ^2) is complex real ext-real Element of REAL
sqrt (((Re z) ^2) + ((Im z) ^2)) is complex real ext-real Element of REAL
|.z.| ^2 is complex real ext-real Element of REAL
|.z.| * |.z.| is complex real ext-real set
z * z is complex set
|.(z * z).| is complex real ext-real Element of REAL
Re (z * z) is complex real ext-real Element of REAL
(Re (z * z)) ^2 is complex real ext-real Element of REAL
(Re (z * z)) * (Re (z * z)) is complex real ext-real set
Im (z * z) is complex real ext-real Element of REAL
(Im (z * z)) ^2 is complex real ext-real Element of REAL
(Im (z * z)) * (Im (z * z)) is complex real ext-real set
((Re (z * z)) ^2) + ((Im (z * z)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (z * z)) ^2) + ((Im (z * z)) ^2)) is complex real ext-real Element of REAL
z is complex real ext-real set
x is ordinal natural complex real ext-real non negative set
x -root z is complex real ext-real set
(x -root z) |^ x is complex real ext-real set
0 + 1 is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
(PI / 2) + (PI / 2) is complex real ext-real non negative Element of REAL
0 + (PI / 2) is complex real ext-real non negative Element of REAL
PI + PI is complex real ext-real non negative Element of REAL
0 + PI is complex real ext-real non negative Element of REAL
3 is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
3 / 2 is non empty complex real ext-real positive non negative Element of REAL
3 * (2 ") is non empty complex real ext-real positive non negative set
(3 / 2) * PI is complex real ext-real non negative Element of REAL
((3 / 2) * PI) + (PI / 2) is complex real ext-real non negative Element of REAL
- (PI / 2) is complex real ext-real non positive Element of REAL
t is complex real ext-real set
z is complex real ext-real set
v is complex real ext-real set
].z,v.[ is V70() V71() V72() Element of K19(REAL)
x is complex real ext-real set
].z,x.[ is V70() V71() V72() Element of K19(REAL)
].x,v.[ is V70() V71() V72() Element of K19(REAL)
].0,PI.[ is V70() V71() V72() Element of K19(REAL)
z is complex real ext-real set
sin . z is complex real ext-real Element of REAL
- z is complex real ext-real set
(- z) + (PI / 2) is complex real ext-real Element of REAL
(- (PI / 2)) + (PI / 2) is complex real ext-real Element of REAL
(PI / 2) - z is complex real ext-real Element of REAL
(PI / 2) + (- z) is complex real ext-real set
cos . ((PI / 2) - z) is complex real ext-real Element of REAL
].(PI / 2),PI.[ is V70() V71() V72() Element of K19(REAL)
PI - (PI / 2) is complex real ext-real Element of REAL
- (PI / 2) is complex real ext-real non positive set
PI + (- (PI / 2)) is complex real ext-real set
z - (PI / 2) is complex real ext-real Element of REAL
z + (- (PI / 2)) is complex real ext-real set
(PI / 2) - (PI / 2) is complex real ext-real Element of REAL
(PI / 2) + (- (PI / 2)) is complex real ext-real set
(PI / 2) - z is complex real ext-real Element of REAL
- z is complex real ext-real set
(PI / 2) + (- z) is complex real ext-real set
- ((PI / 2) - z) is complex real ext-real Element of REAL
cos . (- ((PI / 2) - z)) is complex real ext-real Element of REAL
cos . ((PI / 2) - z) is complex real ext-real Element of REAL
].(PI / 2),PI.[ is V70() V71() V72() Element of K19(REAL)
[.0,PI.] is V70() V71() V72() Element of K19(REAL)
z is complex real ext-real set
sin . z is complex real ext-real Element of REAL
].PI,(2 * PI).[ is V70() V71() V72() Element of K19(REAL)
z is complex real ext-real set
sin . z is complex real ext-real Element of REAL
z - PI is complex real ext-real Element of REAL
- PI is complex real ext-real non positive set
z + (- PI) is complex real ext-real set
sin . (z - PI) is complex real ext-real Element of REAL
PI - z is complex real ext-real Element of REAL
- z is complex real ext-real set
PI + (- z) is complex real ext-real set
- (PI - z) is complex real ext-real Element of REAL
sin . (- (PI - z)) is complex real ext-real Element of REAL
PI + (- z) is complex real ext-real Element of REAL
sin . (PI + (- z)) is complex real ext-real Element of REAL
- (sin . (PI + (- z))) is complex real ext-real Element of REAL
sin . (- z) is complex real ext-real Element of REAL
- (sin . (- z)) is complex real ext-real Element of REAL
- (- (sin . (- z))) is complex real ext-real Element of REAL
- (sin . z) is complex real ext-real Element of REAL
(2 * PI) - PI is complex real ext-real Element of REAL
(2 * PI) + (- PI) is complex real ext-real set
PI - PI is complex real ext-real Element of REAL
PI + (- PI) is complex real ext-real set
[.PI,(2 * PI).] is V70() V71() V72() Element of K19(REAL)
z is complex real ext-real set
sin . z is complex real ext-real Element of REAL
].(- (PI / 2)),(PI / 2).[ is V70() V71() V72() Element of K19(REAL)
z is complex real ext-real set
cos . z is complex real ext-real Element of REAL
z + (PI / 2) is complex real ext-real Element of REAL
sin . (z + (PI / 2)) is complex real ext-real Element of REAL
(- (PI / 2)) + (PI / 2) is complex real ext-real Element of REAL
[.(- (PI / 2)),(PI / 2).] is V70() V71() V72() Element of K19(REAL)
z is complex real ext-real set
cos . z is complex real ext-real Element of REAL
].(PI / 2),((3 / 2) * PI).[ is V70() V71() V72() Element of K19(REAL)
z is complex real ext-real set
cos . z is complex real ext-real Element of REAL
z + (PI / 2) is complex real ext-real Element of REAL
sin . (z + (PI / 2)) is complex real ext-real Element of REAL
[.(PI / 2),((3 / 2) * PI).] is V70() V71() V72() Element of K19(REAL)
z is complex real ext-real set
cos . z is complex real ext-real Element of REAL
].((3 / 2) * PI),(2 * PI).[ is V70() V71() V72() Element of K19(REAL)
z is complex real ext-real set
cos . z is complex real ext-real Element of REAL
z - PI is complex real ext-real Element of REAL
- PI is complex real ext-real non positive set
z + (- PI) is complex real ext-real set
cos . (z - PI) is complex real ext-real Element of REAL
PI - z is complex real ext-real Element of REAL
- z is complex real ext-real set
PI + (- z) is complex real ext-real set
- (PI - z) is complex real ext-real Element of REAL
cos . (- (PI - z)) is complex real ext-real Element of REAL
PI + (- z) is complex real ext-real Element of REAL
cos . (PI + (- z)) is complex real ext-real Element of REAL
cos . (- z) is complex real ext-real Element of REAL
- (cos . (- z)) is complex real ext-real Element of REAL
- (cos . z) is complex real ext-real Element of REAL
(2 * PI) - PI is complex real ext-real Element of REAL
(2 * PI) + (- PI) is complex real ext-real set
((3 / 2) * PI) - PI is complex real ext-real Element of REAL
((3 / 2) * PI) + (- PI) is complex real ext-real set
[.((3 / 2) * PI),(2 * PI).] is V70() V71() V72() Element of K19(REAL)
z is complex real ext-real set
cos . z is complex real ext-real Element of REAL
z is complex real ext-real set
sin z is complex real ext-real set
sin . z is complex real ext-real Element of REAL
z is complex real ext-real set
cos z is complex real ext-real set
cos . z is complex real ext-real Element of REAL
sin | ].(- (PI / 2)),(PI / 2).[ is Relation-like REAL -defined REAL -valued Function-like continuous V46() V47() V48() Element of K19(K20(REAL,REAL))
z is complex real ext-real Element of REAL
diff (sin,z) is complex real ext-real Element of REAL
cos . z is complex real ext-real Element of REAL
sin | ].(PI / 2),((3 / 2) * PI).[ is Relation-like REAL -defined REAL -valued Function-like continuous V46() V47() V48() Element of K19(K20(REAL,REAL))
z is complex real ext-real Element of REAL
diff (sin,z) is complex real ext-real Element of REAL
cos . z is complex real ext-real Element of REAL
cos | ].0,PI.[ is Relation-like REAL -defined REAL -valued Function-like continuous V46() V47() V48() Element of K19(K20(REAL,REAL))
z is complex real ext-real Element of REAL
diff (cos,z) is complex real ext-real Element of REAL
sin . z is complex real ext-real Element of REAL
0 - (sin . z) is complex real ext-real Element of REAL
- (sin . z) is complex real ext-real set
0 + (- (sin . z)) is complex real ext-real set
cos | ].PI,(2 * PI).[ is Relation-like REAL -defined REAL -valued Function-like continuous V46() V47() V48() Element of K19(K20(REAL,REAL))
z is complex real ext-real Element of REAL
diff (cos,z) is complex real ext-real Element of REAL
sin . z is complex real ext-real Element of REAL
0 - (sin . z) is complex real ext-real Element of REAL
- (sin . z) is complex real ext-real set
0 + (- (sin . z)) is complex real ext-real set
sin | [.(- (PI / 2)),(PI / 2).] is Relation-like REAL -defined REAL -valued Function-like continuous V46() V47() V48() Element of K19(K20(REAL,REAL))
z is complex real ext-real Element of REAL
dom sin is set
[.(- (PI / 2)),(PI / 2).] /\ (dom sin) is V70() V71() V72() Element of K19(REAL)
x is complex real ext-real Element of REAL
z + x is complex real ext-real Element of REAL
(z + x) / 2 is complex real ext-real Element of REAL
(z + x) * (2 ") is complex real ext-real set
sin ((z + x) / 2) is complex real ext-real Element of REAL
abs (sin ((z + x) / 2)) is complex real ext-real Element of REAL
Re (sin ((z + x) / 2)) is complex real ext-real Element of REAL
(Re (sin ((z + x) / 2))) ^2 is complex real ext-real Element of REAL
(Re (sin ((z + x) / 2))) * (Re (sin ((z + x) / 2))) is complex real ext-real set
Im (sin ((z + x) / 2)) is complex real ext-real Element of REAL
(Im (sin ((z + x) / 2))) ^2 is complex real ext-real Element of REAL
(Im (sin ((z + x) / 2))) * (Im (sin ((z + x) / 2))) is complex real ext-real set
((Re (sin ((z + x) / 2))) ^2) + ((Im (sin ((z + x) / 2))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (sin ((z + x) / 2))) ^2) + ((Im (sin ((z + x) / 2))) ^2)) is complex real ext-real Element of REAL
sin . ((z + x) / 2) is complex real ext-real Element of REAL
abs (sin . ((z + x) / 2)) is complex real ext-real Element of REAL
Re (sin . ((z + x) / 2)) is complex real ext-real Element of REAL
(Re (sin . ((z + x) / 2))) ^2 is complex real ext-real Element of REAL
(Re (sin . ((z + x) / 2))) * (Re (sin . ((z + x) / 2))) is complex real ext-real set
Im (sin . ((z + x) / 2)) is complex real ext-real Element of REAL
(Im (sin . ((z + x) / 2))) ^2 is complex real ext-real Element of REAL
(Im (sin . ((z + x) / 2))) * (Im (sin . ((z + x) / 2))) is complex real ext-real set
((Re (sin . ((z + x) / 2))) ^2) + ((Im (sin . ((z + x) / 2))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (sin . ((z + x) / 2))) ^2) + ((Im (sin . ((z + x) / 2))) ^2)) is complex real ext-real Element of REAL
].(- (PI / 2)),(PI / 2).[ /\ (dom sin) is V70() V71() V72() Element of K19(REAL)
sin x is complex real ext-real Element of REAL
abs (sin x) is complex real ext-real Element of REAL
Re (sin x) is complex real ext-real Element of REAL
(Re (sin x)) ^2 is complex real ext-real Element of REAL
(Re (sin x)) * (Re (sin x)) is complex real ext-real set
Im (sin x) is complex real ext-real Element of REAL
(Im (sin x)) ^2 is complex real ext-real Element of REAL
(Im (sin x)) * (Im (sin x)) is complex real ext-real set
((Re (sin x)) ^2) + ((Im (sin x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (sin x)) ^2) + ((Im (sin x)) ^2)) is complex real ext-real Element of REAL
sin . x is complex real ext-real Element of REAL
abs (sin . x) is complex real ext-real Element of REAL
Re (sin . x) is complex real ext-real Element of REAL
(Re (sin . x)) ^2 is complex real ext-real Element of REAL
(Re (sin . x)) * (Re (sin . x)) is complex real ext-real set
Im (sin . x) is complex real ext-real Element of REAL
(Im (sin . x)) ^2 is complex real ext-real Element of REAL
(Im (sin . x)) * (Im (sin . x)) is complex real ext-real set
((Re (sin . x)) ^2) + ((Im (sin . x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (sin . x)) ^2) + ((Im (sin . x)) ^2)) is complex real ext-real Element of REAL
sin . z is complex real ext-real Element of REAL
sin . z is complex real ext-real Element of REAL
sin . z is complex real ext-real Element of REAL
sin . z is complex real ext-real Element of REAL
sin . z is complex real ext-real Element of REAL
sin . z is complex real ext-real Element of REAL
sin . z is complex real ext-real Element of REAL
sin . z is complex real ext-real Element of REAL
sin . z is complex real ext-real Element of REAL
sin . z is complex real ext-real Element of REAL
sin | [.(PI / 2),((3 / 2) * PI).] is Relation-like REAL -defined REAL -valued Function-like continuous V46() V47() V48() Element of K19(K20(REAL,REAL))
z is complex real ext-real Element of REAL
dom sin is set
[.(PI / 2),((3 / 2) * PI).] /\ (dom sin) is V70() V71() V72() Element of K19(REAL)
x is complex real ext-real Element of REAL
sin x is complex real ext-real Element of REAL
abs (sin x) is complex real ext-real Element of REAL
Re (sin x) is complex real ext-real Element of REAL
(Re (sin x)) ^2 is complex real ext-real Element of REAL
(Re (sin x)) * (Re (sin x)) is complex real ext-real set
Im (sin x) is complex real ext-real Element of REAL
(Im (sin x)) ^2 is complex real ext-real Element of REAL
(Im (sin x)) * (Im (sin x)) is complex real ext-real set
((Re (sin x)) ^2) + ((Im (sin x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (sin x)) ^2) + ((Im (sin x)) ^2)) is complex real ext-real Element of REAL
sin . x is complex real ext-real Element of REAL
abs (sin . x) is complex real ext-real Element of REAL
Re (sin . x) is complex real ext-real Element of REAL
(Re (sin . x)) ^2 is complex real ext-real Element of REAL
(Re (sin . x)) * (Re (sin . x)) is complex real ext-real set
Im (sin . x) is complex real ext-real Element of REAL
(Im (sin . x)) ^2 is complex real ext-real Element of REAL
(Im (sin . x)) * (Im (sin . x)) is complex real ext-real set
((Re (sin . x)) ^2) + ((Im (sin . x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (sin . x)) ^2) + ((Im (sin . x)) ^2)) is complex real ext-real Element of REAL
sin z is complex real ext-real Element of REAL
abs (sin z) is complex real ext-real Element of REAL
Re (sin z) is complex real ext-real Element of REAL
(Re (sin z)) ^2 is complex real ext-real Element of REAL
(Re (sin z)) * (Re (sin z)) is complex real ext-real set
Im (sin z) is complex real ext-real Element of REAL
(Im (sin z)) ^2 is complex real ext-real Element of REAL
(Im (sin z)) * (Im (sin z)) is complex real ext-real set
((Re (sin z)) ^2) + ((Im (sin z)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (sin z)) ^2) + ((Im (sin z)) ^2)) is complex real ext-real Element of REAL
sin . z is complex real ext-real Element of REAL
abs (sin . z) is complex real ext-real Element of REAL
Re (sin . z) is complex real ext-real Element of REAL
(Re (sin . z)) ^2 is complex real ext-real Element of REAL
(Re (sin . z)) * (Re (sin . z)) is complex real ext-real set
Im (sin . z) is complex real ext-real Element of REAL
(Im (sin . z)) ^2 is complex real ext-real Element of REAL
(Im (sin . z)) * (Im (sin . z)) is complex real ext-real set
((Re (sin . z)) ^2) + ((Im (sin . z)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (sin . z)) ^2) + ((Im (sin . z)) ^2)) is complex real ext-real Element of REAL
z + x is complex real ext-real Element of REAL
(z + x) / 2 is complex real ext-real Element of REAL
(z + x) * (2 ") is complex real ext-real set
sin ((z + x) / 2) is complex real ext-real Element of REAL
abs (sin ((z + x) / 2)) is complex real ext-real Element of REAL
Re (sin ((z + x) / 2)) is complex real ext-real Element of REAL
(Re (sin ((z + x) / 2))) ^2 is complex real ext-real Element of REAL
(Re (sin ((z + x) / 2))) * (Re (sin ((z + x) / 2))) is complex real ext-real set
Im (sin ((z + x) / 2)) is complex real ext-real Element of REAL
(Im (sin ((z + x) / 2))) ^2 is complex real ext-real Element of REAL
(Im (sin ((z + x) / 2))) * (Im (sin ((z + x) / 2))) is complex real ext-real set
((Re (sin ((z + x) / 2))) ^2) + ((Im (sin ((z + x) / 2))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (sin ((z + x) / 2))) ^2) + ((Im (sin ((z + x) / 2))) ^2)) is complex real ext-real Element of REAL
sin . ((z + x) / 2) is complex real ext-real Element of REAL
abs (sin . ((z + x) / 2)) is complex real ext-real Element of REAL
Re (sin . ((z + x) / 2)) is complex real ext-real Element of REAL
(Re (sin . ((z + x) / 2))) ^2 is complex real ext-real Element of REAL
(Re (sin . ((z + x) / 2))) * (Re (sin . ((z + x) / 2))) is complex real ext-real set
Im (sin . ((z + x) / 2)) is complex real ext-real Element of REAL
(Im (sin . ((z + x) / 2))) ^2 is complex real ext-real Element of REAL
(Im (sin . ((z + x) / 2))) * (Im (sin . ((z + x) / 2))) is complex real ext-real set
((Re (sin . ((z + x) / 2))) ^2) + ((Im (sin . ((z + x) / 2))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (sin . ((z + x) / 2))) ^2) + ((Im (sin . ((z + x) / 2))) ^2)) is complex real ext-real Element of REAL
].(PI / 2),((3 / 2) * PI).[ /\ (dom sin) is V70() V71() V72() Element of K19(REAL)
cos | [.0,PI.] is Relation-like REAL -defined REAL -valued Function-like continuous V46() V47() V48() Element of K19(K20(REAL,REAL))
z is complex real ext-real Element of REAL
dom cos is set
[.0,PI.] /\ (dom cos) is V70() V71() V72() Element of K19(REAL)
x is complex real ext-real Element of REAL
cos x is complex real ext-real Element of REAL
abs (cos x) is complex real ext-real Element of REAL
Re (cos x) is complex real ext-real Element of REAL
(Re (cos x)) ^2 is complex real ext-real Element of REAL
(Re (cos x)) * (Re (cos x)) is complex real ext-real set
Im (cos x) is complex real ext-real Element of REAL
(Im (cos x)) ^2 is complex real ext-real Element of REAL
(Im (cos x)) * (Im (cos x)) is complex real ext-real set
((Re (cos x)) ^2) + ((Im (cos x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (cos x)) ^2) + ((Im (cos x)) ^2)) is complex real ext-real Element of REAL
cos . x is complex real ext-real Element of REAL
abs (cos . x) is complex real ext-real Element of REAL
Re (cos . x) is complex real ext-real Element of REAL
(Re (cos . x)) ^2 is complex real ext-real Element of REAL
(Re (cos . x)) * (Re (cos . x)) is complex real ext-real set
Im (cos . x) is complex real ext-real Element of REAL
(Im (cos . x)) ^2 is complex real ext-real Element of REAL
(Im (cos . x)) * (Im (cos . x)) is complex real ext-real set
((Re (cos . x)) ^2) + ((Im (cos . x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (cos . x)) ^2) + ((Im (cos . x)) ^2)) is complex real ext-real Element of REAL
cos z is complex real ext-real Element of REAL
abs (cos z) is complex real ext-real Element of REAL
Re (cos z) is complex real ext-real Element of REAL
(Re (cos z)) ^2 is complex real ext-real Element of REAL
(Re (cos z)) * (Re (cos z)) is complex real ext-real set
Im (cos z) is complex real ext-real Element of REAL
(Im (cos z)) ^2 is complex real ext-real Element of REAL
(Im (cos z)) * (Im (cos z)) is complex real ext-real set
((Re (cos z)) ^2) + ((Im (cos z)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (cos z)) ^2) + ((Im (cos z)) ^2)) is complex real ext-real Element of REAL
cos . z is complex real ext-real Element of REAL
abs (cos . z) is complex real ext-real Element of REAL
Re (cos . z) is complex real ext-real Element of REAL
(Re (cos . z)) ^2 is complex real ext-real Element of REAL
(Re (cos . z)) * (Re (cos . z)) is complex real ext-real set
Im (cos . z) is complex real ext-real Element of REAL
(Im (cos . z)) ^2 is complex real ext-real Element of REAL
(Im (cos . z)) * (Im (cos . z)) is complex real ext-real set
((Re (cos . z)) ^2) + ((Im (cos . z)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (cos . z)) ^2) + ((Im (cos . z)) ^2)) is complex real ext-real Element of REAL
z + x is complex real ext-real Element of REAL
(z + x) / 2 is complex real ext-real Element of REAL
(z + x) * (2 ") is complex real ext-real set
cos ((z + x) / 2) is complex real ext-real Element of REAL
abs (cos ((z + x) / 2)) is complex real ext-real Element of REAL
Re (cos ((z + x) / 2)) is complex real ext-real Element of REAL
(Re (cos ((z + x) / 2))) ^2 is complex real ext-real Element of REAL
(Re (cos ((z + x) / 2))) * (Re (cos ((z + x) / 2))) is complex real ext-real set
Im (cos ((z + x) / 2)) is complex real ext-real Element of REAL
(Im (cos ((z + x) / 2))) ^2 is complex real ext-real Element of REAL
(Im (cos ((z + x) / 2))) * (Im (cos ((z + x) / 2))) is complex real ext-real set
((Re (cos ((z + x) / 2))) ^2) + ((Im (cos ((z + x) / 2))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (cos ((z + x) / 2))) ^2) + ((Im (cos ((z + x) / 2))) ^2)) is complex real ext-real Element of REAL
cos . ((z + x) / 2) is complex real ext-real Element of REAL
abs (cos . ((z + x) / 2)) is complex real ext-real Element of REAL
Re (cos . ((z + x) / 2)) is complex real ext-real Element of REAL
(Re (cos . ((z + x) / 2))) ^2 is complex real ext-real Element of REAL
(Re (cos . ((z + x) / 2))) * (Re (cos . ((z + x) / 2))) is complex real ext-real set
Im (cos . ((z + x) / 2)) is complex real ext-real Element of REAL
(Im (cos . ((z + x) / 2))) ^2 is complex real ext-real Element of REAL
(Im (cos . ((z + x) / 2))) * (Im (cos . ((z + x) / 2))) is complex real ext-real set
((Re (cos . ((z + x) / 2))) ^2) + ((Im (cos . ((z + x) / 2))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (cos . ((z + x) / 2))) ^2) + ((Im (cos . ((z + x) / 2))) ^2)) is complex real ext-real Element of REAL
].0,PI.[ /\ (dom cos) is V70() V71() V72() Element of K19(REAL)
cos | [.PI,(2 * PI).] is Relation-like REAL -defined REAL -valued Function-like continuous V46() V47() V48() Element of K19(K20(REAL,REAL))
z is complex real ext-real Element of REAL
dom cos is set
[.PI,(2 * PI).] /\ (dom cos) is V70() V71() V72() Element of K19(REAL)
x is complex real ext-real Element of REAL
z + x is complex real ext-real Element of REAL
(z + x) / 2 is complex real ext-real Element of REAL
(z + x) * (2 ") is complex real ext-real set
cos ((z + x) / 2) is complex real ext-real Element of REAL
abs (cos ((z + x) / 2)) is complex real ext-real Element of REAL
Re (cos ((z + x) / 2)) is complex real ext-real Element of REAL
(Re (cos ((z + x) / 2))) ^2 is complex real ext-real Element of REAL
(Re (cos ((z + x) / 2))) * (Re (cos ((z + x) / 2))) is complex real ext-real set
Im (cos ((z + x) / 2)) is complex real ext-real Element of REAL
(Im (cos ((z + x) / 2))) ^2 is complex real ext-real Element of REAL
(Im (cos ((z + x) / 2))) * (Im (cos ((z + x) / 2))) is complex real ext-real set
((Re (cos ((z + x) / 2))) ^2) + ((Im (cos ((z + x) / 2))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (cos ((z + x) / 2))) ^2) + ((Im (cos ((z + x) / 2))) ^2)) is complex real ext-real Element of REAL
cos . ((z + x) / 2) is complex real ext-real Element of REAL
abs (cos . ((z + x) / 2)) is complex real ext-real Element of REAL
Re (cos . ((z + x) / 2)) is complex real ext-real Element of REAL
(Re (cos . ((z + x) / 2))) ^2 is complex real ext-real Element of REAL
(Re (cos . ((z + x) / 2))) * (Re (cos . ((z + x) / 2))) is complex real ext-real set
Im (cos . ((z + x) / 2)) is complex real ext-real Element of REAL
(Im (cos . ((z + x) / 2))) ^2 is complex real ext-real Element of REAL
(Im (cos . ((z + x) / 2))) * (Im (cos . ((z + x) / 2))) is complex real ext-real set
((Re (cos . ((z + x) / 2))) ^2) + ((Im (cos . ((z + x) / 2))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (cos . ((z + x) / 2))) ^2) + ((Im (cos . ((z + x) / 2))) ^2)) is complex real ext-real Element of REAL
].PI,(2 * PI).[ /\ (dom cos) is V70() V71() V72() Element of K19(REAL)
cos x is complex real ext-real Element of REAL
abs (cos x) is complex real ext-real Element of REAL
Re (cos x) is complex real ext-real Element of REAL
(Re (cos x)) ^2 is complex real ext-real Element of REAL
(Re (cos x)) * (Re (cos x)) is complex real ext-real set
Im (cos x) is complex real ext-real Element of REAL
(Im (cos x)) ^2 is complex real ext-real Element of REAL
(Im (cos x)) * (Im (cos x)) is complex real ext-real set
((Re (cos x)) ^2) + ((Im (cos x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (cos x)) ^2) + ((Im (cos x)) ^2)) is complex real ext-real Element of REAL
cos . x is complex real ext-real Element of REAL
abs (cos . x) is complex real ext-real Element of REAL
Re (cos . x) is complex real ext-real Element of REAL
(Re (cos . x)) ^2 is complex real ext-real Element of REAL
(Re (cos . x)) * (Re (cos . x)) is complex real ext-real set
Im (cos . x) is complex real ext-real Element of REAL
(Im (cos . x)) ^2 is complex real ext-real Element of REAL
(Im (cos . x)) * (Im (cos . x)) is complex real ext-real set
((Re (cos . x)) ^2) + ((Im (cos . x)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (cos . x)) ^2) + ((Im (cos . x)) ^2)) is complex real ext-real Element of REAL
cos . z is complex real ext-real Element of REAL
cos . z is complex real ext-real Element of REAL
cos . z is complex real ext-real Element of REAL
cos . z is complex real ext-real Element of REAL
cos . z is complex real ext-real Element of REAL
cos . z is complex real ext-real Element of REAL
cos . z is complex real ext-real Element of REAL
cos . z is complex real ext-real Element of REAL
cos . z is complex real ext-real Element of REAL
cos . z is complex real ext-real Element of REAL
[.(- 1),1.] is V70() V71() V72() Element of K19(REAL)
z is complex real ext-real set
sin . z is complex real ext-real Element of REAL
cos . z is complex real ext-real Element of REAL
cos z is complex real ext-real set
abs (cos z) is complex real ext-real Element of REAL
Re (cos z) is complex real ext-real Element of REAL
(Re (cos z)) ^2 is complex real ext-real Element of REAL
(Re (cos z)) * (Re (cos z)) is complex real ext-real set
Im (cos z) is complex real ext-real Element of REAL
(Im (cos z)) ^2 is complex real ext-real Element of REAL
(Im (cos z)) * (Im (cos z)) is complex real ext-real set
((Re (cos z)) ^2) + ((Im (cos z)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (cos z)) ^2) + ((Im (cos z)) ^2)) is complex real ext-real Element of REAL
abs (cos . z) is complex real ext-real Element of REAL
Re (cos . z) is complex real ext-real Element of REAL
(Re (cos . z)) ^2 is complex real ext-real Element of REAL
(Re (cos . z)) * (Re (cos . z)) is complex real ext-real set
Im (cos . z) is complex real ext-real Element of REAL
(Im (cos . z)) ^2 is complex real ext-real Element of REAL
(Im (cos . z)) * (Im (cos . z)) is complex real ext-real set
((Re (cos . z)) ^2) + ((Im (cos . z)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (cos . z)) ^2) + ((Im (cos . z)) ^2)) is complex real ext-real Element of REAL
sin z is complex real ext-real set
abs (sin z) is complex real ext-real Element of REAL
Re (sin z) is complex real ext-real Element of REAL
(Re (sin z)) ^2 is complex real ext-real Element of REAL
(Re (sin z)) * (Re (sin z)) is complex real ext-real set
Im (sin z) is complex real ext-real Element of REAL
(Im (sin z)) ^2 is complex real ext-real Element of REAL
(Im (sin z)) * (Im (sin z)) is complex real ext-real set
((Re (sin z)) ^2) + ((Im (sin z)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (sin z)) ^2) + ((Im (sin z)) ^2)) is complex real ext-real Element of REAL
abs (sin . z) is complex real ext-real Element of REAL
Re (sin . z) is complex real ext-real Element of REAL
(Re (sin . z)) ^2 is complex real ext-real Element of REAL
(Re (sin . z)) * (Re (sin . z)) is complex real ext-real set
Im (sin . z) is complex real ext-real Element of REAL
(Im (sin . z)) ^2 is complex real ext-real Element of REAL
(Im (sin . z)) * (Im (sin . z)) is complex real ext-real set
((Re (sin . z)) ^2) + ((Im (sin . z)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (sin . z)) ^2) + ((Im (sin . z)) ^2)) is complex real ext-real Element of REAL
rng sin is V70() V71() V72() set
z is set
dom sin is set
x is complex real ext-real Element of REAL
sin . (- (PI / 2)) is complex real ext-real Element of REAL
[.1,(sin . (- (PI / 2))).] is V70() V71() V72() Element of K19(REAL)
[.(- 1),1.] \/ [.1,(sin . (- (PI / 2))).] is V70() V71() V72() Element of K19(REAL)
[.(sin . (- (PI / 2))),(sin . (PI / 2)).] is V70() V71() V72() Element of K19(REAL)
[.(sin . (PI / 2)),(sin . (- (PI / 2))).] is V70() V71() V72() Element of K19(REAL)
[.(sin . (- (PI / 2))),(sin . (PI / 2)).] \/ [.(sin . (PI / 2)),(sin . (- (PI / 2))).] is V70() V71() V72() Element of K19(REAL)
v is complex real ext-real Element of REAL
sin . v is complex real ext-real Element of REAL
x is set
sin . x is complex real ext-real Element of REAL
rng cos is V70() V71() V72() set
z is set
dom cos is set
x is complex real ext-real Element of REAL
[.(cos . 0),(cos . PI).] is V70() V71() V72() Element of K19(REAL)
[.(cos . PI),(cos . 0).] is V70() V71() V72() Element of K19(REAL)
[.(cos . 0),(cos . PI).] \/ [.(cos . PI),(cos . 0).] is V70() V71() V72() Element of K19(REAL)
v is complex real ext-real Element of REAL
cos . v is complex real ext-real Element of REAL
x is set
cos . x is complex real ext-real Element of REAL
rng (sin | [.(- (PI / 2)),(PI / 2).]) is V70() V71() V72() set
x is set
dom (sin | [.(- (PI / 2)),(PI / 2).]) is set
(sin | [.(- (PI / 2)),(PI / 2).]) . (PI / 2) is complex real ext-real Element of REAL
(sin | [.(- (PI / 2)),(PI / 2).]) . (- (PI / 2)) is complex real ext-real Element of REAL
sin . (- (PI / 2)) is complex real ext-real Element of REAL
v is complex real ext-real Element of REAL
[.((sin | [.(- (PI / 2)),(PI / 2).]) . (- (PI / 2))),((sin | [.(- (PI / 2)),(PI / 2).]) . (PI / 2)).] is V70() V71() V72() Element of K19(REAL)
(sin | [.(- (PI / 2)),(PI / 2).]) | [.(- (PI / 2)),(PI / 2).] is Relation-like REAL -defined REAL -valued Function-like continuous V46() V47() V48() Element of K19(K20(REAL,REAL))
[.((sin | [.(- (PI / 2)),(PI / 2).]) . (PI / 2)),((sin | [.(- (PI / 2)),(PI / 2).]) . (- (PI / 2))).] is V70() V71() V72() Element of K19(REAL)
[.((sin | [.(- (PI / 2)),(PI / 2).]) . (- (PI / 2))),((sin | [.(- (PI / 2)),(PI / 2).]) . (PI / 2)).] \/ [.((sin | [.(- (PI / 2)),(PI / 2).]) . (PI / 2)),((sin | [.(- (PI / 2)),(PI / 2).]) . (- (PI / 2))).] is V70() V71() V72() Element of K19(REAL)
[.(- (PI / 2)),(PI / 2).] /\ REAL is V70() V71() V72() Element of K19(REAL)
t is complex real ext-real Element of REAL
(sin | [.(- (PI / 2)),(PI / 2).]) . t is complex real ext-real Element of REAL
REAL /\ [.(- (PI / 2)),(PI / 2).] is V70() V71() V72() Element of K19(REAL)
v is set
(sin | [.(- (PI / 2)),(PI / 2).]) . v is complex real ext-real Element of REAL
dom sin is set
t is complex real ext-real Element of REAL
sin . t is complex real ext-real Element of REAL
rng (sin | [.(PI / 2),((3 / 2) * PI).]) is V70() V71() V72() set
x is set
dom (sin | [.(PI / 2),((3 / 2) * PI).]) is set
(sin | [.(PI / 2),((3 / 2) * PI).]) . ((3 / 2) * PI) is complex real ext-real Element of REAL
sin . ((3 / 2) * PI) is complex real ext-real Element of REAL
[.(PI / 2),((3 / 2) * PI).] /\ REAL is V70() V71() V72() Element of K19(REAL)
(sin | [.(PI / 2),((3 / 2) * PI).]) . (PI / 2) is complex real ext-real Element of REAL
(sin | [.(PI / 2),((3 / 2) * PI).]) | [.(PI / 2),((3 / 2) * PI).] is Relation-like REAL -defined REAL -valued Function-like continuous V46() V47() V48() Element of K19(K20(REAL,REAL))
v is complex real ext-real Element of REAL
[.((sin | [.(PI / 2),((3 / 2) * PI).]) . (PI / 2)),((sin | [.(PI / 2),((3 / 2) * PI).]) . ((3 / 2) * PI)).] is V70() V71() V72() Element of K19(REAL)
[.((sin | [.(PI / 2),((3 / 2) * PI).]) . ((3 / 2) * PI)),((sin | [.(PI / 2),((3 / 2) * PI).]) . (PI / 2)).] is V70() V71() V72() Element of K19(REAL)
[.((sin | [.(PI / 2),((3 / 2) * PI).]) . (PI / 2)),((sin | [.(PI / 2),((3 / 2) * PI).]) . ((3 / 2) * PI)).] \/ [.((sin | [.(PI / 2),((3 / 2) * PI).]) . ((3 / 2) * PI)),((sin | [.(PI / 2),((3 / 2) * PI).]) . (PI / 2)).] is V70() V71() V72() Element of K19(REAL)
t is complex real ext-real Element of REAL
(sin | [.(PI / 2),((3 / 2) * PI).]) . t is complex real ext-real Element of REAL
REAL /\ [.(PI / 2),((3 / 2) * PI).] is V70() V71() V72() Element of K19(REAL)
v is set
(sin | [.(PI / 2),((3 / 2) * PI).]) . v is complex real ext-real Element of REAL
dom sin is set
t is complex real ext-real Element of REAL
sin . t is complex real ext-real Element of REAL
rng (cos | [.0,PI.]) is V70() V71() V72() set
x is set
dom (cos | [.0,PI.]) is set
(cos | [.0,PI.]) . PI is complex real ext-real Element of REAL
[.0,PI.] /\ REAL is V70() V71() V72() Element of K19(REAL)
(cos | [.0,PI.]) . 0 is complex real ext-real Element of REAL
(cos | [.0,PI.]) | [.0,PI.] is Relation-like REAL -defined REAL -valued Function-like continuous V46() V47() V48() Element of K19(K20(REAL,REAL))
v is complex real ext-real Element of REAL
[.((cos | [.0,PI.]) . 0),((cos | [.0,PI.]) . PI).] is V70() V71() V72() Element of K19(REAL)
[.((cos | [.0,PI.]) . PI),((cos | [.0,PI.]) . 0).] is V70() V71() V72() Element of K19(REAL)
[.((cos | [.0,PI.]) . 0),((cos | [.0,PI.]) . PI).] \/ [.((cos | [.0,PI.]) . PI),((cos | [.0,PI.]) . 0).] is V70() V71() V72() Element of K19(REAL)
t is complex real ext-real Element of REAL
(cos | [.0,PI.]) . t is complex real ext-real Element of REAL
REAL /\ [.0,PI.] is V70() V71() V72() Element of K19(REAL)
v is set
(cos | [.0,PI.]) . v is complex real ext-real Element of REAL
dom cos is set
t is complex real ext-real Element of REAL
cos . t is complex real ext-real Element of REAL
rng (cos | [.PI,(2 * PI).]) is V70() V71() V72() set
x is set
dom (cos | [.PI,(2 * PI).]) is set
(cos | [.PI,(2 * PI).]) . (2 * PI) is complex real ext-real Element of REAL
[.PI,(2 * PI).] /\ REAL is V70() V71() V72() Element of K19(REAL)
(cos | [.PI,(2 * PI).]) . PI is complex real ext-real Element of REAL
(cos | [.PI,(2 * PI).]) | [.PI,(2 * PI).] is Relation-like REAL -defined REAL -valued Function-like continuous V46() V47() V48() Element of K19(K20(REAL,REAL))
v is complex real ext-real Element of REAL
[.((cos | [.PI,(2 * PI).]) . PI),((cos | [.PI,(2 * PI).]) . (2 * PI)).] is V70() V71() V72() Element of K19(REAL)
[.((cos | [.PI,(2 * PI).]) . (2 * PI)),((cos | [.PI,(2 * PI).]) . PI).] is V70() V71() V72() Element of K19(REAL)
[.((cos | [.PI,(2 * PI).]) . PI),((cos | [.PI,(2 * PI).]) . (2 * PI)).] \/ [.((cos | [.PI,(2 * PI).]) . (2 * PI)),((cos | [.PI,(2 * PI).]) . PI).] is V70() V71() V72() Element of K19(REAL)
t is complex real ext-real Element of REAL
(cos | [.PI,(2 * PI).]) . t is complex real ext-real Element of REAL
REAL /\ [.PI,(2 * PI).] is V70() V71() V72() Element of K19(REAL)
v is set
(cos | [.PI,(2 * PI).]) . v is complex real ext-real Element of REAL
dom cos is set
t is complex real ext-real Element of REAL
cos . t is complex real ext-real Element of REAL
z is complex set
|.z.| is complex real ext-real Element of REAL
Re z is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
Im z is complex real ext-real Element of REAL
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) + ((Im z) ^2) is complex real ext-real Element of REAL
sqrt (((Re z) ^2) + ((Im z) ^2)) is complex real ext-real Element of REAL
(Re z) / |.z.| is complex real ext-real Element of REAL
|.z.| " is complex real ext-real set
(Re z) * (|.z.| ") is complex real ext-real set
K20([.0,PI.],REAL) is V46() V47() V48() set
K19(K20([.0,PI.],REAL)) is set
v is Relation-like [.0,PI.] -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20([.0,PI.],REAL))
t is Relation-like [.0,PI.] -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20([.0,PI.],REAL))
t " is Relation-like REAL -defined [.0,PI.] -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,[.0,PI.]))
K20(REAL,[.0,PI.]) is V46() V47() V48() set
K19(K20(REAL,[.0,PI.])) is set
(t ") . ((Re z) / |.z.|) is complex real ext-real Element of REAL
|.z.| ^2 is complex real ext-real Element of REAL
|.z.| * |.z.| is complex real ext-real set
t is complex real ext-real Element of REAL
- |.z.| is complex real ext-real Element of REAL
rng t is V70() V71() V72() set
dom (t ") is set
t is complex real ext-real Element of REAL
rng (t ") is V70() V71() V72() set
dom t is set
cos t is complex real ext-real Element of REAL
cos . t is complex real ext-real Element of REAL
t . t is complex real ext-real Element of REAL
sin . t is complex real ext-real Element of REAL
(cos . t) ^2 is complex real ext-real Element of REAL
(cos . t) * (cos . t) is complex real ext-real set
(sin . t) ^2 is complex real ext-real Element of REAL
(sin . t) * (sin . t) is complex real ext-real set
((cos . t) ^2) + ((sin . t) ^2) is complex real ext-real Element of REAL
1 - ((cos . t) ^2) is complex real ext-real Element of REAL
- ((cos . t) ^2) is complex real ext-real set
1 + (- ((cos . t) ^2)) is complex real ext-real set
((Re z) / |.z.|) ^2 is complex real ext-real Element of REAL
((Re z) / |.z.|) * ((Re z) / |.z.|) is complex real ext-real set
1 - (((Re z) / |.z.|) ^2) is complex real ext-real Element of REAL
- (((Re z) / |.z.|) ^2) is complex real ext-real set
1 + (- (((Re z) / |.z.|) ^2)) is complex real ext-real set
((Re z) ^2) / (|.z.| ^2) is complex real ext-real Element of REAL
(|.z.| ^2) " is complex real ext-real set
((Re z) ^2) * ((|.z.| ^2) ") is complex real ext-real set
1 - (((Re z) ^2) / (|.z.| ^2)) is complex real ext-real Element of REAL
- (((Re z) ^2) / (|.z.| ^2)) is complex real ext-real set
1 + (- (((Re z) ^2) / (|.z.| ^2))) is complex real ext-real set
(|.z.| ^2) / (|.z.| ^2) is complex real ext-real Element of REAL
(|.z.| ^2) * ((|.z.| ^2) ") is complex real ext-real set
((|.z.| ^2) / (|.z.| ^2)) - (((Re z) ^2) / (|.z.| ^2)) is complex real ext-real Element of REAL
((|.z.| ^2) / (|.z.| ^2)) + (- (((Re z) ^2) / (|.z.| ^2))) is complex real ext-real set
(|.z.| ^2) - ((Re z) ^2) is complex real ext-real Element of REAL
- ((Re z) ^2) is complex real ext-real set
(|.z.| ^2) + (- ((Re z) ^2)) is complex real ext-real set
((|.z.| ^2) - ((Re z) ^2)) / (|.z.| ^2) is complex real ext-real Element of REAL
((|.z.| ^2) - ((Re z) ^2)) * ((|.z.| ^2) ") is complex real ext-real set
(Im z) / |.z.| is complex real ext-real Element of REAL
(Im z) * (|.z.| ") is complex real ext-real set
((Im z) / |.z.|) ^2 is complex real ext-real Element of REAL
((Im z) / |.z.|) * ((Im z) / |.z.|) is complex real ext-real set
sqrt (((Im z) / |.z.|) ^2) is complex real ext-real Element of REAL
abs ((Im z) / |.z.|) is complex real ext-real Element of REAL
Re ((Im z) / |.z.|) is complex real ext-real Element of REAL
(Re ((Im z) / |.z.|)) ^2 is complex real ext-real Element of REAL
(Re ((Im z) / |.z.|)) * (Re ((Im z) / |.z.|)) is complex real ext-real set
Im ((Im z) / |.z.|) is complex real ext-real Element of REAL
(Im ((Im z) / |.z.|)) ^2 is complex real ext-real Element of REAL
(Im ((Im z) / |.z.|)) * (Im ((Im z) / |.z.|)) is complex real ext-real set
((Re ((Im z) / |.z.|)) ^2) + ((Im ((Im z) / |.z.|)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((Im z) / |.z.|)) ^2) + ((Im ((Im z) / |.z.|)) ^2)) is complex real ext-real Element of REAL
abs (Im z) is complex real ext-real Element of REAL
Re (Im z) is complex real ext-real Element of REAL
(Re (Im z)) ^2 is complex real ext-real Element of REAL
(Re (Im z)) * (Re (Im z)) is complex real ext-real set
Im (Im z) is complex real ext-real Element of REAL
(Im (Im z)) ^2 is complex real ext-real Element of REAL
(Im (Im z)) * (Im (Im z)) is complex real ext-real set
((Re (Im z)) ^2) + ((Im (Im z)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (Im z)) ^2) + ((Im (Im z)) ^2)) is complex real ext-real Element of REAL
abs |.z.| is complex real ext-real Element of REAL
Re |.z.| is complex real ext-real Element of REAL
(Re |.z.|) ^2 is complex real ext-real Element of REAL
(Re |.z.|) * (Re |.z.|) is complex real ext-real set
Im |.z.| is complex real ext-real Element of REAL
(Im |.z.|) ^2 is complex real ext-real Element of REAL
(Im |.z.|) * (Im |.z.|) is complex real ext-real set
((Re |.z.|) ^2) + ((Im |.z.|) ^2) is complex real ext-real Element of REAL
sqrt (((Re |.z.|) ^2) + ((Im |.z.|) ^2)) is complex real ext-real Element of REAL
(abs (Im z)) / (abs |.z.|) is complex real ext-real Element of REAL
(abs |.z.|) " is complex real ext-real set
(abs (Im z)) * ((abs |.z.|) ") is complex real ext-real set
(abs (Im z)) / |.z.| is complex real ext-real Element of REAL
(abs (Im z)) * (|.z.| ") is complex real ext-real set
|.z.| * (sin . t) is complex real ext-real Element of REAL
sin t is complex real ext-real Element of REAL
|.z.| * (sin t) is complex real ext-real Element of REAL
|.z.| * (cos t) is complex real ext-real Element of REAL
(|.z.| * (sin t)) * <i> is complex set
(|.z.| * (cos t)) + ((|.z.| * (sin t)) * <i>) is complex set
K20([.PI,(2 * PI).],REAL) is V46() V47() V48() set
K19(K20([.PI,(2 * PI).],REAL)) is set
v is Relation-like [.PI,(2 * PI).] -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20([.PI,(2 * PI).],REAL))
t is Relation-like [.PI,(2 * PI).] -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20([.PI,(2 * PI).],REAL))
t " is Relation-like REAL -defined [.PI,(2 * PI).] -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,[.PI,(2 * PI).]))
K20(REAL,[.PI,(2 * PI).]) is V46() V47() V48() set
K19(K20(REAL,[.PI,(2 * PI).])) is set
(t ") . ((Re z) / |.z.|) is complex real ext-real Element of REAL
- |.z.| is complex real ext-real Element of REAL
rng t is V70() V71() V72() set
dom (t ") is set
t is complex real ext-real Element of REAL
rng (t ") is V70() V71() V72() set
dom t is set
t . (2 * PI) is complex real ext-real Element of REAL
(t ") . 1 is complex real ext-real Element of REAL
cos t is complex real ext-real Element of REAL
cos . t is complex real ext-real Element of REAL
t . t is complex real ext-real Element of REAL
sin . t is complex real ext-real Element of REAL
|.z.| ^2 is complex real ext-real Element of REAL
|.z.| * |.z.| is complex real ext-real set
t is complex real ext-real Element of REAL
cos . t is complex real ext-real Element of REAL
(cos . t) ^2 is complex real ext-real Element of REAL
(cos . t) * (cos . t) is complex real ext-real set
sin . t is complex real ext-real Element of REAL
(sin . t) ^2 is complex real ext-real Element of REAL
(sin . t) * (sin . t) is complex real ext-real set
((cos . t) ^2) + ((sin . t) ^2) is complex real ext-real Element of REAL
1 - ((cos . t) ^2) is complex real ext-real Element of REAL
- ((cos . t) ^2) is complex real ext-real set
1 + (- ((cos . t) ^2)) is complex real ext-real set
((Re z) / |.z.|) ^2 is complex real ext-real Element of REAL
((Re z) / |.z.|) * ((Re z) / |.z.|) is complex real ext-real set
1 - (((Re z) / |.z.|) ^2) is complex real ext-real Element of REAL
- (((Re z) / |.z.|) ^2) is complex real ext-real set
1 + (- (((Re z) / |.z.|) ^2)) is complex real ext-real set
((Re z) ^2) / (|.z.| ^2) is complex real ext-real Element of REAL
(|.z.| ^2) " is complex real ext-real set
((Re z) ^2) * ((|.z.| ^2) ") is complex real ext-real set
1 - (((Re z) ^2) / (|.z.| ^2)) is complex real ext-real Element of REAL
- (((Re z) ^2) / (|.z.| ^2)) is complex real ext-real set
1 + (- (((Re z) ^2) / (|.z.| ^2))) is complex real ext-real set
(|.z.| ^2) / (|.z.| ^2) is complex real ext-real Element of REAL
(|.z.| ^2) * ((|.z.| ^2) ") is complex real ext-real set
((|.z.| ^2) / (|.z.| ^2)) - (((Re z) ^2) / (|.z.| ^2)) is complex real ext-real Element of REAL
((|.z.| ^2) / (|.z.| ^2)) + (- (((Re z) ^2) / (|.z.| ^2))) is complex real ext-real set
(|.z.| ^2) - ((Re z) ^2) is complex real ext-real Element of REAL
- ((Re z) ^2) is complex real ext-real set
(|.z.| ^2) + (- ((Re z) ^2)) is complex real ext-real set
((|.z.| ^2) - ((Re z) ^2)) / (|.z.| ^2) is complex real ext-real Element of REAL
((|.z.| ^2) - ((Re z) ^2)) * ((|.z.| ^2) ") is complex real ext-real set
(Im z) / |.z.| is complex real ext-real Element of REAL
(Im z) * (|.z.| ") is complex real ext-real set
((Im z) / |.z.|) ^2 is complex real ext-real Element of REAL
((Im z) / |.z.|) * ((Im z) / |.z.|) is complex real ext-real set
- (sin . t) is complex real ext-real Element of REAL
sqrt (((Im z) / |.z.|) ^2) is complex real ext-real Element of REAL
abs ((Im z) / |.z.|) is complex real ext-real Element of REAL
Re ((Im z) / |.z.|) is complex real ext-real Element of REAL
(Re ((Im z) / |.z.|)) ^2 is complex real ext-real Element of REAL
(Re ((Im z) / |.z.|)) * (Re ((Im z) / |.z.|)) is complex real ext-real set
Im ((Im z) / |.z.|) is complex real ext-real Element of REAL
(Im ((Im z) / |.z.|)) ^2 is complex real ext-real Element of REAL
(Im ((Im z) / |.z.|)) * (Im ((Im z) / |.z.|)) is complex real ext-real set
((Re ((Im z) / |.z.|)) ^2) + ((Im ((Im z) / |.z.|)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((Im z) / |.z.|)) ^2) + ((Im ((Im z) / |.z.|)) ^2)) is complex real ext-real Element of REAL
abs (Im z) is complex real ext-real Element of REAL
Re (Im z) is complex real ext-real Element of REAL
(Re (Im z)) ^2 is complex real ext-real Element of REAL
(Re (Im z)) * (Re (Im z)) is complex real ext-real set
Im (Im z) is complex real ext-real Element of REAL
(Im (Im z)) ^2 is complex real ext-real Element of REAL
(Im (Im z)) * (Im (Im z)) is complex real ext-real set
((Re (Im z)) ^2) + ((Im (Im z)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (Im z)) ^2) + ((Im (Im z)) ^2)) is complex real ext-real Element of REAL
abs |.z.| is complex real ext-real Element of REAL
Re |.z.| is complex real ext-real Element of REAL
(Re |.z.|) ^2 is complex real ext-real Element of REAL
(Re |.z.|) * (Re |.z.|) is complex real ext-real set
Im |.z.| is complex real ext-real Element of REAL
(Im |.z.|) ^2 is complex real ext-real Element of REAL
(Im |.z.|) * (Im |.z.|) is complex real ext-real set
((Re |.z.|) ^2) + ((Im |.z.|) ^2) is complex real ext-real Element of REAL
sqrt (((Re |.z.|) ^2) + ((Im |.z.|) ^2)) is complex real ext-real Element of REAL
(abs (Im z)) / (abs |.z.|) is complex real ext-real Element of REAL
(abs |.z.|) " is complex real ext-real set
(abs (Im z)) * ((abs |.z.|) ") is complex real ext-real set
(abs (Im z)) / |.z.| is complex real ext-real Element of REAL
(abs (Im z)) * (|.z.| ") is complex real ext-real set
- (abs (Im z)) is complex real ext-real Element of REAL
(- (abs (Im z))) / |.z.| is complex real ext-real Element of REAL
(- (abs (Im z))) * (|.z.| ") is complex real ext-real set
|.z.| * (sin . t) is complex real ext-real Element of REAL
- (Im z) is complex real ext-real Element of REAL
- (- (Im z)) is complex real ext-real Element of REAL
sin t is complex real ext-real Element of REAL
|.z.| * (sin t) is complex real ext-real Element of REAL
cos t is complex real ext-real Element of REAL
|.z.| * (cos t) is complex real ext-real Element of REAL
(|.z.| * (sin t)) * <i> is complex set
(|.z.| * (cos t)) + ((|.z.| * (sin t)) * <i>) is complex set
x is complex real ext-real Element of REAL
v is complex real ext-real Element of REAL
cos v is complex real ext-real Element of REAL
|.z.| * (cos v) is complex real ext-real Element of REAL
sin v is complex real ext-real Element of REAL
|.z.| * (sin v) is complex real ext-real Element of REAL
(|.z.| * (sin v)) * <i> is complex set
(|.z.| * (cos v)) + ((|.z.| * (sin v)) * <i>) is complex set
x is complex real ext-real Element of REAL
cos x is complex real ext-real Element of REAL
|.z.| * (cos x) is complex real ext-real Element of REAL
sin x is complex real ext-real Element of REAL
|.z.| * (sin x) is complex real ext-real Element of REAL
(|.z.| * (sin x)) * <i> is complex set
(|.z.| * (cos x)) + ((|.z.| * (sin x)) * <i>) is complex set
x is complex real ext-real Element of REAL
cos x is complex real ext-real Element of REAL
|.z.| * (cos x) is complex real ext-real Element of REAL
sin x is complex real ext-real Element of REAL
|.z.| * (sin x) is complex real ext-real Element of REAL
(|.z.| * (sin x)) * <i> is complex set
(|.z.| * (cos x)) + ((|.z.| * (sin x)) * <i>) is complex set
x is complex real ext-real Element of REAL
cos x is complex real ext-real Element of REAL
|.z.| * (cos x) is complex real ext-real Element of REAL
sin x is complex real ext-real Element of REAL
|.z.| * (sin x) is complex real ext-real Element of REAL
(|.z.| * (sin x)) * <i> is complex set
(|.z.| * (cos x)) + ((|.z.| * (sin x)) * <i>) is complex set
v is complex real ext-real Element of REAL
cos v is complex real ext-real Element of REAL
|.z.| * (cos v) is complex real ext-real Element of REAL
sin v is complex real ext-real Element of REAL
|.z.| * (sin v) is complex real ext-real Element of REAL
(|.z.| * (sin v)) * <i> is complex set
(|.z.| * (cos v)) + ((|.z.| * (sin v)) * <i>) is complex set
cos . v is complex real ext-real Element of REAL
cos . x is complex real ext-real Element of REAL
sin . v is complex real ext-real Element of REAL
dom cos is set
[.0,PI.] /\ (dom cos) is V70() V71() V72() Element of K19(REAL)
dom cos is set
[.PI,(2 * PI).] /\ (dom cos) is V70() V71() V72() Element of K19(REAL)
sin . x is complex real ext-real Element of REAL
sin . x is complex real ext-real Element of REAL
x is complex real ext-real Element of REAL
cos x is complex real ext-real Element of REAL
|.z.| * (cos x) is complex real ext-real Element of REAL
sin x is complex real ext-real Element of REAL
|.z.| * (sin x) is complex real ext-real Element of REAL
(|.z.| * (sin x)) * <i> is complex set
(|.z.| * (cos x)) + ((|.z.| * (sin x)) * <i>) is complex set
v is complex real ext-real Element of REAL
cos v is complex real ext-real Element of REAL
|.z.| * (cos v) is complex real ext-real Element of REAL
sin v is complex real ext-real Element of REAL
|.z.| * (sin v) is complex real ext-real Element of REAL
(|.z.| * (sin v)) * <i> is complex set
(|.z.| * (cos v)) + ((|.z.| * (sin v)) * <i>) is complex set
t is complex real ext-real Element of REAL
t is complex real ext-real Element of REAL
z is complex set
(z) is complex real ext-real Element of REAL
z is complex real ext-real Element of REAL
(z) is complex real ext-real Element of REAL
0 * <i> is complex set
z + (0 * <i>) is complex set
((z + (0 * <i>))) is complex real ext-real Element of REAL
- 0 is Function-like functional empty complex real ext-real non positive non negative V70() V71() V72() V73() V74() V75() V76() Element of REAL
|.(z + (0 * <i>)).| is complex real ext-real Element of REAL
Re (z + (0 * <i>)) is complex real ext-real Element of REAL
(Re (z + (0 * <i>))) ^2 is complex real ext-real Element of REAL
(Re (z + (0 * <i>))) * (Re (z + (0 * <i>))) is complex real ext-real set
Im (z + (0 * <i>)) is complex real ext-real Element of REAL
(Im (z + (0 * <i>))) ^2 is complex real ext-real Element of REAL
(Im (z + (0 * <i>))) * (Im (z + (0 * <i>))) is complex real ext-real set
((Re (z + (0 * <i>))) ^2) + ((Im (z + (0 * <i>))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (z + (0 * <i>))) ^2) + ((Im (z + (0 * <i>))) ^2)) is complex real ext-real Element of REAL
cos ((z + (0 * <i>))) is complex real ext-real Element of REAL
|.(z + (0 * <i>)).| * (cos ((z + (0 * <i>)))) is complex real ext-real Element of REAL
sin ((z + (0 * <i>))) is complex real ext-real Element of REAL
|.(z + (0 * <i>)).| * (sin ((z + (0 * <i>)))) is complex real ext-real Element of REAL
(|.(z + (0 * <i>)).| * (sin ((z + (0 * <i>))))) * <i> is complex set
(|.(z + (0 * <i>)).| * (cos ((z + (0 * <i>))))) + ((|.(z + (0 * <i>)).| * (sin ((z + (0 * <i>))))) * <i>) is complex set
|.(z + (0 * <i>)).| * (- 1) is complex real ext-real Element of REAL
- 0 is Function-like functional empty complex real ext-real non positive non negative V70() V71() V72() V73() V74() V75() V76() Element of REAL
z is complex real ext-real Element of REAL
(z) is complex real ext-real Element of REAL
0 * <i> is complex set
z + (0 * <i>) is complex set
((z + (0 * <i>))) is complex real ext-real Element of REAL
|.(z + (0 * <i>)).| is complex real ext-real Element of REAL
Re (z + (0 * <i>)) is complex real ext-real Element of REAL
(Re (z + (0 * <i>))) ^2 is complex real ext-real Element of REAL
(Re (z + (0 * <i>))) * (Re (z + (0 * <i>))) is complex real ext-real set
Im (z + (0 * <i>)) is complex real ext-real Element of REAL
(Im (z + (0 * <i>))) ^2 is complex real ext-real Element of REAL
(Im (z + (0 * <i>))) * (Im (z + (0 * <i>))) is complex real ext-real set
((Re (z + (0 * <i>))) ^2) + ((Im (z + (0 * <i>))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (z + (0 * <i>))) ^2) + ((Im (z + (0 * <i>))) ^2)) is complex real ext-real Element of REAL
cos ((z + (0 * <i>))) is complex real ext-real Element of REAL
|.(z + (0 * <i>)).| * (cos ((z + (0 * <i>)))) is complex real ext-real Element of REAL
sin ((z + (0 * <i>))) is complex real ext-real Element of REAL
|.(z + (0 * <i>)).| * (sin ((z + (0 * <i>)))) is complex real ext-real Element of REAL
(|.(z + (0 * <i>)).| * (sin ((z + (0 * <i>))))) * <i> is complex set
(|.(z + (0 * <i>)).| * (cos ((z + (0 * <i>))))) + ((|.(z + (0 * <i>)).| * (sin ((z + (0 * <i>))))) * <i>) is complex set
|.(z + (0 * <i>)).| * 1 is complex real ext-real Element of REAL
z is complex real ext-real Element of REAL
z * <i> is complex set
((z * <i>)) is complex real ext-real Element of REAL
0 + (z * <i>) is complex set
((0 + (z * <i>))) is complex real ext-real Element of REAL
|.(0 + (z * <i>)).| is complex real ext-real Element of REAL
Re (0 + (z * <i>)) is complex real ext-real Element of REAL
(Re (0 + (z * <i>))) ^2 is complex real ext-real Element of REAL
(Re (0 + (z * <i>))) * (Re (0 + (z * <i>))) is complex real ext-real set
Im (0 + (z * <i>)) is complex real ext-real Element of REAL
(Im (0 + (z * <i>))) ^2 is complex real ext-real Element of REAL
(Im (0 + (z * <i>))) * (Im (0 + (z * <i>))) is complex real ext-real set
((Re (0 + (z * <i>))) ^2) + ((Im (0 + (z * <i>))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (0 + (z * <i>))) ^2) + ((Im (0 + (z * <i>))) ^2)) is complex real ext-real Element of REAL
cos ((0 + (z * <i>))) is complex real ext-real Element of REAL
|.(0 + (z * <i>)).| * (cos ((0 + (z * <i>)))) is complex real ext-real Element of REAL
sin ((0 + (z * <i>))) is complex real ext-real Element of REAL
|.(0 + (z * <i>)).| * (sin ((0 + (z * <i>)))) is complex real ext-real Element of REAL
(|.(0 + (z * <i>)).| * (sin ((0 + (z * <i>))))) * <i> is complex set
(|.(0 + (z * <i>)).| * (cos ((0 + (z * <i>))))) + ((|.(0 + (z * <i>)).| * (sin ((0 + (z * <i>))))) * <i>) is complex set
|.(0 + (z * <i>)).| * (- 1) is complex real ext-real Element of REAL
z is complex real ext-real Element of REAL
z * <i> is complex set
((z * <i>)) is complex real ext-real Element of REAL
0 + (z * <i>) is complex set
((0 + (z * <i>))) is complex real ext-real Element of REAL
|.(0 + (z * <i>)).| is complex real ext-real Element of REAL
Re (0 + (z * <i>)) is complex real ext-real Element of REAL
(Re (0 + (z * <i>))) ^2 is complex real ext-real Element of REAL
(Re (0 + (z * <i>))) * (Re (0 + (z * <i>))) is complex real ext-real set
Im (0 + (z * <i>)) is complex real ext-real Element of REAL
(Im (0 + (z * <i>))) ^2 is complex real ext-real Element of REAL
(Im (0 + (z * <i>))) * (Im (0 + (z * <i>))) is complex real ext-real set
((Re (0 + (z * <i>))) ^2) + ((Im (0 + (z * <i>))) ^2) is complex real ext-real Element of REAL
sqrt (((Re (0 + (z * <i>))) ^2) + ((Im (0 + (z * <i>))) ^2)) is complex real ext-real Element of REAL
cos ((0 + (z * <i>))) is complex real ext-real Element of REAL
|.(0 + (z * <i>)).| * (cos ((0 + (z * <i>)))) is complex real ext-real Element of REAL
sin ((0 + (z * <i>))) is complex real ext-real Element of REAL
|.(0 + (z * <i>)).| * (sin ((0 + (z * <i>)))) is complex real ext-real Element of REAL
(|.(0 + (z * <i>)).| * (sin ((0 + (z * <i>))))) * <i> is complex set
(|.(0 + (z * <i>)).| * (cos ((0 + (z * <i>))))) + ((|.(0 + (z * <i>)).| * (sin ((0 + (z * <i>))))) * <i>) is complex set
|.(0 + (z * <i>)).| * 1 is complex real ext-real Element of REAL
(1) is complex real ext-real Element of REAL
(<i>) is complex real ext-real Element of REAL
1 * <i> is complex set
0 + (1 * <i>) is complex set
z is complex set
(z) is complex real ext-real Element of REAL
Re z is complex real ext-real Element of REAL
Im z is complex real ext-real Element of REAL
|.z.| is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) + ((Im z) ^2) is complex real ext-real Element of REAL
sqrt (((Re z) ^2) + ((Im z) ^2)) is complex real ext-real Element of REAL
cos (z) is complex real ext-real Element of REAL
|.z.| * (cos (z)) is complex real ext-real Element of REAL
sin (z) is complex real ext-real Element of REAL
|.z.| * (sin (z)) is complex real ext-real Element of REAL
(|.z.| * (sin (z))) * <i> is complex set
(|.z.| * (cos (z))) + ((|.z.| * (sin (z))) * <i>) is complex set
sin . (z) is complex real ext-real Element of REAL
(Im z) * <i> is complex set
(Re z) + ((Im z) * <i>) is complex set
0 * <i> is complex set
0 + (0 * <i>) is complex set
|.z.| is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) + ((Im z) ^2) is complex real ext-real Element of REAL
sqrt (((Re z) ^2) + ((Im z) ^2)) is complex real ext-real Element of REAL
cos (z) is complex real ext-real Element of REAL
|.z.| * (cos (z)) is complex real ext-real Element of REAL
sin (z) is complex real ext-real Element of REAL
|.z.| * (sin (z)) is complex real ext-real Element of REAL
(|.z.| * (sin (z))) * <i> is complex set
(|.z.| * (cos (z))) + ((|.z.| * (sin (z))) * <i>) is complex set
sin . (z) is complex real ext-real Element of REAL
cos . (z) is complex real ext-real Element of REAL
].(PI / 2),PI.[ is V70() V71() V72() Element of K19(REAL)
z is complex set
(z) is complex real ext-real Element of REAL
Re z is complex real ext-real Element of REAL
Im z is complex real ext-real Element of REAL
|.z.| is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) + ((Im z) ^2) is complex real ext-real Element of REAL
sqrt (((Re z) ^2) + ((Im z) ^2)) is complex real ext-real Element of REAL
cos (z) is complex real ext-real Element of REAL
|.z.| * (cos (z)) is complex real ext-real Element of REAL
sin (z) is complex real ext-real Element of REAL
|.z.| * (sin (z)) is complex real ext-real Element of REAL
(|.z.| * (sin (z))) * <i> is complex set
(|.z.| * (cos (z))) + ((|.z.| * (sin (z))) * <i>) is complex set
cos . (z) is complex real ext-real Element of REAL
sin . (z) is complex real ext-real Element of REAL
(Im z) * <i> is complex set
(Re z) + ((Im z) * <i>) is complex set
0 * <i> is complex set
0 + (0 * <i>) is complex set
|.z.| is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) + ((Im z) ^2) is complex real ext-real Element of REAL
sqrt (((Re z) ^2) + ((Im z) ^2)) is complex real ext-real Element of REAL
cos (z) is complex real ext-real Element of REAL
|.z.| * (cos (z)) is complex real ext-real Element of REAL
sin (z) is complex real ext-real Element of REAL
|.z.| * (sin (z)) is complex real ext-real Element of REAL
(|.z.| * (sin (z))) * <i> is complex set
(|.z.| * (cos (z))) + ((|.z.| * (sin (z))) * <i>) is complex set
sin . (z) is complex real ext-real Element of REAL
cos . (z) is complex real ext-real Element of REAL
].PI,((3 / 2) * PI).[ is V70() V71() V72() Element of K19(REAL)
z is complex set
(z) is complex real ext-real Element of REAL
Re z is complex real ext-real Element of REAL
Im z is complex real ext-real Element of REAL
|.z.| is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) + ((Im z) ^2) is complex real ext-real Element of REAL
sqrt (((Re z) ^2) + ((Im z) ^2)) is complex real ext-real Element of REAL
cos (z) is complex real ext-real Element of REAL
|.z.| * (cos (z)) is complex real ext-real Element of REAL
sin (z) is complex real ext-real Element of REAL
|.z.| * (sin (z)) is complex real ext-real Element of REAL
(|.z.| * (sin (z))) * <i> is complex set
(|.z.| * (cos (z))) + ((|.z.| * (sin (z))) * <i>) is complex set
cos . (z) is complex real ext-real Element of REAL
sin . (z) is complex real ext-real Element of REAL
(Im z) * <i> is complex set
(Re z) + ((Im z) * <i>) is complex set
0 * <i> is complex set
0 + (0 * <i>) is complex set
|.z.| is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) + ((Im z) ^2) is complex real ext-real Element of REAL
sqrt (((Re z) ^2) + ((Im z) ^2)) is complex real ext-real Element of REAL
cos (z) is complex real ext-real Element of REAL
|.z.| * (cos (z)) is complex real ext-real Element of REAL
sin (z) is complex real ext-real Element of REAL
|.z.| * (sin (z)) is complex real ext-real Element of REAL
(|.z.| * (sin (z))) * <i> is complex set
(|.z.| * (cos (z))) + ((|.z.| * (sin (z))) * <i>) is complex set
cos . (z) is complex real ext-real Element of REAL
sin . (z) is complex real ext-real Element of REAL
z is complex set
(z) is complex real ext-real Element of REAL
Re z is complex real ext-real Element of REAL
Im z is complex real ext-real Element of REAL
|.z.| is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) + ((Im z) ^2) is complex real ext-real Element of REAL
sqrt (((Re z) ^2) + ((Im z) ^2)) is complex real ext-real Element of REAL
cos (z) is complex real ext-real Element of REAL
|.z.| * (cos (z)) is complex real ext-real Element of REAL
sin (z) is complex real ext-real Element of REAL
|.z.| * (sin (z)) is complex real ext-real Element of REAL
(|.z.| * (sin (z))) * <i> is complex set
(|.z.| * (cos (z))) + ((|.z.| * (sin (z))) * <i>) is complex set
cos . (z) is complex real ext-real Element of REAL
sin . (z) is complex real ext-real Element of REAL
(Im z) * <i> is complex set
(Re z) + ((Im z) * <i>) is complex set
0 * <i> is complex set
0 + (0 * <i>) is complex set
|.z.| is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) + ((Im z) ^2) is complex real ext-real Element of REAL
sqrt (((Re z) ^2) + ((Im z) ^2)) is complex real ext-real Element of REAL
cos (z) is complex real ext-real Element of REAL
|.z.| * (cos (z)) is complex real ext-real Element of REAL
sin (z) is complex real ext-real Element of REAL
|.z.| * (sin (z)) is complex real ext-real Element of REAL
(|.z.| * (sin (z))) * <i> is complex set
(|.z.| * (cos (z))) + ((|.z.| * (sin (z))) * <i>) is complex set
sin . (z) is complex real ext-real Element of REAL
cos . (z) is complex real ext-real Element of REAL
z is complex set
Im z is complex real ext-real Element of REAL
(z) is complex real ext-real Element of REAL
sin (z) is complex real ext-real Element of REAL
Re z is complex real ext-real Element of REAL
(Im z) * <i> is complex set
0 + ((Im z) * <i>) is complex set
sin . (z) is complex real ext-real Element of REAL
z is complex set
Im z is complex real ext-real Element of REAL
(z) is complex real ext-real Element of REAL
sin (z) is complex real ext-real Element of REAL
Re z is complex real ext-real Element of REAL
(Im z) * <i> is complex set
0 + ((Im z) * <i>) is complex set
sin . (z) is complex real ext-real Element of REAL
z is complex set
Im z is complex real ext-real Element of REAL
(z) is complex real ext-real Element of REAL
sin (z) is complex real ext-real Element of REAL
Re z is complex real ext-real Element of REAL
0 * <i> is complex set
(Re z) + (0 * <i>) is complex set
z is complex set
Im z is complex real ext-real Element of REAL
(z) is complex real ext-real Element of REAL
sin (z) is complex real ext-real Element of REAL
Re z is complex real ext-real Element of REAL
0 * <i> is complex set
(Re z) + (0 * <i>) is complex set
z is complex set
Re z is complex real ext-real Element of REAL
(z) is complex real ext-real Element of REAL
cos (z) is complex real ext-real Element of REAL
Im z is complex real ext-real Element of REAL
0 * <i> is complex set
(Re z) + (0 * <i>) is complex set
cos . (z) is complex real ext-real Element of REAL
z is complex set
Re z is complex real ext-real Element of REAL
(z) is complex real ext-real Element of REAL
cos (z) is complex real ext-real Element of REAL
Im z is complex real ext-real Element of REAL
0 * <i> is complex set
(Re z) + (0 * <i>) is complex set
cos . (z) is complex real ext-real Element of REAL
z is complex set
Re z is complex real ext-real Element of REAL
(z) is complex real ext-real Element of REAL
cos (z) is complex real ext-real Element of REAL
Im z is complex real ext-real Element of REAL
(Im z) * <i> is complex set
0 + ((Im z) * <i>) is complex set
z is complex set
Re z is complex real ext-real Element of REAL
(z) is complex real ext-real Element of REAL
cos (z) is complex real ext-real Element of REAL
0 * <i> is complex set
0 + (0 * <i>) is complex set
Im z is complex real ext-real Element of REAL
(Im z) * <i> is complex set
0 + ((Im z) * <i>) is complex set
z is complex real ext-real set
cos z is complex real ext-real set
sin z is complex real ext-real set
(sin z) * <i> is complex set
(cos z) + ((sin z) * <i>) is complex set
x is ordinal natural complex real ext-real non negative set
((cos z) + ((sin z) * <i>)) |^ x is complex set
x * z is complex real ext-real set
cos (x * z) is complex real ext-real set
sin (x * z) is complex real ext-real set
(sin (x * z)) * <i> is complex set
(cos (x * z)) + ((sin (x * z)) * <i>) is complex set
x + 1 is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
((cos z) + ((sin z) * <i>)) |^ (x + 1) is complex set
((cos (x * z)) + ((sin (x * z)) * <i>)) * ((cos z) + ((sin z) * <i>)) is complex set
(cos (x * z)) * (cos z) is complex real ext-real set
(sin (x * z)) * (sin z) is complex real ext-real set
((cos (x * z)) * (cos z)) - ((sin (x * z)) * (sin z)) is complex real ext-real set
- ((sin (x * z)) * (sin z)) is complex real ext-real set
((cos (x * z)) * (cos z)) + (- ((sin (x * z)) * (sin z))) is complex real ext-real set
(cos (x * z)) * (sin z) is complex real ext-real set
((cos (x * z)) * (sin z)) * <i> is complex set
(((cos (x * z)) * (cos z)) - ((sin (x * z)) * (sin z))) + (((cos (x * z)) * (sin z)) * <i>) is complex set
(cos z) * (sin (x * z)) is complex real ext-real set
((cos z) * (sin (x * z))) * <i> is complex set
((((cos (x * z)) * (cos z)) - ((sin (x * z)) * (sin z))) + (((cos (x * z)) * (sin z)) * <i>)) + (((cos z) * (sin (x * z))) * <i>) is complex set
(x * z) + z is complex real ext-real set
cos ((x * z) + z) is complex real ext-real set
(cos ((x * z) + z)) + (((cos (x * z)) * (sin z)) * <i>) is complex set
((cos ((x * z) + z)) + (((cos (x * z)) * (sin z)) * <i>)) + (((cos z) * (sin (x * z))) * <i>) is complex set
((cos (x * z)) * (sin z)) + ((cos z) * (sin (x * z))) is complex real ext-real set
(((cos (x * z)) * (sin z)) + ((cos z) * (sin (x * z)))) * <i> is complex set
(cos ((x * z) + z)) + ((((cos (x * z)) * (sin z)) + ((cos z) * (sin (x * z)))) * <i>) is complex set
(x + 1) * z is complex real ext-real Element of REAL
cos ((x + 1) * z) is complex real ext-real Element of REAL
sin ((x + 1) * z) is complex real ext-real Element of REAL
(sin ((x + 1) * z)) * <i> is complex set
(cos ((x + 1) * z)) + ((sin ((x + 1) * z)) * <i>) is complex set
(x + 1) * z is complex real ext-real set
cos ((x + 1) * z) is complex real ext-real set
sin ((x + 1) * z) is complex real ext-real set
(sin ((x + 1) * z)) * <i> is complex set
(cos ((x + 1) * z)) + ((sin ((x + 1) * z)) * <i>) is complex set
((cos z) + ((sin z) * <i>)) |^ 0 is complex set
0 * z is complex real ext-real set
cos (0 * z) is complex real ext-real set
sin (0 * z) is complex real ext-real set
(sin (0 * z)) * <i> is complex set
(cos (0 * z)) + ((sin (0 * z)) * <i>) is complex set
z is complex Element of COMPLEX
|.z.| is complex real ext-real Element of REAL
Re z is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
Im z is complex real ext-real Element of REAL
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) + ((Im z) ^2) is complex real ext-real Element of REAL
sqrt (((Re z) ^2) + ((Im z) ^2)) is complex real ext-real Element of REAL
(z) is complex real ext-real Element of REAL
x is ordinal natural complex real ext-real non negative set
z |^ x is complex set
|.z.| |^ x is complex real ext-real Element of REAL
x * (z) is complex real ext-real Element of REAL
cos (x * (z)) is complex real ext-real Element of REAL
(|.z.| |^ x) * (cos (x * (z))) is complex real ext-real Element of REAL
sin (x * (z)) is complex real ext-real Element of REAL
(|.z.| |^ x) * (sin (x * (z))) is complex real ext-real Element of REAL
((|.z.| |^ x) * (sin (x * (z)))) * <i> is complex set
((|.z.| |^ x) * (cos (x * (z)))) + (((|.z.| |^ x) * (sin (x * (z)))) * <i>) is complex set
cos (z) is complex real ext-real Element of REAL
|.z.| * (cos (z)) is complex real ext-real Element of REAL
sin (z) is complex real ext-real Element of REAL
|.z.| * (sin (z)) is complex real ext-real Element of REAL
(|.z.| * (sin (z))) * <i> is complex set
(|.z.| * (cos (z))) + ((|.z.| * (sin (z))) * <i>) is complex set
((|.z.| * (cos (z))) + ((|.z.| * (sin (z))) * <i>)) |^ x is complex set
0 * <i> is complex set
|.z.| + (0 * <i>) is complex set
(sin (z)) * <i> is complex set
(cos (z)) + ((sin (z)) * <i>) is complex set
(|.z.| + (0 * <i>)) * ((cos (z)) + ((sin (z)) * <i>)) is complex set
((|.z.| + (0 * <i>)) * ((cos (z)) + ((sin (z)) * <i>))) |^ x is complex set
(|.z.| + (0 * <i>)) |^ x is complex set
((cos (z)) + ((sin (z)) * <i>)) |^ x is complex set
((|.z.| + (0 * <i>)) |^ x) * (((cos (z)) + ((sin (z)) * <i>)) |^ x) is complex set
(|.z.| |^ x) + (0 * <i>) is complex set
(sin (x * (z))) * <i> is complex set
(cos (x * (z))) + ((sin (x * (z))) * <i>) is complex set
((|.z.| |^ x) + (0 * <i>)) * ((cos (x * (z))) + ((sin (x * (z))) * <i>)) is complex set
1 + 0 is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
0 * (cos (x * (z))) is complex real ext-real Element of REAL
0 * (sin (x * (z))) is complex real ext-real Element of REAL
(0 * (sin (x * (z)))) * <i> is complex set
(0 * (cos (x * (z)))) + ((0 * (sin (x * (z)))) * <i>) is complex set
(0 * (cos (x * (z)))) + (((|.z.| |^ x) * (sin (x * (z)))) * <i>) is complex set
z is complex real ext-real Element of REAL
cos z is complex real ext-real Element of REAL
sin z is complex real ext-real Element of REAL
(sin z) * <i> is complex set
(cos z) + ((sin z) * <i>) is complex set
x is ordinal natural complex real ext-real non negative set
v is ordinal natural complex real ext-real non negative set
(2 * PI) * v is complex real ext-real non negative Element of REAL
z + ((2 * PI) * v) is complex real ext-real Element of REAL
(z + ((2 * PI) * v)) / x is complex real ext-real Element of REAL
x " is complex real ext-real non negative set
(z + ((2 * PI) * v)) * (x ") is complex real ext-real set
cos ((z + ((2 * PI) * v)) / x) is complex real ext-real Element of REAL
sin ((z + ((2 * PI) * v)) / x) is complex real ext-real Element of REAL
(sin ((z + ((2 * PI) * v)) / x)) * <i> is complex set
(cos ((z + ((2 * PI) * v)) / x)) + ((sin ((z + ((2 * PI) * v)) / x)) * <i>) is complex set
((cos ((z + ((2 * PI) * v)) / x)) + ((sin ((z + ((2 * PI) * v)) / x)) * <i>)) |^ x is complex set
x * ((z + ((2 * PI) * v)) / x) is complex real ext-real Element of REAL
cos (x * ((z + ((2 * PI) * v)) / x)) is complex real ext-real Element of REAL
sin (x * ((z + ((2 * PI) * v)) / x)) is complex real ext-real Element of REAL
(sin (x * ((z + ((2 * PI) * v)) / x))) * <i> is complex set
(cos (x * ((z + ((2 * PI) * v)) / x))) + ((sin (x * ((z + ((2 * PI) * v)) / x))) * <i>) is complex set
cos (z + ((2 * PI) * v)) is complex real ext-real Element of REAL
(cos (z + ((2 * PI) * v))) + ((sin (x * ((z + ((2 * PI) * v)) / x))) * <i>) is complex set
sin (z + ((2 * PI) * v)) is complex real ext-real Element of REAL
(sin (z + ((2 * PI) * v))) * <i> is complex set
(cos (z + ((2 * PI) * v))) + ((sin (z + ((2 * PI) * v))) * <i>) is complex set
cos . (z + ((2 * PI) * v)) is complex real ext-real Element of REAL
(cos . (z + ((2 * PI) * v))) + ((sin (z + ((2 * PI) * v))) * <i>) is complex set
sin . (z + ((2 * PI) * v)) is complex real ext-real Element of REAL
(sin . (z + ((2 * PI) * v))) * <i> is complex set
(cos . (z + ((2 * PI) * v))) + ((sin . (z + ((2 * PI) * v))) * <i>) is complex set
sin . z is complex real ext-real Element of REAL
(sin . z) * <i> is complex set
(cos . (z + ((2 * PI) * v))) + ((sin . z) * <i>) is complex set
cos . z is complex real ext-real Element of REAL
(cos . z) + ((sin . z) * <i>) is complex set
(cos . z) + ((sin z) * <i>) is complex set
z is complex set
|.z.| is complex real ext-real Element of REAL
Re z is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
Im z is complex real ext-real Element of REAL
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) + ((Im z) ^2) is complex real ext-real Element of REAL
sqrt (((Re z) ^2) + ((Im z) ^2)) is complex real ext-real Element of REAL
(z) is complex real ext-real Element of REAL
x is ordinal natural complex real ext-real non negative set
x -root |.z.| is complex real ext-real Element of REAL
v is ordinal natural complex real ext-real non negative set
(2 * PI) * v is complex real ext-real non negative Element of REAL
(z) + ((2 * PI) * v) is complex real ext-real Element of REAL
((z) + ((2 * PI) * v)) / x is complex real ext-real Element of REAL
x " is complex real ext-real non negative set
((z) + ((2 * PI) * v)) * (x ") is complex real ext-real set
cos (((z) + ((2 * PI) * v)) / x) is complex real ext-real Element of REAL
(x -root |.z.|) * (cos (((z) + ((2 * PI) * v)) / x)) is complex real ext-real Element of REAL
sin (((z) + ((2 * PI) * v)) / x) is complex real ext-real Element of REAL
(x -root |.z.|) * (sin (((z) + ((2 * PI) * v)) / x)) is complex real ext-real Element of REAL
((x -root |.z.|) * (sin (((z) + ((2 * PI) * v)) / x))) * <i> is complex set
((x -root |.z.|) * (cos (((z) + ((2 * PI) * v)) / x))) + (((x -root |.z.|) * (sin (((z) + ((2 * PI) * v)) / x))) * <i>) is complex set
(((x -root |.z.|) * (cos (((z) + ((2 * PI) * v)) / x))) + (((x -root |.z.|) * (sin (((z) + ((2 * PI) * v)) / x))) * <i>)) |^ x is complex set
0 + 1 is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
0 * <i> is complex set
(x -root |.z.|) + (0 * <i>) is complex set
(sin (((z) + ((2 * PI) * v)) / x)) * <i> is complex set
(cos (((z) + ((2 * PI) * v)) / x)) + ((sin (((z) + ((2 * PI) * v)) / x)) * <i>) is complex set
((x -root |.z.|) + (0 * <i>)) * ((cos (((z) + ((2 * PI) * v)) / x)) + ((sin (((z) + ((2 * PI) * v)) / x)) * <i>)) is complex set
(((x -root |.z.|) + (0 * <i>)) * ((cos (((z) + ((2 * PI) * v)) / x)) + ((sin (((z) + ((2 * PI) * v)) / x)) * <i>))) |^ x is complex set
((x -root |.z.|) + (0 * <i>)) |^ x is complex set
((cos (((z) + ((2 * PI) * v)) / x)) + ((sin (((z) + ((2 * PI) * v)) / x)) * <i>)) |^ x is complex set
(((x -root |.z.|) + (0 * <i>)) |^ x) * (((cos (((z) + ((2 * PI) * v)) / x)) + ((sin (((z) + ((2 * PI) * v)) / x)) * <i>)) |^ x) is complex set
cos (z) is complex real ext-real Element of REAL
sin (z) is complex real ext-real Element of REAL
(sin (z)) * <i> is complex set
(cos (z)) + ((sin (z)) * <i>) is complex set
(((x -root |.z.|) + (0 * <i>)) |^ x) * ((cos (z)) + ((sin (z)) * <i>)) is complex set
|.z.| + (0 * <i>) is complex set
(|.z.| + (0 * <i>)) * ((cos (z)) + ((sin (z)) * <i>)) is complex set
|.z.| * (cos (z)) is complex real ext-real Element of REAL
0 * (sin (z)) is complex real ext-real Element of REAL
(|.z.| * (cos (z))) - (0 * (sin (z))) is complex real ext-real Element of REAL
- (0 * (sin (z))) is complex real ext-real set
(|.z.| * (cos (z))) + (- (0 * (sin (z)))) is complex real ext-real set
|.z.| * (sin (z)) is complex real ext-real Element of REAL
0 * (cos (z)) is complex real ext-real Element of REAL
(|.z.| * (sin (z))) + (0 * (cos (z))) is complex real ext-real Element of REAL
((|.z.| * (sin (z))) + (0 * (cos (z)))) * <i> is complex set
((|.z.| * (cos (z))) - (0 * (sin (z)))) + (((|.z.| * (sin (z))) + (0 * (cos (z)))) * <i>) is complex set
0 * (cos (((z) + ((2 * PI) * v)) / x)) is complex real ext-real Element of REAL
x -root 0 is complex real ext-real Element of REAL
(x -root 0) * (sin (((z) + ((2 * PI) * v)) / x)) is complex real ext-real Element of REAL
((x -root 0) * (sin (((z) + ((2 * PI) * v)) / x))) * <i> is complex set
(0 * (cos (((z) + ((2 * PI) * v)) / x))) + (((x -root 0) * (sin (((z) + ((2 * PI) * v)) / x))) * <i>) is complex set
((0 * (cos (((z) + ((2 * PI) * v)) / x))) + (((x -root 0) * (sin (((z) + ((2 * PI) * v)) / x))) * <i>)) |^ x is complex set
0 * (sin (((z) + ((2 * PI) * v)) / x)) is complex real ext-real Element of REAL
(0 * (sin (((z) + ((2 * PI) * v)) / x))) * <i> is complex set
0 + ((0 * (sin (((z) + ((2 * PI) * v)) / x))) * <i>) is complex set
(0 + ((0 * (sin (((z) + ((2 * PI) * v)) / x))) * <i>)) |^ x is complex set
x is non empty ordinal natural complex real ext-real positive non negative set
z is complex set
|.z.| is complex real ext-real Element of REAL
Re z is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
Im z is complex real ext-real Element of REAL
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) + ((Im z) ^2) is complex real ext-real Element of REAL
sqrt (((Re z) ^2) + ((Im z) ^2)) is complex real ext-real Element of REAL
x -root |.z.| is complex real ext-real Element of REAL
(z) is complex real ext-real Element of REAL
(2 * PI) * 0 is Function-like functional empty complex real ext-real non positive non negative V70() V71() V72() V73() V74() V75() V76() Element of REAL
(z) + ((2 * PI) * 0) is complex real ext-real Element of REAL
((z) + ((2 * PI) * 0)) / x is complex real ext-real Element of REAL
x " is non empty complex real ext-real positive non negative set
((z) + ((2 * PI) * 0)) * (x ") is complex real ext-real set
cos (((z) + ((2 * PI) * 0)) / x) is complex real ext-real Element of REAL
(x -root |.z.|) * (cos (((z) + ((2 * PI) * 0)) / x)) is complex real ext-real Element of REAL
sin (((z) + ((2 * PI) * 0)) / x) is complex real ext-real Element of REAL
(x -root |.z.|) * (sin (((z) + ((2 * PI) * 0)) / x)) is complex real ext-real Element of REAL
((x -root |.z.|) * (sin (((z) + ((2 * PI) * 0)) / x))) * <i> is complex set
((x -root |.z.|) * (cos (((z) + ((2 * PI) * 0)) / x))) + (((x -root |.z.|) * (sin (((z) + ((2 * PI) * 0)) / x))) * <i>) is complex set
v is complex Element of COMPLEX
v |^ x is complex set
z is complex Element of COMPLEX
|.z.| is complex real ext-real Element of REAL
Re z is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
Im z is complex real ext-real Element of REAL
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) + ((Im z) ^2) is complex real ext-real Element of REAL
sqrt (((Re z) ^2) + ((Im z) ^2)) is complex real ext-real Element of REAL
(z) is complex real ext-real Element of REAL
x is non empty ordinal natural complex real ext-real positive non negative set
x -root |.z.| is complex real ext-real Element of REAL
v is ordinal natural complex real ext-real non negative set
(2 * PI) * v is complex real ext-real non negative Element of REAL
(z) + ((2 * PI) * v) is complex real ext-real Element of REAL
((z) + ((2 * PI) * v)) / x is complex real ext-real Element of REAL
x " is non empty complex real ext-real positive non negative set
((z) + ((2 * PI) * v)) * (x ") is complex real ext-real set
cos (((z) + ((2 * PI) * v)) / x) is complex real ext-real Element of REAL
(x -root |.z.|) * (cos (((z) + ((2 * PI) * v)) / x)) is complex real ext-real Element of REAL
sin (((z) + ((2 * PI) * v)) / x) is complex real ext-real Element of REAL
(x -root |.z.|) * (sin (((z) + ((2 * PI) * v)) / x)) is complex real ext-real Element of REAL
((x -root |.z.|) * (sin (((z) + ((2 * PI) * v)) / x))) * <i> is complex set
((x -root |.z.|) * (cos (((z) + ((2 * PI) * v)) / x))) + (((x -root |.z.|) * (sin (((z) + ((2 * PI) * v)) / x))) * <i>) is complex set
t is complex Element of COMPLEX
t |^ x is complex set
z is complex Element of COMPLEX
x is complex (z,1)
x |^ 1 is complex set
z is non empty ordinal natural complex real ext-real positive non negative set
x is complex ( 0 ,z)
v is non empty ordinal natural complex real ext-real positive non negative set
x |^ v is complex set
t is ordinal natural complex real ext-real non negative set
t + 1 is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
t is non empty ordinal natural complex real ext-real positive non negative set
t is non empty ordinal natural complex real ext-real positive non negative set
x |^ t is complex set
(x |^ t) * x is complex set
x |^ z is complex set
x |^ 1 is complex set
z is non empty ordinal natural complex real ext-real positive non negative set
x is complex Element of COMPLEX
v is complex (x,z)
0 + 1 is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
0 |^ z is ordinal natural complex real ext-real non negative Element of REAL
z is complex real ext-real set
cos z is complex real ext-real set
1 * 1 is non empty ordinal natural complex real ext-real positive non negative V56() V69() V70() V71() V72() V73() V74() V75() Element of NAT
sin z is complex real ext-real set
(sin z) * (sin z) is complex real ext-real set
(1 * 1) + ((sin z) * (sin z)) is complex real ext-real Element of REAL
z is complex set
|.z.| is complex real ext-real Element of REAL
Re z is complex real ext-real Element of REAL
(Re z) ^2 is complex real ext-real Element of REAL
(Re z) * (Re z) is complex real ext-real set
Im z is complex real ext-real Element of REAL
(Im z) ^2 is complex real ext-real Element of REAL
(Im z) * (Im z) is complex real ext-real set
((Re z) ^2) + ((Im z) ^2) is complex real ext-real Element of REAL
sqrt (((Re z) ^2) + ((Im z) ^2)) is complex real ext-real Element of REAL
(z) is complex real ext-real Element of REAL
cos (z) is complex real ext-real Element of REAL
|.z.| * (cos (z)) is complex real ext-real Element of REAL
sin (z) is complex real ext-real Element of REAL
|.z.| * (sin (z)) is complex real ext-real Element of REAL
(|.z.| * (sin (z))) * <i> is complex set
(|.z.| * (cos (z))) + ((|.z.| * (sin (z))) * <i>) is complex set