let seq be Real_Sequence; ( seq is V54() implies for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
lower_bound R = seq . n )
assume A1:
seq is V54()
; for n being Nat
for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
lower_bound R = seq . n
let n be Nat; for R being Subset of REAL st R = { (seq . k) where k is Nat : n <= k } holds
lower_bound R = seq . n
A2:
now for r being Real st r in { (seq . k) where k is Nat : n <= k } holds
seq . n <= rlet r be
Real;
( r in { (seq . k) where k is Nat : n <= k } implies seq . n <= r )assume
r in { (seq . k) where k is Nat : n <= k }
;
seq . n <= rthen consider r1 being
Real such that A3:
(
r = r1 &
r1 in { (seq . k) where k is Nat : n <= k } )
;
consider k1 being
Nat such that A4:
r1 = seq . k1
and A5:
n <= k1
by A3;
consider k being
Nat such that A6:
n + k = k1
by A5, NAT_1:10;
thus
seq . n <= r
by A1, A3, A4, A6, SEQM_3:5;
verum end;
let R be Subset of REAL; ( R = { (seq . k) where k is Nat : n <= k } implies lower_bound R = seq . n )
A7:
now for s being Real st 0 < s holds
ex r being Real st
( r in { (seq . k) where k is Nat : n <= k } & r < (seq . n) + s )let s be
Real;
( 0 < s implies ex r being Real st
( r in { (seq . k) where k is Nat : n <= k } & r < (seq . n) + s ) )A8:
seq . n in { (seq . k) where k is Nat : n <= k }
;
assume
0 < s
;
ex r being Real st
( r in { (seq . k) where k is Nat : n <= k } & r < (seq . n) + s )hence
ex
r being
Real st
(
r in { (seq . k) where k is Nat : n <= k } &
r < (seq . n) + s )
by A8, XREAL_1:29;
verum end;
assume A9:
R = { (seq . k) where k is Nat : n <= k }
; lower_bound R = seq . n
then A10:
R <> {}
by SETLIM_1:1;
R is bounded_below
by A1, A9, Th32, LIMFUNC1:1;
hence
lower_bound R = seq . n
by A9, A10, A2, A7, SEQ_4:def 2; verum