Home | Metamath
Proof Explorer Theorem List (p. 315 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | df2ndres 31401* | Definition for a restriction of the 2nd (second member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
β’ (2nd βΎ (π΄ Γ π΅)) = (π₯ β π΄, π¦ β π΅ β¦ π¦) | ||
Theorem | 1stpreimas 31402 | The preimage of a singleton. (Contributed by Thierry Arnoux, 27-Apr-2020.) |
β’ ((Rel π΄ β§ π β π) β (β‘(1st βΎ π΄) β {π}) = ({π} Γ (π΄ β {π}))) | ||
Theorem | 1stpreima 31403 | The preimage by 1st is a 'vertical band'. (Contributed by Thierry Arnoux, 13-Oct-2017.) |
β’ (π΄ β π΅ β (β‘(1st βΎ (π΅ Γ πΆ)) β π΄) = (π΄ Γ πΆ)) | ||
Theorem | 2ndpreima 31404 | The preimage by 2nd is an 'horizontal band'. (Contributed by Thierry Arnoux, 13-Oct-2017.) |
β’ (π΄ β πΆ β (β‘(2nd βΎ (π΅ Γ πΆ)) β π΄) = (π΅ Γ π΄)) | ||
Theorem | curry2ima 31405* | The image of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
β’ πΊ = (πΉ β β‘(1st βΎ (V Γ {πΆ}))) β β’ ((πΉ Fn (π΄ Γ π΅) β§ πΆ β π΅ β§ π· β π΄) β (πΊ β π·) = {π¦ β£ βπ₯ β π· π¦ = (π₯πΉπΆ)}) | ||
Theorem | preiman0 31406 | The preimage of a nonempty set is nonempty. (Contributed by Thierry Arnoux, 9-Jun-2024.) |
β’ ((Fun πΉ β§ π΄ β ran πΉ β§ π΄ β β ) β (β‘πΉ β π΄) β β ) | ||
Theorem | intimafv 31407* | The intersection of an image set, as an indexed intersection of function values. (Contributed by Thierry Arnoux, 15-Jun-2024.) |
β’ ((Fun πΉ β§ π΄ β dom πΉ) β β© (πΉ β π΄) = β© π₯ β π΄ (πΉβπ₯)) | ||
Theorem | supssd 31408* | Inequality deduction for supremum of a subset. (Contributed by Thierry Arnoux, 21-Mar-2017.) |
β’ (π β π Or π΄) & β’ (π β π΅ β πΆ) & β’ (π β πΆ β π΄) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β π΅ π¦π π§))) & β’ (π β βπ₯ β π΄ (βπ¦ β πΆ Β¬ π₯π π¦ β§ βπ¦ β π΄ (π¦π π₯ β βπ§ β πΆ π¦π π§))) β β’ (π β Β¬ sup(πΆ, π΄, π )π sup(π΅, π΄, π )) | ||
Theorem | infssd 31409* | Inequality deduction for infimum of a subset. (Contributed by AV, 4-Oct-2020.) |
β’ (π β π Or π΄) & β’ (π β πΆ β π΅) & β’ (π β βπ₯ β π΄ (βπ¦ β πΆ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β πΆ π§π π¦))) & β’ (π β βπ₯ β π΄ (βπ¦ β π΅ Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β π΅ π§π π¦))) β β’ (π β Β¬ inf(πΆ, π΄, π )π inf(π΅, π΄, π )) | ||
Theorem | imafi2 31410 | The image by a finite set is finite. See also imafi 9053. (Contributed by Thierry Arnoux, 25-Apr-2020.) |
β’ (π΄ β Fin β (π΄ β π΅) β Fin) | ||
Theorem | unifi3 31411 | If a union is finite, then all its elements are finite. See unifi 9219. (Contributed by Thierry Arnoux, 27-Aug-2017.) |
β’ (βͺ π΄ β Fin β π΄ β Fin) | ||
Theorem | snct 31412 | A singleton is countable. (Contributed by Thierry Arnoux, 16-Sep-2016.) |
β’ (π΄ β π β {π΄} βΌ Ο) | ||
Theorem | prct 31413 | An unordered pair is countable. (Contributed by Thierry Arnoux, 16-Sep-2016.) |
β’ ((π΄ β π β§ π΅ β π) β {π΄, π΅} βΌ Ο) | ||
Theorem | mpocti 31414* | An operation is countable if both its domains are countable. (Contributed by Thierry Arnoux, 17-Sep-2017.) |
β’ βπ₯ β π΄ βπ¦ β π΅ πΆ β π β β’ ((π΄ βΌ Ο β§ π΅ βΌ Ο) β (π₯ β π΄, π¦ β π΅ β¦ πΆ) βΌ Ο) | ||
Theorem | abrexct 31415* | An image set of a countable set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016.) |
β’ (π΄ βΌ Ο β {π¦ β£ βπ₯ β π΄ π¦ = π΅} βΌ Ο) | ||
Theorem | mptctf 31416 | A countable mapping set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
β’ β²π₯π΄ β β’ (π΄ βΌ Ο β (π₯ β π΄ β¦ π΅) βΌ Ο) | ||
Theorem | abrexctf 31417* | An image set of a countable set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
β’ β²π₯π΄ β β’ (π΄ βΌ Ο β {π¦ β£ βπ₯ β π΄ π¦ = π΅} βΌ Ο) | ||
Theorem | padct 31418* | Index a countable set with integers and pad with π. (Contributed by Thierry Arnoux, 1-Jun-2020.) |
β’ ((π΄ βΌ Ο β§ π β π β§ Β¬ π β π΄) β βπ(π:ββΆ(π΄ βͺ {π}) β§ π΄ β ran π β§ Fun (β‘π βΎ π΄))) | ||
Theorem | cnvoprabOLD 31419* | The converse of a class abstraction of nested ordered pairs. Obsolete version of cnvoprab 7981 as of 16-Oct-2022, which has nonfreeness hypotheses instead of disjoint variable conditions. (Contributed by Thierry Arnoux, 17-Aug-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ β²π₯π & β’ β²π¦π & β’ (π = β¨π₯, π¦β© β (π β π)) & β’ (π β π β (V Γ V)) β β’ β‘{β¨β¨π₯, π¦β©, π§β© β£ π} = {β¨π§, πβ© β£ π} | ||
Theorem | f1od2 31420* | Sufficient condition for a binary function expressed in maps-to notation to be bijective. (Contributed by Thierry Arnoux, 17-Aug-2017.) |
β’ πΉ = (π₯ β π΄, π¦ β π΅ β¦ πΆ) & β’ ((π β§ (π₯ β π΄ β§ π¦ β π΅)) β πΆ β π) & β’ ((π β§ π§ β π·) β (πΌ β π β§ π½ β π)) & β’ (π β (((π₯ β π΄ β§ π¦ β π΅) β§ π§ = πΆ) β (π§ β π· β§ (π₯ = πΌ β§ π¦ = π½)))) β β’ (π β πΉ:(π΄ Γ π΅)β1-1-ontoβπ·) | ||
Theorem | fcobij 31421* | Composing functions with a bijection yields a bijection between sets of functions. (Contributed by Thierry Arnoux, 25-Aug-2017.) |
β’ (π β πΊ:πβ1-1-ontoβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β (π βm π ) β¦ (πΊ β π)):(π βm π )β1-1-ontoβ(π βm π )) | ||
Theorem | fcobijfs 31422* | Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also mapfien 9278. (Contributed by Thierry Arnoux, 25-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
β’ (π β πΊ:πβ1-1-ontoβπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ π = (πΊβπ) & β’ π = {π β (π βm π ) β£ π finSupp π} & β’ π = {β β (π βm π ) β£ β finSupp π} β β’ (π β (π β π β¦ (πΊ β π)):πβ1-1-ontoβπ) | ||
Theorem | suppss3 31423* | Deduce a function's support's inclusion in another function's support. (Contributed by Thierry Arnoux, 7-Sep-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
β’ πΊ = (π₯ β π΄ β¦ π΅) & β’ (π β π΄ β π) & β’ (π β π β π) & β’ (π β πΉ Fn π΄) & β’ ((π β§ π₯ β π΄ β§ (πΉβπ₯) = π) β π΅ = π) β β’ (π β (πΊ supp π) β (πΉ supp π)) | ||
Theorem | fsuppcurry1 31424* | Finite support of a curried function with a constant first argument. (Contributed by Thierry Arnoux, 7-Jul-2023.) |
β’ πΊ = (π₯ β π΅ β¦ (πΆπΉπ₯)) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΉ Fn (π΄ Γ π΅)) & β’ (π β πΆ β π΄) & β’ (π β πΉ finSupp π) β β’ (π β πΊ finSupp π) | ||
Theorem | fsuppcurry2 31425* | Finite support of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 7-Jul-2023.) |
β’ πΊ = (π₯ β π΄ β¦ (π₯πΉπΆ)) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΉ Fn (π΄ Γ π΅)) & β’ (π β πΆ β π΅) & β’ (π β πΉ finSupp π) β β’ (π β πΊ finSupp π) | ||
Theorem | offinsupp1 31426* | Finite support for a function operation. (Contributed by Thierry Arnoux, 8-Jul-2023.) |
β’ (π β π΄ β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΉ:π΄βΆπ) & β’ (π β πΊ:π΄βΆπ) & β’ (π β πΉ finSupp π) & β’ ((π β§ π₯ β π) β (ππ π₯) = π) β β’ (π β (πΉ βf π πΊ) finSupp π) | ||
Theorem | ffs2 31427 | Rewrite a function's support based with its codomain rather than the universal class. See also fsuppeq 8074. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
β’ πΆ = (π΅ β {π}) β β’ ((π΄ β π β§ π β π β§ πΉ:π΄βΆπ΅) β (πΉ supp π) = (β‘πΉ β πΆ)) | ||
Theorem | ffsrn 31428 | The range of a finitely supported function is finite. (Contributed by Thierry Arnoux, 27-Aug-2017.) |
β’ (π β π β π) & β’ (π β πΉ β π) & β’ (π β Fun πΉ) & β’ (π β (πΉ supp π) β Fin) β β’ (π β ran πΉ β Fin) | ||
Theorem | resf1o 31429* | Restriction of functions to a superset of their support creates a bijection. (Contributed by Thierry Arnoux, 12-Sep-2017.) |
β’ π = {π β (π΅ βm π΄) β£ (β‘π β (π΅ β {π})) β πΆ} & β’ πΉ = (π β π β¦ (π βΎ πΆ)) β β’ (((π΄ β π β§ π΅ β π β§ πΆ β π΄) β§ π β π΅) β πΉ:πβ1-1-ontoβ(π΅ βm πΆ)) | ||
Theorem | maprnin 31430* | Restricting the range of the mapping operator. (Contributed by Thierry Arnoux, 30-Aug-2017.) |
β’ π΄ β V & β’ π΅ β V β β’ ((π΅ β© πΆ) βm π΄) = {π β (π΅ βm π΄) β£ ran π β πΆ} | ||
Theorem | fpwrelmapffslem 31431* | Lemma for fpwrelmapffs 31433. For this theorem, the sets π΄ and π΅ could be infinite, but the relation π itself is finite. (Contributed by Thierry Arnoux, 1-Sep-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
β’ π΄ β V & β’ π΅ β V & β’ (π β πΉ:π΄βΆπ« π΅) & β’ (π β π = {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πΉβπ₯))}) β β’ (π β (π β Fin β (ran πΉ β Fin β§ (πΉ supp β ) β Fin))) | ||
Theorem | fpwrelmap 31432* | Define a canonical mapping between functions from π΄ into subsets of π΅ and the relations with domain π΄ and range within π΅. Note that the same relation is used in axdc2lem 10318 and marypha2lem1 9305. (Contributed by Thierry Arnoux, 28-Aug-2017.) |
β’ π΄ β V & β’ π΅ β V & β’ π = (π β (π« π΅ βm π΄) β¦ {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β β’ π:(π« π΅ βm π΄)β1-1-ontoβπ« (π΄ Γ π΅) | ||
Theorem | fpwrelmapffs 31433* | Define a canonical mapping between finite relations (finite subsets of a cartesian product) and functions with finite support into finite subsets. (Contributed by Thierry Arnoux, 28-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
β’ π΄ β V & β’ π΅ β V & β’ π = (π β (π« π΅ βm π΄) β¦ {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) & β’ π = {π β ((π« π΅ β© Fin) βm π΄) β£ (π supp β ) β Fin} β β’ (π βΎ π):πβ1-1-ontoβ(π« (π΄ Γ π΅) β© Fin) | ||
Theorem | creq0 31434 | The real representation of complex numbers is zero iff both its terms are zero. Cf. crne0 12080. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ = 0 β§ π΅ = 0) β (π΄ + (i Β· π΅)) = 0)) | ||
Theorem | 1nei 31435 | The imaginary unit i is not one. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
β’ 1 β i | ||
Theorem | 1neg1t1neg1 31436 | An integer unit times itself. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
β’ (π β {-1, 1} β (π Β· π) = 1) | ||
Theorem | nnmulge 31437 | Multiplying by a positive integer π yields greater than or equal nonnegative integers. (Contributed by Thierry Arnoux, 13-Dec-2021.) |
β’ ((π β β β§ π β β0) β π β€ (π Β· π)) | ||
Theorem | lt2addrd 31438* | If the right-hand side of a 'less than' relationship is an addition, then we can express the left-hand side as an addition, too, where each term is respectively less than each term of the original right side. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΄ < (π΅ + πΆ)) β β’ (π β βπ β β βπ β β (π΄ = (π + π) β§ π < π΅ β§ π < πΆ)) | ||
Theorem | xrlelttric 31439 | Trichotomy law for extended reals. (Contributed by Thierry Arnoux, 12-Sep-2017.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ β€ π΅ β¨ π΅ < π΄)) | ||
Theorem | xaddeq0 31440 | Two extended reals which add up to zero are each other's negatives. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
β’ ((π΄ β β* β§ π΅ β β*) β ((π΄ +π π΅) = 0 β π΄ = -ππ΅)) | ||
Theorem | xrinfm 31441 | The extended real numbers are unbounded below. (Contributed by Thierry Arnoux, 18-Feb-2018.) (Revised by AV, 28-Sep-2020.) |
β’ inf(β*, β*, < ) = -β | ||
Theorem | le2halvesd 31442 | A sum is less than the whole if each term is less than half. (Contributed by Thierry Arnoux, 29-Nov-2017.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΄ β€ (πΆ / 2)) & β’ (π β π΅ β€ (πΆ / 2)) β β’ (π β (π΄ + π΅) β€ πΆ) | ||
Theorem | xraddge02 31443 | A number is less than or equal to itself plus a nonnegative number. (Contributed by Thierry Arnoux, 28-Dec-2016.) |
β’ ((π΄ β β* β§ π΅ β β*) β (0 β€ π΅ β π΄ β€ (π΄ +π π΅))) | ||
Theorem | xrge0addge 31444 | A number is less than or equal to itself plus a nonnegative number. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
β’ ((π΄ β β* β§ π΅ β (0[,]+β)) β π΄ β€ (π΄ +π π΅)) | ||
Theorem | xlt2addrd 31445* | If the right-hand side of a 'less than' relationship is an addition, then we can express the left-hand side as an addition, too, where each term is respectively less than each term of the original right side. (Contributed by Thierry Arnoux, 15-Mar-2017.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΅ β -β) & β’ (π β πΆ β -β) & β’ (π β π΄ < (π΅ +π πΆ)) β β’ (π β βπ β β* βπ β β* (π΄ = (π +π π) β§ π < π΅ β§ π < πΆ)) | ||
Theorem | xrsupssd 31446 | Inequality deduction for supremum of an extended real subset. (Contributed by Thierry Arnoux, 21-Mar-2017.) |
β’ (π β π΅ β πΆ) & β’ (π β πΆ β β*) β β’ (π β sup(π΅, β*, < ) β€ sup(πΆ, β*, < )) | ||
Theorem | xrge0infss 31447* | Any subset of nonnegative extended reals has an infimum. (Contributed by Thierry Arnoux, 16-Sep-2019.) (Revised by AV, 4-Oct-2020.) |
β’ (π΄ β (0[,]+β) β βπ₯ β (0[,]+β)(βπ¦ β π΄ Β¬ π¦ < π₯ β§ βπ¦ β (0[,]+β)(π₯ < π¦ β βπ§ β π΄ π§ < π¦))) | ||
Theorem | xrge0infssd 31448 | Inequality deduction for infimum of a nonnegative extended real subset. (Contributed by Thierry Arnoux, 16-Sep-2019.) (Revised by AV, 4-Oct-2020.) |
β’ (π β πΆ β π΅) & β’ (π β π΅ β (0[,]+β)) β β’ (π β inf(π΅, (0[,]+β), < ) β€ inf(πΆ, (0[,]+β), < )) | ||
Theorem | xrge0addcld 31449 | Nonnegative extended reals are closed under addition. (Contributed by Thierry Arnoux, 16-Sep-2019.) |
β’ (π β π΄ β (0[,]+β)) & β’ (π β π΅ β (0[,]+β)) β β’ (π β (π΄ +π π΅) β (0[,]+β)) | ||
Theorem | xrge0subcld 31450 | Condition for closure of nonnegative extended reals under subtraction. (Contributed by Thierry Arnoux, 27-May-2020.) |
β’ (π β π΄ β (0[,]+β)) & β’ (π β π΅ β (0[,]+β)) & β’ (π β π΅ β€ π΄) β β’ (π β (π΄ +π -ππ΅) β (0[,]+β)) | ||
Theorem | infxrge0lb 31451 | A member of a set of nonnegative extended reals is greater than or equal to the set's infimum. (Contributed by Thierry Arnoux, 19-Jul-2020.) (Revised by AV, 4-Oct-2020.) |
β’ (π β π΄ β (0[,]+β)) & β’ (π β π΅ β π΄) β β’ (π β inf(π΄, (0[,]+β), < ) β€ π΅) | ||
Theorem | infxrge0glb 31452* | The infimum of a set of nonnegative extended reals is the greatest lower bound. (Contributed by Thierry Arnoux, 19-Jul-2020.) (Revised by AV, 4-Oct-2020.) |
β’ (π β π΄ β (0[,]+β)) & β’ (π β π΅ β (0[,]+β)) β β’ (π β (inf(π΄, (0[,]+β), < ) < π΅ β βπ₯ β π΄ π₯ < π΅)) | ||
Theorem | infxrge0gelb 31453* | The infimum of a set of nonnegative extended reals is greater than or equal to a lower bound. (Contributed by Thierry Arnoux, 19-Jul-2020.) (Revised by AV, 4-Oct-2020.) |
β’ (π β π΄ β (0[,]+β)) & β’ (π β π΅ β (0[,]+β)) β β’ (π β (π΅ β€ inf(π΄, (0[,]+β), < ) β βπ₯ β π΄ π΅ β€ π₯)) | ||
Theorem | xrofsup 31454 | The supremum is preserved by extended addition set operation. (Provided minus infinity is not involved as it does not behave well with addition.) (Contributed by Thierry Arnoux, 20-Mar-2017.) |
β’ (π β π β β*) & β’ (π β π β β*) & β’ (π β sup(π, β*, < ) β -β) & β’ (π β sup(π, β*, < ) β -β) & β’ (π β π = ( +π β (π Γ π))) β β’ (π β sup(π, β*, < ) = (sup(π, β*, < ) +π sup(π, β*, < ))) | ||
Theorem | supxrnemnf 31455 | The supremum of a nonempty set of extended reals which does not contain minus infinity is not minus infinity. (Contributed by Thierry Arnoux, 21-Mar-2017.) |
β’ ((π΄ β β* β§ π΄ β β β§ Β¬ -β β π΄) β sup(π΄, β*, < ) β -β) | ||
Theorem | xnn0gt0 31456 | Nonzero extended nonnegative integers are strictly greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
β’ ((π β β0* β§ π β 0) β 0 < π) | ||
Theorem | xnn01gt 31457 | An extended nonnegative integer is neither 0 nor 1 if and only if it is greater than 1. (Contributed by Thierry Arnoux, 21-Nov-2023.) |
β’ (π β β0* β (Β¬ π β {0, 1} β 1 < π)) | ||
Theorem | nn0xmulclb 31458 | Finite multiplication in the extended nonnegative integers. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
β’ (((π΄ β β0* β§ π΅ β β0*) β§ (π΄ β 0 β§ π΅ β 0)) β ((π΄ Β·e π΅) β β0 β (π΄ β β0 β§ π΅ β β0))) | ||
Theorem | joiniooico 31459 | Disjoint joining an open interval with a closed-below, open-above interval to form a closed-below, open-above interval. (Contributed by Thierry Arnoux, 26-Sep-2017.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ < π΅ β§ π΅ β€ πΆ)) β (((π΄(,)π΅) β© (π΅[,)πΆ)) = β β§ ((π΄(,)π΅) βͺ (π΅[,)πΆ)) = (π΄(,)πΆ))) | ||
Theorem | ubico 31460 | A right-open interval does not contain its right endpoint. (Contributed by Thierry Arnoux, 5-Apr-2017.) |
β’ ((π΄ β β β§ π΅ β β*) β Β¬ π΅ β (π΄[,)π΅)) | ||
Theorem | xeqlelt 31461 | Equality in terms of 'less than or equal to', 'less than'. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ = π΅ β (π΄ β€ π΅ β§ Β¬ π΄ < π΅))) | ||
Theorem | eliccelico 31462 | Relate elementhood to a closed interval with elementhood to the same closed-below, open-above interval or to its upper bound. (Contributed by Thierry Arnoux, 3-Jul-2017.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ β€ π΅) β (πΆ β (π΄[,]π΅) β (πΆ β (π΄[,)π΅) β¨ πΆ = π΅))) | ||
Theorem | elicoelioo 31463 | Relate elementhood to a closed-below, open-above interval with elementhood to the same open interval or to its lower bound. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ < π΅) β (πΆ β (π΄[,)π΅) β (πΆ = π΄ β¨ πΆ β (π΄(,)π΅)))) | ||
Theorem | iocinioc2 31464 | Intersection between two open-below, closed-above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 7-Aug-2017.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ π΄ β€ π΅) β ((π΄(,]πΆ) β© (π΅(,]πΆ)) = (π΅(,]πΆ)) | ||
Theorem | xrdifh 31465 | Class difference of a half-open interval in the extended reals. (Contributed by Thierry Arnoux, 1-Aug-2017.) |
β’ π΄ β β* β β’ (β* β (π΄[,]+β)) = (-β[,)π΄) | ||
Theorem | iocinif 31466 | Relate intersection of two open-below, closed-above intervals with the same upper bound with a conditional construct. (Contributed by Thierry Arnoux, 7-Aug-2017.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β ((π΄(,]πΆ) β© (π΅(,]πΆ)) = if(π΄ < π΅, (π΅(,]πΆ), (π΄(,]πΆ))) | ||
Theorem | difioo 31467 | The difference between two open intervals sharing the same lower bound. (Contributed by Thierry Arnoux, 26-Sep-2017.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ π΄ < π΅) β ((π΄(,)πΆ) β (π΄(,)π΅)) = (π΅[,)πΆ)) | ||
Theorem | difico 31468 | The difference between two closed-below, open-above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 13-Oct-2017.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ β€ π΅ β§ π΅ β€ πΆ)) β ((π΄[,)πΆ) β (π΅[,)πΆ)) = (π΄[,)π΅)) | ||
Theorem | uzssico 31469 | Upper integer sets are a subset of the corresponding closed-below, open-above intervals. (Contributed by Thierry Arnoux, 29-Dec-2021.) |
β’ (π β β€ β (β€β₯βπ) β (π[,)+β)) | ||
Theorem | fz2ssnn0 31470 | A finite set of sequential integers that is a subset of β0. (Contributed by Thierry Arnoux, 8-Dec-2021.) |
β’ (π β β0 β (π...π) β β0) | ||
Theorem | nndiffz1 31471 | Upper set of the positive integers. (Contributed by Thierry Arnoux, 22-Aug-2017.) |
β’ (π β β0 β (β β (1...π)) = (β€β₯β(π + 1))) | ||
Theorem | ssnnssfz 31472* | For any finite subset of β, find a superset in the form of a set of sequential integers. (Contributed by Thierry Arnoux, 13-Sep-2017.) |
β’ (π΄ β (π« β β© Fin) β βπ β β π΄ β (1...π)) | ||
Theorem | fzne1 31473 | Elementhood in a finite set of sequential integers, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
β’ ((πΎ β (π...π) β§ πΎ β π) β πΎ β ((π + 1)...π)) | ||
Theorem | fzm1ne1 31474 | Elementhood of an integer and its predecessor in finite intervals of integers. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
β’ ((πΎ β (π...π) β§ πΎ β π) β (πΎ β 1) β (π...(π β 1))) | ||
Theorem | fzspl 31475 | Split the last element of a finite set of sequential integers. More generic than fzsuc 13417. (Contributed by Thierry Arnoux, 7-Nov-2016.) |
β’ (π β (β€β₯βπ) β (π...π) = ((π...(π β 1)) βͺ {π})) | ||
Theorem | fzdif2 31476 | Split the last element of a finite set of sequential integers. More generic than fzsuc 13417. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ (π β (β€β₯βπ) β ((π...π) β {π}) = (π...(π β 1))) | ||
Theorem | fzodif2 31477 | Split the last element of a half-open range of sequential integers. (Contributed by Thierry Arnoux, 5-Dec-2021.) |
β’ (π β (β€β₯βπ) β ((π..^(π + 1)) β {π}) = (π..^π)) | ||
Theorem | fzodif1 31478 | Set difference of two half-open range of sequential integers sharing the same starting value. (Contributed by Thierry Arnoux, 2-Oct-2023.) |
β’ (πΎ β (π...π) β ((π..^π) β (π..^πΎ)) = (πΎ..^π)) | ||
Theorem | fzsplit3 31479 | Split a finite interval of integers into two parts. (Contributed by Thierry Arnoux, 2-May-2017.) |
β’ (πΎ β (π...π) β (π...π) = ((π...(πΎ β 1)) βͺ (πΎ...π))) | ||
Theorem | bcm1n 31480 | The proportion of one binomial coefficient to another with π decreased by 1. (Contributed by Thierry Arnoux, 9-Nov-2016.) |
β’ ((πΎ β (0...(π β 1)) β§ π β β) β (((π β 1)CπΎ) / (πCπΎ)) = ((π β πΎ) / π)) | ||
Theorem | iundisjfi 31481* | Rewrite a countable union as a disjoint union, finite version. Cf. iundisj 24834. (Contributed by Thierry Arnoux, 15-Feb-2017.) |
β’ β²ππ΅ & β’ (π = π β π΄ = π΅) β β’ βͺ π β (1..^π)π΄ = βͺ π β (1..^π)(π΄ β βͺ π β (1..^π)π΅) | ||
Theorem | iundisj2fi 31482* | A disjoint union is disjoint, finite version. Cf. iundisj2 24835. (Contributed by Thierry Arnoux, 16-Feb-2017.) |
β’ β²ππ΅ & β’ (π = π β π΄ = π΅) β β’ Disj π β (1..^π)(π΄ β βͺ π β (1..^π)π΅) | ||
Theorem | iundisjcnt 31483* | Rewrite a countable union as a disjoint union. (Contributed by Thierry Arnoux, 16-Feb-2017.) |
β’ β²ππ΅ & β’ (π = π β π΄ = π΅) & β’ (π β (π = β β¨ π = (1..^π))) β β’ (π β βͺ π β π π΄ = βͺ π β π (π΄ β βͺ π β (1..^π)π΅)) | ||
Theorem | iundisj2cnt 31484* | A countable disjoint union is disjoint. Cf. iundisj2 24835. (Contributed by Thierry Arnoux, 16-Feb-2017.) |
β’ β²ππ΅ & β’ (π = π β π΄ = π΅) & β’ (π β (π = β β¨ π = (1..^π))) β β’ (π β Disj π β π (π΄ β βͺ π β (1..^π)π΅)) | ||
Theorem | fzone1 31485 | Elementhood in a half-open interval, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
β’ ((πΎ β (π..^π) β§ πΎ β π) β πΎ β ((π + 1)..^π)) | ||
Theorem | fzom1ne1 31486 | Elementhood in a half-open interval, except the lower bound, shifted by one. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
β’ ((πΎ β (π..^π) β§ πΎ β π) β (πΎ β 1) β (π..^(π β 1))) | ||
Theorem | f1ocnt 31487* | Given a countable set π΄, number its elements by providing a one-to-one mapping either with β or an integer range starting from 1. The domain of the function can then be used with iundisjcnt 31483 or iundisj2cnt 31484. (Contributed by Thierry Arnoux, 25-Jul-2020.) |
β’ (π΄ βΌ Ο β βπ(π:dom πβ1-1-ontoβπ΄ β§ (dom π = β β¨ dom π = (1..^((β―βπ΄) + 1))))) | ||
Theorem | fz1nnct 31488 | NN and integer ranges starting from 1 are countable. (Contributed by Thierry Arnoux, 25-Jul-2020.) |
β’ ((π΄ = β β¨ π΄ = (1..^π)) β π΄ βΌ Ο) | ||
Theorem | fz1nntr 31489 | NN and integer ranges starting from 1 are a transitive family of set. (Contributed by Thierry Arnoux, 25-Jul-2020.) |
β’ (((π΄ = β β¨ π΄ = (1..^π)) β§ π β π΄) β (1..^π) β π΄) | ||
Theorem | hashunif 31490* | The cardinality of a disjoint finite union of finite sets. Cf. hashuni 15646. (Contributed by Thierry Arnoux, 17-Feb-2017.) |
β’ β²π₯π & β’ (π β π΄ β Fin) & β’ (π β π΄ β Fin) & β’ (π β Disj π₯ β π΄ π₯) β β’ (π β (β―ββͺ π΄) = Ξ£π₯ β π΄ (β―βπ₯)) | ||
Theorem | hashxpe 31491 | The size of the Cartesian product of two finite sets is the product of their sizes. This is a version of hashxp 14262 valid for infinite sets, which uses extended real numbers. (Contributed by Thierry Arnoux, 27-May-2023.) |
β’ ((π΄ β π β§ π΅ β π) β (β―β(π΄ Γ π΅)) = ((β―βπ΄) Β·e (β―βπ΅))) | ||
Theorem | hashgt1 31492 | Restate "set contains at least two elements" in terms of elementhood. (Contributed by Thierry Arnoux, 21-Nov-2023.) |
β’ (π΄ β π β (Β¬ π΄ β (β‘β― β {0, 1}) β 1 < (β―βπ΄))) | ||
Theorem | dvdszzq 31493 | Divisibility for an integer quotient. (Contributed by Thierry Arnoux, 17-Sep-2023.) |
β’ π = (π΄ / π΅) & β’ (π β π β β) & β’ (π β π β β€) & β’ (π β π΅ β β€) & β’ (π β π΅ β 0) & β’ (π β π β₯ π΄) & β’ (π β Β¬ π β₯ π΅) β β’ (π β π β₯ π) | ||
Theorem | prmdvdsbc 31494 | Condition for a prime number to divide a binomial coefficient. (Contributed by Thierry Arnoux, 17-Sep-2023.) |
β’ ((π β β β§ π β (1...(π β 1))) β π β₯ (πCπ)) | ||
Theorem | numdenneg 31495 | Numerator and denominator of the negative. (Contributed by Thierry Arnoux, 27-Oct-2017.) |
β’ (π β β β ((numerβ-π) = -(numerβπ) β§ (denomβ-π) = (denomβπ))) | ||
Theorem | divnumden2 31496 | Calculate the reduced form of a quotient using gcd. This version extends divnumden 16558 for the negative integers. (Contributed by Thierry Arnoux, 25-Oct-2017.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β ((numerβ(π΄ / π΅)) = -(π΄ / (π΄ gcd π΅)) β§ (denomβ(π΄ / π΅)) = -(π΅ / (π΄ gcd π΅)))) | ||
Theorem | nnindf 31497* | Principle of Mathematical Induction, using a bound-variable hypothesis instead of distinct variables. (Contributed by Thierry Arnoux, 6-May-2018.) |
β’ β²π¦π & β’ (π₯ = 1 β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ + 1) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ π & β’ (π¦ β β β (π β π)) β β’ (π΄ β β β π) | ||
Theorem | nn0min 31498* | Extracting the minimum positive integer for which a property π does not hold. This uses substitutions similar to nn0ind 12529. (Contributed by Thierry Arnoux, 6-May-2018.) |
β’ (π = 0 β (π β π)) & β’ (π = π β (π β π)) & β’ (π = (π + 1) β (π β π)) & β’ (π β Β¬ π) & β’ (π β βπ β β π) β β’ (π β βπ β β0 (Β¬ π β§ π)) | ||
Theorem | subne0nn 31499 | A nonnegative difference is positive if the two numbers are not equal. (Contributed by Thierry Arnoux, 17-Dec-2023.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π β π) β β0) & β’ (π β π β π) β β’ (π β (π β π) β β) | ||
Theorem | ltesubnnd 31500 | Subtracting an integer number from another number decreases it. See ltsubrpd 12918. (Contributed by Thierry Arnoux, 18-Apr-2017.) |
β’ (π β π β β€) & β’ (π β π β β) β β’ (π β ((π + 1) β π) β€ π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |