Metamath Proof Explorer

Table of Contents - 20.45. 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 Functionshttp://dlmf.nist.gov/.

1. Simplify propositional expressions
2. Natural deduction
   1. sbidd
   2. sbidd-misc
3. Greater than, greater than or equal to.
   1. cge-real
   2. cgt
   3. df-gte
   4. df-gt
   5. gte-lte
   6. gt-lt
   7. gte-lteh
   8. gt-lth
   9. ex-gt
   10. ex-gte
4. Hyperbolic trigonometric functions
   1. csinh
   2. ccosh
   3. ctanh
   4. df-sinh
   5. df-cosh
   6. df-tanh
   7. sinhval-named
   8. coshval-named
   9. tanhval-named
   10. sinh-conventional
   11. sinhpcosh
5. Reciprocal trigonometric functions (sec, csc, cot)
   1. csec
   2. ccsc
   3. ccot
   4. df-sec
   5. df-csc
   6. df-cot
   7. secval
   8. cscval
   9. cotval
   10. seccl
   11. csccl
   12. cotcl
   13. reseccl
   14. recsccl
   15. recotcl
   16. recsec
   17. reccsc
   18. reccot
   19. rectan
   20. sec0
   21. onetansqsecsq
   22. cotsqcscsq
6. Identities for "if"
   1. ifnmfalse
7. Other functions
8. Logarithms generalized to arbitrary base using ` logb `
   1. logb2aval
9. Logarithm laws generalized to an arbitrary base - log_
   1. clog-
   2. df-logbALT
10. Gottlob Frege's work: _Begriffsschrift_ and _Grundgesetze der Arithmetik_
11. Formally define terms such as Reflexivity
    1. wreflexive
    2. df-reflexive
    3. wirreflexive
    4. df-irreflexive
12. Algebra helpers
    1. comraddi
    2. mvlraddi
    3. mvrladdi
    4. assraddsubi
    5. joinlmuladdmuli
    6. joinlmulsubmuld
    7. joinlmulsubmuli
    8. mvlrmuld
    9. mvlrmuli
13. Algebra helper examples
    1. i2linesi
    2. i2linesd
14. Formal methods "surprises"
    1. alimp-surprise
    2. alimp-no-surprise
    3. empty-surprise
    4. empty-surprise2
    5. eximp-surprise
    6. eximp-surprise2
15. Allsome quantifier
    1. walsi
    2. walsc
    3. df-alsi
    4. df-alsc
    5. alsconv
    6. alsi1d
    7. alsi2d
    8. alsc1d
    9. alsc2d
    10. alscn0d
    11. alsi-no-surprise
16. Miscellaneous
    1. 5m4e1
    2. 2p2ne5
    3. resolution
    4. testable
17. Theorems about algebraic numbers
    1. aacllem
18. Other results
19. Examples