consider k being Nat, l being odd Nat such that
A1:
n = l * (2 |^ k)
by Th3;
A2: (n * (2 |^ n)) + 1 =
(l * ((2 |^ k) * (2 |^ n))) + 1
by A1
.=
(l * (2 |^ (k + n))) + 1
by NEWTON:8
;
(2 |^ k) + 1 > 0 + 1
by XREAL_1:6;
then
2 |^ k >= 1
by NAT_1:13;
then A3:
(2 |^ k) * l >= 1 * l
by XREAL_1:64;
A4:
2 |^ (k + n) > k + n
by NEWTON:86;
k + n >= n
by NAT_1:11;
then
k + n >= l
by A1, A3, XXREAL_0:2;
then
2 |^ (k + n) > l
by A4, XXREAL_0:2;
hence
CullenNumber n is Proth
by A2; verum