let L be ExtREAL_sequence; :: thesis: ( ( for n, m being Nat st n <= m holds

L . n <= L . m ) implies ( L is convergent & lim L = sup (rng L) ) )

assume A1: for n, m being Nat st n <= m holds

L . n <= L . m ; :: thesis: ( L is convergent & lim L = sup (rng L) )

L . n <= L . m ) implies ( L is convergent & lim L = sup (rng L) ) )

assume A1: for n, m being Nat st n <= m holds

L . n <= L . m ; :: thesis: ( L is convergent & lim L = sup (rng L) )

A2: now :: thesis: for n being Nat holds L . n <= sup (rng L)

let n be Nat; :: thesis: L . n <= sup (rng L)

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

dom L = NAT by FUNCT_2:def 1;

then A3: L . n1 in rng L by FUNCT_1:def 3;

sup (rng L) is UpperBound of rng L by XXREAL_2:def 3;

hence L . n <= sup (rng L) by A3, XXREAL_2:def 1; :: thesis: verum

end;reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

dom L = NAT by FUNCT_2:def 1;

then A3: L . n1 in rng L by FUNCT_1:def 3;

sup (rng L) is UpperBound of rng L by XXREAL_2:def 3;

hence L . n <= sup (rng L) by A3, XXREAL_2:def 1; :: thesis: verum

per cases
( for k0 being Nat holds not -infty < L . k0 or ex k0 being Nat st -infty < L . k0 )
;

end;

suppose A4:
for k0 being Nat holds not -infty < L . k0
; :: thesis: ( L is convergent & lim L = sup (rng L) )

for y being UpperBound of rng L holds -infty <= y by XXREAL_0:5;

then A6: -infty = sup (rng L) by A5, XXREAL_2:def 3;

then L is convergent ;

hence ( L is convergent & lim L = sup (rng L) ) by A7, A6, Def12; :: thesis: verum

end;

now :: thesis: for x being ExtReal st x in rng L holds

x <= -infty

then A5:
-infty is UpperBound of rng L
by XXREAL_2:def 1;x <= -infty

let x be ExtReal; :: thesis: ( x in rng L implies x <= -infty )

assume x in rng L ; :: thesis: x <= -infty

then ex n being object st

( n in dom L & x = L . n ) by FUNCT_1:def 3;

hence x <= -infty by A4; :: thesis: verum

end;assume x in rng L ; :: thesis: x <= -infty

then ex n being object st

( n in dom L & x = L . n ) by FUNCT_1:def 3;

hence x <= -infty by A4; :: thesis: verum

for y being UpperBound of rng L holds -infty <= y by XXREAL_0:5;

then A6: -infty = sup (rng L) by A5, XXREAL_2:def 3;

now :: thesis: for K being Real st K < 0 holds

ex N0 being Nat st

for n being Nat st N0 <= n holds

L . n <= K

then A7:
L is convergent_to_-infty
;ex N0 being Nat st

for n being Nat st N0 <= n holds

L . n <= K

reconsider N0 = 0 as Nat ;

let K be Real; :: thesis: ( K < 0 implies ex N0 being Nat st

for n being Nat st N0 <= n holds

L . n <= K )

assume K < 0 ; :: thesis: ex N0 being Nat st

for n being Nat st N0 <= n holds

L . n <= K

take N0 = N0; :: thesis: for n being Nat st N0 <= n holds

L . n <= K

let n be Nat; :: thesis: ( N0 <= n implies L . n <= K )

assume N0 <= n ; :: thesis: L . n <= K

L . n = -infty by A4, XXREAL_0:6;

hence L . n <= K by XXREAL_0:5; :: thesis: verum

end;let K be Real; :: thesis: ( K < 0 implies ex N0 being Nat st

for n being Nat st N0 <= n holds

L . n <= K )

assume K < 0 ; :: thesis: ex N0 being Nat st

for n being Nat st N0 <= n holds

L . n <= K

take N0 = N0; :: thesis: for n being Nat st N0 <= n holds

L . n <= K

let n be Nat; :: thesis: ( N0 <= n implies L . n <= K )

assume N0 <= n ; :: thesis: L . n <= K

L . n = -infty by A4, XXREAL_0:6;

hence L . n <= K by XXREAL_0:5; :: thesis: verum

then L is convergent ;

hence ( L is convergent & lim L = sup (rng L) ) by A7, A6, Def12; :: thesis: verum

suppose
ex k0 being Nat st -infty < L . k0
; :: thesis: ( L is convergent & lim L = sup (rng L) )

then consider k0 being Nat such that

A8: -infty < L . k0 ;

reconsider k0 = k0 as Element of NAT by ORDINAL1:def 12;

end;A8: -infty < L . k0 ;

reconsider k0 = k0 as Element of NAT by ORDINAL1:def 12;

per cases
( ex K being Real st

for n being Nat holds L . n < K or for K being Real holds

( not 0 < K or ex n being Nat st not L . n < K ) ) ;

end;

for n being Nat holds L . n < K or for K being Real holds

( not 0 < K or ex n being Nat st not L . n < K ) ) ;

suppose
ex K being Real st

for n being Nat holds L . n < K ; :: thesis: ( L is convergent & lim L = sup (rng L) )

for n being Nat holds L . n < K ; :: thesis: ( L is convergent & lim L = sup (rng L) )

then consider K being Real such that

A9: for n being Nat holds L . n < K ;

then A10: sup (rng L) <= K by XXREAL_2:def 3;

K in REAL by XREAL_0:def 1;

then A11: sup (rng L) <> +infty by A10, XXREAL_0:9;

A12: sup (rng L) <> -infty by A2, A8;

then reconsider h = sup (rng L) as Element of REAL by A11, XXREAL_0:14;

A13: for p being Real st 0 < p holds

ex N0 being Nat st

for m being Nat st N0 <= m holds

|.((L . m) - (sup (rng L))).| < p

then A25: L is convergent_to_finite_number by A13;

hence L is convergent ; :: thesis: lim L = sup (rng L)

hence lim L = sup (rng L) by A13, A24, A25, Def12; :: thesis: verum

end;A9: for n being Nat holds L . n < K ;

now :: thesis: for x being ExtReal st x in rng L holds

x <= K

then
K is UpperBound of rng L
by XXREAL_2:def 1;x <= K

let x be ExtReal; :: thesis: ( x in rng L implies x <= K )

assume x in rng L ; :: thesis: x <= K

then ex z being object st

( z in dom L & x = L . z ) by FUNCT_1:def 3;

hence x <= K by A9; :: thesis: verum

end;assume x in rng L ; :: thesis: x <= K

then ex z being object st

( z in dom L & x = L . z ) by FUNCT_1:def 3;

hence x <= K by A9; :: thesis: verum

then A10: sup (rng L) <= K by XXREAL_2:def 3;

K in REAL by XREAL_0:def 1;

then A11: sup (rng L) <> +infty by A10, XXREAL_0:9;

A12: sup (rng L) <> -infty by A2, A8;

then reconsider h = sup (rng L) as Element of REAL by A11, XXREAL_0:14;

A13: for p being Real st 0 < p holds

ex N0 being Nat st

for m being Nat st N0 <= m holds

|.((L . m) - (sup (rng L))).| < p

proof

A24:
h = sup (rng L)
;
let p be Real; :: thesis: ( 0 < p implies ex N0 being Nat st

for m being Nat st N0 <= m holds

|.((L . m) - (sup (rng L))).| < p )

assume A14: 0 < p ; :: thesis: ex N0 being Nat st

for m being Nat st N0 <= m holds

|.((L . m) - (sup (rng L))).| < p

reconsider e = p as R_eal by XXREAL_0:def 1;

sup (rng L) in REAL by A12, A11, XXREAL_0:14;

then consider y being ExtReal such that

A15: y in rng L and

A16: (sup (rng L)) - e < y by A14, MEASURE6:6;

consider x being object such that

A17: x in dom L and

A18: y = L . x by A15, FUNCT_1:def 3;

reconsider N1 = x as Element of NAT by A17;

set N0 = max (N1,k0);

take max (N1,k0) ; :: thesis: for m being Nat st max (N1,k0) <= m holds

|.((L . m) - (sup (rng L))).| < p

end;for m being Nat st N0 <= m holds

|.((L . m) - (sup (rng L))).| < p )

assume A14: 0 < p ; :: thesis: ex N0 being Nat st

for m being Nat st N0 <= m holds

|.((L . m) - (sup (rng L))).| < p

reconsider e = p as R_eal by XXREAL_0:def 1;

sup (rng L) in REAL by A12, A11, XXREAL_0:14;

then consider y being ExtReal such that

A15: y in rng L and

A16: (sup (rng L)) - e < y by A14, MEASURE6:6;

consider x being object such that

A17: x in dom L and

A18: y = L . x by A15, FUNCT_1:def 3;

reconsider N1 = x as Element of NAT by A17;

set N0 = max (N1,k0);

take max (N1,k0) ; :: thesis: for m being Nat st max (N1,k0) <= m holds

|.((L . m) - (sup (rng L))).| < p

hereby :: thesis: verum

let n be Nat; :: thesis: ( max (N1,k0) <= n implies |.((L . n) - (sup (rng L))).| < p )

A19: N1 <= max (N1,k0) by XXREAL_0:25;

assume max (N1,k0) <= n ; :: thesis: |.((L . n) - (sup (rng L))).| < p

then N1 <= n by A19, XXREAL_0:2;

then L . N1 <= L . n by A1;

then (sup (rng L)) - e < L . n by A16, A18, XXREAL_0:2;

then sup (rng L) < (L . n) + e by XXREAL_3:54;

then (sup (rng L)) - (L . n) < e by XXREAL_3:55;

then - e < - ((sup (rng L)) - (L . n)) by XXREAL_3:38;

then A20: - e < (L . n) - (sup (rng L)) by XXREAL_3:26;

A21: L . n <= sup (rng L) by A2;

then sup (rng L) <= (sup (rng L)) + e by XXREAL_3:4;

then sup (rng L) < (sup (rng L)) + e by A22, XXREAL_0:1;

then L . n < (sup (rng L)) + e by A21, XXREAL_0:2;

then (L . n) - (sup (rng L)) < e by XXREAL_3:55;

hence |.((L . n) - (sup (rng L))).| < p by A20, EXTREAL1:22; :: thesis: verum

end;A19: N1 <= max (N1,k0) by XXREAL_0:25;

assume max (N1,k0) <= n ; :: thesis: |.((L . n) - (sup (rng L))).| < p

then N1 <= n by A19, XXREAL_0:2;

then L . N1 <= L . n by A1;

then (sup (rng L)) - e < L . n by A16, A18, XXREAL_0:2;

then sup (rng L) < (L . n) + e by XXREAL_3:54;

then (sup (rng L)) - (L . n) < e by XXREAL_3:55;

then - e < - ((sup (rng L)) - (L . n)) by XXREAL_3:38;

then A20: - e < (L . n) - (sup (rng L)) by XXREAL_3:26;

A21: L . n <= sup (rng L) by A2;

A22: now :: thesis: not sup (rng L) = (sup (rng L)) + e

(sup (rng L)) + 0 <= (sup (rng L)) + e
by A14, XXREAL_3:36;assume A23:
sup (rng L) = (sup (rng L)) + e
; :: thesis: contradiction

(e + (sup (rng L))) + (- (sup (rng L))) = e + ((sup (rng L)) + (- (sup (rng L)))) by A12, A11, XXREAL_3:29

.= e + 0 by XXREAL_3:7

.= e by XXREAL_3:4 ;

hence contradiction by A14, A23, XXREAL_3:7; :: thesis: verum

end;(e + (sup (rng L))) + (- (sup (rng L))) = e + ((sup (rng L)) + (- (sup (rng L)))) by A12, A11, XXREAL_3:29

.= e + 0 by XXREAL_3:7

.= e by XXREAL_3:4 ;

hence contradiction by A14, A23, XXREAL_3:7; :: thesis: verum

then sup (rng L) <= (sup (rng L)) + e by XXREAL_3:4;

then sup (rng L) < (sup (rng L)) + e by A22, XXREAL_0:1;

then L . n < (sup (rng L)) + e by A21, XXREAL_0:2;

then (L . n) - (sup (rng L)) < e by XXREAL_3:55;

hence |.((L . n) - (sup (rng L))).| < p by A20, EXTREAL1:22; :: thesis: verum

then A25: L is convergent_to_finite_number by A13;

hence L is convergent ; :: thesis: lim L = sup (rng L)

hence lim L = sup (rng L) by A13, A24, A25, Def12; :: thesis: verum

suppose A26:
for K being Real holds

( not 0 < K or ex n being Nat st not L . n < K ) ; :: thesis: ( L is convergent & lim L = sup (rng L) )

hence A29: L is convergent ; :: thesis: lim L = sup (rng L)

end;

( not 0 < K or ex n being Nat st not L . n < K ) ; :: thesis: ( L is convergent & lim L = sup (rng L) )

now :: thesis: for K being Real st 0 < K holds

ex N0 being Nat st

for n being Nat st N0 <= n holds

K <= L . n

then A28:
L is convergent_to_+infty
;ex N0 being Nat st

for n being Nat st N0 <= n holds

K <= L . n

let K be Real; :: thesis: ( 0 < K implies ex N0 being Nat st

for n being Nat st N0 <= n holds

K <= L . n )

assume 0 < K ; :: thesis: ex N0 being Nat st

for n being Nat st N0 <= n holds

K <= L . n

then consider N0 being Nat such that

A27: K <= L . N0 by A26;

for n being Nat st N0 <= n holds

K <= L . n ; :: thesis: verum

end;for n being Nat st N0 <= n holds

K <= L . n )

assume 0 < K ; :: thesis: ex N0 being Nat st

for n being Nat st N0 <= n holds

K <= L . n

then consider N0 being Nat such that

A27: K <= L . N0 by A26;

now :: thesis: for n being Nat st N0 <= n holds

K <= L . n

hence
ex N0 being Nat st K <= L . n

let n be Nat; :: thesis: ( N0 <= n implies K <= L . n )

assume N0 <= n ; :: thesis: K <= L . n

then L . N0 <= L . n by A1;

hence K <= L . n by A27, XXREAL_0:2; :: thesis: verum

end;assume N0 <= n ; :: thesis: K <= L . n

then L . N0 <= L . n by A1;

hence K <= L . n by A27, XXREAL_0:2; :: thesis: verum

for n being Nat st N0 <= n holds

K <= L . n ; :: thesis: verum

hence A29: L is convergent ; :: thesis: lim L = sup (rng L)

now :: thesis: not sup (rng L) <> +infty

hence
lim L = sup (rng L)
by A28, A29, Def12; :: thesis: verumassume A30:
sup (rng L) <> +infty
; :: thesis: contradiction

L . k0 <= sup (rng L) by A2;

then reconsider h = sup (rng L) as Element of REAL by A8, A30, XXREAL_0:14;

set K = max (0,h);

0 <= max (0,h) by XXREAL_0:25;

then consider N0 being Nat such that

A31: (max (0,h)) + 1 <= L . N0 by A26;

h + 0 < (max (0,h)) + 1 by XREAL_1:8, XXREAL_0:25;

then sup (rng L) < L . N0 by A31, XXREAL_0:2;

hence contradiction by A2; :: thesis: verum

end;L . k0 <= sup (rng L) by A2;

then reconsider h = sup (rng L) as Element of REAL by A8, A30, XXREAL_0:14;

set K = max (0,h);

0 <= max (0,h) by XXREAL_0:25;

then consider N0 being Nat such that

A31: (max (0,h)) + 1 <= L . N0 by A26;

h + 0 < (max (0,h)) + 1 by XREAL_1:8, XXREAL_0:25;

then sup (rng L) < L . N0 by A31, XXREAL_0:2;

hence contradiction by A2; :: thesis: verum