let n0 be non zero Nat; :: thesis: ( n0 is even & n0 is perfect implies ex p being Nat 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 Nat st
( (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) ) )
then consider k9, n9 being Nat such that
A1: n9 is odd and
A2: k9 > 0 and
A3: n0 = (2 |^ k9) * n9 by Th2;
reconsider n2 = n9 as non zero Nat by A1;
set p = k9 + 1;
A4: (k9 + 1) - 1 = (k9 + 1) -' 1 by XREAL_0:def 2;
then A5: (2 |^ (k9 + 1)) - 1 = ((2 |^ (((k9 + 1) -' 1) + 1)) - 2) + 1
.= (((2 |^ ((k9 + 1) -' 1)) * 2) - 2) + 1 by NEWTON:6
.= (2 * ((2 |^ ((k9 + 1) -' 1)) - 1)) + 1 ;
assume n0 is perfect ; :: thesis: ex p being Nat st
( (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) )
then A6: sigma n0 = 2 * n0 ;
take k9 + 1 ; :: thesis: ( (2 |^ (k9 + 1)) -' 1 is prime & n0 = (2 |^ ((k9 + 1) -' 1)) * ((2 |^ (k9 + 1)) -' 1) )
A7: (2 |^ (k9 + 1)) - 1 > (k9 + 1) - 1 by NEWTON:86, XREAL_1:14;
then A8: (2 |^ (k9 + 1)) - 1 = (2 |^ (k9 + 1)) -' 1 by XREAL_0:def 2;
sigma (2 |^ ((k9 + 1) -' 1)) = ((2 |^ (((k9 + 1) -' 1) + 1)) - 1) / (2 - 1) by Th30, INT_2:28
.= (2 |^ (k9 + 1)) - 1 by A4 ;
then A9: ((2 |^ (k9 + 1)) - 1) * (sigma n9) = (2 * (2 |^ ((k9 + 1) -' 1))) * n9 by A1, A3, A6, A4, Th3, Th37
.= (2 |^ (k9 + 1)) * n9 by A4, NEWTON:6 ;
then (2 |^ (k9 + 1)) -' 1 divides (2 |^ (k9 + 1)) * n2 by A8, INT_1:def 3;
then (2 |^ (k9 + 1)) -' 1 divides n2 by A8, A5, Th3, EULER_1:13;
then consider n99 being Nat such that
A10: n9 = ((2 |^ (k9 + 1)) -' 1) * n99 by NAT_D:def 3;
(sigma n9) * ((2 |^ (k9 + 1)) - 1) = ((2 |^ (k9 + 1)) * n99) * ((2 |^ (k9 + 1)) - 1) by A8, A9, A10;
then A11: sigma n2 = (((2 |^ (k9 + 1)) - 1) * n99) + n99 by A7, XCMPLX_1:5
.= n9 + n99 by A7, A10, XREAL_0:def 2 ;
A12: n99 divides n9 by A10, NAT_D:def 3;
k9 >= 0 + 1 by A2, NAT_1:13;
then k9 + 1 >= 1 + 1 by XREAL_1:7;
then 2 |^ (k9 + 1) > 2 by NEWTON:86, XXREAL_0:2;
then A13: (2 |^ (k9 + 1)) - 1 > 2 - 1 by XREAL_1:14;
then ((2 |^ (k9 + 1)) -' 1) * n2 > 1 * n2 by A8, XREAL_1:68;
then A14: n99 = 1 by A10, A12, A11, Th33;
hence (2 |^ (k9 + 1)) -' 1 is prime by A8, A10, A12, A13, A11, Th33; :: thesis: n0 = (2 |^ ((k9 + 1) -' 1)) * ((2 |^ (k9 + 1)) -' 1)
thus n0 = (2 |^ ((k9 + 1) -' 1)) * ((2 |^ (k9 + 1)) -' 1) by A3, A4, A10, A14; :: thesis: verum