let p be odd Prime; :: thesis: { n where n is Nat : p divides CullenNumber n } is infinite
set S = { n where n is Nat : p divides CullenNumber n } ;
deffunc H₃( Nat) -> set = (p - 1) * (($1 * p) + 1);
consider f being ManySortedSet of NAT such that
A1: for i being Element of NAT holds f . i = H₃(i) from PBOOLE:sch 5();
set R = rng f;
A2: dom f = NAT by PARTFUN1:def 2;
A3: rng f c= { n where n is Nat : p divides CullenNumber n }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in { n where n is Nat : p divides CullenNumber n } )
assume x in rng f ; :: thesis: x in { n where n is Nat : p divides CullenNumber n }
then consider m being object such that
A4: m in dom f and
A5: x = f . m by FUNCT_1:def 3;
reconsider m = m as Element of NAT by A4, PARTFUN1:def 2;
A6: f . m = H₃(m) by A1;
set n = (p - 1) * ((m * p) + 1);
p divides CullenNumber ((p - 1) * ((m * p) + 1)) by Th50;
hence x in { n where n is Nat : p divides CullenNumber n } by A5, A6; :: thesis: verum

end;

for m being Nat ex N being Nat st
( N >= m & N in rng f )

proof

let m be Nat; :: thesis: ex N being Nat st
( N >= m & N in rng f )
take n = H₃(m + 1); :: thesis: ( n >= m & n in rng f )
A7: m + 0 <= m + 1 by XREAL_1:6;
1 < p by INT_2:def 4;
then A8: (m + 1) * 1 <= (m + 1) * p by XREAL_1:64;
A9: ((m + 1) * p) + 0 <= ((m + 1) * p) + 1 by XREAL_1:6;
1 <= p - 1 by INT_2:def 4, INT_1:52;
then 1 * (((m + 1) * p) + 1) <= (p - 1) * (((m + 1) * p) + 1) by XREAL_1:64;
hence n >= m by A7, A8, A9, Th2; :: thesis: n in rng f
f . (m + 1) = n by A1;
hence n in rng f by A2, FUNCT_1:def 3; :: thesis: verum

end;

hence { n where n is Nat : p divides CullenNumber n } is infinite by A3, PYTHTRIP:9; :: thesis: verum