Metamath Proof Explorer

Table of Contents - 20.31. Mathbox for Stefan O'Rear

1. Additional elementary logic and set theory
   1. moxfr
2. Additional theory of functions
   1. imaiinfv
3. Additional topology
   1. elrfi
   2. elrfirn
   3. elrfirn2
   4. cmpfiiin
4. Characterization of closure operators. Kuratowski closure axioms
   1. ismrcd1
   2. ismrcd2
   3. istopclsd
   4. ismrc
5. Algebraic closure systems
   1. cnacs
   2. df-nacs
   3. isnacs
   4. nacsfg
   5. isnacs2
   6. mrefg2
   7. mrefg3
   8. nacsacs
   9. isnacs3
   10. incssnn0
   11. nacsfix
6. Miscellanea 1. Map utilities
   1. constmap
   2. mapco2g
   3. mapco2
   4. mapfzcons
   5. mapfzcons1
   6. mapfzcons1cl
   7. mapfzcons2
7. Miscellanea for polynomials
   1. mptfcl
8. Multivariate polynomials over the integers
   1. cmzpcl
   2. cmzp
   3. df-mzpcl
   4. df-mzp
   5. mzpclval
   6. elmzpcl
   7. mzpclall
   8. mzpcln0
   9. mzpcl1
   10. mzpcl2
   11. mzpcl34
   12. mzpval
   13. dmmzp
   14. mzpincl
   15. mzpconst
   16. mzpf
   17. mzpproj
   18. mzpadd
   19. mzpmul
   20. mzpconstmpt
   21. mzpaddmpt
   22. mzpmulmpt
   23. mzpsubmpt
   24. mzpnegmpt
   25. mzpexpmpt
   26. mzpindd
   27. mzpmfp
   28. mzpsubst
   29. mzprename
   30. mzpresrename
   31. mzpcompact2lem
   32. mzpcompact2
9. Miscellanea for Diophantine sets 1
   1. coeq0i
   2. fzsplit1nn0
10. Diophantine sets 1: definitions
    1. cdioph
    2. df-dioph
    3. eldiophb
    4. eldioph
    5. diophrw
    6. eldioph2lem1
    7. eldioph2lem2
    8. eldioph2
    9. eldioph2b
    10. eldiophelnn0
    11. eldioph3b
    12. eldioph3
11. Diophantine sets 2 miscellanea
    1. ellz1
    2. lzunuz
    3. fz1eqin
    4. lzenom
    5. elmapresaunres2
12. Diophantine sets 2: union and intersection. Monotone Boolean algebra
    1. diophin
    2. diophun
    3. eldiophss
13. Diophantine sets 3: construction
    1. diophrex
    2. eq0rabdioph
    3. eqrabdioph
    4. 0dioph
    5. vdioph
    6. anrabdioph
    7. orrabdioph
    8. 3anrabdioph
    9. 3orrabdioph
14. Diophantine sets 4 miscellanea
    1. 2sbcrex
    2. sbcrexgOLD
    3. 2sbcrexOLD
    4. sbc2rex
    5. sbc2rexgOLD
    6. sbc4rex
    7. sbc4rexgOLD
    8. sbcrot3
    9. sbcrot5
    10. sbccomieg
15. Diophantine sets 4: Quantification
    1. rexrabdioph
    2. rexfrabdioph
    3. 2rexfrabdioph
    4. 3rexfrabdioph
    5. 4rexfrabdioph
    6. 6rexfrabdioph
    7. 7rexfrabdioph
16. Diophantine sets 5: Arithmetic sets
    1. rabdiophlem1
    2. rabdiophlem2
    3. elnn0rabdioph
    4. rexzrexnn0
    5. lerabdioph
    6. eluzrabdioph
    7. elnnrabdioph
    8. ltrabdioph
    9. nerabdioph
    10. dvdsrabdioph
17. Diophantine sets 6: reusability. renumbering of variables
    1. eldioph4b
    2. eldioph4i
    3. diophren
    4. rabrenfdioph
    5. rabren3dioph
18. Pigeonhole Principle and cardinality helpers
    1. fphpd
    2. fphpdo
    3. ctbnfien
    4. fiphp3d
19. A non-closed set of reals is infinite
    1. rencldnfilem
    2. rencldnfi
20. Lagrange's rational approximation theorem
    1. irrapxlem1
    2. irrapxlem2
    3. irrapxlem3
    4. irrapxlem4
    5. irrapxlem5
    6. irrapxlem6
    7. irrapx1
21. Pell equations 1: A nontrivial solution always exists
    1. pellexlem1
    2. pellexlem2
    3. pellexlem3
    4. pellexlem4
    5. pellexlem5
    6. pellexlem6
    7. pellex
22. Pell equations 2: Algebraic number theory of the solution set
    1. csquarenn
    2. cpell1qr
    3. cpell1234qr
    4. cpell14qr
    5. cpellfund
    6. df-squarenn
    7. df-pell1qr
    8. df-pell14qr
    9. df-pell1234qr
    10. df-pellfund
    11. pell1qrval
    12. elpell1qr
    13. pell14qrval
    14. elpell14qr
    15. pell1234qrval
    16. elpell1234qr
    17. pell1234qrre
    18. pell1234qrne0
    19. pell1234qrreccl
    20. pell1234qrmulcl
    21. pell14qrss1234
    22. pell14qrre
    23. pell14qrne0
    24. pell14qrgt0
    25. pell14qrrp
    26. pell1234qrdich
    27. elpell14qr2
    28. pell14qrmulcl
    29. pell14qrreccl
    30. pell14qrdivcl
    31. pell14qrexpclnn0
    32. pell14qrexpcl
    33. pell1qrss14
    34. pell14qrdich
    35. pell1qrge1
    36. pell1qr1
    37. elpell1qr2
    38. pell1qrgaplem
    39. pell1qrgap
    40. pell14qrgap
    41. pell14qrgapw
    42. pellqrexplicit
23. Pell equations 3: characterizing fundamental solution
    1. infmrgelbi
    2. pellqrex
    3. pellfundval
    4. pellfundre
    5. pellfundge
    6. pellfundgt1
    7. pellfundlb
    8. pellfundglb
    9. pellfundex
    10. pellfund14gap
    11. pellfundrp
    12. pellfundne1
24. Logarithm laws generalized to an arbitrary base
    1. reglogcl
    2. reglogltb
    3. reglogleb
    4. reglogmul
    5. reglogexp
    6. reglogbas
    7. reglog1
    8. reglogexpbas
25. Pell equations 4: the positive solution group is infinite cyclic
    1. pellfund14
    2. pellfund14b
26. X and Y sequences 1: Definition and recurrence laws
    1. crmx
    2. crmy
    3. df-rmx
    4. df-rmy
    5. rmxfval
    6. rmyfval
    7. rmspecsqrtnq
    8. rmspecnonsq
    9. qirropth
    10. rmspecfund
    11. rmxyelqirr
    12. rmxypairf1o
    13. rmxyelxp
    14. frmx
    15. frmy
    16. rmxyval
    17. rmspecpos
    18. rmxycomplete
    19. rmxynorm
    20. rmbaserp
    21. rmxyneg
    22. rmxyadd
    23. rmxy1
    24. rmxy0
    25. rmxneg
    26. rmx0
    27. rmx1
    28. rmxadd
    29. rmyneg
    30. rmy0
    31. rmy1
    32. rmyadd
    33. rmxp1
    34. rmyp1
    35. rmxm1
    36. rmym1
    37. rmxluc
    38. rmyluc
    39. rmyluc2
    40. rmxdbl
    41. rmydbl
27. Ordering and induction lemmas for the integers
    1. monotuz
    2. monotoddzzfi
    3. monotoddzz
    4. oddcomabszz
    5. 2nn0ind
    6. zindbi
28. X and Y sequences 2: Order properties
    1. rmxypos
    2. ltrmynn0
    3. ltrmxnn0
    4. lermxnn0
    5. rmxnn
    6. ltrmy
    7. rmyeq0
    8. rmyeq
    9. lermy
    10. rmynn
    11. rmynn0
    12. rmyabs
    13. jm2.24nn
    14. jm2.17a
    15. jm2.17b
    16. jm2.17c
    17. jm2.24
    18. rmygeid
29. Congruential equations
    1. congtr
    2. congadd
    3. congmul
    4. congsym
    5. congneg
    6. congsub
    7. congid
    8. mzpcong
    9. congrep
    10. congabseq
30. Alternating congruential equations
    1. acongid
    2. acongsym
    3. acongneg2
    4. acongtr
    5. acongeq12d
    6. acongrep
    7. fzmaxdif
    8. fzneg
    9. acongeq
    10. dvdsacongtr
31. Additional theorems on integer divisibility
    1. coprmdvdsb
    2. modabsdifz
    3. dvdsabsmod0
32. X and Y sequences 3: Divisibility properties
    1. jm2.18
    2. jm2.19lem1
    3. jm2.19lem2
    4. jm2.19lem3
    5. jm2.19lem4
    6. jm2.19
    7. jm2.21
    8. jm2.22
    9. jm2.23
    10. jm2.20nn
    11. jm2.25lem1
    12. jm2.25
    13. jm2.26a
    14. jm2.26lem3
    15. jm2.26
    16. jm2.15nn0
    17. jm2.16nn0
33. X and Y sequences 4: Diophantine representability of Y
    1. jm2.27a
    2. jm2.27b
    3. jm2.27c
    4. jm2.27
    5. jm2.27dlem1
    6. jm2.27dlem2
    7. jm2.27dlem3
    8. jm2.27dlem4
    9. jm2.27dlem5
    10. rmydioph
34. X and Y sequences 5: Diophantine representability of X, ^, _C
    1. rmxdiophlem
    2. rmxdioph
    3. jm3.1lem1
    4. jm3.1lem2
    5. jm3.1lem3
    6. jm3.1
    7. expdiophlem1
    8. expdiophlem2
    9. expdioph
35. Uncategorized stuff not associated with a major project
    1. setindtr
    2. setindtrs
    3. dford3lem1
    4. dford3lem2
    5. dford3
    6. dford4
    7. wopprc
    8. rpnnen3lem
    9. rpnnen3
36. More equivalents of the Axiom of Choice
    1. axac10
    2. harinf
    3. wdom2d2
    4. ttac
    5. pw2f1ocnv
    6. pw2f1o2
    7. pw2f1o2val
    8. pw2f1o2val2
    9. soeq12d
    10. freq12d
    11. weeq12d
    12. limsuc2
    13. wepwsolem
    14. wepwso
    15. dnnumch1
    16. dnnumch2
    17. dnnumch3lem
    18. dnnumch3
    19. dnwech
    20. fnwe2val
    21. fnwe2lem1
    22. fnwe2lem2
    23. fnwe2lem3
    24. fnwe2
    25. aomclem1
    26. aomclem2
    27. aomclem3
    28. aomclem4
    29. aomclem5
    30. aomclem6
    31. aomclem7
    32. aomclem8
    33. dfac11
    34. kelac1
    35. kelac2lem
    36. kelac2
    37. dfac21
37. Finitely generated left modules
    1. clfig
    2. df-lfig
    3. islmodfg
    4. islssfg
    5. islssfg2
    6. islssfgi
    7. fglmod
    8. lsmfgcl
38. Noetherian left modules I
    1. clnm
    2. df-lnm
    3. islnm
    4. islnm2
    5. lnmlmod
    6. lnmlssfg
    7. lnmlsslnm
    8. lnmfg
    9. kercvrlsm
    10. lmhmfgima
    11. lnmepi
    12. lmhmfgsplit
    13. lmhmlnmsplit
    14. lnmlmic
39. Addenda for structure powers
    1. pwssplit4
    2. filnm
    3. pwslnmlem0
    4. pwslnmlem1
    5. pwslnmlem2
    6. pwslnm
40. Every set admits a group structure iff choice
    1. unxpwdom3
    2. pwfi2f1o
    3. pwfi2en
    4. frlmpwfi
    5. gicabl
    6. imasgim
    7. isnumbasgrplem1
    8. harn0
    9. numinfctb
    10. isnumbasgrplem2
    11. isnumbasgrplem3
    12. isnumbasabl
    13. isnumbasgrp
    14. dfacbasgrp
41. Noetherian rings and left modules II
    1. clnr
    2. df-lnr
    3. islnr
    4. lnrring
    5. lnrlnm
    6. islnr2
    7. islnr3
    8. lnr2i
    9. lpirlnr
    10. lnrfrlm
    11. lnrfg
    12. lnrfgtr
42. Hilbert's Basis Theorem
    1. cldgis
    2. df-ldgis
    3. hbtlem1
    4. hbtlem2
    5. hbtlem7
    6. hbtlem4
    7. hbtlem3
    8. hbtlem5
    9. hbtlem6
    10. hbt
43. Additional material on polynomials [DEPRECATED]
    1. cmnc
    2. cplylt
    3. df-mnc
    4. df-plylt
    5. dgrsub2
    6. elmnc
    7. mncply
    8. mnccoe
    9. mncn0
44. Degree and minimal polynomial of algebraic numbers
    1. cdgraa
    2. cmpaa
    3. df-dgraa
    4. df-mpaa
    5. dgraaval
    6. dgraalem
    7. dgraacl
    8. dgraaf
    9. dgraaub
    10. dgraa0p
    11. mpaaeu
    12. mpaaval
    13. mpaalem
    14. mpaacl
    15. mpaadgr
    16. mpaaroot
    17. mpaamn
45. Algebraic integers I
    1. citgo
    2. cza
    3. df-itgo
    4. df-za
    5. itgoval
    6. aaitgo
    7. itgoss
    8. itgocn
    9. cnsrexpcl
    10. fsumcnsrcl
    11. cnsrplycl
    12. rgspnval
    13. rgspncl
    14. rgspnssid
    15. rgspnmin
    16. rgspnid
    17. rngunsnply
    18. flcidc
46. The determinant / matrix adjugate/adjunct
47. Endomorphism algebra
    1. cmend
    2. df-mend
    3. algstr
    4. algbase
    5. algaddg
    6. algmulr
    7. algsca
    8. algvsca
    9. mendval
    10. mendbas
    11. mendplusgfval
    12. mendplusg
    13. mendmulrfval
    14. mendmulr
    15. mendsca
    16. mendvscafval
    17. mendvsca
    18. mendring
    19. mendlmod
    20. mendassa
48. The class equation
49. Cyclic groups and order
    1. idomrootle
    2. idomodle
    3. fiuneneq
    4. idomsubgmo
    5. proot1mul
    6. proot1hash
    7. proot1ex
50. Cyclotomic polynomials
    1. ccytp
    2. df-cytp
    3. isdomn3
    4. mon1pid
    5. mon1psubm
    6. deg1mhm
    7. cytpfn
    8. cytpval
51. Wedderburn's little theorem
52. Hybrid categories proposal
53. Miscellaneous topology
    1. fgraphopab
    2. fgraphxp
    3. hausgraph
    4. ctopsep
    5. ctoplnd
    6. df-topsep
    7. df-toplnd