let n be odd Nat; :: thesis: n divides (2 |^ (n !)) - 1
set E = Euler n;

per cases ( n <= 1 or n > 1 ) ;

suppose n <= 1 ; :: thesis: n divides (2 |^ (n !)) - 1

then n = 1 by NAT_1:25;
hence n divides (2 |^ (n !)) - 1 by NAT_D:6; :: thesis: verum

end;

suppose n > 1 ; :: thesis: n divides (2 |^ (n !)) - 1

then (2 |^ (Euler n)) mod n = 1 by Lm2, NAT_5:3, EULER_2:18;
then A1: n divides (2 |^ (Euler n)) - 1 by PEPIN:8;
(2 |^ (Euler n)) - 1 divides (2 |^ (n !)) - 1 by Th47, NUMBER05:19;
hence n divides (2 |^ (n !)) - 1 by A1, INT_2:9; :: thesis: verum

end;

end;