let k be Nat; :: thesis: for seq being Real_Sequence holds
( ( seq ^\ k is divergent_to+infty implies seq is divergent_to+infty ) & ( seq ^\ k is divergent_to-infty implies seq is divergent_to-infty ) )
let seq be Real_Sequence; :: thesis: ( ( seq ^\ k is divergent_to+infty implies seq is divergent_to+infty ) & ( seq ^\ k is divergent_to-infty implies seq is divergent_to-infty ) )
thus ( seq ^\ k is divergent_to+infty implies seq is divergent_to+infty ) :: thesis: ( seq ^\ k is divergent_to-infty implies seq is divergent_to-infty )
proof
assume A1: seq ^\ k is divergent_to+infty ; :: thesis: 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 < seq . m
consider n1 being Nat such that
A2: for m being Nat st n1 <= m holds
r < (seq ^\ k) . m by A1;
take n = n1 + k; :: thesis: for m being Nat st n <= m holds
r < seq . m
let m be Nat; :: thesis: ( n <= m implies r < seq . m )
assume n <= m ; :: thesis: r < seq . m
then consider n2 being Nat such that
A3: m = n + n2 by NAT_1:10;
reconsider n2 = n2 as Element of NAT by ORDINAL1:def 12;
A4: r < (seq ^\ k) . (n1 + n2) by A2, NAT_1:12;
(n1 + n2) + k = m by A3;
hence r < seq . m by A4, NAT_1:def 3; :: thesis: verum
end;
assume A5: seq ^\ k is divergent_to-infty ; :: thesis: seq is divergent_to-infty
let r be Real; :: according to LIMFUNC1:def 5 :: thesis: ex n being Nat st
for m being Nat st n <= m holds
seq . m < r
consider n1 being Nat such that
A6: for m being Nat st n1 <= m holds
(seq ^\ k) . m < r by A5;
take n = n1 + k; :: thesis: for m being Nat st n <= m holds
seq . m < r
let m be Nat; :: thesis: ( n <= m implies seq . m < r )
assume n <= m ; :: thesis: seq . m < r
then consider n2 being Nat such that
A7: m = n + n2 by NAT_1:10;
reconsider n2 = n2 as Element of NAT by ORDINAL1:def 12;
A8: (seq ^\ k) . (n1 + n2) < r by A6, NAT_1:12;
(n1 + n2) + k = m by A7;
hence seq . m < r by A8, NAT_1:def 3; :: thesis: verum