![]() |
Metamath
Proof Explorer Theorem List (p. 441 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 | ||
Theorem | nnne1ge2 44001 | A positive integer which is not 1 is greater than or equal to 2. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π β β β§ π β 1) β 2 β€ π) | ||
Theorem | lefldiveq 44002 | A closed enough, smaller real πΆ has the same floor of π΄ when both are divided by π΅. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β+) & β’ (π β πΆ β ((π΄ β (π΄ mod π΅))[,]π΄)) β β’ (π β (ββ(π΄ / π΅)) = (ββ(πΆ / π΅))) | ||
Theorem | negsubdi3d 44003 | Distribution of negative over subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β -(π΄ β π΅) = (-π΄ β -π΅)) | ||
Theorem | ltdiv2dd 44004 | Division of a positive number by both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β πΆ β β+) & β’ (π β π΄ < π΅) β β’ (π β (πΆ / π΅) < (πΆ / π΄)) | ||
Theorem | abssinbd 44005 | Bound for the absolute value of the sine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β β β (absβ(sinβπ΄)) β€ 1) | ||
Theorem | halffl 44006 | Floor of (1 / 2). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (ββ(1 / 2)) = 0 | ||
Theorem | monoords 44007* | Ordering relation for a strictly monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π β§ π β (π...π)) β (πΉβπ) β β) & β’ ((π β§ π β (π..^π)) β (πΉβπ) < (πΉβ(π + 1))) & β’ (π β πΌ β (π...π)) & β’ (π β π½ β (π...π)) & β’ (π β πΌ < π½) β β’ (π β (πΉβπΌ) < (πΉβπ½)) | ||
Theorem | hashssle 44008 | The size of a subset of a finite set is less than the size of the containing set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) TODO (NM): usage (2 times) should be replaced by hashss 14369, and hashssle 44008 should be deleted afterwards. |
β’ ((π΄ β Fin β§ π΅ β π΄) β (β―βπ΅) β€ (β―βπ΄)) | ||
Theorem | lttri5d 44009 | Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β π΅) & β’ (π β Β¬ π΅ < π΄) β β’ (π β π΄ < π΅) | ||
Theorem | fzisoeu 44010* | A finite ordered set has a unique order isomorphism to a generic finite sequence of integers. This theorem generalizes fz1iso 14423 for the base index and also states the uniqueness condition. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π» β Fin) & β’ (π β < Or π») & β’ (π β π β β€) & β’ π = ((β―βπ») + (π β 1)) β β’ (π β β!π π Isom < , < ((π...π), π»)) | ||
Theorem | lt3addmuld 44011 | If three real numbers are less than a fourth real number, the sum of the three real numbers is less than three times the third real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β π΄ < π·) & β’ (π β π΅ < π·) & β’ (π β πΆ < π·) β β’ (π β ((π΄ + π΅) + πΆ) < (3 Β· π·)) | ||
Theorem | absnpncan2d 44012 | Triangular inequality, combined with cancellation law for subtraction (applied twice). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) β β’ (π β (absβ(π΄ β π·)) β€ (((absβ(π΄ β π΅)) + (absβ(π΅ β πΆ))) + (absβ(πΆ β π·)))) | ||
Theorem | fperiodmullem 44013* | A function with period π is also periodic with period nonnegative multiple of π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π β β0) & β’ (π β π β β) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) β β’ (π β (πΉβ(π + (π Β· π))) = (πΉβπ)) | ||
Theorem | fperiodmul 44014* | A function with period T is also periodic with period multiple of T. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π β β) & β’ (π β π β β€) & β’ (π β π β β) & β’ ((π β§ π₯ β β) β (πΉβ(π₯ + π)) = (πΉβπ₯)) β β’ (π β (πΉβ(π + (π Β· π))) = (πΉβπ)) | ||
Theorem | upbdrech 44015* | Choice of an upper bound for a nonempty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β ) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β βπ¦ β β βπ₯ β π΄ π΅ β€ π¦) & β’ πΆ = sup({π§ β£ βπ₯ β π΄ π§ = π΅}, β, < ) β β’ (π β (πΆ β β β§ βπ₯ β π΄ π΅ β€ πΆ)) | ||
Theorem | lt4addmuld 44016 | If four real numbers are less than a fifth real number, the sum of the four real numbers is less than four times the fifth real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΈ β β) & β’ (π β π΄ < πΈ) & β’ (π β π΅ < πΈ) & β’ (π β πΆ < πΈ) & β’ (π β π· < πΈ) β β’ (π β (((π΄ + π΅) + πΆ) + π·) < (4 Β· πΈ)) | ||
Theorem | absnpncan3d 44017 | Triangular inequality, combined with cancellation law for subtraction (applied three times). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β πΈ β β) β β’ (π β (absβ(π΄ β πΈ)) β€ ((((absβ(π΄ β π΅)) + (absβ(π΅ β πΆ))) + (absβ(πΆ β π·))) + (absβ(π· β πΈ)))) | ||
Theorem | upbdrech2 44018* | Choice of an upper bound for a possibly empty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β βπ¦ β β βπ₯ β π΄ π΅ β€ π¦) & β’ πΆ = if(π΄ = β , 0, sup({π§ β£ βπ₯ β π΄ π§ = π΅}, β, < )) β β’ (π β (πΆ β β β§ βπ₯ β π΄ π΅ β€ πΆ)) | ||
Theorem | ssfiunibd 44019* | A finite union of bounded sets is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π§ β βͺ π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β βπ¦ β β βπ§ β π₯ π΅ β€ π¦) & β’ (π β πΆ β βͺ π΄) β β’ (π β βπ€ β β βπ§ β πΆ π΅ β€ π€) | ||
Theorem | fzdifsuc2 44020 | Remove a successor from the end of a finite set of sequential integers. Similar to fzdifsuc 13561, but with a weaker condition. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β (β€β₯β(π β 1)) β (π...π) = ((π...(π + 1)) β {(π + 1)})) | ||
Theorem | fzsscn 44021 | A finite sequence of integers is a set of complex numbers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π...π) β β | ||
Theorem | divcan8d 44022 | A cancellation law for division. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β 0) & β’ (π β π΅ β 0) β β’ (π β (π΅ / (π΄ Β· π΅)) = (1 / π΄)) | ||
Theorem | dmmcand 44023 | Cancellation law for division and multiplication. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β 0) β β’ (π β ((π΄ / π΅) Β· (π΅ Β· πΆ)) = (π΄ Β· πΆ)) | ||
Theorem | fzssre 44024 | A finite sequence of integers is a set of real numbers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π...π) β β | ||
Theorem | bccld 44025 | A binomial coefficient, in its extended domain, is a nonnegative integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π β β0) & β’ (π β πΎ β β€) β β’ (π β (πCπΎ) β β0) | ||
Theorem | leadd12dd 44026 | Addition to both sides of 'less than or equal to'. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β π΄ β€ πΆ) & β’ (π β π΅ β€ π·) β β’ (π β (π΄ + π΅) β€ (πΆ + π·)) | ||
Theorem | fzssnn0 44027 | A finite set of sequential integers that is a subset of β0. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (0...π) β β0 | ||
Theorem | xreqle 44028 | Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ((π΄ β β* β§ π΄ = π΅) β π΄ β€ π΅) | ||
Theorem | xaddlidd 44029 | 0 is a left identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β*) β β’ (π β (0 +π π΄) = π΄) | ||
Theorem | xadd0ge 44030 | A number is less than or equal to itself plus a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β (0[,]+β)) β β’ (π β π΄ β€ (π΄ +π π΅)) | ||
Theorem | elfzolem1 44031 | A member in a half-open integer interval is less than or equal to the upper bound minus 1 . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (πΎ β (π..^π) β πΎ β€ (π β 1)) | ||
Theorem | xrgtned 44032 | 'Greater than' implies not equal. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) β β’ (π β π΅ β π΄) | ||
Theorem | xrleneltd 44033 | 'Less than or equal to' and 'not equals' implies 'less than', for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π΄ β€ π΅) & β’ (π β π΄ β π΅) β β’ (π β π΄ < π΅) | ||
Theorem | xaddcomd 44034 | The extended real addition operation is commutative. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) β β’ (π β (π΄ +π π΅) = (π΅ +π π΄)) | ||
Theorem | supxrre3 44035* | The supremum of a nonempty set of reals, is real if and only if it is bounded-above . (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ((π΄ β β β§ π΄ β β ) β (sup(π΄, β*, < ) β β β βπ₯ β β βπ¦ β π΄ π¦ β€ π₯)) | ||
Theorem | uzfissfz 44036* | For any finite subset of the upper integers, there is a finite set of sequential integers that includes it. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π΄ β π) & β’ (π β π΄ β Fin) β β’ (π β βπ β π π΄ β (π...π)) | ||
Theorem | xleadd2d 44037 | Addition of extended reals preserves the "less than or equal to" relation, in the right slot. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΄ β€ π΅) β β’ (π β (πΆ +π π΄) β€ (πΆ +π π΅)) | ||
Theorem | suprltrp 44038* | The supremum of a nonempty bounded set of reals can be approximated from below by elements of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β) & β’ (π β π΄ β β ) & β’ (π β βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) & β’ (π β π β β+) β β’ (π β βπ§ β π΄ (sup(π΄, β, < ) β π) < π§) | ||
Theorem | xleadd1d 44039 | Addition of extended reals preserves the "less than or equal to" relation, in the left slot. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΄ β€ π΅) β β’ (π β (π΄ +π πΆ) β€ (π΅ +π πΆ)) | ||
Theorem | xreqled 44040 | Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΄ = π΅) β β’ (π β π΄ β€ π΅) | ||
Theorem | xrgepnfd 44041 | An extended real greater than or equal to +β is +β (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β*) & β’ (π β +β β€ π΄) β β’ (π β π΄ = +β) | ||
Theorem | xrge0nemnfd 44042 | A nonnegative extended real is not minus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β (0[,]+β)) β β’ (π β π΄ β -β) | ||
Theorem | supxrgere 44043* | If a real number can be approximated from below by members of a set, then it is less than or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β β*) & β’ (π β π΅ β β) & β’ ((π β§ π₯ β β+) β βπ¦ β π΄ (π΅ β π₯) < π¦) β β’ (π β π΅ β€ sup(π΄, β*, < )) | ||
Theorem | iuneqfzuzlem 44044* | Lemma for iuneqfzuz 44045: here, inclusion is proven; aiuneqfzuz uses this lemma twice, to prove equality. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ π = (β€β₯βπ) β β’ (βπ β π βͺ π β (π...π)π΄ = βͺ π β (π...π)π΅ β βͺ π β π π΄ β βͺ π β π π΅) | ||
Theorem | iuneqfzuz 44045* | If two unions indexed by upper integers are equal if they agree on any partial indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ π = (β€β₯βπ) β β’ (βπ β π βͺ π β (π...π)π΄ = βͺ π β (π...π)π΅ β βͺ π β π π΄ = βͺ π β π π΅) | ||
Theorem | xle2addd 44046 | Adding both side of two inequalities. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π· β β*) & β’ (π β π΄ β€ πΆ) & β’ (π β π΅ β€ π·) β β’ (π β (π΄ +π π΅) β€ (πΆ +π π·)) | ||
Theorem | supxrgelem 44047* | If an extended real number can be approximated from below by members of a set, then it is less than or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ ((π β§ π₯ β β+) β βπ¦ β π΄ π΅ < (π¦ +π π₯)) β β’ (π β π΅ β€ sup(π΄, β*, < )) | ||
Theorem | supxrge 44048* | If an extended real number can be approximated from below by members of a set, then it is less than or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²π₯π & β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ ((π β§ π₯ β β+) β βπ¦ β π΄ π΅ β€ (π¦ +π π₯)) β β’ (π β π΅ β€ sup(π΄, β*, < )) | ||
Theorem | suplesup 44049* | If any element of π΄ can be approximated from below by members of π΅, then the supremum of π΄ is less than or equal to the supremum of π΅. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β*) & β’ (π β βπ₯ β π΄ βπ¦ β β+ βπ§ β π΅ (π₯ β π¦) < π§) β β’ (π β sup(π΄, β*, < ) β€ sup(π΅, β*, < )) | ||
Theorem | infxrglb 44050* | The infimum of a set of extended reals is less than an extended real if and only if the set contains a smaller number. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ ((π΄ β β* β§ π΅ β β*) β (inf(π΄, β*, < ) < π΅ β βπ₯ β π΄ π₯ < π΅)) | ||
Theorem | xadd0ge2 44051 | A number is less than or equal to itself plus a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β (0[,]+β)) β β’ (π β π΄ β€ (π΅ +π π΄)) | ||
Theorem | nepnfltpnf 44052 | An extended real that is not +β is less than +β. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β +β) & β’ (π β π΄ β β*) β β’ (π β π΄ < +β) | ||
Theorem | ltadd12dd 44053 | Addition to both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β π΄ < πΆ) & β’ (π β π΅ < π·) β β’ (π β (π΄ + π΅) < (πΆ + π·)) | ||
Theorem | nemnftgtmnft 44054 | An extended real that is not minus infinity, is larger than minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ ((π΄ β β* β§ π΄ β -β) β -β < π΄) | ||
Theorem | xrgtso 44055 | 'Greater than' is a strict ordering on the extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β‘ < Or β* | ||
Theorem | rpex 44056 | The positive reals form a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β+ β V | ||
Theorem | xrge0ge0 44057 | A nonnegative extended real is nonnegative. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π΄ β (0[,]+β) β 0 β€ π΄) | ||
Theorem | xrssre 44058 | A subset of extended reals that does not contain +β and -β is a subset of the reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β β*) & β’ (π β Β¬ +β β π΄) & β’ (π β Β¬ -β β π΄) β β’ (π β π΄ β β) | ||
Theorem | ssuzfz 44059 | A finite subset of the upper integers is a subset of a finite set of sequential integers. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ π = (β€β₯βπ) & β’ (π β π΄ β π) & β’ (π β π΄ β Fin) β β’ (π β π΄ β (π...sup(π΄, β, < ))) | ||
Theorem | absfun 44060 | The absolute value is a function. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ Fun abs | ||
Theorem | infrpge 44061* | The infimum of a nonempty, bounded subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ β²π₯π & β’ (π β π΄ β β*) & β’ (π β π΄ β β ) & β’ (π β βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) & β’ (π β π΅ β β+) β β’ (π β βπ§ β π΄ π§ β€ (inf(π΄, β*, < ) +π π΅)) | ||
Theorem | xrlexaddrp 44062* | If an extended real number π΄ can be approximated from above, adding positive reals to π΅, then π΄ is less than or equal to π΅. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ ((π β§ π₯ β β+) β π΄ β€ (π΅ +π π₯)) β β’ (π β π΄ β€ π΅) | ||
Theorem | supsubc 44063* | The supremum function distributes over subtraction in a sense similar to that in supaddc 12181. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ (π β π΄ β β) & β’ (π β π΄ β β ) & β’ (π β βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) & β’ (π β π΅ β β) & β’ πΆ = {π§ β£ βπ£ β π΄ π§ = (π£ β π΅)} β β’ (π β (sup(π΄, β, < ) β π΅) = sup(πΆ, β, < )) | ||
Theorem | xralrple2 44064* | Show that π΄ is less than π΅ by showing that there is no positive bound on the difference. A variant on xralrple 13184. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²π₯π & β’ (π β π΄ β β*) & β’ (π β π΅ β (0[,)+β)) β β’ (π β (π΄ β€ π΅ β βπ₯ β β+ π΄ β€ ((1 + π₯) Β· π΅))) | ||
Theorem | nnuzdisj 44065 | The first π elements of the set of nonnegative integers are distinct from any later members. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ ((1...π) β© (β€β₯β(π + 1))) = β | ||
Theorem | ltdivgt1 44066 | Divsion by a number greater than 1. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) β β’ (π β (1 < π΅ β (π΄ / π΅) < π΄)) | ||
Theorem | xrltned 44067 | 'Less than' implies not equal. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) β β’ (π β π΄ β π΅) | ||
Theorem | nnsplit 44068 | Express the set of positive integers as the disjoint (see nnuzdisj 44065) union of the first π values and the rest. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ (π β β β β = ((1...π) βͺ (β€β₯β(π + 1)))) | ||
Theorem | divdiv3d 44069 | Division into a fraction. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β 0) & β’ (π β πΆ β 0) β β’ (π β ((π΄ / π΅) / πΆ) = (π΄ / (πΆ Β· π΅))) | ||
Theorem | abslt2sqd 44070 | Comparison of the square of two numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β (absβπ΄) < (absβπ΅)) β β’ (π β (π΄β2) < (π΅β2)) | ||
Theorem | qenom 44071 | The set of rational numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ β β Ο | ||
Theorem | qct 44072 | The set of rational numbers is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ β βΌ Ο | ||
Theorem | xrltnled 44073 | 'Less than' in terms of 'less than or equal to'. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) β β’ (π β (π΄ < π΅ β Β¬ π΅ β€ π΄)) | ||
Theorem | lenlteq 44074 | 'less than or equal to' but not 'less than' implies 'equal' . (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ β€ π΅) & β’ (π β Β¬ π΄ < π΅) β β’ (π β π΄ = π΅) | ||
Theorem | xrred 44075 | An extended real that is neither minus infinity, nor plus infinity, is real. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΄ β -β) & β’ (π β π΄ β +β) β β’ (π β π΄ β β) | ||
Theorem | rr2sscn2 44076 | The cartesian square of β is a subset of the cartesian square of β. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (β Γ β) β (β Γ β) | ||
Theorem | infxr 44077* | The infimum of a set of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ β²π₯π & β’ β²π¦π & β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β βπ₯ β π΄ Β¬ π₯ < π΅) & β’ (π β βπ₯ β β (π΅ < π₯ β βπ¦ β π΄ π¦ < π₯)) β β’ (π β inf(π΄, β*, < ) = π΅) | ||
Theorem | infxrunb2 44078* | The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π¦ < π₯ β inf(π΄, β*, < ) = -β)) | ||
Theorem | infxrbnd2 44079* | The infimum of a bounded-below set of extended reals is greater than minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π΄ β β* β (βπ₯ β β βπ¦ β π΄ π₯ β€ π¦ β -β < inf(π΄, β*, < ))) | ||
Theorem | infleinflem1 44080 | Lemma for infleinf 44082, case π΅ β β β§ -β < inf(π΅, β*, < ). (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π β β+) & β’ (π β π β π΅) & β’ (π β π β€ (inf(π΅, β*, < ) +π (π / 2))) & β’ (π β π β π΄) & β’ (π β π β€ (π +π (π / 2))) β β’ (π β inf(π΄, β*, < ) β€ (inf(π΅, β*, < ) +π π)) | ||
Theorem | infleinflem2 44081 | Lemma for infleinf 44082, when inf(π΅, β*, < ) = -β. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π β β) & β’ (π β π β π΅) & β’ (π β π < (π β 2)) & β’ (π β π β π΄) & β’ (π β π β€ (π +π 1)) β β’ (π β π < π ) | ||
Theorem | infleinf 44082* | If any element of π΅ can be approximated from above by members of π΄, then the infimum of π΄ is less than or equal to the infimum of π΅. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ ((π β§ π₯ β π΅ β§ π¦ β β+) β βπ§ β π΄ π§ β€ (π₯ +π π¦)) β β’ (π β inf(π΄, β*, < ) β€ inf(π΅, β*, < )) | ||
Theorem | xralrple4 44083* | Show that π΄ is less than π΅ by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β) & β’ (π β π β β) β β’ (π β (π΄ β€ π΅ β βπ₯ β β+ π΄ β€ (π΅ + (π₯βπ)))) | ||
Theorem | xralrple3 44084* | Show that π΄ is less than π΅ by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β 0 β€ πΆ) β β’ (π β (π΄ β€ π΅ β βπ₯ β β+ π΄ β€ (π΅ + (πΆ Β· π₯)))) | ||
Theorem | eluzelzd 44085 | A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π β (β€β₯βπ)) β β’ (π β π β β€) | ||
Theorem | suplesup2 44086* | If any element of π΄ is less than or equal to an element in π΅, then the supremum of π΄ is less than or equal to the supremum of π΅. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ ((π β§ π₯ β π΄) β βπ¦ β π΅ π₯ β€ π¦) β β’ (π β sup(π΄, β*, < ) β€ sup(π΅, β*, < )) | ||
Theorem | recnnltrp 44087 | π is a natural number large enough that its reciprocal is smaller than the given positive πΈ. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ π = ((ββ(1 / πΈ)) + 1) β β’ (πΈ β β+ β (π β β β§ (1 / π) < πΈ)) | ||
Theorem | nnn0 44088 | The set of positive integers is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β β β | ||
Theorem | fzct 44089 | A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π...π) βΌ Ο | ||
Theorem | rpgtrecnn 44090* | Any positive real number is greater than the reciprocal of a positive integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π΄ β β+ β βπ β β (1 / π) < π΄) | ||
Theorem | fzossuz 44091 | A half-open integer interval is a subset of an upper set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π..^π) β (β€β₯βπ) | ||
Theorem | infxrrefi 44092 | The real and extended real infima match when the set is finite. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ ((π΄ β β β§ π΄ β Fin β§ π΄ β β ) β inf(π΄, β*, < ) = inf(π΄, β, < )) | ||
Theorem | xrralrecnnle 44093* | Show that π΄ is less than π΅ by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ (π β π΄ β β*) & β’ (π β π΅ β β) β β’ (π β (π΄ β€ π΅ β βπ β β π΄ β€ (π΅ + (1 / π)))) | ||
Theorem | fzoct 44094 | A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π..^π) βΌ Ο | ||
Theorem | frexr 44095 | A function taking real values, is a function taking extended real values. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β πΉ:π΄βΆβ) β β’ (π β πΉ:π΄βΆβ*) | ||
Theorem | nnrecrp 44096 | The reciprocal of a positive natural number is a positive real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β β β (1 / π) β β+) | ||
Theorem | reclt0d 44097 | The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ (π β π΄ < 0) β β’ (π β (1 / π΄) < 0) | ||
Theorem | lt0neg1dd 44098 | If a number is negative, its negative is positive. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ (π β π΄ < 0) β β’ (π β 0 < -π΄) | ||
Theorem | infxrcld 44099 | The infimum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) β β’ (π β inf(π΄, β*, < ) β β*) | ||
Theorem | xrralrecnnge 44100* | Show that π΄ is less than π΅ by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ β²ππ & β’ (π β π΄ β β) & β’ (π β π΅ β β*) β β’ (π β (π΄ β€ π΅ β βπ β β (π΄ β (1 / π)) β€ π΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |