theorem :: XPRIMES0:825

not 825 is prime