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. Singletons
    5. Unordered pairs
    6. Unordered triples
    7. Conditional operator - misc additions
    8. Set union
    9. Indexed union - misc additions
    10. Indexed intersection - misc additions
    11. 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. Supremum - misc additions
    11. Finite Sets
    12. Countable Sets
  5. Real and Complex Numbers
    1. Complex operations - misc. additions
    2. Ordering on reals - misc additions
    3. Extended reals - misc additions
    4. Extended nonnegative integers - misc additions
    5. Real number intervals - misc additions
    6. Finite intervals of integers - misc additions
    7. Half-open integer ranges - misc additions
    8. The ` # ` (set size) function - misc additions
    9. The greatest common divisor operator - misc. additions
    10. Integers
    11. Decimal numbers
  6. Real and complex functions
    1. Integer powers - misc. additions
    2. 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. wrdfd
    2. wrdres
    3. wrdsplex
    4. wrdfsupp
    5. wrdpmcl
    6. pfx1s2
    7. pfxrn2
    8. pfxrn3
    9. pfxf1
    10. s1f1
    11. s2rnOLD
    12. s2f1
    13. s3rnOLD
    14. s3f1
    15. s3clhash
    16. ccatf1
    17. ccatdmss
    18. pfxlsw2ccat
    19. ccatws1f1o
    20. ccatws1f1olast
    21. wrdt2ind
    22. swrdrn2
    23. swrdrn3
    24. swrdf1
    25. swrdrndisj
    26. Splicing words (substring replacement)
    27. Cyclic shift of words
  9. Extensible Structures
    1. Structure restriction operator
    2. The opposite group
    3. Posets
    4. Complete lattices
    5. Order Theory
    6. Chains
    7. Extended reals Structure - misc additions
    8. 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. Totally ordered monoids and groups
    8. The symmetric group
    9. Transpositions
    10. Permutation Signs
    11. Permutation cycles
    12. The Alternating Group
    13. Signum in an ordered monoid
    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. Totally ordered rings and fields
    29. Ring homomorphisms - misc additions
    30. Scalar restriction operation
    31. The commutative ring of gaussian integers
    32. The archimedean ordered field of real numbers
    33. The quotient map and quotient modules
    34. The ring of integers modulo ` N `
    35. Independent sets and families
    36. Ring associates, ring units
    37. Subgroup sum / Sumset / Minkowski sum
    38. The quotient map
    39. Ideals
    40. Prime Ideals
    41. Maximal Ideals
    42. The semiring of ideals of a ring
    43. Prime Elements
    44. Unique factorization domains
    45. The ring of integers
    46. Univariate Polynomials
    47. Polynomial quotient and polynomial remainder
    48. The subring algebra
    49. Division Ring Extensions
    50. Vector Spaces
    51. Vector Space Dimension
  11. Field Extensions
    1. cfldext
    2. cfinext
    3. calgext
    4. cextdg
    5. df-fldext
    6. df-extdg
    7. df-finext
    8. df-algext
    9. relfldext
    10. brfldext
    11. ccfldextrr
    12. fldextfld1
    13. fldextfld2
    14. fldextsubrg
    15. sdrgfldext
    16. fldextress
    17. brfinext
    18. extdgval
    19. fldextsdrg
    20. fldextsralvec
    21. extdgcl
    22. extdggt0
    23. fldexttr
    24. fldextid
    25. extdgid
    26. fldsdrgfldext
    27. fldsdrgfldext2
    28. extdgmul
    29. finexttrb
    30. extdg1id
    31. extdg1b
    32. fldgenfldext
    33. fldextchr
    34. evls1fldgencl
    35. ccfldsrarelvec
    36. ccfldextdgrr
    37. fldextrspunlsplem
    38. fldextrspunlsp
    39. fldextrspunlem1
    40. fldextrspunfld
    41. fldextrspunlem2
    42. fldextrspundgle
    43. fldextrspundglemul
    44. fldextrspundgdvdslem
    45. fldextrspundgdvds
    46. fldext2rspun
    47. Algebraic numbers
    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. sgncl
    2. sgnclre
    3. sgnneg
    4. sgn3da
    5. sgnmul
    6. sgnmulrp2
    7. sgnsub
    8. sgnnbi
    9. sgnpbi
    10. sgn0bi
    11. sgnsgn
    12. sgnmulsgn
    13. sgnmulsgp
    14. fzssfzo
    15. gsumncl
    16. gsumnunsn
    17. 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