Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Construction of the Integers: Pairs of Natural Numbers up to Equal Differences, with Sum, Product, Negation and Order
lemmalem:integer-construction-nbg-2026aAlgebraSet TheoryPairs (a, b) of natural numbers, thought of as a − b, with (a, b) ~ (c, d) when a + d = b + c, form an equivalence relation; on the classes [a, b] there are unique sum, product, negation and order given by the usual formulas.- Defines an ordered field as a field with a total order that makes it an ordered ring.
- Defines a field as a commutative ring with 0 ≠ 1 in which every nonzero element has a multiplicative inverse.
- Defines a commutative ring (with identity) as a set with two binary operations and two distinguished elements 0 and 1 satisfying the associative, commutative, identity, additive-inverse and distributive laws.
Compatible Operations, Maps and Relations Pass to the Quotient
lemmalem:quotient-compatible-nbg-2026aSet TheoryFor an equivalence relation on a set, a binary operation, a self-map or a relation that respects the equivalence induces exactly one binary operation, self-map or relation on the quotient acting on classes through representatives.The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion
settingset:natural-numbers-nbg-2026cSet TheoryFixes the natural numbers and the natural numbers with zero, with their arithmetic, order, digits, induction and recursion, on top of the ordinary notation for sets and maps; natural numbers are used as numbers only, never as sets.Recursion on the Natural Numbers Starting at One
corollarycor:recursion-natural-numbers-nbg-2026bSet TheoryGiven a set a, a starting value c in a and a map g from N × a to a, there is exactly one map f from N to a with f(1) = c and f(n + 1) = g(n, f(n)) for every natural number n.- The familiar laws of the natural numbers in terms of N, 1, +, · and ≤: commutativity, associativity, distributivity, cancellation, the order laws and trichotomy, a < b exactly when b = a + d, compatibility of the order with + and ·, 1 is least, nothing lies between a and a + 1, e…
- Defines multiplication on omega by recursion, with m · 0 = 0 and m · S(n) = m · n + m, shows it is a binary operation on omega, and fixes that products are formed before sums.
- Defines the digits 2 to 9 as iterated successors of 1, and defines the value of a decimal numeral such as 156 by Horner's rule in base S(9): a numeral with last digit d denotes the shorter numeral times S(9), plus d.
- From dependent choice: for every family of subsets of a set b indexed by N, each with at least one element, there is a sequence in b whose m-th term lies in the m-th subset.
- If R is a relation on a set b in which every element is related to some element, then from any starting point s in b there is a sequence indexed by N starting at s whose consecutive terms are related by R.
The Principle of Induction for the Natural Numbers Starting at One
theoremthm:induction-natural-numbers-nbg-2026aSet TheoryA class of natural numbers that contains 1 and contains the successor of each of its elements is all of N.Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication
lemmalem:natural-numbers-nbg-2026aSet TheoryThe natural numbers are exactly the successors of elements of omega; 1 is the least natural number and is not the successor of a natural number; the successor is injective; S(n) = n + 1 and n · 1 = n; and N is closed under addition and multiplication.- Defines the set N of natural numbers as omega without 0, and the number 1 as the successor of 0.
Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order
lemmalem:omega-multiplication-nbg-2026aSet TheoryMultiplication on omega satisfies m · 0 = 0 · m = 0, both successor rules and m · 1 = 1 · m = m; it distributes over addition, is associative and commutative, has no zero divisors, and multiplication by a nonzero factor preserves the strict order and can be cancelled.Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order
lemmalem:omega-addition-nbg-2026aSet TheoryAddition on omega satisfies m + 0 = 0 + m = m and both successor rules, is associative, commutative and cancellative, is strictly compatible with the order, m ≤ n exactly when n = m + j for some j, and a sum is zero only when both terms are.- Defines addition on omega by recursion, with m + 0 = m and m + S(n) = S(m + n), and shows that it is a binary operation on omega.
- Given a set a, a starting value c in a and a map g from omega × a to a, there is exactly one map f from omega to a with f(0) = c and f(S(n)) = g(n, f(n)) for every n.
The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor
lemmalem:omega-order-nbg-2026aSet TheoryThe order on omega is a well-order whose strict order is membership; zero is its least element; m < S(n) exactly when m ≤ n, so nothing lies strictly between n and its successor; m < n exactly when S(m) ≤ n; and each n is the set of elements of omega below it.