let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is divergent_to+infty & seq2 is convergent & 0 < lim seq2 implies seq1 (#) seq2 is divergent_to+infty )
assume that
A1: seq1 is divergent_to+infty and
A2: seq2 is convergent and
A3: 0 < lim seq2 ; :: thesis: seq1 (#) seq2 is divergent_to+infty
consider n1 being Nat such that
A4: for m being Nat st n1 <= m holds
(lim seq2) / 2 < seq2 . m by A2, A3, Th5;
now :: thesis: ( 0 < (lim seq2) / 2 & ( for n being Nat holds (lim seq2) / 2 <= (seq2 ^\ n1) . n ) )
thus 0 < (lim seq2) / 2 by A3, XREAL_1:215; :: thesis: for n being Nat holds (lim seq2) / 2 <= (seq2 ^\ n1) . n
let n be Nat; :: thesis: (lim seq2) / 2 <= (seq2 ^\ n1) . n
(lim seq2) / 2 < seq2 . (n + n1) by A4, NAT_1:12;
hence (lim seq2) / 2 <= (seq2 ^\ n1) . n by NAT_1:def 3; :: thesis: verum
end;
then (seq1 ^\ n1) (#) (seq2 ^\ n1) is divergent_to+infty by A1, Th22, Th26;
then (seq1 (#) seq2) ^\ n1 is divergent_to+infty by SEQM_3:19;
hence seq1 (#) seq2 is divergent_to+infty by Th7; :: thesis: verum