Type  Label  Description 
Statement 

Theorem  nn0nndivcl 8301 
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 8302 
Extend class notation to include the class of integers.



Definition  dfz 8303 
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 8304 
Membership in the set of integers. (Contributed by NM, 8Jan2002.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  nzadd 8354 
The sum of a real number not being an integer and an integer is not an
integer. Note that "not being an integer" in this case means
"the
negation of is an integer" rather than "is apart from any
integer" (given
excluded middle, those two would be equivalent). (Contributed by AV,
19Jul2021.)



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



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



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



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



Theorem  zltlem1 8359 
Integer ordering relation. (Contributed by NM, 13Nov2004.)



Theorem  zgt0ge1 8360 
An integer greater than
is greater than or equal to .
(Contributed by AV, 14Oct2018.)



Theorem  nnleltp1 8361 
Positive integer ordering relation. (Contributed by NM, 13Aug2001.)
(Proof shortened by Mario Carneiro, 16May2014.)



Theorem  nnltp1le 8362 
Positive integer ordering relation. (Contributed by NM, 19Aug2001.)



Theorem  nnaddm1cl 8363 
Closure of addition of positive integers minus one. (Contributed by NM,
6Aug2003.) (Proof shortened by Mario Carneiro, 16May2014.)



Theorem  nn0ltp1le 8364 
Nonnegative integer ordering relation. (Contributed by Raph Levien,
10Dec2002.) (Proof shortened by Mario Carneiro, 16May2014.)



Theorem  nn0leltp1 8365 
Nonnegative integer ordering relation. (Contributed by Raph Levien,
10Apr2004.)



Theorem  nn0ltlem1 8366 
Nonnegative integer ordering relation. (Contributed by NM, 10May2004.)
(Proof shortened by Mario Carneiro, 16May2014.)



Theorem  znn0sub 8367 
The nonnegative difference of integers is a nonnegative integer.
(Generalization of nn0sub 8368.) (Contributed by NM, 14Jul2005.)



Theorem  nn0sub 8368 
Subtraction of nonnegative integers. (Contributed by NM, 9May2004.)



Theorem  nn0n0n1ge2 8369 
A nonnegative integer which is neither 0 nor 1 is greater than or equal to
2. (Contributed by Alexander van der Vekens, 6Dec2017.)



Theorem  elz2 8370* 
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, 16May2014.)



Theorem  dfz2 8371 
Alternative definition of the integers, based on elz2 8370.
(Contributed
by Mario Carneiro, 16May2014.)



Theorem  nn0sub2 8372 
Subtraction of nonnegative integers. (Contributed by NM, 4Sep2005.)



Theorem  zapne 8373 
Apartness is equivalent to not equal for integers. (Contributed by Jim
Kingdon, 14Mar2020.)

# 

Theorem  zdceq 8374 
Equality of integers is decidable. (Contributed by Jim Kingdon,
14Mar2020.)

DECID


Theorem  zdcle 8375 
Integer is
decidable. (Contributed by Jim Kingdon, 7Apr2020.)

DECID 

Theorem  zdclt 8376 
Integer is
decidable. (Contributed by Jim Kingdon, 1Jun2020.)

DECID 

Theorem  zltlen 8377 
Integer 'Less than' expressed in terms of 'less than or equal to'. Also
see ltleap 7695 which is a similar result for real numbers.
(Contributed by
Jim Kingdon, 14Mar2020.)



Theorem  nn0n0n1ge2b 8378 
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, 17Jan2018.)



Theorem  nn0lt10b 8379 
A nonnegative integer less than is .
(Contributed by Paul
Chapman, 22Jun2011.)



Theorem  nn0lt2 8380 
A nonnegative integer less than 2 must be 0 or 1. (Contributed by
Alexander van der Vekens, 16Sep2018.)



Theorem  nn0lem1lt 8381 
Nonnegative integer ordering relation. (Contributed by NM,
21Jun2005.)



Theorem  nnlem1lt 8382 
Positive integer ordering relation. (Contributed by NM, 21Jun2005.)



Theorem  nnltlem1 8383 
Positive integer ordering relation. (Contributed by NM, 21Jun2005.)



Theorem  nnm1ge0 8384 
A positive integer decreased by 1 is greater than or equal to 0.
(Contributed by AV, 30Oct2018.)



Theorem  nn0ge0div 8385 
Division of a nonnegative integer by a positive number is not negative.
(Contributed by Alexander van der Vekens, 14Apr2018.)



Theorem  zdiv 8386* 
Two ways to express " divides .
(Contributed by NM,
3Oct2008.)



Theorem  zdivadd 8387 
Property of divisibility: if divides
and then it divides
. (Contributed by NM, 3Oct2008.)



Theorem  zdivmul 8388 
Property of divisibility: if divides
then it divides
. (Contributed by NM, 3Oct2008.)



Theorem  zextle 8389* 
An extensionalitylike property for integer ordering. (Contributed by
NM, 29Oct2005.)



Theorem  zextlt 8390* 
An extensionalitylike property for integer ordering. (Contributed by
NM, 29Oct2005.)



Theorem  recnz 8391 
The reciprocal of a number greater than 1 is not an integer. (Contributed
by NM, 3May2005.)



Theorem  btwnnz 8392 
A number between an integer and its successor is not an integer.
(Contributed by NM, 3May2005.)



Theorem  gtndiv 8393 
A larger number does not divide a smaller positive integer. (Contributed
by NM, 3May2005.)



Theorem  halfnz 8394 
Onehalf is not an integer. (Contributed by NM, 31Jul2004.)



Theorem  3halfnz 8395 
Three halves is not an integer. (Contributed by AV, 2Jun2020.)



Theorem  prime 8396* 
Two ways to express " is a prime number (or 1)." (Contributed by
NM, 4May2005.)



Theorem  msqznn 8397 
The square of a nonzero integer is a positive integer. (Contributed by
NM, 2Aug2004.)



Theorem  zneo 8398 
No even integer equals an odd integer (i.e. no integer can be both even
and odd). Exercise 10(a) of [Apostol] p.
28. (Contributed by NM,
31Jul2004.) (Proof shortened by Mario Carneiro, 18May2014.)



Theorem  nneoor 8399 
A positive integer is even or odd. (Contributed by Jim Kingdon,
15Mar2020.)



Theorem  nneo 8400 
A positive integer is even or odd but not both. (Contributed by NM,
1Jan2006.) (Proof shortened by Mario Carneiro, 18May2014.)

