Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for David A. Wheeler
Metamath Proof Explorer
Table of Contents - 20.46. Mathbox for David A. Wheeler
This is the mathbox of David A. Wheeler, dwheeler at dwheeler dot com.
Among other things, I have added a number of formal definitions for
widely-used functions, e.g., those defined in
ISO 80000-2:2009(E)
Quantities and units - Part 2: Mathematical signs and
symbols used in the natural sciences and technology and the
NIST Digital Library of Mathematical Functions http://dlmf.nist.gov/ .
Simplify propositional expressions
Natural deduction
sbidd
sbidd-misc
Greater than, greater than or equal to.
cge-real
cgt
df-gte
df-gt
gte-lte
gt-lt
gte-lteh
gt-lth
ex-gt
ex-gte
Hyperbolic trigonometric functions
csinh
ccosh
ctanh
df-sinh
df-cosh
df-tanh
sinhval-named
coshval-named
tanhval-named
sinh-conventional
sinhpcosh
Reciprocal trigonometric functions (sec, csc, cot)
csec
ccsc
ccot
df-sec
df-csc
df-cot
secval
cscval
cotval
seccl
csccl
cotcl
reseccl
recsccl
recotcl
recsec
reccsc
reccot
rectan
sec0
onetansqsecsq
cotsqcscsq
Identities for "if"
ifnmfalse
Other functions
Logarithms generalized to arbitrary base using ` logb `
logb2aval
Logarithm laws generalized to an arbitrary base - log_
clog-
df-logbALT
Gottlob Frege's work: _Begriffsschrift_ and _Grundgesetze der Arithmetik_
Formally define notions such as reflexivity
wreflexive
df-reflexive
wirreflexive
df-irreflexive
Algebra helpers
comraddi
mvlraddi
mvrladdi
assraddsubi
joinlmuladdmuli
joinlmulsubmuld
joinlmulsubmuli
mvlrmuld
mvlrmuli
Algebra helper examples
i2linesi
i2linesd
Formal methods "surprises"
alimp-surprise
alimp-no-surprise
empty-surprise
empty-surprise2
eximp-surprise
eximp-surprise2
Allsome quantifier
walsi
walsc
df-alsi
df-alsc
alsconv
alsi1d
alsi2d
alsc1d
alsc2d
alscn0d
alsi-no-surprise
Miscellaneous
5m4e1
2p2ne5
resolution
testable
Theorems about algebraic numbers
aacllem
Other results
Examples