let seq be Complex_Sequence; :: thesis: ( seq is bounded implies ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq & seq1 is convergent ) )
assume seq is bounded ; :: thesis: ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq & seq1 is convergent )
then consider r being Real such that
A1: 0 < r and
A2: for n being Nat holds |.(seq . n).| < r by COMSEQ_2:8;
now :: thesis: for n being Nat holds |.((Re seq) . n).| < r
let n be Nat; :: thesis: |.((Re seq) . n).| < r
( |.((Re seq) . n).| = |.(Re (seq . n)).| & |.(Re (seq . n)).| <= |.(seq . n).| ) by Def5, Th13;
hence |.((Re seq) . n).| < r by A2, XXREAL_0:2; :: thesis: verum
end;
then Re seq is bounded by A1, SEQ_2:3;
then consider rseq1 being Real_Sequence such that
A3: rseq1 is subsequence of Re seq and
A4: rseq1 is convergent by SEQ_4:40;
consider Nseq being increasing sequence of NAT such that
A5: rseq1 = (Re seq) * Nseq by A3, VALUED_0:def 17;
A6: now :: thesis: for n being Nat holds |.((seq * Nseq) . n).| < r
let n be Nat; :: thesis: |.((seq * Nseq) . n).| < r
n in NAT by ORDINAL1:def 12;
then |.((seq * Nseq) . n).| = |.(seq . (Nseq . n)).| by FUNCT_2:15;
hence |.((seq * Nseq) . n).| < r by A2; :: thesis: verum
end;
now :: thesis: for n being Nat holds |.((Im (seq * Nseq)) . n).| < r
let n be Nat; :: thesis: |.((Im (seq * Nseq)) . n).| < r
( |.((Im (seq * Nseq)) . n).| = |.(Im ((seq * Nseq) . n)).| & |.(Im ((seq * Nseq) . n)).| <= |.((seq * Nseq) . n).| ) by Def6, Th13;
hence |.((Im (seq * Nseq)) . n).| < r by A6, XXREAL_0:2; :: thesis: verum
end;
then Im (seq * Nseq) is bounded by A1, SEQ_2:3;
then consider rseq2 being Real_Sequence such that
A7: rseq2 is subsequence of Im (seq * Nseq) and
A8: rseq2 is convergent by SEQ_4:40;
consider Nseq1 being increasing sequence of NAT such that
A9: rseq2 = (Im (seq * Nseq)) * Nseq1 by A7, VALUED_0:def 17;
Re ((seq * Nseq) * Nseq1) = (Re (seq * Nseq)) * Nseq1 by Th22
.= rseq1 * Nseq1 by A5, Th22 ;
then A10: Re ((seq * Nseq) * Nseq1) is convergent by A4, SEQ_4:16;
( seq * Nseq is subsequence of seq & (seq * Nseq) * Nseq1 is subsequence of seq * Nseq ) by VALUED_0:def 17;
then A11: (seq * Nseq) * Nseq1 is subsequence of seq by VALUED_0:20;
Im ((seq * Nseq) * Nseq1) is convergent by A8, A9, Th22;
hence ex seq1 being Complex_Sequence st
( seq1 is subsequence of seq & seq1 is convergent ) by A11, A10, Th42; :: thesis: verum