HomeHome Intuitionistic Logic Explorer
Theorem List (p. 81 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 - 8001-8100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremelnnnn0 8001 The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-May-2004.)
 N  NN  N  CC  N  -  1  NN0
 
Theoremelnnnn0b 8002 The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 1-Sep-2005.)
 N  NN  N  NN0  0  <  N
 
Theoremelnnnn0c 8003 The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-Jan-2006.)
 N  NN  N  NN0  1  <_  N
 
Theoremnn0addge1 8004 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
 RR  N  NN0  <_  +  N
 
Theoremnn0addge2 8005 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
 RR  N  NN0  <_  N  +
 
Theoremnn0addge1i 8006 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
 RR   &     N  NN0   =>     <_  +  N
 
Theoremnn0addge2i 8007 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
 RR   &     N  NN0   =>     <_  N  +
 
Theoremnn0le2xi 8008 A nonnegative integer is less than or equal to twice itself. (Contributed by Raph Levien, 10-Dec-2002.)
 N  NN0   =>     N  <_  2  x.  N
 
Theoremnn0lele2xi 8009 'Less than or equal to' implies 'less than or equal to twice' for nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.)
 M  NN0   &     N  NN0   =>     N  <_  M  N  <_  2  x.  M
 
Theoremnn0supp 8010 Two ways to write the support of a function on  NN0. (Contributed by Mario Carneiro, 29-Dec-2014.)
 F : I --> NN0  `' F " _V  \  {
 0 }  `' F " NN
 
Theoremnnnn0d 8011 A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)
 NN   =>     NN0
 
Theoremnn0red 8012 A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
 NN0   =>     RR
 
Theoremnn0cnd 8013 A nonnegative integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
 NN0   =>     CC
 
Theoremnn0ge0d 8014 A nonnegative integer is greater than or equal to zero. (Contributed by Mario Carneiro, 27-May-2016.)
 NN0   =>     0  <_
 
Theoremnn0addcld 8015 Closure of addition of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.)
 NN0   &     NN0   =>     + 
 NN0
 
Theoremnn0mulcld 8016 Closure of multiplication of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.)
 NN0   &     NN0   =>     x. 
 NN0
 
Theoremnn0readdcl 8017 Closure law for addition of reals, restricted to nonnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
 NN0  NN0  +  RR
 
Theoremnn0ge2m1nn 8018 If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 4-Jan-2020.)
 N  NN0  2  <_  N  N  -  1  NN
 
Theoremnn0ge2m1nn0 8019 If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is also a nonnegative integer. (Contributed by Alexander van der Vekens, 1-Aug-2018.)
 N  NN0  2  <_  N  N  -  1  NN0
 
Theoremnn0nndivcl 8020 Closure law for dividing of a nonnegative integer by a positive integer. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
 K  NN0  L  NN  K  L  RR
 
3.4.8  Integers (as a subset of complex numbers)
 
Syntaxcz 8021 Extend class notation to include the class of integers.

 ZZ
 
Definitiondf-z 8022 Define the set of integers, which are the positive and negative integers together with zero. Definition of integers in [Apostol] p. 22. The letter Z abbreviates the German word Zahlen meaning "numbers." (Contributed by NM, 8-Jan-2002.)

 ZZ  { n  RR  |  n  0  n  NN  -u n  NN }
 
Theoremelz 8023 Membership in the set of integers. (Contributed by NM, 8-Jan-2002.)
 N  ZZ  N  RR  N  0  N  NN  -u N  NN
 
Theoremnnnegz 8024 The negative of a positive integer is an integer. (Contributed by NM, 12-Jan-2002.)
 N  NN  -u N  ZZ
 
Theoremzre 8025 An integer is a real. (Contributed by NM, 8-Jan-2002.)
 N  ZZ  N  RR
 
Theoremzcn 8026 An integer is a complex number. (Contributed by NM, 9-May-2004.)
 N  ZZ  N  CC
 
Theoremzrei 8027 An integer is a real number. (Contributed by NM, 14-Jul-2005.)
 ZZ   =>     RR
 
Theoremzssre 8028 The integers are a subset of the reals. (Contributed by NM, 2-Aug-2004.)

 ZZ  C_  RR
 
Theoremzsscn 8029 The integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)

 ZZ  C_  CC
 
Theoremzex 8030 The set of integers exists. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)

 ZZ  _V
 
Theoremelnnz 8031 Positive integer property expressed in terms of integers. (Contributed by NM, 8-Jan-2002.)
 N  NN  N  ZZ  0  <  N
 
Theorem0z 8032 Zero is an integer. (Contributed by NM, 12-Jan-2002.)
 0  ZZ
 
Theorem0zd 8033 Zero is an integer, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
 0  ZZ
 
Theoremelnn0z 8034 Nonnegative integer property expressed in terms of integers. (Contributed by NM, 9-May-2004.)
 N  NN0  N  ZZ  0  <_  N
 
Theoremelznn0nn 8035 Integer property expressed in terms nonnegative integers and positive integers. (Contributed by NM, 10-May-2004.)
 N  ZZ  N  NN0  N  RR  -u N  NN
 
Theoremelznn0 8036 Integer property expressed in terms of nonnegative integers. (Contributed by NM, 9-May-2004.)
 N  ZZ  N  RR  N  NN0  -u N  NN0
 
Theoremelznn 8037 Integer property expressed in terms of positive integers and nonnegative integers. (Contributed by NM, 12-Jul-2005.)
 N  ZZ  N  RR  N  NN  -u N  NN0
 
Theoremnnssz 8038 Positive integers are a subset of integers. (Contributed by NM, 9-Jan-2002.)

 NN  C_  ZZ
 
Theoremnn0ssz 8039 Nonnegative integers are a subset of the integers. (Contributed by NM, 9-May-2004.)

 NN0  C_  ZZ
 
Theoremnnz 8040 A positive integer is an integer. (Contributed by NM, 9-May-2004.)
 N  NN  N  ZZ
 
Theoremnn0z 8041 A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
 N  NN0 
 N  ZZ
 
Theoremnnzi 8042 A positive integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
 N  NN   =>     N  ZZ
 
Theoremnn0zi 8043 A nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
 N  NN0   =>     N  ZZ
 
Theoremelnnz1 8044 Positive integer property expressed in terms of integers. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
 N  NN  N  ZZ  1  <_  N
 
Theoremnnzrab 8045 Positive integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.)

 NN  {  ZZ  |  1  <_  }
 
Theoremnn0zrab 8046 Nonnegative integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.)

 NN0  {  ZZ  |  0  <_  }
 
Theorem1z 8047 One is an integer. (Contributed by NM, 10-May-2004.)
 1  ZZ
 
Theorem1zzd 8048 1 is an integer, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
 1  ZZ
 
Theorem2z 8049 Two is an integer. (Contributed by NM, 10-May-2004.)
 2  ZZ
 
Theorem3z 8050 3 is an integer. (Contributed by David A. Wheeler, 8-Dec-2018.)
 3  ZZ
 
Theorem4z 8051 4 is an integer. (Contributed by BJ, 26-Mar-2020.)
 4  ZZ
 
Theoremznegcl 8052 Closure law for negative integers. (Contributed by NM, 9-May-2004.)
 N  ZZ  -u N  ZZ
 
Theoremneg1z 8053 -1 is an integer (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
 -u 1  ZZ
 
Theoremznegclb 8054 A number is an integer iff its negative is. (Contributed by Stefan O'Rear, 13-Sep-2014.)
 CC  ZZ  -u  ZZ
 
Theoremnn0negz 8055 The negative of a nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
 N  NN0  -u N  ZZ
 
Theoremnn0negzi 8056 The negative of a nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
 N  NN0   =>     -u N  ZZ
 
Theorempeano2z 8057 Second Peano postulate generalized to integers. (Contributed by NM, 13-Feb-2005.)
 N  ZZ  N  +  1  ZZ
 
Theoremzaddcllempos 8058 Lemma for zaddcl 8061. Special case in which  N is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
 M  ZZ  N  NN  M  +  N  ZZ
 
Theorempeano2zm 8059 "Reverse" second Peano postulate for integers. (Contributed by NM, 12-Sep-2005.)
 N  ZZ  N  -  1  ZZ
 
Theoremzaddcllemneg 8060 Lemma for zaddcl 8061. Special case in which  -u N is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
 M  ZZ  N  RR  -u N  NN  M  +  N  ZZ
 
Theoremzaddcl 8061 Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
 M  ZZ  N  ZZ  M  +  N  ZZ
 
Theoremzsubcl 8062 Closure of subtraction of integers. (Contributed by NM, 11-May-2004.)
 M  ZZ  N  ZZ  M  -  N  ZZ
 
Theoremztri3or0 8063 Integer trichotomy (with zero). (Contributed by Jim Kingdon, 14-Mar-2020.)
 N  ZZ  N  <  0  N  0  0  <  N
 
Theoremztri3or 8064 Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.)
 M  ZZ  N  ZZ  M  <  N  M  N  N  <  M
 
Theoremzletric 8065 Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.)
 ZZ  ZZ  <_  <_
 
Theoremzlelttric 8066 Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.)
 ZZ  ZZ  <_  <
 
Theoremzltnle 8067 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 14-Mar-2020.)
 ZZ  ZZ  <  <_
 
Theoremzleloe 8068 Integer 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.)
 ZZ  ZZ  <_  <
 
Theoremznnnlt1 8069 An integer is not a positive integer iff it is less than one. (Contributed by NM, 13-Jul-2005.)
 N  ZZ  N  NN  N  <  1
 
Theoremzletr 8070 Transitive law of ordering for integers. (Contributed by Alexander van der Vekens, 3-Apr-2018.)
 J  ZZ  K  ZZ  L  ZZ  J  <_  K  K  <_  L  J  <_  L
 
Theoremzrevaddcl 8071 Reverse closure law for addition of integers. (Contributed by NM, 11-May-2004.)
 N  ZZ  M  CC  M  +  N  ZZ  M  ZZ
 
Theoremznnsub 8072 The positive difference of unequal integers is a positive integer. (Generalization of nnsub 7733.) (Contributed by NM, 11-May-2004.)
 M  ZZ  N  ZZ  M  <  N  N  -  M  NN
 
Theoremzmulcl 8073 Closure of multiplication of integers. (Contributed by NM, 30-Jul-2004.)
 M  ZZ  N  ZZ  M  x.  N  ZZ
 
Theoremzltp1le 8074 Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
 M  ZZ  N  ZZ  M  <  N  M  +  1  <_  N
 
Theoremzleltp1 8075 Integer ordering relation. (Contributed by NM, 10-May-2004.)
 M  ZZ  N  ZZ  M  <_  N  M  <  N  +  1
 
Theoremzlem1lt 8076 Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
 M  ZZ  N  ZZ  M  <_  N  M  -  1  <  N
 
Theoremzltlem1 8077 Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
 M  ZZ  N  ZZ  M  <  N  M  <_  N  -  1
 
Theoremzgt0ge1 8078 An integer greater than  0 is greater than or equal to  1. (Contributed by AV, 14-Oct-2018.)
 Z  ZZ  0  <  Z  1  <_  Z
 
Theoremnnleltp1 8079 Positive integer ordering relation. (Contributed by NM, 13-Aug-2001.) (Proof shortened by Mario Carneiro, 16-May-2014.)
 NN  NN  <_  <  +  1
 
Theoremnnltp1le 8080 Positive integer ordering relation. (Contributed by NM, 19-Aug-2001.)
 NN  NN  <  +  1  <_
 
Theoremnnaddm1cl 8081 Closure of addition of positive integers minus one. (Contributed by NM, 6-Aug-2003.) (Proof shortened by Mario Carneiro, 16-May-2014.)
 NN  NN  +  -  1  NN
 
Theoremnn0ltp1le 8082 Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Dec-2002.) (Proof shortened by Mario Carneiro, 16-May-2014.)
 M  NN0  N  NN0  M  <  N  M  +  1  <_  N
 
Theoremnn0leltp1 8083 Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Apr-2004.)
 M  NN0  N  NN0  M  <_  N  M  <  N  +  1
 
Theoremnn0ltlem1 8084 Nonnegative integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
 M  NN0  N  NN0  M  <  N  M  <_  N  -  1
 
Theoremznn0sub 8085 The nonnegative difference of integers is a nonnegative integer. (Generalization of nn0sub 8086.) (Contributed by NM, 14-Jul-2005.)
 M  ZZ  N  ZZ  M  <_  N  N  -  M  NN0
 
Theoremnn0sub 8086 Subtraction of nonnegative integers. (Contributed by NM, 9-May-2004.)
 M  NN0  N  NN0  M  <_  N  N  -  M  NN0
 
Theoremnn0n0n1ge2 8087 A nonnegative integer which is neither 0 nor 1 is greater than or equal to 2. (Contributed by Alexander van der Vekens, 6-Dec-2017.)
 N  NN0  N  =/=  0  N  =/=  1  2  <_  N
 
Theoremelz2 8088* Membership in the set of integers. Commonly used in constructions of the integers as equivalence classes under subtraction of the positive integers. (Contributed by Mario Carneiro, 16-May-2014.)
 N  ZZ  NN  NN  N  -
 
Theoremdfz2 8089 Alternative definition of the integers, based on elz2 8088. (Contributed by Mario Carneiro, 16-May-2014.)

 ZZ  -  " NN  X.  NN
 
Theoremnn0sub2 8090 Subtraction of nonnegative integers. (Contributed by NM, 4-Sep-2005.)
 M  NN0  N  NN0  M  <_  N  N  -  M 
 NN0
 
Theoremzapne 8091 Apartness is equivalent to not equal for integers. (Contributed by Jim Kingdon, 14-Mar-2020.)
 M  ZZ  N  ZZ  M #  N  M  =/=  N
 
Theoremzdceq 8092 Equality of integers is decidable. (Contributed by Jim Kingdon, 14-Mar-2020.)
 ZZ  ZZ DECID
 
Theoremzdcle 8093 Integer  <_ is decidable. (Contributed by Jim Kingdon, 7-Apr-2020.)
 ZZ  ZZ DECID  <_
 
Theoremzdclt 8094 Integer  < is decidable. (Contributed by Jim Kingdon, 1-Jun-2020.)
 ZZ  ZZ DECID  <
 
Theoremzltlen 8095 Integer 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 7413 which is a similar result for complex numbers. (Contributed by Jim Kingdon, 14-Mar-2020.)
 ZZ  ZZ  <  <_  =/=
 
Theoremnn0n0n1ge2b 8096 A nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by Alexander van der Vekens, 17-Jan-2018.)
 N  NN0  N  =/=  0  N  =/=  1  2  <_  N
 
Theoremnn0lt10b 8097 A nonnegative integer less than  1 is  0. (Contributed by Paul Chapman, 22-Jun-2011.)
 N  NN0  N  <  1  N  0
 
Theoremnn0lt2 8098 A nonnegative integer less than 2 must be 0 or 1. (Contributed by Alexander van der Vekens, 16-Sep-2018.)
 N  NN0  N  <  2  N  0  N  1
 
Theoremnn0lem1lt 8099 Nonnegative integer ordering relation. (Contributed by NM, 21-Jun-2005.)
 M  NN0  N  NN0  M  <_  N  M  -  1  <  N
 
Theoremnnlem1lt 8100 Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
 M  NN  N  NN  M  <_  N  M  -  1  <  N
    < 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 >