let seq be Real_Sequence; ( seq is convergent & lim seq <> 0 & seq is non-zero implies lim (seq ") = (lim seq) " )
assume that
A1:
seq is convergent
and
A2:
lim seq <> 0
and
A3:
seq is non-zero
; lim (seq ") = (lim seq) "
A4:
seq " is convergent
by A1, A2, A3, Th21;
A5:
0 < |.(lim seq).|
by A2, COMPLEX1:47;
A6:
0 <> |.(lim seq).|
by A2, COMPLEX1:47;
consider n1 being Nat such that
A7:
for m being Nat st n1 <= m holds
|.(lim seq).| / 2 < |.(seq . m).|
by A1, A2, Th16;
0 * 0 < |.(lim seq).| * |.(lim seq).|
by A5;
then A8:
0 < (|.(lim seq).| * |.(lim seq).|) / 2
;
now for p being Real st 0 < p holds
ex n being set st
for m being Nat st n <= m holds
|.(((seq ") . m) - ((lim seq) ")).| < plet p be
Real;
( 0 < p implies ex n being set st
for m being Nat st n <= m holds
|.(((seq ") . m) - ((lim seq) ")).| < p )assume A9:
0 < p
;
ex n being set st
for m being Nat st n <= m holds
|.(((seq ") . m) - ((lim seq) ")).| < pthen
0 * 0 < p * ((|.(lim seq).| * |.(lim seq).|) / 2)
by A8;
then consider n2 being
Nat such that A10:
for
m being
Nat st
n2 <= m holds
|.((seq . m) - (lim seq)).| < p * ((|.(lim seq).| * |.(lim seq).|) / 2)
by A1, Def6;
take n =
n1 + n2;
for m being Nat st n <= m holds
|.(((seq ") . m) - ((lim seq) ")).| < plet m be
Nat;
( n <= m implies |.(((seq ") . m) - ((lim seq) ")).| < p )assume A11:
n <= m
;
|.(((seq ") . m) - ((lim seq) ")).| < p
n2 <= n
by NAT_1:12;
then
n2 <= m
by A11, XXREAL_0:2;
then A12:
|.((seq . m) - (lim seq)).| < p * ((|.(lim seq).| * |.(lim seq).|) / 2)
by A10;
n1 <= n1 + n2
by NAT_1:12;
then
n1 <= m
by A11, XXREAL_0:2;
then A13:
|.(lim seq).| / 2
< |.(seq . m).|
by A7;
A14:
seq . m <> 0
by A3, SEQ_1:5;
then
(seq . m) * (lim seq) <> 0
by A2;
then
0 < |.((seq . m) * (lim seq)).|
by COMPLEX1:47;
then
0 < |.(seq . m).| * |.(lim seq).|
by COMPLEX1:65;
then A15:
|.((seq . m) - (lim seq)).| / (|.(seq . m).| * |.(lim seq).|) < (p * ((|.(lim seq).| * |.(lim seq).|) / 2)) / (|.(seq . m).| * |.(lim seq).|)
by A12, XREAL_1:74;
A16:
(p * ((|.(lim seq).| * |.(lim seq).|) / 2)) / (|.(seq . m).| * |.(lim seq).|) =
(p * ((2 ") * (|.(lim seq).| * |.(lim seq).|))) * ((|.(seq . m).| * |.(lim seq).|) ")
by XCMPLX_0:def 9
.=
(p * (2 ")) * ((|.(lim seq).| * |.(lim seq).|) * ((|.(lim seq).| * |.(seq . m).|) "))
.=
(p * (2 ")) * ((|.(lim seq).| * |.(lim seq).|) * ((|.(lim seq).| ") * (|.(seq . m).| ")))
by XCMPLX_1:204
.=
(p * (2 ")) * ((|.(lim seq).| * (|.(lim seq).| * (|.(lim seq).| "))) * (|.(seq . m).| "))
.=
(p * (2 ")) * ((|.(lim seq).| * 1) * (|.(seq . m).| "))
by A6, XCMPLX_0:def 7
.=
(p * (|.(lim seq).| / 2)) * (|.(seq . m).| ")
.=
(p * (|.(lim seq).| / 2)) / |.(seq . m).|
by XCMPLX_0:def 9
;
A17:
|.(((seq ") . m) - ((lim seq) ")).| =
|.(((seq . m) ") - ((lim seq) ")).|
by VALUED_1:10
.=
|.((seq . m) - (lim seq)).| / (|.(seq . m).| * |.(lim seq).|)
by A2, A14, Th2
;
A18:
0 < |.(lim seq).| / 2
by A5;
A19:
0 <> |.(lim seq).| / 2
by A2, COMPLEX1:47;
0 * 0 < p * (|.(lim seq).| / 2)
by A9, A18;
then A20:
(p * (|.(lim seq).| / 2)) / |.(seq . m).| < (p * (|.(lim seq).| / 2)) / (|.(lim seq).| / 2)
by A13, A18, XREAL_1:76;
(p * (|.(lim seq).| / 2)) / (|.(lim seq).| / 2) =
(p * (|.(lim seq).| / 2)) * ((|.(lim seq).| / 2) ")
by XCMPLX_0:def 9
.=
p * ((|.(lim seq).| / 2) * ((|.(lim seq).| / 2) "))
.=
p * 1
by A19, XCMPLX_0:def 7
.=
p
;
hence
|.(((seq ") . m) - ((lim seq) ")).| < p
by A15, A16, A17, A20, XXREAL_0:2;
verum end;
hence
lim (seq ") = (lim seq) "
by A4, Def6; verum