P. 235 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23401-23500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	log2cnv 23401	Using the Taylor series for arctan ( _i / 3 ), produce a rapidly convergent series for log 2. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- F = ( n e. NN0 |-> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) )   =>    |- seq 0 ( + , F ) ~~> ( log ` 2 )
Theorem	log2tlbnd 23402*	Bound the error term in the series of log2cnv 23401. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- ( N e. NN0 -> ( ( log ` 2 ) - sum_ n e. ( 0 ... ( N - 1 ) ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) ) e. ( 0 [,] ( 3 / ( ( 4 x. ( ( 2 x. N ) + 1 ) ) x. ( 9 ^ N ) ) ) ) )
14.3.8  The Birthday Problem
Theorem	log2ublem1 23403	Lemma for log2ub 23406. The proof of log2ub 23406, which is simply the evaluation of log2tlbnd 23402 for N = 4, takes the form of the addition of five fractions and showing this is less than another fraction. We could just perform exact arithmetic on these fractions, get a large rational number, and just multiply everything to verify the claim, but as anyone who uses decimal numbers for this task knows, it is often better to pick a common denominator d (usually a large power of 10) and work with the closest approximations of the form n / d for some integer n instead. It turns out that for our purposes it is sufficient to take d = ( 3 ^ 7 ) x. 5 x. 7, which is also nice because it shares many factors in common with the fractions in question. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. A ) <_ B   &    |- A e. RR   &    |- D e. NN0   &    |- E e. NN   &    |- B e. NN0   &    |- F e. NN0   &    |- C = ( A + ( D / E ) )   &    |- ( B + F ) = G   &    |- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. D ) <_ ( E x. F )   =>    |- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. C ) <_ G
Theorem	log2ublem2 23404*	Lemma for log2ub 23406. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. sum_ n e. ( 0 ... K ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) ) <_ ( 2 x. B )   &    |- B e. NN0   &    |- F e. NN0   &    |- N e. NN0   &    |- ( N - 1 ) = K   &    |- ( B + F ) = G   &    |- M e. NN0   &    |- ( M + N ) = 3   &    |- ( ( 5 x. 7 ) x. ( 9 ^ M ) ) = ( ( ( 2 x. N ) + 1 ) x. F )   =>    |- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. sum_ n e. ( 0 ... N ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) ) <_ ( 2 x. G )
Theorem	log2ublem3 23405	Lemma for log2ub 23406. In decimal, this is a proof that the first four terms of the series for log 2 is less than 5 3 0 5 6 / 7 6 5 4 5. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. sum_ n e. ( 0 ... 3 ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) ) <_ ;;;; 5 3 0 5 6
Theorem	log2ub 23406	log 2 is less than 2 5 3 / 3 6 5. If written in decimal, this is because log 2 = 0.693147... is less than 253/365 = 0.693151... , so this is a very tight bound, at five decimal places. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- ( log ` 2 ) < (;; 2 5 3 / ;; 3 6 5 )
Theorem	birthdaylem1 23407*	Lemma for birthday 23410. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- S = { f | f : ( 1 ... K ) --> ( 1 ... N ) }   &    |- T = { f | f : ( 1 ... K ) -1-1-> ( 1 ... N ) }   =>    |- ( T C_ S /\ S e. Fin /\ ( N e. NN -> S =/= (/) ) )
Theorem	birthdaylem2 23408*	For general N and K, count the fraction of injective functions from 1 ... K to 1 ... N. (Contributed by Mario Carneiro, 7-May-2015.)
|- S = { f | f : ( 1 ... K ) --> ( 1 ... N ) }   &    |- T = { f | f : ( 1 ... K ) -1-1-> ( 1 ... N ) }   =>    |- ( ( N e. NN /\ K e. ( 0 ... N ) ) -> ( ( # ` T ) / ( # ` S ) ) = ( exp ` sum_ k e. ( 0 ... ( K - 1 ) ) ( log ` ( 1 - ( k / N ) ) ) ) )
Theorem	birthdaylem3 23409*	For general N and K, upper-bound the fraction of injective functions from 1 ... K to 1 ... N. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- S = { f | f : ( 1 ... K ) --> ( 1 ... N ) }   &    |- T = { f | f : ( 1 ... K ) -1-1-> ( 1 ... N ) }   =>    |- ( ( K e. NN0 /\ N e. NN ) -> ( ( # ` T ) / ( # ` S ) ) <_ ( exp ` -u ( ( ( ( K ^ 2 ) - K ) / 2 ) / N ) ) )
Theorem	birthday 23410*	The Birthday Problem. There is a more than even chance that out of 23 people in a room, at least two of them have the same birthday. Mathematically, this is asserting that for K = 2 3 and N = 3 6 5, fewer than half of the set of all functions from 1 ... K to 1 ... N are injective. This is Metamath 100 proof #93. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- S = { f | f : ( 1 ... K ) --> ( 1 ... N ) }   &    |- T = { f | f : ( 1 ... K ) -1-1-> ( 1 ... N ) }   &    |- K = ; 2 3   &    |- N = ;; 3 6 5   =>    |- ( ( # ` T ) / ( # ` S ) ) < ( 1 / 2 )
14.3.9  Areas in R^2
Syntax	carea 23411	Area of regions in the complex plane.
class area
Definition	df-area 23412*	Define the area of a subset of RR X. RR. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- area = ( s e. { t e. ~P ( RR X. RR ) | ( A. x e. RR ( t " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( t " { x } ) ) ) e. L^1 ) } |-> S. RR ( vol ` ( s " { x } ) ) _d x )
Theorem	dmarea 23413*	The domain of the area function is the set of finitely measurable subsets of RR X. RR. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- ( A e. dom area <-> ( A C_ ( RR X. RR ) /\ A. x e. RR ( A " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( A " { x } ) ) ) e. L^1 ) )
Theorem	areambl 23414	The fibers of a measurable region are finitely measurable subsets of RR. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- ( ( S e. dom area /\ A e. RR ) -> ( ( S " { A } ) e. dom vol /\ ( vol ` ( S " { A } ) ) e. RR ) )
Theorem	areass 23415	A measurable region is a subset of RR X. RR. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- ( S e. dom area -> S C_ ( RR X. RR ) )
Theorem	dfarea 23416*	Rewrite df-area 23412 self-referentially. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- area = ( s e. dom area |-> S. RR ( vol ` ( s " { x } ) ) _d x )
Theorem	areaf 23417	Area measurement is a function whose values are nonnegative reals. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- area : dom area --> ( 0 [,) +oo )
Theorem	areacl 23418	The area of a measurable region is a real number. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- ( S e. dom area -> (area ` S ) e. RR )
Theorem	areage0 23419	The area of a measurable region is greater than or equal to zero. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- ( S e. dom area -> 0 <_ (area ` S ) )
Theorem	areaval 23420*	The area of a measurable region is greater than or equal to zero. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- ( S e. dom area -> (area ` S ) = S. RR ( vol ` ( S " { x } ) ) _d x )
14.3.10  More miscellaneous converging sequences
Theorem	rlimcnp 23421*	Relate a limit of a real-valued sequence at infinity to the continuity of the function S ( y ) = R ( 1 / y ) at zero. (Contributed by Mario Carneiro, 1-Mar-2015.)
|- ( ph -> A C_ ( 0 [,) +oo ) )   &    |- ( ph -> 0 e. A )   &    |- ( ph -> B C_ RR+ )   &    |- ( ( ph /\ x e. A ) -> R e. CC )   &    |- ( ( ph /\ x e. RR+ ) -> ( x e. A <-> ( 1 / x ) e. B ) )   &    |- ( x = 0 -> R = C )   &    |- ( x = ( 1 / y ) -> R = S )   &    |- J = ( TopOpen ` ℂfld )   &    |- K = ( J ↾t A )   =>    |- ( ph -> ( ( y e. B |-> S ) ~~> r C <-> ( x e. A |-> R ) e. ( ( K CnP J ) ` 0 ) ) )
Theorem	rlimcnp2 23422*	Relate a limit of a real-valued sequence at infinity to the continuity of the function S ( y ) = R ( 1 / y ) at zero. (Contributed by Mario Carneiro, 1-Mar-2015.)
|- ( ph -> A C_ ( 0 [,) +oo ) )   &    |- ( ph -> 0 e. A )   &    |- ( ph -> B C_ RR )   &    |- ( ph -> C e. CC )   &    |- ( ( ph /\ y e. B ) -> S e. CC )   &    |- ( ( ph /\ y e. RR+ ) -> ( y e. B <-> ( 1 / y ) e. A ) )   &    |- ( y = ( 1 / x ) -> S = R )   &    |- J = ( TopOpen ` ℂfld )   &    |- K = ( J ↾t A )   =>    |- ( ph -> ( ( y e. B |-> S ) ~~> r C <-> ( x e. A |-> if ( x = 0 , C , R ) ) e. ( ( K CnP J ) ` 0 ) ) )
Theorem	rlimcnp3 23423*	Relate a limit of a real-valued sequence at infinity to the continuity of the function S ( y ) = R ( 1 / y ) at zero. (Contributed by Mario Carneiro, 1-Mar-2015.)
|- ( ph -> C e. CC )   &    |- ( ( ph /\ y e. RR+ ) -> S e. CC )   &    |- ( y = ( 1 / x ) -> S = R )   &    |- J = ( TopOpen ` ℂfld )   &    |- K = ( J ↾t ( 0 [,) +oo ) )   =>    |- ( ph -> ( ( y e. RR+ |-> S ) ~~> r C <-> ( x e. ( 0 [,) +oo ) |-> if ( x = 0 , C , R ) ) e. ( ( K CnP J ) ` 0 ) ) )
Theorem	xrlimcnp 23424*	Relate a limit of a real-valued sequence at infinity to the continuity of the corresponding extended real function at +oo. Since any ~~> r limit can be written in the form on the left side of the implication, this shows that real limits are a special case of topological continuity at a point. (Contributed by Mario Carneiro, 8-Sep-2015.)
|- ( ph -> A = ( B u. { +oo } ) )   &    |- ( ph -> B C_ RR )   &    |- ( ( ph /\ x e. A ) -> R e. CC )   &    |- ( x = +oo -> R = C )   &    |- J = ( TopOpen ` ℂfld )   &    |- K = ( (ordTop ` <_ ) ↾t A )   =>    |- ( ph -> ( ( x e. B |-> R ) ~~> r C <-> ( x e. A |-> R ) e. ( ( K CnP J ) ` +oo ) ) )
Theorem	efrlim 23425*	The limit of the sequence ( 1 + A / k ) ^ k is the exponential function. This is often taken as an alternate definition of the exponential function (see also dfef2 23426). (Contributed by Mario Carneiro, 1-Mar-2015.)
|- S = ( 0 ( ball ` ( abs o. - ) ) ( 1 / ( ( abs ` A ) + 1 ) ) )   =>    |- ( A e. CC -> ( k e. RR+ |-> ( ( 1 + ( A / k ) ) ^c k ) ) ~~> r ( exp ` A ) )
Theorem	dfef2 23426*	The limit of the sequence ( 1 + A / k ) ^ k as k goes to +oo is ( exp ` A ). This is another common definition of _e. (Contributed by Mario Carneiro, 1-Mar-2015.)
|- ( ph -> F e. V )   &    |- ( ph -> A e. CC )   &    |- ( ( ph /\ k e. NN ) -> ( F ` k ) = ( ( 1 + ( A / k ) ) ^ k ) )   =>    |- ( ph -> F ~~> ( exp ` A ) )
Theorem	cxplim 23427*	A power to a negative exponent goes to zero as the base becomes large. (Contributed by Mario Carneiro, 15-Sep-2014.) (Revised by Mario Carneiro, 18-May-2016.)
|- ( A e. RR+ -> ( n e. RR+ |-> ( 1 / ( n ^c A ) ) ) ~~> r 0 )
Theorem	sqrtlim 23428	The inverse square root function converges to zero. (Contributed by Mario Carneiro, 18-May-2016.)
|- ( n e. RR+ |-> ( 1 / ( sqr ` n ) ) ) ~~> r 0
Theorem	rlimcxp 23429*	Any power to a positive exponent of a converging sequence also converges. (Contributed by Mario Carneiro, 18-Sep-2014.)
|- ( ( ph /\ n e. A ) -> B e. V )   &    |- ( ph -> ( n e. A |-> B ) ~~> r 0 )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( n e. A |-> ( B ^c C ) ) ~~> r 0 )
Theorem	o1cxp 23430*	An eventually bounded function taken to a nonnegative power is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ph -> C e. CC )   &    |- ( ph -> 0 <_ ( Re ` C ) )   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> ( x e. A |-> B ) e. O(1) )   =>    |- ( ph -> ( x e. A |-> ( B ^c C ) ) e. O(1) )
Theorem	cxp2limlem 23431*	A linear factor grows slower than any exponential with base greater than 1. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ( A e. RR /\ 1 < A ) -> ( n e. RR+ |-> ( n / ( A ^c n ) ) ) ~~> r 0 )
Theorem	cxp2lim 23432*	Any power grows slower than any exponential with base greater than 1. (Contributed by Mario Carneiro, 18-Sep-2014.)
|- ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( n e. RR+ |-> ( ( n ^c A ) / ( B ^c n ) ) ) ~~> r 0 )
Theorem	cxploglim 23433*	The logarithm grows slower than any positive power. (Contributed by Mario Carneiro, 18-Sep-2014.)
|- ( A e. RR+ -> ( n e. RR+ |-> ( ( log ` n ) / ( n ^c A ) ) ) ~~> r 0 )
Theorem	cxploglim2 23434*	Every power of the logarithm grows slower than any positive power. (Contributed by Mario Carneiro, 20-May-2016.)
|- ( ( A e. CC /\ B e. RR+ ) -> ( n e. RR+ |-> ( ( ( log ` n ) ^c A ) / ( n ^c B ) ) ) ~~> r 0 )
Theorem	divsqrtsumlem 23435*	Lemma for divsqrsum 23437 and divsqrtsum2 23438. (Contributed by Mario Carneiro, 18-May-2016.)
|- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqr ` n ) ) - ( 2 x. ( sqr ` x ) ) ) )   =>    |- ( F : RR+ --> RR /\ F e. dom ~~> r /\ ( ( F ~~> r L /\ A e. RR+ ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( 1 / ( sqr ` A ) ) ) )
Theorem	divsqrsumf 23436*	The function F used in divsqrsum 23437 is a real function. (Contributed by Mario Carneiro, 12-May-2016.)
|- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqr ` n ) ) - ( 2 x. ( sqr ` x ) ) ) )   =>    |- F : RR+ --> RR
Theorem	divsqrsum 23437*	The sum sum_ n <_ x ( 1 / sqr n ) is asymptotic to 2 sqr x + L with a finite limit L. (In fact, this limit is zeta ( 1 / 2 ) ~~ -u 1 period 4 6 ....) (Contributed by Mario Carneiro, 9-May-2016.)
|- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqr ` n ) ) - ( 2 x. ( sqr ` x ) ) ) )   =>    |- F e. dom ~~> r
Theorem	divsqrtsum2 23438*	A bound on the distance of the sum sum_ n <_ x ( 1 / sqr n ) from its asymptotic value 2 sqr x + L. (Contributed by Mario Carneiro, 18-May-2016.)
|- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqr ` n ) ) - ( 2 x. ( sqr ` x ) ) ) )   &    |- ( ph -> F ~~> r L )   =>    |- ( ( ph /\ A e. RR+ ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( 1 / ( sqr ` A ) ) )
Theorem	divsqrtsumo1 23439*	The sum sum_ n <_ x ( 1 / sqr n ) has the asymptotic expansion 2 sqr x + L + O ( 1 / sqr x ), for some L. (Contributed by Mario Carneiro, 10-May-2016.)
|- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqr ` n ) ) - ( 2 x. ( sqr ` x ) ) ) )   &    |- ( ph -> F ~~> r L )   =>    |- ( ph -> ( y e. RR+ |-> ( ( ( F ` y ) - L ) x. ( sqr ` y ) ) ) e. O(1) )
14.3.11  Inequality of arithmetic and geometric means
Theorem	cvxcl 23440*	Closure of a 0-1 linear combination in a convex set. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- ( ph -> D C_ RR )   &    |- ( ( ph /\ ( x e. D /\ y e. D ) ) -> ( x [,] y ) C_ D )   =>    |- ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) e. D )
Theorem	scvxcvx 23441*	A strictly convex function is convex. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- ( ph -> D C_ RR )   &    |- ( ph -> F : D --> RR )   &    |- ( ( ph /\ ( a e. D /\ b e. D ) ) -> ( a [,] b ) C_ D )   &    |- ( ( ph /\ ( x e. D /\ y e. D /\ x < y ) /\ t e. ( 0 (,) 1 ) ) -> ( F ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) < ( ( t x. ( F ` x ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) )   =>    |- ( ( ph /\ ( X e. D /\ Y e. D /\ T e. ( 0 [,] 1 ) ) ) -> ( F ` ( ( T x. X ) + ( ( 1 - T ) x. Y ) ) ) <_ ( ( T x. ( F ` X ) ) + ( ( 1 - T ) x. ( F ` Y ) ) ) )
Theorem	jensenlem1 23442*	Lemma for jensen 23444. (Contributed by Mario Carneiro, 4-Jun-2016.)
|- ( ph -> D C_ RR )   &    |- ( ph -> F : D --> RR )   &    |- ( ( ph /\ ( a e. D /\ b e. D ) ) -> ( a [,] b ) C_ D )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> T : A --> ( 0 [,) +oo ) )   &    |- ( ph -> X : A --> D )   &    |- ( ph -> 0 < (ℂfld gsumg T ) )   &    |- ( ( ph /\ ( x e. D /\ y e. D /\ t e. ( 0 [,] 1 ) ) ) -> ( F ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) <_ ( ( t x. ( F ` x ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) )   &    |- ( ph -> -. z e. B )   &    |- ( ph -> ( B u. { z } ) C_ A )   &    |- S = (ℂfld gsumg ( T |` B ) )   &    |- L = (ℂfld gsumg ( T |` ( B u. { z } ) ) )   =>    |- ( ph -> L = ( S + ( T ` z ) ) )
Theorem	jensenlem2 23443*	Lemma for jensen 23444. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- ( ph -> D C_ RR )   &    |- ( ph -> F : D --> RR )   &    |- ( ( ph /\ ( a e. D /\ b e. D ) ) -> ( a [,] b ) C_ D )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> T : A --> ( 0 [,) +oo ) )   &    |- ( ph -> X : A --> D )   &    |- ( ph -> 0 < (ℂfld gsumg T ) )   &    |- ( ( ph /\ ( x e. D /\ y e. D /\ t e. ( 0 [,] 1 ) ) ) -> ( F ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) <_ ( ( t x. ( F ` x ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) )   &    |- ( ph -> -. z e. B )   &    |- ( ph -> ( B u. { z } ) C_ A )   &    |- S = (ℂfld gsumg ( T |` B ) )   &    |- L = (ℂfld gsumg ( T |` ( B u. { z } ) ) )   &    |- ( ph -> S e. RR+ )   &    |- ( ph -> ( (ℂfld gsumg ( ( T oF x. X ) |` B ) ) / S ) e. D )   &    |- ( ph -> ( F ` ( (ℂfld gsumg ( ( T oF x. X ) |` B ) ) / S ) ) <_ ( (ℂfld gsumg ( ( T oF x. ( F o. X ) ) |` B ) ) / S ) )   =>    |- ( ph -> ( ( (ℂfld gsumg ( ( T oF x. X ) |` ( B u. { z } ) ) ) / L ) e. D /\ ( F ` ( (ℂfld gsumg ( ( T oF x. X ) |` ( B u. { z } ) ) ) / L ) ) <_ ( (ℂfld gsumg ( ( T oF x. ( F o. X ) ) |` ( B u. { z } ) ) ) / L ) ) )
Theorem	jensen 23444*	Jensen's inequality, a finite extension of the definition of convexity (the last hypothesis). (Contributed by Mario Carneiro, 21-Jun-2015.) (Proof shortened by AV, 27-Jul-2019.)
|- ( ph -> D C_ RR )   &    |- ( ph -> F : D --> RR )   &    |- ( ( ph /\ ( a e. D /\ b e. D ) ) -> ( a [,] b ) C_ D )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> T : A --> ( 0 [,) +oo ) )   &    |- ( ph -> X : A --> D )   &    |- ( ph -> 0 < (ℂfld gsumg T ) )   &    |- ( ( ph /\ ( x e. D /\ y e. D /\ t e. ( 0 [,] 1 ) ) ) -> ( F ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) <_ ( ( t x. ( F ` x ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) )   =>    |- ( ph -> ( ( (ℂfld gsumg ( T oF x. X ) ) / (ℂfld gsumg T ) ) e. D /\ ( F ` ( (ℂfld gsumg ( T oF x. X ) ) / (ℂfld gsumg T ) ) ) <_ ( (ℂfld gsumg ( T oF x. ( F o. X ) ) ) / (ℂfld gsumg T ) ) ) )
Theorem	amgmlem 23445	Lemma for amgm 23446. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- M = (mulGrp ` ℂfld )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> F : A --> RR+ )   =>    |- ( ph -> ( ( M gsumg F ) ^c ( 1 / ( # ` A ) ) ) <_ ( (ℂfld gsumg F ) / ( # ` A ) ) )
Theorem	amgm 23446	Inequality of arithmetic and geometric means. Here ( M gsumg F ) calculates the group sum within the multiplicative monoid of the complex numbers (or in other words, it multiplies the elements F ( x ) , x e. A together), and (ℂfld gsumg F ) calculates the group sum in the additive group (i.e. the sum of the elements). This is Metamath 100 proof #38. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- M = (mulGrp ` ℂfld )   =>    |- ( ( A e. Fin /\ A =/= (/) /\ F : A --> ( 0 [,) +oo ) ) -> ( ( M gsumg F ) ^c ( 1 / ( # ` A ) ) ) <_ ( (ℂfld gsumg F ) / ( # ` A ) ) )
14.3.12  Euler-Mascheroni constant
Syntax	cem 23447	The Euler-Mascheroni constant. (The label abbreviates Euler-Mascheroni.)
class gamma
Definition	df-em 23448	Define the Euler-Mascheroni constant, gamma = 0.577... . This is the limit of the series sum_ k e. ( 1 ... m ) ( 1 / k ) - ( log ` m ), with a proof that the limit exists in emcl 23458. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- gamma = sum_ k e. NN ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) )
Theorem	logdifbnd 23449	Bound on the difference of logs. (Contributed by Mario Carneiro, 23-May-2016.)
|- ( A e. RR+ -> ( ( log ` ( A + 1 ) ) - ( log ` A ) ) <_ ( 1 / A ) )
Theorem	logdiflbnd 23450	Lower bound on the difference of logs. (Contributed by Mario Carneiro, 3-Jul-2017.)
|- ( A e. RR+ -> ( 1 / ( A + 1 ) ) <_ ( ( log ` ( A + 1 ) ) - ( log ` A ) ) )
Theorem	emcllem1 23451*	Lemma for emcl 23458. The series F and G are sequences of real numbers that approach gamma from above and below, respectively. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- F = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) )   &    |- G = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) )   =>    |- ( F : NN --> RR /\ G : NN --> RR )
Theorem	emcllem2 23452*	Lemma for emcl 23458. F is increasing, and G is decreasing. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- F = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) )   &    |- G = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) )   =>    |- ( N e. NN -> ( ( F ` ( N + 1 ) ) <_ ( F ` N ) /\ ( G ` N ) <_ ( G ` ( N + 1 ) ) ) )
Theorem	emcllem3 23453*	Lemma for emcl 23458. The function H is the difference between F and G. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- F = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) )   &    |- G = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) )   &    |- H = ( n e. NN |-> ( log ` ( 1 + ( 1 / n ) ) ) )   =>    |- ( N e. NN -> ( H ` N ) = ( ( F ` N ) - ( G ` N ) ) )
Theorem	emcllem4 23454*	Lemma for emcl 23458. The difference between series F and G tends to zero. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- F = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) )   &    |- G = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) )   &    |- H = ( n e. NN |-> ( log ` ( 1 + ( 1 / n ) ) ) )   =>    |- H ~~> 0
Theorem	emcllem5 23455*	Lemma for emcl 23458. The partial sums of the series T, which is used in the definition df-em 23448, is in fact the same as G. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- F = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) )   &    |- G = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) )   &    |- H = ( n e. NN |-> ( log ` ( 1 + ( 1 / n ) ) ) )   &    |- T = ( n e. NN |-> ( ( 1 / n ) - ( log ` ( 1 + ( 1 / n ) ) ) ) )   =>    |- G = seq 1 ( + , T )
Theorem	emcllem6 23456*	Lemma for emcl 23458. By the previous lemmas, F and G must approach a common limit, which is gamma by definition. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- F = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) )   &    |- G = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) )   &    |- H = ( n e. NN |-> ( log ` ( 1 + ( 1 / n ) ) ) )   &    |- T = ( n e. NN |-> ( ( 1 / n ) - ( log ` ( 1 + ( 1 / n ) ) ) ) )   =>    |- ( F ~~> gamma /\ G ~~> gamma )
Theorem	emcllem7 23457*	Lemma for emcl 23458 and harmonicbnd 23459. Derive bounds on gamma as F ( 1 ) and G ( 1 ). (Contributed by Mario Carneiro, 11-Jul-2014.) (Revised by Mario Carneiro, 9-Apr-2016.)
|- F = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) )   &    |- G = ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` ( n + 1 ) ) ) )   &    |- H = ( n e. NN |-> ( log ` ( 1 + ( 1 / n ) ) ) )   &    |- T = ( n e. NN |-> ( ( 1 / n ) - ( log ` ( 1 + ( 1 / n ) ) ) ) )   =>    |- ( gamma e. ( ( 1 - ( log ` 2 ) ) [,] 1 ) /\ F : NN --> ( gamma [,] 1 ) /\ G : NN --> ( ( 1 - ( log ` 2 ) ) [,] gamma ) )
Theorem	emcl 23458	Closure and bounds for the Euler-Mascheroni constant. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- gamma e. ( ( 1 - ( log ` 2 ) ) [,] 1 )
Theorem	harmonicbnd 23459*	A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 9-Apr-2016.)
|- ( N e. NN -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` N ) ) e. ( gamma [,] 1 ) )
Theorem	harmonicbnd2 23460*	A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- ( N e. NN -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) e. ( ( 1 - ( log ` 2 ) ) [,] gamma ) )
Theorem	emre 23461	The Euler-Mascheroni constant is a real number. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- gamma e. RR
Theorem	emgt0 23462	The Euler-Mascheroni constant is positive. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- 0 < gamma
Theorem	harmonicbnd3 23463*	A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- ( N e. NN0 -> ( sum_ m e. ( 1 ... N ) ( 1 / m ) - ( log ` ( N + 1 ) ) ) e. ( 0 [,] gamma ) )
Theorem	harmoniclbnd 23464*	A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.)
|- ( A e. RR+ -> ( log ` A ) <_ sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) )
Theorem	harmonicubnd 23465*	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 23466*	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 23467*	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 ) ) ) )
14.4  Basic number theory
14.4.1  Wilson's theorem
Theorem	wilthlem1 23468	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 14328, ( 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 23469*	Lemma for wilth 23471: 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 23468 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.) (Proof shortened by AV, 27-Jul-2019.)
|- 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 23470*	Lemma for wilth 23471. Here we round out the argument of wilthlem2 23469 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.) (Proof shortened by AV, 27-Jul-2019.)
|- 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 23471	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 23470 for the forward implication. This is Metamath 100 proof #51. (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 ) ) )
14.4.2  The Fundamental Theorem of Algebra
Theorem	ftalem1 23472*	Lemma for fta 23479: "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 23473*	Lemma for fta 23479. 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 23474*	Lemma for fta 23479. 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 23472; 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 23475*	Lemma for fta 23479: Closure of the auxiliary variables for ftalem5 23476. (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 23476*	Lemma for fta 23479: Main proof. We have already shifted the minimum found in ftalem3 23474 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 23477*	Lemma for fta 23479: Discharge the auxiliary variables in ftalem5 23476. (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 23478*	Lemma for fta 23479. 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 23479*	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 23480	Lemma for basel 23489. 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 23481*	Lemma for basel 23489. 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 23482*	Lemma for basel 23489. 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 23483*	Lemma for basel 23489. By basellem3 23482, 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 22830. (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 23484*	Lemma for basel 23489. Using vieta1 22834, 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 23485	Lemma for basel 23489. 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 23486	Lemma for basel 23489. 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 23487*	Lemma for basel 23489. 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 23484. (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 23488*	Lemma for basel 23489. Since by basellem8 23487 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 13475. 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 23489	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 23490	Extend class notation with the first Chebyshev function.
class theta
Syntax	cvma 23491	Extend class notation with the von Mangoldt function.
class Λ
Syntax	cchp 23492	Extend class notation with the second Chebyshev function.
class ψ
Syntax	cppi 23493	Extend class notation with the prime-counting function pi.
class π
Syntax	cmu 23494	Extend class notation with the Möbius function.
class mmu
Syntax	csgm 23495	Extend class notation with the divisor function.
class sigma
Definition	df-cht 23496*	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 23497*	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 23498*	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 23499	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 23500*	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 } ) ) ) )