P. 240 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23901-24000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tanatan 23901	The arctangent function is an inverse to tan. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. dom arctan -> ( tan ` (arctan ` A ) ) = A )
Theorem	atandmtan 23902	The tangent function has range contained in the domain of the arctangent. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) e. dom arctan )
Theorem	cosatan 23903	The cosine of an arctangent. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( A e. dom arctan -> ( cos ` (arctan ` A ) ) = ( 1 / ( sqr ` ( 1 + ( A ^ 2 ) ) ) ) )
Theorem	cosatanne0 23904	The arctangent function has range contained in the domain of the tangent. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( A e. dom arctan -> ( cos ` (arctan ` A ) ) =/= 0 )
Theorem	atantan 23905	The arctangent function is an inverse to tan. (Contributed by Mario Carneiro, 5-Apr-2015.)
|- ( ( A e. CC /\ ( Re ` A ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) ) -> (arctan ` ( tan ` A ) ) = A )
Theorem	atantanb 23906	Relationship between tangent and arctangent. (Contributed by Mario Carneiro, 5-Apr-2015.)
|- ( ( A e. dom arctan /\ B e. CC /\ ( Re ` B ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) ) -> ( (arctan ` A ) = B <-> ( tan ` B ) = A ) )
Theorem	atanbndlem 23907	Lemma for atanbnd 23908. (Contributed by Mario Carneiro, 5-Apr-2015.)
|- ( A e. RR+ -> (arctan ` A ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) )
Theorem	atanbnd 23908	The arctangent function is bounded by pi / 2 on the reals. (Contributed by Mario Carneiro, 5-Apr-2015.)
|- ( A e. RR -> (arctan ` A ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) )
Theorem	atanord 23909	The arctangent function is strictly increasing. (Contributed by Mario Carneiro, 5-Apr-2015.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> (arctan ` A ) < (arctan ` B ) ) )
Theorem	atan1 23910	The arctangent of 1 is pi / 4. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- (arctan ` 1 ) = ( pi / 4 )
Theorem	bndatandm 23911	A point in the open unit disk is in the domain of the arctangent. (Contributed by Mario Carneiro, 5-Apr-2015.)
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. dom arctan )
Theorem	atans 23912*	The "domain of continuity" of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   &    |- S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }   =>    |- ( A e. S <-> ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. D ) )
Theorem	atans2 23913*	It suffices to show that 1 - _i A and 1 + _i A are in the continuity domain of log to show that A is in the continuity domain of arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   &    |- S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }   =>    |- ( A e. S <-> ( A e. CC /\ ( 1 - ( _i x. A ) ) e. D /\ ( 1 + ( _i x. A ) ) e. D ) )
Theorem	atansopn 23914*	The domain of continuity of the arctangent is an open set. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   &    |- S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }   =>    |- S e. ( TopOpen ` ℂfld )
Theorem	atansssdm 23915*	The domain of continuity of the arctangent is a subset of the actual domain of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   &    |- S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }   =>    |- S C_ dom arctan
Theorem	ressatans 23916*	The real number line is a subset of the domain of continuity of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   &    |- S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }   =>    |- RR C_ S
Theorem	dvatan 23917*	The derivative of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   &    |- S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }   =>    |- ( CC _D (arctan |` S ) ) = ( x e. S |-> ( 1 / ( 1 + ( x ^ 2 ) ) ) )
Theorem	atancn 23918*	The arctangent is a continuous function. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- D = ( CC \ ( -oo (,] 0 ) )   &    |- S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }   =>    |- (arctan |` S ) e. ( S -cn-> CC )
Theorem	atantayl 23919*	The Taylor series for arctan ( A ). (Contributed by Mario Carneiro, 1-Apr-2015.)
|- F = ( n e. NN |-> ( ( ( _i x. ( ( -u _i ^ n ) - ( _i ^ n ) ) ) / 2 ) x. ( ( A ^ n ) / n ) ) )   =>    |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , F ) ~~> (arctan ` A ) )
Theorem	atantayl2 23920*	The Taylor series for arctan ( A ). (Contributed by Mario Carneiro, 1-Apr-2015.)
|- F = ( n e. NN |-> if ( 2 || n , 0 , ( ( -u 1 ^ ( ( n - 1 ) / 2 ) ) x. ( ( A ^ n ) / n ) ) ) )   =>    |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , F ) ~~> (arctan ` A ) )
Theorem	atantayl3 23921*	The Taylor series for arctan ( A ). (Contributed by Mario Carneiro, 7-Apr-2015.)
|- F = ( n e. NN0 |-> ( ( -u 1 ^ n ) x. ( ( A ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) )   =>    |- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , F ) ~~> (arctan ` A ) )
Theorem	leibpilem1 23922	Lemma for leibpi 23924. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- ( ( N e. NN0 /\ ( -. N = 0 /\ -. 2 || N ) ) -> ( N e. NN /\ ( ( N - 1 ) / 2 ) e. NN0 ) )
Theorem	leibpilem2 23923*	The Leibniz formula for pi. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- F = ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) )   &    |- G = ( k e. NN0 |-> if ( ( k = 0 \/ 2 || k ) , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) / k ) ) )   &    |- A e. _V   =>    |- ( seq 0 ( + , F ) ~~> A <-> seq 0 ( + , G ) ~~> A )
Theorem	leibpi 23924	The Leibniz formula for pi. This proof depends on three main facts: (1) the series F is convergent, because it is an alternating series (iseralt 13806). (2) Using leibpilem2 23923 to rewrite the series as a power series, it is the x = 1 special case of the Taylor series for arctan (atantayl2 23920). (3) Although we cannot directly plug x = 1 into atantayl2 23920, Abel's theorem (abelth2 23453) says that the limit along any sequence converging to 1, such as 1 - 1 / n, of the power series converges to the power series extended to 1, and then since arctan is continuous at 1 (atancn 23918) we get the desired result. This is Metamath 100 proof #26. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- F = ( n e. NN0 |-> ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) )   =>    |- seq 0 ( + , F ) ~~> ( pi / 4 )
Theorem	leibpisum 23925	The Leibniz formula for pi. This version of leibpi 23924 looks nicer but does not assert that the series is convergent so is not as practically useful. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- sum_ n e. NN0 ( ( -u 1 ^ n ) / ( ( 2 x. n ) + 1 ) ) = ( pi / 4 )
Theorem	log2cnv 23926	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 23927*	Bound the error term in the series of log2cnv 23926. (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.9  The Birthday Problem
Theorem	log2ublem1 23928	Lemma for log2ub 23931. The proof of log2ub 23931, which is simply the evaluation of log2tlbnd 23927 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 23929*	Lemma for log2ub 23931. (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 23930	Lemma for log2ub 23931. 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 23931	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	log2le1 23932	log 2 is less than 1. This is just a weaker form of log2ub 23931 when no tight upper bound is required. (Contributed by Thierry Arnoux, 27-Sep-2017.)
|- ( log ` 2 ) < 1
Theorem	birthdaylem1 23933*	Lemma for birthday 23936. (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 23934*	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 23935*	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 23936*	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.10  Areas in R^2
Syntax	carea 23937	Area of regions in the complex plane.
class area
Definition	df-area 23938*	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 23939*	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 23940	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 23941	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 23942*	Rewrite df-area 23938 self-referentially. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- area = ( s e. dom area |-> S. RR ( vol ` ( s " { x } ) ) _d x )
Theorem	areaf 23943	Area measurement is a function whose values are nonnegative reals. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- area : dom area --> ( 0 [,) +oo )
Theorem	areacl 23944	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 23945	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 23946*	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.11  More miscellaneous converging sequences
Theorem	rlimcnp 23947*	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 23948*	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 23949*	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 23950*	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 23951*	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 23952). (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 23952*	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 23953*	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 23954	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 23955*	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 23956*	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 23957*	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 23958*	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 23959*	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 23960*	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 23961*	Lemma for divsqrsum 23963 and divsqrtsum2 23964. (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 23962*	The function F used in divsqrsum 23963 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 23963*	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 23964*	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 23965*	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.12  Inequality of arithmetic and geometric means
Theorem	cvxcl 23966*	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 23967*	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 23968*	Lemma for jensen 23970. (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 23969*	Lemma for jensen 23970. (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 23970*	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 23971	Lemma for amgm 23972. (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 23972	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.13  Euler-Mascheroni constant
Syntax	cem 23973	The Euler-Mascheroni constant. (The label abbreviates Euler-Mascheroni.)
class gamma
Definition	df-em 23974	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 23984. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- gamma = sum_ k e. NN ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) )
Theorem	logdifbnd 23975	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 23976	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 23977*	Lemma for emcl 23984. 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 23978*	Lemma for emcl 23984. 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 23979*	Lemma for emcl 23984. 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 23980*	Lemma for emcl 23984. 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 23981*	Lemma for emcl 23984. The partial sums of the series T, which is used in the definition df-em 23974, 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 23982*	Lemma for emcl 23984. 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 23983*	Lemma for emcl 23984 and harmonicbnd 23985. 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 23984	Closure and bounds for the Euler-Mascheroni constant. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- gamma e. ( ( 1 - ( log ` 2 ) ) [,] 1 )
Theorem	harmonicbnd 23985*	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 23986*	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 23987	The Euler-Mascheroni constant is a real number. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- gamma e. RR
Theorem	emgt0 23988	The Euler-Mascheroni constant is positive. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- 0 < gamma
Theorem	harmonicbnd3 23989*	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 23990*	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 23991*	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 23992*	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 23993*	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.3.14  Zeta function
Syntax	czeta 23994	The Riemann zeta function.
class zeta
Definition	df-zeta 23995*	Define the Riemann zeta function. This definition uses a series expansion of the alternating zeta function ~? zetaalt that is convergent everywhere except 1, but going from the alternating zeta function to the regular zeta function requires dividing by 1 - 2 ^ ( 1 - s ), which has zeroes other than 1. To extract the correct value of the zeta function at these points, we extend the divided alternating zeta function by continuity. (Contributed by Mario Carneiro, 18-Jul-2014.)
|- zeta = ( iota_ f e. ( ( CC \ { 1 } ) -cn-> CC ) A. s e. ( CC \ { 1 } ) ( ( 1 - ( 2 ^c ( 1 - s ) ) ) x. ( f ` s ) ) = sum_ n e. NN0 ( sum_ k e. ( 0 ... n ) ( ( ( -u 1 ^ k ) x. ( n _C k ) ) x. ( ( k + 1 ) ^c s ) ) / ( 2 ^ ( n + 1 ) ) ) )
Theorem	zetacvg 23996*	The zeta series is convergent. (Contributed by Mario Carneiro, 18-Jul-2014.)
|- ( ph -> S e. CC )   &    |- ( ph -> 1 < ( Re ` S ) )   &    |- ( ( ph /\ k e. NN ) -> ( F ` k ) = ( k ^c -u S ) )   =>    |- ( ph -> seq 1 ( + , F ) e. dom ~~> )
14.3.15  Gamma function
Syntax	clgam 23997	Logarithm of the Gamma function.
class log _G
Syntax	cgam 23998	The Gamma function.
class _G
Syntax	cigam 23999	The inverse Gamma function.
class 1/ _G
Definition	df-lgam 24000*	Define the log-Gamma function. We can work with this form of the gamma function a bit easier than the equivalent expression for the gamma function itself, and moreover this function is not actually equal to log ( _G ( x ) ) because the branch cuts are placed differently (we do have exp ( log _G ( x ) ) = _G ( x ), though). This definition is attributed to Euler, and unlike the usual integral definition is defined on the entire complex plane except the nonpositive integers ZZ \ NN, where the function has simple poles. (Contributed by Mario Carneiro, 12-Jul-2014.)
|- log _G = ( z e. ( CC \ ( ZZ \ NN ) ) |-> ( sum_ m e. NN ( ( z x. ( log ` ( ( m + 1 ) / m ) ) ) - ( log ` ( ( z / m ) + 1 ) ) ) - ( log ` z ) ) )