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