given n being Nat such that A1: 1 < n and
A2: n divides (2 |^ n) - 1 ; :: thesis: contradiction
defpred S₁[ Nat] means ( 1 < $1 & $1 divides (2 |^ $1) - 1 );
A3: ex k being Nat st S₁[k] by A1, A2;
consider N being Nat such that
A4: S₁[N] and
A5: for n being Nat st S₁[n] holds
N <= n from NAT_1:sch 5(A3);
N divides (2 |^ N) - 1 by A4;
then reconsider N = N as odd Element of NAT by A4, ORDINAL1:def 12;
set E = Euler N;
set d = N gcd (Euler N);
A6: 1 mod N = 1 by A4, NAT_D:14;
reconsider k = (2 |^ N) - 1 as Nat ;
2,N are_coprime by A4, Th45;
then (2 |^ (Euler N)) mod N = 1 by A4, EULER_2:18;
then ((2 |^ (Euler N)) - 1) mod N = (1 - 1) mod N by A6, INT_6:7
.= 0 ;
then N divides (2 |^ (Euler N)) - 1 by INT_1:62;
then A7: N divides ((2 |^ N) - 1) gcd ((2 |^ (Euler N)) - 1) by A4, INT_2:def 2;
A8: ((2 |^ N) - 1) gcd ((2 |^ (Euler N)) - 1) = (2 |^ (N gcd (Euler N))) - 1 by Th26;

A9: now :: thesis: not N gcd (Euler N) <= 1

assume N gcd (Euler N) <= 1 ; :: thesis: contradiction
then ( N gcd (Euler N) < 1 or N gcd (Euler N) = 1 ) by XXREAL_0:1;
hence contradiction by A4, A7, A8, NAT_1:14, WSIERP_1:15; :: thesis: verum

end;

A10: N gcd (Euler N) <= Euler N by Th13;
A11: N gcd (Euler N) divides N by INT_2:def 2;
A12: Euler N <= N - 1 by A4, EULER_1:19;
N - 1 < N - 0 by XREAL_1:15;
then Euler N < N by A12, XXREAL_0:2;
then N gcd (Euler N) < N by A10, XXREAL_0:2;
hence contradiction by A5, A11, A9, A7, A8, INT_2:9; :: thesis: verum