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