let R be non empty Subset of REAL; :: thesis: ( R is bounded_below implies ex s being Real_Sequence st
( s is non-increasing & s is convergent & rng s c= R & lim s = lower_bound R ) )
reconsider rs = lower_bound R as Real ;
defpred S1[ Nat, Real] means ( $2 in R & ( for r00 being Real st r00 = $2 holds
rs + (1 / ($1 + 1)) > r00 ) );
assume A1: R is bounded_below ; :: thesis: ex s being Real_Sequence st
( s is non-increasing & s is convergent & rng s c= R & lim s = lower_bound R )
A2: for n being Element of NAT ex r being Element of REAL st S1[n,r]
proof
let n be Element of NAT ; :: thesis: ex r being Element of REAL st S1[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 2;
for r00 being Real st r00 = r0 holds
rs + (1 / (n + 1)) > r00 by A4;
hence ex r being Element of REAL st S1[n,r] by A3; :: thesis: verum
end;
ex s1 being sequence of REAL st
for n being Element of NAT holds S1[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 S2[ 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 S2[n,x,y]
proof
let n be Nat; :: thesis: for x being set ex y being set st S2[n,x,y]
thus for x being set ex y being set st S2[n,x,y] :: thesis: verum
proof
let x be set ; :: thesis: ex y being set st S2[n,x,y]
now :: thesis: ( ( x is not Real & ex y being set st
( ( x is Real implies for r1, r2 being Real
for n1 being Nat st r1 = x & r2 = s1 . (n1 + 1) & n1 = n holds
( ( r1 >= r2 implies y = x ) & ( r1 < r2 implies y = s1 . (n1 + 1) ) ) ) & ( x is not Real implies y = 1 ) ) ) or ( x is Real & ex y being set st S2[n,x,y] ) )
per cases ( not x is Real or x is Real ) ;
case x is not Real ; :: thesis: ex y being set st
( ( x is Real implies for r1, r2 being Real
for n1 being Nat st r1 = x & r2 = s1 . (n1 + 1) & n1 = n holds
( ( r1 >= r2 implies y = x ) & ( r1 < r2 implies y = s1 . (n1 + 1) ) ) ) & ( x is not Real implies y = 1 ) )
hence ex y being set st
( ( x is Real implies for r1, r2 being Real
for n1 being Nat st r1 = x & r2 = s1 . (n1 + 1) & n1 = n holds
( ( r1 >= r2 implies y = x ) & ( r1 < r2 implies y = s1 . (n1 + 1) ) ) ) & ( x is not Real implies y = 1 ) ) ; :: thesis: verum
end;
case A7: x is Real ; :: thesis: ex y being set st S2[n,x,y]
then reconsider r10 = x as Real ;
reconsider r20 = s1 . (n + 1) as Real ;
now :: thesis: ( ( r10 <= r20 & ex y being set st S2[n,x,y] ) or ( r10 > r20 & ex y being set st S2[n,x,y] ) )
per cases ( r10 <= r20 or r10 > r20 ) ;
case r10 <= r20 ; :: thesis: ex y being set st S2[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 S2[n,x,y] by A7; :: thesis: verum
end;
case r10 > r20 ; :: thesis: ex y being set st S2[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 S2[n,x,y] by A7; :: thesis: verum
end;
end;
end;
hence ex y being set st S2[n,x,y] ; :: thesis: verum
end;
end;
end;
hence ex y being set st S2[n,x,y] ; :: thesis: verum
end;
end;
ex f being Function st
( dom f = NAT & f . 0 = s1 . 0 & ( for n being Nat holds S2[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 S2[n,s2 . n,s2 . (n + 1)] ;
A11: rng s2 c= REAL
proof
defpred S3[ 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 S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
reconsider r2 = s1 . (k + 1) as Real ;
assume A15: s2 . k in REAL ; :: thesis: S3[k + 1]
then reconsider r1 = s2 . k as Real ;
now :: thesis: ( ( r1 <= r2 & S3[k + 1] ) or ( r1 > r2 & S3[k + 1] ) )
per cases ( r1 <= r2 or r1 > r2 ) ;
case r1 <= r2 ; :: thesis: S3[k + 1]
hence S3[k + 1] by A10, A15; :: thesis: verum
end;
case r1 > r2 ; :: thesis: S3[k + 1]
then s2 . (k + 1) = s1 . (k + 1) by A10;
hence S3[k + 1] ; :: thesis: verum
end;
end;
end;
hence S3[k + 1] ; :: thesis: verum
end;
A16: S3[ 0 ] by A9;
for m being Nat holds S3[m] from NAT_1:sch 2(A16, A14);
 then s2 . n in REAL ;
hence y in REAL by A13; :: thesis: verum
end;
then reconsider s3 = s2 as Real_Sequence by A8, FUNCT_2:2;
defpred S3[ Nat] means s1 . $1 >= s3 . $1;
A17: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
A18: k in NAT by ORDINAL1:def 12;
assume s1 . k >= s3 . k ; :: thesis: S3[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;
now :: thesis: ( ( r1 <= r2 & S3[k + 1] ) or ( r1 > r2 & S3[k + 1] ) )
per cases ( r1 <= r2 or r1 > r2 ) ;
case r1 <= r2 ; :: thesis: S3[k + 1]
hence S3[k + 1] by A10; :: thesis: verum
end;
case r1 > r2 ; :: thesis: S3[k + 1]
hence S3[k + 1] by A10; :: thesis: verum
end;
end;
end;
hence S3[k + 1] ; :: thesis: verum
end;
A19: S3[ 0 ] by A9;
A20: for n4 being Nat holds S3[n4] from NAT_1:sch 2(A19, A17);
 defpred S4[ Nat] means ( 0 <= $1 implies s3 . 0 >= s3 . $1 );
A21: for n4 being Nat holds s3 . n4 >= s3 . (n4 + 1)
proof
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 ;
now :: thesis: ( ( r1 <= r2 & s3 . n4 >= s3 . (n4 + 1) ) or ( r1 > r2 & s3 . n4 >= s3 . (n4 + 1) ) )
per cases ( r1 <= r2 or r1 > r2 ) ;
case r1 <= r2 ; :: thesis: s3 . n4 >= s3 . (n4 + 1)
hence s3 . n4 >= s3 . (n4 + 1) by A10; :: thesis: verum
end;
case r1 > r2 ; :: thesis: s3 . n4 >= s3 . (n4 + 1)
hence s3 . n4 >= s3 . (n4 + 1) by A10; :: thesis: verum
end;
end;
end;
hence s3 . n4 >= s3 . (n4 + 1) ; :: thesis: verum
end;
A22: for k being Nat st S4[k] holds
S4[k + 1]
proof
let k be Nat; :: thesis: ( S4[k] implies S4[k + 1] )
assume A23: ( 0 <= k implies s3 . 0 >= s3 . k ) ; :: thesis: S4[k + 1]
now :: thesis: ( 0 <= k + 1 implies s3 . 0 >= s3 . (k + 1) )
assume 0 <= k + 1 ; :: thesis: s3 . 0 >= s3 . (k + 1)
A24: s3 . k >= s3 . (k + 1) by A21;
now :: thesis: ( ( 0 < k + 1 & s3 . 0 >= s3 . (k + 1) ) or ( 0 = k + 1 & s3 . 0 >= s3 . (k + 1) ) )
per cases ( 0 < k + 1 or 0 = k + 1 ) ;
case 0 < k + 1 ; :: thesis: s3 . 0 >= s3 . (k + 1)
thus s3 . 0 >= s3 . (k + 1) by A23, A24, XXREAL_0:2; :: thesis: verum
end;
case 0 = k + 1 ; :: thesis: s3 . 0 >= s3 . (k + 1)
hence s3 . 0 >= s3 . (k + 1) ; :: thesis: verum
end;
end;
end;
hence s3 . 0 >= s3 . (k + 1) ; :: thesis: verum
end;
hence S4[k + 1] ; :: thesis: verum
end;
defpred S5[ Nat] means for n4 being Nat st $1 <= n4 holds
s3 . $1 >= s3 . n4;
A25: for k being Nat st S5[k] holds
S5[k + 1]
proof
let k be Nat; :: thesis: ( S5[k] implies S5[k + 1] )
assume for n5 being Nat st k <= n5 holds
s3 . k >= s3 . n5 ; :: thesis: S5[k + 1]
defpred S6[ Nat] means ( k + 1 <= $1 implies s3 . (k + 1) >= s3 . $1 );
A26: for i being Nat st S6[i] holds
S6[i + 1]
proof
let i be Nat; :: thesis: ( S6[i] implies S6[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;
A28: now :: thesis: ( ( r1 <= r2 & s3 . i >= s3 . (i + 1) ) or ( r1 > r2 & s3 . i >= s3 . (i + 1) ) )
per cases ( r1 <= r2 or r1 > r2 ) ;
case r1 <= r2 ; :: thesis: s3 . i >= s3 . (i + 1)
hence s3 . i >= s3 . (i + 1) by A10; :: thesis: verum
end;
case r1 > r2 ; :: thesis: s3 . i >= s3 . (i + 1)
hence s3 . i >= s3 . (i + 1) by A10; :: thesis: verum
end;
end;
end;
assume A29: ( k + 1 <= i implies s3 . (k + 1) >= s3 . i ) ; :: thesis: S6[i + 1]
now :: thesis: ( k + 1 <= i + 1 implies s3 . (k + 1) >= s3 . (i + 1) )
assume A30: k + 1 <= i + 1 ; :: thesis: s3 . (k + 1) >= s3 . (i + 1)
now :: thesis: ( ( k + 1 < i + 1 & s3 . (k + 1) >= s3 . (i + 1) ) or ( k + 1 = i + 1 & s3 . (k + 1) >= s3 . (i + 1) ) )
per cases ( k + 1 < i + 1 or k + 1 = i + 1 ) by A30, XXREAL_0:1;
case k + 1 < i + 1 ; :: thesis: s3 . (k + 1) >= s3 . (i + 1)
hence s3 . (k + 1) >= s3 . (i + 1) by A29, A28, NAT_1:13, XXREAL_0:2; :: thesis: verum
end;
case k + 1 = i + 1 ; :: thesis: s3 . (k + 1) >= s3 . (i + 1)
hence s3 . (k + 1) >= s3 . (i + 1) ; :: thesis: verum
end;
end;
end;
hence s3 . (k + 1) >= s3 . (i + 1) ; :: thesis: verum
end;
hence S6[i + 1] ; :: thesis: verum
end;
A31: S6[ 0 ] ;
thus for n4 being Nat holds S6[n4] from NAT_1:sch 2(A31, A26); :: thesis: verum
end;
A32: S4[ 0 ] ;
for n4 being Nat holds S4[n4] from NAT_1:sch 2(A32, A22);
 then A33: S5[ 0 ] ;
for m4 being Nat holds S5[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-increasing by SEQM_3:def 4;
A35: rng s3 c= R
proof
defpred S6[ Nat] 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 S6[k] holds
S6[k + 1]
proof
let k be Nat; :: thesis: ( S6[k] implies S6[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: S6[k + 1]
now :: thesis: ( ( r1 <= r2 & S6[k + 1] ) or ( r1 > r2 & S6[k + 1] ) )
per cases ( r1 <= r2 or r1 > r2 ) ;
case r1 <= r2 ; :: thesis: S6[k + 1]
hence S6[k + 1] by A10, A39; :: thesis: verum
end;
case r1 > r2 ; :: thesis: S6[k + 1]
then s2 . (k + 1) = s1 . (k + 1) by A10;
hence S6[k + 1] by A5; :: thesis: verum
end;
end;
end;
hence S6[k + 1] ; :: thesis: verum
end;
A40: S6[ 0 ] by A5, A9;
for nn being Nat holds S6[nn] from NAT_1:sch 2(A40, A37);
 hence y in R by A36; :: thesis: verum
end;
for n being Nat holds s3 . n > (lower_bound R) - 1
proof
let n be Nat; :: thesis: s3 . n > (lower_bound R) - 1
A41: n in NAT by ORDINAL1:def 12;
lower_bound R < (lower_bound R) + 1 by XREAL_1:29;
then A42: lower_bound R > (lower_bound R) - 1 by XREAL_1:19;
s3 . n in rng s3 by A8, FUNCT_1:def 3, A41;
then s3 . n >= lower_bound R by A1, A35, SEQ_4:def 2;
hence s3 . n > (lower_bound R) - 1 by A42, XXREAL_0:2; :: thesis: verum
end;
then A43: s3 is bounded_below by SEQ_2:def 4;
A44: for r being Real st r > 0 holds
(lower_bound R) + r > lim s3
proof
let r be Real; :: thesis: ( r > 0 implies (lower_bound R) + r > lim s3 )
assume A45: r > 0 ; :: thesis: (lower_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:8;
then A48: rs + r > s1 . n2 by A5, XXREAL_0:2, A47;
A49: s3 . n2 >= lim s3 by A34, A43, SEQ_4:38;
s1 . n2 >= s3 . n2 by A20;
then rs + r > s3 . n2 by A48, XXREAL_0:2;
hence (lower_bound R) + r > lim s3 by A49, XXREAL_0:2; :: thesis: verum
end;
A50: now :: thesis: not lower_bound R < lim s3
reconsider r = (lim s3) - (lower_bound R) as Real ;
assume lower_bound R < lim s3 ; :: thesis: contradiction
then r > 0 by XREAL_1:50;
then (lower_bound R) + ((lim s3) + (- (lower_bound R))) > lim s3 by A44;
hence contradiction ; :: thesis: verum
end;
A51: for n being Nat holds s3 . n >= lower_bound R
proof
let n be Nat; :: thesis: s3 . n >= lower_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 >= lower_bound R by A1, A35, SEQ_4:def 2; :: thesis: verum
end;
for n being Nat holds s3 . n > (lower_bound R) - 1
proof
let n be Nat; :: thesis: s3 . n > (lower_bound R) - 1
lower_bound R < (lower_bound R) + 1 by XREAL_1:29;
then A53: lower_bound R > (lower_bound R) - 1 by XREAL_1:19;
s3 . n >= lower_bound R by A51;
hence s3 . n > (lower_bound R) - 1 by A53, XXREAL_0:2; :: thesis: verum
end;
then A54: s3 is bounded_below by SEQ_2:def 4;
then lim s3 >= lower_bound R by A34, A51, PREPOWER:1;
hence ex s being Real_Sequence st
( s is non-increasing & s is convergent & rng s c= R & lim s = lower_bound R ) by A34, A35, A54, A50, XXREAL_0:1; :: thesis: verum