![]() |
Metamath
Proof Explorer Theorem List (p. 420 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-itgo 41901* | A complex number is said to be integral over a subset if it is the root of a monic polynomial with coefficients from the subset. This definition is typically not used for fields but it works there, see aaitgo 41904. This definition could work for subsets of an arbitrary ring with a more general definition of polynomials. TODO: use Monic. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ IntgOver = (π β π« β β¦ {π₯ β β β£ βπ β (Polyβπ )((πβπ₯) = 0 β§ ((coeffβπ)β(degβπ)) = 1)}) | ||
Definition | df-za 41902 | Define an algebraic integer as a complex number which is the root of a monic integer polynomial. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ β€ = (IntgOverββ€) | ||
Theorem | itgoval 41903* | Value of the integral-over function. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ (π β β β (IntgOverβπ) = {π₯ β β β£ βπ β (Polyβπ)((πβπ₯) = 0 β§ ((coeffβπ)β(degβπ)) = 1)}) | ||
Theorem | aaitgo 41904 | The standard algebraic numbers πΈ are generated by IntgOver. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ πΈ = (IntgOverββ) | ||
Theorem | itgoss 41905 | An integral element is integral over a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ ((π β π β§ π β β) β (IntgOverβπ) β (IntgOverβπ)) | ||
Theorem | itgocn 41906 | All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ (IntgOverβπ) β β | ||
Theorem | cnsrexpcl 41907 | Exponentiation is closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β (SubRingββfld)) & β’ (π β π β π) & β’ (π β π β β0) β β’ (π β (πβπ) β π) | ||
Theorem | fsumcnsrcl 41908* | Finite sums are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β (SubRingββfld)) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β π) β β’ (π β Ξ£π β π΄ π΅ β π) | ||
Theorem | cnsrplycl 41909 | Polynomials are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β (SubRingββfld)) & β’ (π β π β (PolyβπΆ)) & β’ (π β π β π) & β’ (π β πΆ β π) β β’ (π β (πβπ) β π) | ||
Theorem | rgspnval 41910* | Value of the ring-span of a set of elements in a ring. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
β’ (π β π β Ring) & β’ (π β π΅ = (Baseβπ )) & β’ (π β π΄ β π΅) & β’ (π β π = (RingSpanβπ )) & β’ (π β π = (πβπ΄)) β β’ (π β π = β© {π‘ β (SubRingβπ ) β£ π΄ β π‘}) | ||
Theorem | rgspncl 41911 | The ring-span of a set is a subring. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
β’ (π β π β Ring) & β’ (π β π΅ = (Baseβπ )) & β’ (π β π΄ β π΅) & β’ (π β π = (RingSpanβπ )) & β’ (π β π = (πβπ΄)) β β’ (π β π β (SubRingβπ )) | ||
Theorem | rgspnssid 41912 | The ring-span of a set contains the set. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β Ring) & β’ (π β π΅ = (Baseβπ )) & β’ (π β π΄ β π΅) & β’ (π β π = (RingSpanβπ )) & β’ (π β π = (πβπ΄)) β β’ (π β π΄ β π) | ||
Theorem | rgspnmin 41913 | The ring-span is contained in all subspaces which contain all the generators. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β Ring) & β’ (π β π΅ = (Baseβπ )) & β’ (π β π΄ β π΅) & β’ (π β π = (RingSpanβπ )) & β’ (π β π = (πβπ΄)) & β’ (π β π β (SubRingβπ )) & β’ (π β π΄ β π) β β’ (π β π β π) | ||
Theorem | rgspnid 41914 | The span of a subring is itself. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β Ring) & β’ (π β π΄ β (SubRingβπ )) & β’ (π β π = ((RingSpanβπ )βπ΄)) β β’ (π β π = π΄) | ||
Theorem | rngunsnply 41915* | Adjoining one element to a ring results in a set of polynomial evaluations. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π΅ β (SubRingββfld)) & β’ (π β π β β) & β’ (π β π = ((RingSpanββfld)β(π΅ βͺ {π}))) β β’ (π β (π β π β βπ β (Polyβπ΅)π = (πβπ))) | ||
Theorem | flcidc 41916* | Finite linear combinations with an indicator function. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ (π β πΉ = (π β π β¦ if(π = πΎ, 1, 0))) & β’ (π β π β Fin) & β’ (π β πΎ β π) & β’ ((π β§ π β π) β π΅ β β) β β’ (π β Ξ£π β π ((πΉβπ) Β· π΅) = β¦πΎ / πβ¦π΅) | ||
Syntax | cmend 41917 | Syntax for module endomorphism algebra. |
class MEndo | ||
Definition | df-mend 41918* | Define the endomorphism algebra of a module. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
β’ MEndo = (π β V β¦ β¦(π LMHom π) / πβ¦({β¨(Baseβndx), πβ©, β¨(+gβndx), (π₯ β π, π¦ β π β¦ (π₯ βf (+gβπ)π¦))β©, β¨(.rβndx), (π₯ β π, π¦ β π β¦ (π₯ β π¦))β©} βͺ {β¨(Scalarβndx), (Scalarβπ)β©, β¨( Β·π βndx), (π₯ β (Baseβ(Scalarβπ)), π¦ β π β¦ (((Baseβπ) Γ {π₯}) βf ( Β·π βπ)π¦))β©})) | ||
Theorem | algstr 41919 | Lemma to shorten proofs of algbase 41920 through algvsca 41924. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ π΄ Struct β¨1, 6β© | ||
Theorem | algbase 41920 | The base set of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ (π΅ β π β π΅ = (Baseβπ΄)) | ||
Theorem | algaddg 41921 | The additive operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ ( + β π β + = (+gβπ΄)) | ||
Theorem | algmulr 41922 | The multiplicative operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ ( Γ β π β Γ = (.rβπ΄)) | ||
Theorem | algsca 41923 | The set of scalars of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ (π β π β π = (Scalarβπ΄)) | ||
Theorem | algvsca 41924 | The scalar product operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π΄ = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©}) β β’ ( Β· β π β Β· = ( Β·π βπ΄)) | ||
Theorem | mendval 41925* | Value of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
β’ π΅ = (π LMHom π) & β’ + = (π₯ β π΅, π¦ β π΅ β¦ (π₯ βf (+gβπ)π¦)) & β’ Γ = (π₯ β π΅, π¦ β π΅ β¦ (π₯ β π¦)) & β’ π = (Scalarβπ) & β’ Β· = (π₯ β (Baseβπ), π¦ β π΅ β¦ (((Baseβπ) Γ {π₯}) βf ( Β·π βπ)π¦)) β β’ (π β π β (MEndoβπ) = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Γ β©} βͺ {β¨(Scalarβndx), πβ©, β¨( Β·π βndx), Β· β©})) | ||
Theorem | mendbas 41926 | Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
β’ π΄ = (MEndoβπ) β β’ (π LMHom π) = (Baseβπ΄) | ||
Theorem | mendplusgfval 41927* | Addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.) |
β’ π΄ = (MEndoβπ) & β’ π΅ = (Baseβπ΄) & β’ + = (+gβπ) β β’ (+gβπ΄) = (π₯ β π΅, π¦ β π΅ β¦ (π₯ βf + π¦)) | ||
Theorem | mendplusg 41928 | A specific addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π΅ = (Baseβπ΄) & β’ + = (+gβπ) & β’ β = (+gβπ΄) β β’ ((π β π΅ β§ π β π΅) β (π β π) = (π βf + π)) | ||
Theorem | mendmulrfval 41929* | Multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.) |
β’ π΄ = (MEndoβπ) & β’ π΅ = (Baseβπ΄) β β’ (.rβπ΄) = (π₯ β π΅, π¦ β π΅ β¦ (π₯ β π¦)) | ||
Theorem | mendmulr 41930 | A specific multiplication in the module endormoprhism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = (.rβπ΄) β β’ ((π β π΅ β§ π β π΅) β (π Β· π) = (π β π)) | ||
Theorem | mendsca 41931 | The module endomorphism algebra has the same scalars as the underlying module. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.) |
β’ π΄ = (MEndoβπ) & β’ π = (Scalarβπ) β β’ π = (Scalarβπ΄) | ||
Theorem | mendvscafval 41932* | Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) (Proof shortened by AV, 31-Oct-2024.) |
β’ π΄ = (MEndoβπ) & β’ Β· = ( Β·π βπ) & β’ π΅ = (Baseβπ΄) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) & β’ πΈ = (Baseβπ) β β’ ( Β·π βπ΄) = (π₯ β πΎ, π¦ β π΅ β¦ ((πΈ Γ {π₯}) βf Β· π¦)) | ||
Theorem | mendvsca 41933 | A specific scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ Β· = ( Β·π βπ) & β’ π΅ = (Baseβπ΄) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ) & β’ πΈ = (Baseβπ) & β’ β = ( Β·π βπ΄) β β’ ((π β πΎ β§ π β π΅) β (π β π) = ((πΈ Γ {π}) βf Β· π)) | ||
Theorem | mendring 41934 | The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΄ = (MEndoβπ) β β’ (π β LMod β π΄ β Ring) | ||
Theorem | mendlmod 41935 | The module endomorphism algebra is a left module. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π = (Scalarβπ) β β’ ((π β LMod β§ π β CRing) β π΄ β LMod) | ||
Theorem | mendassa 41936 | The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π = (Scalarβπ) β β’ ((π β LMod β§ π β CRing) β π΄ β AssAlg) | ||
Theorem | idomrootle 41937* | No element of an integral domain can have more than π π-th roots. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
β’ π΅ = (Baseβπ ) & β’ β = (.gβ(mulGrpβπ )) β β’ ((π β IDomn β§ π β π΅ β§ π β β) β (β―β{π¦ β π΅ β£ (π β π¦) = π}) β€ π) | ||
Theorem | idomodle 41938* | Limit on the number of π-th roots of unity in an integral domain. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ πΊ = ((mulGrpβπ ) βΎs (Unitβπ )) & β’ π΅ = (BaseβπΊ) & β’ π = (odβπΊ) β β’ ((π β IDomn β§ π β β) β (β―β{π₯ β π΅ β£ (πβπ₯) β₯ π}) β€ π) | ||
Theorem | fiuneneq 41939 | Two finite sets of equal size have a union of the same size iff they were equal. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ ((π΄ β π΅ β§ π΄ β Fin) β ((π΄ βͺ π΅) β π΄ β π΄ = π΅)) | ||
Theorem | idomsubgmo 41940* | The units of an integral domain have at most one subgroup of any single finite cardinality. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Revised by NM, 17-Jun-2017.) |
β’ πΊ = ((mulGrpβπ ) βΎs (Unitβπ )) β β’ ((π β IDomn β§ π β β) β β*π¦ β (SubGrpβπΊ)(β―βπ¦) = π) | ||
Theorem | proot1mul 41941 | Any primitive π-th root of unity is a multiple of any other. (Contributed by Stefan O'Rear, 2-Nov-2015.) |
β’ πΊ = ((mulGrpβπ ) βΎs (Unitβπ )) & β’ π = (odβπΊ) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ (((π β IDomn β§ π β β) β§ (π β (β‘π β {π}) β§ π β (β‘π β {π}))) β π β (πΎβ{π})) | ||
Theorem | proot1hash 41942 | If an integral domain has a primitive π-th root of unity, it has exactly (Οβπ) of them. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ πΊ = ((mulGrpβπ ) βΎs (Unitβπ )) & β’ π = (odβπΊ) β β’ ((π β IDomn β§ π β β β§ π β (β‘π β {π})) β (β―β(β‘π β {π})) = (Οβπ)) | ||
Theorem | proot1ex 41943 | The complex field has primitive π-th roots of unity for all π. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ πΊ = ((mulGrpββfld) βΎs (β β {0})) & β’ π = (odβπΊ) β β’ (π β β β (-1βπ(2 / π)) β (β‘π β {π})) | ||
Syntax | ccytp 41944 | Syntax for the sequence of cyclotomic polynomials. |
class CytP | ||
Definition | df-cytp 41945* | The Nth cyclotomic polynomial is the polynomial which has as its zeros precisely the primitive Nth roots of unity. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ CytP = (π β β β¦ ((mulGrpβ(Poly1ββfld)) Ξ£g (π β (β‘(odβ((mulGrpββfld) βΎs (β β {0}))) β {π}) β¦ ((var1ββfld)(-gβ(Poly1ββfld))((algScβ(Poly1ββfld))βπ))))) | ||
Theorem | isdomn3 41946 | Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (mulGrpβπ ) β β’ (π β Domn β (π β Ring β§ (π΅ β { 0 }) β (SubMndβπ))) | ||
Theorem | mon1pid 41947 | Monicity and degree of the unit polynomial. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π = (Poly1βπ ) & β’ 1 = (1rβπ) & β’ π = (Monic1pβπ ) & β’ π· = ( deg1 βπ ) β β’ (π β NzRing β ( 1 β π β§ (π·β 1 ) = 0)) | ||
Theorem | mon1psubm 41948 | Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π = (Poly1βπ ) & β’ π = (Monic1pβπ ) & β’ π = (mulGrpβπ) β β’ (π β NzRing β π β (SubMndβπ)) | ||
Theorem | deg1mhm 41949 | Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π· = ( deg1 βπ ) & β’ π΅ = (Baseβπ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π = ((mulGrpβπ) βΎs (π΅ β { 0 })) & β’ π = (βfld βΎs β0) β β’ (π β Domn β (π· βΎ (π΅ β { 0 })) β (π MndHom π)) | ||
Theorem | cytpfn 41950 | Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ CytP Fn β | ||
Theorem | cytpval 41951* | Substitutions for the Nth cyclotomic polynomial. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π = ((mulGrpββfld) βΎs (β β {0})) & β’ π = (odβπ) & β’ π = (Poly1ββfld) & β’ π = (var1ββfld) & β’ π = (mulGrpβπ) & β’ β = (-gβπ) & β’ π΄ = (algScβπ) β β’ (π β β β (CytPβπ) = (π Ξ£g (π β (β‘π β {π}) β¦ (π β (π΄βπ))))) | ||
Theorem | fgraphopab 41952* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (πΉ:π΄βΆπ΅ β πΉ = {β¨π, πβ© β£ ((π β π΄ β§ π β π΅) β§ (πΉβπ) = π)}) | ||
Theorem | fgraphxp 41953* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (πΉ:π΄βΆπ΅ β πΉ = {π₯ β (π΄ Γ π΅) β£ (πΉβ(1st βπ₯)) = (2nd βπ₯)}) | ||
Theorem | hausgraph 41954 | The graph of a continuous function into a Hausdorff space is closed. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ ((πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β πΉ β (Clsdβ(π½ Γt πΎ))) | ||
Syntax | ctopsep 41955 | The class of separable topologies. |
class TopSep | ||
Syntax | ctoplnd 41956 | The class of LindelΓΆf topologies. |
class TopLnd | ||
Definition | df-topsep 41957* | A topology is separable iff it has a countable dense subset. (Contributed by Stefan O'Rear, 8-Jan-2015.) |
β’ TopSep = {π β Top β£ βπ₯ β π« βͺ π(π₯ βΌ Ο β§ ((clsβπ)βπ₯) = βͺ π)} | ||
Definition | df-toplnd 41958* | A topology is LindelΓΆf iff every open cover has a countable subcover. (Contributed by Stefan O'Rear, 8-Jan-2015.) |
β’ TopLnd = {π₯ β Top β£ βπ¦ β π« π₯(βͺ π₯ = βͺ π¦ β βπ§ β π« π₯(π§ βΌ Ο β§ βͺ π₯ = βͺ π§))} | ||
Theorem | r1sssucd 41959 | Deductive form of r1sssuc 9778. (Contributed by Noam Pasman, 19-Jan-2025.) |
β’ (π β π΄ β On) β β’ (π β (π 1βπ΄) β (π 1βsuc π΄)) | ||
Theorem | iocunico 41960 | Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ < π΅ β§ π΅ < πΆ)) β ((π΄(,]π΅) βͺ (π΅[,)πΆ)) = (π΄(,)πΆ)) | ||
Theorem | iocinico 41961 | The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ < π΅ β§ π΅ < πΆ)) β ((π΄(,]π΅) β© (π΅[,)πΆ)) = {π΅}) | ||
Theorem | iocmbl 41962 | An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.) |
β’ ((π΄ β β* β§ π΅ β β) β (π΄(,]π΅) β dom vol) | ||
Theorem | cnioobibld 41963* | A bounded, continuous function on an open bounded interval is integrable. The function must be bounded. For a counterexample, consider πΉ = (π₯ β (0(,)1) β¦ (1 / π₯)). See cniccibl 25358 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β βπ₯ β β βπ¦ β dom πΉ(absβ(πΉβπ¦)) β€ π₯) β β’ (π β πΉ β πΏ1) | ||
Theorem | arearect 41964 | The area of a rectangle whose sides are parallel to the coordinate axes in (β Γ β) is its width multiplied by its height. (Contributed by Jon Pennant, 19-Mar-2019.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β & β’ π΄ β€ π΅ & β’ πΆ β€ π· & β’ π = ((π΄[,]π΅) Γ (πΆ[,]π·)) β β’ (areaβπ) = ((π΅ β π΄) Β· (π· β πΆ)) | ||
Theorem | areaquad 41965* | The area of a quadrilateral with two sides which are parallel to the y-axis in (β Γ β) is its width multiplied by the average height of its higher edge minus the average height of its lower edge. Co-author TA. (Contributed by Jon Pennant, 31-May-2019.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β & β’ πΈ β β & β’ πΉ β β & β’ π΄ < π΅ & β’ πΆ β€ πΈ & β’ π· β€ πΉ & β’ π = (πΆ + (((π₯ β π΄) / (π΅ β π΄)) Β· (π· β πΆ))) & β’ π = (πΈ + (((π₯ β π΄) / (π΅ β π΄)) Β· (πΉ β πΈ))) & β’ π = {β¨π₯, π¦β© β£ (π₯ β (π΄[,]π΅) β§ π¦ β (π[,]π))} β β’ (areaβπ) = ((((πΉ + πΈ) / 2) β ((π· + πΆ) / 2)) Β· (π΅ β π΄)) | ||
Theorem | uniel 41966* | Two ways to say a union is an element of a class. (Contributed by RP, 27-Jan-2025.) |
β’ (βͺ π΄ β π΅ β βπ₯ β π΅ βπ§(π§ β π₯ β βπ¦ β π΄ π§ β π¦)) | ||
Theorem | unielss 41967* | Two ways to say the union of a class is an element of a subclass. (Contributed by RP, 29-Jan-2025.) |
β’ (π΄ β π΅ β (βͺ π΅ β π΄ β βπ₯ β π΄ βπ¦ β π΅ π¦ β π₯)) | ||
Theorem | unielid 41968* | Two ways to say the union of a class is an element of that class. (Contributed by RP, 27-Jan-2025.) |
β’ (βͺ π΄ β π΄ β βπ₯ β π΄ βπ¦ β π΄ π¦ β π₯) | ||
Theorem | ssunib 41969* | Two ways to say a class is a subclass of a union. (Contributed by RP, 27-Jan-2025.) |
β’ (π΄ β βͺ π΅ β βπ₯ β π΄ βπ¦ β π΅ π₯ β π¦) | ||
Theorem | rp-intrabeq 41970* | Equality theorem for supremum of sets of ordinals. (Contributed by RP, 23-Jan-2025.) |
β’ (π΄ = π΅ β β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯} = β© {π₯ β On β£ βπ¦ β π΅ π¦ β π₯}) | ||
Theorem | rp-unirabeq 41971* | Equality theorem for infimum of non-empty classes of ordinals. (Contributed by RP, 23-Jan-2025.) |
β’ (π΄ = π΅ β βͺ {π₯ β On β£ βπ¦ β π΄ π₯ β π¦} = βͺ {π₯ β On β£ βπ¦ β π΅ π₯ β π¦}) | ||
Theorem | onmaxnelsup 41972* | Two ways to say the maximum element of a class of ordinals is also the supremum of that class. (Contributed by RP, 27-Jan-2025.) |
β’ (π΄ β On β (Β¬ π΄ β βͺ π΄ β βπ₯ β π΄ βπ¦ β π΄ π¦ β π₯)) | ||
Theorem | onsupneqmaxlim0 41973 | If the supremum of a class of ordinals is not in that class, then the supremum is a limit ordinal or empty. (Contributed by RP, 27-Jan-2025.) |
β’ (π΄ β On β (π΄ β βͺ π΄ β βͺ π΄ = βͺ βͺ π΄)) | ||
Theorem | onsupcl2 41974 | The supremum of a set of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.) |
β’ (π΄ β π« On β βͺ π΄ β On) | ||
Theorem | onuniintrab 41975* | The union of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. Closed form of uniordint 7789. (Contributed by RP, 28-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β βͺ π΄ = β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯}) | ||
Theorem | onintunirab 41976* | The intersection of a non-empty class of ordinals is the union of every ordinal less-than-or-equal to every element of that class. (Contributed by RP, 29-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β β ) β β© π΄ = βͺ {π₯ β On β£ βπ¦ β π΄ π₯ β π¦}) | ||
Theorem | onsupnmax 41977 | If the union of a class of ordinals is not the maximum element of that class, then the union is a limit ordinal or empty. But this isn't a biconditional since π΄ could be a non-empty set where a limit ordinal or the empty set happens to be the largest element. (Contributed by RP, 27-Jan-2025.) |
β’ (π΄ β On β (Β¬ βͺ π΄ β π΄ β βͺ π΄ = βͺ βͺ π΄)) | ||
Theorem | onsupuni 41978 | The supremum of a set of ordinals is the union of that set. Lemma 2.10 of [Schloeder] p. 5. (Contributed by RP, 19-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β sup(π΄, On, E ) = βͺ π΄) | ||
Theorem | onsupuni2 41979 | The supremum of a set of ordinals is the union of that set. (Contributed by RP, 22-Jan-2025.) |
β’ (π΄ β π« On β sup(π΄, On, E ) = βͺ π΄) | ||
Theorem | onsupintrab 41980* | The supremum of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. Definition 2.9 of [Schloeder] p. 5. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β sup(π΄, On, E ) = β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯}) | ||
Theorem | onsupintrab2 41981* | The supremum of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. (Contributed by RP, 23-Jan-2025.) |
β’ (π΄ β π« On β sup(π΄, On, E ) = β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯}) | ||
Theorem | onsupcl3 41982* | The supremum of a set of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯} β On) | ||
Theorem | onsupex3 41983* | The supremum of a set of ordinals exists. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯} β V) | ||
Theorem | onuniintrab2 41984* | The union of a set of ordinals is the intersection of every ordinal greater-than-or-equal to every member of the set. (Contributed by RP, 23-Jan-2025.) |
β’ (π΄ β π« On β βͺ π΄ = β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯}) | ||
Theorem | oninfint 41985 | The infimum of a non-empty class of ordinals is the intersection of that class. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β β ) β inf(π΄, On, E ) = β© π΄) | ||
Theorem | oninfunirab 41986* | The infimum of a non-empty class of ordinals is the union of every ordinal less-than-or-equal to every element of that class. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β β ) β inf(π΄, On, E ) = βͺ {π₯ β On β£ βπ¦ β π΄ π₯ β π¦}) | ||
Theorem | oninfcl2 41987* | The infimum of a non-empty class of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β β ) β βͺ {π₯ β On β£ βπ¦ β π΄ π₯ β π¦} β On) | ||
Theorem | onsupmaxb 41988 | The union of a class of ordinals is an element is an element of that class if and only if there is a maximum element of that class under the epsilon relation, which is to say that the domain of the restricted epsilon relation is not the whole class. (Contributed by RP, 25-Jan-2025.) |
β’ (π΄ β On β (dom ( E β© (π΄ Γ π΄)) = π΄ β Β¬ βͺ π΄ β π΄)) | ||
Theorem | onexgt 41989* | For any ordinal, there is always a larger ordinal. (Contributed by RP, 1-Feb-2025.) |
β’ (π΄ β On β βπ₯ β On π΄ β π₯) | ||
Theorem | onexomgt 41990* | For any ordinal, there is always a larger product of omega. (Contributed by RP, 1-Feb-2025.) |
β’ (π΄ β On β βπ₯ β On π΄ β (Ο Β·o π₯)) | ||
Theorem | omlimcl2 41991 | The product of a limit ordinal with any nonzero ordinal is a limit ordinal. (Contributed by RP, 8-Jan-2025.) |
β’ (((π΄ β On β§ (π΅ β πΆ β§ Lim π΅)) β§ β β π΄) β Lim (π΅ Β·o π΄)) | ||
Theorem | onexlimgt 41992* | For any ordinal, there is always a larger limit ordinal. (Contributed by RP, 1-Feb-2025.) |
β’ (π΄ β On β βπ₯ β On (Lim π₯ β§ π΄ β π₯)) | ||
Theorem | onexoegt 41993* | For any ordinal, there is always a larger power of omega. (Contributed by RP, 1-Feb-2025.) |
β’ (π΄ β On β βπ₯ β On π΄ β (Ο βo π₯)) | ||
Theorem | oninfex2 41994* | The infimum of a non-empty class of ordinals exists. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β β ) β βͺ {π₯ β On β£ βπ¦ β π΄ π₯ β π¦} β V) | ||
Theorem | onsupeqmax 41995* | Condition when the supremum of a set of ordinals is the maximum element of that set. (Contributed by RP, 24-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β (βπ₯ β π΄ βπ¦ β π΄ π¦ β π₯ β βͺ π΄ β π΄)) | ||
Theorem | onsupeqnmax 41996* | Condition when the supremum of a class of ordinals is not the maximum element of that class. (Contributed by RP, 27-Jan-2025.) |
β’ (π΄ β On β (βπ₯ β π΄ βπ¦ β π΄ π₯ β π¦ β (βͺ π΄ = βͺ βͺ π΄ β§ Β¬ βͺ π΄ β π΄))) | ||
Theorem | onsuplub 41997* | The supremum of a set of ordinals is the least upper bound. (Contributed by RP, 27-Jan-2025.) |
β’ (((π΄ β On β§ π΄ β π) β§ π΅ β On) β (π΅ β βͺ π΄ β βπ§ β π΄ π΅ β π§)) | ||
Theorem | onsupnub 41998* | An upper bound of a set of ordinals is not less than the supremum. (Contributed by RP, 27-Jan-2025.) |
β’ (((π΄ β On β§ π΄ β π) β§ (π΅ β On β§ βπ§ β π΄ π§ β π΅)) β βͺ π΄ β π΅) | ||
Theorem | onfisupcl 41999 | Sufficient condition when the supremum of a set of ordinals is the maximum element of that set. See ordunifi 9293. (Contributed by RP, 27-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β ((π΄ β Fin β§ π΄ β β ) β βͺ π΄ β π΄)) | ||
Theorem | onelord 42000 | Every element of a ordinal is an ordinal. Lemma 1.3 of [Schloeder] p. 1. Based on onelon 6390 and eloni 6375. (Contributed by RP, 15-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β π΄) β Ord π΅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |