let rseq1 be Real_Sequence; :: thesis: for seq2 being Complex_Sequence st rseq1 is summable & ex m being Nat st
for n being Nat st m <= n holds
|.(seq2 . n).| <= rseq1 . n holds
seq2 is absolutely_summable
let seq2 be Complex_Sequence; :: thesis: ( rseq1 is summable & ex m being Nat st
for n being Nat st m <= n holds
|.(seq2 . n).| <= rseq1 . n implies seq2 is absolutely_summable )
assume that
A1: rseq1 is summable and
A2: ex m being Nat st
for n being Nat st m <= n holds
|.(seq2 . n).| <= rseq1 . n ; :: thesis: seq2 is absolutely_summable
consider m being Nat such that
A3: for n being Nat st m <= n holds
|.(seq2 . n).| <= rseq1 . n by A2;
A4: now :: thesis: for n being Nat holds 0 <= |.seq2.| . n
let n be Nat; :: thesis: 0 <= |.seq2.| . n
|.(seq2 . n).| = |.seq2.| . n by VALUED_1:18;
hence 0 <= |.seq2.| . n by COMPLEX1:46; :: thesis: verum
end;
now :: thesis: for n being Nat st m <= n holds
|.seq2.| . n <= rseq1 . n
let n be Nat; :: thesis: ( m <= n implies |.seq2.| . n <= rseq1 . n )
assume m <= n ; :: thesis: |.seq2.| . n <= rseq1 . n
then |.(seq2 . n).| <= rseq1 . n by A3;
hence |.seq2.| . n <= rseq1 . n by VALUED_1:18; :: thesis: verum
end;
hence |.seq2.| is summable by A1, A4, SERIES_1:19; :: according to COMSEQ_3:def 9 :: thesis: verum