let n be Nat; :: thesis: not 8 divides (3 |^ n) + 1

per cases ( n is odd or n is even ) ;

suppose n is odd ; :: thesis: not 8 divides (3 |^ n) + 1

then consider k being Nat such that
A1: n = (2 * k) + 1 by ABIAN:9;
A2: 3 |^ ((2 * k) + 1) = (3 |^ (2 * k)) * 3 by NEWTON:6;
3 |^ (2 * k),1 are_congruent_mod 8 by Th65;
then (3 |^ (2 * k)) * 3,1 * 3 are_congruent_mod 8 by Lm14, INT_1:18;
then (3 |^ ((2 * k) + 1)) + 1,4 are_congruent_mod 8 by A2;
then ((3 |^ n) + 1) mod 8 = 4 mod 8 by A1, NAT_D:64
.= 4 by NAT_D:24 ;
hence not 8 divides (3 |^ n) + 1 by INT_1:62; :: thesis: verum

end;

suppose n is even ; :: thesis: not 8 divides (3 |^ n) + 1

then consider k being Nat such that
A3: n = 2 * k ;
3 |^ (2 * k),1 are_congruent_mod 8 by Th65;
then (3 |^ (2 * k)) + 1,1 + 1 are_congruent_mod 8 ;
then ((3 |^ n) + 1) mod 8 = 2 mod 8 by A3, NAT_D:64
.= 2 by NAT_D:24 ;
hence not 8 divides (3 |^ n) + 1 by INT_1:62; :: thesis: verum

end;

end;