let seq1, seq2 be ExtREAL_sequence; ( seq1 is convergent & seq2 is convergent & ( for n being Nat holds seq1 . n <= seq2 . n ) implies lim seq1 <= lim seq2 )
assume that
A1:
seq1 is convergent
and
A2:
seq2 is convergent
and
A3:
for n being Nat holds seq1 . n <= seq2 . n
; lim seq1 <= lim seq2
per cases
( seq1 is convergent_to_finite_number or seq1 is convergent_to_+infty or seq1 is convergent_to_-infty )
by A1, MESFUNC5:def 11;
suppose A4:
seq1 is
convergent_to_finite_number
;
lim seq1 <= lim seq2A5:
not
seq2 is
convergent_to_-infty
per cases
( seq2 is convergent_to_finite_number or seq2 is convergent_to_+infty )
by A2, A5, MESFUNC5:def 11;
suppose A9:
seq2 is
convergent_to_finite_number
;
lim seq1 <= lim seq2consider k1 being
Nat such that A10:
seq1 ^\ k1 is
bounded
by A4, Th19;
seq1 ^\ k1 is
bounded_above
by A10;
then
rng (seq1 ^\ k1) is
bounded_above
;
then consider UB being
Real such that A11:
UB is
UpperBound of
rng (seq1 ^\ k1)
by XXREAL_2:def 10;
consider k2 being
Nat such that A12:
seq2 ^\ k2 is
bounded
by A9, Th19;
reconsider k =
max (
k1,
k2) as
Element of
NAT by ORDINAL1:def 12;
A13:
lim seq2 = lim (seq2 ^\ k)
by A9, Th20;
A14:
dom (seq1 ^\ k1) = NAT
by FUNCT_2:def 1;
then A17:
rng (seq1 ^\ k) c= rng (seq1 ^\ k1)
;
then
UB is
UpperBound of
rng (seq1 ^\ k)
by A11, XXREAL_2:6;
then
rng (seq1 ^\ k) is
bounded_above
by XXREAL_2:def 10;
then A18:
seq1 ^\ k is
bounded_above
;
seq1 ^\ k1 is
bounded_below
by A10;
then
rng (seq1 ^\ k1) is
bounded_below
;
then consider LB being
Real such that A19:
LB is
LowerBound of
rng (seq1 ^\ k1)
by XXREAL_2:def 9;
LB is
LowerBound of
rng (seq1 ^\ k)
by A17, A19, XXREAL_2:5;
then
rng (seq1 ^\ k) is
bounded_below
by XXREAL_2:def 9;
then
seq1 ^\ k is
bounded_below
;
then
seq1 ^\ k is
bounded
by A18;
then reconsider rseq1 =
seq1 ^\ k as
Real_Sequence by Th11;
seq2 ^\ k2 is
bounded_below
by A12;
then
rng (seq2 ^\ k2) is
bounded_below
;
then consider LB being
Real such that A20:
LB is
LowerBound of
rng (seq2 ^\ k2)
by XXREAL_2:def 9;
A21:
lim seq1 = lim (seq1 ^\ k)
by A4, Th20;
seq2 ^\ k2 is
bounded_above
by A12;
then
rng (seq2 ^\ k2) is
bounded_above
;
then consider UB being
Real such that A22:
UB is
UpperBound of
rng (seq2 ^\ k2)
by XXREAL_2:def 10;
A23:
dom (seq2 ^\ k2) = NAT
by FUNCT_2:def 1;
then A26:
rng (seq2 ^\ k) c= rng (seq2 ^\ k2)
;
then
UB is
UpperBound of
rng (seq2 ^\ k)
by A22, XXREAL_2:6;
then
rng (seq2 ^\ k) is
bounded_above
by XXREAL_2:def 10;
then A27:
seq2 ^\ k is
bounded_above
;
LB is
LowerBound of
rng (seq2 ^\ k)
by A20, A26, XXREAL_2:5;
then
rng (seq2 ^\ k) is
bounded_below
by XXREAL_2:def 9;
then
seq2 ^\ k is
bounded_below
;
then
seq2 ^\ k is
bounded
by A27;
then reconsider rseq2 =
seq2 ^\ k as
Real_Sequence by Th11;
A28:
seq2 ^\ k is
convergent_to_finite_number
by A9, Th20;
then A29:
rseq2 is
convergent
by Th15;
A30:
for
n being
Nat holds
rseq1 . n <= rseq2 . n
A32:
seq1 ^\ k is
convergent_to_finite_number
by A4, Th20;
then A33:
lim (seq1 ^\ k) = lim rseq1
by Th15;
A34:
lim (seq2 ^\ k) = lim rseq2
by A28, Th15;
rseq1 is
convergent
by A32, Th15;
hence
lim seq1 <= lim seq2
by A29, A33, A34, A30, A21, A13, SEQ_2:18;
verum end; end; end; end;