P. 239 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23801-23900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	atandm 23801	Since the property is a little lengthy, we abbreviate A e. CC /\ A =/= -u _i /\ A =/= _i as A e. dom arctan. This is the necessary precondition for the definition of arctan to make sense. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. dom arctan <-> ( A e. CC /\ A =/= -u _i /\ A =/= _i ) )
Theorem	atandm2 23802	This form of atandm 23801 is a bit more useful for showing that the logarithms in df-atan 23792 are well-defined. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. dom arctan <-> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) )
Theorem	atandm3 23803	A compact form of atandm 23801. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. dom arctan <-> ( A e. CC /\ ( A ^ 2 ) =/= -u 1 ) )
Theorem	atandm4 23804	A compact form of atandm 23801. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( A e. dom arctan <-> ( A e. CC /\ ( 1 + ( A ^ 2 ) ) =/= 0 ) )
Theorem	atanf 23805	Domain and range of the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- arctan : ( CC \ { -u _i , _i } ) --> CC
Theorem	atancl 23806	Closure for the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. dom arctan -> (arctan ` A ) e. CC )
Theorem	asinval 23807	Value of the arcsin function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. CC -> (arcsin ` A ) = ( -u _i x. ( log ` ( ( _i x. A ) + ( sqr ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
Theorem	acosval 23808	Value of the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. CC -> (arccos ` A ) = ( ( pi / 2 ) - (arcsin ` A ) ) )
Theorem	atanval 23809	Value of the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. dom arctan -> (arctan ` A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
Theorem	atanre 23810	A real number is in the domain of the arctangent function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. RR -> A e. dom arctan )
Theorem	asinneg 23811	The arcsine function is odd. (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( A e. CC -> (arcsin ` -u A ) = -u (arcsin ` A ) )
Theorem	acosneg 23812	The negative symmetry relation of the arccosine. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( A e. CC -> (arccos ` -u A ) = ( pi - (arccos ` A ) ) )
Theorem	efiasin 23813	The exponential of the arcsine function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. CC -> ( exp ` ( _i x. (arcsin ` A ) ) ) = ( ( _i x. A ) + ( sqr ` ( 1 - ( A ^ 2 ) ) ) ) )
Theorem	sinasin 23814	The arcsine function is an inverse to sin. This is the main property that justifies the notation arcsin or sin ^ -u 1. Because sin is not an injection, the other converse identity asinsin 23817 is only true under limited circumstances. (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( A e. CC -> ( sin ` (arcsin ` A ) ) = A )
Theorem	cosacos 23815	The arccosine function is an inverse to cos. (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( A e. CC -> ( cos ` (arccos ` A ) ) = A )
Theorem	asinsinlem 23816	Lemma for asinsin 23817. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ( A e. CC /\ ( Re ` A ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) ) -> 0 < ( Re ` ( exp ` ( _i x. A ) ) ) )
Theorem	asinsin 23817	The arcsine function composed with sin is equal to the identity. This plus sinasin 23814 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 23821). (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ( A e. CC /\ ( Re ` A ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) ) -> (arcsin ` ( sin ` A ) ) = A )
Theorem	acoscos 23818	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 23819	The arcsine of 1 is pi / 2. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- (arcsin ` 1 ) = ( pi / 2 )
Theorem	acos1 23820	The arcsine of 1 is pi / 2. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- (arccos ` 1 ) = 0
Theorem	reasinsin 23821	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 23822	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 23823	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 23824	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 23825	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 23826	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 23827	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 23828	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 23829	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 23830	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 23831	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 23832	The arctangent function is odd. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( A e. dom arctan -> (arctan ` -u A ) = -u (arctan ` A ) )
Theorem	atan0 23833	The arctangent of zero is zero. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- (arctan ` 0 ) = 0
Theorem	atandmcj 23834	The arctangent function distributes under conjugation. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. dom arctan -> ( * ` A ) e. dom arctan )
Theorem	atancj 23835	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 23832 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 23836	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 23837	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 23838	Lemma for atanlogadd 23839. (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 23839	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 23840	Lemma for atanlogsub 23841. (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 23841	A variation on atanlogadd 23839, 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 23842	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 23843	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 23844	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 23845	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 23846	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 23847	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 23848	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 23849	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 23850	Lemma for atanbnd 23851. (Contributed by Mario Carneiro, 5-Apr-2015.)
|- ( A e. RR+ -> (arctan ` A ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) )
Theorem	atanbnd 23851	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 23852	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 23853	The arctangent of 1 is pi / 4. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- (arctan ` 1 ) = ( pi / 4 )
Theorem	bndatandm 23854	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 23855*	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 23856*	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 23857*	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 23858*	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 23859*	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 23860*	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 23861*	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 23862*	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 23863*	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 23864*	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 23865	Lemma for leibpi 23867. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- ( ( N e. NN0 /\ ( -. N = 0 /\ -. 2 || N ) ) -> ( N e. NN /\ ( ( N - 1 ) / 2 ) e. NN0 ) )
Theorem	leibpilem2 23866*	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 23867	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 13751). (2) Using leibpilem2 23866 to rewrite the series as a power series, it is the x = 1 special case of the Taylor series for arctan (atantayl2 23863). (3) Although we cannot directly plug x = 1 into atantayl2 23863, Abel's theorem (abelth2 23396) 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 23861) 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 23868	The Leibniz formula for pi. This version of leibpi 23867 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 23869	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 23870*	Bound the error term in the series of log2cnv 23869. (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 23871	Lemma for log2ub 23874. The proof of log2ub 23874, which is simply the evaluation of log2tlbnd 23870 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 23872*	Lemma for log2ub 23874. (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 23873	Lemma for log2ub 23874. 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 23874	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 23875	log 2 is less than 1. This is just a weaker form of log2ub 23874 when no tight upper bound is required. (Contributed by Thierry Arnoux, 27-Sep-2017.)
|- ( log ` 2 ) < 1
Theorem	birthdaylem1 23876*	Lemma for birthday 23879. (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 23877*	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 23878*	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 23879*	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 23880	Area of regions in the complex plane.
class area
Definition	df-area 23881*	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 23882*	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 23883	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 23884	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 23885*	Rewrite df-area 23881 self-referentially. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- area = ( s e. dom area |-> S. RR ( vol ` ( s " { x } ) ) _d x )
Theorem	areaf 23886	Area measurement is a function whose values are nonnegative reals. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- area : dom area --> ( 0 [,) +oo )
Theorem	areacl 23887	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 23888	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 23889*	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 23890*	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 23891*	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 23892*	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 23893*	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 23894*	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 23895). (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 23895*	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 23896*	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 23897	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 23898*	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 23899*	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 23900*	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 )