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 5 :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(seq1 + seq2) . m < r
consider n1 being Element of NAT such that
A3: for m being Element of NAT st n1 <= m holds
seq1 . m < r / 2 by A1, Def5;
consider n2 being Element of NAT such that
A4: for m being Element of NAT st n2 <= m holds
seq2 . m < r / 2 by A2, Def5;
take n = max n1,n2; :: thesis: for m being Element of NAT st n <= m holds
(seq1 + seq2) . m < r
let m be Element of NAT ; :: thesis: ( n <= m implies (seq1 + seq2) . m < r )
assume A5: n <= m ; :: thesis: (seq1 + seq2) . m < r
n2 <= n by XXREAL_0:25;
then n2 <= m by A5, XXREAL_0:2;
then A6: seq2 . m < r / 2 by A4;
n1 <= n by XXREAL_0:25;
then n1 <= m by A5, XXREAL_0:2;
then seq1 . m < r / 2 by A3;
then (seq1 . m) + (seq2 . m) < (r / 2) + (r / 2) by A6, XREAL_1:10;
hence (seq1 + seq2) . m < r by SEQ_1:11; :: thesis: verum