let seq be Complex_Sequence; :: thesis: for r being Real st r > 0 & ex m being Element of NAT st
for n being Element of 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 Element of NAT st
for n being Element of NAT st n >= m holds
|.(seq . n).| >= r & |.seq.| is convergent implies lim |.seq.| <> 0 )
assume A1: ( r > 0 & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
|.(seq . n).| >= r ) ; :: thesis: ( not |.seq.| is convergent or lim |.seq.| <> 0 )
then consider m being Element of NAT such that
A2: for n being Element of NAT st n >= m holds
|.(seq . n).| >= r ;

now

let n be Element of NAT ; :: thesis: ( n >= m implies abs (|.seq.| . n) >= r )
assume A3: n >= m ; :: thesis: abs (|.seq.| . n) >= r
0 <= |.seq.| . n by Lm3;
then abs (|.seq.| . n) = |.seq.| . n by ABSVALUE:def 1
.= |.(seq . n).| by VALUED_1:18 ;
hence abs (|.seq.| . n) >= r by A2, A3; :: thesis: verum

end;

hence ( not |.seq.| is convergent or lim |.seq.| <> 0 ) by A1, SERIES_1:43; :: thesis: verum