let f be eventually-non-zero Real_Sequence; :: thesis: for n being Nat holds f ^\ n is eventually-non-zero

let n be Nat; :: thesis: f ^\ n is eventually-non-zero

set g = f ^\ n;

let k be Nat; :: according to LIOUVIL1:def 3 :: thesis: ex N being Nat st

( k <= N & (f ^\ n) . N <> 0 )

consider N being Nat such that

A1: ( k + n <= N & f . N <> 0 ) by ENZ;

k <= N - n by A1, XREAL_1:19;

then N - n in NAT by INT_1:3;

then reconsider Nn = N - n as Nat ;

take Nn ; :: thesis: ( k <= Nn & (f ^\ n) . Nn <> 0 )

(f ^\ n) . Nn = f . (Nn + n) by NAT_1:def 3

.= f . N ;

hence ( k <= Nn & (f ^\ n) . Nn <> 0 ) by A1, XREAL_1:19; :: thesis: verum

let n be Nat; :: thesis: f ^\ n is eventually-non-zero

set g = f ^\ n;

let k be Nat; :: according to LIOUVIL1:def 3 :: thesis: ex N being Nat st

( k <= N & (f ^\ n) . N <> 0 )

consider N being Nat such that

A1: ( k + n <= N & f . N <> 0 ) by ENZ;

k <= N - n by A1, XREAL_1:19;

then N - n in NAT by INT_1:3;

then reconsider Nn = N - n as Nat ;

take Nn ; :: thesis: ( k <= Nn & (f ^\ n) . Nn <> 0 )

(f ^\ n) . Nn = f . (Nn + n) by NAT_1:def 3

.= f . N ;

hence ( k <= Nn & (f ^\ n) . Nn <> 0 ) by A1, XREAL_1:19; :: thesis: verum