let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is divergent_to+infty & ex r being Real st
( r > 0 & ( for n being Nat holds seq2 . n >= r ) ) implies seq1 (#) seq2 is divergent_to+infty )
assume that
A1: seq1 is divergent_to+infty and
A2: ex r being Real st
( r > 0 & ( for n being Nat holds seq2 . n >= r ) ) ; :: thesis: seq1 (#) seq2 is divergent_to+infty
consider M being Real such that
A3: M > 0 and
A4: for n being Nat holds seq2 . n >= M by A2;
let r be Real; :: according to LIMFUNC1:def 4 :: thesis: ex n being Nat st
for m being Nat st n <= m holds
r < (seq1 (#) seq2) . m
A5: 0 <= |.r.| by COMPLEX1:46;
consider n being Nat such that
A6: for m being Nat st n <= m holds
|.r.| / M < seq1 . m by A1;
take n ; :: thesis: for m being Nat st n <= m holds
r < (seq1 (#) seq2) . m
let m be Nat; :: thesis: ( n <= m implies r < (seq1 (#) seq2) . m )
assume n <= m ; :: thesis: r < (seq1 (#) seq2) . m
then |.r.| / M < seq1 . m by A6;
then (|.r.| / M) * M < (seq1 . m) * (seq2 . m) by A3, A4, A5, XREAL_1:97;
then A7: |.r.| < (seq1 . m) * (seq2 . m) by A3, XCMPLX_1:87;
r <= |.r.| by ABSVALUE:4;
then r < (seq1 . m) * (seq2 . m) by A7, XXREAL_0:2;
hence r < (seq1 (#) seq2) . m by SEQ_1:8; :: thesis: verum