:: 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

(PI / 2) + H

[.((- (PI / 2)) + H

((3 / 2) * PI) + H

[.((PI / 2) + H

PI + H

[.H

(2 * PI) + H

[.(PI + H

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

0 + H

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

r - H

H

(PI + H

- g is V22() real ext-real integer set

(2 * PI) * (- g) is V22() real ext-real Element of REAL

r + H

sin . (r + H

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

(2 * PI) + H

r - H

(PI + H

((2 * PI) + H

- g is V22() real ext-real integer set

(2 * PI) * (- g) is V22() real ext-real Element of REAL

r + H

sin . (r + H

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

(PI / 2) + H

((PI / 2) + H

r + (PI / 2) is V22() real ext-real Element of REAL

PI + H

sin (r + (PI / 2)) is V22() real ext-real Element of REAL

((- (PI / 2)) + H

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

((3 / 2) * PI) + H

r + (PI / 2) is V22() real ext-real Element of REAL

((PI / 2) + H

PI + H

(((3 / 2) * PI) + H

(2 * PI) + H

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

(2 * PI) + H

r - PI is V22() real ext-real Element of REAL

(((3 / 2) * PI) + H

(PI / 2) + H

PI + H

((2 * PI) + H

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

PI + H

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

0 + H

(- (PI / 2)) + H

(PI / 2) + H

((3 / 2) * PI) + H

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

h + H

(2 * PI) + H

(PI / 2) + H

((3 / 2) * PI) + H

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

h + H

(2 * PI) + H

(PI / 2) + H

((3 / 2) * PI) + H

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

h + H

(2 * PI) + H

PI + H

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

h + H

(2 * PI) + H

PI + H

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

H

r - H

((PI / 2) + H

sin (r - H

- g is V22() real ext-real integer set

(2 * PI) * (- g) is V22() real ext-real Element of REAL

r + H

sin (r + H

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

H

r - H

(((3 / 2) * PI) + H

sin (r - H

- g is V22() real ext-real integer set

(2 * PI) * (- g) is V22() real ext-real Element of REAL

r + H

sin (r + H

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

(2 * PI) + H

r - H

(((3 / 2) * PI) + H

((2 * PI) + H

sin (r - H

- g is V22() real ext-real integer set

(2 * PI) * (- g) is V22() real ext-real Element of REAL

r + H

sin (r + H

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

(2 * PI) + H

r - H

((PI / 2) + H

((2 * PI) + H

sin (r - H

- g is V22() real ext-real integer set

(2 * PI) * (- g) is V22() real ext-real Element of REAL

r + H

sin (r + H

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

r - H

H

((2 * PI) + H

cos (r - H

- g is V22() real ext-real integer set

(2 * PI) * (- g) is V22() real ext-real Element of REAL

r + H

cos (r + H

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

H

r - H

(PI + H

cos (r - H

- g is V22() real ext-real integer set

(2 * PI) * (- g) is V22() real ext-real Element of REAL

r + H

cos (r + H

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

(2 * PI) + H

r - H

(PI + H

((2 * PI) + H

cos (r - H

- g is V22() real ext-real integer set

(2 * PI) * (- g) is V22() real ext-real Element of REAL

r + H

cos (r + H

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))/] / 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

(PI / 2) - (PI / 2) is V22() real ext-real Element of REAL

((PI / 2) + H

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

(((3 / 2) * PI) + H

(- (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))/] / 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

((PI / 2) + H

(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

((3 / 2) * PI) - ((3 / 2) * PI) is V22() real ext-real Element of REAL

(((3 / 2) * PI) + H

(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))/] / 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

(PI + H

0 - PI is non empty V22() real ext-real non positive negative Element of REAL

H

- 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))/] / 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

(PI + H

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

f is V22() real ext-real set

f + H

[.(h + H

g + (2 * PI) is V22() real ext-real Element of REAL

(f + H

(h + H

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

f + H

[.(h + H

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

f is V22() real ext-real set

f + H

[.(h + H

[.(h + H

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

f + H

[.(h + H

[.(h + H

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

f is V22() real ext-real set

f + H

[.(h + H

g - (2 * PI) is V22() real ext-real Element of REAL

(f + H

(h + H

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

f + H

[.(h + H

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

f is V22() real ext-real set

f + H

[.(h + H

[.(h + H

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

f + H

[.(h + H

[.(h + H

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

(PI / 2) + H

[.((- (PI / 2)) + H

sin | [.((- (PI / 2)) + H

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

(PI / 2) + H

[.((- (PI / 2)) + H

sin | [.((- (PI / 2)) + H

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

(PI / 2) + H

[.((- (PI / 2)) + H

sin | [.((- (PI / 2)) + H

(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

(PI / 2) + H

[.((- (PI / 2)) + H

x is V22() real ext-real Element of REAL

[.((- (PI / 2)) + H

s is V22() real ext-real Element of REAL

x + (2 * PI) is V22() real ext-real Element of REAL

[.((- (PI / 2)) + H

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

(PI / 2) + H

[.((- (PI / 2)) + H

x is V22() real ext-real Element of REAL

[.((- (PI / 2)) + H

s is V22() real ext-real Element of REAL

x - (2 * PI) is V22() real ext-real Element of REAL

[.((- (PI / 2)) + H

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

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

((3 / 2) * PI) + H

[.((PI / 2) + H

sin | [.((PI / 2) + H

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

((3 / 2) * PI) + H

[.((PI / 2) + H

sin | [.((PI / 2) + H

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

((3 / 2) * PI) + H

[.((PI / 2) + H

sin | [.((PI