let m, k be Nat; :: thesis: ( m >= k & k >= 2 implies not (2 |^ ((m !) + k)) - 1 is Prime )
assume A0: ( m >= k & k >= 2 ) ; :: thesis: (2 |^ ((m !) + k)) - 1 is not Prime
2 |^ k > k by NEWTON:86;
then A1: (2 |^ k) - 1 <> 1 by A0;
a2: 0 + k < (m !) + k by XREAL_1:8;
then 2 |^ k divides 2 |^ ((m !) + k) by NEWTON:89;
then C1: 2 |^ k <= 2 |^ ((m !) + k) by NAT_D:7;
2 |^ k <> 2 |^ ((m !) + k)

proof

assume 2 |^ k = 2 |^ ((m !) + k) ; :: thesis: contradiction
hence contradiction by a2, PEPIN:30; :: thesis: verum

end;

then 2 |^ k < 2 |^ ((m !) + k) by C1, XXREAL_0:1;
then A2: (2 |^ k) - 1 < (2 |^ ((m !) + k)) - 1 by XREAL_1:14;
k divides m ! by A0, NEWTON:41;
then k divides (m !) + k by NAT_D:8;
then (2 |^ k) - 1 divides (2 |^ ((m !) + k)) - 1 by NUMBER05:19;
then not (2 |^ ((m !) + k)) - 1 is prime by A1, A2;
hence (2 |^ ((m !) + k)) - 1 is not Prime ; :: thesis: verum