Home | Metamath
Proof Explorer Theorem List (p. 409 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | retire 40801 | Commuted version of itrere 40800. (Contributed by SN, 27-Jun-2024.) |
β’ (π β β β ((π Β· i) β β β π = 0)) | ||
Theorem | cnreeu 40802 | The reals in the expression given by cnre 11085 uniquely define a complex number. (Contributed by SN, 27-Jun-2024.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π‘ β β) & β’ (π β π’ β β) β β’ (π β ((π + (i Β· π )) = (π‘ + (i Β· π’)) β (π = π‘ β§ π = π’))) | ||
Theorem | sn-sup2 40803* | sup2 12044 with exactly the same proof except for using sn-ltp1 40797 instead of ltp1 11928, saving ax-mulcom 11048. (Contributed by SN, 26-Jun-2024.) |
β’ ((π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ (π¦ < π₯ β¨ π¦ = π₯)) β βπ₯ β β (βπ¦ β π΄ Β¬ π₯ < π¦ β§ βπ¦ β β (π¦ < π₯ β βπ§ β π΄ π¦ < π§))) | ||
Looking at a corner in 3D space, one can see three right angles. It is impossible to draw three lines in 2D space such that any two of these lines are perpendicular, but a good enough representation is made by casting lines from the 2D surface. Points along the same cast line are collapsed into one point on the 2D surface. In many cases, the 2D surface is smaller than whatever needs to be represented. If the lines cast were perpendicular to the 2D surface, then only areas as small as the 2D surface could be represented. To fix this, the lines need to get further apart as they go farther from the 2D surface. On the other side of the 2D surface the lines will get closer together and intersect at a point. (Because it's defined that way). From this perspective, two parallel lines in 3D space will be represented by two lines that seem to intersect at a point "at infinity". Considering all maximal classes of parallel lines on a 2D plane in 3D space, these classes will all appear to intersect at different points at infinity, forming a line at infinity. Therefore the real projective plane can be thought of as the real affine plane together with the line at infinity. The projective plane takes care of some exceptions that may be found in the affine plane. For example, consider the curve that is the zeroes of π¦ = π₯β2. Any line connecting the point (0, 1) to the x-axis intersects with the curve twice, except for the vertical line between (0, 1) and (0, 0). In the projective plane, the curve becomes an ellipse and there is no exception. While it may not seem like it, points at infinity and points corresponding to the affine plane are the same type of point. Consider a line going through the origin in 3D (affine) space. Either it intersects the plane π§ = 1 once, or it is entirely within the plane π§ = 0. If it is entirely within the plane π§ = 0, then it corresponds to the point at infinity intersecting all lines on the plane π§ = 1 with the same slope. Else it corresponds to the point in the 2D plane π§ = 1 that it intersects. So there is a bijection between 3D lines through the origin and points on the real projective plane. The concept of projective spaces generalizes the projective plane to any dimension. | ||
Syntax | cprjsp 40804 | Extend class notation with the projective space function. |
class βπ£π π | ||
Definition | df-prjsp 40805* | Define the projective space function. In the bijection between 3D lines through the origin and points in the projective plane (see section comment), this is equivalent to making any two 3D points (excluding the origin) equivalent iff one is a multiple of another. This definition does not quite give all the properties needed, since the scalars of a left vector space can be "less dense" than the vectors (for example, equivocating rational multiples of real numbers). Compare df-lsatoms 37333. (Contributed by BJ and SN, 29-Apr-2023.) |
β’ βπ£π π = (π£ β LVec β¦ β¦((Baseβπ£) β {(0gβπ£)}) / πβ¦(π / {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ βπ β (Baseβ(Scalarβπ£))π₯ = (π( Β·π βπ£)π¦))})) | ||
Theorem | prjspval 40806* | Value of the projective space function, which is also known as the projectivization of π. (Contributed by Steven Nguyen, 29-Apr-2023.) |
β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) β β’ (π β LVec β (βπ£π πβπ) = (π΅ / {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))})) | ||
Theorem | prjsprel 40807* | Utility theorem regarding the relation used in βπ£π π. (Contributed by Steven Nguyen, 29-Apr-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} β β’ (π βΌ π β ((π β π΅ β§ π β π΅) β§ βπ β πΎ π = (π Β· π))) | ||
Theorem | prjspertr 40808* | The relation in βπ£π π is transitive. (Contributed by Steven Nguyen, 1-May-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) β β’ ((π β LMod β§ (π βΌ π β§ π βΌ π)) β π βΌ π) | ||
Theorem | prjsperref 40809* | The relation in βπ£π π is reflexive. (Contributed by Steven Nguyen, 30-Apr-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) β β’ (π β LMod β (π β π΅ β π βΌ π)) | ||
Theorem | prjspersym 40810* | The relation in βπ£π π is symmetric. (Contributed by Steven Nguyen, 1-May-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) β β’ ((π β LVec β§ π βΌ π) β π βΌ π) | ||
Theorem | prjsper 40811* | The relation used to define βπ£π π is an equivalence relation. (Contributed by Steven Nguyen, 1-May-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) β β’ (π β LVec β βΌ Er π΅) | ||
Theorem | prjspreln0 40812* | Two nonzero vectors are equivalent by a nonzero scalar. (Contributed by Steven Nguyen, 31-May-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) & β’ 0 = (0gβπ) β β’ (π β LVec β (π βΌ π β ((π β π΅ β§ π β π΅) β§ βπ β (πΎ β { 0 })π = (π Β· π)))) | ||
Theorem | prjspvs 40813* | A nonzero multiple of a vector is equivalent to the vector. (Contributed by Steven Nguyen, 6-Jun-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) & β’ 0 = (0gβπ) β β’ ((π β LVec β§ π β π΅ β§ π β (πΎ β { 0 })) β (π Β· π) βΌ π) | ||
Theorem | prjsprellsp 40814* | Two vectors are equivalent iff their spans are equal. (Contributed by Steven Nguyen, 31-May-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LVec β§ (π β π΅ β§ π β π΅)) β (π βΌ π β (πβ{π}) = (πβ{π}))) | ||
Theorem | prjspeclsp 40815* | The vectors equivalent to a vector π are the nonzero vectors in the span of π. (Contributed by Steven Nguyen, 6-Jun-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LVec β§ π β π΅) β [π] βΌ = ((πβ{π}) β {(0gβπ)})) | ||
Theorem | prjspval2 40816* | Alternate definition of projective space. (Contributed by Steven Nguyen, 7-Jun-2023.) |
β’ 0 = (0gβπ) & β’ π΅ = ((Baseβπ) β { 0 }) & β’ π = (LSpanβπ) β β’ (π β LVec β (βπ£π πβπ) = βͺ π§ β π΅ {((πβ{π§}) β { 0 })}) | ||
Syntax | cprjspn 40817 | Extend class notation with the n-dimensional projective space function. |
class βπ£π πn | ||
Definition | df-prjspn 40818* | Define the n-dimensional projective space function. A projective space of dimension 1 is a projective line, and a projective space of dimension 2 is a projective plane. Compare df-ehl 24672. This space is considered n-dimensional because the vector space (π freeLMod (0...π)) is (n+1)-dimensional and the βπ£π π function returns equivalence classes with respect to a linear (1-dimensional) relation. (Contributed by BJ and Steven Nguyen, 29-Apr-2023.) |
β’ βπ£π πn = (π β β0, π β DivRing β¦ (βπ£π πβ(π freeLMod (0...π)))) | ||
Theorem | prjspnval 40819 | Value of the n-dimensional projective space function. (Contributed by Steven Nguyen, 1-May-2023.) |
β’ ((π β β0 β§ πΎ β DivRing) β (πβπ£π πnπΎ) = (βπ£π πβ(πΎ freeLMod (0...π)))) | ||
Theorem | prjspnerlem 40820* | A lemma showing that the equivalence relation used in prjspnval2 40821 and the equivalence relation used in prjspval 40806 are equal, but only with the antecedent πΎ β DivRing. (Contributed by SN, 15-Jul-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β π π₯ = (π Β· π¦))} & β’ π = (πΎ freeLMod (0...π)) & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (BaseβπΎ) & β’ Β· = ( Β·π βπ) β β’ (πΎ β DivRing β βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β (Baseβ(Scalarβπ))π₯ = (π Β· π¦))}) | ||
Theorem | prjspnval2 40821* | Value of the n-dimensional projective space function, expanded. (Contributed by Steven Nguyen, 15-Jul-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β π π₯ = (π Β· π¦))} & β’ π = (πΎ freeLMod (0...π)) & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (BaseβπΎ) & β’ Β· = ( Β·π βπ) β β’ ((π β β0 β§ πΎ β DivRing) β (πβπ£π πnπΎ) = (π΅ / βΌ )) | ||
Theorem | prjspner 40822* | The relation used to define βπ£π π (and indirectly βπ£π πn through df-prjspn 40818) is an equivalence relation. This is a lemma that converts the equivalence relation used in results like prjspertr 40808 and prjspersym 40810 (see prjspnerlem 40820). Several theorems are covered in one thanks to the theorems around df-er 8581. (Contributed by SN, 14-Aug-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β π π₯ = (π Β· π¦))} & β’ π = (πΎ freeLMod (0...π)) & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (BaseβπΎ) & β’ Β· = ( Β·π βπ) & β’ (π β πΎ β DivRing) β β’ (π β βΌ Er π΅) | ||
Theorem | prjspnvs 40823* | A nonzero multiple of a vector is equivalent to the vector. This converts the equivalence relation used in prjspvs 40813 (see prjspnerlem 40820). (Contributed by SN, 8-Aug-2024.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β π π₯ = (π Β· π¦))} & β’ π = (πΎ freeLMod (0...π)) & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (BaseβπΎ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπΎ) & β’ (π β πΎ β DivRing) & β’ (π β π β π΅) & β’ (π β πΆ β π) & β’ (π β πΆ β 0 ) β β’ (π β (πΆ Β· π) βΌ π) | ||
Theorem | prjspnssbas 40824 | A projective point spans a subset of the (nonzero) affine points. (Contributed by SN, 17-Jan-2025.) |
β’ π = (πβπ£π πnπΎ) & β’ π = (πΎ freeLMod (0...π)) & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ (π β π β β0) & β’ (π β πΎ β DivRing) β β’ (π β π β π« π΅) | ||
Theorem | prjspnn0 40825 | A projective point is nonempty. (Contributed by SN, 17-Jan-2025.) |
β’ π = (πβπ£π πnπΎ) & β’ π = (πΎ freeLMod (0...π)) & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ (π β π β β0) & β’ (π β πΎ β DivRing) & β’ (π β π΄ β π) β β’ (π β π΄ β β ) | ||
Theorem | 0prjspnlem 40826 | Lemma for 0prjspn 40831. The given unit vector is a nonzero vector. (Contributed by Steven Nguyen, 16-Jul-2023.) |
β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (πΎ freeLMod (0...0)) & β’ 1 = ((πΎ unitVec (0...0))β0) β β’ (πΎ β DivRing β 1 β π΅) | ||
Theorem | prjspnfv01 40827* | Any vector is equivalent to a vector whose zeroth coordinate is 0 or 1 (proof of the value of the zeroth coordinate). (Contributed by SN, 13-Aug-2023.) |
β’ πΉ = (π β π΅ β¦ if((πβ0) = 0 , π, ((πΌβ(πβ0)) Β· π))) & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (πΎ freeLMod (0...π)) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπΎ) & β’ 1 = (1rβπΎ) & β’ πΌ = (invrβπΎ) & β’ (π β πΎ β DivRing) & β’ (π β π β β0) & β’ (π β π β π΅) β β’ (π β ((πΉβπ)β0) = if((πβ0) = 0 , 0 , 1 )) | ||
Theorem | prjspner01 40828* | Any vector is equivalent to a vector whose zeroth coordinate is 0 or 1 (proof of the equivalence). (Contributed by SN, 13-Aug-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β π π₯ = (π Β· π¦))} & β’ πΉ = (π β π΅ β¦ if((πβ0) = 0 , π, ((πΌβ(πβ0)) Β· π))) & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (πΎ freeLMod (0...π)) & β’ Β· = ( Β·π βπ) & β’ π = (BaseβπΎ) & β’ 0 = (0gβπΎ) & β’ πΌ = (invrβπΎ) & β’ (π β πΎ β DivRing) & β’ (π β π β β0) & β’ (π β π β π΅) β β’ (π β π βΌ (πΉβπ)) | ||
Theorem | prjspner1 40829* | Two vectors whose zeroth coordinate is nonzero are equivalent if and only if they have the same representative in the (n-1)-dimensional affine subspace { x0 = 1 } . For example, vectors in 3D space whose π₯ coordinate is nonzero are equivalent iff they intersect at the plane π₯ = 1 at the same point (also see section header). (Contributed by SN, 13-Aug-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β π π₯ = (π Β· π¦))} & β’ πΉ = (π β π΅ β¦ if((πβ0) = 0 , π, ((πΌβ(πβ0)) Β· π))) & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (πΎ freeLMod (0...π)) & β’ Β· = ( Β·π βπ) & β’ π = (BaseβπΎ) & β’ 0 = (0gβπΎ) & β’ πΌ = (invrβπΎ) & β’ (π β πΎ β DivRing) & β’ (π β π β β0) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β (πβ0) β 0 ) & β’ (π β (πβ0) β 0 ) β β’ (π β (π βΌ π β (πΉβπ) = (πΉβπ))) | ||
Theorem | 0prjspnrel 40830* | In the zero-dimensional projective space, all vectors are equivalent to the unit vector. (Contributed by Steven Nguyen, 7-Jun-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β π π₯ = (π Β· π¦))} & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ Β· = ( Β·π βπ) & β’ π = (BaseβπΎ) & β’ π = (πΎ freeLMod (0...0)) & β’ 1 = ((πΎ unitVec (0...0))β0) β β’ ((πΎ β DivRing β§ π β π΅) β π βΌ 1 ) | ||
Theorem | 0prjspn 40831 | A zero-dimensional projective space has only 1 point. (Contributed by Steven Nguyen, 9-Jun-2023.) |
β’ π = (πΎ freeLMod (0...0)) & β’ π΅ = ((Baseβπ) β {(0gβπ)}) β β’ (πΎ β DivRing β (0βπ£π πnπΎ) = {π΅}) | ||
Syntax | cprjcrv 40832 | Extend class notation with the projective curve function. |
class βπ£π πCrv | ||
Definition | df-prjcrv 40833* | Define the projective curve function. This takes a homogeneous polynomial and outputs the homogeneous coordinates where the polynomial evaluates to zero (the "zero set"). (In other words, scalar multiples are collapsed into the same projective point. See mhphf4 40642 and prjspvs 40813). (Contributed by SN, 23-Nov-2024.) |
β’ βπ£π πCrv = (π β β0, π β Field β¦ (π β βͺ ran ((0...π) mHomP π) β¦ {π β (πβπ£π πnπ) β£ ((((0...π) eval π)βπ) β π) = {(0gβπ)}})) | ||
Theorem | prjcrvfval 40834* | Value of the projective curve function. (Contributed by SN, 23-Nov-2024.) |
β’ π» = ((0...π) mHomP πΎ) & β’ πΈ = ((0...π) eval πΎ) & β’ π = (πβπ£π πnπΎ) & β’ 0 = (0gβπΎ) & β’ (π β π β β0) & β’ (π β πΎ β Field) β β’ (π β (πβπ£π πCrvπΎ) = (π β βͺ ran π» β¦ {π β π β£ ((πΈβπ) β π) = { 0 }})) | ||
Theorem | prjcrvval 40835* | Value of the projective curve function. (Contributed by SN, 23-Nov-2024.) |
β’ π» = ((0...π) mHomP πΎ) & β’ πΈ = ((0...π) eval πΎ) & β’ π = (πβπ£π πnπΎ) & β’ 0 = (0gβπΎ) & β’ (π β π β β0) & β’ (π β πΎ β Field) & β’ (π β πΉ β βͺ ran π») β β’ (π β ((πβπ£π πCrvπΎ)βπΉ) = {π β π β£ ((πΈβπΉ) β π) = { 0 }}) | ||
Theorem | prjcrv0 40836 | The "curve" (zero set) corresponding to the zero polynomial contains all coordinates. (Contributed by SN, 23-Nov-2024.) |
β’ π = ((0...π) mPoly πΎ) & β’ 0 = (0gβπ) & β’ π = (πβπ£π πnπΎ) & β’ (π β π β β0) & β’ (π β πΎ β Field) β β’ (π β ((πβπ£π πCrvπΎ)β 0 ) = π) | ||
Theorem | dffltz 40837* | Fermat's Last Theorem (FLT) for nonzero integers is equivalent to the original scope of natural numbers. The backwards direction takes (πβπ) + (πβπ) = (πβπ), and adds the negative of any negative term to both sides, thus creating the corresponding equation with only positive integers. There are six combinations of negativity, so the proof is particularly long. (Contributed by Steven Nguyen, 27-Feb-2023.) |
β’ (βπ β (β€β₯β3)βπ₯ β β βπ¦ β β βπ§ β β ((π₯βπ) + (π¦βπ)) β (π§βπ) β βπ β (β€β₯β3)βπ β (β€ β {0})βπ β (β€ β {0})βπ β (β€ β {0})((πβπ) + (πβπ)) β (πβπ)) | ||
Theorem | fltmul 40838 | A counterexample to FLT stays valid when scaled. The hypotheses are more general than they need to be for convenience. (There does not seem to be a standard term for Fermat or Pythagorean triples extended to any π β β0, so the label is more about the context in which this theorem is used). (Contributed by SN, 20-Aug-2024.) |
β’ (π β π β β) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β β0) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) β β’ (π β (((π Β· π΄)βπ) + ((π Β· π΅)βπ)) = ((π Β· πΆ)βπ)) | ||
Theorem | fltdiv 40839 | A counterexample to FLT stays valid when scaled. The hypotheses are more general than they need to be for convenience. (Contributed by SN, 20-Aug-2024.) |
β’ (π β π β β) & β’ (π β π β 0) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β β0) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) β β’ (π β (((π΄ / π)βπ) + ((π΅ / π)βπ)) = ((πΆ / π)βπ)) | ||
Theorem | flt0 40840 | A counterexample for FLT does not exist for π = 0. (Contributed by SN, 20-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β β0) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) β β’ (π β π β β) | ||
Theorem | fltdvdsabdvdsc 40841 | Any factor of both π΄ and π΅ also divides πΆ. This establishes the validity of fltabcoprmex 40842. (Contributed by SN, 21-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β β) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) β β’ (π β (π΄ gcd π΅) β₯ πΆ) | ||
Theorem | fltabcoprmex 40842 | A counterexample to FLT implies a counterexample to FLT with π΄, π΅ (assigned to π΄ / (π΄ gcd π΅) and π΅ / (π΄ gcd π΅)) coprime (by divgcdcoprm0 16475). (Contributed by SN, 20-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β β0) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) β β’ (π β (((π΄ / (π΄ gcd π΅))βπ) + ((π΅ / (π΄ gcd π΅))βπ)) = ((πΆ / (π΄ gcd π΅))βπ)) | ||
Theorem | fltaccoprm 40843 | A counterexample to FLT with π΄, π΅ coprime also has π΄, πΆ coprime. (Contributed by SN, 20-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β β0) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) & β’ (π β (π΄ gcd π΅) = 1) β β’ (π β (π΄ gcd πΆ) = 1) | ||
Theorem | fltbccoprm 40844 | A counterexample to FLT with π΄, π΅ coprime also has π΅, πΆ coprime. Proven from fltaccoprm 40843 using commutativity of addition. (Contributed by SN, 20-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β β0) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) & β’ (π β (π΄ gcd π΅) = 1) β β’ (π β (π΅ gcd πΆ) = 1) | ||
Theorem | fltabcoprm 40845 | A counterexample to FLT with π΄, πΆ coprime also has π΄, π΅ coprime. Converse of fltaccoprm 40843. (Contributed by SN, 22-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β (π΄ gcd πΆ) = 1) & β’ (π β ((π΄β2) + (π΅β2)) = (πΆβ2)) β β’ (π β (π΄ gcd π΅) = 1) | ||
Theorem | infdesc 40846* | Infinite descent. The hypotheses say that π is lower bounded, and that if π holds for an integer in π, it holds for a smaller integer in π. By infinite descent, eventually we cannot go any smaller, therefore π holds for no integer in π. (Contributed by SN, 20-Aug-2024.) |
β’ (π¦ = π₯ β (π β π)) & β’ (π¦ = π§ β (π β π)) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ (π₯ β π β§ π)) β βπ§ β π (π β§ π§ < π₯)) β β’ (π β {π¦ β π β£ π} = β ) | ||
Theorem | fltne 40847 | If a counterexample to FLT exists, its addends are not equal. (Contributed by SN, 1-Jun-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β (β€β₯β2)) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) β β’ (π β π΄ β π΅) | ||
Theorem | flt4lem 40848 | Raising a number to the fourth power is equivalent to squaring it twice. (Contributed by SN, 21-Aug-2024.) |
β’ (π β π΄ β β) β β’ (π β (π΄β4) = ((π΄β2)β2)) | ||
Theorem | flt4lem1 40849 | Satisfy the antecedent used in several pythagtrip 16640 lemmas, with π΄, πΆ coprime rather than π΄, π΅. (Contributed by SN, 21-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β Β¬ 2 β₯ π΄) & β’ (π β (π΄ gcd πΆ) = 1) & β’ (π β ((π΄β2) + (π΅β2)) = (πΆβ2)) β β’ (π β ((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄))) | ||
Theorem | flt4lem2 40850 | If π΄ is even, π΅ is odd. (Contributed by SN, 22-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β 2 β₯ π΄) & β’ (π β (π΄ gcd πΆ) = 1) & β’ (π β ((π΄β2) + (π΅β2)) = (πΆβ2)) β β’ (π β Β¬ 2 β₯ π΅) | ||
Theorem | flt4lem3 40851 | Equivalent to pythagtriplem4 16625. Show that πΆ + π΄ and πΆ β π΄ are coprime. (Contributed by SN, 22-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β 2 β₯ π΄) & β’ (π β (π΄ gcd πΆ) = 1) & β’ (π β ((π΄β2) + (π΅β2)) = (πΆβ2)) β β’ (π β ((πΆ + π΄) gcd (πΆ β π΄)) = 1) | ||
Theorem | flt4lem4 40852 | If the product of two coprime factors is a perfect square, the factors are perfect squares. (Contributed by SN, 22-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β (π΄ gcd π΅) = 1) & β’ (π β (π΄ Β· π΅) = (πΆβ2)) β β’ (π β (π΄ = ((π΄ gcd πΆ)β2) β§ π΅ = ((π΅ gcd πΆ)β2))) | ||
Theorem | flt4lem5 40853 | In the context of the lemmas of pythagtrip 16640, π and π are coprime. (Contributed by SN, 23-Aug-2024.) |
β’ π = (((ββ(πΆ + π΅)) + (ββ(πΆ β π΅))) / 2) & β’ π = (((ββ(πΆ + π΅)) β (ββ(πΆ β π΅))) / 2) β β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β (π gcd π) = 1) | ||
Theorem | flt4lem5elem 40854 | Version of fltaccoprm 40843 and fltbccoprm 40844 where π is not squared. This can be proved in general for any polynomial in three variables: using prmdvdsncoprmbd 16536, dvds2addd 16108, and prmdvdsexp 16525, we can show that if two variables are coprime, the third is also coprime to the two. (Contributed by SN, 24-Aug-2024.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β π = ((π β2) + (πβ2))) & β’ (π β (π gcd π) = 1) β β’ (π β ((π gcd π) = 1 β§ (π gcd π) = 1)) | ||
Theorem | flt4lem5a 40855 | Part 1 of Equation 1 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. (Contributed by SN, 22-Aug-2024.) |
β’ π = (((ββ(πΆ + (π΅β2))) + (ββ(πΆ β (π΅β2)))) / 2) & β’ π = (((ββ(πΆ + (π΅β2))) β (ββ(πΆ β (π΅β2)))) / 2) & β’ π = (((ββ(π + π)) + (ββ(π β π))) / 2) & β’ π = (((ββ(π + π)) β (ββ(π β π))) / 2) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β Β¬ 2 β₯ π΄) & β’ (π β (π΄ gcd πΆ) = 1) & β’ (π β ((π΄β4) + (π΅β4)) = (πΆβ2)) β β’ (π β ((π΄β2) + (πβ2)) = (πβ2)) | ||
Theorem | flt4lem5b 40856 | Part 2 of Equation 1 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. (Contributed by SN, 22-Aug-2024.) |
β’ π = (((ββ(πΆ + (π΅β2))) + (ββ(πΆ β (π΅β2)))) / 2) & β’ π = (((ββ(πΆ + (π΅β2))) β (ββ(πΆ β (π΅β2)))) / 2) & β’ π = (((ββ(π + π)) + (ββ(π β π))) / 2) & β’ π = (((ββ(π + π)) β (ββ(π β π))) / 2) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β Β¬ 2 β₯ π΄) & β’ (π β (π΄ gcd πΆ) = 1) & β’ (π β ((π΄β4) + (π΅β4)) = (πΆβ2)) β β’ (π β (2 Β· (π Β· π)) = (π΅β2)) | ||
Theorem | flt4lem5c 40857 | Part 2 of Equation 2 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. (Contributed by SN, 22-Aug-2024.) |
β’ π = (((ββ(πΆ + (π΅β2))) + (ββ(πΆ β (π΅β2)))) / 2) & β’ π = (((ββ(πΆ + (π΅β2))) β (ββ(πΆ β (π΅β2)))) / 2) & β’ π = (((ββ(π + π)) + (ββ(π β π))) / 2) & β’ π = (((ββ(π + π)) β (ββ(π β π))) / 2) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β Β¬ 2 β₯ π΄) & β’ (π β (π΄ gcd πΆ) = 1) & β’ (π β ((π΄β4) + (π΅β4)) = (πΆβ2)) β β’ (π β π = (2 Β· (π Β· π))) | ||
Theorem | flt4lem5d 40858 | Part 3 of Equation 2 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. (Contributed by SN, 23-Aug-2024.) |
β’ π = (((ββ(πΆ + (π΅β2))) + (ββ(πΆ β (π΅β2)))) / 2) & β’ π = (((ββ(πΆ + (π΅β2))) β (ββ(πΆ β (π΅β2)))) / 2) & β’ π = (((ββ(π + π)) + (ββ(π β π))) / 2) & β’ π = (((ββ(π + π)) β (ββ(π β π))) / 2) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β Β¬ 2 β₯ π΄) & β’ (π β (π΄ gcd πΆ) = 1) & β’ (π β ((π΄β4) + (π΅β4)) = (πΆβ2)) β β’ (π β π = ((π β2) + (πβ2))) | ||
Theorem | flt4lem5e 40859 | Satisfy the hypotheses of flt4lem4 40852. (Contributed by SN, 23-Aug-2024.) |
β’ π = (((ββ(πΆ + (π΅β2))) + (ββ(πΆ β (π΅β2)))) / 2) & β’ π = (((ββ(πΆ + (π΅β2))) β (ββ(πΆ β (π΅β2)))) / 2) & β’ π = (((ββ(π + π)) + (ββ(π β π))) / 2) & β’ π = (((ββ(π + π)) β (ββ(π β π))) / 2) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β Β¬ 2 β₯ π΄) & β’ (π β (π΄ gcd πΆ) = 1) & β’ (π β ((π΄β4) + (π΅β4)) = (πΆβ2)) β β’ (π β (((π gcd π) = 1 β§ (π gcd π) = 1 β§ (π gcd π) = 1) β§ (π β β β§ π β β β§ π β β) β§ ((π Β· (π Β· π)) = ((π΅ / 2)β2) β§ (π΅ / 2) β β))) | ||
Theorem | flt4lem5f 40860 | Final equation of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. Given π΄β4 + π΅β4 = πΆβ2, provide a smaller solution. This satisfies the infinite descent condition. (Contributed by SN, 24-Aug-2024.) |
β’ π = (((ββ(πΆ + (π΅β2))) + (ββ(πΆ β (π΅β2)))) / 2) & β’ π = (((ββ(πΆ + (π΅β2))) β (ββ(πΆ β (π΅β2)))) / 2) & β’ π = (((ββ(π + π)) + (ββ(π β π))) / 2) & β’ π = (((ββ(π + π)) β (ββ(π β π))) / 2) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β Β¬ 2 β₯ π΄) & β’ (π β (π΄ gcd πΆ) = 1) & β’ (π β ((π΄β4) + (π΅β4)) = (πΆβ2)) β β’ (π β ((π gcd (π΅ / 2))β2) = (((π gcd (π΅ / 2))β4) + ((π gcd (π΅ / 2))β4))) | ||
Theorem | flt4lem6 40861 | Remove shared factors in a solution to π΄β4 + π΅β4 = πΆβ2. (Contributed by SN, 24-Jul-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β ((π΄β4) + (π΅β4)) = (πΆβ2)) β β’ (π β (((π΄ / (π΄ gcd π΅)) β β β§ (π΅ / (π΄ gcd π΅)) β β β§ (πΆ / ((π΄ gcd π΅)β2)) β β) β§ (((π΄ / (π΄ gcd π΅))β4) + ((π΅ / (π΄ gcd π΅))β4)) = ((πΆ / ((π΄ gcd π΅)β2))β2))) | ||
Theorem | flt4lem7 40862* | Convert flt4lem5f 40860 into a convenient form for nna4b4nsq 40863. TODO-SN: The change to (π΄ gcd π΅) = 1 points at some inefficiency in the lemmas. (Contributed by SN, 25-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β Β¬ 2 β₯ π΄) & β’ (π β (π΄ gcd π΅) = 1) & β’ (π β ((π΄β4) + (π΅β4)) = (πΆβ2)) β β’ (π β βπ β β (βπ β β ββ β β (Β¬ 2 β₯ π β§ ((π gcd β) = 1 β§ ((πβ4) + (ββ4)) = (πβ2))) β§ π < πΆ)) | ||
Theorem | nna4b4nsq 40863 | Strengthening of Fermat's last theorem for exponent 4, where the sum is only assumed to be a square. (Contributed by SN, 23-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β ((π΄β4) + (π΅β4)) β (πΆβ2)) | ||
Theorem | fltltc 40864 | (πΆβπ) is the largest term and therefore π΅ < πΆ. (Contributed by Steven Nguyen, 22-Aug-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β (β€β₯β3)) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) β β’ (π β π΅ < πΆ) | ||
Theorem | fltnltalem 40865 | Lemma for fltnlta 40866. A lower bound for π΄ based on pwdif 15687. (Contributed by Steven Nguyen, 22-Aug-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β (β€β₯β3)) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) β β’ (π β ((πΆ β π΅) Β· ((πΆβ(π β 1)) + ((π β 1) Β· (π΅β(π β 1))))) < (π΄βπ)) | ||
Theorem | fltnlta 40866 | In a Fermat counterexample, the exponent π is less than all three numbers (π΄, π΅, and πΆ). Note that π΄ < π΅ (hypothesis) and π΅ < πΆ (fltltc 40864). See https://youtu.be/EymVXkPWxyc 40864 for an outline. (Contributed by SN, 24-Aug-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β (β€β₯β3)) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) & β’ (π β π΄ < π΅) β β’ (π β π < π΄) | ||
Theorem | binom2d 40867 | Deduction form of binom2. (Contributed by Igor Ieskov, 14-Dec-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β ((π΄ + π΅)β2) = (((π΄β2) + (2 Β· (π΄ Β· π΅))) + (π΅β2))) | ||
Theorem | cu3addd 40868 | Cube of sum of three numbers. (Contributed by Igor Ieskov, 14-Dec-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β (((π΄ + π΅) + πΆ)β3) = (((((π΄β3) + (3 Β· ((π΄β2) Β· π΅))) + ((3 Β· (π΄ Β· (π΅β2))) + (π΅β3))) + (((3 Β· ((π΄β2) Β· πΆ)) + (((3 Β· 2) Β· (π΄ Β· π΅)) Β· πΆ)) + (3 Β· ((π΅β2) Β· πΆ)))) + (((3 Β· (π΄ Β· (πΆβ2))) + (3 Β· (π΅ Β· (πΆβ2)))) + (πΆβ3)))) | ||
Theorem | sqnegd 40869 | The square of the negative of a number. (Contributed by Igor Ieskov, 21-Jan-2024.) |
β’ (π β π΄ β β) β β’ (π β (-π΄β2) = (π΄β2)) | ||
Theorem | negexpidd 40870 | The sum of a real number to the power of N and the negative of the number to the power of N equals zero if N is a nonnegative odd integer. (Contributed by Igor Ieskov, 21-Jan-2024.) |
β’ (π β π΄ β β) & β’ (π β π β β0) & β’ (π β Β¬ 2 β₯ π) β β’ (π β ((π΄βπ) + (-π΄βπ)) = 0) | ||
Theorem | rexlimdv3d 40871* | An extended version of rexlimdvv 3202 to include three set variables. (Contributed by Igor Ieskov, 21-Jan-2024.) |
β’ (π β ((π₯ β π΄ β§ π¦ β π΅ β§ π§ β πΆ) β (π β π))) β β’ (π β (βπ₯ β π΄ βπ¦ β π΅ βπ§ β πΆ π β π)) | ||
Theorem | 3cubeslem1 40872 | Lemma for 3cubes 40878. (Contributed by Igor Ieskov, 22-Jan-2024.) |
β’ (π β π΄ β β) β β’ (π β 0 < (((π΄ + 1)β2) β π΄)) | ||
Theorem | 3cubeslem2 40873 | Lemma for 3cubes 40878. Used to show that the denominators in 3cubeslem4 40877 are nonzero. (Contributed by Igor Ieskov, 22-Jan-2024.) |
β’ (π β π΄ β β) β β’ (π β Β¬ ((((3β3) Β· (π΄β2)) + ((3β2) Β· π΄)) + 3) = 0) | ||
Theorem | 3cubeslem3l 40874 | Lemma for 3cubes 40878. (Contributed by Igor Ieskov, 22-Jan-2024.) |
β’ (π β π΄ β β) β β’ (π β (π΄ Β· (((((3β3) Β· (π΄β2)) + ((3β2) Β· π΄)) + 3)β3)) = (((π΄β7) Β· (3β9)) + (((π΄β6) Β· (3β9)) + (((π΄β5) Β· ((3β8) + (3β8))) + (((π΄β4) Β· (((3β7) Β· 2) + (3β6))) + (((π΄β3) Β· ((3β6) + (3β6))) + (((π΄β2) Β· (3β5)) + (π΄ Β· (3β3))))))))) | ||
Theorem | 3cubeslem3r 40875 | Lemma for 3cubes 40878. (Contributed by Igor Ieskov, 22-Jan-2024.) |
β’ (π β π΄ β β) β β’ (π β ((((((3β3) Β· (π΄β3)) β 1)β3) + (((-((3β3) Β· (π΄β3)) + ((3β2) Β· π΄)) + 1)β3)) + ((((3β3) Β· (π΄β2)) + ((3β2) Β· π΄))β3)) = (((π΄β7) Β· (3β9)) + (((π΄β6) Β· (3β9)) + (((π΄β5) Β· ((3β8) + (3β8))) + (((π΄β4) Β· (((3β7) Β· 2) + (3β6))) + (((π΄β3) Β· ((3β6) + (3β6))) + (((π΄β2) Β· (3β5)) + (π΄ Β· (3β3))))))))) | ||
Theorem | 3cubeslem3 40876 | Lemma for 3cubes 40878. (Contributed by Igor Ieskov, 22-Jan-2024.) |
β’ (π β π΄ β β) β β’ (π β (π΄ Β· (((((3β3) Β· (π΄β2)) + ((3β2) Β· π΄)) + 3)β3)) = ((((((3β3) Β· (π΄β3)) β 1)β3) + (((-((3β3) Β· (π΄β3)) + ((3β2) Β· π΄)) + 1)β3)) + ((((3β3) Β· (π΄β2)) + ((3β2) Β· π΄))β3))) | ||
Theorem | 3cubeslem4 40877 | Lemma for 3cubes 40878. This is Ryley's explicit formula for decomposing a rational π΄ into a sum of three rational cubes. (Contributed by Igor Ieskov, 22-Jan-2024.) |
β’ (π β π΄ β β) β β’ (π β π΄ = (((((((3β3) Β· (π΄β3)) β 1) / ((((3β3) Β· (π΄β2)) + ((3β2) Β· π΄)) + 3))β3) + ((((-((3β3) Β· (π΄β3)) + ((3β2) Β· π΄)) + 1) / ((((3β3) Β· (π΄β2)) + ((3β2) Β· π΄)) + 3))β3)) + (((((3β3) Β· (π΄β2)) + ((3β2) Β· π΄)) / ((((3β3) Β· (π΄β2)) + ((3β2) Β· π΄)) + 3))β3))) | ||
Theorem | 3cubes 40878* | Every rational number is a sum of three rational cubes. See S. Ryley, The Ladies' Diary 122 (1825), 35. (Contributed by Igor Ieskov, 22-Jan-2024.) |
β’ (π΄ β β β βπ β β βπ β β βπ β β π΄ = (((πβ3) + (πβ3)) + (πβ3))) | ||
Theorem | rntrclfvOAI 40879 | The range of the transitive closure is equal to the range of the relation. (Contributed by OpenAI, 7-Jul-2020.) |
β’ (π β π β ran (t+βπ ) = ran π ) | ||
Theorem | moxfr 40880* | Transfer at-most-one between related expressions. (Contributed by Stefan O'Rear, 12-Feb-2015.) |
β’ π΄ β V & β’ β!π¦ π₯ = π΄ & β’ (π₯ = π΄ β (π β π)) β β’ (β*π₯π β β*π¦π) | ||
Theorem | imaiinfv 40881* | Indexed intersection of an image. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ ((πΉ Fn π΄ β§ π΅ β π΄) β β© π₯ β π΅ (πΉβπ₯) = β© (πΉ β π΅)) | ||
Theorem | elrfi 40882* | Elementhood in a set of relative finite intersections. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ ((π΅ β π β§ πΆ β π« π΅) β (π΄ β (fiβ({π΅} βͺ πΆ)) β βπ£ β (π« πΆ β© Fin)π΄ = (π΅ β© β© π£))) | ||
Theorem | elrfirn 40883* | Elementhood in a set of relative finite intersections of an indexed family of sets. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ ((π΅ β π β§ πΉ:πΌβΆπ« π΅) β (π΄ β (fiβ({π΅} βͺ ran πΉ)) β βπ£ β (π« πΌ β© Fin)π΄ = (π΅ β© β© π¦ β π£ (πΉβπ¦)))) | ||
Theorem | elrfirn2 40884* | Elementhood in a set of relative finite intersections of an indexed family of sets (implicit). (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ ((π΅ β π β§ βπ¦ β πΌ πΆ β π΅) β (π΄ β (fiβ({π΅} βͺ ran (π¦ β πΌ β¦ πΆ))) β βπ£ β (π« πΌ β© Fin)π΄ = (π΅ β© β© π¦ β π£ πΆ))) | ||
Theorem | cmpfiiin 40885* | In a compact topology, a system of closed sets with nonempty finite intersections has a nonempty intersection. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ π = βͺ π½ & β’ (π β π½ β Comp) & β’ ((π β§ π β πΌ) β π β (Clsdβπ½)) & β’ ((π β§ (π β πΌ β§ π β Fin)) β (π β© β© π β π π) β β ) β β’ (π β (π β© β© π β πΌ π) β β ) | ||
Theorem | ismrcd1 40886* | Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 17431), isotone (satisfies mrcss 17430), and idempotent (satisfies mrcidm 17433) has a collection of fixed points which is a Moore collection, and itself is the closure operator for that collection. This can be taken as an alternate definition for the closure operators. This is the first half, ismrcd2 40887 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ (π β π΅ β π) & β’ (π β πΉ:π« π΅βΆπ« π΅) & β’ ((π β§ π₯ β π΅) β π₯ β (πΉβπ₯)) & β’ ((π β§ π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) & β’ ((π β§ π₯ β π΅) β (πΉβ(πΉβπ₯)) = (πΉβπ₯)) β β’ (π β dom (πΉ β© I ) β (Mooreβπ΅)) | ||
Theorem | ismrcd2 40887* | Second half of ismrcd1 40886. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ (π β π΅ β π) & β’ (π β πΉ:π« π΅βΆπ« π΅) & β’ ((π β§ π₯ β π΅) β π₯ β (πΉβπ₯)) & β’ ((π β§ π₯ β π΅ β§ π¦ β π₯) β (πΉβπ¦) β (πΉβπ₯)) & β’ ((π β§ π₯ β π΅) β (πΉβ(πΉβπ₯)) = (πΉβπ₯)) β β’ (π β πΉ = (mrClsβdom (πΉ β© I ))) | ||
Theorem | istopclsd 40888* | A closure function which satisfies sscls 22329, clsidm 22340, cls0 22353, and clsun 34695 defines a (unique) topology which it is the closure function on. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ (π β π΅ β π) & β’ (π β πΉ:π« π΅βΆπ« π΅) & β’ ((π β§ π₯ β π΅) β π₯ β (πΉβπ₯)) & β’ ((π β§ π₯ β π΅) β (πΉβ(πΉβπ₯)) = (πΉβπ₯)) & β’ (π β (πΉββ ) = β ) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (πΉβ(π₯ βͺ π¦)) = ((πΉβπ₯) βͺ (πΉβπ¦))) & β’ π½ = {π§ β π« π΅ β£ (πΉβ(π΅ β π§)) = (π΅ β π§)} β β’ (π β (π½ β (TopOnβπ΅) β§ (clsβπ½) = πΉ)) | ||
Theorem | ismrc 40889* | A function is a Moore closure operator iff it satisfies mrcssid 17431, mrcss 17430, and mrcidm 17433. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
β’ (πΉ β (mrCls β (Mooreβπ΅)) β (π΅ β V β§ πΉ:π« π΅βΆπ« π΅ β§ βπ₯βπ¦((π₯ β π΅ β§ π¦ β π₯) β (π₯ β (πΉβπ₯) β§ (πΉβπ¦) β (πΉβπ₯) β§ (πΉβ(πΉβπ₯)) = (πΉβπ₯))))) | ||
Syntax | cnacs 40890 | Class of Noetherian closure systems. |
class NoeACS | ||
Definition | df-nacs 40891* | Define a closure system of Noetherian type (not standard terminology) as an algebraic system where all closed sets are finitely generated. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ NoeACS = (π₯ β V β¦ {π β (ACSβπ₯) β£ βπ β π βπ β (π« π₯ β© Fin)π = ((mrClsβπ)βπ)}) | ||
Theorem | isnacs 40892* | Expand definition of Noetherian-type closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ (πΆ β (NoeACSβπ) β (πΆ β (ACSβπ) β§ βπ β πΆ βπ β (π« π β© Fin)π = (πΉβπ))) | ||
Theorem | nacsfg 40893* | In a Noetherian-type closure system, all closed sets are finitely generated. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (NoeACSβπ) β§ π β πΆ) β βπ β (π« π β© Fin)π = (πΉβπ)) | ||
Theorem | isnacs2 40894 | Express Noetherian-type closure system with fewer quantifiers. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ (πΆ β (NoeACSβπ) β (πΆ β (ACSβπ) β§ (πΉ β (π« π β© Fin)) = πΆ)) | ||
Theorem | mrefg2 40895* | Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ (πΆ β (Mooreβπ) β (βπ β (π« π β© Fin)π = (πΉβπ) β βπ β (π« π β© Fin)π = (πΉβπ))) | ||
Theorem | mrefg3 40896* | Slight variation on finite generation for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ πΉ = (mrClsβπΆ) β β’ ((πΆ β (Mooreβπ) β§ π β πΆ) β (βπ β (π« π β© Fin)π = (πΉβπ) β βπ β (π« π β© Fin)π β (πΉβπ))) | ||
Theorem | nacsacs 40897 | A closure system of Noetherian type is algebraic. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ (πΆ β (NoeACSβπ) β πΆ β (ACSβπ)) | ||
Theorem | isnacs3 40898* | A choice-free order equivalent to the Noetherian condition on a closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ (πΆ β (NoeACSβπ) β (πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π β π ))) | ||
Theorem | incssnn0 40899* | Transitivity induction of subsets, lemma for nacsfix 40900. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ ((βπ₯ β β0 (πΉβπ₯) β (πΉβ(π₯ + 1)) β§ π΄ β β0 β§ π΅ β (β€β₯βπ΄)) β (πΉβπ΄) β (πΉβπ΅)) | ||
Theorem | nacsfix 40900* | An increasing sequence of closed sets in a Noetherian-type closure system eventually fixates. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0 (πΉβπ₯) β (πΉβ(π₯ + 1))) β βπ¦ β β0 βπ§ β (β€β₯βπ¦)(πΉβπ§) = (πΉβπ¦)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |