Home | Metamath
Proof Explorer Theorem List (p. 251 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pcbcctr 25001* | Prime count of a central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.) |
Theorem | bcmono 25002 | The binomial coefficient is monotone in its second argument, up to the midway point. (Contributed by Mario Carneiro, 5-Mar-2014.) |
Theorem | bcmax 25003 | The binomial coefficient takes its maximum value at the center. (Contributed by Mario Carneiro, 5-Mar-2014.) |
Theorem | bcp1ctr 25004 | Ratio of two central binomial coefficients. (Contributed by Mario Carneiro, 10-Mar-2014.) |
Theorem | bclbnd 25005 | A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.) |
Theorem | efexple 25006 | Convert a bound on a power to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.) |
Theorem | bpos1lem 25007* | Lemma for bpos1 25008. (Contributed by Mario Carneiro, 12-Mar-2014.) |
Theorem | bpos1 25008* | 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.) (Proof shortened by AV, 15-Sep-2021.) |
; | ||
Theorem | bposlem1 25009 | An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014.) |
Theorem | bposlem2 25010 | There are no odd primes in the range dividing the -th central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.) |
Theorem | bposlem3 25011* | Lemma for bpos 25018. Since the binomial coefficient does not have any primes in the range or by bposlem2 25010 and prmfac1 15431, 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.) |
Theorem | bposlem4 25012* | Lemma for bpos 25018. (Contributed by Mario Carneiro, 13-Mar-2014.) |
Theorem | bposlem5 25013* | Lemma for bpos 25018. Bound the product of all small primes in the binomial coefficient. (Contributed by Mario Carneiro, 15-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.) |
Theorem | bposlem6 25014* | Lemma for bpos 25018. 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.) (Revised by Wolf Lammen, 12-Sep-2020.) |
Theorem | bposlem7 25015* | Lemma for bpos 25018. The function is decreasing. (Contributed by Mario Carneiro, 13-Mar-2014.) |
Theorem | bposlem8 25016 | Lemma for bpos 25018. Evaluate and show it is less than . (Contributed by Mario Carneiro, 14-Mar-2014.) |
; ; | ||
Theorem | bposlem9 25017* | Lemma for bpos 25018. Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.) |
; | ||
Theorem | bpos 25018* | 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. This is Metamath 100 proof #98. (Contributed by Mario Carneiro, 14-Mar-2014.) |
If the congruence has a solution we say that is a quadratic residue . If the congruence has no solution we say that is a quadratic nonresidue , see definition in [ApostolNT] p. 178. The Legendre symbol is defined in a way that its value is if is a quadratic residue and if is a quadratic nonresidue (and if divides ), see lgsqr 25076. Originally, the Legendre symbol was defined for odd primes only (and arbitrary integers ) by Adrien-Marie Legendre in 1798, see definition in [ApostolNT] p. 179. It was generalized to be defined for any positive odd integer by Carl Gustav Jacob Jacobi in 1837 (therefore called "Jacobi symbol" since then), see definition in [ApostolNT] p. 188. Finally, it was generalized to be defined for any integer by Leopold Kronecker in 1885 (therefore called "Kronecker symbol" since then). The definition df-lgs 25020 for the "Legendre symbol" is actually the definition of the "Kronecker symbol". Since only one definition (and one class symbol) are provided in set.mm, the names "Legendre symbol", "Jacobi symbol" and "Kronecker symbol" are used synonymously for , but mostly it is called "Legendre symbol", even if it is used in the context of a "Jacobi symbol" or "Kronecker symbol". | ||
Syntax | clgs 25019 | Extend class notation with the Legendre symbol function. |
Definition | df-lgs 25020* | Define the Legendre symbol (actually the Kronecker symbol, which extends the Legendre symbol to all integers, and also the Jacobi symbol, which restricts the Kronecker symbol to positive odd integers). See definition in [ApostolNT] p. 179 resp. definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | zabsle1 25021 | is the set of all integers with absolute value at most . (Contributed by AV, 13-Jul-2021.) |
Theorem | lgslem1 25022 | 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.) |
Theorem | lgslem2 25023 | The set of all integers with absolute value at most contains . (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgslem3 25024* | The set of all integers with absolute value at most is closed under multiplication. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgslem4 25025* | The function is closed in integers with absolute value less than (namely , see zabsle1 25021). (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsval 25026* | Value of the Legendre symbol at an arbitrary integer. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsfval 25027* | Value of the function which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsfcl2 25028* | The function is closed in integers with absolute value less than (namely , see zabsle1 25021). (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgscllem 25029* | The Legendre symbol is an element of . (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsfcl 25030* | Closure of the function which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsfle1 25031* | The function has magnitude less or equal to . (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsval2lem 25032* | Lemma for lgsval2 25038. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsval4lem 25033* | Lemma for lgsval4 25042. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgscl2 25034* | The Legendre symbol is an integer with absolute value less or equal to . (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgs0 25035 | The Legendre symbol when the second argument is zero. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgscl 25036 | The Legendre symbol is an integer. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsle1 25037 | The Legendre symbol has absolute value less or equal to . Together with lgscl 25036 this implies that it takes values in . (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsval2 25038 | 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.) |
Theorem | lgs2 25039 | The Legendre symbol at . (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsval3 25040 | The Legendre symbol at an odd prime (this is the traditional domain of the Legendre symbol). (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsvalmod 25041 | The Legendre symbol is equivalent to , . This theorem is also called "Euler's criterion", see theorem 9.2 in [ApostolNT] p. 180, or a representation of Euler's criterion using the Legendre symbol, see also lgsqr 25076. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsval4 25042* | Restate lgsval 25026 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.) |
Theorem | lgsfcl3 25043* | Closure of the function which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsval4a 25044* | Same as lgsval4 25042 for positive . (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgscl1 25045 | The value of the Legendre symbol is either -1 or 0 or 1. (Contributed by AV, 13-Jul-2021.) |
Theorem | lgsneg 25046 | 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.) |
Theorem | lgsneg1 25047 | The Legendre symbol for nonnegative first parameter is unchanged by negation of the second. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsmod 25048 | The Legendre (Jacobi) symbol is preserved under reduction when is odd. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsdilem 25049 | Lemma for lgsdi 25059 and lgsdir 25057: the sign part of the Legendre symbol is multiplicative. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsdir2lem1 25050 | Lemma for lgsdir2 25055. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsdir2lem2 25051 | Lemma for lgsdir2 25055. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsdir2lem3 25052 | Lemma for lgsdir2 25055. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsdir2lem4 25053 | Lemma for lgsdir2 25055. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsdir2lem5 25054 | Lemma for lgsdir2 25055. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsdir2 25055 | The Legendre symbol is completely multiplicative at . (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsdirprm 25056 | The Legendre symbol is completely multiplicative at the primes. See theorem 9.3 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsdir 25057 | The Legendre symbol is completely multiplicative in its left argument. Generalization of theorem 9.9(a) in [ApostolNT] p. 188 (which assumes that and are odd positive integers). Together with lgsqr 25076 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.) |
Theorem | lgsdilem2 25058* | Lemma for lgsdi 25059. (Contributed by Mario Carneiro, 4-Feb-2015.) |
Theorem | lgsdi 25059 | The Legendre symbol is completely multiplicative in its right argument. Generalization of theorem 9.9(b) in [ApostolNT] p. 188 (which assumes that and are odd positive integers). (Contributed by Mario Carneiro, 5-Feb-2015.) |
Theorem | lgsne0 25060 | The Legendre symbol is nonzero (and hence equal to or ) precisely when the arguments are coprime. (Contributed by Mario Carneiro, 5-Feb-2015.) |
Theorem | lgsabs1 25061 | The Legendre symbol is nonzero (and hence equal to or ) precisely when the arguments are coprime. (Contributed by Mario Carneiro, 5-Feb-2015.) |
Theorem | lgssq 25062 | The Legendre symbol at a square is equal to . Together with lgsmod 25048 this implies that the Legendre symbol takes value at every quadratic residue. (Contributed by Mario Carneiro, 5-Feb-2015.) (Revised by AV, 20-Jul-2021.) |
Theorem | lgssq2 25063 | The Legendre symbol at a square is equal to . (Contributed by Mario Carneiro, 5-Feb-2015.) |
Theorem | lgsprme0 25064 | The Legendre symbol at any prime (even at 2) is iff the prime does not divide the first argument. See definition in [ApostolNT] p. 179. (Contributed by AV, 20-Jul-2021.) |
Theorem | 1lgs 25065 | The Legendre symbol at . See example 1 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 28-Apr-2016.) |
Theorem | lgs1 25066 | The Legendre symbol at . See definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 28-Apr-2016.) |
Theorem | lgsmodeq 25067 | The Legendre (Jacobi) symbol is preserved under reduction when is odd. Theorem 9.9(c) in [ApostolNT] p. 188. (Contributed by AV, 20-Jul-2021.) |
Theorem | lgsmulsqcoprm 25068 | The Legendre (Jacobi) symbol is preserved under multiplication with a square of an integer coprime to the second argument. Theorem 9.9(d) in [ApostolNT] p. 188. (Contributed by AV, 20-Jul-2021.) |
Theorem | lgsdirnn0 25069 | Variation on lgsdir 25057 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.) |
Theorem | lgsdinn0 25070 | Variation on lgsdi 25059 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.) |
Theorem | lgsqrlem1 25071 | Lemma for lgsqr 25076. (Contributed by Mario Carneiro, 15-Jun-2015.) |
ℤ/nℤ Poly1 deg1 eval1 .gmulGrp var1 RHom | ||
Theorem | lgsqrlem2 25072* | Lemma for lgsqr 25076. (Contributed by Mario Carneiro, 15-Jun-2015.) |
ℤ/nℤ Poly1 deg1 eval1 .gmulGrp var1 RHom | ||
Theorem | lgsqrlem3 25073* | Lemma for lgsqr 25076. (Contributed by Mario Carneiro, 15-Jun-2015.) |
ℤ/nℤ Poly1 deg1 eval1 .gmulGrp var1 RHom | ||
Theorem | lgsqrlem4 25074* | Lemma for lgsqr 25076. (Contributed by Mario Carneiro, 15-Jun-2015.) |
ℤ/nℤ Poly1 deg1 eval1 .gmulGrp var1 RHom | ||
Theorem | lgsqrlem5 25075* | Lemma for lgsqr 25076. (Contributed by Mario Carneiro, 15-Jun-2015.) |
Theorem | lgsqr 25076* | The Legendre symbol for odd primes is iff the number is not a multiple of the prime (in which case it is , see lgsne0 25060) and the number is a quadratic residue (it is for nonresidues by the process of elimination from lgsabs1 25061). Given our definition of the Legendre symbol, this theorem is equivalent to Euler's criterion. (Contributed by Mario Carneiro, 15-Jun-2015.) |
Theorem | lgsqrmod 25077* | If the Legendre symbol of an integer for an odd prime is , then the number is a quadratic residue . (Contributed by AV, 20-Aug-2021.) |
Theorem | lgsqrmodndvds 25078* | If the Legendre symbol of an integer for an odd prime is , then the number is a quadratic residue with a solution of the congruence (mod ) which is not divisible by the prime. (Contributed by AV, 20-Aug-2021.) |
Theorem | lgsdchrval 25079* | 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 | ||
Theorem | lgsdchr 25080* | 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 | ||
Gauss' Lemma is valid for any integer not dividing the given prime number. In the following, only the special case for 2 (not dividing any odd prime) is proven, see gausslemma2d 25099. The general case is still to prove. | ||
Theorem | gausslemma2dlem0a 25081 | Auxiliary lemma 1 for gausslemma2d 25099. (Contributed by AV, 9-Jul-2021.) |
Theorem | gausslemma2dlem0b 25082 | Auxiliary lemma 2 for gausslemma2d 25099. (Contributed by AV, 9-Jul-2021.) |
Theorem | gausslemma2dlem0c 25083 | Auxiliary lemma 3 for gausslemma2d 25099. (Contributed by AV, 13-Jul-2021.) |
Theorem | gausslemma2dlem0d 25084 | Auxiliary lemma 4 for gausslemma2d 25099. (Contributed by AV, 9-Jul-2021.) |
Theorem | gausslemma2dlem0e 25085 | Auxiliary lemma 5 for gausslemma2d 25099. (Contributed by AV, 9-Jul-2021.) |
Theorem | gausslemma2dlem0f 25086 | Auxiliary lemma 6 for gausslemma2d 25099. (Contributed by AV, 9-Jul-2021.) |
Theorem | gausslemma2dlem0g 25087 | Auxiliary lemma 7 for gausslemma2d 25099. (Contributed by AV, 9-Jul-2021.) |
Theorem | gausslemma2dlem0h 25088 | Auxiliary lemma 8 for gausslemma2d 25099. (Contributed by AV, 9-Jul-2021.) |
Theorem | gausslemma2dlem0i 25089 | Auxiliary lemma 9 for gausslemma2d 25099. (Contributed by AV, 14-Jul-2021.) |
Theorem | gausslemma2dlem1a 25090* | Lemma for gausslemma2dlem1 25091. (Contributed by AV, 1-Jul-2021.) |
Theorem | gausslemma2dlem1 25091* | Lemma 1 for gausslemma2d 25099. (Contributed by AV, 5-Jul-2021.) |
Theorem | gausslemma2dlem2 25092* | Lemma 2 for gausslemma2d 25099. (Contributed by AV, 4-Jul-2021.) |
Theorem | gausslemma2dlem3 25093* | Lemma 3 for gausslemma2d 25099. (Contributed by AV, 4-Jul-2021.) |
Theorem | gausslemma2dlem4 25094* | Lemma 4 for gausslemma2d 25099. (Contributed by AV, 16-Jun-2021.) |
Theorem | gausslemma2dlem5a 25095* | Lemma for gausslemma2dlem5 25096. (Contributed by AV, 8-Jul-2021.) |
Theorem | gausslemma2dlem5 25096* | Lemma 5 for gausslemma2d 25099. (Contributed by AV, 9-Jul-2021.) |
Theorem | gausslemma2dlem6 25097* | Lemma 6 for gausslemma2d 25099. (Contributed by AV, 16-Jun-2021.) |
Theorem | gausslemma2dlem7 25098* | Lemma 7 for gausslemma2d 25099. (Contributed by AV, 13-Jul-2021.) |
Theorem | gausslemma2d 25099* | Gauss' Lemma (see also theorem 9.6 in [ApostolNT] p. 182) for integer : Let p be an odd prime. Let S={2,4,6,...,(p-1)}. Let n denote the number of elements of S whose least positive residue modulo p is greater than p/2. Then ( 2 | p ) = (-1)^n. (Contributed by AV, 14-Jul-2021.) |
Theorem | lgseisenlem1 25100* | Lemma for lgseisen 25104. 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.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |