let seq1, seq2 be Real_Sequence; ( seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative implies ( (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) & lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) ) )
A1:
for seq1, seq2 being Real_Sequence st seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative holds
lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2)
proof
let seq1,
seq2 be
Real_Sequence;
( seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative implies lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) )
assume that A2:
(
seq1 is
bounded &
seq1 is
nonnegative )
and A3:
(
seq2 is
bounded &
seq2 is
nonnegative )
;
lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2)
set seq3 =
superior_realsequence seq1;
set seq4 =
superior_realsequence seq2;
set seq5 =
superior_realsequence (seq1 (#) seq2);
A4:
superior_realsequence (seq1 (#) seq2) is
convergent
by A2, A3, Th58;
A5:
(
lower_bound (superior_realsequence (seq1 (#) seq2)) = lim (superior_realsequence (seq1 (#) seq2)) &
lower_bound (superior_realsequence seq1) = lim (superior_realsequence seq1) )
by A2, A3, Th58;
A6:
lower_bound (superior_realsequence seq2) = lim (superior_realsequence seq2)
by A3, Th58;
A7:
for
n being
Nat holds
(superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) (#) (superior_realsequence seq2)) . n
A8:
(
superior_realsequence seq1 is
convergent &
superior_realsequence seq2 is
convergent )
by A2, A3, Th58;
then
(superior_realsequence seq1) (#) (superior_realsequence seq2) is
convergent
;
then
lim (superior_realsequence (seq1 (#) seq2)) <= lim ((superior_realsequence seq1) (#) (superior_realsequence seq2))
by A4, A7, SEQ_2:18;
hence
lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2)
by A8, A5, A6, SEQ_2:15;
verum
end;
for seq1, seq2 being Real_Sequence st seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative holds
(lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2)
proof
let seq1,
seq2 be
Real_Sequence;
( seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative implies (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) )
assume that A9:
(
seq1 is
bounded &
seq1 is
nonnegative )
and A10:
(
seq2 is
bounded &
seq2 is
nonnegative )
;
(lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2)
set seq3 =
inferior_realsequence seq1;
set seq4 =
inferior_realsequence seq2;
set seq5 =
inferior_realsequence (seq1 (#) seq2);
A11:
inferior_realsequence (seq1 (#) seq2) is
convergent
by A9, A10, Th57;
A12:
(
upper_bound (inferior_realsequence (seq1 (#) seq2)) = lim (inferior_realsequence (seq1 (#) seq2)) &
upper_bound (inferior_realsequence seq1) = lim (inferior_realsequence seq1) )
by A9, A10, Th57;
A13:
upper_bound (inferior_realsequence seq2) = lim (inferior_realsequence seq2)
by A10, Th57;
A14:
for
n being
Nat holds
(inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) (#) (inferior_realsequence seq2)) . n
A15:
(
inferior_realsequence seq1 is
convergent &
inferior_realsequence seq2 is
convergent )
by A9, A10, Th57;
then
(inferior_realsequence seq1) (#) (inferior_realsequence seq2) is
convergent
;
then
lim (inferior_realsequence (seq1 (#) seq2)) >= lim ((inferior_realsequence seq1) (#) (inferior_realsequence seq2))
by A11, A14, SEQ_2:18;
hence
(lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2)
by A15, A12, A13, SEQ_2:15;
verum
end;
hence
( seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative implies ( (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) & lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) ) )
by A1; verum