![]() |
Metamath
Proof Explorer Theorem List (p. 135 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 | ioopos 13401 | The set of positive reals expressed as an open interval. (Contributed by NM, 7-May-2007.) |
β’ (0(,)+β) = {π₯ β β β£ 0 < π₯} | ||
Theorem | ioorp 13402 | The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007.) |
β’ (0(,)+β) = β+ | ||
Theorem | iooshf 13403 | Shift the arguments of the open interval function. (Contributed by NM, 17-Aug-2008.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β ((π΄ β π΅) β (πΆ(,)π·) β π΄ β ((πΆ + π΅)(,)(π· + π΅)))) | ||
Theorem | iocssre 13404 | A closed-above interval with real upper bound is a set of reals. (Contributed by FL, 29-May-2014.) |
β’ ((π΄ β β* β§ π΅ β β) β (π΄(,]π΅) β β) | ||
Theorem | icossre 13405 | A closed-below interval with real lower bound is a set of reals. (Contributed by Mario Carneiro, 14-Jun-2014.) |
β’ ((π΄ β β β§ π΅ β β*) β (π΄[,)π΅) β β) | ||
Theorem | iccssre 13406 | A closed real interval is a set of reals. (Contributed by FL, 6-Jun-2007.) (Proof shortened by Paul Chapman, 21-Jan-2008.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) | ||
Theorem | iccssxr 13407 | A closed interval is a set of extended reals. (Contributed by FL, 28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.) |
β’ (π΄[,]π΅) β β* | ||
Theorem | iocssxr 13408 | An open-below, closed-above interval is a subset of the extended reals. (Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro, 4-Jul-2014.) |
β’ (π΄(,]π΅) β β* | ||
Theorem | icossxr 13409 | A closed-below, open-above interval is a subset of the extended reals. (Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro, 4-Jul-2014.) |
β’ (π΄[,)π΅) β β* | ||
Theorem | ioossicc 13410 | An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) |
β’ (π΄(,)π΅) β (π΄[,]π΅) | ||
Theorem | iccssred 13411 | A closed real interval is a set of reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΄[,]π΅) β β) | ||
Theorem | eliccxr 13412 | A member of a closed interval is an extended real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π΄ β (π΅[,]πΆ) β π΄ β β*) | ||
Theorem | icossicc 13413 | A closed-below, open-above interval is a subset of its closure. (Contributed by Thierry Arnoux, 25-Oct-2016.) |
β’ (π΄[,)π΅) β (π΄[,]π΅) | ||
Theorem | iocssicc 13414 | A closed-above, open-below interval is a subset of its closure. (Contributed by Thierry Arnoux, 1-Apr-2017.) |
β’ (π΄(,]π΅) β (π΄[,]π΅) | ||
Theorem | ioossico 13415 | An open interval is a subset of its closure-below. (Contributed by Thierry Arnoux, 3-Mar-2017.) |
β’ (π΄(,)π΅) β (π΄[,)π΅) | ||
Theorem | iocssioo 13416 | Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (π΄ β€ πΆ β§ π· < π΅)) β (πΆ(,]π·) β (π΄(,)π΅)) | ||
Theorem | icossioo 13417 | Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (π΄ < πΆ β§ π· β€ π΅)) β (πΆ[,)π·) β (π΄(,)π΅)) | ||
Theorem | ioossioo 13418 | Condition for an open interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 26-Sep-2017.) |
β’ (((π΄ β β* β§ π΅ β β*) β§ (π΄ β€ πΆ β§ π· β€ π΅)) β (πΆ(,)π·) β (π΄(,)π΅)) | ||
Theorem | iccsupr 13419* | A nonempty subset of a closed real interval satisfies the conditions for the existence of its supremum (see suprcl 12174). (Contributed by Paul Chapman, 21-Jan-2008.) |
β’ (((π΄ β β β§ π΅ β β) β§ π β (π΄[,]π΅) β§ πΆ β π) β (π β β β§ π β β β§ βπ₯ β β βπ¦ β π π¦ β€ π₯)) | ||
Theorem | elioopnf 13420 | Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π΄ β β* β (π΅ β (π΄(,)+β) β (π΅ β β β§ π΄ < π΅))) | ||
Theorem | elioomnf 13421 | Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014.) |
β’ (π΄ β β* β (π΅ β (-β(,)π΄) β (π΅ β β β§ π΅ < π΄))) | ||
Theorem | elicopnf 13422 | Membership in a closed unbounded interval of reals. (Contributed by Mario Carneiro, 16-Sep-2014.) |
β’ (π΄ β β β (π΅ β (π΄[,)+β) β (π΅ β β β§ π΄ β€ π΅))) | ||
Theorem | repos 13423 | Two ways of saying that a real number is positive. (Contributed by NM, 7-May-2007.) |
β’ (π΄ β (0(,)+β) β (π΄ β β β§ 0 < π΄)) | ||
Theorem | ioof 13424 | The set of open intervals of extended reals maps to subsets of reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) |
β’ (,):(β* Γ β*)βΆπ« β | ||
Theorem | iccf 13425 | The set of closed intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ [,]:(β* Γ β*)βΆπ« β* | ||
Theorem | unirnioo 13426 | The union of the range of the open interval function. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 30-Jan-2014.) |
β’ β = βͺ ran (,) | ||
Theorem | dfioo2 13427* | Alternate definition of the set of open intervals of extended reals. (Contributed by NM, 1-Mar-2007.) (Revised by Mario Carneiro, 1-Sep-2015.) |
β’ (,) = (π₯ β β*, π¦ β β* β¦ {π€ β β β£ (π₯ < π€ β§ π€ < π¦)}) | ||
Theorem | ioorebas 13428 | Open intervals are elements of the set of all open intervals. (Contributed by Mario Carneiro, 26-Mar-2015.) |
β’ (π΄(,)π΅) β ran (,) | ||
Theorem | xrge0neqmnf 13429 | A nonnegative extended real is not equal to minus infinity. (Contributed by Thierry Arnoux, 9-Jun-2017.) (Proof shortened by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π΄ β (0[,]+β) β π΄ β -β) | ||
Theorem | xrge0nre 13430 | An extended real which is not a real is plus infinity. (Contributed by Thierry Arnoux, 16-Oct-2017.) |
β’ ((π΄ β (0[,]+β) β§ Β¬ π΄ β β) β π΄ = +β) | ||
Theorem | elrege0 13431 | The predicate "is a nonnegative real". (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) |
β’ (π΄ β (0[,)+β) β (π΄ β β β§ 0 β€ π΄)) | ||
Theorem | nn0rp0 13432 | A nonnegative integer is a nonnegative real number. (Contributed by AV, 24-May-2020.) |
β’ (π β β0 β π β (0[,)+β)) | ||
Theorem | rge0ssre 13433 | Nonnegative real numbers are real numbers. (Contributed by Thierry Arnoux, 9-Sep-2018.) (Proof shortened by AV, 8-Sep-2019.) |
β’ (0[,)+β) β β | ||
Theorem | elxrge0 13434 | Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.) |
β’ (π΄ β (0[,]+β) β (π΄ β β* β§ 0 β€ π΄)) | ||
Theorem | 0e0icopnf 13435 | 0 is a member of (0[,)+β). (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ 0 β (0[,)+β) | ||
Theorem | 0e0iccpnf 13436 | 0 is a member of (0[,]+β). (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ 0 β (0[,]+β) | ||
Theorem | ge0addcl 13437 | The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 19-Jun-2014.) |
β’ ((π΄ β (0[,)+β) β§ π΅ β (0[,)+β)) β (π΄ + π΅) β (0[,)+β)) | ||
Theorem | ge0mulcl 13438 | The nonnegative reals are closed under multiplication. (Contributed by Mario Carneiro, 19-Jun-2014.) |
β’ ((π΄ β (0[,)+β) β§ π΅ β (0[,)+β)) β (π΄ Β· π΅) β (0[,)+β)) | ||
Theorem | ge0xaddcl 13439 | The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π΄ β (0[,]+β) β§ π΅ β (0[,]+β)) β (π΄ +π π΅) β (0[,]+β)) | ||
Theorem | ge0xmulcl 13440 | The nonnegative extended reals are closed under multiplication. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π΄ β (0[,]+β) β§ π΅ β (0[,]+β)) β (π΄ Β·e π΅) β (0[,]+β)) | ||
Theorem | lbicc2 13441 | The lower bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by FL, 29-May-2014.) (Revised by Mario Carneiro, 9-Sep-2015.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ β€ π΅) β π΄ β (π΄[,]π΅)) | ||
Theorem | ubicc2 13442 | The upper bound of a closed interval is a member of it. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by FL, 29-May-2014.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ β€ π΅) β π΅ β (π΄[,]π΅)) | ||
Theorem | elicc01 13443 | Membership in the closed real interval between 0 and 1, also called the closed unit interval. (Contributed by AV, 20-Aug-2022.) |
β’ (π β (0[,]1) β (π β β β§ 0 β€ π β§ π β€ 1)) | ||
Theorem | elunitrn 13444 | The closed unit interval is a subset of the set of the real numbers. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 21-Dec-2016.) |
β’ (π΄ β (0[,]1) β π΄ β β) | ||
Theorem | elunitcn 13445 | The closed unit interval is a subset of the set of the complex numbers. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 21-Dec-2016.) |
β’ (π΄ β (0[,]1) β π΄ β β) | ||
Theorem | 0elunit 13446 | Zero is an element of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013.) |
β’ 0 β (0[,]1) | ||
Theorem | 1elunit 13447 | One is an element of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013.) |
β’ 1 β (0[,]1) | ||
Theorem | iooneg 13448 | Membership in a negated open real interval. (Contributed by Paul Chapman, 26-Nov-2007.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πΆ β (π΄(,)π΅) β -πΆ β (-π΅(,)-π΄))) | ||
Theorem | iccneg 13449 | Membership in a negated closed real interval. (Contributed by Paul Chapman, 26-Nov-2007.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (πΆ β (π΄[,]π΅) β -πΆ β (-π΅[,]-π΄))) | ||
Theorem | icoshft 13450 | A shifted real is a member of a shifted, closed-below, open-above real interval. (Contributed by Paul Chapman, 25-Mar-2008.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π β (π΄[,)π΅) β (π + πΆ) β ((π΄ + πΆ)[,)(π΅ + πΆ)))) | ||
Theorem | icoshftf1o 13451* | Shifting a closed-below, open-above interval is one-to-one onto. (Contributed by Paul Chapman, 25-Mar-2008.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) |
β’ πΉ = (π₯ β (π΄[,)π΅) β¦ (π₯ + πΆ)) β β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β πΉ:(π΄[,)π΅)β1-1-ontoβ((π΄ + πΆ)[,)(π΅ + πΆ))) | ||
Theorem | icoun 13452 | The union of two adjacent left-closed right-open real intervals is a left-closed right-open real interval. (Contributed by Paul Chapman, 15-Mar-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ β€ π΅ β§ π΅ β€ πΆ)) β ((π΄[,)π΅) βͺ (π΅[,)πΆ)) = (π΄[,)πΆ)) | ||
Theorem | icodisj 13453 | Adjacent left-closed right-open real intervals are disjoint. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ ((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β ((π΄[,)π΅) β© (π΅[,)πΆ)) = β ) | ||
Theorem | ioounsn 13454 | The union of an open interval with its upper endpoint is a left-open right-closed interval. (Contributed by Jon Pennant, 8-Jun-2019.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ < π΅) β ((π΄(,)π΅) βͺ {π΅}) = (π΄(,]π΅)) | ||
Theorem | snunioo 13455 | The closure of one end of an open real interval. (Contributed by Paul Chapman, 15-Mar-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ < π΅) β ({π΄} βͺ (π΄(,)π΅)) = (π΄[,)π΅)) | ||
Theorem | snunico 13456 | The closure of the open end of a right-open real interval. (Contributed by Mario Carneiro, 16-Jun-2014.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ β€ π΅) β ((π΄[,)π΅) βͺ {π΅}) = (π΄[,]π΅)) | ||
Theorem | snunioc 13457 | The closure of the open end of a left-open real interval. (Contributed by Thierry Arnoux, 28-Mar-2017.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ β€ π΅) β ({π΄} βͺ (π΄(,]π΅)) = (π΄[,]π΅)) | ||
Theorem | prunioo 13458 | The closure of an open real interval. (Contributed by Paul Chapman, 15-Mar-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.) |
β’ ((π΄ β β* β§ π΅ β β* β§ π΄ β€ π΅) β ((π΄(,)π΅) βͺ {π΄, π΅}) = (π΄[,]π΅)) | ||
Theorem | ioodisj 13459 | If the upper bound of one open interval is less than or equal to the lower bound of the other, the intervals are disjoint. (Contributed by Jeff Hankins, 13-Jul-2009.) |
β’ ((((π΄ β β* β§ π΅ β β*) β§ (πΆ β β* β§ π· β β*)) β§ π΅ β€ πΆ) β ((π΄(,)π΅) β© (πΆ(,)π·)) = β ) | ||
Theorem | ioojoin 13460 | Join two open intervals to create a third. (Contributed by NM, 11-Aug-2008.) (Proof shortened by Mario Carneiro, 16-Jun-2014.) |
β’ (((π΄ β β* β§ π΅ β β* β§ πΆ β β*) β§ (π΄ < π΅ β§ π΅ < πΆ)) β (((π΄(,)π΅) βͺ {π΅}) βͺ (π΅(,)πΆ)) = (π΄(,)πΆ)) | ||
Theorem | difreicc 13461 | The class difference of β and a closed interval. (Contributed by FL, 18-Jun-2007.) |
β’ ((π΄ β β β§ π΅ β β) β (β β (π΄[,]π΅)) = ((-β(,)π΄) βͺ (π΅(,)+β))) | ||
Theorem | iccsplit 13462 | Split a closed interval into the union of two closed intervals. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β (π΄[,]π΅)) β (π΄[,]π΅) = ((π΄[,]πΆ) βͺ (πΆ[,]π΅))) | ||
Theorem | iccshftr 13463 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π΄ + π ) = πΆ & β’ (π΅ + π ) = π· β β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β (π β (π΄[,]π΅) β (π + π ) β (πΆ[,]π·))) | ||
Theorem | iccshftri 13464 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ π΄ β β & β’ π΅ β β & β’ π β β & β’ (π΄ + π ) = πΆ & β’ (π΅ + π ) = π· β β’ (π β (π΄[,]π΅) β (π + π ) β (πΆ[,]π·)) | ||
Theorem | iccshftl 13465 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π΄ β π ) = πΆ & β’ (π΅ β π ) = π· β β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β)) β (π β (π΄[,]π΅) β (π β π ) β (πΆ[,]π·))) | ||
Theorem | iccshftli 13466 | Membership in a shifted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ π΄ β β & β’ π΅ β β & β’ π β β & β’ (π΄ β π ) = πΆ & β’ (π΅ β π ) = π· β β’ (π β (π΄[,]π΅) β (π β π ) β (πΆ[,]π·)) | ||
Theorem | iccdil 13467 | Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π΄ Β· π ) = πΆ & β’ (π΅ Β· π ) = π· β β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β+)) β (π β (π΄[,]π΅) β (π Β· π ) β (πΆ[,]π·))) | ||
Theorem | iccdili 13468 | Membership in a dilated interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ π΄ β β & β’ π΅ β β & β’ π β β+ & β’ (π΄ Β· π ) = πΆ & β’ (π΅ Β· π ) = π· β β’ (π β (π΄[,]π΅) β (π Β· π ) β (πΆ[,]π·)) | ||
Theorem | icccntr 13469 | Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (π΄ / π ) = πΆ & β’ (π΅ / π ) = π· β β’ (((π΄ β β β§ π΅ β β) β§ (π β β β§ π β β+)) β (π β (π΄[,]π΅) β (π / π ) β (πΆ[,]π·))) | ||
Theorem | icccntri 13470 | Membership in a contracted interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ π΄ β β & β’ π΅ β β & β’ π β β+ & β’ (π΄ / π ) = πΆ & β’ (π΅ / π ) = π· β β’ (π β (π΄[,]π΅) β (π / π ) β (πΆ[,]π·)) | ||
Theorem | divelunit 13471 | A condition for a ratio to be a member of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013.) |
β’ (((π΄ β β β§ 0 β€ π΄) β§ (π΅ β β β§ 0 < π΅)) β ((π΄ / π΅) β (0[,]1) β π΄ β€ π΅)) | ||
Theorem | lincmb01cmp 13472 | A linear combination of two reals which lies in the interval between them. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 8-Sep-2015.) |
β’ (((π΄ β β β§ π΅ β β β§ π΄ < π΅) β§ π β (0[,]1)) β (((1 β π) Β· π΄) + (π Β· π΅)) β (π΄[,]π΅)) | ||
Theorem | iccf1o 13473* | Describe a bijection from [0, 1] to an arbitrary nontrivial closed interval [π΄, π΅]. (Contributed by Mario Carneiro, 8-Sep-2015.) |
β’ πΉ = (π₯ β (0[,]1) β¦ ((π₯ Β· π΅) + ((1 β π₯) Β· π΄))) β β’ ((π΄ β β β§ π΅ β β β§ π΄ < π΅) β (πΉ:(0[,]1)β1-1-ontoβ(π΄[,]π΅) β§ β‘πΉ = (π¦ β (π΄[,]π΅) β¦ ((π¦ β π΄) / (π΅ β π΄))))) | ||
Theorem | iccen 13474 | Any nontrivial closed interval is equinumerous to the unit interval. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 8-Sep-2015.) |
β’ ((π΄ β β β§ π΅ β β β§ π΄ < π΅) β (0[,]1) β (π΄[,]π΅)) | ||
Theorem | xov1plusxeqvd 13475 | A complex number π is positive real iff π / (1 + π) is in (0(,)1). Deduction form. (Contributed by David Moews, 28-Feb-2017.) |
β’ (π β π β β) & β’ (π β π β -1) β β’ (π β (π β β+ β (π / (1 + π)) β (0(,)1))) | ||
Theorem | unitssre 13476 | (0[,]1) is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.) |
β’ (0[,]1) β β | ||
Theorem | unitsscn 13477 | The closed unit interval is a subset of the set of the complex numbers. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
β’ (0[,]1) β β | ||
Theorem | supicc 13478 | Supremum of a bounded set of real numbers. (Contributed by Thierry Arnoux, 17-May-2019.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΄ β (π΅[,]πΆ)) & β’ (π β π΄ β β ) β β’ (π β sup(π΄, β, < ) β (π΅[,]πΆ)) | ||
Theorem | supiccub 13479 | The supremum of a bounded set of real numbers is an upper bound. (Contributed by Thierry Arnoux, 20-May-2019.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΄ β (π΅[,]πΆ)) & β’ (π β π΄ β β ) & β’ (π β π· β π΄) β β’ (π β π· β€ sup(π΄, β, < )) | ||
Theorem | supicclub 13480* | The supremum of a bounded set of real numbers is the least upper bound. (Contributed by Thierry Arnoux, 23-May-2019.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΄ β (π΅[,]πΆ)) & β’ (π β π΄ β β ) & β’ (π β π· β π΄) β β’ (π β (π· < sup(π΄, β, < ) β βπ§ β π΄ π· < π§)) | ||
Theorem | supicclub2 13481* | The supremum of a bounded set of real numbers is the least upper bound. (Contributed by Thierry Arnoux, 23-May-2019.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΄ β (π΅[,]πΆ)) & β’ (π β π΄ β β ) & β’ (π β π· β π΄) & β’ ((π β§ π§ β π΄) β π§ β€ π·) β β’ (π β sup(π΄, β, < ) β€ π·) | ||
Theorem | zltaddlt1le 13482 | The sum of an integer and a real number between 0 and 1 is less than or equal to a second integer iff the sum is less than the second integer. (Contributed by AV, 1-Jul-2021.) |
β’ ((π β β€ β§ π β β€ β§ π΄ β (0(,)1)) β ((π + π΄) < π β (π + π΄) β€ π)) | ||
Theorem | xnn0xrge0 13483 | An extended nonnegative integer is an extended nonnegative real. (Contributed by AV, 10-Dec-2020.) |
β’ (π΄ β β0* β π΄ β (0[,]+β)) | ||
Syntax | cfz 13484 |
Extend class notation to include the notation for a contiguous finite set
of integers. Read "π...π " as "the set of integers
from π to
π inclusive".
This symbol is also used informally in some comments to denote an ellipsis, e.g., π΄ + π΄β2 + ... + π΄β(π β 1). |
class ... | ||
Definition | df-fz 13485* | Define an operation that produces a finite set of sequential integers. Read "π...π " as "the set of integers from π to π inclusive". See fzval 13486 for its value and additional comments. (Contributed by NM, 6-Sep-2005.) |
β’ ... = (π β β€, π β β€ β¦ {π β β€ β£ (π β€ π β§ π β€ π)}) | ||
Theorem | fzval 13486* | The value of a finite set of sequential integers. E.g., 2...5 means the set {2, 3, 4, 5}. A special case of this definition (starting at 1) appears as Definition 11-2.1 of [Gleason] p. 141, where βk means our 1...π; he calls these sets segments of the integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
β’ ((π β β€ β§ π β β€) β (π...π) = {π β β€ β£ (π β€ π β§ π β€ π)}) | ||
Theorem | fzval2 13487 | An alternative way of expressing a finite set of sequential integers. (Contributed by Mario Carneiro, 3-Nov-2013.) |
β’ ((π β β€ β§ π β β€) β (π...π) = ((π[,]π) β© β€)) | ||
Theorem | fzf 13488 | Establish the domain and codomain of the finite integer sequence function. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 16-Nov-2013.) |
β’ ...:(β€ Γ β€)βΆπ« β€ | ||
Theorem | elfz1 13489 | Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) |
β’ ((π β β€ β§ π β β€) β (πΎ β (π...π) β (πΎ β β€ β§ π β€ πΎ β§ πΎ β€ π))) | ||
Theorem | elfz 13490 | Membership in a finite set of sequential integers. (Contributed by NM, 29-Sep-2005.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β (πΎ β (π...π) β (π β€ πΎ β§ πΎ β€ π))) | ||
Theorem | elfz2 13491 | Membership in a finite set of sequential integers. We use the fact that an operation's value is empty outside of its domain to show π β β€ and π β β€. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (πΎ β (π...π) β ((π β β€ β§ π β β€ β§ πΎ β β€) β§ (π β€ πΎ β§ πΎ β€ π))) | ||
Theorem | elfzd 13492 | Membership in a finite set of sequential integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β β€) & β’ (π β π β€ πΎ) & β’ (π β πΎ β€ π) β β’ (π β πΎ β (π...π)) | ||
Theorem | elfz5 13493 | Membership in a finite set of sequential integers. (Contributed by NM, 26-Dec-2005.) |
β’ ((πΎ β (β€β₯βπ) β§ π β β€) β (πΎ β (π...π) β πΎ β€ π)) | ||
Theorem | elfz4 13494 | Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (((π β β€ β§ π β β€ β§ πΎ β β€) β§ (π β€ πΎ β§ πΎ β€ π)) β πΎ β (π...π)) | ||
Theorem | elfzuzb 13495 | Membership in a finite set of sequential integers in terms of sets of upper integers. (Contributed by NM, 18-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (πΎ β (π...π) β (πΎ β (β€β₯βπ) β§ π β (β€β₯βπΎ))) | ||
Theorem | eluzfz 13496 | Membership in a finite set of sequential integers. (Contributed by NM, 4-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ ((πΎ β (β€β₯βπ) β§ π β (β€β₯βπΎ)) β πΎ β (π...π)) | ||
Theorem | elfzuz 13497 | A member of a finite set of sequential integers belongs to an upper set of integers. (Contributed by NM, 17-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (πΎ β (π...π) β πΎ β (β€β₯βπ)) | ||
Theorem | elfzuz3 13498 | Membership in a finite set of sequential integers implies membership in an upper set of integers. (Contributed by NM, 28-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (πΎ β (π...π) β π β (β€β₯βπΎ)) | ||
Theorem | elfzel2 13499 | Membership in a finite set of sequential integer implies the upper bound is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (πΎ β (π...π) β π β β€) | ||
Theorem | elfzel1 13500 | Membership in a finite set of sequential integer implies the lower bound is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
β’ (πΎ β (π...π) β π β β€) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |