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 that
A1: seq1 is divergent_to+infty and
A2: 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
A3: 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
A4: for m being Element of NAT st n2 <= m holds
sqrt (abs r) < seq2 . m by A2, 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 A5: n <= m ; :: thesis: r < (seq1 (#) seq2) . m
n2 <= n by XXREAL_0:25;
then n2 <= m by A5, XXREAL_0:2;
then A6: sqrt (abs r) < seq2 . m by A4;
n1 <= n by XXREAL_0:25;
then n1 <= m by A5, XXREAL_0:2;
then A7: sqrt (abs r) < seq1 . m by A3;
A8: abs r >= 0 by COMPLEX1:46;
then sqrt (abs r) >= 0 by SQUARE_1:def 2;
then (sqrt (abs r)) ^2 < (seq1 . m) * (seq2 . m) by A7, A6, XREAL_1:96;
then A9: abs r < (seq1 . m) * (seq2 . m) by A8, SQUARE_1:def 2;
r <= abs r by ABSVALUE:4;
then r < (seq1 . m) * (seq2 . m) by A9, XXREAL_0:2;
hence r < (seq1 (#) seq2) . m by SEQ_1:8; :: thesis: verum