let n be Nat; :: thesis: ( n <= 341 & n divides (2 |^ n) - 2 & not n divides (3 |^ n) - 3 implies n = 341 )
assume n <= 341 ; :: thesis: ( not n divides (2 |^ n) - 2 or n divides (3 |^ n) - 3 or n = 341 )

per cases then ( n = 341 or n < 341 ) by XXREAL_0:1;

suppose n = 341 ; :: thesis: ( not n divides (2 |^ n) - 2 or n divides (3 |^ n) - 3 or n = 341 )

hence ( not n divides (2 |^ n) - 2 or n divides (3 |^ n) - 3 or n = 341 ) ; :: thesis: verum

end;

suppose A1: n < 341 ; :: thesis: ( not n divides (2 |^ n) - 2 or n divides (3 |^ n) - 3 or n = 341 )

assume that
A2: n divides (2 |^ n) - 2 and
A3: not n divides (3 |^ n) - 3 ; :: thesis: n = 341
n is composite by A2, A3, Th62;
then n in {341,561,645,1105} by A1, A2, Th49, XXREAL_0:2;
then ( n = 341 or n = 561 or n = 645 or n = 1105 ) by ENUMSET1:def 2;
hence n = 341 by A1; :: thesis: verum

end;

end;