Database
REAL AND COMPLEX NUMBERS
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 ).

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