Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Difference of Two Natural Numbers with Zero
definitiondef:natural-number-difference-nbg-2026aAlgebraSet TheoryFor natural numbers with zero m ≤ n, the difference n − m is the unique natural number with zero that added to m gives n.Positive, Nonnegative, Negative and Nonpositive Elements of an Ordered Ring
definitiondef:sign-ordered-ring-nbg-2026aAlgebraAn element x of an ordered ring is positive if 0 < x, nonnegative if 0 ≤ x, negative if x < 0, and nonpositive if x ≤ 0.Natural Numbers Read in an Ordered Field Agree with the Canonical Embedding of the Rationals
lemmalem:ordered-field-numerals-nbg-2026aAlgebraIn every ordered field, a natural number with zero read as a multiple of 1 is the image of that natural number under the canonical embedding of the rationals.Natural Numbers Read in the Integers and in the Rationals Agree with Their Embeddings
lemmalem:numeral-images-nbg-2026aAlgebraThe image of a natural number with zero as a multiple of 1 in the integers, and in the rationals, coincides with its image under the canonical embeddings.- Fixes the standard notation in commutative rings, fields and ordered fields: negatives, differences, powers, finite sums and products, natural numbers read as multiples of 1, reciprocals and quotients, the order notation, absolute values and the sign words.
Arbitrary Positive Slack, and Approximation of Suprema and Infima, in the Real Numbers
lemmalem:real-approximation-nbg-2026aAnalysisAlgebraIn the real numbers, an inequality that holds up to every positive slack holds exactly, a nonnegative number below every positive number is zero, and the supremum or infimum of a nonempty set bounded above or below is approached by elements of the set, strictly and within every p…Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares
lemmalem:ordered-field-inequalities-nbg-2026bAlgebraFurther rules of order in an ordered field: mixed transitivity, adding a strict and a weak inequality, strict sign reversal, positivity of products, positivity of the natural numbers, halving, order of reciprocals, the strict absolute-value bound, the reverse triangle inequality,…Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field
lemmalem:commutative-ring-rules-nbg-2026bAlgebraIn a commutative ring, multiplying by zero gives zero, the sign rules hold, squares of sums and differences expand and differences of squares factor; a field has no zero divisors.The Image of a Natural Number in a Commutative Ring
definitiondef:natural-number-image-ring-nbg-2026bAlgebraThe image of a natural number n in a commutative ring is the sum of n copies of the unit, and the image of 0 is 0.- If e and e' are neutral elements of the same binary operation, then e = e*e' = e'.
Sums over Finite Sets in a Commutative Ring and in an Ordered Field: Distributivity, Products of Sums, Vanishing Terms, Sums over Pairs, Expanding Products of Sums, Counting, Comparison, Monotonicity and the Triangle Inequality
lemmalem:finite-set-sums-nbg-2026cAlgebraSums over finite sets in a commutative ring distribute over multiplication, commute with differences, multiply as a sum over the product set, ignore vanishing terms, give the number of elements times a constant term, can be taken over dependent pairs, and a product of sums expand…Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals
lemmalem:finite-set-operation-properties-nbg-2026bAlgebraFor an associative and commutative operation with a neutral element, the iterated operation over finite sets is additive over disjoint unions, invariant under reindexing by a bijection, computed over a product of sets as an iterated double operation in either order, combines term…Sums and Products over a Finite Set and over an Interval
definitiondef:finite-set-operation-nbg-2026bAlgebraFor an associative and commutative operation, the iterated operation of a map over a nonempty finite set is taken along any enumeration of the set, over the empty set it is the neutral element, and over an interval {m,...,n} it gives the sums and products from k=m to n.The Iterated Operation over a Finite Set Does Not Depend on the Enumeration
lemmalem:finite-set-operation-nbg-2026bAlgebraFor an associative and commutative operation, iterating it over the values of a map on a nonempty finite set gives the same result for every enumeration of the set.Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality
lemmalem:natural-powers-nbg-2026cAlgebraPowers satisfy the exponent laws and the factorisation of x^n - y^n; in a field the powers of a nonzero element are nonzero and the geometric sum formula holds; in an ordered field powers of nonnegative elements are nonnegative and strictly increasing in the base, monotone in the…Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality
lemmalem:finite-sums-nbg-2026bAlgebraFinite sums in a commutative ring distribute over multiplication, commute with negatives and differences, telescope, and a sum of n equal terms is n times the term; in an ordered field sums preserve (strict) inequalities between terms, a sum of nonnegative terms dominates each te…Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms
lemmalem:iterated-operation-properties-nbg-2026bAlgebraAn iterated operation obeys its recursion; for an associative operation it splits into the iterated operations of two consecutive blocks; for an associative and commutative operation it is unchanged by reordering the terms and combines termwise; and maps preserving the operation…- For an element x of a set with a multiplication, x^n is the product of n copies of x, and x^0 is the neutral element when there is one.
Iterated Operations: Finite Sums and Finite Products
definitiondef:iterated-operation-nbg-2026bAlgebraThe iterated operation of a list a_1,...,a_n combines its terms from left to right; written additively it is the finite sum, written multiplicatively the finite product.- For a binary operation on a set and a list a_1,...,a_n of its elements, there is exactly one list of partial results s_1,...,s_n with s_1=a_1 and s_{k+1}=s_k * a_{k+1}.