:: SIN_COS6 semantic presentation

REAL is V70() V71() V72() V76() set
NAT is V70() V71() V72() V73() V74() V75() V76() Element of K19(REAL)
K19(REAL) is set
COMPLEX is 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 V70() V71() V72() V73() V76() set
INT is 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
sin is Relation-like REAL -defined REAL -valued Function-like V33( REAL , REAL ) continuous V46() V47() V48() Element of K19(K20(REAL,REAL))
cos is Relation-like REAL -defined REAL -valued Function-like V33( REAL , REAL ) continuous V46() V47() V48() Element of K19(K20(REAL,REAL))
dom sin is V70() V71() V72() Element of K19(REAL)
dom cos is V70() V71() V72() Element of K19(REAL)
1 is non empty natural V22() real ext-real positive non negative integer V69() V70() V71() V72() V73() V74() V75() Element of NAT
0 is Function-like functional empty natural V22() real ext-real non positive non negative integer V69() V70() V71() V72() V73() V74() V75() V76() Element of NAT
the Function-like functional empty V70() V71() V72() V73() V74() V75() V76() set is Function-like functional empty V70() V71() V72() V73() V74() V75() V76() set
cos . 0 is V22() real ext-real Element of REAL
sin . 0 is V22() real ext-real Element of REAL
cos 0 is V22() real ext-real Element of REAL
sin 0 is V22() real ext-real Element of REAL
PI is V22() 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 natural V22() real ext-real positive non negative integer V69() V70() V71() V72() V73() V74() V75() Element of NAT
].0,4.[ is V29() V70() V71() V72() Element of K19(REAL)
PI is V22() real ext-real Element of REAL
2 is non empty natural V22() real ext-real positive non negative integer V69() V70() V71() V72() V73() V74() V75() Element of NAT
PI / 2 is V22() real ext-real Element of REAL
cos . (PI / 2) is V22() real ext-real Element of REAL
sin . (PI / 2) is V22() real ext-real Element of REAL
cos . PI is V22() real ext-real Element of REAL
- 1 is non empty V22() real ext-real non positive negative integer Element of REAL
sin . PI is V22() real ext-real Element of REAL
PI + (PI / 2) is V22() real ext-real Element of REAL
cos . (PI + (PI / 2)) is V22() real ext-real Element of REAL
sin . (PI + (PI / 2)) is V22() real ext-real Element of REAL
2 * PI is V22() real ext-real Element of REAL
cos . (2 * PI) is V22() real ext-real Element of REAL
sin . (2 * PI) is V22() real ext-real Element of REAL
cos (PI / 2) is V22() real ext-real Element of REAL
sin (PI / 2) is V22() real ext-real Element of REAL
cos PI is V22() real ext-real Element of REAL
sin PI is V22() real ext-real Element of REAL
cos (PI + (PI / 2)) is V22() real ext-real Element of REAL
sin (PI + (PI / 2)) is V22() real ext-real Element of REAL
cos (2 * PI) is V22() real ext-real Element of REAL
sin (2 * PI) is V22() real ext-real Element of REAL
- (PI / 2) is V22() real ext-real Element of REAL
3 is non empty natural V22() real ext-real positive non negative integer V69() V70() V71() V72() V73() V74() V75() Element of NAT
3 / 2 is non empty V22() real ext-real positive non negative Element of REAL
(3 / 2) * PI is V22() real ext-real Element of REAL
].0,PI.[ is V29() V70() V71() V72() Element of K19(REAL)
[.0,PI.] is V28() V70() V71() V72() Element of K19(REAL)
].PI,(2 * PI).[ is V29() V70() V71() V72() Element of K19(REAL)
].(- (PI / 2)),(PI / 2).[ is V29() V70() V71() V72() Element of K19(REAL)
[.(- (PI / 2)),(PI / 2).] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.(- (PI / 2)),(PI / 2).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
[.(PI / 2),((3 / 2) * PI).] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.(PI / 2),((3 / 2) * PI).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
cos | [.0,PI.] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
[.PI,(2 * PI).] is V28() V70() V71() V72() Element of K19(REAL)
cos | [.PI,(2 * PI).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
[.(- 1),1.] is V28() V70() V71() V72() Element of K19(REAL)
rng (sin | [.(- (PI / 2)),(PI / 2).]) is V70() V71() V72() set
rng (sin | [.(PI / 2),((3 / 2) * PI).]) is V70() V71() V72() set
rng (cos | [.0,PI.]) is V70() V71() V72() set
rng (cos | [.PI,(2 * PI).]) is V70() V71() V72() set
- 1 is non empty V22() real ext-real non positive negative integer set
r is V22() real ext-real set
g is V22() real ext-real set
r / g is V22() real ext-real set
[\(r / g)/] is V22() real ext-real integer set
g / g is V22() real ext-real set
(g / g) - 1 is V22() real ext-real Element of REAL
(r / g) - 1 is V22() real ext-real Element of REAL
1 - 1 is V22() real ext-real integer Element of REAL
r is Relation-like Function-like set
g is set
r | g is Relation-like Function-like set
h is set
r | h is Relation-like Function-like set
f is set
dom (r | h) is set
x is set
(r | h) . f is set
(r | h) . x is set
dom r is set
(dom r) /\ h is set
(dom r) /\ g is set
dom (r | g) is set
(r | g) . f is set
r . f is set
r . x is set
(r | g) . x is set
r is V22() real ext-real set
sin r is V22() real ext-real set
sin . r is V22() real ext-real Element of REAL
r is V22() real ext-real set
sin r is V22() real ext-real set
sin . r is V22() real ext-real Element of REAL
r is V22() real ext-real set
cos r is V22() real ext-real set
cos . r is V22() real ext-real Element of REAL
r is V22() real ext-real set
cos r is V22() real ext-real set
cos . r is V22() real ext-real Element of REAL
(2 * PI) * 0 is V22() real ext-real Element of REAL
(- (PI / 2)) + H₁( 0 ) is V22() real ext-real Element of REAL
(PI / 2) + H₁( 0 ) is V22() real ext-real Element of REAL
[.((- (PI / 2)) + H₁( 0 )),((PI / 2) + H₁( 0 )).] is V28() V70() V71() V72() Element of K19(REAL)
((3 / 2) * PI) + H₁( 0 ) is V22() real ext-real Element of REAL
[.((PI / 2) + H₁( 0 )),(((3 / 2) * PI) + H₁( 0 )).] is V28() V70() V71() V72() Element of K19(REAL)
PI + H₁( 0 ) is V22() real ext-real Element of REAL
[.H₁( 0 ),(PI + H₁( 0 )).] is V28() V70() V71() V72() Element of K19(REAL)
(2 * PI) + H₁( 0 ) is V22() real ext-real Element of REAL
[.(PI + H₁( 0 )),((2 * PI) + H₁( 0 )).] is V28() V70() V71() V72() Element of K19(REAL)
r is V22() real ext-real set
r ^2 is V22() real ext-real set
r * r is V22() real ext-real set
g is V22() real ext-real set
g ^2 is V22() real ext-real set
g * g is V22() real ext-real set
(r ^2) + (g ^2) is V22() real ext-real set
- (g ^2) is V22() real ext-real set
- 0 is Function-like functional empty V22() real ext-real non positive non negative integer V70() V71() V72() V73() V74() V75() V76() Element of REAL
(r ^2) - ((r ^2) + (g ^2)) is V22() real ext-real set
PI / 1 is non empty V22() real ext-real positive non negative Element of REAL
1 * PI is non empty V22() real ext-real positive non negative Element of REAL
(2 * PI) * 1 is non empty V22() real ext-real positive non negative Element of REAL
(PI / 2) + H₁(1) is V22() real ext-real Element of REAL
0 + H₁(1) is V22() real ext-real Element of REAL
sin (- (PI / 2)) is V22() real ext-real Element of REAL
sin . (- (PI / 2)) is V22() real ext-real Element of REAL
(- (PI / 2)) + (2 * PI) is V22() real ext-real Element of REAL
sin . ((- (PI / 2)) + (2 * PI)) is V22() real ext-real Element of REAL
r is V22() real ext-real set
sin . r is V22() real ext-real Element of REAL
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
r + ((2 * PI) * g) is V22() real ext-real Element of REAL
sin . (r + ((2 * PI) * g)) is V22() real ext-real Element of REAL
sin r is V22() real ext-real set
sin (r + ((2 * PI) * g)) is V22() real ext-real Element of REAL
cos (- (PI / 2)) is V22() real ext-real Element of REAL
cos . (- (PI / 2)) is V22() real ext-real Element of REAL
(- (PI / 2)) + (2 * PI) is V22() real ext-real Element of REAL
cos . ((- (PI / 2)) + (2 * PI)) is V22() real ext-real Element of REAL
r is V22() real ext-real set
cos . r is V22() real ext-real Element of REAL
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
r + ((2 * PI) * g) is V22() real ext-real Element of REAL
cos . (r + ((2 * PI) * g)) is V22() real ext-real Element of REAL
cos r is V22() real ext-real set
cos (r + ((2 * PI) * g)) is V22() real ext-real Element of REAL
r is V22() real ext-real set
sin r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
PI + ((2 * PI) * g) is V22() real ext-real Element of REAL
PI + H₁(g) is V22() real ext-real Element of REAL
r - H₁(g) is V22() real ext-real Element of REAL
H₁(g) - H₁(g) is V22() real ext-real Element of REAL
(PI + H₁(g)) - H₁(g) is V22() real ext-real Element of REAL
- g is V22() real ext-real integer set
(2 * PI) * (- g) is V22() real ext-real Element of REAL
r + H₁( - g) is V22() real ext-real Element of REAL
sin . (r + H₁( - g)) is V22() real ext-real Element of REAL
sin . r is V22() real ext-real Element of REAL
r is V22() real ext-real set
sin r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
PI + ((2 * PI) * g) is V22() real ext-real Element of REAL
(2 * PI) + ((2 * PI) * g) is V22() real ext-real Element of REAL
PI + H₁(g) is V22() real ext-real Element of REAL
(2 * PI) + H₁(g) is V22() real ext-real Element of REAL
r - H₁(g) is V22() real ext-real Element of REAL
(PI + H₁(g)) - H₁(g) is V22() real ext-real Element of REAL
((2 * PI) + H₁(g)) - H₁(g) is V22() real ext-real Element of REAL
- g is V22() real ext-real integer set
(2 * PI) * (- g) is V22() real ext-real Element of REAL
r + H₁( - g) is V22() real ext-real Element of REAL
sin . (r + H₁( - g)) is V22() real ext-real Element of REAL
sin . r is V22() real ext-real Element of REAL
r is V22() real ext-real set
cos r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
(- (PI / 2)) + ((2 * PI) * g) is V22() real ext-real Element of REAL
(PI / 2) + ((2 * PI) * g) is V22() real ext-real Element of REAL
(- (PI / 2)) + H₁(g) is V22() real ext-real Element of REAL
(PI / 2) + H₁(g) is V22() real ext-real Element of REAL
((PI / 2) + H₁(g)) + (PI / 2) is V22() real ext-real Element of REAL
r + (PI / 2) is V22() real ext-real Element of REAL
PI + H₁(g) is V22() real ext-real Element of REAL
sin (r + (PI / 2)) is V22() real ext-real Element of REAL
((- (PI / 2)) + H₁(g)) + (PI / 2) is V22() real ext-real Element of REAL
r is V22() real ext-real set
cos r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
(PI / 2) + ((2 * PI) * g) is V22() real ext-real Element of REAL
((3 / 2) * PI) + ((2 * PI) * g) is V22() real ext-real Element of REAL
(PI / 2) + H₁(g) is V22() real ext-real Element of REAL
((3 / 2) * PI) + H₁(g) is V22() real ext-real Element of REAL
r + (PI / 2) is V22() real ext-real Element of REAL
((PI / 2) + H₁(g)) + (PI / 2) is V22() real ext-real Element of REAL
PI + H₁(g) is V22() real ext-real Element of REAL
(((3 / 2) * PI) + H₁(g)) + (PI / 2) is V22() real ext-real Element of REAL
(2 * PI) + H₁(g) is V22() real ext-real Element of REAL
sin (r + (PI / 2)) is V22() real ext-real Element of REAL
r is V22() real ext-real set
cos r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
((3 / 2) * PI) + ((2 * PI) * g) is V22() real ext-real Element of REAL
(2 * PI) + ((2 * PI) * g) is V22() real ext-real Element of REAL
((3 / 2) * PI) + H₁(g) is V22() real ext-real Element of REAL
(2 * PI) + H₁(g) is V22() real ext-real Element of REAL
r - PI is V22() real ext-real Element of REAL
(((3 / 2) * PI) + H₁(g)) - PI is V22() real ext-real Element of REAL
(PI / 2) + H₁(g) is V22() real ext-real Element of REAL
PI + H₁(g) is V22() real ext-real Element of REAL
((2 * PI) + H₁(g)) - PI is V22() real ext-real Element of REAL
cos (r - PI) is V22() real ext-real Element of REAL
PI - r is V22() real ext-real Element of REAL
- (PI - r) is V22() real ext-real Element of REAL
cos (- (PI - r)) is V22() real ext-real Element of REAL
- r is V22() real ext-real set
PI + (- r) is V22() real ext-real Element of REAL
cos (PI + (- r)) is V22() real ext-real Element of REAL
cos (- r) is V22() real ext-real set
- (cos (- r)) is V22() real ext-real set
- (cos r) is V22() real ext-real set
r is V22() real ext-real set
sin r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
PI + ((2 * PI) * g) is V22() real ext-real Element of REAL
0 + ((2 * PI) * g) is V22() real ext-real Element of REAL
sin (0 + ((2 * PI) * g)) is V22() real ext-real Element of REAL
r is V22() real ext-real set
sin r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
PI + ((2 * PI) * g) is V22() real ext-real Element of REAL
(2 * PI) + ((2 * PI) * g) is V22() real ext-real Element of REAL
r is V22() real ext-real set
cos r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
(- (PI / 2)) + ((2 * PI) * g) is V22() real ext-real Element of REAL
(PI / 2) + ((2 * PI) * g) is V22() real ext-real Element of REAL
r is V22() real ext-real set
cos r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
(PI / 2) + ((2 * PI) * g) is V22() real ext-real Element of REAL
((3 / 2) * PI) + ((2 * PI) * g) is V22() real ext-real Element of REAL
r is V22() real ext-real set
cos r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
((3 / 2) * PI) + ((2 * PI) * g) is V22() real ext-real Element of REAL
(2 * PI) + ((2 * PI) * g) is V22() real ext-real Element of REAL
r is V22() real ext-real set
sin r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
(2 * PI) + ((2 * PI) * g) is V22() real ext-real Element of REAL
PI + ((2 * PI) * g) is V22() real ext-real Element of REAL
(2 * PI) + H₁(g) is V22() real ext-real Element of REAL
PI + H₁(g) is V22() real ext-real Element of REAL
r is V22() real ext-real set
cos r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
(2 * PI) + ((2 * PI) * g) is V22() real ext-real Element of REAL
(PI / 2) + ((2 * PI) * g) is V22() real ext-real Element of REAL
((3 / 2) * PI) + ((2 * PI) * g) is V22() real ext-real Element of REAL
(2 * PI) + H₁(g) is V22() real ext-real Element of REAL
0 + H₁(g) is V22() real ext-real Element of REAL
(- (PI / 2)) + H₁(g) is V22() real ext-real Element of REAL
(PI / 2) + H₁(g) is V22() real ext-real Element of REAL
((3 / 2) * PI) + H₁(g) is V22() real ext-real Element of REAL
r is V22() real ext-real set
sin r is V22() real ext-real set
r / (2 * PI) is V22() real ext-real Element of REAL
[\(r / (2 * PI))/] is V22() real ext-real integer set
(2 * PI) * [\(r / (2 * PI))/] is V22() real ext-real Element of REAL
((3 / 2) * PI) + ((2 * PI) * [\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
- [\(r / (2 * PI))/] is V22() real ext-real integer set
(2 * PI) * (- [\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
((2 * PI) * (- [\(r / (2 * PI))/])) + r is V22() real ext-real Element of REAL
h is V22() real ext-real set
cos r is V22() real ext-real set
(cos r) * (cos r) is V22() real ext-real set
(- 1) * (- 1) is non empty V22() real ext-real positive non negative integer Element of REAL
((cos r) * (cos r)) + ((- 1) * (- 1)) is V22() real ext-real Element of REAL
0 + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
h + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
(2 * PI) + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
(PI / 2) + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
((3 / 2) * PI) + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
r is V22() real ext-real set
sin r is V22() real ext-real set
r / (2 * PI) is V22() real ext-real Element of REAL
[\(r / (2 * PI))/] is V22() real ext-real integer set
(2 * PI) * [\(r / (2 * PI))/] is V22() real ext-real Element of REAL
(PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
- [\(r / (2 * PI))/] is V22() real ext-real integer set
(2 * PI) * (- [\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
((2 * PI) * (- [\(r / (2 * PI))/])) + r is V22() real ext-real Element of REAL
h is V22() real ext-real set
cos r is V22() real ext-real set
(cos r) * (cos r) is V22() real ext-real set
1 * 1 is non empty V22() real ext-real positive non negative integer Element of REAL
((cos r) * (cos r)) + (1 * 1) is V22() real ext-real Element of REAL
0 + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
h + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
(2 * PI) + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
(PI / 2) + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
((3 / 2) * PI) + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
r is V22() real ext-real set
cos r is V22() real ext-real set
r / (2 * PI) is V22() real ext-real Element of REAL
[\(r / (2 * PI))/] is V22() real ext-real integer set
(2 * PI) * [\(r / (2 * PI))/] is V22() real ext-real Element of REAL
PI + ((2 * PI) * [\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
- [\(r / (2 * PI))/] is V22() real ext-real integer set
(2 * PI) * (- [\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
((2 * PI) * (- [\(r / (2 * PI))/])) + r is V22() real ext-real Element of REAL
h is V22() real ext-real set
sin r is V22() real ext-real set
(sin r) * (sin r) is V22() real ext-real set
(- 1) * (- 1) is non empty V22() real ext-real positive non negative integer Element of REAL
((sin r) * (sin r)) + ((- 1) * (- 1)) is V22() real ext-real Element of REAL
0 + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
h + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
(2 * PI) + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
PI + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
r is V22() real ext-real set
cos r is V22() real ext-real set
r / (2 * PI) is V22() real ext-real Element of REAL
[\(r / (2 * PI))/] is V22() real ext-real integer set
(2 * PI) * [\(r / (2 * PI))/] is V22() real ext-real Element of REAL
- [\(r / (2 * PI))/] is V22() real ext-real integer set
(2 * PI) * (- [\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
((2 * PI) * (- [\(r / (2 * PI))/])) + r is V22() real ext-real Element of REAL
h is V22() real ext-real set
sin r is V22() real ext-real set
(sin r) * (sin r) is V22() real ext-real set
1 * 1 is non empty V22() real ext-real positive non negative integer Element of REAL
((sin r) * (sin r)) + (1 * 1) is V22() real ext-real Element of REAL
0 + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
h + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
(2 * PI) + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
PI + H₁([\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
r is V22() real ext-real set
sin r is V22() real ext-real set
r / (2 * PI) is V22() real ext-real Element of REAL
[\(r / (2 * PI))/] is V22() real ext-real integer set
(2 * PI) * [\(r / (2 * PI))/] is V22() real ext-real Element of REAL
((3 / 2) * PI) + ((2 * PI) * [\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
((3 / 2) * PI) + ((2 * PI) * 0) is V22() real ext-real Element of REAL
r is V22() real ext-real set
sin r is V22() real ext-real set
r / (2 * PI) is V22() real ext-real Element of REAL
[\(r / (2 * PI))/] is V22() real ext-real integer set
(2 * PI) * [\(r / (2 * PI))/] is V22() real ext-real Element of REAL
(PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
(PI / 2) + ((2 * PI) * 0) is V22() real ext-real Element of REAL
r is V22() real ext-real set
cos r is V22() real ext-real set
r / (2 * PI) is V22() real ext-real Element of REAL
[\(r / (2 * PI))/] is V22() real ext-real integer set
(2 * PI) * [\(r / (2 * PI))/] is V22() real ext-real Element of REAL
PI + ((2 * PI) * [\(r / (2 * PI))/]) is V22() real ext-real Element of REAL
PI + ((2 * PI) * 0) is V22() real ext-real Element of REAL
r is V22() real ext-real set
sin r is V22() real ext-real set
1 / 2 is non empty V22() real ext-real positive non negative Element of REAL
(1 / 2) * PI is non empty V22() real ext-real positive non negative Element of REAL
r is V22() real ext-real set
sin r is V22() real ext-real set
r is V22() real ext-real set
sin r is V22() real ext-real set
r is V22() real ext-real set
sin r is V22() real ext-real set
r is V22() real ext-real set
cos r is V22() real ext-real set
r is V22() real ext-real set
cos r is V22() real ext-real set
r is V22() real ext-real set
cos r is V22() real ext-real set
r is V22() real ext-real set
sin r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
(PI / 2) + ((2 * PI) * g) is V22() real ext-real Element of REAL
(PI / 2) + H₁(g) is V22() real ext-real Element of REAL
H₁(g) - H₁(g) is V22() real ext-real Element of REAL
r - H₁(g) is V22() real ext-real Element of REAL
((PI / 2) + H₁(g)) - H₁(g) is V22() real ext-real Element of REAL
sin (r - H₁(g)) is V22() real ext-real Element of REAL
- g is V22() real ext-real integer set
(2 * PI) * (- g) is V22() real ext-real Element of REAL
r + H₁( - g) is V22() real ext-real Element of REAL
sin (r + H₁( - g)) is V22() real ext-real Element of REAL
r is V22() real ext-real set
sin r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
((3 / 2) * PI) + ((2 * PI) * g) is V22() real ext-real Element of REAL
((3 / 2) * PI) + H₁(g) is V22() real ext-real Element of REAL
H₁(g) - H₁(g) is V22() real ext-real Element of REAL
r - H₁(g) is V22() real ext-real Element of REAL
(((3 / 2) * PI) + H₁(g)) - H₁(g) is V22() real ext-real Element of REAL
sin (r - H₁(g)) is V22() real ext-real Element of REAL
- g is V22() real ext-real integer set
(2 * PI) * (- g) is V22() real ext-real Element of REAL
r + H₁( - g) is V22() real ext-real Element of REAL
sin (r + H₁( - g)) is V22() real ext-real Element of REAL
r is V22() real ext-real set
sin r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
((3 / 2) * PI) + ((2 * PI) * g) is V22() real ext-real Element of REAL
(2 * PI) + ((2 * PI) * g) is V22() real ext-real Element of REAL
((3 / 2) * PI) + H₁(g) is V22() real ext-real Element of REAL
(2 * PI) + H₁(g) is V22() real ext-real Element of REAL
r - H₁(g) is V22() real ext-real Element of REAL
(((3 / 2) * PI) + H₁(g)) - H₁(g) is V22() real ext-real Element of REAL
((2 * PI) + H₁(g)) - H₁(g) is V22() real ext-real Element of REAL
sin (r - H₁(g)) is V22() real ext-real Element of REAL
- g is V22() real ext-real integer set
(2 * PI) * (- g) is V22() real ext-real Element of REAL
r + H₁( - g) is V22() real ext-real Element of REAL
sin (r + H₁( - g)) is V22() real ext-real Element of REAL
r is V22() real ext-real set
sin r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
(PI / 2) + ((2 * PI) * g) is V22() real ext-real Element of REAL
(2 * PI) + ((2 * PI) * g) is V22() real ext-real Element of REAL
(PI / 2) + H₁(g) is V22() real ext-real Element of REAL
(2 * PI) + H₁(g) is V22() real ext-real Element of REAL
r - H₁(g) is V22() real ext-real Element of REAL
((PI / 2) + H₁(g)) - H₁(g) is V22() real ext-real Element of REAL
((2 * PI) + H₁(g)) - H₁(g) is V22() real ext-real Element of REAL
sin (r - H₁(g)) is V22() real ext-real Element of REAL
- g is V22() real ext-real integer set
(2 * PI) * (- g) is V22() real ext-real Element of REAL
r + H₁( - g) is V22() real ext-real Element of REAL
sin (r + H₁( - g)) is V22() real ext-real Element of REAL
r is V22() real ext-real set
cos r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
(2 * PI) + ((2 * PI) * g) is V22() real ext-real Element of REAL
(2 * PI) + H₁(g) is V22() real ext-real Element of REAL
r - H₁(g) is V22() real ext-real Element of REAL
H₁(g) - H₁(g) is V22() real ext-real Element of REAL
((2 * PI) + H₁(g)) - H₁(g) is V22() real ext-real Element of REAL
cos (r - H₁(g)) is V22() real ext-real Element of REAL
- g is V22() real ext-real integer set
(2 * PI) * (- g) is V22() real ext-real Element of REAL
r + H₁( - g) is V22() real ext-real Element of REAL
cos (r + H₁( - g)) is V22() real ext-real Element of REAL
r is V22() real ext-real set
cos r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
PI + ((2 * PI) * g) is V22() real ext-real Element of REAL
PI + H₁(g) is V22() real ext-real Element of REAL
H₁(g) - H₁(g) is V22() real ext-real Element of REAL
r - H₁(g) is V22() real ext-real Element of REAL
(PI + H₁(g)) - H₁(g) is V22() real ext-real Element of REAL
cos (r - H₁(g)) is V22() real ext-real Element of REAL
- g is V22() real ext-real integer set
(2 * PI) * (- g) is V22() real ext-real Element of REAL
r + H₁( - g) is V22() real ext-real Element of REAL
cos (r + H₁( - g)) is V22() real ext-real Element of REAL
r is V22() real ext-real set
cos r is V22() real ext-real set
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
PI + ((2 * PI) * g) is V22() real ext-real Element of REAL
(2 * PI) + ((2 * PI) * g) is V22() real ext-real Element of REAL
PI + H₁(g) is V22() real ext-real Element of REAL
(2 * PI) + H₁(g) is V22() real ext-real Element of REAL
r - H₁(g) is V22() real ext-real Element of REAL
(PI + H₁(g)) - H₁(g) is V22() real ext-real Element of REAL
((2 * PI) + H₁(g)) - H₁(g) is V22() real ext-real Element of REAL
cos (r - H₁(g)) is V22() real ext-real Element of REAL
- g is V22() real ext-real integer set
(2 * PI) * (- g) is V22() real ext-real Element of REAL
r + H₁( - g) is V22() real ext-real Element of REAL
cos (r + H₁( - g)) is V22() real ext-real Element of REAL
r is V22() real ext-real set
(2 * PI) * r is V22() real ext-real Element of REAL
cos ((2 * PI) * r) is V22() real ext-real Element of REAL
frac r is V22() real ext-real Element of REAL
[\r/] is V22() real ext-real integer set
h is non empty V22() real ext-real positive non negative set
[\r/] + h is V22() real ext-real set
g is non empty V22() real ext-real positive non negative set
g * PI is non empty V22() real ext-real positive non negative Element of REAL
(g * PI) * 1 is non empty V22() real ext-real positive non negative Element of REAL
(g * PI) * h is non empty V22() real ext-real positive non negative Element of REAL
(2 * PI) * ([\r/] + h) is V22() real ext-real Element of REAL
cos ((2 * PI) * ([\r/] + h)) is V22() real ext-real Element of REAL
(2 * PI) * [\r/] is V22() real ext-real Element of REAL
(2 * PI) * h is non empty V22() real ext-real positive non negative Element of REAL
((2 * PI) * [\r/]) + ((2 * PI) * h) is V22() real ext-real Element of REAL
cos (((2 * PI) * [\r/]) + ((2 * PI) * h)) is V22() real ext-real Element of REAL
cos ((2 * PI) * h) is V22() real ext-real Element of REAL
sin .: [.(- (PI / 2)),(PI / 2).] is V70() V71() V72() Element of K19(REAL)
sin .: ].(- (PI / 2)),(PI / 2).[ is V70() V71() V72() Element of K19(REAL)
].(- 1),1.[ is V29() V70() V71() V72() Element of K19(REAL)
sin | ].(- (PI / 2)),(PI / 2).[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
sin | [.(- (PI / 2)),(PI / 2).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
rng (sin | ].(- (PI / 2)),(PI / 2).[) is V70() V71() V72() Element of K19(REAL)
rng (sin | [.(- (PI / 2)),(PI / 2).]) is V70() V71() V72() Element of K19(REAL)
r is set
g is set
sin . g is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
h / (2 * PI) is V22() real ext-real Element of REAL
[\(h / (2 * PI))/] is V22() real ext-real integer set
(2 * PI) * [\(h / (2 * PI))/] is V22() real ext-real Element of REAL
H₁([\(h / (2 * PI))/]) / ((2 * PI) * 1) is V22() real ext-real Element of REAL
[\(h / (2 * PI))/] / 1 is V22() real ext-real Element of REAL
sin . h is V22() real ext-real Element of REAL
sin h is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
(PI / 2) + H₁([\(h / (2 * PI))/]) is V22() real ext-real Element of REAL
(PI / 2) - (PI / 2) is V22() real ext-real Element of REAL
((PI / 2) + H₁([\(h / (2 * PI))/])) - (PI / 2) is V22() real ext-real Element of REAL
(- (PI / 2)) - (PI / 2) is V22() real ext-real Element of REAL
(- 1) * PI is non empty V22() real ext-real non positive negative Element of REAL
((- 1) * PI) / (2 * PI) is non empty V22() real ext-real non positive negative Element of REAL
(- 1) / 2 is non empty V22() real ext-real non positive negative Element of REAL
((3 / 2) * PI) + H₁([\(h / (2 * PI))/]) is V22() real ext-real Element of REAL
(((3 / 2) * PI) + H₁([\(h / (2 * PI))/])) - ((3 / 2) * PI) is V22() real ext-real Element of REAL
(- (PI / 2)) - ((3 / 2) * PI) is V22() real ext-real Element of REAL
- (2 * PI) is non empty V22() real ext-real non positive negative Element of REAL
(- (2 * PI)) / (2 * PI) is non empty V22() real ext-real non positive negative Element of REAL
(2 * PI) / (2 * PI) is non empty V22() real ext-real positive non negative Element of REAL
- ((2 * PI) / (2 * PI)) is non empty V22() real ext-real non positive negative Element of REAL
(- 1) + 1 is V22() real ext-real integer Element of REAL
(PI / 2) - ((3 / 2) * PI) is V22() real ext-real Element of REAL
- PI is non empty V22() real ext-real non positive negative Element of REAL
(- PI) / (2 * PI) is non empty V22() real ext-real non positive negative Element of REAL
r is set
g is V22() real ext-real Element of REAL
dom (sin | [.(- (PI / 2)),(PI / 2).]) is V70() V71() V72() Element of K19(REAL)
h is set
(sin | [.(- (PI / 2)),(PI / 2).]) . h is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
sin . f is V22() real ext-real Element of REAL
sin .: [.(PI / 2),((3 / 2) * PI).] is V70() V71() V72() Element of K19(REAL)
].(PI / 2),((3 / 2) * PI).[ is V29() V70() V71() V72() Element of K19(REAL)
sin .: ].(PI / 2),((3 / 2) * PI).[ is V70() V71() V72() Element of K19(REAL)
sin | ].(PI / 2),((3 / 2) * PI).[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
sin | [.(PI / 2),((3 / 2) * PI).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
rng (sin | ].(PI / 2),((3 / 2) * PI).[) is V70() V71() V72() Element of K19(REAL)
rng (sin | [.(PI / 2),((3 / 2) * PI).]) is V70() V71() V72() Element of K19(REAL)
r is set
g is set
sin . g is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
h / (2 * PI) is V22() real ext-real Element of REAL
[\(h / (2 * PI))/] is V22() real ext-real integer set
(2 * PI) * [\(h / (2 * PI))/] is V22() real ext-real Element of REAL
H₁([\(h / (2 * PI))/]) / ((2 * PI) * 1) is V22() real ext-real Element of REAL
[\(h / (2 * PI))/] / 1 is V22() real ext-real Element of REAL
sin . h is V22() real ext-real Element of REAL
sin h is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
(PI / 2) + H₁([\(h / (2 * PI))/]) is V22() real ext-real Element of REAL
((PI / 2) + H₁([\(h / (2 * PI))/])) - (PI / 2) is V22() real ext-real Element of REAL
(PI / 2) - (PI / 2) is V22() real ext-real Element of REAL
0 + 1 is non empty V22() real ext-real positive non negative integer Element of REAL
((3 / 2) * PI) - (PI / 2) is V22() real ext-real Element of REAL
(1 * PI) / (2 * PI) is non empty V22() real ext-real positive non negative Element of REAL
1 / 2 is non empty V22() real ext-real positive non negative Element of REAL
((3 / 2) * PI) + H₁([\(h / (2 * PI))/]) is V22() real ext-real Element of REAL
((3 / 2) * PI) - ((3 / 2) * PI) is V22() real ext-real Element of REAL
(((3 / 2) * PI) + H₁([\(h / (2 * PI))/])) - ((3 / 2) * PI) is V22() real ext-real Element of REAL
(PI / 2) - ((3 / 2) * PI) is V22() real ext-real Element of REAL
(- 1) * PI is non empty V22() real ext-real non positive negative Element of REAL
((- 1) * PI) / (2 * PI) is non empty V22() real ext-real non positive negative Element of REAL
(- 1) / 2 is non empty V22() real ext-real non positive negative Element of REAL
r is set
g is V22() real ext-real Element of REAL
dom (sin | [.(PI / 2),((3 / 2) * PI).]) is V70() V71() V72() Element of K19(REAL)
h is set
(sin | [.(PI / 2),((3 / 2) * PI).]) . h is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
sin . f is V22() real ext-real Element of REAL
cos .: [.0,PI.] is V70() V71() V72() Element of K19(REAL)
cos .: ].0,PI.[ is V70() V71() V72() Element of K19(REAL)
cos | ].0,PI.[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
cos | [.0,PI.] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
rng (cos | ].0,PI.[) is V70() V71() V72() Element of K19(REAL)
rng (cos | [.0,PI.]) is V70() V71() V72() Element of K19(REAL)
r is set
g is set
cos . g is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
h / (2 * PI) is V22() real ext-real Element of REAL
[\(h / (2 * PI))/] is V22() real ext-real integer set
(2 * PI) * [\(h / (2 * PI))/] is V22() real ext-real Element of REAL
H₁([\(h / (2 * PI))/]) / ((2 * PI) * 1) is V22() real ext-real Element of REAL
[\(h / (2 * PI))/] / 1 is V22() real ext-real Element of REAL
cos . h is V22() real ext-real Element of REAL
cos h is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
(1 * PI) / (2 * PI) is non empty V22() real ext-real positive non negative Element of REAL
1 / 2 is non empty V22() real ext-real positive non negative Element of REAL
0 + 1 is non empty V22() real ext-real positive non negative integer Element of REAL
PI + H₁([\(h / (2 * PI))/]) is V22() real ext-real Element of REAL
(PI + H₁([\(h / (2 * PI))/])) - PI is V22() real ext-real Element of REAL
0 - PI is non empty V22() real ext-real non positive negative Element of REAL
H₁([\(h / (2 * PI))/]) / (2 * PI) is V22() real ext-real Element of REAL
- PI is non empty V22() real ext-real non positive negative Element of REAL
(- PI) / (2 * PI) is non empty V22() real ext-real non positive negative Element of REAL
- ((1 * PI) / (2 * PI)) is non empty V22() real ext-real non positive negative Element of REAL
- (1 / 2) is non empty V22() real ext-real non positive negative Element of REAL
PI - PI is V22() real ext-real Element of REAL
r is set
g is V22() real ext-real Element of REAL
dom (cos | [.0,PI.]) is V70() V71() V72() Element of K19(REAL)
h is set
(cos | [.0,PI.]) . h is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
cos . f is V22() real ext-real Element of REAL
cos .: [.PI,(2 * PI).] is V70() V71() V72() Element of K19(REAL)
cos .: ].PI,(2 * PI).[ is V70() V71() V72() Element of K19(REAL)
cos | ].PI,(2 * PI).[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
cos | [.PI,(2 * PI).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
rng (cos | ].PI,(2 * PI).[) is V70() V71() V72() Element of K19(REAL)
rng (cos | [.PI,(2 * PI).]) is V70() V71() V72() Element of K19(REAL)
r is set
g is set
cos . g is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
h / (2 * PI) is V22() real ext-real Element of REAL
[\(h / (2 * PI))/] is V22() real ext-real integer set
(2 * PI) * [\(h / (2 * PI))/] is V22() real ext-real Element of REAL
H₁([\(h / (2 * PI))/]) / ((2 * PI) * 1) is V22() real ext-real Element of REAL
[\(h / (2 * PI))/] / 1 is V22() real ext-real Element of REAL
cos . h is V22() real ext-real Element of REAL
cos h is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
(2 * PI) / (2 * PI) is non empty V22() real ext-real positive non negative Element of REAL
1 + 0 is non empty V22() real ext-real positive non negative integer Element of REAL
PI + H₁([\(h / (2 * PI))/]) is V22() real ext-real Element of REAL
(PI + H₁([\(h / (2 * PI))/])) - PI is V22() real ext-real Element of REAL
PI - PI is V22() real ext-real Element of REAL
0 / (2 * PI) is Function-like functional empty V22() real ext-real non positive non negative V70() V71() V72() V73() V74() V75() V76() Element of REAL
0 + 1 is non empty V22() real ext-real positive non negative integer Element of REAL
(2 * PI) - PI is V22() real ext-real Element of REAL
(1 * PI) / (2 * PI) is non empty V22() real ext-real positive non negative Element of REAL
1 / 2 is non empty V22() real ext-real positive non negative Element of REAL
r is set
g is V22() real ext-real Element of REAL
dom (cos | [.PI,(2 * PI).]) is V70() V71() V72() Element of K19(REAL)
h is set
(cos | [.PI,(2 * PI).]) . h is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
cos . f is V22() real ext-real Element of REAL
g is V22() real ext-real set
h is V22() real ext-real set
r is V22() real ext-real integer set
(2 * PI) * r is V22() real ext-real Element of REAL
h + H₁(r) is V22() real ext-real Element of REAL
f is V22() real ext-real set
f + H₁(r) is V22() real ext-real Element of REAL
[.(h + H₁(r)),(f + H₁(r)).] is V28() V70() V71() V72() Element of K19(REAL)
g + (2 * PI) is V22() real ext-real Element of REAL
(f + H₁(r)) + (2 * PI) is V22() real ext-real Element of REAL
(h + H₁(r)) + (2 * PI) is V22() real ext-real Element of REAL
r + 1 is V22() real ext-real integer Element of REAL
(2 * PI) * (r + 1) is V22() real ext-real Element of REAL
h + H₁(r + 1) is V22() real ext-real Element of REAL
f + H₁(r + 1) is V22() real ext-real Element of REAL
[.(h + H₁(r + 1)),(f + H₁(r + 1)).] is V28() V70() V71() V72() Element of K19(REAL)
g is V22() real ext-real set
h is V22() real ext-real set
r is V22() real ext-real integer set
(2 * PI) * r is V22() real ext-real Element of REAL
h + H₁(r) is V22() real ext-real Element of REAL
f is V22() real ext-real set
f + H₁(r) is V22() real ext-real Element of REAL
[.(h + H₁(r)),(f + H₁(r)).] is V28() V70() V71() V72() Element of K19(REAL)
[.(h + H₁(r)),(f + H₁(r)).] /\ REAL is V70() V71() V72() Element of K19(REAL)
g + (2 * PI) is V22() real ext-real Element of REAL
r + 1 is V22() real ext-real integer Element of REAL
(2 * PI) * (r + 1) is V22() real ext-real Element of REAL
h + H₁(r + 1) is V22() real ext-real Element of REAL
f + H₁(r + 1) is V22() real ext-real Element of REAL
[.(h + H₁(r + 1)),(f + H₁(r + 1)).] is V28() V70() V71() V72() Element of K19(REAL)
[.(h + H₁(r + 1)),(f + H₁(r + 1)).] /\ REAL is V70() V71() V72() Element of K19(REAL)
g is V22() real ext-real set
h is V22() real ext-real set
r is V22() real ext-real integer set
(2 * PI) * r is V22() real ext-real Element of REAL
h + H₁(r) is V22() real ext-real Element of REAL
f is V22() real ext-real set
f + H₁(r) is V22() real ext-real Element of REAL
[.(h + H₁(r)),(f + H₁(r)).] is V28() V70() V71() V72() Element of K19(REAL)
g - (2 * PI) is V22() real ext-real Element of REAL
(f + H₁(r)) - (2 * PI) is V22() real ext-real Element of REAL
(h + H₁(r)) - (2 * PI) is V22() real ext-real Element of REAL
r - 1 is V22() real ext-real integer Element of REAL
(2 * PI) * (r - 1) is V22() real ext-real Element of REAL
h + H₁(r - 1) is V22() real ext-real Element of REAL
f + H₁(r - 1) is V22() real ext-real Element of REAL
[.(h + H₁(r - 1)),(f + H₁(r - 1)).] is V28() V70() V71() V72() Element of K19(REAL)
g is V22() real ext-real set
h is V22() real ext-real set
r is V22() real ext-real integer set
(2 * PI) * r is V22() real ext-real Element of REAL
h + H₁(r) is V22() real ext-real Element of REAL
f is V22() real ext-real set
f + H₁(r) is V22() real ext-real Element of REAL
[.(h + H₁(r)),(f + H₁(r)).] is V28() V70() V71() V72() Element of K19(REAL)
[.(h + H₁(r)),(f + H₁(r)).] /\ REAL is V70() V71() V72() Element of K19(REAL)
g - (2 * PI) is V22() real ext-real Element of REAL
r - 1 is V22() real ext-real integer Element of REAL
(2 * PI) * (r - 1) is V22() real ext-real Element of REAL
h + H₁(r - 1) is V22() real ext-real Element of REAL
f + H₁(r - 1) is V22() real ext-real Element of REAL
[.(h + H₁(r - 1)),(f + H₁(r - 1)).] is V28() V70() V71() V72() Element of K19(REAL)
[.(h + H₁(r - 1)),(f + H₁(r - 1)).] /\ REAL is V70() V71() V72() Element of K19(REAL)
r is V22() real ext-real integer set
(2 * PI) * r is V22() real ext-real Element of REAL
(- (PI / 2)) + ((2 * PI) * r) is V22() real ext-real Element of REAL
(PI / 2) + ((2 * PI) * r) is V22() real ext-real Element of REAL
[.((- (PI / 2)) + ((2 * PI) * r)),((PI / 2) + ((2 * PI) * r)).] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.((- (PI / 2)) + ((2 * PI) * r)),((PI / 2) + ((2 * PI) * r)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
(- (PI / 2)) + H₁(g) is V22() real ext-real Element of REAL
(PI / 2) + H₁(g) is V22() real ext-real Element of REAL
[.((- (PI / 2)) + H₁(g)),((PI / 2) + H₁(g)).] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.((- (PI / 2)) + H₁(g)),((PI / 2) + H₁(g)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
g - 1 is V22() real ext-real integer Element of REAL
(2 * PI) * (g - 1) is V22() real ext-real Element of REAL
(- (PI / 2)) + H₁(g - 1) is V22() real ext-real Element of REAL
(PI / 2) + H₁(g - 1) is V22() real ext-real Element of REAL
[.((- (PI / 2)) + H₁(g - 1)),((PI / 2) + H₁(g - 1)).] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.((- (PI / 2)) + H₁(g - 1)),((PI / 2) + H₁(g - 1)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
g + 1 is V22() real ext-real integer Element of REAL
(2 * PI) * (g + 1) is V22() real ext-real Element of REAL
(- (PI / 2)) + H₁(g + 1) is V22() real ext-real Element of REAL
(PI / 2) + H₁(g + 1) is V22() real ext-real Element of REAL
[.((- (PI / 2)) + H₁(g + 1)),((PI / 2) + H₁(g + 1)).] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.((- (PI / 2)) + H₁(g + 1)),((PI / 2) + H₁(g + 1)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
(g - 1) + 1 is V22() real ext-real integer Element of REAL
(2 * PI) * ((g - 1) + 1) is V22() real ext-real Element of REAL
(- (PI / 2)) + H₁((g - 1) + 1) is V22() real ext-real Element of REAL
(PI / 2) + H₁((g - 1) + 1) is V22() real ext-real Element of REAL
[.((- (PI / 2)) + H₁((g - 1) + 1)),((PI / 2) + H₁((g - 1) + 1)).] is V28() V70() V71() V72() Element of K19(REAL)
x is V22() real ext-real Element of REAL
[.((- (PI / 2)) + H₁(g - 1)),((PI / 2) + H₁(g - 1)).] /\ (dom sin) is V70() V71() V72() Element of K19(REAL)
s is V22() real ext-real Element of REAL
x + (2 * PI) is V22() real ext-real Element of REAL
[.((- (PI / 2)) + H₁((g - 1) + 1)),((PI / 2) + H₁((g - 1) + 1)).] /\ (dom sin) is V70() V71() V72() Element of K19(REAL)
s + (2 * PI) is V22() real ext-real Element of REAL
s + ((2 * PI) * 1) is V22() real ext-real Element of REAL
sin . (s + ((2 * PI) * 1)) is V22() real ext-real Element of REAL
sin . (x + (2 * PI)) is V22() real ext-real Element of REAL
sin . s is V22() real ext-real Element of REAL
x + ((2 * PI) * 1) is V22() real ext-real Element of REAL
sin . (x + ((2 * PI) * 1)) is V22() real ext-real Element of REAL
sin . x is V22() real ext-real Element of REAL
(g + 1) - 1 is V22() real ext-real integer Element of REAL
(2 * PI) * ((g + 1) - 1) is V22() real ext-real Element of REAL
(- (PI / 2)) + H₁((g + 1) - 1) is V22() real ext-real Element of REAL
(PI / 2) + H₁((g + 1) - 1) is V22() real ext-real Element of REAL
[.((- (PI / 2)) + H₁((g + 1) - 1)),((PI / 2) + H₁((g + 1) - 1)).] is V28() V70() V71() V72() Element of K19(REAL)
x is V22() real ext-real Element of REAL
[.((- (PI / 2)) + H₁(g + 1)),((PI / 2) + H₁(g + 1)).] /\ (dom sin) is V70() V71() V72() Element of K19(REAL)
s is V22() real ext-real Element of REAL
x - (2 * PI) is V22() real ext-real Element of REAL
[.((- (PI / 2)) + H₁((g - 1) + 1)),((PI / 2) + H₁((g - 1) + 1)).] /\ (dom sin) is V70() V71() V72() Element of K19(REAL)
s - (2 * PI) is V22() real ext-real Element of REAL
(2 * PI) * (- 1) is non empty V22() real ext-real non positive negative Element of REAL
s + ((2 * PI) * (- 1)) is V22() real ext-real Element of REAL
sin . (s + ((2 * PI) * (- 1))) is V22() real ext-real Element of REAL
sin . (x - (2 * PI)) is V22() real ext-real Element of REAL
sin . s is V22() real ext-real Element of REAL
x + ((2 * PI) * (- 1)) is V22() real ext-real Element of REAL
sin . (x + ((2 * PI) * (- 1))) is V22() real ext-real Element of REAL
sin . x is V22() real ext-real Element of REAL
sin | [.((- (PI / 2)) + H₁( 0 )),((PI / 2) + H₁( 0 )).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
r is V22() real ext-real integer set
(2 * PI) * r is V22() real ext-real Element of REAL
(PI / 2) + ((2 * PI) * r) is V22() real ext-real Element of REAL
((3 / 2) * PI) + ((2 * PI) * r) is V22() real ext-real Element of REAL
[.((PI / 2) + ((2 * PI) * r)),(((3 / 2) * PI) + ((2 * PI) * r)).] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.((PI / 2) + ((2 * PI) * r)),(((3 / 2) * PI) + ((2 * PI) * r)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
(PI / 2) + H₁(g) is V22() real ext-real Element of REAL
((3 / 2) * PI) + H₁(g) is V22() real ext-real Element of REAL
[.((PI / 2) + H₁(g)),(((3 / 2) * PI) + H₁(g)).] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.((PI / 2) + H₁(g)),(((3 / 2) * PI) + H₁(g)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
g - 1 is V22() real ext-real integer Element of REAL
(2 * PI) * (g - 1) is V22() real ext-real Element of REAL
(PI / 2) + H₁(g - 1) is V22() real ext-real Element of REAL
((3 / 2) * PI) + H₁(g - 1) is V22() real ext-real Element of REAL
[.((PI / 2) + H₁(g - 1)),(((3 / 2) * PI) + H₁(g - 1)).] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.((PI / 2) + H₁(g - 1)),(((3 / 2) * PI) + H₁(g - 1)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
g + 1 is V22() real ext-real integer Element of REAL
(2 * PI) * (g + 1) is V22() real ext-real Element of REAL
(PI / 2) + H₁(g + 1) is V22() real ext-real Element of REAL
((3 / 2) * PI) + H₁(g + 1) is V22() real ext-real Element of REAL
[.((PI / 2) + H₁(g + 1)),(((3 / 2) * PI) + H₁(g + 1)).] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.((PI / 2) + H₁(g + 1)),(((3 / 2) * PI) + H₁(g + 1)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
(g - 1) + 1 is V22() real ext-real integer Element of REAL
(2 * PI) * ((g - 1) + 1) is V22() real ext-real Element of REAL
(PI / 2) + H₁((g - 1) + 1) is V22() real ext-real Element of REAL
((3 / 2) * PI) + H₁((g - 1) + 1) is V22() real ext-real Element of REAL
[.((PI / 2) + H₁((g - 1) + 1)),(((3 / 2) * PI) + H₁((g - 1) + 1)).] is V28() V70() V71() V72() Element of K19(REAL)
x is V22() real ext-real Element of REAL
[.((PI / 2) + H₁(g - 1)),(((3 / 2) * PI) + H₁(g - 1)).] /\ (dom sin) is V70() V71() V72() Element of K19(REAL)
s is V22() real ext-real Element of REAL
x + (2 * PI) is V22() real ext-real Element of REAL
[.((PI / 2) + H₁((g - 1) + 1)),(((3 / 2) * PI) + H₁((g - 1) + 1)).] /\ (dom sin) is V70() V71() V72() Element of K19(REAL)
s + (2 * PI) is V22() real ext-real Element of REAL
sin . (x + (2 * PI)) is V22() real ext-real Element of REAL
s + ((2 * PI) * 1) is V22() real ext-real Element of REAL
sin . (s + ((2 * PI) * 1)) is V22() real ext-real Element of REAL
x + ((2 * PI) * 1) is V22() real ext-real Element of REAL
sin . (x + ((2 * PI) * 1)) is V22() real ext-real Element of REAL
sin . s is V22() real ext-real Element of REAL
sin . x is V22() real ext-real Element of REAL
(g + 1) - 1 is V22() real ext-real integer Element of REAL
(2 * PI) * ((g + 1) - 1) is V22() real ext-real Element of REAL
(PI / 2) + H₁((g + 1) - 1) is V22() real ext-real Element of REAL
((3 / 2) * PI) + H₁((g + 1) - 1) is V22() real ext-real Element of REAL
[.((PI / 2) + H₁((g + 1) - 1)),(((3 / 2) * PI) + H₁((g + 1) - 1)).] is V28() V70() V71() V72() Element of K19(REAL)
x is V22() real ext-real Element of REAL
[.((PI / 2) + H₁(g + 1)),(((3 / 2) * PI) + H₁(g + 1)).] /\ (dom sin) is V70() V71() V72() Element of K19(REAL)
s is V22() real ext-real Element of REAL
x - (2 * PI) is V22() real ext-real Element of REAL
[.((PI / 2) + H₁((g - 1) + 1)),(((3 / 2) * PI) + H₁((g - 1) + 1)).] /\ (dom sin) is V70() V71() V72() Element of K19(REAL)
s - (2 * PI) is V22() real ext-real Element of REAL
sin . (x - (2 * PI)) is V22() real ext-real Element of REAL
(2 * PI) * (- 1) is non empty V22() real ext-real non positive negative Element of REAL
s + ((2 * PI) * (- 1)) is V22() real ext-real Element of REAL
sin . (s + ((2 * PI) * (- 1))) is V22() real ext-real Element of REAL
x + ((2 * PI) * (- 1)) is V22() real ext-real Element of REAL
sin . (x + ((2 * PI) * (- 1))) is V22() real ext-real Element of REAL
sin . s is V22() real ext-real Element of REAL
sin . x is V22() real ext-real Element of REAL
sin | [.((PI / 2) + H₁( 0 )),(((3 / 2) * PI) + H₁( 0 )).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
r is V22() real ext-real integer set
(2 * PI) * r is V22() real ext-real Element of REAL
PI + ((2 * PI) * r) is V22() real ext-real Element of REAL
[.((2 * PI) * r),(PI + ((2 * PI) * r)).] is V28() V70() V71() V72() Element of K19(REAL)
cos | [.((2 * PI) * r),(PI + ((2 * PI) * r)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
PI + H₁(g) is V22() real ext-real Element of REAL
[.H₁(g),(PI + H₁(g)).] is V28() V70() V71() V72() Element of K19(REAL)
cos | [.H₁(g),(PI + H₁(g)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
g - 1 is V22() real ext-real integer Element of REAL
(2 * PI) * (g - 1) is V22() real ext-real Element of REAL
PI + H₁(g - 1) is V22() real ext-real Element of REAL
[.H₁(g - 1),(PI + H₁(g - 1)).] is V28() V70() V71() V72() Element of K19(REAL)
cos | [.H₁(g - 1),(PI + H₁(g - 1)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
g + 1 is V22() real ext-real integer Element of REAL
(2 * PI) * (g + 1) is V22() real ext-real Element of REAL
PI + H₁(g + 1) is V22() real ext-real Element of REAL
[.H₁(g + 1),(PI + H₁(g + 1)).] is V28() V70() V71() V72() Element of K19(REAL)
cos | [.H₁(g + 1),(PI + H₁(g + 1)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
(g - 1) + 1 is V22() real ext-real integer Element of REAL
(2 * PI) * ((g - 1) + 1) is V22() real ext-real Element of REAL
0 + H₁((g - 1) + 1) is V22() real ext-real Element of REAL
PI + H₁((g - 1) + 1) is V22() real ext-real Element of REAL
[.(0 + H₁((g - 1) + 1)),(PI + H₁((g - 1) + 1)).] is V28() V70() V71() V72() Element of K19(REAL)
0 + H₁(g - 1) is V22() real ext-real Element of REAL
[.(0 + H₁(g - 1)),(PI + H₁(g - 1)).] is V28() V70() V71() V72() Element of K19(REAL)
x is V22() real ext-real Element of REAL
[.H₁(g - 1),(PI + H₁(g - 1)).] /\ (dom cos) is V70() V71() V72() Element of K19(REAL)
s is V22() real ext-real Element of REAL
x + (2 * PI) is V22() real ext-real Element of REAL
[.(0 + H₁((g - 1) + 1)),(PI + H₁((g - 1) + 1)).] /\ (dom cos) is V70() V71() V72() Element of K19(REAL)
s + (2 * PI) is V22() real ext-real Element of REAL
cos . (x + (2 * PI)) is V22() real ext-real Element of REAL
s + ((2 * PI) * 1) is V22() real ext-real Element of REAL
cos . (s + ((2 * PI) * 1)) is V22() real ext-real Element of REAL
x + ((2 * PI) * 1) is V22() real ext-real Element of REAL
cos . (x + ((2 * PI) * 1)) is V22() real ext-real Element of REAL
cos . s is V22() real ext-real Element of REAL
cos . x is V22() real ext-real Element of REAL
0 + H₁(g + 1) is V22() real ext-real Element of REAL
[.(0 + H₁(g + 1)),(PI + H₁(g + 1)).] is V28() V70() V71() V72() Element of K19(REAL)
(g + 1) - 1 is V22() real ext-real integer Element of REAL
(2 * PI) * ((g + 1) - 1) is V22() real ext-real Element of REAL
PI + H₁((g + 1) - 1) is V22() real ext-real Element of REAL
[.H₁((g + 1) - 1),(PI + H₁((g + 1) - 1)).] is V28() V70() V71() V72() Element of K19(REAL)
x is V22() real ext-real Element of REAL
[.H₁(g + 1),(PI + H₁(g + 1)).] /\ (dom cos) is V70() V71() V72() Element of K19(REAL)
s is V22() real ext-real Element of REAL
x - (2 * PI) is V22() real ext-real Element of REAL
[.(0 + H₁((g - 1) + 1)),(PI + H₁((g - 1) + 1)).] /\ (dom cos) is V70() V71() V72() Element of K19(REAL)
s - (2 * PI) is V22() real ext-real Element of REAL
cos . (x - (2 * PI)) is V22() real ext-real Element of REAL
(2 * PI) * (- 1) is non empty V22() real ext-real non positive negative Element of REAL
s + ((2 * PI) * (- 1)) is V22() real ext-real Element of REAL
cos . (s + ((2 * PI) * (- 1))) is V22() real ext-real Element of REAL
x + ((2 * PI) * (- 1)) is V22() real ext-real Element of REAL
cos . (x + ((2 * PI) * (- 1))) is V22() real ext-real Element of REAL
cos . s is V22() real ext-real Element of REAL
cos . x is V22() real ext-real Element of REAL
cos | [.H₁( 0 ),(PI + H₁( 0 )).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
r is V22() real ext-real integer set
(2 * PI) * r is V22() real ext-real Element of REAL
PI + ((2 * PI) * r) is V22() real ext-real Element of REAL
(2 * PI) + ((2 * PI) * r) is V22() real ext-real Element of REAL
[.(PI + ((2 * PI) * r)),((2 * PI) + ((2 * PI) * r)).] is V28() V70() V71() V72() Element of K19(REAL)
cos | [.(PI + ((2 * PI) * r)),((2 * PI) + ((2 * PI) * r)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
g is V22() real ext-real integer set
(2 * PI) * g is V22() real ext-real Element of REAL
PI + H₁(g) is V22() real ext-real Element of REAL
(2 * PI) + H₁(g) is V22() real ext-real Element of REAL
[.(PI + H₁(g)),((2 * PI) + H₁(g)).] is V28() V70() V71() V72() Element of K19(REAL)
cos | [.(PI + H₁(g)),((2 * PI) + H₁(g)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
g - 1 is V22() real ext-real integer Element of REAL
(2 * PI) * (g - 1) is V22() real ext-real Element of REAL
PI + H₁(g - 1) is V22() real ext-real Element of REAL
(2 * PI) + H₁(g - 1) is V22() real ext-real Element of REAL
[.(PI + H₁(g - 1)),((2 * PI) + H₁(g - 1)).] is V28() V70() V71() V72() Element of K19(REAL)
cos | [.(PI + H₁(g - 1)),((2 * PI) + H₁(g - 1)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
g + 1 is V22() real ext-real integer Element of REAL
(2 * PI) * (g + 1) is V22() real ext-real Element of REAL
PI + H₁(g + 1) is V22() real ext-real Element of REAL
(2 * PI) + H₁(g + 1) is V22() real ext-real Element of REAL
[.(PI + H₁(g + 1)),((2 * PI) + H₁(g + 1)).] is V28() V70() V71() V72() Element of K19(REAL)
cos | [.(PI + H₁(g + 1)),((2 * PI) + H₁(g + 1)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
(g - 1) + 1 is V22() real ext-real integer Element of REAL
(2 * PI) * ((g - 1) + 1) is V22() real ext-real Element of REAL
PI + H₁((g - 1) + 1) is V22() real ext-real Element of REAL
(2 * PI) + H₁((g - 1) + 1) is V22() real ext-real Element of REAL
[.(PI + H₁((g - 1) + 1)),((2 * PI) + H₁((g - 1) + 1)).] is V28() V70() V71() V72() Element of K19(REAL)
x is V22() real ext-real Element of REAL
[.(PI + H₁(g - 1)),((2 * PI) + H₁(g - 1)).] /\ (dom cos) is V70() V71() V72() Element of K19(REAL)
s is V22() real ext-real Element of REAL
x + (2 * PI) is V22() real ext-real Element of REAL
[.(PI + H₁((g - 1) + 1)),((2 * PI) + H₁((g - 1) + 1)).] /\ (dom cos) is V70() V71() V72() Element of K19(REAL)
s + (2 * PI) is V22() real ext-real Element of REAL
s + ((2 * PI) * 1) is V22() real ext-real Element of REAL
cos . (s + ((2 * PI) * 1)) is V22() real ext-real Element of REAL
cos . (x + (2 * PI)) is V22() real ext-real Element of REAL
cos . s is V22() real ext-real Element of REAL
x + ((2 * PI) * 1) is V22() real ext-real Element of REAL
cos . (x + ((2 * PI) * 1)) is V22() real ext-real Element of REAL
cos . x is V22() real ext-real Element of REAL
(g + 1) - 1 is V22() real ext-real integer Element of REAL
(2 * PI) * ((g + 1) - 1) is V22() real ext-real Element of REAL
PI + H₁((g + 1) - 1) is V22() real ext-real Element of REAL
(2 * PI) + H₁((g + 1) - 1) is V22() real ext-real Element of REAL
[.(PI + H₁((g + 1) - 1)),((2 * PI) + H₁((g + 1) - 1)).] is V28() V70() V71() V72() Element of K19(REAL)
x is V22() real ext-real Element of REAL
[.(PI + H₁(g + 1)),((2 * PI) + H₁(g + 1)).] /\ (dom cos) is V70() V71() V72() Element of K19(REAL)
s is V22() real ext-real Element of REAL
x - (2 * PI) is V22() real ext-real Element of REAL
[.(PI + H₁((g - 1) + 1)),((2 * PI) + H₁((g - 1) + 1)).] /\ (dom cos) is V70() V71() V72() Element of K19(REAL)
s - (2 * PI) is V22() real ext-real Element of REAL
(2 * PI) * (- 1) is non empty V22() real ext-real non positive negative Element of REAL
s + ((2 * PI) * (- 1)) is V22() real ext-real Element of REAL
cos . (s + ((2 * PI) * (- 1))) is V22() real ext-real Element of REAL
cos . (x - (2 * PI)) is V22() real ext-real Element of REAL
cos . s is V22() real ext-real Element of REAL
x + ((2 * PI) * (- 1)) is V22() real ext-real Element of REAL
cos . (x + ((2 * PI) * (- 1))) is V22() real ext-real Element of REAL
cos . x is V22() real ext-real Element of REAL
cos | [.(PI + H₁( 0 )),((2 * PI) + H₁( 0 )).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
r is V22() real ext-real integer set
(2 * PI) * r is V22() real ext-real Element of REAL
(- (PI / 2)) + ((2 * PI) * r) is V22() real ext-real Element of REAL
(PI / 2) + ((2 * PI) * r) is V22() real ext-real Element of REAL
[.((- (PI / 2)) + ((2 * PI) * r)),((PI / 2) + ((2 * PI) * r)).] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.((- (PI / 2)) + ((2 * PI) * r)),((PI / 2) + ((2 * PI) * r)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
r is V22() real ext-real integer set
(2 * PI) * r is V22() real ext-real Element of REAL
(PI / 2) + ((2 * PI) * r) is V22() real ext-real Element of REAL
((3 / 2) * PI) + ((2 * PI) * r) is V22() real ext-real Element of REAL
[.((PI / 2) + ((2 * PI) * r)),(((3 / 2) * PI) + ((2 * PI) * r)).] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.((PI / 2) + ((2 * PI) * r)),(((3 / 2) * PI) + ((2 * PI) * r)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
sin | [.(- (PI / 2)),(PI / 2).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
sin | [.(PI / 2),((3 / 2) * PI).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
[.(- (PI / 2)),0.] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.(- (PI / 2)),0.] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
[.0,(PI / 2).] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.0,(PI / 2).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
[.(PI / 2),PI.] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.(PI / 2),PI.] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
[.PI,((3 / 2) * PI).] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.PI,((3 / 2) * PI).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
[.((3 / 2) * PI),(2 * PI).] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.((3 / 2) * PI),(2 * PI).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
(- (PI / 2)) + H₁(1) is V22() real ext-real Element of REAL
[.((- (PI / 2)) + H₁(1)),((PI / 2) + H₁(1)).] is V28() V70() V71() V72() Element of K19(REAL)
sin | [.((- (PI / 2)) + H₁(1)),((PI / 2) + H₁(1)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
sin | ].(- (PI / 2)),(PI / 2).[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
sin | ].(PI / 2),((3 / 2) * PI).[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
].(- (PI / 2)),0.[ is V29() V70() V71() V72() Element of K19(REAL)
sin | ].(- (PI / 2)),0.[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
].0,(PI / 2).[ is V29() V70() V71() V72() Element of K19(REAL)
sin | ].0,(PI / 2).[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
].(PI / 2),PI.[ is V29() V70() V71() V72() Element of K19(REAL)
sin | ].(PI / 2),PI.[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
].PI,((3 / 2) * PI).[ is V29() V70() V71() V72() Element of K19(REAL)
sin | ].PI,((3 / 2) * PI).[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
].((3 / 2) * PI),(2 * PI).[ is V29() V70() V71() V72() Element of K19(REAL)
sin | ].((3 / 2) * PI),(2 * PI).[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
r is V22() real ext-real integer set
(2 * PI) * r is V22() real ext-real Element of REAL
PI + ((2 * PI) * r) is V22() real ext-real Element of REAL
[.((2 * PI) * r),(PI + ((2 * PI) * r)).] is V28() V70() V71() V72() Element of K19(REAL)
cos | [.((2 * PI) * r),(PI + ((2 * PI) * r)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
r is V22() real ext-real integer set
(2 * PI) * r is V22() real ext-real Element of REAL
PI + ((2 * PI) * r) is V22() real ext-real Element of REAL
(2 * PI) + ((2 * PI) * r) is V22() real ext-real Element of REAL
[.(PI + ((2 * PI) * r)),((2 * PI) + ((2 * PI) * r)).] is V28() V70() V71() V72() Element of K19(REAL)
cos | [.(PI + ((2 * PI) * r)),((2 * PI) + ((2 * PI) * r)).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
cos | [.0,PI.] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
cos | [.PI,(2 * PI).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
cos | [.0,(PI / 2).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
cos | [.(PI / 2),PI.] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
cos | [.PI,((3 / 2) * PI).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
cos | [.((3 / 2) * PI),(2 * PI).] is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
cos | ].0,PI.[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
cos | ].PI,(2 * PI).[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
cos | ].0,(PI / 2).[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
cos | ].(PI / 2),PI.[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
cos | ].PI,((3 / 2) * PI).[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
cos | ].((3 / 2) * PI),(2 * PI).[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
r is V22() real ext-real set
sin r is V22() real ext-real set
cos r is V22() real ext-real set
g is V22() real ext-real set
sin g is V22() real ext-real set
cos g is V22() real ext-real set
h is V22() real ext-real integer set
(2 * PI) * h is V22() real ext-real Element of REAL
(2 * PI) + ((2 * PI) * h) is V22() real ext-real Element of REAL
r - g is V22() real ext-real set
cos (r - g) is V22() real ext-real set
(cos r) * (cos g) is V22() real ext-real set
(sin r) * (sin g) is V22() real ext-real set
((cos r) * (cos g)) + ((sin r) * (sin g)) is V22() real ext-real set
sin (r - g) is V22() real ext-real set
(sin r) * (cos g) is V22() real ext-real set
(cos r) * (sin g) is V22() real ext-real set
((sin r) * (cos g)) - ((cos r) * (sin g)) is V22() real ext-real set
g - r is V22() real ext-real set
cos (g - r) is V22() real ext-real set
sin (g - r) is V22() real ext-real set
(sin g) * (cos r) is V22() real ext-real set
(cos g) * (sin r) is V22() real ext-real set
((sin g) * (cos r)) - ((cos g) * (sin r)) is V22() real ext-real set
((2 * PI) + ((2 * PI) * h)) + g is V22() real ext-real Element of REAL
r + ((2 * PI) * h) is V22() real ext-real Element of REAL
(((2 * PI) + ((2 * PI) * h)) + g) - ((2 * PI) * h) is V22() real ext-real Element of REAL
(r + ((2 * PI) * h)) - ((2 * PI) * h) is V22() real ext-real Element of REAL
(2 * PI) + g is V22() real ext-real Element of REAL
g + 0 is V22() real ext-real Element of REAL
((2 * PI) + ((2 * PI) * h)) + r is V22() real ext-real Element of REAL
g + ((2 * PI) * h) is V22() real ext-real Element of REAL
(((2 * PI) + ((2 * PI) * h)) + r) - ((2 * PI) * h) is V22() real ext-real Element of REAL
(g + ((2 * PI) * h)) - ((2 * PI) * h) is V22() real ext-real Element of REAL
(2 * PI) + r is V22() real ext-real Element of REAL
r + 0 is V22() real ext-real Element of REAL
(sin | [.(- (PI / 2)),(PI / 2).]) " is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
() is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
r is set
() . r is V22() real ext-real Element of REAL
r is set
(r) is set
() . r is V22() real ext-real Element of REAL
() " is Relation-like Function-like set
rng () is V70() V71() V72() Element of K19(REAL)
dom (sin | [.(- (PI / 2)),(PI / 2).]) is V70() V71() V72() Element of K19(REAL)
dom () is V70() V71() V72() Element of K19(REAL)
() * (sin | [.(- (PI / 2)),(PI / 2).]) is Relation-like Function-like one-to-one V46() V47() V48() set
id [.(- 1),1.] is Relation-like [.(- 1),1.] -defined [.(- 1),1.] -valued Function-like one-to-one total V46() V47() V48() Element of K19(K20([.(- 1),1.],[.(- 1),1.]))
K20([.(- 1),1.],[.(- 1),1.]) is V46() V47() V48() set
K19(K20([.(- 1),1.],[.(- 1),1.])) is set
() * (sin | [.(- (PI / 2)),(PI / 2).]) is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
(sin | [.(- (PI / 2)),(PI / 2).]) * () is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
id [.(- (PI / 2)),(PI / 2).] is Relation-like [.(- (PI / 2)),(PI / 2).] -defined [.(- (PI / 2)),(PI / 2).] -valued Function-like one-to-one total V46() V47() V48() Element of K19(K20([.(- (PI / 2)),(PI / 2).],[.(- (PI / 2)),(PI / 2).]))
K20([.(- (PI / 2)),(PI / 2).],[.(- (PI / 2)),(PI / 2).]) is V46() V47() V48() set
K19(K20([.(- (PI / 2)),(PI / 2).],[.(- (PI / 2)),(PI / 2).])) is set
(sin | [.(- (PI / 2)),(PI / 2).]) * () is Relation-like Function-like one-to-one V46() V47() V48() set
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
sin (r) is V22() real ext-real Element of REAL
sin . (() . r) is V22() real ext-real Element of REAL
(sin | [.(- (PI / 2)),(PI / 2).]) . (() . r) is V22() real ext-real set
(id [.(- 1),1.]) . r is V22() real ext-real Element of REAL
r is V22() real ext-real set
sin r is V22() real ext-real set
((sin r)) is V22() real ext-real Element of REAL
() . (sin r) is V22() real ext-real Element of REAL
dom (sin | [.(- (PI / 2)),(PI / 2).]) is V70() V71() V72() Element of K19(REAL)
sin . r is V22() real ext-real Element of REAL
() . (sin . r) is V22() real ext-real Element of REAL
(sin | [.(- (PI / 2)),(PI / 2).]) . r is V22() real ext-real Element of REAL
() . ((sin | [.(- (PI / 2)),(PI / 2).]) . r) is V22() real ext-real Element of REAL
(id [.(- (PI / 2)),(PI / 2).]) . r is V22() real ext-real Element of REAL
((- 1)) is V22() real ext-real Element of REAL
() . (- 1) is V22() real ext-real Element of REAL
(0) is V22() real ext-real Element of REAL
() . 0 is V22() real ext-real Element of REAL
(1) is V22() real ext-real Element of REAL
() . 1 is V22() real ext-real Element of REAL
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
- r is V22() real ext-real set
((- r)) is V22() real ext-real Element of REAL
() . (- r) is V22() real ext-real Element of REAL
- ((- r)) is V22() real ext-real Element of REAL
- (- 1) is non empty V22() real ext-real positive non negative integer Element of REAL
- (- (PI / 2)) is V22() real ext-real Element of REAL
1 * (- r) is V22() real ext-real Element of REAL
0 - (1 * (- r)) is V22() real ext-real Element of REAL
cos ((- r)) is V22() real ext-real Element of REAL
(sin 0) * (cos ((- r))) is V22() real ext-real Element of REAL
sin ((- r)) is V22() real ext-real Element of REAL
(cos 0) * (sin ((- r))) is V22() real ext-real Element of REAL
((sin 0) * (cos ((- r)))) - ((cos 0) * (sin ((- r)))) is V22() real ext-real Element of REAL
0 - ((- r)) is V22() real ext-real Element of REAL
sin (0 - ((- r))) is V22() real ext-real Element of REAL
r is V22() real ext-real set
r ^2 is V22() real ext-real set
r * r is V22() real ext-real set
g is V22() real ext-real set
g ^2 is V22() real ext-real set
g * g is V22() real ext-real set
(g ^2) + (r ^2) is V22() real ext-real set
(g) is V22() real ext-real Element of REAL
() . g is V22() real ext-real Element of REAL
cos (g) is V22() real ext-real Element of REAL
sin . (g) is V22() real ext-real Element of REAL
(sin . (g)) ^2 is V22() real ext-real Element of REAL
(sin . (g)) * (sin . (g)) is V22() real ext-real set
cos . (g) is V22() real ext-real Element of REAL
(cos . (g)) ^2 is V22() real ext-real Element of REAL
(cos . (g)) * (cos . (g)) is V22() real ext-real set
((sin . (g)) ^2) + ((cos . (g)) ^2) is V22() real ext-real Element of REAL
1 - ((sin . (g)) ^2) is V22() real ext-real Element of REAL
sin (g) is V22() real ext-real Element of REAL
(sin (g)) ^2 is V22() real ext-real Element of REAL
(sin (g)) * (sin (g)) is V22() real ext-real set
1 - ((sin (g)) ^2) is V22() real ext-real Element of REAL
1 - (g ^2) is V22() real ext-real Element of REAL
- r is V22() real ext-real set
- (- r) is V22() real ext-real set
- (- (- r)) is V22() real ext-real set
r is V22() real ext-real set
r ^2 is V22() real ext-real set
r * r is V22() real ext-real set
- r is V22() real ext-real set
g is V22() real ext-real set
g ^2 is V22() real ext-real set
g * g is V22() real ext-real set
(g ^2) + (r ^2) is V22() real ext-real set
(g) is V22() real ext-real Element of REAL
() . g is V22() real ext-real Element of REAL
cos (g) is V22() real ext-real Element of REAL
sin . (g) is V22() real ext-real Element of REAL
(sin . (g)) ^2 is V22() real ext-real Element of REAL
(sin . (g)) * (sin . (g)) is V22() real ext-real set
cos . (g) is V22() real ext-real Element of REAL
(cos . (g)) ^2 is V22() real ext-real Element of REAL
(cos . (g)) * (cos . (g)) is V22() real ext-real set
((sin . (g)) ^2) + ((cos . (g)) ^2) is V22() real ext-real Element of REAL
1 - ((sin . (g)) ^2) is V22() real ext-real Element of REAL
sin (g) is V22() real ext-real Element of REAL
(sin (g)) ^2 is V22() real ext-real Element of REAL
(sin (g)) * (sin (g)) is V22() real ext-real set
1 - ((sin (g)) ^2) is V22() real ext-real Element of REAL
1 - (g ^2) is V22() real ext-real Element of REAL
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
cos (r) is V22() real ext-real Element of REAL
r ^2 is V22() real ext-real set
r * r is V22() real ext-real set
1 - (r ^2) is V22() real ext-real Element of REAL
sqrt (1 - (r ^2)) is V22() real ext-real Element of REAL
(r ^2) + 0 is V22() real ext-real Element of REAL
1 ^2 is V22() real ext-real Element of REAL
1 * 1 is non empty V22() real ext-real positive non negative integer set
(sqrt (1 - (r ^2))) ^2 is V22() real ext-real Element of REAL
(sqrt (1 - (r ^2))) * (sqrt (1 - (r ^2))) is V22() real ext-real set
(r ^2) + ((sqrt (1 - (r ^2))) ^2) is V22() real ext-real Element of REAL
(r ^2) + (1 - (r ^2)) is V22() real ext-real Element of REAL
() | [.(- 1),1.] is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
(sin | [.(- (PI / 2)),(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 one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
((sin | [.(- (PI / 2)),(PI / 2).]) | [.(- (PI / 2)),(PI / 2).]) " is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
(((sin | [.(- (PI / 2)),(PI / 2).]) | [.(- (PI / 2)),(PI / 2).]) ") | ((sin | [.(- (PI / 2)),(PI / 2).]) .: [.(- (PI / 2)),(PI / 2).]) is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
r is V22() real ext-real set
diff ((),r) is V22() real ext-real Element of REAL
r ^2 is V22() real ext-real set
r * r is V22() real ext-real set
1 - (r ^2) is V22() real ext-real Element of REAL
sqrt (1 - (r ^2)) is V22() real ext-real Element of REAL
1 / (sqrt (1 - (r ^2))) is V22() real ext-real Element of REAL
() | ].(- 1),1.[ is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
dom (sin | ].(- (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)
() . r is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
diff ((sin | ].(- (PI / 2)),(PI / 2).[),x0) is V22() real ext-real Element of REAL
(sin | ].(- (PI / 2)),(PI / 2).[) `| ].(- (PI / 2)),(PI / 2).[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
((sin | ].(- (PI / 2)),(PI / 2).[) `| ].(- (PI / 2)),(PI / 2).[) . x0 is V22() real ext-real Element of REAL
sin `| ].(- (PI / 2)),(PI / 2).[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
(sin `| ].(- (PI / 2)),(PI / 2).[) . x0 is V22() real ext-real Element of REAL
diff (sin,x0) is V22() real ext-real Element of REAL
cos . x0 is V22() real ext-real Element of REAL
(sin | ].(- (PI / 2)),(PI / 2).[) " is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
(sin | [.(- (PI / 2)),(PI / 2).]) | ].(- (PI / 2)),(PI / 2).[ is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
((sin | [.(- (PI / 2)),(PI / 2).]) | ].(- (PI / 2)),(PI / 2).[) " is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
(sin | [.(- (PI / 2)),(PI / 2).]) .: ].(- (PI / 2)),(PI / 2).[ is V70() V71() V72() Element of K19(REAL)
((sin | [.(- (PI / 2)),(PI / 2).]) ") | ((sin | [.(- (PI / 2)),(PI / 2).]) .: ].(- (PI / 2)),(PI / 2).[) is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
(sin | ].(- (PI / 2)),(PI / 2).[) | ].(- (PI / 2)),(PI / 2).[ is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
dom ((sin | ].(- (PI / 2)),(PI / 2).[) ") is V70() V71() V72() Element of K19(REAL)
x0 is V22() real ext-real Element of REAL
(() | ].(- 1),1.[) . r is V22() real ext-real Element of REAL
(r) is V22() real ext-real Element of REAL
diff ((sin | ].(- (PI / 2)),(PI / 2).[),(() . r)) is V22() real ext-real Element of REAL
((sin | ].(- (PI / 2)),(PI / 2).[) `| ].(- (PI / 2)),(PI / 2).[) . (() . r) is V22() real ext-real Element of REAL
(sin `| ].(- (PI / 2)),(PI / 2).[) . (() . r) is V22() real ext-real Element of REAL
diff (sin,(() . r)) is V22() real ext-real Element of REAL
cos . (() . r) is V22() real ext-real Element of REAL
cos (r) is V22() real ext-real Element of REAL
() `| ].(- 1),1.[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
(() `| ].(- 1),1.[) . r is V22() real ext-real Element of REAL
(() | ].(- 1),1.[) `| ].(- 1),1.[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
((() | ].(- 1),1.[) `| ].(- 1),1.[) . r is V22() real ext-real Element of REAL
diff ((() | ].(- 1),1.[),r) is V22() real ext-real Element of REAL
dom (sin | [.(- (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 one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
((sin | [.(- (PI / 2)),(PI / 2).]) | [.(- (PI / 2)),(PI / 2).]) " is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
(sin | [.(- (PI / 2)),(PI / 2).]) .: [.(- (PI / 2)),(PI / 2).] is V70() V71() V72() Element of K19(REAL)
(((sin | [.(- (PI / 2)),(PI / 2).]) | [.(- (PI / 2)),(PI / 2).]) ") | ((sin | [.(- (PI / 2)),(PI / 2).]) .: [.(- (PI / 2)),(PI / 2).]) is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
(cos | [.0,PI.]) " is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
() is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
r is set
() . r is V22() real ext-real Element of REAL
r is set
(r) is set
() . r is V22() real ext-real Element of REAL
() " is Relation-like Function-like set
rng () is V70() V71() V72() Element of K19(REAL)
dom (cos | [.0,PI.]) is V70() V71() V72() Element of K19(REAL)
dom () is V70() V71() V72() Element of K19(REAL)
() * (cos | [.0,PI.]) is Relation-like Function-like one-to-one V46() V47() V48() set
() * (cos | [.0,PI.]) is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
(cos | [.0,PI.]) * () is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
id [.0,PI.] is Relation-like [.0,PI.] -defined [.0,PI.] -valued Function-like one-to-one total V46() V47() V48() Element of K19(K20([.0,PI.],[.0,PI.]))
K20([.0,PI.],[.0,PI.]) is V46() V47() V48() set
K19(K20([.0,PI.],[.0,PI.])) is set
(cos | [.0,PI.]) * () is Relation-like Function-like one-to-one V46() V47() V48() set
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
cos (r) is V22() real ext-real Element of REAL
cos . (() . r) is V22() real ext-real Element of REAL
(cos | [.0,PI.]) . (() . r) is V22() real ext-real set
(id [.(- 1),1.]) . r is V22() real ext-real Element of REAL
r is V22() real ext-real set
cos r is V22() real ext-real set
((cos r)) is V22() real ext-real Element of REAL
() . (cos r) is V22() real ext-real Element of REAL
dom (cos | [.0,PI.]) is V70() V71() V72() Element of K19(REAL)
cos . r is V22() real ext-real Element of REAL
() . (cos . r) is V22() real ext-real Element of REAL
(cos | [.0,PI.]) . r is V22() real ext-real Element of REAL
() . ((cos | [.0,PI.]) . r) is V22() real ext-real Element of REAL
(id [.0,PI.]) . r is V22() real ext-real Element of REAL
((- 1)) is V22() real ext-real Element of REAL
() . (- 1) is V22() real ext-real Element of REAL
(0) is V22() real ext-real Element of REAL
() . 0 is V22() real ext-real Element of REAL
(1) is V22() real ext-real Element of REAL
() . 1 is V22() real ext-real Element of REAL
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
- r is V22() real ext-real set
((- r)) is V22() real ext-real Element of REAL
() . (- r) is V22() real ext-real Element of REAL
PI - ((- r)) is V22() real ext-real Element of REAL
- (- 1) is non empty V22() real ext-real positive non negative integer Element of REAL
0 + ((- r)) is V22() real ext-real Element of REAL
PI + 0 is non empty V22() real ext-real positive non negative Element of REAL
PI + ((- r)) is V22() real ext-real Element of REAL
(- 1) * (- r) is V22() real ext-real Element of REAL
cos ((- r)) is V22() real ext-real Element of REAL
(cos PI) * (cos ((- r))) is V22() real ext-real Element of REAL
sin ((- r)) is V22() real ext-real Element of REAL
(sin PI) * (sin ((- r))) is V22() real ext-real Element of REAL
((cos PI) * (cos ((- r)))) + ((sin PI) * (sin ((- r)))) is V22() real ext-real Element of REAL
cos (PI - ((- r))) is V22() real ext-real Element of REAL
r is V22() real ext-real set
r ^2 is V22() real ext-real set
r * r is V22() real ext-real set
g is V22() real ext-real set
g ^2 is V22() real ext-real set
g * g is V22() real ext-real set
(g ^2) + (r ^2) is V22() real ext-real set
(g) is V22() real ext-real Element of REAL
() . g is V22() real ext-real Element of REAL
sin (g) is V22() real ext-real Element of REAL
sin . (g) is V22() real ext-real Element of REAL
(sin . (g)) ^2 is V22() real ext-real Element of REAL
(sin . (g)) * (sin . (g)) is V22() real ext-real set
cos . (g) is V22() real ext-real Element of REAL
(cos . (g)) ^2 is V22() real ext-real Element of REAL
(cos . (g)) * (cos . (g)) is V22() real ext-real set
((sin . (g)) ^2) + ((cos . (g)) ^2) is V22() real ext-real Element of REAL
1 - ((cos . (g)) ^2) is V22() real ext-real Element of REAL
cos (g) is V22() real ext-real Element of REAL
(cos (g)) ^2 is V22() real ext-real Element of REAL
(cos (g)) * (cos (g)) is V22() real ext-real set
1 - ((cos (g)) ^2) is V22() real ext-real Element of REAL
1 - (g ^2) is V22() real ext-real Element of REAL
- r is V22() real ext-real set
- (- r) is V22() real ext-real set
- (- (- r)) is V22() real ext-real set
r is V22() real ext-real set
r ^2 is V22() real ext-real set
r * r is V22() real ext-real set
- r is V22() real ext-real set
g is V22() real ext-real set
g ^2 is V22() real ext-real set
g * g is V22() real ext-real set
(g ^2) + (r ^2) is V22() real ext-real set
(g) is V22() real ext-real Element of REAL
() . g is V22() real ext-real Element of REAL
sin (g) is V22() real ext-real Element of REAL
sin . (g) is V22() real ext-real Element of REAL
(sin . (g)) ^2 is V22() real ext-real Element of REAL
(sin . (g)) * (sin . (g)) is V22() real ext-real set
cos . (g) is V22() real ext-real Element of REAL
(cos . (g)) ^2 is V22() real ext-real Element of REAL
(cos . (g)) * (cos . (g)) is V22() real ext-real set
((sin . (g)) ^2) + ((cos . (g)) ^2) is V22() real ext-real Element of REAL
1 - ((cos . (g)) ^2) is V22() real ext-real Element of REAL
cos (g) is V22() real ext-real Element of REAL
(cos (g)) ^2 is V22() real ext-real Element of REAL
(cos (g)) * (cos (g)) is V22() real ext-real set
1 - ((cos (g)) ^2) is V22() real ext-real Element of REAL
1 - (g ^2) is V22() real ext-real Element of REAL
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
sin (r) is V22() real ext-real Element of REAL
r ^2 is V22() real ext-real set
r * r is V22() real ext-real set
1 - (r ^2) is V22() real ext-real Element of REAL
sqrt (1 - (r ^2)) is V22() real ext-real Element of REAL
(r ^2) + 0 is V22() real ext-real Element of REAL
1 ^2 is V22() real ext-real Element of REAL
1 * 1 is non empty V22() real ext-real positive non negative integer set
(sqrt (1 - (r ^2))) ^2 is V22() real ext-real Element of REAL
(sqrt (1 - (r ^2))) * (sqrt (1 - (r ^2))) is V22() real ext-real set
(r ^2) + ((sqrt (1 - (r ^2))) ^2) is V22() real ext-real Element of REAL
(r ^2) + (1 - (r ^2)) is V22() real ext-real Element of REAL
() | [.(- 1),1.] is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
(cos | [.0,PI.]) .: [.0,PI.] is V70() V71() V72() Element of K19(REAL)
(cos | [.0,PI.]) | [.0,PI.] is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
((cos | [.0,PI.]) | [.0,PI.]) " is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
(((cos | [.0,PI.]) | [.0,PI.]) ") | ((cos | [.0,PI.]) .: [.0,PI.]) is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
r is V22() real ext-real set
diff ((),r) is V22() real ext-real Element of REAL
r ^2 is V22() real ext-real set
r * r is V22() real ext-real set
1 - (r ^2) is V22() real ext-real Element of REAL
sqrt (1 - (r ^2)) is V22() real ext-real Element of REAL
1 / (sqrt (1 - (r ^2))) is V22() real ext-real Element of REAL
- (1 / (sqrt (1 - (r ^2)))) is V22() real ext-real Element of REAL
() | ].(- 1),1.[ is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
dom (cos | ].0,PI.[) is V70() V71() V72() Element of K19(REAL)
].0,PI.[ /\ REAL is V70() V71() V72() Element of K19(REAL)
() . r is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
sin . x0 is V22() real ext-real Element of REAL
- (sin . x0) is V22() real ext-real Element of REAL
- (- (sin . x0)) is V22() real ext-real Element of REAL
diff ((cos | ].0,PI.[),x0) is V22() real ext-real Element of REAL
(cos | ].0,PI.[) `| ].0,PI.[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
((cos | ].0,PI.[) `| ].0,PI.[) . x0 is V22() real ext-real Element of REAL
cos `| ].0,PI.[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
(cos `| ].0,PI.[) . x0 is V22() real ext-real Element of REAL
diff (cos,x0) is V22() real ext-real Element of REAL
(cos | ].0,PI.[) " is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
(cos | [.0,PI.]) | ].0,PI.[ is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
((cos | [.0,PI.]) | ].0,PI.[) " is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
(cos | [.0,PI.]) .: ].0,PI.[ is V70() V71() V72() Element of K19(REAL)
((cos | [.0,PI.]) ") | ((cos | [.0,PI.]) .: ].0,PI.[) is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
(cos | ].0,PI.[) | ].0,PI.[ is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
dom ((cos | ].0,PI.[) ") is V70() V71() V72() Element of K19(REAL)
x0 is V22() real ext-real Element of REAL
(() | ].(- 1),1.[) . r is V22() real ext-real Element of REAL
(r) is V22() real ext-real Element of REAL
diff ((cos | ].0,PI.[),(() . r)) is V22() real ext-real Element of REAL
((cos | ].0,PI.[) `| ].0,PI.[) . (() . r) is V22() real ext-real Element of REAL
(cos `| ].0,PI.[) . (() . r) is V22() real ext-real Element of REAL
diff (cos,(() . r)) is V22() real ext-real Element of REAL
sin . (() . r) is V22() real ext-real Element of REAL
- (sin . (() . r)) is V22() real ext-real Element of REAL
sin (r) is V22() real ext-real Element of REAL
- (sin (r)) is V22() real ext-real Element of REAL
- (sqrt (1 - (r ^2))) is V22() real ext-real Element of REAL
() `| ].(- 1),1.[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
(() `| ].(- 1),1.[) . r is V22() real ext-real Element of REAL
(() | ].(- 1),1.[) `| ].(- 1),1.[ is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of K19(K20(REAL,REAL))
((() | ].(- 1),1.[) `| ].(- 1),1.[) . r is V22() real ext-real Element of REAL
diff ((() | ].(- 1),1.[),r) is V22() real ext-real Element of REAL
1 / (- (sqrt (1 - (r ^2)))) is V22() real ext-real Element of REAL
(- 1) / (sqrt (1 - (r ^2))) is V22() real ext-real Element of REAL
dom (cos | [.0,PI.]) is V70() V71() V72() Element of K19(REAL)
(cos | [.0,PI.]) | [.0,PI.] is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
((cos | [.0,PI.]) | [.0,PI.]) " is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
(cos | [.0,PI.]) .: [.0,PI.] is V70() V71() V72() Element of K19(REAL)
(((cos | [.0,PI.]) | [.0,PI.]) ") | ((cos | [.0,PI.]) .: [.0,PI.]) is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of K19(K20(REAL,REAL))
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
(r) + (r) is V22() real ext-real Element of REAL
(- (PI / 2)) + (PI / 2) is V22() real ext-real Element of REAL
(r) - (PI / 2) is V22() real ext-real Element of REAL
- ((r) - (PI / 2)) is V22() real ext-real Element of REAL
- (- (PI / 2)) is V22() real ext-real Element of REAL
(PI / 2) + (PI / 2) is non empty V22() real ext-real positive non negative Element of REAL
cos (r) is V22() real ext-real Element of REAL
(sin (PI / 2)) * (cos (r)) is V22() real ext-real Element of REAL
sin (r) is V22() real ext-real Element of REAL
(cos (PI / 2)) * (sin (r)) is V22() real ext-real Element of REAL
((sin (PI / 2)) * (cos (r))) - ((cos (PI / 2)) * (sin (r))) is V22() real ext-real Element of REAL
(PI / 2) - (r) is V22() real ext-real Element of REAL
sin ((PI / 2) - (r)) is V22() real ext-real Element of REAL
r is V22() real ext-real set
- r is V22() real ext-real set
((- r)) is V22() real ext-real Element of REAL
() . (- r) is V22() real ext-real Element of REAL
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
((- r)) - (r) is V22() real ext-real Element of REAL
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
(r) + (r) is V22() real ext-real Element of REAL
(PI / 2) + 0 is non empty V22() real ext-real positive non negative Element of REAL
- (- 1) is non empty V22() real ext-real positive non negative integer Element of REAL
- (- r) is V22() real ext-real set
((- (- r))) is V22() real ext-real Element of REAL
() . (- (- r)) is V22() real ext-real Element of REAL
PI - ((- (- r))) is V22() real ext-real Element of REAL
(r) + (PI / 2) is V22() real ext-real Element of REAL
r is V22() real ext-real set
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
- r is V22() real ext-real set
((- r)) is V22() real ext-real Element of REAL
() . (- r) is V22() real ext-real Element of REAL
(r) - ((- r)) is V22() real ext-real Element of REAL
(r) is V22() real ext-real Element of REAL
() . r is V22() real ext-real Element of REAL
(r) + (r) is V22() real ext-real Element of REAL
(PI / 2) + 0 is non empty V22() real ext-real positive non negative Element of REAL
- (- 1) is non empty V22() real ext-real positive non negative integer Element of REAL
- (- r) is V22() real ext-real set
((- (- r))) is V22() real ext-real Element of REAL
() . (- (- r)) is V22() real ext-real Element of REAL
- ((- (- r))) is V22() real ext-real Element of REAL
(r) - (PI / 2) is V22() real ext-real Element of REAL