Metamath Proof Explorer


Table of Contents - 6.2.1. Elementary properties

Remark: to represent odd prime numbers, i.e., all prime numbers except , the idiom is used. It is a little bit shorter than . Both representations can be converted into each other by eldifsn.

  1. cprime
  2. df-prm
  3. isprm
  4. prmnn
  5. prmz
  6. prmssnn
  7. prmex
  8. 0nprm
  9. 1nprm
  10. 1idssfct
  11. isprm2lem
  12. isprm2
  13. isprm3
  14. isprm4
  15. prmind2
  16. prmind
  17. dvdsprime
  18. nprm
  19. nprmi
  20. dvdsnprmd
  21. prm2orodd
  22. 2prm
  23. 2mulprm
  24. 3prm
  25. 4nprm
  26. prmuz2
  27. prmgt1
  28. prmm2nn0
  29. oddprmgt2
  30. oddprmge3
  31. ge2nprmge4
  32. sqnprm
  33. dvdsprm
  34. exprmfct
  35. prmdvdsfz
  36. nprmdvds1
  37. isprm5
  38. isprm7
  39. maxprmfct
  40. divgcdodd