let p be Nat; for n0 being non zero Nat st (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) holds
n0 is perfect
let n0 be non zero Nat; ( (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:6
.=
((2 |^ p) - 1) * ((2 |^ p) - 1)
.=
((2 |^ p) - 1) ^2
by SQUARE_1:def 1
.=
(((2 |^ p) ^2) - ((2 * (2 |^ p)) * 1)) + (1 ^2)
by SQUARE_1:5
.=
(((2 |^ p) * (2 |^ p)) - (2 * (2 |^ p))) + (1 ^2)
by SQUARE_1:def 1
.=
(((2 |^ p) * (2 |^ p)) - (2 * (2 |^ p))) + (1 * 1)
by SQUARE_1:def 1
.=
((2 |^ p) * ((2 |^ p) - 2)) + 1
;
2 |^ p > p
by NEWTON:86;
then
2 |^ p >= p + 1
by NAT_1:13;
then A2:
(2 |^ p) - 2 >= (p + 1) - 2
by XREAL_1:9;
assume A3:
(2 |^ p) -' 1 is prime
; ( not n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) or n0 is perfect )
A4:
now not p <= 1assume A5:
p <= 1
;
contradiction end;
then A6:
p - 1 > 1 - 1
by XREAL_1:9;
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:9;
then A8:
p -' 2 = p - 2
by XREAL_0:def 2;
then A9:
p = (p -' 2) + 2
;
2 |^ p > p
by NEWTON:86;
then
2 |^ p > 1
by A4, XXREAL_0:2;
then A10:
(2 |^ p) - 1 > 1 - 1
by XREAL_1:9;
then A11:
(2 |^ p) - 1 = (2 |^ p) -' 1
by XREAL_0:def 2;
reconsider n2 = (2 |^ p) -' 1 as non zero Nat by A10, XREAL_0:def 2;
assume A12:
n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1)
; n0 is perfect
p -' 1 = (p -' 2) + 1
by A6, A8, XREAL_0:def 2;
then
2 |^ (p -' 1),n2 are_coprime
by A3, A11, A9, Th1, EULER_1:2;
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:28
.=
(sigma (n2 |^ 1)) * ((2 |^ p) -' 1)
by A7, A11
.=
(((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:89
.=
((2 |^ (p -' 1)) * 2) * ((2 |^ p) -' 1)
by NEWTON:6
.=
2 * n0
by A12
;
hence
n0 is perfect
; verum