let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq <> 0 & seq is non-empty implies seq " is convergent )
assume that
A1: seq is convergent and
A2: lim seq <> 0 and
A3: seq is non-empty ; :: thesis: seq " is convergent
A4: 0 < abs (lim seq) by A2, COMPLEX1:47;
A5: 0 <> abs (lim seq) by A2, COMPLEX1:47;
consider n1 being Element of NAT such that
A6: for m being Element of NAT st n1 <= m holds
(abs (lim seq)) / 2 < abs (seq . m) by A1, A2, Th30;
0 * 0 < (abs (lim seq)) * (abs (lim seq)) by A4, XREAL_1:96;
then A7: 0 < ((abs (lim seq)) * (abs (lim seq))) / 2 by XREAL_1:215;
take (lim seq) " ; :: according to SEQ_2:def 6 :: thesis: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq ") . m) - ((lim seq) ")) < p
let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq ") . m) - ((lim seq) ")) < p )
assume A8: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq ") . m) - ((lim seq) ")) < p
then 0 * 0 < p * (((abs (lim seq)) * (abs (lim seq))) / 2) by A7, XREAL_1:96;
then consider n2 being Element of NAT such that
A9: for m being Element of NAT st n2 <= m holds
abs ((seq . m) - (lim seq)) < p * (((abs (lim seq)) * (abs (lim seq))) / 2) by A1, Def7;
take n = n1 + n2; :: thesis: for m being Element of NAT st n <= m holds
abs (((seq ") . m) - ((lim seq) ")) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((seq ") . m) - ((lim seq) ")) < p )
assume A10: n <= m ; :: thesis: abs (((seq ") . m) - ((lim seq) ")) < p
n2 <= n by NAT_1:12;
then n2 <= m by A10, XXREAL_0:2;
then A11: abs ((seq . m) - (lim seq)) < p * (((abs (lim seq)) * (abs (lim seq))) / 2) by A9;
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A10, XXREAL_0:2;
then A12: (abs (lim seq)) / 2 < abs (seq . m) by A6;
A13: seq . m <> 0 by A3, SEQ_1:5;
then (seq . m) * (lim seq) <> 0 by A2, XCMPLX_1:6;
then 0 < abs ((seq . m) * (lim seq)) by COMPLEX1:47;
then 0 < (abs (seq . m)) * (abs (lim seq)) by COMPLEX1:65;
then A14: (abs ((seq . m) - (lim seq))) / ((abs (seq . m)) * (abs (lim seq))) < (p * (((abs (lim seq)) * (abs (lim seq))) / 2)) / ((abs (seq . m)) * (abs (lim seq))) by A11, XREAL_1:74;
A15: (p * (((abs (lim seq)) * (abs (lim seq))) / 2)) / ((abs (seq . m)) * (abs (lim seq))) = (p * ((2 ") * ((abs (lim seq)) * (abs (lim seq))))) * (((abs (seq . m)) * (abs (lim seq))) ") by XCMPLX_0:def 9
.= (p * (2 ")) * (((abs (lim seq)) * (abs (lim seq))) * (((abs (lim seq)) * (abs (seq . m))) "))
.= (p * (2 ")) * (((abs (lim seq)) * (abs (lim seq))) * (((abs (lim seq)) ") * ((abs (seq . m)) "))) by XCMPLX_1:204
.= (p * (2 ")) * (((abs (lim seq)) * ((abs (lim seq)) * ((abs (lim seq)) "))) * ((abs (seq . m)) "))
.= (p * (2 ")) * (((abs (lim seq)) * 1) * ((abs (seq . m)) ")) by A5, XCMPLX_0:def 7
.= (p * ((abs (lim seq)) / 2)) * ((abs (seq . m)) ")
.= (p * ((abs (lim seq)) / 2)) / (abs (seq . m)) by XCMPLX_0:def 9 ;
A16: abs (((seq ") . m) - ((lim seq) ")) = abs (((seq . m) ") - ((lim seq) ")) by VALUED_1:10
.= (abs ((seq . m) - (lim seq))) / ((abs (seq . m)) * (abs (lim seq))) by A2, A13, Th11 ;
A17: 0 < (abs (lim seq)) / 2 by A4, XREAL_1:215;
A18: 0 <> (abs (lim seq)) / 2 by A2, COMPLEX1:47;
0 * 0 < p * ((abs (lim seq)) / 2) by A8, A17, XREAL_1:96;
then A19: (p * ((abs (lim seq)) / 2)) / (abs (seq . m)) < (p * ((abs (lim seq)) / 2)) / ((abs (lim seq)) / 2) by A12, A17, XREAL_1:76;
(p * ((abs (lim seq)) / 2)) / ((abs (lim seq)) / 2) = (p * ((abs (lim seq)) / 2)) * (((abs (lim seq)) / 2) ") by XCMPLX_0:def 9
.= p * (((abs (lim seq)) / 2) * (((abs (lim seq)) / 2) "))
.= p * 1 by A18, XCMPLX_0:def 7
.= p ;
hence abs (((seq ") . m) - ((lim seq) ")) < p by A14, A15, A16, A19, XXREAL_0:2; :: thesis: verum