let p be natural number ; :: thesis: for n0 being non zero natural number st (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) holds
n0 is perfect
let n0 be non zero natural number ; :: thesis: ( (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) implies n0 is perfect )
assume A1: (2 |^ p) -' 1 is prime ; :: thesis: ( not n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) or n0 is perfect )
assume A2: n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) ; :: thesis: n0 is perfect

A3: now

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

per cases ( p = 0 or p = 1 ) by A4, 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 A1; :: 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 A1, INT_2:def 5; :: thesis: verum

end;

end;

end;

then A5: p - 1 > 1 - 1 by XREAL_1:11;
then A6: p -' 1 = p - 1 by XREAL_0:def 2;
set n1 = 2 |^ (p -' 1);
A7: 2 |^ p > p by NEWTON:105;
2 |^ p > 1 by A3, XXREAL_0:2, NEWTON:105;
then A8: (2 |^ p) - 1 > 1 - 1 by XREAL_1:11;
then A9: (2 |^ p) - 1 = (2 |^ p) -' 1 by XREAL_0:def 2;
reconsider n2 = (2 |^ p) -' 1 as non zero natural number by A8, XREAL_0:def 2;
set k = p -' 2;
p >= 1 + 1 by A3, NAT_1:13;
then p - 2 >= 2 - 2 by XREAL_1:11;
then p -' 2 = p - 2 by XREAL_0:def 2;
then ( p -' 1 = (p -' 2) + 1 & p = (p -' 2) + 2 ) by A5, XREAL_0:def 2;
then A10: 2 |^ (p -' 1),n2 are_relative_prime by A1, EULER_1:3, A9, Th1;
A11: ((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 + 1 by A7, NAT_1:13;
then A12: (2 |^ p) - 2 >= (p + 1) - 2 by XREAL_1:11;
sigma n0 = (sigma (2 |^ (p -' 1))) * (sigma n2) by A2, A10, Th37
.= (((2 |^ ((p -' 1) + 1)) - 1) / (2 - 1)) * (sigma n2) by INT_2:44, Th30
.= (sigma (n2 |^ 1)) * ((2 |^ p) -' 1) by A6, A9, NEWTON:10
.= (((n2 |^ (1 + 1)) - 1) / (n2 - 1)) * ((2 |^ p) -' 1) by A1, Th30
.= (2 |^ ((p -' 1) + 1)) * ((2 |^ p) -' 1) by A6, A9, A12, A5, XCMPLX_1:90, A11
.= ((2 |^ (p -' 1)) * 2) * ((2 |^ p) -' 1) by NEWTON:11
.= 2 * n0 by A2 ;
hence n0 is perfect by Def6; :: thesis: verum