Metamath Proof Explorer

Table of Contents - 20. SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)

1. Mathboxes for user contributions
   1. Mathbox guidelines
2. Mathbox for Stefan Allan
   1. sa-abvi
   2. xfree
   3. xfree2
   4. addltmulALT
3. Mathbox for Thierry Arnoux
   1. Propositional Calculus - misc additions
   2. Predicate Calculus
   3. General Set Theory
   4. Relations and Functions
   5. Real and Complex Numbers
   6. Decimal expansion
   7. Words over a set - misc additions
   8. Extensible Structures
   9. Algebra
   10. Field Extensions
   11. Matrices
   12. Topology
   13. Uniform Stuctures and Spaces
   14. Topology and algebraic structures
   15. Real and complex functions
   16. Mixed Function/Constant operation
   17. Abstract measure
   18. Integration
   19. Euler's partition theorem
   20. Sequences defined by strong recursion
   21. Fibonacci Numbers
   22. Probability
   23. Signum (sgn or sign) function - misc. additions
   24. Polynomials with real coefficients - misc additions
   25. Descartes's rule of signs
   26. Number Theory
   27. Elementary Geometry
   28. LeftPad Project
4. Mathbox for Jonathan Ben-Naim
   1. w-bnj17
   2. df-bnj17
   3. c-bnj14
   4. df-bnj14
   5. w-bnj13
   6. df-bnj13
   7. w-bnj15
   8. df-bnj15
   9. c-bnj18
   10. df-bnj18
   11. w-bnj19
   12. df-bnj19
   13. First-order logic and set theory
   14. Well founded induction and recursion
   15. The existence of a minimal element in certain classes
   16. Well-founded induction
   17. Well-founded recursion, part 1 of 3
   18. Well-founded recursion, part 2 of 3
   19. Well-founded recursion, part 3 of 3
5. Mathbox for BTernaryTau
   1. exdifsn
   2. srcmpltd
   3. prsrcmpltd
   4. zltp1ne
   5. nnltp1ne
   6. nn0ltp1ne
   7. 0nn0m1nnn0
   8. fisshasheq
   9. dff15
   10. hashfundm
   11. hashf1dmrn
   12. hashf1dmcdm
   13. funen1cnv
   14. f1resveqaeq
   15. f1resrcmplf1dlem
   16. f1resrcmplf1d
   17. f1resfz0f1d
   18. revpfxsfxrev
   19. swrdrevpfx
   20. lfuhgr
   21. lfuhgr2
   22. lfuhgr3
   23. cplgredgex
   24. cusgredgex
   25. cusgredgex2
   26. pfxwlk
   27. revwlk
   28. revwlkb
   29. swrdwlk
   30. pthhashvtx
   31. pthisspthorcycl
   32. spthcycl
   33. usgrgt2cycl
   34. usgrcyclgt2v
   35. subgrwlk
   36. subgrtrl
   37. subgrpth
   38. subgrcycl
   39. cusgr3cyclex
   40. loop1cycl
   41. 2cycld
   42. 2cycl2d
   43. umgr2cycllem
   44. umgr2cycl
   45. Acyclic graphs
6. Mathbox for Mario Carneiro
   1. Predicate calculus with all distinct variables
   2. Miscellaneous stuff
   3. Derangements and the Subfactorial
   4. The Erdős-Szekeres theorem
   5. Euler's partition theorem
   6. The Kuratowski closure-complement theorem
   7. Retracts and sections
   8. Path-connected and simply connected spaces
   9. Covering maps
   10. Normal numbers
   11. Compactification
   12. Godel-sets of formulas - part 1
   13. Godel-sets of formulas - part 2
   14. Models of ZF
   15. Metamath formal systems
   16. Grammatical formal systems
   17. Models of formal systems
   18. Splitting fields
   19. p-adic number fields
7. Mathbox for Filip Cernatescu
   1. problem1
   2. problem2
   3. problem3
   4. problem4
   5. problem5
   6. quad3
8. Mathbox for Paul Chapman
   1. Propositional calculus
   2. Prime numbers
   3. Finite set induction
   4. The ` # ` (set size) function
   5. Real and complex numbers (cont.)
   6. Miscellaneous theorems
9. Mathbox for Drahflow
10. Mathbox for Scott Fenton
    1. ZFC Axioms in primitive form
    2. Untangled classes
    3. Extra propositional calculus theorems
    4. Misc. Useful Theorems
    5. Properties of real and complex numbers
    6. Infinite products
    7. Factorial limits
    8. Greatest common divisor and divisibility
    9. Properties of relationships
    10. Properties of functions and mappings
    11. Set induction (or epsilon induction)
    12. Ordinal numbers
    13. Defined equality axioms
    14. Hypothesis builders
    15. (Trans)finite Recursion Theorems
    16. Transitive closure under a relationship
    17. Founded Induction
    18. Ordering Ordinal Sequences
    19. Well-founded zero, successor, and limits
    20. Founded Partial Recursion
    21. Surreal Numbers
    22. Surreal Numbers: Ordering
    23. Surreal Numbers: Birthday Function
    24. Surreal Numbers: Density
    25. Surreal Numbers: Full-Eta Property
    26. Surreal numbers - ordering theorems
    27. Surreal numbers - birthday theorems
    28. Surreal numbers: Conway cuts
    29. Surreal numbers - cuts and options
    30. Quantifier-free definitions
    31. Alternate ordered pairs
    32. Geometry in the Euclidean space
    33. Forward difference
    34. Rank theorems
    35. Hereditarily Finite Sets
11. Mathbox for Jeff Hankins
    1. Miscellany
    2. Basic topological facts
    3. Topology of the real numbers
    4. Refinements
    5. Neighborhood bases determine topologies
    6. Lattice structure of topologies
    7. Filter bases
    8. Directed sets, nets
12. Mathbox for Anthony Hart
    1. Propositional Calculus
    2. Predicate Calculus
    3. Miscellaneous single axioms
    4. Connective Symmetry
13. Mathbox for Chen-Pang He
    1. Ordinal topology
14. Mathbox for Jeff Hoffman
    1. Inferences for finite induction on generic function values
    2. gdc.mm
15. Mathbox for Asger C. Ipsen
    1. Continuous nowhere differentiable functions
16. Mathbox for BJ
    1. Propositional calculus
    2. Modal logic
    3. Provability logic
    4. First-order logic
    5. Set theory
    6. Extended real and complex numbers, real and complex projective lines
    7. Monoids
    8. Affine, Euclidean, and Cartesian geometry
    9. Monoid of endomorphisms
17. Mathbox for Jim Kingdon
    1. Circle constant
    2. Number theory
18. Mathbox for ML
    1. Miscellaneous
    2. Cartesian exponentiation
    3. Topology
19. Mathbox for Wolf Lammen
    1. wl-section-prop
    2. ax-luk1
    3. ax-luk2
    4. ax-luk3
    5. 1. Bootstrapping
    6. Implication chains
    7. Alternative development of hadd
    8. An alternative axiom ~ ax-13
    9. Other stuff
    10. 1. Restricted Quantifiers
20. Mathbox for Brendan Leahy
    1. rabiun
    2. iundif1
    3. imadifss
    4. cureq
    5. unceq
    6. curf
    7. uncf
    8. curfv
    9. uncov
    10. curunc
    11. unccur
    12. phpreu
    13. finixpnum
    14. fin2solem
    15. fin2so
    16. ltflcei
    17. leceifl
    18. sin2h
    19. cos2h
    20. tan2h
    21. lindsadd
    22. lindsdom
    23. lindsenlbs
    24. matunitlindflem1
    25. matunitlindflem2
    26. matunitlindf
    27. ptrest
    28. ptrecube
    29. poimirlem1
    30. poimirlem2
    31. poimirlem3
    32. poimirlem4
    33. poimirlem5
    34. poimirlem6
    35. poimirlem7
    36. poimirlem8
    37. poimirlem9
    38. poimirlem10
    39. poimirlem11
    40. poimirlem12
    41. poimirlem13
    42. poimirlem14
    43. poimirlem15
    44. poimirlem16
    45. poimirlem17
    46. poimirlem18
    47. poimirlem19
    48. poimirlem20
    49. poimirlem21
    50. poimirlem22
    51. poimirlem23
    52. poimirlem24
    53. poimirlem25
    54. poimirlem26
    55. poimirlem27
    56. poimirlem28
    57. poimirlem29
    58. poimirlem30
    59. poimirlem31
    60. poimirlem32
    61. poimir
    62. broucube
    63. heicant
    64. opnmbllem0
    65. mblfinlem1
    66. mblfinlem2
    67. mblfinlem3
    68. mblfinlem4
    69. ismblfin
    70. ovoliunnfl
    71. ex-ovoliunnfl
    72. voliunnfl
    73. volsupnfl
    74. mbfresfi
    75. mbfposadd
    76. cnambfre
    77. dvtanlem
    78. dvtan
    79. itg2addnclem
    80. itg2addnclem2
    81. itg2addnclem3
    82. itg2addnc
    83. itg2gt0cn
    84. ibladdnclem
    85. ibladdnc
    86. itgaddnclem1
    87. itgaddnclem2
    88. itgaddnc
    89. iblsubnc
    90. itgsubnc
    91. iblabsnclem
    92. iblabsnc
    93. iblmulc2nc
    94. itgmulc2nclem1
    95. itgmulc2nclem2
    96. itgmulc2nc
    97. itgabsnc
    98. itggt0cn
    99. ftc1cnnclem
    100. ftc1cnnc
    101. ftc1anclem1
    102. ftc1anclem2
    103. ftc1anclem3
    104. ftc1anclem4
    105. ftc1anclem5
    106. ftc1anclem6
    107. ftc1anclem7
    108. ftc1anclem8
    109. ftc1anc
    110. ftc2nc
    111. asindmre
    112. dvasin
    113. dvacos
    114. dvreasin
    115. dvreacos
    116. areacirclem1
    117. areacirclem2
    118. areacirclem3
    119. areacirclem4
    120. areacirclem5
    121. areacirc
21. Mathbox for Jeff Madsen
    1. Logic and set theory
    2. Real and complex numbers; integers
    3. Sequences and sums
    4. Topology
    5. Metric spaces
    6. Continuous maps and homeomorphisms
    7. Boundedness
    8. Isometries
    9. Heine-Borel Theorem
    10. Banach Fixed Point Theorem
    11. Euclidean space
    12. Intervals (continued)
    13. Operation properties
    14. Groups and related structures
    15. Group homomorphism and isomorphism
    16. Rings
    17. Division Rings
    18. Ring homomorphisms
    19. Commutative rings
    20. Ideals
    21. Prime rings and integral domains
    22. Ideal generators
22. Mathbox for Giovanni Mascellani
    1. Tools for automatic proof building
    2. Tseitin axioms
    3. Equality deductions
    4. Miscellanea
23. Mathbox for Peter Mazsa
    1. Notations
    2. Preparatory theorems
    3. Range Cartesian product
    4. Cosets by ` R `
    5. Relations
    6. Subset relations
    7. Reflexivity
    8. Converse reflexivity
    9. Symmetry
    10. Reflexivity and symmetry
    11. Transitivity
    12. Equivalence relations
    13. Redundancy
    14. Domain quotients
    15. Equivalence relations on domain quotients
    16. Functions
    17. Disjoints vs. converse functions
24. Mathbox for Rodolfo Medina
    1. Partitions
25. Mathbox for Norm Megill
    1. Predicate calculus with equality: Older axiomatization (1 rule, 14 schemes)
    2. Obsolete schemes ax-c4,c5,c7,c10,c11,c11n,c15,c9,c14,c16
    3. Rederive new axioms ax-4, ax-10, ax-6, ax-12, ax-13 from old
    4. Legacy theorems using obsolete axioms
    5. Experiments with weak deduction theorem
    6. Miscellanea
    7. Atoms, hyperplanes, and covering in a left vector space (or module)
    8. Functionals and kernels of a left vector space (or module)
    9. Opposite rings and dual vector spaces
    10. Ortholattices and orthomodular lattices
    11. Atomic lattices with covering property
    12. Hilbert lattices
    13. Projective geometries based on Hilbert lattices
    14. Construction of a vector space from a Hilbert lattice
    15. Construction of involution and inner product from a Hilbert lattice
26. Mathbox for metakunt
    1. addassnni
    2. addcomnni
    3. mulassnni
    4. mulcomnni
    5. gcdcomnni
    6. gcdnegnni
    7. neggcdnni
    8. gcdmultiplei
    9. gcdaddmzz2nni
    10. gcdaddmzz2nncomi
    11. gcdnncli
    12. 12gcd5e1
    13. 60gcd6e6
    14. 60gcd7e1
    15. 420gcd8e4
    16. lcmeprodgcdi
    17. 12lcm5e60
    18. 60lcm6e60
    19. 60lcm7e420
    20. 420lcm8e840
    21. 3factsumint1
    22. 3factsumint2
    23. 3factsumint3
    24. 3factsumint4
    25. 3factsumint
    26. ineq2pow2tnd
    27. lcmineqlem1
    28. lcmineqlem2
    29. lcmineqlem3
    30. lcmfunnnd
    31. lcm1un
    32. lcm2un
    33. lcm3un
    34. lcm4un
    35. lcm5un
    36. lcm6un
    37. lcm7un
    38. lcm8un
    39. andiff
    40. fac2xp3
    41. facp2
    42. prodsplit
    43. 2xp3dxp2ge1d
    44. factwoffsmonot
27. Mathbox for Steven Nguyen
    1. ${
    2. Arithmetic theorems
    3. Exponents
    4. Real subtraction
    5. Looking at a corner in 3D space, one can see three right angles. It is
    6. $( TODO:
28. Mathbox for Igor Ieskov
    1. binom2d
    2. cu3addd
    3. sqnegd
    4. negexpidd
    5. rexlimdv3d
    6. 3cubeslem1
    7. 3cubeslem2
    8. 3cubeslem3l
    9. 3cubeslem3r
    10. 3cubeslem3
    11. 3cubeslem4
    12. 3cubes
29. Mathbox for Larry Lesyna
30. Mathbox for OpenAI
    1. rntrclfvOAI
31. Mathbox for Stefan O'Rear
    1. Additional elementary logic and set theory
    2. Additional theory of functions
    3. Additional topology
    4. Characterization of closure operators. Kuratowski closure axioms
    5. Algebraic closure systems
    6. Miscellanea 1. Map utilities
    7. Miscellanea for polynomials
    8. Multivariate polynomials over the integers
    9. Miscellanea for Diophantine sets 1
    10. Diophantine sets 1: definitions
    11. Diophantine sets 2 miscellanea
    12. Diophantine sets 2: union and intersection. Monotone Boolean algebra
    13. Diophantine sets 3: construction
    14. Diophantine sets 4 miscellanea
    15. Diophantine sets 4: Quantification
    16. Diophantine sets 5: Arithmetic sets
    17. Diophantine sets 6: reusability. renumbering of variables
    18. Pigeonhole Principle and cardinality helpers
    19. A non-closed set of reals is infinite
    20. Lagrange's rational approximation theorem
    21. Pell equations 1: A nontrivial solution always exists
    22. Pell equations 2: Algebraic number theory of the solution set
    23. Pell equations 3: characterizing fundamental solution
    24. Logarithm laws generalized to an arbitrary base
    25. Pell equations 4: the positive solution group is infinite cyclic
    26. X and Y sequences 1: Definition and recurrence laws
    27. Ordering and induction lemmas for the integers
    28. X and Y sequences 2: Order properties
    29. Congruential equations
    30. Alternating congruential equations
    31. Additional theorems on integer divisibility
    32. X and Y sequences 3: Divisibility properties
    33. X and Y sequences 4: Diophantine representability of Y
    34. X and Y sequences 5: Diophantine representability of X, ^, _C
    35. Uncategorized stuff not associated with a major project
    36. More equivalents of the Axiom of Choice
    37. Finitely generated left modules
    38. Noetherian left modules I
    39. Addenda for structure powers
    40. Every set admits a group structure iff choice
    41. Noetherian rings and left modules II
    42. Hilbert's Basis Theorem
    43. Additional material on polynomials [DEPRECATED]
    44. Degree and minimal polynomial of algebraic numbers
    45. Algebraic integers I
    46. The determinant / matrix adjugate/adjunct
    47. Endomorphism algebra
    48. The class equation
    49. Cyclic groups and order
    50. Cyclotomic polynomials
    51. Wedderburn's little theorem
    52. Hybrid categories proposal
    53. Miscellaneous topology
32. Mathbox for Jon Pennant
    1. iocunico
    2. iocinico
    3. iocmbl
    4. cnioobibld
    5. arearect
    6. areaquad
33. Mathbox for Richard Penner
    1. Short Studies
    2. Additional statements on relations and subclasses
    3. Propositions from _Begriffsschrift_
    4. Exploring Topology via Seifert and Threlfall
    5. Exploring Higher Homotopy via Kerodon
34. Mathbox for Stanislas Polu
    1. inductionexd
    2. IMO Problems
    3. INT Inequalities Proof Generator
    4. N-Digit Addition Proof Generator
    5. AM-GM (for k = 2,3,4)
35. Mathbox for Rohan Ridenour
    1. Misc
    2. Shorter primitive equivalent of ax-groth
36. Mathbox for Steve Rodriguez
    1. Miscellanea
    2. Ratio test for infinite series convergence and divergence
    3. Multiples
    4. Function operations
    5. Calculus
    6. The generalized binomial coefficient operation
    7. Binomial series
37. Mathbox for Andrew Salmon
    1. Principia Mathematica * 10
    2. Principia Mathematica * 11
    3. Predicate Calculus
    4. Principia Mathematica * 13 and * 14
    5. Set Theory
    6. Arithmetic
    7. Geometry
38. Mathbox for Alan Sare
    1. Auxiliary theorems for the Virtual Deduction tool
    2. Supplementary unification deductions
    3. Conventional Metamath proofs, some derived from VD proofs
    4. What is Virtual Deduction?
    5. Virtual Deduction Theorems
    6. Theorems proved using Virtual Deduction
    7. Theorems proved using Virtual Deduction with mmj2 assistance
    8. Virtual Deduction transcriptions of textbook proofs
    9. Theorems proved using conjunction-form Virtual Deduction
    10. Theorems with a VD proof in conventional notation derived from a VD proof
    11. Theorems with a proof in conventional notation derived from a VD proof
39. Mathbox for Glauco Siliprandi
    1. Miscellanea
    2. Functions
    3. Ordering on real numbers - Real and complex numbers basic operations
    4. Real intervals
    5. Finite sums
    6. Finite multiplication of numbers and finite multiplication of functions
    7. Limits
    8. Trigonometry
    9. Continuous Functions
    10. Derivatives
    11. Integrals
    12. Stone Weierstrass theorem - real version
    13. Wallis' product for π
    14. Stirling's approximation formula for ` n ` factorial
    15. Dirichlet kernel
    16. Fourier Series
    17. e is transcendental
    18. n-dimensional Euclidean space
    19. Basic measure theory
40. Mathbox for Saveliy Skresanov
    1. Ceva's theorem
    2. Simple groups
41. Mathbox for Jarvin Udandy
    1. hirstL-ax3
    2. ax3h
    3. aibandbiaiffaiffb
    4. aibandbiaiaiffb
    5. notatnand
    6. aistia
    7. aisfina
    8. bothtbothsame
    9. bothfbothsame
    10. aiffbbtat
    11. aisbbisfaisf
    12. axorbtnotaiffb
    13. aiffnbandciffatnotciffb
    14. axorbciffatcxorb
    15. aibnbna
    16. aibnbaif
    17. aiffbtbat
    18. astbstanbst
    19. aistbistaandb
    20. aisbnaxb
    21. atbiffatnnb
    22. bisaiaisb
    23. atbiffatnnbalt
    24. abnotbtaxb
    25. abnotataxb
    26. conimpf
    27. conimpfalt
    28. aistbisfiaxb
    29. aisfbistiaxb
    30. aifftbifffaibif
    31. aifftbifffaibifff
    32. atnaiana
    33. ainaiaandna
    34. abcdta
    35. abcdtb
    36. abcdtc
    37. abcdtd
    38. abciffcbatnabciffncba
    39. abciffcbatnabciffncbai
    40. nabctnabc
    41. jabtaib
    42. onenotinotbothi
    43. twonotinotbothi
    44. clifte
    45. cliftet
    46. clifteta
    47. cliftetb
    48. confun
    49. confun2
    50. confun3
    51. confun4
    52. confun5
    53. plcofph
    54. pldofph
    55. plvcofph
    56. plvcofphax
    57. plvofpos
    58. mdandyv0
    59. mdandyv1
    60. mdandyv2
    61. mdandyv3
    62. mdandyv4
    63. mdandyv5
    64. mdandyv6
    65. mdandyv7
    66. mdandyv8
    67. mdandyv9
    68. mdandyv10
    69. mdandyv11
    70. mdandyv12
    71. mdandyv13
    72. mdandyv14
    73. mdandyv15
    74. mdandyvr0
    75. mdandyvr1
    76. mdandyvr2
    77. mdandyvr3
    78. mdandyvr4
    79. mdandyvr5
    80. mdandyvr6
    81. mdandyvr7
    82. mdandyvr8
    83. mdandyvr9
    84. mdandyvr10
    85. mdandyvr11
    86. mdandyvr12
    87. mdandyvr13
    88. mdandyvr14
    89. mdandyvr15
    90. mdandyvrx0
    91. mdandyvrx1
    92. mdandyvrx2
    93. mdandyvrx3
    94. mdandyvrx4
    95. mdandyvrx5
    96. mdandyvrx6
    97. mdandyvrx7
    98. mdandyvrx8
    99. mdandyvrx9
    100. mdandyvrx10
    101. mdandyvrx11
    102. mdandyvrx12
    103. mdandyvrx13
    104. mdandyvrx14
    105. mdandyvrx15
    106. H15NH16TH15IH16
    107. dandysum2p2e4
    108. mdandysum2p2e4
42. Mathbox for Adhemar
    1. adh-jarrsc
    2. Minimal implicational calculus
43. Mathbox for Alexander van der Vekens
    1. General auxiliary theorems (1)
    2. Alternative for Russell's definition of a description binder
    3. Double restricted existential uniqueness
    4. Alternative definitions of function and operation values
    5. Alternative definitions of function values (2)
    6. General auxiliary theorems (2)
    7. Preimages of function values
    8. Partitions of real intervals
    9. Shifting functions with an integer range domain
    10. Words over a set (extension)
    11. Unordered pairs
    12. Number theory (extension)
    13. Even and odd numbers
    14. Number theory (extension 2)
    15. Graph theory (extension)
    16. Monoids (extension)
    17. Magmas and internal binary operations (alternate approach)
    18. Categories (extension)
    19. Rings (extension)
    20. Basic algebraic structures (extension)
    21. Linear algebra (extension)
    22. Complexity theory
    23. Elementary geometry (extension)
44. Mathbox for Emmett Weisz
    1. Miscellaneous Theorems
    2. Set Recursion
    3. Construction of Games and Surreal Numbers
45. Mathbox for David A. Wheeler
    1. Simplify propositional expressions
    2. Natural deduction
    3. Greater than, greater than or equal to.
    4. Hyperbolic trigonometric functions
    5. Reciprocal trigonometric functions (sec, csc, cot)
    6. Identities for "if"
    7. Other functions
    8. Logarithms generalized to arbitrary base using ` logb `
    9. Logarithm laws generalized to an arbitrary base - log_
    10. Gottlob Frege's work: _Begriffsschrift_ and _Grundgesetze der Arithmetik_
    11. Formally define terms such as Reflexivity
    12. Algebra helpers
    13. Algebra helper examples
    14. Formal methods "surprises"
    15. Allsome quantifier
    16. Miscellaneous
    17. Theorems about algebraic numbers
    18. Other results
    19. Examples
46. Mathbox for Kunhao Zheng
    1. Weighted AM-GM inequality