let n be Nat; :: thesis: ( n divides (2 |^ n) - 2 & not n divides (3 |^ n) - 3 implies n is composite )
assume that
A1: n divides (2 |^ n) - 2 and
A2: not n divides (3 |^ n) - 3 ; :: thesis: n is composite
A3: not 3 |^ n,3 are_congruent_mod n by A2;
assume not n is composite ; :: thesis: contradiction

per cases then ( 1 + 1 > n or ( 2 <= n & n is prime ) ) by NUMBER02:def 1;

suppose 1 + 1 > n ; :: thesis: contradiction

then n <= 0 + 1 by NAT_1:13;
then not not n = 0 & ... & not n = 1 ;
hence contradiction by A1, A2, NEWTON:4; :: thesis: verum

end;

suppose that A4: 2 <= n and
A5: n is prime ; :: thesis: contradiction

(3 |^ n) mod n <> 3 mod n by A3, A4, NAT_D:64;
hence contradiction by A5, EULER_2:19; :: thesis: verum

end;

end;