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

 Color key: Metamath Proof Explorer (1-21498) Hilbert Space Explorer (21499-23021) Users' Mathboxes (23022-32154)

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

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

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

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

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

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

Theoremdchrpt 20506* 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 20507* 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 20508* 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 20509* Lemma for sumdchr 20511. (Contributed by Mario Carneiro, 28-Apr-2016.)
DChr              ℤ/n

Theoremdchrhash 20510 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 20511* 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 20512* 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 20513* 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 20514 Value of the central binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.)

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

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

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

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

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

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

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

Theorembpos1 20522* 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 20523 An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014.)

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

Theorembposlem3 20525* Lemma for bpos 20532. Since the binomial coefficient does not have any primes in the range or by bposlem2 20524 and prmfac1 12797, 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 20526* Lemma for bpos 20532. (Contributed by Mario Carneiro, 13-Mar-2014.)

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

Theorembposlem6 20528* Lemma for bpos 20532. 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 20529* Lemma for bpos 20532. The function is decreasing. (Contributed by Mario Carneiro, 13-Mar-2014.)

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

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

Theorembpos 20532* 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 20533 Extend class notation with the Legendre symbol function.

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

Theoremlgslem1 20535 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 20536 The set of all integers with absolute value at most contains . (Contributed by Mario Carneiro, 4-Feb-2015.)

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

Theoremlgslem4 20538* 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 20539* Value of the Legendre symbol at an arbitrary integer. (Contributed by Mario Carneiro, 4-Feb-2015.)

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

Theoremlgsfcl2 20541* 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 20542* The Legendre symbol is an element of . (Contributed by Mario Carneiro, 4-Feb-2015.)

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

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

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

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

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

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

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

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

Theoremlgsval2 20551 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 20552 The Legendre symbol at . (Contributed by Mario Carneiro, 4-Feb-2015.)

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

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

Theoremlgsval4 20555* Restate lgsval 20539 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 20556* Closure of the function which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.)

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

Theoremlgsneg 20558 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 20559 The Legendre symbol for nonnegative first parameter is unchanged by negation of the second. (Contributed by Mario Carneiro, 4-Feb-2015.)

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

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

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

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

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

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

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

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

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

Theoremlgsdir 20569 The Legendre symbol is completely multiplicative in its left argument. Together with lgsqr 20585 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 20570* Lemma for lgsdi 20571. (Contributed by Mario Carneiro, 4-Feb-2015.)

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

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

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

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

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

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

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

Theoremlgsdirnn0 20578 Variation on lgsdir 20569 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 20579 Variation on lgsdi 20571 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 20580 Lemma for lgsqr 20585. (Contributed by Mario Carneiro, 15-Jun-2015.)
ℤ/n       Poly1              deg1        eval1       .gmulGrp       var1                            RHom

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

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

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

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

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

Theoremlgsdchrval 20586* 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 20587* 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

Theoremlgseisenlem1 20588* Lemma for lgseisen 20592. If and , then for any even , is also an even integer . To simplify these statements, we divide all the even numbers by , so that it becomes the statement that is an integer between and . (Contributed by Mario Carneiro, 17-Jun-2015.)

Theoremlgseisenlem2 20589* Lemma for lgseisen 20592. The function is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 17-Jun-2015.)

Theoremlgseisenlem3 20590* Lemma for lgseisen 20592. (Contributed by Mario Carneiro, 17-Jun-2015.)
ℤ/n       mulGrp       RHom       g

Theoremlgseisenlem4 20591* Lemma for lgseisen 20592. The function is an injection (and hence a bijection by the pigeonhole principle). (Contributed by Mario Carneiro, 18-Jun-2015.)
ℤ/n       mulGrp       RHom

Theoremlgseisen 20592* Eisenstein's lemma, an expression for when are distinct odd primes. (Contributed by Mario Carneiro, 18-Jun-2015.)

Theoremlgsquadlem1 20593* Lemma for lgsquad 20596. Count the members of with odd coordinates. (Contributed by Mario Carneiro, 19-Jun-2015.)

Theoremlgsquadlem2 20594* Lemma for lgsquad 20596. Count the members of with even coordinates, and combine with lgsquadlem1 20593 to get the total count of lattice points in (up to parity). (Contributed by Mario Carneiro, 18-Jun-2015.)

Theoremlgsquad 20596 The Law of Quadratic Reciprocity. If and are distinct odd primes, then the product of the Legendre symbols and is the parity of . This uses Eisenstein's proof, which also has a nice geometric interpretation - see https://en.wikipedia.org/wiki/Proofs_of_quadratic_reciprocity. (Contributed by Mario Carneiro, 19-Jun-2015.)