P. 233 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23201-23300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ppiublem2 23201	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	ppiub 23202	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. RR /\ 0 <_ N ) -> (π ` N ) <_ ( ( N / 3 ) + 2 ) )
Theorem	vmalelog 23203	The von Mangoldt function is less than the natural log. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. NN -> (Λ ` A ) <_ ( log ` A ) )
Theorem	chtlepsi 23204	The first Chebyshev function is less than the second. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. RR -> ( theta ` A ) <_ (ψ ` A ) )
Theorem	chprpcl 23205	Closure of the second Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 8-Apr-2016.)
|- ( ( A e. RR /\ 2 <_ A ) -> (ψ ` A ) e. RR+ )
Theorem	chpeq0 23206	The second Chebyshev function is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 9-Apr-2016.)
|- ( A e. RR -> ( (ψ ` A ) = 0 <-> A < 2 ) )
Theorem	chteq0 23207	The first Chebyshev function is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 9-Apr-2016.)
|- ( A e. RR -> ( ( theta ` A ) = 0 <-> A < 2 ) )
Theorem	chtleppi 23208	Upper bound on the theta function. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. RR+ -> ( theta ` A ) <_ ( (π ` A ) x. ( log ` A ) ) )
Theorem	chtublem 23209	Lemma for chtub 23210. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( N e. NN -> ( theta ` ( ( 2 x. N ) - 1 ) ) <_ ( ( theta ` N ) + ( ( log ` 4 ) x. ( N - 1 ) ) ) )
Theorem	chtub 23210	An upper bound on the Chebyshev function. (Contributed by Mario Carneiro, 13-Mar-2014.) (Revised 22-Sep-2014.)
|- ( ( N e. RR /\ 2 < N ) -> ( theta ` N ) < ( ( log ` 2 ) x. ( ( 2 x. N ) - 3 ) ) )
Theorem	fsumvma 23211*	Rewrite a sum over the von Mangoldt function as a sum over prime powers. (Contributed by Mario Carneiro, 15-Apr-2016.)
|- ( x = ( p ^ k ) -> B = C )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A C_ NN )   &    |- ( ph -> P e. Fin )   &    |- ( ph -> ( ( p e. P /\ k e. K ) <-> ( ( p e. Prime /\ k e. NN ) /\ ( p ^ k ) e. A ) ) )   &    |- ( ( ph /\ x e. A ) -> B e. CC )   &    |- ( ( ph /\ ( x e. A /\ (Λ ` x ) = 0 ) ) -> B = 0 )   =>    |- ( ph -> sum_ x e. A B = sum_ p e. P sum_ k e. K C )
Theorem	fsumvma2 23212*	Apply fsumvma 23211 for the common case of all numbers less than a real number A. (Contributed by Mario Carneiro, 30-Apr-2016.)
|- ( x = ( p ^ k ) -> B = C )   &    |- ( ph -> A e. RR )   &    |- ( ( ph /\ x e. ( 1 ... ( |_ ` A ) ) ) -> B e. CC )   &    |- ( ( ph /\ ( x e. ( 1 ... ( |_ ` A ) ) /\ (Λ ` x ) = 0 ) ) -> B = 0 )   =>    |- ( ph -> sum_ x e. ( 1 ... ( |_ ` A ) ) B = sum_ p e. ( ( 0 [,] A ) i^i Prime ) sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) C )
Theorem	pclogsum 23213*	The logarithmic analogue of pcprod 14264. The sum of the logarithms of the primes dividing A multiplied by their powers yields the logarithm of A. (Contributed by Mario Carneiro, 15-Apr-2016.)
|- ( A e. NN -> sum_ p e. ( ( 1 ... A ) i^i Prime ) ( ( p pCnt A ) x. ( log ` p ) ) = ( log ` A ) )
Theorem	vmasum 23214*	The sum of the von Mangoldt function over the divisors of n. Equation 9.2.4 of [Shapiro], p. 328. (Contributed by Mario Carneiro, 15-Apr-2016.)
|- ( A e. NN -> sum_ n e. { x e. NN | x || A } (Λ ` n ) = ( log ` A ) )
Theorem	logfac2 23215*	Another expression for the logarithm of a factorial, in terms of the von Mangoldt function. Equation 9.2.7 of [Shapiro], p. 329. (Contributed by Mario Carneiro, 15-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( log ` ( ! ` ( |_ ` A ) ) ) = sum_ k e. ( 1 ... ( |_ ` A ) ) ( (Λ ` k ) x. ( |_ ` ( A / k ) ) ) )
Theorem	chpval2 23216*	Express the second Chebyshev function directly as a sum over the primes less than A (instead of indirectly through the von Mangoldt function). (Contributed by Mario Carneiro, 8-Apr-2016.)
|- ( A e. RR -> (ψ ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( ( log ` p ) x. ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )
Theorem	chpchtsum 23217*	The second Chebyshev function is the sum of the theta function at arguments quickly approaching zero. (This is usually stated as an infinite sum, but after a certain point, the terms are all zero, and it is easier for us to use an explicit finite sum.) (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. RR -> (ψ ` A ) = sum_ k e. ( 1 ... ( |_ ` A ) ) ( theta ` ( A ^c ( 1 / k ) ) ) )
Theorem	chpub 23218	An upper bound on the second Chebyshev function. (Contributed by Mario Carneiro, 8-Apr-2016.)
|- ( ( A e. RR /\ 1 <_ A ) -> (ψ ` A ) <_ ( ( theta ` A ) + ( ( sqr ` A ) x. ( log ` A ) ) ) )
Theorem	logfacubnd 23219	A simple upper bound on the logarithm of a factorial. (Contributed by Mario Carneiro, 16-Apr-2016.)
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( log ` ( ! ` ( |_ ` A ) ) ) <_ ( A x. ( log ` A ) ) )
Theorem	logfaclbnd 23220	A lower bound on the logarithm of a factorial. (Contributed by Mario Carneiro, 16-Apr-2016.)
|- ( A e. RR+ -> ( A x. ( ( log ` A ) - 2 ) ) <_ ( log ` ( ! ` ( |_ ` A ) ) ) )
Theorem	logfacbnd3 23221	Show the stronger statement log ( x ! ) = x log x - x + O ( log x ) alluded to in logfacrlim 23222. (Contributed by Mario Carneiro, 20-May-2016.)
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) <_ ( ( log ` A ) + 1 ) )
Theorem	logfacrlim 23222	Combine the estimates logfacubnd 23219 and logfaclbnd 23220, to get log ( x ! ) = x log x + O ( x ). Equation 9.2.9 of [Shapiro], p. 329. This is a weak form of the even stronger statement, log ( x ! ) = x log x - x + O ( log x ). (Contributed by Mario Carneiro, 16-Apr-2016.) (Revised by Mario Carneiro, 21-May-2016.)
|- ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ~~> r 1
Theorem	logexprlim 23223*	The sum sum_ n <_ x , log ^ N ( x / n ) has the asymptotic expansion ( N ! ) x + o ( x ). (More precisely, the omitted term has order O ( log ^ N ( x ) / x ).) (Contributed by Mario Carneiro, 22-May-2016.)
|- ( N e. NN0 -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ N ) / x ) ) ~~> r ( ! ` N ) )
Theorem	logfacrlim2 23224*	Write out logfacrlim 23222 as a sum of logs. (Contributed by Mario Carneiro, 18-May-2016.) (Revised by Mario Carneiro, 22-May-2016.)
|- ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) ~~> r 1
14.4.5  Perfect Number Theorem
Theorem	mersenne 23225	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 23226	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 23227	Lemma for perfect 23229. (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 23228	Lemma for perfect 23229. (Contributed by Mario Carneiro, 17-May-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 -> ( B e. Prime /\ B = ( ( 2 ^ ( A + 1 ) ) - 1 ) ) )
Theorem	perfect 23229*	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). (It follows from this that p is also prime.) 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 ) ) ) ) )
14.4.6  Characters of Z/nZ
Syntax	cdchr 23230	Extend class notation with the group of Dirichlet characters.
class DChr
Definition	df-dchr 23231*	The group of Dirichlet characters mod n is the set of monoid homomorphisms from ZZ / n ZZ to the multiplicative monoid of the complex numbers, equipped with the group operation of pointwise multiplication. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- DChr = ( n e. NN |-> [_ (ℤ/nℤ ` n ) / z ]_ [_ { x e. ( (mulGrp ` z ) MndHom (mulGrp ` ℂfld ) ) | ( ( ( Base ` z ) \ (Unit ` z ) ) X. { 0 } ) C_ x } / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. } )
Theorem	dchrval 23232*	Value of the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- B = ( Base ` Z )   &    |- U = (Unit ` Z )   &    |- ( ph -> N e. NN )   &    |- ( ph -> D = { x e. ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) ) | ( ( B \ U ) X. { 0 } ) C_ x } )   =>    |- ( ph -> G = { <. ( Base ` ndx ) , D >. , <. ( +g ` ndx ) , ( oF x. |` ( D X. D ) ) >. } )
Theorem	dchrbas 23233*	Base set of the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- B = ( Base ` Z )   &    |- U = (Unit ` Z )   &    |- ( ph -> N e. NN )   &    |- D = ( Base ` G )   =>    |- ( ph -> D = { x e. ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) ) | ( ( B \ U ) X. { 0 } ) C_ x } )
Theorem	dchrelbas 23234	A Dirichlet character is a monoid homomorphism from the multiplicative monoid on ℤ/nℤ to the multiplicative monoid of CC, which is zero off the group of units of ℤ/nℤ. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- B = ( Base ` Z )   &    |- U = (Unit ` Z )   &    |- ( ph -> N e. NN )   &    |- D = ( Base ` G )   =>    |- ( ph -> ( X e. D <-> ( X e. ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) ) /\ ( ( B \ U ) X. { 0 } ) C_ X ) ) )
Theorem	dchrelbas2 23235*	A Dirichlet character is a monoid homomorphism from the multiplicative monoid on ℤ/nℤ to the multiplicative monoid of CC, which is zero off the group of units of ℤ/nℤ. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- B = ( Base ` Z )   &    |- U = (Unit ` Z )   &    |- ( ph -> N e. NN )   &    |- D = ( Base ` G )   =>    |- ( ph -> ( X e. D <-> ( X e. ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) ) /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) ) )
Theorem	dchrelbas3 23236*	A Dirichlet character is a monoid homomorphism from the multiplicative monoid on ℤ/nℤ to the multiplicative monoid of CC, which is zero off the group of units of ℤ/nℤ. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- B = ( Base ` Z )   &    |- U = (Unit ` Z )   &    |- ( ph -> N e. NN )   &    |- D = ( Base ` G )   =>    |- ( ph -> ( X e. D <-> ( X : B --> CC /\ ( A. x e. U A. y e. U ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) ) ) )
Theorem	dchrelbasd 23237*	A Dirichlet character is a monoid homomorphism from the multiplicative monoid on ℤ/nℤ to the multiplicative monoid of CC, which is zero off the group of units of ℤ/nℤ. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- B = ( Base ` Z )   &    |- U = (Unit ` Z )   &    |- ( ph -> N e. NN )   &    |- D = ( Base ` G )   &    |- ( k = x -> X = A )   &    |- ( k = y -> X = C )   &    |- ( k = ( x ( .r ` Z ) y ) -> X = E )   &    |- ( k = ( 1r ` Z ) -> X = Y )   &    |- ( ( ph /\ k e. U ) -> X e. CC )   &    |- ( ( ph /\ ( x e. U /\ y e. U ) ) -> E = ( A x. C ) )   &    |- ( ph -> Y = 1 )   =>    |- ( ph -> ( k e. B |-> if ( k e. U , X , 0 ) ) e. D )
Theorem	dchrrcl 23238	Reverse closure for a Dirichlet character. (Contributed by Mario Carneiro, 12-May-2016.)
|- G = (DChr ` N )   &    |- D = ( Base ` G )   =>    |- ( X e. D -> N e. NN )
Theorem	dchrmhm 23239	A Dirichlet character is a monoid homomorphism. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   =>    |- D C_ ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) )
Theorem	dchrf 23240	A Dirichlet character is a function. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- ( ph -> X e. D )   =>    |- ( ph -> X : B --> CC )
Theorem	dchrelbas4 23241*	A Dirichlet character is a monoid homomorphism from the multiplicative monoid on ℤ/nℤ to the multiplicative monoid of CC, which is zero off the group of units of ℤ/nℤ. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- L = ( ZRHom ` Z )   =>    |- ( X e. D <-> ( N e. NN /\ X e. ( (mulGrp ` Z ) MndHom (mulGrp ` ℂfld ) ) /\ A. x e. ZZ ( 1 < ( x gcd N ) -> ( X ` ( L ` x ) ) = 0 ) ) )
Theorem	dchrzrh1 23242	Value of a Dirichlet character at one. (Contributed by Mario Carneiro, 4-May-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> X e. D )   =>    |- ( ph -> ( X ` ( L ` 1 ) ) = 1 )
Theorem	dchrzrhcl 23243	A Dirichlet character takes values in the complex numbers. (Contributed by Mario Carneiro, 12-May-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> X e. D )   &    |- ( ph -> A e. ZZ )   =>    |- ( ph -> ( X ` ( L ` A ) ) e. CC )
Theorem	dchrzrhmul 23244	A Dirichlet character is completely multiplicative. (Contributed by Mario Carneiro, 4-May-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- L = ( ZRHom ` Z )   &    |- ( ph -> X e. D )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> C e. ZZ )   =>    |- ( ph -> ( X ` ( L ` ( A x. C ) ) ) = ( ( X ` ( L ` A ) ) x. ( X ` ( L ` C ) ) ) )
Theorem	dchrplusg 23245	Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- .x. = ( +g ` G )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> .x. = ( oF x. |` ( D X. D ) ) )
Theorem	dchrmul 23246	Group operation on the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- .x. = ( +g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> Y e. D )   =>    |- ( ph -> ( X .x. Y ) = ( X oF x. Y ) )
Theorem	dchrmulcl 23247	Closure of the group operation on Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- .x. = ( +g ` G )   &    |- ( ph -> X e. D )   &    |- ( ph -> Y e. D )   =>    |- ( ph -> ( X .x. Y ) e. D )
Theorem	dchrn0 23248	A Dirichlet character is nonzero on the units of ℤ/nℤ. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- U = (Unit ` Z )   &    |- ( ph -> X e. D )   &    |- ( ph -> A e. B )   =>    |- ( ph -> ( ( X ` A ) =/= 0 <-> A e. U ) )
Theorem	dchr1cl 23249*	Closure of the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- U = (Unit ` Z )   &    |- .1. = ( k e. B |-> if ( k e. U , 1 , 0 ) )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> .1. e. D )
Theorem	dchrmulid2 23250*	Left identity for the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- U = (Unit ` Z )   &    |- .1. = ( k e. B |-> if ( k e. U , 1 , 0 ) )   &    |- .x. = ( +g ` G )   &    |- ( ph -> X e. D )   =>    |- ( ph -> ( .1. .x. X ) = X )
Theorem	dchrinvcl 23251*	Closure of the group inverse operation on Dirichlet characters. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- U = (Unit ` Z )   &    |- .1. = ( k e. B |-> if ( k e. U , 1 , 0 ) )   &    |- .x. = ( +g ` G )   &    |- ( ph -> X e. D )   &    |- K = ( k e. B |-> if ( k e. U , ( 1 / ( X ` k ) ) , 0 ) )   =>    |- ( ph -> ( K e. D /\ ( K .x. X ) = .1. ) )
Theorem	dchrabl 23252	The set of Dirichlet characters is an Abelian group. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- G = (DChr ` N )   =>    |- ( N e. NN -> G e. Abel )
Theorem	dchrfi 23253	The group of Dirichlet characters is a finite group. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- G = (DChr ` N )   &    |- D = ( Base ` G )   =>    |- ( N e. NN -> D e. Fin )
Theorem	dchrghm 23254	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.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- U = (Unit ` Z )   &    |- H = ( (mulGrp ` Z ) ↾s U )   &    |- M = ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) )   &    |- ( ph -> X e. D )   =>    |- ( ph -> ( X |` U ) e. ( H GrpHom M ) )
Theorem	dchr1 23255	Value of the principal Dirichlet character. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- .1. = ( 0g ` G )   &    |- U = (Unit ` Z )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A e. U )   =>    |- ( ph -> ( .1. ` A ) = 1 )
Theorem	dchreq 23256*	A Dirichlet character is determined by its values on the unit group. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- U = (Unit ` Z )   &    |- ( ph -> X e. D )   &    |- ( ph -> Y e. D )   =>    |- ( ph -> ( X = Y <-> A. k e. U ( X ` k ) = ( Y ` k ) ) )
Theorem	dchrresb 23257	A Dirichlet character is determined by its values on the unit group. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- U = (Unit ` Z )   &    |- ( ph -> X e. D )   &    |- ( ph -> Y e. D )   =>    |- ( ph -> ( ( X |` U ) = ( Y |` U ) <-> X = Y ) )
Theorem	dchrabs 23258	A Dirichlet character takes values on the unit circle. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- ( ph -> X e. D )   &    |- Z = (ℤ/nℤ ` N )   &    |- U = (Unit ` Z )   &    |- ( ph -> A e. U )   =>    |- ( ph -> ( abs ` ( X ` A ) ) = 1 )
Theorem	dchrinv 23259	The inverse of a Dirichlet character is the conjugate (which is also the multiplicative inverse, because the values of X are unimodular). (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- ( ph -> X e. D )   &    |- I = ( invg ` G )   =>    |- ( ph -> ( I ` X ) = ( * o. X ) )
Theorem	dchrabs2 23260	A Dirichlet character takes values inside the unit circle. (Contributed by Mario Carneiro, 3-May-2016.)
|- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- Z = (ℤ/nℤ ` N )   &    |- B = ( Base ` Z )   &    |- ( ph -> X e. D )   &    |- ( ph -> A e. B )   =>    |- ( ph -> ( abs ` ( X ` A ) ) <_ 1 )
Theorem	dchr1re 23261	The principal Dirichlet character is a real character. (Contributed by Mario Carneiro, 2-May-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- .1. = ( 0g ` G )   &    |- B = ( Base ` Z )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> .1. : B --> RR )
Theorem	dchrptlem1 23262*	Lemma for dchrpt 23265. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- .1. = ( 1r ` Z )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A =/= .1. )   &    |- U = (Unit ` Z )   &    |- H = ( (mulGrp ` Z ) ↾s U )   &    |- .x. = (.g ` H )   &    |- S = ( k e. dom W |-> ran ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) )   &    |- ( ph -> A e. U )   &    |- ( ph -> W e. Word U )   &    |- ( ph -> H dom DProd S )   &    |- ( ph -> ( H DProd S ) = U )   &    |- P = ( HdProj S )   &    |- O = ( od ` H )   &    |- T = ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) )   &    |- ( ph -> I e. dom W )   &    |- ( ph -> ( ( P ` I ) ` A ) =/= .1. )   &    |- X = ( u e. U |-> ( iota h E. m e. ZZ ( ( ( P ` I ) ` u ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) )   =>    |- ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) -> ( X ` C ) = ( T ^ M ) )
Theorem	dchrptlem2 23263*	Lemma for dchrpt 23265. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- .1. = ( 1r ` Z )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A =/= .1. )   &    |- U = (Unit ` Z )   &    |- H = ( (mulGrp ` Z ) ↾s U )   &    |- .x. = (.g ` H )   &    |- S = ( k e. dom W |-> ran ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) )   &    |- ( ph -> A e. U )   &    |- ( ph -> W e. Word U )   &    |- ( ph -> H dom DProd S )   &    |- ( ph -> ( H DProd S ) = U )   &    |- P = ( HdProj S )   &    |- O = ( od ` H )   &    |- T = ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) )   &    |- ( ph -> I e. dom W )   &    |- ( ph -> ( ( P ` I ) ` A ) =/= .1. )   &    |- X = ( u e. U |-> ( iota h E. m e. ZZ ( ( ( P ` I ) ` u ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) )   =>    |- ( ph -> E. x e. D ( x ` A ) =/= 1 )
Theorem	dchrptlem3 23264*	Lemma for dchrpt 23265. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- .1. = ( 1r ` Z )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A =/= .1. )   &    |- U = (Unit ` Z )   &    |- H = ( (mulGrp ` Z ) ↾s U )   &    |- .x. = (.g ` H )   &    |- S = ( k e. dom W |-> ran ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) )   &    |- ( ph -> A e. U )   &    |- ( ph -> W e. Word U )   &    |- ( ph -> H dom DProd S )   &    |- ( ph -> ( H DProd S ) = U )   =>    |- ( ph -> E. x e. D ( x ` A ) =/= 1 )
Theorem	dchrpt 23265*	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.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- .1. = ( 1r ` Z )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A =/= .1. )   &    |- ( ph -> A e. B )   =>    |- ( ph -> E. x e. D ( x ` A ) =/= 1 )
Theorem	dchrsum2 23266*	An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character X is 0 if X is non-principal and phi ( n ) otherwise. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- U = (Unit ` Z )   =>    |- ( ph -> sum_ a e. U ( X ` a ) = if ( X = .1. , ( phi ` N ) , 0 ) )
Theorem	dchrsum 23267*	An orthogonality relation for Dirichlet characters: the sum of all the values of a Dirichlet character X is 0 if X is non-principal and phi ( n ) otherwise. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- .1. = ( 0g ` G )   &    |- ( ph -> X e. D )   &    |- B = ( Base ` Z )   =>    |- ( ph -> sum_ a e. B ( X ` a ) = if ( X = .1. , ( phi ` N ) , 0 ) )
Theorem	sumdchr2 23268*	Lemma for sumdchr 23270. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- Z = (ℤ/nℤ ` N )   &    |- .1. = ( 1r ` Z )   &    |- B = ( Base ` Z )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A e. B )   =>    |- ( ph -> sum_ x e. D ( x ` A ) = if ( A = .1. , ( # ` D ) , 0 ) )
Theorem	dchrhash 23269	There are exactly phi ( N ) Dirichlet characters modulo N. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- D = ( Base ` G )   =>    |- ( N e. NN -> ( # ` D ) = ( phi ` N ) )
Theorem	sumdchr 23270*	An orthogonality relation for Dirichlet characters: the sum of x ( A ) for fixed A and all x is 0 if A = 1 and phi ( n ) otherwise. Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- Z = (ℤ/nℤ ` N )   &    |- .1. = ( 1r ` Z )   &    |- B = ( Base ` Z )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A e. B )   =>    |- ( ph -> sum_ x e. D ( x ` A ) = if ( A = .1. , ( phi ` N ) , 0 ) )
Theorem	dchr2sum 23271*	An orthogonality relation for Dirichlet characters: the sum of X ( a ) x. * Y ( a ) over all a is nonzero only when X = Y. Part of Theorem 6.5.2 of [Shapiro] p. 232. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- Z = (ℤ/nℤ ` N )   &    |- D = ( Base ` G )   &    |- B = ( Base ` Z )   &    |- ( ph -> X e. D )   &    |- ( ph -> Y e. D )   =>    |- ( ph -> sum_ a e. B ( ( X ` a ) x. ( * ` ( Y ` a ) ) ) = if ( X = Y , ( phi ` N ) , 0 ) )
Theorem	sum2dchr 23272*	An orthogonality relation for Dirichlet characters: the sum of x ( A ) for fixed A and all x is 0 if A = 1 and phi ( n ) otherwise. Part of Theorem 6.5.2 of [Shapiro] p. 232. (Contributed by Mario Carneiro, 28-Apr-2016.)
|- G = (DChr ` N )   &    |- D = ( Base ` G )   &    |- Z = (ℤ/nℤ ` N )   &    |- B = ( Base ` Z )   &    |- U = (Unit ` Z )   &    |- ( ph -> N e. NN )   &    |- ( ph -> A e. B )   &    |- ( ph -> C e. U )   =>    |- ( ph -> sum_ x e. D ( ( x ` A ) x. ( * ` ( x ` C ) ) ) = if ( A = C , ( phi ` N ) , 0 ) )
14.4.7  Bertrand's postulate
Theorem	bcctr 23273	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 23274*	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 23275	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 23276	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 23277	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 23278	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	efexple 23279	Convert a bound on a power to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.)
|- ( ( ( A e. RR /\ 1 < A ) /\ N e. ZZ /\ B e. RR+ ) -> ( ( A ^ N ) <_ B <-> N <_ ( |_ ` ( ( log ` B ) / ( log ` A ) ) ) ) )
Theorem	bpos1lem 23280*	Lemma for bpos1 23281. (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 23281*	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.)
|- ( ( N e. NN /\ N <_ ; 6 4 ) -> E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
Theorem	bposlem1 23282	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 23283	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 23284*	Lemma for bpos 23291. Since the binomial coefficient does not have any primes in the range ( 2 N / 3 , N ] or ( 2 N , +oo ) by bposlem2 23283 and prmfac1 14109, 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 23285*	Lemma for bpos 23291. (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 23286*	Lemma for bpos 23291. Bound the product of all small primes in the binomial coefficient. (Contributed by Mario Carneiro, 15-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 -> ( seq 1 ( x. , F ) ` M ) <_ ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) )
Theorem	bposlem6 23287*	Lemma for bpos 23291. 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.)
|- ( 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 23288*	Lemma for bpos 23291. The function F is decreasing. (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 23289	Lemma for bpos 23291. Evaluate F ( 6 4 ) and show it 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 23290*	Lemma for bpos 23291. Derive a contradiction. (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 ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ; 6 4 < N )   &    |- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )   =>    |- ( ph -> ps )
Theorem	bpos 23291*	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 ) ) )
14.4.8  Legendre symbol
Syntax	clgs 23292	Extend class notation with the Legendre symbol function.
class /L
Definition	df-lgs 23293*	Define the Legendre symbol (actually the Kronecker symbol, which extends the Legendre symbol to all integers). (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	lgslem1 23294	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 23295	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 23296*	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 23297*	The function F is closed in integers with absolute value less than 1 (namely { -u 1 , 0 , 1 } although this representation is less useful to us). (Contributed by Mario Carneiro, 4-Feb-2015.)
|- 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 23298*	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	lgsfval 23299*	Value 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 ) )   =>    |- ( 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 23300*	The function F is closed in integers with absolute value less than 1 (namely { -u 1 , 0 , 1 } although this representation is less useful to us). (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 )