Home | Metamath
Proof Explorer Theorem List (p. 277 of 324) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-22341) |
Hilbert Space Explorer
(22342-23864) |
Users' Mathboxes
(23865-32387) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | stoweidlem23 27601* | This lemma is used to prove the existence of a function p_{t} as in the beginning of Lemma 1 [BrosowskiDeutsh] p. 90: 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. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem24 27602* | This lemma proves that for sufficiently large, q_{n}( t ) > ( 1 - epsilon ), for all in : see Lemma 1 [BrosowskiDeutsh] p. 90, (at the bottom of page 90). is used to represent q_{n} in the paper, to represent in the paper, to represent , to represent δ, and to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem25 27603* | This lemma proves that for n sufficiently large, q_{n}( t ) < ε, for all in : see Lemma 1 [BrosowskiDeutsh] p. 91 (at the top of page 91). is used to represent q_{n} in the paper, to represent n in the paper, to represent k, to represent δ, to represent p, and to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem26 27604* | This lemma is used to prove that there is a function as in the proof of [BrosowskiDeutsh] p. 92: this lemma proves that g(t) > ( j - 4 / 3 ) * ε. Here is used to represnt j in the paper, is used to represent A in the paper, is used to represent t, and is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem27 27605* | 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. Here is used to represent p_{(t}_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem28 27606* | There exists a δ as in Lemma 1 [BrosowskiDeutsh] p. 90: 0 < delta < 1 and p >= delta on . Here is used to represent δ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem29 27607* | 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 27608* | 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 27609* | 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 27610* | 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 27611* | 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 27612* | 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 27613* | 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 27614* | 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 27615* | 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 27616* | 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 27617* | 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 27618* | 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 27619* | 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 27620* | 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 27621* | 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 27622* | 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 27623* | 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 27624* | 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 27625* | Subtracting a constant from a real continuous function gives another continuous function. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | stoweidlem48 27626* | 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 27627* | 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 27628* | 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 27629* | 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 27630* | 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 27631* | 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 27632* | 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 27633* | 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 27634* | 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 27635* | 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 27636* | 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 27637* | 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 27638* | 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 27639* | 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 27640* | 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 27641* | 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 27642* | 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 27641: often times it will be better to use stoweid 27641 in other proofs (but this version is probably easier to be read and understood). (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
Theorem | wallispilem1 27643* | is monotone: increasing the exponent, the integral decreases. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | wallispilem2 27644* | 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 27645* | I maps to real values (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | wallispilem4 27646* | maps to explicit expression for the ratio of two consecutive values of (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
Theorem | wallispilem5 27647* | The sequence converges to 1. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
Theorem | wallispi 27648* | Wallis' formula for π : Wallis' product converges to π / 2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | wallispi2lem1 27649 | 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 27650 | 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 27651 | 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 27652 | A simple limit of fractions is computed. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
Theorem | stirlinglem2 27653 | maps to positive reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem3 27654 | 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 27655* | 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 27656* | 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 27657* | A series that converges to log (N+1)/N (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem7 27658* | Algebraic manipulation of the formula for J(n) (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem8 27659 | If converges to , then converges to C^2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem9 27660* | 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 27661* | 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 27662* | is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem12 27663* | The sequence is bounded below. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirlinglem13 27664* | 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 27665* | 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 27666* | The Stirling's formula is proven using a number of local definitions. The main theorem stirling 27667 will use this final lemma, but it will not expose the local definitions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
Theorem | stirling 27667 | 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 27668 | Stirling's approximation formula for factorial: here convergence is expressed with respect to the standard topology on the reals. The main theorem stirling 27667 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 27669* | Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarim 27670* | Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarac 27671* | Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigaraf 27672* | Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarmf 27673* | Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigaras 27674* | Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarms 27675* | Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarls 27676* | Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.) |
Theorem | sigarid 27677* | Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
Theorem | sigarexp 27678* | Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017.) |
Theorem | sigarperm 27679* | 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 27680* | 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 27681* | Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.) |
Theorem | sigariz 27682* | 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 27683* | Given three points , and such that |