Metamath Proof Explorer

Table of Contents - 6.2. Elementary prime number theory

1. Elementary properties
   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
2. Coprimality and Euclid's lemma (cont.)
   1. coprm
   2. prmrp
   3. euclemma
   4. isprm6
   5. prmdvdsexp
   6. prmdvdsexpb
   7. prmdvdsexpr
   8. prmdvdssq
   9. prmdvdssqOLD
   10. prmexpb
   11. prmfac1
   12. rpexp
   13. rpexp1i
   14. rpexp12i
   15. prmndvdsfaclt
   16. prmdvdsncoprmbd
   17. ncoprmlnprm
   18. cncongrprm
   19. isevengcd2
   20. isoddgcd1
   21. 3lcm2e6
3. Properties of the canonical representation of a rational
   1. cnumer
   2. cdenom
   3. df-numer
   4. df-denom
   5. qnumval
   6. qdenval
   7. qnumdencl
   8. qnumcl
   9. qdencl
   10. fnum
   11. fden
   12. qnumdenbi
   13. qnumdencoprm
   14. qeqnumdivden
   15. qmuldeneqnum
   16. divnumden
   17. divdenle
   18. qnumgt0
   19. qgt0numnn
   20. nn0gcdsq
   21. zgcdsq
   22. numdensq
   23. numsq
   24. densq
   25. qden1elz
   26. zsqrtelqelz
   27. nonsq
4. Euler's theorem
   1. codz
   2. cphi
   3. df-odz
   4. df-phi
   5. phival
   6. phicl2
   7. phicl
   8. phibndlem
   9. phibnd
   10. phicld
   11. phi1
   12. dfphi2
   13. hashdvds
   14. phiprmpw
   15. phiprm
   16. crth
   17. phimullem
   18. phimul
   19. eulerthlem1
   20. eulerthlem2
   21. eulerth
   22. fermltl
   23. prmdiv
   24. prmdiveq
   25. prmdivdiv
   26. hashgcdlem
   27. hashgcdeq
   28. phisum
   29. odzval
   30. odzcllem
   31. odzcl
   32. odzid
   33. odzdvds
   34. odzphi
5. Arithmetic modulo a prime number
   1. modprm1div
   2. m1dvdsndvds
   3. modprminv
   4. modprminveq
   5. vfermltl
   6. vfermltlALT
   7. powm2modprm
   8. reumodprminv
   9. modprm0
   10. nnnn0modprm0
   11. modprmn0modprm0
6. Pythagorean Triples
   1. coprimeprodsq
   2. coprimeprodsq2
   3. oddprm
   4. nnoddn2prm
   5. oddn2prm
   6. nnoddn2prmb
   7. prm23lt5
   8. prm23ge5
   9. pythagtriplem1
   10. pythagtriplem2
   11. pythagtriplem3
   12. pythagtriplem4
   13. pythagtriplem10
   14. pythagtriplem6
   15. pythagtriplem7
   16. pythagtriplem8
   17. pythagtriplem9
   18. pythagtriplem11
   19. pythagtriplem12
   20. pythagtriplem13
   21. pythagtriplem14
   22. pythagtriplem15
   23. pythagtriplem16
   24. pythagtriplem17
   25. pythagtriplem18
   26. pythagtriplem19
   27. pythagtrip
   28. iserodd
7. The prime count function
   1. cpc
   2. df-pc
   3. pclem
   4. pcprecl
   5. pcprendvds
   6. pcprendvds2
   7. pcpre1
   8. pcpremul
   9. pcval
   10. pceulem
   11. pceu
   12. pczpre
   13. pczcl
   14. pccl
   15. pccld
   16. pcmul
   17. pcdiv
   18. pcqmul
   19. pc0
   20. pc1
   21. pcqcl
   22. pcqdiv
   23. pcrec
   24. pcexp
   25. pcxcl
   26. pcge0
   27. pczdvds
   28. pcdvds
   29. pczndvds
   30. pcndvds
   31. pczndvds2
   32. pcndvds2
   33. pcdvdsb
   34. pcelnn
   35. pceq0
   36. pcidlem
   37. pcid
   38. pcneg
   39. pcabs
   40. pcdvdstr
   41. pcgcd1
   42. pcgcd
   43. pc2dvds
   44. pc11
   45. pcz
   46. pcprmpw2
   47. pcprmpw
   48. dvdsprmpweq
   49. dvdsprmpweqnn
   50. dvdsprmpweqle
   51. difsqpwdvds
   52. pcaddlem
   53. pcadd
   54. pcadd2
   55. pcmptcl
   56. pcmpt
   57. pcmpt2
   58. pcmptdvds
   59. pcprod
   60. sumhash
   61. fldivp1
   62. pcfaclem
   63. pcfac
   64. pcbc
   65. qexpz
   66. expnprm
   67. oddprmdvds
8. Pocklington's theorem
   1. prmpwdvds
   2. pockthlem
   3. pockthg
   4. pockthi
9. Infinite primes theorem
   1. unbenlem
   2. unben
   3. infpnlem1
   4. infpnlem2
   5. infpn
   6. infpn2
   7. prmunb
   8. prminf
10. Sum of prime reciprocals
    1. prmreclem1
    2. prmreclem2
    3. prmreclem3
    4. prmreclem4
    5. prmreclem5
    6. prmreclem6
    7. prmrec
11. Fundamental theorem of arithmetic
    1. 1arithlem1
    2. 1arithlem2
    3. 1arithlem3
    4. 1arithlem4
    5. 1arith
    6. 1arith2
12. Lagrange's four-square theorem
    1. cgz
    2. df-gz
    3. elgz
    4. gzcn
    5. zgz
    6. igz
    7. gznegcl
    8. gzcjcl
    9. gzaddcl
    10. gzmulcl
    11. gzreim
    12. gzsubcl
    13. gzabssqcl
    14. 4sqlem5
    15. 4sqlem6
    16. 4sqlem7
    17. 4sqlem8
    18. 4sqlem9
    19. 4sqlem10
    20. 4sqlem1
    21. 4sqlem2
    22. 4sqlem3
    23. 4sqlem4a
    24. 4sqlem4
    25. mul4sqlem
    26. mul4sq
    27. 4sqlem11
    28. 4sqlem12
    29. 4sqlem13
    30. 4sqlem14
    31. 4sqlem15
    32. 4sqlem16
    33. 4sqlem17
    34. 4sqlem18
    35. 4sqlem19
    36. 4sq
13. Van der Waerden's theorem
    1. cvdwa
    2. cvdwm
    3. cvdwp
    4. df-vdwap
    5. df-vdwmc
    6. df-vdwpc
    7. vdwapfval
    8. vdwapf
    9. vdwapval
    10. vdwapun
    11. vdwapid1
    12. vdwap0
    13. vdwap1
    14. vdwmc
    15. vdwmc2
    16. vdwpc
    17. vdwlem1
    18. vdwlem2
    19. vdwlem3
    20. vdwlem4
    21. vdwlem5
    22. vdwlem6
    23. vdwlem7
    24. vdwlem8
    25. vdwlem9
    26. vdwlem10
    27. vdwlem11
    28. vdwlem12
    29. vdwlem13
    30. vdw
    31. vdwnnlem1
    32. vdwnnlem2
    33. vdwnnlem3
    34. vdwnn
14. Ramsey's theorem
    1. cram
    2. ramtlecl
    3. df-ram
    4. hashbcval
    5. hashbccl
    6. hashbcss
    7. hashbc0
    8. hashbc2
    9. 0hashbc
    10. ramval
    11. ramcl2lem
    12. ramtcl
    13. ramtcl2
    14. ramtub
    15. ramub
    16. ramub2
    17. rami
    18. ramcl2
    19. ramxrcl
    20. ramubcl
    21. ramlb
    22. 0ram
    23. 0ram2
    24. ram0
    25. 0ramcl
    26. ramz2
    27. ramz
    28. ramub1lem1
    29. ramub1lem2
    30. ramub1
    31. ramcl
    32. ramsey
15. Primorial function
    1. cprmo
    2. df-prmo
    3. prmoval
    4. prmocl
    5. prmone0
    6. prmo0
    7. prmo1
    8. prmop1
    9. prmonn2
    10. prmo2
    11. prmo3
    12. prmdvdsprmo
    13. prmdvdsprmop
    14. fvprmselelfz
    15. fvprmselgcd1
    16. prmolefac
    17. prmodvdslcmf
    18. prmolelcmf
16. Prime gaps
    1. prmgaplem1
    2. prmgaplem2
    3. prmgaplcmlem1
    4. prmgaplcmlem2
    5. prmgaplem3
    6. prmgaplem4
    7. prmgaplem5
    8. prmgaplem6
    9. prmgaplem7
    10. prmgaplem8
    11. prmgap
    12. prmgaplcm
    13. prmgapprmolem
    14. prmgapprmo
17. Decimal arithmetic (cont.)
    1. dec2dvds
    2. dec5dvds
    3. dec5dvds2
    4. dec5nprm
    5. dec2nprm
    6. modxai
    7. mod2xi
    8. modxp1i
    9. mod2xnegi
    10. modsubi
    11. gcdi
    12. gcdmodi
    13. decexp2
    14. numexp0
    15. numexp1
    16. numexpp1
    17. numexp2x
    18. decsplit0b
    19. decsplit0
    20. decsplit1
    21. decsplit
    22. karatsuba
    23. 2exp4
    24. 2exp5
    25. 2exp6
    26. 2exp7
    27. 2exp8
    28. 2exp11
    29. 2exp16
    30. 3exp3
    31. 2expltfac
18. Cyclical shifts of words (cont.)
    1. cshwsidrepsw
    2. cshwsidrepswmod0
    3. cshwshashlem1
    4. cshwshashlem2
    5. cshwshashlem3
    6. cshwsdisj
    7. cshwsiun
    8. cshwsex
    9. cshws0
    10. cshwrepswhash1
    11. cshwshashnsame
    12. cshwshash
19. Specific prime numbers
    1. prmlem0
    2. prmlem1a
    3. prmlem1
    4. 5prm
    5. 6nprm
    6. 7prm
    7. 8nprm
    8. 9nprm
    9. 10nprm
    10. 11prm
    11. 13prm
    12. 17prm
    13. 19prm
    14. 23prm
    15. prmlem2
    16. 37prm
    17. 43prm
    18. 83prm
    19. 139prm
    20. 163prm
    21. 317prm
    22. 631prm
    23. prmo4
    24. prmo5
    25. prmo6
20. Very large primes
    1. 1259lem1
    2. 1259lem2
    3. 1259lem3
    4. 1259lem4
    5. 1259lem5
    6. 1259prm
    7. 2503lem1
    8. 2503lem2
    9. 2503lem3
    10. 2503prm
    11. 4001lem1
    12. 4001lem2
    13. 4001lem3
    14. 4001lem4
    15. 4001prm