set M = Mersenne 17;
assume not Mersenne 17 is prime ; :: thesis: contradiction
then consider n being Element of NAT such that
A1: 1 < n and
A2: n * n <= Mersenne 17 and
A3: n is prime and
A4: n divides Mersenne 17 by Lm13, NAT_4:14;
set p = (2 * 8) + 1;
consider k being Nat such that
A5: n = ((2 * k) * ((2 * 8) + 1)) + 1 by A3, A4, XPRIMES1:17, Th23;
n = (34 * k) + 1 by A5;
then not not k = 0 & ... & not k = 10 by A2, Lm13, Lm26, NAT_1:60;

per cases then ( k = 0 or k = 1 or k = 2 or k = 3 or k = 4 or k = 5 or k = 6 or k = 7 or k = 8 or k = 9 or k = 10 ) ;

suppose k = 0 ; :: thesis: contradiction

hence contradiction by A1, A5; :: thesis: verum

end;

suppose k = 1 ; :: thesis: contradiction

hence contradiction by A3, A5, XPRIMES0:35; :: thesis: verum

end;

suppose k = 2 ; :: thesis: contradiction

hence contradiction by A3, A5, XPRIMES0:69; :: thesis: verum

end;

suppose A6: k = 3 ; :: thesis: contradiction

Mersenne 17 = (103 * 1272) + 55 by Lm13;
hence contradiction by A4, A5, A6, NAT_4:9; :: thesis: verum

end;

suppose A7: k = 4 ; :: thesis: contradiction

Mersenne 17 = (137 * 956) + 99 by Lm13;
hence contradiction by A4, A5, A7, NAT_4:9; :: thesis: verum

end;

suppose k = 5 ; :: thesis: contradiction

hence contradiction by A3, A5, XPRIMES0:171; :: thesis: verum

end;

suppose k = 6 ; :: thesis: contradiction

hence contradiction by A3, A5, XPRIMES0:205; :: thesis: verum

end;

suppose A8: k = 7 ; :: thesis: contradiction

Mersenne 17 = (239 * 548) + 99 by Lm13;
hence contradiction by A4, A5, A8, NAT_4:9; :: thesis: verum

end;

suppose k = 8 ; :: thesis: contradiction

hence contradiction by A3, A5, XPRIMES0:273; :: thesis: verum

end;

suppose A9: k = 9 ; :: thesis: contradiction

Mersenne 17 = (307 * 426) + 289 by Lm13;
hence contradiction by A4, A5, A9, NAT_4:9; :: thesis: verum

end;

suppose k = 10 ; :: thesis: contradiction

hence contradiction by A3, A5, XPRIMES0:341; :: thesis: verum

end;

end;