P. 209 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 - 20801-20900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	harmonicubnd 20801*	A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- ( ( A e. RR /\ 1 <_ A ) -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) <_ ( ( log ` A ) + 1 ) )
Theorem	harmonicbnd4 20802*	The asymptotic behavior of sum_ m <_ A , 1 / m = log A + gamma + O ( 1 / A ). (Contributed by Mario Carneiro, 14-May-2016.)
|- ( A e. RR+ -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) <_ ( 1 / A ) )
Theorem	fsumharmonic 20803*	Bound a finite sum based on the harmonic series, where the "strong" bound C only applies asymptotically, and there is a "weak" bound R for the remaining values. (Contributed by Mario Carneiro, 18-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> ( T e. RR /\ 1 <_ T ) )   &    |- ( ph -> ( R e. RR /\ 0 <_ R ) )   &    |- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> B e. CC )   &    |- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> C e. RR )   &    |- ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) -> 0 <_ C )   &    |- ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ T <_ ( A / n ) ) -> ( abs ` B ) <_ ( C x. n ) )   &    |- ( ( ( ph /\ n e. ( 1 ... ( |_ ` A ) ) ) /\ ( A / n ) < T ) -> ( abs ` B ) <_ R )   =>    |- ( ph -> ( abs ` sum_ n e. ( 1 ... ( |_ ` A ) ) ( B / n ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` A ) ) C + ( R x. ( ( log ` T ) + 1 ) ) ) )
13.4  Basic number theory
13.4.1  Wilson's theorem
Theorem	wilthlem1 20804	The only elements that are equal to their own inverses in the multiplicative group of nonzero elements in ZZ / P ZZ are 1 and -u 1 == P - 1. (Note that from prmdiveq 13130, ( N ^ ( P - 2 ) ) mod P is the modular inverse of N in ZZ / P ZZ. (Contributed by Mario Carneiro, 24-Jan-2015.)
|- ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( N = ( ( N ^ ( P - 2 ) ) mod P ) <-> ( N = 1 \/ N = ( P - 1 ) ) ) )
Theorem	wilthlem2 20805*	Lemma for wilth 20807: induction step. The "hand proof" version of this theorem works by writing out the list of all numbers from 1 to P - 1 in pairs such that a number is paired with its inverse. Every number has a unique inverse different from itself except 1 and P - 1, and so each pair multiplies to 1, and 1 and P - 1 == -u 1 multiply to -u 1, so the full product is equal to -u 1. Here we make this precise by doing the product pair by pair. The induction hypothesis says that every subset S of 1 ... ( P - 1 ) that is closed under inverse (i.e. all pairs are matched up) and contains P - 1 multiplies to -u 1 mod P. Given such a set, we take out one element z =/= P - 1. If there are no such elements, then S = { P - 1 } which forms the base case. Otherwise, S \ { z , z ^ -u 1 } is also closed under inverse and contains P - 1, so the induction hypothesis says that this equals -u 1; and the remaining two elements are either equal to each other, in which case wilthlem1 20804 gives that z = 1 or P - 1, and we've already excluded the second case, so the product gives 1; or z =/= z ^ -u 1 and their product is 1. In either case the accumulated product is unaffected. (Contributed by Mario Carneiro, 24-Jan-2015.)
|- T = (mulGrp ` ℂfld )   &    |- A = { x e. ~P ( 1 ... ( P - 1 ) ) | ( ( P - 1 ) e. x /\ A. y e. x ( ( y ^ ( P - 2 ) ) mod P ) e. x ) }   &    |- ( ph -> P e. Prime )   &    |- ( ph -> S e. A )   &    |- ( ph -> A. s e. A ( s C. S -> ( ( T gsumg ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) )   =>    |- ( ph -> ( ( T gsumg ( _I |` S ) ) mod P ) = ( -u 1 mod P ) )
Theorem	wilthlem3 20806*	Lemma for wilth 20807. Here we round out the argument of wilthlem2 20805 with the final step of the induction. The induction argument shows that every subset of 1 ... ( P - 1 ) that is closed under inverse and contains P - 1 multiplies to -u 1 mod P, and clearly 1 ... ( P - 1 ) itself is such a set. Thus, the product of all the elements is -u 1, and all that is left is to translate the group sum notation (which we used for its unordered summing capabilities) into an ordered sequence to match the definition of the factorial. (Contributed by Mario Carneiro, 24-Jan-2015.)
|- T = (mulGrp ` ℂfld )   &    |- A = { x e. ~P ( 1 ... ( P - 1 ) ) | ( ( P - 1 ) e. x /\ A. y e. x ( ( y ^ ( P - 2 ) ) mod P ) e. x ) }   =>    |- ( P e. Prime -> P || ( ( ! ` ( P - 1 ) ) + 1 ) )
Theorem	wilth 20807	Wilson's theorem. A number is prime iff it is greater or equal to 2 and ( N - 1 ) ! is congruent to -u 1, mod N, or alternatively if N divides ( N - 1 ) ! + 1. In this part of the proof we show the relatively simple reverse implication; see wilthlem3 20806 for the forward implication. (Contributed by Mario Carneiro, 24-Jan-2015.) (Proof shortened by Fan Zheng, 16-Jun-2016.)
|- ( N e. Prime <-> ( N e. ( ZZ>= ` 2 ) /\ N || ( ( ! ` ( N - 1 ) ) + 1 ) ) )
13.4.2  The Fundamental Theorem of Algebra
Theorem	ftalem1 20808*	Lemma for fta 20815: "growth lemma". There exists some r such that F is arbitrarily close in proportion to its dominant term. (Contributed by Mario Carneiro, 14-Sep-2014.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> E e. RR+ )   &    |- T = ( sum_ k e. ( 0 ... ( N - 1 ) ) ( abs ` ( A ` k ) ) / E )   =>    |- ( ph -> E. r e. RR A. x e. CC ( r < ( abs ` x ) -> ( abs ` ( ( F ` x ) - ( ( A ` N ) x. ( x ^ N ) ) ) ) < ( E x. ( ( abs ` x ) ^ N ) ) ) )
Theorem	ftalem2 20809*	Lemma for fta 20815. There exists some r such that F has magnitude greater than F ( 0 ) outside the closed ball B(0,r). (Contributed by Mario Carneiro, 14-Sep-2014.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> N e. NN )   &    |- U = if ( if ( 1 <_ s , s , 1 ) <_ T , T , if ( 1 <_ s , s , 1 ) )   &    |- T = ( ( abs ` ( F ` 0 ) ) / ( ( abs ` ( A ` N ) ) / 2 ) )   =>    |- ( ph -> E. r e. RR+ A. x e. CC ( r < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) )
Theorem	ftalem3 20810*	Lemma for fta 20815. There exists a global minimum of the function abs o. F. The proof uses a circle of radius r where r is the value coming from ftalem1 20808; since this is a compact set, the minimum on this disk is achieved, and this must then be the global minimum. (Contributed by Mario Carneiro, 14-Sep-2014.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> N e. NN )   &    |- D = { y e. CC | ( abs ` y ) <_ R }   &    |- J = ( TopOpen ` ℂfld )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> A. x e. CC ( R < ( abs ` x ) -> ( abs ` ( F ` 0 ) ) < ( abs ` ( F ` x ) ) ) )   =>    |- ( ph -> E. z e. CC A. x e. CC ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` x ) ) )
Theorem	ftalem4 20811*	Lemma for fta 20815: Closure of the auxiliary variables for ftalem5 20812. (Contributed by Mario Carneiro, 20-Sep-2014.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ( F ` 0 ) =/= 0 )   &    |- K = sup ( { n e. NN | ( A ` n ) =/= 0 } , RR , `' < )   &    |- T = ( -u ( ( F ` 0 ) / ( A ` K ) ) ^ c ( 1 / K ) )   &    |- U = ( ( abs ` ( F ` 0 ) ) / ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) )   &    |- X = if ( 1 <_ U , 1 , U )   =>    |- ( ph -> ( ( K e. NN /\ ( A ` K ) =/= 0 ) /\ ( T e. CC /\ U e. RR+ /\ X e. RR+ ) ) )
Theorem	ftalem5 20812*	Lemma for fta 20815: Main proof. We have already shifted the minimum found in ftalem3 20810 to zero by a change of variables, and now we show that the minimum value is zero. Expanding in a series about the minimum value, let K be the lowest term in the polynomial that is nonzero, and let T be a K-th root of -u F ( 0 ) / A ( K ). Then an evaluation of F ( T X ) where X is a sufficiently small positive number yields F ( 0 ) for the first term and -u F ( 0 ) x. X ^ K for the K-th term, and all higher terms are bounded because X is small. Thus, abs ( F ( T X ) ) <_ abs ( F ( 0 ) ) ( 1 - X ^ K ) < abs ( F ( 0 ) ), in contradiction to our choice of F ( 0 ) as the minimum. (Contributed by Mario Carneiro, 14-Sep-2014.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ( F ` 0 ) =/= 0 )   &    |- K = sup ( { n e. NN | ( A ` n ) =/= 0 } , RR , `' < )   &    |- T = ( -u ( ( F ` 0 ) / ( A ` K ) ) ^ c ( 1 / K ) )   &    |- U = ( ( abs ` ( F ` 0 ) ) / ( sum_ k e. ( ( K + 1 ) ... N ) ( abs ` ( ( A ` k ) x. ( T ^ k ) ) ) + 1 ) )   &    |- X = if ( 1 <_ U , 1 , U )   =>    |- ( ph -> E. x e. CC ( abs ` ( F ` x ) ) < ( abs ` ( F ` 0 ) ) )
Theorem	ftalem6 20813*	Lemma for fta 20815: Discharge the auxiliary variables in ftalem5 20812. (Contributed by Mario Carneiro, 20-Sep-2014.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ( F ` 0 ) =/= 0 )   =>    |- ( ph -> E. x e. CC ( abs ` ( F ` x ) ) < ( abs ` ( F ` 0 ) ) )
Theorem	ftalem7 20814*	Lemma for fta 20815. Shift the minimum away from zero by a change of variables. (Contributed by Mario Carneiro, 14-Sep-2014.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> X e. CC )   &    |- ( ph -> ( F ` X ) =/= 0 )   =>    |- ( ph -> -. A. x e. CC ( abs ` ( F ` X ) ) <_ ( abs ` ( F ` x ) ) )
Theorem	fta 20815*	The Fundamental Theorem of Algebra. Any polynomial with positive degree (i.e. non-constant) has a root. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ( F e. (Poly ` S ) /\ (deg ` F ) e. NN ) -> E. z e. CC ( F ` z ) = 0 )
13.4.3  The Basel problem (ζ(2) = π2/6)
Theorem	basellem1 20816	Lemma for basel 20825. Closure of the sequence of roots. (Contributed by Mario Carneiro, 30-Jul-2014.)
|- N = ( ( 2 x. M ) + 1 )   =>    |- ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( ( K x. pi ) / N ) e. ( 0 (,) ( pi / 2 ) ) )
Theorem	basellem2 20817*	Lemma for basel 20825. Show that P is a polynomial of degree M, and compute its coefficient function. (Contributed by Mario Carneiro, 30-Jul-2014.)
|- N = ( ( 2 x. M ) + 1 )   &    |- P = ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) )   =>    |- ( M e. NN -> ( P e. (Poly ` CC ) /\ (deg ` P ) = M /\ (coeff ` P ) = ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ) )
Theorem	basellem3 20818*	Lemma for basel 20825. Using the binomial theorem and de Moivre's formula, we have the identity _e ^ _i N x / ( sin x ) ^ n = sum_ m e. ( 0 ... N ) ( N _C m ) ( _i ^ m ) ( cot x ) ^ ( N - m ), so taking imaginary parts yields sin ( N x ) / ( sin x ) ^ N = sum_ j e. ( 0 ... M ) ( N _C 2 j ) ( -u 1 ) ^ ( M - j ) ( cot x ) ^ ( -u 2 j ) = P ( ( cot x ) ^ 2 ), where N = 2 M + 1. (Contributed by Mario Carneiro, 30-Jul-2014.)
|- N = ( ( 2 x. M ) + 1 )   &    |- P = ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) )   =>    |- ( ( M e. NN /\ A e. ( 0 (,) ( pi / 2 ) ) ) -> ( P ` ( ( tan ` A ) ^ -u 2 ) ) = ( ( sin ` ( N x. A ) ) / ( ( sin ` A ) ^ N ) ) )
Theorem	basellem4 20819*	Lemma for basel 20825. By basellem3 20818, the expression P ( ( cot x ) ^ 2 ) = sin ( N x ) / ( sin x ) ^ N goes to zero whenever x = n pi / N for some n e. ( 1 ... M ), so this function enumerates M distinct roots of a degree- M polynomial, which must therefore be all the roots by fta1 20178. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- N = ( ( 2 x. M ) + 1 )   &    |- P = ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) )   &    |- T = ( n e. ( 1 ... M ) |-> ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) )   =>    |- ( M e. NN -> T : ( 1 ... M ) -1-1-onto-> ( `' P " { 0 } ) )
Theorem	basellem5 20820*	Lemma for basel 20825. Using vieta1 20182, we can calculate the sum of the roots of P as the quotient of the top two coefficients, and since the function T enumerates the roots, we are left with an equation that sums the cot ^ 2 function at the M different roots. (Contributed by Mario Carneiro, 29-Jul-2014.)
|- N = ( ( 2 x. M ) + 1 )   &    |- P = ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) )   &    |- T = ( n e. ( 1 ... M ) |-> ( ( tan ` ( ( n x. pi ) / N ) ) ^ -u 2 ) )   =>    |- ( M e. NN -> sum_ k e. ( 1 ... M ) ( ( tan ` ( ( k x. pi ) / N ) ) ^ -u 2 ) = ( ( ( 2 x. M ) x. ( ( 2 x. M ) - 1 ) ) / 6 ) )
Theorem	basellem6 20821	Lemma for basel 20825. The function G goes to zero because it is bounded by 1 / n. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- G = ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) )   =>    |- G ~~> 0
Theorem	basellem7 20822	Lemma for basel 20825. The function 1 + A x. G for any fixed A goes to 1. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- G = ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) )   &    |- A e. CC   =>    |- ( ( NN X. { 1 } ) o F + ( ( NN X. { A } ) o F x. G ) ) ~~> 1
Theorem	basellem8 20823*	Lemma for basel 20825. The function F of partial sums of the inverse squares is bounded below by J and above by K, obtained by summing the inequality cot ^ 2 x <_ 1 / x ^ 2 <_ csc ^ 2 x = cot ^ 2 x + 1 over the M roots of the polynomial P, and applying the identity basellem5 20820. (Contributed by Mario Carneiro, 29-Jul-2014.)
|- G = ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) )   &    |- F = seq 1 ( + , ( n e. NN |-> ( n ^ -u 2 ) ) )   &    |- H = ( ( NN X. { ( ( pi ^ 2 ) / 6 ) } ) o F x. ( ( NN X. { 1 } ) o F - G ) )   &    |- J = ( H o F x. ( ( NN X. { 1 } ) o F + ( ( NN X. { -u 2 } ) o F x. G ) ) )   &    |- K = ( H o F x. ( ( NN X. { 1 } ) o F + G ) )   &    |- N = ( ( 2 x. M ) + 1 )   =>    |- ( M e. NN -> ( ( J ` M ) <_ ( F ` M ) /\ ( F ` M ) <_ ( K ` M ) ) )
Theorem	basellem9 20824*	Lemma for basel 20825. Since by basellem8 20823 F is bounded by two expressions that tend to pi ^ 2 / 6, F must also go to pi ^ 2 / 6 by the squeeze theorem climsqz 12389. But the series F is exactly the partial sums of k ^ -u 2, so it follows that this is also the value of the infinite sum sum_ k e. NN ( k ^ -u 2 ). (Contributed by Mario Carneiro, 28-Jul-2014.)
|- G = ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) )   &    |- F = seq 1 ( + , ( n e. NN |-> ( n ^ -u 2 ) ) )   &    |- H = ( ( NN X. { ( ( pi ^ 2 ) / 6 ) } ) o F x. ( ( NN X. { 1 } ) o F - G ) )   &    |- J = ( H o F x. ( ( NN X. { 1 } ) o F + ( ( NN X. { -u 2 } ) o F x. G ) ) )   &    |- K = ( H o F x. ( ( NN X. { 1 } ) o F + G ) )   =>    |- sum_ k e. NN ( k ^ -u 2 ) = ( ( pi ^ 2 ) / 6 )
Theorem	basel 20825	The sum of the inverse squares is pi ^ 2 / 6. This is commonly known as the Basel problem, with the first known proof attributed to Euler. See http://en.wikipedia.org/wiki/Basel_problem. This particular proof approach is due to Cauchy (1821). (Contributed by Mario Carneiro, 30-Jul-2014.)
|- sum_ k e. NN ( k ^ -u 2 ) = ( ( pi ^ 2 ) / 6 )
13.4.4  Number-theoretical functions
Syntax	ccht 20826	Extend class notation with the first Chebyshev function.
class theta
Syntax	cvma 20827	Extend class notation with the von Mangoldt function.
class Λ
Syntax	cchp 20828	Extend class notation with the second Chebyshev function.
class ψ
Syntax	cppi 20829	Extend class notation with the prime Pi function.
class π
Syntax	cmu 20830	Extend class notation with the Möbius function.
class mmu
Syntax	csgm 20831	Extend class notation with the divisor function.
class sigma
Definition	df-cht 20832*	Define the first Chebyshev function, which adds up the logarithms of all primes less than x. The symbol used to represent this function is sometimes the variant greek letter theta shown here and sometimes the greek letter psi, ψ; however, this notation can also refer to the second Chebyshev function, which adds up the logarithms of prime powers instead. See https://en.wikipedia.org/wiki/Chebyshev_function for a discussion of the two functions. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- theta = ( x e. RR |-> sum_ p e. ( ( 0 [,] x ) i^i Prime ) ( log ` p ) )
Definition	df-vma 20833*	Define the von Mangoldt function, which gives the logarithm of the prime at a prime power, and is zero elsewhere. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- Λ = ( x e. NN |-> [_ { p e. Prime | p || x } / s ]_ if ( ( # ` s ) = 1 , ( log ` U. s ) , 0 ) )
Definition	df-chp 20834*	Define the second Chebyshev function, which adds up the logarithms of the primes corresponding to the prime powers less than x. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ψ = ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) (Λ ` n ) )
Definition	df-ppi 20835	Define the prime π function, which counts the number of primes less than or equal to x. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- π = ( x e. RR |-> ( # ` ( ( 0 [,] x ) i^i Prime ) ) )
Definition	df-mu 20836*	Define the Möbius function, which is zero for non-squarefree numbers and is -u 1 or 1 for squarefree numbers according as to the number of prime divisors of the number is even or odd. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- mmu = ( x e. NN |-> if ( E. p e. Prime ( p ^ 2 ) || x , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || x } ) ) ) )
Definition	df-sgm 20837*	Define the divisor function, which counts the number of divisors of n, to the power x. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- sigma = ( x e. CC , n e. NN |-> sum_ k e. { p e. NN | p || n } ( k ^ c x ) )
Theorem	efnnfsumcl 20838*	Finite sum closure in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   &    |- ( ( ph /\ k e. A ) -> ( exp ` B ) e. NN )   =>    |- ( ph -> ( exp ` sum_ k e. A B ) e. NN )
Theorem	ppisval 20839	The set of primes less than A expressed using a finite set of integers. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) = ( ( 2 ... ( |_ ` A ) ) i^i Prime ) )
Theorem	ppisval2 20840	The set of primes less than A expressed using a finite set of integers. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. RR /\ 2 e. ( ZZ>= ` M ) ) -> ( ( 0 [,] A ) i^i Prime ) = ( ( M ... ( |_ ` A ) ) i^i Prime ) )
Theorem	ppifi 20841	The set of primes less than A is a finite set. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( A e. RR -> ( ( 0 [,] A ) i^i Prime ) e. Fin )
Theorem	sgmss 20842*	The set of divisors of a number is a subset of a finite set. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. NN -> { p e. NN | p || A } C_ ( 1 ... A ) )
Theorem	prmdvdsfi 20843*	The set of prime divisors of a number is a finite set. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. NN -> { p e. Prime | p || A } e. Fin )
Theorem	chtf 20844	Domain and range of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- theta : RR --> RR
Theorem	chtcl 20845	Real closure of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( A e. RR -> ( theta ` A ) e. RR )
Theorem	chtval 20846*	Value of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( A e. RR -> ( theta ` A ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( log ` p ) )
Theorem	efchtcl 20847	The Chebyshev function is closed in the log-integers. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 7-Apr-2016.)
|- ( A e. RR -> ( exp ` ( theta ` A ) ) e. NN )
Theorem	chtge0 20848	The Chebyshev function is always positive. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( A e. RR -> 0 <_ ( theta ` A ) )
Theorem	vmaval 20849*	Value of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- S = { p e. Prime | p || A }   =>    |- ( A e. NN -> (Λ ` A ) = if ( ( # ` S ) = 1 , ( log ` U. S ) , 0 ) )
Theorem	isppw 20850*	Two ways to say that A is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. NN -> ( (Λ ` A ) =/= 0 <-> E! p e. Prime p || A ) )
Theorem	isppw2 20851*	Two ways to say that A is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. NN -> ( (Λ ` A ) =/= 0 <-> E. p e. Prime E. k e. NN A = ( p ^ k ) ) )
Theorem	vmappw 20852	Value of the von Mangoldt function at a prime power. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( ( P e. Prime /\ K e. NN ) -> (Λ ` ( P ^ K ) ) = ( log ` P ) )
Theorem	vmaprm 20853	Value of the von Mangoldt function at a prime. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( P e. Prime -> (Λ ` P ) = ( log ` P ) )
Theorem	vmacl 20854	Closure for the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. NN -> (Λ ` A ) e. RR )
Theorem	vmaf 20855	Functionality of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- Λ : NN --> RR
Theorem	efvmacl 20856	The von Mangoldt is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. NN -> ( exp ` (Λ ` A ) ) e. NN )
Theorem	vmage0 20857	The von Mangoldt function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. NN -> 0 <_ (Λ ` A ) )
Theorem	chpval 20858*	Value of the second Chebyshev function, or summary von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. RR -> (ψ ` A ) = sum_ n e. ( 1 ... ( |_ ` A ) ) (Λ ` n ) )
Theorem	chpf 20859	Functionality of the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ψ : RR --> RR
Theorem	chpcl 20860	Closure for the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. RR -> (ψ ` A ) e. RR )
Theorem	efchpcl 20861	The second Chebyshev function is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. RR -> ( exp ` (ψ ` A ) ) e. NN )
Theorem	chpge0 20862	The second Chebyshev function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. RR -> 0 <_ (ψ ` A ) )
Theorem	ppival 20863	Value of the prime pi function. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( A e. RR -> (π ` A ) = ( # ` ( ( 0 [,] A ) i^i Prime ) ) )
Theorem	ppival2 20864	Value of the prime pi function. (Contributed by Mario Carneiro, 18-Sep-2014.)
|- ( A e. ZZ -> (π ` A ) = ( # ` ( ( 2 ... A ) i^i Prime ) ) )
Theorem	ppival2g 20865	Value of the prime pi function. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. ZZ /\ 2 e. ( ZZ>= ` M ) ) -> (π ` A ) = ( # ` ( ( M ... A ) i^i Prime ) ) )
Theorem	ppif 20866	Domain and range of the prime pi function. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- π : RR --> NN0
Theorem	ppicl 20867	Real closure of the prime pi function. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( A e. RR -> (π ` A ) e. NN0 )
Theorem	muval 20868*	The value of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. NN -> ( mmu ` A ) = if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) )
Theorem	muval1 20869	The value of the Möbius function at a non-squarefree number. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- ( ( A e. NN /\ P e. ( ZZ>= ` 2 ) /\ ( P ^ 2 ) || A ) -> ( mmu ` A ) = 0 )
Theorem	muval2 20870*	The value of the Möbius function at a squarefree number. (Contributed by Mario Carneiro, 3-Oct-2014.)
|- ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) -> ( mmu ` A ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) )
Theorem	isnsqf 20871*	Two ways to say that a number is not squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.)
|- ( A e. NN -> ( ( mmu ` A ) = 0 <-> E. p e. Prime ( p ^ 2 ) || A ) )
Theorem	issqf 20872*	Two ways to say that a number is squarefree. (Contributed by Mario Carneiro, 3-Oct-2014.)
|- ( A e. NN -> ( ( mmu ` A ) =/= 0 <-> A. p e. Prime ( p pCnt A ) <_ 1 ) )
Theorem	sqfpc 20873	The prime count of a squarefree number is at most 1. (Contributed by Mario Carneiro, 1-Jul-2015.)
|- ( ( A e. NN /\ ( mmu ` A ) =/= 0 /\ P e. Prime ) -> ( P pCnt A ) <_ 1 )
Theorem	dvdssqf 20874	A divisor of a squarefree number is squarefree. (Contributed by Mario Carneiro, 1-Jul-2015.)
|- ( ( A e. NN /\ B e. NN /\ B || A ) -> ( ( mmu ` A ) =/= 0 -> ( mmu ` B ) =/= 0 ) )
Theorem	sqf11 20875*	A squarefree number is completely determined by the set of its prime divisors. (Contributed by Mario Carneiro, 1-Jul-2015.)
|- ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) -> ( A = B <-> A. p e. Prime ( p || A <-> p || B ) ) )
Theorem	muf 20876	The Möbius function is a function into the integers. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- mmu : NN --> ZZ
Theorem	mucl 20877	Closure of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. NN -> ( mmu ` A ) e. ZZ )
Theorem	sgmval 20878*	The value of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 21-Jun-2015.)
|- ( ( A e. CC /\ B e. NN ) -> ( A sigma B ) = sum_ k e. { p e. NN | p || B } ( k ^ c A ) )
Theorem	sgmval2 20879*	The value of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- ( ( A e. ZZ /\ B e. NN ) -> ( A sigma B ) = sum_ k e. { p e. NN | p || B } ( k ^ A ) )
Theorem	0sgm 20880*	The value of the sum-of-divisors function, usually denoted σ<SUB>0</SUB>(<i>n</i>). (Contributed by Mario Carneiro, 21-Jun-2015.)
|- ( A e. NN -> ( 0 sigma A ) = ( # ` { p e. NN | p || A } ) )
Theorem	sgmf 20881	The divisor function is a function into the complex numbers. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 21-Jun-2015.)
|- sigma : ( CC X. NN ) --> CC
Theorem	sgmcl 20882	Closure of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. CC /\ B e. NN ) -> ( A sigma B ) e. CC )
Theorem	sgmnncl 20883	Closure of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- ( ( A e. NN0 /\ B e. NN ) -> ( A sigma B ) e. NN )
Theorem	mule1 20884	The Möbius function takes on values in magnitude at most 1. (Together with mucl 20877, this implies that it takes a value in { -u 1 , 0 , 1 } for every natural number.) (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. NN -> ( abs ` ( mmu ` A ) ) <_ 1 )
Theorem	chtfl 20885	The Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. RR -> ( theta ` ( |_ ` A ) ) = ( theta ` A ) )
Theorem	chpfl 20886	The second Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 9-Apr-2016.)
|- ( A e. RR -> (ψ ` ( |_ ` A ) ) = (ψ ` A ) )
Theorem	ppiprm 20887	The prime pi function at a prime. (Contributed by Mario Carneiro, 19-Sep-2014.)
|- ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> (π ` ( A + 1 ) ) = ( (π ` A ) + 1 ) )
Theorem	ppinprm 20888	The prime pi function at a non-prime. (Contributed by Mario Carneiro, 19-Sep-2014.)
|- ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> (π ` ( A + 1 ) ) = (π ` A ) )
Theorem	chtprm 20889	The Chebyshev function at a prime. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> ( theta ` ( A + 1 ) ) = ( ( theta ` A ) + ( log ` ( A + 1 ) ) ) )
Theorem	chtnprm 20890	The Chebyshev function at a non-prime. (Contributed by Mario Carneiro, 19-Sep-2014.)
|- ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> ( theta ` ( A + 1 ) ) = ( theta ` A ) )
Theorem	chpp1 20891	The second Chebyshev function at a successor. (Contributed by Mario Carneiro, 11-Apr-2016.)
|- ( A e. NN0 -> (ψ ` ( A + 1 ) ) = ( (ψ ` A ) + (Λ ` ( A + 1 ) ) ) )
Theorem	chtwordi 20892	The Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( theta ` A ) <_ ( theta ` B ) )
Theorem	chpwordi 20893	The second Chebyshev function is weakly increasing. (Contributed by Mario Carneiro, 9-Apr-2016.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> (ψ ` A ) <_ (ψ ` B ) )
Theorem	chtdif 20894*	The difference of the Chebyshev function at two points sums the logarithms of the primes in an interval. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( N e. ( ZZ>= ` M ) -> ( ( theta ` N ) - ( theta ` M ) ) = sum_ p e. ( ( ( M + 1 ) ... N ) i^i Prime ) ( log ` p ) )
Theorem	efchtdvds 20895	The exponentiated Chebyshev function forms a divisibility chain between any two points. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( exp ` ( theta ` A ) ) || ( exp ` ( theta ` B ) ) )
Theorem	ppifl 20896	The prime pi function does not change off the integers. (Contributed by Mario Carneiro, 18-Sep-2014.)
|- ( A e. RR -> (π ` ( |_ ` A ) ) = (π ` A ) )
Theorem	ppip1le 20897	The prime pi function cannot locally increase faster than the identity function. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- ( A e. RR -> (π ` ( A + 1 ) ) <_ ( (π ` A ) + 1 ) )
Theorem	ppiwordi 20898	The prime pi function is weakly increasing. (Contributed by Mario Carneiro, 19-Sep-2014.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> (π ` A ) <_ (π ` B ) )
Theorem	ppidif 20899	The difference of the prime pi function at two points counts the number of primes in an interval. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- ( N e. ( ZZ>= ` M ) -> ( (π ` N ) - (π ` M ) ) = ( # ` ( ( ( M + 1 ) ... N ) i^i Prime ) ) )
Theorem	ppi1 20900	The prime pi function at 1. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- (π ` 1 ) = 0