Type  Label  Description 
Statement 

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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  nn0n0n1ge2 8047 
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 8048* 
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 8049 
Alternative definition of the integers, based on elz2 8048.
(Contributed
by Mario Carneiro, 16May2014.)



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



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

# 

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

DECID


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

DECID 

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

DECID 

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



Theorem  nn0n0n1ge2b 8056 
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 8057 
A nonnegative integer less than is .
(Contributed by Paul
Chapman, 22Jun2011.)



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



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



Theorem  zneo 8075 
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 8076 
A positive integer is even or odd. (Contributed by Jim Kingdon,
15Mar2020.)



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



Theorem  nneoi 8078 
A positive integer is even or odd but not both. (Contributed by NM,
20Aug2001.)



Theorem  zeo 8079 
An integer is even or odd. (Contributed by NM, 1Jan2006.)



Theorem  zeo2 8080 
An integer is even or odd but not both. (Contributed by Mario Carneiro,
12Sep2015.)



Theorem  peano2uz2 8081* 
Second Peano postulate for upper integers. (Contributed by NM,
3Oct2004.)



Theorem  peano5uzti 8082* 
Peano's inductive postulate for upper integers. (Contributed by NM,
6Jul2005.) (Revised by Mario Carneiro, 25Jul2013.)



Theorem  peano5uzi 8083* 
Peano's inductive postulate for upper integers. (Contributed by NM,
6Jul2005.) (Revised by Mario Carneiro, 3May2014.)



Theorem  dfuzi 8084* 
An expression for the upper integers that start at that is
analogous to dfnn2 7657 for positive integers. (Contributed by NM,
6Jul2005.) (Proof shortened by Mario Carneiro, 3May2014.)



Theorem  uzind 8085* 
Induction on the upper integers that start at . The first four
hypotheses give us the substitution instances we need; the last two are
the basis and the induction step. (Contributed by NM, 5Jul2005.)



Theorem  uzind2 8086* 
Induction on the upper integers that start after an integer .
The first four hypotheses give us the substitution instances we need;
the last two are the basis and the induction step. (Contributed by NM,
25Jul2005.)



Theorem  uzind3 8087* 
Induction on the upper integers that start at an integer . The
first four hypotheses give us the substitution instances we need, and
the last two are the basis and the induction step. (Contributed by NM,
26Jul2005.)



Theorem  nn0ind 8088* 
Principle of Mathematical Induction (inference schema) on nonnegative
integers. The first four hypotheses give us the substitution instances
we need; the last two are the basis and the induction step.
(Contributed by NM, 13May2004.)



Theorem  fzind 8089* 
Induction on the integers from to
inclusive . The first
four hypotheses give us the substitution instances we need; the last two
are the basis and the induction step. (Contributed by Paul Chapman,
31Mar2011.)



Theorem  fnn0ind 8090* 
Induction on the integers from to
inclusive . The first
four hypotheses give us the substitution instances we need; the last two
are the basis and the induction step. (Contributed by Paul Chapman,
31Mar2011.)



Theorem  nn0indraph 8091* 
Principle of Mathematical Induction (inference schema) on nonnegative
integers. The first four hypotheses give us the substitution instances
we need; the last two are the basis and the induction step. Raph Levien
remarks: "This seems a bit painful. I wonder if an explicit
substitution version would be easier." (Contributed by Raph
Levien,
10Apr2004.)



Theorem  zindd 8092* 
Principle of Mathematical Induction on all integers, deduction version.
The first five hypotheses give the substitutions; the last three are the
basis, the induction, and the extension to negative numbers.
(Contributed by Paul Chapman, 17Apr2009.) (Proof shortened by Mario
Carneiro, 4Jan2017.)



Theorem  btwnz 8093* 
Any real number can be sandwiched between two integers. Exercise 2 of
[Apostol] p. 28. (Contributed by NM,
10Nov2004.)



Theorem  nn0zd 8094 
A positive integer is an integer. (Contributed by Mario Carneiro,
28May2016.)



Theorem  nnzd 8095 
A nonnegative integer is an integer. (Contributed by Mario Carneiro,
28May2016.)



Theorem  zred 8096 
An integer is a real number. (Contributed by Mario Carneiro,
28May2016.)



Theorem  zcnd 8097 
An integer is a complex number. (Contributed by Mario Carneiro,
28May2016.)



Theorem  znegcld 8098 
Closure law for negative integers. (Contributed by Mario Carneiro,
28May2016.)



Theorem  peano2zd 8099 
Deduction from second Peano postulate generalized to integers.
(Contributed by Mario Carneiro, 28May2016.)



Theorem  zaddcld 8100 
Closure of addition of integers. (Contributed by Mario Carneiro,
28May2016.)

