HomeHome Intuitionistic Logic Explorer
Theorem List (p. 85 of 94)
< 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 - 8401-8500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremltmuldiv2d 8401 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   &     RR   &     C  RR+   =>     C  x.  <  <  C
 
Theoremlemuldivd 8402 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
 RR   &     RR   &     C  RR+   =>     x.  C  <_  <_  C
 
Theoremlemuldiv2d 8403 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
 RR   &     RR   &     C  RR+   =>     C  x.  <_  <_  C
 
Theoremltdivmuld 8404 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   &     RR   &     C  RR+   =>     C 
 <  <  C  x.
 
Theoremltdivmul2d 8405 'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   &     RR   &     C  RR+   =>     C 
 <  <  x.  C
 
Theoremledivmuld 8406 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   &     RR   &     C  RR+   =>     C 
 <_  <_  C  x.
 
Theoremledivmul2d 8407 'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   &     RR   &     C  RR+   =>     C 
 <_  <_  x.  C
 
Theoremltmul1dd 8408 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.)
 RR   &     RR   &     C  RR+   &     <    =>     x.  C  <  x.  C
 
Theoremltmul2dd 8409 Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by Mario Carneiro, 30-May-2016.)
 RR   &     RR   &     C  RR+   &     <    =>     C  x.  <  C  x.
 
Theoremltdiv1dd 8410 Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
 RR   &     RR   &     C  RR+   &     <    =>     C  <  C
 
Theoremlediv1dd 8411 Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
 RR   &     RR   &     C  RR+   &     <_    =>     C  <_  C
 
Theoremlediv12ad 8412 Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   &     RR   &     C  RR+   &     D  RR   &     0  <_    &     <_    &     C  <_  D   =>     D  <_  C
 
Theoremltdiv23d 8413 Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   &     RR+   &     C  RR+   &     <  C   =>     C  <
 
Theoremlediv23d 8414 Swap denominator with other side of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   &     RR+   &     C  RR+   &     <_  C   =>     C  <_
 
Theoremlt2mul2divd 8415 The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   &     RR+   &     C  RR   &     D  RR+   =>     x.  <  C  x.  D  D  <  C
 
3.5.2  Infinity and the extended real number system (cont.)
 
Syntaxcxne 8416 Extend class notation to include the negative of an extended real.
 -e
 
Syntaxcxad 8417 Extend class notation to include addition of extended reals.
 +e
 
Syntaxcxmu 8418 Extend class notation to include multiplication of extended reals.

 xe
 
Definitiondf-xneg 8419 Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.)
 -e  if +oo , -oo ,  if -oo , +oo ,  -u
 
Definitiondf-xadd 8420* Define addition over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)

 +e  RR* ,  RR*  |->  if +oo
 ,  if -oo ,  0 , +oo ,  if -oo ,  if +oo ,  0 , -oo ,  if +oo , +oo ,  if -oo , -oo ,  +
 
Definitiondf-xmul 8421* Define multiplication over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
 xe  RR* ,  RR*  |->  if  0  0 ,  0 ,  if 0  < +oo  < 
 0 -oo  0  < +oo  <  0 -oo , +oo ,  if 0  < -oo  <  0 +oo  0  < -oo  <  0 +oo , -oo ,  x.
 
Theorempnfxr 8422 Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.)
+oo  RR*
 
Theorempnfex 8423 Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
+oo  _V
 
Theoremmnfxr 8424 Minus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
-oo  RR*
 
Theoremltxr 8425 The 'less than' binary relation on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. (Contributed by NM, 14-Oct-2005.)
 RR*  RR*  <  RR  RR  <RR -oo +oo  RR +oo -oo  RR
 
Theoremelxr 8426 Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)
 RR*  RR +oo -oo
 
Theorempnfnemnf 8427 Plus and minus infinity are different elements of  RR*. (Contributed by NM, 14-Oct-2005.)
+oo  =/= -oo
 
Theoremmnfnepnf 8428 Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
-oo  =/= +oo
 
Theoremxrnemnf 8429 An extended real other than minus infinity is real or positive infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  =/= -oo  RR +oo
 
Theoremxrnepnf 8430 An extended real other than plus infinity is real or negative infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  =/= +oo  RR -oo
 
Theoremxrltnr 8431 The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.)
 RR*  <
 
Theoremltpnf 8432 Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
 RR  < +oo
 
Theorem0ltpnf 8433 Zero is less than plus infinity (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
 0  < +oo
 
Theoremmnflt 8434 Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)
 RR -oo  <
 
Theoremmnflt0 8435 Minus infinity is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
-oo  <  0
 
Theoremmnfltpnf 8436 Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
-oo  < +oo
 
Theoremmnfltxr 8437 Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006.)
 RR +oo -oo  <
 
Theorempnfnlt 8438 No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.)
 RR* +oo  <
 
Theoremnltmnf 8439 No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.)
 RR*  < -oo
 
Theorempnfge 8440 Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)
 RR*  <_ +oo
 
Theorem0lepnf 8441 0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.)
 0  <_ +oo
 
Theoremnn0pnfge0 8442 If a number is a nonnegative integer or positive infinity, it is greater than or equal to 0. (Contributed by Alexander van der Vekens, 6-Jan-2018.)
 N  NN0  N +oo  0  <_  N
 
Theoremmnfle 8443 Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.)
 RR* -oo  <_
 
Theoremxrltnsym 8444 Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005.)
 RR*  RR*  <  <
 
Theoremxrltnsym2 8445 'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007.)
 RR*  RR*  <  <
 
Theoremxrlttr 8446 Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.)
 RR*  RR*  C  RR*  <  <  C  <  C
 
Theoremxrltso 8447 'Less than' is a weakly linear ordering on the extended reals. (Contributed by NM, 15-Oct-2005.)

 <  Or  RR*
 
Theoremxrlttri3 8448 Extended real version of lttri3 6855. (Contributed by NM, 9-Feb-2006.)
 RR*  RR*  <  <
 
Theoremxrltle 8449 'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.)
 RR*  RR*  <  <_
 
Theoremxrleid 8450 'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007.)
 RR*  <_
 
Theoremxrletri3 8451 Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
 RR*  RR*  <_  <_
 
Theoremxrlelttr 8452 Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
 RR*  RR*  C  RR*  <_  <  C  <  C
 
Theoremxrltletr 8453 Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
 RR*  RR*  C  RR*  <  <_  C  <  C
 
Theoremxrletr 8454 Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.)
 RR*  RR*  C  RR*  <_  <_  C  <_  C
 
Theoremxrlttrd 8455 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
 RR*   &     RR*   &     C  RR*   &     <    &     <  C   =>     <  C
 
Theoremxrlelttrd 8456 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
 RR*   &     RR*   &     C  RR*   &     <_    &     <  C   =>     <  C
 
Theoremxrltletrd 8457 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
 RR*   &     RR*   &     C  RR*   &     <    &     <_  C   =>     <  C
 
Theoremxrletrd 8458 Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
 RR*   &     RR*   &     C  RR*   &     <_    &     <_  C   =>     <_  C
 
Theoremxrltne 8459 'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.)
 RR*  RR*  <  =/=
 
Theoremnltpnft 8460 An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.)
 RR* +oo  < +oo
 
Theoremngtmnft 8461 An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.)
 RR* -oo -oo  <
 
Theoremxrrebnd 8462 An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.)
 RR*  RR -oo  <  < +oo
 
Theoremxrre 8463 A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.)
 RR*  RR -oo  <  <_  RR
 
Theoremxrre2 8464 An extended real between two others is real. (Contributed by NM, 6-Feb-2007.)
 RR*  RR*  C  RR*  <  <  C  RR
 
Theoremxrre3 8465 A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.)
 RR*  RR 
 <_  < +oo  RR
 
Theoremge0gtmnf 8466 A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  0  <_ -oo  <
 
Theoremge0nemnf 8467 A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  0  <_  =/= -oo
 
Theoremxrrege0 8468 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 8469* 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 8470 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 8471 Minus +oo. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)
 -e +oo -oo
 
Theoremxnegmnf 8472 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 8473 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 8474 The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
 -e 0  0
 
Theoremxnegcl 8475 Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  -e  RR*
 
Theoremxnegneg 8476 Extended real version of negneg 7017. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  -e  -e
 
Theoremxneg11 8477 Extended real version of neg11 7018. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  RR*  -e  -e
 
Theoremxltnegi 8478 Forward direction of xltneg 8479. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  RR*  <  -e  <  -e
 
Theoremxltneg 8479 Extended real version of ltneg 7212. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  RR*  <  -e  <  -e
 
Theoremxleneg 8480 Extended real version of leneg 7215. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  RR*  <_  -e  <_  -e
 
Theoremxlt0neg1 8481 Extended real version of lt0neg1 7218. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  <  0  0  <  -e
 
Theoremxlt0neg2 8482 Extended real version of lt0neg2 7219. (Contributed by Mario Carneiro, 20-Aug-2015.)
 RR*  0  <  -e  <  0
 
Theoremxle0neg1 8483 Extended real version of le0neg1 7220. (Contributed by Mario Carneiro, 9-Sep-2015.)
 RR*  <_  0  0  <_  -e
 
Theoremxle0neg2 8484 Extended real version of le0neg2 7221. (Contributed by Mario Carneiro, 9-Sep-2015.)
 RR*  0  <_  -e  <_  0
 
Theoremxnegcld 8485 Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.)
 RR*   =>     -e  RR*
 
Theoremxrex 8486 The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
 RR*  _V
 
3.5.3  Real number intervals
 
Syntaxcioo 8487 Extend class notation with the set of open intervals of extended reals.
 (,)
 
Syntaxcioc 8488 Extend class notation with the set of open-below, closed-above intervals of extended reals.
 (,]
 
Syntaxcico 8489 Extend class notation with the set of closed-below, open-above intervals of extended reals.
 [,)
 
Syntaxcicc 8490 Extend class notation with the set of closed intervals of extended reals.
 [,]
 
Definitiondf-ioo 8491* Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.)

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

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

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

 [,]  RR* ,  RR*  |->  {  RR*  |  <_  <_  }
 
Theoremixxval 8495* 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 8496* 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 8497* 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 8498* 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 8499* 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 8500* 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
    < 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-9381
  Copyright terms: Public domain < Previous  Next >