let seq be Complex_Sequence; :: thesis: for r being Real st r > 0 & ex m being Nat st
for n being Nat st n >= m holds
|.(seq . n).| >= r & |.seq.| is convergent holds
lim |.seq.| <> 0
let r be Real; :: thesis: ( r > 0 & ex m being Nat st
for n being Nat st n >= m holds
|.(seq . n).| >= r & |.seq.| is convergent implies lim |.seq.| <> 0 )
assume that
A1: r > 0 and
A2: ex m being Nat st
for n being Nat st n >= m holds
|.(seq . n).| >= r ; :: thesis: ( not |.seq.| is convergent or lim |.seq.| <> 0 )
consider m being Nat such that
A3: for n being Nat st n >= m holds
|.(seq . n).| >= r by A2;
now :: thesis: for n being Nat st n >= m holds
|.(|.seq.| . n).| >= r
let n be Nat; :: thesis: ( n >= m implies |.(|.seq.| . n).| >= r )
assume A4: n >= m ; :: thesis: |.(|.seq.| . n).| >= r
0 <= |.seq.| . n by Lm3;
then |.(|.seq.| . n).| = |.seq.| . n by ABSVALUE:def 1
.= |.(seq . n).| by VALUED_1:18 ;
hence |.(|.seq.| . n).| >= r by A3, A4; :: thesis: verum
end;
hence ( not |.seq.| is convergent or lim |.seq.| <> 0 ) by A1, SERIES_1:38; :: thesis: verum