thus for i, j being Nat st 0 < i & i <= 7 holds
ex k being Nat st (ArProg (j,i)) . k is Fibonacci :: thesis: for k being Nat holds not (ArProg (4,8)) . k is Fibonacci

proof

let i, j be Nat; :: thesis: ( 0 < i & i <= 7 implies ex k being Nat st (ArProg (j,i)) . k is Fibonacci )
assume A1: ( 0 < i & i <= 7 ) ; :: thesis: ex k being Nat st (ArProg (j,i)) . k is Fibonacci
consider k being Nat such that
A2: k > 0 and
A3: ( Fib 0, Fib k are_congruent_mod i & Fib 1, Fib (k + 1) are_congruent_mod i ) by A1, Th10;
A4: ( 1 = 1 + 0 & k + 1 = (0 + k) + 1 & 0 + k = k ) ;
consider f being Nat such that
A5: (Fib f) mod i = j mod i by A1, INT_1:58, Th9;
ex w being Nat st f + (k * w) >= j

proof

per cases ( f >= j or f < j ) ;

suppose f >= j ; :: thesis: ex w being Nat st f + (k * w) >= j

then f + (k * 0) >= j ;
hence ex w being Nat st f + (k * w) >= j ; :: thesis: verum

end;

suppose f < j ; :: thesis: ex w being Nat st f + (k * w) >= j

then A6: 0 < j - f by XREAL_1:50;
consider i being Integer such that
A7: ( k * i <= j - f & j - f <= k * (i + 1) ) by A2, NIVEN:5;
i + 1 > 0 by A6, A7;
then reconsider i1 = i + 1 as Element of NAT by INT_1:3;
(j - f) + f <= (k * i1) + f by A7, XREAL_1:6;
hence ex w being Nat st f + (k * w) >= j ; :: thesis: verum

end;

end;

end;

then consider w being Nat such that
A8: f + (k * w) >= j ;
Fib ((f + (k * w)) + 2) >= f + (k * w) by Th8;
then A9: Fib ((f + (k * w)) + 2) >= j by A8, XXREAL_0:2;
2 * k >= 2 * 1 by A2, NAT_1:14, XREAL_1:64;
then (f + (k * w)) + (2 * k) >= (f + (k * w)) + 2 by XREAL_1:6;
then Fib ((k * (2 + w)) + f) >= Fib ((f + (k * w)) + 2) by FIB_NUM2:45;
then A10: Fib ((k * (2 + w)) + f) >= j by A9, XXREAL_0:2;
(k * (2 + w)) + f,0 + f are_congruent_mod k ;
then (Fib ((k * (2 + w)) + f)) mod i = j mod i by A4, A3, Th11, A5, NAT_D:64;
then consider z being Integer such that
A11: Fib ((k * (2 + w)) + f) = (z * i) + j by A1, NAT_D:64, NAT_6:9;
z >= 0 by A1, A11, A10, XREAL_1:30;
then reconsider z = z as Element of NAT by INT_1:3;
(ArProg (j,i)) . z = (z * i) + j by NUMBER06:7;
hence ex k being Nat st (ArProg (j,i)) . k is Fibonacci by A11; :: thesis: verum

end;

let k be Nat; :: thesis: not (ArProg (4,8)) . k is Fibonacci
( Fib 0, Fib (0 + 12) are_congruent_mod 8 & Fib (0 + 1), Fib ((0 + 12) + 1) are_congruent_mod 8 ) by Th13;
then A12: for x, y being Nat st x,y are_congruent_mod 12 holds
Fib x, Fib y are_congruent_mod 8 by Th11;
for x being Nat st x < 12 holds
(Fib x) mod 8 <> 4 by Th13;
hence not (ArProg (4,8)) . k is Fibonacci by A12, Th12; :: thesis: verum