Home Metamath Proof ExplorerTheorem List (p. 210 of 321) < Previous  Next > Browser slow? Try the Unicode version.

 Color key: Metamath Proof Explorer (1-22269) Hilbert Space Explorer (22270-23792) Users' Mathboxes (23793-32079)

Theorem List for Metamath Proof Explorer - 20901-21000   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremdchrn0 20901 A Dirichlet character is nonzero on the units of ℤ/nℤ. (Contributed by Mario Carneiro, 18-Apr-2016.)
DChr       ℤ/n                     Unit

Theoremdchr1cl 20902* Closure of the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016.)
DChr       ℤ/n                     Unit

Theoremdchrmulid2 20903* Left identity for the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016.)
DChr       ℤ/n                     Unit

Theoremdchrinvcl 20904* Closure of the group inverse operation on Dirichlet characters. (Contributed by Mario Carneiro, 19-Apr-2016.)
DChr       ℤ/n                     Unit

Theoremdchrabl 20905 The set of Dirichlet characters is an Abelian group. (Contributed by Mario Carneiro, 19-Apr-2016.)
DChr

Theoremdchrfi 20906 The group of Dirichlet characters is a finite group. (Contributed by Mario Carneiro, 19-Apr-2016.)
DChr

Theoremdchrghm 20907 A Dirichlet character restricted to the unit group of ℤ/nℤ is a group homomorphism into the multiplicative group of nonzero complex numbers. (Contributed by Mario Carneiro, 21-Apr-2016.)
DChr       ℤ/n              Unit       mulGrps        mulGrpflds

Theoremdchr1 20908 Value of the principal Dirichlet character. (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr       ℤ/n              Unit

Theoremdchreq 20909* A Dirichlet character is determined by its values on the unit group. (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr       ℤ/n              Unit

Theoremdchrresb 20910 A Dirichlet character is determined by its values on the unit group. (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr       ℤ/n              Unit

Theoremdchrabs 20911 A Dirichlet character takes values on the unit circle. (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr                     ℤ/n       Unit

Theoremdchrinv 20912 The inverse of a Dirichlet character is the conjugate (which is also the multiplicative inverse, because the values of are unimodular). (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr

Theoremdchrabs2 20913 A Dirichlet character takes values inside the unit circle. (Contributed by Mario Carneiro, 3-May-2016.)
DChr              ℤ/n

Theoremdchr1re 20914 The principal Dirichlet character is a real character. (Contributed by Mario Carneiro, 2-May-2016.)
DChr       ℤ/n

Theoremdchrptlem1 20915* Lemma for dchrpt 20918. (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr       ℤ/n                                          Unit       mulGrps        .g                     Word        DProd        DProd        dProj

Theoremdchrptlem2 20916* Lemma for dchrpt 20918. (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr       ℤ/n                                          Unit       mulGrps        .g                     Word        DProd        DProd        dProj

Theoremdchrptlem3 20917* Lemma for dchrpt 20918. (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr       ℤ/n                                          Unit       mulGrps        .g                     Word        DProd        DProd

Theoremdchrpt 20918* For any element other than 1, there is a Dirichlet character that is not one at the given element. (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr       ℤ/n

Theoremdchrsum2 20919* An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character is if is non-principal and otherwise. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr       ℤ/n                            Unit

Theoremdchrsum 20920* An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character is if is non-principal and otherwise. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr       ℤ/n

Theoremsumdchr2 20921* Lemma for sumdchr 20923. (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr              ℤ/n

Theoremdchrhash 20922 There are exactly Dirichlet characters modulo . Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr

Theoremsumdchr 20923* An orthogonality relation for Dirichlet characters: the sum of for fixed and all is if and otherwise. Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr              ℤ/n

Theoremdchr2sum 20924* An orthogonality relation for Dirichlet characters: the sum of over all is nonzero only when . Part of Theorem 6.5.2 of [Shapiro] p. 232. (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr       ℤ/n

Theoremsum2dchr 20925* An orthogonality relation for Dirichlet characters: the sum of for fixed and all is if and otherwise. Part of Theorem 6.5.2 of [Shapiro] p. 232. (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr              ℤ/n              Unit

13.4.7  Bertrand's postulate

Theorembcctr 20926 Value of the central binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.)

Theorempcbcctr 20927* Prime count of a central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)

Theorembcmono 20928 The binomial coefficient is monotone in its second argument, up to the midway point. (Contributed by Mario Carneiro, 5-Mar-2014.)

Theorembcmax 20929 The binomial coefficient takes its maximum value at the center. (Contributed by Mario Carneiro, 5-Mar-2014.)

Theorembcp1ctr 20930 Ratio of two central binomial coefficients. (Contributed by Mario Carneiro, 10-Mar-2014.)

Theorembclbnd 20931 A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.)

Theoremefexple 20932 Convert a bound on a power to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.)

Theorembpos1lem 20933* Lemma for bpos1 20934. (Contributed by Mario Carneiro, 12-Mar-2014.)

Theorembpos1 20934* Bertrand's postulate, checked numerically for , using the prime sequence . (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
;

Theorembposlem1 20935 An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014.)

Theorembposlem2 20936 There are no odd primes in the range dividing the -th central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)

Theorembposlem3 20937* Lemma for bpos 20944. Since the binomial coefficient does not have any primes in the range or by bposlem2 20936 and prmfac1 13045, respectively, and it does not have any in the range by hypothesis, the product of the primes up through must be sufficient to compose the whole binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.)

Theorembposlem4 20938* Lemma for bpos 20944. (Contributed by Mario Carneiro, 13-Mar-2014.)

Theorembposlem5 20939* Lemma for bpos 20944. Bound the product of all small primes in the binomial coefficient. (Contributed by Mario Carneiro, 15-Mar-2014.)

Theorembposlem6 20940* Lemma for bpos 20944. By using the various bounds at our disposal, arrive at an inequality that is false for large enough. (Contributed by Mario Carneiro, 14-Mar-2014.)

Theorembposlem7 20941* Lemma for bpos 20944. The function is decreasing. (Contributed by Mario Carneiro, 13-Mar-2014.)

Theorembposlem8 20942 Lemma for bpos 20944. Evaluate and show it is less than . (Contributed by Mario Carneiro, 14-Mar-2014.)
; ;

Theorembposlem9 20943* Lemma for bpos 20944. Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014.)
;

Theorembpos 20944* Bertrand's postulate: there is a prime between and for every positive integer . This proof follows Erdős's method, for the most part, but with some refinements due to Shigenori Tochiori to save us some calculations of large primes. See http://en.wikipedia.org/wiki/Proof_of_Bertrand%27s_postulate for an overview of the proof strategy. (Contributed by Mario Carneiro, 14-Mar-2014.)

13.4.8  Legendre symbol

Syntaxclgs 20945 Extend class notation with the Legendre symbol function.

Definitiondf-lgs 20946* Define the Legendre symbol (actually the Kronecker symbol, which extends the Legendre symbol to all integers). (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgslem1 20947 When is coprime to the prime , is equivalent to or , and so adding makes it equivalent to or . (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgslem2 20948 The set of all integers with absolute value at most contains . (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgslem3 20949* The set of all integers with absolute value at most is closed under multiplication. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgslem4 20950* The function is closed in integers with absolute value less than (namely although this representation is less useful to us). (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsval 20951* Value of the Legendre symbol at an arbitrary integer. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsfval 20952* Value of the function which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsfcl2 20953* The function is closed in integers with absolute value less than (namely although this representation is less useful to us). (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgscllem 20954* The Legendre symbol is an element of . (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsfcl 20955* Closure of the function which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsfle1 20956* The function has magnitude less or equal to . (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsval2lem 20957* Lemma for lgsval2 20963. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsval4lem 20958* Lemma for lgsval4 20967. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgscl2 20959* The Legendre symbol is an integer with absolute value less or equal to . (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgs0 20960 The Legendre symbol when the second argument is zero. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgscl 20961 The Legendre symbol is an integer. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsle1 20962 The Legendre symbol has absolute value less or equal to . Together with lgscl 20961 this implies that it takes values in . (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsval2 20963 The Legendre symbol at a prime (this is the traditional domain of the Legendre symbol, except for the addition of prime ). (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgs2 20964 The Legendre symbol at . (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsval3 20965 The Legendre symbol at an odd prime (this is the traditional domain of the Legendre symbol). (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsvalmod 20966 The Legendre symbol is equivalent to , . (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsval4 20967* Restate lgsval 20951 for nonzero , where the function has been abbreviated into a self-referential expression taking the value of on the primes as given. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsfcl3 20968* Closure of the function which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsval4a 20969* Same as lgsval4 20967 for positive . (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsneg 20970 The Legendre symbol is either even or odd under negation with respect to the second parameter according to the sign of the first. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsneg1 20971 The Legendre symbol for nonnegative first parameter is unchanged by negation of the second. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsmod 20972 The Legendre (Jacobi) symbol is preserved under reduction when is odd. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsdilem 20973 Lemma for lgsdi 20983 and lgsdir 20981: the sign part of the Legendre symbol is multiplicative. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsdir2lem1 20974 Lemma for lgsdir2 20979. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsdir2lem2 20975 Lemma for lgsdir2 20979. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsdir2lem3 20976 Lemma for lgsdir2 20979. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsdir2lem4 20977 Lemma for lgsdir2 20979. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsdir2lem5 20978 Lemma for lgsdir2 20979. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsdir2 20979 The Legendre symbol is completely multiplicative at . (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsdirprm 20980 The Legendre symbol is completely multiplicative at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsdir 20981 The Legendre symbol is completely multiplicative in its left argument. Together with lgsqr 20997 this implies that the product of two quadratic residues or nonresidues is a residue, and the product of a residue and a nonresidue is a nonresidue. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsdilem2 20982* Lemma for lgsdi 20983. (Contributed by Mario Carneiro, 4-Feb-2015.)

Theoremlgsdi 20983 The Legendre symbol is completely multiplicative in its right argument. (Contributed by Mario Carneiro, 5-Feb-2015.)

Theoremlgsne0 20984 The Legendre symbol is nonzero (and hence equal to or ) precisely when the arguments are coprime. (Contributed by Mario Carneiro, 5-Feb-2015.)

Theoremlgsabs1 20985 The Legendre symbol is nonzero (and hence equal to or ) precisely when the arguments are coprime. (Contributed by Mario Carneiro, 5-Feb-2015.)

Theoremlgssq 20986 The Legendre symbol at a square is equal to . Together with lgsmod 20972 this implies that the Legendre symbol takes value at every quadratic residue. (Contributed by Mario Carneiro, 5-Feb-2015.)

Theoremlgssq2 20987 The Legendre symbol at a square is equal to . (Contributed by Mario Carneiro, 5-Feb-2015.)

Theorem1lgs 20988 The Legendre symbol at . (Contributed by Mario Carneiro, 28-Apr-2016.)

Theoremlgs1 20989 The Legendre symbol at . (Contributed by Mario Carneiro, 28-Apr-2016.)

Theoremlgsdirnn0 20990 Variation on lgsdir 20981 valid for all but only for positive . (The exact location of the failure of this law is for , , in which case but .) (Contributed by Mario Carneiro, 28-Apr-2016.)

Theoremlgsdinn0 20991 Variation on lgsdi 20983 valid for all but only for positive . (The exact location of the failure of this law is for , , and some in which case but when is not a quadratic residue mod .) (Contributed by Mario Carneiro, 28-Apr-2016.)

Theoremlgsqrlem1 20992 Lemma for lgsqr 20997. (Contributed by Mario Carneiro, 15-Jun-2015.)
ℤ/n       Poly1              deg1        eval1       .gmulGrp       var1                            RHom

Theoremlgsqrlem2 20993* Lemma for lgsqr 20997. (Contributed by Mario Carneiro, 15-Jun-2015.)
ℤ/n       Poly1              deg1        eval1       .gmulGrp       var1                            RHom

Theoremlgsqrlem3 20994* Lemma for lgsqr 20997. (Contributed by Mario Carneiro, 15-Jun-2015.)
ℤ/n       Poly1              deg1        eval1       .gmulGrp       var1                            RHom

Theoremlgsqrlem4 20995* Lemma for lgsqr 20997. (Contributed by Mario Carneiro, 15-Jun-2015.)
ℤ/n       Poly1              deg1        eval1       .gmulGrp       var1                            RHom

Theoremlgsqrlem5 20996* Lemma for lgsqr 20997. (Contributed by Mario Carneiro, 15-Jun-2015.)

Theoremlgsqr 20997* The Legendre symbol for odd primes is iff the number is not a multiple of the prime (in which case it is , see lgsne0 20984) and the number is a quadratic residue (it is for nonresidues by the process of elimination from lgsabs1 20985). Given our definition of the Legendre symbol, this theorem is equivalent to Euler's criterion. (Contributed by Mario Carneiro, 15-Jun-2015.)

Theoremlgsdchrval 20998* The Legendre symbol function , where is an odd positive number, is a Dirichlet character modulo . (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr       ℤ/n                     RHom

Theoremlgsdchr 20999* The Legendre symbol function , where is an odd positive number, is a real Dirichlet character modulo . (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr       ℤ/n                     RHom