Home | Metamath
Proof Explorer Theorem List (p. 272 of 323) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-21606) |
Hilbert Space Explorer
(21607-23129) |
Users' Mathboxes
(23130-32206) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | stoweidlem29 27101* | When the hypothesis for the extreme value theorem hold, then the inf of the range of the function belongs to the range, it is real and it a lower bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem30 27102* | This lemma is used to prove the existence of a function p as in Lemma 1 [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_{(t}_0) = 0, and p > 0 on T - U. Z is used for t_{0}, P is used for p, is used for p_{(t}_i). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem31 27103* | This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91: assuming that is a finite subset of , indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all ranging in the finite indexing set, 0 ≤ x_{i} ≤ 1, x_{i} < ε / m on V(t_{i}), and x_{i} > 1 - ε / m on . Here M is used to represent m in the paper, is used to represent ε in the paper, v_{i} is used to represent V(t_{i}). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem32 27104* | If a set A of real functions from a common domain T is a subalgebra and it contains constants, then it is closed under the sum of a finite number of functions, indexed by G and finally scaled by a real Y. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem33 27105* | If a set of real functions from a common domain is closed under addition, multiplication and it contains constants, then it is closed under subtraction. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem34 27106* | This lemma proves that for all in there is a as in the proof of [BrosowskiDeutsh] p. 91 (at the bottom of page 91 and at the top of page 92): (j-4/3) * ε < f(t) <= (j-1/3) * ε , g(t) < (j+1/3) * ε, and g(t) > (j-4/3) * ε. Here is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem35 27107* | This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_{(t}_0) = 0, and p > 0 on T - U. Here is used to represent p_{(t}_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem36 27108* | This lemma is used to prove the existence of a function p_{t} as in Lemma 1 of [BrosowskiDeutsh] p. 90 (at the beginning of Lemma 1): for all t in T - U, there exists a function p in the subalgebra, such that p_{t} ( t_{0} ) = 0 , p_{t} ( t ) > 0, and 0 <= p_{t} <= 1. Z is used for t_{0} , S is used for t e. T - U , h is used for p_{t} . G is used for (h_{t})^2 and the final h is a normalized version of G ( divided by its norm, see the variable N ). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem37 27109* | This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_{(t}_0) = 0, and p > 0 on T - U. Z is used for t_{0}, P is used for p, is used for p_{(t}_i). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem38 27110* | This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_{(t}_0) = 0, and p > 0 on T - U. Z is used for t_{0}, P is used for p, is used for p_{(t}_i). (Contributed by GlaucoSiliprandi, 20-Apr-2017.) |
Theorem | stoweidlem39 27111* | This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91: assuming that is a finite subset of , indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all i ranging in the finite indexing set, 0 ≤ x_{i} ≤ 1, x_{i} < ε / m on V(t_{i}), and x_{i} > 1 - ε / m on . Here is used to represent A in the paper's Lemma 2 (because is used for the subalgebra), is used to represent m in the paper, is used to represent ε, and v_{i} is used to represent V(t_{i}). is just a local definition, used to shorten statements. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem40 27112* | This lemma proves that q_{n} is in the subalgebra, as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90. Q is used to represent q_{n} in the paper, N is used to represent n in the paper, and M is used to represent k^n in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem41 27113* | This lemma is used to prove that there exists x as in Lemma 1 of [BrosowskiDeutsh] p. 90: 0 <= x(t) <= 1 for all t in T, x(t) < epsilon for all t in V, x(t) > 1 - epsilon for all t in T \ U. Here we prove the very last step of the proof of Lemma 1: "The result follows from taking x = 1 - q_{n"};. Here is used to represent ε in the paper, and to represent q_{n} in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem42 27114* | This lemma is used to prove that built as in Lemma 2 of [BrosowskiDeutsh] p. 91, is such that x > 1 - ε on B. Here is used to represent in the paper, and E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem43 27115* | This lemma is used to prove the existence of a function p_{t} as in Lemma 1 of [BrosowskiDeutsh] p. 90 (at the beginning of Lemma 1): for all t in T - U, there exists a function p_{t} in the subalgebra, such that p_{t}( t_{0} ) = 0 , p_{t} ( t ) > 0, and 0 <= p_{t} <= 1. Hera Z is used for t_{0} , S is used for t e. T - U , h is used for p_{t}. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem44 27116* | This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_{(t}_0) = 0, and p > 0 on T - U. Z is used to represent t_{0} in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem45 27117* | This lemma proves that, given an appropriate (in another theorem we prove such a exists), there exists a function q_{n} as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91 ( at the top of page 91): 0 <= q_{n} <= 1 , q_{n} < ε on T \ U, and q_{n} > 1 - ε on . We use y to represent the final q_{n} in the paper (the one with n large enough), to represent in the paper, to represent , to represent δ, to represent ε, and to represent . (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem46 27118* | This lemma proves that sets U(t) as defined in Lemma 1 of [BrosowskiDeutsh] p. 90, are a cover of T \ U. Using this lemma, in a later theorem we will prove that a finite subcover exists. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem47 27119* | Subtracting a constant from a real continuous function gives another continuous function. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem48 27120* | This lemma is used to prove that built as in Lemma 2 of [BrosowskiDeutsh] p. 91, is such that x < ε on . Here is used to represent in the paper, is used to represent ε in the paper, and is used to represent in the paper (because is always used to represent the subalgebra). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem49 27121* | There exists a function q_{n} as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 91 (at the top of page 91): 0 <= q_{n} <= 1 , q_{n} < ε on , and q_{n} > 1 - ε on . Here y is used to represent the final q_{n} in the paper (the one with n large enough), represents in the paper, represents , represents δ, represents ε, and represents . (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem50 27122* | This lemma proves that sets U(t) as defined in Lemma 1 of [BrosowskiDeutsh] p. 90, contain a finite subcover of T \ U. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem51 27123* | There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. Here is used to represent in the paper, because here is used for the subalgebra of functions. is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem52 27124* | There exists a neighborood V as in Lemma 1 of [BrosowskiDeutsh] p. 90. Here Z is used to represent t_{0} in the paper, and v is used to represent V in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem53 27125* | This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_{(t}_0) = 0, and p > 0 on T - U. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem54 27126* | There exists a function as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. Here is used to represent in the paper, because here is used for the subalgebra of functions. is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem55 27127* | This lemma proves the existence of a function p as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_{(t}_0) = 0, and p > 0 on T - U. Here Z is used to represent t_{0} in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem56 27128* | This theorem proves Lemma 1 in [BrosowskiDeutsh] p. 90. Here is used to represent t_{0} in the paper, is used to represent in the paper, and is used to represent ε (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem57 27129* | There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. In this theorem, it is proven the non-trivial case (the closed set D is nonempty). Here D is used to represent A in the paper, because the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem58 27130* | This theorem proves Lemma 2 in [BrosowskiDeutsh] p. 91. Here D is used to represent the set A of Lemma 2, because here the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem59 27131* | This lemma proves that there exists a function as in the proof in [BrosowskiDeutsh] p. 91, after Lemma 2: x_{j} is in the subalgebra, 0 <= x_{j} <= 1, x_{j} < ε / n on A_{j} (meaning A in the paper), x_{j} > 1 - \epslon / n on B_{j}. Here is used to represent A in the paper (because A is used for the subalgebra of functions), is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem60 27132* | This lemma proves that there exists a function g as in the proof in [BrosowskiDeutsh] p. 91 (this parte of the proof actually spans through pages 91-92): g is in the subalgebra, and for all in , there is a such that (j-4/3)*ε < f(t) <= (j-1/3)*ε and (j-4/3)*ε < g(t) < (j+1/3)*ε. Here is used to represent f in the paper, and is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem61 27133* | This lemma proves that there exists a function as in the proof in [BrosowskiDeutsh] p. 92: is in the subalgebra, and for all in , abs( f(t) - g(t) ) < 2*ε. Here is used to represent f in the paper, and is used to represent ε. For this lemma there's the further assumption that the function to be approximated is nonnegative (this assumption is removed in a later theorem). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem62 27134* | This theorem proves the Stone Weierstrass theorem for the non-trivial case in which T is nonempty. The proof follows [BrosowskiDeutsh] p. 89 (through page 92). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweid 27135* | This theorem proves the Stone-Weierstrass theorem for real valued functions: let be a compact topology on , and be the set of real continuous functions on . Assume that is a subalgebra of (closed under addition and multiplication of functions) containing constant functions and discriminating points (if and are distinct points in , then there exists a function in such that h(r) is distinct from h(t) ). Then, for any continuous function and for any positive real , there exists a function in the subalgebra , such that approximates up to ( represents the usual ε value). As a classical example, given any a,b reals, the closed interval could be taken, along with the subalgebra of real polynomials on , and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on . The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stowei 27136* | This theorem proves the Stone-Weierstrass theorem for real valued functions: let be a compact topology on , and be the set of real continuous functions on . Assume that is a subalgebra of (closed under addition and multiplication of functions) containing constant functions and discriminating points (if and are distinct points in , then there exists a function in such that h(r) is distinct from h(t) ). Then, for any continuous function and for any positive real , there exists a function in the subalgebra , such that approximates up to ( represents the usual ε value). As a classical example, given any a,b reals, the closed interval could be taken, along with the subalgebra of real polynomials on , and then use this theorem to easily prove that real polynomials are dense in the standard metric space of continuous functions on . The proof and lemmas are written following [BrosowskiDeutsh] p. 89 (through page 92). Some effort is put in avoiding the use of the axiom of choice. The deduction version of this theorem is stoweid 27135: often times it will be better to use stoweid 27135 in other proofs (but this version is probably easier to be read and understood). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | wallispilem1 27137* | is monotone: increasing the exponent, the integral decreases. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | wallispilem2 27138* | A first set of properties for the sequence that will be used in the proof of the Wallis product formula (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | wallispilem3 27139* | I maps to real values (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | wallispilem4 27140* | maps to explicit expression for the ratio of two consecutive values of (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
Theorem | wallispilem5 27141* | The sequence converges to 1. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
Theorem | wallispi 27142* | Wallis' formula for π : Wallis' product converges to π / 2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | wallispi2lem1 27143 | An intermediate step between the first version of the Wallis' formula for π and the second version of Wallis' formula. This second version will then be used to prove Stirling's approximation formula for the factorial. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
Theorem | wallispi2lem2 27144 | Two expressions are proven to be equal, and this is used to complete the proof of the second version of Wallis' formula for π . (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
Theorem | wallispi2 27145 | An alternative version of Wallis' formula for π ; this second formula uses factorials and it is later used to proof Stirling's approximation formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem1 27146 | A simple limit of fractions is computed. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
Theorem | stirlinglem2 27147 | maps to positive reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem3 27148 | Long but simple algebraic transformations are applied to show that , the Wallis formula for π , can be expressed in terms of , the Stirling's approximation formula for the factorial, up to a constant factor. This will allow (in a later theorem) to determine the right constant factor to be put into the , in order to get the exact Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem4 27149* | Algebraic manipulation of n ) - ( B . It will be used in other theorems to show that is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem5 27150* | If is between and , then a series (without alternating negative and positive terms) is given that converges to log (1+T)/(1-T) . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem6 27151* | A series that converges to log (N+1)/N (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem7 27152* | Algebraic manipulation of the formula for J(n) (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem8 27153 | If converges to , then converges to C^2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem9 27154* | is expressed as a limit of a series. This result will be used both to prove that is decreasing and to prove that is bounded (below). It will follow that converges in the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem10 27155* | A bound for any B(N)-B(N + 1) that will allow to find a lower bound for the whole sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem11 27156* | is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem12 27157* | The sequence is bounded below. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem13 27158* | is decreasing and has a lower bound, then it converges. Since is , in another theorem it is proven that converges as well. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem14 27159* | The sequence converges to a positive real. This proves that the Stirling's formula converges to the factorial, up to a constant. In another theorem, using Wallis' formula for π& , such constant is exactly determined, thus proving the Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem15 27160* | The Stirling's formula is proven using a number of local definitions. The main theorem stirling 27161 will use this final lemma, but it will not expose the local definitions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirling 27161 | Stirling's approximation formula for factorial. The proof follows two major steps: first it is proven that and factorial are asymptotically equivalent, up to an unknown constant. Then, using Wallis' formula for π it is proven that the unknown constant is the square root of π and then the exact Stirling's formula is established. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlingr 27162 | Stirling's approximation formula for factorial: here convergence is expressed with respect to the standard topology on the reals. The main theorem stirling 27161 is proven for convergence in the topology of complex numbers. The variable is used to denote convergence with respect to the standard topology on the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | sigarval 27163* | Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarim 27164* | Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarac 27165* | Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigaraf 27166* | Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarmf 27167* | Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigaras 27168* | Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarms 27169* | Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarls 27170* | Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarid 27171* | Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
Theorem | sigarexp 27172* | Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
Theorem | sigarperm 27173* | Signed area acts as a double area of a triangle . Here we prove that cyclically permuting the vertices doesn't change the area. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
Theorem | sigardiv 27174* | If signed area between vectors and is zero, then those vectors lie on the same line. (Contributed by Saveliy Skresanov, 22-Sep-2017.) |
Theorem | sigarimcd 27175* | Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
Theorem | sigariz 27176* | If signed area is zero, the signed area with swapped arguments is also zero. Deduction version. ( Contributed by Saveliy Skresanov, 23-Sep-2017.) (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
Theorem | sigarcol 27177* | Given three points , and such that , the point lies on the line going through and iff the corresponding signed area is zero. That justifies the usage of signed area as a collinearity indicator. (Contributed by Saveliy Skresanov, 22-Sep-2017.) |
Theorem | sharhght 27178* | Let be a triangle, and let lie on the line . Then (doubled) areas of triangles and relate as lengths of corresponding bases and . (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
Theorem | sigaradd 27179* | Subtracting (double) area of from yields the (double) area of . (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
Theorem | cevathlem1 27180 | Ceva's theorem first lemma. Multiplies three identities and divides by the common factors. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
Theorem | cevathlem2 27181* | Ceva's theorem second lemma. Relate (doubled) areas of triangles and with of segments and . (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
Theorem | cevath 27182* |
Ceva's theorem. Let be a triangle and let
points ,
and lie on sides , ,
correspondingly. Suppose that cevians , and
intersect at one point . Then triangle's sides are partitioned
into segments and their lengths satisfy a certain identity. Here we
obtain a bit stronger version by using complex numbers themselves
instead of their absolute values.
The proof goes by applying cevathlem2 27181 three times and then using cevathlem1 27180 to multiply obtained identities and prove the theorem. In the theorem statement we are using function as a collinearity indicator. For justification of that use, see sigarcol 27177. (Contributed by Saveliy Skresanov, 24-Sep-2017.) |
Theorem | hirstL-ax3 27183 | The third axiom of a system called "L" but proven to be a theorem since set.mm uses a different third axiom. This is named hirst after Holly P. Hirst and Jeffry L. Hirst. Axiom A3 of [Mendelson] p. 35. (Contributed by Jarvin Udandy, 7-Feb-2015.) (Proof modification is discouraged.) |
Theorem | ax3h 27184 | Recovery of ax-3 7 from hirstL-ax3 27183. (Contributed by Jarvin Udandy, 3-Jul-2015.) |
Theorem | aibandbiaiffaiffb 27185 | A closed form showing (a implies b and b implies a) same-as (a same-as b) (Contributed by Jarvin Udandy, 3-Sep-2016.) |