let i, j, k be Nat; :: thesis: ( 0 < j & k < i & ( for x, y being Nat st x,y are_congruent_mod j holds
Fib x, Fib y are_congruent_mod i ) & ( for x being Nat st x < j holds
(Fib x) mod i <> k ) implies for m being Nat holds not (ArProg (k,i)) . m is Fibonacci )
assume that
A1: ( 0 < j & k < i ) and
A2: for x, y being Nat st x,y are_congruent_mod j holds
Fib x, Fib y are_congruent_mod i and
A3: for x being Nat st x < j holds
(Fib x) mod i <> k ; :: thesis: for m being Nat holds not (ArProg (k,i)) . m is Fibonacci
let m be Nat; :: thesis: not (ArProg (k,i)) . m is Fibonacci
assume (ArProg (k,i)) . m is Fibonacci ; :: thesis: contradiction
then consider f being Nat such that
A4: (ArProg (k,i)) . m = Fib f ;
(ArProg (k,i)) . m = k + (i * m) by NUMBER06:7;
then A5: (Fib f) mod i = k by A1, A4, NUMBER02:16;
A6: (Fib (f mod j)) mod i <> k by A3, A1, INT_1:58;
Fib f, Fib (f mod j) are_congruent_mod i by A2, A1, NUMPOLY1:4;
hence contradiction by A5, A6, NAT_D:64; :: thesis: verum