( ((0 * 8) + 0) mod 8 = 0 & ((18 * 8) + 0) mod 8 = 0 & ((8 * 0) + 1) mod 8 = 1 & ((8 * 29) + 1) mod 8 = 1 ) by NUMBER02:16;
hence ( Fib 0, Fib 12 are_congruent_mod 8 & Fib 1, Fib (12 + 1) are_congruent_mod 8 ) by Th7, PRE_FF:1, NAT_D:64; :: thesis: for x being Nat st x < 12 holds
( (Fib x) mod 8 <> 4 & (Fib x) mod 8 <> 6 )
let x be Nat; :: thesis: ( x < 12 implies ( (Fib x) mod 8 <> 4 & (Fib x) mod 8 <> 6 ) )
assume A1: x < 12 ; :: thesis: ( (Fib x) mod 8 <> 4 & (Fib x) mod 8 <> 6 )
A2: not not x = 0 & ... & not x = 12 by A1;
( ((0 * 8) + 0) mod 8 = 0 & ((8 * 0) + 1) mod 8 = 1 & ((0 * 8) + 2) mod 8 = 2 & ((8 * 0) + 3) mod 8 = 3 & ((0 * 8) + 5) mod 8 = 5 & ((8 * 1) + 0) mod 8 = 0 & ((1 * 8) + 5) mod 8 = 5 & ((8 * 2) + 5) mod 8 = 5 & ((3 * 8) + 5) mod 8 = 5 & ((8 * 4) + 2) mod 8 = 2 & ((8 * 6) + 7) mod 8 = 7 & ((11 * 8) + 1) mod 8 = 1 ) by NUMBER02:16;
hence ( (Fib x) mod 8 <> 4 & (Fib x) mod 8 <> 6 ) by A1, A2, Th7, FIB_NUM2:21, FIB_NUM2:22, FIB_NUM2:23, PRE_FF:1, NUMBER06:46; :: thesis: verum