let seq1, seq2 be ExtREAL_sequence; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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;

end;

suppose A4:
seq1 is convergent_to_finite_number
; :: thesis: lim seq1 <= lim seq2

A5:
not seq2 is convergent_to_-infty

end;proof

assume A6:
seq2 is convergent_to_-infty
; :: thesis: contradiction

hence contradiction by A4, MESFUNC5:51; :: thesis: verum

end;now :: thesis: for g being Real st g < 0 holds

ex n being Nat st

for m being Nat st n <= m holds

seq1 . m <= g

then
seq1 is convergent_to_-infty
by MESFUNC5:def 10;ex n being Nat st

for m being Nat st n <= m holds

seq1 . m <= g

let g be Real; :: thesis: ( g < 0 implies ex n being Nat st

for m being Nat st n <= m holds

seq1 . m <= g )

assume g < 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

seq1 . m <= g

then consider n being Nat such that

A7: for m being Nat st n <= m holds

seq2 . m <= g by A6, MESFUNC5:def 10;

for m being Nat st n <= m holds

seq1 . m <= g ; :: thesis: verum

end;for m being Nat st n <= m holds

seq1 . m <= g )

assume g < 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

seq1 . m <= g

then consider n being Nat such that

A7: for m being Nat st n <= m holds

seq2 . m <= g by A6, MESFUNC5:def 10;

now :: thesis: for m being Nat st n <= m holds

seq1 . m <= g

hence
ex n being Nat st seq1 . m <= g

let m be Nat; :: thesis: ( n <= m implies seq1 . m <= g )

A8: seq1 . m <= seq2 . m by A3;

assume n <= m ; :: thesis: seq1 . m <= g

then seq2 . m <= g by A7;

hence seq1 . m <= g by A8, XXREAL_0:2; :: thesis: verum

end;A8: seq1 . m <= seq2 . m by A3;

assume n <= m ; :: thesis: seq1 . m <= g

then seq2 . m <= g by A7;

hence seq1 . m <= g by A8, XXREAL_0:2; :: thesis: verum

for m being Nat st n <= m holds

seq1 . m <= g ; :: thesis: verum

hence contradiction by A4, MESFUNC5:51; :: thesis: verum

per cases
( seq2 is convergent_to_finite_number or seq2 is convergent_to_+infty )
by A2, A5, MESFUNC5:def 11;

end;

suppose A9:
seq2 is convergent_to_finite_number
; :: thesis: lim seq1 <= lim seq2

consider 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 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 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

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; :: thesis: verum

end;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;

now :: thesis: for y being object st y in rng (seq1 ^\ k) holds

y in rng (seq1 ^\ k1)

then A17:
rng (seq1 ^\ k) c= rng (seq1 ^\ k1)
;y in rng (seq1 ^\ k1)

reconsider k2 = k - k1 as Element of NAT by INT_1:5, XXREAL_0:25;

let y be object ; :: thesis: ( y in rng (seq1 ^\ k) implies y in rng (seq1 ^\ k1) )

assume y in rng (seq1 ^\ k) ; :: thesis: y in rng (seq1 ^\ k1)

then consider n being object such that

A15: n in dom (seq1 ^\ k) and

A16: (seq1 ^\ k) . n = y by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A15;

y = seq1 . (k + n) by A16, NAT_1:def 3;

then y = seq1 . (k1 + (k2 + n)) ;

then y = (seq1 ^\ k1) . (k2 + n) by NAT_1:def 3;

hence y in rng (seq1 ^\ k1) by A14, FUNCT_1:def 3; :: thesis: verum

end;let y be object ; :: thesis: ( y in rng (seq1 ^\ k) implies y in rng (seq1 ^\ k1) )

assume y in rng (seq1 ^\ k) ; :: thesis: y in rng (seq1 ^\ k1)

then consider n being object such that

A15: n in dom (seq1 ^\ k) and

A16: (seq1 ^\ k) . n = y by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A15;

y = seq1 . (k + n) by A16, NAT_1:def 3;

then y = seq1 . (k1 + (k2 + n)) ;

then y = (seq1 ^\ k1) . (k2 + n) by NAT_1:def 3;

hence y in rng (seq1 ^\ k1) by A14, FUNCT_1:def 3; :: thesis: verum

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;

now :: thesis: for y being object st y in rng (seq2 ^\ k) holds

y in rng (seq2 ^\ k2)

then A26:
rng (seq2 ^\ k) c= rng (seq2 ^\ k2)
;y in rng (seq2 ^\ k2)

reconsider k3 = k - k2 as Element of NAT by INT_1:5, XXREAL_0:25;

let y be object ; :: thesis: ( y in rng (seq2 ^\ k) implies y in rng (seq2 ^\ k2) )

assume y in rng (seq2 ^\ k) ; :: thesis: y in rng (seq2 ^\ k2)

then consider n being object such that

A24: n in dom (seq2 ^\ k) and

A25: (seq2 ^\ k) . n = y by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A24;

y = seq2 . (k + n) by A25, NAT_1:def 3;

then y = seq2 . (k2 + (k3 + n)) ;

then y = (seq2 ^\ k2) . (k3 + n) by NAT_1:def 3;

hence y in rng (seq2 ^\ k2) by A23, FUNCT_1:def 3; :: thesis: verum

end;let y be object ; :: thesis: ( y in rng (seq2 ^\ k) implies y in rng (seq2 ^\ k2) )

assume y in rng (seq2 ^\ k) ; :: thesis: y in rng (seq2 ^\ k2)

then consider n being object such that

A24: n in dom (seq2 ^\ k) and

A25: (seq2 ^\ k) . n = y by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A24;

y = seq2 . (k + n) by A25, NAT_1:def 3;

then y = seq2 . (k2 + (k3 + n)) ;

then y = (seq2 ^\ k2) . (k3 + n) by NAT_1:def 3;

hence y in rng (seq2 ^\ k2) by A23, FUNCT_1:def 3; :: thesis: verum

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

proof

A32:
seq1 ^\ k is convergent_to_finite_number
by A4, Th20;
let n be Nat; :: thesis: rseq1 . n <= rseq2 . n

A31: (seq2 ^\ k) . n = seq2 . (k + n) by NAT_1:def 3;

(seq1 ^\ k) . n = seq1 . (k + n) by NAT_1:def 3;

hence rseq1 . n <= rseq2 . n by A3, A31; :: thesis: verum

end;A31: (seq2 ^\ k) . n = seq2 . (k + n) by NAT_1:def 3;

(seq1 ^\ k) . n = seq1 . (k + n) by NAT_1:def 3;

hence rseq1 . n <= rseq2 . n by A3, A31; :: thesis: verum

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; :: thesis: verum

suppose A35:
seq2 is convergent_to_+infty
; :: thesis: lim seq1 <= lim seq2

then
seq2 is convergent
by MESFUNC5:def 11;

then lim seq2 = +infty by A35, MESFUNC5:def 12;

hence lim seq1 <= lim seq2 by XXREAL_0:3; :: thesis: verum

end;then lim seq2 = +infty by A35, MESFUNC5:def 12;

hence lim seq1 <= lim seq2 by XXREAL_0:3; :: thesis: verum

suppose A36:
seq1 is convergent_to_+infty
; :: thesis: lim seq1 <= lim seq2

then seq2 is convergent by MESFUNC5:def 11;

then lim seq2 = +infty by A39, MESFUNC5:def 12;

hence lim seq1 <= lim seq2 by XXREAL_0:3; :: thesis: verum

end;

now :: thesis: for g being Real st 0 < g holds

ex n being Nat st

for m being Nat st n <= m holds

g <= seq2 . m

then A39:
seq2 is convergent_to_+infty
by MESFUNC5:def 9;ex n being Nat st

for m being Nat st n <= m holds

g <= seq2 . m

let g be Real; :: thesis: ( 0 < g implies ex n being Nat st

for m being Nat st n <= m holds

g <= seq2 . m )

assume 0 < g ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

g <= seq2 . m

then consider n being Nat such that

A37: for m being Nat st n <= m holds

g <= seq1 . m by A36, MESFUNC5:def 9;

for m being Nat st n <= m holds

g <= seq2 . m ; :: thesis: verum

end;for m being Nat st n <= m holds

g <= seq2 . m )

assume 0 < g ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

g <= seq2 . m

then consider n being Nat such that

A37: for m being Nat st n <= m holds

g <= seq1 . m by A36, MESFUNC5:def 9;

now :: thesis: for m being Nat st n <= m holds

g <= seq2 . m

hence
ex n being Nat st g <= seq2 . m

let m be Nat; :: thesis: ( n <= m implies g <= seq2 . m )

A38: seq1 . m <= seq2 . m by A3;

assume n <= m ; :: thesis: g <= seq2 . m

then g <= seq1 . m by A37;

hence g <= seq2 . m by A38, XXREAL_0:2; :: thesis: verum

end;A38: seq1 . m <= seq2 . m by A3;

assume n <= m ; :: thesis: g <= seq2 . m

then g <= seq1 . m by A37;

hence g <= seq2 . m by A38, XXREAL_0:2; :: thesis: verum

for m being Nat st n <= m holds

g <= seq2 . m ; :: thesis: verum

then seq2 is convergent by MESFUNC5:def 11;

then lim seq2 = +infty by A39, MESFUNC5:def 12;

hence lim seq1 <= lim seq2 by XXREAL_0:3; :: thesis: verum

suppose A40:
seq1 is convergent_to_-infty
; :: thesis: lim seq1 <= lim seq2

then
seq1 is convergent
by MESFUNC5:def 11;

then lim seq1 = -infty by A40, MESFUNC5:def 12;

hence lim seq1 <= lim seq2 by XXREAL_0:5; :: thesis: verum

end;then lim seq1 = -infty by A40, MESFUNC5:def 12;

hence lim seq1 <= lim seq2 by XXREAL_0:5; :: thesis: verum