P. 247 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24601-24700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	acosf 24601	Domain and range of the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- arccos : CC --> CC
Theorem	acoscl 24602	Closure for the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. CC -> (arccos ` A ) e. CC )
Theorem	atandm 24603	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 24604	This form of atandm 24603 is a bit more useful for showing that the logarithms in df-atan 24594 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 24605	A compact form of atandm 24603. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. dom arctan <-> ( A e. CC /\ ( A ^ 2 ) =/= -u 1 ) )
Theorem	atandm4 24606	A compact form of atandm 24603. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( A e. dom arctan <-> ( A e. CC /\ ( 1 + ( A ^ 2 ) ) =/= 0 ) )
Theorem	atanf 24607	Domain and range of the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- arctan : ( CC \ { -u _i , _i } ) --> CC
Theorem	atancl 24608	Closure for the arctan function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. dom arctan -> (arctan ` A ) e. CC )
Theorem	asinval 24609	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 24610	Value of the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. CC -> (arccos ` A ) = ( ( pi / 2 ) - (arcsin ` A ) ) )
Theorem	atanval 24611	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 24612	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 24613	The arcsine function is odd. (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( A e. CC -> (arcsin ` -u A ) = -u (arcsin ` A ) )
Theorem	acosneg 24614	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 24615	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 24616	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 24619 is only true under limited circumstances. (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( A e. CC -> ( sin ` (arcsin ` A ) ) = A )
Theorem	cosacos 24617	The arccosine function is an inverse to cos. (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( A e. CC -> ( cos ` (arccos ` A ) ) = A )
Theorem	asinsinlem 24618	Lemma for asinsin 24619. (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 24619	The arcsine function composed with sin is equal to the identity. This plus sinasin 24616 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 24623). (Contributed by Mario Carneiro, 2-Apr-2015.)
|- ( ( A e. CC /\ ( Re ` A ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) ) -> (arcsin ` ( sin ` A ) ) = A )
Theorem	acoscos 24620	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 24621	The arcsine of 1 is pi / 2. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- (arcsin ` 1 ) = ( pi / 2 )
Theorem	acos1 24622	The arcsine of 1 is pi / 2. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- (arccos ` 1 ) = 0
Theorem	reasinsin 24623	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 24624	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 24625	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 24626	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 24627	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 24628	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 24629	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 24630	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 24631	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 24632	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 24633	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 24634	The arctangent function is odd. (Contributed by Mario Carneiro, 3-Apr-2015.)
|- ( A e. dom arctan -> (arctan ` -u A ) = -u (arctan ` A ) )
Theorem	atan0 24635	The arctangent of zero is zero. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- (arctan ` 0 ) = 0
Theorem	atandmcj 24636	The arctangent function distributes under conjugation. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( A e. dom arctan -> ( * ` A ) e. dom arctan )
Theorem	atancj 24637	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 24634 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 24638	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 24639	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 24640	Lemma for atanlogadd 24641. (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 24641	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 24642	Lemma for atanlogsub 24643. (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 24643	A variation on atanlogadd 24641, 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 24644	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 24645	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 24646	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 24647	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 24648	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 24649	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 24650	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 24651	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 24652	Lemma for atanbnd 24653. (Contributed by Mario Carneiro, 5-Apr-2015.)
|- ( A e. RR+ -> (arctan ` A ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) )
Theorem	atanbnd 24653	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 24654	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 24655	The arctangent of 1 is pi / 4. (Contributed by Mario Carneiro, 2-Apr-2015.)
|- (arctan ` 1 ) = ( pi / 4 )
Theorem	bndatandm 24656	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 24657*	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 24658*	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 24659*	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 24660*	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 24661*	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 24662*	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 24663*	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 24664*	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 24665*	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 24666*	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 24667	Lemma for leibpi 24669. (Contributed by Mario Carneiro, 7-Apr-2015.)
|- ( ( N e. NN0 /\ ( -. N = 0 /\ -. 2 || N ) ) -> ( N e. NN /\ ( ( N - 1 ) / 2 ) e. NN0 ) )
Theorem	leibpilem2 24668*	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 24669	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 14415). (2) Using leibpilem2 24668 to rewrite the series as a power series, it is the x = 1 special case of the Taylor series for arctan (atantayl2 24665). (3) Although we cannot directly plug x = 1 into atantayl2 24665, Abel's theorem (abelth2 24196) 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 24663) 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 24670	The Leibniz formula for pi. This version of leibpi 24669 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 24671	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 24672*	Bound the error term in the series of log2cnv 24671. (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 24673	Lemma for log2ub 24676. The proof of log2ub 24676, which is simply the evaluation of log2tlbnd 24672 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 1 0) 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 24674*	Lemma for log2ub 24676. (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 24675	Lemma for log2ub 24676. 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.) (Proof shortened by AV, 15-Sep-2021.)
|- ( ( ( 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 24676	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.) (Proof shortened by AV, 16-Sep-2021.)
|- ( log ` 2 ) < (;; 2 5 3 / ;; 3 6 5 )
Theorem	log2le1 24677	log 2 is less than 1. This is just a weaker form of log2ub 24676 when no tight upper bound is required. (Contributed by Thierry Arnoux, 27-Sep-2017.)
|- ( log ` 2 ) < 1
Theorem	birthdaylem1 24678*	Lemma for birthday 24681. (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 24679*	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 24680*	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 24681*	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 24682	Area of regions in the complex plane.
class area
Definition	df-area 24683*	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 24684*	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 24685	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 24686	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 24687*	Rewrite df-area 24683 self-referentially. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- area = ( s e. dom area |-> S. RR ( vol ` ( s " { x } ) ) _d x )
Theorem	areaf 24688	Area measurement is a function whose values are nonnegative reals. (Contributed by Mario Carneiro, 21-Jun-2015.)
|- area : dom area --> ( 0 [,) +oo )
Theorem	areacl 24689	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 24690	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 24691*	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 24692*	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 24693*	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 24694*	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 24695*	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 24696*	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 24697). (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 24697*	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 24698*	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 24699	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 24700*	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 )