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.Uniqueness of the Complex Numbers: Every Field Generated over an Embedded Copy of the Reals by a Square Root of -1 Is Uniquely Isomorphic to C
theoremthm:complex-numbers-unique-nbg-2026aAlgebraIf a field K contains an injective homomorphic copy of the reals and an element u with u squared equal to -1 such that every element of K has the form a+bu with a, b in that copy, then exactly one map from C to K preserves sums and products, extends the embedding and sends i to u…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).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.
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).
Products over Finite Sets: a Single Factor, Vanishing in a Field, and Signs and Monotonicity in an Ordered Ring
lemmalem:finite-products-nbg-2026aAlgebraA product over a finite set whose factors are all 1 but one equals that factor; in a field it vanishes exactly when a factor does; and in an ordered ring it is nonnegative for nonnegative factors and monotone in them.- For m and n in N_0, m divides n if n=mk for some k in N_0.
Parity: Every Natural Number with Zero Is Either Even or Odd, and Parity of Natural Numbers
lemmalem:parity-nbg-2026aAlgebraSet TheoryEvery element of N_0 is even or odd and not both, and for a natural number the witnesses can be taken in N.- An element n of N_0 is even if n=2k and odd if n=2k+1 for some k in N_0.
A Sum of Natural Numbers Exceeds Each Summand and Is Not One
lemmalem:natural-number-sums-nbg-2026aAlgebraSet TheoryFor natural numbers a and b, the sum a+b is strictly greater than a and differs from 1.- If one integer is less than another, then it is less than the other by at least one.
The Maximum and Minimum of Two Elements of an Ordered Field: Sum, Difference and Absolute Value
lemmalem:max-min-ordered-field-nbg-2026aAlgebraIn an ordered field the maximum and minimum of two elements add up to their sum and differ by the absolute value of their difference, and the absolute value of an element is the maximum of it and its negative.The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products
lemmalem:natural-number-image-ring-nbg-2026bAlgebraSet TheoryThe images of 0 and 1 in a commutative ring are its zero and unit, and the image of a sum, product, difference, power, finite sum or finite product of natural numbers with zero is the corresponding expression in the images.