Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers
settingset:complex-numbers-nbg-2026aAnalysisAlgebraStanding notation for the complex numbers: the field C of pairs of reals with its imaginary unit i, the real numbers (and through them the naturals, integers and rationals) identified with their images under a |-> (a,0), and the canonical form a + bi with i^2 = -1.Conjugation and Modulus of Complex Numbers: Field Automorphism, Real and Imaginary Parts, Multiplicativity, Inverses, Component Bounds, Triangle Inequalities and Finite Sums
lemmalem:complex-conjugate-modulus-nbg-2026aAnalysisAlgebraComplex conjugation is an involutive field automorphism of C fixing exactly the reals; real and imaginary parts are additive and real-homogeneous; the modulus is nonnegative, definite, multiplicative, bounded by and bounding the components, satisfies the triangle and reverse tria…- The modulus of z is the square root of (Re z)^2 + (Im z)^2; for a real number it is its absolute value, so the notation |x| is unambiguous.
- The complex conjugate of z is Re z - (Im z) i.
Real and Imaginary Parts of a Complex Number
definitiondef:real-imaginary-parts-nbg-2026aAnalysisAlgebraThe 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-2026aAnalysisAlgebraThe 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-2026aAnalysisAlgebraDefines 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-2026aAnalysisThe 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-2026aAnalysisFor 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-2026aAnalysisThe 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-2026aAnalysisThe 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-2026aAnalysisConvergent 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-2026aAnalysisA 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-2026aAnalysisDefines 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.Every Sequence in a Totally Ordered Set Has a Monotone Subsequence
lemmalem:monotone-subsequence-nbg-2026aAnalysisEvery sequence in a totally ordered set has a nondecreasing subsequence or a strictly decreasing subsequence, and in particular a monotone subsequence.The Factorial: Recursion, Positivity and Bounds by Powers
lemmalem:factorial-nbg-2026aAnalysisCombinatoricsThe factorial satisfies 0! = 1 and (n+1)! = (n+1)·n!, is at least 1 and nondecreasing, and (n+1)! lies between 2^n and (n+1)^(n+1).- The factorial n! of n in the natural numbers with zero is the product of 1, ..., n in the natural numbers with zero, the empty product being 1.
- In a totally ordered set, any two elements a and b have a maximum and a minimum, which are the larger and the smaller of the two, and they are the least upper and greatest lower bounds of a and b.
Properties of k-th Roots: Inverse to Powers, Absolute Values, Products, Monotonicity, Subadditivity, Differences and Limits
lemmalem:root-properties-nbg-2026aAnalysisThe k-th root inverts the k-th power on nonnegative reals, the square root of a square is the absolute value, roots are multiplicative, strictly increasing and subadditive, the difference of roots is at most the root of the difference, and roots of a convergent nonnegative sequen…- The k-th root of a nonnegative real number x is the unique nonnegative real number whose k-th power is x; the second root is the square root.