let j be Nat; :: thesis: ( 0 < j & j <= 7 implies ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j ) )
assume A1: ( 0 < j & j <= 7 ) ; :: thesis: ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j )
not not j = 0 & ... & not j = 7 by A1;

per cases then ( j = 1 or j = 2 or j = 3 or j = 4 or j = 5 or j = 6 or j = 7 ) by A1;

suppose j = 1 ; :: thesis: ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j )

then ( Fib 0, Fib 1 are_congruent_mod j & Fib 1, Fib (1 + 1) are_congruent_mod j ) by INT_1:13;
hence ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j ) ; :: thesis: verum

end;

suppose A2: j = 2 ; :: thesis: ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j )

A3: ( ((0 * j) + 0) mod j = 0 & ((j * 0) + 1) mod j = 1 ) by A2;
( ((2 * 1) + 0) mod 2 = 0 & ((2 * 1) + 1) mod 2 = 1 ) ;
then ( Fib 0, Fib 3 are_congruent_mod j & Fib 1, Fib (3 + 1) are_congruent_mod j ) by A2, A3, PRE_FF:1, NAT_D:64, FIB_NUM2:22, FIB_NUM2:23;
hence ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j ) ; :: thesis: verum

end;

suppose A4: j = 3 ; :: thesis: ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j )

A5: ( ((0 * j) + 0) mod j = 0 & ((j * 0) + 1) mod j = 1 ) by A4, NUMBER02:16;
( ((3 * 7) + 0) mod j = 0 & ((3 * 11) + 1) mod j = 1 ) by A4, NUMBER02:16;
then ( Fib 0, Fib 8 are_congruent_mod j & Fib 1, Fib (8 + 1) are_congruent_mod j ) by A4, A5, PRE_FF:1, NAT_D:64, Th7;
hence ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j ) ; :: thesis: verum

end;

suppose A6: j = 4 ; :: thesis: ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j )

A7: ( ((0 * j) + 0) mod j = 0 & ((j * 0) + 1) mod j = 1 ) by A6, NUMBER02:16;
( ((4 * 2) + 0) mod j = 0 & ((4 * 3) + 1) mod j = 1 ) by A6, NUMBER02:16;
then ( Fib 0, Fib 6 are_congruent_mod j & Fib 1, Fib (6 + 1) are_congruent_mod j ) by A6, A7, PRE_FF:1, NAT_D:64, Th7;
hence ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j ) ; :: thesis: verum

end;

suppose A8: j = 5 ; :: thesis: ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j )

A9: ( ((0 * j) + 0) mod j = 0 & ((j * 0) + 1) mod j = 1 ) by A8, NUMBER02:16;
( ((5 * 1353) + 0) mod j = 0 & ((5 * 2189) + 1) mod j = 1 ) by A8, NUMBER02:16;
then ( Fib 0, Fib 20 are_congruent_mod j & Fib 1, Fib (20 + 1) are_congruent_mod j ) by A8, A9, PRE_FF:1, NAT_D:64, Th7;
hence ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j ) ; :: thesis: verum

end;

suppose A10: j = 6 ; :: thesis: ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j )

A11: ( ((0 * j) + 0) mod j = 0 & ((j * 0) + 1) mod j = 1 ) by A10, NUMBER02:16;
( ((6 * 7728) + 0) mod j = 0 & ((6 * 12504) + 1) mod j = 1 ) by A10, NUMBER02:16;
then ( Fib 0, Fib 24 are_congruent_mod j & Fib 1, Fib (24 + 1) are_congruent_mod j ) by A10, A11, PRE_FF:1, NAT_D:64, Th7;
hence ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j ) ; :: thesis: verum

end;

suppose A12: j = 7 ; :: thesis: ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j )

A13: ( ((0 * j) + 0) mod j = 0 & ((j * 0) + 1) mod j = 1 ) by A12, NUMBER02:16;
( ((7 * 141) + 0) mod j = 0 & ((7 * 228) + 1) mod j = 1 ) by A12, NUMBER02:16;
then ( Fib 0, Fib 16 are_congruent_mod j & Fib 1, Fib (16 + 1) are_congruent_mod j ) by A12, A13, PRE_FF:1, NAT_D:64, Th7;
hence ex i being Nat st
( i > 0 & Fib 0, Fib i are_congruent_mod j & Fib 1, Fib (i + 1) are_congruent_mod j ) ; :: thesis: verum

end;

end;