P. 233 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23201-23300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	asinsin 23201	The arcsine function composed with sin is equal to the identity. This plus sinasin 23198 allow us to view sin and arcsin as inverse operations to each other. For ease of use, we have not defined precisely the correct domain of correctness of this identity; in addition to the main region described here it is also true for some points on the branch cuts, namely when A = ( pi / 2 ) - _i y for nonnegative real y and also symmetrically at A = _i y - ( pi / 2 ). In particular, when restricted to reals this identity extends to the closed interval [ -u ( pi / 2 ) , ( pi / 2 ) ], not just the open interval (see reasinsin 23205). (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ( A e. CC /\ ( Re ` A ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) ) -> (arcsin ` ( sin ` A ) ) = A )
Theorem	acoscos 23202	The arccosine function is an inverse to cos. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) pi ) ) -> (arccos ` ( cos ` A ) ) = A )
Theorem	asin1 23203	The arcsine of 1 is pi / 2. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- (arcsin ` 1 ) = ( pi / 2 )
Theorem	acos1 23204	The arcsine of 1 is pi / 2. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- (arccos ` 1 ) = 0
Theorem	reasinsin 23205	The arcsine function composed with sin is equal to the identity. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. ( -u ( pi / 2 ) [,] ( pi / 2 ) ) -> (arcsin ` ( sin ` A ) ) = A )
Theorem	asinsinb 23206	Relationship between sine and arcsine. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ( A e. CC /\ B e. CC /\ ( Re ` B ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) ) -> ( (arcsin ` A ) = B <-> ( sin ` B ) = A ) )
Theorem	acoscosb 23207	Relationship between sine and arcsine. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ( A e. CC /\ B e. CC /\ ( Re ` B ) e. ( 0 (,) pi ) ) -> ( (arccos ` A ) = B <-> ( cos ` B ) = A ) )
Theorem	asinbnd 23208	The arcsine function has range within a vertical strip of the complex plane with real part between -u pi / 2 and pi / 2. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. CC -> ( Re ` (arcsin ` A ) ) e. ( -u ( pi / 2 ) [,] ( pi / 2 ) ) )
Theorem	acosbnd 23209	The arccosine function has range within a vertical strip of the complex plane with real part between 0 and pi. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. CC -> ( Re ` (arccos ` A ) ) e. ( 0 [,] pi ) )
Theorem	asinrebnd 23210	Bounds on the arcsine function. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. ( -u 1 [,] 1 ) -> (arcsin ` A ) e. ( -u ( pi / 2 ) [,] ( pi / 2 ) ) )
Theorem	asinrecl 23211	The arcsine function is real in its principal domain. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. ( -u 1 [,] 1 ) -> (arcsin ` A ) e. RR )
Theorem	acosrecl 23212	The arccosine function is real in its principal domain. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. ( -u 1 [,] 1 ) -> (arccos ` A ) e. RR )
Theorem	cosasin 23213	The cosine of the arcsine of A is sqr ( 1 - A ^ 2 ). (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. CC -> ( cos ` (arcsin ` A ) ) = ( sqr ` ( 1 - ( A ^ 2 ) ) ) )
Theorem	sinacos 23214	The sine of the arccosine of A is sqr ( 1 - A ^ 2 ). (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. CC -> ( sin ` (arccos ` A ) ) = ( sqr ` ( 1 - ( A ^ 2 ) ) ) )
Theorem	atandmneg 23215	The domain of the arctangent function is closed under negatives. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( A e. dom arctan -> -u A e. dom arctan )
Theorem	atanneg 23216	The arctangent function is odd. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( A e. dom arctan -> (arctan ` -u A ) = -u (arctan ` A ) )
Theorem	atan0 23217	The arctangent of zero is zero. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- (arctan ` 0 ) = 0
Theorem	atandmcj 23218	The arctangent function distributes under conjugation. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. dom arctan -> ( * ` A ) e. dom arctan )
Theorem	atancj 23219	The arctangent function distributes under conjugation. (The condition that Re ( A ) =/= 0 is necessary because the branch cuts are chosen so that the negative imaginary line "agrees with" neighboring values with negative real part, while the positive imaginary line agrees with values with positive real part. This makes atanneg 23216 true unconditionally but messes up conjugation symmetry, and it is impossible to have both in a single-valued function. The claim is true on the imaginary line between -u 1 and 1, though.) (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( A e. dom arctan /\ ( * ` (arctan ` A ) ) = (arctan ` ( * ` A ) ) ) )
Theorem	atanrecl 23220	The arctangent function is real for all real inputs. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. RR -> (arctan ` A ) e. RR )
Theorem	efiatan 23221	Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. dom arctan -> ( exp ` ( _i x. (arctan ` A ) ) ) = ( ( sqr ` ( 1 + ( _i x. A ) ) ) / ( sqr ` ( 1 - ( _i x. A ) ) ) ) )
Theorem	atanlogaddlem 23222	Lemma for atanlogadd 23223. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( ( A e. dom arctan /\ 0 <_ ( Re ` A ) ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )
Theorem	atanlogadd 23223	The rule sqr ( z w ) = ( sqr z ) ( sqr w ) is not always true on the complex numbers, but it is true when the arguments of z and w sum to within the interval ( -u pi , pi ], so there are some cases such as this one with z = 1 + _i A and w = 1 - _i A which are true unconditionally. This result can also be stated as " sqr ( 1 + z ) + sqr ( 1 - z ) is analytic". (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( A e. dom arctan -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )
Theorem	atanlogsublem 23224	Lemma for atanlogsub 23225. (Contributed by Mario Carneiro, 4-Apr-2015.)
|- ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. ( -u pi (,) pi ) )
Theorem	atanlogsub 23225	A variation on atanlogadd 23223, to show that sqr ( 1 + _i z ) / sqr ( 1 - _i z ) = sqr ( ( 1 + _i z ) / ( 1 - _i z ) ) under more limited conditions. (Contributed by Mario Carneiro, 4-Apr-2015.)
|- ( ( A e. dom arctan /\ ( Re ` A ) =/= 0 ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )
Theorem	efiatan2 23226	Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( A e. dom arctan -> ( exp ` ( _i x. (arctan ` A ) ) ) = ( ( 1 + ( _i x. A ) ) / ( sqr ` ( 1 + ( A ^ 2 ) ) ) ) )
Theorem	2efiatan 23227	Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. dom arctan -> ( exp ` ( 2 x. ( _i x. (arctan ` A ) ) ) ) = ( ( ( 2 x. _i ) / ( A + _i ) ) - 1 ) )
Theorem	tanatan 23228	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 23229	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 23230	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 23231	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 23232	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 23233	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 23234	Lemma for atanbnd 23235. (Contributed by Mario Carneiro, 5-Apr-2015.)
|- ( A e. RR+ -> (arctan ` A ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) )
Theorem	atanbnd 23235	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 23236	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 23237	The arctangent of 1 is pi / 4. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- (arctan ` 1 ) = ( pi / 4 )
Theorem	bndatandm 23238	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 23239*	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 23240*	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 23241*	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 23242*	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 23243*	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 23244*	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 23245*	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 23246*	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 23247*	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 23248*	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 23249	Lemma for leibpi 23251. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- ( ( N e. NN0 /\ ( -. N = 0 /\ -. 2 || N ) ) -> ( N e. NN /\ ( ( N - 1 ) / 2 ) e. NN0 ) )
Theorem	leibpilem2 23250*	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 23251	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 13489). (2) Using leibpilem2 23250 to rewrite the series as a power series, it is the x = 1 special case of the Taylor series for arctan (atantayl2 23247). (3) Although we cannot directly plug x = 1 into atantayl2 23247, Abel's theorem (abelth2 22815) 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 23245) 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 23252	The Leibniz formula for pi. This version of leibpi 23251 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 23253	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 23254*	Bound the error term in the series of log2cnv 23253. (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 23255	Lemma for log2ub 23258. The proof of log2ub 23258, which is simply the evaluation of log2tlbnd 23254 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 23256*	Lemma for log2ub 23258. (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 23257	Lemma for log2ub 23258. 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 23258	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 23259*	Lemma for birthday 23262. (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 23260*	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 23261*	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 23262*	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 23263	Area of regions in the complex plane.
class area
Definition	df-area 23264*	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 23265*	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 23266	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 23267	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 23268*	Rewrite df-area 23264 self-referentially. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- area = ( s e. dom area |-> S. RR ( vol ` ( s " { x } ) ) _d x )
Theorem	areaf 23269	Area measurement is a function whose values are nonnegative reals. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- area : dom area --> ( 0 [,) +oo )
Theorem	areacl 23270	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 23271	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 23272*	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 23273*	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 23274*	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 23275*	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 23276*	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 23277*	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 23278). (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 23278*	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 23279*	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 23280	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 23281*	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 23282*	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 23283*	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 23284*	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 23285*	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 23286*	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 23287*	Lemma for divsqrsum 23289 and divsqrtsum2 23290. (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 23288*	The function F used in divsqrsum 23289 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 23289*	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 23290*	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 23291*	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 23292*	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 23293*	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 23294*	Lemma for jensen 23296. (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 23295*	Lemma for jensen 23296. (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 23296*	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 23297	Lemma for amgm 23298. (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 23298	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 23299	The Euler-Mascheroni constant. (The label abbreviates Euler-Mascheroni.)
class gamma
Definition	df-em 23300	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 23310. (Contributed by Mario Carneiro, 11-Jul-2014.)
|- gamma = sum_ k e. NN ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) )