:: 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 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) * ((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
(((Re seq) (#) (D)) + ((Im 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 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))
((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 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)) - ((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 Function-like total complex-valued ext-real-valued real-valued set
- 1 is non zero complex real ext-real non positive negative set
(- 1) (#) ((D) (#) (seq)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((D) (#) (seq)) + (- ((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))
(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))
((D) (#) (seq)) + ((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 (#) seq) . m is complex Element of COMPLEX
Re ((D (#) seq) . m) is complex real ext-real Element of REAL
D . m is complex Element of COMPLEX
seq . m is complex Element of COMPLEX
(D . m) * (seq . m) is complex Element of COMPLEX
Re ((D . m) * (seq . m)) is complex real ext-real Element of REAL
Re (D . m) is complex real ext-real Element of REAL
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
Im (D . m) is complex real ext-real Element of REAL
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
((Re (D . m)) * (Re (seq . m))) - ((Im (D . m)) * (Im (seq . m))) is complex real ext-real Element of REAL
(Re (D . m)) * (Im (seq . m)) is complex real ext-real Element of REAL
(Re (seq . m)) * (Im (D . m)) is complex real ext-real Element of REAL
((Re (D . m)) * (Im (seq . m))) + ((Re (seq . m)) * (Im (D . m))) is complex real ext-real Element of REAL
(((Re (D . m)) * (Im (seq . m))) + ((Re (seq . m)) * (Im (D . m)))) * <i> is complex set
(((Re (D . m)) * (Re (seq . m))) - ((Im (D . m)) * (Im (seq . m)))) + ((((Re (D . m)) * (Im (seq . m))) + ((Re (seq . m)) * (Im (D . m)))) * <i>) is complex set
Re ((((Re (D . m)) * (Re (seq . m))) - ((Im (D . m)) * (Im (seq . m)))) + ((((Re (D . m)) * (Im (seq . m))) + ((Re (seq . m)) * (Im (D . m)))) * <i>)) is complex real ext-real Element of REAL
(D) . m is complex real ext-real Element of REAL
((D) . m) * (Re (seq . m)) is complex real ext-real Element of REAL
(((D) . m) * (Re (seq . m))) - ((Im (D . m)) * (Im (seq . 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) * ((seq) . m)) - ((Im (D . m)) * (Im (seq . m))) is complex real ext-real Element of REAL
(seq) . m is complex real ext-real Element of REAL
(Im (D . m)) * ((seq) . m) is complex real ext-real Element of REAL
(((D) . m) * ((seq) . m)) - ((Im (D . m)) * ((seq) . m)) is complex real ext-real Element of REAL
(D) . m is complex real ext-real Element of REAL
((D) . m) * ((seq) . m) is complex real ext-real Element of REAL
(((D) . m) * ((seq) . m)) - (((D) . m) * ((seq) . m)) is complex real ext-real Element of REAL
((D) (#) (seq)) . m is complex real ext-real Element of REAL
(((D) (#) (seq)) . m) - (((D) . m) * ((seq) . m)) is complex real ext-real Element of REAL
((D) (#) (seq)) . m is complex real ext-real Element of REAL
(((D) (#) (seq)) . m) - (((D) (#) (seq)) . m) is complex real ext-real Element of REAL
- (((D) (#) (seq)) . m) is complex real ext-real Element of REAL
(((D) (#) (seq)) . m) + (- (((D) (#) (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) + ((- ((D) (#) (seq))) . m) is complex real ext-real Element of REAL
(((D) (#) (seq)) - ((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 (#) seq) . m is complex Element of COMPLEX
Im ((D (#) seq) . m) is complex real ext-real Element of REAL
D . m is complex Element of COMPLEX
seq . m is complex Element of COMPLEX
(D . m) * (seq . m) is complex Element of COMPLEX
Im ((D . m) * (seq . m)) is complex real ext-real Element of REAL
Re (D . m) is complex real ext-real Element of REAL
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
Im (D . m) is complex real ext-real Element of REAL
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
((Re (D . m)) * (Re (seq . m))) - ((Im (D . m)) * (Im (seq . m))) is complex real ext-real Element of REAL
(Re (D . m)) * (Im (seq . m)) is complex real ext-real Element of REAL
(Re (seq . m)) * (Im (D . m)) is complex real ext-real Element of REAL
((Re (D . m)) * (Im (seq . m))) + ((Re (seq . m)) * (Im (D . m))) is complex real ext-real Element of REAL
(((Re (D . m)) * (Im (seq . m))) + ((Re (seq . m)) * (Im (D . m)))) * <i> is complex set
(((Re (D . m)) * (Re (seq . m))) - ((Im (D . m)) * (Im (seq . m)))) + ((((Re (D . m)) * (Im (seq . m))) + ((Re (seq . m)) * (Im (D . m)))) * <i>) is complex set
Im ((((Re (D . m)) * (Re (seq . m))) - ((Im (D . m)) * (Im (seq . m)))) + ((((Re (D . m)) * (Im (seq . m))) + ((Re (seq . m)) * (Im (D . m)))) * <i>)) is complex real ext-real Element of REAL
(seq) . m is complex real ext-real Element of REAL
(Im (D . m)) * ((seq) . m) is complex real ext-real Element of REAL
((Re (D . m)) * (Im (seq . m))) + ((Im (D . m)) * ((seq) . m)) is complex real ext-real Element of REAL
(D) . m is complex real ext-real Element of REAL
((D) . m) * (Im (seq . m)) is complex real ext-real Element of REAL
(((D) . m) * (Im (seq . m))) + ((Im (D . m)) * ((seq) . 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) * ((seq) . m)) + ((Im (D . m)) * ((seq) . m)) is complex real ext-real Element of REAL
(D) . m is complex real ext-real Element of REAL
((D) . m) * ((seq) . m) is complex real ext-real Element of REAL
(((D) . m) * ((seq) . m)) + (((D) . m) * ((seq) . m)) is complex real ext-real Element of REAL
((D) (#) (seq)) . m is complex real ext-real Element of REAL
(((D) (#) (seq)) . m) + (((D) . m) * ((seq) . m)) is complex real ext-real Element of REAL
((D) (#) (seq)) . m is complex real ext-real Element of REAL
(((D) (#) (seq)) . m) + (((D) (#) (seq)) . m) is complex real ext-real Element of REAL
(((D) (#) (seq)) + ((D) (#) (seq))) . m is complex real ext-real Element of REAL
D is Relation-like NAT -defined NAT -valued Function-like non zero total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
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 total complex-valued set
seq * D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued subsequence of seq
dom (seq * D) is V62() V63() V64() V65() V66() V67() 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 NAT -valued Function-like non zero total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
(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))
(D) * seq is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (D)
((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))
(D) * seq is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (D)
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
seq . 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 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
((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
((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 . 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 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) * 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 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 Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (D)
D ^\ seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued subsequence of D
((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 subsequence of (D)
((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
m + 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) . (m + seq) is complex real ext-real Element of REAL
D . (m + seq) is complex Element of COMPLEX
Re (D . (m + seq)) 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
((D) ^\ seq) . m is complex real ext-real Element of REAL
(D) . (m + seq) is complex real ext-real Element of REAL
Im (D . (m + seq)) is complex real ext-real Element of REAL
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))
Partial_Sums D is Relation-like NAT -defined Function-like total complex-valued set
dom (Partial_Sums D) is V62() V63() V64() V65() V66() V67() set
rng (Partial_Sums D) is V62() 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 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
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 COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
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 Element of COMPLEX
seq + 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 . (seq + 1) is complex Element of COMPLEX
(D) . (seq + 1) is complex Element of COMPLEX
0c + (D . (seq + 1)) is complex Element of COMPLEX
((D) . seq) + (D . (seq + 1)) is complex Element of COMPLEX
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 . 0 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.| 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
|.D.| . seq is complex real ext-real Element of REAL
(Partial_Sums |.D.|) . seq is complex real ext-real Element of REAL
seq + 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.| . (seq + 1) is complex real ext-real Element of REAL
(Partial_Sums |.D.|) . (seq + 1) is complex real ext-real Element of REAL
|.0c.| is complex real ext-real Element of REAL
|.0c.| + (|.D.| . (seq + 1)) is complex real ext-real Element of REAL
D . seq is complex Element of COMPLEX
|.(D . seq).| is complex real ext-real Element of REAL
|.(D . seq).| + (|.D.| . (seq + 1)) is complex real ext-real Element of REAL
((Partial_Sums |.D.|) . seq) + (|.D.| . (seq + 1)) 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
(Partial_Sums |.D.|) . 0 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
|.(D . seq).| 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))
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))
(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))
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))
((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
(Partial_Sums (D)) . seq is complex real ext-real Element of REAL
((D)) . seq is complex real ext-real Element of REAL
seq + 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)) . (seq + 1) is complex real ext-real Element of REAL
((D)) . (seq + 1) is complex real ext-real Element of REAL
(D) . (seq + 1) is complex real ext-real Element of REAL
(((D)) . seq) + ((D) . (seq + 1)) is complex real ext-real Element of REAL
D . (seq + 1) is complex Element of COMPLEX
Re (D . (seq + 1)) is complex real ext-real Element of REAL
(((D)) . seq) + (Re (D . (seq + 1))) 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)) + (Re (D . (seq + 1))) is complex real ext-real Element of REAL
((D) . seq) + (D . (seq + 1)) is complex Element of COMPLEX
Re (((D) . seq) + (D . (seq + 1))) is complex real ext-real Element of REAL
(D) . (seq + 1) is complex Element of COMPLEX
Re ((D) . (seq + 1)) 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)) . seq is complex real ext-real Element of REAL
seq + 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)) . (seq + 1) is complex real ext-real Element of REAL
((D)) . (seq + 1) is complex real ext-real Element of REAL
(D) . (seq + 1) is complex real ext-real Element of REAL
(((D)) . seq) + ((D) . (seq + 1)) is complex real ext-real Element of REAL
D . (seq + 1) is complex Element of COMPLEX
Im (D . (seq + 1)) is complex real ext-real Element of REAL
(((D)) . seq) + (Im (D . (seq + 1))) 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)) + (Im (D . (seq + 1))) is complex real ext-real Element of REAL
((D) . seq) + (D . (seq + 1)) is complex Element of COMPLEX
Im (((D) . seq) + (D . (seq + 1))) is complex real ext-real Element of REAL
(D) . (seq + 1) is complex Element of COMPLEX
Im ((D) . (seq + 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
D . 0 is complex Element of COMPLEX
Im (D . 0) is complex real ext-real Element of REAL
(D) . 0 is complex Element of COMPLEX
Im ((D) . 0) is complex real ext-real Element of REAL
((D)) . 0 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
Re (D . 0) is complex real ext-real Element of REAL
Re ((D) . 0) is complex real ext-real Element of REAL
((D)) . 0 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 COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,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))
(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))
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 COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,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 COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,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))
(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
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 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))
((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))
((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) 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))
(Partial_Sums (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))
(Partial_Sums (D)) + (- ((seq))) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued 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))
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))
(Partial_Sums (D)) - (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))
- (Partial_Sums (seq)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (Partial_Sums (seq)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(Partial_Sums (D)) + (- (Partial_Sums (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))
- (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
Partial_Sums ((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))
Partial_Sums ((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))
(((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)) 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) 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))
(Partial_Sums (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))
(Partial_Sums (D)) + (- ((seq))) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued 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))
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))
(Partial_Sums (D)) - (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))
- (Partial_Sums (seq)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (Partial_Sums (seq)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(Partial_Sums (D)) + (- (Partial_Sums (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))
- (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
Partial_Sums ((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))
Partial_Sums ((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))
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 COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq is complex set
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 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 COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,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
((seq (#) D)) . m is complex Element of COMPLEX
(seq (#) (D)) . m is complex Element of COMPLEX
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 (#) D)) . (m + 1) is complex Element of COMPLEX
(seq (#) D) . (m + 1) is complex Element of COMPLEX
(((seq (#) D)) . m) + ((seq (#) D) . (m + 1)) is complex Element of COMPLEX
(D) . m is complex Element of COMPLEX
seq * ((D) . m) is complex set
(seq * ((D) . m)) + ((seq (#) D) . (m + 1)) is complex set
D . (m + 1) is complex Element of COMPLEX
seq * (D . (m + 1)) is complex set
(seq * ((D) . m)) + (seq * (D . (m + 1))) is complex set
((D) . m) + (D . (m + 1)) is complex Element of COMPLEX
seq * (((D) . m) + (D . (m + 1))) is complex set
(D) . (m + 1) is complex Element of COMPLEX
seq * ((D) . (m + 1)) is complex set
(seq (#) (D)) . (m + 1) is complex Element of COMPLEX
((seq (#) D)) . 0 is complex Element of COMPLEX
(seq (#) D) . 0 is complex Element of COMPLEX
D . 0 is complex Element of COMPLEX
seq * (D . 0) is complex set
(D) . 0 is complex Element of COMPLEX
seq * ((D) . 0) is complex set
(seq (#) (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) 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))
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
(D) . seq is complex Element of COMPLEX
|.((D) . seq).| is complex real ext-real Element of REAL
(Partial_Sums |.D.|) . 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
(D) . m is complex Element of COMPLEX
|.((D) . m).| is complex real ext-real Element of REAL
(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
D . (m + 1) is complex Element of COMPLEX
|.(D . (m + 1)).| is complex real ext-real Element of REAL
|.((D) . m).| + |.(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
(D) . (m + 1) is complex Element of COMPLEX
|.((D) . (m + 1)).| is complex real ext-real Element of REAL
((D) . m) + (D . (m + 1)) is complex Element of COMPLEX
|.(((D) . m) + (D . (m + 1))).| is complex real ext-real Element of REAL
|.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
(Partial_Sums |.D.|) . (m + 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
D . 0 is complex Element of COMPLEX
|.(D . 0).| is complex real ext-real Element of REAL
(D) . 0 is complex Element of COMPLEX
|.((D) . 0).| 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 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))
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
(D) . seq is complex Element of COMPLEX
(Partial_Sums |.D.|) . 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
(D) . m is complex Element of COMPLEX
((D) . seq) - ((D) . m) is complex Element of COMPLEX
|.(((D) . seq) - ((D) . m)).| 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.|) . m) is complex real ext-real Element of REAL
abs (((Partial_Sums |.D.|) . seq) - ((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
(Partial_Sums |.D.|) . 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
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
n + (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.|) . (n + (n + 1)) is complex real ext-real Element of REAL
((Partial_Sums |.D.|) . (n + (n + 1))) - ((Partial_Sums |.D.|) . n) is complex real ext-real Element of REAL
n + 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 + n) is complex real ext-real Element of REAL
(n + 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 + n) + 1) is complex real ext-real Element of REAL
((Partial_Sums |.D.|) . (n + n)) + (|.D.| . ((n + n) + 1)) is complex real ext-real Element of REAL
(((Partial_Sums |.D.|) . (n + n)) + (|.D.| . ((n + n) + 1))) - ((Partial_Sums |.D.|) . n) is complex real ext-real Element of REAL
D . ((n + n) + 1) is complex Element of COMPLEX
|.(D . ((n + n) + 1)).| is complex real ext-real Element of REAL
((Partial_Sums |.D.|) . (n + n)) + |.(D . ((n + n) + 1)).| is complex real ext-real Element of REAL
(((Partial_Sums |.D.|) . (n + n)) + |.(D . ((n + n) + 1)).|) - ((Partial_Sums |.D.|) . n) is complex real ext-real Element of REAL
((Partial_Sums |.D.|) . (n + n)) - ((Partial_Sums |.D.|) . n) is complex real ext-real Element of REAL
(((Partial_Sums |.D.|) . (n + n)) - ((Partial_Sums |.D.|) . n)) + |.(D . ((n + n) + 1)).| 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
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
n + 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 + n) is complex real ext-real Element of REAL
(Partial_Sums |.D.|) . n is complex real ext-real Element of REAL
((Partial_Sums |.D.|) . (n + n)) - ((Partial_Sums |.D.|) . n) is complex real ext-real Element of REAL
abs (((Partial_Sums |.D.|) . (n + n)) - ((Partial_Sums |.D.|) . 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
(D) . n is complex Element of COMPLEX
(Partial_Sums |.D.|) . 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
(D) . n is complex Element of COMPLEX
((D) . n) - ((D) . n) is complex Element of COMPLEX
|.(((D) . n) - ((D) . n)).| is complex real ext-real Element of REAL
(Partial_Sums |.D.|) . n is complex real ext-real Element of REAL
((Partial_Sums |.D.|) . n) - ((Partial_Sums |.D.|) . n) is complex real ext-real Element of REAL
abs (((Partial_Sums |.D.|) . n) - ((Partial_Sums |.D.|) . n)) is complex real ext-real Element of REAL
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
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
n2 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 + n2 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 + n2) is complex Element of COMPLEX
((D) . (n + n2)) - ((D) . n) is complex Element of COMPLEX
|.(((D) . (n + n2)) - ((D) . n)).| is complex real ext-real Element of REAL
(Partial_Sums |.D.|) . (n + n2) is complex real ext-real Element of REAL
((Partial_Sums |.D.|) . (n + n2)) - ((Partial_Sums |.D.|) . n) is complex real ext-real Element of REAL
abs (((Partial_Sums |.D.|) . (n + n2)) - ((Partial_Sums |.D.|) . n)) is complex real ext-real Element of REAL
(n + n2) + 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 + n2) + 1) is complex Element of COMPLEX
(((D) . (n + n2)) - ((D) . n)) + (D . ((n + n2) + 1)) is complex Element of COMPLEX
|.((((D) . (n + n2)) - ((D) . n)) + (D . ((n + n2) + 1))).| is complex real ext-real Element of REAL
|.(D . ((n + n2) + 1)).| is complex real ext-real Element of REAL
|.(((D) . (n + n2)) - ((D) . n)).| + |.(D . ((n + n2) + 1)).| is complex real ext-real Element of REAL
(abs (((Partial_Sums |.D.|) . (n + n2)) - ((Partial_Sums |.D.|) . n))) + |.(D . ((n + n2) + 1)).| is complex real ext-real Element of REAL
n2 + 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 + (n2 + 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 + (n2 + 1)) is complex Element of COMPLEX
((D) . (n + (n2 + 1))) - ((D) . n) is complex Element of COMPLEX
|.(((D) . (n + (n2 + 1))) - ((D) . n)).| is complex real ext-real Element of REAL
((D) . (n + n2)) + (D . ((n + n2) + 1)) is complex Element of COMPLEX
(((D) . (n + n2)) + (D . ((n + n2) + 1))) - ((D) . n) is complex Element of COMPLEX
|.((((D) . (n + n2)) + (D . ((n + n2) + 1))) - ((D) . n)).| is complex real ext-real Element of REAL
(((Partial_Sums |.D.|) . (n + n2)) - ((Partial_Sums |.D.|) . n)) + |.(D . ((n + n2) + 1)).| is complex real ext-real Element of REAL
((Partial_Sums |.D.|) . (n + n2)) + |.(D . ((n + n2) + 1)).| is complex real ext-real Element of REAL
(((Partial_Sums |.D.|) . (n + n2)) + |.(D . ((n + n2) + 1)).|) - ((Partial_Sums |.D.|) . n) is complex real ext-real Element of REAL
|.D.| . ((n + n2) + 1) is complex real ext-real Element of REAL
((Partial_Sums |.D.|) . (n + n2)) + (|.D.| . ((n + n2) + 1)) is complex real ext-real Element of REAL
(((Partial_Sums |.D.|) . (n + n2)) + (|.D.| . ((n + n2) + 1))) - ((Partial_Sums |.D.|) . n) is complex real ext-real Element of REAL
(Partial_Sums |.D.|) . (n + (n2 + 1)) is complex real ext-real Element of REAL
((Partial_Sums |.D.|) . (n + (n2 + 1))) - ((Partial_Sums |.D.|) . n) is complex real ext-real Element of REAL
abs (((Partial_Sums |.D.|) . (n + (n2 + 1))) - ((Partial_Sums |.D.|) . 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
(D) . (n + 0) is complex Element of COMPLEX
((D) . (n + 0)) - ((D) . n) is complex Element of COMPLEX
|.(((D) . (n + 0)) - ((D) . n)).| is complex real ext-real Element of REAL
(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
abs (((Partial_Sums |.D.|) . (n + 0)) - ((Partial_Sums |.D.|) . 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
(D) . n is complex Element of COMPLEX
(Partial_Sums |.D.|) . 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
(D) . n is complex Element of COMPLEX
((D) . n) - ((D) . n) is complex Element of COMPLEX
|.(((D) . n) - ((D) . n)).| is complex real ext-real Element of REAL
(Partial_Sums |.D.|) . n is complex real ext-real Element of REAL
((Partial_Sums |.D.|) . n) - ((Partial_Sums |.D.|) . n) is complex real ext-real Element of REAL
abs (((Partial_Sums |.D.|) . n) - ((Partial_Sums |.D.|) . n)) is complex real ext-real Element of REAL
((D) . n) - ((D) . n) is complex Element of COMPLEX
|.(((D) . n) - ((D) . n)).| is complex real ext-real Element of REAL
((Partial_Sums |.D.|) . n) - ((Partial_Sums |.D.|) . n) is complex real ext-real Element of REAL
abs (((Partial_Sums |.D.|) . n) - ((Partial_Sums |.D.|) . n)) is complex real ext-real Element of REAL
- (((Partial_Sums |.D.|) . n) - ((Partial_Sums |.D.|) . n)) is complex real ext-real Element of REAL
abs (- (((Partial_Sums |.D.|) . n) - ((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))
(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))
(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))
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
(Partial_Sums (D)) ^\ seq is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of Partial_Sums (D)
(D) ^\ seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued subsequence of (D)
(((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))
(Partial_Sums (D)) ^\ seq is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of Partial_Sums (D)
(((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
((Partial_Sums (D)) ^\ seq) . m is complex real ext-real Element of REAL
m + 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)) . (m + seq) 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)) . (m + seq) is complex real ext-real Element of REAL
(D) . (m + seq) is complex Element of COMPLEX
Re ((D) . (m + seq)) 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
((Partial_Sums (D)) ^\ seq) . m is complex real ext-real Element of REAL
(Partial_Sums (D)) . (m + seq) 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)) . (m + seq) is complex real ext-real Element of REAL
Im ((D) . (m + seq)) is complex real ext-real Element of REAL
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))
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
seq ^\ 1 is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued subsequence of seq
((seq ^\ 1)) 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 COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(seq) ^\ 1 is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued subsequence of (seq)
((seq) ^\ 1) - 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 Function-like total complex-valued set
- 1 is non zero complex real ext-real non positive negative set
(- 1) (#) D is Relation-like NAT -defined Function-like total complex-valued set
((seq) ^\ 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))
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
D . m is complex Element of COMPLEX
Re (D . m) is complex real ext-real Element of REAL
Re (seq . 0) 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) . 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))
(D) . m is complex real ext-real Element of REAL
Im (D . m) is complex real ext-real Element of REAL
Im (seq . 0) 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) . 0 is complex real ext-real Element of REAL
(((seq ^\ 1))) 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 ^\ 1)) 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 ^\ 1)) 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) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (seq)
Partial_Sums ((seq) ^\ 1) 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))
(Partial_Sums (seq)) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of Partial_Sums (seq)
((Partial_Sums (seq)) ^\ 1) - (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 Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (D) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((Partial_Sums (seq)) ^\ 1) + (- (D)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(((seq) ^\ 1)) 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) ^\ 1)) - (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) ^\ 1)) + (- (D)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((((seq) ^\ 1) - 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 ^\ 1))) 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 ^\ 1)) 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 ^\ 1)) 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) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (seq)
Partial_Sums ((seq) ^\ 1) 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))
(Partial_Sums (seq)) ^\ 1 is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of Partial_Sums (seq)
((Partial_Sums (seq)) ^\ 1) - (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 Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (D) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((Partial_Sums (seq)) ^\ 1) + (- (D)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(((seq) ^\ 1)) 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) ^\ 1)) - (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) ^\ 1)) + (- (D)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
((((seq) ^\ 1) - 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 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))
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
|.D.| . seq 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))
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))
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 COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,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))
(seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,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 Element of COMPLEX
(seq) . m 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 Element of COMPLEX
(seq) . 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 Element of COMPLEX
(seq) . (n + 1) is complex Element of COMPLEX
D . (n + 1) is complex Element of COMPLEX
((seq) . n) + (D . (n + 1)) is complex Element of COMPLEX
seq . (n + 1) is complex Element of COMPLEX
((seq) . n) + (seq . (n + 1)) is complex Element of COMPLEX
(D) . 0 is complex Element of COMPLEX
(seq) . 0 is complex Element of COMPLEX
D . 0 is complex Element of COMPLEX
seq . 0 is complex Element of COMPLEX
D 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 COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
1r - D is complex Element of COMPLEX
seq 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))
((seq)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
1r - seq 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
((seq)) . m is complex Element of COMPLEX
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 Element of COMPLEX
(seq) . (m + 1) is complex Element of COMPLEX
1r - (seq,(m + 1)) is complex Element of COMPLEX
(1r - (seq,(m + 1))) / (1r - seq) is complex Element of COMPLEX
((seq)) . (m + 1) is complex Element of COMPLEX
(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 Element of COMPLEX
(seq) . ((m + 1) + 1) is complex Element of COMPLEX
1r - (seq,((m + 1) + 1)) is complex Element of COMPLEX
(1r - (seq,((m + 1) + 1))) / (1r - seq) is complex Element of COMPLEX
(seq,(m + 1)) * 1r is complex Element of COMPLEX
((1r - (seq,(m + 1))) / (1r - seq)) + ((seq,(m + 1)) * 1r) is complex Element of COMPLEX
(1r - seq) / (1r - seq) is complex Element of COMPLEX
(seq,(m + 1)) * ((1r - seq) / (1r - seq)) is complex Element of COMPLEX
((1r - (seq,(m + 1))) / (1r - seq)) + ((seq,(m + 1)) * ((1r - seq) / (1r - seq))) is complex Element of COMPLEX
(seq,(m + 1)) * (1r - seq) is complex Element of COMPLEX
((seq,(m + 1)) * (1r - seq)) / (1r - seq) is complex Element of COMPLEX
((1r - (seq,(m + 1))) / (1r - seq)) + (((seq,(m + 1)) * (1r - seq)) / (1r - seq)) is complex Element of COMPLEX
(seq,(m + 1)) * seq is complex Element of COMPLEX
(seq,(m + 1)) - ((seq,(m + 1)) * seq) is complex Element of COMPLEX
(1r - (seq,(m + 1))) + ((seq,(m + 1)) - ((seq,(m + 1)) * seq)) is complex Element of COMPLEX
((1r - (seq,(m + 1))) + ((seq,(m + 1)) - ((seq,(m + 1)) * seq))) / (1r - seq) is complex Element of COMPLEX
1r - ((seq,(m + 1)) * seq) is complex Element of COMPLEX
(1r - ((seq,(m + 1)) * seq)) / (1r - seq) is complex Element of COMPLEX
((seq)) . 0 is complex Element of COMPLEX
(seq) . 0 is complex Element of COMPLEX
1 * seq is complex set
1r - (1 * seq) is complex set
(1r - (1 * seq)) / (1r - seq) is complex Element of COMPLEX
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 Element of COMPLEX
(seq) . (0 + 1) is complex Element of COMPLEX
1r - (seq,(0 + 1)) is complex Element of COMPLEX
(1r - (seq,(0 + 1))) / (1r - seq) is complex Element of COMPLEX
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
seq + 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,(seq + 1)) is complex Element of COMPLEX
(D) . (seq + 1) is complex Element of COMPLEX
1r - (D,(seq + 1)) is complex Element of COMPLEX
(1r - (D,(seq + 1))) / (1r - D) 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 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
seq is complex Element of COMPLEX
1r - seq 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))
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
(seq) . m is complex Element of COMPLEX
(D . 0) * ((seq) . m) is complex Element of COMPLEX
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 . (m + 1) is complex Element of COMPLEX
seq * ((D . 0) * ((seq) . m)) is complex Element of COMPLEX
seq * ((seq) . m) is complex Element of COMPLEX
(D . 0) * (seq * ((seq) . m)) is complex Element of COMPLEX
(seq) . (m + 1) is complex Element of COMPLEX
(D . 0) * ((seq) . (m + 1)) 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 Element of COMPLEX
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 Element of COMPLEX
(seq) . (m + 1) is complex Element of COMPLEX
1r - (seq,(m + 1)) is complex Element of COMPLEX
(1r - (seq,(m + 1))) / (1r - seq) is complex Element of COMPLEX
(D . 0) * ((1r - (seq,(m + 1))) / (1r - seq)) is complex Element of COMPLEX
(D . 0) * 1r is complex Element of COMPLEX
(seq) . 0 is complex Element of COMPLEX
(D . 0) * ((seq) . 0) is complex Element of COMPLEX
(D . 0) (#) (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 . 0) (#) (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 COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(D . 0) (#) ((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)) . m is complex Element of COMPLEX
(D . 0) * (((seq)) . m) is complex Element of 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 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 Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
n is complex real ext-real set
n is complex real ext-real set
m is complex real ext-real Element of REAL
n2 is complex real ext-real Element of REAL
n2 * <i> is complex set
m + (n2 * <i>) is complex set
n is complex Element of COMPLEX
m is complex real ext-real Element of REAL
m / 2 is complex real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
n2 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V48() V61() V62() V63() V64() V65() V66() V67() Element of NAT
n1 + n2 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 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 . m is complex Element of COMPLEX
(m . m) - n is complex Element of COMPLEX
|.((m . m) - n).| is complex real ext-real Element of REAL
Re (m . m) is complex real ext-real Element of REAL
D . m is complex real ext-real Element of REAL
Re n is complex real ext-real Element of REAL
Re ((m . m) - n) is complex real ext-real Element of REAL
(D . m) - m is complex real ext-real Element of REAL
Im (m . m) is complex real ext-real Element of REAL
seq . m is complex real ext-real Element of REAL
Im n is complex real ext-real Element of REAL
Im ((m . m) - n) is complex real ext-real Element of REAL
(seq . m) - n2 is complex real ext-real Element of REAL
abs ((seq . m) - n2) is complex real ext-real Element of REAL
abs ((D . m) - m) is complex real ext-real Element of REAL
(m / 2) + (m / 2) is complex real ext-real Element of REAL
(abs ((D . m) - m)) + (abs ((seq . m) - n2)) is complex real ext-real Element of REAL
abs (Re ((m . m) - n)) is complex real ext-real Element of REAL
abs (Im ((m . m) - n)) is complex real ext-real Element of REAL
(abs (Re ((m . m) - n))) + (abs (Im ((m . m) - 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
m . m is complex Element of COMPLEX
(m . m) - n is complex Element of COMPLEX
|.((m . m) - n).| is complex real ext-real Element of REAL
m is complex real ext-real Element of REAL
n is complex Element of COMPLEX
n is complex Element of COMPLEX
Re n is complex real ext-real Element of REAL
m is complex real ext-real set
n2 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) - (Re n) is complex real ext-real Element of REAL
abs ((D . n) - (Re n)) is complex real ext-real Element of REAL
m . n is complex Element of COMPLEX
(m . n) - n is complex Element of COMPLEX
|.((m . n) - n).| is complex real ext-real Element of REAL
Re (m . n) is complex real ext-real Element of REAL
D . n is complex real ext-real Element of REAL
Re ((m . n) - n) is complex real ext-real Element of REAL
(Re (m . n)) - (Re n) is complex real ext-real Element of REAL
(D . n) - (Re n) is complex real ext-real Element of REAL
abs ((D . n) - (Re n)) is complex real ext-real Element of REAL
Im n is complex real ext-real Element of REAL
n is complex real ext-real 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
n2 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 . n2 is complex real ext-real Element of REAL
(seq . n2) - (Im n) is complex real ext-real Element of REAL
abs ((seq . n2) - (Im n)) is complex real ext-real Element of REAL
m . n2 is complex Element of COMPLEX
(m . n2) - n is complex Element of COMPLEX
|.((m . n2) - n).| is complex real ext-real Element of REAL
Im ((m . n2) - n) is complex real ext-real Element of REAL
Im (m . n2) is complex real ext-real Element of REAL
(Im (m . n2)) - (Im n) is complex real ext-real Element of REAL
seq . n2 is complex real ext-real Element of REAL
(seq . n2) - (Im n) is complex real ext-real Element of REAL
abs ((seq . n2) - (Im 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 convergent 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 convergent Element of K19(K20(NAT,REAL))
lim D is complex real ext-real Element of REAL
lim seq is complex real ext-real Element of REAL
(lim seq) * <i> is complex set
(lim D) + ((lim seq) * <i>) is complex set
m is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
lim m is complex Element of COMPLEX
n is complex Element of COMPLEX
n is complex real ext-real Element of REAL
n / 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
n2 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 + n2 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 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 . m is complex Element of COMPLEX
(m . m) - n is complex Element of COMPLEX
|.((m . m) - n).| is complex real ext-real Element of REAL
seq . m is complex real ext-real Element of REAL
(seq . m) - (lim seq) is complex real ext-real Element of REAL
abs ((seq . m) - (lim seq)) is complex real ext-real Element of REAL
D . m is complex real ext-real Element of REAL
(D . m) - (lim D) is complex real ext-real Element of REAL
abs ((D . m) - (lim D)) is complex real ext-real Element of REAL
(n / 2) + (n / 2) is complex real ext-real Element of REAL
(abs ((D . m) - (lim D))) + (abs ((seq . m) - (lim seq))) is complex real ext-real Element of REAL
Re (m . m) is complex real ext-real Element of REAL
Re n is complex real ext-real Element of REAL
Re ((m . m) - n) is complex real ext-real Element of REAL
Im (m . m) is complex real ext-real Element of REAL
Im n is complex real ext-real Element of REAL
Im ((m . m) - n) is complex real ext-real Element of REAL
abs (Re ((m . m) - n)) is complex real ext-real Element of REAL
abs (Im ((m . m) - n)) is complex real ext-real Element of REAL
(abs (Re ((m . m) - n))) + (abs (Im ((m . m) - 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))
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))
lim D is complex real ext-real Element of REAL
lim seq is complex real ext-real Element of REAL
m is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued bounded convergent Element of K19(K20(NAT,COMPLEX))
lim m is complex Element of COMPLEX
Re (lim m) is complex real ext-real Element of REAL
Im (lim m) is complex real ext-real Element of REAL
n is complex real ext-real set
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 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
(seq . m) - (Im (lim m)) is complex real ext-real Element of REAL
abs ((seq . m) - (Im (lim m))) is complex real ext-real Element of REAL
m . m is complex Element of COMPLEX
(m . m) - (lim m) is complex Element of COMPLEX
|.((m . m) - (lim m)).| is complex real ext-real Element of REAL
Im (m . m) is complex real ext-real Element of REAL
Im ((m . m) - (lim m)) is complex real ext-real Element of REAL
(Im (m . m)) - (Im (lim m)) is complex real ext-real Element of REAL
n is complex real ext-real set
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 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
(D . m) - (Re (lim m)) is complex real ext-real Element of REAL
abs ((D . m) - (Re (lim m))) is complex real ext-real Element of REAL
m . m is complex Element of COMPLEX
Re (m . m) is complex real ext-real Element of REAL
(m . m) - (lim m) is complex Element of COMPLEX
Re ((m . m) - (lim m)) is complex real ext-real Element of REAL
|.((m . m) - (lim 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 bounded convergent 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))
lim (D) is complex real ext-real Element of REAL
lim D is complex Element of COMPLEX
Re (lim D) is complex real ext-real Element of REAL
lim (D) is complex real ext-real Element of REAL
Im (lim D) 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 Element of COMPLEX
Re (D . 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
(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
D is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued bounded convergent 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 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 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 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))
lim D is complex Element of COMPLEX
Re (lim D) is complex real ext-real Element of REAL
lim (D) is complex real ext-real Element of REAL
Im (lim D) is complex real ext-real Element of REAL
lim (D) 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 Element of COMPLEX
Re (D . 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
(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
(lim (D)) * <i> is complex set
(lim (D)) + ((lim (D)) * <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 . 0 is complex Element of COMPLEX
lim D is complex Element of COMPLEX
seq is complex Element of COMPLEX
|.seq.| is complex real ext-real Element of REAL
m 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))
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 Element of COMPLEX
|.(D . 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
|.seq.| to_power (n + 1) is complex real ext-real Element of REAL
D . (n + 1) is complex Element of COMPLEX
|.(D . (n + 1)).| is complex real ext-real Element of REAL
(n + 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.| to_power ((n + 1) + 1) is complex real ext-real Element of REAL
(D . n) * seq is complex Element of COMPLEX
|.((D . n) * seq).| is complex real ext-real Element of REAL
(|.seq.| to_power (n + 1)) * |.seq.| is complex real ext-real Element of REAL
|.seq.| to_power 1 is complex real ext-real Element of REAL
(|.seq.| to_power (n + 1)) * (|.seq.| to_power 1) 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.| to_power (0 + 1) 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
D . n is complex Element of COMPLEX
|.(D . 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
|.seq.| to_power (n + 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))
abs (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))
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
(abs (D)) . n is complex real ext-real Element of REAL
(D) . n is complex real ext-real Element of REAL
abs ((D) . n) is complex real ext-real Element of REAL
D . n is complex Element of COMPLEX
Re (D . n) is complex real ext-real Element of REAL
abs (Re (D . n)) is complex real ext-real Element of REAL
|.(D . 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
|.seq.| to_power (n + 1) is complex real ext-real Element of REAL
m . 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
D . n is complex Element of COMPLEX
|.(D . 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
|.seq.| to_power (n + 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))
abs (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))
(abs (D)) . n is complex real ext-real Element of REAL
(D) . n is complex real ext-real Element of REAL
abs ((D) . n) is complex real ext-real Element of REAL
Im (D . n) is complex real ext-real Element of REAL
abs (Im (D . n)) is complex real ext-real Element of REAL
m . n is complex real ext-real Element of REAL
C . 0 is complex real ext-real Element of REAL
lim C is complex real ext-real Element of REAL
lim 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
(abs (D)) . n is complex real ext-real Element of REAL
(D) . n is complex real ext-real Element of REAL
abs ((D) . n) is complex real ext-real Element of REAL
C . n is complex real ext-real Element of REAL
lim (abs (D)) 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
(abs (D)) . n is complex real ext-real Element of REAL
(D) . n is complex real ext-real Element of REAL
abs ((D) . n) is complex real ext-real Element of REAL
C . n is complex real ext-real Element of REAL
lim (abs (D)) is complex real ext-real Element of REAL
lim (D) is complex real ext-real Element of REAL
Im (lim D) is complex real ext-real Element of REAL
lim (D) is complex real ext-real Element of REAL
Re (lim D) 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 complex Element of COMPLEX
|.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
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 . (m + 1) is complex Element of COMPLEX
(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 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))
(seq) . ((m + 1) + 1) is complex Element of COMPLEX
(seq,(m + 1)) is complex Element of COMPLEX
(seq) . (m + 1) is complex Element of COMPLEX
(seq,(m + 1)) * seq is complex Element of COMPLEX
D . m is complex Element of COMPLEX
(D . m) * seq 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 Element of COMPLEX
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
(0c,(m + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of COMPLEX
(0c) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(0c) . (m + 1) is complex Element of COMPLEX
(0c) . m is complex Element of COMPLEX
((0c) . m) * 0c is complex Element of COMPLEX
D . 0 is complex Element of COMPLEX
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 Element of COMPLEX
(seq) . (0 + 1) 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))
lim |.D.| is complex real ext-real Element of 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
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
|.D.| . n is complex real ext-real Element of REAL
abs (|.D.| . n) is complex real ext-real Element of REAL
D . n is complex Element of COMPLEX
|.(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))
(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 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
D . m is complex Element of COMPLEX
(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
(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 Element of COMPLEX
(D . n) - (D . m) is complex Element of COMPLEX
|.((D . n) - (D . m)).| is complex real ext-real Element of REAL
Re ((D . n) - (D . m)) is complex real ext-real Element of REAL
Re (D . n) is complex real ext-real Element of REAL
Re (D . m) is complex real ext-real Element of REAL
(Re (D . n)) - (Re (D . m)) is complex real ext-real Element of REAL
((D) . n) - (Re (D . m)) 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))
seq is complex real ext-real 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
D . m is complex Element of COMPLEX
(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
(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 Element of COMPLEX
(D . n) - (D . m) is complex Element of COMPLEX
|.((D . n) - (D . m)).| is complex real ext-real Element of REAL
Im ((D . n) - (D . m)) is complex real ext-real Element of REAL
Im (D . n) is complex real ext-real Element of REAL
Im (D . m) is complex real ext-real Element of REAL
(Im (D . n)) - (Im (D . m)) is complex real ext-real Element of REAL
((D) . n) - (Im (D . m)) is complex real ext-real Element of REAL
seq is complex Element of COMPLEX
m is complex real ext-real Element of REAL
m / 2 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
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
(D . m) - seq is complex Element of COMPLEX
|.((D . m) - seq).| is complex real ext-real Element of REAL
D . n is complex Element of COMPLEX
(D . n) - seq is complex Element of COMPLEX
|.((D . n) - seq).| is complex real ext-real Element of REAL
(m / 2) + (m / 2) is complex real ext-real Element of REAL
|.((D . m) - seq).| + |.((D . n) - seq).| is complex real ext-real Element of REAL
seq - (D . n) is complex Element of COMPLEX
|.(seq - (D . n)).| is complex real ext-real Element of REAL
|.((D . m) - seq).| + |.(seq - (D . n)).| is complex real ext-real Element of REAL
(D . m) - (D . n) is complex Element of COMPLEX
|.((D . m) - (D . n)).| is complex real ext-real Element of REAL
seq is complex real ext-real Element of REAL
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))
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 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 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 Element of COMPLEX
(D . n) - (D . m) is complex Element of COMPLEX
|.((D . n) - (D . m)).| is complex real ext-real Element of REAL
D . n is complex Element of COMPLEX
(D . n) - (D . m) is complex Element of COMPLEX
|.((D . n) - (D . m)).| is complex real ext-real Element of REAL
(seq / 2) + (seq / 2) is complex real ext-real Element of REAL
|.((D . n) - (D . m)).| + |.((D . n) - (D . m)).| is complex real ext-real Element of REAL
((D . n) - (D . m)) - ((D . n) - (D . m)) is complex Element of COMPLEX
|.(((D . n) - (D . m)) - ((D . n) - (D . m))).| is complex real ext-real Element of REAL
(D . n) - (D . n) is complex Element of COMPLEX
|.((D . n) - (D . 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
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 Element of COMPLEX
D . n is complex Element of COMPLEX
(D . n) - (D . n) is complex Element of COMPLEX
|.((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))
lim D 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))
lim seq is complex Element of 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))
abs (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
(abs (seq)) . m is complex real ext-real Element of REAL
(seq) . m is complex real ext-real Element of REAL
abs ((seq) . m) is complex real ext-real Element of REAL
C . m is complex real ext-real Element of REAL
C . 0 is complex real ext-real Element of REAL
lim C 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) . 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
(abs (seq)) . m is complex real ext-real Element of REAL
abs (Re (seq . m)) is complex real ext-real Element of REAL
|.(seq . m).| is complex real ext-real Element of REAL
D . m is complex real ext-real Element of REAL
lim (abs (seq)) 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))
abs (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
(abs (seq)) . m is complex real ext-real Element of REAL
(seq) . m is complex real ext-real Element of REAL
abs ((seq) . m) is complex real ext-real Element of REAL
C . 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) . 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
(abs (seq)) . m is complex real ext-real Element of REAL
abs ((seq) . m) is complex real ext-real Element of REAL
abs (Im (seq . m)) is complex real ext-real Element of REAL
|.(seq . m).| is complex real ext-real Element of REAL
D . m is complex real ext-real Element of REAL
lim (abs (seq)) is complex real ext-real Element of REAL
lim (seq) is complex real ext-real Element of REAL
Im (lim seq) is complex real ext-real Element of REAL
lim (seq) is complex real ext-real Element of REAL
Re (lim seq) 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 Relation-like NAT -defined NAT -valued Function-like non zero total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
(m,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) * m is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (seq)
(seq) * m is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (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 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))
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
abs ((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
abs (Re (D . m)) is complex real ext-real Element of REAL
|.(D . m).| is complex real ext-real Element of REAL
m 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))
n is Relation-like NAT -defined NAT -valued Function-like non zero total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
(D) * n is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (D)
(n,D) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,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,D) . n is complex Element of COMPLEX
|.((n,D) . n).| is complex real ext-real Element of REAL
n . 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 . n) is complex Element of COMPLEX
|.(D . (n . n)).| is complex real ext-real Element of REAL
((n,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))
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,D)) . n is complex real ext-real Element of REAL
abs (((n,D)) . n) is complex real ext-real Element of REAL
(n,D) . n is complex Element of COMPLEX
Im ((n,D) . n) is complex real ext-real Element of REAL
abs (Im ((n,D) . n)) is complex real ext-real Element of REAL
|.((n,D) . n).| is complex real ext-real Element of REAL
n 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 Relation-like NAT -defined NAT -valued Function-like non zero total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
((n,D)) * m is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of ((n,D))
(m,(n,D)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((m,(n,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))
((n,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))
((n,D)) * m is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of ((n,D))
m * m is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of m
((m,(n,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))
NAT --> 0c is Relation-like NAT -defined COMPLEX -valued RAT -valued Function-like constant non zero total V18( NAT , COMPLEX ) T-Sequence-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(NAT,COMPLEX))
((NAT --> 0c)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,COMPLEX))
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
(NAT --> 0c) . m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V61() 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
((NAT --> 0c)) . m is complex real ext-real set
(((NAT --> 0c)) . m) - 0c is complex real ext-real set
|.((((NAT --> 0c)) . m) - 0c).| 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 COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,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))
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))
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 non-decreasing Element of K19(K20(NAT,REAL))
m is complex real ext-real set
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 |.seq.|) . n is complex real ext-real Element of REAL
((Partial_Sums |.seq.|) . n) - 0 is complex real ext-real Element of REAL
abs (((Partial_Sums |.seq.|) . n) - 0) is complex real ext-real Element of REAL
(Partial_Sums |.seq.|) . n is complex real ext-real Element of REAL
((Partial_Sums |.seq.|) . n) - 0 is complex real ext-real Element of REAL
abs (((Partial_Sums |.seq.|) . n) - 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
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
(NAT --> 0c) . seq is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative V61() 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))
|.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 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))
lim seq 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))
((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))
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))
((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))
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))
lim (seq) is complex real ext-real Element of REAL
Im (lim seq) is complex real ext-real Element of REAL
lim (seq) is complex real ext-real Element of REAL
Re (lim seq) 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 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))
(seq) 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))
lim (seq) is complex Element of COMPLEX
Sum (seq) is complex real ext-real Element of 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))
lim (Partial_Sums (seq)) is complex real ext-real Element of REAL
Sum (seq) is complex real ext-real Element of 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))
lim (Partial_Sums (seq)) is complex real ext-real Element of REAL
(Sum (seq)) * <i> is complex set
(Sum (seq)) + ((Sum (seq)) * <i>) is complex 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))
lim ((seq)) 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))
lim ((seq)) is complex real ext-real Element of REAL
Re (lim (seq)) is complex real ext-real Element of REAL
Im (lim (seq)) 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 bounded convergent () 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 convergent Element of K19(K20(NAT,REAL))
m 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 convergent Element of K19(K20(NAT,REAL))
m 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 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))
lim (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))
seq + m is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((seq + m)) is complex Element of COMPLEX
((seq + m)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((seq + m)) is complex Element of COMPLEX
(m) 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))
lim (m) is complex Element of COMPLEX
(seq) + (m) is complex Element of COMPLEX
(seq) + (m) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((seq) + (m)) is complex Element of COMPLEX
(lim (seq)) + (lim (m)) 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))
(seq) 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))
lim (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))
seq - 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 is Relation-like NAT -defined Function-like total complex-valued set
- 1 is non zero complex real ext-real non positive negative set
(- 1) (#) m is Relation-like NAT -defined Function-like total complex-valued set
seq + (- m) is Relation-like NAT -defined Function-like total complex-valued set
((seq - m)) is complex Element of COMPLEX
((seq - m)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((seq - m)) is complex Element of COMPLEX
(m) 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))
lim (m) is complex Element of COMPLEX
(seq) - (m) is complex Element of COMPLEX
(seq) - (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) is Relation-like NAT -defined Function-like total complex-valued set
(- 1) (#) (m) is Relation-like NAT -defined Function-like total complex-valued set
(seq) + (- (m)) is Relation-like NAT -defined Function-like total complex-valued set
lim ((seq) - (m)) is complex Element of COMPLEX
(lim (seq)) - (lim (m)) is complex Element of COMPLEX
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued bounded convergent () Element of K19(K20(NAT,COMPLEX))
m is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued bounded convergent () Element of K19(K20(NAT,COMPLEX))
seq + m is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued bounded convergent Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
seq - m is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued bounded convergent Element of K19(K20(NAT,COMPLEX))
- m is Relation-like NAT -defined Function-like total complex-valued set
- 1 is non zero complex real ext-real non positive negative set
(- 1) (#) m is Relation-like NAT -defined Function-like total complex-valued set
seq + (- m) is Relation-like NAT -defined Function-like total complex-valued set
n 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 COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(seq) 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))
lim (seq) is complex Element of COMPLEX
m is complex set
m (#) seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((m (#) seq)) is complex Element of COMPLEX
((m (#) seq)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((m (#) seq)) is complex Element of COMPLEX
m * (seq) is complex set
m (#) (seq) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
lim (m (#) (seq)) is complex Element of COMPLEX
m is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued bounded convergent () Element of K19(K20(NAT,COMPLEX))
seq is complex Element of COMPLEX
seq (#) m is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued bounded convergent Element of K19(K20(NAT,COMPLEX))
n 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 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))
(seq) 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))
lim (seq) is complex Element of COMPLEX
Sum (seq) is complex real ext-real Element of 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))
lim (Partial_Sums (seq)) is complex real ext-real Element of REAL
Sum (seq) is complex real ext-real Element of 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))
lim (Partial_Sums (seq)) is complex real ext-real Element of REAL
(Sum (seq)) * <i> is complex set
(Sum (seq)) + ((Sum (seq)) * <i>) is complex 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))
((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))
lim ((seq)) is complex real ext-real Element of REAL
Im (lim (seq)) is complex real ext-real Element of REAL
lim ((seq)) is complex real ext-real Element of REAL
Re (lim (seq)) 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))
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 Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued subsequence of seq
((seq ^\ m)) 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))
(seq) ^\ m is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (seq)
((seq ^\ m)) 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))
(seq) ^\ m is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (seq)
seq is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued bounded convergent () Element of K19(K20(NAT,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
seq ^\ m is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued subsequence of seq
n 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 COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,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
seq ^\ m is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued subsequence of seq
((seq ^\ m)) 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))
(seq) ^\ m is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (seq)
((seq ^\ m)) 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))
(seq) ^\ m is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (seq)
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 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))
lim (seq) is complex Element of 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))
Sum (seq) is complex real ext-real Element of 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))
lim (Partial_Sums (seq)) 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))
Sum (seq) is complex real ext-real Element of 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))
lim (Partial_Sums (seq)) is complex real ext-real Element of REAL
(Sum (seq)) * <i> is complex set
(Sum (seq)) + ((Sum (seq)) * <i>) is complex set
Re (seq) is complex real ext-real Element of REAL
Im (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
(seq) . m is complex Element of COMPLEX
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 Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued subsequence of seq
((seq ^\ (m + 1))) is complex Element of COMPLEX
((seq ^\ (m + 1))) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
lim ((seq ^\ (m + 1))) is complex Element of COMPLEX
((seq) . m) + ((seq ^\ (m + 1))) is complex Element of COMPLEX
((seq ^\ (m + 1))) 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))
Sum ((seq ^\ (m + 1))) is complex real ext-real Element of REAL
Partial_Sums ((seq ^\ (m + 1))) 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))
lim (Partial_Sums ((seq ^\ (m + 1)))) is complex real ext-real Element of REAL
((seq ^\ (m + 1))) 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))
Sum ((seq ^\ (m + 1))) is complex real ext-real Element of REAL
Partial_Sums ((seq ^\ (m + 1))) 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))
lim (Partial_Sums ((seq ^\ (m + 1)))) is complex real ext-real Element of REAL
(Sum ((seq ^\ (m + 1)))) * <i> is complex set
(Sum ((seq ^\ (m + 1)))) + ((Sum ((seq ^\ (m + 1)))) * <i>) is complex set
(Partial_Sums (seq)) . m is complex real ext-real Element of REAL
(seq) ^\ (m + 1) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (seq)
Sum ((seq) ^\ (m + 1)) is complex real ext-real Element of REAL
Partial_Sums ((seq) ^\ (m + 1)) 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))
lim (Partial_Sums ((seq) ^\ (m + 1))) is complex real ext-real Element of REAL
((Partial_Sums (seq)) . m) + (Sum ((seq) ^\ (m + 1))) 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
(((seq)) . m) + (Sum ((seq) ^\ (m + 1))) is complex real ext-real Element of REAL
(((seq)) . m) + (Sum ((seq ^\ (m + 1)))) is complex real ext-real Element of REAL
Im ((seq ^\ (m + 1))) is complex real ext-real Element of REAL
(((seq)) . m) + (Im ((seq ^\ (m + 1)))) is complex real ext-real Element of REAL
Im ((seq) . m) is complex real ext-real Element of REAL
(Im ((seq) . m)) + (Im ((seq ^\ (m + 1)))) is complex real ext-real Element of REAL
Im (((seq) . m) + ((seq ^\ (m + 1)))) is complex real ext-real Element of REAL
(Partial_Sums (seq)) . m is complex real ext-real Element of REAL
(seq) ^\ (m + 1) is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of (seq)
Sum ((seq) ^\ (m + 1)) is complex real ext-real Element of REAL
Partial_Sums ((seq) ^\ (m + 1)) 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))
lim (Partial_Sums ((seq) ^\ (m + 1))) is complex real ext-real Element of REAL
((Partial_Sums (seq)) . m) + (Sum ((seq) ^\ (m + 1))) 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
(((seq)) . m) + (Sum ((seq) ^\ (m + 1))) is complex real ext-real Element of REAL
(((seq)) . m) + (Sum ((seq ^\ (m + 1)))) is complex real ext-real Element of REAL
Re ((seq ^\ (m + 1))) is complex real ext-real Element of REAL
(((seq)) . m) + (Re ((seq ^\ (m + 1)))) is complex real ext-real Element of REAL
Re ((seq) . m) is complex real ext-real Element of REAL
(Re ((seq) . m)) + (Re ((seq ^\ (m + 1)))) is complex real ext-real Element of REAL
Re (((seq) . m) + ((seq ^\ (m + 1)))) 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))
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 non-decreasing 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.| . 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 convergent summable 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 non-decreasing Element of K19(K20(NAT,REAL))
m 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 COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
m is complex real ext-real Element of REAL
n 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))
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))
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 non-decreasing Element of K19(K20(NAT,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 |.seq.|) . 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
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 |.seq.|) . m is complex real ext-real Element of REAL
(Partial_Sums |.seq.|) . n is complex real ext-real Element of REAL
((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n) is complex real ext-real Element of REAL
abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) 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) . m is complex Element of COMPLEX
(seq) . n is complex Element of COMPLEX
((seq) . m) - ((seq) . n) is complex Element of COMPLEX
|.(((seq) . m) - ((seq) . n)).| 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))
the Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued bounded convergent () () Element of K19(K20(NAT,COMPLEX)) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued bounded convergent () () Element of K19(K20(NAT,COMPLEX))
seq is complex Element of COMPLEX
|.seq.| 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 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))
lim ((seq)) is complex Element of COMPLEX
1r - seq is complex Element of COMPLEX
1r / (1r - seq) is complex Element of COMPLEX
NAT --> 1r is Relation-like NAT -defined COMPLEX -valued Function-like constant non zero total V18( NAT , COMPLEX ) T-Sequence-like complex-valued Element of K19(K20(NAT,COMPLEX))
n is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
lim 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
((seq)) . 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
(seq) . (n + 1) is complex Element of COMPLEX
1r - (seq,(n + 1)) is complex Element of COMPLEX
(1r - (seq,(n + 1))) / (1r - seq) is complex Element of COMPLEX
n . n is complex Element of COMPLEX
1r - (n . n) is complex Element of COMPLEX
(1r - (n . n)) / (1r - seq) is complex Element of COMPLEX
(NAT --> 1r) . n is complex Element of COMPLEX
((NAT --> 1r) . n) - (n . n) is complex Element of COMPLEX
1r * (((NAT --> 1r) . n) - (n . n)) is complex Element of COMPLEX
(1r * (((NAT --> 1r) . n) - (n . n))) / (1r - seq) is complex Element of COMPLEX
- (n . n) is complex Element of COMPLEX
((NAT --> 1r) . n) + (- (n . n)) is complex Element of COMPLEX
(1r / (1r - seq)) * (((NAT --> 1r) . n) + (- (n . n))) is complex Element of COMPLEX
- n is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(- 1) (#) n is Relation-like NAT -defined Function-like total complex-valued set
(- n) . n is complex Element of COMPLEX
((NAT --> 1r) . n) + ((- n) . n) is complex Element of COMPLEX
(1r / (1r - seq)) * (((NAT --> 1r) . n) + ((- n) . n)) is complex Element of COMPLEX
(NAT --> 1r) - n is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
- n is Relation-like NAT -defined Function-like total complex-valued set
(NAT --> 1r) + (- n) is Relation-like NAT -defined Function-like total complex-valued set
((NAT --> 1r) - n) . n is complex Element of COMPLEX
(1r / (1r - seq)) * (((NAT --> 1r) - n) . n) is complex Element of COMPLEX
(1r / (1r - seq)) (#) ((NAT --> 1r) - n) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
((1r / (1r - seq)) (#) ((NAT --> 1r) - n)) . 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
(NAT --> 1r) . n is complex Element of COMPLEX
lim ((NAT --> 1r) - n) is complex Element of COMPLEX
lim (NAT --> 1r) is complex Element of COMPLEX
(lim (NAT --> 1r)) - (lim n) is complex Element of COMPLEX
lim ((1r / (1r - seq)) (#) ((NAT --> 1r) - n)) is complex Element of COMPLEX
(1r / (1r - seq)) * 1r 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))
(seq) 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))
lim (seq) is complex Element of COMPLEX
seq . 0 is complex Element of COMPLEX
m is complex Element of COMPLEX
|.m.| is complex real ext-real Element of REAL
1r - m is complex Element of COMPLEX
(seq . 0) / (1r - m) 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
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) is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,COMPLEX))
(m) . (n + 1) is complex Element of COMPLEX
1r - (m,(n + 1)) is complex Element of COMPLEX
(1r - (m,(n + 1))) / (1r - m) is complex Element of COMPLEX
(seq . 0) * ((1r - (m,(n + 1))) / (1r - m)) 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)) . n is complex Element of COMPLEX
(seq . 0) * (((m)) . n) is complex Element of COMPLEX
(seq . 0) (#) ((m)) 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) (#) ((m))) . n is complex Element of COMPLEX
((m)) is complex Element of COMPLEX
lim ((m)) is complex Element of COMPLEX
(seq . 0) * ((m)) is complex Element of COMPLEX
1r / (1r - m) is complex Element of COMPLEX
(seq . 0) * (1r / (1r - m)) is complex Element of COMPLEX
(seq . 0) * 1r is complex Element of COMPLEX
((seq . 0) * 1r) / (1r - m) is complex Element of 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))
m is Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued Element of K19(K20(NAT,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 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 complex Element of COMPLEX
|.(m . n).| is complex real ext-real Element of REAL
|.m.| 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.| . 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
m . n is complex Element of COMPLEX
|.(m . n).| is complex real ext-real Element of REAL
seq . n is complex real ext-real Element of REAL
|.m.| . n 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))
Sum |.seq.| is complex real ext-real Element of 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 non-decreasing Element of K19(K20(NAT,REAL))
lim (Partial_Sums |.seq.|) is complex real ext-real Element of REAL
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.| 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))
Sum |.m.| is complex real ext-real Element of REAL
Partial_Sums |.m.| is Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued non-decreasing Element of K19(K20(NAT,REAL))
lim (Partial_Sums |.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))
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 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))
lim seq is complex real ext-real Element of REAL
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.| 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))
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 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))
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.| 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))
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 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
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))
lim seq is complex real ext-real Element of REAL
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.| 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))
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 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))
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.| 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))
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 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
seq . n is complex real ext-real Element of REAL
2 to_power n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of REAL
|.m.| . (2 to_power n) is complex real ext-real Element of REAL
(2 to_power n) * (|.m.| . (2 to_power n)) 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))
m is complex real ext-real Element of REAL
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 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))
lim seq is complex real ext-real Element of REAL
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.| 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))
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 complex Element of COMPLEX
|.m.| . n is complex real ext-real Element of REAL
|.(m . n).| is complex real ext-real Element of REAL
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
|.m.| . (n + 1) is complex real ext-real Element of REAL
(|.m.| . (n + 1)) / (|.m.| . n) is complex real ext-real Element of REAL
abs |.m.| 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 |.m.|) . (n + 1) is complex real ext-real Element of REAL
((abs |.m.|) . (n + 1)) / (|.m.| . n) is complex real ext-real Element of REAL
(abs |.m.|) . n is complex real ext-real Element of REAL
((abs |.m.|) . (n + 1)) / ((abs |.m.|) . n) 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))
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
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
seq . n is complex Element of COMPLEX
|.(seq . n).| is complex real ext-real Element of REAL
|.seq.| . n is complex real ext-real Element of REAL
abs |.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))
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
(abs |.seq.|) . (n + 1) is complex real ext-real Element of REAL
(abs |.seq.|) . n is complex real ext-real Element of REAL
((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) is complex real ext-real Element of REAL