let n0 be non zero natural number ; :: thesis: ( n0 is even & n0 is perfect implies ex p being natural number st
( (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) ) )
assume n0 is even ; :: thesis: ( not n0 is perfect or ex p being natural number st
( (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) ) )
then consider k', n' being natural number such that
A1: ( not n' is even & k' > 0 & n0 = (2 |^ k') * n' ) by Th2;
assume n0 is perfect ; :: thesis: ex p being natural number st
( (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) )
then A2: sigma n0 = 2 * n0 by Def6;
k' >= 0 + 1 by A1, NAT_1:13;
then A3: k' + 1 >= 1 + 1 by XREAL_1:9;
set p = k' + 1;
A4: (k' + 1) - 1 = (k' + 1) -' 1 by XREAL_0:def 2;
take k' + 1 ; :: thesis: ( (2 |^ (k' + 1)) -' 1 is prime & n0 = (2 |^ ((k' + 1) -' 1)) * ((2 |^ (k' + 1)) -' 1) )
reconsider n2 = n' as non zero natural number by A1;
A5: (2 |^ (k' + 1)) - 1 > (k' + 1) - 1 by NEWTON:105, XREAL_1:16;
A6: (2 |^ (k' + 1)) - 1 = (2 |^ (k' + 1)) -' 1 by A5, XREAL_0:def 2;
sigma (2 |^ ((k' + 1) -' 1)) = ((2 |^ (((k' + 1) -' 1) + 1)) - 1) / (2 - 1) by INT_2:44, Th30
.= (2 |^ (k' + 1)) - 1 by A4 ;
then A7: ((2 |^ (k' + 1)) - 1) * (sigma n') = (2 * (2 |^ ((k' + 1) -' 1))) * n' by A4, Th37, A1, Th3, A2
.= (2 |^ (k' + 1)) * n' by A4, NEWTON:11 ;
then A8: (2 |^ (k' + 1)) -' 1 divides (2 |^ (k' + 1)) * n2 by A6, INT_1:def 9;
(2 |^ (k' + 1)) - 1 = ((2 |^ (((k' + 1) -' 1) + 1)) - 2) + 1 by A4
.= (((2 |^ ((k' + 1) -' 1)) * 2) - 2) + 1 by NEWTON:11
.= (2 * ((2 |^ ((k' + 1) -' 1)) - 1)) + 1 ;
then (2 |^ (k' + 1)) -' 1 divides n2 by A8, EULER_1:14, A6, Th3;
then consider n'' being natural number such that
A9: n' = ((2 |^ (k' + 1)) -' 1) * n'' by NAT_D:def 3;
A10: n'' divides n' by A9, NAT_D:def 3;
2 |^ (k' + 1) > 2 by NEWTON:105, A3, XXREAL_0:2;
then (2 |^ (k' + 1)) - 1 > 2 - 1 by XREAL_1:16;
then A11: ((2 |^ (k' + 1)) -' 1) * n2 > 1 * n2 by A6, XREAL_1:70;
(sigma n') * ((2 |^ (k' + 1)) - 1) = ((2 |^ (k' + 1)) * n'') * ((2 |^ (k' + 1)) - 1) by A6, A9, A7;
then sigma n2 = (((2 |^ (k' + 1)) - 1) * n'') + n'' by A5, XCMPLX_1:5
.= n' + n'' by A5, XREAL_0:def 2, A9 ;
then A12: ( n'' = 1 & n' is prime ) by Th33, A10, A11, A9;
hence (2 |^ (k' + 1)) -' 1 is prime by A9; :: thesis: n0 = (2 |^ ((k' + 1) -' 1)) * ((2 |^ (k' + 1)) -' 1)
thus n0 = (2 |^ ((k' + 1) -' 1)) * ((2 |^ (k' + 1)) -' 1) by A9, A12, A1, A4; :: thesis: verum