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 Nat st
for m being Nat st n <= m holds
r < (seq1 (#) seq2) . m
consider n1 being Nat such that
A3: for m being Nat st n1 <= m holds
sqrt |.r.| < seq1 . m by A1;
consider n2 being Nat such that
A4: for m being Nat st n2 <= m holds
sqrt |.r.| < seq2 . m by A2;
reconsider n = max (n1,n2) as Nat by TARSKI:1;
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 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 |.r.| < seq2 . m by A4;
n1 <= n by XXREAL_0:25;
then n1 <= m by A5, XXREAL_0:2;
then A7: sqrt |.r.| < seq1 . m by A3;
A8: |.r.| >= 0 by COMPLEX1:46;
then sqrt |.r.| >= 0 by SQUARE_1:def 2;
then (sqrt |.r.|) ^2 < (seq1 . m) * (seq2 . m) by A7, A6, XREAL_1:96;
then A9: |.r.| < (seq1 . m) * (seq2 . m) by A8, SQUARE_1:def 2;
r <= |.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