P. 210 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 20901-21000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cht1 20901	The Chebyshev function at 1. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( theta ` 1 ) = 0
Theorem	vma1 20902	The von Mangoldt function at 1. (Contributed by Mario Carneiro, 9-Apr-2016.)
|- (Λ ` 1 ) = 0
Theorem	chp1 20903	The second Chebyshev function at 1. (Contributed by Mario Carneiro, 9-Apr-2016.)
|- (ψ ` 1 ) = 0
Theorem	ppi1i 20904	Inference form of ppiprm 20887. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- M e. NN0   &    |- N = ( M + 1 )   &    |- (π ` M ) = K   &    |- N e. Prime   =>    |- (π ` N ) = ( K + 1 )
Theorem	ppi2i 20905	Inference form of ppinprm 20888. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- M e. NN0   &    |- N = ( M + 1 )   &    |- (π ` M ) = K   &    |- -. N e. Prime   =>    |- (π ` N ) = K
Theorem	ppi2 20906	The prime pi function at 2. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- (π ` 2 ) = 1
Theorem	ppi3 20907	The prime pi function at 3. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- (π ` 3 ) = 2
Theorem	cht2 20908	The Chebyshev function at 2. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( theta ` 2 ) = ( log ` 2 )
Theorem	cht3 20909	The Chebyshev function at 3. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( theta ` 3 ) = ( log ` 6 )
Theorem	ppinncl 20910	Closure of the prime pi function in the positive integers. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- ( ( A e. RR /\ 2 <_ A ) -> (π ` A ) e. NN )
Theorem	chtrpcl 20911	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 20912	The prime pi 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 20913	The prime pi function is strictly less than the identity. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. RR+ -> (π ` A ) < A )
Theorem	prmorcht 20914	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 20915	Lemma for mumul 20917. 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 20916	Lemma for mumul 20917. 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 20917	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 20918*	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	dvdsdivcl 20919*	The complement of a divisor of N is also a divisor of N. (Contributed by Mario Carneiro, 2-Jul-2015.)
|- ( ( N e. NN /\ A e. { x e. NN | x || N } ) -> ( N / A ) e. { x e. NN | x || N } )
Theorem	dvdsflip 20920*	An involution of the divisors of a number. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro, 13-May-2016.)
|- A = { x e. NN | x || N }   &    |- F = ( y e. A |-> ( N / y ) )   =>    |- ( N e. NN -> F : A -1-1-onto-> A )
Theorem	fsumdvdsdiaglem 20921*	A "diagonal commutation" of divisor sums analogous to fsum0diag 12516. (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 20922*	A "diagonal commutation" of divisor sums analogous to fsum0diag 12516. (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 20923*	A double commutation of divisor sums based on fsumdvdsdiag 20922. 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 20924*	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 20925*	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 20926*	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 20927*	Lemma for fsumfldivdiag 20928. (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 20928*	The right-hand side of dvdsflsumcom 20926 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 20929*	The sum of the Möbius function over the divisors of N gives one if N = 1, but otherwise always sums to zero. This makes the Möbius function useful for inverting divisor sums; see also muinv 20931. (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 20930*	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 20931*	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. (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 20932*	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 20933*	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 20934*	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 20935	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 20936	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 20937	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 20938	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 20939	Lemma for ppiub 20941. (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 20940	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 20941	An upper bound on the Gauss prime pi 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 20942	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 20943	The first Chebyshev function is less than the second. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. RR -> ( theta ` A ) <_ (ψ ` A ) )
Theorem	chprpcl 20944	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 20945	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 20946	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 20947	Upper bound on the theta function. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. RR+ -> ( theta ` A ) <_ ( (π ` A ) x. ( log ` A ) ) )
Theorem	chtublem 20948	Lemma for chtub 20949. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( N e. NN -> ( theta ` ( ( 2 x. N ) - 1 ) ) <_ ( ( theta ` N ) + ( ( log ` 4 ) x. ( N - 1 ) ) ) )
Theorem	chtub 20949	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 20950*	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 20951*	Apply fsumvma 20950 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 20952*	The logarithmic analogue of pcprod 13219. 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 20953*	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 20954*	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 20955*	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 20956*	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 20957	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 20958	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 20959	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 20960	Show the stronger statement log ( x ! ) = x log x - x + O ( log x ) alluded to in logfacrlim 20961. (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 20961	Combine the estimates logfacubnd 20958 and logfaclbnd 20959, 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 20962*	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 20963*	Write out logfacrlim 20961 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
13.4.5  Perfect Number Theorem
Theorem	mersenne 20964	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 20965	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 20966	Lemma for perfect 20968. (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 20967	Lemma for perfect 20968. (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 20968*	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.) (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 ) ) ) ) )
13.4.6  Characters of Z/nZ
Syntax	cdchr 20969	Extend class notation with the group of Dirichlet characters.
class DChr
Definition	df-dchr 20970*	The group of Dirichlet characters mod n is the set of monoid homomorphisms from ZZ / n ZZ to the multiplicative monoid of the complexes, 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 ) , ( o F x. |` ( b X. b ) ) >. } )
Theorem	dchrval 20971*	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 ) , ( o F x. |` ( D X. D ) ) >. } )
Theorem	dchrbas 20972*	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 20973	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 20974*	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 20975*	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 20976*	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 20977	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 20978	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 20979	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 20980*	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 20981	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 20982	A Dirichlet character takes values in the complexes. (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 20983	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 20984	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. = ( o F x. |` ( D X. D ) ) )
Theorem	dchrmul 20985	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 o F x. Y ) )
Theorem	dchrmulcl 20986	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 20987	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 20988*	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 20989*	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 20990*	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 20991	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 20992	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 20993	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 20994	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 20995*	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 20996	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 20997	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 20998	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 = ( inv g ` G )   =>    |- ( ph -> ( I ` X ) = ( * o. X ) )
Theorem	dchrabs2 20999	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 21000	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 )