P. 249 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24801-24900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ftalem3 24801*	Lemma for fta 24806. 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 24799; 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 24802*	Lemma for fta 24806: Closure of the auxiliary variables for ftalem5 24803. (Contributed by Mario Carneiro, 20-Sep-2014.) (Revised by AV, 28-Sep-2020.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ( F ` 0 ) =/= 0 )   &    |- K = inf ( { 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 24803*	Lemma for fta 24806: Main proof. We have already shifted the minimum found in ftalem3 24801 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.) (Revised by AV, 28-Sep-2020.)
|- A = (coeff ` F )   &    |- N = (deg ` F )   &    |- ( ph -> F e. (Poly ` S ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ( F ` 0 ) =/= 0 )   &    |- K = inf ( { 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 24804*	Lemma for fta 24806: Discharge the auxiliary variables in ftalem5 24803. (Contributed by Mario Carneiro, 20-Sep-2014.) (Proof shortened by AV, 28-Sep-2020.)
|- 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 24805*	Lemma for fta 24806. 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 24806*	The Fundamental Theorem of Algebra. Any polynomial with positive degree (i.e. non-constant) has a root. This is Metamath 100 proof #2. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ( F e. (Poly ` S ) /\ (deg ` F ) e. NN ) -> E. z e. CC ( F ` z ) = 0 )
14.4.3  The Basel problem (ζ(2) = π2/6)
Theorem	basellem1 24807	Lemma for basel 24816. Closure of the sequence of roots. (Contributed by Mario Carneiro, 30-Jul-2014.) Replace OLD theorem. (Revised ba Wolf Lammen, 18-Sep-2020.)
|- N = ( ( 2 x. M ) + 1 )   =>    |- ( ( M e. NN /\ K e. ( 1 ... M ) ) -> ( ( K x. pi ) / N ) e. ( 0 (,) ( pi / 2 ) ) )
Theorem	basellem2 24808*	Lemma for basel 24816. 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 24809*	Lemma for basel 24816. 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 24810*	Lemma for basel 24816. By basellem3 24809, 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 24063. (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 24811*	Lemma for basel 24816. Using vieta1 24067, 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 24812	Lemma for basel 24816. 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 24813	Lemma for basel 24816. 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 } ) oF + ( ( NN X. { A } ) oF x. G ) ) ~~> 1
Theorem	basellem8 24814*	Lemma for basel 24816. 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 24811. (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 ) } ) oF x. ( ( NN X. { 1 } ) oF - G ) )   &    |- J = ( H oF x. ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) )   &    |- K = ( H oF x. ( ( NN X. { 1 } ) oF + G ) )   &    |- N = ( ( 2 x. M ) + 1 )   =>    |- ( M e. NN -> ( ( J ` M ) <_ ( F ` M ) /\ ( F ` M ) <_ ( K ` M ) ) )
Theorem	basellem9 24815*	Lemma for basel 24816. Since by basellem8 24814 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 14371. 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 ) } ) oF x. ( ( NN X. { 1 } ) oF - G ) )   &    |- J = ( H oF x. ( ( NN X. { 1 } ) oF + ( ( NN X. { -u 2 } ) oF x. G ) ) )   &    |- K = ( H oF x. ( ( NN X. { 1 } ) oF + G ) )   =>    |- sum_ k e. NN ( k ^ -u 2 ) = ( ( pi ^ 2 ) / 6 )
Theorem	basel 24816	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). This is Metamath 100 proof #14. (Contributed by Mario Carneiro, 30-Jul-2014.)
|- sum_ k e. NN ( k ^ -u 2 ) = ( ( pi ^ 2 ) / 6 )
14.4.4  Number-theoretical functions
Syntax	ccht 24817	Extend class notation with the first Chebyshev function.
class theta
Syntax	cvma 24818	Extend class notation with the von Mangoldt function.
class Λ
Syntax	cchp 24819	Extend class notation with the second Chebyshev function.
class ψ
Syntax	cppi 24820	Extend class notation with the prime-counting function pi.
class π
Syntax	cmu 24821	Extend class notation with the Möbius function.
class mmu
Syntax	csgm 24822	Extend class notation with the divisor function.
class sigma
Definition	df-cht 24823*	Define the first Chebyshev function, which adds up the logarithms of all primes less than x, see definition in [ApostolNT] p. 75. 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 df-chp 24825. 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 24824*	Define the von Mangoldt function, which gives the logarithm of the prime at a prime power, and is zero elsewhere, see definition in [ApostolNT] p. 32. (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 24825*	Define the second Chebyshev function, which adds up the logarithms of the primes corresponding to the prime powers less than x, see definition in [ApostolNT] p. 75. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ψ = ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) (Λ ` n ) )
Definition	df-ppi 24826	Define the prime π function, which counts the number of primes less than or equal to x, see definition in [ApostolNT] p. 8. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- π = ( x e. RR |-> ( # ` ( ( 0 [,] x ) i^i Prime ) ) )
Definition	df-mu 24827*	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, see definition in [ApostolNT] p. 24. (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 24828*	Define the sum of positive divisors function ( x sigma n ), which is the sum of the xth powers of the positive integer divisors of n, see definition in [ApostolNT] p. 38. For x = 0, ( x sigma n ) counts the number of divisors of n, i.e. ( 0 sigma n ) is the divisor function, see remark in [ApostolNT] p. 38. (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 24829*	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 24830	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 24831	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 24832	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	prmdvdsfi 24833*	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 24834	Domain and range of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- theta : RR --> RR
Theorem	chtcl 24835	Real closure of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( A e. RR -> ( theta ` A ) e. RR )
Theorem	chtval 24836*	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 24837	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 24838	The Chebyshev function is always positive. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( A e. RR -> 0 <_ ( theta ` A ) )
Theorem	vmaval 24839*	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 24840*	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 24841*	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 24842	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 24843	Value of the von Mangoldt function at a prime. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( P e. Prime -> (Λ ` P ) = ( log ` P ) )
Theorem	vmacl 24844	Closure for the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. NN -> (Λ ` A ) e. RR )
Theorem	vmaf 24845	Functionality of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- Λ : NN --> RR
Theorem	efvmacl 24846	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 24847	The von Mangoldt function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. NN -> 0 <_ (Λ ` A ) )
Theorem	chpval 24848*	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 24849	Functionality of the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ψ : RR --> RR
Theorem	chpcl 24850	Closure for the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. RR -> (ψ ` A ) e. RR )
Theorem	efchpcl 24851	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 24852	The second Chebyshev function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016.)
|- ( A e. RR -> 0 <_ (ψ ` A ) )
Theorem	ppival 24853	Value of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( A e. RR -> (π ` A ) = ( # ` ( ( 0 [,] A ) i^i Prime ) ) )
Theorem	ppival2 24854	Value of the prime-counting function pi. (Contributed by Mario Carneiro, 18-Sep-2014.)
|- ( A e. ZZ -> (π ` A ) = ( # ` ( ( 2 ... A ) i^i Prime ) ) )
Theorem	ppival2g 24855	Value of the prime-counting function pi. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. ZZ /\ 2 e. ( ZZ>= ` M ) ) -> (π ` A ) = ( # ` ( ( M ... A ) i^i Prime ) ) )
Theorem	ppif 24856	Domain and range of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- π : RR --> NN0
Theorem	ppicl 24857	Real closure of the prime-counting function pi. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( A e. RR -> (π ` A ) e. NN0 )
Theorem	muval 24858*	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 24859	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 24860*	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 24861*	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 24862*	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 24863	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 24864	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 24865*	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 24866	The Möbius function is a function into the integers. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- mmu : NN --> ZZ
Theorem	mucl 24867	Closure of the Möbius function. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. NN -> ( mmu ` A ) e. ZZ )
Theorem	sgmval 24868*	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 24869*	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 24870*	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 24871	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 24872	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 24873	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 24874	The Möbius function takes on values in magnitude at most 1. (Together with mucl 24867, this implies that it takes a value in { -u 1 , 0 , 1 } for every positive integer.) (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. NN -> ( abs ` ( mmu ` A ) ) <_ 1 )
Theorem	chtfl 24875	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 24876	The second Chebyshev function does not change off the integers. (Contributed by Mario Carneiro, 9-Apr-2016.)
|- ( A e. RR -> (ψ ` ( |_ ` A ) ) = (ψ ` A ) )
Theorem	ppiprm 24877	The prime-counting function π at a prime. (Contributed by Mario Carneiro, 19-Sep-2014.)
|- ( ( A e. ZZ /\ ( A + 1 ) e. Prime ) -> (π ` ( A + 1 ) ) = ( (π ` A ) + 1 ) )
Theorem	ppinprm 24878	The prime-counting function π at a non-prime. (Contributed by Mario Carneiro, 19-Sep-2014.)
|- ( ( A e. ZZ /\ -. ( A + 1 ) e. Prime ) -> (π ` ( A + 1 ) ) = (π ` A ) )
Theorem	chtprm 24879	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 24880	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 24881	The second Chebyshev function at a successor. (Contributed by Mario Carneiro, 11-Apr-2016.)
|- ( A e. NN0 -> (ψ ` ( A + 1 ) ) = ( (ψ ` A ) + (Λ ` ( A + 1 ) ) ) )
Theorem	chtwordi 24882	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 24883	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 24884*	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 24885	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 24886	The prime-counting function π does not change off the integers. (Contributed by Mario Carneiro, 18-Sep-2014.)
|- ( A e. RR -> (π ` ( |_ ` A ) ) = (π ` A ) )
Theorem	ppip1le 24887	The prime-counting 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 24888	The prime-counting function π is weakly increasing. (Contributed by Mario Carneiro, 19-Sep-2014.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> (π ` A ) <_ (π ` B ) )
Theorem	ppidif 24889	The difference of the prime-counting function π at two points counts the number of primes in an interval. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- ( N e. ( ZZ>= ` M ) -> ( (π ` N ) - (π ` M ) ) = ( # ` ( ( ( M + 1 ) ... N ) i^i Prime ) ) )
Theorem	ppi1 24890	The prime-counting function π at 1. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- (π ` 1 ) = 0
Theorem	cht1 24891	The Chebyshev function at 1. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( theta ` 1 ) = 0
Theorem	vma1 24892	The von Mangoldt function at 1. (Contributed by Mario Carneiro, 9-Apr-2016.)
|- (Λ ` 1 ) = 0
Theorem	chp1 24893	The second Chebyshev function at 1. (Contributed by Mario Carneiro, 9-Apr-2016.)
|- (ψ ` 1 ) = 0
Theorem	ppi1i 24894	Inference form of ppiprm 24877. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- M e. NN0   &    |- N = ( M + 1 )   &    |- (π ` M ) = K   &    |- N e. Prime   =>    |- (π ` N ) = ( K + 1 )
Theorem	ppi2i 24895	Inference form of ppinprm 24878. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- M e. NN0   &    |- N = ( M + 1 )   &    |- (π ` M ) = K   &    |- -. N e. Prime   =>    |- (π ` N ) = K
Theorem	ppi2 24896	The prime-counting function π at 2. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- (π ` 2 ) = 1
Theorem	ppi3 24897	The prime-counting function π at 3. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- (π ` 3 ) = 2
Theorem	cht2 24898	The Chebyshev function at 2. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( theta ` 2 ) = ( log ` 2 )
Theorem	cht3 24899	The Chebyshev function at 3. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( theta ` 3 ) = ( log ` 6 )
Theorem	ppinncl 24900	Closure of the prime-counting function π in the positive integers. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- ( ( A e. RR /\ 2 <_ A ) -> (π ` A ) e. NN )