let seq be Real_Sequence; :: thesis: ( seq is convergent iff for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < s )
thus ( seq is convergent implies for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < s ) :: thesis: ( ( for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < s ) implies seq is convergent )
proof
assume seq is convergent ; :: thesis: for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < s
then consider g1 being Real such that
A1: for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g1).| < s ;
let s be Real; :: thesis: ( 0 < s implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < s )
assume 0 < s ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < s
then consider n1 being Nat such that
A2: for m being Nat st n1 <= m holds
|.((seq . m) - g1).| < s / 2 by A1;
take n = n1; :: thesis: for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < s
let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - (seq . n)).| < s )
assume n <= m ; :: thesis: |.((seq . m) - (seq . n)).| < s
then A3: |.((seq . m) - g1).| < s / 2 by A2;
A4: |.(((seq . m) - g1) + (g1 - (seq . n))).| <= |.((seq . m) - g1).| + |.(g1 - (seq . n)).| by COMPLEX1:56;
|.((seq . n) - g1).| < s / 2 by A2;
then |.(- (g1 - (seq . n))).| < s / 2 ;
then |.(g1 - (seq . n)).| < s / 2 by COMPLEX1:52;
then |.((seq . m) - g1).| + |.(g1 - (seq . n)).| < (s / 2) + (s / 2) by A3, XREAL_1:8;
hence |.((seq . m) - (seq . n)).| < s by A4, XXREAL_0:2; :: thesis: verum
end;
assume A5: for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < s ; :: thesis: seq is convergent
then consider n1 being Nat such that
A6: for m being Nat st n1 <= m holds
|.((seq . m) - (seq . n1)).| < 1 ;
consider r1 being Real such that
A7: 0 < r1 and
A8: for m being Nat st m <= n1 holds
|.(seq . m).| < r1 by SEQ_2:4;
now :: thesis: ex r being set st
( 0 < r & ( for m being Nat holds |.(seq . m).| < r ) )
take r = (r1 + |.(seq . n1).|) + 1; :: thesis: ( 0 < r & ( for m being Nat holds |.(seq . m).| < r ) )
0 + 0 < r1 + |.(seq . n1).| by A7, COMPLEX1:46, XREAL_1:8;
hence 0 < r ; :: thesis: for m being Nat holds |.(seq . m).| < r
let m be Nat; :: thesis: |.(seq . m).| < r
A9: now :: thesis: ( n1 <= m implies |.(seq . m).| < r )
assume n1 <= m ; :: thesis: |.(seq . m).| < r
then A10: |.((seq . m) - (seq . n1)).| < 1 by A6;
|.(seq . m).| - |.(seq . n1).| <= |.((seq . m) - (seq . n1)).| by COMPLEX1:59;
then |.(seq . m).| - |.(seq . n1).| < 1 by A10, XXREAL_0:2;
then (|.(seq . m).| - |.(seq . n1).|) + |.(seq . n1).| < 1 + |.(seq . n1).| by XREAL_1:6;
then 0 + |.(seq . m).| < r1 + (|.(seq . n1).| + 1) by A7, XREAL_1:8;
hence |.(seq . m).| < r ; :: thesis: verum
end;
now :: thesis: ( m <= n1 implies |.(seq . m).| < r )
assume m <= n1 ; :: thesis: |.(seq . m).| < r
then |.(seq . m).| < r1 by A8;
then |.(seq . m).| + 0 < r1 + |.(seq . n1).| by COMPLEX1:46, XREAL_1:8;
hence |.(seq . m).| < r by XREAL_1:8; :: thesis: verum
end;
hence |.(seq . m).| < r by A9; :: thesis: verum
end;
then seq is bounded by SEQ_2:3;
then consider seq1 being Real_Sequence such that
A11: seq1 is subsequence of seq and
A12: seq1 is convergent by Th40;
consider g1 being Real such that
A13: for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - g1).| < s by A12;
take g1 ; :: according to SEQ_2:def 6 :: thesis: for b1 being object holds
( b1 <= 0 or ex b2 being set st
for b3 being set holds
( not b2 <= b3 or not b1 <= |.((seq . b3) - g1).| ) )
let s be Real; :: thesis: ( s <= 0 or ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not s <= |.((seq . b2) - g1).| ) )
assume A14: 0 < s ; :: thesis: ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not s <= |.((seq . b2) - g1).| )
then consider n1 being Nat such that
A15: for m being Nat st n1 <= m holds
|.((seq1 . m) - g1).| < s / 3 by A13;
consider n2 being Nat such that
A16: for m being Nat st n2 <= m holds
|.((seq . m) - (seq . n2)).| < s / 3 by A5, A14;
take n = n1 + n2; :: thesis: for b1 being set holds
( not n <= b1 or not s <= |.((seq . b1) - g1).| )
let m be Nat; :: thesis: ( not n <= m or not s <= |.((seq . m) - g1).| )
assume A17: n <= m ; :: thesis: not s <= |.((seq . m) - g1).|
consider Nseq being V45() sequence of NAT such that
A18: seq1 = seq * Nseq by A11, VALUED_0:def 17;
A19: m in NAT by ORDINAL1:def 12;
n1 <= n by NAT_1:12;
then n1 <= m by A17, XXREAL_0:2;
then |.(((seq * Nseq) . m) - g1).| < s / 3 by A18, A15;
then A20: |.((seq . (Nseq . m)) - g1).| < s / 3 by FUNCT_2:15, A19;
n2 <= n by NAT_1:12;
then A21: n2 <= m by A17, XXREAL_0:2;
m <= Nseq . m by SEQM_3:14;
then n2 <= Nseq . m by A21, XXREAL_0:2;
then |.((seq . (Nseq . m)) - (seq . n2)).| < s / 3 by A16;
then |.(- ((seq . n2) - (seq . (Nseq . m)))).| < s / 3 ;
then A22: |.((seq . n2) - (seq . (Nseq . m))).| < s / 3 by COMPLEX1:52;
|.((seq . m) - (seq . n2)).| < s / 3 by A16, A21;
then A23: |.((seq . m) - (seq . n2)).| + |.((seq . n2) - (seq . (Nseq . m))).| < (s / 3) + (s / 3) by A22, XREAL_1:8;
|.(((seq . m) - (seq . n2)) + ((seq . n2) - (seq . (Nseq . m)))).| <= |.((seq . m) - (seq . n2)).| + |.((seq . n2) - (seq . (Nseq . m))).| by COMPLEX1:56;
then |.((seq . m) - (seq . (Nseq . m))).| < (s / 3) + (s / 3) by A23, XXREAL_0:2;
then A24: |.((seq . m) - (seq . (Nseq . m))).| + |.((seq . (Nseq . m)) - g1).| < ((s / 3) + (s / 3)) + (s / 3) by A20, XREAL_1:8;
|.(((seq . m) - (seq . (Nseq . m))) + ((seq . (Nseq . m)) - g1)).| <= |.((seq . m) - (seq . (Nseq . m))).| + |.((seq . (Nseq . m)) - g1).| by COMPLEX1:56;
hence not s <= |.((seq . m) - g1).| by A24, XXREAL_0:2; :: thesis: verum