let R be non empty Subset of REAL; :: thesis: ( R is bounded_above implies ex s being Real_Sequence st

( s is non-decreasing & s is convergent & rng s c= R & lim s = upper_bound R ) )

reconsider rs = upper_bound R as Real ;

defpred S_{1}[ Nat, Real] means ( $2 in R & ( for r00 being Real st r00 = $2 holds

rs - (1 / ($1 + 1)) < r00 ) );

assume A1: R is bounded_above ; :: thesis: ex s being Real_Sequence st

( s is non-decreasing & s is convergent & rng s c= R & lim s = upper_bound R )

A2: for n being Element of NAT ex r being Element of REAL st S_{1}[n,r]

for n being Element of NAT holds S_{1}[n,s1 . n]
from FUNCT_2:sch 3(A2);

then consider s1 being sequence of REAL such that

A5: for n being Element of NAT holds

( s1 . n in R & ( for r0 being Real st r0 = s1 . n holds

rs - (1 / (n + 1)) < r0 ) ) ;

defpred S_{2}[ set , set , set ] means ( ( $2 is Real implies for r1, r2 being Real

for n1 being Nat st r1 = $2 & r2 = s1 . (n1 + 1) & n1 = $1 holds

( ( r1 >= r2 implies $3 = $2 ) & ( r1 < r2 implies $3 = s1 . (n1 + 1) ) ) ) & ( $2 is not Real implies $3 = 1 ) );

A6: for n being Nat

for x being set ex y being set st S_{2}[n,x,y]

( dom f = NAT & f . 0 = s1 . 0 & ( for n being Nat holds S_{2}[n,f . n,f . (n + 1)] ) )
from RECDEF_1:sch 1(A6);

then consider s2 being Function such that

A8: dom s2 = NAT and

A9: s2 . 0 = s1 . 0 and

A10: for n being Nat holds S_{2}[n,s2 . n,s2 . (n + 1)]
;

A11: rng s2 c= REAL

defpred S_{3}[ Nat] means s1 . $1 <= s3 . $1;

A17: for k being Nat st S_{3}[k] holds

S_{3}[k + 1]
_{3}[ 0 ]
by A9;

A20: for n4 being Nat holds S_{3}[n4]
from NAT_1:sch 2(A19, A17);

defpred S_{4}[ Nat] means ( 0 <= $1 implies s3 . 0 <= s3 . $1 );

A21: for n4 being Nat holds s3 . n4 <= s3 . (n4 + 1)_{4}[k] holds

S_{4}[k + 1]
_{5}[ Nat] means for n4 being Nat st $1 <= n4 holds

s3 . $1 <= s3 . n4;

A25: for k being Nat st S_{5}[k] holds

S_{5}[k + 1]
_{4}[ 0 ]
;

for n4 being Nat holds S_{4}[n4]
from NAT_1:sch 2(A32, A22);

then A33: S_{5}[ 0 ]
;

for m4 being Nat holds S_{5}[m4]
from NAT_1:sch 2(A33, A25);

then for m4, n4 being Nat st m4 in dom s3 & n4 in dom s3 & m4 <= n4 holds

s3 . m4 <= s3 . n4 ;

then A34: s3 is non-decreasing by SEQM_3:def 3;

A35: rng s3 c= R

A44: for r being Real st r > 0 holds

(upper_bound R) - r < lim s3

then lim s3 <= upper_bound R by A34, A51, PREPOWER:2;

hence ex s being Real_Sequence st

( s is non-decreasing & s is convergent & rng s c= R & lim s = upper_bound R ) by A34, A35, A53, A50, XXREAL_0:1; :: thesis: verum

( s is non-decreasing & s is convergent & rng s c= R & lim s = upper_bound R ) )

reconsider rs = upper_bound R as Real ;

defpred S

rs - (1 / ($1 + 1)) < r00 ) );

assume A1: R is bounded_above ; :: thesis: ex s being Real_Sequence st

( s is non-decreasing & s is convergent & rng s c= R & lim s = upper_bound R )

A2: for n being Element of NAT ex r being Element of REAL st S

proof

ex s1 being sequence of REAL st
let n be Element of NAT ; :: thesis: ex r being Element of REAL st S_{1}[n,r]

(n + 1) " > 0 ;

then 1 / (n + 1) > 0 by XCMPLX_1:215;

then consider r0 being Real such that

A3: r0 in R and

A4: rs - (1 / (n + 1)) < r0 by A1, SEQ_4:def 1;

for r00 being Real st r00 = r0 holds

rs - (1 / (n + 1)) < r00 by A4;

hence ex r being Element of REAL st S_{1}[n,r]
by A3; :: thesis: verum

end;(n + 1) " > 0 ;

then 1 / (n + 1) > 0 by XCMPLX_1:215;

then consider r0 being Real such that

A3: r0 in R and

A4: rs - (1 / (n + 1)) < r0 by A1, SEQ_4:def 1;

for r00 being Real st r00 = r0 holds

rs - (1 / (n + 1)) < r00 by A4;

hence ex r being Element of REAL st S

for n being Element of NAT holds S

then consider s1 being sequence of REAL such that

A5: for n being Element of NAT holds

( s1 . n in R & ( for r0 being Real st r0 = s1 . n holds

rs - (1 / (n + 1)) < r0 ) ) ;

defpred S

for n1 being Nat st r1 = $2 & r2 = s1 . (n1 + 1) & n1 = $1 holds

( ( r1 >= r2 implies $3 = $2 ) & ( r1 < r2 implies $3 = s1 . (n1 + 1) ) ) ) & ( $2 is not Real implies $3 = 1 ) );

A6: for n being Nat

for x being set ex y being set st S

proof

ex f being Function st
let n be Nat; :: thesis: for x being set ex y being set st S_{2}[n,x,y]

thus for x being set ex y being set st S_{2}[n,x,y]
:: thesis: verum

end;thus for x being set ex y being set st S

proof

let x be set ; :: thesis: ex y being set st S_{2}[n,x,y]

_{2}[n,x,y]
; :: thesis: verum

end;now :: thesis: ( ( x is not Real & ex y being set st S_{2}[n,x,y] ) or ( x is Real & ex y being set st S_{2}[n,x,y] ) )end;

hence
ex y being set st Sper cases
( not x is Real or x is Real )
;

end;

case A7:
x is Real
; :: thesis: ex y being set st S_{2}[n,x,y]

then reconsider r10 = x as Real ;

reconsider r20 = s1 . (n + 1) as Real ;

_{2}[n,x,y]
; :: thesis: verum

end;reconsider r20 = s1 . (n + 1) as Real ;

now :: thesis: ( ( r10 >= r20 & ex y being set st S_{2}[n,x,y] ) or ( r10 < r20 & ex y being set st S_{2}[n,x,y] ) )end;

hence
ex y being set st Sper cases
( r10 >= r20 or r10 < r20 )
;

end;

case
r10 >= r20
; :: thesis: ex y being set st S_{2}[n,x,y]

then
for r1, r2 being Real

for n1 being Nat st r1 = x & r2 = s1 . (n1 + 1) & n1 = n holds

( ( r1 >= r2 implies x = x ) & ( r1 < r2 implies x = s1 . (n1 + 1) ) ) ;

hence ex y being set st S_{2}[n,x,y]
by A7; :: thesis: verum

end;for n1 being Nat st r1 = x & r2 = s1 . (n1 + 1) & n1 = n holds

( ( r1 >= r2 implies x = x ) & ( r1 < r2 implies x = s1 . (n1 + 1) ) ) ;

hence ex y being set st S

case
r10 < r20
; :: thesis: ex y being set st S_{2}[n,x,y]

then
for r1, r2 being Real

for n1 being Nat st r1 = x & r2 = s1 . (n1 + 1) & n1 = n holds

( ( r1 >= r2 implies s1 . (n + 1) = x ) & ( r1 < r2 implies s1 . (n + 1) = s1 . (n1 + 1) ) ) ;

hence ex y being set st S_{2}[n,x,y]
by A7; :: thesis: verum

end;for n1 being Nat st r1 = x & r2 = s1 . (n1 + 1) & n1 = n holds

( ( r1 >= r2 implies s1 . (n + 1) = x ) & ( r1 < r2 implies s1 . (n + 1) = s1 . (n1 + 1) ) ) ;

hence ex y being set st S

( dom f = NAT & f . 0 = s1 . 0 & ( for n being Nat holds S

then consider s2 being Function such that

A8: dom s2 = NAT and

A9: s2 . 0 = s1 . 0 and

A10: for n being Nat holds S

A11: rng s2 c= REAL

proof

then reconsider s3 = s2 as Real_Sequence by A8, FUNCT_2:2;
defpred S_{3}[ Nat] means s2 . $1 in REAL ;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s2 or y in REAL )

assume y in rng s2 ; :: thesis: y in REAL

then consider x being object such that

A12: x in dom s2 and

A13: y = s2 . x by FUNCT_1:def 3;

reconsider n = x as Nat by A8, A12;

A14: for k being Nat st S_{3}[k] holds

S_{3}[k + 1]
_{3}[ 0 ]
by A9;

for m being Nat holds S_{3}[m]
from NAT_1:sch 2(A16, A14);

then s2 . n in REAL ;

hence y in REAL by A13; :: thesis: verum

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s2 or y in REAL )

assume y in rng s2 ; :: thesis: y in REAL

then consider x being object such that

A12: x in dom s2 and

A13: y = s2 . x by FUNCT_1:def 3;

reconsider n = x as Nat by A8, A12;

A14: for k being Nat st S

S

proof

A16:
S
let k be Nat; :: thesis: ( S_{3}[k] implies S_{3}[k + 1] )

reconsider r2 = s1 . (k + 1) as Real ;

assume A15: s2 . k in REAL ; :: thesis: S_{3}[k + 1]

then reconsider r1 = s2 . k as Real ;

hence S_{3}[k + 1]
; :: thesis: verum

end;reconsider r2 = s1 . (k + 1) as Real ;

assume A15: s2 . k in REAL ; :: thesis: S

then reconsider r1 = s2 . k as Real ;

hence S

for m being Nat holds S

then s2 . n in REAL ;

hence y in REAL by A13; :: thesis: verum

defpred S

A17: for k being Nat st S

S

proof

A19:
S
let k be Nat; :: thesis: ( S_{3}[k] implies S_{3}[k + 1] )

A18: k in NAT by ORDINAL1:def 12;

assume s1 . k <= s3 . k ; :: thesis: S_{3}[k + 1]

reconsider r2 = s1 . (k + 1) as Real ;

s2 . k in rng s2 by A8, FUNCT_1:def 3, A18;

then reconsider r1 = s2 . k as Real by A11;

hence S_{3}[k + 1]
; :: thesis: verum

end;A18: k in NAT by ORDINAL1:def 12;

assume s1 . k <= s3 . k ; :: thesis: S

reconsider r2 = s1 . (k + 1) as Real ;

s2 . k in rng s2 by A8, FUNCT_1:def 3, A18;

then reconsider r1 = s2 . k as Real by A11;

hence S

A20: for n4 being Nat holds S

defpred S

A21: for n4 being Nat holds s3 . n4 <= s3 . (n4 + 1)

proof

A22:
for k being Nat st S
let n4 be Nat; :: thesis: s3 . n4 <= s3 . (n4 + 1)

reconsider r2 = s1 . (n4 + 1) as Real ;

dom s3 = NAT by FUNCT_2:def 1;

then reconsider r1 = s2 . n4 as Real ;

end;reconsider r2 = s1 . (n4 + 1) as Real ;

dom s3 = NAT by FUNCT_2:def 1;

then reconsider r1 = s2 . n4 as Real ;

now :: thesis: ( ( r1 >= r2 & s3 . n4 <= s3 . (n4 + 1) ) or ( r1 < r2 & s3 . n4 <= s3 . (n4 + 1) ) )

hence
s3 . n4 <= s3 . (n4 + 1)
; :: thesis: verumend;

S

proof

defpred S
let k be Nat; :: thesis: ( S_{4}[k] implies S_{4}[k + 1] )

assume A23: ( 0 <= k implies s3 . 0 <= s3 . k ) ; :: thesis: S_{4}[k + 1]

_{4}[k + 1]
; :: thesis: verum

end;assume A23: ( 0 <= k implies s3 . 0 <= s3 . k ) ; :: thesis: S

now :: thesis: ( 0 <= k + 1 implies s3 . 0 <= s3 . (k + 1) )

hence
Sassume
0 <= k + 1
; :: thesis: s3 . 0 <= s3 . (k + 1)

A24: s3 . k <= s3 . (k + 1) by A21;

hence s3 . 0 <= s3 . (k + 1) ; :: thesis: verum

end;A24: s3 . k <= s3 . (k + 1) by A21;

hence s3 . 0 <= s3 . (k + 1) ; :: thesis: verum

s3 . $1 <= s3 . n4;

A25: for k being Nat st S

S

proof

A32:
S
let k be Nat; :: thesis: ( S_{5}[k] implies S_{5}[k + 1] )

assume for n5 being Nat st k <= n5 holds

s3 . k <= s3 . n5 ; :: thesis: S_{5}[k + 1]

defpred S_{6}[ Nat] means ( k + 1 <= $1 implies s3 . (k + 1) <= s3 . $1 );

A26: for i being Nat st S_{6}[i] holds

S_{6}[i + 1]
_{6}[ 0 ]
;

for n4 being Nat holds S_{6}[n4]
from NAT_1:sch 2(A31, A26);

hence S_{5}[k + 1]
; :: thesis: verum

end;assume for n5 being Nat st k <= n5 holds

s3 . k <= s3 . n5 ; :: thesis: S

defpred S

A26: for i being Nat st S

S

proof

A31:
S
let i be Nat; :: thesis: ( S_{6}[i] implies S_{6}[i + 1] )

A27: i in NAT by ORDINAL1:def 12;

reconsider r2 = s1 . (i + 1) as Real ;

s2 . i in rng s2 by A8, FUNCT_1:def 3, A27;

then reconsider r1 = s2 . i as Real by A11;

_{6}[i + 1]

_{6}[i + 1]
; :: thesis: verum

end;A27: i in NAT by ORDINAL1:def 12;

reconsider r2 = s1 . (i + 1) as Real ;

s2 . i in rng s2 by A8, FUNCT_1:def 3, A27;

then reconsider r1 = s2 . i as Real by A11;

A28: now :: thesis: ( ( r1 >= r2 & s3 . i <= s3 . (i + 1) ) or ( r1 < r2 & s3 . i <= s3 . (i + 1) ) )

assume A29:
( k + 1 <= i implies s3 . (k + 1) <= s3 . i )
; :: thesis: Send;

now :: thesis: ( k + 1 <= i + 1 implies s3 . (k + 1) <= s3 . (i + 1) )

hence
Sassume A30:
k + 1 <= i + 1
; :: thesis: s3 . (k + 1) <= s3 . (i + 1)

end;now :: thesis: ( ( k + 1 < i + 1 & s3 . (k + 1) <= s3 . (i + 1) ) or ( k + 1 = i + 1 & s3 . (k + 1) <= s3 . (i + 1) ) )

hence
s3 . (k + 1) <= s3 . (i + 1)
; :: thesis: verumend;

for n4 being Nat holds S

hence S

for n4 being Nat holds S

then A33: S

for m4 being Nat holds S

then for m4, n4 being Nat st m4 in dom s3 & n4 in dom s3 & m4 <= n4 holds

s3 . m4 <= s3 . n4 ;

then A34: s3 is non-decreasing by SEQM_3:def 3;

A35: rng s3 c= R

proof

for n being Nat holds s3 . n < (upper_bound R) + 1
defpred S_{6}[ set ] means s3 . $1 in R;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s3 or y in R )

assume y in rng s3 ; :: thesis: y in R

then A36: ex x being object st

( x in dom s3 & y = s3 . x ) by FUNCT_1:def 3;

A37: for k being Nat st S_{6}[k] holds

S_{6}[k + 1]
_{6}[ 0 ]
by A5, A9;

for nn being Nat holds S_{6}[nn]
from NAT_1:sch 2(A40, A37);

hence y in R by A36; :: thesis: verum

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s3 or y in R )

assume y in rng s3 ; :: thesis: y in R

then A36: ex x being object st

( x in dom s3 & y = s3 . x ) by FUNCT_1:def 3;

A37: for k being Nat st S

S

proof

A40:
S
let k be Nat; :: thesis: ( S_{6}[k] implies S_{6}[k + 1] )

A38: k in NAT by ORDINAL1:def 12;

reconsider r2 = s1 . (k + 1) as Real ;

s2 . k in rng s2 by A8, FUNCT_1:def 3, A38;

then reconsider r1 = s2 . k as Real by A11;

assume A39: s3 . k in R ; :: thesis: S_{6}[k + 1]

hence S_{6}[k + 1]
; :: thesis: verum

end;A38: k in NAT by ORDINAL1:def 12;

reconsider r2 = s1 . (k + 1) as Real ;

s2 . k in rng s2 by A8, FUNCT_1:def 3, A38;

then reconsider r1 = s2 . k as Real by A11;

assume A39: s3 . k in R ; :: thesis: S

hence S

for nn being Nat holds S

hence y in R by A36; :: thesis: verum

proof

then A43:
s3 is bounded_above
by SEQ_2:def 3;
let n be Nat; :: thesis: s3 . n < (upper_bound R) + 1

A41: n in NAT by ORDINAL1:def 12;

s3 . n in rng s3 by A8, FUNCT_1:def 3, A41;

then A42: s3 . n <= upper_bound R by A1, A35, SEQ_4:def 1;

upper_bound R < (upper_bound R) + 1 by XREAL_1:29;

hence s3 . n < (upper_bound R) + 1 by A42, XXREAL_0:2; :: thesis: verum

end;A41: n in NAT by ORDINAL1:def 12;

s3 . n in rng s3 by A8, FUNCT_1:def 3, A41;

then A42: s3 . n <= upper_bound R by A1, A35, SEQ_4:def 1;

upper_bound R < (upper_bound R) + 1 by XREAL_1:29;

hence s3 . n < (upper_bound R) + 1 by A42, XXREAL_0:2; :: thesis: verum

A44: for r being Real st r > 0 holds

(upper_bound R) - r < lim s3

proof

let r be Real; :: thesis: ( r > 0 implies (upper_bound R) - r < lim s3 )

assume A45: r > 0 ; :: thesis: (upper_bound R) - r < lim s3

consider n2 being Nat such that

A46: 1 / r < n2 by SEQ_4:3;

A47: n2 in NAT by ORDINAL1:def 12;

n2 < n2 + 1 by XREAL_1:29;

then 1 / r < n2 + 1 by A46, XXREAL_0:2;

then (1 / r) * r < (n2 + 1) * r by A45, XREAL_1:68;

then 1 < (n2 + 1) * r by A45, XCMPLX_1:106;

then 1 / (n2 + 1) < ((n2 + 1) * r) / (n2 + 1) by XREAL_1:74;

then 1 / (n2 + 1) < r by XCMPLX_1:89;

then rs - (1 / (n2 + 1)) > rs - r by XREAL_1:10;

then A48: rs - r < s1 . n2 by A5, XXREAL_0:2, A47;

A49: s3 . n2 <= lim s3 by A34, A43, SEQ_4:37;

s1 . n2 <= s3 . n2 by A20;

then rs - r < s3 . n2 by A48, XXREAL_0:2;

hence (upper_bound R) - r < lim s3 by A49, XXREAL_0:2; :: thesis: verum

end;assume A45: r > 0 ; :: thesis: (upper_bound R) - r < lim s3

consider n2 being Nat such that

A46: 1 / r < n2 by SEQ_4:3;

A47: n2 in NAT by ORDINAL1:def 12;

n2 < n2 + 1 by XREAL_1:29;

then 1 / r < n2 + 1 by A46, XXREAL_0:2;

then (1 / r) * r < (n2 + 1) * r by A45, XREAL_1:68;

then 1 < (n2 + 1) * r by A45, XCMPLX_1:106;

then 1 / (n2 + 1) < ((n2 + 1) * r) / (n2 + 1) by XREAL_1:74;

then 1 / (n2 + 1) < r by XCMPLX_1:89;

then rs - (1 / (n2 + 1)) > rs - r by XREAL_1:10;

then A48: rs - r < s1 . n2 by A5, XXREAL_0:2, A47;

A49: s3 . n2 <= lim s3 by A34, A43, SEQ_4:37;

s1 . n2 <= s3 . n2 by A20;

then rs - r < s3 . n2 by A48, XXREAL_0:2;

hence (upper_bound R) - r < lim s3 by A49, XXREAL_0:2; :: thesis: verum

A50: now :: thesis: not upper_bound R > lim s3

A51:
for n being Nat holds s3 . n <= upper_bound R
reconsider r = (upper_bound R) - (lim s3) as Real ;

assume upper_bound R > lim s3 ; :: thesis: contradiction

then r > 0 by XREAL_1:50;

then (upper_bound R) - r < lim s3 by A44;

hence contradiction ; :: thesis: verum

end;assume upper_bound R > lim s3 ; :: thesis: contradiction

then r > 0 by XREAL_1:50;

then (upper_bound R) - r < lim s3 by A44;

hence contradiction ; :: thesis: verum

proof

for n being Nat holds s3 . n < (upper_bound R) + 1
let n be Nat; :: thesis: s3 . n <= upper_bound R

A52: n in NAT by ORDINAL1:def 12;

dom s3 = NAT by FUNCT_2:def 1;

then s3 . n in rng s3 by FUNCT_1:def 3, A52;

hence s3 . n <= upper_bound R by A1, A35, SEQ_4:def 1; :: thesis: verum

end;A52: n in NAT by ORDINAL1:def 12;

dom s3 = NAT by FUNCT_2:def 1;

then s3 . n in rng s3 by FUNCT_1:def 3, A52;

hence s3 . n <= upper_bound R by A1, A35, SEQ_4:def 1; :: thesis: verum

proof

then A53:
s3 is bounded_above
by SEQ_2:def 3;
let n be Nat; :: thesis: s3 . n < (upper_bound R) + 1

( upper_bound R < (upper_bound R) + 1 & s3 . n <= upper_bound R ) by A51, XREAL_1:29;

hence s3 . n < (upper_bound R) + 1 by XXREAL_0:2; :: thesis: verum

end;( upper_bound R < (upper_bound R) + 1 & s3 . n <= upper_bound R ) by A51, XREAL_1:29;

hence s3 . n < (upper_bound R) + 1 by XXREAL_0:2; :: thesis: verum

then lim s3 <= upper_bound R by A34, A51, PREPOWER:2;

hence ex s being Real_Sequence st

( s is non-decreasing & s is convergent & rng s c= R & lim s = upper_bound R ) by A34, A35, A53, A50, XXREAL_0:1; :: thesis: verum