theorem :: XPRIMES0:420

not 420 is prime