let L be ExtREAL_sequence; :: thesis: for c being ExtReal st ( for n being Nat holds L . n = c ) holds

( L is convergent & lim L = c & lim L = sup (rng L) )

let c be ExtReal; :: thesis: ( ( for n being Nat holds L . n = c ) implies ( L is convergent & lim L = c & lim L = sup (rng L) ) )

reconsider cc = c as R_eal by XXREAL_0:def 1;

A1: dom L = NAT by FUNCT_2:def 1;

c in ExtREAL by XXREAL_0:def 1;

then A2: ( c in REAL or c in {-infty,+infty} ) by XBOOLE_0:def 3, XXREAL_0:def 4;

assume A3: for n being Nat holds L . n = c ; :: thesis: ( L is convergent & lim L = c & lim L = sup (rng L) )

then A4: L . 1 = c ;

( L is convergent & lim L = c & lim L = sup (rng L) )

let c be ExtReal; :: thesis: ( ( for n being Nat holds L . n = c ) implies ( L is convergent & lim L = c & lim L = sup (rng L) ) )

reconsider cc = c as R_eal by XXREAL_0:def 1;

A1: dom L = NAT by FUNCT_2:def 1;

c in ExtREAL by XXREAL_0:def 1;

then A2: ( c in REAL or c in {-infty,+infty} ) by XBOOLE_0:def 3, XXREAL_0:def 4;

assume A3: for n being Nat holds L . n = c ; :: thesis: ( L is convergent & lim L = c & lim L = sup (rng L) )

then A4: L . 1 = c ;

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

v <= c

then A5:
c is UpperBound of rng L
by XXREAL_2:def 1;v <= c

let v be ExtReal; :: thesis: ( v in rng L implies v <= c )

assume v in rng L ; :: thesis: v <= c

then ex n being object st

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

hence v <= c by A3; :: thesis: verum

end;assume v in rng L ; :: thesis: v <= c

then ex n being object st

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

hence v <= c by A3; :: thesis: verum

per cases
( c in REAL or c = -infty or c = +infty )
by A2, TARSKI:def 2;

end;

suppose
c in REAL
; :: thesis: ( L is convergent & lim L = c & lim L = sup (rng L) )

then reconsider rc = c as Real ;

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

then lim L = cc by A6, A8, Def12;

hence lim L = c ; :: thesis: lim L = sup (rng L)

hence lim L = sup (rng L) by A5, A1, A4, FUNCT_1:3, XXREAL_2:55; :: thesis: verum

end;A6: now :: thesis: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((L . m) - rc).| < p

then A8:
L is convergent_to_finite_number
;ex n being Nat st

for m being Nat st n <= m holds

|.((L . m) - rc).| < p

reconsider n = 0 as Nat ;

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st

for m being Nat st n <= m holds

|.((L . m) - rc).| < p )

assume A7: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((L . m) - rc).| < p

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

|.((L . m) - rc).| < p

let m be Nat; :: thesis: ( n <= m implies |.((L . m) - rc).| < p )

assume n <= m ; :: thesis: |.((L . m) - rc).| < p

(L . m) - rc = (L . m) - (L . m) by A3;

then (L . m) - rc = 0 by XXREAL_3:7;

hence |.((L . m) - rc).| < p by A7, EXTREAL1:16; :: thesis: verum

end;let p be Real; :: thesis: ( 0 < p implies ex n being Nat st

for m being Nat st n <= m holds

|.((L . m) - rc).| < p )

assume A7: 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((L . m) - rc).| < p

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

|.((L . m) - rc).| < p

let m be Nat; :: thesis: ( n <= m implies |.((L . m) - rc).| < p )

assume n <= m ; :: thesis: |.((L . m) - rc).| < p

(L . m) - rc = (L . m) - (L . m) by A3;

then (L . m) - rc = 0 by XXREAL_3:7;

hence |.((L . m) - rc).| < p by A7, EXTREAL1:16; :: thesis: verum

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

then lim L = cc by A6, A8, Def12;

hence lim L = c ; :: thesis: lim L = sup (rng L)

hence lim L = sup (rng L) by A5, A1, A4, FUNCT_1:3, XXREAL_2:55; :: thesis: verum

suppose A9:
c = -infty
; :: thesis: ( L is convergent & lim L = c & lim L = sup (rng L) )

for p being Real st p < 0 holds

ex n being Nat st

for m being Nat st n <= m holds

L . m <= p

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

hence lim L = c by A9, A11, Def12; :: thesis: lim L = sup (rng L)

hence lim L = sup (rng L) by A5, A1, A4, FUNCT_1:3, XXREAL_2:55; :: thesis: verum

end;ex n being Nat st

for m being Nat st n <= m holds

L . m <= p

proof

then A11:
L is convergent_to_-infty
;
let p be Real; :: thesis: ( p < 0 implies ex n being Nat st

for m being Nat st n <= m holds

L . m <= p )

assume p < 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

L . m <= p

take 0 ; :: thesis: for m being Nat st 0 <= m holds

L . m <= p

A10: p in REAL by XREAL_0:def 1;

L . m <= p ; :: thesis: verum

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

L . m <= p )

assume p < 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

L . m <= p

take 0 ; :: thesis: for m being Nat st 0 <= m holds

L . m <= p

A10: p in REAL by XREAL_0:def 1;

now :: thesis: for m being Nat st 0 <= m holds

L . m < p

hence
for m being Nat st 0 <= m holds L . m < p

let m be Nat; :: thesis: ( 0 <= m implies L . m < p )

assume 0 <= m ; :: thesis: L . m < p

L . m = -infty by A3, A9;

hence L . m < p by A10, XXREAL_0:12; :: thesis: verum

end;assume 0 <= m ; :: thesis: L . m < p

L . m = -infty by A3, A9;

hence L . m < p by A10, XXREAL_0:12; :: thesis: verum

L . m <= p ; :: thesis: verum

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

hence lim L = c by A9, A11, Def12; :: thesis: lim L = sup (rng L)

hence lim L = sup (rng L) by A5, A1, A4, FUNCT_1:3, XXREAL_2:55; :: thesis: verum

suppose A12:
c = +infty
; :: thesis: ( L is convergent & lim L = c & lim L = sup (rng L) )

for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

p <= L . m

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

hence lim L = c by A12, A14, Def12; :: thesis: lim L = sup (rng L)

hence lim L = sup (rng L) by A5, A1, A4, FUNCT_1:3, XXREAL_2:55; :: thesis: verum

end;ex n being Nat st

for m being Nat st n <= m holds

p <= L . m

proof

then A14:
L is convergent_to_+infty
;
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st

for m being Nat st n <= m holds

p <= L . m )

assume 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

p <= L . m

take 0 ; :: thesis: for m being Nat st 0 <= m holds

p <= L . m

A13: p in REAL by XREAL_0:def 1;

p <= L . m ; :: thesis: verum

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

p <= L . m )

assume 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

p <= L . m

take 0 ; :: thesis: for m being Nat st 0 <= m holds

p <= L . m

A13: p in REAL by XREAL_0:def 1;

now :: thesis: for m being Nat st 0 <= m holds

p < L . m

hence
for m being Nat st 0 <= m holds p < L . m

let m be Nat; :: thesis: ( 0 <= m implies p < L . m )

assume 0 <= m ; :: thesis: p < L . m

L . m = +infty by A3, A12;

hence p < L . m by A13, XXREAL_0:9; :: thesis: verum

end;assume 0 <= m ; :: thesis: p < L . m

L . m = +infty by A3, A12;

hence p < L . m by A13, XXREAL_0:9; :: thesis: verum

p <= L . m ; :: thesis: verum

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

hence lim L = c by A12, A14, Def12; :: thesis: lim L = sup (rng L)

hence lim L = sup (rng L) by A5, A1, A4, FUNCT_1:3, XXREAL_2:55; :: thesis: verum