:: COMSEQ_3 semantic presentation

REAL is non zero V50() V62() V63() V64() V68() set
NAT is non zero epsilon-transitive epsilon-connected ordinal V62() V63() V64() V65() V66() V67() V68() Element of K19(REAL)
K19(REAL) is set
0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V62() V63() V64() V65() V66() V67() V68() set
1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
{0,1} is non zero V62() V63() V64() V65() V66() V67() set
INT is non zero V50() V62() V63() V64() V65() V66() V68() set
COMPLEX is non zero V50() V62() V68() set
omega is non zero epsilon-transitive epsilon-connected ordinal V62() V63() V64() V65() V66() V67() V68() set
K19(omega) is set
K19(NAT) is set
RAT is non zero V50() V62() V63() V64() V65() V68() set
K20(NAT,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
K20(COMPLEX,COMPLEX) is complex-valued set
K19(K20(COMPLEX,COMPLEX)) is set
K20(COMPLEX,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(COMPLEX,REAL)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(REAL,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) 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 zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V48() V61() V62() V63() V64() V65() V66() V67() V68() Element of NAT
2 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
1r is complex Element of COMPLEX
<i> is complex Element of COMPLEX
|.0.| is complex real ext-real V61() Element of REAL
|.1r.| is complex real ext-real Element of REAL
K20(NAT,COMPLEX) is complex-valued set
K19(K20(NAT,COMPLEX)) is set
K19(K20(NAT,NAT)) is set
0c is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V62() V63() V64() V65() V66() V67() V68() Element of COMPLEX
0 * <i> is complex set
0 + (0 * <i>) is complex set
C is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
C + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
D + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(D + 1) * <i> is complex set
C is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs C is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums (abs C) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
D is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(abs C) . D is complex real ext-real Element of REAL
(Partial_Sums (abs C)) . D is complex real ext-real Element of REAL
D + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(abs C) . (D + 1) is complex real ext-real Element of REAL
(Partial_Sums (abs C)) . (D + 1) is complex real ext-real Element of REAL
0 + ((abs C) . (D + 1)) is complex real ext-real Element of REAL
abs 0 is complex real ext-real V61() Element of REAL
(abs 0) + ((abs C) . (D + 1)) is complex real ext-real Element of REAL
C . D is complex real ext-real Element of REAL
abs (C . D) is complex real ext-real Element of REAL
(abs (C . D)) + ((abs C) . (D + 1)) is complex real ext-real Element of REAL
((Partial_Sums (abs C)) . D) + ((abs C) . (D + 1)) is complex real ext-real Element of REAL
D is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums (abs C)) . D is complex real ext-real Element of REAL
(abs C) . 0 is complex real ext-real Element of REAL
(Partial_Sums (abs C)) . 0 is complex real ext-real Element of REAL
(abs C) . D is complex real ext-real Element of REAL
C . D is complex real ext-real Element of REAL
abs (C . D) is complex real ext-real Element of REAL
abs 0 is complex real ext-real V61() Element of REAL
C is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs C is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums (abs C) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
D is complex real ext-real set
seq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums (abs C)) . seq is complex real ext-real Element of REAL
((Partial_Sums (abs C)) . seq) - 0 is complex real ext-real Element of REAL
abs (((Partial_Sums (abs C)) . seq) - 0) is complex real ext-real Element of REAL
(Partial_Sums (abs C)) . seq is complex real ext-real Element of REAL
((Partial_Sums (abs C)) . seq) - 0 is complex real ext-real Element of REAL
abs (((Partial_Sums (abs C)) . seq) - 0) is complex real ext-real Element of REAL
0 - 0 is zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V62() V63() V64() V65() V66() V67() V68() Element of REAL
abs (0 - 0) is complex real ext-real Element of REAL
NAT --> 0 is Relation-like NAT -defined NAT -valued INT -valued RAT -valued Function-like constant non zero total V18( NAT , NAT ) T-Sequence-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(NAT,NAT))
C is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
D is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
C . D is complex real ext-real Element of REAL
D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is complex real ext-real Element of REAL
seq / 2 is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
D . m is complex real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
D . n is complex real ext-real Element of REAL
(D . n) - (D . m) is complex real ext-real Element of REAL
abs ((D . n) - (D . m)) is complex real ext-real Element of REAL
D . n is complex real ext-real Element of REAL
(D . n) - (D . m) is complex real ext-real Element of REAL
abs ((D . n) - (D . m)) is complex real ext-real Element of REAL
(seq / 2) + (seq / 2) is complex real ext-real Element of REAL
(abs ((D . n) - (D . m))) + (abs ((D . n) - (D . m))) is complex real ext-real Element of REAL
(D . n) - (D . n) is complex real ext-real Element of REAL
abs ((D . n) - (D . n)) is complex real ext-real Element of REAL
((D . n) - (D . m)) - ((D . n) - (D . m)) is complex real ext-real Element of REAL
abs (((D . n) - (D . m)) - ((D . n) - (D . m))) is complex real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
D . n is complex real ext-real Element of REAL
D . n is complex real ext-real Element of REAL
(D . n) - (D . n) is complex real ext-real Element of REAL
abs ((D . n) - (D . n)) is complex real ext-real Element of REAL
D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums D) . m is complex real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
m + n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums D) . (m + n) is complex real ext-real Element of REAL
((Partial_Sums D) . (m + n)) - ((Partial_Sums D) . m) is complex real ext-real Element of REAL
seq * n is complex real ext-real Element of REAL
(m + n) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
D . ((m + n) + 1) is complex real ext-real Element of REAL
(seq * n) + (D . ((m + n) + 1)) is complex real ext-real Element of REAL
(seq * n) + seq is complex real ext-real Element of REAL
n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
m + (n + 1) is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums D) . (m + (n + 1)) is complex real ext-real Element of REAL
((Partial_Sums D) . (m + (n + 1))) - ((Partial_Sums D) . m) is complex real ext-real Element of REAL
((Partial_Sums D) . (m + n)) + (D . ((m + n) + 1)) is complex real ext-real Element of REAL
(((Partial_Sums D) . (m + n)) + (D . ((m + n) + 1))) - ((Partial_Sums D) . m) is complex real ext-real Element of REAL
(((Partial_Sums D) . (m + n)) - ((Partial_Sums D) . m)) + (D . ((m + n) + 1)) is complex real ext-real Element of REAL
seq * (n + 1) is complex real ext-real Element of REAL
m + 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums D) . (m + 0) is complex real ext-real Element of REAL
((Partial_Sums D) . (m + 0)) - ((Partial_Sums D) . m) is complex real ext-real Element of REAL
seq * 0 is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
m + n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums D) . (m + n) is complex real ext-real Element of REAL
(Partial_Sums D) . m is complex real ext-real Element of REAL
((Partial_Sums D) . (m + n)) - ((Partial_Sums D) . m) is complex real ext-real Element of REAL
seq * n is complex real ext-real Element of REAL
D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums D) . m is complex real ext-real Element of REAL
m + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
seq * (m + 1) is complex real ext-real Element of REAL
D . (m + 1) is complex real ext-real Element of REAL
(seq * (m + 1)) + (D . (m + 1)) is complex real ext-real Element of REAL
(seq * (m + 1)) + seq is complex real ext-real Element of REAL
(Partial_Sums D) . (m + 1) is complex real ext-real Element of REAL
((Partial_Sums D) . m) + (D . (m + 1)) is complex real ext-real Element of REAL
(m + 1) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
seq * ((m + 1) + 1) is complex real ext-real Element of REAL
(Partial_Sums D) . 0 is complex real ext-real Element of REAL
D . 0 is complex real ext-real Element of REAL
0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
seq * (0 + 1) is complex real ext-real Element of REAL
D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums seq is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums D) . m is complex real ext-real Element of REAL
(Partial_Sums seq) . m is complex real ext-real Element of REAL
n is complex real ext-real Element of REAL
n * ((Partial_Sums seq) . m) is complex real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums D) . n is complex real ext-real Element of REAL
(Partial_Sums seq) . n is complex real ext-real Element of REAL
n * ((Partial_Sums seq) . n) is complex real ext-real Element of REAL
n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
D . (n + 1) is complex real ext-real Element of REAL
seq . (n + 1) is complex real ext-real Element of REAL
n * (seq . (n + 1)) is complex real ext-real Element of REAL
(n * ((Partial_Sums seq) . n)) + (D . (n + 1)) is complex real ext-real Element of REAL
(n * ((Partial_Sums seq) . n)) + (n * (seq . (n + 1))) is complex real ext-real Element of REAL
(Partial_Sums D) . (n + 1) is complex real ext-real Element of REAL
((Partial_Sums D) . n) + (D . (n + 1)) is complex real ext-real Element of REAL
((Partial_Sums seq) . n) + (seq . (n + 1)) is complex real ext-real Element of REAL
n * (((Partial_Sums seq) . n) + (seq . (n + 1))) is complex real ext-real Element of REAL
(Partial_Sums seq) . (n + 1) is complex real ext-real Element of REAL
n * ((Partial_Sums seq) . (n + 1)) is complex real ext-real Element of REAL
(Partial_Sums D) . 0 is complex real ext-real Element of REAL
(Partial_Sums seq) . 0 is complex real ext-real Element of REAL
n * ((Partial_Sums seq) . 0) is complex real ext-real Element of REAL
D . 0 is complex real ext-real Element of REAL
seq . 0 is complex real ext-real Element of REAL
n * (seq . 0) is complex real ext-real Element of REAL
D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums seq is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
n is complex real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums D) . n is complex real ext-real Element of REAL
(Partial_Sums seq) . n is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
n + m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums D) . (n + m) is complex real ext-real Element of REAL
((Partial_Sums D) . (n + m)) - ((Partial_Sums D) . n) is complex real ext-real Element of REAL
(Partial_Sums seq) . (n + m) is complex real ext-real Element of REAL
((Partial_Sums seq) . (n + m)) - ((Partial_Sums seq) . n) is complex real ext-real Element of REAL
n * (((Partial_Sums seq) . (n + m)) - ((Partial_Sums seq) . n)) is complex real ext-real Element of REAL
m + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
n + (m + 1) is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums D) . (n + (m + 1)) is complex real ext-real Element of REAL
((Partial_Sums D) . (n + (m + 1))) - ((Partial_Sums D) . n) is complex real ext-real Element of REAL
(Partial_Sums seq) . (n + (m + 1)) is complex real ext-real Element of REAL
((Partial_Sums seq) . (n + (m + 1))) - ((Partial_Sums seq) . n) is complex real ext-real Element of REAL
n * (((Partial_Sums seq) . (n + (m + 1))) - ((Partial_Sums seq) . n)) is complex real ext-real Element of REAL
(n + m) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
D . ((n + m) + 1) is complex real ext-real Element of REAL
((Partial_Sums D) . (n + m)) + (D . ((n + m) + 1)) is complex real ext-real Element of REAL
seq . ((n + m) + 1) is complex real ext-real Element of REAL
n * (seq . ((n + m) + 1)) is complex real ext-real Element of REAL
((Partial_Sums D) . (n + m)) + (n * (seq . ((n + m) + 1))) is complex real ext-real Element of REAL
(((Partial_Sums D) . (n + m)) + (n * (seq . ((n + m) + 1)))) - ((Partial_Sums D) . n) is complex real ext-real Element of REAL
(((Partial_Sums D) . (n + m)) - ((Partial_Sums D) . n)) + (n * (seq . ((n + m) + 1))) is complex real ext-real Element of REAL
(n * (((Partial_Sums seq) . (n + m)) - ((Partial_Sums seq) . n))) + (n * (seq . ((n + m) + 1))) is complex real ext-real Element of REAL
((Partial_Sums seq) . (n + m)) + (seq . ((n + m) + 1)) is complex real ext-real Element of REAL
(((Partial_Sums seq) . (n + m)) + (seq . ((n + m) + 1))) - ((Partial_Sums seq) . n) is complex real ext-real Element of REAL
n * ((((Partial_Sums seq) . (n + m)) + (seq . ((n + m) + 1))) - ((Partial_Sums seq) . n)) is complex real ext-real Element of REAL
n + 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums D) . (n + 0) is complex real ext-real Element of REAL
((Partial_Sums D) . (n + 0)) - ((Partial_Sums D) . n) is complex real ext-real Element of REAL
(Partial_Sums seq) . (n + 0) is complex real ext-real Element of REAL
((Partial_Sums seq) . (n + 0)) - ((Partial_Sums seq) . n) is complex real ext-real Element of REAL
n * (((Partial_Sums seq) . (n + 0)) - ((Partial_Sums seq) . n)) is complex real ext-real Element of REAL
D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Partial_Sums D is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums D) . seq is complex real ext-real Element of REAL
(Partial_Sums D) . m is complex real ext-real Element of REAL
((Partial_Sums D) . seq) - ((Partial_Sums D) . seq) is complex real ext-real Element of REAL
((Partial_Sums D) . m) - ((Partial_Sums D) . seq) is complex real ext-real Element of REAL
abs (((Partial_Sums D) . m) - ((Partial_Sums D) . seq)) is complex real ext-real Element of REAL
(Partial_Sums D) . 0 is complex real ext-real Element of REAL
seq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums D) . seq is complex real ext-real Element of REAL
D . 0 is complex real ext-real Element of REAL
abs ((Partial_Sums D) . seq) is complex real ext-real Element of REAL
seq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums D) . m is complex real ext-real Element of REAL
(Partial_Sums D) . seq is complex real ext-real Element of REAL
((Partial_Sums D) . m) - ((Partial_Sums D) . seq) is complex real ext-real Element of REAL
abs (((Partial_Sums D) . m) - ((Partial_Sums D) . seq)) is complex real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(Partial_Sums D) . n is complex real ext-real Element of REAL
abs ((Partial_Sums D) . n) is complex real ext-real Element of REAL
D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
lim D is complex Element of COMPLEX
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
D - seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- seq is Relation-like NAT -defined Function-like total complex-valued set
- 1 is non zero complex real ext-real non positive negative set
(- 1) (#) seq is Relation-like NAT -defined Function-like total complex-valued set
D + (- seq) is Relation-like NAT -defined Function-like total complex-valued set
lim (D - seq) is complex Element of COMPLEX
lim seq is complex Element of COMPLEX
(lim D) - (lim seq) is complex Element of COMPLEX
D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
|.D.| is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
D . seq is complex Element of COMPLEX
|.(D . seq).| is complex real ext-real Element of REAL
|.D.| . seq is complex real ext-real Element of REAL
D is complex set
seq is complex Element of COMPLEX
m is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
m . 0 is complex Element of COMPLEX
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
m . (n + 1) is complex Element of COMPLEX
m . n is complex Element of COMPLEX
(m . n) * D is complex set
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq . 0 is complex Element of COMPLEX
m is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
m . 0 is complex Element of COMPLEX
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
seq . n is complex Element of COMPLEX
m . n is complex Element of COMPLEX
n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
seq . (n + 1) is complex Element of COMPLEX
m . (n + 1) is complex Element of COMPLEX
(m . n) * D is complex set
D is complex set
seq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
D |^ seq is complex set
(D) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(D) . seq is complex Element of COMPLEX
n is complex Element of COMPLEX
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
D |^ n is complex set
(D) . n is complex Element of COMPLEX
n + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
D |^ (n + 1) is complex set
(D) . (n + 1) is complex Element of COMPLEX
((D) . n) * D is complex set
D |^ 0 is complex set
(D) . 0 is complex Element of COMPLEX
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
D |^ m is complex set
(D) . m is complex Element of COMPLEX
D is complex Element of COMPLEX
(D,0) is complex Element of COMPLEX
(D) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(D) . 0 is complex Element of COMPLEX
D is Relation-like Function-like complex-valued set
dom D is set
m is Relation-like Function-like set
dom m is set
m is Relation-like Function-like set
dom m is set
n is Relation-like Function-like set
dom n is set
n is set
m . n is set
D . n is complex set
Re (D . n) is complex real ext-real Element of REAL
n . n is set
m is Relation-like Function-like set
dom m is set
m is Relation-like Function-like set
dom m is set
n is Relation-like Function-like set
dom n is set
n is set
m . n is set
D . n is complex set
Im (D . n) is complex real ext-real Element of REAL
n . n is set
D is Relation-like Function-like complex-valued set
(D) is Relation-like Function-like set
seq is set
dom (D) is set
(D) . seq is set
D . seq is complex set
Re (D . seq) is complex real ext-real Element of REAL
(D) is Relation-like Function-like set
seq is set
dom (D) is set
(D) . seq is set
D . seq is complex set
Im (D . seq) is complex real ext-real Element of REAL
D is set
K20(D,COMPLEX) is complex-valued set
K19(K20(D,COMPLEX)) is set
seq is Relation-like D -defined COMPLEX -valued Function-like complex-valued Element of K19(K20(D,COMPLEX))
(seq) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K20(D,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(D,REAL)) is set
dom seq is set
rng (seq) is V62() V63() V64() set
dom (seq) is set
(seq) is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom seq is set
rng (seq) is V62() V63() V64() set
dom (seq) is set
D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(D) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(NAT,D) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
dom (NAT,D) is V62() V63() V64() V65() V66() V67() set
dom D is V62() V63() V64() V65() V66() V67() set
seq is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(NAT,D) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
dom (NAT,D) is V62() V63() V64() V65() V66() V67() set
dom D is V62() V63() V64() V65() V66() V67() set
dom seq is V62() V63() V64() V65() V66() V67() set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
seq . m is complex real ext-real Element of REAL
D . m is complex Element of COMPLEX
Re (D . m) is complex real ext-real Element of REAL
m is set
seq . m is complex real ext-real Element of REAL
D . m is complex set
Re (D . m) is complex real ext-real Element of REAL
(NAT,D) . m is complex real ext-real Element of REAL
(D) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(NAT,D) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
dom (NAT,D) is V62() V63() V64() V65() V66() V67() set
dom D is V62() V63() V64() V65() V66() V67() set
seq is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(NAT,D) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
dom (NAT,D) is V62() V63() V64() V65() V66() V67() set
dom D is V62() V63() V64() V65() V66() V67() set
dom seq is V62() V63() V64() V65() V66() V67() set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
seq . m is complex real ext-real Element of REAL
D . m is complex Element of COMPLEX
Im (D . m) is complex real ext-real Element of REAL
m is set
seq . m is complex real ext-real Element of REAL
D . m is complex set
Im (D . m) is complex real ext-real Element of REAL
(NAT,D) . m is complex real ext-real Element of REAL
D is complex Element of COMPLEX
|.D.| is complex real ext-real Element of REAL
Re D is complex real ext-real Element of REAL
abs (Re D) is complex real ext-real Element of REAL
Im D is complex real ext-real Element of REAL
abs (Im D) is complex real ext-real Element of REAL
(abs (Re D)) + (abs (Im D)) is complex real ext-real Element of REAL
(Im D) * <i> is complex set
(Re D) + ((Im D) * <i>) is complex set
(Re D) + (0 * <i>) is complex set
|.((Re D) + (0 * <i>)).| is complex real ext-real Element of REAL
0 + ((Im D) * <i>) is complex set
|.(0 + ((Im D) * <i>)).| is complex real ext-real Element of REAL
|.((Re D) + (0 * <i>)).| + |.(0 + ((Im D) * <i>)).| is complex real ext-real Element of REAL
Re (0 + ((Im D) * <i>)) is complex real ext-real Element of REAL
Im (0 + ((Im D) * <i>)) is complex real ext-real Element of REAL
D is complex Element of COMPLEX
Re D is complex real ext-real Element of REAL
abs (Re D) is complex real ext-real Element of REAL
|.D.| is complex real ext-real Element of REAL
Im D is complex real ext-real Element of REAL
abs (Im D) is complex real ext-real Element of REAL
(Re D) ^2 is complex real ext-real Element of REAL
(Re D) * (Re D) is complex real ext-real set
(Im D) ^2 is complex real ext-real Element of REAL
(Im D) * (Im D) is complex real ext-real set
0 + ((Im D) ^2) is complex real ext-real Element of REAL
((Re D) ^2) + ((Im D) ^2) is complex real ext-real Element of REAL
sqrt ((Im D) ^2) is complex real ext-real Element of REAL
sqrt (((Re D) ^2) + ((Im D) ^2)) is complex real ext-real Element of REAL
0 + ((Re D) ^2) is complex real ext-real Element of REAL
((Im D) ^2) + ((Re D) ^2) is complex real ext-real Element of REAL
sqrt ((Re D) ^2) is complex real ext-real Element of REAL
D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
D . m is complex Element of COMPLEX
Im (D . m) is complex real ext-real Element of REAL
(seq) . m is complex real ext-real Element of REAL
seq . m is complex Element of COMPLEX
Im (seq . m) is complex real ext-real Element of REAL
Re (D . m) is complex real ext-real Element of REAL
(seq) . m is complex real ext-real Element of REAL
Re (seq . m) is complex real ext-real Element of REAL
D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(D) + (seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
D + seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((D + seq)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(D) + (seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((D + seq)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
((D) + (seq)) . m is complex real ext-real Element of REAL
(D) . m is complex real ext-real Element of REAL
(seq) . m is complex real ext-real Element of REAL
((D) . m) + ((seq) . m) is complex real ext-real Element of REAL
D . m is complex Element of COMPLEX
Re (D . m) is complex real ext-real Element of REAL
(Re (D . m)) + ((seq) . m) is complex real ext-real Element of REAL
seq . m is complex Element of COMPLEX
Re (seq . m) is complex real ext-real Element of REAL
(Re (D . m)) + (Re (seq . m)) is complex real ext-real Element of REAL
(D . m) + (seq . m) is complex Element of COMPLEX
Re ((D . m) + (seq . m)) is complex real ext-real Element of REAL
(D + seq) . m is complex Element of COMPLEX
Re ((D + seq) . m) is complex real ext-real Element of REAL
((D + seq)) . m is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
((D) + (seq)) . m is complex real ext-real Element of REAL
(D) . m is complex real ext-real Element of REAL
(seq) . m is complex real ext-real Element of REAL
((D) . m) + ((seq) . m) is complex real ext-real Element of REAL
D . m is complex Element of COMPLEX
Im (D . m) is complex real ext-real Element of REAL
(Im (D . m)) + ((seq) . m) is complex real ext-real Element of REAL
seq . m is complex Element of COMPLEX
Im (seq . m) is complex real ext-real Element of REAL
(Im (D . m)) + (Im (seq . m)) is complex real ext-real Element of REAL
(D . m) + (seq . m) is complex Element of COMPLEX
Im ((D . m) + (seq . m)) is complex real ext-real Element of REAL
(D + seq) . m is complex Element of COMPLEX
Im ((D + seq) . m) is complex real ext-real Element of REAL
((D + seq)) . m is complex real ext-real Element of REAL
D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- 1 is non zero complex real ext-real non positive negative set
(- 1) (#) (D) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1) (#) D is Relation-like NAT -defined Function-like total complex-valued set
((- D)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) (#) (D) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((- D)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(- (D)) . seq is complex real ext-real Element of REAL
(D) . seq is complex real ext-real Element of REAL
- ((D) . seq) is complex real ext-real Element of REAL
D . seq is complex Element of COMPLEX
Re (D . seq) is complex real ext-real Element of REAL
- (Re (D . seq)) is complex real ext-real Element of REAL
- (D . seq) is complex Element of COMPLEX
Re (- (D . seq)) is complex real ext-real Element of REAL
(- D) . seq is complex Element of COMPLEX
Re ((- D) . seq) is complex real ext-real Element of REAL
((- D)) . seq is complex real ext-real Element of REAL
seq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(- (D)) . seq is complex real ext-real Element of REAL
(D) . seq is complex real ext-real Element of REAL
- ((D) . seq) is complex real ext-real Element of REAL
D . seq is complex Element of COMPLEX
Im (D . seq) is complex real ext-real Element of REAL
- (Im (D . seq)) is complex real ext-real Element of REAL
- (D . seq) is complex Element of COMPLEX
Im (- (D . seq)) is complex real ext-real Element of REAL
(- D) . seq is complex Element of COMPLEX
Im ((- D) . seq) is complex real ext-real Element of REAL
((- D)) . seq is complex real ext-real Element of REAL
D is complex real ext-real Element of REAL
seq is complex Element of COMPLEX
Re seq is complex real ext-real Element of REAL
D * (Re seq) is complex real ext-real Element of REAL
D * seq is complex set
Re (D * seq) is complex real ext-real Element of REAL
Im seq is complex real ext-real Element of REAL
D * (Im seq) is complex real ext-real Element of REAL
Im (D * seq) is complex real ext-real Element of REAL
D + (0 * <i>) is complex set
Re D is complex real ext-real Element of REAL
Im D is complex real ext-real Element of REAL
m is complex Element of COMPLEX
Re m is complex real ext-real Element of REAL
(Re m) * (Re seq) is complex real ext-real Element of REAL
Im m is complex real ext-real Element of REAL
(Im m) * (Im seq) is complex real ext-real Element of REAL
((Re m) * (Re seq)) - ((Im m) * (Im seq)) is complex real ext-real Element of REAL
(Re m) * (Im seq) is complex real ext-real Element of REAL
(Re seq) * (Im m) is complex real ext-real Element of REAL
((Re m) * (Im seq)) + ((Re seq) * (Im m)) is complex real ext-real Element of REAL
(((Re m) * (Im seq)) + ((Re seq) * (Im m))) * <i> is complex set
(((Re m) * (Re seq)) - ((Im m) * (Im seq))) + ((((Re m) * (Im seq)) + ((Re seq) * (Im m))) * <i>) is complex set
(D * (Im seq)) * <i> is complex set
(D * (Re seq)) + ((D * (Im seq)) * <i>) is complex set
D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(D) - (seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- 1 is non zero complex real ext-real non positive negative set
(- 1) (#) (seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(D) + (- (seq)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
D - seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- seq is Relation-like NAT -defined Function-like total complex-valued set
(- 1) (#) seq is Relation-like NAT -defined Function-like total complex-valued set
D + (- seq) is Relation-like NAT -defined Function-like total complex-valued set
((D - seq)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(D) - (seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (seq) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(D) + (- (seq)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((D - seq)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
((D) - (seq)) . m is complex real ext-real Element of REAL
(D) . m is complex real ext-real Element of REAL
- (seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- (seq)) . m is complex real ext-real Element of REAL
((D) . m) + ((- (seq)) . m) is complex real ext-real Element of REAL
- seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((- seq)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((- seq)) . m is complex real ext-real Element of REAL
((D) . m) + (((- seq)) . m) is complex real ext-real Element of REAL
(D) + ((- seq)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((D) + ((- seq))) . m is complex real ext-real Element of REAL
((D - seq)) . m is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
((D) - (seq)) . m is complex real ext-real Element of REAL
(D) . m is complex real ext-real Element of REAL
- (seq) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- (seq)) . m is complex real ext-real Element of REAL
((D) . m) + ((- (seq)) . m) is complex real ext-real Element of REAL
((- seq)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((- seq)) . m is complex real ext-real Element of REAL
((D) . m) + (((- seq)) . m) is complex real ext-real Element of REAL
(D) + ((- seq)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((D) + ((- seq))) . m is complex real ext-real Element of REAL
((D - seq)) . m is complex real ext-real Element of REAL
D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is complex real ext-real Element of REAL
seq (#) (D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq (#) D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((seq (#) D)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq (#) (D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((seq (#) D)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(seq (#) (D)) . m is complex real ext-real Element of REAL
(D) . m is complex real ext-real Element of REAL
seq * ((D) . m) is complex real ext-real Element of REAL
D . m is complex Element of COMPLEX
Re (D . m) is complex real ext-real Element of REAL
seq * (Re (D . m)) is complex real ext-real Element of REAL
seq * (D . m) is complex set
Re (seq * (D . m)) is complex real ext-real Element of REAL
(seq (#) D) . m is complex Element of COMPLEX
Re ((seq (#) D) . m) is complex real ext-real Element of REAL
((seq (#) D)) . m is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
(seq (#) (D)) . m is complex real ext-real Element of REAL
(D) . m is complex real ext-real Element of REAL
seq * ((D) . m) is complex real ext-real Element of REAL
D . m is complex Element of COMPLEX
Im (D . m) is complex real ext-real Element of REAL
seq * (Im (D . m)) is complex real ext-real Element of REAL
seq * (D . m) is complex set
Im (seq * (D . m)) is complex real ext-real Element of REAL
(seq (#) D) . m is complex Element of COMPLEX
Im ((seq (#) D) . m) is complex real ext-real Element of REAL
((seq (#) D)) . m is complex real ext-real Element of REAL
D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
seq is complex Element of COMPLEX
seq (#) D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((seq (#) D)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Re seq is complex real ext-real Element of REAL
(Re seq) (#) (D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Im seq is complex real ext-real Element of REAL
(Im seq) (#) (D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((Re seq) (#) (D)) - ((Im seq) (#) (D)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- ((Im seq) (#) (D)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- 1 is non zero complex real ext-real non positive negative set
(- 1) (#) ((Im seq) (#) (D)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((Re seq) (#) (D)) + (- ((Im seq) (#) (D))) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((seq (#) D)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(Re seq) (#) (D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(Im seq) (#) (D) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((Re seq) (#) (D)) + ((Im seq) (#) (D)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
((seq (#) D)) . m is complex real ext-real Element of REAL
(seq (#) D) . m is complex Element of COMPLEX
Re ((seq (#) D) . m) is complex real ext-real Element of REAL
D . m is complex Element of COMPLEX
seq * (D . m) is complex Element of COMPLEX
Re (seq * (D . m)) is complex real ext-real Element of REAL
Re (D . m) is complex real ext-real Element of REAL
(Re seq) * (Re (D . m)) is complex real ext-real Element of REAL
Im (D . m) is complex real ext-real Element of REAL
(Im seq) * (Im (D . m)) is complex real ext-real Element of REAL
((Re seq) * (Re (D . m))) - ((Im seq) * (Im (D . m))) is complex real ext-real Element of REAL
(Re seq) * (Im (D . m)) is complex real ext-real Element of REAL
(Re (D . m)) * (Im seq) is complex real ext-real Element of REAL
((Re seq) * (Im (D . m))) + ((Re (D . m)) * (Im seq)) is complex real ext-real Element of REAL
(((Re seq) * (Im (D . m))) + ((Re (D . m)) * (Im seq))) * <i> is complex set
(((Re seq) * (Re (D . m))) - ((Im seq) * (Im (D . m)))) + ((((Re seq) * (Im (D . m))) + ((Re (D . m)) * (Im seq))) * <i>) is complex set
Re ((((Re seq) * (Re (D . m))) - ((Im seq) * (Im (D . m)))) + ((((Re seq) * (Im (D . m))) + ((Re (D . m)) * (Im seq))) * <i>)) is complex real ext-real Element of REAL
(D) . m is complex real ext-real Element of REAL
(Re seq) * ((D) . m) is complex real ext-real Element of REAL
((Re seq) * ((D) . m)) - ((Im seq) * (Im (D . m))) is complex real ext-real Element of REAL
(D) . m is complex real ext-real Element of REAL
(Im seq) * ((D) . m) is complex real ext-real Element of REAL
((Re seq) * ((D) . m)) - ((Im seq) * ((D) . m)) is complex real ext-real Element of REAL
((Re seq) (#) (D)) . m is complex real ext-real Element of REAL
(((Re seq) (#) (D)) . m) - ((Im seq) * ((D) . m)) is complex real ext-real Element of REAL
((Im seq) (#) (D)) . m is complex real ext-real Element of REAL
(((Re seq) (#) (D)) . m) - (((Im seq) (#) (D)) . m) is complex real ext-real Element of REAL
- (((Im seq) (#) (D)) . m) is complex real ext-real Element of REAL
(((Re seq) (#) (D)) . m) + (- (((Im seq) (#) (D)) . m)) is complex real ext-real Element of REAL
- ((Im seq) (#) (D)) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- ((Im seq) (#) (D))) . m is complex real ext-real Element of REAL
(((Re seq) (#) (D)) . m) + ((- ((Im seq) (#) (D))) . m) is complex real ext-real Element of REAL
(((Re seq) (#) (D)) - ((Im seq) (#) (D))) . m is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
((seq (#) D)) . m is complex real ext-real Element of REAL
(seq (#) D) . m is complex Element of COMPLEX
Im ((seq (#) D) . m) is complex real ext-real Element of REAL
D . m is complex Element of COMPLEX
seq * (D . m) is complex Element of COMPLEX
Im (seq * (D . m)) is complex real ext-real Element of REAL
Re (D . m) is complex real ext-real Element of REAL
(Re seq) * (Re (D . m)) is complex real ext-real Element of REAL
Im (D . m) is complex real ext-real Element of REAL
(Im seq) * (Im (D . m)) is complex real ext-real Element of REAL
((Re seq) * (Re (D . m))) - ((Im seq) * (Im (D . m))) is complex real ext-real Element of REAL
(Re seq) * (Im (D . m)) is complex real ext-real Element of REAL
(Re (D . m)) * (Im seq) is complex real ext-real Element of REAL
((Re seq) * (Im (D . m))) + ((Re (D . m)) * (Im seq)) is complex real ext-real Element of REAL
(((Re seq) * (Im (D . m))) + ((Re (D . m)) * (Im seq))) * <i> is complex set
(((Re seq) * (Re (D . m))) - ((Im seq) * (Im (D . m)))) + ((((Re seq) * (Im (D . m))) + ((Re (D . m)) * (Im seq))) * <i>) is complex set
Im ((((Re seq) * (Re (D . m))) - ((Im seq) * (Im (D . m)))) + ((((Re seq) * (Im (D . m))) + ((Re (D . m)) * (Im seq))) * <i>)) is complex real ext-real Element of REAL
(D) . m is complex real ext-real Element of REAL
(Im seq) * ((D) . m) is complex real ext-real Element of REAL
((Re seq) * (Im (D . m))) + ((Im seq) * ((D) . m)) is complex