![]() |
Metamath
Proof Explorer Theorem List (p. 426 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mpaaroot 42501 | The minimal polynomial of an algebraic number has the number as a root. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β ((minPolyAAβπ΄)βπ΄) = 0) | ||
Theorem | mpaamn 42502 | Minimal polynomial is monic. (Contributed by Stefan O'Rear, 25-Nov-2014.) |
β’ (π΄ β πΈ β ((coeffβ(minPolyAAβπ΄))β(degAAβπ΄)) = 1) | ||
Syntax | citgo 42503 | Extend class notation with the integral-over predicate. |
class IntgOver | ||
Syntax | cza 42504 | Extend class notation with the class of algebraic integers. |
class β€ | ||
Definition | df-itgo 42505* | 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 42508. 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 42506 | 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 42507* | Value of the integral-over function. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ (π β β β (IntgOverβπ) = {π₯ β β β£ βπ β (Polyβπ)((πβπ₯) = 0 β§ ((coeffβπ)β(degβπ)) = 1)}) | ||
Theorem | aaitgo 42508 | The standard algebraic numbers πΈ are generated by IntgOver. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ πΈ = (IntgOverββ) | ||
Theorem | itgoss 42509 | An integral element is integral over a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ ((π β π β§ π β β) β (IntgOverβπ) β (IntgOverβπ)) | ||
Theorem | itgocn 42510 | All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) |
β’ (IntgOverβπ) β β | ||
Theorem | cnsrexpcl 42511 | Exponentiation is closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β (SubRingββfld)) & β’ (π β π β π) & β’ (π β π β β0) β β’ (π β (πβπ) β π) | ||
Theorem | fsumcnsrcl 42512* | Finite sums are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β (SubRingββfld)) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β π) β β’ (π β Ξ£π β π΄ π΅ β π) | ||
Theorem | cnsrplycl 42513 | Polynomials are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β (SubRingββfld)) & β’ (π β π β (PolyβπΆ)) & β’ (π β π β π) & β’ (π β πΆ β π) β β’ (π β (πβπ) β π) | ||
Theorem | rgspnval 42514* | 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 42515 | The ring-span of a set is a subring. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
β’ (π β π β Ring) & β’ (π β π΅ = (Baseβπ )) & β’ (π β π΄ β π΅) & β’ (π β π = (RingSpanβπ )) & β’ (π β π = (πβπ΄)) β β’ (π β π β (SubRingβπ )) | ||
Theorem | rgspnssid 42516 | The ring-span of a set contains the set. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β Ring) & β’ (π β π΅ = (Baseβπ )) & β’ (π β π΄ β π΅) & β’ (π β π = (RingSpanβπ )) & β’ (π β π = (πβπ΄)) β β’ (π β π΄ β π) | ||
Theorem | rgspnmin 42517 | 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 42518 | The span of a subring is itself. (Contributed by Stefan O'Rear, 30-Nov-2014.) |
β’ (π β π β Ring) & β’ (π β π΄ β (SubRingβπ )) & β’ (π β π = ((RingSpanβπ )βπ΄)) β β’ (π β π = π΄) | ||
Theorem | rngunsnply 42519* | 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 42520* | Finite linear combinations with an indicator function. (Contributed by Stefan O'Rear, 5-Dec-2014.) |
β’ (π β πΉ = (π β π β¦ if(π = πΎ, 1, 0))) & β’ (π β π β Fin) & β’ (π β πΎ β π) & β’ ((π β§ π β π) β π΅ β β) β β’ (π β Ξ£π β π ((πΉβπ) Β· π΅) = β¦πΎ / πβ¦π΅) | ||
Syntax | cmend 42521 | Syntax for module endomorphism algebra. |
class MEndo | ||
Definition | df-mend 42522* | 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 42523 | Lemma to shorten proofs of algbase 42524 through algvsca 42528. (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 42524 | 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 42525 | 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 42526 | 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 42527 | 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 42528 | 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 42529* | 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 42530 | Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.) |
β’ π΄ = (MEndoβπ) β β’ (π LMHom π) = (Baseβπ΄) | ||
Theorem | mendplusgfval 42531* | 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 42532 | A specific addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π΅ = (Baseβπ΄) & β’ + = (+gβπ) & β’ β = (+gβπ΄) β β’ ((π β π΅ β§ π β π΅) β (π β π) = (π βf + π)) | ||
Theorem | mendmulrfval 42533* | 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 42534 | A specific multiplication in the module endormoprhism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = (.rβπ΄) β β’ ((π β π΅ β§ π β π΅) β (π Β· π) = (π β π)) | ||
Theorem | mendsca 42535 | 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 42536* | 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 42537 | 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 42538 | The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ π΄ = (MEndoβπ) β β’ (π β LMod β π΄ β Ring) | ||
Theorem | mendlmod 42539 | The module endomorphism algebra is a left module. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π = (Scalarβπ) β β’ ((π β LMod β§ π β CRing) β π΄ β LMod) | ||
Theorem | mendassa 42540 | The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π΄ = (MEndoβπ) & β’ π = (Scalarβπ) β β’ ((π β LMod β§ π β CRing) β π΄ β AssAlg) | ||
Theorem | idomodle 42541* | 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 42542 | 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 42543* | 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 42544 | 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 42545 | 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 42546 | 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 42547 | Syntax for the sequence of cyclotomic polynomials. |
class CytP | ||
Definition | df-cytp 42548* | 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 42549 | 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 | mon1psubm 42550 | Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π = (Poly1βπ ) & β’ π = (Monic1pβπ ) & β’ π = (mulGrpβπ) β β’ (π β NzRing β π β (SubMndβπ)) | ||
Theorem | deg1mhm 42551 | 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 42552 | Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ CytP Fn β | ||
Theorem | cytpval 42553* | 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 42554* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (πΉ:π΄βΆπ΅ β πΉ = {β¨π, πβ© β£ ((π β π΄ β§ π β π΅) β§ (πΉβπ) = π)}) | ||
Theorem | fgraphxp 42555* | Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (πΉ:π΄βΆπ΅ β πΉ = {π₯ β (π΄ Γ π΅) β£ (πΉβ(1st βπ₯)) = (2nd βπ₯)}) | ||
Theorem | hausgraph 42556 | 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 42557 | The class of separable topologies. |
class TopSep | ||
Syntax | ctoplnd 42558 | The class of LindelΓΆf topologies. |
class TopLnd | ||
Definition | df-topsep 42559* | 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 42560* | 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 42561 | Deductive form of r1sssuc 9798. (Contributed by Noam Pasman, 19-Jan-2025.) |
β’ (π β π΄ β On) β β’ (π β (π 1βπ΄) β (π 1βsuc π΄)) | ||
Theorem | iocunico 42562 | Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ < π΅ β§ π΅ < πΆ)) β ((π΄(,]π΅) βͺ (π΅[,)πΆ)) = (π΄(,)πΆ)) | ||
Theorem | iocinico 42563 | The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ < π΅ β§ π΅ < πΆ)) β ((π΄(,]π΅) β© (π΅[,)πΆ)) = {π΅}) | ||
Theorem | iocmbl 42564 | An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.) |
β’ ((π΄ β β* β§ π΅ β β) β (π΄(,]π΅) β dom vol) | ||
Theorem | cnioobibld 42565* | 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 25757 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) & β’ (π β βπ₯ β β βπ¦ β dom πΉ(absβ(πΉβπ¦)) β€ π₯) β β’ (π β πΉ β πΏ1) | ||
Theorem | arearect 42566 | 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 42567* | 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 42568* | Two ways to say a union is an element of a class. (Contributed by RP, 27-Jan-2025.) |
β’ (βͺ π΄ β π΅ β βπ₯ β π΅ βπ§(π§ β π₯ β βπ¦ β π΄ π§ β π¦)) | ||
Theorem | unielss 42569* | Two ways to say the union of a class is an element of a subclass. (Contributed by RP, 29-Jan-2025.) |
β’ (π΄ β π΅ β (βͺ π΅ β π΄ β βπ₯ β π΄ βπ¦ β π΅ π¦ β π₯)) | ||
Theorem | unielid 42570* | Two ways to say the union of a class is an element of that class. (Contributed by RP, 27-Jan-2025.) |
β’ (βͺ π΄ β π΄ β βπ₯ β π΄ βπ¦ β π΄ π¦ β π₯) | ||
Theorem | ssunib 42571* | Two ways to say a class is a subclass of a union. (Contributed by RP, 27-Jan-2025.) |
β’ (π΄ β βͺ π΅ β βπ₯ β π΄ βπ¦ β π΅ π₯ β π¦) | ||
Theorem | rp-intrabeq 42572* | Equality theorem for supremum of sets of ordinals. (Contributed by RP, 23-Jan-2025.) |
β’ (π΄ = π΅ β β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯} = β© {π₯ β On β£ βπ¦ β π΅ π¦ β π₯}) | ||
Theorem | rp-unirabeq 42573* | Equality theorem for infimum of non-empty classes of ordinals. (Contributed by RP, 23-Jan-2025.) |
β’ (π΄ = π΅ β βͺ {π₯ β On β£ βπ¦ β π΄ π₯ β π¦} = βͺ {π₯ β On β£ βπ¦ β π΅ π₯ β π¦}) | ||
Theorem | onmaxnelsup 42574* | 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 42575 | 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 42576 | The supremum of a set of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.) |
β’ (π΄ β π« On β βͺ π΄ β On) | ||
Theorem | onuniintrab 42577* | 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 7798. (Contributed by RP, 28-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β βͺ π΄ = β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯}) | ||
Theorem | onintunirab 42578* | 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 42579 | 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 42580 | 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 42581 | 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 42582* | 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 42583* | 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 42584* | The supremum of a set of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯} β On) | ||
Theorem | onsupex3 42585* | The supremum of a set of ordinals exists. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β π) β β© {π₯ β On β£ βπ¦ β π΄ π¦ β π₯} β V) | ||
Theorem | onuniintrab2 42586* | 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 42587 | 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 42588* | 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 42589* | The infimum of a non-empty class of ordinals is an ordinal. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β β ) β βͺ {π₯ β On β£ βπ¦ β π΄ π₯ β π¦} β On) | ||
Theorem | onsupmaxb 42590 | 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 42591* | For any ordinal, there is always a larger ordinal. (Contributed by RP, 1-Feb-2025.) |
β’ (π΄ β On β βπ₯ β On π΄ β π₯) | ||
Theorem | onexomgt 42592* | For any ordinal, there is always a larger product of omega. (Contributed by RP, 1-Feb-2025.) |
β’ (π΄ β On β βπ₯ β On π΄ β (Ο Β·o π₯)) | ||
Theorem | omlimcl2 42593 | 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 42594* | For any ordinal, there is always a larger limit ordinal. (Contributed by RP, 1-Feb-2025.) |
β’ (π΄ β On β βπ₯ β On (Lim π₯ β§ π΄ β π₯)) | ||
Theorem | onexoegt 42595* | For any ordinal, there is always a larger power of omega. (Contributed by RP, 1-Feb-2025.) |
β’ (π΄ β On β βπ₯ β On π΄ β (Ο βo π₯)) | ||
Theorem | oninfex2 42596* | The infimum of a non-empty class of ordinals exists. (Contributed by RP, 23-Jan-2025.) |
β’ ((π΄ β On β§ π΄ β β ) β βͺ {π₯ β On β£ βπ¦ β π΄ π₯ β π¦} β V) | ||
Theorem | onsupeqmax 42597* | 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 42598* | 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 42599* | The supremum of a set of ordinals is the least upper bound. (Contributed by RP, 27-Jan-2025.) |
β’ (((π΄ β On β§ π΄ β π) β§ π΅ β On) β (π΅ β βͺ π΄ β βπ§ β π΄ π΅ β π§)) | ||
Theorem | onsupnub 42600* | An upper bound of a set of ordinals is not less than the supremum. (Contributed by RP, 27-Jan-2025.) |
β’ (((π΄ β On β§ π΄ β π) β§ (π΅ β On β§ βπ§ β π΄ π§ β π΅)) β βͺ π΄ β π΅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |