let p be natural number ; :: thesis: for n0 being natural non zero number st (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) holds
n0 is perfect
let n0 be natural non zero number ; :: 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:11
.= ((2 |^ p) - 1) * ((2 |^ p) - 1) by NEWTON:10
.= ((2 |^ p) - 1) ^2 by SQUARE_1:def 3
.= (((2 |^ p) ^2 ) - ((2 * (2 |^ p)) * 1)) + (1 ^2 ) by SQUARE_1:64
.= (((2 |^ p) * (2 |^ p)) - (2 * (2 |^ p))) + (1 ^2 ) by SQUARE_1:def 3
.= (((2 |^ p) * (2 |^ p)) - (2 * (2 |^ p))) + (1 * 1) by SQUARE_1:def 3
.= ((2 |^ p) * ((2 |^ p) - 2)) + 1 ;
2 |^ p > p by NEWTON:105;
then 2 |^ p >= p + 1 by NAT_1:13;
then A2: (2 |^ p) - 2 >= (p + 1) - 2 by XREAL_1:11;
assume A3: (2 |^ p) -' 1 is prime ; :: thesis: ( not n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) or n0 is perfect )

A4: now

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

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

suppose p = 0 ; :: thesis: contradiction

then (2 |^ p) -' 1 = 1 -' 1 by NEWTON:9
.= 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 by NEWTON:10
.= 2 - 1 by XREAL_0:def 2
.= 1 ;
hence contradiction by A3, INT_2:def 5; :: thesis: verum

end;

end;

end;

then A6: p - 1 > 1 - 1 by XREAL_1:11;
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:11;
then A8: p -' 2 = p - 2 by XREAL_0:def 2;
then A9: p = (p -' 2) + 2 ;
2 |^ p > 1 by A4, NEWTON:105, XXREAL_0:2;
then A10: (2 |^ p) - 1 > 1 - 1 by XREAL_1:11;
then A11: (2 |^ p) - 1 = (2 |^ p) -' 1 by XREAL_0:def 2;
reconsider n2 = (2 |^ p) -' 1 as natural non zero number 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_relative_prime by A3, A11, A9, Th1, EULER_1:3;
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:44
.= (sigma (n2 |^ 1)) * ((2 |^ p) -' 1) by A7, A11, NEWTON:10
.= (((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:90
.= ((2 |^ (p -' 1)) * 2) * ((2 |^ p) -' 1) by NEWTON:11
.= 2 * n0 by A12 ;
hence n0 is perfect by Def6; :: thesis: verum