let k, n be Nat; :: thesis: for p being odd Prime st n = (p - 1) * ((k * p) + 1) holds
p divides CullenNumber n
let p be odd Prime; :: thesis: ( n = (p - 1) * ((k * p) + 1) implies p divides CullenNumber n )
assume A1: n = (p - 1) * ((k * p) + 1) ; :: thesis: p divides CullenNumber n
then A2: (2 |^ n) mod p = 1 by Th49;
p - 1 < p - 0 by XREAL_1:15;
then A3: (p - 1) mod p = p - 1 by NAT_D:24;
A4: ((k * p) + 1) mod p = 1 mod p by NAT_D:21
.= 1 by INT_2:def 4, NAT_D:14 ;
A5: ((p - 1) * ((k * p) + 1)) mod p = (((p - 1) mod p) * (((k * p) + 1) mod p)) mod p by NAT_D:67
.= (p - 1) mod p by A4 ;
(n * (2 |^ n)) mod p = ((n mod p) * ((2 |^ n) mod p)) mod p by NAT_D:67;
then (CullenNumber n) mod p = ((p - 1) + 1) mod p by A1, A2, A3, A5, NAT_D:22
.= 0 by NAT_D:25 ;
hence p divides CullenNumber n by INT_1:62; :: thesis: verum