Metamath Proof Explorer

Table of Contents - 14.4. Basic number theory

Wilson's theorem
1. wilthlem1
2. wilthlem2
3. wilthlem3
4. wilth
5. wilthimp
The Fundamental Theorem of Algebra
1. ftalem1
2. ftalem2
3. ftalem3
4. ftalem4
5. ftalem5
6. ftalem6
7. ftalem7
8. fta
The Basel problem (ζ(2) = π²/6)
1. basellem1
2. basellem2
3. basellem3
4. basellem4
5. basellem5
6. basellem6
7. basellem7
8. basellem8
9. basellem9
10. basel
Number-theoretical functions
1. ccht
2. cvma
3. cchp
4. cppi
5. cmu
6. csgm
7. df-cht
8. df-vma
9. df-chp
10. df-ppi
11. df-mu
12. df-sgm
13. efnnfsumcl
14. ppisval
15. ppisval2
16. ppifi
17. prmdvdsfi
18. chtf
19. chtcl
20. chtval
21. efchtcl
22. chtge0
23. vmaval
24. isppw
25. isppw2
26. vmappw
27. vmaprm
28. vmacl
29. vmaf
30. efvmacl
31. vmage0
32. chpval
33. chpf
34. chpcl
35. efchpcl
36. chpge0
37. ppival
38. ppival2
39. ppival2g
40. ppif
41. ppicl
42. muval
43. muval1
44. muval2
45. isnsqf
46. issqf
47. sqfpc
48. dvdssqf
49. sqf11
50. muf
51. mucl
52. sgmval
53. sgmval2
54. 0sgm
55. sgmf
56. sgmcl
57. sgmnncl
58. mule1
59. chtfl
60. chpfl
61. ppiprm
62. ppinprm
63. chtprm
64. chtnprm
65. chpp1
66. chtwordi
67. chpwordi
68. chtdif
69. efchtdvds
70. ppifl
71. ppip1le
72. ppiwordi
73. ppidif
74. ppi1
75. cht1
76. vma1
77. chp1
78. ppi1i
79. ppi2i
80. ppi2
81. ppi3
82. cht2
83. cht3
84. ppinncl
85. chtrpcl
86. ppieq0
87. ppiltx
88. prmorcht
89. mumullem1
90. mumullem2
91. mumul
92. sqff1o
93. fsumdvdsdiaglem
94. fsumdvdsdiag
95. fsumdvdscom
96. dvdsppwf1o
97. dvdsflf1o
98. dvdsflsumcom
99. fsumfldivdiaglem
100. fsumfldivdiag
101. musum
102. musumsum
103. muinv
104. dvdsmulf1o
105. fsumdvdsmul
106. sgmppw
107. 0sgmppw
108. 1sgmprm
109. 1sgm2ppw
110. sgmmul
111. ppiublem1
112. ppiublem2
113. ppiub
114. vmalelog
115. chtlepsi
116. chprpcl
117. chpeq0
118. chteq0
119. chtleppi
120. chtublem
121. chtub
122. fsumvma
123. fsumvma2
124. pclogsum
125. vmasum
126. logfac2
127. chpval2
128. chpchtsum
129. chpub
130. logfacubnd
131. logfaclbnd
132. logfacbnd3
133. logfacrlim
134. logexprlim
135. logfacrlim2
Perfect Number Theorem
1. mersenne
2. perfect1
3. perfectlem1
4. perfectlem2
5. perfect
Characters of Z/nZ
1. cdchr
2. df-dchr
3. dchrval
4. dchrbas
5. dchrelbas
6. dchrelbas2
7. dchrelbas3
8. dchrelbasd
9. dchrrcl
10. dchrmhm
11. dchrf
12. dchrelbas4
13. dchrzrh1
14. dchrzrhcl
15. dchrzrhmul
16. dchrplusg
17. dchrmul
18. dchrmulcl
19. dchrn0
20. dchr1cl
21. dchrmulid2
22. dchrinvcl
23. dchrabl
24. dchrfi
25. dchrghm
26. dchr1
27. dchreq
28. dchrresb
29. dchrabs
30. dchrinv
31. dchrabs2
32. dchr1re
33. dchrptlem1
34. dchrptlem2
35. dchrptlem3
36. dchrpt
37. dchrsum2
38. dchrsum
39. sumdchr2
40. dchrhash
41. sumdchr
42. dchr2sum
43. sum2dchr
Bertrand's postulate
1. bcctr
2. pcbcctr
3. bcmono
4. bcmax
5. bcp1ctr
6. bclbnd
7. efexple
8. bpos1lem
9. bpos1
10. bposlem1
11. bposlem2
12. bposlem3
13. bposlem4
14. bposlem5
15. bposlem6
16. bposlem7
17. bposlem8
18. bposlem9
19. bpos
Quadratic residues and the Legendre symbol
1. clgs
2. df-lgs
3. zabsle1
4. lgslem1
5. lgslem2
6. lgslem3
7. lgslem4
8. lgsval
9. lgsfval
10. lgsfcl2
11. lgscllem
12. lgsfcl
13. lgsfle1
14. lgsval2lem
15. lgsval4lem
16. lgscl2
17. lgs0
18. lgscl
19. lgsle1
20. lgsval2
21. lgs2
22. lgsval3
23. lgsvalmod
24. lgsval4
25. lgsfcl3
26. lgsval4a
27. lgscl1
28. lgsneg
29. lgsneg1
30. lgsmod
31. lgsdilem
32. lgsdir2lem1
33. lgsdir2lem2
34. lgsdir2lem3
35. lgsdir2lem4
36. lgsdir2lem5
37. lgsdir2
38. lgsdirprm
39. lgsdir
40. lgsdilem2
41. lgsdi
42. lgsne0
43. lgsabs1
44. lgssq
45. lgssq2
46. lgsprme0
47. 1lgs
48. lgs1
49. lgsmodeq
50. lgsmulsqcoprm
51. lgsdirnn0
52. lgsdinn0
53. lgsqrlem1
54. lgsqrlem2
55. lgsqrlem3
56. lgsqrlem4
57. lgsqrlem5
58. lgsqr
59. lgsqrmod
60. lgsqrmodndvds
61. lgsdchrval
62. lgsdchr
Gauss' Lemma
Quadratic reciprocity
1. lgseisenlem1
2. lgseisenlem2
3. lgseisenlem3
4. lgseisenlem4
5. lgseisen
6. lgsquadlem1
7. lgsquadlem2
8. lgsquadlem3
9. lgsquad
10. lgsquad2lem1
11. lgsquad2lem2
12. lgsquad2
13. lgsquad3
14. m1lgs
15. 2lgslem1a1
16. 2lgslem1a2
17. 2lgslem1a
18. 2lgslem1b
19. 2lgslem1c
20. 2lgslem1
21. 2lgslem2
22. 2lgslem3a
23. 2lgslem3b
24. 2lgslem3c
25. 2lgslem3d
26. 2lgslem3a1
27. 2lgslem3b1
28. 2lgslem3c1
29. 2lgslem3d1
30. 2lgslem3
31. 2lgs2
32. 2lgslem4
33. 2lgs
34. 2lgsoddprmlem1
35. 2lgsoddprmlem2
36. 2lgsoddprmlem3a
37. 2lgsoddprmlem3b
38. 2lgsoddprmlem3c
39. 2lgsoddprmlem3d
40. 2lgsoddprmlem3
41. 2lgsoddprmlem4
42. 2lgsoddprm
All primes 4n+1 are the sum of two squares
1. 2sqlem1
2. 2sqlem2
3. mul2sq
4. 2sqlem3
5. 2sqlem4
6. 2sqlem5
7. 2sqlem6
8. 2sqlem7
9. 2sqlem8a
10. 2sqlem8
11. 2sqlem9
12. 2sqlem10
13. 2sqlem11
14. 2sq
15. 2sqblem
16. 2sqb
17. 2sq2
18. 2sqn0
19. 2sqcoprm
20. 2sqmod
21. 2sqmo
22. 2sqnn0
23. 2sqnn
24. addsq2reu
25. addsqn2reu
26. addsqrexnreu
27. addsqnreup
28. addsq2nreurex
29. addsqn2reurex2
30. 2sqreulem1
31. 2sqreultlem
32. 2sqreultblem
33. 2sqreunnlem1
34. 2sqreunnltlem
35. 2sqreunnltblem
36. 2sqreulem2
37. 2sqreulem3
38. 2sqreulem4
39. 2sqreunnlem2
40. 2sqreu
41. 2sqreunn
42. 2sqreult
43. 2sqreultb
44. 2sqreunnlt
45. 2sqreunnltb
46. 2sqreuop
47. 2sqreuopnn
48. 2sqreuoplt
49. 2sqreuopltb
50. 2sqreuopnnlt
51. 2sqreuopnnltb
52. 2sqreuopb
Chebyshev's Weak Prime Number Theorem, Dirichlet's Theorem
The Prime Number Theorem
1. mudivsum
2. mulogsumlem
3. mulogsum
4. logdivsum
5. mulog2sumlem1
6. mulog2sumlem2
7. mulog2sumlem3
8. mulog2sum
9. vmalogdivsum2
10. vmalogdivsum
11. 2vmadivsumlem
12. 2vmadivsum
13. logsqvma
14. logsqvma2
15. log2sumbnd
16. selberglem1
17. selberglem2
18. selberglem3
19. selberg
20. selbergb
21. selberg2lem
22. selberg2
23. selberg2b
24. chpdifbndlem1
25. chpdifbndlem2
26. chpdifbnd
27. logdivbnd
28. selberg3lem1
29. selberg3lem2
30. selberg3
31. selberg4lem1
32. selberg4
33. pntrval
34. pntrf
35. pntrmax
36. pntrsumo1
37. pntrsumbnd
38. pntrsumbnd2
39. selbergr
40. selberg3r
41. selberg4r
42. selberg34r
43. pntsval
44. pntsf
45. selbergs
46. selbergsb
47. pntsval2
48. pntrlog2bndlem1
49. pntrlog2bndlem2
50. pntrlog2bndlem3
51. pntrlog2bndlem4
52. pntrlog2bndlem5
53. pntrlog2bndlem6a
54. pntrlog2bndlem6
55. pntrlog2bnd
56. pntpbnd1a
57. pntpbnd1
58. pntpbnd2
59. pntpbnd
60. pntibndlem1
61. pntibndlem2a
62. pntibndlem2
63. pntibndlem3
64. pntibnd
65. pntlemd
66. pntlemc
67. pntlema
68. pntlemb
69. pntlemg
70. pntlemh
71. pntlemn
72. pntlemq
73. pntlemr
74. pntlemj
75. pntlemi
76. pntlemf
77. pntlemk
78. pntlemo
79. pntleme
80. pntlem3
81. pntlemp
82. pntleml
83. pnt3
84. pnt2
85. pnt
Ostrowski's theorem
1. abvcxp
2. padicfval
3. padicval
4. ostth2lem1
5. qrngbas
6. qdrng
7. qrng0
8. qrng1
9. qrngneg
10. qrngdiv
11. qabvle
12. qabvexp
13. ostthlem1
14. ostthlem2
15. qabsabv
16. padicabv
17. padicabvf
18. padicabvcxp
19. ostth1
20. ostth2lem2
21. ostth2lem3
22. ostth2lem4
23. ostth2
24. ostth3
25. ostth