let seq be Real_Sequence; :: thesis: ( seq is convergent implies lim (abs seq) = |.(lim seq).| )
assume A1: seq is convergent ; :: thesis: lim (abs seq) = |.(lim seq).|
now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((abs seq) . m) - |.(lim seq).|).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((abs seq) . m) - |.(lim seq).|).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((abs seq) . m) - |.(lim seq).|).| < p
then consider n1 being Nat such that
A2: for m being Nat st n1 <= m holds
|.((seq . m) - (lim seq)).| < p by A1, SEQ_2:def 7;
take n = n1; :: thesis: for m being Nat st n <= m holds
|.(((abs seq) . m) - |.(lim seq).|).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((abs seq) . m) - |.(lim seq).|).| < p )
|.((lim seq) - (seq . m)).| = |.(- ((seq . m) - (lim seq))).|
.= |.((seq . m) - (lim seq)).| by COMPLEX1:52 ;
then |.(lim seq).| - |.(seq . m).| <= |.((seq . m) - (lim seq)).| by COMPLEX1:59;
then ( |.(seq . m).| - |.(lim seq).| <= |.((seq . m) - (lim seq)).| & - |.((seq . m) - (lim seq)).| <= - (|.(lim seq).| - |.(seq . m).|) ) by COMPLEX1:59, XREAL_1:24;
then |.(|.(seq . m).| - |.(lim seq).|).| <= |.((seq . m) - (lim seq)).| by ABSVALUE:5;
then A3: |.(((abs seq) . m) - |.(lim seq).|).| <= |.((seq . m) - (lim seq)).| by SEQ_1:12;
assume n <= m ; :: thesis: |.(((abs seq) . m) - |.(lim seq).|).| < p
then |.((seq . m) - (lim seq)).| < p by A2;
hence |.(((abs seq) . m) - |.(lim seq).|).| < p by A3, XXREAL_0:2; :: thesis: verum
end;
hence lim (abs seq) = |.(lim seq).| by A1, SEQ_2:def 7; :: thesis: verum