let seq be ExtREAL_sequence; :: thesis: ( seq is convergent_to_-infty implies ( not seq is convergent_to_+infty & not seq is convergent_to_finite_number ) )

assume A1: seq is convergent_to_-infty ; :: thesis: ( not seq is convergent_to_+infty & not seq is convergent_to_finite_number )

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 ;

reconsider g1 = g as R_eal by XXREAL_0:def 1;

assume A1: seq is convergent_to_-infty ; :: thesis: ( not seq is convergent_to_+infty & not seq is convergent_to_finite_number )

hereby :: thesis: not seq is convergent_to_finite_number

assume
seq is convergent_to_finite_number
; :: thesis: contradictionassume
seq is convergent_to_+infty
; :: thesis: contradiction

then consider n1 being Nat such that

A2: for m being Nat st n1 <= m holds

1 <= seq . m ;

consider n2 being Nat such that

A3: for m being Nat st n2 <= m holds

seq . m <= - 1 by A1;

reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;

set m = max (n1,n2);

seq . (max (n1,n2)) <= - 1 by A3, XXREAL_0:25;

hence contradiction by A2, XXREAL_0:25; :: thesis: verum

end;then consider n1 being Nat such that

A2: for m being Nat st n1 <= m holds

1 <= seq . m ;

consider n2 being Nat such that

A3: for m being Nat st n2 <= m holds

seq . m <= - 1 by A1;

reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;

set m = max (n1,n2);

seq . (max (n1,n2)) <= - 1 by A3, XXREAL_0:25;

hence contradiction by A2, XXREAL_0:25; :: thesis: verum

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 ;

reconsider g1 = g as R_eal by XXREAL_0:def 1;

per cases
( g > 0 or g = 0 or g < 0 )
;

end;

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;

A8: for m being Nat st n2 <= m holds

seq . m <= - g1 by A1, A5;

reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;

set m = max (n1,n2);

0 < seq . (max (n1,n2)) by A7, XXREAL_0:25;

hence contradiction by A5, A8, XXREAL_0:25; :: thesis: verum

end;A6: for m being Nat st n1 <= m holds

|.((seq . m) - g).| < g by A4;

A7: now :: thesis: for m being Element of NAT st n1 <= m holds

0 < seq . m

consider n2 being Nat such that 0 < seq . m

let m be Element of NAT ; :: thesis: ( n1 <= m implies 0 < seq . m )

assume n1 <= m ; :: thesis: 0 < seq . m

then |.((seq . m) - g1).| < g by A6;

then - g1 < (seq . m) - g by EXTREAL1:21;

then (- g) + g < seq . m by XXREAL_3:53;

hence 0 < seq . m ; :: thesis: verum

end;assume n1 <= m ; :: thesis: 0 < seq . m

then |.((seq . m) - g1).| < g by A6;

then - g1 < (seq . m) - g by EXTREAL1:21;

then (- g) + g < seq . m by XXREAL_3:53;

hence 0 < seq . m ; :: thesis: verum

A8: for m being Nat st n2 <= m holds

seq . m <= - g1 by A1, A5;

reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;

set m = max (n1,n2);

0 < seq . (max (n1,n2)) by A7, XXREAL_0:25;

hence contradiction by A5, A8, XXREAL_0:25; :: thesis: verum

suppose A9:
g = 0
; :: thesis: contradiction

consider n1 being Nat such that

A10: for m being Nat st n1 <= m holds

|.((seq . m) - g).| < 1 by A4;

consider n2 being Nat such that

A11: for m being Nat st n2 <= m holds

seq . m <= - 1 by A1;

reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;

reconsider jj = 1 as R_eal by XXREAL_0:def 1;

set m = max (n1,n2);

|.((seq . (max (n1,n2))) - g1).| < 1 by A10, XXREAL_0:25;

then - jj < (seq . (max (n1,n2))) - g1 by EXTREAL1:21;

then (- 1) + g < seq . (max (n1,n2)) by XXREAL_3:53;

then - 1 < seq . (max (n1,n2)) by A9;

then - 1 < seq . (max (n1,n2)) ;

hence contradiction by A11, XXREAL_0:25; :: thesis: verum

end;A10: for m being Nat st n1 <= m holds

|.((seq . m) - g).| < 1 by A4;

consider n2 being Nat such that

A11: for m being Nat st n2 <= m holds

seq . m <= - 1 by A1;

reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;

reconsider jj = 1 as R_eal by XXREAL_0:def 1;

set m = max (n1,n2);

|.((seq . (max (n1,n2))) - g1).| < 1 by A10, XXREAL_0:25;

then - jj < (seq . (max (n1,n2))) - g1 by EXTREAL1:21;

then (- 1) + g < seq . (max (n1,n2)) by XXREAL_3:53;

then - 1 < seq . (max (n1,n2)) by A9;

then - 1 < seq . (max (n1,n2)) ;

hence contradiction by A11, XXREAL_0:25; :: thesis: verum

suppose A12:
g < 0
; :: thesis: contradiction

then consider n1 being Nat such that

A13: for m being Nat st n1 <= m holds

|.((seq . m) - g).| < - g1 by A4;

A15: for m being Nat st n2 <= m holds

seq . m <= 2 * g by A1, A12;

reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;

set m = max (n1,n2);

seq . (max (n1,n2)) <= 2 * g by A15, XXREAL_0:25;

hence contradiction by A14, XXREAL_0:25; :: thesis: verum

end;A13: for m being Nat st n1 <= m holds

|.((seq . m) - g).| < - g1 by A4;

A14: now :: thesis: for m being Element of NAT st n1 <= m holds

2 * g < seq . m

consider n2 being Nat such that 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) - g1).| < - g1 by A13;

then - (- g1) < (seq . m) - g by EXTREAL1:21;

then g1 + g < seq . m by XXREAL_3:53;

then g + g < seq . m ;

hence 2 * g < seq . m ; :: thesis: verum

end;assume n1 <= m ; :: thesis: 2 * g < seq . m

then |.((seq . m) - g1).| < - g1 by A13;

then - (- g1) < (seq . m) - g by EXTREAL1:21;

then g1 + g < seq . m by XXREAL_3:53;

then g + g < seq . m ;

hence 2 * g < seq . m ; :: thesis: verum

A15: for m being Nat st n2 <= m holds

seq . m <= 2 * g by A1, A12;

reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 12;

set m = max (n1,n2);

seq . (max (n1,n2)) <= 2 * g by A15, XXREAL_0:25;

hence contradiction by A14, XXREAL_0:25; :: thesis: verum