:: SIN_COS semantic presentation

REAL is non empty V46() V47() V48() V52() V65() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V46() V47() V48() V49() V50() V51() V52() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V46() V52() V65() set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V46() V47() V48() V49() V50() V51() V52() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
{{},1} is non empty V46() V47() V48() V49() V50() V51() set
INT is non empty V46() V47() V48() V49() V50() V52() V65() set
K20(REAL,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) is set
K20(NAT,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
omega is non empty epsilon-transitive epsilon-connected ordinal V46() V47() V48() V49() V50() V51() V52() set
K19(omega) is set
K19(NAT) is set
RAT is non empty V46() V47() V48() V49() V52() V65() set
K20(NAT,COMPLEX) is complex-valued set
K19(K20(NAT,COMPLEX)) is set
K20(COMPLEX,COMPLEX) is complex-valued set
K19(K20(COMPLEX,COMPLEX)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(K20(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(K20(NAT,NAT),NAT)) is set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V46() V47() V48() V49() V50() V51() V52() V62() V63() Element of NAT
K19(K20(NAT,NAT)) is set
1r is complex Element of COMPLEX
Re 0 is complex real ext-real Element of REAL
Im 0 is complex real ext-real Element of REAL
Re 1r is complex real ext-real Element of REAL
Im 1r is complex real ext-real Element of REAL
<i> is complex Element of COMPLEX
K88(REAL,0,1,0,1) is Relation-like {0,1} -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20({0,1},REAL))
{0,1} is non empty V46() V47() V48() V49() V50() V51() set
K20({0,1},REAL) is complex-valued ext-real-valued real-valued set
K19(K20({0,1},REAL)) is set
1r *' is complex Element of COMPLEX
(Im 1r) * <i> is complex set
(Re 1r) - ((Im 1r) * <i>) is complex set
- ((Im 1r) * <i>) is complex set
(Re 1r) + (- ((Im 1r) * <i>)) is complex set
|.0.| is complex real ext-real V63() Element of REAL
(Re 0) ^2 is complex real ext-real Element of REAL
(Re 0) * (Re 0) is complex real ext-real set
(Im 0) ^2 is complex real ext-real Element of REAL
(Im 0) * (Im 0) is complex real ext-real set
((Re 0) ^2) + ((Im 0) ^2) is complex real ext-real Element of REAL
sqrt (((Re 0) ^2) + ((Im 0) ^2)) is complex real ext-real Element of REAL
|.1r.| is complex real ext-real Element of REAL
(Re 1r) ^2 is complex real ext-real Element of REAL
(Re 1r) * (Re 1r) is complex real ext-real set
(Im 1r) ^2 is complex real ext-real Element of REAL
(Im 1r) * (Im 1r) is complex real ext-real set
((Re 1r) ^2) + ((Im 1r) ^2) is complex real ext-real Element of REAL
sqrt (((Re 1r) ^2) + ((Im 1r) ^2)) is complex real ext-real Element of REAL
0c is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V46() V47() V48() V49() V50() V51() V52() Element of COMPLEX
{0} is non empty V46() V47() V48() V49() V50() V51() set
0 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
1 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
2 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
- 1 is non empty complex real ext-real non positive negative set
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(bq,bq) is complex Element of COMPLEX
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is set
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(a,bq) is complex real ext-real Element of COMPLEX
F₁(bq,a) is complex set
(a,bq) * F₁(bq,a) is complex set
1 * F₁(bq,a) is complex set
0 * F₁(bq,a) is complex set
b is set
th1 is set
bq is Relation-like Function-like set
dom bq is set
a is set
bq . a is set
b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
F₁(bq,b) is complex set
a is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
b is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
th1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
b . th1 is complex Element of COMPLEX
F₁(bq,th1) is complex set
th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
F₁(bq,th2) is complex set
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is set
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(a,bq) is complex real ext-real Element of COMPLEX
F₁(bq,a) is complex real ext-real set
(a,bq) * F₁(bq,a) is complex real ext-real set
1 * F₁(bq,a) is complex real ext-real Element of REAL
0 * F₁(bq,a) is complex real ext-real Element of REAL
b is set
th1 is set
bq is Relation-like Function-like set
dom bq is set
a is set
bq . a is set
b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
F₁(bq,b) is complex real ext-real set
a is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
b is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
th1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
b . th1 is complex real ext-real Element of REAL
F₁(bq,th1) is complex real ext-real set
th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
F₁(bq,th2) is complex real ext-real set
bq is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
bq . 0 is complex real ext-real Element of REAL
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq . (bq + 1) is complex real ext-real Element of REAL
bq . bq is complex real ext-real Element of REAL
(bq . bq) * (bq + 1) is complex real ext-real Element of REAL
bq is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
bq . 0 is complex real ext-real Element of REAL
bq is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
bq . 0 is complex real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq . a is complex real ext-real Element of REAL
bq . a is complex real ext-real Element of REAL
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq . (a + 1) is complex real ext-real Element of REAL
bq . (a + 1) is complex real ext-real Element of REAL
(bq . a) * (a + 1) is complex real ext-real Element of REAL
() is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
bq ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . bq is complex real ext-real Element of REAL
() . 0 is complex real ext-real Element of REAL
0 ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
() . bq is complex real ext-real Element of REAL
bq ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
() . (bq + 1) is complex real ext-real Element of REAL
(() . bq) * (bq + 1) is complex real ext-real Element of REAL
(bq + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is complex real ext-real Element of REAL
a is complex real ext-real Element of REAL
() . 0 is complex real ext-real Element of REAL
() . 1 is complex real ext-real Element of REAL
() . 2 is complex real ext-real Element of REAL
bq is complex set
bq is complex real ext-real set
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . bq is complex real ext-real Element of REAL
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(bq + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . (bq + 1) is complex real ext-real Element of REAL
bq ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . bq is complex real ext-real Element of REAL
(bq !) * (bq + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(bq -' 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . (bq -' 1) is complex real ext-real Element of REAL
((bq -' 1) !) * bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . bq is complex real ext-real Element of REAL
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq -' bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(bq -' bq) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . (bq -' bq) is complex real ext-real Element of REAL
bq + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(bq + 1) - bq is complex real ext-real Element of REAL
- bq is complex real ext-real non positive set
(bq + 1) + (- bq) is complex real ext-real set
((bq -' bq) !) * ((bq + 1) - bq) is complex real ext-real Element of REAL
(bq + 1) -' bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
((bq + 1) -' bq) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . ((bq + 1) -' bq) is complex real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
a -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(a -' 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
a - 1 is complex real ext-real Element of REAL
a + (- 1) is complex real ext-real set
(a - 1) + 1 is complex real ext-real Element of REAL
a ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . a is complex real ext-real Element of REAL
(a -' 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . (a -' 1) is complex real ext-real Element of REAL
((a -' 1) !) * a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(a + 1) -' b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(a + 1) - b is complex real ext-real Element of REAL
- b is complex real ext-real non positive set
(a + 1) + (- b) is complex real ext-real set
a - b is complex real ext-real Element of REAL
a + (- b) is complex real ext-real set
(a - b) + 1 is complex real ext-real Element of REAL
a -' b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(a -' b) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
((a + 1) -' b) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . ((a + 1) -' b) is complex real ext-real Element of REAL
(a -' b) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . (a -' b) is complex real ext-real Element of REAL
0 * <i> is complex set
((a -' b) + 1) + (0 * <i>) is complex set
((a -' b) !) * (((a -' b) + 1) + (0 * <i>)) is complex set
((a - b) + 1) + (0 * <i>) is complex set
((a -' b) !) * (((a - b) + 1) + (0 * <i>)) is complex set
((a -' b) !) * ((a + 1) - b) is complex real ext-real Element of REAL
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . bq is complex real ext-real Element of REAL
bq is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
a is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq . b is complex Element of COMPLEX
b ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . b is complex real ext-real Element of REAL
bq -' b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(bq -' b) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . (bq -' b) is complex real ext-real Element of REAL
(b !) * ((bq -' b) !) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
(bq !) / ((b !) * ((bq -' b) !)) is non empty complex real ext-real positive non negative Element of REAL
((b !) * ((bq -' b) !)) " is non empty complex real ext-real positive non negative set
(bq !) * (((b !) * ((bq -' b) !)) ") is non empty complex real ext-real positive non negative set
a . b is complex Element of COMPLEX
b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq . b is complex Element of COMPLEX
a . b is complex Element of COMPLEX
b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
a is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq . b is complex Element of COMPLEX
b ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . b is complex real ext-real Element of REAL
bq -' b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(bq -' b) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . (bq -' b) is complex real ext-real Element of REAL
(b !) * ((bq -' b) !) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
1r / ((b !) * ((bq -' b) !)) is complex Element of COMPLEX
((b !) * ((bq -' b) !)) " is non empty complex real ext-real positive non negative set
1r * (((b !) * ((bq -' b) !)) ") is complex set
a . b is complex Element of COMPLEX
b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq . b is complex Element of COMPLEX
a . b is complex Element of COMPLEX
b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
bq is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
bq . 0 is complex Element of COMPLEX
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq . (a + 1) is complex Element of COMPLEX
bq . a is complex Element of COMPLEX
bq is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
bq . 0 is complex Element of COMPLEX
a is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
a . 0 is complex Element of COMPLEX
b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq . b is complex Element of COMPLEX
a . b is complex Element of COMPLEX
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq . (b + 1) is complex Element of COMPLEX
a . (b + 1) is complex Element of COMPLEX
bq . b is complex Element of COMPLEX
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
bq is complex Element of COMPLEX
a is complex Element of COMPLEX
b is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
th1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
b . th2 is complex Element of COMPLEX
(bq) . th2 is complex Element of COMPLEX
bq |^ th2 is complex set
bq GeoSeq is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(bq GeoSeq) . th2 is complex Element of COMPLEX
((bq) . th2) * (bq |^ th2) is complex set
bq -' th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
a |^ (bq -' th2) is complex set
a GeoSeq is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(a GeoSeq) . (bq -' th2) is complex Element of COMPLEX
(((bq) . th2) * (bq |^ th2)) * (a |^ (bq -' th2)) is complex set
th1 . th2 is complex Element of COMPLEX
th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
b . th2 is complex Element of COMPLEX
th1 . th2 is complex Element of COMPLEX
th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
bq is complex Element of COMPLEX
a is complex Element of COMPLEX
b is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
th1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
b . th2 is complex Element of COMPLEX
(bq) . th2 is complex Element of COMPLEX
bq |^ th2 is complex set
bq GeoSeq is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(bq GeoSeq) . th2 is complex Element of COMPLEX
((bq) . th2) * (bq |^ th2) is complex set
bq -' th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
a |^ (bq -' th2) is complex set
a GeoSeq is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(a GeoSeq) . (bq -' th2) is complex Element of COMPLEX
(((bq) . th2) * (bq |^ th2)) * (a |^ (bq -' th2)) is complex set
th1 . th2 is complex Element of COMPLEX
th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
b . th2 is complex Element of COMPLEX
th1 . th2 is complex Element of COMPLEX
th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is complex Element of COMPLEX
(bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
a is complex Element of COMPLEX
(a) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Partial_Sums (a) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
b is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
th1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
b . th2 is complex Element of COMPLEX
(bq) . th2 is complex Element of COMPLEX
bq -' th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(Partial_Sums (a)) . (bq -' th2) is complex Element of COMPLEX
((bq) . th2) * ((Partial_Sums (a)) . (bq -' th2)) is complex Element of COMPLEX
th1 . th2 is complex Element of COMPLEX
th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
b . th2 is complex Element of COMPLEX
th1 . th2 is complex Element of COMPLEX
th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is complex real ext-real set
(bq) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
bq is complex real ext-real set
(bq) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums (bq) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(Partial_Sums (bq)) . a is complex real ext-real Element of REAL
b is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
th1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
b . th2 is complex real ext-real Element of REAL
(bq) . th2 is complex real ext-real Element of REAL
a -' th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(Partial_Sums (bq)) . (a -' th2) is complex real ext-real Element of REAL
((Partial_Sums (bq)) . a) - ((Partial_Sums (bq)) . (a -' th2)) is complex real ext-real Element of REAL
- ((Partial_Sums (bq)) . (a -' th2)) is complex real ext-real set
((Partial_Sums (bq)) . a) + (- ((Partial_Sums (bq)) . (a -' th2))) is complex real ext-real set
((bq) . th2) * (((Partial_Sums (bq)) . a) - ((Partial_Sums (bq)) . (a -' th2))) is complex real ext-real Element of REAL
th1 . th2 is complex real ext-real Element of REAL
th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
b . th2 is complex real ext-real Element of REAL
th1 . th2 is complex real ext-real Element of REAL
th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is complex Element of COMPLEX
(bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
bq is complex Element of COMPLEX
(bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Partial_Sums (bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(Partial_Sums (bq)) . a is complex Element of COMPLEX
b is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
th1 is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
b . th2 is complex Element of COMPLEX
(bq) . th2 is complex Element of COMPLEX
a -' th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(Partial_Sums (bq)) . (a -' th2) is complex Element of COMPLEX
((Partial_Sums (bq)) . a) - ((Partial_Sums (bq)) . (a -' th2)) is complex Element of COMPLEX
- ((Partial_Sums (bq)) . (a -' th2)) is complex set
((Partial_Sums (bq)) . a) + (- ((Partial_Sums (bq)) . (a -' th2))) is complex set
((bq) . th2) * (((Partial_Sums (bq)) . a) - ((Partial_Sums (bq)) . (a -' th2))) is complex Element of COMPLEX
th1 . th2 is complex Element of COMPLEX
th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
b . th2 is complex Element of COMPLEX
th1 . th2 is complex Element of COMPLEX
th2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is complex real ext-real Element of REAL
a is complex real ext-real Element of REAL
a * <i> is complex set
bq + (a * <i>) is complex set
bq is complex real ext-real Element of REAL
b is complex real ext-real Element of REAL
b * <i> is complex set
bq + (b * <i>) is complex set
(bq + (a * <i>)) * (bq + (b * <i>)) is complex set
bq * bq is complex real ext-real Element of REAL
a * b is complex real ext-real Element of REAL
(bq * bq) - (a * b) is complex real ext-real Element of REAL
- (a * b) is complex real ext-real set
(bq * bq) + (- (a * b)) is complex real ext-real set
bq * b is complex real ext-real Element of REAL
bq * a is complex real ext-real Element of REAL
(bq * b) + (bq * a) is complex real ext-real Element of REAL
((bq * b) + (bq * a)) * <i> is complex set
((bq * bq) - (a * b)) + (((bq * b) + (bq * a)) * <i>) is complex set
(bq + (b * <i>)) *' is complex Element of COMPLEX
Re (bq + (b * <i>)) is complex real ext-real Element of REAL
Im (bq + (b * <i>)) is complex real ext-real Element of REAL
(Im (bq + (b * <i>))) * <i> is complex set
(Re (bq + (b * <i>))) - ((Im (bq + (b * <i>))) * <i>) is complex set
- ((Im (bq + (b * <i>))) * <i>) is complex set
(Re (bq + (b * <i>))) + (- ((Im (bq + (b * <i>))) * <i>)) is complex set
- b is complex real ext-real Element of REAL
(- b) * <i> is complex set
bq + ((- b) * <i>) is complex set
bq - ((Im (bq + (b * <i>))) * <i>) is complex set
bq + (- ((Im (bq + (b * <i>))) * <i>)) is complex set
bq - (b * <i>) is complex set
- (b * <i>) is complex set
bq + (- (b * <i>)) is complex set
0 * <i> is complex set
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(bq + 1) + (0 * <i>) is complex set
bq is complex set
(bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(bq) . (bq + 1) is complex Element of COMPLEX
(bq) . bq is complex Element of COMPLEX
((bq) . bq) * bq is complex set
(((bq) . bq) * bq) / ((bq + 1) + (0 * <i>)) is complex Element of COMPLEX
((bq + 1) + (0 * <i>)) " is complex set
(((bq) . bq) * bq) * (((bq + 1) + (0 * <i>)) ") is complex set
(bq) . 0 is complex Element of COMPLEX
|.((bq) . bq).| is complex real ext-real Element of REAL
Re ((bq) . bq) is complex real ext-real Element of REAL
(Re ((bq) . bq)) ^2 is complex real ext-real Element of REAL
(Re ((bq) . bq)) * (Re ((bq) . bq)) is complex real ext-real set
Im ((bq) . bq) is complex real ext-real Element of REAL
(Im ((bq) . bq)) ^2 is complex real ext-real Element of REAL
(Im ((bq) . bq)) * (Im ((bq) . bq)) is complex real ext-real set
((Re ((bq) . bq)) ^2) + ((Im ((bq) . bq)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((bq) . bq)) ^2) + ((Im ((bq) . bq)) ^2)) is complex real ext-real Element of REAL
|.bq.| is complex real ext-real Element of REAL
Re bq is complex real ext-real Element of REAL
(Re bq) ^2 is complex real ext-real Element of REAL
(Re bq) * (Re bq) is complex real ext-real set
Im bq is complex real ext-real Element of REAL
(Im bq) ^2 is complex real ext-real Element of REAL
(Im bq) * (Im bq) is complex real ext-real set
((Re bq) ^2) + ((Im bq) ^2) is complex real ext-real Element of REAL
sqrt (((Re bq) ^2) + ((Im bq) ^2)) is complex real ext-real Element of REAL
(|.bq.|) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(|.bq.|) . bq is complex real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(bq) . (a + 1) is complex Element of COMPLEX
bq |^ (a + 1) is complex set
bq GeoSeq is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(bq GeoSeq) . (a + 1) is complex Element of COMPLEX
(a + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . (a + 1) is complex real ext-real Element of REAL
(bq |^ (a + 1)) / ((a + 1) !) is complex Element of COMPLEX
((a + 1) !) " is non empty complex real ext-real positive non negative set
(bq |^ (a + 1)) * (((a + 1) !) ") is complex set
(bq GeoSeq) . a is complex Element of COMPLEX
((bq GeoSeq) . a) * bq is complex set
(((bq GeoSeq) . a) * bq) / ((a + 1) !) is complex Element of COMPLEX
(((bq GeoSeq) . a) * bq) * (((a + 1) !) ") is complex set
bq |^ a is complex set
(bq |^ a) * bq is complex set
a ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . a is complex real ext-real Element of REAL
(a + 1) + (0 * <i>) is complex set
(a !) * ((a + 1) + (0 * <i>)) is complex set
((bq |^ a) * bq) / ((a !) * ((a + 1) + (0 * <i>))) is complex Element of COMPLEX
((a !) * ((a + 1) + (0 * <i>))) " is complex set
((bq |^ a) * bq) * (((a !) * ((a + 1) + (0 * <i>))) ") is complex set
(bq |^ a) / (a !) is complex Element of COMPLEX
(a !) " is non empty complex real ext-real positive non negative set
(bq |^ a) * ((a !) ") is complex set
bq / ((a + 1) + (0 * <i>)) is complex Element of COMPLEX
((a + 1) + (0 * <i>)) " is complex set
bq * (((a + 1) + (0 * <i>)) ") is complex set
((bq |^ a) / (a !)) * (bq / ((a + 1) + (0 * <i>))) is complex Element of COMPLEX
((bq |^ a) / (a !)) * bq is complex set
(((bq |^ a) / (a !)) * bq) / ((a + 1) + (0 * <i>)) is complex Element of COMPLEX
(((bq |^ a) / (a !)) * bq) * (((a + 1) + (0 * <i>)) ") is complex set
(bq) . a is complex Element of COMPLEX
((bq) . a) * bq is complex set
(((bq) . a) * bq) / ((a + 1) + (0 * <i>)) is complex Element of COMPLEX
(((bq) . a) * bq) * (((a + 1) + (0 * <i>)) ") is complex set
bq |^ 0 is complex set
(bq GeoSeq) . 0 is complex Element of COMPLEX
(bq |^ 0) / (0 !) is complex Element of COMPLEX
(0 !) " is non empty complex real ext-real positive non negative set
(bq |^ 0) * ((0 !) ") is complex set
(|.bq.|) . 0 is complex real ext-real Element of REAL
|.bq.| |^ 0 is complex real ext-real Element of REAL
|.bq.| GeoSeq is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(|.bq.| GeoSeq) . 0 is complex Element of COMPLEX
(|.bq.| |^ 0) / (0 !) is complex real ext-real Element of REAL
(|.bq.| |^ 0) * ((0 !) ") is complex real ext-real set
1 / (() . 0) is complex real ext-real Element of REAL
(() . 0) " is complex real ext-real set
1 * ((() . 0) ") is complex real ext-real set
1 / 1 is non empty complex real ext-real positive non negative Element of REAL
1 " is non empty complex real ext-real positive non negative set
1 * (1 ") is non empty complex real ext-real positive non negative set
|.((bq) . 0).| is complex real ext-real Element of REAL
Re ((bq) . 0) is complex real ext-real Element of REAL
(Re ((bq) . 0)) ^2 is complex real ext-real Element of REAL
(Re ((bq) . 0)) * (Re ((bq) . 0)) is complex real ext-real set
Im ((bq) . 0) is complex real ext-real Element of REAL
(Im ((bq) . 0)) ^2 is complex real ext-real Element of REAL
(Im ((bq) . 0)) * (Im ((bq) . 0)) is complex real ext-real set
((Re ((bq) . 0)) ^2) + ((Im ((bq) . 0)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((bq) . 0)) ^2) + ((Im ((bq) . 0)) ^2)) is complex real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(bq) . a is complex Element of COMPLEX
|.((bq) . a).| is complex real ext-real Element of REAL
Re ((bq) . a) is complex real ext-real Element of REAL
(Re ((bq) . a)) ^2 is complex real ext-real Element of REAL
(Re ((bq) . a)) * (Re ((bq) . a)) is complex real ext-real set
Im ((bq) . a) is complex real ext-real Element of REAL
(Im ((bq) . a)) ^2 is complex real ext-real Element of REAL
(Im ((bq) . a)) * (Im ((bq) . a)) is complex real ext-real set
((Re ((bq) . a)) ^2) + ((Im ((bq) . a)) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((bq) . a)) ^2) + ((Im ((bq) . a)) ^2)) is complex real ext-real Element of REAL
(|.bq.|) . a is complex real ext-real Element of REAL
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(a + 1) + (0 * <i>) is complex set
|.((a + 1) + (0 * <i>)).| is complex real ext-real Element of REAL
Re ((a + 1) + (0 * <i>)) is complex real ext-real Element of REAL
(Re ((a + 1) + (0 * <i>))) ^2 is complex real ext-real Element of REAL
(Re ((a + 1) + (0 * <i>))) * (Re ((a + 1) + (0 * <i>))) is complex real ext-real set
Im ((a + 1) + (0 * <i>)) is complex real ext-real Element of REAL
(Im ((a + 1) + (0 * <i>))) ^2 is complex real ext-real Element of REAL
(Im ((a + 1) + (0 * <i>))) * (Im ((a + 1) + (0 * <i>))) is complex real ext-real set
((Re ((a + 1) + (0 * <i>))) ^2) + ((Im ((a + 1) + (0 * <i>))) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((a + 1) + (0 * <i>))) ^2) + ((Im ((a + 1) + (0 * <i>))) ^2)) is complex real ext-real Element of REAL
(bq) . (a + 1) is complex Element of COMPLEX
|.((bq) . (a + 1)).| is complex real ext-real Element of REAL
Re ((bq) . (a + 1)) is complex real ext-real Element of REAL
(Re ((bq) . (a + 1))) ^2 is complex real ext-real Element of REAL
(Re ((bq) . (a + 1))) * (Re ((bq) . (a + 1))) is complex real ext-real set
Im ((bq) . (a + 1)) is complex real ext-real Element of REAL
(Im ((bq) . (a + 1))) ^2 is complex real ext-real Element of REAL
(Im ((bq) . (a + 1))) * (Im ((bq) . (a + 1))) is complex real ext-real set
((Re ((bq) . (a + 1))) ^2) + ((Im ((bq) . (a + 1))) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((bq) . (a + 1))) ^2) + ((Im ((bq) . (a + 1))) ^2)) is complex real ext-real Element of REAL
((bq) . a) * bq is complex set
(((bq) . a) * bq) / ((a + 1) + (0 * <i>)) is complex Element of COMPLEX
((a + 1) + (0 * <i>)) " is complex set
(((bq) . a) * bq) * (((a + 1) + (0 * <i>)) ") is complex set
|.((((bq) . a) * bq) / ((a + 1) + (0 * <i>))).| is complex real ext-real Element of REAL
Re ((((bq) . a) * bq) / ((a + 1) + (0 * <i>))) is complex real ext-real Element of REAL
(Re ((((bq) . a) * bq) / ((a + 1) + (0 * <i>)))) ^2 is complex real ext-real Element of REAL
(Re ((((bq) . a) * bq) / ((a + 1) + (0 * <i>)))) * (Re ((((bq) . a) * bq) / ((a + 1) + (0 * <i>)))) is complex real ext-real set
Im ((((bq) . a) * bq) / ((a + 1) + (0 * <i>))) is complex real ext-real Element of REAL
(Im ((((bq) . a) * bq) / ((a + 1) + (0 * <i>)))) ^2 is complex real ext-real Element of REAL
(Im ((((bq) . a) * bq) / ((a + 1) + (0 * <i>)))) * (Im ((((bq) . a) * bq) / ((a + 1) + (0 * <i>)))) is complex real ext-real set
((Re ((((bq) . a) * bq) / ((a + 1) + (0 * <i>)))) ^2) + ((Im ((((bq) . a) * bq) / ((a + 1) + (0 * <i>)))) ^2) is complex real ext-real Element of REAL
sqrt (((Re ((((bq) . a) * bq) / ((a + 1) + (0 * <i>)))) ^2) + ((Im ((((bq) . a) * bq) / ((a + 1) + (0 * <i>)))) ^2)) is complex real ext-real Element of REAL
|.(((bq) . a) * bq).| is complex real ext-real Element of REAL
Re (((bq) . a) * bq) is complex real ext-real Element of REAL
(Re (((bq) . a) * bq)) ^2 is complex real ext-real Element of REAL
(Re (((bq) . a) * bq)) * (Re (((bq) . a) * bq)) is complex real ext-real set
Im (((bq) . a) * bq) is complex real ext-real Element of REAL
(Im (((bq) . a) * bq)) ^2 is complex real ext-real Element of REAL
(Im (((bq) . a) * bq)) * (Im (((bq) . a) * bq)) is complex real ext-real set
((Re (((bq) . a) * bq)) ^2) + ((Im (((bq) . a) * bq)) ^2) is complex real ext-real Element of REAL
sqrt (((Re (((bq) . a) * bq)) ^2) + ((Im (((bq) . a) * bq)) ^2)) is complex real ext-real Element of REAL
|.(((bq) . a) * bq).| / |.((a + 1) + (0 * <i>)).| is complex real ext-real Element of REAL
|.((a + 1) + (0 * <i>)).| " is complex real ext-real set
|.(((bq) . a) * bq).| * (|.((a + 1) + (0 * <i>)).| ") is complex real ext-real set
((|.bq.|) . a) * |.bq.| is complex real ext-real Element of REAL
(((|.bq.|) . a) * |.bq.|) / |.((a + 1) + (0 * <i>)).| is complex real ext-real Element of REAL
(((|.bq.|) . a) * |.bq.|) * (|.((a + 1) + (0 * <i>)).| ") is complex real ext-real set
|.bq.| |^ a is complex real ext-real Element of REAL
(|.bq.| GeoSeq) . a is complex Element of COMPLEX
a ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . a is complex real ext-real Element of REAL
(|.bq.| |^ a) / (a !) is complex real ext-real Element of REAL
(a !) " is non empty complex real ext-real positive non negative set
(|.bq.| |^ a) * ((a !) ") is complex real ext-real set
((|.bq.| |^ a) / (a !)) * |.bq.| is complex real ext-real Element of REAL
(((|.bq.| |^ a) / (a !)) * |.bq.|) / |.((a + 1) + (0 * <i>)).| is complex real ext-real Element of REAL
(((|.bq.| |^ a) / (a !)) * |.bq.|) * (|.((a + 1) + (0 * <i>)).| ") is complex real ext-real set
(|.bq.| |^ a) * |.bq.| is complex real ext-real Element of REAL
(a !) * |.((a + 1) + (0 * <i>)).| is complex real ext-real Element of REAL
((|.bq.| |^ a) * |.bq.|) / ((a !) * |.((a + 1) + (0 * <i>)).|) is complex real ext-real Element of REAL
((a !) * |.((a + 1) + (0 * <i>)).|) " is complex real ext-real set
((|.bq.| |^ a) * |.bq.|) * (((a !) * |.((a + 1) + (0 * <i>)).|) ") is complex real ext-real set
(a + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of REAL
() . (a + 1) is complex real ext-real Element of REAL
((|.bq.| |^ a) * |.bq.|) / ((a + 1) !) is complex real ext-real Element of REAL
((a + 1) !) " is non empty complex real ext-real positive non negative set
((|.bq.| |^ a) * |.bq.|) * (((a + 1) !) ") is complex real ext-real set
|.bq.| |^ (a + 1) is complex real ext-real Element of REAL
(|.bq.| GeoSeq) . (a + 1) is complex Element of COMPLEX
(|.bq.| |^ (a + 1)) / ((a + 1) !) is complex real ext-real Element of REAL
(|.bq.| |^ (a + 1)) * (((a + 1) !) ") is complex real ext-real set
(|.bq.|) . (a + 1) is complex real ext-real Element of REAL
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq -' 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(bq) . bq is complex Element of COMPLEX
bq . (bq -' 1) is complex Element of COMPLEX
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq - 1 is complex real ext-real Element of REAL
bq + (- 1) is complex real ext-real set
bq . a is complex Element of COMPLEX
bq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
bq is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Partial_Sums bq is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(Partial_Sums bq) . bq is complex Element of COMPLEX
(bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Partial_Sums (bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(Partial_Sums (bq)) . bq is complex Element of COMPLEX
bq . bq is complex Element of COMPLEX
((Partial_Sums (bq)) . bq) + (bq . bq) is complex Element of COMPLEX
(Partial_Sums bq) . 0 is complex Element of COMPLEX
bq . 0 is complex Element of COMPLEX
0c + (bq . 0) is complex Element of COMPLEX
(bq) . 0 is complex Element of COMPLEX
((bq) . 0) + (bq . 0) is complex Element of COMPLEX
(Partial_Sums (bq)) . 0 is complex Element of COMPLEX
((Partial_Sums (bq)) . 0) + (bq . 0) is complex Element of COMPLEX
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(Partial_Sums bq) . a is complex Element of COMPLEX
(Partial_Sums (bq)) . a is complex Element of COMPLEX
bq . a is complex Element of COMPLEX
((Partial_Sums (bq)) . a) + (bq . a) is complex Element of COMPLEX
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(Partial_Sums bq) . (a + 1) is complex Element of COMPLEX
(Partial_Sums (bq)) . (a + 1) is complex Element of COMPLEX
bq . (a + 1) is complex Element of COMPLEX
((Partial_Sums (bq)) . (a + 1)) + (bq . (a + 1)) is complex Element of COMPLEX
(((Partial_Sums (bq)) . a) + (bq . a)) + (bq . (a + 1)) is complex Element of COMPLEX
(bq) . (a + 1) is complex Element of COMPLEX
((Partial_Sums (bq)) . a) + ((bq) . (a + 1)) is complex Element of COMPLEX
(((Partial_Sums (bq)) . a) + ((bq) . (a + 1))) + (bq . (a + 1)) is complex Element of COMPLEX
bq is complex Element of COMPLEX
bq is complex Element of COMPLEX
bq + bq is complex Element of COMPLEX
a is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(bq + bq) |^ a is complex set
(bq + bq) GeoSeq is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((bq + bq) GeoSeq) . a is complex Element of COMPLEX
(a,bq,bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Partial_Sums (a,bq,bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(Partial_Sums (a,bq,bq)) . a is complex Element of COMPLEX
0 -' 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(0,bq,bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Partial_Sums (0,bq,bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(Partial_Sums (0,bq,bq)) . 0 is complex Element of COMPLEX
(0,bq,bq) . 0 is complex Element of COMPLEX
(0) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(0) . 0 is complex Element of COMPLEX
bq |^ 0 is complex set
bq GeoSeq is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(bq GeoSeq) . 0 is complex Element of COMPLEX
((0) . 0) * (bq |^ 0) is complex set
bq |^ 0 is complex set
bq GeoSeq is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(bq GeoSeq) . 0 is complex Element of COMPLEX
(((0) . 0) * (bq |^ 0)) * (bq |^ 0) is complex set
1 * 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
1 / (1 * 1) is non empty complex real ext-real positive non negative Element of REAL
(1 * 1) " is non empty complex real ext-real positive non negative set
1 * ((1 * 1) ") is non empty complex real ext-real positive non negative set
(1 / (1 * 1)) * (bq |^ 0) is complex set
((1 / (1 * 1)) * (bq |^ 0)) * (bq |^ 0) is complex set
1r * ((bq GeoSeq) . 0) is complex Element of COMPLEX
(bq + bq) |^ 0 is complex set
((bq + bq) GeoSeq) . 0 is complex Element of COMPLEX
b is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(bq + bq) |^ b is complex set
((bq + bq) GeoSeq) . b is complex Element of COMPLEX
(b,bq,bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Partial_Sums (b,bq,bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(Partial_Sums (b,bq,bq)) . b is complex Element of COMPLEX
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
(bq + bq) |^ (b + 1) is complex set
((bq + bq) GeoSeq) . (b + 1) is complex Element of COMPLEX
((b + 1),bq,bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Partial_Sums ((b + 1),bq,bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(Partial_Sums ((b + 1),bq,bq)) . (b + 1) is complex Element of COMPLEX
(((bq + bq) GeoSeq) . b) * (bq + bq) is complex Element of COMPLEX
(bq + bq) (#) (Partial_Sums (b,bq,bq)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
((bq + bq) (#) (Partial_Sums (b,bq,bq))) . b is complex Element of COMPLEX
(bq + bq) (#) (b,bq,bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
Partial_Sums ((bq + bq) (#) (b,bq,bq)) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(Partial_Sums ((bq + bq) (#) (b,bq,bq))) . b is complex Element of COMPLEX
th1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V46() V47() V48() V49() V50() V51() V62() V63() Element of NAT
((bq + bq) (#) (b,bq,bq)) . th1 is complex Element of COMPLEX
(b,bq,bq) . th1 is complex Element of COMPLEX
(bq + bq) * ((b,bq,bq) . th1) is complex Element of COMPLEX
bq * ((b,bq,bq) . th1) is complex Element of COMPLEX
bq * ((b,bq,bq) . th1) is complex Element of COMPLEX
(bq * ((b,bq,bq) . th1)) + (bq * ((b,bq,bq) . th1)) is complex Element of COMPLEX
bq (#) (b,bq,bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(bq (#) (b,bq,bq)) . th1 is complex Element of COMPLEX
((bq (#) (b,bq,bq)) . th1) + (bq * ((b,bq,bq) . th1)) is complex Element of COMPLEX
bq (#) (b,bq,bq) is Relation-like NAT -defined COMPLEX -valued Function-like non empty total quasi_total complex-valued Element of K19(K20(NAT,COMPLEX))
(bq (#) (b,bq,bq)) . th1 is complex Element of