theorem :: PEPIN:45

for n, p, q, k1, k2 being Nat st p is prime & q is prime & p <> q & n = p * q & k1, Euler n are_coprime & (k1 * k2) mod (Euler n) = 1 holds
for m being Element of NAT st m < n holds
Crypto ((Crypto (m,n,k1)),n,k2) = m