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