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) )

2 |^ (k9 + 1) > k9 + 1 by NEWTON:86;

then A7: (2 |^ (k9 + 1)) - 1 > (k9 + 1) - 1 by 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 B01: k9 + 1 >= 1 + 1 by XREAL_1:7;

2 |^ (k9 + 1) > k9 + 1 by NEWTON:86;

then 2 |^ (k9 + 1) > 2 by B01, 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

( (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) )

2 |^ (k9 + 1) > k9 + 1 by NEWTON:86;

then A7: (2 |^ (k9 + 1)) - 1 > (k9 + 1) - 1 by 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 B01: k9 + 1 >= 1 + 1 by XREAL_1:7;

2 |^ (k9 + 1) > k9 + 1 by NEWTON:86;

then 2 |^ (k9 + 1) > 2 by B01, 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