Home Intuitionistic Logic ExplorerTheorem List (p. 83 of 102) < 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 - 8201-8300   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theorem5nn0 8201 5 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)

Theorem6nn0 8202 6 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)

Theorem7nn0 8203 7 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)

Theorem8nn0 8204 8 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)

Theorem9nn0 8205 9 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)

Theorem10nn0 8206 10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)

Theoremnn0ge0 8207 A nonnegative integer is greater than or equal to zero. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 16-May-2014.)

Theoremnn0nlt0 8208 A nonnegative integer is not less than zero. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)

Theoremnn0ge0i 8209 Nonnegative integers are nonnegative. (Contributed by Raph Levien, 10-Dec-2002.)

Theoremnn0le0eq0 8210 A nonnegative integer is less than or equal to zero iff it is equal to zero. (Contributed by NM, 9-Dec-2005.)

Theoremnn0p1gt0 8211 A nonnegative integer increased by 1 is greater than 0. (Contributed by Alexander van der Vekens, 3-Oct-2018.)

Theoremnnnn0addcl 8212 A positive integer plus a nonnegative integer is a positive integer. (Contributed by NM, 20-Apr-2005.) (Proof shortened by Mario Carneiro, 16-May-2014.)

Theoremnn0nnaddcl 8213 A nonnegative integer plus a positive integer is a positive integer. (Contributed by NM, 22-Dec-2005.)

Theorem0mnnnnn0 8214 The result of subtracting a positive integer from 0 is not a nonnegative integer. (Contributed by Alexander van der Vekens, 19-Mar-2018.)

Theoremun0addcl 8215 If is closed under addition, then so is . (Contributed by Mario Carneiro, 17-Jul-2014.)

Theoremun0mulcl 8216 If is closed under multiplication, then so is . (Contributed by Mario Carneiro, 17-Jul-2014.)

Theoremnn0addcl 8217 Closure of addition of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.) (Proof shortened by Mario Carneiro, 17-Jul-2014.)

Theoremnn0mulcl 8218 Closure of multiplication of nonnegative integers. (Contributed by NM, 22-Jul-2004.) (Proof shortened by Mario Carneiro, 17-Jul-2014.)

Theoremnn0addcli 8219 Closure of addition of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-2002.)

Theoremnn0mulcli 8220 Closure of multiplication of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-2002.)

Theoremnn0p1nn 8221 A nonnegative integer plus 1 is a positive integer. (Contributed by Raph Levien, 30-Jun-2006.) (Revised by Mario Carneiro, 16-May-2014.)

Theorempeano2nn0 8222 Second Peano postulate for nonnegative integers. (Contributed by NM, 9-May-2004.)

Theoremnnm1nn0 8223 A positive integer minus 1 is a nonnegative integer. (Contributed by Jason Orendorff, 24-Jan-2007.) (Revised by Mario Carneiro, 16-May-2014.)

Theoremelnn0nn 8224 The nonnegative integer property expressed in terms of positive integers. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)

Theoremelnnnn0 8225 The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-May-2004.)

Theoremelnnnn0b 8226 The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 1-Sep-2005.)

Theoremelnnnn0c 8227 The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-Jan-2006.)

Theoremnn0addge1 8228 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)

Theoremnn0addge2 8229 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)

Theoremnn0addge1i 8230 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)

Theoremnn0addge2i 8231 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)

Theoremnn0le2xi 8232 A nonnegative integer is less than or equal to twice itself. (Contributed by Raph Levien, 10-Dec-2002.)

Theoremnn0lele2xi 8233 'Less than or equal to' implies 'less than or equal to twice' for nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.)

Theoremnn0supp 8234 Two ways to write the support of a function on . (Contributed by Mario Carneiro, 29-Dec-2014.)

Theoremnnnn0d 8235 A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)

Theoremnn0red 8236 A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)

Theoremnn0cnd 8237 A nonnegative integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)

Theoremnn0ge0d 8238 A nonnegative integer is greater than or equal to zero. (Contributed by Mario Carneiro, 27-May-2016.)

Theoremnn0addcld 8239 Closure of addition of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.)

Theoremnn0mulcld 8240 Closure of multiplication of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.)

Theoremnn0readdcl 8241 Closure law for addition of reals, restricted to nonnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.)

Theoremnn0ge2m1nn 8242 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.)

Theoremnn0ge2m1nn0 8243 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.)

Theoremnn0nndivcl 8244 Closure law for dividing of a nonnegative integer by a positive integer. (Contributed by Alexander van der Vekens, 14-Apr-2018.)

3.4.8  Integers (as a subset of complex numbers)

Syntaxcz 8245 Extend class notation to include the class of integers.

Definitiondf-z 8246 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.)

Theoremelz 8247 Membership in the set of integers. (Contributed by NM, 8-Jan-2002.)

Theoremnnnegz 8248 The negative of a positive integer is an integer. (Contributed by NM, 12-Jan-2002.)

Theoremzre 8249 An integer is a real. (Contributed by NM, 8-Jan-2002.)

Theoremzcn 8250 An integer is a complex number. (Contributed by NM, 9-May-2004.)

Theoremzrei 8251 An integer is a real number. (Contributed by NM, 14-Jul-2005.)

Theoremzssre 8252 The integers are a subset of the reals. (Contributed by NM, 2-Aug-2004.)

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

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

Theoremelnnz 8255 Positive integer property expressed in terms of integers. (Contributed by NM, 8-Jan-2002.)

Theorem0z 8256 Zero is an integer. (Contributed by NM, 12-Jan-2002.)

Theorem0zd 8257 Zero is an integer, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)

Theoremelnn0z 8258 Nonnegative integer property expressed in terms of integers. (Contributed by NM, 9-May-2004.)

Theoremelznn0nn 8259 Integer property expressed in terms nonnegative integers and positive integers. (Contributed by NM, 10-May-2004.)

Theoremelznn0 8260 Integer property expressed in terms of nonnegative integers. (Contributed by NM, 9-May-2004.)

Theoremelznn 8261 Integer property expressed in terms of positive integers and nonnegative integers. (Contributed by NM, 12-Jul-2005.)

Theoremnnssz 8262 Positive integers are a subset of integers. (Contributed by NM, 9-Jan-2002.)

Theoremnn0ssz 8263 Nonnegative integers are a subset of the integers. (Contributed by NM, 9-May-2004.)

Theoremnnz 8264 A positive integer is an integer. (Contributed by NM, 9-May-2004.)

Theoremnn0z 8265 A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)

Theoremnnzi 8266 A positive integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)

Theoremnn0zi 8267 A nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)

Theoremelnnz1 8268 Positive integer property expressed in terms of integers. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)

Theoremnnzrab 8269 Positive integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.)

Theoremnn0zrab 8270 Nonnegative integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.)

Theorem1z 8271 One is an integer. (Contributed by NM, 10-May-2004.)

Theorem1zzd 8272 1 is an integer, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)

Theorem2z 8273 Two is an integer. (Contributed by NM, 10-May-2004.)

Theorem3z 8274 3 is an integer. (Contributed by David A. Wheeler, 8-Dec-2018.)

Theorem4z 8275 4 is an integer. (Contributed by BJ, 26-Mar-2020.)

Theoremznegcl 8276 Closure law for negative integers. (Contributed by NM, 9-May-2004.)

Theoremneg1z 8277 -1 is an integer (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)

Theoremznegclb 8278 A number is an integer iff its negative is. (Contributed by Stefan O'Rear, 13-Sep-2014.)

Theoremnn0negz 8279 The negative of a nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)

Theoremnn0negzi 8280 The negative of a nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)

Theorempeano2z 8281 Second Peano postulate generalized to integers. (Contributed by NM, 13-Feb-2005.)

Theoremzaddcllempos 8282 Lemma for zaddcl 8285. Special case in which is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)

Theorempeano2zm 8283 "Reverse" second Peano postulate for integers. (Contributed by NM, 12-Sep-2005.)

Theoremzaddcllemneg 8284 Lemma for zaddcl 8285. Special case in which is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)

Theoremzaddcl 8285 Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)

Theoremzsubcl 8286 Closure of subtraction of integers. (Contributed by NM, 11-May-2004.)

Theoremztri3or0 8287 Integer trichotomy (with zero). (Contributed by Jim Kingdon, 14-Mar-2020.)

Theoremztri3or 8288 Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.)

Theoremzletric 8289 Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.)

Theoremzlelttric 8290 Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.)

Theoremzltnle 8291 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 14-Mar-2020.)

Theoremzleloe 8292 Integer 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.)

Theoremznnnlt1 8293 An integer is not a positive integer iff it is less than one. (Contributed by NM, 13-Jul-2005.)

Theoremzletr 8294 Transitive law of ordering for integers. (Contributed by Alexander van der Vekens, 3-Apr-2018.)

Theoremzrevaddcl 8295 Reverse closure law for addition of integers. (Contributed by NM, 11-May-2004.)

Theoremznnsub 8296 The positive difference of unequal integers is a positive integer. (Generalization of nnsub 7952.) (Contributed by NM, 11-May-2004.)

Theoremzmulcl 8297 Closure of multiplication of integers. (Contributed by NM, 30-Jul-2004.)

Theoremzltp1le 8298 Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)

Theoremzleltp1 8299 Integer ordering relation. (Contributed by NM, 10-May-2004.)

Theoremzlem1lt 8300 Integer ordering relation. (Contributed by NM, 13-Nov-2004.)

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-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10124
 Copyright terms: Public domain < Previous  Next >