Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- For natural numbers with zero m and n, the interval {m,...,n} consists of the k with m ≤ k ≤ n, and [n] denotes {1,...,n}.
The Natural Numbers with Zero and Their Embedding into the Integers
lemmalem:natural-numbers-with-zero-nbg-2026aAlgebraSet TheoryThe set of natural numbers with zero is the set of natural numbers together with zero, and sending zero to the integer zero and each natural number n to the integer ι(n) gives an injective map into the integers that preserves sums, products and order, with the nonnegative integer…Multiplication of Dedekind Cuts: Associativity, Commutativity, Unit, Distributivity, Reciprocals and Nonnegative Products
lemmalem:dedekind-cut-multiplication-nbg-2026aAlgebraSet TheoryMultiplication of Dedekind cuts is associative, commutative and distributive over addition, has the cut of 1 as unit, gives every nonzero cut a reciprocal, keeps products of nonnegative cuts nonnegative, and multiplies rational cuts like the rationals.Addition and Order of Dedekind Cuts: an Ordered Abelian Group in Which Every Nonempty Set Bounded Above Has a Supremum
lemmalem:dedekind-cut-addition-order-nbg-2026aAlgebraSet TheoryAddition of Dedekind cuts is associative and commutative with neutral element the zero cut and inverses given by the negative; it respects inclusion; every nonempty set of cuts bounded above has its union as supremum; and rational cuts add and compare like the rationals.- The real numbers are the Dedekind cuts of the rationals, ordered by inclusion, added elementwise, and multiplied through the products of their absolute values with the sign fixed by the signs of the factors; zero and one are the cuts of the rationals 0 and 1.
Construction of the Dedekind Cuts: They Form a Set Totally Ordered by Inclusion, Closed under Sums, Negatives and Products of Nonnegative Cuts
lemmalem:dedekind-cut-construction-nbg-2026aAlgebraSet TheoryThe downward-closed proper nonempty sets of rationals without a greatest element form a set, totally ordered by inclusion; rational cuts, sums, negatives and products of nonnegative cuts are again such sets.The Integers and the Rational Numbers, with the Natural Numbers and the Integers Identified with Subsets of the Rationals
settingset:rational-numbers-nbg-2026cAlgebraSet TheoryFixes the integers as an ordered ring and the rationals as an ordered field, with the standard notation, and identifies natural numbers, integers and sets of them with their images in the rationals, so that N ⊆ N_0 ⊆ Z ⊆ Q.The Natural Numbers and the Integers inside the Rational Numbers
lemmalem:rational-embedding-nbg-2026aAlgebraSet TheoryInside the rationals, the natural numbers sit via n ↦ j(ι(n)), which is injective, positive and preserves 1, sums, products and order; the negations of Z and Q are their ring negatives; and every rational [x, m] is the quotient of the integer x by the natural number m.Rules of Arithmetic and Order in an Ordered Field
lemmalem:ordered-field-rules-nbg-2026aAlgebraSet TheoryThe familiar rules in an ordered field: zero products, signs, reciprocals, adding and multiplying inequalities, squares are nonnegative and 0 < 1, reciprocals of positive elements, the midpoint of two elements lies strictly between them, and the properties of absolute value inclu…- Defines the absolute value |x| in an ordered field as x when 0 ≤ x and −x otherwise.
Negatives, Differences, Reciprocals and Quotients
definitiondef:field-inverses-nbg-2026aAlgebraSet TheoryDefines the negative −x and the difference x − y in a commutative ring, and the reciprocal y⁻¹ and the quotient x/y for y ≠ 0 in a field.- In a commutative ring every element has exactly one additive inverse, and in a field every nonzero element has exactly one multiplicative inverse.
- Defines the first and second components p₁ and p₂ of an ordered pair p, the unique sets with p = (p₁, p₂).
- A formula for the values defines exactly one map, on a set or on a Cartesian product, and a formula in two variables defines exactly one relation on a set.
- Defines an ordered ring as a commutative ring with a total order such that adding the same element preserves the order and products of nonnegative elements are nonnegative.
The Rational Numbers Form an Archimedean Ordered Field Containing the Integers
lemmalem:rationals-nbg-2026aAlgebraSet TheoryThe rational numbers form an Archimedean ordered field whose strict order is the strict relation of its order; the integers embed into it preserving 0, 1, the operations and the order, two fractions are equal exactly when their cross products agree, and each fraction times its de…- Defines the rational numbers as the classes [x, m] of pairs of an integer and a natural number (thought of as x/m), with the sum, product, negation and order of the construction lemma, the rationals 0 and 1, and the embedding x ↦ [x, 1] of the integers.
Construction of the Rationals: Pairs of an Integer and a Natural Number up to Equal Ratios, with Sum, Product, Negation and Order
lemmalem:rational-construction-nbg-2026aAlgebraSet TheoryPairs (x, m) of an integer and a natural number, thought of as x/m, with (x, m) ≈ (y, n) when x·n = y·m, form an equivalence relation; on the classes [x, m] there are unique sum, product, negation and order given by the usual formulas.The Integers Form an Ordered Ring Containing the Natural Numbers as Its Positive Elements
lemmalem:integers-nbg-2026aAlgebraSet TheoryThe integers form an ordered commutative ring; negation behaves as expected; the embedding of N is injective and preserves 1, sums, products and the order; [a, b] = ι(a) − ι(b); every integer is positive (the image of N), zero or negative; and there are no zero divisors, so nonze…- Defines the integers as the classes [a, b] of pairs of natural numbers (thought of as a − b), with the sum, product, negation and order of the construction lemma, the integers 0 = [1, 1] and 1 = [2, 1], and the embedding n ↦ [n + 1, 1] of N.