let p be Nat; :: thesis: for n0 being non zero Nat st (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) holds
n0 is perfect
let n0 be non zero Nat; :: thesis: ( (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) implies n0 is perfect )
set n1 = 2 |^ (p -' 1);
set k = p -' 2;
A1: ((2 |^ p) - 1) |^ 2 = ((2 |^ p) - 1) |^ (1 + 1)
.= (((2 |^ p) - 1) |^ 1) * ((2 |^ p) - 1) by NEWTON:6
.= ((2 |^ p) - 1) * ((2 |^ p) - 1)
.= ((2 |^ p) - 1) ^2 by SQUARE_1:def 1
.= (((2 |^ p) ^2) - ((2 * (2 |^ p)) * 1)) + (1 ^2) by SQUARE_1:5
.= (((2 |^ p) * (2 |^ p)) - (2 * (2 |^ p))) + (1 ^2) by SQUARE_1:def 1
.= (((2 |^ p) * (2 |^ p)) - (2 * (2 |^ p))) + (1 * 1) by SQUARE_1:def 1
.= ((2 |^ p) * ((2 |^ p) - 2)) + 1 ;
2 |^ p > p by NEWTON:86;
then 2 |^ p >= p + 1 by NAT_1:13;
then A2: (2 |^ p) - 2 >= (p + 1) - 2 by XREAL_1:9;
assume A3: (2 |^ p) -' 1 is prime ; :: thesis: ( not n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) or n0 is perfect )

A4: now :: thesis: not p <= 1

assume A5: p <= 1 ; :: thesis: contradiction

per cases ( p = 0 or p = 1 ) by A5, NAT_1:25;

suppose p = 0 ; :: thesis: contradiction

then (2 |^ p) -' 1 = 1 -' 1 by NEWTON:4
.= 1 - 1 by XREAL_0:def 2
.= 0 ;
hence contradiction by A3; :: thesis: verum

end;

suppose p = 1 ; :: thesis: contradiction

then (2 |^ p) -' 1 = 2 -' 1
.= 2 - 1 by XREAL_0:def 2
.= 1 ;
hence contradiction by A3, INT_2:def 4; :: thesis: verum

end;

end;

end;

then A6: p - 1 > 1 - 1 by XREAL_1:9;
then A7: p -' 1 = p - 1 by XREAL_0:def 2;
p >= 1 + 1 by A4, NAT_1:13;
then p - 2 >= 2 - 2 by XREAL_1:9;
then A8: p -' 2 = p - 2 by XREAL_0:def 2;
then A9: p = (p -' 2) + 2 ;
2 |^ p > p by NEWTON:86;
then 2 |^ p > 1 by A4, XXREAL_0:2;
then A10: (2 |^ p) - 1 > 1 - 1 by XREAL_1:9;
then A11: (2 |^ p) - 1 = (2 |^ p) -' 1 by XREAL_0:def 2;
reconsider n2 = (2 |^ p) -' 1 as non zero Nat by A10, XREAL_0:def 2;
assume A12: n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) ; :: thesis: n0 is perfect
p -' 1 = (p -' 2) + 1 by A6, A8, XREAL_0:def 2;
then 2 |^ (p -' 1),n2 are_coprime by A3, A11, A9, Th1, EULER_1:2;
then sigma n0 = (sigma (2 |^ (p -' 1))) * (sigma n2) by A12, Th37
.= (((2 |^ ((p -' 1) + 1)) - 1) / (2 - 1)) * (sigma n2) by Th30, INT_2:28
.= (sigma (n2 |^ 1)) * ((2 |^ p) -' 1) by A7, A11
.= (((n2 |^ (1 + 1)) - 1) / (n2 - 1)) * ((2 |^ p) -' 1) by A3, Th30
.= (2 |^ ((p -' 1) + 1)) * ((2 |^ p) -' 1) by A6, A7, A11, A1, A2, XCMPLX_1:89
.= ((2 |^ (p -' 1)) * 2) * ((2 |^ p) -' 1) by NEWTON:6
.= 2 * n0 by A12 ;
hence n0 is perfect ; :: thesis: verum