Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Real and Imaginary Parts of a Complex Number
definitiondef:real-imaginary-parts-nbg-2026bAnalysisAlgebraThe real part and the imaginary part of a complex number z are the real numbers a and b with z = a + bi.The Complex Numbers Form a Field Containing the Real Numbers: i Squared Is -1 and Not Real, the Canonical Form a + bi and Its Arithmetic, and Numerals
lemmalem:complex-numbers-nbg-2026bAnalysisAlgebraThe pairs of real numbers form a field into which the reals embed by a -> (a,0), preserving the field operations and the images of natural numbers; i = (0,1) satisfies i^2 = -1 and is not real, every complex number is a + bi for exactly one pair of reals, and canonical forms add…The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit
definitiondef:complex-numbers-nbg-2026cAnalysisAlgebraDefines the complex numbers as ordered pairs of real numbers, with componentwise addition, the multiplication (a,b)(c,d) = (ac − bd, ad + bc), and the imaginary unit i = (0,1).Standard Examples of Series: the Harmonic Series, the Reciprocals of the Squares, a Centred Quadratic Sum and the Exponential Series
lemmalem:series-examples-nbg-2026bAnalysisThe harmonic series diverges, its partial sums being unbounded; the partial sums of the reciprocals of the squares are at most two minus the reciprocal of the index, so that series converges with sum at most two; a quadratic sum taken symmetrically about its centre is bounded ind…Properties of the Limit Superior and the Limit Inferior: Tail Formula, Order, Comparison, Bounds, Eventual and Frequent Inequalities, Subsequences, Negation and Convergence
lemmalem:limit-superior-inferior-nbg-2026bAnalysisFor bounded real sequences, the limit superior is the infimum of the tail suprema and the limit inferior the supremum of the tail infima; the limit inferior is at most the limit superior; both are monotone in the sequence and respect eventual bounds; the terms eventually lie with…The Limit Superior and the Limit Inferior of a Bounded Sequence of Real Numbers
definitiondef:limit-superior-inferior-nbg-2026bAnalysisThe limit superior and the limit inferior of a bounded real sequence are the limits of its tail suprema and of its tail infima.Tail Suprema and Tail Infima of a Bounded Sequence of Real Numbers
lemmalem:tail-bounds-nbg-2026bAnalysisThe terms of a bounded real sequence from any index on form a nonempty bounded set, with a supremum and an infimum that bracket the term at that index; these tail suprema decrease and tail infima increase with the index, and they converge to their infimum and supremum respectivel…Elementary Properties of Series of Real Numbers: Linearity, Null Terms, the Cauchy Criterion, Index Shifts, Tails, Order and Telescoping
lemmalem:series-nbg-2026bAnalysisConvergent series of real numbers can be added and scaled termwise, have null terms and null tails, satisfy the Cauchy criterion, may be shifted by finitely many terms, are compared termwise, and a telescoping series converges exactly when the underlying sequence does.Series of Real Numbers with Nonnegative Terms, Comparison, Absolute Convergence and the Geometric Series
lemmalem:nonnegative-series-nbg-2026bAnalysisA series of nonnegative reals converges exactly when its partial sums are bounded above, its sum then being their supremum; the comparison test, including the comparison of tails; absolute convergence implies convergence, with the triangle inequality and a dominated form; and the…Series of Real Numbers: Partial Sums, Convergence, the Sum and Absolute Convergence
definitiondef:series-nbg-2026eAnalysisDefines the partial sums of a real sequence, convergence and divergence of its series, the sum of a convergent series as the limit of the partial sums, and absolute convergence.Rules of Order in an Ordered Ring: Differences, Sums, Negatives, Products and Squares
lemmalem:ordered-ring-rules-nbg-2026aAlgebraThe basic rules of order in an ordered ring: comparison through differences, adding and negating inequalities, multiplying by nonnegative or nonpositive elements, the signs of products, nonnegativity of squares and of 1, and multiplying inequalities between nonnegative elements.- In a commutative ring, (s+t)^2 = s^2+2st+t^2 and (s+t)^4 = s^4+4s^3t+6s^2t^2+4st^3+t^4.
The Number of Elements of a Disjoint Finite Union
lemmalem:disjoint-union-count-nbg-2026aCombinatoricsSet TheoryThe number of elements of a union of finitely many pairwise disjoint finite sets is the sum of their numbers of elements, and equals the number of sets times r when each has r elements.Finite Sets: Removing an Element, Injective Self-Maps, Infinite Sets, Sets of Permutations, Pairs and Extended Tuples
lemmalem:finite-set-counting-nbg-2026bCombinatoricsSet TheoryRemoving an element from a finite set lowers its number of elements by one, injective self-maps of finite sets are bijections, the natural numbers are infinite, the set of permutations of [n] is finite and nonempty, and two standard bijections: onto a slice of a product and onto…The Number of Integers between Two Integers
lemmalem:integer-intervals-nbg-2026bCombinatoricsSet TheoryFor integers a at most b, the integers x with a at most x at most b form a finite set with b-a+1 elements.Iterated Operations over an Interval: Extracting One Term and Reversing the Order
lemmalem:finite-sum-extraction-nbg-2026aAlgebraCombinatoricsFor an associative and commutative operation, one term can be taken out of the iterated operation over an interval, and the order of the terms can be reversed.- In a commutative ring the n-th power of a sum x+y is the sum over k from 0 to n of the binomial coefficient of n and k times x^k y^(n-k).
- The binomial coefficient of two natural numbers with zero is the value at that pair of the unique map satisfying Pascal's recursion.
Bijections between Intervals: the Gap Map and the Reversal
lemmalem:interval-bijections-nbg-2026aCombinatoricsSet TheorySkipping one value j gives a bijection from [n] onto [n+1] without j, and a maps to N+1-a gives a bijection of [N] onto itself that is its own inverse.Binomial Coefficients: Existence and Uniqueness by Pascal's Recursion, Vanishing above the Diagonal, Diagonal and First Values, the Factorial Formula and Symmetry
lemmalem:binomial-coefficients-nbg-2026aCombinatoricsThere is exactly one map on pairs of natural numbers with zero satisfying Pascal's recursion with the boundary values 1 and 0, and it vanishes above the diagonal, is 1 on the diagonal and n at k=1, satisfies the factorial formula and is symmetric.