let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is divergent_to+infty & seq2 is divergent_to+infty implies seq1 (#) seq2 is divergent_to+infty )
assume A1: ( seq1 is divergent_to+infty & seq2 is divergent_to+infty ) ; :: thesis: seq1 (#) seq2 is divergent_to+infty
let r be Real; :: according to LIMFUNC1:def 4 :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
r < (seq1 (#) seq2) . m
consider n1 being Element of NAT such that
A2: for m being Element of NAT st n1 <= m holds
sqrt (abs r) < seq1 . m by A1, Def4;
consider n2 being Element of NAT such that
A3: for m being Element of NAT st n2 <= m holds
sqrt (abs r) < seq2 . m by A1, Def4;
take n = max n1,n2; :: thesis: for m being Element of NAT st n <= m holds
r < (seq1 (#) seq2) . m
let m be Element of NAT ; :: thesis: ( n <= m implies r < (seq1 (#) seq2) . m )
assume A4: n <= m ; :: thesis: r < (seq1 (#) seq2) . m
n1 <= n by XXREAL_0:25;
then n1 <= m by A4, XXREAL_0:2;
then A5: sqrt (abs r) < seq1 . m by A2;
n2 <= n by XXREAL_0:25;
then n2 <= m by A4, XXREAL_0:2;
then A6: sqrt (abs r) < seq2 . m by A3;
A7: abs r >= 0 by COMPLEX1:132;
then sqrt (abs r) >= 0 by SQUARE_1:def 4;
then (sqrt (abs r)) ^2 < (seq1 . m) * (seq2 . m) by A5, A6, XREAL_1:98;
then A8: abs r < (seq1 . m) * (seq2 . m) by A7, SQUARE_1:def 4;
r <= abs r by ABSVALUE:11;
then r < (seq1 . m) * (seq2 . m) by A8, XXREAL_0:2;
hence r < (seq1 (#) seq2) . m by SEQ_1:12; :: thesis: verum