let seq be Real_Sequence; :: thesis: ( ( seq is divergent_to+infty or seq is divergent_to-infty ) implies abs seq is divergent_to+infty )
assume A1: ( seq is divergent_to+infty or seq is divergent_to-infty ) ; :: thesis: abs seq 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 < (abs seq) . m
now :: thesis: ex n being Nat st
for m being Nat st n <= m holds
r < (abs seq) . m
per cases ( seq is divergent_to+infty or seq is divergent_to-infty ) by A1;
suppose seq is divergent_to+infty ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
r < (abs seq) . m
then consider n being Nat such that
A2: for m being Nat st n <= m holds
|.r.| < seq . m ;
take n = n; :: thesis: for m being Nat st n <= m holds
r < (abs seq) . m
let m be Nat; :: thesis: ( n <= m implies r < (abs seq) . m )
assume n <= m ; :: thesis: r < (abs seq) . m
then ( r <= |.r.| & |.r.| < seq . m ) by A2, ABSVALUE:4;
then A3: r < seq . m by XXREAL_0:2;
seq . m <= |.(seq . m).| by ABSVALUE:4;
then seq . m <= (abs seq) . m by SEQ_1:12;
hence r < (abs seq) . m by A3, XXREAL_0:2; :: thesis: verum
end;
suppose seq is divergent_to-infty ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
r < (abs seq) . m
then consider n being Nat such that
A4: for m being Nat st n <= m holds
seq . m < - r ;
take n = n; :: thesis: for m being Nat st n <= m holds
r < (abs seq) . m
let m be Nat; :: thesis: ( n <= m implies r < (abs seq) . m )
- |.(seq . m).| <= seq . m by ABSVALUE:4;
then A5: - ((abs seq) . m) <= seq . m by SEQ_1:12;
assume n <= m ; :: thesis: r < (abs seq) . m
then seq . m < - r by A4;
then - ((abs seq) . m) < - r by A5, XXREAL_0:2;
hence r < (abs seq) . m by XREAL_1:24; :: thesis: verum
end;
end;
end;
hence ex n being Nat st
for m being Nat st n <= m holds
r < (abs seq) . m ; :: thesis: verum