let R be non empty Subset of REAL; ( 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 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_above
; 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 S1[n,r]
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;
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]
verumproof
let x be
set ;
ex y being set st S2[n,x,y]
now ( ( x is not Real & ex y being set st S2[n,x,y] ) 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
;
ex y being set st S2[n,x,y]hence
ex
y being
set st
S2[
n,
x,
y]
;
verum end; case A7:
x is
Real
;
ex y being set st S2[n,x,y]then reconsider r10 =
x as
Real ;
reconsider r20 =
s1 . (n + 1) as
Real ;
now ( ( 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
;
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;
verum end; case
r10 < r20
;
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;
verum end; end; end; hence
ex
y being
set st
S2[
n,
x,
y]
;
verum end; end; end;
hence
ex
y being
set st
S2[
n,
x,
y]
;
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
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]
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)
A22:
for k being Nat st S4[k] holds
S4[k + 1]
proof
let k be
Nat;
( S4[k] implies S4[k + 1] )
assume A23:
(
0 <= k implies
s3 . 0 <= s3 . k )
;
S4[k + 1]
hence
S4[
k + 1]
;
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;
( S5[k] implies S5[k + 1] )
assume
for
n5 being
Nat st
k <= n5 holds
s3 . k <= s3 . n5
;
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]
A31:
S6[
0 ]
;
for
n4 being
Nat holds
S6[
n4]
from NAT_1:sch 2(A31, A26);
hence
S5[
k + 1]
;
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-decreasing
by SEQM_3:def 3;
A35:
rng s3 c= R
for n being Nat holds s3 . n < (upper_bound R) + 1
then A43:
s3 is bounded_above
by SEQ_2:def 3;
A44:
for r being Real st r > 0 holds
(upper_bound R) - r < lim s3
A51:
for n being Nat holds s3 . n <= upper_bound R
for n being Nat holds s3 . n < (upper_bound R) + 1
then A53:
s3 is bounded_above
by SEQ_2:def 3;
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; verum