let seq be Real_Sequence; :: thesis: ( seq is divergent_to-infty implies ( not seq is divergent_to+infty & not seq is convergent ) )
assume A1: seq is divergent_to-infty ; :: thesis: ( not seq is divergent_to+infty & not seq is convergent )
hereby :: thesis: not seq is convergent
assume seq is divergent_to+infty ; :: thesis: contradiction
then consider n1 being Nat such that
A2: for m being Nat st n1 <= m holds
0 < seq . m by LIMFUNC1:def 4;
consider n2 being Nat such that
A3: for m being Nat st n2 <= m holds
seq . m < 0 by A1, LIMFUNC1:def 5;
reconsider m = max (n1,n2) as Element of NAT by ORDINAL1:def 12;
( seq . m < 0 & seq . m > 0 ) by A2, A3, XXREAL_0:25;
hence contradiction ; :: thesis: verum
end;
assume seq is convergent ; :: thesis: contradiction
then consider g being Real such that
A4: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p by SEQ_2:def 6;
per cases ( g > 0 or g < 0 or g = 0 ) ;
suppose A5: g > 0 ; :: thesis: contradiction
then consider n1 being Nat such that
A6: for m being Nat st n1 <= m holds
|.((seq . m) - g).| < g by A4;
A7: now :: thesis: for m being Nat st n1 <= m holds
0 < seq . m
let m be Nat; :: thesis: ( n1 <= m implies 0 < seq . m )
assume n1 <= m ; :: thesis: 0 < seq . m
then |.((seq . m) - g).| < g by A6;
then A8: - g < - |.((seq . m) - g).| by XREAL_1:24;
- |.((seq . m) - g).| <= (seq . m) - g by ABSVALUE:4;
then - g < (seq . m) - g by A8, XXREAL_0:2;
then (- g) + g < seq . m by XREAL_1:20;
hence 0 < seq . m ; :: thesis: verum
end;
consider n2 being Nat such that
A9: for m being Nat st n2 <= m holds
seq . m < - g by A1, LIMFUNC1:def 5;
reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;
reconsider m = max (n1,n2) as Element of NAT ;
0 < seq . m by A7, XXREAL_0:25;
hence contradiction by A5, A9, XXREAL_0:25; :: thesis: verum
end;
suppose g < 0 ; :: thesis: contradiction
then consider n1 being Nat such that
A10: for m being Nat st n1 <= m holds
|.((seq . m) - g).| < - g by A4, XREAL_1:58;
A11: now :: thesis: for m being Element of NAT st n1 <= m holds
2 * g < seq . m
let m be Element of NAT ; :: thesis: ( n1 <= m implies 2 * g < seq . m )
assume n1 <= m ; :: thesis: 2 * g < seq . m
then |.((seq . m) - g).| < - g by A10;
then A12: - (- g) < - |.((seq . m) - g).| by XREAL_1:24;
- |.((seq . m) - g).| <= (seq . m) - g by ABSVALUE:4;
then - (- g) < (seq . m) - g by A12, XXREAL_0:2;
then g + g < seq . m by XREAL_1:20;
hence 2 * g < seq . m ; :: thesis: verum
end;
consider n2 being Nat such that
A13: for m being Nat st n2 <= m holds
seq . m < 2 * g by A1, LIMFUNC1:def 5;
reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;
reconsider m = max (n1,n2) as Element of NAT ;
2 * g < seq . m by A11, XXREAL_0:25;
hence contradiction by A13, XXREAL_0:25; :: thesis: verum
end;
suppose A14: g = 0 ; :: thesis: contradiction
consider n1 being Nat such that
A15: for m being Nat st n1 <= m holds
|.((seq . m) - g).| < 1 by A4;
consider n2 being Nat such that
A16: for m being Nat st n2 <= m holds
seq . m < - 1 by A1, LIMFUNC1:def 5;
reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;
reconsider m = max (n1,n2) as Element of NAT ;
A17: |.((seq . m) - 0).| < 1 by A14, A15, XXREAL_0:25;
A18: seq . m < - 1 by A16, XXREAL_0:25;
- (- 1) < - (seq . m) by A18, XREAL_1:24;
hence contradiction by A17, A18, ABSVALUE:def 1; :: thesis: verum
end;
end;