let n, k, m be Nat; :: thesis: ( n > 1 & m > 1 implies Mersenne n <> k |^ m )
set M = Mersenne n;
assume Z0: ( n > 1 & m > 1 ) ; :: thesis: Mersenne n <> k |^ m
assume ZA: Mersenne n = k |^ m ; :: thesis: contradiction
WW: Mersenne n = (2 |^ n) - 1 by GR_CY_3:def 3;
then A2: k |^ m = (2 |^ n) - 1 by ZA;
FO: (k |^ m) + 1 = 2 |^ n by ZA, WW;
2 |^ n >= 2 |^ 1 by PREPOWER:93, Z0;
then (2 |^ n) - 1 >= (2 |^ 1) - 1 by XREAL_1:9;
then OO: Mersenne n >= 1 by WW;
O1: k <> 0

proof

assume k = 0 ; :: thesis: contradiction
then (2 |^ n) - 1 = 0 by A2, Z0, NEWTON:11;
hence contradiction by WW, OO; :: thesis: verum

end;

F1: n > 1 by Z0;
then F2: n >= 1 + 1 by NAT_1:13;
2 |^ n >= 2 |^ 2 by F2, PREPOWER:93;
then 2 |^ n >= 4 by POWER:60;
then (2 |^ n) - 1 >= 4 - 1 by XREAL_1:9;
then WA: Mersenne n >= 3 by WW;
R1: k is odd

proof

assume k is even ; :: thesis: contradiction
hence contradiction by A2, Z0; :: thesis: verum

end;

VV: m is odd

proof

assume G0: m is even ; :: thesis: contradiction
k |^ m is odd by R1;
then (k |^ m) mod 8 = 1 by G0, NEWTON06:74;
then ex t being Nat st
( k |^ m = (8 * t) + 1 & 1 < 8 ) by NAT_D:def 2;
then consider t being Nat such that
B1: k |^ m = (8 * t) + 1 ;
BB: (k |^ m) + 1 = 2 * ((4 * t) + 1) by B1;
A3: (k |^ m) + 1 = 2 |^ n by A2;
n >= 1 + 1 by F1, NAT_1:13;
then n - 1 >= (1 + 1) - 1 by XREAL_1:9;
then A5: n -' 1 = n - 1 by NAT_D:39;
n >= 3

proof

assume n < 3 ; :: thesis: contradiction
then n < 2 + 1 ;
then n <= 2 by NAT_1:13;
then not not n = 0 & ... & not n = 2 ;

per cases then ( n = 0 or n = 1 or n = 2 ) ;

suppose n = 0 ; :: thesis: contradiction

then Mersenne n = 0 by GR_CY_3:16;
hence contradiction by WA; :: thesis: verum

end;

suppose n = 1 ; :: thesis: contradiction

then Mersenne n = 1 by GR_CY_3:17;
hence contradiction by WA; :: thesis: verum

end;

suppose n = 2 ; :: thesis: contradiction

then Y1: Mersenne n = 3 by GR_CY_3:18;
Y2: Mersenne n = k |^ m by ZA;
then Y9: 3 = k |^ m by Y1;
Y8: m > 1 by Z0;
Y3: m >= 1 + 1 by Z0, NAT_1:13;

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

suppose k <= 1 ; :: thesis: contradiction

then k < 1 + 1 by NAT_1:13;
then ( k = 0 or k = 1 ) by NAT_1:23;
hence contradiction by Y9, Y8, NEWTON:11; :: thesis: verum

end;

suppose Y5: k > 1 ; :: thesis: contradiction

then Y7: k >= 1 + 1 by NAT_1:13;
Y6: k |^ m >= k |^ 2 by Y3, Y5, PREPOWER:93;
k to_power 2 >= 2 to_power 2 by Y7, PREPOWER:9;
then k |^ 2 >= 4 by POWER:60;
hence contradiction by Y1, Y2, Y6, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

end;

then n - 1 >= 3 - 1 by XREAL_1:9;
then a4: (n -' 1) - 1 >= 2 - 1 by A5, XREAL_1:9;
(n -' 2) + 1 = ((n -' 1) -' 1) + 1 by NAT_D:45
.= n -' 1 by a4, NAT_D:43 ;
then U1: n -' 1 = (n -' 2) + 1 ;
n = (n -' 1) + 1 by F1, XREAL_1:235;
then 2 |^ n = (2 |^ (n -' 1)) * 2 by NEWTON:6
.= ((2 |^ (n -' 2)) * 2) * 2 by NEWTON:6, U1
.= 4 * (2 |^ (n -' 2)) ;
then 2 * 2 divides 2 * ((4 * t) + 1) by A3, BB;
then T2: 2 divides (4 * t) + 1 by GROUP_22:1;
(2 * 2) * t is even ;
hence contradiction by T2; :: thesis: verum

end;

ZE: k <> 1

proof

assume k = 1 ; :: thesis: contradiction
hence contradiction by WW, WA, A2; :: thesis: verum

end;

U1: ( k > 0 & k <> 1 ) by O1, ZE;
consider i being Nat such that
J1: m = (2 * i) + 1 by VV, ABIAN:9;
k + 1 divides (k |^ ((2 * i) + 1)) + (1 |^ ((2 * i) + 1)) by NEWTON01:35;
then C1: k + 1 divides (k |^ m) + 1 by J1;
set R = ((k |^ m) + 1) div (k + 1);
FG: (k |^ m) + 1 = (k + 1) * (((k |^ m) + 1) div (k + 1)) by C1;
then FZ: ((k |^ m) + 1) div (k + 1) divides 2 |^ n by FO;
set m1 = m -' 1;
m >= 1 + 1 by Z0, NAT_1:13;
then m - 1 >= 2 - 1 by XREAL_1:9;
then GT: m - 1 >= 1 ;
then CI: m = (m -' 1) + 1 by NAT_D:43;
CP: m -' 1 = m - 1 by GT, XREAL_0:def 2;
m is odd by VV;
then CL: (- 1) |^ ((m -' 1) + 1) = - 1 by CP;
(k |^ ((m -' 1) + 1)) - ((- 1) |^ ((m -' 1) + 1)) = (k - (- 1)) * (Sum ((k,(- 1)) Subnomial (m -' 1))) by NEWTON04:51;
then (k |^ ((m -' 1) + 1)) - ((- 1) |^ ((m -' 1) + 1)) = (k + 1) * (Sum ((k,(- 1)) Subnomial (m -' 1))) ;
then (k |^ m) + 1 = (k + 1) * (Sum ((k,(- 1)) Subnomial (m -' 1))) by CL, CI;
then FD: (k + 1) * (((k |^ m) + 1) div (k + 1)) = (k + 1) * (Sum ((k,(- 1)) Subnomial (m -' 1))) ;
HU: ((k |^ m) + 1) div (k + 1) = Sum ((k,(- 1)) Subnomial (m -' 1)) by FD, XCMPLX_1:5;
HJ: len ((k,(- 1)) Subnomial (m -' 1)) = m by CI, NEWTON04:def 2;
then D2: len ((k,(- 1)) Subnomial (m -' 1)) is odd by VV;
set SS = (k,(- 1)) Subnomial (m -' 1);
SE: for i, l, j being Nat st i in dom ((k,(- 1)) Subnomial (m -' 1)) & j = i - 1 & l = (m -' 1) - j holds
((k,(- 1)) Subnomial (m -' 1)) . i = (k |^ l) * ((- 1) |^ j) by NEWTON04:def 2;
D1: for i being Nat st i in dom ((k,(- 1)) Subnomial (m -' 1)) holds
((k,(- 1)) Subnomial (m -' 1)) . i is odd

proof

let i be Nat; :: thesis: ( i in dom ((k,(- 1)) Subnomial (m -' 1)) implies ((k,(- 1)) Subnomial (m -' 1)) . i is odd )
assume UU: i in dom ((k,(- 1)) Subnomial (m -' 1)) ; :: thesis: ((k,(- 1)) Subnomial (m -' 1)) . i is odd
then ( 1 <= i & i <= len ((k,(- 1)) Subnomial (m -' 1)) ) by FINSEQ_3:25;
then UY: ( 1 <= i & i <= m ) by HJ;
then reconsider j = i - 1 as Nat ;
i - 1 <= m - 1 by UY, XREAL_1:9;
then (m -' 1) - j >= j - j by CP, XREAL_1:9;
then reconsider l = (m -' 1) - j as Nat by INT_1:3;
DS: ((k,(- 1)) Subnomial (m -' 1)) . i = (k |^ l) * ((- 1) |^ j) by UU, SE;
0 is even ;
then 0 - 1 is odd ;
hence ((k,(- 1)) Subnomial (m -' 1)) . i is odd by DS, R1; :: thesis: verum

end;

((k |^ m) + 1) div (k + 1) is odd by D1, D2, HU, OddSum;
then ((k |^ m) + 1) div (k + 1) = 1 by FZ, OddEven;
then 2 |^ n = k + 1 by FG, FO;
then k to_power m = k to_power 1 by A2;
hence contradiction by Z0, U1, POWER:50; :: thesis: verum