Metamath Proof Explorer

Table of Contents - 21.3. Mathbox for Thierry Arnoux

  1. Propositional Calculus - misc additions
    1. ad11antr
    2. simp-12l
    3. simp-12r
    4. an42ds
    5. an52ds
    6. an62ds
    7. an72ds
    8. an82ds
    9. syl22anbrc
    10. bian1d
    11. bian1dOLD
    12. orim12da
    13. or3di
    14. or3dir
    15. 3o1cs
    16. 3o2cs
    17. 3o3cs
    18. 13an22anass
  2. Predicate Calculus
    1. Predicate Calculus - misc additions
    2. Restricted quantification - misc additions
    3. Equality
    4. Double restricted existential uniqueness quantification
    5. Double restricted existential uniqueness quantification syntax
    6. Substitution (without distinct variables) - misc additions
    7. Existential "at most one" - misc additions
    8. Existential uniqueness - misc additions
    9. Restricted "at most one" - misc additions
    10. Restricted iota (description binder)
  3. General Set Theory
    1. Class abstractions (a.k.a. class builders)
    2. Image Sets
    3. Set relations and operations - misc additions
    4. Unordered pairs
    5. Unordered triples
    6. Conditional operator - misc additions
    7. Set union
    8. Indexed union - misc additions
    9. Indexed intersection - misc additions
    10. Disjointness - misc additions
  4. Relations and Functions
    1. Relations - misc additions
    2. Functions - misc additions
    3. Operations - misc additions
    4. The mapping operation
    5. Support of a function
    6. Explicit Functions with one or two points as a domain
    7. Isomorphisms - misc. additions
    8. Disjointness (additional proof requiring functions)
    9. First and second members of an ordered pair - misc additions
    10. Finite Sets
    11. Countable Sets
  5. Real and Complex Numbers
    1. sgnval2
    2. Complex operations - misc. additions
    3. Ordering on reals - misc additions
    4. Extended reals - misc additions
    5. Extended nonnegative integers - misc additions
    6. Real number intervals - misc additions
    7. Finite intervals of integers - misc additions
    8. Half-open integer ranges - misc additions
    9. The ` # ` (set size) function - misc additions
    10. The greatest common divisor operator - misc. additions
    11. Integers
    12. Decimal numbers
  6. Real and complex functions
    1. Signum (sgn or sign) function - misc. additions
    2. Integer powers - misc. additions
    3. Indicator Functions
  7. Decimal expansion
    1. cdp2
    2. df-dp2
    3. dp2eq1
    4. dp2eq2
    5. dp2eq1i
    6. dp2eq2i
    7. dp2eq12i
    8. dp20u
    9. dp20h
    10. dp2cl
    11. dp2clq
    12. rpdp2cl
    13. rpdp2cl2
    14. dp2lt10
    15. dp2lt
    16. dp2ltsuc
    17. dp2ltc
    18. Decimal point
    19. Division in the extended real number system
  8. Words over a set - misc additions
    1. wrdres
    2. wrdsplex
    3. wrdfsupp
    4. wrdpmcl
    5. pfx1s2
    6. pfxrn2
    7. pfxrn3
    8. pfxf1
    9. s1f1
    10. s2rnOLD
    11. s2f1
    12. s3rnOLD
    13. s3f1
    14. s3clhash
    15. ccatf1
    16. ccatdmss
    17. pfxlsw2ccat
    18. ccatws1f1o
    19. ccatws1f1olast
    20. wrdt2ind
    21. swrdrn2
    22. swrdrn3
    23. swrdf1
    24. swrdrndisj
    25. Splicing words (substring replacement)
    26. Cyclic shift of words
  9. Extensible Structures
    1. Structure restriction operator
    2. Posets
    3. Complete lattices
    4. Order Theory
    5. Chains
    6. Extended reals Structure - misc additions
    7. The extended nonnegative real numbers commutative monoid
  10. Algebra
    1. Monoids
    2. Monoids Homomorphisms
    3. Groups - misc additions
    4. Finitely supported group sums - misc additions
    5. Group or monoid sums over words
    6. Centralizers and centers - misc additions
    7. The symmetric group
    8. Transpositions
    9. Permutation Signs
    10. Permutation cycles
    11. The Alternating Group
    12. Signum in an ordered monoid
    13. Fixed points
    14. The Archimedean property for generic ordered algebraic structures
    15. Semiring left modules
    16. Simple groups
    17. Rings - misc additions
    18. Subrings generated by a set
    19. The zero ring
    20. Localization of rings
    21. Integral Domains
    22. Euclidean Domains
    23. Division Rings
    24. The field of rational numbers
    25. Subfields
    26. Field of fractions
    27. Field extensions generated by a set
    28. Ring homomorphisms - misc additions
    29. Scalar restriction operation
    30. The commutative ring of gaussian integers
    31. The archimedean ordered field of real numbers
    32. The quotient map and quotient modules
    33. The ring of integers modulo ` N `
    34. Independent sets and families
    35. Ring associates, ring units
    36. Subgroup sum / Sumset / Minkowski sum
    37. The quotient map
    38. Ideals
    39. Prime Ideals
    40. Maximal Ideals
    41. The semiring of ideals of a ring
    42. Prime Elements
    43. Unique factorization domains
    44. The ring of integers
    45. Univariate Polynomials
    46. Polynomial quotient and polynomial remainder
    47. Multivariate Polynomials
    48. The subring algebra
    49. Division Ring Extensions
    50. Vector Spaces
    51. Vector Space Dimension
  11. Field Extensions
    1. cfldext
    2. cfinext
    3. cextdg
    4. df-fldext
    5. df-extdg
    6. df-finext
    7. relfldext
    8. brfldext
    9. ccfldextrr
    10. fldextfld1
    11. fldextfld2
    12. fldextsubrg
    13. sdrgfldext
    14. fldextress
    15. brfinext
    16. extdgval
    17. fldextsdrg
    18. fldextsralvec
    19. extdgcl
    20. extdggt0
    21. fldexttr
    22. fldextid
    23. extdgid
    24. fldsdrgfldext
    25. fldsdrgfldext2
    26. extdgmul
    27. finextfldext
    28. finexttrb
    29. extdg1id
    30. extdg1b
    31. fldgenfldext
    32. fldextchr
    33. evls1fldgencl
    34. ccfldsrarelvec
    35. ccfldextdgrr
    36. fldextrspunlsplem
    37. fldextrspunlsp
    38. fldextrspunlem1
    39. fldextrspunfld
    40. fldextrspunlem2
    41. fldextrspundgle
    42. fldextrspundglemul
    43. fldextrspundgdvdslem
    44. fldextrspundgdvds
    45. fldext2rspun
    46. Algebraic numbers
    47. Algebraic extensions
    48. Minimal polynomials
    49. Quadratic Field Extensions
    50. Towers of quadratic extentions
  12. Constructible Numbers
    1. cconstr
    2. df-constr
    3. constrrtll
    4. constrrtlc1
    5. constrrtlc2
    6. constrrtcclem
    7. constrrtcc
    8. isconstr
    9. constr0
    10. constrsuc
    11. constrlim
    12. constrsscn
    13. constrsslem
    14. constr01
    15. constrss
    16. constrmon
    17. constrconj
    18. constrfin
    19. constrelextdg2
    20. constrextdg2lem
    21. constrextdg2
    22. constrext2chnlem
    23. constrfiss
    24. constrllcllem
    25. constrlccllem
    26. constrcccllem
    27. constrcbvlem
    28. constrllcl
    29. constrlccl
    30. constrcccl
    31. constrext2chn
    32. constrcn
    33. nn0constr
    34. constraddcl
    35. constrnegcl
    36. zconstr
    37. constrdircl
    38. iconstr
    39. constrremulcl
    40. constrcjcl
    41. constrrecl
    42. constrimcl
    43. constrmulcl
    44. constrreinvcl
    45. constrinvcl
    46. constrcon
    47. constrsdrg
    48. constrfld
    49. constrresqrtcl
    50. constrabscl
    51. constrsqrtcl
    52. Impossible constructions
  13. Matrices
    1. Submatrices
    2. Matrix literals
    3. Laplace expansion of determinants
  14. Topology
    1. ist0cld
    2. Open maps
    3. Regular spaces
    4. Topology of the unit circle
    5. Refinements
    6. Open cover refinement property
    7. Lindelöf spaces
    8. Paracompact spaces
    9. Spectrum of a ring
    10. Pseudometrics
    11. Continuity - misc additions
    12. Topology of the closed unit interval
    13. Topology of ` ( RR X. RR ) `
    14. Order topology - misc. additions
    15. Continuity in topological spaces - misc. additions
    16. Topology of the extended nonnegative real numbers ordered monoid
    17. Limits - misc additions
    18. Univariate polynomials
  15. Uniform Stuctures and Spaces
    1. Hausdorff uniform completion
  16. Topology and algebraic structures
    1. The norm on the ring of the integer numbers
    2. Topological ` ZZ ` -modules
    3. Canonical embedding of the field of the rational numbers into a division ring
    4. Canonical embedding of the real numbers into a complete ordered field
    5. Embedding from the extended real numbers into a complete lattice
    6. Canonical embeddings into the ordered field of the real numbers
    7. Topological Manifolds
    8. Extended sum
  17. Mixed Function/Constant operation
    1. cofc
    2. df-ofc
    3. ofceq
    4. ofcfval
    5. ofcval
    6. ofcfn
    7. ofcfeqd2
    8. ofcfval3
    9. ofcf
    10. ofcfval2
    11. ofcfval4
    12. ofcc
    13. ofcof
  18. Abstract measure
    1. Sigma-Algebra
    2. Generated sigma-Algebra
    3. lambda and pi-Systems, Rings of Sets
    4. The Borel algebra on the real numbers
    5. Product Sigma-Algebra
    6. Measures
    7. The counting measure
    8. The Lebesgue measure - misc additions
    9. The Dirac delta measure
    10. The 'almost everywhere' relation
    11. Measurable functions
    12. Borel Algebra on ` ( RR X. RR ) `
    13. Caratheodory's extension theorem
    14. Caratheodory's extension theorem: examples and applications
    15. Caratheodory's extension theorem: measure on RR ^ N
  19. Integration
    1. Lebesgue integral - misc additions
    2. Bochner integral
  20. Euler's partition theorem
    1. oddpwdc
    2. oddpwdcv
    3. eulerpartlemsv1
    4. eulerpartlemelr
    5. eulerpartlemsv2
    6. eulerpartlemsf
    7. eulerpartlems
    8. eulerpartlemsv3
    9. eulerpartlemgc
    10. eulerpartleme
    11. eulerpartlemv
    12. eulerpartlemo
    13. eulerpartlemd
    14. eulerpartlem1
    15. eulerpartlemb
    16. eulerpartlemt0
    17. eulerpartlemf
    18. eulerpartlemt
    19. eulerpartgbij
    20. eulerpartlemgv
    21. eulerpartlemr
    22. eulerpartlemmf
    23. eulerpartlemgvv
    24. eulerpartlemgu
    25. eulerpartlemgh
    26. eulerpartlemgf
    27. eulerpartlemgs2
    28. eulerpartlemn
    29. eulerpart
  21. Sequences defined by strong recursion
    1. csseq
    2. df-sseq
    3. subiwrd
    4. subiwrdlen
    5. iwrdsplit
    6. sseqval
    7. sseqfv1
    8. sseqfn
    9. sseqmw
    10. sseqf
    11. sseqfres
    12. sseqfv2
    13. sseqp1
  22. Fibonacci Numbers
    1. cfib
    2. df-fib
    3. fiblem
    4. fib0
    5. fib1
    6. fibp1
    7. fib2
    8. fib3
    9. fib4
    10. fib5
    11. fib6
  23. Probability
    1. Probability Theory
    2. Conditional Probabilities
    3. Real-valued Random Variables
    4. Preimage set mapping operator
    5. Distribution Functions
    6. Cumulative Distribution Functions
    7. Probabilities - example
    8. Bertrand's Ballot Problem
  24. Signum (sgn or sign) function - misc. additions
    1. fzssfzo
    2. gsumncl
    3. gsumnunsn
    4. Operations on words
  25. Polynomials with real coefficients - misc additions
    1. plymul02
    2. plymulx0
    3. plymulx
    4. plyrecld
    5. signsplypnf
    6. signsply0
  26. Descartes's rule of signs
    1. Sign changes in a word over real numbers
    2. Counting sign changes in a word over real numbers
    3. Sign changes in a polynomial with real coefficients
  27. Number Theory
    1. iblidicc
    2. rpsqrtcn
    3. divsqrtid
    4. cxpcncf1
    5. efmul2picn
    6. fct2relem
    7. ftc2re
    8. fdvposlt
    9. fdvneggt
    10. fdvposle
    11. fdvnegge
    12. prodfzo03
    13. actfunsnf1o
    14. actfunsnrndisj
    15. itgexpif
    16. fsum2dsub
    17. Representations of a number as sums of integers
    18. Vinogradov Trigonometric Sums and the Circle Method
    19. The Ternary Goldbach Conjecture: Final Statement
  28. Elementary Geometry
    1. Two-dimensional geometry
    2. Morley's Miracle
    3. Outer Five Segment (not used, no need to move to main)
  29. LeftPad Project
    1. clpad
    2. df-lpad
    3. lpadval
    4. lpadlem1
    5. lpadlem3
    6. lpadlen1
    7. lpadlem2
    8. lpadlen2
    9. lpadmax
    10. lpadleft
    11. lpadright