Metamath Proof Explorer

Table of Contents - 5. REAL AND COMPLEX NUMBERS

This section derives the basics of real and complex numbers. We first construct and axiomatize real and complex numbers (e.g., ax-resscn). After that, we derive their basic properties, various operations like addition (df-add) and sine (df-sin), and subsets such as the integers (df-z) and natural numbers (df-nn).

  1. Construction and axiomatization of real and complex numbers
    1. Dedekind-cut construction of real and complex numbers
    2. Final derivation of real and complex number postulates
    3. Real and complex number postulates restated as axioms
  2. Derive the basic properties from the field axioms
    1. Some deductions from the field axioms for complex numbers
    2. Infinity and the extended real number system
    3. Restate the ordering postulates with extended real "less than"
    4. Ordering on reals
    5. Initial properties of the complex numbers
  3. Real and complex numbers - basic operations
    1. Addition
    2. Subtraction
    3. Multiplication
    4. Ordering on reals (cont.)
    5. Reciprocals
    6. Division
    7. Ordering on reals (cont.)
    8. Completeness Axiom and Suprema
    9. Imaginary and complex number properties
    10. Function operation analogue theorems
  4. Integer sets
    1. Positive integers (as a subset of complex numbers)
    2. Principle of mathematical induction
    3. Decimal representation of numbers
    4. Some properties of specific numbers
    5. Simple number properties
    6. The Archimedean property
    7. Nonnegative integers (as a subset of complex numbers)
    8. Extended nonnegative integers
    9. Integers (as a subset of complex numbers)
    10. Decimal arithmetic
    11. Upper sets of integers
    12. Well-ordering principle for bounded-below sets of integers
    13. Rational numbers (as a subset of complex numbers)
    14. Existence of the set of complex numbers
  5. Order sets
    1. Positive reals (as a subset of complex numbers)
    2. Infinity and the extended real number system (cont.)
    3. Supremum and infimum on the extended reals
    4. Real number intervals
    5. Finite intervals of integers
    6. Finite intervals of nonnegative integers
    7. Half-open integer ranges
  6. Elementary integer functions
    1. The floor and ceiling functions
    2. The modulo (remainder) operation
    3. Miscellaneous theorems about integers
    4. Strong induction over upper sets of integers
    5. Finitely supported functions over the nonnegative integers
    6. The infinite sequence builder "seq" - extension
    7. Integer powers
    8. Ordered pair theorem for nonnegative integers
    9. Factorial function
    10. The binomial coefficient operation
    11. The ` # ` (set size) function
  7. Words over a set
    1. Definitions and basic theorems
    2. Last symbol of a word
    3. Concatenations of words
    4. Singleton words
    5. Concatenations with singleton words
    6. Subwords/substrings
    7. Prefixes of a word
    8. Subwords of subwords
    9. Subwords and concatenations
    10. Subwords of concatenations
    11. Splicing words (substring replacement)
    12. Reversing words
    13. Repeated symbol words
    14. Cyclical shifts of words
    15. Mapping words by a function
    16. Longer string literals
  8. Reflexive and transitive closures of relations
    1. The reflexive and transitive properties of relations
    2. Basic properties of closures
    3. Definitions and basic properties of transitive closures
    4. Exponentiation of relations
    5. Reflexive-transitive closure as an indexed union
    6. Principle of transitive induction.
  9. Elementary real and complex functions
    1. The "shift" operation
    2. Signum (sgn or sign) function
    3. Real and imaginary parts; conjugate
    4. Square root; absolute value
  10. Elementary limits and convergence
    1. Superior limit (lim sup)
    2. Limits
    3. Finite and infinite sums
    4. The binomial theorem
    5. The inclusion/exclusion principle
    6. Infinite sums (cont.)
    7. Miscellaneous converging and diverging sequences
    8. Arithmetic series
    9. Geometric series
    10. Ratio test for infinite series convergence
    11. Mertens' theorem
    12. Finite and infinite products
    13. Falling and Rising Factorial
    14. Bernoulli polynomials and sums of k-th powers
  11. Elementary trigonometry
    1. The exponential, sine, and cosine functions
    2. _e is irrational
  12. Cardinality of real and complex number subsets
    1. Countability of integers and rationals
    2. The reals are uncountable