Type  Label  Description 
Statement 

Theorem  5nn0 8201 
5 is a nonnegative integer. (Contributed by Mario Carneiro,
19Apr2015.)



Theorem  6nn0 8202 
6 is a nonnegative integer. (Contributed by Mario Carneiro,
19Apr2015.)



Theorem  7nn0 8203 
7 is a nonnegative integer. (Contributed by Mario Carneiro,
19Apr2015.)



Theorem  8nn0 8204 
8 is a nonnegative integer. (Contributed by Mario Carneiro,
19Apr2015.)



Theorem  9nn0 8205 
9 is a nonnegative integer. (Contributed by Mario Carneiro,
19Apr2015.)



Theorem  10nn0 8206 
10 is a nonnegative integer. (Contributed by Mario Carneiro,
19Apr2015.)



Theorem  nn0ge0 8207 
A nonnegative integer is greater than or equal to zero. (Contributed by
NM, 9May2004.) (Revised by Mario Carneiro, 16May2014.)



Theorem  nn0nlt0 8208 
A nonnegative integer is not less than zero. (Contributed by NM,
9May2004.) (Revised by Mario Carneiro, 27May2016.)



Theorem  nn0ge0i 8209 
Nonnegative integers are nonnegative. (Contributed by Raph Levien,
10Dec2002.)



Theorem  nn0le0eq0 8210 
A nonnegative integer is less than or equal to zero iff it is equal to
zero. (Contributed by NM, 9Dec2005.)



Theorem  nn0p1gt0 8211 
A nonnegative integer increased by 1 is greater than 0. (Contributed by
Alexander van der Vekens, 3Oct2018.)



Theorem  nnnn0addcl 8212 
A positive integer plus a nonnegative integer is a positive integer.
(Contributed by NM, 20Apr2005.) (Proof shortened by Mario Carneiro,
16May2014.)



Theorem  nn0nnaddcl 8213 
A nonnegative integer plus a positive integer is a positive integer.
(Contributed by NM, 22Dec2005.)



Theorem  0mnnnnn0 8214 
The result of subtracting a positive integer from 0 is not a nonnegative
integer. (Contributed by Alexander van der Vekens, 19Mar2018.)



Theorem  un0addcl 8215 
If is closed under
addition, then so is
.
(Contributed by Mario Carneiro, 17Jul2014.)



Theorem  un0mulcl 8216 
If is closed under
multiplication, then so is .
(Contributed by Mario Carneiro, 17Jul2014.)



Theorem  nn0addcl 8217 
Closure of addition of nonnegative integers. (Contributed by Raph Levien,
10Dec2002.) (Proof shortened by Mario Carneiro, 17Jul2014.)



Theorem  nn0mulcl 8218 
Closure of multiplication of nonnegative integers. (Contributed by NM,
22Jul2004.) (Proof shortened by Mario Carneiro, 17Jul2014.)



Theorem  nn0addcli 8219 
Closure of addition of nonnegative integers, inference form.
(Contributed by Raph Levien, 10Dec2002.)



Theorem  nn0mulcli 8220 
Closure of multiplication of nonnegative integers, inference form.
(Contributed by Raph Levien, 10Dec2002.)



Theorem  nn0p1nn 8221 
A nonnegative integer plus 1 is a positive integer. (Contributed by Raph
Levien, 30Jun2006.) (Revised by Mario Carneiro, 16May2014.)



Theorem  peano2nn0 8222 
Second Peano postulate for nonnegative integers. (Contributed by NM,
9May2004.)



Theorem  nnm1nn0 8223 
A positive integer minus 1 is a nonnegative integer. (Contributed by
Jason Orendorff, 24Jan2007.) (Revised by Mario Carneiro,
16May2014.)



Theorem  elnn0nn 8224 
The nonnegative integer property expressed in terms of positive integers.
(Contributed by NM, 10May2004.) (Proof shortened by Mario Carneiro,
16May2014.)



Theorem  elnnnn0 8225 
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 10May2004.)



Theorem  elnnnn0b 8226 
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 1Sep2005.)



Theorem  elnnnn0c 8227 
The positive integer property expressed in terms of nonnegative integers.
(Contributed by NM, 10Jan2006.)



Theorem  nn0addge1 8228 
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10Mar2005.)



Theorem  nn0addge2 8229 
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10Mar2005.)



Theorem  nn0addge1i 8230 
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10Mar2005.)



Theorem  nn0addge2i 8231 
A number is less than or equal to itself plus a nonnegative integer.
(Contributed by NM, 10Mar2005.)



Theorem  nn0le2xi 8232 
A nonnegative integer is less than or equal to twice itself.
(Contributed by Raph Levien, 10Dec2002.)



Theorem  nn0lele2xi 8233 
'Less than or equal to' implies 'less than or equal to twice' for
nonnegative integers. (Contributed by Raph Levien, 10Dec2002.)



Theorem  nn0supp 8234 
Two ways to write the support of a function on . (Contributed by
Mario Carneiro, 29Dec2014.)



Theorem  nnnn0d 8235 
A positive integer is a nonnegative integer. (Contributed by Mario
Carneiro, 27May2016.)



Theorem  nn0red 8236 
A nonnegative integer is a real number. (Contributed by Mario Carneiro,
27May2016.)



Theorem  nn0cnd 8237 
A nonnegative integer is a complex number. (Contributed by Mario
Carneiro, 27May2016.)



Theorem  nn0ge0d 8238 
A nonnegative integer is greater than or equal to zero. (Contributed by
Mario Carneiro, 27May2016.)



Theorem  nn0addcld 8239 
Closure of addition of nonnegative integers, inference form.
(Contributed by Mario Carneiro, 27May2016.)



Theorem  nn0mulcld 8240 
Closure of multiplication of nonnegative integers, inference form.
(Contributed by Mario Carneiro, 27May2016.)



Theorem  nn0readdcl 8241 
Closure law for addition of reals, restricted to nonnegative integers.
(Contributed by Alexander van der Vekens, 6Apr2018.)



Theorem  nn0ge2m1nn 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, 1Aug2018.) (Revised by AV, 4Jan2020.)



Theorem  nn0ge2m1nn0 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, 1Aug2018.)



Theorem  nn0nndivcl 8244 
Closure law for dividing of a nonnegative integer by a positive integer.
(Contributed by Alexander van der Vekens, 14Apr2018.)



3.4.8 Integers (as a subset of complex
numbers)


Syntax  cz 8245 
Extend class notation to include the class of integers.



Definition  dfz 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, 8Jan2002.)



Theorem  elz 8247 
Membership in the set of integers. (Contributed by NM, 8Jan2002.)



Theorem  nnnegz 8248 
The negative of a positive integer is an integer. (Contributed by NM,
12Jan2002.)



Theorem  zre 8249 
An integer is a real. (Contributed by NM, 8Jan2002.)



Theorem  zcn 8250 
An integer is a complex number. (Contributed by NM, 9May2004.)



Theorem  zrei 8251 
An integer is a real number. (Contributed by NM, 14Jul2005.)



Theorem  zssre 8252 
The integers are a subset of the reals. (Contributed by NM,
2Aug2004.)



Theorem  zsscn 8253 
The integers are a subset of the complex numbers. (Contributed by NM,
2Aug2004.)



Theorem  zex 8254 
The set of integers exists. (Contributed by NM, 30Jul2004.) (Revised
by Mario Carneiro, 17Nov2014.)



Theorem  elnnz 8255 
Positive integer property expressed in terms of integers. (Contributed by
NM, 8Jan2002.)



Theorem  0z 8256 
Zero is an integer. (Contributed by NM, 12Jan2002.)



Theorem  0zd 8257 
Zero is an integer, deductive form (common case). (Contributed by David
A. Wheeler, 8Dec2018.)



Theorem  elnn0z 8258 
Nonnegative integer property expressed in terms of integers. (Contributed
by NM, 9May2004.)



Theorem  elznn0nn 8259 
Integer property expressed in terms nonnegative integers and positive
integers. (Contributed by NM, 10May2004.)



Theorem  elznn0 8260 
Integer property expressed in terms of nonnegative integers. (Contributed
by NM, 9May2004.)



Theorem  elznn 8261 
Integer property expressed in terms of positive integers and nonnegative
integers. (Contributed by NM, 12Jul2005.)



Theorem  nnssz 8262 
Positive integers are a subset of integers. (Contributed by NM,
9Jan2002.)



Theorem  nn0ssz 8263 
Nonnegative integers are a subset of the integers. (Contributed by NM,
9May2004.)



Theorem  nnz 8264 
A positive integer is an integer. (Contributed by NM, 9May2004.)



Theorem  nn0z 8265 
A nonnegative integer is an integer. (Contributed by NM, 9May2004.)



Theorem  nnzi 8266 
A positive integer is an integer. (Contributed by Mario Carneiro,
18Feb2014.)



Theorem  nn0zi 8267 
A nonnegative integer is an integer. (Contributed by Mario Carneiro,
18Feb2014.)



Theorem  elnnz1 8268 
Positive integer property expressed in terms of integers. (Contributed by
NM, 10May2004.) (Proof shortened by Mario Carneiro, 16May2014.)



Theorem  nnzrab 8269 
Positive integers expressed as a subset of integers. (Contributed by NM,
3Oct2004.)



Theorem  nn0zrab 8270 
Nonnegative integers expressed as a subset of integers. (Contributed by
NM, 3Oct2004.)



Theorem  1z 8271 
One is an integer. (Contributed by NM, 10May2004.)



Theorem  1zzd 8272 
1 is an integer, deductive form (common case). (Contributed by David A.
Wheeler, 6Dec2018.)



Theorem  2z 8273 
Two is an integer. (Contributed by NM, 10May2004.)



Theorem  3z 8274 
3 is an integer. (Contributed by David A. Wheeler, 8Dec2018.)



Theorem  4z 8275 
4 is an integer. (Contributed by BJ, 26Mar2020.)



Theorem  znegcl 8276 
Closure law for negative integers. (Contributed by NM, 9May2004.)



Theorem  neg1z 8277 
1 is an integer (common case). (Contributed by David A. Wheeler,
5Dec2018.)



Theorem  znegclb 8278 
A number is an integer iff its negative is. (Contributed by Stefan
O'Rear, 13Sep2014.)



Theorem  nn0negz 8279 
The negative of a nonnegative integer is an integer. (Contributed by NM,
9May2004.)



Theorem  nn0negzi 8280 
The negative of a nonnegative integer is an integer. (Contributed by
Mario Carneiro, 18Feb2014.)



Theorem  peano2z 8281 
Second Peano postulate generalized to integers. (Contributed by NM,
13Feb2005.)



Theorem  zaddcllempos 8282 
Lemma for zaddcl 8285. Special case in which is a positive integer.
(Contributed by Jim Kingdon, 14Mar2020.)



Theorem  peano2zm 8283 
"Reverse" second Peano postulate for integers. (Contributed by NM,
12Sep2005.)



Theorem  zaddcllemneg 8284 
Lemma for zaddcl 8285. Special case in which is a positive
integer. (Contributed by Jim Kingdon, 14Mar2020.)



Theorem  zaddcl 8285 
Closure of addition of integers. (Contributed by NM, 9May2004.) (Proof
shortened by Mario Carneiro, 16May2014.)



Theorem  zsubcl 8286 
Closure of subtraction of integers. (Contributed by NM, 11May2004.)



Theorem  ztri3or0 8287 
Integer trichotomy (with zero). (Contributed by Jim Kingdon,
14Mar2020.)



Theorem  ztri3or 8288 
Integer trichotomy. (Contributed by Jim Kingdon, 14Mar2020.)



Theorem  zletric 8289 
Trichotomy law. (Contributed by Jim Kingdon, 27Mar2020.)



Theorem  zlelttric 8290 
Trichotomy law. (Contributed by Jim Kingdon, 17Apr2020.)



Theorem  zltnle 8291 
'Less than' expressed in terms of 'less than or equal to'. (Contributed
by Jim Kingdon, 14Mar2020.)



Theorem  zleloe 8292 
Integer 'Less than or equal to' expressed in terms of 'less than' or
'equals'. (Contributed by Jim Kingdon, 8Apr2020.)



Theorem  znnnlt1 8293 
An integer is not a positive integer iff it is less than one.
(Contributed by NM, 13Jul2005.)



Theorem  zletr 8294 
Transitive law of ordering for integers. (Contributed by Alexander van
der Vekens, 3Apr2018.)



Theorem  zrevaddcl 8295 
Reverse closure law for addition of integers. (Contributed by NM,
11May2004.)



Theorem  znnsub 8296 
The positive difference of unequal integers is a positive integer.
(Generalization of nnsub 7952.) (Contributed by NM, 11May2004.)



Theorem  zmulcl 8297 
Closure of multiplication of integers. (Contributed by NM,
30Jul2004.)



Theorem  zltp1le 8298 
Integer ordering relation. (Contributed by NM, 10May2004.) (Proof
shortened by Mario Carneiro, 16May2014.)



Theorem  zleltp1 8299 
Integer ordering relation. (Contributed by NM, 10May2004.)



Theorem  zlem1lt 8300 
Integer ordering relation. (Contributed by NM, 13Nov2004.)

