:: FUNCT_9 semantic presentation

REAL is non empty V45() V134() V135() V136() V140() set
NAT is V134() V135() V136() V137() V138() V139() V140() Element of K6(REAL)
K6(REAL) is set
omega is V134() V135() V136() V137() V138() V139() V140() set
K6(omega) is set
K6(NAT) is set
RAT is non empty V45() V134() V135() V136() V137() V140() set
1 is non empty ordinal natural complex real V30() V31() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT
K7(1,1) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
INT is non empty V45() V134() V135() V136() V137() V138() V140() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K7(K7(REAL,REAL),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty ordinal natural complex real V30() V31() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT
K7(2,2) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K7(K7(2,2),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(K7(2,2),REAL)) is set
COMPLEX is non empty V45() V134() V140() set
K6(K7(REAL,REAL)) is set
K312(2) is V158() L15()
the U1 of K312(2) is set
{} is set
the empty Relation-like non-empty empty-yielding RAT -valued complex-valued ext-real-valued real-valued natural-valued V134() V135() V136() V137() V138() V139() V140() set is empty Relation-like non-empty empty-yielding RAT -valued complex-valued ext-real-valued real-valued natural-valued V134() V135() V136() V137() V138() V139() V140() set
{{},1} is set
K7(NAT,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(NAT,REAL)) is set
K7(NAT,COMPLEX) is Relation-like complex-valued set
K6(K7(NAT,COMPLEX)) is set
K7(COMPLEX,COMPLEX) is Relation-like complex-valued set
K6(K7(COMPLEX,COMPLEX)) is set
sin is Relation-like Function-like V27( REAL , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
K411(REAL,sin) is V134() V135() V136() Element of K6(REAL)
cos is Relation-like Function-like V27( REAL , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
K411(REAL,cos) is V134() V135() V136() Element of K6(REAL)
PI is non empty complex real V30() V31() V32() Element of REAL
2 * PI is non empty complex real V30() V31() V32() Element of REAL
PI / 2 is non empty complex real V30() V31() V32() Element of REAL
2 " is non empty complex real V30() V31() V32() set
PI * (2 ") is non empty complex real V30() V31() V32() set
0 is ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT
{0} is V134() V135() V136() V137() V138() V139() set
t is complex real V30() set
c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom c₂ is set
i is complex real V30() set
i + t is complex real V30() set
i - t is complex real V30() set
- t is complex real V30() set
i + (- t) is complex real V30() set
c₂ . i is complex real V30() set
c₂ . (i + t) is complex real V30() set
(i - t) + t is complex real V30() set
i is complex real V30() set
i + t is complex real V30() set
i - t is complex real V30() set
- t is complex real V30() set
i + (- t) is complex real V30() set
c₂ . i is complex real V30() set
c₂ . (i + t) is complex real V30() set
i is complex real V30() set
i + t is complex real V30() set
c₂ . i is complex real V30() set
c₂ . (i + t) is complex real V30() set
(i + t) - t is complex real V30() set
- t is complex real V30() set
(i + t) + (- t) is complex real V30() set
t is complex real V30() set
c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
i is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ + i is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom c₂ is set
k is complex real V30() set
k + t is complex real V30() set
k - t is complex real V30() set
- t is complex real V30() set
k + (- t) is complex real V30() set
c₂ . k is complex real V30() set
c₂ . (k + t) is complex real V30() set
dom (c₂ + i) is set
k is complex real V30() set
k + t is complex real V30() set
k - t is complex real V30() set
- t is complex real V30() set
k + (- t) is complex real V30() set
(c₂ + i) . k is complex real V30() set
(c₂ + i) . (k + t) is complex real V30() set
dom i is set
(dom c₂) /\ (dom i) is set
c₂ . k is complex real V30() set
i . k is complex real V30() set
(c₂ . k) + (i . k) is complex real V30() set
c₂ . (k + t) is complex real V30() set
(c₂ . (k + t)) + (i . k) is complex real V30() set
i . (k + t) is complex real V30() set
(c₂ . (k + t)) + (i . (k + t)) is complex real V30() set
t is complex real V30() set
c₂ is complex real V30() set
REAL --> c₂ is non empty Relation-like REAL -defined Function-like constant total V27( REAL ,{c₂}) complex-valued ext-real-valued real-valued Element of K6(K7(REAL,{c₂}))
{c₂} is V134() V135() V136() set
K7(REAL,{c₂}) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(REAL,{c₂})) is set
dom (REAL --> c₂) is non empty set
k is complex real V30() set
k + t is complex real V30() set
(REAL --> c₂) . k is complex real V30() set
(REAL --> c₂) . (k + t) is complex real V30() set
t is complex real V30() set
c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
i is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ - i is Relation-like Function-like complex-valued ext-real-valued real-valued set
- i is Relation-like Function-like complex-valued ext-real-valued real-valued set
- 1 is non empty complex real V30() V31() V32() integer set
(- 1) (#) i is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ + (- i) is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom c₂ is set
k is complex real V30() set
k + t is complex real V30() set
k - t is complex real V30() set
- t is complex real V30() set
k + (- t) is complex real V30() set
c₂ . k is complex real V30() set
c₂ . (k + t) is complex real V30() set
dom (c₂ - i) is set
k is complex real V30() set
k + t is complex real V30() set
k - t is complex real V30() set
- t is complex real V30() set
k + (- t) is complex real V30() set
(c₂ - i) . k is complex real V30() set
(c₂ - i) . (k + t) is complex real V30() set
dom i is set
(dom c₂) /\ (dom i) is set
c₂ . k is complex real V30() set
i . k is complex real V30() set
(c₂ . k) - (i . k) is complex real V30() set
- (i . k) is complex real V30() set
(c₂ . k) + (- (i . k)) is complex real V30() set
c₂ . (k + t) is complex real V30() set
(c₂ . (k + t)) - (i . k) is complex real V30() set
(c₂ . (k + t)) + (- (i . k)) is complex real V30() set
i . (k + t) is complex real V30() set
(c₂ . (k + t)) - (i . (k + t)) is complex real V30() set
- (i . (k + t)) is complex real V30() set
(c₂ . (k + t)) + (- (i . (k + t))) is complex real V30() set
t is complex real V30() set
c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
i is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ (#) i is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom c₂ is set
k is complex real V30() set
k + t is complex real V30() set
k - t is complex real V30() set
- t is complex real V30() set
k + (- t) is complex real V30() set
c₂ . k is complex real V30() set
c₂ . (k + t) is complex real V30() set
dom (c₂ (#) i) is set
k is complex real V30() set
k + t is complex real V30() set
k - t is complex real V30() set
- t is complex real V30() set
k + (- t) is complex real V30() set
(c₂ (#) i) . k is complex real V30() set
(c₂ (#) i) . (k + t) is complex real V30() set
dom i is set
(dom c₂) /\ (dom i) is set
c₂ . k is complex real V30() set
i . k is complex real V30() set
(c₂ . k) * (i . k) is complex real V30() set
c₂ . (k + t) is complex real V30() set
(c₂ . (k + t)) * (i . k) is complex real V30() set
i . (k + t) is complex real V30() set
(c₂ . (k + t)) * (i . (k + t)) is complex real V30() set
t is complex real V30() set
c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
i is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ /" i is Relation-like Function-like complex-valued ext-real-valued real-valued set
i " is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ (#) (i ") is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom c₂ is set
k is complex real V30() set
k + t is complex real V30() set
k - t is complex real V30() set
- t is complex real V30() set
k + (- t) is complex real V30() set
c₂ . k is complex real V30() set
c₂ . (k + t) is complex real V30() set
dom (c₂ /" i) is set
k is complex real V30() set
k + t is complex real V30() set
k - t is complex real V30() set
- t is complex real V30() set
k + (- t) is complex real V30() set
(c₂ /" i) . k is complex real V30() set
(c₂ /" i) . (k + t) is complex real V30() set
dom i is set
(dom c₂) /\ (dom i) is set
c₂ . k is complex real V30() set
i . k is complex real V30() set
(c₂ . k) / (i . k) is complex real V30() set
(i . k) " is complex real V30() set
(c₂ . k) * ((i . k) ") is complex real V30() set
c₂ . (k + t) is complex real V30() set
(c₂ . (k + t)) / (i . k) is complex real V30() set
(c₂ . (k + t)) * ((i . k) ") is complex real V30() set
i . (k + t) is complex real V30() set
(c₂ . (k + t)) / (i . (k + t)) is complex real V30() set
(i . (k + t)) " is complex real V30() set
(c₂ . (k + t)) * ((i . (k + t)) ") is complex real V30() set
t is complex real V30() set
c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
- c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
- 1 is non empty complex real V30() V31() V32() integer set
(- 1) (#) c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom c₂ is set
i is complex real V30() set
i + t is complex real V30() set
i - t is complex real V30() set
- t is complex real V30() set
i + (- t) is complex real V30() set
c₂ . i is complex real V30() set
c₂ . (i + t) is complex real V30() set
dom (- c₂) is set
i is complex real V30() set
i + t is complex real V30() set
i - t is complex real V30() set
- t is complex real V30() set
i + (- t) is complex real V30() set
(- c₂) . i is complex real V30() set
(- c₂) . (i + t) is complex real V30() set
c₂ . i is complex real V30() set
- (c₂ . i) is complex real V30() set
c₂ . (i + t) is complex real V30() set
- (c₂ . (i + t)) is complex real V30() set
t is complex real V30() set
c₂ is complex real V30() set
i is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ (#) i is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom i is set
k is complex real V30() set
k + t is complex real V30() set
k - t is complex real V30() set
- t is complex real V30() set
k + (- t) is complex real V30() set
i . k is complex real V30() set
i . (k + t) is complex real V30() set
dom (c₂ (#) i) is set
k is complex real V30() set
k + t is complex real V30() set
k - t is complex real V30() set
- t is complex real V30() set
k + (- t) is complex real V30() set
(c₂ (#) i) . k is complex real V30() set
(c₂ (#) i) . (k + t) is complex real V30() set
i . k is complex real V30() set
c₂ * (i . k) is complex real V30() set
i . (k + t) is complex real V30() set
c₂ * (i . (k + t)) is complex real V30() set
t is complex real V30() set
c₂ is complex real V30() set
i is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ + i is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom i is set
k is complex real V30() set
k + t is complex real V30() set
k - t is complex real V30() set
- t is complex real V30() set
k + (- t) is complex real V30() set
i . k is complex real V30() set
i . (k + t) is complex real V30() set
dom (c₂ + i) is set
k is complex real V30() set
k + t is complex real V30() set
k - t is complex real V30() set
- t is complex real V30() set
k + (- t) is complex real V30() set
(c₂ + i) . k is complex real V30() set
(c₂ + i) . (k + t) is complex real V30() set
i . k is complex real V30() set
c₂ + (i . k) is complex real V30() set
i . (k + t) is complex real V30() set
c₂ + (i . (k + t)) is complex real V30() set
t is complex real V30() set
i is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ is complex real V30() set
i - c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
- c₂ is complex real V30() set
(- c₂) + i is Relation-like Function-like complex-valued ext-real-valued real-valued set
t is complex real V30() set
c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
|.c₂.| is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom c₂ is set
i is complex real V30() set
i + t is complex real V30() set
i - t is complex real V30() set
- t is complex real V30() set
i + (- t) is complex real V30() set
c₂ . i is complex real V30() set
c₂ . (i + t) is complex real V30() set
dom |.c₂.| is set
i is complex real V30() set
i + t is complex real V30() set
i - t is complex real V30() set
- t is complex real V30() set
i + (- t) is complex real V30() set
|.c₂.| . i is complex real V30() set
|.c₂.| . (i + t) is complex real V30() set
c₂ . i is complex real V30() set
|.(c₂ . i).| is complex real V30() Element of REAL
c₂ . (i + t) is complex real V30() set
|.(c₂ . (i + t)).| is complex real V30() Element of REAL
t is complex real V30() set
c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ " is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom c₂ is set
i is complex real V30() set
i + t is complex real V30() set
i - t is complex real V30() set
- t is complex real V30() set
i + (- t) is complex real V30() set
c₂ . i is complex real V30() set
c₂ . (i + t) is complex real V30() set
dom (c₂ ") is set
i is complex real V30() set
i + t is complex real V30() set
i - t is complex real V30() set
- t is complex real V30() set
i + (- t) is complex real V30() set
(c₂ ") . i is complex real V30() set
(c₂ ") . (i + t) is complex real V30() set
c₂ . i is complex real V30() set
(c₂ . i) " is complex real V30() set
c₂ . (i + t) is complex real V30() set
(c₂ . (i + t)) " is complex real V30() set
t is complex real V30() set
c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ ^2 is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ (#) c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
t is complex real V30() set
c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom c₂ is set
i is complex real V30() set
c₂ . i is complex real V30() set
i - t is complex real V30() set
- t is complex real V30() set
i + (- t) is complex real V30() set
c₂ . (i - t) is complex real V30() set
i + t is complex real V30() set
(i - t) + t is complex real V30() set
c₂ . ((i - t) + t) is complex real V30() set
t is complex real V30() set
- t is complex real V30() set
c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom c₂ is set
i is complex real V30() set
i + (- t) is complex real V30() set
i - (- t) is complex real V30() set
- (- t) is complex real V30() set
i + (- (- t)) is complex real V30() set
c₂ . i is complex real V30() set
c₂ . (i + (- t)) is complex real V30() set
i + t is complex real V30() set
i - t is complex real V30() set
t is complex real V30() set
c₂ is complex real V30() set
t + c₂ is complex real V30() set
i is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom i is set
k is complex real V30() set
k + (t + c₂) is complex real V30() set
k - (t + c₂) is complex real V30() set
- (t + c₂) is complex real V30() set
k + (- (t + c₂)) is complex real V30() set
i . k is complex real V30() set
i . (k + (t + c₂)) is complex real V30() set
k + t is complex real V30() set
k - t is complex real V30() set
- t is complex real V30() set
k + (- t) is complex real V30() set
(k + t) + c₂ is complex real V30() set
(k - t) - c₂ is complex real V30() set
- c₂ is complex real V30() set
(k - t) + (- c₂) is complex real V30() set
i . (k + t) is complex real V30() set
i . ((k + t) + c₂) is complex real V30() set
t is complex real V30() set
c₂ is complex real V30() set
t - c₂ is complex real V30() set
- c₂ is complex real V30() set
t + (- c₂) is complex real V30() set
i is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom i is set
k is complex real V30() set
k + (t - c₂) is complex real V30() set
k - (t - c₂) is complex real V30() set
- (t - c₂) is complex real V30() set
k + (- (t - c₂)) is complex real V30() set
i . k is complex real V30() set
i . (k + (t - c₂)) is complex real V30() set
k + t is complex real V30() set
k - t is complex real V30() set
- t is complex real V30() set
k + (- t) is complex real V30() set
(k + t) - c₂ is complex real V30() set
(k + t) + (- c₂) is complex real V30() set
(k - t) + c₂ is complex real V30() set
k - c₂ is complex real V30() set
k + (- c₂) is complex real V30() set
(k - c₂) + t is complex real V30() set
i . ((k - c₂) + t) is complex real V30() set
i . (k - c₂) is complex real V30() set
(k - c₂) + c₂ is complex real V30() set
i . ((k - c₂) + c₂) is complex real V30() set
t is complex real V30() set
2 * t is complex real V30() Element of REAL
c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom c₂ is set
i is complex real V30() set
i + (2 * t) is complex real V30() Element of REAL
i - (2 * t) is complex real V30() Element of REAL
- (2 * t) is complex real V30() set
i + (- (2 * t)) is complex real V30() set
c₂ . i is complex real V30() set
c₂ . (i + (2 * t)) is complex real V30() set
i + t is complex real V30() set
i - t is complex real V30() set
- t is complex real V30() set
i + (- t) is complex real V30() set
(i + t) + t is complex real V30() set
(i - t) - t is complex real V30() set
(i - t) + (- t) is complex real V30() set
c₂ . ((i + t) + t) is complex real V30() set
(i + t) - t is complex real V30() set
(i + t) + (- t) is complex real V30() set
c₂ . ((i + t) - t) is complex real V30() set
t is complex real V30() set
c₂ is complex real V30() set
t + c₂ is complex real V30() set
i is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom i is set
k is complex real V30() set
k + (t + c₂) is complex real V30() set
k - (t + c₂) is complex real V30() set
- (t + c₂) is complex real V30() set
k + (- (t + c₂)) is complex real V30() set
i . k is complex real V30() set
i . (k + (t + c₂)) is complex real V30() set
k + t is complex real V30() set
k - t is complex real V30() set
- t is complex real V30() set
k + (- t) is complex real V30() set
k + c₂ is complex real V30() set
k - c₂ is complex real V30() set
- c₂ is complex real V30() set
k + (- c₂) is complex real V30() set
(k + t) + c₂ is complex real V30() set
(k - t) - c₂ is complex real V30() set
(k - t) + (- c₂) is complex real V30() set
(k + c₂) + t is complex real V30() set
i . ((k + c₂) + t) is complex real V30() set
(k + c₂) - c₂ is complex real V30() set
(k + c₂) + (- c₂) is complex real V30() set
i . ((k + c₂) - c₂) is complex real V30() set
t is complex real V30() set
c₂ is complex real V30() set
t - c₂ is complex real V30() set
- c₂ is complex real V30() set
t + (- c₂) is complex real V30() set
i is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom i is set
k is complex real V30() set
k + (t - c₂) is complex real V30() set
k - (t - c₂) is complex real V30() set
- (t - c₂) is complex real V30() set
k + (- (t - c₂)) is complex real V30() set
i . k is complex real V30() set
i . (k + (t - c₂)) is complex real V30() set
k + t is complex real V30() set
k - t is complex real V30() set
- t is complex real V30() set
k + (- t) is complex real V30() set
k + c₂ is complex real V30() set
k - c₂ is complex real V30() set
k + (- c₂) is complex real V30() set
(k + t) - c₂ is complex real V30() set
(k + t) + (- c₂) is complex real V30() set
(k - t) + c₂ is complex real V30() set
(k - c₂) + t is complex real V30() set
i . ((k - c₂) + t) is complex real V30() set
(k - c₂) + c₂ is complex real V30() set
i . ((k - c₂) + c₂) is complex real V30() set
t is complex real V30() set
2 * t is complex real V30() Element of REAL
c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom c₂ is set
i is complex real V30() set
i + (2 * t) is complex real V30() Element of REAL
i - (2 * t) is complex real V30() Element of REAL
- (2 * t) is complex real V30() set
i + (- (2 * t)) is complex real V30() set
c₂ . i is complex real V30() set
c₂ . (i + (2 * t)) is complex real V30() set
i + t is complex real V30() set
i - t is complex real V30() set
- t is complex real V30() set
i + (- t) is complex real V30() set
(i + t) + t is complex real V30() set
(i - t) - t is complex real V30() set
(i - t) + (- t) is complex real V30() set
c₂ . ((i + t) + t) is complex real V30() set
c₂ . (i + t) is complex real V30() set
(c₂ . (i + t)) " is complex real V30() set
(c₂ . i) " is complex real V30() set
((c₂ . i) ") " is complex real V30() set
dom sin is set
t is complex real V30() set
t + (2 * PI) is complex real V30() Element of REAL
t - (2 * PI) is complex real V30() Element of REAL
- (2 * PI) is non empty complex real V30() V31() V32() set
t + (- (2 * PI)) is complex real V30() set
sin . t is complex real V30() set
sin . (t + (2 * PI)) is complex real V30() Element of REAL
t is non empty complex real V30() set
REAL --> t is non empty Relation-like non-empty REAL -defined Function-like constant total V27( REAL ,{t}) complex-valued ext-real-valued real-valued Element of K6(K7(REAL,{t}))
{t} is V134() V135() V136() set
K7(REAL,{t}) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(REAL,{t})) is set
t is non empty complex real V30() set
c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued (t) set
i is Relation-like Function-like complex-valued ext-real-valued real-valued (t) set
c₂ + i is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ - i is Relation-like Function-like complex-valued ext-real-valued real-valued set
- i is Relation-like Function-like complex-valued ext-real-valued real-valued set
- 1 is non empty complex real V30() V31() V32() integer set
(- 1) (#) i is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ + (- i) is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ (#) i is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ /" i is Relation-like Function-like complex-valued ext-real-valued real-valued set
i " is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ (#) (i ") is Relation-like Function-like complex-valued ext-real-valued real-valued set
t is Relation-like Function-like complex-valued ext-real-valued real-valued () set
- t is Relation-like Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) t is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ is complex real V30() set
t is Relation-like Function-like complex-valued ext-real-valued real-valued () set
c₂ is complex real V30() set
c₂ (#) t is Relation-like Function-like complex-valued ext-real-valued real-valued set
i is complex real V30() set
c₂ + t is Relation-like Function-like complex-valued ext-real-valued real-valued set
i is complex real V30() set
t - c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued set
- c₂ is complex real V30() set
(- c₂) + t is Relation-like Function-like complex-valued ext-real-valued real-valued () set
t is Relation-like Function-like complex-valued ext-real-valued real-valued () set
|.t.| is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ is complex real V30() set
t " is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ is complex real V30() set
t ^2 is Relation-like Function-like complex-valued ext-real-valued real-valued set
t (#) t is Relation-like Function-like complex-valued ext-real-valued real-valued set
c₂ is complex real V30() set
dom cos is set
t is complex real V30() set
t + (2 * PI) is complex real V30() Element of REAL
t - (2 * PI) is complex real V30() Element of REAL
- (2 * PI) is non empty complex real V30() V31() V32() set
t + (- (2 * PI)) is complex real V30() set
cos . t is complex real V30() set
cos . (t + (2 * PI)) is complex real V30() Element of REAL
t is ordinal natural complex real V30() V32() integer set
t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (t + 1) is non empty complex real V30() V31() V32() Element of REAL
0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer set
c₂ + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (c₂ + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
dom sin is set
i is complex real V30() set
sin . i is complex real V30() set
i + ((2 * PI) * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
sin . (i + ((2 * PI) * ((c₂ + 1) + 1))) is complex real V30() Element of REAL
i + ((2 * PI) * (c₂ + 1)) is complex real V30() Element of REAL
sin . (i + ((2 * PI) * (c₂ + 1))) is complex real V30() Element of REAL
(i + ((2 * PI) * (c₂ + 1))) + (2 * PI) is complex real V30() Element of REAL
sin . ((i + ((2 * PI) * (c₂ + 1))) + (2 * PI)) is complex real V30() Element of REAL
i is complex real V30() set
i + ((2 * PI) * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
i - ((2 * PI) * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
- ((2 * PI) * ((c₂ + 1) + 1)) is non empty complex real V30() V31() V32() set
i + (- ((2 * PI) * ((c₂ + 1) + 1))) is complex real V30() set
sin . i is complex real V30() set
sin . (i + ((2 * PI) * ((c₂ + 1) + 1))) is complex real V30() Element of REAL
t is non empty complex real V30() integer set
(2 * PI) * t is non empty complex real V30() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT
- c₂ is complex real V30() V31() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
- t is non empty complex real V30() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (i + 1) is non empty complex real V30() V31() V32() Element of REAL
- ((2 * PI) * (i + 1)) is non empty complex real V30() V31() V32() Element of REAL
t is ordinal natural complex real V30() V32() integer set
t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (t + 1) is non empty complex real V30() V31() V32() Element of REAL
0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer set
c₂ + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (c₂ + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
dom cos is set
i is complex real V30() set
cos . i is complex real V30() set
i + ((2 * PI) * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
cos . (i + ((2 * PI) * ((c₂ + 1) + 1))) is complex real V30() Element of REAL
i + ((2 * PI) * (c₂ + 1)) is complex real V30() Element of REAL
cos . (i + ((2 * PI) * (c₂ + 1))) is complex real V30() Element of REAL
(i + ((2 * PI) * (c₂ + 1))) + (2 * PI) is complex real V30() Element of REAL
cos . ((i + ((2 * PI) * (c₂ + 1))) + (2 * PI)) is complex real V30() Element of REAL
i is complex real V30() set
i + ((2 * PI) * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
i - ((2 * PI) * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
- ((2 * PI) * ((c₂ + 1) + 1)) is non empty complex real V30() V31() V32() set
i + (- ((2 * PI) * ((c₂ + 1) + 1))) is complex real V30() set
cos . i is complex real V30() set
cos . (i + ((2 * PI) * ((c₂ + 1) + 1))) is complex real V30() Element of REAL
t is non empty complex real V30() integer set
(2 * PI) * t is non empty complex real V30() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT
- c₂ is complex real V30() V31() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
- t is non empty complex real V30() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (i + 1) is non empty complex real V30() V31() V32() Element of REAL
- ((2 * PI) * (i + 1)) is non empty complex real V30() V31() V32() Element of REAL
cosec is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
K375(REAL,REAL,sin) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom cosec is set
t is complex real V30() set
t + (2 * PI) is complex real V30() Element of REAL
t - (2 * PI) is complex real V30() Element of REAL
- (2 * PI) is non empty complex real V30() V31() V32() set
t + (- (2 * PI)) is complex real V30() set
cosec . t is complex real V30() set
cosec . (t + (2 * PI)) is complex real V30() set
dom sin is set
sin " {0} is set
(dom sin) \ (sin " {0}) is Element of K6((dom sin))
K6((dom sin)) is set
sin . t is complex real V30() set
sin . (t + (2 * PI)) is complex real V30() Element of REAL
sin . (t - (2 * PI)) is complex real V30() Element of REAL
(t - (2 * PI)) + (2 * PI) is complex real V30() Element of REAL
sin . ((t - (2 * PI)) + (2 * PI)) is complex real V30() Element of REAL
(sin . (t + (2 * PI))) " is complex real V30() Element of REAL
(sin . t) " is complex real V30() set
sec is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
K375(REAL,REAL,cos) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom sec is set
t is complex real V30() set
t + (2 * PI) is complex real V30() Element of REAL
t - (2 * PI) is complex real V30() Element of REAL
- (2 * PI) is non empty complex real V30() V31() V32() set
t + (- (2 * PI)) is complex real V30() set
sec . t is complex real V30() set
sec . (t + (2 * PI)) is complex real V30() set
dom cos is set
cos " {0} is set
(dom cos) \ (cos " {0}) is Element of K6((dom cos))
K6((dom cos)) is set
cos . t is complex real V30() set
cos . (t + (2 * PI)) is complex real V30() Element of REAL
cos . (t - (2 * PI)) is complex real V30() Element of REAL
(t - (2 * PI)) + (2 * PI) is complex real V30() Element of REAL
cos . ((t - (2 * PI)) + (2 * PI)) is complex real V30() Element of REAL
(cos . (t + (2 * PI))) " is complex real V30() Element of REAL
(cos . t) " is complex real V30() set
t is ordinal natural complex real V30() V32() integer set
t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (t + 1) is non empty complex real V30() V31() V32() Element of REAL
0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer set
c₂ + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (c₂ + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
dom sec is set
i is complex real V30() set
i + ((2 * PI) * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
i - ((2 * PI) * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
- ((2 * PI) * ((c₂ + 1) + 1)) is non empty complex real V30() V31() V32() set
i + (- ((2 * PI) * ((c₂ + 1) + 1))) is complex real V30() set
sec . i is complex real V30() set
sec . (i + ((2 * PI) * ((c₂ + 1) + 1))) is complex real V30() set
i + ((2 * PI) * (c₂ + 1)) is complex real V30() Element of REAL
i - ((2 * PI) * (c₂ + 1)) is complex real V30() Element of REAL
- ((2 * PI) * (c₂ + 1)) is non empty complex real V30() V31() V32() set
i + (- ((2 * PI) * (c₂ + 1))) is complex real V30() set
sec . (i + ((2 * PI) * (c₂ + 1))) is complex real V30() set
dom cos is set
cos " {0} is set
(dom cos) \ (cos " {0}) is Element of K6((dom cos))
K6((dom cos)) is set
cos . (i + ((2 * PI) * (c₂ + 1))) is complex real V30() Element of REAL
cos . (i - ((2 * PI) * (c₂ + 1))) is complex real V30() Element of REAL
(i + ((2 * PI) * (c₂ + 1))) + (2 * PI) is complex real V30() Element of REAL
cos . ((i + ((2 * PI) * (c₂ + 1))) + (2 * PI)) is complex real V30() Element of REAL
cos . (i - ((2 * PI) * ((c₂ + 1) + 1))) is complex real V30() Element of REAL
(i - ((2 * PI) * ((c₂ + 1) + 1))) + (2 * PI) is complex real V30() Element of REAL
cos . ((i - ((2 * PI) * ((c₂ + 1) + 1))) + (2 * PI)) is complex real V30() Element of REAL
(cos . ((i + ((2 * PI) * (c₂ + 1))) + (2 * PI))) " is complex real V30() Element of REAL
(cos . (i + ((2 * PI) * (c₂ + 1)))) " is complex real V30() Element of REAL
t is non empty complex real V30() integer set
(2 * PI) * t is non empty complex real V30() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT
- c₂ is complex real V30() V31() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
- t is non empty complex real V30() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (i + 1) is non empty complex real V30() V31() V32() Element of REAL
- ((2 * PI) * (i + 1)) is non empty complex real V30() V31() V32() Element of REAL
t is ordinal natural complex real V30() V32() integer set
t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (t + 1) is non empty complex real V30() V31() V32() Element of REAL
0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer set
c₂ + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (c₂ + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
dom cosec is set
i is complex real V30() set
i + ((2 * PI) * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
i - ((2 * PI) * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
- ((2 * PI) * ((c₂ + 1) + 1)) is non empty complex real V30() V31() V32() set
i + (- ((2 * PI) * ((c₂ + 1) + 1))) is complex real V30() set
cosec . i is complex real V30() set
cosec . (i + ((2 * PI) * ((c₂ + 1) + 1))) is complex real V30() set
i + ((2 * PI) * (c₂ + 1)) is complex real V30() Element of REAL
i - ((2 * PI) * (c₂ + 1)) is complex real V30() Element of REAL
- ((2 * PI) * (c₂ + 1)) is non empty complex real V30() V31() V32() set
i + (- ((2 * PI) * (c₂ + 1))) is complex real V30() set
cosec . (i + ((2 * PI) * (c₂ + 1))) is complex real V30() set
dom sin is set
sin " {0} is set
(dom sin) \ (sin " {0}) is Element of K6((dom sin))
K6((dom sin)) is set
sin . (i + ((2 * PI) * (c₂ + 1))) is complex real V30() Element of REAL
sin . (i - ((2 * PI) * (c₂ + 1))) is complex real V30() Element of REAL
(i + ((2 * PI) * (c₂ + 1))) + (2 * PI) is complex real V30() Element of REAL
sin . ((i + ((2 * PI) * (c₂ + 1))) + (2 * PI)) is complex real V30() Element of REAL
sin . (i - ((2 * PI) * ((c₂ + 1) + 1))) is complex real V30() Element of REAL
(i - ((2 * PI) * ((c₂ + 1) + 1))) + (2 * PI) is complex real V30() Element of REAL
sin . ((i - ((2 * PI) * ((c₂ + 1) + 1))) + (2 * PI)) is complex real V30() Element of REAL
(sin . ((i + ((2 * PI) * (c₂ + 1))) + (2 * PI))) " is complex real V30() Element of REAL
(sin . (i + ((2 * PI) * (c₂ + 1)))) " is complex real V30() Element of REAL
t is non empty complex real V30() integer set
(2 * PI) * t is non empty complex real V30() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT
- c₂ is complex real V30() V31() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
- t is non empty complex real V30() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (i + 1) is non empty complex real V30() V31() V32() Element of REAL
- ((2 * PI) * (i + 1)) is non empty complex real V30() V31() V32() Element of REAL
tan is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
K372(REAL,REAL,sin,cos) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom tan is set
t is complex real V30() set
t + PI is complex real V30() Element of REAL
t - PI is complex real V30() Element of REAL
- PI is non empty complex real V30() V31() V32() set
t + (- PI) is complex real V30() set
tan . t is complex real V30() set
tan . (t + PI) is complex real V30() set
dom cos is set
dom sin is set
cos " {0} is set
(dom cos) \ (cos " {0}) is Element of K6((dom cos))
K6((dom cos)) is set
(dom sin) /\ ((dom cos) \ (cos " {0})) is Element of K6((dom cos))
cos . t is complex real V30() set
cos . (t + PI) is complex real V30() Element of REAL
- (cos . t) is complex real V30() set
cos . (t - PI) is complex real V30() Element of REAL
(t - PI) + (2 * PI) is complex real V30() Element of REAL
cos . ((t - PI) + (2 * PI)) is complex real V30() Element of REAL
sin . (t + PI) is complex real V30() Element of REAL
(sin . (t + PI)) / (cos . (t + PI)) is complex real V30() Element of REAL
(cos . (t + PI)) " is complex real V30() set
(sin . (t + PI)) * ((cos . (t + PI)) ") is complex real V30() set
sin . t is complex real V30() set
- (sin . t) is complex real V30() set
(- (sin . t)) / (cos . (t + PI)) is complex real V30() Element of REAL
(- (sin . t)) * ((cos . (t + PI)) ") is complex real V30() set
(- (sin . t)) / (- (cos . t)) is complex real V30() set
(- (cos . t)) " is complex real V30() set
(- (sin . t)) * ((- (cos . t)) ") is complex real V30() set
(sin . t) / (cos . t) is complex real V30() set
(cos . t) " is complex real V30() set
(sin . t) * ((cos . t) ") is complex real V30() set
cot is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
K372(REAL,REAL,cos,sin) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom cot is set
t is complex real V30() set
t + PI is complex real V30() Element of REAL
t - PI is complex real V30() Element of REAL
- PI is non empty complex real V30() V31() V32() set
t + (- PI) is complex real V30() set
cot . t is complex real V30() set
cot . (t + PI) is complex real V30() set
dom sin is set
dom cos is set
sin " {0} is set
(dom sin) \ (sin " {0}) is Element of K6((dom sin))
K6((dom sin)) is set
(dom cos) /\ ((dom sin) \ (sin " {0})) is Element of K6((dom sin))
sin . t is complex real V30() set
sin . (t + PI) is complex real V30() Element of REAL
- (sin . t) is complex real V30() set
sin . (t - PI) is complex real V30() Element of REAL
(t - PI) + (2 * PI) is complex real V30() Element of REAL
sin . ((t - PI) + (2 * PI)) is complex real V30() Element of REAL
cos . (t + PI) is complex real V30() Element of REAL
(cos . (t + PI)) / (sin . (t + PI)) is complex real V30() Element of REAL
(sin . (t + PI)) " is complex real V30() set
(cos . (t + PI)) * ((sin . (t + PI)) ") is complex real V30() set
cos . t is complex real V30() set
- (cos . t) is complex real V30() set
(- (cos . t)) / (sin . (t + PI)) is complex real V30() Element of REAL
(- (cos . t)) * ((sin . (t + PI)) ") is complex real V30() set
(- (cos . t)) / (- (sin . t)) is complex real V30() set
(- (sin . t)) " is complex real V30() set
(- (cos . t)) * ((- (sin . t)) ") is complex real V30() set
(cos . t) / (sin . t) is complex real V30() set
(sin . t) " is complex real V30() set
(cos . t) * ((sin . t) ") is complex real V30() set
t is ordinal natural complex real V30() V32() integer set
t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (t + 1) is non empty complex real V30() V31() V32() Element of REAL
0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer set
c₂ + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (c₂ + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
dom tan is set
i is complex real V30() set
i + (PI * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
i - (PI * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
- (PI * ((c₂ + 1) + 1)) is non empty complex real V30() V31() V32() set
i + (- (PI * ((c₂ + 1) + 1))) is complex real V30() set
tan . i is complex real V30() set
tan . (i + (PI * ((c₂ + 1) + 1))) is complex real V30() set
i + (PI * (c₂ + 1)) is complex real V30() Element of REAL
i - (PI * (c₂ + 1)) is complex real V30() Element of REAL
- (PI * (c₂ + 1)) is non empty complex real V30() V31() V32() set
i + (- (PI * (c₂ + 1))) is complex real V30() set
tan . (i + (PI * (c₂ + 1))) is complex real V30() set
dom cos is set
dom sin is set
cos " {0} is set
(dom cos) \ (cos " {0}) is Element of K6((dom cos))
K6((dom cos)) is set
(dom sin) /\ ((dom cos) \ (cos " {0})) is Element of K6((dom cos))
cos . (i + (PI * (c₂ + 1))) is complex real V30() Element of REAL
cos . (i - (PI * (c₂ + 1))) is complex real V30() Element of REAL
(i + (PI * (c₂ + 1))) + PI is complex real V30() Element of REAL
cos . ((i + (PI * (c₂ + 1))) + PI) is complex real V30() Element of REAL
- (cos . (i + (PI * (c₂ + 1)))) is complex real V30() Element of REAL
(i - (PI * ((c₂ + 1) + 1))) + PI is complex real V30() Element of REAL
cos . ((i - (PI * ((c₂ + 1) + 1))) + PI) is complex real V30() Element of REAL
cos . (i - (PI * ((c₂ + 1) + 1))) is complex real V30() Element of REAL
- (cos . (i - (PI * ((c₂ + 1) + 1)))) is complex real V30() Element of REAL
- (cos . (i - (PI * (c₂ + 1)))) is complex real V30() Element of REAL
sin . ((i + (PI * (c₂ + 1))) + PI) is complex real V30() Element of REAL
(sin . ((i + (PI * (c₂ + 1))) + PI)) / (cos . ((i + (PI * (c₂ + 1))) + PI)) is complex real V30() Element of REAL
(cos . ((i + (PI * (c₂ + 1))) + PI)) " is complex real V30() set
(sin . ((i + (PI * (c₂ + 1))) + PI)) * ((cos . ((i + (PI * (c₂ + 1))) + PI)) ") is complex real V30() set
sin . (i + (PI * (c₂ + 1))) is complex real V30() Element of REAL
- (sin . (i + (PI * (c₂ + 1)))) is complex real V30() Element of REAL
(- (sin . (i + (PI * (c₂ + 1))))) / (cos . ((i + (PI * (c₂ + 1))) + PI)) is complex real V30() Element of REAL
(- (sin . (i + (PI * (c₂ + 1))))) * ((cos . ((i + (PI * (c₂ + 1))) + PI)) ") is complex real V30() set
(- (sin . (i + (PI * (c₂ + 1))))) / (- (cos . (i + (PI * (c₂ + 1))))) is complex real V30() Element of REAL
(- (cos . (i + (PI * (c₂ + 1))))) " is complex real V30() set
(- (sin . (i + (PI * (c₂ + 1))))) * ((- (cos . (i + (PI * (c₂ + 1))))) ") is complex real V30() set
(sin . (i + (PI * (c₂ + 1)))) / (cos . (i + (PI * (c₂ + 1)))) is complex real V30() Element of REAL
(cos . (i + (PI * (c₂ + 1)))) " is complex real V30() set
(sin . (i + (PI * (c₂ + 1)))) * ((cos . (i + (PI * (c₂ + 1)))) ") is complex real V30() set
t is non empty complex real V30() integer set
PI * t is non empty complex real V30() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT
- c₂ is complex real V30() V31() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
- t is non empty complex real V30() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (i + 1) is non empty complex real V30() V31() V32() Element of REAL
- (PI * (i + 1)) is non empty complex real V30() V31() V32() Element of REAL
t is ordinal natural complex real V30() V32() integer set
t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (t + 1) is non empty complex real V30() V31() V32() Element of REAL
0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer set
c₂ + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (c₂ + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
dom cot is set
i is complex real V30() set
i + (PI * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
i - (PI * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
- (PI * ((c₂ + 1) + 1)) is non empty complex real V30() V31() V32() set
i + (- (PI * ((c₂ + 1) + 1))) is complex real V30() set
cot . i is complex real V30() set
cot . (i + (PI * ((c₂ + 1) + 1))) is complex real V30() set
i + (PI * (c₂ + 1)) is complex real V30() Element of REAL
i - (PI * (c₂ + 1)) is complex real V30() Element of REAL
- (PI * (c₂ + 1)) is non empty complex real V30() V31() V32() set
i + (- (PI * (c₂ + 1))) is complex real V30() set
cot . (i + (PI * (c₂ + 1))) is complex real V30() set
dom sin is set
dom cos is set
sin " {0} is set
(dom sin) \ (sin " {0}) is Element of K6((dom sin))
K6((dom sin)) is set
(dom cos) /\ ((dom sin) \ (sin " {0})) is Element of K6((dom sin))
sin . (i + (PI * (c₂ + 1))) is complex real V30() Element of REAL
sin . (i - (PI * (c₂ + 1))) is complex real V30() Element of REAL
(i + (PI * (c₂ + 1))) + PI is complex real V30() Element of REAL
sin . ((i + (PI * (c₂ + 1))) + PI) is complex real V30() Element of REAL
- (sin . (i + (PI * (c₂ + 1)))) is complex real V30() Element of REAL
(i - (PI * ((c₂ + 1) + 1))) + PI is complex real V30() Element of REAL
sin . ((i - (PI * ((c₂ + 1) + 1))) + PI) is complex real V30() Element of REAL
sin . (i - (PI * ((c₂ + 1) + 1))) is complex real V30() Element of REAL
- (sin . (i - (PI * ((c₂ + 1) + 1)))) is complex real V30() Element of REAL
- (sin . (i - (PI * (c₂ + 1)))) is complex real V30() Element of REAL
cos . ((i + (PI * (c₂ + 1))) + PI) is complex real V30() Element of REAL
(cos . ((i + (PI * (c₂ + 1))) + PI)) / (sin . ((i + (PI * (c₂ + 1))) + PI)) is complex real V30() Element of REAL
(sin . ((i + (PI * (c₂ + 1))) + PI)) " is complex real V30() set
(cos . ((i + (PI * (c₂ + 1))) + PI)) * ((sin . ((i + (PI * (c₂ + 1))) + PI)) ") is complex real V30() set
cos . (i + (PI * (c₂ + 1))) is complex real V30() Element of REAL
- (cos . (i + (PI * (c₂ + 1)))) is complex real V30() Element of REAL
(- (cos . (i + (PI * (c₂ + 1))))) / (sin . ((i + (PI * (c₂ + 1))) + PI)) is complex real V30() Element of REAL
(- (cos . (i + (PI * (c₂ + 1))))) * ((sin . ((i + (PI * (c₂ + 1))) + PI)) ") is complex real V30() set
(- (cos . (i + (PI * (c₂ + 1))))) / (- (sin . (i + (PI * (c₂ + 1))))) is complex real V30() Element of REAL
(- (sin . (i + (PI * (c₂ + 1))))) " is complex real V30() set
(- (cos . (i + (PI * (c₂ + 1))))) * ((- (sin . (i + (PI * (c₂ + 1))))) ") is complex real V30() set
(cos . (i + (PI * (c₂ + 1)))) / (sin . (i + (PI * (c₂ + 1)))) is complex real V30() Element of REAL
(sin . (i + (PI * (c₂ + 1)))) " is complex real V30() set
(cos . (i + (PI * (c₂ + 1)))) * ((sin . (i + (PI * (c₂ + 1)))) ") is complex real V30() set
t is non empty complex real V30() integer set
PI * t is non empty complex real V30() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT
- c₂ is complex real V30() V31() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
- t is non empty complex real V30() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (i + 1) is non empty complex real V30() V31() V32() Element of REAL
- (PI * (i + 1)) is non empty complex real V30() V31() V32() Element of REAL
|.sin.| is Relation-like Function-like total complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
dom |.sin.| is set
t is complex real V30() set
t + PI is complex real V30() Element of REAL
t - PI is complex real V30() Element of REAL
- PI is non empty complex real V30() V31() V32() set
t + (- PI) is complex real V30() set
|.sin.| . t is complex real V30() set
|.sin.| . (t + PI) is complex real V30() set
dom sin is set
sin (t + PI) is complex real V30() Element of REAL
K130(sin,(t + PI)) is complex real V30() Element of REAL
|.(sin (t + PI)).| is complex real V30() Element of REAL
sin . t is complex real V30() set
- (sin . t) is complex real V30() set
|.(- (sin . t)).| is complex real V30() Element of REAL
|.(sin . t).| is complex real V30() Element of REAL
|.cos.| is Relation-like Function-like total complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
dom |.cos.| is set
t is complex real V30() set
t + PI is complex real V30() Element of REAL
t - PI is complex real V30() Element of REAL
- PI is non empty complex real V30() V31() V32() set
t + (- PI) is complex real V30() set
|.cos.| . t is complex real V30() set
|.cos.| . (t + PI) is complex real V30() set
dom cos is set
cos (t + PI) is complex real V30() Element of REAL
K130(cos,(t + PI)) is complex real V30() Element of REAL
|.(cos (t + PI)).| is complex real V30() Element of REAL
cos . t is complex real V30() set
- (cos . t) is complex real V30() set
|.(- (cos . t)).| is complex real V30() Element of REAL
|.(cos . t).| is complex real V30() Element of REAL
t is ordinal natural complex real V30() V32() integer set
t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (t + 1) is non empty complex real V30() V31() V32() Element of REAL
0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer set
c₂ + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (c₂ + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
dom |.sin.| is set
i is complex real V30() set
i + (PI * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
i - (PI * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
- (PI * ((c₂ + 1) + 1)) is non empty complex real V30() V31() V32() set
i + (- (PI * ((c₂ + 1) + 1))) is complex real V30() set
|.sin.| . i is complex real V30() set
|.sin.| . (i + (PI * ((c₂ + 1) + 1))) is complex real V30() set
i + (PI * (c₂ + 1)) is complex real V30() Element of REAL
i - (PI * (c₂ + 1)) is complex real V30() Element of REAL
- (PI * (c₂ + 1)) is non empty complex real V30() V31() V32() set
i + (- (PI * (c₂ + 1))) is complex real V30() set
dom sin is set
(i + (PI * (c₂ + 1))) + PI is complex real V30() Element of REAL
sin . ((i + (PI * (c₂ + 1))) + PI) is complex real V30() Element of REAL
|.(sin . ((i + (PI * (c₂ + 1))) + PI)).| is complex real V30() Element of REAL
sin . (i + (PI * (c₂ + 1))) is complex real V30() Element of REAL
- (sin . (i + (PI * (c₂ + 1)))) is complex real V30() Element of REAL
|.(- (sin . (i + (PI * (c₂ + 1))))).| is complex real V30() Element of REAL
|.(sin . (i + (PI * (c₂ + 1)))).| is complex real V30() Element of REAL
|.sin.| . (i + (PI * (c₂ + 1))) is complex real V30() set
t is non empty complex real V30() integer set
PI * t is non empty complex real V30() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT
- c₂ is complex real V30() V31() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
- t is non empty complex real V30() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (i + 1) is non empty complex real V30() V31() V32() Element of REAL
- (PI * (i + 1)) is non empty complex real V30() V31() V32() Element of REAL
t is ordinal natural complex real V30() V32() integer set
t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (t + 1) is non empty complex real V30() V31() V32() Element of REAL
0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer set
c₂ + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (c₂ + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
dom |.cos.| is set
i is complex real V30() set
i + (PI * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
i - (PI * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
- (PI * ((c₂ + 1) + 1)) is non empty complex real V30() V31() V32() set
i + (- (PI * ((c₂ + 1) + 1))) is complex real V30() set
|.cos.| . i is complex real V30() set
|.cos.| . (i + (PI * ((c₂ + 1) + 1))) is complex real V30() set
i + (PI * (c₂ + 1)) is complex real V30() Element of REAL
i - (PI * (c₂ + 1)) is complex real V30() Element of REAL
- (PI * (c₂ + 1)) is non empty complex real V30() V31() V32() set
i + (- (PI * (c₂ + 1))) is complex real V30() set
dom cos is set
(i + (PI * (c₂ + 1))) + PI is complex real V30() Element of REAL
cos . ((i + (PI * (c₂ + 1))) + PI) is complex real V30() Element of REAL
|.(cos . ((i + (PI * (c₂ + 1))) + PI)).| is complex real V30() Element of REAL
cos . (i + (PI * (c₂ + 1))) is complex real V30() Element of REAL
- (cos . (i + (PI * (c₂ + 1)))) is complex real V30() Element of REAL
|.(- (cos . (i + (PI * (c₂ + 1))))).| is complex real V30() Element of REAL
|.(cos . (i + (PI * (c₂ + 1)))).| is complex real V30() Element of REAL
|.cos.| . (i + (PI * (c₂ + 1))) is complex real V30() set
t is non empty complex real V30() integer set
PI * t is non empty complex real V30() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT
- c₂ is complex real V30() V31() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
- t is non empty complex real V30() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (i + 1) is non empty complex real V30() V31() V32() Element of REAL
- (PI * (i + 1)) is non empty complex real V30() V31() V32() Element of REAL
|.sin.| + |.cos.| is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (|.sin.| + |.cos.|) is set
t is complex real V30() set
t + (PI / 2) is complex real V30() Element of REAL
t - (PI / 2) is complex real V30() Element of REAL
- (PI / 2) is non empty complex real V30() V31() V32() set
t + (- (PI / 2)) is complex real V30() set
(|.sin.| + |.cos.|) . t is complex real V30() set
(|.sin.| + |.cos.|) . (t + (PI / 2)) is complex real V30() set
dom |.sin.| is set
dom |.cos.| is set
(dom |.sin.|) /\ (dom |.cos.|) is set
|.sin.| . (t + (PI / 2)) is complex real V30() set
|.cos.| . (t + (PI / 2)) is complex real V30() set
(|.sin.| . (t + (PI / 2))) + (|.cos.| . (t + (PI / 2))) is complex real V30() set
sin . (t + (PI / 2)) is complex real V30() Element of REAL
|.(sin . (t + (PI / 2))).| is complex real V30() Element of REAL
|.(sin . (t + (PI / 2))).| + (|.cos.| . (t + (PI / 2))) is complex real V30() Element of REAL
cos . (t + (PI / 2)) is complex real V30() Element of REAL
|.(cos . (t + (PI / 2))).| is complex real V30() Element of REAL
|.(sin . (t + (PI / 2))).| + |.(cos . (t + (PI / 2))).| is complex real V30() Element of REAL
cos . t is complex real V30() set
|.(cos . t).| is complex real V30() Element of REAL
|.(cos . t).| + |.(cos . (t + (PI / 2))).| is complex real V30() Element of REAL
sin . t is complex real V30() set
- (sin . t) is complex real V30() set
|.(- (sin . t)).| is complex real V30() Element of REAL
|.(cos . t).| + |.(- (sin . t)).| is complex real V30() Element of REAL
|.(sin . t).| is complex real V30() Element of REAL
|.(cos . t).| + |.(sin . t).| is complex real V30() Element of REAL
|.cos.| . t is complex real V30() set
(|.cos.| . t) + |.(sin . t).| is complex real V30() Element of REAL
|.sin.| . t is complex real V30() set
(|.cos.| . t) + (|.sin.| . t) is complex real V30() set
t is ordinal natural complex real V30() V32() integer set
t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(PI / 2) * (t + 1) is non empty complex real V30() V31() V32() Element of REAL
0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(PI / 2) * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer set
c₂ + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(PI / 2) * (c₂ + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(PI / 2) * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
dom (|.sin.| + |.cos.|) is set
dom |.sin.| is set
dom |.cos.| is set
(dom |.sin.|) /\ (dom |.cos.|) is set
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(PI / 2) * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
i is complex real V30() set
i + ((PI / 2) * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
i - ((PI / 2) * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
- ((PI / 2) * ((c₂ + 1) + 1)) is non empty complex real V30() V31() V32() set
i + (- ((PI / 2) * ((c₂ + 1) + 1))) is complex real V30() set
(|.sin.| + |.cos.|) . i is complex real V30() set
(|.sin.| + |.cos.|) . (i + ((PI / 2) * ((c₂ + 1) + 1))) is complex real V30() set
|.sin.| . (i + ((PI / 2) * ((c₂ + 1) + 1))) is complex real V30() set
|.cos.| . (i + ((PI / 2) * ((c₂ + 1) + 1))) is complex real V30() set
(|.sin.| . (i + ((PI / 2) * ((c₂ + 1) + 1)))) + (|.cos.| . (i + ((PI / 2) * ((c₂ + 1) + 1)))) is complex real V30() set
sin . (i + ((PI / 2) * ((c₂ + 1) + 1))) is complex real V30() Element of REAL
|.(sin . (i + ((PI / 2) * ((c₂ + 1) + 1)))).| is complex real V30() Element of REAL
|.(sin . (i + ((PI / 2) * ((c₂ + 1) + 1)))).| + (|.cos.| . (i + ((PI / 2) * ((c₂ + 1) + 1)))) is complex real V30() Element of REAL
i + ((PI / 2) * (c₂ + 1)) is complex real V30() Element of REAL
(i + ((PI / 2) * (c₂ + 1))) + (PI / 2) is complex real V30() Element of REAL
sin . ((i + ((PI / 2) * (c₂ + 1))) + (PI / 2)) is complex real V30() Element of REAL
|.(sin . ((i + ((PI / 2) * (c₂ + 1))) + (PI / 2))).| is complex real V30() Element of REAL
cos . ((i + ((PI / 2) * (c₂ + 1))) + (PI / 2)) is complex real V30() Element of REAL
|.(cos . ((i + ((PI / 2) * (c₂ + 1))) + (PI / 2))).| is complex real V30() Element of REAL
|.(sin . ((i + ((PI / 2) * (c₂ + 1))) + (PI / 2))).| + |.(cos . ((i + ((PI / 2) * (c₂ + 1))) + (PI / 2))).| is complex real V30() Element of REAL
cos . (i + ((PI / 2) * (c₂ + 1))) is complex real V30() Element of REAL
|.(cos . (i + ((PI / 2) * (c₂ + 1)))).| is complex real V30() Element of REAL
|.(cos . (i + ((PI / 2) * (c₂ + 1)))).| + |.(cos . ((i + ((PI / 2) * (c₂ + 1))) + (PI / 2))).| is complex real V30() Element of REAL
sin . (i + ((PI / 2) * (c₂ + 1))) is complex real V30() Element of REAL
- (sin . (i + ((PI / 2) * (c₂ + 1)))) is complex real V30() Element of REAL
|.(- (sin . (i + ((PI / 2) * (c₂ + 1))))).| is complex real V30() Element of REAL
|.(cos . (i + ((PI / 2) * (c₂ + 1)))).| + |.(- (sin . (i + ((PI / 2) * (c₂ + 1))))).| is complex real V30() Element of REAL
|.(sin . (i + ((PI / 2) * (c₂ + 1)))).| is complex real V30() Element of REAL
|.(cos . (i + ((PI / 2) * (c₂ + 1)))).| + |.(sin . (i + ((PI / 2) * (c₂ + 1)))).| is complex real V30() Element of REAL
|.cos.| . (i + ((PI / 2) * (c₂ + 1))) is complex real V30() set
(|.cos.| . (i + ((PI / 2) * (c₂ + 1)))) + |.(sin . (i + ((PI / 2) * (c₂ + 1)))).| is complex real V30() Element of REAL
|.sin.| . (i + ((PI / 2) * (c₂ + 1))) is complex real V30() set
(|.cos.| . (i + ((PI / 2) * (c₂ + 1)))) + (|.sin.| . (i + ((PI / 2) * (c₂ + 1)))) is complex real V30() set
(|.sin.| + |.cos.|) . (i + ((PI / 2) * (c₂ + 1))) is complex real V30() set
t is non empty complex real V30() integer set
(PI / 2) * t is non empty complex real V30() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT
- c₂ is complex real V30() V31() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
- t is non empty complex real V30() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(PI / 2) * (i + 1) is non empty complex real V30() V31() V32() Element of REAL
- ((PI / 2) * (i + 1)) is non empty complex real V30() V31() V32() Element of REAL
sin ^2 is Relation-like Function-like total complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
sin (#) sin is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom (sin ^2) is set
t is complex real V30() set
t + PI is complex real V30() Element of REAL
t - PI is complex real V30() Element of REAL
- PI is non empty complex real V30() V31() V32() set
t + (- PI) is complex real V30() set
(sin ^2) . t is complex real V30() set
(sin ^2) . (t + PI) is complex real V30() set
dom sin is set
sin (t + PI) is complex real V30() Element of REAL
K130(sin,(t + PI)) is complex real V30() Element of REAL
(sin (t + PI)) ^2 is complex real V30() Element of REAL
(sin (t + PI)) * (sin (t + PI)) is complex real V30() set
sin . t is complex real V30() set
- (sin . t) is complex real V30() set
(- (sin . t)) ^2 is set
(- (sin . t)) * (- (sin . t)) is complex real V30() set
(sin . t) ^2 is set
(sin . t) * (sin . t) is complex real V30() set
cos ^2 is Relation-like Function-like total complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
cos (#) cos is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom (cos ^2) is set
t is complex real V30() set
t + PI is complex real V30() Element of REAL
t - PI is complex real V30() Element of REAL
- PI is non empty complex real V30() V31() V32() set
t + (- PI) is complex real V30() set
(cos ^2) . t is complex real V30() set
(cos ^2) . (t + PI) is complex real V30() set
dom cos is set
cos (t + PI) is complex real V30() Element of REAL
K130(cos,(t + PI)) is complex real V30() Element of REAL
(cos (t + PI)) ^2 is complex real V30() Element of REAL
(cos (t + PI)) * (cos (t + PI)) is complex real V30() set
cos . t is complex real V30() set
- (cos . t) is complex real V30() set
(- (cos . t)) ^2 is set
(- (cos . t)) * (- (cos . t)) is complex real V30() set
(cos . t) ^2 is set
(cos . t) * (cos . t) is complex real V30() set
t is ordinal natural complex real V30() V32() integer set
t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (t + 1) is non empty complex real V30() V31() V32() Element of REAL
0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer set
c₂ + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (c₂ + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
dom (sin ^2) is set
i is complex real V30() set
i + (PI * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
i - (PI * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
- (PI * ((c₂ + 1) + 1)) is non empty complex real V30() V31() V32() set
i + (- (PI * ((c₂ + 1) + 1))) is complex real V30() set
(sin ^2) . i is complex real V30() set
(sin ^2) . (i + (PI * ((c₂ + 1) + 1))) is complex real V30() set
dom sin is set
i + (PI * (c₂ + 1)) is complex real V30() Element of REAL
(i + (PI * (c₂ + 1))) + PI is complex real V30() Element of REAL
sin . ((i + (PI * (c₂ + 1))) + PI) is complex real V30() Element of REAL
(sin . ((i + (PI * (c₂ + 1))) + PI)) ^2 is complex real V30() Element of REAL
(sin . ((i + (PI * (c₂ + 1))) + PI)) * (sin . ((i + (PI * (c₂ + 1))) + PI)) is complex real V30() set
sin . (i + (PI * (c₂ + 1))) is complex real V30() Element of REAL
- (sin . (i + (PI * (c₂ + 1)))) is complex real V30() Element of REAL
(- (sin . (i + (PI * (c₂ + 1))))) ^2 is complex real V30() Element of REAL
(- (sin . (i + (PI * (c₂ + 1))))) * (- (sin . (i + (PI * (c₂ + 1))))) is complex real V30() set
(sin . (i + (PI * (c₂ + 1)))) ^2 is complex real V30() Element of REAL
(sin . (i + (PI * (c₂ + 1)))) * (sin . (i + (PI * (c₂ + 1)))) is complex real V30() set
(sin ^2) . (i + (PI * (c₂ + 1))) is complex real V30() set
t is non empty complex real V30() integer set
PI * t is non empty complex real V30() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT
- c₂ is complex real V30() V31() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
- t is non empty complex real V30() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (i + 1) is non empty complex real V30() V31() V32() Element of REAL
- (PI * (i + 1)) is non empty complex real V30() V31() V32() Element of REAL
t is ordinal natural complex real V30() V32() integer set
t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (t + 1) is non empty complex real V30() V31() V32() Element of REAL
0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer set
c₂ + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (c₂ + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
dom (cos ^2) is set
i is complex real V30() set
i + (PI * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
i - (PI * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
- (PI * ((c₂ + 1) + 1)) is non empty complex real V30() V31() V32() set
i + (- (PI * ((c₂ + 1) + 1))) is complex real V30() set
(cos ^2) . i is complex real V30() set
(cos ^2) . (i + (PI * ((c₂ + 1) + 1))) is complex real V30() set
dom cos is set
i + (PI * (c₂ + 1)) is complex real V30() Element of REAL
(i + (PI * (c₂ + 1))) + PI is complex real V30() Element of REAL
cos . ((i + (PI * (c₂ + 1))) + PI) is complex real V30() Element of REAL
(cos . ((i + (PI * (c₂ + 1))) + PI)) ^2 is complex real V30() Element of REAL
(cos . ((i + (PI * (c₂ + 1))) + PI)) * (cos . ((i + (PI * (c₂ + 1))) + PI)) is complex real V30() set
cos . (i + (PI * (c₂ + 1))) is complex real V30() Element of REAL
- (cos . (i + (PI * (c₂ + 1)))) is complex real V30() Element of REAL
(- (cos . (i + (PI * (c₂ + 1))))) ^2 is complex real V30() Element of REAL
(- (cos . (i + (PI * (c₂ + 1))))) * (- (cos . (i + (PI * (c₂ + 1))))) is complex real V30() set
(cos . (i + (PI * (c₂ + 1)))) ^2 is complex real V30() Element of REAL
(cos . (i + (PI * (c₂ + 1)))) * (cos . (i + (PI * (c₂ + 1)))) is complex real V30() set
(cos ^2) . (i + (PI * (c₂ + 1))) is complex real V30() set
t is non empty complex real V30() integer set
PI * t is non empty complex real V30() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT
- c₂ is complex real V30() V31() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
- t is non empty complex real V30() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (i + 1) is non empty complex real V30() V31() V32() Element of REAL
- (PI * (i + 1)) is non empty complex real V30() V31() V32() Element of REAL
sin (#) cos is Relation-like Function-like total complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (sin (#) cos) is set
t is complex real V30() set
t + PI is complex real V30() Element of REAL
t - PI is complex real V30() Element of REAL
- PI is non empty complex real V30() V31() V32() set
t + (- PI) is complex real V30() set
(sin (#) cos) . t is complex real V30() set
(sin (#) cos) . (t + PI) is complex real V30() set
dom sin is set
dom cos is set
(dom sin) /\ (dom cos) is set
sin . (t + PI) is complex real V30() Element of REAL
cos . (t + PI) is complex real V30() Element of REAL
(sin . (t + PI)) * (cos . (t + PI)) is complex real V30() Element of REAL
sin . t is complex real V30() set
- (sin . t) is complex real V30() set
(- (sin . t)) * (cos . (t + PI)) is complex real V30() Element of REAL
cos . t is complex real V30() set
- (cos . t) is complex real V30() set
(- (sin . t)) * (- (cos . t)) is complex real V30() set
(sin . t) * (cos . t) is complex real V30() set
t is ordinal natural complex real V30() V32() integer set
t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (t + 1) is non empty complex real V30() V31() V32() Element of REAL
0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer set
c₂ + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (c₂ + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
(c₂ + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * ((c₂ + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
dom (sin (#) cos) is set
i is complex real V30() set
i + (PI * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
i - (PI * ((c₂ + 1) + 1)) is complex real V30() Element of REAL
- (PI * ((c₂ + 1) + 1)) is non empty complex real V30() V31() V32() set
i + (- (PI * ((c₂ + 1) + 1))) is complex real V30() set
(sin (#) cos) . i is complex real V30() set
(sin (#) cos) . (i + (PI * ((c₂ + 1) + 1))) is complex real V30() set
i + (PI * (c₂ + 1)) is complex real V30() Element of REAL
i - (PI * (c₂ + 1)) is complex real V30() Element of REAL
- (PI * (c₂ + 1)) is non empty complex real V30() V31() V32() set
i + (- (PI * (c₂ + 1))) is complex real V30() set
dom cos is set
dom sin is set
(dom cos) /\ (dom sin) is set
(i + (PI * (c₂ + 1))) + PI is complex real V30() Element of REAL
sin . ((i + (PI * (c₂ + 1))) + PI) is complex real V30() Element of REAL
cos . ((i + (PI * (c₂ + 1))) + PI) is complex real V30() Element of REAL
(sin . ((i + (PI * (c₂ + 1))) + PI)) * (cos . ((i + (PI * (c₂ + 1))) + PI)) is complex real V30() Element of REAL
sin . (i + (PI * (c₂ + 1))) is complex real V30() Element of REAL
- (sin . (i + (PI * (c₂ + 1)))) is complex real V30() Element of REAL
(- (sin . (i + (PI * (c₂ + 1))))) * (cos . ((i + (PI * (c₂ + 1))) + PI)) is complex real V30() Element of REAL
cos . (i + (PI * (c₂ + 1))) is complex real V30() Element of REAL
- (cos . (i + (PI * (c₂ + 1)))) is complex real V30() Element of REAL
(- (sin . (i + (PI * (c₂ + 1))))) * (- (cos . (i + (PI * (c₂ + 1))))) is complex real V30() Element of REAL
(sin . (i + (PI * (c₂ + 1)))) * (cos . (i + (PI * (c₂ + 1)))) is complex real V30() Element of REAL
(sin (#) cos) . (i + (PI * (c₂ + 1))) is complex real V30() set
t is non empty complex real V30() integer set
PI * t is non empty complex real V30() Element of REAL
c₂ is ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT
- c₂ is complex real V30() V31() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
- t is non empty complex real V30() integer set
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
PI * (i + 1) is non empty complex real V30() V31() V32() Element of REAL
- (PI * (i + 1)) is non empty complex real V30() V31() V32() Element of REAL
t is complex real V30() set
c₂ is complex real V30() set
c₂ (#) sin is Relation-like Function-like total complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
t + (c₂ (#) sin) is Relation-like Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
dom (t + (c₂ (#) sin)) is set
i is complex real V30() set
i + (2 * PI) is complex real V30() Element of REAL
i - (2 * PI) is complex real V30() Element of REAL
- (2 * PI) is non empty complex real V30() V31() V32() set
i + (- (2 * PI)) is complex real V30() set
(t + (c₂ (#) sin)) . i is complex real V30() set
(t + (c₂ (#) sin)) . (i + (2 * PI)) is complex real V30() set
dom (c₂ (#) sin) is set
dom sin is set
(c₂ (#) sin) . (i + (2 * PI)) is complex real V30() set
t + ((c₂ (#) sin) . (i + (2 * PI))) is complex real V30() set
sin . (i + (2 * PI)) is complex real V30() Element of REAL
c₂ * (sin . (i + (2 * PI))) is complex real V30() Element of REAL
t + (c₂ * (sin . (i + (2 * PI)))) is complex real V30() Element of REAL
sin . i is complex real V30() set
c₂ * (sin . i) is complex real V30() set
t + (c₂ * (sin . i)) is complex real V30() set
(c₂ (#) sin) . i is complex real V30() set
t + ((c₂ (#) sin) . i) is complex real V30() set
t is complex real V30() set
c₂ is complex real V30() set
c₂ (#) cos is Relation-like Function-like total complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
t + (c₂ (#) cos) is Relation-like Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
dom (t + (c₂ (#) cos)) is set
i is complex real V30() set
i + (2 * PI) is complex real V30() Element of REAL
i - (2 * PI) is complex real V30() Element of REAL
- (2 * PI) is non empty complex real V30() V31() V32() set
i + (- (2 * PI)) is complex real V30() set
(t + (c₂ (#) cos)) . i is complex real V30() set
(t + (c₂ (#) cos)) . (i + (2 * PI)) is complex real V30() set
dom (c₂ (#) cos) is set
dom cos is set
(c₂ (#) cos) . (i + (2 * PI)) is complex real V30() set
t + ((c₂ (#) cos) . (i + (2 * PI))) is complex real V30() set
cos . (i + (2 * PI)) is complex real V30() Element of REAL
c₂ * (cos . (i + (2 * PI))) is complex real V30() Element of REAL
t + (c₂ * (cos . (i + (2 * PI)))) is complex real V30() Element of REAL
cos . i is complex real V30() set
c₂ * (cos . i) is complex real V30() set
t + (c₂ * (cos . i)) is complex real V30() set
(c₂ (#) cos) . i is complex real V30() set
t + ((c₂ (#) cos) . i) is complex real V30() set
t is complex real V30() set
c₂ is complex real V30() set
c₂ (#) sin is Relation-like Function-like total complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
t + (c₂ (#) sin) is Relation-like Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (i + 1) is non empty complex real V30() V31() V32() Element of REAL
0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL
k is ordinal natural complex real V30() V32() integer set
k + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (k + 1) is non empty complex real V30() V31() V32() Element of REAL
(k + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * ((k + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
(k + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * ((k + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
dom (t + (c₂ (#) sin)) is set
m is complex real V30() set
m + ((2 * PI) * ((k + 1) + 1)) is complex real V30() Element of REAL
m - ((2 * PI) * ((k + 1) + 1)) is complex real V30() Element of REAL
- ((2 * PI) * ((k + 1) + 1)) is non empty complex real V30() V31() V32() set
m + (- ((2 * PI) * ((k + 1) + 1))) is complex real V30() set
(t + (c₂ (#) sin)) . m is complex real V30() set
(t + (c₂ (#) sin)) . (m + ((2 * PI) * ((k + 1) + 1))) is complex real V30() set
dom (c₂ (#) sin) is set
dom sin is set
m + ((2 * PI) * (k + 1)) is complex real V30() Element of REAL
m - ((2 * PI) * (k + 1)) is complex real V30() Element of REAL
- ((2 * PI) * (k + 1)) is non empty complex real V30() V31() V32() set
m + (- ((2 * PI) * (k + 1))) is complex real V30() set
(c₂ (#) sin) . (m + ((2 * PI) * ((k + 1) + 1))) is complex real V30() set
t + ((c₂ (#) sin) . (m + ((2 * PI) * ((k + 1) + 1)))) is complex real V30() set
(m + ((2 * PI) * (k + 1))) + (2 * PI) is complex real V30() Element of REAL
sin . ((m + ((2 * PI) * (k + 1))) + (2 * PI)) is complex real V30() Element of REAL
c₂ * (sin . ((m + ((2 * PI) * (k + 1))) + (2 * PI))) is complex real V30() Element of REAL
t + (c₂ * (sin . ((m + ((2 * PI) * (k + 1))) + (2 * PI)))) is complex real V30() Element of REAL
sin . (m + ((2 * PI) * (k + 1))) is complex real V30() Element of REAL
c₂ * (sin . (m + ((2 * PI) * (k + 1)))) is complex real V30() Element of REAL
t + (c₂ * (sin . (m + ((2 * PI) * (k + 1))))) is complex real V30() Element of REAL
(c₂ (#) sin) . (m + ((2 * PI) * (k + 1))) is complex real V30() set
t + ((c₂ (#) sin) . (m + ((2 * PI) * (k + 1)))) is complex real V30() set
(t + (c₂ (#) sin)) . (m + ((2 * PI) * (k + 1))) is complex real V30() set
t is complex real V30() set
c₂ is complex real V30() set
c₂ (#) sin is Relation-like Function-like total complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
t + (c₂ (#) sin) is Relation-like Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
i is non empty complex real V30() integer set
(2 * PI) * i is non empty complex real V30() Element of REAL
k is ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT
- k is complex real V30() V31() integer set
m is ordinal natural complex real V30() V32() integer set
m + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
- i is non empty complex real V30() integer set
m is ordinal natural complex real V30() V32() integer set
m + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (m + 1) is non empty complex real V30() V31() V32() Element of REAL
- ((2 * PI) * (m + 1)) is non empty complex real V30() V31() V32() Element of REAL
i is non empty complex real V30() integer set
(2 * PI) * i is non empty complex real V30() Element of REAL
t is complex real V30() set
t (#) sin is Relation-like Function-like total complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
c₂ is complex real V30() set
(t (#) sin) - c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
- c₂ is complex real V30() set
(- c₂) + (t (#) sin) is Relation-like Function-like complex-valued ext-real-valued real-valued () set
t is complex real V30() set
c₂ is complex real V30() set
c₂ (#) cos is Relation-like Function-like total complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
t + (c₂ (#) cos) is Relation-like Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
i is ordinal natural complex real V30() V32() integer set
i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (i + 1) is non empty complex real V30() V31() V32() Element of REAL
0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL
k is ordinal natural complex real V30() V32() integer set
k + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (k + 1) is non empty complex real V30() V31() V32() Element of REAL
(k + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * ((k + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
(k + 1) + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * ((k + 1) + 1) is non empty complex real V30() V31() V32() Element of REAL
dom (t + (c₂ (#) cos)) is set
m is complex real V30() set
m + ((2 * PI) * ((k + 1) + 1)) is complex real V30() Element of REAL
m - ((2 * PI) * ((k + 1) + 1)) is complex real V30() Element of REAL
- ((2 * PI) * ((k + 1) + 1)) is non empty complex real V30() V31() V32() set
m + (- ((2 * PI) * ((k + 1) + 1))) is complex real V30() set
(t + (c₂ (#) cos)) . m is complex real V30() set
(t + (c₂ (#) cos)) . (m + ((2 * PI) * ((k + 1) + 1))) is complex real V30() set
dom (c₂ (#) cos) is set
dom cos is set
m + ((2 * PI) * (k + 1)) is complex real V30() Element of REAL
m - ((2 * PI) * (k + 1)) is complex real V30() Element of REAL
- ((2 * PI) * (k + 1)) is non empty complex real V30() V31() V32() set
m + (- ((2 * PI) * (k + 1))) is complex real V30() set
(c₂ (#) cos) . (m + ((2 * PI) * ((k + 1) + 1))) is complex real V30() set
t + ((c₂ (#) cos) . (m + ((2 * PI) * ((k + 1) + 1)))) is complex real V30() set
(m + ((2 * PI) * (k + 1))) + (2 * PI) is complex real V30() Element of REAL
cos . ((m + ((2 * PI) * (k + 1))) + (2 * PI)) is complex real V30() Element of REAL
c₂ * (cos . ((m + ((2 * PI) * (k + 1))) + (2 * PI))) is complex real V30() Element of REAL
t + (c₂ * (cos . ((m + ((2 * PI) * (k + 1))) + (2 * PI)))) is complex real V30() Element of REAL
cos . (m + ((2 * PI) * (k + 1))) is complex real V30() Element of REAL
c₂ * (cos . (m + ((2 * PI) * (k + 1)))) is complex real V30() Element of REAL
t + (c₂ * (cos . (m + ((2 * PI) * (k + 1))))) is complex real V30() Element of REAL
(c₂ (#) cos) . (m + ((2 * PI) * (k + 1))) is complex real V30() set
t + ((c₂ (#) cos) . (m + ((2 * PI) * (k + 1)))) is complex real V30() set
(t + (c₂ (#) cos)) . (m + ((2 * PI) * (k + 1))) is complex real V30() set
t is complex real V30() set
c₂ is complex real V30() set
c₂ (#) cos is Relation-like Function-like total complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
t + (c₂ (#) cos) is Relation-like Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
i is non empty complex real V30() integer set
(2 * PI) * i is non empty complex real V30() Element of REAL
k is ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT
- k is complex real V30() V31() integer set
m is ordinal natural complex real V30() V32() integer set
m + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
- i is non empty complex real V30() integer set
m is ordinal natural complex real V30() V32() integer set
m + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL
(2 * PI) * (m + 1) is non empty complex real V30() V31() V32() Element of REAL
- ((2 * PI) * (m + 1)) is non empty complex real V30() V31() V32() Element of REAL
i is non empty complex real V30() integer set
(2 * PI) * i is non empty complex real V30() Element of REAL
t is complex real V30() set
t (#) cos is Relation-like Function-like total complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
c₂ is complex real V30() set
(t (#) cos) - c₂ is Relation-like Function-like complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))
- c₂ is complex real V30() set
(- c₂) + (t (#) cos) is Relation-like Function-like complex-valued ext-real-valued real-valued () set
t is complex real V30() set
c₂ is complex real V30() set
REAL --> c₂ is non empty Relation-like REAL -defined Function-like constant total V27( REAL ,{c₂}) complex-valued ext-real-valued real-valued Element of K6(K7(REAL,{c₂}))
{c₂} is V134() V135() V136() set
K7(REAL,{c₂}) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(REAL,{c₂})) is set
t is complex real V30() set
REAL --> t is non empty Relation-like REAL -defined Function-like constant total V27( REAL ,{t}) complex-valued ext-real-valued real-valued Element of K6(K7(REAL,{t}))
{t} is V134() V135() V136() set
K7(REAL,{t}) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(REAL,{t})) is set
t is non empty complex real V30() set
the complex real V30() Element of REAL is complex real V30() Element of REAL
REAL --> the complex real V30() Element of REAL is non empty Relation-like REAL -defined REAL -valued Function-like constant total V27( REAL , REAL ) complex-valued ext-real-valued real-valued () Element of K6(K7(REAL,REAL))