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
r / 2 < seq1 . m by A1;
consider n2 being Nat such that
A4: for m being Nat st n2 <= m holds
r / 2 < 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: 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:8;
hence r < (seq1 + seq2) . m by SEQ_1:7; :: thesis: verum