![]() |
Metamath
Proof Explorer Theorem List (p. 417 of 480) | < 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: | ![]() (1-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sn-subeu 41601* | negeu 11454 without ax-mulcom 11176 and complex number version of resubeu 41552. (Contributed by SN, 5-May-2024.) |
β’ ((π΄ β β β§ π΅ β β) β β!π₯ β β (π΄ + π₯) = π΅) | ||
Theorem | sn-subcl 41602 | subcl 11463 without ax-mulcom 11176. (Contributed by SN, 5-May-2024.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ β π΅) β β) | ||
Theorem | sn-subf 41603 | subf 11466 without ax-mulcom 11176. (Contributed by SN, 5-May-2024.) |
β’ β :(β Γ β)βΆβ | ||
Theorem | resubeqsub 41604 | Equivalence between real subtraction and subtraction. (Contributed by SN, 5-May-2024.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ ββ π΅) = (π΄ β π΅)) | ||
Theorem | subresre 41605 | Subtraction restricted to the reals. (Contributed by SN, 5-May-2024.) |
β’ ββ = ( β βΎ (β Γ β)) | ||
Theorem | addinvcom 41606 | A number commutes with its additive inverse. Compare remulinvcom 41607. (Contributed by SN, 5-May-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (π΄ + π΅) = 0) β β’ (π β (π΅ + π΄) = 0) | ||
Theorem | remulinvcom 41607 | A left multiplicative inverse is a right multiplicative inverse. Proven without ax-mulcom 11176. (Contributed by SN, 5-Feb-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (π΄ Β· π΅) = 1) β β’ (π β (π΅ Β· π΄) = 1) | ||
Theorem | remullid 41608 | Commuted version of ax-1rid 11182 without ax-mulcom 11176. (Contributed by SN, 5-Feb-2024.) |
β’ (π΄ β β β (1 Β· π΄) = π΄) | ||
Theorem | sn-1ticom 41609 | Lemma for sn-mullid 41610 and it1ei 41611. (Contributed by SN, 27-May-2024.) |
β’ (1 Β· i) = (i Β· 1) | ||
Theorem | sn-mullid 41610 | mullid 11217 without ax-mulcom 11176. (Contributed by SN, 27-May-2024.) |
β’ (π΄ β β β (1 Β· π΄) = π΄) | ||
Theorem | it1ei 41611 | 1 is a multiplicative identity for i (see sn-mullid 41610 for commuted version). (Contributed by SN, 1-Jun-2024.) |
β’ (i Β· 1) = i | ||
Theorem | ipiiie0 41612 | The multiplicative inverse of i (per i4 14172) is also its additive inverse. (Contributed by SN, 30-Jun-2024.) |
β’ (i + (i Β· (i Β· i))) = 0 | ||
Theorem | remulcand 41613 | Commuted version of remulcan2d 41479 without ax-mulcom 11176. (Contributed by SN, 21-Feb-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β πΆ β 0) β β’ (π β ((πΆ Β· π΄) = (πΆ Β· π΅) β π΄ = π΅)) | ||
Theorem | sn-0tie0 41614 | Lemma for sn-mul02 41615. Commuted version of sn-it0e0 41590. (Contributed by SN, 30-Jun-2024.) |
β’ (0 Β· i) = 0 | ||
Theorem | sn-mul02 41615 | mul02 11396 without ax-mulcom 11176. See https://github.com/icecream17/Stuff/blob/main/math/0A%3D0.md 11176 for an outline. (Contributed by SN, 30-Jun-2024.) |
β’ (π΄ β β β (0 Β· π΄) = 0) | ||
Theorem | sn-ltaddpos 41616 | ltaddpos 11708 without ax-mulcom 11176. (Contributed by SN, 13-Feb-2024.) |
β’ ((π΄ β β β§ π΅ β β) β (0 < π΄ β π΅ < (π΅ + π΄))) | ||
Theorem | sn-ltaddneg 41617 | ltaddneg 11433 without ax-mulcom 11176. (Contributed by SN, 25-Jan-2025.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ < 0 β (π΅ + π΄) < π΅)) | ||
Theorem | reposdif 41618 | Comparison of two numbers whose difference is positive. Compare posdif 11711. (Contributed by SN, 13-Feb-2024.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ < π΅ β 0 < (π΅ ββ π΄))) | ||
Theorem | relt0neg1 41619 | Comparison of a real and its negative to zero. Compare lt0neg1 11724. (Contributed by SN, 13-Feb-2024.) |
β’ (π΄ β β β (π΄ < 0 β 0 < (0 ββ π΄))) | ||
Theorem | relt0neg2 41620 | Comparison of a real and its negative to zero. Compare lt0neg2 11725. (Contributed by SN, 13-Feb-2024.) |
β’ (π΄ β β β (0 < π΄ β (0 ββ π΄) < 0)) | ||
Theorem | sn-addlt0d 41621 | The sum of negative numbers is negative. (Contributed by SN, 25-Jan-2025.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < 0) & β’ (π β π΅ < 0) β β’ (π β (π΄ + π΅) < 0) | ||
Theorem | sn-addgt0d 41622 | The sum of positive numbers is positive. Proof of addgt0d 11793 without ax-mulcom 11176. (Contributed by SN, 25-Jan-2025.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β 0 < π΄) & β’ (π β 0 < π΅) β β’ (π β 0 < (π΄ + π΅)) | ||
Theorem | sn-nnne0 41623 | nnne0 12250 without ax-mulcom 11176. (Contributed by SN, 25-Jan-2025.) |
β’ (π΄ β β β π΄ β 0) | ||
Theorem | reelznn0nn 41624 | elznn0nn 12576 restated using df-resub 41541. (Contributed by SN, 25-Jan-2025.) |
β’ (π β β€ β (π β β0 β¨ (π β β β§ (0 ββ π) β β))) | ||
Theorem | nn0addcom 41625 | Addition is commutative for nonnegative integers. Proven without ax-mulcom 11176. (Contributed by SN, 1-Feb-2025.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ + π΅) = (π΅ + π΄)) | ||
Theorem | zaddcomlem 41626 | Lemma for zaddcom 41627. (Contributed by SN, 1-Feb-2025.) |
β’ (((π΄ β β β§ (0 ββ π΄) β β) β§ π΅ β β0) β (π΄ + π΅) = (π΅ + π΄)) | ||
Theorem | zaddcom 41627 | Addition is commutative for integers. Proven without ax-mulcom 11176. (Contributed by SN, 25-Jan-2025.) |
β’ ((π΄ β β€ β§ π΅ β β€) β (π΄ + π΅) = (π΅ + π΄)) | ||
Theorem | renegmulnnass 41628 | Move multiplication by a natural number inside and outside negation. (Contributed by SN, 25-Jan-2025.) |
β’ (π β π΄ β β) & β’ (π β π β β) β β’ (π β ((0 ββ π΄) Β· π) = (0 ββ (π΄ Β· π))) | ||
Theorem | nn0mulcom 41629 | Multiplication is commutative for nonnegative integers. Proven without ax-mulcom 11176. (Contributed by SN, 25-Jan-2025.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ Β· π΅) = (π΅ Β· π΄)) | ||
Theorem | zmulcomlem 41630 | Lemma for zmulcom 41631. (Contributed by SN, 25-Jan-2025.) |
β’ (((π΄ β β β§ (0 ββ π΄) β β) β§ π΅ β β0) β (π΄ Β· π΅) = (π΅ Β· π΄)) | ||
Theorem | zmulcom 41631 | Multiplication is commutative for integers. Proven without ax-mulcom 11176. From this result and grpcominv1 41388, we can show that rationals commute under multiplication without using ax-mulcom 11176. (Contributed by SN, 25-Jan-2025.) |
β’ ((π΄ β β€ β§ π΅ β β€) β (π΄ Β· π΅) = (π΅ Β· π΄)) | ||
Theorem | mulgt0con1dlem 41632 | Lemma for mulgt0con1d 41633. Contraposes a positive deduction to a negative deduction. (Contributed by SN, 26-Jun-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (0 < π΄ β 0 < π΅)) & β’ (π β (π΄ = 0 β π΅ = 0)) β β’ (π β (π΅ < 0 β π΄ < 0)) | ||
Theorem | mulgt0con1d 41633 | Counterpart to mulgt0con2d 41634, though not a lemma of anything. This is the first use of ax-pre-mulgt0 11189. (Contributed by SN, 26-Jun-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β 0 < π΅) & β’ (π β (π΄ Β· π΅) < 0) β β’ (π β π΄ < 0) | ||
Theorem | mulgt0con2d 41634 | Lemma for mulgt0b2d 41635 and contrapositive of mulgt0 11295. (Contributed by SN, 26-Jun-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β 0 < π΄) & β’ (π β (π΄ Β· π΅) < 0) β β’ (π β π΅ < 0) | ||
Theorem | mulgt0b2d 41635 | Biconditional, deductive form of mulgt0 11295. The second factor is positive iff the product is. Note that the commuted form cannot be proven since resubdi 41571 does not have a commuted form. (Contributed by SN, 26-Jun-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β 0 < π΄) β β’ (π β (0 < π΅ β 0 < (π΄ Β· π΅))) | ||
Theorem | sn-ltmul2d 41636 | ltmul2d 13062 without ax-mulcom 11176. (Contributed by SN, 26-Jun-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β 0 < πΆ) β β’ (π β ((πΆ Β· π΄) < (πΆ Β· π΅) β π΄ < π΅)) | ||
Theorem | sn-0lt1 41637 | 0lt1 11740 without ax-mulcom 11176. (Contributed by SN, 13-Feb-2024.) |
β’ 0 < 1 | ||
Theorem | sn-ltp1 41638 | ltp1 12058 without ax-mulcom 11176. (Contributed by SN, 13-Feb-2024.) |
β’ (π΄ β β β π΄ < (π΄ + 1)) | ||
Theorem | reneg1lt0 41639 | Lemma for sn-inelr 41640. (Contributed by SN, 1-Jun-2024.) |
β’ (0 ββ 1) < 0 | ||
Theorem | sn-inelr 41640 | inelr 12206 without ax-mulcom 11176. (Contributed by SN, 1-Jun-2024.) |
β’ Β¬ i β β | ||
Theorem | itrere 41641 | i times a real is real iff the real is zero. (Contributed by SN, 27-Jun-2024.) |
β’ (π β β β ((i Β· π ) β β β π = 0)) | ||
Theorem | retire 41642 | Commuted version of itrere 41641. (Contributed by SN, 27-Jun-2024.) |
β’ (π β β β ((π Β· i) β β β π = 0)) | ||
Theorem | cnreeu 41643 | The reals in the expression given by cnre 11215 uniquely define a complex number. (Contributed by SN, 27-Jun-2024.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π‘ β β) & β’ (π β π’ β β) β β’ (π β ((π + (i Β· π )) = (π‘ + (i Β· π’)) β (π = π‘ β§ π = π’))) | ||
Theorem | sn-sup2 41644* | sup2 12174 with exactly the same proof except for using sn-ltp1 41638 instead of ltp1 12058, saving ax-mulcom 11176. (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 41645 | Extend class notation with the projective space function. |
class βπ£π π | ||
Definition | df-prjsp 41646* | 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, making equivalent rational multiples of real numbers). Compare df-lsatoms 38149. (Contributed by BJ and SN, 29-Apr-2023.) |
β’ βπ£π π = (π£ β LVec β¦ β¦((Baseβπ£) β {(0gβπ£)}) / πβ¦(π / {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ βπ β (Baseβ(Scalarβπ£))π₯ = (π( Β·π βπ£)π¦))})) | ||
Theorem | prjspval 41647* | 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 41648* | Utility theorem regarding the relation used in βπ£π π. (Contributed by Steven Nguyen, 29-Apr-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} β β’ (π βΌ π β ((π β π΅ β§ π β π΅) β§ βπ β πΎ π = (π Β· π))) | ||
Theorem | prjspertr 41649* | The relation in βπ£π π is transitive. (Contributed by Steven Nguyen, 1-May-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) β β’ ((π β LMod β§ (π βΌ π β§ π βΌ π)) β π βΌ π) | ||
Theorem | prjsperref 41650* | The relation in βπ£π π is reflexive. (Contributed by Steven Nguyen, 30-Apr-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) β β’ (π β LMod β (π β π΅ β π βΌ π)) | ||
Theorem | prjspersym 41651* | The relation in βπ£π π is symmetric. (Contributed by Steven Nguyen, 1-May-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) β β’ ((π β LVec β§ π βΌ π) β π βΌ π) | ||
Theorem | prjsper 41652* | The relation used to define βπ£π π is an equivalence relation. (Contributed by Steven Nguyen, 1-May-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) β β’ (π β LVec β βΌ Er π΅) | ||
Theorem | prjspreln0 41653* | 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 41654* | 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 41655* | Two vectors are equivalent iff their spans are equal. (Contributed by Steven Nguyen, 31-May-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LVec β§ (π β π΅ β§ π β π΅)) β (π βΌ π β (πβ{π}) = (πβ{π}))) | ||
Theorem | prjspeclsp 41656* | 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 41657* | Alternate definition of projective space. (Contributed by Steven Nguyen, 7-Jun-2023.) |
β’ 0 = (0gβπ) & β’ π΅ = ((Baseβπ) β { 0 }) & β’ π = (LSpanβπ) β β’ (π β LVec β (βπ£π πβπ) = βͺ π§ β π΅ {((πβ{π§}) β { 0 })}) | ||
Syntax | cprjspn 41658 | Extend class notation with the n-dimensional projective space function. |
class βπ£π πn | ||
Definition | df-prjspn 41659* | 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 25134. 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 41660 | Value of the n-dimensional projective space function. (Contributed by Steven Nguyen, 1-May-2023.) |
β’ ((π β β0 β§ πΎ β DivRing) β (πβπ£π πnπΎ) = (βπ£π πβ(πΎ freeLMod (0...π)))) | ||
Theorem | prjspnerlem 41661* | A lemma showing that the equivalence relation used in prjspnval2 41662 and the equivalence relation used in prjspval 41647 are equal, but only with the antecedent πΎ β DivRing. (Contributed by SN, 15-Jul-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β π π₯ = (π Β· π¦))} & β’ π = (πΎ freeLMod (0...π)) & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (BaseβπΎ) & β’ Β· = ( Β·π βπ) β β’ (πΎ β DivRing β βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β (Baseβ(Scalarβπ))π₯ = (π Β· π¦))}) | ||
Theorem | prjspnval2 41662* | 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 41663* | The relation used to define βπ£π π (and indirectly βπ£π πn through df-prjspn 41659) is an equivalence relation. This is a lemma that converts the equivalence relation used in results like prjspertr 41649 and prjspersym 41651 (see prjspnerlem 41661). Several theorems are covered in one thanks to the theorems around df-er 8705. (Contributed by SN, 14-Aug-2023.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β π π₯ = (π Β· π¦))} & β’ π = (πΎ freeLMod (0...π)) & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (BaseβπΎ) & β’ Β· = ( Β·π βπ) & β’ (π β πΎ β DivRing) β β’ (π β βΌ Er π΅) | ||
Theorem | prjspnvs 41664* | A nonzero multiple of a vector is equivalent to the vector. This converts the equivalence relation used in prjspvs 41654 (see prjspnerlem 41661). (Contributed by SN, 8-Aug-2024.) |
β’ βΌ = {β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β π π₯ = (π Β· π¦))} & β’ π = (πΎ freeLMod (0...π)) & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ π = (BaseβπΎ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπΎ) & β’ (π β πΎ β DivRing) & β’ (π β π β π΅) & β’ (π β πΆ β π) & β’ (π β πΆ β 0 ) β β’ (π β (πΆ Β· π) βΌ π) | ||
Theorem | prjspnssbas 41665 | 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 41666 | A projective point is nonempty. (Contributed by SN, 17-Jan-2025.) |
β’ π = (πβπ£π πnπΎ) & β’ π = (πΎ freeLMod (0...π)) & β’ π΅ = ((Baseβπ) β {(0gβπ)}) & β’ (π β π β β0) & β’ (π β πΎ β DivRing) & β’ (π β π΄ β π) β β’ (π β π΄ β β ) | ||
Theorem | 0prjspnlem 41667 | Lemma for 0prjspn 41672. 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 41668* | 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 41669* | 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 41670* | 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 41671* | 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 41672 | 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 41673 | Extend class notation with the projective curve function. |
class βπ£π πCrv | ||
Definition | df-prjcrv 41674* | 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 41474 and prjspvs 41654). (Contributed by SN, 23-Nov-2024.) |
β’ βπ£π πCrv = (π β β0, π β Field β¦ (π β βͺ ran ((0...π) mHomP π) β¦ {π β (πβπ£π πnπ) β£ ((((0...π) eval π)βπ) β π) = {(0gβπ)}})) | ||
Theorem | prjcrvfval 41675* | 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 41676* | 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 41677 | 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 41678* | 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 41679 | 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 41680 | 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 41681 | A counterexample for FLT does not exist for π = 0. (Contributed by SN, 20-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β β0) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) β β’ (π β π β β) | ||
Theorem | fltdvdsabdvdsc 41682 | Any factor of both π΄ and π΅ also divides πΆ. This establishes the validity of fltabcoprmex 41683. (Contributed by SN, 21-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β β) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) β β’ (π β (π΄ gcd π΅) β₯ πΆ) | ||
Theorem | fltabcoprmex 41683 | A counterexample to FLT implies a counterexample to FLT with π΄, π΅ (assigned to π΄ / (π΄ gcd π΅) and π΅ / (π΄ gcd π΅)) coprime (by divgcdcoprm0 16606). (Contributed by SN, 20-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β β0) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) β β’ (π β (((π΄ / (π΄ gcd π΅))βπ) + ((π΅ / (π΄ gcd π΅))βπ)) = ((πΆ / (π΄ gcd π΅))βπ)) | ||
Theorem | fltaccoprm 41684 | A counterexample to FLT with π΄, π΅ coprime also has π΄, πΆ coprime. (Contributed by SN, 20-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β β0) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) & β’ (π β (π΄ gcd π΅) = 1) β β’ (π β (π΄ gcd πΆ) = 1) | ||
Theorem | fltbccoprm 41685 | A counterexample to FLT with π΄, π΅ coprime also has π΅, πΆ coprime. Proven from fltaccoprm 41684 using commutativity of addition. (Contributed by SN, 20-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β β0) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) & β’ (π β (π΄ gcd π΅) = 1) β β’ (π β (π΅ gcd πΆ) = 1) | ||
Theorem | fltabcoprm 41686 | A counterexample to FLT with π΄, πΆ coprime also has π΄, π΅ coprime. Converse of fltaccoprm 41684. (Contributed by SN, 22-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β (π΄ gcd πΆ) = 1) & β’ (π β ((π΄β2) + (π΅β2)) = (πΆβ2)) β β’ (π β (π΄ gcd π΅) = 1) | ||
Theorem | infdesc 41687* | 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 41688 | If a counterexample to FLT exists, its addends are not equal. (Contributed by SN, 1-Jun-2023.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π β (β€β₯β2)) & β’ (π β ((π΄βπ) + (π΅βπ)) = (πΆβπ)) β β’ (π β π΄ β π΅) | ||
Theorem | flt4lem 41689 | Raising a number to the fourth power is equivalent to squaring it twice. (Contributed by SN, 21-Aug-2024.) |
β’ (π β π΄ β β) β β’ (π β (π΄β4) = ((π΄β2)β2)) | ||
Theorem | flt4lem1 41690 | Satisfy the antecedent used in several pythagtrip 16771 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 41691 | If π΄ is even, π΅ is odd. (Contributed by SN, 22-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β 2 β₯ π΄) & β’ (π β (π΄ gcd πΆ) = 1) & β’ (π β ((π΄β2) + (π΅β2)) = (πΆβ2)) β β’ (π β Β¬ 2 β₯ π΅) | ||
Theorem | flt4lem3 41692 | Equivalent to pythagtriplem4 16756. Show that πΆ + π΄ and πΆ β π΄ are coprime. (Contributed by SN, 22-Aug-2024.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β 2 β₯ π΄) & β’ (π β (π΄ gcd πΆ) = 1) & β’ (π β ((π΄β2) + (π΅β2)) = (πΆβ2)) β β’ (π β ((πΆ + π΄) gcd (πΆ β π΄)) = 1) | ||
Theorem | flt4lem4 41693 | 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 41694 | In the context of the lemmas of pythagtrip 16771, π and π are coprime. (Contributed by SN, 23-Aug-2024.) |
β’ π = (((ββ(πΆ + π΅)) + (ββ(πΆ β π΅))) / 2) & β’ π = (((ββ(πΆ + π΅)) β (ββ(πΆ β π΅))) / 2) β β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ ((π΄β2) + (π΅β2)) = (πΆβ2) β§ ((π΄ gcd π΅) = 1 β§ Β¬ 2 β₯ π΄)) β (π gcd π) = 1) | ||
Theorem | flt4lem5elem 41695 | Version of fltaccoprm 41684 and fltbccoprm 41685 where π is not squared. This can be proved in general for any polynomial in three variables: using prmdvdsncoprmbd 16667, dvds2addd 16239, and prmdvdsexp 16656, 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 41696 | 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 41697 | 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 41698 | 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 41699 | 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 41700 | Satisfy the hypotheses of flt4lem4 41693. (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) β β))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |