HomeHome Intuitionistic Logic Explorer
Theorem List (p. 86 of 95)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 8501-8600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremngtmnft 8501 An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.)
 RR* -oo -oo  <
 
Theoremxrrebnd 8502 An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.)
 RR*  RR -oo  <  < +oo
 
Theoremxrre 8503 A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.)
 RR*  RR -oo  <  <_  RR
 
Theoremxrre2 8504 An extended real between two others is real. (Contributed by NM, 6-Feb-2007.)
 RR*  RR*  C  RR*  <  <  C  RR
 
Theoremxrre3 8505 A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.)
 RR*  RR 
 <_  < +oo  RR
 
Theoremge0gtmnf 8506 A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  0  <_ -oo  <
 
Theoremge0nemnf 8507 A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  0  <_  =/= -oo
 
Theoremxrrege0 8508 A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  RR  0 
 <_  <_  RR
 
Theoremz2ge 8509* There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.)
 M  ZZ  N  ZZ  k 
 ZZ  M  <_  k  N  <_  k
 
Theoremxnegeq 8510 Equality of two extended numbers with  -e in front of them. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
 -e  -e
 
Theoremxnegpnf 8511 Minus +oo. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)
 -e +oo -oo
 
Theoremxnegmnf 8512 Minus -oo. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
 -e -oo +oo
 
Theoremrexneg 8513 Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
 RR  -e  -u
 
Theoremxneg0 8514 The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
 -e 0  0
 
Theoremxnegcl 8515 Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  -e  RR*
 
Theoremxnegneg 8516 Extended real version of negneg 7057. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  -e  -e
 
Theoremxneg11 8517 Extended real version of neg11 7058. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  RR*  -e  -e
 
Theoremxltnegi 8518 Forward direction of xltneg 8519. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  RR*  <  -e  <  -e
 
Theoremxltneg 8519 Extended real version of ltneg 7252. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  RR*  <  -e  <  -e
 
Theoremxleneg 8520 Extended real version of leneg 7255. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  RR*  <_  -e  <_  -e
 
Theoremxlt0neg1 8521 Extended real version of lt0neg1 7258. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  <  0  0  <  -e
 
Theoremxlt0neg2 8522 Extended real version of lt0neg2 7259. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  0  <  -e  <  0
 
Theoremxle0neg1 8523 Extended real version of le0neg1 7260. (Contributed by Mario Carneiro, 9-Sep-2015.)
 RR*  <_  0  0  <_  -e
 
Theoremxle0neg2 8524 Extended real version of le0neg2 7261. (Contributed by Mario Carneiro, 9-Sep-2015.)
 RR*  0  <_  -e  <_  0
 
Theoremxnegcld 8525 Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.)
 RR*   =>     -e  RR*
 
Theoremxrex 8526 The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
 RR*  _V
 
3.5.3  Real number intervals
 
Syntaxcioo 8527 Extend class notation with the set of open intervals of extended reals.
 (,)
 
Syntaxcioc 8528 Extend class notation with the set of open-below, closed-above intervals of extended reals.
 (,]
 
Syntaxcico 8529 Extend class notation with the set of closed-below, open-above intervals of extended reals.
 [,)
 
Syntaxcicc 8530 Extend class notation with the set of closed intervals of extended reals.
 [,]
 
Definitiondf-ioo 8531* Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.)

 (,)  RR* ,  RR*  |->  {  RR*  |  <  <  }
 
Definitiondf-ioc 8532* Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)

 (,]  RR* ,  RR*  |->  {  RR*  |  <  <_  }
 
Definitiondf-ico 8533* Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)

 [,)  RR* ,  RR*  |->  {  RR*  |  <_  <  }
 
Definitiondf-icc 8534* Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.)

 [,]  RR* ,  RR*  |->  {  RR*  |  <_  <_  }
 
Theoremixxval 8535* Value of the interval function. (Contributed by Mario Carneiro, 3-Nov-2013.)
 O  RR* ,  RR*  |->  {  RR*  |  R  S }   =>     RR*  RR*  O  {  RR*  |  R  S }
 
Theoremelixx1 8536* Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.)
 O  RR* ,  RR*  |->  {  RR*  |  R  S }   =>     RR*  RR*  C  O  C  RR*  R C  C S
 
Theoremixxf 8537* The set of intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
 O  RR* ,  RR*  |->  {  RR*  |  R  S }   =>     O : RR*  X.  RR* --> ~P RR*
 
Theoremixxex 8538* The set of intervals of extended reals exists. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
 O  RR* ,  RR*  |->  {  RR*  |  R  S }   =>     O  _V
 
Theoremixxssxr 8539* The set of intervals of extended reals maps to subsets of extended reals. (Contributed by Mario Carneiro, 4-Jul-2014.)
 O  RR* ,  RR*  |->  {  RR*  |  R  S }   =>     O  C_  RR*
 
Theoremelixx3g 8540* Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show  RR* and  RR*. (Contributed by Mario Carneiro, 3-Nov-2013.)
 O  RR* ,  RR*  |->  {  RR*  |  R  S }   =>     C  O  RR*  RR*  C  RR*  R C  C S
 
Theoremixxssixx 8541* An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
 O  RR* ,  RR*  |->  {  RR*  |  R  S }   &     P  RR* ,  RR*  |->  {  RR*  |  T  U }   &     RR*  RR*  R  T   &     RR*  RR*  S  U   =>     O  C_  P
 
Theoremixxdisj 8542* Split an interval into disjoint pieces. (Contributed by Mario Carneiro, 16-Jun-2014.)
 O  RR* ,  RR*  |->  {  RR*  |  R  S }   &     P  RR* ,  RR*  |->  {  RR*  |  T  U }   &     RR*  RR*  T  S   =>     RR*  RR*  C  RR*  O 
 i^i  P C  (/)
 
Theoremixxss1 8543* Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)
 O  RR* ,  RR*  |->  {  RR*  |  R  S }   &     P  RR* ,  RR*  |->  {  RR*  |  T  S }   &     RR*  RR*  RR*  W  T  R   =>     RR*  W  P C  C_  O C
 
Theoremixxss2 8544* Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)
 O  RR* ,  RR*  |->  {  RR*  |  R  S }   &     P  RR* ,  RR*  |->  {  RR*  |  R  T }   &     RR*  RR*  C  RR*  T  W C  S C   =>     C  RR*  W C  P  C_  O C
 
Theoremixxss12 8545* Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro, 28-Apr-2015.)
 O  RR* ,  RR*  |->  {  RR*  |  R  S }   &     P  RR* ,  RR*  |->  {  RR*  |  T  U }   &     RR*  C  RR*  RR*  W C  C T  R   &     RR*  D  RR*  RR*  U D  D X  S   =>     RR*  RR*  W C  D X  C P D  C_  O
 
Theoremiooex 8546 The set of open intervals of extended reals exists. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)

 (,)  _V
 
Theoremiooval 8547* Value of the open interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
 RR*  RR*  (,)  {  RR*  | 
 <  <  }
 
Theoremiooidg 8548 An open interval with identical lower and upper bounds is empty. (Contributed by Jim Kingdon, 29-Mar-2020.)
 RR*  (,)  (/)
 
Theoremelioo3g 8549 Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show  RR* and  RR*. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
 C  (,)  RR*  RR*  C  RR* 
 <  C  C  <
 
Theoremelioo1 8550 Membership in an open interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
 RR*  RR*  C  (,)  C  RR*  <  C  C  <
 
Theoremelioore 8551 A member of an open interval of reals is a real. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 3-Nov-2013.)
 (,) C  RR
 
Theoremlbioog 8552 An open interval does not contain its left endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
 RR*  RR*  (,)
 
Theoremubioog 8553 An open interval does not contain its right endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
 RR*  RR*  (,)
 
Theoremiooval2 8554* Value of the open interval function. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
 RR*  RR*  (,)  {  RR  | 
 <  <  }
 
Theoremiooss1 8555 Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.)
 RR*  <_  (,) C  C_  (,) C
 
Theoremiooss2 8556 Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
 C  RR*  <_  C  (,)  C_  (,) C
 
Theoremiocval 8557* Value of the open-below, closed-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
 RR*  RR*  (,]  {  RR*  | 
 <  <_  }
 
Theoremicoval 8558* Value of the closed-below, open-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
 RR*  RR*  [,)  {  RR*  | 
 <_  <  }
 
Theoremiccval 8559* Value of the closed interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
 RR*  RR*  [,]  {  RR*  | 
 <_  <_  }
 
Theoremelioo2 8560 Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007.)
 RR*  RR*  C  (,)  C  RR  <  C  C  <
 
Theoremelioc1 8561 Membership in an open-below, closed-above interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
 RR*  RR*  C  (,]  C  RR*  <  C  C  <_
 
Theoremelico1 8562 Membership in a closed-below, open-above interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
 RR*  RR*  C  [,)  C  RR*  <_  C  C  <
 
Theoremelicc1 8563 Membership in a closed interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
 RR*  RR*  C  [,]  C  RR*  <_  C  C  <_
 
Theoremiccid 8564 A closed interval with identical lower and upper bounds is a singleton. (Contributed by Jeff Hankins, 13-Jul-2009.)
 RR*  [,]  { }
 
Theoremicc0r 8565 An empty closed interval of extended reals. (Contributed by Jim Kingdon, 30-Mar-2020.)
 RR*  RR*  <  [,]  (/)
 
Theoremeliooxr 8566 An inhabited open interval spans an interval of extended reals. (Contributed by NM, 17-Aug-2008.)
 (,) C  RR*  C  RR*
 
Theoremeliooord 8567 Ordering implied by a member of an open interval of reals. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 9-May-2014.)
 (,) C  <  <  C
 
Theoremubioc1 8568 The upper bound belongs to an open-below, closed-above interval. See ubicc2 8623. (Contributed by FL, 29-May-2014.)
 RR*  RR*  <  (,]
 
Theoremlbico1 8569 The lower bound belongs to a closed-below, open-above interval. See lbicc2 8622. (Contributed by FL, 29-May-2014.)
 RR*  RR*  <  [,)
 
Theoremiccleub 8570 An element of a closed interval is less than or equal to its upper bound. (Contributed by Jeff Hankins, 14-Jul-2009.)
 RR*  RR*  C  [,]  C  <_
 
Theoremiccgelb 8571 An element of a closed interval is more than or equal to its lower bound (Contributed by Thierry Arnoux, 23-Dec-2016.)
 RR*  RR*  C  [,]  <_  C
 
Theoremelioo5 8572 Membership in an open interval of extended reals. (Contributed by NM, 17-Aug-2008.)
 RR*  RR*  C  RR*  C  (,) 
 <  C  C  <
 
Theoremelioo4g 8573 Membership in an open interval of extended reals. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.)
 C  (,)  RR*  RR*  C  RR 
 <  C  C  <
 
Theoremioossre 8574 An open interval is a set of reals. (Contributed by NM, 31-May-2007.)
 (,)  C_  RR
 
Theoremelioc2 8575 Membership in an open-below, closed-above real interval. (Contributed by Paul Chapman, 30-Dec-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
 RR*  RR  C  (,]  C  RR  <  C  C  <_
 
Theoremelico2 8576 Membership in a closed-below, open-above real interval. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 14-Jun-2014.)
 RR  RR*  C  [,)  C  RR  <_  C  C  <
 
Theoremelicc2 8577 Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
 RR  RR  C  [,]  C  RR  <_  C  C  <_
 
Theoremelicc2i 8578 Inference for membership in a closed interval. (Contributed by Scott Fenton, 3-Jun-2013.)
 RR   &     RR   =>     C  [,]  C  RR  <_  C  C  <_
 
Theoremelicc4 8579 Membership in a closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.)
 RR*  RR*  C  RR*  C  [,] 
 <_  C  C  <_
 
Theoremiccss 8580 Condition for a closed interval to be a subset of another closed interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 20-Feb-2015.)
 RR  RR  <_  C  D  <_  C [,] D  C_  [,]
 
Theoremiccssioo 8581 Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
 RR*  RR* 
 <  C  D  <  C [,] D  C_  (,)
 
Theoremicossico 8582 Condition for a closed-below, open-above interval to be a subset of a closed-below, open-above interval. (Contributed by Thierry Arnoux, 21-Sep-2017.)
 RR*  RR* 
 <_  C  D  <_  C [,) D  C_  [,)
 
Theoremiccss2 8583 Condition for a closed interval to be a subset of another closed interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
 C  [,]  D 
 [,]  C [,] D  C_  [,]
 
Theoremiccssico 8584 Condition for a closed interval to be a subset of a half-open interval. (Contributed by Mario Carneiro, 9-Sep-2015.)
 RR*  RR* 
 <_  C  D  <  C [,] D  C_  [,)
 
Theoremiccssioo2 8585 Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
 C  (,)  D 
 (,)  C [,] D  C_  (,)
 
Theoremiccssico2 8586 Condition for a closed interval to be a subset of a closed-below, open-above interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
 C  [,)  D 
 [,)  C [,] D  C_  [,)
 
Theoremioomax 8587 The open interval from minus to plus infinity. (Contributed by NM, 6-Feb-2007.)
-oo (,) +oo  RR
 
Theoremiccmax 8588 The closed interval from minus to plus infinity. (Contributed by Mario Carneiro, 4-Jul-2014.)
-oo [,] +oo  RR*
 
Theoremioopos 8589 The set of positive reals expressed as an open interval. (Contributed by NM, 7-May-2007.)
 0 (,) +oo  {  RR  |  0  <  }
 
Theoremioorp 8590 The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007.)
 0 (,) +oo  RR+
 
Theoremiooshf 8591 Shift the arguments of the open interval function. (Contributed by NM, 17-Aug-2008.)
 RR  RR  C  RR  D  RR  -  C (,) D  C  +  (,) D  +
 
Theoremiocssre 8592 A closed-above interval with real upper bound is a set of reals. (Contributed by FL, 29-May-2014.)
 RR*  RR  (,]  C_  RR
 
Theoremicossre 8593 A closed-below interval with real lower bound is a set of reals. (Contributed by Mario Carneiro, 14-Jun-2014.)
 RR  RR*  [,)  C_  RR
 
Theoremiccssre 8594 A closed real interval is a set of reals. (Contributed by FL, 6-Jun-2007.) (Proof shortened by Paul Chapman, 21-Jan-2008.)
 RR  RR  [,]  C_  RR
 
Theoremiccssxr 8595 A closed interval is a set of extended reals. (Contributed by FL, 28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.)
 [,]  C_  RR*
 
Theoremiocssxr 8596 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.)
 (,]  C_  RR*
 
Theoremicossxr 8597 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.)
 [,)  C_  RR*
 
Theoremioossicc 8598 An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.)
 (,)  C_  [,]
 
Theoremicossicc 8599 A closed-below, open-above interval is a subset of its closure. (Contributed by Thierry Arnoux, 25-Oct-2016.)
 [,)  C_  [,]
 
Theoremiocssicc 8600 A closed-above, open-below interval is a subset of its closure. (Contributed by Thierry Arnoux, 1-Apr-2017.)
 (,]  C_  [,]
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9457
  Copyright terms: Public domain < Previous  Next >