P. 163 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16201-16300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ppiqsval 16201	The set of primes less than A expressed using a finite set of integers. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. QQ -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
Theorem	ppiqsval2 16202	The set of primes less than A expressed using a finite set of integers. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. QQ /\ 2 e. ( ZZ>= ` M ) ) -> ( ( 0 [,] A ) i^i Prime ) = ( ( M ... ( |_ ` A ) ) i^i Prime ) )
Theorem	ppiqfi 16203	The set of primes less than A is a finite set. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( A e. QQ -> ( ( 0 [,] A ) i^i Prime ) e. Fin )
Theorem	prmdvdsfi 16204*	The set of prime divisors of a number is a finite set. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. NN -> { p e. Prime | p || A } e. Fin )
Theorem	chtqcl 16205	Rational closure of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( A e. QQ -> ( theta ` A ) e. RR )
Theorem	chtqval 16206*	Value of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( A e. QQ -> ( theta ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) )
Theorem	efchtqcl 16207	The Chebyshev function is closed in the log-integers. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 7-Apr-2016.)
|- ( A e. QQ -> ( exp ` ( theta ` A ) ) e. NN )
Theorem	chtqge0 16208	The Chebyshev function is always positive. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( A e. QQ -> 0 <_ ( theta ` A ) )
Theorem	ppiqval 16209	Value of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( A e. QQ -> (π ` A ) = (♯ ` ( ( 0 [,] A ) i^i Prime ) ) )
Theorem	ppival2 16210	Value of the prime-counting function pi. (Contributed by Mario Carneiro, 18-Sep-2014.)
|- ( A e. ZZ -> (π ` A ) = (♯ ` ( ( 2 ... A ) i^i Prime ) ) )
Theorem	ppival2g 16211	Value of the prime-counting function pi. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. ZZ /\ 2 e. ( ZZ>= ` M ) ) -> (π ` A ) = (♯ ` ( ( M ... A ) i^i Prime ) ) )
Theorem	ppiqcl 16212	Rational closure of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( A e. QQ -> (π ` A ) e. NN0 )
Theorem	sgmval 16213*	The value of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 21-Jun-2015.)
|- ( ( A e. CC /\ B e. NN ) -> ( A sigma B ) = sum_ k e. { p e. NN | p || B } ( k ^c A ) )
Theorem	sgmval2 16214*	The value of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- ( ( A e. ZZ /\ B e. NN ) -> ( A sigma B ) = sum_ k e. { p e. NN | p || B } ( k ^ A ) )
Theorem	0sgm 16215*	The value of the sum-of-divisors function, usually denoted σ<SUB>0</SUB>(<i>n</i>). (Contributed by Mario Carneiro, 21-Jun-2015.)
|- ( A e. NN -> ( 0 sigma A ) = (♯ ` { p e. NN | p || A } ) )
Theorem	sgmf 16216	The divisor function is a function into the complex numbers. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 21-Jun-2015.)
|- sigma : ( CC X. NN ) --> CC
Theorem	sgmcl 16217	Closure of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. CC /\ B e. NN ) -> ( A sigma B ) e. CC )
Theorem	sgmnncl 16218	Closure of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- ( ( A e. NN0 /\ B e. NN ) -> ( A sigma B ) e. NN )
Theorem	chtqfl 16219	The Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. QQ -> ( theta ` ( |_ ` A ) ) = ( theta ` A ) )
Theorem	ppiprm 16220	The prime-counting function π at a prime. (Contributed by Mario Carneiro, 19-Sep-2014.)
|- ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> (π ` ( A + 1 ) ) = ( (π ` A ) + 1 ) )
Theorem	ppinprm 16221	The prime-counting function π at a non-prime. (Contributed by Mario Carneiro, 19-Sep-2014.)
|- ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> (π ` ( A + 1 ) ) = (π ` A ) )
Theorem	chtprm 16222	The Chebyshev function at a prime. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( theta ` ( A + 1 ) ) = ( ( theta ` A ) + ( log ` ( A + 1 ) ) ) )
Theorem	chtnprm 16223	The Chebyshev function at a non-prime. (Contributed by Mario Carneiro, 19-Sep-2014.)
|- ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( theta ` ( A + 1 ) ) = ( theta ` A ) )
Theorem	chtqwordi 16224	The Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. QQ /\ B e. QQ /\ A <_ B ) -> ( theta ` A ) <_ ( theta ` B ) )
Theorem	chtdif 16225*	The difference of the Chebyshev function at two points sums the logarithms of the primes in an interval. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( N e. ( ZZ>= ` M ) -> ( ( theta ` N ) - ( theta ` M ) ) = sum_ p e. ( ( ( M + 1 ) ... N ) i^i Prime ) ( log ` p ) )
Theorem	efchtqdvds 16226	The exponentiated Chebyshev function forms a divisibility chain between any two points. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. QQ /\ B e. QQ /\ A <_ B ) -> ( exp ` ( theta ` A ) ) || ( exp ` ( theta ` B ) ) )
Theorem	ppiqfl 16227	The prime-counting function π does not change off the integers. (Contributed by Mario Carneiro, 18-Sep-2014.)
|- ( A e. QQ -> (π ` ( |_ ` A ) ) = (π ` A ) )
Theorem	ppiqp1le 16228	The prime-counting function π cannot locally increase faster than the identity function. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- ( A e. QQ -> (π ` ( A + 1 ) ) <_ ( (π ` A ) + 1 ) )
Theorem	ppiqwordi 16229	The prime-counting function π is weakly increasing. (Contributed by Mario Carneiro, 19-Sep-2014.)
|- ( ( A e. QQ /\ B e. QQ /\ A <_ B ) -> (π ` A ) <_ (π ` B ) )
Theorem	ppidif 16230	The difference of the prime-counting function π at two points counts the number of primes in an interval. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- ( N e. ( ZZ>= ` M ) -> ( (π ` N ) - (π ` M ) ) = (♯ ` ( ( ( M + 1 ) ... N ) i^i Prime ) ) )
Theorem	ppi1 16231	The prime-counting function π at 1. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- (π ` 1 ) = 0
Theorem	cht1 16232	The Chebyshev function at 1. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( theta ` 1 ) = 0
Theorem	ppi1i 16233	Inference form of ppiprm 16220. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- M e. NN0   &    |- N = ( M + 1 )   &    |- (π ` M ) = K   &    |- N e. Prime   =>    |- (π ` N ) = ( K + 1 )
Theorem	ppi2i 16234	Inference form of ppinprm 16221. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- M e. NN0   &    |- N = ( M + 1 )   &    |- (π ` M ) = K   &    |- -. N e. Prime   =>    |- (π ` N ) = K
Theorem	ppi2 16235	The prime-counting function π at 2. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- (π ` 2 ) = 1
Theorem	ppi3 16236	The prime-counting function π at 3. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- (π ` 3 ) = 2
Theorem	cht2 16237	The Chebyshev function at 2. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( theta ` 2 ) = ( log ` 2 )
Theorem	cht3 16238	The Chebyshev function at 3. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( theta ` 3 ) = ( log ` 6 )
Theorem	ppiqnncl 16239	Closure of the prime-counting function π in the positive integers. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- ( ( A e. QQ /\ 2 <_ A ) -> (π ` A ) e. NN )
Theorem	chtqrpcl 16240	Closure of the Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. QQ /\ 2 <_ A ) -> ( theta ` A ) e. RR+ )
Theorem	ppiqeq0 16241	The prime-counting function π is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. QQ -> ( (π ` A ) = 0 <-> A < 2 ) )
Theorem	ppiqltx 16242	The prime-counting function π is strictly less than the identity. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. QQ /\ 0 < A ) -> (π ` A ) < A )
Theorem	prmorcht 16243	Relate the primorial (product of the primes up to A) to the Chebyshev function. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- F = ( n e. NN |-> if ( n e. Prime , n , 1 ) )   =>    |- ( A e. NN -> ( exp ` ( theta ` A ) ) = ( seq 1 ( x. , F ) ` A ) )
Theorem	dvdsppwf1o 16244*	A bijection between the divisors of a prime power and the integers less than or equal to the exponent. (Contributed by Mario Carneiro, 5-May-2016.)
|- F = ( n e. ( 0 ... A ) |-> ( P ^ n ) )   =>    |- ( ( P e. Prime /\ A e. NN0 ) -> F : ( 0 ... A ) -1-1-onto-> { x e. NN | x || ( P ^ A ) } )
Theorem	mpodvdsmulf1o 16245*	If M and N are two coprime integers, multiplication forms a bijection from the set of pairs <. j , k >. where j || M and k || N, to the set of divisors of M x. N. (Contributed by GG, 18-Apr-2025.)
|- ( ph -> M e. NN )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ( M gcd N ) = 1 )   &    |- X = { x e. NN | x || M }   &    |- Y = { x e. NN | x || N }   &    |- Z = { x e. NN | x || ( M x. N ) }   =>    |- ( ph -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z )
Theorem	fsumdvdsmul 16246*	Product of two divisor sums. (This is also the main part of the proof that " sum_ k || N F ( k ) is a multiplicative function if F is".) (Contributed by Mario Carneiro, 2-Jul-2015.) Avoid ax-mulf 8303. (Revised by GG, 18-Apr-2025.)
|- ( ph -> M e. NN )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ( M gcd N ) = 1 )   &    |- X = { x e. NN | x || M }   &    |- Y = { x e. NN | x || N }   &    |- Z = { x e. NN | x || ( M x. N ) }   &    |- ( ( ph /\ j e. X ) -> A e. CC )   &    |- ( ( ph /\ k e. Y ) -> B e. CC )   &    |- ( ( ph /\ ( j e. X /\ k e. Y ) ) -> ( A x. B ) = D )   &    |- ( i = ( j x. k ) -> C = D )   =>    |- ( ph -> ( sum_ j e. X A x. sum_ k e. Y B ) = sum_ i e. Z C )
Theorem	sgmppw 16247*	The value of the divisor function at a prime power. (Contributed by Mario Carneiro, 17-May-2016.)
|- ( ( A e. CC /\ P e. Prime /\ N e. NN0 ) -> ( A sigma ( P ^ N ) ) = sum_ k e. ( 0 ... N ) ( ( P ^c A ) ^ k ) )
Theorem	0sgmppw 16248	A prime power P ^ K has K + 1 divisors. (Contributed by Mario Carneiro, 17-May-2016.)
|- ( ( P e. Prime /\ K e. NN0 ) -> ( 0 sigma ( P ^ K ) ) = ( K + 1 ) )
Theorem	1sgmprm 16249	The sum of divisors for a prime is P + 1 because the only divisors are 1 and P. (Contributed by Mario Carneiro, 17-May-2016.)
|- ( P e. Prime -> ( 1 sigma P ) = ( P + 1 ) )
Theorem	1sgm2ppw 16250	The sum of the divisors of 2 ^ ( N - 1 ). (Contributed by Mario Carneiro, 17-May-2016.)
|- ( N e. NN -> ( 1 sigma ( 2 ^ ( N - 1 ) ) ) = ( ( 2 ^ N ) - 1 ) )
Theorem	sgmmul 16251	The divisor function for fixed parameter A is a multiplicative function. (Contributed by Mario Carneiro, 2-Jul-2015.)
|- ( ( A e. CC /\ ( M e. NN /\ N e. NN /\ ( M gcd N ) = 1 ) ) -> ( A sigma ( M x. N ) ) = ( ( A sigma M ) x. ( A sigma N ) ) )
Theorem	ppiublem1 16252	Lemma for ppiqub 16254. (Contributed by Mario Carneiro, 12-Mar-2014.)
|- ( N <_ 6 /\ ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( N ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) ) )   &    |- M e. NN0   &    |- N = ( M + 1 )   &    |- ( 2 || M \/ 3 || M \/ M e. { 1 , 5 } )   =>    |- ( M <_ 6 /\ ( ( P e. Prime /\ 4 <_ P ) -> ( ( P mod 6 ) e. ( M ... 5 ) -> ( P mod 6 ) e. { 1 , 5 } ) ) )
Theorem	ppiublem2 16253	A prime greater than 3 does not divide 2 or 3, so its residue mod 6 is 1 or 5. (Contributed by Mario Carneiro, 12-Mar-2014.)
|- ( ( P e. Prime /\ 4 <_ P ) -> ( P mod 6 ) e. { 1 , 5 } )
Theorem	ppiqub 16254	An upper bound on the prime-counting function π, which counts the number of primes less than N. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( ( N e. QQ /\ 0 <_ N ) -> (π ` N ) <_ ( ( N / 3 ) + 2 ) )
Theorem	chtqleppi 16255	Upper bound on the theta function. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. QQ /\ 0 < A ) -> ( theta ` A ) <_ ( (π ` A ) x. ( log ` A ) ) )
Theorem	chtublem 16256	Lemma for chtqub 16257. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( N e. NN -> ( theta ` ( ( 2 x. N ) - 1 ) ) <_ ( ( theta ` N ) + ( ( log ` 4 ) x. ( N - 1 ) ) ) )
Theorem	chtqub 16257	An upper bound on the Chebyshev function. (Contributed by Mario Carneiro, 13-Mar-2014.) (Revised 22-Sep-2014.)
|- ( ( N e. QQ /\ 2 < N ) -> ( theta ` N ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) )
11.4.3  Perfect Number Theorem
Theorem	mersenne 16258	A Mersenne prime is a prime number of the form 2 ^ P - 1. This theorem shows that the P in this expression is necessarily also prime. (Contributed by Mario Carneiro, 17-May-2016.)
|- ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> P e. Prime )
Theorem	perfect1 16259	Euclid's contribution to the Euclid-Euler theorem. A number of the form 2 ^ ( p - 1 ) x. ( 2 ^ p - 1 ) is a perfect number. (Contributed by Mario Carneiro, 17-May-2016.)
|- ( ( P e. ZZ /\ ( ( 2 ^ P ) - 1 ) e. Prime ) -> ( 1 sigma ( ( 2 ^ ( P - 1 ) ) x. ( ( 2 ^ P ) - 1 ) ) ) = ( ( 2 ^ P ) x. ( ( 2 ^ P ) - 1 ) ) )
Theorem	perfectlem1 16260	Lemma for perfect 16262. (Contributed by Mario Carneiro, 7-Jun-2016.)
|- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> -. 2 || B )   &    |- ( ph -> ( 1 sigma ( ( 2 ^ A ) x. B ) ) = ( 2 x. ( ( 2 ^ A ) x. B ) ) )   =>    |- ( ph -> ( ( 2 ^ ( A + 1 ) ) e. NN /\ ( ( 2 ^ ( A + 1 ) ) - 1 ) e. NN /\ ( B / ( ( 2 ^ ( A + 1 ) ) - 1 ) ) e. NN ) )
Theorem	perfectlem2 16261	Lemma for perfect 16262. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by Wolf Lammen, 17-Sep-2020.)
|- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> -. 2 || B )   &    |- ( ph -> ( 1 sigma ( ( 2 ^ A ) x. B ) ) = ( 2 x. ( ( 2 ^ A ) x. B ) ) )   =>    |- ( ph -> ( B e. Prime /\ B = ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
Theorem	perfect 16262*	The Euclid-Euler theorem, or Perfect Number theorem. A positive even integer N is a perfect number (that is, its divisor sum is 2 N) if and only if it is of the form 2 ^ ( p - 1 ) x. ( 2 ^ p - 1 ), where 2 ^ p - 1 is prime (a Mersenne prime), and therefore p is also prime, see mersenne 16258. This is Metamath 100 proof #70. (Contributed by Mario Carneiro, 17-May-2016.)
|- ( ( N e. NN /\ 2 || N ) -> ( ( 1 sigma N ) = ( 2 x. N ) <-> E. p e. ZZ ( ( ( 2 ^ p ) - 1 ) e. Prime /\ N = ( ( 2 ^ ( p - 1 ) ) x. ( ( 2 ^ p ) - 1 ) ) ) ) )
11.4.4  Bertrand's postulate
Theorem	bcctr 16263	Value of the central binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( N e. NN0 -> ( ( 2 x. N ) _C N ) = ( ( ! ` ( 2 x. N ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) )
Theorem	pcbcctr 16264*	Prime count of a central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)
|- ( ( N e. NN /\ P e. Prime ) -> ( P pCnt ( ( 2 x. N ) _C N ) ) = sum_ k e. ( 1 ... ( 2 x. N ) ) ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) )
Theorem	bcmono 16265	The binomial coefficient is monotone in its second argument, up to the midway point. (Contributed by Mario Carneiro, 5-Mar-2014.)
|- ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) -> ( N _C A ) <_ ( N _C B ) )
Theorem	bcmax 16266	The binomial coefficient takes its maximum value at the center. (Contributed by Mario Carneiro, 5-Mar-2014.)
|- ( ( N e. NN0 /\ K e. ZZ ) -> ( ( 2 x. N ) _C K ) <_ ( ( 2 x. N ) _C N ) )
Theorem	bcp1ctr 16267	Ratio of two central binomial coefficients. (Contributed by Mario Carneiro, 10-Mar-2014.)
|- ( N e. NN0 -> ( ( 2 x. ( N + 1 ) ) _C ( N + 1 ) ) = ( ( ( 2 x. N ) _C N ) x. ( 2 x. ( ( ( 2 x. N ) + 1 ) / ( N + 1 ) ) ) ) )
Theorem	bclbnd 16268	A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.)
|- ( N e. ( ZZ>= ` 4 ) -> ( ( 4 ^ N ) / N ) < ( ( 2 x. N ) _C N ) )
Theorem	prmefexple 16269	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.)
|- ( ( A e. Prime /\ N e. ZZ /\ B e. NN ) -> ( ( A ^ N ) <_ B <-> N <_ ( |_ ` ( ( log ` B ) / ( log ` A ) ) ) ) )
Theorem	bpos1lem 16270*	Lemma for bpos1 . (Contributed by Mario Carneiro, 12-Mar-2014.)
|- ( E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) -> ph )   &    |- ( N e. ( ZZ>= ` P ) -> ph )   &    |- P e. Prime   &    |- A e. NN0   &    |- ( A x. 2 ) = B   &    |- A < P   &    |- ( P < B \/ P = B )   =>    |- ( N e. ( ZZ>= ` A ) -> ph )
Theorem	bpos1 16271*	Bertrand's postulate, checked numerically for N <_ 6 4, using the prime sequence 2 , 3 , 5 , 7 , 1 3 , 2 3 , 4 3 , 8 3. (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.)
|- ( ( N e. NN /\ N <_ ; 6 4 ) -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
Theorem	bposlem1 16272	An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014.)
|- ( ( N e. NN /\ P e. Prime ) -> ( P ^ ( P pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) )
Theorem	bposlem2 16273	There are no odd primes in the range ( 2 N / 3 , N ] dividing the N-th central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)
|- ( ph -> N e. NN )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> 2 < P )   &    |- ( ph -> ( ( 2 x. N ) / 3 ) < P )   &    |- ( ph -> P <_ N )   =>    |- ( ph -> ( P pCnt ( ( 2 x. N ) _C N ) ) = 0 )
Theorem	bposlem3 16274*	Lemma for bpos . Since the binomial coefficient does not have any primes in the range ( 2 N / 3 , N ] or ( 2 N , +oo ) by bposlem2 16273 and prmfac1 12950, respectively, and it does not have any in the range ( N , 2 N ] by hypothesis, the product of the primes up through 2 N / 3 must be sufficient to compose the whole binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( ph -> N e. ( ZZ>= ` 5 ) )   &    |- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )   &    |- F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )   &    |- K = ( |_ ` ( ( 2 x. N ) / 3 ) )   =>    |- ( ph -> ( seq 1 ( x. , F ) ` K ) = ( ( 2 x. N ) _C N ) )
Theorem	bposlem4 16275*	Lemma for bpos . (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( ph -> N e. ( ZZ>= ` 5 ) )   &    |- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )   &    |- F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )   &    |- K = ( |_ ` ( ( 2 x. N ) / 3 ) )   &    |- M = ( |_ ` ( sqr ` ( 2 x. N ) ) )   =>    |- ( ph -> M e. ( 3 ... K ) )
Theorem	bposlem5 16276*	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.)
|- ( ph -> N e. ( ZZ>= ` 5 ) )   &    |- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )   &    |- F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )   &    |- K = ( |_ ` ( ( 2 x. N ) / 3 ) )   &    |- M = ( |_ ` ( sqr ` ( 2 x. N ) ) )   =>    |- ( ph -> ( seq 1 ( x. , F ) ` M ) <_ ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) )
Theorem	bposlem6 16277*	Lemma for bpos 16281. By using the various bounds at our disposal, arrive at an inequality that is false for N large enough. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Wolf Lammen, 12-Sep-2020.)
|- ( ph -> N e. ( ZZ>= ` 5 ) )   &    |- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )   &    |- F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )   &    |- K = ( |_ ` ( ( 2 x. N ) / 3 ) )   &    |- M = ( |_ ` ( sqr ` ( 2 x. N ) ) )   =>    |- ( ph -> ( ( 4 ^ N ) / N ) < ( ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )
Theorem	bposlem7 16278*	Lemma for bpos 16281. The function F is strictly decreasing for arguments greater than 7. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- F = ( n e. NN |-> ( ( ( ( sqr ` 2 ) x. ( G ` ( sqr ` n ) ) ) + ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqr ` ( 2 x. n ) ) ) ) )   &    |- G = ( x e. RR+ |-> ( ( log ` x ) / x ) )   &    |- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> ( _e ^ 2 ) <_ A )   &    |- ( ph -> ( _e ^ 2 ) <_ B )   =>    |- ( ph -> ( A < B -> ( F ` B ) < ( F ` A ) ) )
Theorem	bposlem8 16279	Lemma for bpos 16281. Show that F ( 6 4 ) is less than log 2. (Contributed by Mario Carneiro, 14-Mar-2014.)
|- F = ( n e. NN |-> ( ( ( ( sqr ` 2 ) x. ( G ` ( sqr ` n ) ) ) + ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqr ` ( 2 x. n ) ) ) ) )   &    |- G = ( x e. RR+ |-> ( ( log ` x ) / x ) )   =>    |- ( ( F ` ; 6 4 ) e. RR /\ ( F ` ; 6 4 ) < ( log ` 2 ) )
Theorem	bposlem9 16280*	Lemma for bpos 16281. Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.)
|- F = ( n e. NN |-> ( ( ( ( sqr ` 2 ) x. ( G ` ( sqr ` n ) ) ) + ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqr ` ( 2 x. n ) ) ) ) )   &    |- G = ( x e. RR+ |-> ( ( log ` x ) / x ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ; 6 4 < N )   &    |- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )   =>    |- ( ph -> ps )
Theorem	bpos 16281*	Bertrand's postulate: there is a prime between N and 2 N for every positive integer N. 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.)
|- ( N e. NN -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
11.4.5  Quadratic residues and the Legendre symbol If the congruence ( ( x ^ 2 ) mod p ) = ( n mod p ) has a solution we say that n is a quadratic residue mod p. If the congruence has no solution we say that n is a quadratic nonresidue mod p, see definition in [ApostolNT] p. 178. The Legendre symbol ( n /L p ) is defined in a way that its value is 1 if n is a quadratic residue mod p and -u 1 if n is a quadratic nonresidue mod p (and 0 if p divides n). Originally, the Legendre symbol ( N /L P ) was defined for odd primes P only (and arbitrary integers N) 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 16283 for the "Legendre symbol" /L 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 /L, but mostly it is called "Legendre symbol", even if it is used in the context of a "Jacobi symbol" or "Kronecker symbol".
Syntax	clgs 16282	Extend class notation with the Legendre symbol function.
class /L
Definition	df-lgs 16283*	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.)
|- /L = ( a e. ZZ , n e. ZZ |-> if ( n = 0 , if ( ( a ^ 2 ) = 1 , 1 , 0 ) , ( if ( ( n < 0 /\ a < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , ( m e. NN |-> if ( m e. Prime , ( if ( m = 2 , if ( 2 || a , 0 , if ( ( a mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( a ^ ( ( m - 1 ) / 2 ) ) + 1 ) mod m ) - 1 ) ) ^ ( m pCnt n ) ) , 1 ) ) ) ` ( abs ` n ) ) ) ) )
Theorem	zabsle1 16284	{ -u 1 , 0 , 1 } is the set of all integers with absolute value at most 1. (Contributed by AV, 13-Jul-2021.)
|- ( Z e. ZZ -> ( Z e. { -u 1 , 0 , 1 } <-> ( abs ` Z ) <_ 1 ) )
Theorem	lgslem1 16285	When a is coprime to the prime p, a ^ ( ( p - 1 ) / 2 ) is equivalent mod p to 1 or -u 1, and so adding 1 makes it equivalent to 0 or 2. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) /\ -. P || A ) -> ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) e. { 0 , 2 } )
Theorem	lgslem2 16286	The set Z of all integers with absolute value at most 1 contains { -u 1 , 0 , 1 }. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- Z = { x e. ZZ | ( abs ` x ) <_ 1 }   =>    |- ( -u 1 e. Z /\ 0 e. Z /\ 1 e. Z )
Theorem	lgslem3 16287*	The set Z of all integers with absolute value at most 1 is closed under multiplication. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- Z = { x e. ZZ | ( abs ` x ) <_ 1 }   =>    |- ( ( A e. Z /\ B e. Z ) -> ( A x. B ) e. Z )
Theorem	lgslem4 16288*	Lemma for lgsfcl2 16291. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 19-Mar-2022.)
|- Z = { x e. ZZ | ( abs ` x ) <_ 1 }   =>    |- ( ( A e. ZZ /\ P e. ( Prime \ { 2 } ) ) -> ( ( ( ( A ^ ( ( P - 1 ) / 2 ) ) + 1 ) mod P ) - 1 ) e. Z )
Theorem	lgsval 16289*	Value of the Legendre symbol at an arbitrary integer. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )   =>    |- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) = if ( N = 0 , if ( ( A ^ 2 ) = 1 , 1 , 0 ) , ( if ( ( N < 0 /\ A < 0 ) , -u 1 , 1 ) x. ( seq 1 ( x. , F ) ` ( abs ` N ) ) ) ) )
Theorem	lgsfvalg 16290*	Value of the function F which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by Jim Kingdon, 4-Nov-2024.)
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )   =>    |- ( ( A e. ZZ /\ N e. NN /\ M e. NN ) -> ( F ` M ) = if ( M e. Prime , ( if ( M = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( M - 1 ) / 2 ) ) + 1 ) mod M ) - 1 ) ) ^ ( M pCnt N ) ) , 1 ) )
Theorem	lgsfcl2 16291*	The function F is closed in integers with absolute value less than 1 (namely { -u 1 , 0 , 1 }, see zabsle1 16284). (Contributed by Mario Carneiro, 4-Feb-2015.)
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )   &    |- Z = { x e. ZZ | ( abs ` x ) <_ 1 }   =>    |- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> F : NN --> Z )
Theorem	lgscllem 16292*	The Legendre symbol is an element of Z. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )   &    |- Z = { x e. ZZ | ( abs ` x ) <_ 1 }   =>    |- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. Z )
Theorem	lgsfcl 16293*	Closure of the function F which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )   =>    |- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> F : NN --> ZZ )
Theorem	lgsfle1 16294*	The function F has magnitude less or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )   =>    |- ( ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) /\ M e. NN ) -> ( abs ` ( F ` M ) ) <_ 1 )
Theorem	lgsval2lem 16295*	Lemma for lgsval2 16301. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )   =>    |- ( ( A e. ZZ /\ N e. Prime ) -> ( A /L N ) = if ( N = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( N - 1 ) / 2 ) ) + 1 ) mod N ) - 1 ) ) )
Theorem	lgsval4lem 16296*	Lemma for lgsval4 16305. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- F = ( n e. NN |-> if ( n e. Prime , ( if ( n = 2 , if ( 2 || A , 0 , if ( ( A mod 8 ) e. { 1 , 7 } , 1 , -u 1 ) ) , ( ( ( ( A ^ ( ( n - 1 ) / 2 ) ) + 1 ) mod n ) - 1 ) ) ^ ( n pCnt N ) ) , 1 ) )   =>    |- ( ( A e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> F = ( n e. NN |-> if ( n e. Prime , ( ( A /L n ) ^ ( n pCnt N ) ) , 1 ) ) )
Theorem	lgscl2 16297*	The Legendre symbol is an integer with absolute value less than or equal to 1. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- Z = { x e. ZZ | ( abs ` x ) <_ 1 }   =>    |- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. Z )
Theorem	lgs0 16298	The Legendre symbol when the second argument is zero. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( A e. ZZ -> ( A /L 0 ) = if ( ( A ^ 2 ) = 1 , 1 , 0 ) )
Theorem	lgscl 16299	The Legendre symbol is an integer. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. ZZ )
Theorem	lgsle1 16300	The Legendre symbol has absolute value less than or equal to 1. Together with lgscl 16299 this implies that it takes values in { -u 1 , 0 , 1 }. (Contributed by Mario Carneiro, 4-Feb-2015.)
|- ( ( A e. ZZ /\ N e. ZZ ) -> ( abs ` ( A /L N ) ) <_ 1 )