P. 250 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24901-25000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	chtrpcl 24901	Closure of the Chebyshev function in the positive reals. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. RR /\ 2 <_ A ) -> ( theta ` A ) e. RR+ )
Theorem	ppieq0 24902	The prime-counting function π is zero iff its argument is less than 2. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. RR -> ( (π ` A ) = 0 <-> A < 2 ) )
Theorem	ppiltx 24903	The prime-counting function π is strictly less than the identity. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. RR+ -> (π ` A ) < A )
Theorem	prmorcht 24904	Relate the primorial (product of the first n primes) 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	mumullem1 24905	Lemma for mumul 24907. A multiple of a non-squarefree number is non-squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.)
|- ( ( ( A e. NN /\ B e. NN ) /\ ( mmu ` A ) = 0 ) -> ( mmu ` ( A x. B ) ) = 0 )
Theorem	mumullem2 24906	Lemma for mumul 24907. The product of two coprime squarefree numbers is squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.)
|- ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( mmu ` ( A x. B ) ) =/= 0 )
Theorem	mumul 24907	The Möbius function is a multiplicative function. This is one of the primary interests of the Möbius function as an arithmetic function. (Contributed by Mario Carneiro, 3-Oct-2014.)
|- ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) -> ( mmu ` ( A x. B ) ) = ( ( mmu ` A ) x. ( mmu ` B ) ) )
Theorem	sqff1o 24908*	There is a bijection from the squarefree divisors of a number N to the powerset of the prime divisors of N. Among other things, this implies that a number has 2 ^ k squarefree divisors where k is the number of prime divisors, and a squarefree number has 2 ^ k divisors (because all divisors of a squarefree number are squarefree). The inverse function to F takes the product of all the primes in some subset of prime divisors of N. (Contributed by Mario Carneiro, 1-Jul-2015.)
|- S = { x e. NN | ( ( mmu ` x ) =/= 0 /\ x || N ) }   &    |- F = ( n e. S |-> { p e. Prime | p || n } )   &    |- G = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )   =>    |- ( N e. NN -> F : S -1-1-onto-> ~P { p e. Prime | p || N } )
Theorem	fsumdvdsdiaglem 24909*	A "diagonal commutation" of divisor sums analogous to fsum0diag 14509. (Contributed by Mario Carneiro, 2-Jul-2015.) (Revised by Mario Carneiro, 8-Apr-2016.)
|- ( ph -> N e. NN )   =>    |- ( ph -> ( ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) -> ( k e. { x e. NN | x || N } /\ j e. { x e. NN | x || ( N / k ) } ) ) )
Theorem	fsumdvdsdiag 24910*	A "diagonal commutation" of divisor sums analogous to fsum0diag 14509. (Contributed by Mario Carneiro, 2-Jul-2015.) (Revised by Mario Carneiro, 8-Apr-2016.)
|- ( ph -> N e. NN )   &    |- ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || ( N / j ) } ) ) -> A e. CC )   =>    |- ( ph -> sum_ j e. { x e. NN | x || N } sum_ k e. { x e. NN | x || ( N / j ) } A = sum_ k e. { x e. NN | x || N } sum_ j e. { x e. NN | x || ( N / k ) } A )
Theorem	fsumdvdscom 24911*	A double commutation of divisor sums based on fsumdvdsdiag 24910. Note that A depends on both j and k. (Contributed by Mario Carneiro, 13-May-2016.)
|- ( ph -> N e. NN )   &    |- ( j = ( k x. m ) -> A = B )   &    |- ( ( ph /\ ( j e. { x e. NN | x || N } /\ k e. { x e. NN | x || j } ) ) -> A e. CC )   =>    |- ( ph -> sum_ j e. { x e. NN | x || N } sum_ k e. { x e. NN | x || j } A = sum_ k e. { x e. NN | x || N } sum_ m e. { x e. NN | x || ( N / k ) } B )
Theorem	dvdsppwf1o 24912*	A bijection from the divisors of a prime power to the integers less than the prime count. (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	dvdsflf1o 24913*	A bijection from the numbers less than N / A to the multiples of A less than N. Useful for some sum manipulations. (Contributed by Mario Carneiro, 3-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> N e. NN )   &    |- F = ( n e. ( 1 ... ( |_ ` ( A / N ) ) ) |-> ( N x. n ) )   =>    |- ( ph -> F : ( 1 ... ( |_ ` ( A / N ) ) ) -1-1-onto-> { x e. ( 1 ... ( |_ ` A ) ) | N || x } )
Theorem	dvdsflsumcom 24914*	A sum commutation from sum_ n <_ A , sum_ d || n , B ( n , d ) to sum_ d <_ A , sum_ m <_ A / d , B ( n , d m ). (Contributed by Mario Carneiro, 4-May-2016.)
|- ( n = ( d x. m ) -> B = C )   &    |- ( ph -> A e. RR )   &    |- ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ d e. { x e. NN | x || n } ) ) -> B e. CC )   =>    |- ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ d e. { x e. NN | x || n } B = sum_ d e. ( 1 ... ( |_ ` A ) ) sum_ m e. ( 1 ... ( |_ ` ( A / d ) ) ) C )
Theorem	fsumfldivdiaglem 24915*	Lemma for fsumfldivdiag 24916. (Contributed by Mario Carneiro, 10-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) -> ( m e. ( 1 ... ( |_ ` A ) ) /\ n e. ( 1 ... ( |_ ` ( A / m ) ) ) ) ) )
Theorem	fsumfldivdiag 24916*	The right-hand side of dvdsflsumcom 24914 is commutative in the variables, because it can be written as the manifestly symmetric sum over those <. m , n >. such that m x. n <_ A. (Contributed by Mario Carneiro, 4-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> B e. CC )   =>    |- ( ph -> sum_ n e. ( 1 ... ( |_ ` A ) ) sum_ m e. ( 1 ... ( |_ ` ( A / n ) ) ) B = sum_ m e. ( 1 ... ( |_ ` A ) ) sum_ n e. ( 1 ... ( |_ ` ( A / m ) ) ) B )
Theorem	musum 24917*	The sum of the Möbius function over the divisors of N gives one if N = 1, but otherwise always sums to zero. Theorem 2.1 in [ApostolNT] p. 25. This makes the Möbius function useful for inverting divisor sums; see also muinv 24919. (Contributed by Mario Carneiro, 2-Jul-2015.)
|- ( N e. NN -> sum_ k e. { n e. NN | n || N } ( mmu ` k ) = if ( N = 1 , 1 , 0 ) )
Theorem	musumsum 24918*	Evaluate a collapsing sum over the Möbius function. (Contributed by Mario Carneiro, 4-May-2016.)
|- ( m = 1 -> B = C )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A C_ NN )   &    |- ( ph -> 1 e. A )   &    |- ( ( ph /\ m e. A ) -> B e. CC )   =>    |- ( ph -> sum_ m e. A sum_ k e. { n e. NN | n || m } ( ( mmu ` k ) x. B ) = C )
Theorem	muinv 24919*	The Möbius inversion formula. If G ( n ) = sum_ k || n F ( k ) for every n e. NN, then F ( n ) = sum_ k || n mmu ( k ) G ( n / k ) = sum_ k || n mmu ( n / k ) G ( k ), i.e. the Möbius function is the Dirichlet convolution inverse of the constant function 1. Theorem 2.9 in [ApostolNT] p. 32. (Contributed by Mario Carneiro, 2-Jul-2015.)
|- ( ph -> F : NN --> CC )   &    |- ( ph -> G = ( n e. NN |-> sum_ k e. { x e. NN | x || n } ( F ` k ) ) )   =>    |- ( ph -> F = ( m e. NN |-> sum_ j e. { x e. NN | x || m } ( ( mmu ` j ) x. ( G ` ( m / j ) ) ) ) )
Theorem	dvdsmulf1o 24920*	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 Mario Carneiro, 2-Jul-2015.)
|- ( 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. |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z )
Theorem	fsumdvdsmul 24921*	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.)
|- ( 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 24922*	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 24923	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 24924	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 24925	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 24926	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 24927	Lemma for ppiub 24929. (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 24928	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 24929	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 24930	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 24931	The first Chebyshev function is less than the second. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. RR -> ( theta ` A ) <_ (ψ ` A ) )
Theorem	chprpcl 24932	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 24933	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 24934	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 24935	Upper bound on the theta function. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. RR+ -> ( theta ` A ) <_ ( (π ` A ) x. ( log ` A ) ) )
Theorem	chtublem 24936	Lemma for chtub 24937. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( N e. NN -> ( theta ` ( ( 2 x. N ) - 1 ) ) <_ ( ( theta ` N ) + ( ( log ` 4 ) x. ( N - 1 ) ) ) )
Theorem	chtub 24937	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 24938*	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 24939*	Apply fsumvma 24938 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 24940*	The logarithmic analogue of pcprod 15599. 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 24941*	The sum of the von Mangoldt function over the divisors of n. Equation 9.2.4 of [Shapiro], p. 328 and theorem 2.10 in [ApostolNT] p. 32. (Contributed by Mario Carneiro, 15-Apr-2016.)
|- ( A e. NN -> sum_ n e. { x e. NN | x || A } (Λ ` n ) = ( log ` A ) )
Theorem	logfac2 24942*	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 24943*	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 24944*	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 24945	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 24946	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 24947	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 24948	Show the stronger statement log ( x ! ) = x log x - x + O ( log x ) alluded to in logfacrlim 24949. (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 24949	Combine the estimates logfacubnd 24946 and logfaclbnd 24947, 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 24950*	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 24951*	Write out logfacrlim 24949 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 24952	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 24953	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 24954	Lemma for perfect 24956. (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 24955	Lemma for perfect 24956. (Contributed by Mario Carneiro, 17-May-2016.) Replace OLD theorem. (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 24956*	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 24957	Extend class notation with the group of Dirichlet characters.
class DChr
Definition	df-dchr 24958*	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 24959*	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 24960*	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 24961	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 24962*	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 24963*	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 24964*	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 24965	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 24966	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 24967	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 24968*	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 24969	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 24970	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 24971	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 24972	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 24973	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 24974	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 24975	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 24976*	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 24977*	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 24978*	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 24979	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 24980	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 24981	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 24982	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 24983*	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 24984	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 24985	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 24986	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 24987	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 24988	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 24989*	Lemma for dchrpt 24992. (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 24990*	Lemma for dchrpt 24992. (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 24991*	Lemma for dchrpt 24992. (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 24992*	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 24993*	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 24994*	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 24995*	Lemma for sumdchr 24997. (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 24996	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 24997*	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 24998*	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 24999*	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 25000	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 ) ) ) )