P. 164 of Theorem List - Intuitionistic Logic Explorer

Home	Intuitionistic Logic Explorer Theorem List (p. 164 of 174)	< Previous Next >
		Browser slow? Try the Unicode version.
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List

**Theorem List for Intuitionistic Logic Explorer -** 16301-16400 *Has distinct variable group(s)
Type	Label	Description
Statement

Theorem	1sgm2ppw 16301	The sum of the divisors of . (Contributed by Mario Carneiro, 17-May-2016.)


Theorem	sgmmul 16302	The divisor function for fixed parameter is a multiplicative function. (Contributed by Mario Carneiro, 2-Jul-2015.)
$/\$ $/\$ $/\$

Theorem	ppiublem1 16303	Lemma for ppiqub 16305. (Contributed by Mario Carneiro, 12-Mar-2014.)
$/\$ $/\$ $\/$ $\/$ $/\$ $/\$

Theorem	ppiublem2 16304	A prime greater than does not divide or , so its residue is or . (Contributed by Mario Carneiro, 12-Mar-2014.)
$/\$

Theorem	ppiqub 16305	An upper bound on the prime-counting function π, which counts the number of primes less than . (Contributed by Mario Carneiro, 13-Mar-2014.)
$/\$ π

Theorem	chtqleppi 16306	Upper bound on the function. (Contributed by Mario Carneiro, 22-Sep-2014.)
$/\$ π

Theorem	chtublem 16307	Lemma for chtqub 16308. (Contributed by Mario Carneiro, 13-Mar-2014.)


Theorem	chtqub 16308	An upper bound on the Chebyshev function. (Contributed by Mario Carneiro, 13-Mar-2014.) (Revised 22-Sep-2014.)
$/\$

11.4.3 Perfect Number Theorem

Theorem	mersenne 16309	A Mersenne prime is a prime number of the form . This theorem shows that the in this expression is necessarily also prime. (Contributed by Mario Carneiro, 17-May-2016.)
$/\$

Theorem	perfect1 16310	Euclid's contribution to the Euclid-Euler theorem. A number of the form is a perfect number. (Contributed by Mario Carneiro, 17-May-2016.)
$/\$

Theorem	perfectlem1 16311	Lemma for perfect 16313. (Contributed by Mario Carneiro, 7-Jun-2016.)
$/\$ $/\$

Theorem	perfectlem2 16312	Lemma for perfect 16313. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by Wolf Lammen, 17-Sep-2020.)
$/\$

Theorem	perfect 16313*	The Euclid-Euler theorem, or Perfect Number theorem. A positive even integer is a perfect number (that is, its divisor sum is ) if and only if it is of the form , where is prime (a Mersenne prime), and therefore is also prime, see mersenne 16309. This is Metamath 100 proof #70. (Contributed by Mario Carneiro, 17-May-2016.)
$/\$ $/\$

11.4.4 Bertrand's postulate

Theorem	bcctr 16314	Value of the central binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.)


Theorem	pcbcctr 16315*	Prime count of a central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)
$/\$

Theorem	bcmono 16316	The binomial coefficient is monotone in its second argument, up to the midway point. (Contributed by Mario Carneiro, 5-Mar-2014.)
$/\$ $/\$

Theorem	bcmax 16317	The binomial coefficient takes its maximum value at the center. (Contributed by Mario Carneiro, 5-Mar-2014.)
$/\$

Theorem	bcp1ctr 16318	Ratio of two central binomial coefficients. (Contributed by Mario Carneiro, 10-Mar-2014.)


Theorem	bclbnd 16319	A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.)


Theorem	prmefexple 16320	Convert a bound on a power of a prime to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Jim Kingdon, 21-Aug-2026.)
$/\$ $/\$

Theorem	bpos1lem 16321*	Lemma for bpos1 . (Contributed by Mario Carneiro, 12-Mar-2014.)
$/\$ $\/$

Theorem	bpos1 16322*	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 16323	An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014.)
$/\$

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


Theorem	bposlem3 16325*	Lemma for bpos . Since the binomial coefficient does not have any primes in the range or by bposlem2 16324 and prmfac1 12957, 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 16326*	Lemma for bpos . (Contributed by Mario Carneiro, 13-Mar-2014.)
$/\$

Theorem	bposlem5 16327*	Lemma for bpos . 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 16328*	Lemma for bpos 16332. 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 16329*	Lemma for bpos 16332. The function is strictly decreasing for arguments greater than 7. (Contributed by Mario Carneiro, 13-Mar-2014.)


Theorem	bposlem8 16330	Lemma for bpos 16332. Show that is less than . (Contributed by Mario Carneiro, 14-Mar-2014.)
; $/\$ ;

Theorem	bposlem9 16331*	Lemma for bpos 16332. Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.)
; $/\$

Theorem	bpos 16332*	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.)
$/\$

11.4.5 Quadratic residues and the Legendre symbol 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 ). 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 16334 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 16333	Extend class notation with the Legendre symbol function.


Definition	df-lgs 16334*	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 16335	is the set of all integers with absolute value at most . (Contributed by AV, 13-Jul-2021.)


Theorem	lgslem1 16336	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 16337	The set of all integers with absolute value at most contains . (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$ $/\$

Theorem	lgslem3 16338*	The set of all integers with absolute value at most is closed under multiplication. (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$

Theorem	lgslem4 16339*	Lemma for lgsfcl2 16342. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 19-Mar-2022.)
$/\$ $\$

Theorem	lgsval 16340*	Value of the Legendre symbol at an arbitrary integer. (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$ $/\$

Theorem	lgsfvalg 16341*	Value of the function which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by Jim Kingdon, 4-Nov-2024.)
$/\$ $/\$

Theorem	lgsfcl2 16342*	The function is closed in integers with absolute value less than (namely , see zabsle1 16335). (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$ $/\$

Theorem	lgscllem 16343*	The Legendre symbol is an element of . (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$

Theorem	lgsfcl 16344*	Closure of the function which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$ $/\$

Theorem	lgsfle1 16345*	The function has magnitude less or equal to . (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$ $/\$ $/\$

Theorem	lgsval2lem 16346*	Lemma for lgsval2 16352. (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$

Theorem	lgsval4lem 16347*	Lemma for lgsval4 16356. (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$ $/\$

Theorem	lgscl2 16348*	The Legendre symbol is an integer with absolute value less than or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$

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


Theorem	lgscl 16350	The Legendre symbol is an integer. (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$

Theorem	lgsle1 16351	The Legendre symbol has absolute value less than or equal to 1. Together with lgscl 16350 this implies that it takes values in . (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$

Theorem	lgsval2 16352	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 16353	The Legendre symbol at . (Contributed by Mario Carneiro, 4-Feb-2015.)


Theorem	lgsval3 16354	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 16355	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. (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$ $\$

Theorem	lgsval4 16356*	Restate lgsval 16340 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 16357*	Closure of the function which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$ $/\$

Theorem	lgsval4a 16358*	Same as lgsval4 16356 for positive . (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$

Theorem	lgscl1 16359	The value of the Legendre symbol is either -1 or 0 or 1. (Contributed by AV, 13-Jul-2021.)
$/\$

Theorem	lgsneg 16360	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 16361	The Legendre symbol for nonnegative first parameter is unchanged by negation of the second. (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$

Theorem	lgsmod 16362	The Legendre (Jacobi) symbol is preserved under reduction when is odd. (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$ $/\$

Theorem	lgsdilem 16363	Lemma for lgsdi 16373 and lgsdir 16371: the sign part of the Legendre symbol is multiplicative. (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	lgsdir2lem1 16364	Lemma for lgsdir2 16369. (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$ $/\$ $/\$

Theorem	lgsdir2lem2 16365	Lemma for lgsdir2 16369. (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	lgsdir2lem3 16366	Lemma for lgsdir2 16369. (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$

Theorem	lgsdir2lem4 16367	Lemma for lgsdir2 16369. (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$ $/\$

Theorem	lgsdir2lem5 16368	Lemma for lgsdir2 16369. (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$ $/\$ $/\$

Theorem	lgsdir2 16369	The Legendre symbol is completely multiplicative at . (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$

Theorem	lgsdirprm 16370	The Legendre symbol is completely multiplicative at the primes. See theorem 9.3 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 18-Mar-2022.)
$/\$ $/\$

Theorem	lgsdir 16371	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). (Contributed by Mario Carneiro, 4-Feb-2015.)
$/\$ $/\$ $/\$ $/\$

Theorem	lgsdilem2 16372*	Lemma for lgsdi 16373. (Contributed by Mario Carneiro, 4-Feb-2015.)


Theorem	lgsdi 16373	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 16374	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 16375	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 16376	The Legendre symbol at a square is equal to . Together with lgsmod 16362 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 16377	The Legendre symbol at a square is equal to . (Contributed by Mario Carneiro, 5-Feb-2015.)
$/\$ $/\$

Theorem	lgsprme0 16378	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 16379	The Legendre symbol at . See example 1 in [ApostolNT] p. 180. (Contributed by Mario Carneiro, 28-Apr-2016.)


Theorem	lgs1 16380	The Legendre symbol at . See definition in [ApostolNT] p. 188. (Contributed by Mario Carneiro, 28-Apr-2016.)


Theorem	lgsmodeq 16381	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 16382	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 16383	Variation on lgsdir 16371 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 16384	Variation on lgsdi 16373 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.)
$/\$ $/\$

11.4.6 Gauss' Lemma 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 16405. The general case is still to prove.

Theorem	gausslemma2dlem0a 16385	Auxiliary lemma 1 for gausslemma2d 16405. (Contributed by AV, 9-Jul-2021.)
$\$

Theorem	gausslemma2dlem0b 16386	Auxiliary lemma 2 for gausslemma2d 16405. (Contributed by AV, 9-Jul-2021.)
$\$

Theorem	gausslemma2dlem0c 16387	Auxiliary lemma 3 for gausslemma2d 16405. (Contributed by AV, 13-Jul-2021.)
$\$

Theorem	gausslemma2dlem0d 16388	Auxiliary lemma 4 for gausslemma2d 16405. (Contributed by AV, 9-Jul-2021.)
$\$

Theorem	gausslemma2dlem0e 16389	Auxiliary lemma 5 for gausslemma2d 16405. (Contributed by AV, 9-Jul-2021.)
$\$

Theorem	gausslemma2dlem0f 16390	Auxiliary lemma 6 for gausslemma2d 16405. (Contributed by AV, 9-Jul-2021.)
$\$

Theorem	gausslemma2dlem0g 16391	Auxiliary lemma 7 for gausslemma2d 16405. (Contributed by AV, 9-Jul-2021.)
$\$

Theorem	gausslemma2dlem0h 16392	Auxiliary lemma 8 for gausslemma2d 16405. (Contributed by AV, 9-Jul-2021.)
$\$

Theorem	gausslemma2dlem0i 16393	Auxiliary lemma 9 for gausslemma2d 16405. (Contributed by AV, 14-Jul-2021.)
$\$

Theorem	gausslemma2dlem1a 16394*	Lemma for gausslemma2dlem1 16397. (Contributed by AV, 1-Jul-2021.)
$\$

Theorem	gausslemma2dlem1cl 16395	Lemma for gausslemma2dlem1 16397. Closure of the body of the definition of . (Contributed by Jim Kingdon, 10-Aug-2025.)
$\$

Theorem	gausslemma2dlem1f1o 16396*	Lemma for gausslemma2dlem1 16397. (Contributed by Jim Kingdon, 9-Aug-2025.)
$\$

Theorem	gausslemma2dlem1 16397*	Lemma 1 for gausslemma2d 16405. (Contributed by AV, 5-Jul-2021.)
$\$

Theorem	gausslemma2dlem2 16398*	Lemma 2 for gausslemma2d 16405. (Contributed by AV, 4-Jul-2021.)
$\$

Theorem	gausslemma2dlem3 16399*	Lemma 3 for gausslemma2d 16405. (Contributed by AV, 4-Jul-2021.)
$\$

Theorem	gausslemma2dlem4 16400*	Lemma 4 for gausslemma2d 16405. (Contributed by AV, 16-Jun-2021.)
$\$

< Previous Next >

Page List Jump to page: Contents 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17398

< Previous Next >