set M = Mersenne 19;
assume not Mersenne 19 is prime ; :: thesis: contradiction
then consider n being Element of NAT such that
A1: 1 < n and
A2: n * n <= Mersenne 19 and
A3: n is prime and
A4: n divides Mersenne 19 by Lm14, NAT_4:14;
set p = (2 * 9) + 1;
consider k being Nat such that
A5: n = ((2 * k) * ((2 * 9) + 1)) + 1 by A3, A4, XPRIMES1:19, Th23;
n = (38 * k) + 1 by A5;
then not not k = 0 & ... & not k = 19 by A2, Lm14, Lm27, 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 or k = 11 or k = 12 or k = 13 or k = 14 or k = 15 or k = 16 or k = 17 or k = 18 or k = 19 ) ;

suppose k = 0 ; :: thesis: contradiction

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

end;

suppose k = 1 ; :: thesis: contradiction

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

end;

suppose k = 2 ; :: thesis: contradiction

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

end;

suppose k = 3 ; :: thesis: contradiction

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

end;

suppose k = 4 ; :: thesis: contradiction

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

end;

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

Mersenne 19 = (191 * 2744) + 183 by Lm14;
hence contradiction by A4, A5, A6, NAT_4:9; :: thesis: verum

end;

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

Mersenne 19 = (229 * 2289) + 106 by Lm14;
hence contradiction by A4, A5, A7, NAT_4:9; :: thesis: verum

end;

suppose k = 7 ; :: thesis: contradiction

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

end;

suppose k = 8 ; :: thesis: contradiction

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

end;

suppose k = 9 ; :: thesis: contradiction

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

end;

suppose k = 10 ; :: thesis: contradiction

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

end;

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

Mersenne 19 = (419 * 1251) + 118 by Lm14;
hence contradiction by A4, A5, A8, NAT_4:9; :: thesis: verum

end;

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

Mersenne 19 = (457 * 1147) + 108 by Lm14;
hence contradiction by A4, A5, A9, NAT_4:9; :: thesis: verum

end;

suppose k = 13 ; :: thesis: contradiction

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

end;

suppose k = 14 ; :: thesis: contradiction

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

end;

suppose A10: k = 15 ; :: thesis: contradiction

Mersenne 19 = (571 * 918) + 109 by Lm14;
hence contradiction by A4, A5, A10, NAT_4:9; :: thesis: verum

end;

suppose k = 16 ; :: thesis: contradiction

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

end;

suppose A11: k = 17 ; :: thesis: contradiction

Mersenne 19 = (647 * 810) + 217 by Lm14;
hence contradiction by A4, A5, A11, NAT_4:9; :: thesis: verum

end;

suppose k = 18 ; :: thesis: contradiction

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

end;

suppose k = 19 ; :: thesis: contradiction

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

end;

end;