Home | Metamath
Proof Explorer Theorem List (p. 312 of 468) | < 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-29329) |
Hilbert Space Explorer
(29330-30852) |
Users' Mathboxes
(30853-46765) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mptctf 31101 | A countable mapping set is countable, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Thierry Arnoux, 8-Mar-2017.) |
β’ β²π₯π΄ β β’ (π΄ βΌ Ο β (π₯ β π΄ β¦ π΅) βΌ Ο) | ||
Theorem | abrexctf 31102* | 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 31103* | Index a countable set with integers and pad with π. (Contributed by Thierry Arnoux, 1-Jun-2020.) |
β’ ((π΄ βΌ Ο β§ π β π β§ Β¬ π β π΄) β βπ(π:ββΆ(π΄ βͺ {π}) β§ π΄ β ran π β§ Fun (β‘π βΎ π΄))) | ||
Theorem | cnvoprabOLD 31104* | The converse of a class abstraction of nested ordered pairs. Obsolete version of cnvoprab 7932 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 31105* | 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 31106* | 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 31107* | Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also mapfien 9215. (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 31108* | 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 31109* | Finite support of a curried function with a constant first argument. (Contributed by Thierry Arnoux, 7-Jul-2023.) |
β’ πΊ = (π₯ β π΅ β¦ (πΆπΉπ₯)) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΉ Fn (π΄ Γ π΅)) & β’ (π β πΆ β π΄) & β’ (π β πΉ finSupp π) β β’ (π β πΊ finSupp π) | ||
Theorem | fsuppcurry2 31110* | Finite support of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 7-Jul-2023.) |
β’ πΊ = (π₯ β π΄ β¦ (π₯πΉπΆ)) & β’ (π β π β π) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΉ Fn (π΄ Γ π΅)) & β’ (π β πΆ β π΅) & β’ (π β πΉ finSupp π) β β’ (π β πΊ finSupp π) | ||
Theorem | offinsupp1 31111* | Finite support for a function operation. (Contributed by Thierry Arnoux, 8-Jul-2023.) |
β’ (π β π΄ β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΉ:π΄βΆπ) & β’ (π β πΊ:π΄βΆπ) & β’ (π β πΉ finSupp π) & β’ ((π β§ π₯ β π) β (ππ π₯) = π) β β’ (π β (πΉ βf π πΊ) finSupp π) | ||
Theorem | ffs2 31112 | Rewrite a function's support based with its codomain rather than the universal class. See also fsuppeq 8022. (Contributed by Thierry Arnoux, 27-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.) |
β’ πΆ = (π΅ β {π}) β β’ ((π΄ β π β§ π β π β§ πΉ:π΄βΆπ΅) β (πΉ supp π) = (β‘πΉ β πΆ)) | ||
Theorem | ffsrn 31113 | The range of a finitely supported function is finite. (Contributed by Thierry Arnoux, 27-Aug-2017.) |
β’ (π β π β π) & β’ (π β πΉ β π) & β’ (π β Fun πΉ) & β’ (π β (πΉ supp π) β Fin) β β’ (π β ran πΉ β Fin) | ||
Theorem | resf1o 31114* | 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 31115* | Restricting the range of the mapping operator. (Contributed by Thierry Arnoux, 30-Aug-2017.) |
β’ π΄ β V & β’ π΅ β V β β’ ((π΅ β© πΆ) βm π΄) = {π β (π΅ βm π΄) β£ ran π β πΆ} | ||
Theorem | fpwrelmapffslem 31116* | Lemma for fpwrelmapffs 31118. 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 31117* | 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 10254 and marypha2lem1 9242. (Contributed by Thierry Arnoux, 28-Aug-2017.) |
β’ π΄ β V & β’ π΅ β V & β’ π = (π β (π« π΅ βm π΄) β¦ {β¨π₯, π¦β© β£ (π₯ β π΄ β§ π¦ β (πβπ₯))}) β β’ π:(π« π΅ βm π΄)β1-1-ontoβπ« (π΄ Γ π΅) | ||
Theorem | fpwrelmapffs 31118* | 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 31119 | The real representation of complex numbers is zero iff both its terms are zero. Cf. crne0 12016. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ = 0 β§ π΅ = 0) β (π΄ + (i Β· π΅)) = 0)) | ||
Theorem | 1nei 31120 | The imaginary unit i is not one. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
β’ 1 β i | ||
Theorem | 1neg1t1neg1 31121 | An integer unit times itself. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
β’ (π β {-1, 1} β (π Β· π) = 1) | ||
Theorem | nnmulge 31122 | Multiplying by a positive integer π yields greater than or equal nonnegative integers. (Contributed by Thierry Arnoux, 13-Dec-2021.) |
β’ ((π β β β§ π β β0) β π β€ (π Β· π)) | ||
Theorem | lt2addrd 31123* | 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 31124 | Trichotomy law for extended reals. (Contributed by Thierry Arnoux, 12-Sep-2017.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ β€ π΅ β¨ π΅ < π΄)) | ||
Theorem | xaddeq0 31125 | Two extended reals which add up to zero are each other's negatives. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
β’ ((π΄ β β* β§ π΅ β β*) β ((π΄ +π π΅) = 0 β π΄ = -ππ΅)) | ||
Theorem | xrinfm 31126 | The extended real numbers are unbounded below. (Contributed by Thierry Arnoux, 18-Feb-2018.) (Revised by AV, 28-Sep-2020.) |
β’ inf(β*, β*, < ) = -β | ||
Theorem | le2halvesd 31127 | 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 31128 | A number is less than or equal to itself plus a nonnegative number. (Contributed by Thierry Arnoux, 28-Dec-2016.) |
β’ ((π΄ β β* β§ π΅ β β*) β (0 β€ π΅ β π΄ β€ (π΄ +π π΅))) | ||
Theorem | xrge0addge 31129 | A number is less than or equal to itself plus a nonnegative number. (Contributed by Thierry Arnoux, 19-Jul-2020.) |
β’ ((π΄ β β* β§ π΅ β (0[,]+β)) β π΄ β€ (π΄ +π π΅)) | ||
Theorem | xlt2addrd 31130* | 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 31131 | Inequality deduction for supremum of an extended real subset. (Contributed by Thierry Arnoux, 21-Mar-2017.) |
β’ (π β π΅ β πΆ) & β’ (π β πΆ β β*) β β’ (π β sup(π΅, β*, < ) β€ sup(πΆ, β*, < )) | ||
Theorem | xrge0infss 31132* | 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 31133 | 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 31134 | Nonnegative extended reals are closed under addition. (Contributed by Thierry Arnoux, 16-Sep-2019.) |
β’ (π β π΄ β (0[,]+β)) & β’ (π β π΅ β (0[,]+β)) β β’ (π β (π΄ +π π΅) β (0[,]+β)) | ||
Theorem | xrge0subcld 31135 | Condition for closure of nonnegative extended reals under subtraction. (Contributed by Thierry Arnoux, 27-May-2020.) |
β’ (π β π΄ β (0[,]+β)) & β’ (π β π΅ β (0[,]+β)) & β’ (π β π΅ β€ π΄) β β’ (π β (π΄ +π -ππ΅) β (0[,]+β)) | ||
Theorem | infxrge0lb 31136 | 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 31137* | 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 31138* | 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 31139 | 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 31140 | 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 31141 | Nonzero extended nonnegative integers are strictly greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
β’ ((π β β0* β§ π β 0) β 0 < π) | ||
Theorem | xnn01gt 31142 | 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 31143 | Finite multiplication in the extended nonnegative integers. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
β’ (((π΄ β β0* β§ π΅ β β0*) β§ (π΄ β 0 β§ π΅ β 0)) β ((π΄ Β·e π΅) β β0 β (π΄ β β0 β§ π΅ β β0))) | ||
Theorem | joiniooico 31144 | 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 31145 | A right-open interval does not contain its right endpoint. (Contributed by Thierry Arnoux, 5-Apr-2017.) |
β’ ((π΄ β β β§ π΅ β β*) β Β¬ π΅ β (π΄[,)π΅)) | ||
Theorem | xeqlelt 31146 | Equality in terms of 'less than or equal to', 'less than'. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
β’ ((π΄ β β* β§ π΅ β β*) β (π΄ = π΅ β (π΄ β€ π΅ β§ Β¬ π΄ < π΅))) | ||
Theorem | eliccelico 31147 | 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 31148 | 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 31149 | Intersection between two open-below, closed-above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 7-Aug-2017.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ π΄ β€ π΅) β ((π΄(,]πΆ) β© (π΅(,]πΆ)) = (π΅(,]πΆ)) | ||
Theorem | xrdifh 31150 | Class difference of a half-open interval in the extended reals. (Contributed by Thierry Arnoux, 1-Aug-2017.) |
β’ π΄ β β* β β’ (β* β (π΄[,]+β)) = (-β[,)π΄) | ||
Theorem | iocinif 31151 | 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 31152 | The difference between two open intervals sharing the same lower bound. (Contributed by Thierry Arnoux, 26-Sep-2017.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ π΄ < π΅) β ((π΄(,)πΆ) β (π΄(,)π΅)) = (π΅[,)πΆ)) | ||
Theorem | difico 31153 | The difference between two closed-below, open-above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 13-Oct-2017.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ β€ π΅ β§ π΅ β€ πΆ)) β ((π΄[,)πΆ) β (π΅[,)πΆ)) = (π΄[,)π΅)) | ||
Theorem | uzssico 31154 | Upper integer sets are a subset of the corresponding closed-below, open-above intervals. (Contributed by Thierry Arnoux, 29-Dec-2021.) |
β’ (π β β€ β (β€β₯βπ) β (π[,)+β)) | ||
Theorem | fz2ssnn0 31155 | A finite set of sequential integers that is a subset of β0. (Contributed by Thierry Arnoux, 8-Dec-2021.) |
β’ (π β β0 β (π...π) β β0) | ||
Theorem | nndiffz1 31156 | Upper set of the positive integers. (Contributed by Thierry Arnoux, 22-Aug-2017.) |
β’ (π β β0 β (β β (1...π)) = (β€β₯β(π + 1))) | ||
Theorem | ssnnssfz 31157* | 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 31158 | Elementhood in a finite set of sequential integers, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
β’ ((πΎ β (π...π) β§ πΎ β π) β πΎ β ((π + 1)...π)) | ||
Theorem | fzm1ne1 31159 | Elementhood of an integer and its predecessor in finite intervals of integers. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
β’ ((πΎ β (π...π) β§ πΎ β π) β (πΎ β 1) β (π...(π β 1))) | ||
Theorem | fzspl 31160 | Split the last element of a finite set of sequential integers. More generic than fzsuc 13353. (Contributed by Thierry Arnoux, 7-Nov-2016.) |
β’ (π β (β€β₯βπ) β (π...π) = ((π...(π β 1)) βͺ {π})) | ||
Theorem | fzdif2 31161 | Split the last element of a finite set of sequential integers. More generic than fzsuc 13353. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
β’ (π β (β€β₯βπ) β ((π...π) β {π}) = (π...(π β 1))) | ||
Theorem | fzodif2 31162 | Split the last element of a half-open range of sequential integers. (Contributed by Thierry Arnoux, 5-Dec-2021.) |
β’ (π β (β€β₯βπ) β ((π..^(π + 1)) β {π}) = (π..^π)) | ||
Theorem | fzodif1 31163 | Set difference of two half-open range of sequential integers sharing the same starting value. (Contributed by Thierry Arnoux, 2-Oct-2023.) |
β’ (πΎ β (π...π) β ((π..^π) β (π..^πΎ)) = (πΎ..^π)) | ||
Theorem | fzsplit3 31164 | Split a finite interval of integers into two parts. (Contributed by Thierry Arnoux, 2-May-2017.) |
β’ (πΎ β (π...π) β (π...π) = ((π...(πΎ β 1)) βͺ (πΎ...π))) | ||
Theorem | bcm1n 31165 | 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 31166* | Rewrite a countable union as a disjoint union, finite version. Cf. iundisj 24761. (Contributed by Thierry Arnoux, 15-Feb-2017.) |
β’ β²ππ΅ & β’ (π = π β π΄ = π΅) β β’ βͺ π β (1..^π)π΄ = βͺ π β (1..^π)(π΄ β βͺ π β (1..^π)π΅) | ||
Theorem | iundisj2fi 31167* | A disjoint union is disjoint, finite version. Cf. iundisj2 24762. (Contributed by Thierry Arnoux, 16-Feb-2017.) |
β’ β²ππ΅ & β’ (π = π β π΄ = π΅) β β’ Disj π β (1..^π)(π΄ β βͺ π β (1..^π)π΅) | ||
Theorem | iundisjcnt 31168* | Rewrite a countable union as a disjoint union. (Contributed by Thierry Arnoux, 16-Feb-2017.) |
β’ β²ππ΅ & β’ (π = π β π΄ = π΅) & β’ (π β (π = β β¨ π = (1..^π))) β β’ (π β βͺ π β π π΄ = βͺ π β π (π΄ β βͺ π β (1..^π)π΅)) | ||
Theorem | iundisj2cnt 31169* | A countable disjoint union is disjoint. Cf. iundisj2 24762. (Contributed by Thierry Arnoux, 16-Feb-2017.) |
β’ β²ππ΅ & β’ (π = π β π΄ = π΅) & β’ (π β (π = β β¨ π = (1..^π))) β β’ (π β Disj π β π (π΄ β βͺ π β (1..^π)π΅)) | ||
Theorem | fzone1 31170 | Elementhood in a half-open interval, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
β’ ((πΎ β (π..^π) β§ πΎ β π) β πΎ β ((π + 1)..^π)) | ||
Theorem | fzom1ne1 31171 | Elementhood in a half-open interval, except the lower bound, shifted by one. (Contributed by Thierry Arnoux, 1-Jan-2024.) |
β’ ((πΎ β (π..^π) β§ πΎ β π) β (πΎ β 1) β (π..^(π β 1))) | ||
Theorem | f1ocnt 31172* | 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 31168 or iundisj2cnt 31169. (Contributed by Thierry Arnoux, 25-Jul-2020.) |
β’ (π΄ βΌ Ο β βπ(π:dom πβ1-1-ontoβπ΄ β§ (dom π = β β¨ dom π = (1..^((β―βπ΄) + 1))))) | ||
Theorem | fz1nnct 31173 | NN and integer ranges starting from 1 are countable. (Contributed by Thierry Arnoux, 25-Jul-2020.) |
β’ ((π΄ = β β¨ π΄ = (1..^π)) β π΄ βΌ Ο) | ||
Theorem | fz1nntr 31174 | NN and integer ranges starting from 1 are a transitive family of set. (Contributed by Thierry Arnoux, 25-Jul-2020.) |
β’ (((π΄ = β β¨ π΄ = (1..^π)) β§ π β π΄) β (1..^π) β π΄) | ||
Theorem | hashunif 31175* | The cardinality of a disjoint finite union of finite sets. Cf. hashuni 15587. (Contributed by Thierry Arnoux, 17-Feb-2017.) |
β’ β²π₯π & β’ (π β π΄ β Fin) & β’ (π β π΄ β Fin) & β’ (π β Disj π₯ β π΄ π₯) β β’ (π β (β―ββͺ π΄) = Ξ£π₯ β π΄ (β―βπ₯)) | ||
Theorem | hashxpe 31176 | The size of the Cartesian product of two finite sets is the product of their sizes. This is a version of hashxp 14198 valid for infinite sets, which uses extended real numbers. (Contributed by Thierry Arnoux, 27-May-2023.) |
β’ ((π΄ β π β§ π΅ β π) β (β―β(π΄ Γ π΅)) = ((β―βπ΄) Β·e (β―βπ΅))) | ||
Theorem | hashgt1 31177 | Restate "set contains at least two elements" in terms of elementhood. (Contributed by Thierry Arnoux, 21-Nov-2023.) |
β’ (π΄ β π β (Β¬ π΄ β (β‘β― β {0, 1}) β 1 < (β―βπ΄))) | ||
Theorem | dvdszzq 31178 | Divisibility for an integer quotient. (Contributed by Thierry Arnoux, 17-Sep-2023.) |
β’ π = (π΄ / π΅) & β’ (π β π β β) & β’ (π β π β β€) & β’ (π β π΅ β β€) & β’ (π β π΅ β 0) & β’ (π β π β₯ π΄) & β’ (π β Β¬ π β₯ π΅) β β’ (π β π β₯ π) | ||
Theorem | prmdvdsbc 31179 | Condition for a prime number to divide a binomial coefficient. (Contributed by Thierry Arnoux, 17-Sep-2023.) |
β’ ((π β β β§ π β (1...(π β 1))) β π β₯ (πCπ)) | ||
Theorem | numdenneg 31180 | Numerator and denominator of the negative. (Contributed by Thierry Arnoux, 27-Oct-2017.) |
β’ (π β β β ((numerβ-π) = -(numerβπ) β§ (denomβ-π) = (denomβπ))) | ||
Theorem | divnumden2 31181 | Calculate the reduced form of a quotient using gcd. This version extends divnumden 16501 for the negative integers. (Contributed by Thierry Arnoux, 25-Oct-2017.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ -π΅ β β) β ((numerβ(π΄ / π΅)) = -(π΄ / (π΄ gcd π΅)) β§ (denomβ(π΄ / π΅)) = -(π΅ / (π΄ gcd π΅)))) | ||
Theorem | nnindf 31182* | Principle of Mathematical Induction, using a bound-variable hypothesis instead of distinct variables. (Contributed by Thierry Arnoux, 6-May-2018.) |
β’ β²π¦π & β’ (π₯ = 1 β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ + 1) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ π & β’ (π¦ β β β (π β π)) β β’ (π΄ β β β π) | ||
Theorem | nn0min 31183* | Extracting the minimum positive integer for which a property π does not hold. This uses substitutions similar to nn0ind 12465. (Contributed by Thierry Arnoux, 6-May-2018.) |
β’ (π = 0 β (π β π)) & β’ (π = π β (π β π)) & β’ (π = (π + 1) β (π β π)) & β’ (π β Β¬ π) & β’ (π β βπ β β π) β β’ (π β βπ β β0 (Β¬ π β§ π)) | ||
Theorem | subne0nn 31184 | A nonnegative difference is positive if the two numbers are not equal. (Contributed by Thierry Arnoux, 17-Dec-2023.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β (π β π) β β0) & β’ (π β π β π) β β’ (π β (π β π) β β) | ||
Theorem | ltesubnnd 31185 | Subtracting an integer number from another number decreases it. See ltsubrpd 12854. (Contributed by Thierry Arnoux, 18-Apr-2017.) |
β’ (π β π β β€) & β’ (π β π β β) β β’ (π β ((π + 1) β π) β€ π) | ||
Theorem | fprodeq02 31186* | If one of the factors is zero the product is zero. (Contributed by Thierry Arnoux, 11-Dec-2021.) |
β’ (π = πΎ β π΅ = πΆ) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β πΎ β π΄) & β’ (π β πΆ = 0) β β’ (π β βπ β π΄ π΅ = 0) | ||
Theorem | pr01ssre 31187 | The range of the indicator function is a subset of β. (Contributed by Thierry Arnoux, 14-Aug-2017.) |
β’ {0, 1} β β | ||
Theorem | fprodex01 31188* | A product of factors equal to zero or one is zero exactly when one of the factors is zero. (Contributed by Thierry Arnoux, 11-Dec-2021.) |
β’ (π = π β π΅ = πΆ) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β {0, 1}) β β’ (π β βπ β π΄ π΅ = if(βπ β π΄ πΆ = 1, 1, 0)) | ||
Theorem | prodpr 31189* | A product over a pair is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
β’ (π = π΄ β π· = πΈ) & β’ (π = π΅ β π· = πΉ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΈ β β) & β’ (π β πΉ β β) & β’ (π β π΄ β π΅) β β’ (π β βπ β {π΄, π΅}π· = (πΈ Β· πΉ)) | ||
Theorem | prodtp 31190* | A product over a triple is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
β’ (π = π΄ β π· = πΈ) & β’ (π = π΅ β π· = πΉ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΈ β β) & β’ (π β πΉ β β) & β’ (π β π΄ β π΅) & β’ (π = πΆ β π· = πΊ) & β’ (π β πΆ β π) & β’ (π β πΊ β β) & β’ (π β π΄ β πΆ) & β’ (π β π΅ β πΆ) β β’ (π β βπ β {π΄, π΅, πΆ}π· = ((πΈ Β· πΉ) Β· πΊ)) | ||
Theorem | fsumub 31191* | An upper bound for a term of a positive finite sum. (Contributed by Thierry Arnoux, 27-Dec-2021.) |
β’ (π = πΎ β π΅ = π·) & β’ (π β π΄ β Fin) & β’ (π β Ξ£π β π΄ π΅ = πΆ) & β’ ((π β§ π β π΄) β π΅ β β+) & β’ (π β πΎ β π΄) β β’ (π β π· β€ πΆ) | ||
Theorem | fsumiunle 31192* | Upper bound for a sum of nonnegative terms over an indexed union. The inequality may be strict if the indexed union is non-disjoint, since in the right hand side, a summand may be counted several times. (Contributed by Thierry Arnoux, 1-Jan-2021.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π₯ β π΄) β π΅ β Fin) & β’ (((π β§ π₯ β π΄) β§ π β π΅) β πΆ β β) & β’ (((π β§ π₯ β π΄) β§ π β π΅) β 0 β€ πΆ) β β’ (π β Ξ£π β βͺ π₯ β π΄ π΅πΆ β€ Ξ£π₯ β π΄ Ξ£π β π΅ πΆ) | ||
Theorem | dfdec100 31193 | Split the hundreds from a decimal value. (Contributed by Thierry Arnoux, 25-Dec-2021.) |
β’ π΄ β β0 & β’ π΅ β β0 & β’ πΆ β β β β’ ;;π΄π΅πΆ = ((;;100 Β· π΄) + ;π΅πΆ) | ||
Define a decimal expansion constructor. The decimal expansions built with this constructor are not meant to be used alone outside of this chapter. Rather, they are meant to be used exclusively as part of a decimal number with a decimal fraction, for example (3._1_4_1_59). That decimal point operator is defined in the next section. The bulk of these constructions have originally been proposed by David A. Wheeler on 12-May-2015, and discussed with Mario Carneiro in this thread: https://groups.google.com/g/metamath/c/2AW7T3d2YiQ. | ||
Syntax | cdp2 31194 | Constant used for decimal fraction constructor. See df-dp2 31195. |
class _π΄π΅ | ||
Definition | df-dp2 31195 | Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12488. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.) |
β’ _π΄π΅ = (π΄ + (π΅ / ;10)) | ||
Theorem | dp2eq1 31196 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ (π΄ = π΅ β _π΄πΆ = _π΅πΆ) | ||
Theorem | dp2eq2 31197 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ (π΄ = π΅ β _πΆπ΄ = _πΆπ΅) | ||
Theorem | dp2eq1i 31198 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ π΄ = π΅ β β’ _π΄πΆ = _π΅πΆ | ||
Theorem | dp2eq2i 31199 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ π΄ = π΅ β β’ _πΆπ΄ = _πΆπ΅ | ||
Theorem | dp2eq12i 31200 | Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.) |
β’ π΄ = π΅ & β’ πΆ = π· β β’ _π΄πΆ = _π΅π· |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |