(2 |^ 6) - 2 = (((((2 * 2) * 2) * 2) * 2) * 2) - 2 by Th2
.= (6 * 10) + 2 ;
hence not 6 divides (2 |^ 6) - 2 by Th34; :: thesis: ( 6 divides (3 |^ 6) - 3 & ( for n being Nat holds
( not n < 6 or n divides (2 |^ n) - 2 or not n divides (3 |^ n) - 3 ) ) )
(3 |^ 6) - 3 = (((((3 * 3) * 3) * 3) * 3) * 3) - 3 by Th2
.= 6 * 121 ;
hence 6 divides (3 |^ 6) - 3 ; :: thesis: for n being Nat holds
( not n < 6 or n divides (2 |^ n) - 2 or not n divides (3 |^ n) - 3 )
let n be Nat; :: thesis: ( not n < 6 or n divides (2 |^ n) - 2 or not n divides (3 |^ n) - 3 )
assume that
A1: n < 6 and
A2: not n divides (2 |^ n) - 2 ; :: thesis: not n divides (3 |^ n) - 3
not not n = 0 & ... & not n = 6 - 1 by A1, Th7;
then A3: not not n = 0 & ... & not n = 5 ;

per cases ( n = 0 or n = 4 ) by A2, A3, INT_2:28, PEPIN:41, PEPIN:59, INT_2:12, NEWTON02:138;

suppose n = 0 ; :: thesis: not n divides (3 |^ n) - 3

hence not n divides (3 |^ n) - 3 by NEWTON:4; :: thesis: verum

end;

suppose A4: n = 4 ; :: thesis: not n divides (3 |^ n) - 3

(3 |^ 4) - 3 = (((3 * 3) * 3) * 3) - 3 by POLYEQ_5:3
.= (4 * 19) + 2 ;
hence not n divides (3 |^ n) - 3 by A4, Th32; :: thesis: verum

end;

end;